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

Commits: 8741ee4f by Jean-Alexandre Barszcz at 2021-01-04T18:30:51-05:00 * src/opslexp.ml (clean_decls): Oops, make it check for metavars.

- - - - - 14d0ad7a by Jean-Alexandre Barszcz at 2021-01-04T18:30:51-05:00 * src/elab.ml (sform_letin): Remove unnecessary scope_level bump.

- - - - - 1c6e109b by Jean-Alexandre Barszcz at 2021-01-04T18:30:51-05:00 * src/elab.ml (sform_letin): Make `let` bidirectional.

- - - - - fecec539 by Jean-Alexandre Barszcz at 2021-01-04T18:30:51-05:00 * src/opslexp.ml (fv): Check that the memoized value is still ok.

- - - - -

2 changed files:

- src/elab.ml - src/opslexp.ml

Changes:

===================================== 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 ===================================== @@ -975,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

@@ -1173,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 @@ -1186,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. **)

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