Jean-Alexandre Barszcz pushed to branch master at Stefan / Typer

Commits: c34d6d0c by Jean-Alexandre Barszcz at 2020-09-13T17:06:35-04:00 Fix an issue in the unification of metavariables

The issue was that unification was not idempotent in certain cases. In particular, when unifying a metavar that has a non-identity substitution (let's say lxp1) with a term (let's say lxp2) that refers to some metavariables, the corresponding metavariable references in the associated term (thus in lxp1 after association) could have different substitutions from the same references in lxp2. See the added comment for a more detailed example.

- - - - - 023ea461 by Jean-Alexandre Barszcz at 2020-09-13T17:06:35-04:00 Move the Eq builtin to debruijn.ml to make it available for elab.

- - - - - b4d53239 by Jean-Alexandre Barszcz at 2020-09-13T17:06:35-04:00 Make Eq.refl available to the ocaml code

* src/debruijn.ml : Add a definition of the lexp for Eq.refl

* src/builtin.ml : Register the constant Eq.refl

* btl/builtins.typer (Eq_refl) : Use the builtin variable ##Eq.refl instead of registering the builtin with the `Built-in` form. This ensures that we have the right variable and type, and might help to keep things in sync between the ocaml and typer code.

- - - - - efe2032d by Jean-Alexandre Barszcz at 2020-09-13T17:06:35-04:00 Make the case elaboration code more consistent

This commit doesn't substantially change the behavior of the case elaboration, but makes the code a bit more consistent and might save some unnecessary metavariables in some cases.

- - - - - 4c632a1f by Jean-Alexandre Barszcz at 2020-09-14T15:56:01-04:00 Add dependent elimination

This commit changes elaboration, conversion, typechecking, erasure, and the computation of free variables and WHNFs for case expressions, to account for the fact that the context of all the branches of case expressions is extended with a proof of equality between the branch's head and the case's target. Careful elimination of this equality proof with Eq_cast makes dependent elimination possible.

- - - - - b082a329 by Jean-Alexandre Barszcz at 2020-09-14T15:56:01-04:00 Conversion for metavariables

- - - - - fd990da1 by Jean-Alexandre Barszcz at 2020-09-14T15:56:01-04:00 Case conversion

- - - - -

10 changed files:

- btl/builtins.typer - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml - tests/elab_test.ml - tests/eval_test.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -48,7 +48,7 @@ Void = typecons Void; %% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l %% Eq' : (l : TypeLevel) ≡> Type_ l -> Type_ l -> Type_ l Eq_refl : ((x : ?t) ≡> Eq x x); -Eq_refl = Built-in "Eq.refl"; +Eq_refl = ##Eq.refl;

Eq_cast : (x : ?) ≡> (y : ?) ≡> (p : Eq x y)

===================================== src/builtin.ml ===================================== @@ -99,19 +99,6 @@ let dloc = DB.dloc let op_binary t = mkArrow (Anormal, (dloc, None), t, dloc, mkArrow (Anormal, (dloc, None), t, dloc, t))

-let type_eq = - let lv = (dloc, Some "l") in - let tv = (dloc, Some "t") in - mkArrow (Aerasable, lv, - DB.type_level, dloc, - mkArrow (Aerasable, tv, - mkSort (dloc, Stype (mkVar (lv, 0))), dloc, - mkArrow (Anormal, (dloc, None), - mkVar (tv, 0), dloc, - mkArrow (Anormal, (dloc, None), - mkVar (tv, 1), dloc, - mkSort (dloc, Stype (mkVar (lv, 3))))))) - let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx

(* Typer list as seen during runtime. *) @@ -161,7 +148,9 @@ let register_builtin_csts () = add_builtin_cst "Integer" DB.type_integer; add_builtin_cst "Float" DB.type_float; add_builtin_cst "String" DB.type_string; - add_builtin_cst "Elab_Context" DB.type_elabctx + add_builtin_cst "Elab_Context" DB.type_elabctx; + add_builtin_cst "Eq" DB.type_eq; + add_builtin_cst "Eq.refl" DB.eq_refl

let register_builtin_types () = let _ = new_builtin_type "Sexp" DB.type0 in @@ -175,7 +164,6 @@ let register_builtin_types () = "Array" (mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0)) in let _ = new_builtin_type "FileHandle" DB.type0 in - let _ = new_builtin_type "Eq" type_eq in ()

let _ = register_builtin_csts ();

