From 364decf59c14ec8a672d3c4d46fa1939ea0e52d3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 16 Nov 2014 12:52:13 +0100
Subject: 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").
---
 grammar/q_coqast.ml4 | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

(limited to 'grammar')

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 02becc4967..d6d13375e6 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -46,6 +46,10 @@ let mlexpr_of_reference = function
   | Libnames.Ident (loc,id) ->
     let loc = of_coqloc loc in <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >>
 
+let mlexpr_of_union f g = function
+  | Util.Inl a -> <:expr< Util.Inl $f a$ >>
+  | Util.Inr b -> <:expr< Util.Inr $g b$ >>
+
 let mlexpr_of_located f (loc,x) =
   let loc = of_coqloc loc in
   <:expr< ($dloc$, $f x$) >>
@@ -184,10 +188,15 @@ let rec mlexpr_of_constr = function
 let mlexpr_of_occ_constr =
   mlexpr_of_occurrences mlexpr_of_constr
 
+let mlexpr_of_occ_ref_or_constr =
+  mlexpr_of_occurrences
+    (mlexpr_of_union
+       (mlexpr_of_by_notation mlexpr_of_reference) mlexpr_of_constr)
+
 let mlexpr_of_red_expr = function
   | Genredexpr.Red b -> <:expr< Genredexpr.Red $mlexpr_of_bool b$ >>
   | Genredexpr.Hnf -> <:expr< Genredexpr.Hnf >>
-  | Genredexpr.Simpl o -> <:expr< Genredexpr.Simpl $mlexpr_of_option mlexpr_of_occ_constr o$ >>
+  | Genredexpr.Simpl o -> <:expr< Genredexpr.Simpl $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >>
   | Genredexpr.Cbv f ->
       <:expr< Genredexpr.Cbv $mlexpr_of_red_flags f$ >>
   | Genredexpr.Cbn f ->
@@ -203,8 +212,8 @@ let mlexpr_of_red_expr = function
   | Genredexpr.Pattern l ->
       let f = mlexpr_of_list mlexpr_of_occ_constr in
       <:expr< Genredexpr.Pattern $f l$ >>
-  | Genredexpr.CbvVm o -> <:expr< Genredexpr.CbvVm $mlexpr_of_option mlexpr_of_occ_constr o$ >>
-  | Genredexpr.CbvNative o -> <:expr< Genredexpr.CbvNative $mlexpr_of_option mlexpr_of_occ_constr o$ >>
+  | Genredexpr.CbvVm o -> <:expr< Genredexpr.CbvVm $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >>
+  | Genredexpr.CbvNative o -> <:expr< Genredexpr.CbvNative $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >>
   | Genredexpr.ExtraRedExpr s ->
       <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >>
 
-- 
cgit v1.2.3