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

Commits: bc81cad7 by Jean-Alexandre Barszcz at 2020-11-05T14:13:57-05:00 * src/opslexp.ml (clean_map): Fix the erasure of Case expressions.

Substitute the erased variables in the branch bodies.

* tests/eval_test.ml: Test the fix.

- - - - - 9111345b by Jean-Alexandre Barszcz at 2020-11-05T14:15:56-05:00 * src/opslexp.ml: Name the substitute dummy used for erasure.

(erasure_dummy): The new dummy.

(erase_type, clean_default, clean_map): Use it.

- - - - - e04cd437 by Jean-Alexandre Barszcz at 2020-11-05T14:16:00-05:00 * tests/utest_main.ml (main): Quote arguments to system commands.

This make it possible to focus on tests that have spaces in their title.

- - - - - 44b54d2a by Jean-Alexandre Barszcz at 2020-11-05T14:16:00-05:00 * src/opslexp.ml (erase_type): Fail for all (even erased) metavars.

* btl/builtins.typer (Eq_comm): Correct the FIXME.

- - - - - 98183f18 by Jean-Alexandre Barszcz at 2020-11-05T14:16:00-05:00 * src/elab.ml (sform_load): Raise error when file is not found.

- - - - - eab5fa77 by Jean-Alexandre Barszcz at 2020-11-05T14:16:00-05:00 * src/elab.ml (move_typelevel_to_front -> sort_generalized_metavars)

Replace `move_typelevel_to_front` with the new function `sort_generalized_metavars`, which, in addition to bringing the typelevel parameters to the front, sorts the remaining generalized metavariables topologically so that later variables can depend on ealier ones, and ignores metavariables that are in lower scope levels.

(generalize): Call the new function.

- - - - - 7bcbc61e by Jean-Alexandre Barszcz at 2020-11-05T14:16:00-05:00 * src/lexp.ml (hc_eq, eq): Catch exception from `List.for_all2`.

- - - - - bb33116e by Jean-Alexandre Barszcz at 2020-11-05T14:20:44-05:00 * src/elab.ml (sform_identifier): Add error in elab of metavars.

Add a FIXME and an internal error instead of using a wrong substitution in the elaboration of a repeated metavariable.

- - - - - 0b414a46 by Jean-Alexandre Barszcz at 2020-11-05T14:20:44-05:00 * src/opslexp.ml (eq_cast_whnf): New, adds WHNF for `Eq.cast`.

(lexp_whnf_aux): Add the reduction of calls to builtins, for registered builtins.

* tests/elab_test.ml: Test the WHNF of `Eq.cast`.

- - - - -

7 changed files:

