Stefan pushed to branch master at Stefan / Typer

Commits: d21c5eb6 by Stefan Monnier at 2018-07-25T19:13:16Z Allow `let` vars to be erasable in some circumstances

* src/opslexp.ml (nerased_let): New function. (check'): Use it. * tests/eval_test.ml ("Let-erased"): New test.

- - - - -

3 changed files:

- src/lexp.ml - src/opslexp.ml - tests/eval_test.ml

Changes:

===================================== src/lexp.ml ===================================== @@ -215,7 +215,7 @@ let mkCall (f, es) * that is transient and hence immediately GC'd. *) let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000

-(* When building the type of a tuple (x1=e1, x2=e2, ..., xn=en) +(* When computing the type of "load"ed modules * we end up building substitutions of the form * * ((Susp e3 (((Susp e2 (e1 · id)) · e1 · id) @@ -223,11 +223,18 @@ let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000 * · ((Susp e2 (e1 · id)) · e1 · id) * · e1 · id) * - * with exponential size (but lots of sharing). So it's indispensible + * with 2^n size (but lots of sharing). So it's indispensible * to memoize the computation to avoid the exponential waste of time. * - * FIXME: I still don't understand why we build substitutions - * of such a shape! *) + * This shows up because of the dependent type of `let`: + * + * let z = e₃ in e : τ[e₃/z] + * let y = e₂ in let z = e₃ in e : (τ[e₃/z])[e₂/y] = τ[(e₃[e₂/y])/z,e₂/y] + * let x = e₁ in let y = e₂ in let z = e₃ in e + * : (τ[(e₃[e₂/y])/z,e₂/y])[e₁/x] + * = τ[(e₃[(e₂[e₁/x])/y,e₁/x])/z,(e₂[e₁/x])/y,e₁/x] + * ... + *)

let rec mkSusp e s = if S.identity_p s then e else

===================================== src/opslexp.ml ===================================== @@ -366,6 +366,31 @@ let dbset_push ak erased = let nerased = DB.set_sink 1 erased in if ak = P.Aerasable then DB.set_set 0 nerased else nerased

+let nerased_let defs erased = + (* Let bindings are not erasable, with the important exception of + * let-bindings of the form `x = y` where `y` is an erasable var. + * This exception is designed so that macros like `case` which need to + * rebind variables to user-specified names can do so without having + * to pay attention to whether the var is erasable or not. + *) + (* FIXME: Maybe allow more cases of erasable let-bindings. *) + let nerased = DB.set_sink (List.length defs) erased in + let es = List.map + (fun (_v, e, _t) -> + (* Look for `x = y` where `y` is an erasable var. + * FIXME: `nerased` assumes all the vars in `defs` + * will be non-erasable, so in `let x = z; y = x ...` + * where `z` is erasable, `x` will be found + * to be erasable, but not `y`. *) + match e with Var (_, idx) -> DB.set_mem idx nerased + | _ -> false) + defs in + if not (List.mem true es) then nerased else + List.fold_left + (fun erased e + -> dbset_push (if e then P.Aerasable else P.Aexplicit) erased) + erased es + (* "check ctx e" should return τ when "Δ ⊢ e : τ" *) let rec check' erased ctx e = let check = check' in @@ -433,14 +458,17 @@ let rec check' erased ctx e = -> (let _ = check_type DB.set_empty ctx t in DB.lctx_extend ctx v ForwardRef t)) ctx defs in - (* FIXME: Allow erasable let-bindings! *) - let nerased = DB.set_sink (List.length defs) erased in + let nerased = nerased_let defs erased in let nctx = DB.lctx_extend_rec ctx defs in (* FIXME: Termination checking! Positivity-checker! *) let _ = List.fold_left (fun n (v, e, t) - -> assert_type nctx e - (push_susp t (S.shift n)) - (check nerased nctx e); + -> assert_type + nctx e + (push_susp t (S.shift n)) + (check (if DB.set_mem (n - 1) nerased + then DB.set_empty + else nerased) + nctx e); n - 1) (List.length defs) defs in mkSusp (check nerased nctx e)

===================================== tests/eval_test.ml ===================================== @@ -92,7 +92,7 @@ let _ = test_eval_eqv_named "let TrueProp = typecons TrueProp I; I = datacons TrueProp I; x = let a = 1; b = 2 in I - in (case x | I => c) : Int;" (* == *) "3" + in (case x | I => c);" (* == *) "3"

let _ = test_eval_eqv_named "Let3" @@ -104,7 +104,15 @@ let _ = test_eval_eqv_named TrueProp = typecons TrueProp I; I = datacons TrueProp I; x = let a = 1; b = 2 in I - in (case x | I => c) : Int;" (* == *) "3" + in (case x | I => c);" (* == *) "3" + +let _ = test_eval_eqv_named + "Let-erasable" + + "c = 3; e = 1; f = 2; d = 4;" + + "let id = lambda t ≡> lambda (x : t) -> x; + in (lambda t ≡> let t1 = t in id (t := t1)) 3" (* == *) "3"

(* Lambda * ------------------------ *)

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