===================================== src/debruijn.ml ===================================== @@ -96,6 +96,37 @@ let type_integer = mkBuiltin ((dloc, "Integer"), type0, None) let type_float = mkBuiltin ((dloc, "Float"), type0, None) let type_string = mkBuiltin ((dloc, "String"), type0, None) let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0, None) +let type_eq_type = + let lv = (dloc, Some "l") in + let tv = (dloc, Some "t") in + mkArrow (Aerasable, lv, + type_level, dloc, + mkArrow (Aerasable, tv, + mkSort (dloc, Stype (mkVar (lv, 0))), dloc, + mkArrow (Anormal, (dloc, None), + mkVar (tv, 0), dloc, + mkArrow (Anormal, (dloc, None), + mkVar (tv, 1), dloc, + mkSort (dloc, Stype (mkVar (lv, 3))))))) +let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type, None) +let eq_refl = + let lv = (dloc, Some "l") in + let tv = (dloc, Some "t") in + let xv = (dloc, Some "x") in + mkBuiltin ((dloc, "Eq.refl"), + mkArrow (Aerasable, lv, + type_level, dloc, + mkArrow (Aerasable, tv, + mkSort (dloc, Stype (mkVar (lv, 0))), dloc, + mkArrow (Aerasable, xv, + mkVar (tv, 0), dloc, + mkCall (type_eq, + [Aerasable, mkVar (lv, 2); + Aerasable, mkVar (tv, 1); + Anormal, mkVar (xv, 0); + Anormal, mkVar (xv, 0)])))), + None) +

(* easier to debug with type annotations *) type env_elem = (vname * varbind * ltype)

===================================== src/elab.ml ===================================== @@ -467,11 +467,11 @@ let rec meta_to_var ids (e : lexp) = -> let ncases = SMap.map (fun (l, fields, e) - -> (l, fields, loop (o + List.length fields) e)) + -> (l, fields, loop (o + List.length fields + 1) e)) cases in mkCase (l, loop o e, loop o t, ncases, match default with None -> None - | Some (v, e) -> Some (v, loop (1 + o) e)) + | Some (v, e) -> Some (v, loop (2 + o) e)) | Metavar (id, s, name) -> if IMap.mem id ids then mkVar (name, o + count - IMap.find id ids) @@ -736,20 +736,24 @@ and check_case rtype (loc, target, ppatterns) ctx =

(* get target and its type *) let tlxp, tltp = infer target ctx in + let tknd = OL.get_type (ectx_to_lctx ctx) tltp in + let tlvl = match OL.lexp'_whnf tknd (ectx_to_lctx ctx) with + | Sort (_, Stype l) -> l + | _ -> fatal "Target lexp's kind is not a sort" in let it_cs_as = ref None in let ltarget = ref tlxp in

let get_cs_as it' lctor = + let unify_ind expected actual = + match Unif.unify actual expected (ectx_to_lctx ctx) with + | (_::_) + -> lexp_error loc lctor + ("Expected pattern of type `" ^ lexp_string expected + ^ "` but got `" ^ lexp_string actual ^ "`") + | [] -> () in match !it_cs_as with | Some (it, cs, args) - -> let _ = match Unif.unify it' it (ectx_to_lctx ctx) with - | (_::_) - -> lexp_error loc lctor - ("Expected pattern of type `" - ^ lexp_string it ^ "` but got `" - ^ lexp_string it' ^ "`") - | [] -> () in - (cs, args) + -> unify_ind it it'; (cs, args) | None -> match OL.lexp'_whnf it' (ectx_to_lctx ctx) with | Inductive (_, _, fargs, constructors) @@ -771,8 +775,9 @@ and check_case rtype (loc, target, ppatterns) ctx = | 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 + match OL.lexp'_whnf it (ectx_to_lctx ctx) with | Inductive (_, _, fargs, constructors) -> assert (List.length fargs = List.length targs); constructors @@ -780,16 +785,36 @@ and check_case rtype (loc, target, ppatterns) ctx = ("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) =

+ let shift_to_extended_ctx nctx lexp = + mkSusp lexp (S.shift (M.length (ectx_to_lctx nctx) + - M.length (ectx_to_lctx ctx))) in + + let ctx_extend_with_eq nctx head_lexp = + (* Add a proof of equality between the target and the branch + head to the context *) + let tlxp' = shift_to_extended_ctx nctx tlxp in + let tltp' = shift_to_extended_ctx nctx tltp in + let tlvl' = shift_to_extended_ctx nctx tlvl in + let eqty = mkCall (DB.type_eq, + [(Aerasable, tlvl'); (* Typelevel *) + (Aerasable, tltp'); (* Inductive type *) + (Anormal, head_lexp); (* Lexp of the branch head *) + (Anormal, tlxp')]) (* Target lexp *) + in ctx_extend nctx (loc, None) Variable eqty + in + let add_default v = (if dflt != None then uniqueness_warn pat); let nctx = ctx_extend ctx v Variable tltp in - let rtype' = mkSusp rtype (S.shift (M.length (ectx_to_lctx nctx) - - M.length (ectx_to_lctx ctx))) in + let head_lexp = mkVar (v, 0) in + let nctx = ctx_extend_with_eq nctx head_lexp in + let rtype' = shift_to_extended_ctx nctx rtype in let lexp = check pexp rtype' nctx in lbranches, Some (v, lexp) in

