diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-06-11 01:56:11 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-11 01:56:11 +0200 |
commit | a6d137969a2ddf44f2a51b3465dc62584ca1c026 (patch) | |
tree | 570c46a316306e180933fd744c48f15825af22ab | |
parent | 51a56b1aacb516af513de64c00dd7e796f661484 (diff) |
[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.
-rw-r--r-- | kernel/nativelambda.ml | 3 |
1 files changed, 1 insertions, 2 deletions
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 |