Configurable simpl tactic

The problem that this patch tries to solve is that sometimes the
unfolding behaviour of simpl is too aggressive, frequently exposing
match constructs. Moreover one may want some constants to never be
unfolded by simpl (like in the Math-Comp library where the nosimpl hack
is pervasive). Finally, one may want some constants to be volatile,
always unfolded by simple when applied to enough arguments, even if they
do not hide a fixpoint or a match.

A new vernacular command to be indroduced in a following patch attaches
to constants an extra-logical piece of information. It declares wich
arguments must be checked to evaluate to a constructor before performing
the unfolding of the constant (in the same spirit simpl considers as
such the recursive argument of an inner fixpoint).

Examples:

Arguments minus !x !y.
  (* x and y must evaluate to a constructor for simpl to unfold minus *)

  (S x - y)   --- simpl ---> (S x - y)
  (S x - S y) --- simpl ---> (x - y)

Definition fcomp A B C (f : B -> C) (g : A -> B) x := f (g x).
Arguments fcomp A B C f g x /.
Infix "\o" := fcomp (at level 50, left associativity) : nat_scope.
  (* fcomp hides no fix, but simpl will unfold if applied to 6 arguments *)

  (fun x => (f \o g) x) = f \o g  --- simpl ---> (fun x => f (g x)) = f \o g

Arguments minus x y : simpl never.
  (* simpl will never unfold minus *)

  (S x - S y) --- simpl ---> (S x - S y)

Definition nid (x : nat) := x.
Arguments nid / x.
  (* nid is volatile, unfolded by simpl when applied to 0 or more arguments *)

  nid   --- simpl ---> (fun x => x)

