Simon Génier pushed to branch there-can-be-only-one-inductive at Stefan / Typer

Commits: 613a8806 by Simon Génier at 2020-11-29T17:08:36-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.

- - - - -

8 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

Changes:

===================================== btl/builtins.typer ===================================== @@ -192,13 +192,15 @@ 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

===================================== btl/empty.typer =====================================

===================================== src/elab.ml ===================================== @@ -443,28 +443,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 @@ -782,37 +776,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) = @@ -1561,7 +1545,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"; @@ -1593,12 +1577,13 @@ 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) + let () = print_endline ("sform_typecons: " ^ name) in + (mkInductive (loc, label, map_ctor), Lazy)

let sform_hastype ctx loc sargs ot = match sargs with @@ -2007,7 +1992,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

type attribute_key = (int * string) (* rev_dbi * Var name *) @@ -58,9 +58,11 @@ module AttributeMap = Map.Make (struct type t = attribute_key let compare = comp * 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, ... *) @@ -74,9 +76,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 *) @@ -220,15 +220,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 @@ -249,6 +244,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 = @@ -277,11 +275,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 @@ -307,18 +302,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, m) = hc (Builtin (v, t, m)) -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, m) = hc (Builtin (v, t, m)) +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)) @@ -392,21 +387,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 @@ -517,7 +507,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 @@ -554,21 +544,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, @@ -621,21 +607,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, @@ -710,14 +692,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), @@ -950,9 +927,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 @@ -1033,21 +1007,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 @@ -1145,11 +1108,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 ===================================== @@ -196,21 +196,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 @@ -362,29 +358,26 @@ 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 rec conv_fields ctx vs fields1 fields2 = + match fields1, fields2 with + | ([], []) -> true + | ((ak1,vd1,t1)::fields1, (ak2,vd2,t2)::fields2) + -> ak1 == ak2 + && (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 +403,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 +441,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) -> @@ -695,53 +686,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 = @@ -758,17 +738,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 @@ -803,7 +779,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 @@ -831,29 +807,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"); @@ -940,23 +905,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 @@ -1021,67 +982,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) @@ -1123,11 +1065,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) @@ -1208,7 +1150,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 =

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/613a880662f091a5b0cbda29ea495b6f86...