New command Declare Reduction <id> := <conv_expr>.

 Let's avoid writing huge "Eval ... in ..." lines :-)
 Will be used in particular soon in NMake for defining function via
  Definition ... := Eval ... in ...

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

10 files changed, 115 insertions, 16 deletions

diff --git a/CHANGES b/CHANGES
index a7dec737a..f06cbb2e1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -94,6 +94,8 @@ Vernacular commands
 - Include Type is now deprecated since Include now accept both modules and
   module types.
 - Declare ML Module supports Local option.
+- New command "Declare Reduction <id> := <conv_expr>", allowing to write
+  later "Eval <id> in ...". This command accepts a Local variant.
 
 Tools
 
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 316a02f1b..c71df4e22 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -1020,6 +1020,21 @@ command is prefixed by {\tt Local}. In the latter case, the behavior
 regarding sections and modules is the same as for the {\tt
   Transparent} and {\tt Opaque} commands.
 
+\subsection{\tt Declare Reduction \ident\ := {\rm\sl convtactic}.}
+
+This command allows to give a short name to a reduction expression,
+for instance {\tt lazy beta delta [foo bar]}. This short name can
+then be used in {\tt Eval \ident\ in ...} or {\tt eval} directives.
+This command accepts the {\tt Local} modifier, for discarding
+this reduction name at the end of the file or module. For the moment
+the name cannot be qualified. In particular declaring the same name
+in several modules or in several functor applications will be refused
+if these declarations are not local. The name \ident\ cannot be used
+directly as an Ltac tactic, but nothing prevent the user to also
+perform a {\tt Ltac \ident\ := {\rm\sl convtactic}}.
+
+\SeeAlso sections \ref{Conversion-tactics}
+
 \subsection{\tt Set Virtual Machine
 \label{SetVirtualMachine}
 \comindex{Set Virtual Machine}}
diff --git a/ide/coq.ml b/ide/coq.ml
index 3dc3e1431..920d466fc 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -275,6 +275,7 @@ let rec attribute_of_vernac_command = function
   | VernacHints _ -> []
   | VernacSyntacticDefinition _ -> []
   | VernacDeclareImplicits _ -> []
+  | VernacDeclareReduction _ -> []
   | VernacReserve _ -> []
   | VernacGeneralizable _ -> []
   | VernacSetOpacity _ -> []
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f0d90b11b..2eec7848a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -807,6 +807,12 @@ GEXTEND Gram
       |	IDENT "Debug"; IDENT "Off" ->
           VernacSetOption (None,["Ltac";"Debug"], BoolValue false)
 
+(* registration of a custom reduction *)
+
+      | IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":=";
+         r = Tactic.red_expr ->
+	   VernacDeclareReduction (use_locality(),s,r)
+
  ] ];
     END
 ;;
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 6d3cf76b2..e88165773 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -892,6 +892,9 @@ let rec pr_vernac = function
       (if io = None then mt() else int (Option.get io) ++ str ": ") ++
       pr_mayeval r c
   | VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_constrarg c)
+  | VernacDeclareReduction (b,s,r) ->
+     pr_locality b ++ str "Declare Reduction " ++ str s ++ str " := " ++
+     pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r
   | VernacPrint p ->
       let pr_printable = function
 	| PrintFullContext -> str"Print All"
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index e85c12c59..cd9137fd0 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -878,7 +878,7 @@ let _ = add_map "field_cond"
 (*                       (function -1|8|10->Eval|9->Rec|_->Prot)]);;*)
 
 
-let _ = Redexpr.declare_red_expr "simpl_field_expr"
+let _ = Redexpr.declare_reduction "simpl_field_expr"
   (protect_red "field")
 
 
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index fa6a6f3ec..b0a01caa7 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -21,6 +21,7 @@ open Tacred
 open Closure
 open RedFlags
 open Libobject
+open Summary
 
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env _ c =
@@ -98,11 +99,10 @@ let (inStrategy,outStrategy) =
 let set_strategy local str =
   Lib.add_anonymous_leaf (inStrategy (local,str))
 
-let _ =
-  Summary.declare_summary "Transparent constants and variables"
-    { Summary.freeze_function = Conv_oracle.freeze;
-      Summary.unfreeze_function = Conv_oracle.unfreeze;
-      Summary.init_function = Conv_oracle.init }
+let _ = declare_summary "Transparent constants and variables"
+    { freeze_function = Conv_oracle.freeze;
+      unfreeze_function = Conv_oracle.unfreeze;
+      init_function = Conv_oracle.init }
 
 
 (* Generic reduction: reduction functions used in reduction tactics *)
@@ -135,14 +135,32 @@ let make_flag f =
 
 let is_reference = function PRef _ | PVar _ -> true | _ -> false
 
+(* table of custom reductino fonctions, not synchronized,
+   filled via ML calls to [declare_reduction] *)
+let reduction_tab = ref Stringmap.empty
+
+(* table of custom reduction expressions, synchronized,
+   filled by command Declare Reduction *)
 let red_expr_tab = ref Stringmap.empty
 
-let declare_red_expr s f =
-  try
-    let _ = Stringmap.find s !red_expr_tab in
-    error ("There is already a reduction expression of name "^s)
-  with Not_found ->
-    red_expr_tab := Stringmap.add s f !red_expr_tab
+let declare_reduction s f =
+  if Stringmap.mem s !reduction_tab || Stringmap.mem s !red_expr_tab
+  then error ("There is already a reduction expression of name "^s)
+  else reduction_tab := Stringmap.add s f !reduction_tab
+
+let check_custom = function
+  | ExtraRedExpr s ->
+      if not (Stringmap.mem s !reduction_tab || Stringmap.mem s !red_expr_tab)
+      then error ("Reference to undefined reduction expression "^s)
+  |_ -> ()
+
+let decl_red_expr s e =
+  if Stringmap.mem s !reduction_tab || Stringmap.mem s !red_expr_tab
+  then error ("There is already a reduction expression of name "^s)
+  else begin
+    check_custom e;
+    red_expr_tab := Stringmap.add s e !red_expr_tab
+  end
 
 let out_arg = function
   | ArgVar _ -> anomaly "Unevaluated or_var variable"
