Jean-Alexandre Barszcz pushed to branch ja/various_fixes at Stefan / Typer

Commits: c3a0c909 by Simon Génier at 2020-12-15T13:40:02-05:00 Qualify the constructors to fix warning 40.

- - - - - 88ed302a by Jean-Alexandre Barszcz at 2020-12-15T13:40:02-05:00 * src/opslexp.ml (clean_decls): Oops, make it check for metavars.

- - - - - bca144df by Jean-Alexandre Barszcz at 2020-12-15T13:40:02-05:00 * src/elab.ml (sform_letin): Remove unnecessary scope_level bump.

- - - - - 2e6e34d2 by Jean-Alexandre Barszcz at 2020-12-15T13:40:02-05:00 * src/elab.ml (sform_letin): Make `let` bidirectional.

- - - - - 4d942a98 by Jean-Alexandre Barszcz at 2020-12-15T13:40:02-05:00 * src/opslexp.ml (fv): Check that the memoized value is still ok.

- - - - -

5 changed files:

- src/REPL.ml - src/debruijn.ml - src/elab.ml - src/opslexp.ml - tests/unify_test.ml

Changes:

===================================== src/REPL.ml ===================================== @@ -66,7 +66,7 @@ let print_input_line i = let ieval_error = Log.log_error ~section:"IEVAL"

let print_and_clear_log () = - if (not Log.typer_log_config.print_at_log) then + if (not Log.typer_log_config.Log.print_at_log) then Log.print_and_clear_log ()

let handle_stopped_compilation msg =

===================================== src/debruijn.ml ===================================== @@ -43,6 +43,7 @@ module M = Myers open Fmt

module S = Subst +module P = Pexp

let fatal = Log.log_fatal ~section:"DEBRUIJN"

@@ -99,13 +100,13 @@ let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) let type_eq_type = let lv = (dloc, Some "l") in let tv = (dloc, Some "t") in - mkArrow (Aerasable, lv, + mkArrow (P.Aerasable, lv, type_level, dloc, - mkArrow (Aerasable, tv, + mkArrow (P.Aerasable, tv, mkSort (dloc, Stype (mkVar (lv, 0))), dloc, - mkArrow (Anormal, (dloc, None), + mkArrow (P.Anormal, (dloc, None), mkVar (tv, 0), dloc, - mkArrow (Anormal, (dloc, None), + mkArrow (P.Anormal, (dloc, None), mkVar (tv, 1), dloc, mkSort (dloc, Stype (mkVar (lv, 3))))))) let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) @@ -114,17 +115,17 @@ let eq_refl = let tv = (dloc, Some "t") in let xv = (dloc, Some "x") in mkBuiltin ((dloc, "Eq.refl"), - mkArrow (Aerasable, lv, + mkArrow (P.Aerasable, lv, type_level, dloc, - mkArrow (Aerasable, tv, + mkArrow (P.Aerasable, tv, mkSort (dloc, Stype (mkVar (lv, 0))), dloc, - mkArrow (Aerasable, xv, + mkArrow (P.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)]))))) + [P.Aerasable, mkVar (lv, 2); + P.Aerasable, mkVar (tv, 1); + P.Anormal, mkVar (xv, 0); + P.Anormal, mkVar (xv, 0)])))))

(* easier to debug with type annotations *)

===================================== src/elab.ml ===================================== @@ -1690,11 +1690,16 @@ let rec sform_case ctx loc sargs ot = match sargs with let sform_letin ctx loc sargs ot = match sargs with | [sdecls; sbody] -> let declss, nctx = lexp_p_decls [sdecls] [] ctx in - (* FIXME: Use `elaborate`. *) - let bdy, ltp = infer sbody (ectx_new_scope nctx) in - let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in - (lexp_let_decls declss bdy nctx, - Inferred (mkSusp ltp s)) + let s, off = + List.fold_left (fun (s, off) decls -> + (OL.lexp_defs_subst loc s decls, off + List.length decls)) + (S.identity, 0) declss in + let ot = U.option_map (fun t -> mkSusp t (S.shift off)) ot in + let bdy, ot = elaborate nctx sbody ot in + let ot = match ot with + | Inferred t -> Inferred (mkSusp t s) + | _ -> ot in + (lexp_let_decls declss bdy nctx, ot) | _ -> sexp_error loc "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc

