From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- proofs/redexpr.ml | 131 ++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 92 insertions(+), 39 deletions(-) (limited to 'proofs/redexpr.ml') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index ad8ee3a2..b0a01caa 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: redexpr.ml 11481 2008-10-20 19:23:51Z herbelin $ *) +(* $Id$ *) open Pp open Util @@ -15,11 +15,13 @@ open Term open Declarations open Libnames open Rawterm +open Pattern open Reductionops open Tacred open Closure open RedFlags open Libobject +open Summary (* call by value normalisation function using the virtual machine *) let cbv_vm env _ c = @@ -40,18 +42,18 @@ let set_strategy_one ref l = let cb = Global.lookup_constant sp in if cb.const_body <> None & cb.const_opaque then errorlabstrm "set_transparent_const" - (str "Cannot make" ++ spc () ++ + (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 + List.iter (fun (lev,ql) -> List.iter (fun q -> set_strategy_one q lev) ql) str -let subst_strategy (_,subs,(local,obj)) = +let subst_strategy (subs,(local,obj)) = local, list_smartmap (fun (k,ql as entry) -> @@ -62,7 +64,7 @@ let subst_strategy (_,subs,(local,obj)) = let map_strategy f l = let l' = List.fold_right - (fun (lev,ql) str -> + (fun (lev,ql) str -> let ql' = List.fold_right (fun q ql -> match f q with @@ -71,21 +73,15 @@ let map_strategy f l = if ql'=[] then str else (lev,ql')::str) l [] in if l'=[] then None else Some (false,l') -let export_strategy (local,obj) = - if local then None else - map_strategy (function - EvalVarRef _ -> None - | EvalConstRef _ as q -> Some q) obj - -let classify_strategy (_,(local,_ as obj)) = +let classify_strategy (local,_ as obj) = if local then Dispose else Substitute obj let disch_ref ref = match ref with - EvalConstRef c -> + EvalConstRef c -> let c' = Lib.discharge_con c in if c==c' then Some ref else Some (EvalConstRef c') - | _ -> Some ref + | EvalVarRef id -> if Lib.is_in_section (VarRef id) then None else Some ref let discharge_strategy (_,(local,obj)) = if local then None else @@ -97,26 +93,22 @@ let (inStrategy,outStrategy) = load_function = (fun _ (_,obj) -> cache_strategy obj); subst_function = subst_strategy; discharge_function = discharge_strategy; - classify_function = classify_strategy; - export_function = export_strategy } + classify_function = classify_strategy } let set_strategy local str = Lib.add_anonymous_leaf (inStrategy (local,str)) -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 _ = declare_summary "Transparent constants and variables" + { freeze_function = Conv_oracle.freeze; + unfreeze_function = Conv_oracle.unfreeze; + init_function = Conv_oracle.init } (* Generic reduction: reduction functions used in reduction tactics *) -type red_expr = (constr, evaluable_global_reference) red_expr_gen - +type red_expr = + (constr, evaluable_global_reference, constr_pattern) red_expr_gen let make_flag_constant = function | EvalVarRef id -> fVAR id @@ -141,17 +133,34 @@ let make_flag f = f.rConst red in red -let is_reference c = - try let _ref = global_of_constr c in true with _ -> false +let is_reference = function PRef _ | PVar _ -> true | _ -> false + +(* table of custom reductino fonctions, not synchronized, + filled via ML calls to [declare_reduction] *) +let reduction_tab = ref Stringmap.empty +(* table of custom reduction expressions, synchronized, + filled by command Declare Reduction *) 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 declare_reduction s f = + if Stringmap.mem s !reduction_tab || Stringmap.mem s !red_expr_tab + then error ("There is already a reduction expression of name "^s) + else reduction_tab := Stringmap.add s f !reduction_tab + +let check_custom = function + | ExtraRedExpr s -> + if not (Stringmap.mem s !reduction_tab || Stringmap.mem s !red_expr_tab) + then error ("Reference to undefined reduction expression "^s) + |_ -> () + +let decl_red_expr s e = + if Stringmap.mem s !reduction_tab || Stringmap.mem s !red_expr_tab + then error ("There is already a reduction expression of name "^s) + else begin + check_custom e; + red_expr_tab := Stringmap.add s e !red_expr_tab + end let out_arg = function | ArgVar _ -> anomaly "Unevaluated or_var variable" @@ -160,13 +169,14 @@ let out_arg = function let out_with_occurrences ((b,l),c) = ((b,List.map out_arg l), c) -let reduction_of_red_expr = function - | Red internal -> - if internal then (try_red_product,DEFAULTcast) +let rec reduction_of_red_expr = function + | Red internal -> + if internal then (try_red_product,DEFAULTcast) else (red_product,DEFAULTcast) | Hnf -> (hnf_constr,DEFAULTcast) | Simpl (Some (_,c as lp)) -> - (contextually (is_reference c) (out_with_occurrences lp) simpl,DEFAULTcast) + (contextually (is_reference c) (out_with_occurrences lp) + (fun _ -> simpl),DEFAULTcast) | Simpl None -> (simpl,DEFAULTcast) | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast) | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast) @@ -174,6 +184,49 @@ let reduction_of_red_expr = function | Fold cl -> (fold_commands cl,DEFAULTcast) | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast) | ExtraRedExpr s -> - (try (Stringmap.find s !red_expr_tab,DEFAULTcast) - with Not_found -> error("unknown user-defined reduction \""^s^"\"")) + (try (Stringmap.find s !reduction_tab,DEFAULTcast) + with Not_found -> + (try reduction_of_red_expr (Stringmap.find s !red_expr_tab) + with Not_found -> + error("unknown user-defined reduction \""^s^"\""))) | CbvVm -> (cbv_vm ,VMcast) + + +let subst_flags subs flags = + { flags with rConst = List.map subs flags.rConst } + +let subst_occs subs (occ,e) = (occ,subs e) + +let subst_gen_red_expr subs_a subs_b subs_c = function + | Fold l -> Fold (List.map subs_a l) + | Pattern occs_l -> Pattern (List.map (subst_occs subs_a) occs_l) + | Simpl occs_o -> Simpl (Option.map (subst_occs subs_c) occs_o) + | Unfold occs_l -> Unfold (List.map (subst_occs subs_b) occs_l) + | Cbv flags -> Cbv (subst_flags subs_b flags) + | Lazy flags -> Lazy (subst_flags subs_b flags) + | e -> e + +let subst_red_expr subs e = + subst_gen_red_expr + (Mod_subst.subst_mps subs) + (Mod_subst.subst_evaluable_reference subs) + (Pattern.subst_pattern subs) + e + +let (inReduction,_) = + declare_object + {(default_object "REDUCTION") with + cache_function = (fun (_,(_,s,e)) -> decl_red_expr s e); + load_function = (fun _ (_,(_,s,e)) -> decl_red_expr s e); + subst_function = + (fun (subs,(b,s,e)) -> b,s,subst_red_expr subs e); + classify_function = + (fun ((b,_,_) as obj) -> if b then Dispose else Substitute obj) } + +let declare_red_expr locality s expr = + Lib.add_anonymous_leaf (inReduction (locality,s,expr)) + +let _ = declare_summary "Declare Reduction" + { freeze_function = (fun () -> !red_expr_tab); + unfreeze_function = ((:=) red_expr_tab); + init_function = (fun () -> red_expr_tab := Stringmap.empty) } -- cgit v1.2.3