summaryrefslogtreecommitdiff
path: root/proofs/redexpr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/redexpr.ml')
-rw-r--r--proofs/redexpr.ml103
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)