@@ -151,7 +169,7 @@ let out_arg = function
 let out_with_occurrences ((b,l),c) =
   ((b,List.map out_arg l), c)
 
-let reduction_of_red_expr = function
+let rec reduction_of_red_expr = function
   | Red internal ->
       if internal then (try_red_product,DEFAULTcast)
       else (red_product,DEFAULTcast)
@@ -166,6 +184,49 @@ let reduction_of_red_expr = function
   | Fold cl -> (fold_commands cl,DEFAULTcast)
   | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast)
   | ExtraRedExpr s ->
-      (try (Stringmap.find s !red_expr_tab,DEFAULTcast)
-      with Not_found -> error("unknown user-defined reduction \""^s^"\""))
+      (try (Stringmap.find s !reduction_tab,DEFAULTcast)
+      with Not_found ->
+	(try reduction_of_red_expr (Stringmap.find s !red_expr_tab)
+	 with Not_found ->
+	   error("unknown user-defined reduction \""^s^"\"")))
   | CbvVm -> (cbv_vm ,VMcast)
+
+
+let subst_flags subs flags =
+  { flags with rConst = List.map subs flags.rConst }
+
+let subst_occs subs (occ,e) = (occ,subs e)
+
+let subst_gen_red_expr subs_a subs_b subs_c = function
+  | Fold l -> Fold (List.map subs_a l)
+  | Pattern occs_l -> Pattern (List.map (subst_occs subs_a) occs_l)
+  | Simpl occs_o -> Simpl (Option.map (subst_occs subs_c) occs_o)
+  | Unfold occs_l -> Unfold (List.map (subst_occs subs_b) occs_l)
+  | Cbv flags -> Cbv (subst_flags subs_b flags)
+  | Lazy flags -> Lazy (subst_flags subs_b flags)
+  | e -> e
+
+let subst_red_expr subs e =
+  subst_gen_red_expr
+    (Mod_subst.subst_mps subs)
+    (Mod_subst.subst_evaluable_reference subs)
+    (Pattern.subst_pattern subs)
+    e
+
+let (inReduction,_) =
+  declare_object
+    {(default_object "REDUCTION") with
+       cache_function = (fun (_,(_,s,e)) -> decl_red_expr s e);
+       load_function = (fun _ (_,(_,s,e)) -> decl_red_expr s e);
+       subst_function =
+	(fun (subs,(b,s,e)) -> b,s,subst_red_expr subs e);
+       classify_function =
+	(fun ((b,_,_) as obj) -> if b then Dispose else Substitute obj) }
+
+let declare_red_expr locality s expr =
+    Lib.add_anonymous_leaf (inReduction (locality,s,expr))
+
+let _ = declare_summary "Declare Reduction"
+  { freeze_function = (fun () -> !red_expr_tab);
+    unfreeze_function = ((:=) red_expr_tab);
+    init_function = (fun () -> red_expr_tab := Stringmap.empty) }
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index 63237aa20..03d97ce35 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -24,7 +24,13 @@ val out_with_occurrences : 'a with_occurrences -> occurrences * 'a
 val reduction_of_red_expr : red_expr -> reduction_function * cast_kind
 (* [true] if we should use the vm to verify the reduction *)
 
-val declare_red_expr : string -> reduction_function -> unit
+(* Adding a custom reduction (function to be use at the ML level)
+   NB: the effect is permanent. *)
+val declare_reduction : string -> reduction_function -> unit
+
+(* Adding a custom reduction (function to be called a vernac command).
+   The boolean flag is the locality. *)
+val declare_red_expr : bool -> string -> red_expr -> unit
 
 (* Opaque and Transparent commands. *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b56b0b26f..f299f3a51 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1050,6 +1050,9 @@ let vernac_check_may_eval redexp glopt rc =
 	then (Option.get !pcoq).print_eval redfun env evmap rc j
 	else msg (print_eval redfun env evmap rc j)
 
+let vernac_declare_reduction locality s r =
+  declare_red_expr locality s (interp_redexp (Global.env()) Evd.empty r)
+
   (* The same but avoiding the current goal context if any *)
 let vernac_global_check c =
   let evmap = Evd.empty in
@@ -1391,6 +1394,7 @@ let interp c = match c with
   | VernacMemOption (key,v) -> vernac_mem_option key v
   | VernacPrintOption key -> vernac_print_option key
   | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval r g c
+  | VernacDeclareReduction (b,s,r) -> vernac_declare_reduction b s r
   | VernacGlobalCheck c -> vernac_global_check c
   | VernacPrint p -> vernac_print p
   | VernacSearch (s,r) -> vernac_search s r
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 8e5f2d8fc..6d538bde8 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -323,6 +323,7 @@ type vernac_expr =
   | VernacPrintOption of Goptions.option_name
   | VernacCheckMayEval of raw_red_expr option * int option * constr_expr
   | VernacGlobalCheck of constr_expr
+  | VernacDeclareReduction of locality_flag * string * raw_red_expr
   | VernacPrint of printable
   | VernacSearch of searchable * search_restriction
   | VernacLocate of locatable