From a6d137969a2ddf44f2a51b3465dc62584ca1c026 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 11 Jun 2018 01:56:11 +0200 Subject: [native_compute] Delay computations with toplevel match This is an easy improvement on examples like: Fixpoint zero (n : nat) := match n with | O => O | S p => zero p + zero p end. Definition foo := if true then zero 100 else 0. Eval native_compute in if true then 0 else foo. I didn't add a test case, because our current testing infrastructure is too fragile for that. --- kernel/nativelambda.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 0325a00b4..3736a0f9a 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -432,7 +432,6 @@ module Renv = r end -(* What about pattern matching ?*) let is_lazy prefix t = match kind t with | App (f,args) -> @@ -448,7 +447,7 @@ let is_lazy prefix t = with Not_found -> true) | _ -> true end - | LetIn _ -> true + | LetIn _ | Case _ | Proj _ -> true | _ -> false let evar_value sigma ev = sigma.evars_val ev -- cgit v1.2.3