@@ -870,9 +895,15 @@ and check_case rtype (loc, target, ppatterns) ctx = make_nctx nctx (ssink var s) pargs cargs pe ((ak, var)::acc) in let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in - let rtype' = mkSusp rtype - (S.shift (M.length (ectx_to_lctx nctx) - - M.length (ectx_to_lctx ctx))) in + let head_lexp_ctor = + shift_to_extended_ctx nctx + (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs)) in + let head_lexp_args = + List.mapi (fun i (ak, vname) -> + (ak, mkVar (vname, List.length fargs - i - 1))) fargs in + let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) in + let nctx = ctx_extend_with_eq nctx head_lexp in + let rtype' = shift_to_extended_ctx nctx rtype in let lexp = check pexp rtype' nctx in SMap.add cons_name (loc, fargs, lexp) lbranches, dflt

===================================== src/inverse_subst.ml ===================================== @@ -304,11 +304,12 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = -> let s' = L.fold_left (fun s (_,ov) -> ssink ov s) s cargs in - (l, cargs, apply_inv_subst e s')) + let s'' = ssink (l, None) s' in + (l, cargs, apply_inv_subst e s'')) cases, match default with | None -> default - | Some (v,e) -> Some (v, apply_inv_subst e (ssink v s))) + | Some (v,e) -> Some (v, apply_inv_subst e (ssink (l, None) (ssink v s)))) | Metavar (id, s', name) -> match metavar_lookup id with | MVal e -> apply_inv_subst (push_susp e s') s

===================================== src/lexp.ml ===================================== @@ -574,11 +574,11 @@ let rec push_susp e s = (* Push a suspension one level down. *) -> let s' = L.fold_left (fun s (_,ov) -> ssink ov s) s cargs in - (l, cargs, mkSusp e s')) + (l, cargs, mkSusp e (ssink (l, None) s'))) cases, match default with | None -> default - | Some (v,e) -> Some (v, mkSusp e (ssink v s))) + | Some (v,e) -> Some (v, mkSusp e (ssink (l, None) (ssink v s)))) (* Susp should never appear around Var/Susp/Metavar because mkSusp * pushes the subst into them eagerly. IOW if there's a Susp(Var..) * or Susp(Metavar..) it's because some chunk of code should use mkSusp @@ -641,11 +641,12 @@ let clean e = -> let s' = L.fold_left (fun s (_,ov) -> ssink ov s) s cargs in - (l, cargs, clean s' e)) + let s'' = ssink (l, None) s' in + (l, cargs, clean s'' e)) cases, match default with | None -> default - | Some (v,e) -> Some (v, clean (ssink v s) e)) + | Some (v,e) -> Some (v, clean (ssink (l, None) (ssink v s)) e)) | Susp (e, s') -> clean (scompose s' s) e | Var _ -> if S.identity_p s then e else clean S.identity (mkSusp e s)

===================================== src/opslexp.ml ===================================== @@ -38,6 +38,22 @@ module S = Subst (* module L = List *) module DB = Debruijn

+type set_plexp = (lexp * lexp) list +type sort_compose_result + = SortResult of ltype + | SortInvalid + | SortK1NotType + | SortK2NotType +type mv_set = (scope_level * ltype * ctx_length * vname) IMap.t + (* Metavars that appear in non-erasable positions. *) + * unit IMap.t + +module LMap + (* Memoization table. FIXME: Ideally the keys should be "weak", but + * I haven't found any such functionality in OCaml's libs. *) + = Hashtbl.Make + (struct type t = lexp let hash = Hashtbl.hash let equal = (==) end) + let error_tc = Log.log_error ~section:"TC" let warning_tc = Log.log_warning ~section:"TC"

@@ -133,8 +149,13 @@ let lexp_close lctx e = * return value as little as possible since WHNF will inherently introduce * call-by-name behavior. *)