Arguments minus x y : simpl nomatch.
  (* triggers for minus the "new" simpl heuristic I discussed with Hugo:

       if reducing the fix would leave a match in "head" position
       then don't unfold

     a suggestion for a better name (for "nomatch") would be appreciated *)

  (0 - y)  --- simpl ---> 0
  (S x - y)  --- simpl ---> (S x - y)
  (S x - S y) --- simpl ---> (x - y)

  (minus 0) --- simpl ---> (minus 0)

  (* This last test does not work as one may expect, i.e.

  (minus 0) --- simpl ---> (fun _ => 0)

  The point is that simpl is implemented as "strong whd_simpl"
  and after unfolding minus you have

    (fun m => match 0 => 0 | S n' => ...n' - m'... end)

  that is already in whd and exposes a match, that of course "strong"
  would reduce away but at that stage we don't know, and reducing by
  hand under the lambda is against whd reduction. So further discussion
  on that idea is needed. *)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14716 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 280 insertions, 11 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b6c67555d4..4cf1e2345c 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -16,6 +16,7 @@ open Termops
 open Namegen
 open Declarations
 open Inductive
+open Libobject
 open Environ
 open Closure
 open Reductionops
@@ -515,27 +516,127 @@ let special_red_case env sigma whfun (ci, p, c, lf)  =
   in
   redrec (c, empty_stack)
 
+(* data structure to hold the map kn -> rec_args for simpl *)
+
+type behaviour = {
+  b_nargs: int;
+  b_recargs: int list;
+  b_dont_expose_case: bool;
+}
+
+let behaviour_table = ref (Refmap.empty : behaviour Refmap.t)
+
+let _ =
+  Summary.declare_summary "simplbehaviour"
+    { Summary.freeze_function = (fun () -> !behaviour_table);
+      Summary.unfreeze_function = (fun x -> behaviour_table := x);
+      Summary.init_function = (fun () -> behaviour_table := Refmap.empty) }
+
+type simpl_flag = [ `SimplDontExposeCase | `SimplNeverUnfold ]
+type req =
+  | ReqLocal
+  | ReqGlobal of global_reference * (int list * int * simpl_flag list)
+
+let load_simpl_behaviour _ (_,(_,(r, b))) =
+  behaviour_table := Refmap.add r b !behaviour_table
+
+let cache_simpl_behaviour o = load_simpl_behaviour 1 o
+
+let classify_simpl_behaviour = function
+  | ReqLocal, _ -> Dispose
+  | ReqGlobal _, _ as o -> Substitute o
+
+let subst_simpl_behaviour (subst, (_, (r,o as orig))) =
+  ReqLocal,
+  let r' = fst (subst_global subst r) in if r==r' then orig else (r',o)
+
+let discharge_simpl_behaviour = function
+  | _,(ReqGlobal (ConstRef c, req), (_, b)) ->
+     let c' = pop_con c in
+     let vars = Lib.section_segment_of_constant c in
+     let extra = List.length vars in
+     let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in
+     let recargs' = List.map ((+) extra) b.b_recargs in
+     let b' = { b with b_nargs = nargs'; b_recargs = recargs' } in
+     Some (ReqGlobal (ConstRef c', req), (ConstRef c', b'))
+  | _ -> None
+
+let rebuild_simpl_behaviour = function
+  | req, (ConstRef c, _ as x) -> req, x
+  | _ -> assert false
+
+let inSimplBehaviour = declare_object { (default_object "SIMPLBEHAVIOUR") with
+  load_function = load_simpl_behaviour;
+  cache_function = cache_simpl_behaviour;
+  classify_function = classify_simpl_behaviour;
+  subst_function = subst_simpl_behaviour;
+  discharge_function = discharge_simpl_behaviour;
+  rebuild_function = rebuild_simpl_behaviour;
+}
+
+let set_simpl_behaviour local r (recargs, nargs, flags as req) =
+  let nargs = if List.mem `SimplNeverUnfold flags then max_int else nargs in
+  let nargs = List.fold_left max nargs recargs in
+  let behaviour = {
+    b_nargs = nargs; b_recargs = recargs;
+    b_dont_expose_case = List.mem `SimplDontExposeCase flags } in
+  let req = if local then ReqLocal else ReqGlobal (r, req) in
+  Lib.add_anonymous_leaf (inSimplBehaviour (req, (r, behaviour)))
+;;
+
+let get_simpl_behaviour r =
+  try
+    let b = Refmap.find r !behaviour_table in
+    let flags =
+      if b.b_nargs = max_int then [`SimplNeverUnfold]
+      else if b.b_dont_expose_case then [`SimplDontExposeCase] else [] in
+    Some (b.b_recargs, (if b.b_nargs = max_int then -1 else b.b_nargs), flags)
+  with Not_found -> None
+
+let get_behaviour = function
+  | EvalVar _ | EvalRel _ | EvalEvar _ -> raise Not_found
+  | EvalConst c -> Refmap.find (ConstRef c) !behaviour_table
+
+let recargs r =
+  try let b = get_behaviour r in Some (b.b_recargs, b.b_nargs)
+  with Not_found -> None
+
+let dont_expose_case r =
+  try (get_behaviour r).b_dont_expose_case with Not_found -> false
+
 (* [red_elim_const] contracts iota/fix/cofix redexes hidden behind
    constants by keeping the name of the constants in the recursive calls;
    it fails if no redex is around *)
 
 let rec red_elim_const env sigma ref largs =
-  match reference_eval sigma env ref with
-    | EliminationCases n when stack_args_size largs >= n ->
+  let nargs = stack_args_size largs in
+  let largs, unfold_anyway =
+    match recargs ref with
+    | None -> largs, false
+    | Some (_,n) when nargs < n -> raise Redelimination
+    | Some (l,n) ->
+        List.fold_left (fun stack i ->
+          let arg = stack_nth stack i in
+          let rarg = whd_construct_state env sigma (arg, empty_stack) in
+          match kind_of_term (fst rarg) with
+          | Construct _ -> stack_assign stack i (app_stack rarg)
+          | _ -> raise Redelimination)
+        largs l, n >= 0 && l = [] && nargs >= n in
+  try match reference_eval sigma env ref with
+    | EliminationCases n when nargs >= n ->
 	let c = reference_value sigma env ref in
 	let c', lrest = whd_betadelta_state env sigma (c,largs) in
 	let whfun = whd_simpl_state env sigma in
         (special_red_case env sigma whfun (destCase c'), lrest)
-    | EliminationFix (min,minfxargs,infos) when stack_args_size largs >=min ->
+    | EliminationFix (min,minfxargs,infos) when nargs >= min ->
 	let c = reference_value sigma env ref in
 	let d, lrest = whd_betadelta_state env sigma (c,largs) in
 	let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) largs in
 	let whfun = whd_construct_state env sigma in
 	(match reduce_fix_use_function env sigma f whfun (destFix d) lrest with
 	   | NotReducible -> raise Redelimination
-	   | Reduced (c,rest) -> (nf_beta sigma c, rest))
-    | EliminationMutualFix (min,refgoal,refinfos)
-	when stack_args_size largs >= min ->
+           | Reduced (c,rest) -> (nf_beta sigma c, rest))
+    | EliminationMutualFix (min,refgoal,refinfos) when nargs >= min ->
 	let rec descend ref args =
 	  let c = reference_value sigma env ref in
 	  if ref = refgoal then
@@ -551,6 +652,9 @@ let rec red_elim_const env sigma ref largs =
 	   | NotReducible -> raise Redelimination
 	   | Reduced (c,rest) -> (nf_beta sigma c, rest))
     | _ -> raise Redelimination
+    with Redelimination when unfold_anyway ->
+       let c = reference_value sigma env ref in
+       whd_betaiotazeta sigma (app_stack (c, largs)), empty_stack
 
 (* reduce to whd normal form or to an applied constant that does not hide
    a reducible iota/fix/cofix redex (the "simpl" tactic) *)
@@ -578,7 +682,14 @@ and whd_simpl_state env sigma s =
       | _ when isEvalRef env x ->
 	  let ref = destEvalRef x in
           (try
-	    redrec (red_elim_const env sigma ref stack)
+            let hd, _ as s' = redrec (red_elim_const env sigma ref stack) in
+            let rec is_case x = match kind_of_term x with
+              | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
+              | App (hd, _) -> is_case hd
+              | Case _ -> true
+              | _ -> false in
+            if dont_expose_case ref && is_case hd then raise Redelimination
+            else s'
            with Redelimination ->
 	     s)
       | _ -> s
@@ -919,7 +1030,7 @@ let one_step_reduce env sigma c =
       | _ when isEvalRef env x ->
 	  let ref = destEvalRef x in
           (try
-            red_elim_const env sigma ref stack
+             red_elim_const env sigma ref stack
            with Redelimination ->
 	     match reference_opt_value sigma env ref with
 	       | Some d -> d, stack
@@ -959,7 +1070,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
 	  with Not_found ->
           try
 	    let t' = nf_betaiota sigma (one_step_reduce env sigma t) in
-	    elimrec env t' l
+            elimrec env t' l
           with NotStepReducible ->
 	    errorlabstrm ""
 	      (str "Cannot recognize a statement based on " ++
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index d713eae42a..f0f5f66d31 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -15,6 +15,7 @@ open Closure
 open Glob_term
 open Termops
 open Pattern
+open Libnames
 
 type reduction_tactic_error =
     InvalidAbstraction of env * constr * (env * Type_errors.type_error)
@@ -43,6 +44,14 @@ val red_product : reduction_function
 (** Red (raise Redelimination if nothing reducible) *)
 val try_red_product : reduction_function
 
+(** Tune the behaviour of simpl for the given constant name *)
+type simpl_flag = [ `SimplDontExposeCase | `SimplNeverUnfold ]
+
+val set_simpl_behaviour :
+  bool -> global_reference -> (int list * int * simpl_flag list) -> unit
+val get_simpl_behaviour :
+  global_reference -> (int list * int * simpl_flag list) option
+
 (** Simpl *)
 val simpl : reduction_function
 
@@ -85,10 +94,10 @@ val reduce_to_quantified_ind : env ->  evar_map -> types -> inductive * types
 (** [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form
    [t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *)
 val reduce_to_quantified_ref :
-  env ->  evar_map -> Libnames.global_reference -> types -> types
+  env ->  evar_map -> global_reference -> types -> types
 
 val reduce_to_atomic_ref :
-  env ->  evar_map -> Libnames.global_reference -> types -> types
+  env ->  evar_map -> global_reference -> types -> types
 
 val contextually : bool -> occurrences * constr_pattern ->
   (patvar_map -> reduction_function) -> reduction_function
diff --git a/test-suite/success/simpl_tuning.v b/test-suite/success/simpl_tuning.v
new file mode 100644
index 0000000000..d4191b939b
--- /dev/null
+++ b/test-suite/success/simpl_tuning.v
@@ -0,0 +1,149 @@
+(* as it is dynamically inferred by simpl *)
+Arguments minus !n / m.
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (match y with O => S x | S _ => _ end = 0) => idtac end.
+Abort. 
+
+(* we avoid exposing a match *)
+Arguments minus n m : simpl nomatch. 
+
+Lemma foo x : minus 0 x = 0.
+simpl.
+match goal with |- (0 = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (S x - y = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
+simpl.
+match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
+Abort.
+
+(* we unfold as soon as we have 1 args, but we avoid exposing a match *)
+Arguments minus n / m : simpl nomatch. 
+
+Lemma foo : minus 0 = fun x => 0.
+simpl.
+match goal with |- minus 0 = _ => idtac end.
+Abort.
+(* This does not work as one may expect. The point is that simpl is implemented
+   as "strong (whd_simpl_state)" and after unfolding minus you have
+   (fun m => match 0 => 0 | S n => ...) that is already in whd and exposes
+   a match, that of course "strong" would reduce away but at that stage
+   we don't know, and reducing by hand under the lambda is against whd *) 
+
+(* extra tuning for the usual heuristic *)
+Arguments minus !n / m : simpl nomatch. 
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (S x - y = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
+simpl.
+match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
+Abort.
+
+(* full control *)
+Arguments minus !n !m /.
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (S x - y = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
+simpl.
+match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
+Abort.
+
+(* omitting /, that being immediately after the last ! is irrelevant *)
+Arguments minus !n !m.
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (S x - y = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
+simpl.
+match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
+Abort.
+
+Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := 
+  fun x => (f (fst x), g (snd x)).
+
+Delimit Scope foo_scope with F.
+Notation "@@" := nat (only parsing) : foo_scope.
+Notation "@@" := (fun x => x) (only parsing).
+
+Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never.
+
+Lemma foo x : @pf @@ nat @@ nat nat @@ x = pf @@ @@ x.
+Abort.
+
+Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
+
+(* fcomp is unfolded if applied to 6 args *)
+Arguments fcomp {A B C}%type f g x /.
+
+Notation "f \o g" := (fcomp f g) (at level 50).
+
+Lemma foo (f g h : nat -> nat) x : pf (f \o g) h x = pf f h (g (fst x), snd x).
+simpl.
+match goal with |- (pf (f \o g) h x = _) => idtac end.
+case x; intros x1 x2. 
+simpl.
+match goal with |- (pf (f \o g) h _ = pf f h _) => idtac end.
+unfold pf; simpl.
+match goal with |- (f (g x1), h x2) = (f (g x1), h x2) => idtac end.
+Abort. 
+
+Definition volatile := fun x : nat => x.
+Arguments volatile /.
+
+Lemma foo : volatile = volatile.
+simpl.
+match goal with |- (fun _ => _) = _ => idtac end.
+Abort.
+
+Set Implicit Arguments.
+
+Section S1.
+
+Variable T1 : Type.
+
+Section S2.
+
+Variable T2 : Type.
+
+Fixpoint f (x : T1) (y : T2) n (v : unit) m {struct n} : nat :=
+  match n, m with
+  | 0,_ => 0
+  | S _, 0 => n
+  | S n', S m' => f x y n' v m' end.
+
+Global Arguments f x y !n !v !m.
+
+Lemma foo x y n m : f x y (S n) tt m = f x y (S n) tt (S m).
+simpl.
+match goal with |- (f _ _ _ _ _ = f _ _ _ _ _) => idtac end.
+Abort.
+
+End S2.
+
+Lemma foo T x y n m : @f T x y (S n) tt m = @f T x y (S n) tt (S m).
+simpl.
+match goal with |- (f _ _ _ _ _ = f _ _ _ _ _) => idtac end.
+Abort.
+
+End S1.
+
+Arguments f : clear implicits and scopes.
+