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

Commits: 71d21e7e by Jean-Alexandre Barszcz at 2020-12-01T14:45:35-05:00 * src/opslexp.ml (clean_decls): Oops, make it check for metavars.

- - - - - 06fa7a53 by Jean-Alexandre Barszcz at 2020-12-01T14:45:35-05:00 * src/elab.ml (sform_letin): Remove unnecessary scope_level bump.

- - - - - f9676605 by Jean-Alexandre Barszcz at 2020-12-01T14:45:35-05:00 * src/elab.ml (sform_letin): Make `let` bidirectional.

- - - - - d8893681 by Jean-Alexandre Barszcz at 2020-12-01T14:45:36-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 ===================================== @@ -1788,11 +1788,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 ===================================== @@ -973,11 +973,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 association, we check that no free + metavars are actually associated. For this to work, we assume + that the table changes monotonously: metavariables can be + associated, but the associations 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

@@ -1184,6 +1195,9 @@ let erase_type lxp = ("Metavariables in erase_type :"); erase_type lxp

+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/0b414a4694f0f468b0534f003d03de675...