-let lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = +(* FIXME This large letrec closes the loop between lexp_whnf_aux and + get_type so that we can use get_type in the WHNF of a case to get + the inductive type of the target (and it's typelevel). A better + solution would be to add these values as annotations in the lexp + datatype. *) let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = + let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = match lexp_lexp' e with | Var v -> (match lookup_value ctx v with | None -> e @@ -157,6 +178,12 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = | _ -> e) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> let e' = lexp_whnf_aux e ctx in + let get_refl e = + let etype = get_type ctx e in (* FIXME we should not need get_type here *) + let elevel = match lexp'_whnf (get_type ctx etype) ctx with + | Sort (_, Stype l) -> l + | _ -> 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 @@ -173,11 +200,14 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = (s, targs)) (S.identity, targs) 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 with Not_found -> match default with | Some (v,default) - -> lexp_whnf_aux (push_susp default (S.substitute e')) ctx + -> let subst = S.cons (get_refl e') (S.substitute e') in + lexp_whnf_aux (push_susp default subst) ctx | _ -> Log.log_error ~section:"WHNF" ~loc:l ("Unhandled constructor " ^ name ^ "in case expression"); @@ -203,29 +233,28 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp =

in lexp_whnf_aux e ctx

-let lexp'_whnf e (ctx : DB.lexp_context) : lexp' = +and lexp'_whnf e (ctx : DB.lexp_context) : lexp' = lexp_lexp' (lexp_whnf_aux e ctx)

-let lexp_whnf e (ctx : DB.lexp_context) : lexp = +and lexp_whnf e (ctx : DB.lexp_context) : lexp = lexp_whnf_aux e ctx

(** A very naive implementation of sets of pairs of lexps. *) -type set_plexp = (lexp * lexp) list -let set_empty : set_plexp = [] -let set_member_p (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool +and set_empty : set_plexp = [] +and set_member_p (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool = try let _ = List.find (fun (e1', e2') -> L.eq e1 e1' && L.eq e2 e2') s in true with Not_found -> false -let set_add (s : set_plexp) (e1 : lexp) (e2 : lexp) : set_plexp +and set_add (s : set_plexp) (e1 : lexp) (e2 : lexp) : set_plexp = (* assert (not (set_member_p s e1 e2)); *) ((e1, e2) :: s) -let set_shift_n (s : set_plexp) (n : U.db_offset) +and set_shift_n (s : set_plexp) (n : U.db_offset) = List.map (let s = S.shift n in fun (e1, e2) -> (Lexp.push_susp e1 s, Lexp.push_susp e2 s)) s -let set_shift s : set_plexp = set_shift_n s 1 +and set_shift s : set_plexp = set_shift_n s 1

(********* Testing if two types are "convertible" aka "equivalent" *********)

@@ -235,7 +264,7 @@ let set_shift s : set_plexp = set_shift_n s 1 * `c` is the maximum "constant" level that occurs in `e` * and `m` maps variable indices to the maxmimum depth at which they were * found. *) -let level_canon e = +and level_canon e = let add_var_depth v d ((c,m) as acc) = let o = try IMap.find v m with Not_found -> -1 in if o < d then (c, IMap.add v d m) else acc in @@ -255,14 +284,14 @@ let level_canon e = | _ -> (max_int, m) in canon e 0 (0,IMap.empty)

-let level_leq (c1, m1) (c2, m2) = +and level_leq (c1, m1) (c2, m2) = c1 <= c2 && c1 != max_int && IMap.for_all (fun i d -> try d <= IMap.find i m2 with Not_found -> false) m1

(* Returns true if e₁ and e₂ are equal (upto alpha/beta/...). *) -let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = +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' || @@ -330,19 +359,109 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | _,_ -> false in l1 == l2 && conv_args ctx vs' args1 args2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2 - (* I'm not sure to understand how to compare two Metavar * - * Should I do a `lookup`? Or is it that simple: *) - (*| (Metavar (id1,_,_), Metavar (id2,_,_)) -> id1 = id2*) - (* FIXME: Various missing cases, such as Case. *) + | (Case (_, target1, r1, cases1, def1), Case (_, target2, r2, cases2, def2)) + -> (* FIXME The termination of this case conversion is very + fragile. Indeed, we recurse in all branches, bypassing any + termination condition. Checking syntactic equality as a + base case seems to be sufficient in simple cases, but it + is probably not enough in general. *) + eq e1' e2' || ( + conv_p target1 target2 && + conv_p r1 r2 && ( + (* Compare the branches *) + (* We can arbitrarily use target1 since target1 and target2 + are convertible *) + let target = target1 in + let etype = lexp_whnf (get_type ctx target) ctx in + let ekind = get_type ctx etype in + let elvl = match lexp'_whnf ekind ctx with + | Sort (_, Stype l) -> l + | _ -> Log.log_fatal ~loc:(lexp_location ekind) + "Target lexp's kind is not a sort"; in + (* 1. Get the inductive for the field types *) + let it, aargs = match lexp_lexp' etype with + | Call (f, args) -> (f, args) + | _ -> (etype, []) in + (* 2. Build the substitution for the inductive arguments *) + let fargs, ctors = + (match lexp'_whnf it ctx with + | Inductive (_, _, fargs, constructors) + -> fargs, 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 + let tltp = mkSusp etype subst in + let tlvl = mkSusp elvl subst in + let eqty = mkCall (DB.type_eq, + [(Aerasable, tlvl); (* Typelevel *) + (Aerasable, tltp); (* Inductive type *) + (Anormal, hlxp); (* Lexp of the branch head *) + (Anormal, tlxp)]) in (* Target lexp *) + DB.lexp_ctx_cons ctx (DB.dloc, None) Variable eqty in + (* The map module doesn't have a function to compare two + maps with the key (which is needed to get the field types + from the inductive. Instead, we work with the lists of + associations. *) + (try + List.for_all2 (fun (l1, (_, fields1, e1)) (l2, (_, fields2, e2)) -> + l1 = l2 && + let fieldtypes = SMap.find l1 ctors in + let rec mkctx ctx args s i vdefs1 vdefs2 fieldtypes = + match vdefs1, vdefs2, fieldtypes with + | [], [], [] -> Some (ctx, List.rev args, s) + | (ak1, vdef1)::vdefs1, (ak2, vdef2)::vdefs2, + (ak', vdef', ftype)::fieldtypes + -> if ak1 = ak2 && ak2 = ak' then + mkctx + (DB.lexp_ctx_cons ctx vdef1 Variable (mkSusp ftype s)) + ((ak1, (mkVar (vdef1, i)))::args) + (ssink vdef1 s) + (i - 1) + vdefs1 vdefs2 fieldtypes + else None + | _,_,_ -> None in + match mkctx ctx [] fargs_subst (List.length fields1) + fields1 fields2 fieldtypes with + | None -> false + | Some (nctx, args, _subst) -> + let offset = (List.length fields1) in + let subst = S.shift offset in + let eaargs = + List.map (fun (_, a) -> (P.Aerasable, a)) aargs in + let ctor = mkSusp (mkCall (mkCons (it, (DB.dloc, l1)), + eaargs)) subst in + let hlxp = mkCall (ctor, args) in + let nctx = ctx_extend_with_eq nctx subst hlxp in + conv_p' nctx (set_shift_n vs' (offset + 1)) e1 e2 + ) (SMap.bindings cases1) (SMap.bindings cases2) + with + | Invalid_argument _ -> false (* If the lists have different length *) + ) + && (match (def1, def2) with + | (Some (v1, e1), Some (v2, e2)) -> + let nctx = DB.lctx_extend ctx v1 Variable etype in + let subst = S.shift 1 in + let hlxp = mkVar ((DB.dloc, None), 0) in + let nctx = ctx_extend_with_eq nctx subst hlxp in + conv_p' nctx (set_shift_n vs' 2) e1 e2 + | None, None -> true + | _, _ -> false))) + | (Metavar (id1,s1,_), Metavar (id2,s2,_)) when id1 == id2 -> + (* FIXME Should we use conversion on the terms of the + substitution instead of syntactic equality? *) + subst_eq s1 s2 | (_, _) -> false

