Stefan pushed to branch master at Stefan / Typer

Commits: fbffe328 by Stefan Monnier at 2017-02-11T20:15:49-05:00 * src/debruijn.ml (lctx_view): New function

(lct_view): New type. * src/opslexp.ml (lctx_to_subst): * src/eval.ml (from_lctx): Use it.

- - - - -

4 changed files:

- src/debruijn.ml - src/eval.ml - src/inverse_subst.ml - src/opslexp.ml

Changes:

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -306,6 +306,27 @@ let env_lookup_type ctx (v : vref): lexp = let env_lookup_expr ctx (v : vref): lexp option = lctx_lookup_value (ectx_to_lctx ctx) v

+type lct_view = + | CVempty + | CVlet of vname option * varbind * ltype * lexp_context + | CVfix of (vname option * varbind * ltype) list * lexp_context + +let rec lctx_view lctx = + match lctx with + | Myers.Mnil -> CVempty + | Myers.Mcons ((0, loname, odef, t), lctx, _, _) + -> CVlet (loname, odef, t, lctx) + | Myers.Mcons ((1, loname, odef, t), lctx, _, _) + -> let rec loop i lctx defs = + match lctx with + | Myers.Mcons ((o, loname, odef, t), lctx, _, _) + when o = i + -> loop (i + 1) lctx ((loname, odef, t) :: defs) + | _ -> CVfix (defs, lctx) in + loop 2 lctx [(loname, odef, t)] + | _ -> U.internal_error "Unexpected lexp_context shape!" + + (** Sets of DeBruijn indices **)

type set = db_offset * unit VMap.t

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -645,51 +645,54 @@ let closed_p rctx (fvs, mvs) = (* FIXME: Handle metavars! *) && VMap.is_empty mvs

-let rec from_lctx meta_ctx (lctx: lexp_context): runtime_env = - (* FIXME: `eval` with a disabled runIO. *) - let from_lctx' (lctx: lexp_context): runtime_env = - match lctx with - | Myers.Mnil -> Myers.nil - | Myers.Mcons ((0, loname, def, _), lctx, _, _) - -> let rctx = from_lctx meta_ctx lctx in - Myers.cons (roname loname, - ref (match def with +let from_lctx meta_ctx (lctx: lexp_context): runtime_env = + (* FIXME: `eval` with a disabled IO.run. *) + let rec from_lctx' (lctx: lexp_context): runtime_env = + match lctx_view lctx with + | CVempty -> Myers.nil + | CVlet (loname, def, _, lctx) + -> let rctx = from_lctx lctx in + Myers.cons (roname loname, + ref (match def with + | LetDef e + -> let e = L.clean meta_ctx e in + if closed_p rctx (OL.fv e) then + eval (OL.erase_type e) rctx + else Vundefined + | _ -> Vundefined)) + rctx + | CVfix (defs, lctx) + -> let fvs = List.fold_left + (fun fvs (_, odef, _) + -> match odef with | LetDef e - -> let e = L.clean meta_ctx e in - if closed_p rctx (OL.fv e) then - eval (OL.erase_type e) rctx - else Vundefined - | _ -> Vundefined)) - rctx - | Myers.Mcons ((1, loname, LetDef e, _), lctx, _, _) - -> let rec getdefs i lctx rdefs fvs = - match lctx with - | Myers.Mcons ((o, loname, LetDef e, _), lctx, _, _) - when o = i - -> let e = L.clean meta_ctx e in - getdefs (i + 1) lctx ((loname, e) :: rdefs) - (OL.fv_union fvs (OL.fv e)) - | _ -> (lctx, rdefs, fvs) in - let (lctx, rdefs, fvs) = getdefs 2 lctx [(loname, e)] OL.fv_empty in - let rctx = from_lctx meta_ctx lctx in - let (nrctx, evs) - = List.fold_left (fun (rctx, evs) (loname, e) - -> let rc = ref Vundefined in - (Myers.cons (roname loname, rc) rctx, - (e, rc)::evs)) - (rctx, []) rdefs in - let _ = - if closed_p rctx (OL.fv_hoist (List.length rdefs) fvs) then - List.iter (fun (e, rc) -> rc := eval (OL.erase_type e) nrctx) evs - else () in - nrctx - | _ -> U.internal_error "Unexpected lexp_context shape!" - in - try CMap.find ctx_memo lctx - with Not_found - -> let r = from_lctx' lctx in - CMap.add ctx_memo lctx r; - r + -> OL.fv_union fvs (OL.fv (L.clean meta_ctx e)) + | _ -> fvs) + OL.fv_empty + defs in + let rctx = from_lctx lctx in + let (nrctx, evs, alldefs) + = List.fold_left (fun (rctx, evs, alldefs) (loname, odef, _) + -> let rc = ref Vundefined in + let nrctx = Myers.cons (roname loname, rc) rctx in + match odef with + | LetDef e -> (nrctx, (e, rc)::evs, alldefs) + | _ -> nrctx, [], false) + (rctx, [], true) defs in + let _ = + (* FIXME: Evaluate those defs that we can, even if not all defs + * are present! *) + if alldefs && closed_p rctx (OL.fv_hoist (List.length defs) fvs) then + List.iter (fun (e, rc) -> rc := eval (OL.erase_type e) nrctx) evs + else () in + nrctx + and from_lctx lctx = + try CMap.find ctx_memo lctx + with Not_found + -> let r = from_lctx' lctx in + CMap.add ctx_memo lctx r; + r + in from_lctx lctx

