Simon Génier pushed to branch master at Stefan / Typer
Commits: 0590a584 by Simon Génier at 2021-04-04T21:50:28-04:00 Use the environment augmented with the new bindings for type erasure.
- - - - - b3886bc0 by Simon Génier at 2021-04-04T21:51:47-04:00 Remove a test testing incorrect code.
- - - - - 0e3dcf79 by Simon Génier at 2021-04-05T00:18:00-04:00 Merge branch 'broken-tests-2021-04'
- - - - -
2 changed files:
- src/eval.ml - tests/eval_test.ml
Changes:
===================================== src/eval.ml ===================================== @@ -1171,8 +1171,9 @@ let from_lctx (lctx: lexp_context): runtime_env = let _ = (* FIXME: Evaluate those defs that we can, even if not all defs * are present! *) + let lctx' = DB.lctx_extend_rec lctx defs in if alldefs && closed_p rctx (OL.fv_hoist (List.length defs) fvs) then - List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx e) nrctx) evs + List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx' e) nrctx) evs else () in nrctx and from_lctx lctx =
===================================== tests/eval_test.ml ===================================== @@ -86,18 +86,6 @@ let _ = test_eval_eqv_named x = let a = 1; b = 2 in I in (case x | I => c);" (* == *) "3"
-let _ = test_eval_eqv_named - "Let3" - - "c = 3; e = 1; f = 2; d = 4;" - - "let TrueProp : Type; - I : TrueProp; - TrueProp = typecons TrueProp I; - I = datacons TrueProp I; - x = let a = 1; b = 2 in I - in (case x | I => c);" (* == *) "3" - let _ = test_eval_eqv_named "Let-erasable"
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/424af536858c8f2c3e00bd88f0db25725...
Afficher les réponses par date