-let conv_p (ctx : DB.lexp_context) e1 e2 +and conv_p (ctx : DB.lexp_context) e1 e2 = if e1 == e2 then true else conv_p' ctx set_empty e1 e2

(********* Testing if a lexp is properly typed *********)

-let rec mkSLlub ctx e1 e2 = +and mkSLlub ctx e1 e2 = let lwhnf1 = lexp_whnf e1 ctx in let lwhnf2 = lexp_whnf e2 ctx in match (lexp_lexp' lwhnf1, lexp_lexp' lwhnf2) with @@ -357,13 +476,7 @@ let rec mkSLlub ctx e1 e2 = else if level_leq ce2 ce1 then e1 else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *)

-type sort_compose_result - = SortResult of ltype - | SortInvalid - | SortK1NotType - | SortK2NotType - -let sort_compose ctx1 ctx2 l ak k1 k2 = +and sort_compose ctx1 ctx2 l ak k1 k2 = (* BEWARE! Technically `k2` can refer to `v`, but this should only happen * if `v` is a TypeLevel. *) let lwhnf1 = lexp'_whnf k1 ctx1 in @@ -403,11 +516,11 @@ let sort_compose ctx1 ctx2 l ak k1 k2 = | (Sort (_, _), _) -> SortK2NotType | (_, _) -> SortK1NotType

-let dbset_push ak erased = +and dbset_push ak erased = let nerased = DB.set_sink 1 erased in if ak = P.Aerasable then DB.set_set 0 nerased else nerased