(* build a rctx from a ectx. *) let from_ectx meta_ctx (ctx: elab_context): runtime_env =

===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -1,6 +1,6 @@ (* inverse_subst.ml --- Computing the inverse of a substitution

-Copyright (C) 2016 Free Software Foundation, Inc. +Copyright (C) 2016-2017 Free Software Foundation, Inc.

Author: Vincent Bonnevalle tiv.crb@gmail.com

@@ -29,6 +29,14 @@ this program. If not, see http://www.gnu.org/licenses/. *) * X = e[σ⁻¹] * * where σ⁻¹ is such that e[σ⁻¹][σ] = e[σ⁻¹ ∘ σ] = e + * + * Another way to look at it is that + * + * X[σ] = e ==> X[σ][σ⁻¹] = e[σ⁻¹] + * + * so if we can find a σ⁻¹ such that σ ∘ σ⁻¹ = Id, e have X = e[σ⁻¹] + * + * So either left or right inverse can be used! *)

open Lexp

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -1,6 +1,6 @@ (* opslexp.ml --- Operations on Lexps

-Copyright (C) 2011-2016 Free Software Foundation, Inc. +Copyright (C) 2011-2017 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -72,30 +72,28 @@ let rec lexp_defs_subst l s defs = match defs with (** Convert a lexp_context into a substitution. *)

let rec lctx_to_subst lctx = - match lctx with - | Myers.Mnil -> Subst.identity - | Myers.Mcons ((0, _, LetDef e, _), lctx, _, _) + match DB.lctx_view lctx with + | DB.CVempty -> Subst.identity + | DB.CVlet (_, LetDef e, _, lctx) -> let s = lctx_to_subst lctx in - L.scompose (S.substitute e) s - | Myers.Mcons ((0, ov, _, _), lctx, _, _) + L.scompose (S.substitute e) s + | DB.CVlet (ov, _, _, lctx) -> let s = lctx_to_subst lctx in - (* Here we decide to keep those vars in the target domain. - * Another option would be to map them to `L.impossible`, - * hence making the target domain be empty (i.e. making the substitution - * generate closed results). *) - L.ssink (maybev ov) s - | Myers.Mcons ((1, ov, LetDef e, t), lctx, _, _) - -> let rec getdefs i lctx rdefs = - match lctx with - | Myers.Mcons ((o, ov, LetDef e, t), lctx, _, _) - when o = i - -> getdefs (i + 1) lctx ((maybev ov, e, t) :: rdefs) - | _ -> (lctx, List.rev rdefs) in - let (lctx, defs) = getdefs 2 lctx [(maybev ov, e, t)] in - let s1 = lctx_to_subst lctx in - let s2 = lexp_defs_subst DB.dloc S.identity defs in - L.scompose s2 s1 - | _ -> U.internal_error "Unexpected lexp_context shape!" + (* Here we decide to keep those vars in the target domain. + * Another option would be to map them to `L.impossible`, + * hence making the target domain be empty (i.e. making the substitution + * generate closed results). *) + L.ssink (maybev ov) s + | DB.CVfix (defs, lctx) + -> let s1 = lctx_to_subst lctx in + let s2 = lexp_defs_subst DB.dloc S.identity + (List.map (fun (oname, odef, t) + -> (maybev oname, + (match odef with LetDef e -> e + | _ -> L.impossible), + t)) + (List.rev defs)) in + L.scompose s2 s1

(* Take an expression `e` that is "closed" relatively to context lctx * and return an equivalent expression valid in the empty context.

View it on GitLab: https://gitlab.com/monnier/typer/commit/fbffe328a3fe059cd96b260f136258a8f43c...