===================================== src/opslexp.ml ===================================== @@ -194,7 +194,10 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = 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 + mkCall (DB.eq_refl, + [P.Aerasable, elevel; + P.Aerasable, etype; + P.Aerasable, e]) in let reduce it name aargs = let targs = match lexp_lexp' (lexp_whnf_aux it ctx) with | Inductive (_,_,fargs,_) -> fargs @@ -423,10 +426,10 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = 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 *) + [(P.Aerasable, tlvl); (* Typelevel *) + (P.Aerasable, tltp); (* Inductive type *) + (P.Anormal, hlxp); (* Lexp of the branch head *) + (P.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 @@ -773,12 +776,12 @@ and check'' erased ctx e = 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 *) + [(P.Aerasable, tlvl); (* Typelevel *) + (P.Aerasable, tltp); (* Inductive type *) + (P.Anormal, hlxp); (* Lexp of the branch head *) + (P.Anormal, tlxp)]) in (* Target lexp *) (* The eq proof is erasable. *) - let nerased = dbset_push Aerasable nerased in + let nerased = dbset_push P.Aerasable nerased in let nctx = DB.lexp_ctx_cons ctx (l, None) Variable eqty in (nerased, nctx) in SMap.iter @@ -972,11 +975,22 @@ and fv (e : lexp) : (DB.set * mv_set) = -> let (fvs, mvs) = fv_erase (fv (push_susp t s)) in (fvs, mv_set_add mvs id (sl, t, cl, name))) in - (* FIXME: Flush the memoization table whenever the metavar table - * is modified, since that can affect the output of `fv`. *) - try LMap.find fv_memo e - with Not_found - -> let r = fv' e in + let ofvs = LMap.find_opt fv_memo e in + (* The memoized value depends on the metavariable table. When it + changes, we have to recompute the free variables. Instead of + flushing the table after every instantiation, we check that no + free metavars are actually instantiated. For this to work, we + assume that the table changes monotonously: metavariables can be + instantiated, but the instantiations cannot be undone. *) + match ofvs with + | Some ((_, (mvfs, _)) as fvs) + when IMap.for_all + (fun mv _ -> match metavar_lookup mv with + | MVar _ -> true + | MVal _ -> false) + mvfs + -> fvs + | _ -> let r = fv' e in LMap.add fv_memo e r; r

@@ -1170,6 +1184,9 @@ and clean_map cases = (l, args, erase_type (L.push_susp expr subst)) in SMap.map clean_branch cases

+(* The following entry points to erasure, `erase_type` and + `clean_decls`, check that no metavariables are left before + performing the erasure itself. *) let erase_type lxp = let _, (mvs, _) = fv lxp in if not (IMap.is_empty mvs) then @@ -1183,6 +1200,11 @@ let erase_type lxp = ("Metavariables in erase_type :"); erase_type lxp

+(* Textually identical to the previous definition of `clean_decls`, + but calls the new `erase_type`, which checks for metavars. *) +let clean_decls decls = + List.map (fun (v, lxp, _) -> (v, (erase_type lxp))) decls +

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

===================================== tests/unify_test.ml ===================================== @@ -29,6 +29,7 @@ open Fmt open Utest_lib

module U = Util +module P = Pexp

(* default environment *) let ectx = Elab.default_ectx @@ -98,10 +99,10 @@ let _ = (fun (ectx, i) (name, lexp) -> Elab.ctx_extend ectx (dloc, Some name) Variable (shift lexp i), i + 1) (ectx, 0) - [("f", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); - ("g", (mkArrow (Anormal, (dloc, None), nat, dloc, shift nat 1))); - ("h", (mkArrow (Anormal, (dloc, Some "x"), nat, dloc, - mkArrow (Anormal, (dloc, Some "y"), shift nat 1, + [("f", (mkArrow (P.Anormal, (dloc, None), nat, dloc, shift nat 1))); + ("g", (mkArrow (P.Anormal, (dloc, None), nat, dloc, shift nat 1))); + ("h", (mkArrow (P.Anormal, (dloc, Some "x"), nat, dloc, + mkArrow (P.Anormal, (dloc, Some "y"), shift nat 1, dloc, shift nat 2)))); ("a", nat); ("b", nat)] in

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