-let nerased_let defs erased = +and nerased_let defs erased = (* Let bindings are not erasable, with the important exception of * let-bindings of the form `x = y` where `y` is an erasable var. * This exception is designed so that macros like `case` which need to @@ -433,7 +546,7 @@ let nerased_let defs erased = erased es

(* "check ctx e" should return τ when "Δ ⊢ e : τ" *) -let rec check'' erased ctx e = +and check'' erased ctx e = let check = check'' in let assert_type ctx e t t' = if conv_p ctx t t' then () @@ -608,7 +721,14 @@ let rec check'' erased ctx e = match lexp_lexp' e with | Call (f, args) -> (f, args) | _ -> (e,[]) in - let etype = lexp_whnf (check erased ctx e) ctx in + let etype = lexp_whnf (check erased ctx e) ctx in + (* FIXME save the type in the case lexp instead of recomputing + it over and over again *) + let ekind = get_type ctx etype in + let elvl = match lexp'_whnf ekind ctx with + | Sort (_, Stype l) -> l + | _ -> Log.log_error ~loc:(lexp_location ekind) + "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 -> @@ -622,27 +742,46 @@ let rec check'' erased ctx e = | _,_ -> (error_tc ~loc:l "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in + let ctx_extend_with_eq ctx subst hlxp nerased = + let tlxp = mkSusp e subst in + let tltp = mkSusp etype subst in + let tlvl = mkSusp elvl subst in + let eqty = mkCall (DB.type_eq, + [(Aerasable, tlvl); (* Typelevel *) + (Aerasable, tltp); (* Inductive type *) + (Anormal, hlxp); (* Lexp of the branch head *) + (Anormal, tlxp)]) in (* Target lexp *) + (* The eq proof is erasable. *) + let nerased = dbset_push Aerasable nerased in + let nctx = DB.lexp_ctx_cons ctx (l, None) Variable eqty in + (nerased, nctx) in SMap.iter (fun name (l, vdefs, branch) -> let fieldtypes = SMap.find name constructors in - let rec mkctx erased ctx s vdefs fieldtypes = + let rec mkctx erased ctx s hlxp vdefs fieldtypes = match vdefs, fieldtypes with - | [], [] -> (erased, ctx) + | [], [] -> (erased, ctx, hlxp) (* FIXME: If ak is Aerasable, make sure the var only * appears in type annotations. *) | (ak, vdef)::vdefs, (ak', vdef', ftype)::fieldtypes -> mkctx (dbset_push ak erased) (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) - (S.cons (mkVar (vdef, 0)) - (S.mkShift s 1)) + (ssink vdef s) + (mkCall (mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) vdefs fieldtypes | _,_ -> (error_tc ~loc:l "Wrong number of args to constructor!"; - (erased, ctx)) in - let (nerased, nctx) = mkctx erased ctx s vdefs fieldtypes in + (erased, ctx, hlxp)) in + let hctor = + 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 + let subst = S.shift (List.length vdefs) in + let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp nerased in assert_type nctx branch (check nerased nctx branch) - (mkSusp ret (S.shift (List.length fieldtypes)))) + (mkSusp ret (S.shift ((List.length fieldtypes) + 1)))) branches; let diff = SMap.cardinal constructors - SMap.cardinal branches in (match default with @@ -650,8 +789,13 @@ let rec check'' erased ctx e = -> if diff <= 0 then warning_tc ~loc:l "Redundant default clause"; let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in - assert_type nctx d (check (DB.set_sink 1 erased) nctx d) - (mkSusp ret (S.shift 1)) + let nerased = DB.set_sink 1 erased in + let subst = S.shift 1 in + let hlxp = mkVar ((l, None), 0) in + let (nerased, nctx) = + ctx_extend_with_eq nctx subst hlxp nerased in + assert_type nctx d (check nerased nctx d) + (mkSusp ret (S.shift 2)) | None -> if diff > 0 then error_tc ~loc:l ("Non-exhaustive match: " @@ -697,24 +841,21 @@ let rec check'' erased ctx e = check erased ctx e | MVar (_, t, _) -> push_susp t s)

-let check' ctx e = +and check' ctx e = let res = check'' DB.set_empty ctx e in (Log.stop_on_error (); res)

-let check = check' +and check ctx e = check' ctx e

(** Compute the set of free (meta)variables. **)

-let rec list_union l1 l2 = match l1 with +and list_union l1 l2 = match l1 with | [] -> l2 | (x::l1) -> list_union l1 (if List.mem x l2 then l2 else (x::l2))

-type mv_set = (scope_level * ltype * ctx_length * vname) IMap.t - (* Metavars that appear in non-erasable positions. *) - * unit IMap.t -let mv_set_empty : mv_set = (IMap.empty, IMap.empty) -let mv_set_add (ms, nes) id x : mv_set = (IMap.add id x ms, IMap.add id () nes) -let mv_set_union ((ms1, nes1) : mv_set) ((ms2, nes2) : mv_set) : mv_set +and mv_set_empty : mv_set = (IMap.empty, IMap.empty) +and mv_set_add (ms, nes) id x : mv_set = (IMap.add id x ms, IMap.add id () nes) +and mv_set_union ((ms1, nes1) : mv_set) ((ms2, nes2) : mv_set) : mv_set = (IMap.merge (fun _m oss1 oss2 -> match (oss1, oss2) with | (None, _) -> oss2 @@ -730,25 +871,19 @@ let mv_set_union ((ms1, nes1) : mv_set) ((ms2, nes2) : mv_set) : mv_set Some ss1) ms1 ms2, IMap.merge (fun _m _o1 _o2 -> Some ()) nes1 nes2) -let mv_set_erase (ms, _nes) = (ms, IMap.empty) +and mv_set_erase (ms, _nes) = (ms, IMap.empty)

-module LMap - (* Memoization table. FIXME: Ideally the keys should be "weak", but - * I haven't found any such functionality in OCaml's libs. *) - = Hashtbl.Make - (struct type t = lexp let hash = Hashtbl.hash let equal = (==) end) -let fv_memo = LMap.create 1000 +and fv_memo = LMap.create 1000

-let fv_empty = (DB.set_empty, mv_set_empty) -let fv_union (fv1, mv1) (fv2, mv2) +and fv_empty = (DB.set_empty, mv_set_empty) +and fv_union (fv1, mv1) (fv2, mv2) = (DB.set_union fv1 fv2, mv_set_union mv1 mv2) -let fv_sink n (fvs, mvs) = (DB.set_sink n fvs, mvs) -let fv_hoist n (fvs, mvs) = (DB.set_hoist n fvs, mvs) -let fv_erase (fvs, mvs) = (fvs, mv_set_erase mvs) +and fv_sink n (fvs, mvs) = (DB.set_sink n fvs, mvs) +and fv_hoist n (fvs, mvs) = (DB.set_hoist n fvs, mvs) +and fv_erase (fvs, mvs) = (fvs, mv_set_erase mvs)

-let rec fv (e : lexp) : (DB.set * mv_set) = - let fv' e = - match lexp_lexp' e with +and fv (e : lexp) : (DB.set * mv_set) = + let fv' e = match lexp_lexp' e with | Imm _ -> fv_empty | SortLevel SLz -> fv_empty | SortLevel (SLsucc e) -> fv e @@ -800,9 +935,9 @@ let rec fv (e : lexp) : (DB.set * mv_set) = -> let s = fv_union (fv e) (fv_erase (fv t)) in let s = match def with | None -> s - | Some (_, e) -> fv_union s (fv_hoist 1 (fv e)) in + | Some (_, e) -> fv_union s (fv_hoist 2 (fv e)) in SMap.fold (fun _ (_, fields, e) s - -> fv_union s (fv_hoist (List.length fields) (fv e))) + -> fv_union s (fv_hoist (List.length fields + 1) (fv e))) cases s | Metavar (id, s, name) -> (match metavar_lookup id with @@ -822,7 +957,7 @@ let rec fv (e : lexp) : (DB.set * mv_set) = (** Finding the type of a expression. **) (* This should never signal any warning/error. *)

-let rec get_type ctx e = +and get_type ctx e = match lexp_lexp' e with | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int @@ -948,7 +1083,7 @@ let rec erase_type (lxp: lexp): E.elexp =

| L.Case(l, target, _, cases, default) -> E.Case(l, (erase_type target), (clean_map cases), - (clean_maybe default)) + (clean_default default))

