diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-16 12:52:13 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-16 15:22:36 +0100 |
| commit | 364decf59c14ec8a672d3c4d46fa1939ea0e52d3 (patch) | |
| tree | fd774da7b8f5b98f7e8fe47a2065881e6bc85aee /intf/genredexpr.mli | |
| parent | 4c576db3ed40328caa37144eb228365f497293e5 (diff) | |
Enforcing a stronger difference between the two syntaxes "simpl
reference" and "simpl pattern" in the code (maybe we should have
merged them instead, but I finally decided to enforce their
difference, even if some compatibility is to be preversed - the idea
is that at some time "simpl reference" would only call a weak-head
simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n)
rather than S(S(n)) which could be useful for better using induction
hypotheses.
In the process we also implement the following:
- 'simpl "+"' is accepted to reduce all applicative subterms whose
head symbol is written "+" (in the toplevel scope); idem for
vm_compute and native_compute
- 'simpl reference' works even if reference has maximally inserted
implicit arguments (this solves the "simpl fst" incompatibility)
- compatibility of ltac expressions referring to vm_compute and
native_compute with functor application should now work (i.e.
vm_compute and native_compute are now taken into account in
tacsubst.ml)
- for compatibility, "simpl eq" (assuming no maximal implicit args in
eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed.
By the way, is "mul" on nat defined optimally? "3*n" simplifies to
"n+(n+(n+0))". Are there some advantages of this compared to have it
simplified to "n+n+n" (i.e. to "(n+n)+n").
Diffstat (limited to 'intf/genredexpr.mli')
| -rw-r--r-- | intf/genredexpr.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli index 1096ecb1f..a59278bb0 100644 --- a/intf/genredexpr.mli +++ b/intf/genredexpr.mli @@ -32,7 +32,7 @@ type 'a glob_red_flag = { type ('a,'b,'c) red_expr_gen = | Red of bool | Hnf - | Simpl of 'c Locus.with_occurrences option + | Simpl of ('b,'c) Util.union Locus.with_occurrences option | Cbv of 'b glob_red_flag | Cbn of 'b glob_red_flag | Lazy of 'b glob_red_flag @@ -40,8 +40,8 @@ type ('a,'b,'c) red_expr_gen = | Fold of 'a list | Pattern of 'a Locus.with_occurrences list | ExtraRedExpr of string - | CbvVm of 'c Locus.with_occurrences option - | CbvNative of 'c Locus.with_occurrences option + | CbvVm of ('b,'c) Util.union Locus.with_occurrences option + | CbvNative of ('b,'c) Util.union Locus.with_occurrences option type ('a,'b,'c) may_eval = | ConstrTerm of 'a |