Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 80 insertions, 23 deletions

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index ad277caa..072a38b6 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: redexpr.ml 9058 2006-07-22 17:42:45Z bgregoir $ *)
+(* $Id: redexpr.ml 11094 2008-06-10 19:35:23Z herbelin $ *)
 
 open Pp
 open Util
@@ -19,7 +19,7 @@ open Reductionops
 open Tacred
 open Closure
 open RedFlags
-
+open Libobject
 
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env _ c =
@@ -27,22 +27,79 @@ let cbv_vm env _ c =
   Vnorm.cbv_vm env c ctyp
 
 
-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 set_strategy_one ref l  =
+  let k =
+    match ref with
+      | EvalConstRef sp -> ConstKey sp
+      | EvalVarRef id -> VarKey id in
+  Conv_oracle.set_strategy k l;
+  match k,l with
+      ConstKey sp, Conv_oracle.Opaque ->
+        Csymtable.set_opaque_const sp
+    | ConstKey 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.");
+        Csymtable.set_transparent_const sp
+    | _ -> ()
+
+let cache_strategy str =
+  List.iter 
+    (fun (lev,ql) -> List.iter (fun q -> set_strategy_one q lev) ql)
+    str
+
+let subst_strategy (_,subs,obj) =
+  list_smartmap
+    (fun (k,ql as entry) ->
+      let ql' = list_smartmap (Mod_subst.subst_evaluable_reference subs) ql in
+      if ql==ql' then entry else (k,ql'))
+    obj
+
+
+let map_strategy f l =
+  let l'  = List.fold_right
+    (fun (lev,ql) str -> 
+      let ql' = List.fold_right
+        (fun q ql ->
+          match f q with
+              Some q' -> q' :: ql
+            | None -> ql) ql [] in
+      if ql'=[] then str else (lev,ql')::str) l [] in
+  if l'=[] then None else Some l'
+
+let export_strategy obj =
+  map_strategy (function
+      EvalVarRef _ -> None
+    | EvalConstRef _ as q -> Some q) obj
+
+let classify_strategy (_,obj) = Substitute obj
+
+let disch_ref ref =
+  match ref with
+      EvalConstRef c -> 
+        let c' = Lib.discharge_con c in
+        if c==c' then Some ref else Some (EvalConstRef c')
+    | _ -> Some ref
+
+let discharge_strategy (_,obj) =
+  map_strategy disch_ref obj
+
+let (inStrategy,outStrategy) =
+  declare_object {(default_object "STRATEGY") with
+                    cache_function = (fun (_,obj) -> cache_strategy obj);
+		    load_function = (fun _ (_,obj) -> cache_strategy obj);
+		    subst_function = subst_strategy;
+                    discharge_function = discharge_strategy;
+		    classify_function = classify_strategy;
+                    export_function = export_strategy }
+
+
+let set_strategy local str =
+  if local then cache_strategy str
+  else Lib.add_anonymous_leaf (inStrategy str)
 
 let _ = 
   Summary.declare_summary "Transparent constants and variables"
@@ -70,7 +127,7 @@ let make_flag f =
   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
+        let red = red_add_transparent red (Conv_oracle.get_transp_state()) in
 	List.fold_right
 	  (fun v red -> red_sub red (make_flag_constant v))
 	  f.rConst red
@@ -97,8 +154,8 @@ let out_arg = function
   | ArgVar _ -> anomaly "Unevaluated or_var variable"
   | ArgArg x -> x
 
-let out_with_occurrences (l,c) =
-  (List.map out_arg l, c)
+let out_with_occurrences ((b,l),c) =
+  ((b,List.map out_arg l), c)
 
 let reduction_of_red_expr = function
   | Red internal -> 
@@ -106,8 +163,8 @@ let reduction_of_red_expr = function
       else (red_product,DEFAULTcast)
   | Hnf -> (hnf_constr,DEFAULTcast)
   | Simpl (Some (_,c as lp)) ->
-      (contextually (is_reference c) (out_with_occurrences lp) nf,DEFAULTcast)
-  | Simpl None -> (nf,DEFAULTcast)
+    (contextually (is_reference c) (out_with_occurrences lp) simpl,DEFAULTcast)
+  | Simpl None -> (simpl,DEFAULTcast)
   | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast)
   | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast)
   | Unfold ubinds -> (unfoldn (List.map out_with_occurrences ubinds),DEFAULTcast)