| L.Susp(l, s) -> erase_type (L.push_susp l s)

@@ -977,10 +1112,12 @@ and filter_arg_list lst = and clean_decls decls = List.map (fun (v, lxp, _) -> (v, (erase_type lxp))) decls

-and clean_maybe lxp = - match lxp with - | Some (v, lxp) -> Some (v, erase_type lxp) - | None -> None +and clean_default lxp = + match lxp with + | Some (v, lxp) -> + Some (v, + erase_type (L.push_susp lxp (S.substitute DB.type0))) + | None -> None

and clean_map cases = let clean_arg_list lst = @@ -994,7 +1131,8 @@ and clean_map cases = clean_arg_list lst [] in

SMap.map (fun (l, args, expr) - -> (l, (clean_arg_list args), (erase_type expr))) + -> (l, (clean_arg_list args), + erase_type (L.push_susp expr (S.substitute DB.type0)))) cases

(** Turning a set of declarations into an object. **)

===================================== src/unification.ml ===================================== @@ -291,16 +291,35 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) | lxp' when occurs_in idx lxp' -> [(CKimpossible, ctx, lxp1, lxp2)] | lxp' -> metavar_table := associate idx lxp' (!metavar_table); - match unify t (OL.get_type ctx lxp) ctx with - | [] as r -> r - (* FIXME: Let's ignore the error for now. *) - | _ - -> log_info ?loc:None - ("Unification of metavar type failed:\n " - ^ lexp_string t ^ " != " - ^ lexp_string (OL.get_type ctx lxp) - ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); - [(CKresidual, ctx, lxp1, lxp2)] in + let type_unif_residue = + match unify t (OL.get_type ctx lxp) ctx with + | [] as r -> r + (* FIXME: Let's ignore the error for now. *) + | _ + -> log_info ?loc:None + ("Unification of metavar type failed:\n " + ^ lexp_string t ^ " != " + ^ lexp_string (OL.get_type ctx lxp) + ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); + [(CKresidual, ctx, lxp1, lxp2)] in + (* FIXME Here, we unify lxp1 with lxp2 again, because that + the metavariables occuring in the associated term might + have different substitutions from the corresponding + metavariables on the other side (due to subst inversion + not being a perfect inverse of subtitution application). + + For example, when unifying `?τ↑1[114]` with `(List[56] + ?ℓ↑0[117] ?a↑0[118])`, we associate the metavar ?τ[114] + with the lexp `(List[55] ?ℓ() · ↑0[117] ?a() · ↑0[118])` + (after applying the inverse substitution of ↑1), and the + lexp (?τ↑1[114]) becomes `(List[56] ?ℓ(↑1 () · ↑0)[117] + ?a(↑1 () · ↑0)[118])`, which is not exactly the same as + the right-hand side. My solution/kludge to this problem is + to do a second unification to fix the metavar + substitutions on the right-hand side, but there is + probably a cleaner way to solve this. *) + let second_unif_residue = unify lxp1 lxp2 ctx in + List.append type_unif_residue second_unif_residue in match lexp_lexp' lxp2 with | Metavar (idx2, s2, name) -> if idx = idx2 then

