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

1 files changed, 11 insertions, 2 deletions

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