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

2 files changed, 6 insertions, 105 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index cae0705c05..ce09bf8aa7 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -26,31 +26,6 @@ open Rawterm
 exception Elimconst
 exception Redelimination
 
-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 }
-
 let is_evaluable env ref =
   match ref with
       EvalConstRef kn ->
@@ -503,7 +478,7 @@ and construct_const env sigma =
 
 (* Red reduction tactic: reduction to a product *)
 
-let internal_red_product env sigma c = 
+let try_red_product env sigma c = 
   let simpfun = clos_norm_flags betaiotazeta env sigma in
   let rec redrec env x =
     match kind_of_term x with
@@ -533,11 +508,9 @@ let internal_red_product env sigma c =
   in redrec env c
 
 let red_product env sigma c = 
-  try internal_red_product env sigma c
+  try try_red_product env sigma c
   with Redelimination -> error "Not reducible"
 
-(* Hnf reduction tactic: *)
-
 let hnf_constr env sigma c = 
   let rec redrec (x, largs as s) =
     match kind_of_term x with
@@ -610,9 +583,6 @@ let whd_nf env sigma c =
 
 let nf env sigma c = strong whd_nf env sigma c
 
-let is_reference c = 
-  try let r = reference_of_constr c in true with _ -> false
-
 let is_head c t =
   match kind_of_term t with
     | App (f,_) -> f = c
@@ -804,11 +774,6 @@ let cbv_betadeltaiota env sigma =  cbv_norm_flags betadeltaiota env sigma
 
 let compute = cbv_betadeltaiota
 
-(* call by value reduction functions using virtual machine *)
-let cbv_vm env _ c =
-  let ctyp = (fst (Typeops.infer env c)).uj_type in
-  Vconv.cbv_vm env c ctyp
-
 (* Pattern *)
 
 (* gives [na:ta]c' such that c converts to ([na:ta]c' a), abstracting only
@@ -828,58 +793,6 @@ let pattern_occs loccs_trm env sigma c =
   let _ = Typing.type_of env sigma abstr_trm in
   applist(abstr_trm, List.map snd loccs_trm)
 
-(* Generic reduction: reduction functions used in reduction tactics *)
-
-type red_expr = (constr, evaluable_global_reference) red_expr_gen
-
-open RedFlags
-
-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 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_redexp = function
-  | Red internal -> if internal then internal_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 
 (* Used in several tactics. *)
 
 exception NotStepReducible
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 0c093694c1..b7d8c1b85c 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -24,9 +24,12 @@ val is_evaluable : env -> evaluable_global_reference -> bool
 
 exception Redelimination
 
-(* Red (raise Redelimination if nothing reducible) *)
+(* Red (raise user error if nothing reducible) *)
 val red_product : reduction_function
 
+(* Red (raise Redelimination if nothing reducible) *)
+val try_red_product : reduction_function
+
 (* Hnf *)
 val hnf_constr :  reduction_function
 
@@ -51,9 +54,6 @@ val cbv_norm_flags : Closure.RedFlags.reds ->  reduction_function
   val cbv_betadeltaiota :  reduction_function
   val compute :  reduction_function  (* = [cbv_betadeltaiota] *)
 
-(* Call by value strategy (uses virtual machine) *)
-val cbv_vm : reduction_function
-
 (* [reduce_to_atomic_ind env sigma t] puts [t] in the form [t'=(I args)]
    with [I] an inductive definition;
    returns [I] and [t'] or fails with a user error *)
@@ -72,17 +72,5 @@ val reduce_to_quantified_ref :
 val reduce_to_atomic_ref :
   env ->  evar_map -> Libnames.global_reference -> types -> types
 
-type red_expr = (constr, evaluable_global_reference) red_expr_gen
-
 val contextually : bool -> constr occurrences -> reduction_function
   -> reduction_function
-val reduction_of_redexp : 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