diff options
Diffstat (limited to 'proofs/redexpr.ml')
| -rw-r--r-- | proofs/redexpr.ml | 103 |
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) |