===================================== tests/elab_test.ml ===================================== @@ -72,4 +72,72 @@ example2 : alwaysbool (box Int); example2 = true; |}

+let _ = add_elab_test_decl + "depelim with Nats" + {| +type Nat + | Z + | S Nat; + +Nat_induction : + (P : Nat -> Type_ ?l) ≡> + P Z -> + ((n : Nat) -> P n -> P (S n)) -> + ((n : Nat) -> P n); +Nat_induction base step n = + ##case_ (n + | Z => Eq_cast (p := ##DeBruijn 0) (f := P) base + | S n' => Eq_cast (p := ##DeBruijn 0) (f := P) (step n' (Nat_induction (P := P) base step n'))); + +plus : Nat -> Nat -> Nat; +plus x y = + case x + | Z => y + | S x' => S (plus x' y); + ++0_identity : (n : Nat) -> Eq (plus n Z) n; ++0_identity = + Nat_induction + (P := (lambda n -> Eq (plus n Z) n)) + Eq_refl + (lambda n-1 n-1+0=n-1 -> + Eq_cast + (p := n-1+0=n-1) + (f := lambda n-1_n -> Eq (S (plus n-1 Z)) (S n-1_n)) + Eq_refl); + |} + +let _ = add_elab_test_decl + "case conversion" + {| +unify = + macro ( + lambda sxps -> + do {vname <- gensym (); + IO_return + (quote ((uquote vname) : (uquote (Sexp_node (Sexp_symbol "##Eq") sxps)); + (uquote vname) = Eq_refl; + )); + }); + +case_ = ##case_; + +type Nat + | S Nat + | Z; + +plus : ?; +plus x y = + case x + | Z => y + | S n => S (plus n y); + +f x y b = + case b + | true => plus x y + | false => Z; + +unify (f Z (S Z)) (f (S Z) Z); + |} + let _ = run_all ()

===================================== tests/eval_test.ml ===================================== @@ -427,7 +427,7 @@ Not prop = (contra : prop) ≡> False; head : (ls : List ?τ) -> (p : Not (Eq nil ls)) -> ?τ; head ls p = ##case_ (ls - | nil => unvoid (##DeBruijn 0) + | nil => unvoid (p (contra := (##DeBruijn 0))) | cons x xs => x);

l = (cons 0 nil);

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/a5a05e7b3285a8abe9bfb12788023aa98...