- btl/builtins.typer - src/elab.ml - src/lexp.ml - src/opslexp.ml - tests/elab_test.ml - tests/eval_test.ml - tests/utest_main.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -63,10 +63,11 @@ Eq_cast = Built-in "Eq.cast"; %% Eq_comm : Eq ?x ?y -> Eq ?y ?x`; Eq_comm : (x : ?t) ≡> (y : ?t) ≡> Eq x y -> Eq y x; Eq_comm p = Eq_cast (f := lambda xy -> Eq xy x) - %% FIXME: The code is incorrectly accepted even without - %% this `(p := p)` because we just get a metavar which - %% remains uninstantiated and undetected (and then gets - %% throw away by erasure)! + %% FIXME: The code is incorrectly accepted even + %% without this `(p := p)` because we just get a + %% metavar which remains uninstantiated and then + %% the definition gets ignored in the runtime + %% environment (see Eval.from_lctx). (p := p) Eq_refl;

===================================== src/elab.ml ===================================== @@ -480,16 +480,37 @@ let rec meta_to_var ids (e : lexp) = | _ -> mkMetavar (id, adjust_subst o s, name) in loop 0 e

-let move_typelevel_to_front ctx mfvs = - (* TypeLevel arguments have to come first, so move them accordingly. *) - List.sort - (fun (id1, vname1, mt1) (id2, vname2, mt2) - -> let tl1 = OL.conv_p ctx mt1 type_level in - let tl2 = OL.conv_p ctx mt2 type_level in - if tl1 - then if tl2 then 0 else -1 - else if tl2 then 1 else 0) - mfvs +let sort_generalized_metavars sl cl ctx mfvs = + (* TypeLevel parameters have to come first, and the metavariables + must be sorted topologically, so that the type of a parameter can + only refer to earlier parameters. + + We do a DFS through the metavariable types to sort them and we + store any TypeLevel argument in a separate list. *) + let rec handle_metavar id (sl', mt, cl', vname) (* The metavar *) + ((typelevels, (* The front of the list (in reverse) *) + params, (* The rest of the list (in reverse) *) + seen) (* The set of indices already added to the lists *) + as acc) = + if sl' < sl || (* This metavar appears in the context, so we can't + generalize over it. *) + (IMap.mem id seen) (* We've already handled this metavar, skip it. *) + then acc else + (assert (cl' >= cl); + let mt = if cl' > cl then + Inverse_subst.apply_inv_subst mt (S.shift (cl' - cl)) + else mt in + let mv = (id, vname, mt) in + if (OL.conv_p ctx mt type_level) then + ((mv :: typelevels), params, (IMap.add id () seen)) + else + let (_, (mt_mfvs, _)) = OL.fv mt in + let (typelevels, params, seen) = handle_metavars mt_mfvs acc in + (typelevels, mv :: params, (IMap.add id () seen)) + ) + and handle_metavars ids acc = IMap.fold handle_metavar ids acc in + let (typelevels, params, _) = handle_metavars mfvs ([], [], IMap.empty) in + List.append (List.rev typelevels) (List.rev params)

(* Generalize expression `e` with respect to its uninstantiated metavars.. * `wrap` is the function that adds the relevant quantification, typically @@ -502,24 +523,9 @@ let generalize (nctx : elab_context) e = if mfvs = IMap.empty then (fun wrap e -> e) (* Nothing to generalize, yay! *) else - let mfvs = IMap.fold (fun idx (sl', mt, cl', vname) fvs - -> if sl' < sl then - (* This metavar appears in the context, - * so we can't generalize over it. *) - fvs - else ( - assert (cl' >= cl); - (idx, vname, - if cl' > cl then - Inverse_subst.apply_inv_subst - mt (S.shift (cl' - cl)) - else - mt) - :: fvs)) - mfvs [] in - (* FIXME: Sort `mvfs' topologically! *) + (* Sort `mvfs' topologically, and bring typelevel args to the front *) + let mfvs = sort_generalized_metavars sl cl (ectx_to_lctx nctx) mfvs in let len = List.length mfvs in - let mfvs = move_typelevel_to_front (ectx_to_lctx nctx) mfvs in fun wrap e -> let rec loop ids n mfvs = assert (n = IMap.cardinal ids); @@ -1643,7 +1649,22 @@ let sform_identifier ctx loc sargs ot = let subst = S.shift ctx_shift in let (_, _, rmmap) = ectx_get_scope ctx in if not (name = "") && SMap.mem name (!rmmap) then - (mkMetavar (SMap.find name (!rmmap), subst, (loc, Some name)), Lazy) + let idx = SMap.find name (!rmmap) in + match (metavar_lookup idx) with + | MVar (sl',_,_) + -> if sl = sl' then + (mkMetavar (idx, subst, (loc, Some name)), Lazy) + else + (* FIXME: The variable is from another scope_level! It + means that `subst` is not the right substitution for + the metavar! *) + fatal ~loc ("Bug in the elaboration of a metavar" + ^ " repeated at a different scope level!") + | MVal _ + -> (* FIXME: We face the same problem as above, but here, + the situation is worse, we don't even know the scope + level! *) + fatal ~loc "Bug in the elaboration of a repeated metavar!" else let t = match ot with | None -> newMetatype octx sl loc @@ -1841,7 +1862,11 @@ let in_pervasive = ref true let sform_load usr_elctx loc sargs ot =

let read_file file_name elctx = - let pres = prelex_file file_name in + let pres = + try prelex_file file_name with + | Sys_error _ + -> error ~loc + ("Could not load `" ^ file_name ^ "`: file not found."); [] in let sxps = lex default_stt pres in let _, elctx = lexp_p_decls [] sxps elctx in elctx in

===================================== src/lexp.ml ===================================== @@ -252,7 +252,7 @@ let lexp'_hash (lp : lexp') = (* Equality function for hash table * using physical equality for "sub-lexp" and compare for `subst`. *) let hc_eq e1 e2 = - match (lexp_lexp' e1, lexp_lexp' e2) with + try match (lexp_lexp' e1, lexp_lexp' e2) with | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 | (Imm (Float (_, x1)), Imm (Float (_, x2))) -> x1 = x2 | (Imm (String (_, s1)), Imm (String (_, s2))) -> s1 = s2 @@ -294,6 +294,8 @@ let hc_eq e1 e2 = | (Metavar (i1, s1, _), Metavar (i2, s2, _)) -> i1 = i2 && compare s1 s2 = 0 | _ -> false + with + | Invalid_argument _ -> false (* Different lengths in List.for_all2. *)

module WHC = Weak.Make (struct type t = lexp let equal x y = hc_eq x y @@ -1119,7 +1121,7 @@ and lexp_str_decls ctx decls = (** Syntactic equality (i.e. without β). *******)

let rec eq e1 e2 = - e1 == e2 || + try e1 == e2 || match (lexp_lexp' e1, lexp_lexp' e2) with | (Imm s1, Imm s2) -> sexp_equal s1 s2 | (SortLevel SLz, SortLevel SLz) -> true @@ -1171,6 +1173,8 @@ let rec eq e1 e2 = | MVal l -> eq e1 (push_susp l s2) | _ -> false) | _ -> false + with + | Invalid_argument _ -> false (* Different lengths in List.for_all2. *)

and subst_eq s1 s2 = s1 == s2 ||

===================================== src/opslexp.ml ===================================== @@ -54,10 +54,17 @@ module LMap = Hashtbl.Make (struct type t = lexp let hash = Hashtbl.hash let equal = (==) end)

+let reducible_builtins + = ref (SMap.empty : (DB.lexp_context + -> (P.arg_kind * lexp) list (* The builtin's args *) + -> lexp option) SMap.t) + let error_tc = Log.log_error ~section:"TC" let warning_tc = Log.log_warning ~section:"TC"

-(* `conv_erase` is supposed to be safe according to the ICC papers. *) +(* `conv_erase` is supposed to be safe according to the ICC papers. + It might be incompatible with the reduction of `Eq.cast`, though. See : + https://mailman.iro.umontreal.ca/pipermail/typer/2020-October/000870.html *) let conv_erase = true (* Makes conv ignore erased terms. *)

(* `impredicative_erase` is inconsistent: as shown in samples/hurkens.typer @@ -175,6 +182,10 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = args)) ctx | Call (f', xs1) -> mkCall (f', List.append xs1 xs) + | Builtin ((_, name), _, _) + -> (match SMap.find_opt name (!reducible_builtins) with + | Some f -> U.option_default e (f ctx args) + | None -> e) | _ -> e) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> let e' = lexp_whnf_aux e ctx in @@ -239,6 +250,22 @@ and lexp'_whnf e (ctx : DB.lexp_context) : lexp' = and lexp_whnf e (ctx : DB.lexp_context) : lexp = lexp_whnf_aux e ctx

+and eq_cast_whnf ctx args = + match args with + | [_l; _t; _x; _y; (_, p); _f; (_, fx)] + -> (match lexp'_whnf p ctx with + | Call (refl, _) when conv_p ctx refl DB.eq_refl + -> Some (lexp_whnf fx ctx) + | _ -> None) + | _ -> None + +and register_reducible_builtins () = + reducible_builtins := + List.fold_right + (fun (n, f) m -> SMap.add n f m) [ + ("Eq.cast", eq_cast_whnf) + ] !reducible_builtins + (** A very naive implementation of sets of pairs of lexps. *) and set_empty : set_plexp = [] and set_member_p (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool @@ -1060,8 +1087,18 @@ and get_type ctx e = | MVal e -> get_type ctx (push_susp e s) | MVar (_, t, _) -> push_susp t s)

+(* FIXME: Remove the mutual recursion between `lexp_whnf` and + `get_type`, and move this closer to the `lexp_whnf`. *) +let _ = register_reducible_builtins () + (*********** Type erasure, before evaluation. *****************)

+(* References to erasable bindings shouldn't appear in the bodies of + lexps that are being erased, but we need to adjust the debruijn + indices of other vars, hence we substitute erasable variables with + a dummy. *) +let erasure_dummy = DB.type0 + let rec erase_type (lxp: lexp): E.elexp = match lexp_lexp' lxp with | L.Imm(s) -> E.Imm(s) @@ -1069,9 +1106,7 @@ let rec erase_type (lxp: lexp): E.elexp = | L.Var(v) -> E.Var(v) | L.Cons(_, s) -> E.Cons(s) | L.Lambda (P.Aerasable, _, _, body) -> - (* The var shouldn't appear in body, basically, but we need - * to adjust the debruijn indices of other vars, hence the subst. *) - erase_type (L.push_susp body (S.substitute DB.type0)) + erase_type (L.push_susp body (S.substitute erasure_dummy)) | L.Lambda (_, vdef, _, body) -> E.Lambda (vdef, erase_type body)

@@ -1116,24 +1151,39 @@ and clean_default lxp = match lxp with | Some (v, lxp) -> Some (v, - erase_type (L.push_susp lxp (S.substitute DB.type0))) + erase_type (L.push_susp lxp (S.substitute erasure_dummy))) | None -> None

and clean_map cases = - let clean_arg_list lst = - let rec clean_arg_list lst acc = - match lst with - | (kind, var)::tl -> - let acc = if kind != P.Aerasable then - var::acc else acc in - clean_arg_list tl acc - | [] -> List.rev acc in - clean_arg_list lst [] in - - SMap.map (fun (l, args, expr) - -> (l, (clean_arg_list args), - erase_type (L.push_susp expr (S.substitute DB.type0)))) - cases + let clean_branch (l, args, expr) = + let rec clean_arg_list args acc subst = + match args with + | (P.Aerasable, _)::tl -> + (* Drop the variable and substitute it in the body. *) + clean_arg_list tl acc (S.cons erasure_dummy subst) + | (kind, var)::tl -> + (* Keep the variable and sink the substitution. *) + clean_arg_list tl (var::acc) (ssink var subst) + | [] -> + (List.rev acc, subst) in + let args, subst = clean_arg_list args [] S.identity in + let subst = (S.cons erasure_dummy subst) in (* Substitute the equality. *) + (l, args, erase_type (L.push_susp expr subst)) in + SMap.map clean_branch cases + +let erase_type lxp = + let _, (mvs, _) = fv lxp in + if not (IMap.is_empty mvs) then + Log.log_fatal + ~print_action:(fun () -> + IMap.iter (fun i (_, t, _, (l, n)) -> + print_endline ("\t" ^ (Log.string_of_location l) + ^ " ?" ^ (U.option_default "" n) + ^ "[" ^ (string_of_int i) ^ "] : " ^ (lexp_string t)) + ) mvs) + ("Metavariables in erase_type :"); + erase_type lxp +

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

===================================== tests/elab_test.ml ===================================== @@ -158,4 +158,62 @@ f x y b = unify (f Z (S Z)) (f (S Z) Z); |}

+let _ = add_elab_test_decl + "WHNF of Eq.cast" + {| +x = (4 : Int); +y = x; + +p : Eq x y; +p = Eq_refl; + +test : Eq (Eq_cast (p := p) (f := lambda _ -> Unit) ()) (); +test = Eq_refl; + |} + +let _ = add_elab_test_decl + "Decidable at the type level" + {| +Decidable = + typecons (Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ)) + (yes (p :: prop)) (no (p :: Not prop)); +yes = datacons Decidable yes; +no = datacons Decidable no; + +true≠false (p : Eq true false) = + Eq_cast (p := p) + (f := lambda tf -> case tf + | true => True + | false => False) + (); % This is unit, an inhabitant of `True`. + +false≠true (p : Eq false true) = true≠false (Eq_comm p); + +decideBoolEq : (a : Bool) => (b : Bool) => Decidable (Eq a b); +decideBoolEq = + lambda (a : Bool) (b : Bool) => + case a return (Decidable (Eq a b)) + | true => + (case b return (Decidable (Eq true b)) + | true => yes (p := Eq_refl) + | false => no (p := true≠false)) + | false => + (case b return (Decidable (Eq false b)) + | true => no (p := false≠true) + | false => yes (p := Eq_refl)); + +getProof : + (l : TypeLevel) ≡> + (prop : Type_ l) ≡> + (d : Decidable prop) -> + case d | yes => prop | no => Not prop; +getProof d = + case d return (case d | yes => prop | no => Not prop) + | yes (p := p) => p + | no (p := p) => p; + +test = + (getProof (decideBoolEq : Decidable (Eq true true)) : Eq true true); + |} + let _ = run_all ()

===================================== tests/eval_test.ml ===================================== @@ -445,6 +445,23 @@ nil≠l = |} "head l nil≠l" "0"

+let _ = test_eval_eqv_named + "Erasable cons args" + {| +P = (a : Type) ≡> a -> Not (Not a); +p : P; +p = lambda a ≡> lambda x notx -> notx x; + +tP : Decidable (ℓ := ?ℓ₀) P; +tP = (datacons (Decidable (ℓ := ?ℓ₀)) true) (prop := P) (p := p); + +res = + case tP + | (datacons ? true) (p := _) => tP % A ref to the ctx + | (datacons ? false) (p := _) => tP; + |} + "res" "tP" + let _ = add_test "EVAL" "int overflows" (fun () -> let check_op op biop a b =

===================================== tests/utest_main.ml ===================================== @@ -130,17 +130,20 @@ let main () = let exit_code = ref 0 in let failed_test = ref 0 in let tests_n = ref 0 in - let test_args = " --samples " ^ root_folder ^ - " --verbose " ^ (string_of_int !global_verbose_lvl) ^ - (if not (!global_ftitle = "") then - (" --ftitle " ^ !global_ftitle) else "") in + let test_args = + ["--samples"; root_folder; + "--verbose"; (string_of_int !global_verbose_lvl)] @ + (if not (!global_ftitle = "") then + ["--ftitle"; !global_ftitle] else []) in

List.iter (fun file -> flush stdout;

if must_run file then ( tests_n := !tests_n + 1; - exit_code := Sys.command (folder ^ file ^ test_args); + let command = String.concat " " (List.map Filename.quote + ((folder ^ file)::test_args)) in + exit_code := Sys.command command;

(if !exit_code != 0 then( (if verbose 1 then print_file_name (!tests_n) files_n file false);

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