diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/redexpr.ml | 64 | ||||
| -rw-r--r-- | proofs/redexpr.mli | 6 |
2 files changed, 67 insertions, 3 deletions
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 28e121ab2f..27db717558 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -19,14 +19,19 @@ open Reductionops open Tacred open Closure open RedFlags - +open Libobject (* call by value normalisation function using the virtual machine *) let cbv_vm env _ c = let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in Vnorm.cbv_vm env c ctyp -let set_strategy k l = + +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 -> @@ -41,6 +46,61 @@ let set_strategy k l = 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" { Summary.freeze_function = Conv_oracle.freeze; diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index 404a8a196d..68c1fd6693 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -26,7 +26,11 @@ val declare_red_expr : string -> reduction_function -> unit (* Opaque and Transparent commands. *) -val set_strategy : 'a tableKey -> Conv_oracle.level -> unit +(* Sets the expansion strategy of a constant. When the boolean is + true, the effect is non-synchronous (i.e. it does not survive + section and module closure). *) +val set_strategy : + bool -> (Conv_oracle.level * evaluable_global_reference list) list -> unit (* call by value normalisation function using the virtual machine *) val cbv_vm : reduction_function |