Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dans redexpr.ml

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

4 files changed, 142 insertions, 4 deletions

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
new file mode 100644
index 000000000..47d468bd3
--- /dev/null
+++ b/proofs/redexpr.ml
@@ -0,0 +1,106 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Term
+open Declarations
+open Libnames
+open Rawterm
+open Reductionops
+open Tacred
+open Closure
+open RedFlags
+
+let set_opaque_const sp = 
+  Conv_oracle.set_opaque_const sp;
+  Csymtable.set_opaque_const sp
+
+let set_transparent_const sp =
+  let cb = Global.lookup_constant sp in
+  if cb.const_body <> None & cb.const_opaque then
+    errorlabstrm "set_transparent_const"
+      (str "Cannot make" ++ spc () ++ 
+         Nametab.pr_global_env Idset.empty (ConstRef sp) ++
+         spc () ++ str "transparent because it was declared opaque.");
+  Conv_oracle.set_transparent_const sp;
+  Csymtable.set_transparent_const sp
+
+let set_opaque_var      = Conv_oracle.set_opaque_var
+let set_transparent_var = Conv_oracle.set_transparent_var
+
+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;
+      Summary.survive_module = false;
+      Summary.survive_section = false }
+
+(* call by value reduction functions using virtual machine *)
+let cbv_vm env _ c =
+  let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in
+  Vconv.cbv_vm env c ctyp
+
+(* Generic reduction: reduction functions used in reduction tactics *)
+
+type red_expr = (constr, evaluable_global_reference) red_expr_gen
+
+
+let make_flag_constant = function
+  | EvalVarRef id -> fVAR id
+  | EvalConstRef sp -> fCONST sp
+
+let make_flag f =
+  let red = no_red in
+  let red = if f.rBeta then red_add red fBETA else red in
+  let red = if f.rIota then red_add red fIOTA else red in
+  let red = if f.rZeta then red_add red fZETA else red in
+  let red =
+    if f.rDelta then (* All but rConst *)
+        let red = red_add red fDELTA in
+        let red = red_add_transparent red (Conv_oracle.freeze ()) in
+	List.fold_right
+	  (fun v red -> red_sub red (make_flag_constant v))
+	  f.rConst red
+    else (* Only rConst *)
+        let red = red_add_transparent (red_add red fDELTA) all_opaque in
+	List.fold_right
+	  (fun v red -> red_add red (make_flag_constant v))
+	  f.rConst red
+  in red
+
+let is_reference c = 
+  try let r = reference_of_constr c in true with _ -> false
+
+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 reduction_of_red_expr = function
+  | Red internal -> if internal then try_red_product else red_product
+  | Hnf -> hnf_constr
+  | Simpl (Some (_,c as lp)) -> contextually (is_reference c) lp nf
+  | Simpl None -> nf
+  | Cbv f -> cbv_norm_flags (make_flag f)
+  | Lazy f -> clos_norm_flags (make_flag f)
+  | Unfold ubinds -> unfoldn ubinds
+  | Fold cl -> fold_commands cl
+  | Pattern lp -> pattern_occs lp
+  | ExtraRedExpr s ->
+      (try Stringmap.find s !red_expr_tab
+      with Not_found -> error("unknown user-defined reduction \""^s^"\""))
+  | CbvVm -> cbv_vm 
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
new file mode 100644
index 000000000..a0b7100b6
--- /dev/null
+++ b/proofs/redexpr.mli
@@ -0,0 +1,31 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+open Names
+open Term
+open Closure
+open Rawterm
+open Reductionops
+
+(* Call by value strategy (uses virtual machine) *)
+val cbv_vm : reduction_function
+
+type red_expr = (constr, evaluable_global_reference) red_expr_gen
+
+val reduction_of_red_expr : red_expr -> reduction_function
+
+val declare_red_expr : string -> reduction_function -> unit
+
+(* Opaque and Transparent commands. *)
+val set_opaque_const      : constant -> unit
+val set_transparent_const : constant -> unit
+
+val set_opaque_var      : identifier -> unit
+val set_transparent_var : identifier -> unit
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 0ddcd6116..37dc016c9 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -18,6 +18,7 @@ open Environ
 open Reductionops
 open Evd
 open Typing
+open Redexpr
 open Tacred
 open Proof_trees
 open Proof_type
@@ -90,8 +91,8 @@ let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
 
 let pf_parse_const gls = compose (pf_global gls) id_of_string
 
-let pf_reduction_of_redexp gls re c = 
-  reduction_of_redexp re (pf_env gls) (project gls) c 
+let pf_reduction_of_red_expr gls re c = 
+  reduction_of_red_expr re (pf_env gls) (project gls) c 
 
 let pf_apply f gls = f (pf_env gls) (project gls)
 let pf_reduce = pf_apply
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 4fbc102cc..22b9de0b7 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -18,7 +18,7 @@ open Reduction
 open Proof_trees
 open Proof_type
 open Refiner
-open Tacred
+open Redexpr
 open Tacexpr
 open Rawterm
 (*i*)
@@ -62,7 +62,7 @@ val pf_get_hyp_typ        : goal sigma -> identifier -> types
 val pf_get_new_id  : identifier      -> goal sigma -> identifier
 val pf_get_new_ids : identifier list -> goal sigma -> identifier list
 
-val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr
+val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> constr
 
 
 val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a