Simon Génier pushed to branch there-can-be-only-one-inductive at Stefan / Typer
Commits: 108d4679 by Simon Génier at 2020-12-08T15:47:35-05:00 Remove arguments to inductive types.
There used to be two ways to express indexed types: one could either add parameters directly on the type or put the type behind a lambda. These two are semantically equivalent, so we unify them into the latter in this patch.
- - - - -
9 changed files:
- btl/builtins.typer - + btl/empty.typer - src/elab.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml - + tests/opslexp_test.ml
Changes:
===================================== btl/builtins.typer ===================================== @@ -192,288 +192,292 @@ Sexp_debug_print = Built-in "Sexp.debug_print" : Sexp -> IO Sexp; %% -----------------------------------------------------
%% FIXME: "List : ?" should be sufficient but triggers -List : Type_ ?ℓ -> Type_ ?ℓ; %% List a = typecons List (nil) (cons a (List a)); %% nil = lambda a ≡> datacons (List a) nil; %% cons = lambda a ≡> datacons (List a) cons; -List = typecons (List (ℓ ::: TypeLevel) (a : Type_ ℓ)) (nil) (cons a (List a)); -nil = datacons List nil; -cons = datacons List cons; +List : (ℓ : TypeLevel) ≡> Type_ ℓ -> Type_ ℓ; +List = lambda ℓ ≡> lambda α -> typecons List (nil) (cons α (List (ℓ := ℓ) α)); +nil : (ℓ : TypeLevel) ≡> (α : Type_ ℓ) ≡> List (ℓ := ℓ) α; +nil = lambda ℓ ≡> lambda α ≡> datacons (List α) nil; +cons : (ℓ : TypeLevel) ≡> (α : Type_ ℓ) ≡> α -> List (ℓ := ℓ) α -> List (ℓ := ℓ) α; +cons = lambda ℓ ≡> lambda α ≡> datacons (List α) cons;
-%%%% Macro-related definitions +% %%%% Macro-related definitions + +Sexp_node : Sexp -> List Sexp -> Sexp; +Sexp_node = Built-in "Sexp.node";
Sexp_block = Built-in "Sexp.block" : String -> Sexp; Sexp_symbol = Built-in "Sexp.symbol" : String -> Sexp; Sexp_string = Built-in "Sexp.string" : String -> Sexp; -Sexp_node = Built-in "Sexp.node" : Sexp -> List Sexp -> Sexp; Sexp_integer = Built-in "Sexp.integer" : Integer -> Sexp; Sexp_float = Built-in "Sexp.float" : Float -> Sexp;
-Macro = typecons (Macro) - (macro (List Sexp -> IO Sexp)); -macro = datacons Macro macro; - -Macro_expand : Macro -> List Sexp -> IO Sexp; -Macro_expand = lambda m -> lambda args -> case m - | macro f => f args; - -Sexp_dispatch : Sexp - -> (node : Sexp -> List Sexp -> ?a) - -> (symbol : String -> ?a) - -> (string : String -> ?a) - -> (int : Integer -> ?a) - -> (float : Float -> ?a) - -> (block : Sexp -> ?a) - -> ?a ; -Sexp_dispatch = Built-in "Sexp.dispatch"; - -%% -%% Parse a block using the grammar in the passed context -%% -Reader_parse = Built-in "Reader.parse" : Elab_Context -> Sexp -> List Sexp; - -%%%% Array (without IO, but they could be added easily) - -%% -%% Takes an index, a new value and an array -%% Returns a copy of the array with the element -%% at the specified index set to the new value -%% -%% Array_set is in O(N) where N is the length -%% -Array_set : Int -> ?a -> Array ?a -> Array ?a; -Array_set = Built-in "Array.set"; - -%% -%% Takes an element and an array -%% Returns a copy of the array with the new element at the end -%% -%% Array_append is in O(N) where N is the length -%% -Array_append : ?a -> Array ?a -> Array ?a; -Array_append = Built-in "Array.append"; - -%% -%% Takes an Int (n) and a value -%% Returns an array containing n times the value -%% -Array_create : Int -> ?a -> Array ?a; -Array_create = Built-in "Array.create"; - -%% -%% Takes an array -%% Returns the number of element in the array -%% -Array_length : Array ?a -> Int; -Array_length = Built-in "Array.length"; - -%% -%% Takes a default value, an index and an array -%% Returns the value in the array at the specified index or -%% the default value if the index is out of bounds -%% -Array_get : ?a -> Int -> Array ?a -> ?a; -Array_get = Built-in "Array.get"; - -%% -%% It returns an empty array -%% -%% let Typer deduce the value of (a : Type) -%% -Array_empty : Unit -> Array ?a; -Array_empty = Built-in "Array.empty"; - -%%%% Monads - -%% Builtin bind -IO_bind : IO ?a -> (?a -> IO ?b) -> IO ?b; -IO_bind = Built-in "IO.bind"; - -IO_return : ?a -> IO ?a; -IO_return = Built-in "IO.return"; - -%% `runIO` should have type IO Unit -> b -> b -%% or IO a -> b -> b, which means "run the IO, throw away the result, -%% and then return the second argument unchanged". The "dummy" b argument -%% is actually crucial to make sure the result of runIO is used, otherwise -%% the whole call would look like a dead function call and could be -%% optimized away! -IO_run : IO Unit -> ?a -> ?a; -IO_run = Built-in "IO.run"; - -%% File monad - -%% Define operations on file handle. -File_open = Built-in "File.open" : String -> String -> IO FileHandle; -File_stdout = Built-in "File.stdout" : Unit -> FileHandle; -File_write = Built-in "File.write" : FileHandle -> String -> IO Unit; -File_read = Built-in "File.read" : FileHandle -> Int -> IO String; - -Sys_cpu_time = Built-in "Sys.cpu_time" : Unit -> IO Float; -Sys_exit = Built-in "Sys.exit" : Int -> IO Unit; - -%% -%% Ref (modifiable value) -%% -%% Conceptualy: -%% Ref : Type -> Type; -%% Ref = typecons (Ref (a : Type)) (Ref a); -%% - -%% -%% Takes a value -%% Returns a value modifiable in the IO monad -%% and which already contain the specified value -%% -Ref_make : ?a -> IO (Ref ?a); -Ref_make = Built-in "Ref.make"; - -%% -%% Takes a Ref -%% Returns in the IO monad the value in the Ref -%% -Ref_read : Ref ?a -> IO ?a; -Ref_read = Built-in "Ref.read"; - -%% -%% Takes a value and a Ref -%% Returns the an empty command -%% and set the Ref to contain specified value -%% -Ref_write : ?a -> Ref ?a -> IO Unit; -Ref_write = Built-in "Ref.write"; - -%% -%% gensym for macro -%% -%% Generate pseudo-unique symbol -%% -%% At least they cannot be obtained outside macro. -%% In macro you should NOT use symbol of the form " %gensym% ...". -%% Assume the three dots to be anything. -%% -gensym = Built-in "gensym" : Unit -> IO Sexp; - -%%%% Function on Elab_Context - -%% -%% Get the current context of elaboration -%% -Elab_getenv = Built-in "Elab.getenv" : Unit -> IO Elab_Context; - -%% -%% Check if a symbol is defined in a particular context -%% -Elab_isbound = Built-in "Elab.isbound" : String -> Elab_Context -> Bool; - -%% -%% Check if a symbol is a constructor in a particular context -%% -Elab_isconstructor = Built-in "Elab.isconstructor" - : String -> Elab_Context -> Bool; - -%% -%% Check if the n'th field of a constructor is erasable -%% If the constructor isn't defined it will always return false -%% -Elab_is-nth-erasable = Built-in "Elab.is-nth-erasable" : String -> Int -> Elab_Context -> Bool; - -%% -%% Check if a field of a constructor is erasable -%% If the constructor or the field aren't defined it will always return false -%% -Elab_is-arg-erasable = Built-in "Elab.is-arg-erasable" : String -> String -> Elab_Context -> Bool; - -%% -%% Get n'th field of a constructor -%% It return "_" in case the field isn't defined -%% see pervasive.typer for a more convenient function -%% -Elab_nth-arg' = Built-in "Elab.nth-arg" : String -> Int -> Elab_Context -> String; - -%% -%% Get the position of a field in a constructor -%% It return -1 in case the field isn't defined -%% see pervasive.typer for a more convenient function -%% -Elab_arg-pos' = Built-in "Elab.arg-pos" : String -> String -> Elab_Context -> Int; - -%% -%% Get the docstring associated with a symbol -%% -Elab_debug-doc = Built-in "Elab.debug-doc" : String -> Elab_Context -> String; - -%%%% Unit test helper IO - -%% -%% Print message and/or fail (terminate) -%% And location is printed before the error -%% - -%% -%% Voluntarily fail -%% use case: next unit tests are not worth testing -%% -%% Takes a "section" and a "message" as argument -%% -Test_fatal = Built-in "Test.fatal" : String -> String -> IO Unit; - -%% -%% Throw a warning, very similar to `Test_info` -%% but it's possible to implement a parameter for user who want it to sometimes be fatal -%% -%% Takes a "section" and a "message" as argument -%% -Test_warning = Built-in "Test.warning" : String -> String -> IO Unit; - -%% -%% Just print a message with location of the call -%% -%% Takes a "section" and a "message" as argument -%% -Test_info = Built-in "Test.info" : String -> String -> IO Unit; - -%% -%% Get a string representing location of call ("file:line:column") -%% -Test_location = Built-in "Test.location" : Unit -> String; - -%% -%% Do some test which print a message: "[ OK]" or "[FAIL]" -%% followed by a message passed as argument -%% - -%% -%% Takes a message and a boolean which should be true -%% Returns true if the boolean was true -%% -Test_true = Built-in "Test.true" : String -> Bool -> IO Bool; - -%% -%% Takes a message and a boolean which should be false -%% Returns true if the boolean was false -%% -Test_false = Built-in "Test.false" : String -> Bool -> IO Bool; - -%% -%% Takes a message and two arbitrary value of the same type -%% Returns true when the two value are equal -%% -Test_eq : String -> ?a -> ?a -> IO Bool; -Test_eq = Built-in "Test.eq"; - -%% -%% Takes a message and two arbitrary value of the same type -%% Returns true when the two value are not equal -%% -Test_neq : String -> ?a -> ?a -> IO Bool; -Test_neq = Built-in "Test.neq"; - -%% -%% Given a string, return an opaque DataconsLabel that identifies a data -%% constructor. -%% -datacons-label<-string : String -> ##DataconsLabel; -datacons-label<-string = Built-in "datacons-label<-string"; - -%%% builtins.typer ends here. +% Macro = typecons (Macro) +% (macro (List Sexp -> IO Sexp)); +% macro = datacons Macro macro; + +% Macro_expand : Macro -> List Sexp -> IO Sexp; +% Macro_expand = lambda m -> lambda args -> case m +% | macro f => f args; + +% Sexp_dispatch : Sexp +% -> (node : Sexp -> List Sexp -> ?a) +% -> (symbol : String -> ?a) +% -> (string : String -> ?a) +% -> (int : Integer -> ?a) +% -> (float : Float -> ?a) +% -> (block : Sexp -> ?a) +% -> ?a ; +% Sexp_dispatch = Built-in "Sexp.dispatch"; + +% %% +% %% Parse a block using the grammar in the passed context +% %% +% Reader_parse = Built-in "Reader.parse" : Elab_Context -> Sexp -> List Sexp; + +% %%%% Array (without IO, but they could be added easily) + +% %% +% %% Takes an index, a new value and an array +% %% Returns a copy of the array with the element +% %% at the specified index set to the new value +% %% +% %% Array_set is in O(N) where N is the length +% %% +% Array_set : Int -> ?a -> Array ?a -> Array ?a; +% Array_set = Built-in "Array.set"; + +% %% +% %% Takes an element and an array +% %% Returns a copy of the array with the new element at the end +% %% +% %% Array_append is in O(N) where N is the length +% %% +% Array_append : ?a -> Array ?a -> Array ?a; +% Array_append = Built-in "Array.append"; + +% %% +% %% Takes an Int (n) and a value +% %% Returns an array containing n times the value +% %% +% Array_create : Int -> ?a -> Array ?a; +% Array_create = Built-in "Array.create"; + +% %% +% %% Takes an array +% %% Returns the number of element in the array +% %% +% Array_length : Array ?a -> Int; +% Array_length = Built-in "Array.length"; + +% %% +% %% Takes a default value, an index and an array +% %% Returns the value in the array at the specified index or +% %% the default value if the index is out of bounds +% %% +% Array_get : ?a -> Int -> Array ?a -> ?a; +% Array_get = Built-in "Array.get"; + +% %% +% %% It returns an empty array +% %% +% %% let Typer deduce the value of (a : Type) +% %% +% Array_empty : Unit -> Array ?a; +% Array_empty = Built-in "Array.empty"; + +% %%%% Monads + +% %% Builtin bind +% IO_bind : IO ?a -> (?a -> IO ?b) -> IO ?b; +% IO_bind = Built-in "IO.bind"; + +% IO_return : ?a -> IO ?a; +% IO_return = Built-in "IO.return"; + +% %% `runIO` should have type IO Unit -> b -> b +% %% or IO a -> b -> b, which means "run the IO, throw away the result, +% %% and then return the second argument unchanged". The "dummy" b argument +% %% is actually crucial to make sure the result of runIO is used, otherwise +% %% the whole call would look like a dead function call and could be +% %% optimized away! +% IO_run : IO Unit -> ?a -> ?a; +% IO_run = Built-in "IO.run"; + +% %% File monad + +% %% Define operations on file handle. +% File_open = Built-in "File.open" : String -> String -> IO FileHandle; +% File_stdout = Built-in "File.stdout" : Unit -> FileHandle; +% File_write = Built-in "File.write" : FileHandle -> String -> IO Unit; +% File_read = Built-in "File.read" : FileHandle -> Int -> IO String; + +% Sys_cpu_time = Built-in "Sys.cpu_time" : Unit -> IO Float; +% Sys_exit = Built-in "Sys.exit" : Int -> IO Unit; + +% %% +% %% Ref (modifiable value) +% %% +% %% Conceptualy: +% %% Ref : Type -> Type; +% %% Ref = typecons (Ref (a : Type)) (Ref a); +% %% + +% %% +% %% Takes a value +% %% Returns a value modifiable in the IO monad +% %% and which already contain the specified value +% %% +% Ref_make : ?a -> IO (Ref ?a); +% Ref_make = Built-in "Ref.make"; + +% %% +% %% Takes a Ref +% %% Returns in the IO monad the value in the Ref +% %% +% Ref_read : Ref ?a -> IO ?a; +% Ref_read = Built-in "Ref.read"; + +% %% +% %% Takes a value and a Ref +% %% Returns the an empty command +% %% and set the Ref to contain specified value +% %% +% Ref_write : ?a -> Ref ?a -> IO Unit; +% Ref_write = Built-in "Ref.write"; + +% %% +% %% gensym for macro +% %% +% %% Generate pseudo-unique symbol +% %% +% %% At least they cannot be obtained outside macro. +% %% In macro you should NOT use symbol of the form " %gensym% ...". +% %% Assume the three dots to be anything. +% %% +% gensym = Built-in "gensym" : Unit -> IO Sexp; + +% %%%% Function on Elab_Context + +% %% +% %% Get the current context of elaboration +% %% +% Elab_getenv = Built-in "Elab.getenv" : Unit -> IO Elab_Context; + +% %% +% %% Check if a symbol is defined in a particular context +% %% +% Elab_isbound = Built-in "Elab.isbound" : String -> Elab_Context -> Bool; + +% %% +% %% Check if a symbol is a constructor in a particular context +% %% +% Elab_isconstructor = Built-in "Elab.isconstructor" +% : String -> Elab_Context -> Bool; + +% %% +% %% Check if the n'th field of a constructor is erasable +% %% If the constructor isn't defined it will always return false +% %% +% Elab_is-nth-erasable = Built-in "Elab.is-nth-erasable" : String -> Int -> Elab_Context -> Bool; + +% %% +% %% Check if a field of a constructor is erasable +% %% If the constructor or the field aren't defined it will always return false +% %% +% Elab_is-arg-erasable = Built-in "Elab.is-arg-erasable" : String -> String -> Elab_Context -> Bool; + +% %% +% %% Get n'th field of a constructor +% %% It return "_" in case the field isn't defined +% %% see pervasive.typer for a more convenient function +% %% +% Elab_nth-arg' = Built-in "Elab.nth-arg" : String -> Int -> Elab_Context -> String; + +% %% +% %% Get the position of a field in a constructor +% %% It return -1 in case the field isn't defined +% %% see pervasive.typer for a more convenient function +% %% +% Elab_arg-pos' = Built-in "Elab.arg-pos" : String -> String -> Elab_Context -> Int; + +% %% +% %% Get the docstring associated with a symbol +% %% +% Elab_debug-doc = Built-in "Elab.debug-doc" : String -> Elab_Context -> String; + +% %%%% Unit test helper IO + +% %% +% %% Print message and/or fail (terminate) +% %% And location is printed before the error +% %% + +% %% +% %% Voluntarily fail +% %% use case: next unit tests are not worth testing +% %% +% %% Takes a "section" and a "message" as argument +% %% +% Test_fatal = Built-in "Test.fatal" : String -> String -> IO Unit; + +% %% +% %% Throw a warning, very similar to `Test_info` +% %% but it's possible to implement a parameter for user who want it to sometimes be fatal +% %% +% %% Takes a "section" and a "message" as argument +% %% +% Test_warning = Built-in "Test.warning" : String -> String -> IO Unit; + +% %% +% %% Just print a message with location of the call +% %% +% %% Takes a "section" and a "message" as argument +% %% +% Test_info = Built-in "Test.info" : String -> String -> IO Unit; + +% %% +% %% Get a string representing location of call ("file:line:column") +% %% +% Test_location = Built-in "Test.location" : Unit -> String; + +% %% +% %% Do some test which print a message: "[ OK]" or "[FAIL]" +% %% followed by a message passed as argument +% %% + +% %% +% %% Takes a message and a boolean which should be true +% %% Returns true if the boolean was true +% %% +% Test_true = Built-in "Test.true" : String -> Bool -> IO Bool; + +% %% +% %% Takes a message and a boolean which should be false +% %% Returns true if the boolean was false +% %% +% Test_false = Built-in "Test.false" : String -> Bool -> IO Bool; + +% %% +% %% Takes a message and two arbitrary value of the same type +% %% Returns true when the two value are equal +% %% +% Test_eq : String -> ?a -> ?a -> IO Bool; +% Test_eq = Built-in "Test.eq"; + +% %% +% %% Takes a message and two arbitrary value of the same type +% %% Returns true when the two value are not equal +% %% +% Test_neq : String -> ?a -> ?a -> IO Bool; +% Test_neq = Built-in "Test.neq"; + +% %% +% %% Given a string, return an opaque DataconsLabel that identifies a data +% %% constructor. +% %% +% datacons-label<-string : String -> ##DataconsLabel; +% datacons-label<-string = Built-in "datacons-label<-string"; + +% %%% builtins.typer ends here.
===================================== btl/empty.typer =====================================
===================================== src/elab.ml ===================================== @@ -158,6 +158,16 @@ let elab_check_proper_type (ctx : elab_context) ltp var = raise e
let elab_check_def (ctx : elab_context) var lxp ltype = + let () = print_endline "elab_check_def" in + let () = print_endline ("\tvar: " ^ get_vname_name var) in + let () = print_endline ("\tlxp: " ^ lexp_string lxp) in + let () = + match lxp with + | Builtin (_, lbuiltin_type), _ -> + print_endline ("\tlbuiltin_type: " ^ lexp_string lbuiltin_type) + | _ -> () + in + let () = print_endline ("\ttype: " ^ lexp_string ltype) in let lctx = ectx_to_lctx ctx in let loc = lexp_location lxp in
@@ -204,19 +214,23 @@ let ctx_define (ctx: elab_context) var lxp ltype = ectx_extend ctx var (LetDef (0, lxp)) ltype
let ctx_define_rec (ctx: elab_context) decls = + let () = print_endline ("ctx_define_rec: start") in let nctx = ectx_extend_rec ctx decls in + let () = print_endline ("ctx_define_rec: extented") in let _ = List.fold_left (fun n (var, lxp, ltp) -> elab_check_proper_type nctx (push_susp ltp (S.shift n)) var; n - 1) (List.length decls) decls in + let () = print_endline ("ctx_define_rec: proper types checked") in let _ = List.fold_left (fun n (var, lxp, ltp) -> elab_check_def nctx var lxp (push_susp ltp (S.shift n)); n - 1) (List.length decls) decls in + let () = print_endline ("ctx_define_rec: done") in nctx
(* The main job of lexp (currently) is to determine variable name (index) @@ -443,28 +457,22 @@ let rec meta_to_var ids (e : lexp) = -> mkLambda (ak, v, loop o t, loop (1 + o) e) | Call (f, args) -> mkCall (loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args) - | Inductive (l, label, args, cases) - -> let alen = List.length args in - let (_, nargs) - = List.fold_right (fun (ak, v, t) (o', args) - -> let o' = o' - 1 in - (o', (ak, v, loop (o' + o) t) - :: args)) - args (alen, []) in - let ncases - = SMap.map - (fun fields - -> let flen = List.length fields in - let (_, nfields) - = List.fold_right - (fun (ak, v, t) (o', fields) - -> let o' = o' - 1 in - (o', (ak, v, loop (o' + o) t) - :: fields)) - fields (flen + alen, []) in - nfields) - cases in - mkInductive (l, label, nargs, ncases) + | Inductive (l, ((_, name) as label), cases) + -> let () = print_endline ("meta_to_var: Inductive " ^ name) in + let ncases + = SMap.map + (fun fields + -> let flen = List.length fields in + let (_, nfields) + = List.fold_right + (fun (ak, v, t) (o', fields) + -> let o' = o' - 1 in + (o', (ak, v, loop (o' + o) t) + :: fields)) + fields (flen, []) in + nfields) + cases in + mkInductive (l, label, ncases) | Cons (t, l) -> mkCons (loop o t, l) | Case (l, e, t, cases, default) -> let ncases @@ -753,37 +761,27 @@ and check_case rtype (loc, target, ppatterns) ctx = -> unify_ind it it'; (cs, args) | None -> match OL.lexp'_whnf it' (ectx_to_lctx ctx) with - | Inductive (_, _, fargs, constructors) - -> let (s, targs) = List.fold_left - (fun (s, targs) (ak, name, t) - -> let arg = newMetavar - (ectx_to_lctx ctx) - (ectx_to_scope_level ctx) - name (mkSusp t s) in - (S.cons arg s, (ak, arg) :: targs)) - (S.identity, []) - fargs in - let (cs, args) = (constructors, List.rev targs) in - ltarget := check_inferred ctx tlxp tltp (mkCall (it', args)); - it_cs_as := Some (it', cs, args); - (cs, args) - | _ -> let call_split e = - match OL.lexp'_whnf e (ectx_to_lctx ctx) with - | Call (f, args) -> (f, args) - | _ -> (e,[]) in - let (it, targs) = call_split tltp in - unify_ind it it'; - let constructors = - match OL.lexp'_whnf it (ectx_to_lctx ctx) with - | Inductive (_, _, fargs, constructors) - -> assert (List.length fargs = List.length targs); - constructors - | _ -> lexp_error (sexp_location target) tlxp - ("Can't `case` on objects of this type: " - ^ lexp_string tltp); - SMap.empty in - it_cs_as := Some (it, constructors, targs); - (constructors, targs) in + | Inductive (_, _, constructors) + -> ltarget := check_inferred ctx tlxp tltp (mkCall (it', [])); + it_cs_as := Some (it', constructors, []); + (constructors, []) + | _ -> let call_split e = + match OL.lexp'_whnf e (ectx_to_lctx ctx) with + | Call (f, args) -> (f, args) + | _ -> (e, []) in + let (it, targs) = call_split tltp in + unify_ind it it'; + let constructors = + match OL.lexp'_whnf it (ectx_to_lctx ctx) with + | Inductive (_, _, constructors) + -> assert (List.length targs == 0); + constructors + | _ -> lexp_error (sexp_location target) tlxp + ("Can't `case` on objects of this type: " + ^ lexp_string tltp); + SMap.empty in + it_cs_as := Some (it, constructors, targs); + (constructors, targs) in
(* Read patterns one by one *) let fold_fun (lbranches, dflt) (pat, pexp) = @@ -1156,15 +1154,20 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) match Myers.nth i (ectx_to_lctx nctx) with | (v', ForwardRef, t) -> let adjusted_t = push_susp t (S.shift (i + 1)) in + let () = print_endline ("CHECKING: " ^ vname ^ " : " ^ lexp_string adjusted_t) in let e = check pexp adjusted_t nctx in let (grm, ec, lc, sl) = nctx in let d = (v', LetDef (i + 1, e), t) in - (IMap.add i ((l, Some vname), e, t) map, - (grm, ec, Myers.set_nth i d lc, sl)) + let res = (IMap.add i ((l, Some vname), e, t) map, + (grm, ec, Myers.set_nth i d lc, sl)) in + res | _ -> Log.internal_error "Defining same slot!") defs (IMap.empty, nctx) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in - decls, ctx_define_rec ectx decls + let () = print_endline ("BEFORE: ctx_define_rec") in + let res = decls, ctx_define_rec ectx decls in + let () = print_endline ("AFTER: ctx_define_rec") in + res
and infer_and_generalize_type (ctx : elab_context) se name = let nctx = ectx_new_scope ctx in @@ -1312,6 +1315,7 @@ and lexp_decls_1 let pending_defs = ((v, sexp) :: pending_defs) in if SMap.is_empty pending_decls then let nctx = ectx_new_scope nctx in + let () = print_endline ("CHECKING: " ^ String.concat " " (List.map (fun x -> snd (fst x)) pending_defs)) in let decls, nctx = lexp_check_decls ectx nctx pending_defs in decls, sdecls, toks, nctx else @@ -1408,11 +1412,11 @@ let sform_built_in ctx loc sargs ot = * performance of type-inference (at least until we have proper * memoization of push_susp and/or whnf). *) -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in - let bi = mkBuiltin ((loc, name), ltp') in - if not (SMap.mem name (!EV.builtin_functions)) then - sexp_error loc ("Unknown built-in `" ^ name ^ "`"); - BI.add_builtin_cst name bi; - (bi, Checked) + let bi = mkBuiltin ((loc, name), ltp') in + if not (SMap.mem name (!EV.builtin_functions)) then + sexp_error loc ("Unknown built-in `" ^ name ^ "`"); + BI.add_builtin_cst name bi; + (bi, Checked) | None -> error ~loc "Built-in's type not provided by context!"; sform_dummy_ret ctx loc)
@@ -1463,7 +1467,7 @@ let sform_typecons ctx loc sargs ot = -> let (label, formals) = match formals with | Node (label, formals) -> (label, formals) | _ -> (formals, []) in - let label = match label with + let (_, name) as label = match label with | Symbol label -> label | _ -> let loc = sexp_location label in sexp_error loc "Unrecognized inductive type name"; @@ -1495,12 +1499,12 @@ let sform_typecons ctx loc sargs ot = | Symbol s -> (s, [])::pcases
| _ -> sexp_error (sexp_location case) - "Unrecognized constructor declaration"; + "Unrecognized constructor declaration"; pcases) constrs [] in
let map_ctor = lexp_parse_inductive ctors nctx in - (mkInductive (loc, label, formals, map_ctor), Lazy) + mkInductive (loc, label, map_ctor), Lazy
let sform_hastype ctx loc sargs ot = match sargs with @@ -1906,7 +1910,7 @@ let default_ectx
builtin_size := get_size lctx; let ectx = dynamic_bind in_pervasive true - (fun () -> read_file (btl_folder ^ "/pervasive.typer") lctx) in + (fun () -> read_file (btl_folder ^ "/empty.typer") lctx) in let _ = sform_default_ectx := ectx in ectx with e ->
===================================== src/eval.ml ===================================== @@ -812,14 +812,18 @@ let erasable_p name nth ectx = | (k, _, _) -> k = Aerasable ) else false | _ -> false in - try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with - | Cons (e, _) when is_var e - -> (match (env_lookup_expr ectx (get_var e)) with - | Some i when is_inductive i - -> is_erasable (get_inductive_ctor (get_inductive i)) - | _ -> false) - | _ -> false + try + let idx = senv_lookup name ectx in + match + OL.lexp'_whnf + (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) + with + | Cons (e, _) when is_var e + -> (match (env_lookup_expr ectx (get_var e)) with + | Some (Inductive (_, _, constructors), _) -> is_erasable constructors + | _ -> false) + | _ -> false with Senv_Lookup_Fail _ -> false
let erasable_p2 t name ectx = @@ -833,14 +837,18 @@ let erasable_p2 t name ectx = | _ -> false) args) | _ -> false in - try let idx = senv_lookup t ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some t), idx)) (ectx_to_lctx ectx) with - | Cons (e, _) when is_var e - -> (match (env_lookup_expr ectx (get_var e)) with - | Some i when is_inductive i - -> is_erasable (get_inductive_ctor (get_inductive i)) - | _ -> false) - | _ -> false + try + let idx = senv_lookup t ectx in + match + OL.lexp'_whnf + (mkVar ((dummy_location, Some t), idx)) + (ectx_to_lctx ectx) + with + | Cons (e, _) when is_var e + -> (match env_lookup_expr ectx (get_var e) with + | Some (Inductive (_, _, constructors), _) -> is_erasable constructors + | _ -> false) + | _ -> false with Senv_Lookup_Fail _ -> false
let nth_ctor_arg name nth ectx = @@ -851,14 +859,18 @@ let nth_ctor_arg name nth ectx = | _ -> "_" | exception (Failure _) -> "_" ) | _ -> "_" in - try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with - | Cons (e, _) when is_var e - -> (match (env_lookup_expr ectx (get_var e)) with - | Some i when is_inductive i - -> find_nth (get_inductive_ctor (get_inductive i)) - | _ -> "_") - | _ -> "_" + try + let idx = senv_lookup name ectx in + match + OL.lexp'_whnf + (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) + with + | Cons (e, _) when is_var e + -> (match (env_lookup_expr ectx (get_var e)) with + | Some (Inductive (_, _, constructors), _) -> find_nth constructors + | _ -> "_") + | _ -> "_" with Senv_Lookup_Fail _ -> "_"
let ctor_arg_pos name arg ectx = @@ -872,14 +884,18 @@ let ctor_arg_pos name arg ectx = | None -> (-1) | Some n -> n ) | _ -> (-1) in - try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with - | Cons (e, _) when is_var e - -> (match (env_lookup_expr ectx (get_var e)) with - | Some i when is_inductive i - -> find_arg (get_inductive_ctor (get_inductive i)) - | _ -> (-1)) - | _ -> (-1) + try + let idx = senv_lookup name ectx in + match + OL.lexp'_whnf + (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) + with + | Cons (e, _) when is_var e + -> (match (env_lookup_expr ectx (get_var e)) with + | Some (Inductive (_, _, constructors), _) -> find_arg constructors + | _ -> (-1)) + | _ -> (-1) with Senv_Lookup_Fail _ -> (-1)
let is_constructor loc depth args_val = match args_val with
===================================== src/inverse_subst.ml ===================================== @@ -281,22 +281,18 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = | Call (f, args) -> mkCall (apply_inv_subst f s, L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s)) args) - | Inductive (l, label, args, cases) - -> let (s, nargs) - = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, (ak, v, apply_inv_subst t s) :: nargs)) - (s, []) args in - let nargs = List.rev nargs in - let ncases = SMap.map (fun args - -> let (_, ncase) - = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, - (ak, v, apply_inv_subst t s) - :: nargs)) - (s, []) args in - L.rev ncase) - cases in - mkInductive (l, label, nargs, ncases) + | Inductive (l, label, cases) + -> let inv_subst_case args = + let (_, ncase) = + L.fold_left (fun (s, nargs) (ak, v, t) + -> (ssink v s, + (ak, v, apply_inv_subst t s) + :: nargs)) + (s, []) args + in + L.rev ncase + in + mkInductive (l, label, SMap.map inv_subst_case cases) | Cons (it, name) -> mkCons (apply_inv_subst it s, name) | Case (l, e, ret, cases, default) -> mkCase (l, apply_inv_subst e s, apply_inv_subst ret s,
===================================== src/lexp.ml ===================================== @@ -37,7 +37,7 @@ module S = Subst type vname = U.vname type vref = U.vref type meta_id = int (* Identifier of a meta variable. *) - +type location = U.location type label = symbol
(*************** Elaboration to Lexp *********************) @@ -55,9 +55,11 @@ type label = symbol * And the type of the 3rd binding is defined in the scope of the * surrounded context extended with the first and the second bindings. *)
+ type ltype = lexp and subst = lexp S.subst (* Here we want a pair of `Lexp` and its hash value to avoid re-hashing "sub-Lexp". *) + and inductive = location * label * ((arg_kind * vname * ltype) list) SMap.t and lexp = lexp' * int and lexp' = | Imm of sexp (* Used for strings, ... *) @@ -71,9 +73,7 @@ type ltype = lexp | Arrow of arg_kind * vname * ltype * U.location * ltype | Lambda of arg_kind * vname * ltype * lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) - | Inductive of U.location * label - * ((arg_kind * vname * ltype) list) (* formal Args *) - * ((arg_kind * vname * ltype) list) SMap.t + | Inductive of inductive | Cons of lexp * symbol (* = Type info * ctor_name *) | Case of U.location * lexp * ltype (* The type of the return value of all branches *) @@ -213,15 +213,10 @@ let lexp'_hash (lp : lexp') = -> U.combine_hash 8 (U.combine_hash (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) (U.combine_hash (lexp_hash t) (lexp_hash e))) - | Inductive (l, n, a, cs) + | Inductive (l, n, cs) -> U.combine_hash 9 (U.combine_hash (U.combine_hash (Hashtbl.hash l) (Hashtbl.hash n)) - (U.combine_hash (U.combine_hashes - (List.map (fun e -> let (ak, n, lt) = e in - (U.combine_hash (Hashtbl.hash ak) - (U.combine_hash (Hashtbl.hash n) (lexp_hash lt)))) - a)) - (Hashtbl.hash cs))) + (Hashtbl.hash cs)) | Cons (t, n) -> U.combine_hash 10 (U.combine_hash (lexp_hash t) (Hashtbl.hash n)) | Case (l, e, rt, bs, d) -> U.combine_hash 11 (U.combine_hash @@ -242,6 +237,9 @@ let lexp'_hash (lp : lexp') = | Susp (lp, subst) -> U.combine_hash 14 (U.combine_hash (lexp_hash lp) (Hashtbl.hash subst))
+let datacons_equal (ak1, _, e1) (ak2, _, e2) = + ak1 = ak2 && e1 == e2 + (* Equality function for hash table * using physical equality for "sub-lexp" and compare for `subst`. *) let hc_eq e1 e2 = @@ -270,11 +268,8 @@ let hc_eq e1 e2 = | (Call (e1, as1), Call (e2, as2)) -> e1 == e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && e1 == e2) as1 as2 - | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) - -> l1 = l2 && List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && e1 == e2) as1 as2 - && SMap.equal (List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && e1 == e2)) ctor1 ctor2 + | (Inductive (_, l1, ctor1), Inductive (_, l2, ctor2)) + -> l1 = l2 && SMap.equal (List.for_all2 datacons_equal) ctor1 ctor2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> t1 == t2 && l1 = l2 | (Case (_, e1, r1, ctor1, def1), Case (_, e2, r2, ctor2, def2)) -> e1 == e2 && r1 == r2 && SMap.equal @@ -300,18 +295,18 @@ let hc_table : WHC.t = WHC.create 1000 let hc (l : lexp') : lexp = WHC.merge hc_table (l, lexp'_hash l)
-let mkImm s = hc (Imm s) -let mkSortLevel l = hc (SortLevel l) -let mkSort (l, s) = hc (Sort (l, s)) -let mkBuiltin (v, t) = hc (Builtin (v, t)) -let mkVar v = hc (Var v) -let mkLet (l, ds, e) = hc (Let (l, ds, e)) -let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) -let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) -let mkInductive (l, n, a, cs) = hc (Inductive (l, n, a, cs)) -let mkCons (t, n) = hc (Cons (t, n)) -let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) -let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) +let mkImm s = hc (Imm s) +let mkSortLevel l = hc (SortLevel l) +let mkSort (l, s) = hc (Sort (l, s)) +let mkBuiltin (v, t) = hc (Builtin (v, t)) +let mkVar v = hc (Var v) +let mkLet (l, ds, e) = hc (Let (l, ds, e)) +let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) +let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) +let mkInductive (l, n, cs) = hc (Inductive (l, n, cs)) +let mkCons (t, n) = hc (Cons (t, n)) +let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) +let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) let mkCall (f, es) = match lexp_lexp' f, es with | Call (f', es'), _ -> hc (Call (f', es' @ es)) @@ -385,21 +380,16 @@ let get_var_db_index v = let get_var_vname v = let (n, idx) = v in n
-let pred_inductive l pred = +let pred_inductive l (pred : inductive -> bool) = match lexp_lexp' l with - | Inductive (l, n, a, cs) -> pred (l, n, a, cs) - | _ -> false + | Inductive inductive -> pred inductive + | _ -> false
let get_inductive l = match lexp_lexp' l with - | Inductive (l, n, a, cs) -> (l, n, a, cs) + | Inductive (l, n, cs) -> (l, n, cs) | _ -> Log.log_fatal ~section:"internal" "Lexp is not Inductive "
-let get_inductive_ctor i = - let (l, n, a, cs) = i in cs - -let is_inductive l = pred_inductive l (fun e -> true) - (********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. * Maybe it would be cleaner to just move subst.ml into lexp.ml @@ -510,7 +500,7 @@ let rec lexp_location e = | Arrow (_,_,_,l,_) -> l | Lambda (_,(l,_),_,_) -> l | Call (f,_) -> lexp_location f - | Inductive (l,_,_,_) -> l + | Inductive (l,_,_) -> l | Cons (_,(l,_)) -> l | Case (l,_,_,_,_) -> l | Susp (e, _) -> lexp_location e @@ -547,21 +537,17 @@ let rec push_susp e s = (* Push a suspension one level down. *) | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s, mkSusp e (ssink v s)) | Call (f, args) -> mkCall (mkSusp f s, L.map (fun (ak, arg) -> (ak, mkSusp arg s)) args) - | Inductive (l, label, args, cases) - -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, (ak, v, mkSusp t s) :: nargs)) - (s, []) args in - let nargs = List.rev nargs in - let ncases = SMap.map (fun args - -> let (_, ncase) - = L.fold_left (fun (s, nargs) (ak, v, t) + | Inductive (l, label, cases) + -> let ncases = SMap.map (fun args + -> let (_, ncase) + = L.fold_left (fun (s, nargs) (ak, v, t) -> (ssink v s, - (ak, v, mkSusp t s) + (ak, v, mkSusp t s) :: nargs)) (s, []) args in - L.rev ncase) - cases in - mkInductive (l, label, nargs, ncases) + L.rev ncase) + cases in + mkInductive (l, label, ncases) | Cons (it, name) -> mkCons (mkSusp it s, name) | Case (l, e, ret, cases, default) -> mkCase (l, mkSusp e s, mkSusp ret s, @@ -614,21 +600,17 @@ let clean e = | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e) | Call (f, args) -> mkCall (clean s f, L.map (fun (ak, arg) -> (ak, clean s arg)) args) - | Inductive (l, label, args, cases) - -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, (ak, v, clean s t) :: nargs)) - (s, []) args in - let nargs = List.rev nargs in - let ncases = SMap.map (fun args - -> let (_, ncase) - = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, - (ak, v, clean s t) - :: nargs)) - (s, []) args in - L.rev ncase) - cases in - mkInductive (l, label, nargs, ncases) + | Inductive (l, label, cases) + -> let ncases = SMap.map (fun args + -> let (_, ncase) + = L.fold_left (fun (s, nargs) (ak, v, t) + -> (ssink v s, + (ak, v, clean s t) + :: nargs)) + (s, []) args in + L.rev ncase) + cases in + mkInductive (l, label, ncases) | Cons (it, name) -> mkCons (clean s it, name) | Case (l, e, ret, cases, default) -> mkCase (l, clean s e, clean s ret, @@ -689,7 +671,7 @@ let rec lexp_unparse lxp = -> (* (vdef * lexp * ltype) list *) let sdecls = List.fold_left (fun acc (vdef, lxp, ltp) - -> Node (Symbol (U.dummy_location, "_=_"), + -> Node (Symbol (U.dummy_location, "_:_"), [Symbol (sname vdef); lexp_unparse ltp]) :: Node (Symbol (U.dummy_location, "_=_"), [Symbol (sname vdef); lexp_unparse lxp]) @@ -703,14 +685,9 @@ let rec lexp_unparse lxp = let sargs = List.map (fun (kind, elem) -> lexp_unparse elem) largs in Node (lexp_unparse lxp, sargs)
- | Inductive(loc, label, lfargs, ctors) -> - (* (arg_kind * vdef * ltype) list *) - (* (arg_kind * pvar * pexp option) list *) - let pfargs = List.map (fun (kind, vdef, ltp) -> - (kind, sname vdef, Some (lexp_unparse ltp))) lfargs in - + | Inductive (loc, label, ctors) -> Node (stypecons, - Node (Symbol label, List.map pexp_u_formal_arg pfargs) + Symbol label :: List.map (fun (name, types) -> Node (Symbol (loc, name), @@ -943,9 +920,6 @@ and lexp_str ctx (exp : lexp) : string = let kind_str k = match k with | Anormal -> "->" | Aimplicit -> "=>" | Aerasable -> "≡>" in
- let kindp_str k = match k with - | Anormal -> ":" | Aimplicit -> "::" | Aerasable -> ":::" in - let get_name fname = match lexp_lexp' fname with | Builtin ((_, name), _) -> name, 0 @@ -1026,21 +1000,10 @@ and lexp_str ctx (exp : lexp) : string = | _ -> let args = List.fold_left print_arg "" args in "(" ^ (lexp_str' fname) ^ args ^ ")")
- | Inductive (_, (_, name), [], ctors) -> + | Inductive (_, (_, name), ctors) -> (keyword "typecons") ^ " (" ^ name ^") " ^ newline ^ (lexp_str_ctor ctx ctors)
- | Inductive (_, (_, name), args, ctors) - -> let args_str - = List.fold_left - (fun str (arg_kind, (_, name), ltype) - -> str ^ " (" ^ maybename name ^ " " ^ (kindp_str arg_kind) ^ " " - ^ (lexp_str' ltype) ^ ")") - "" args in - - (keyword "typecons") ^ " (" ^ name ^ args_str ^") " ^ - (lexp_str_ctor ctx ctors) - | Case (_, target, _ret, map, dflt) ->( let str = (keyword "case ") ^ (lexp_str' target) in let arg_str arg @@ -1138,11 +1101,8 @@ let rec eq e1 e2 = | (Call (e1, as1), Call (e2, as2)) -> eq e1 e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq e1 e2) as1 as2 - | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) - -> l1 = l2 && List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2) as1 as2 - && SMap.equal (List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2)) ctor1 ctor2 + | (Inductive (_, l1, ctor1), Inductive (_, l2, ctor2)) + -> l1 = l2 && SMap.equal (List.for_all2 datacons_equal) ctor1 ctor2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> eq t1 t2 && l1 = l2 | (Case (_, e1, r1, ctor1, def1), Case (_, e2, r2, ctor2, def2)) -> eq e1 e2 && eq r1 r2 && SMap.equal
===================================== src/opslexp.ml ===================================== @@ -26,6 +26,7 @@ module IMap = U.IMap (* open Lexer *) open Sexp module P = Pexp +open Pexp (* open Myers *) (* open Grammar *) open Lexp @@ -196,21 +197,17 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = | _ -> Log.internal_error "" in mkCall (DB.eq_refl, [Aerasable, elevel; Aerasable, etype; Aerasable, e]) in let reduce it name aargs = - let targs = match lexp_lexp' (lexp_whnf_aux it ctx) with - | Inductive (_,_,fargs,_) -> fargs - | _ -> Log.log_error "Case on a non-inductive type in whnf!"; [] in + let () = match lexp_lexp' (lexp_whnf_aux it ctx) with + | Inductive _ -> () + | _ -> Log.log_error "Case on a non-inductive type in whnf!" in try let (_, _, branch) = SMap.find name branches in - let (subst, _) - = List.fold_left - (fun (s, targs) (_, arg) -> - match targs with - | [] -> (S.cons (lexp_whnf_aux arg ctx) s, []) - | _targ::targs -> - (* Ignore the type arguments *) - (s, targs)) - (S.identity, targs) - aargs in + let subst = + List.fold_left + (fun s (_, arg) -> S.cons (lexp_whnf_aux arg ctx) s) + S.identity + aargs + in (* Substitute case Eq variable by the proof (Eq.refl l t e') *) let subst = S.cons (get_refl e') subst in lexp_whnf_aux (push_susp branch subst) ctx @@ -322,9 +319,8 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let e1' = lexp_whnf e1 ctx in let e2' = lexp_whnf e2 ctx in e1' == e2' || - let changed = not (e1 == e1' && e2 == e2') in - if changed && set_member_p vs e1' e2' then true else - let vs' = if changed then set_add vs e1' e2' else vs in + if set_member_p vs e1' e2' then true else + let vs' = set_add vs e1' e2' in let conv_p = conv_p' ctx vs' in match (lexp_lexp' e1', lexp_lexp' e2') with | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 @@ -362,29 +358,47 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = && (conv_erase && ak1 = P.Aerasable || conv_p t1 t2)) true args1 args2 in conv_p f1 f2 && conv_arglist_p args1 args2 - | (Inductive (_, l1, args1, cases1), Inductive (_, l2, args2, cases2)) - -> let rec conv_fields ctx vs fields1 fields2 = - match fields1, fields2 with - | ([], []) -> true - | ((ak1,vd1,t1)::fields1, (ak2,vd2,t2)::fields2) - -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_fields (DB.lexp_ctx_cons ctx vd1 Variable t1) - (set_shift vs) - fields1 fields2 - | _,_ -> false in - let rec conv_args ctx vs args1 args2 = - match args1, args2 with - | ([], []) -> - (* Args checked alright, now go on with the fields, - * using the new context. *) - SMap.equal (conv_fields ctx vs) cases1 cases2 - | ((ak1,l1,t1)::args1, (ak2,l2,t2)::args2) - -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_args (DB.lexp_ctx_cons ctx l1 Variable t1) - (set_shift vs) - args1 args2 - | _,_ -> false in - l1 == l2 && conv_args ctx vs' args1 args2 + | (Inductive (_, ((_, name_l) as l1), cases1), Inductive (_, ((_, name_r) as l2), cases2)) + -> let () = print_endline ("conv_p of " ^ name_l ^ " and " ^ name_r) in + let show_case meta consname args = + let show_arg ctx (_, (_, name as n), ty) = + let name = + match name with + | Some name -> name + | None -> "(noname)" + in + print_endline ("[" ^ meta ^ "] " ^ name ^ ": " ^ lexp_string ty); + print_endline ("[" ^ meta ^ "] whnf " ^ name ^ ": " ^ lexp_string (lexp_whnf ty ctx)); + let ctx' = DB.lexp_ctx_cons ctx n Variable ty in + ctx' + in + print_endline ("[" ^ meta ^ "] " ^ consname); + let _ = List.fold_left show_arg ctx args in + () + in + SMap.iter (show_case "l") cases1; + SMap.iter (show_case "r") cases2; + let rec conv_fields ctx vs fields1 fields2 = + match fields1, fields2 with + | ([], []) -> true + | ((ak1, vd1, t1) :: fields1, (ak2, vd2, t2) :: fields2) + -> ak1 == ak2 + && (let t1' = lexp_whnf t1 ctx in + let t2' = lexp_whnf t2 ctx in + let () = print_endline ("Comparing types " ^ lexp_string t1' ^ " and " ^ lexp_string t2') in + let res = conv_p' ctx vs t1' t2' in + let () = print_endline ("Done comparing types " ^ lexp_string t1' ^ " and " ^ lexp_string t2') in + res + && conv_fields + (DB.lexp_ctx_cons ctx vd1 Variable t1') + (set_shift vs) + fields1 + fields2) + | _, _ -> false + in + let res = l1 == l2 && SMap.equal (conv_fields ctx vs') cases1 cases2 in + let () = print_endline "Done" in + res | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2 | (Case (_, target1, r1, cases1, def1), Case (_, target2, r2, cases2, def2)) -> (* FIXME The termination of this case conversion is very @@ -410,13 +424,11 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | Call (f, args) -> (f, args) | _ -> (etype, []) in (* 2. Build the substitution for the inductive arguments *) - let fargs, ctors = + let ctors = (match lexp'_whnf it ctx with - | Inductive (_, _, fargs, constructors) - -> fargs, constructors + | Inductive (_, _, constructors) + -> constructors | _ -> Log.log_fatal ("Case of non-inductive in conv_p")) in - let fargs_subst = List.fold_left2 (fun s _farg (_, aarg) -> S.cons aarg s) - S.identity fargs aargs in (* 3. Compare the branches *) let ctx_extend_with_eq ctx subst hlxp = let tlxp = mkSusp target subst in @@ -450,7 +462,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = vdefs1 vdefs2 fieldtypes else None | _,_,_ -> None in - match mkctx ctx [] fargs_subst (List.length fields1) + match mkctx ctx [] Subst.identity (List.length fields1) fields1 fields2 fieldtypes with | None -> false | Some (nctx, args, _subst) -> @@ -694,53 +706,42 @@ and check'' erased ctx e = ^ lexp_string ft ^ ")!"); ft)) ft args - | Inductive (l, label, args, cases) - -> let rec arg_loop ctx erased args = - match args with - | [] - -> let level - = SMap.fold - (fun _ case level -> - let (level, _, _, _) = - List.fold_left - (fun (level, ictx, erased, n) (ak, v, t) -> - ((let lwhnf = lexp_whnf (check_type erased ictx t) ictx in - match lexp_lexp' lwhnf with - | Sort (_, Stype _) - when ak == P.Aerasable && impredicative_erase - -> level - | Sort (_, Stype level') - -> mkSLlub ctx level - (* We need to unshift because the final type - * cannot refer to the fields! *) - (* FIXME: If it does refer, - * we get an ugly error! *) - (mkSusp level' (L.sunshift n)) - | tt -> error_tc ~loc:(lexp_location t) - ~print_action:(fun _ -> - DB.print_lexp_ctx ictx; print_newline () - ) - ("Field type " - ^ lexp_string t - ^ " is not a Type! (" - ^ lexp_string lwhnf ^")"); - level), - DB.lctx_extend ictx v Variable t, - DB.set_sink 1 erased, - n + 1)) - (level, ctx, erased, 0) - case in - level) - cases (mkSortLevel SLz) in - mkSort (l, Stype level) - | (ak, v, t)::args - -> let _k = check_type DB.set_empty ctx t in - mkArrow (ak, v, t, lexp_location t, - arg_loop (DB.lctx_extend ctx v Variable t) - (dbset_push ak erased) - args) in - let tct = arg_loop ctx erased args in - tct + | Inductive (l, label, cases) + -> let level + = SMap.fold + (fun _ case level -> + let (level, _, _, _) = + List.fold_left + (fun (level, ictx, erased, n) (ak, v, t) -> + ((let lwhnf = lexp_whnf (check_type erased ictx t) ictx in + match lexp_lexp' lwhnf with + | Sort (_, Stype _) + when ak == P.Aerasable && impredicative_erase + -> level + | Sort (_, Stype level') + -> mkSLlub ctx level + (* We need to unshift because the final type + * cannot refer to the fields! *) + (* FIXME: If it does refer, + * we get an ugly error! *) + (mkSusp level' (L.sunshift n)) + | tt -> error_tc ~loc:(lexp_location t) + ~print_action:(fun _ -> + DB.print_lexp_ctx ictx; print_newline () + ) + ("Field type " + ^ lexp_string t + ^ " is not a Type! (" + ^ lexp_string lwhnf ^")"); + level), + DB.lctx_extend ictx v Variable t, + DB.set_sink 1 erased, + n + 1)) + (level, ctx, erased, 0) + case in + level) + cases (mkSortLevel SLz) in + mkSort (l, Stype level) | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) -> let call_split e = @@ -757,17 +758,13 @@ and check'' erased ctx e = "Target lexp's kind is not a sort"; DB.level0 in let it, aargs = call_split etype in (match lexp'_whnf it ctx, aargs with - | Inductive (_, _, fargs, constructors), aargs -> - let rec mksubst s fargs aargs = - match fargs, aargs with - | [], [] -> s - | _farg::fargs, (_ak, aarg)::aargs - (* We don't check aarg's type, because we assume that `check` - * returns a valid type. *) - -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (error_tc ~loc:l - "Wrong arg number to inductive type!"; s) in - let s = mksubst S.identity fargs aargs in + | Inductive (_, _, constructors), aargs -> + let () = match aargs with + | [] -> () + | _ + -> let message = "Wrong arg number to inductive type!" in + error_tc ~loc:l message + in let ctx_extend_with_eq ctx subst hlxp nerased = let tlxp = mkSusp e subst in let tltp = mkSusp etype subst in @@ -802,7 +799,7 @@ and check'' erased ctx e = mkCall (mkCons (it, (l, name)), List.map (fun (_, a) -> (P.Aerasable, a)) aargs) in let (nerased, nctx, hlxp) = - mkctx erased ctx s hctor vdefs fieldtypes in + mkctx erased ctx Subst.identity hctor vdefs fieldtypes in let subst = S.shift (List.length vdefs) in let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp nerased in assert_type nctx branch @@ -830,29 +827,18 @@ and check'' erased ctx e = ret | Cons (t, (l, name)) -> (match lexp'_whnf t ctx with - | Inductive (l, _, fargs, constructors) + | Inductive (l, _, constructors) -> (try let fieldtypes = SMap.find name constructors in - let rec indtype fargs start_index = - match fargs with - | [] -> [] - | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index)) - :: indtype fargs (start_index - 1) in let rec fieldargs ftypes = match ftypes with - | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs), - indtype fargs (nargs - 1)) + | [] -> let nargs = List.length fieldtypes in + mkCall (mkSusp t (S.shift nargs), []) | (ak, vd, ftype) :: ftypes -> mkArrow (ak, vd, ftype, lexp_location ftype, - fieldargs ftypes) in - let rec buildtype fargs = - match fargs with - | [] -> fieldargs fieldtypes - | (ak, ((l,_) as vd), atype) :: fargs - -> mkArrow (P.Aerasable, vd, atype, l, - buildtype fargs) in - buildtype fargs + fieldargs ftypes) + in + fieldargs fieldtypes with Not_found -> (error_tc ~loc:l ("Constructor "" ^ name ^ "" does not exist"); @@ -939,23 +925,19 @@ and fv (e : lexp) : (DB.set * mv_set) = then fv_erase afvs else afvs)) (fv f) args - | Inductive (_, _, args, cases) - -> let alen = List.length args in - let s - = List.fold_left (fun s (_, _, t) - -> fv_sink 1 (fv_union s (fv t))) - fv_empty args in - let s - = SMap.fold - (fun _ fields s - -> fv_union + | Inductive (_, _, cases) + -> let s = + SMap.fold + (fun _ fields s + -> fv_union s (fv_hoist (List.length fields) (List.fold_left (fun s (_, _, t) -> fv_sink 1 (fv_union s (fv t))) fv_empty fields))) - cases s in - fv_hoist alen s + cases fv_empty + in + fv_hoist 0 s | Cons (t, _) -> fv_erase (fv t) | Case (_, e, t, cases, def) -> let s = fv_union (fv e) (fv_erase (fv t)) in @@ -1020,67 +1002,48 @@ and get_type ctx e = -> mkSusp t2 (S.substitute arg) | _ -> ft) ft args - | Inductive (l, label, args, cases) + | Inductive (l, label, cases) (* FIXME: Use `check` here but silencing errors? *) - -> let rec arg_loop args ctx = - match args with - | [] - -> let level - = SMap.fold - (fun _ case level -> - let (level, _, _) = - List.fold_left - (fun (level, ictx, n) (ak, v, t) -> - ((match lexp'_whnf (get_type ictx t) ictx with - | Sort (_, Stype _) - when ak == P.Aerasable && impredicative_erase - -> level - | Sort (_, Stype level') - -> mkSLlub ctx level - (* We need to unshift because the final type - * cannot refer to the fields! *) - (mkSusp level' (L.sunshift n)) - | tt -> level), - DB.lctx_extend ictx v Variable t, - n + 1)) - (level, ctx, 0) - case in - level) - cases (mkSortLevel SLz) in - mkSort (l, Stype level) - | (ak, v, t)::args - -> mkArrow (ak, v, t, lexp_location t, - arg_loop args (DB.lctx_extend ctx v Variable t)) in - let tct = arg_loop args ctx in - tct + -> let level + = SMap.fold + (fun _ case level -> + let (level, _, _) = + List.fold_left + (fun (level, ictx, n) (ak, v, t) -> + ((match lexp'_whnf (get_type ictx t) ictx with + | Sort (_, Stype _) + when ak == P.Aerasable && impredicative_erase + -> level + | Sort (_, Stype level') + -> mkSLlub ctx level + (* We need to unshift because the final type + * cannot refer to the fields! *) + (mkSusp level' (L.sunshift n)) + | tt -> level), + DB.lctx_extend ictx v Variable t, + n + 1)) + (level, ctx, 0) + case in + level) + cases (mkSortLevel SLz) in + mkSort (l, Stype level) | Case (l, e, ret, branches, default) -> ret | Cons (t, (l, name)) -> (match lexp'_whnf t ctx with - | Inductive (l, _, fargs, constructors) - -> (try - let fieldtypes = SMap.find name constructors in - let rec indtype fargs start_index = - match fargs with - | [] -> [] - | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index)) - :: indtype fargs (start_index - 1) in - let rec fieldargs ftypes = - match ftypes with - | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs), - indtype fargs (nargs - 1)) - | (ak, vd, ftype) :: ftypes - -> mkArrow (ak, vd, ftype, lexp_location ftype, - fieldargs ftypes) in - let rec buildtype fargs = - match fargs with - | [] -> fieldargs fieldtypes - | (ak, ((l,_) as vd), atype) :: fargs - -> mkArrow (P.Aerasable, vd, atype, l, - buildtype fargs) in - buildtype fargs - with Not_found -> DB.type_int) - | _ -> DB.type_int) + | Inductive (l, _, constructors) + -> (try + let fieldtypes = SMap.find name constructors in + let rec fieldargs ftypes = + match ftypes with + | [] -> let nargs = List.length fieldtypes in + mkCall (mkSusp t (S.shift nargs), + []) + | (ak, vd, ftype) :: ftypes + -> mkArrow (ak, vd, ftype, lexp_location ftype, + fieldargs ftypes) in + fieldargs fieldtypes + with Not_found -> DB.type_int) + | _ -> DB.type_int) | Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> get_type ctx (push_susp e s) @@ -1122,11 +1085,11 @@ let rec erase_type (lxp: lexp): E.elexp = | L.Susp(l, s) -> erase_type (L.push_susp l s)
(* To be thrown out *) - | L.Arrow _ -> E.Type lxp - | L.SortLevel _ -> E.Type lxp - | L.Sort _ -> E.Type lxp + | L.Arrow _ -> E.Type lxp + | L.SortLevel _ -> E.Type lxp + | L.Sort _ -> E.Type lxp (* Still useful to some extent. *) - | L.Inductive(l, label, _, _) -> E.Type lxp + | L.Inductive (l, label, _) -> E.Type lxp | L.Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> erase_type (push_susp e s) @@ -1207,7 +1170,7 @@ let ctx2tup ctx nctx = let types = List.rev types in (*Log.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*)
- mkCall (mkCons (mkInductive (loc, type_label, [], + mkCall (mkCons (mkInductive (loc, type_label, SMap.add cons_name (List.map (fun (oname, t) -> (P.Aimplicit, oname,
===================================== src/unification.ml ===================================== @@ -79,13 +79,13 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | Lambda (_, _, t, e) -> oi t || oi e | Call (f, args) -> List.fold_left (fun o (_, arg) -> o || oi arg) (oi f) args - | Inductive (_, _, args, cases) + | Inductive (_, _, cases) -> SMap.fold (fun _ fields o -> List.fold_left (fun o (_, _, t) -> o || oi t) o fields) cases - (List.fold_left (fun o (_, _, t) -> o || oi t) false args) + false | Cons (t, _) -> oi t | Case (_, e, t, cases, def) -> let o = oi e || oi t in @@ -565,12 +565,12 @@ and is_same arglist arglist2 =
and unify_inductive lxp1 lxp2 ctx vs = match lexp_lexp' lxp1, lexp_lexp' lxp2 with - | (Inductive (_loc1, label1, args1, consts1), - Inductive (_loc2, label2, args2, consts2)) - -> unify_inductive' ctx vs args1 args2 consts1 consts2 lxp1 lxp2 + | (Inductive (_loc1, label1, consts1), + Inductive (_loc2, label2, consts2)) + -> unify_inductive' ctx vs consts1 consts2 lxp1 lxp2 | _, _ -> [(CKimpossible, ctx, lxp1, lxp2)]
-and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 = +and unify_inductive' ctx vs consts1 consts2 e1 e2 = let unif_formals ctx vs args1 args2 = if not (List.length args1 == List.length args2) then (ctx, vs, [(CKimpossible, ctx, e1, e2)]) @@ -582,7 +582,6 @@ and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 = else (unify' t1 t2 ctx vs) @ residue)) (ctx, vs, []) (List.combine args1 args2) in - let (ctx, vs, residue) = unif_formals ctx vs args1 args2 in if not (SMap.cardinal consts1 == SMap.cardinal consts2) then [(CKimpossible, ctx, e1, e2)] else @@ -592,7 +591,7 @@ and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 = = unif_formals ctx vs args1 args2 in residue' @ residue | exception Not_found -> [(CKimpossible, ctx, e1, e2)]) - consts1 residue + consts1 []
(** unify the SMap of list in Inductive *) (* and unify_induct_sub_list l1 l2 subst =
===================================== tests/opslexp_test.ml ===================================== @@ -0,0 +1,77 @@ +(* Copyright (C) 2020 Free Software Foundation, Inc. + * + * Author: Simon Génier simon.genier@umontreal.ca + * Keywords: languages, lisp, dependent types. + * + * This file is part of Typer. + * + * Typer is free software; you can redistribute it and/or modify it under the + * terms of the GNU General Public License as published by the Free Software + * Foundation, either version 3 of the License, or (at your option) any later + * version. + * + * Typer is distributed in the hope that it will be useful, but WITHOUT ANY + * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS + * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more + * details. + * + * You should have received a copy of the GNU General Public License along + * with this program. If not, see http://www.gnu.org/licenses/. *) + +open Utest_lib +open Util + +let assert_conv_p + (name : string) + ?(setup : string option) + (l : string) + (r : string) + : unit = + + let run () = + let ectx = Elab.default_ectx in + let ectx = + match setup with + | Some setup' -> snd (Elab.lexp_decl_str setup' ectx) + | None -> ectx + in + let last_metavar = !Unification.global_last_metavar in + let ls = Elab.lexp_expr_str l ectx in + let l' = + match ls with + | [l'] -> l' + | _ -> failwith "expected a single lexp" + in + Unification.global_last_metavar := last_metavar; + let rs = Elab.lexp_expr_str r ectx in + let r' = + match rs with + | [r'] -> r' + | _ -> failwith "expected a single lexp" + in + if Opslexp.conv_p (Debruijn.ectx_to_lctx ectx) l' r' + then success + else failure + in + add_test "OPSLEXP" name run + +let () = + assert_conv_p + "Inductive types under a lambda" + ~setup:{| + List0 : Type -> Type; + List0 = lambda α -> typecons List0 (nil) (cons α (List0 α)); + |} + "List0" + "List0"; + + assert_conv_p + "???" + ~setup:{| + List0 : Type -> Type; + List0 = lambda α -> typecons List0 (nil) (cons α (List0 α)); + |} + "lambda α -> datacons (List0 α) nil" + "lambda α -> datacons (List0 α) nil"; + + run_all ()
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/108d467994d3afad78da669aab7ececfad...