Stefan pushed to branch master at Stefan / Typer

Commits: 31c63489 by Stefan Monnier at 2016-10-28T23:55:25-04:00 * src/lparse.ml (_lexp_p_infer): Fix return type of `Let`

* src/opslexp.ml (lexp_defs_subst): New function. (lexp_whnf): Return original exp in `Case`. Complete commented out `Let` case.

* tests/eval_test.ml ("Let2"): New test.

- - - - -

3 changed files:

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

Changes:

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -233,11 +233,12 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = (make_var name (-1) loc), dltype))

(* Let, Variable declaration + local scope. *) - | Plet(loc, decls, body) - -> let decls, nctx = _lexp_decls decls ctx trace in + | Plet (loc, decls, body) + -> let declss, nctx = _lexp_decls decls ctx trace in let bdy, ltp = lexp_infer body nctx in - (* FIXME: Bring `ltp` back from `nctx` scope to `ctx` scope! *) - (lexp_let_decls decls bdy nctx trace), ltp + let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in + (lexp_let_decls declss bdy nctx trace), + mkSusp ltp s

(* ------------------------------------------------------------------ *) | Parrow (kind, ovar, tp, loc, expr) @@ -334,7 +335,6 @@ let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype =

| Phastype (_, pxp, ptp) -> let ltp = lexp_type_infer ptp ctx None trace in - (* FIXME: Check proper type! *) (_lexp_p_check pxp ltp ctx trace), ltp

| _ -> pexp_fatal tloc p "Unhandled Pexp"

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -113,6 +113,11 @@ and conv_p' (s1:lexp S.subst) (s2:lexp S.subst) e1 e2 : bool =

and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2

+(* Extend a substitution S with a (mutually recursive) set + * of definitions DEFS. *) +let lexp_defs_subst l s defs = + List.fold_left (fun s (_, lexp, _) -> S.cons (Let (l, defs, lexp)) s) + s defs

(* Reduce to weak head normal form. * WHNF implies: @@ -131,7 +136,6 @@ and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2 * return value as little as possible since WHNF will inherently introduce * call-by-name behavior. *) let rec lexp_whnf e (ctx : DB.lexp_context) = match e with - (* | Let (_, defs, body) -> FIXME!! Need recursive substitutions! *) | Var v -> (match lookup_value ctx v with | None -> e (* We can do this blindly even for recursive definitions! @@ -175,7 +179,17 @@ let rec lexp_whnf e (ctx : DB.lexp_context) = match e with (match e' with | Cons (_, (_, name)) -> reduce name [] | Call (Cons (_, (_, name)), aargs) -> reduce name aargs - | _ -> Case (l, e', rt, branches, default)) + | _ -> Case (l, e, rt, branches, default)) + + (* FIXME: + * - This should be correct, but requires improvements in conv_p + * to avoid inf-looping! + * - I'd really prefer to use "native" recursive substitutions, using + * ideally a trick similar to the db_offsets in lexp_context! + * + * | Let (l, defs, body) + * -> push_susp body (lexp_defs_subst l S.identity defs) *) + | e -> e

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -82,6 +82,15 @@ let _ = test_eval_eqv_named "let a = 10; x = 50; y = 60; b = 20; in a + b;" (* == *) "30"

+let _ = test_eval_eqv_named + "Let2" + + "c = 3; e = 1; f = 2; d = 4;" + + "let TrueProp = inductive_ TrueProp I; I = inductive-cons TrueProp I; + x = let a = 1; b = 2 in I + in (case x | I => c) : Int;" (* == *) "3" + (* Lambda * ------------------------ *)

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