From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- proofs/redexpr.ml | 156 +++++++++++++++++++++++++++++++----------------------- 1 file changed, 89 insertions(+), 67 deletions(-) (limited to 'proofs/redexpr.ml') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 3c2431a1..18588867 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -1,25 +1,26 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* !simplIsCbn); + Goptions.optwrite = (fun a -> simplIsCbn:=a); +} 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; + Global.set_strategy k l; match k,l with ConstKey sp, Conv_oracle.Opaque -> Csymtable.set_opaque_const sp @@ -44,7 +67,7 @@ let set_strategy_one ref l = | OpaqueDef _ -> errorlabstrm "set_transparent_const" (str "Cannot make" ++ spc () ++ - Nametab.pr_global_env Idset.empty (ConstRef sp) ++ + Nametab.pr_global_env Id.Set.empty (ConstRef sp) ++ spc () ++ str "transparent because it was declared opaque."); | _ -> Csymtable.set_transparent_const sp) | _ -> () @@ -56,9 +79,9 @@ let cache_strategy (_,str) = let subst_strategy (subs,(local,obj)) = local, - list_smartmap + List.smartmap (fun (k,ql as entry) -> - let ql' = list_smartmap (Mod_subst.subst_evaluable_reference subs) ql in + let ql' = List.smartmap (Mod_subst.subst_evaluable_reference subs) ql in if ql==ql' then entry else (k,ql')) obj @@ -71,8 +94,8 @@ let map_strategy f l = 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 (false,l') + if List.is_empty ql' then str else (lev,ql')::str) l [] in + if List.is_empty l' then None else Some (false,l') let classify_strategy (local,_ as obj) = if local then Dispose else Substitute obj @@ -103,12 +126,6 @@ let inStrategy : strategy_obj -> obj = let set_strategy local str = Lib.add_anonymous_leaf (inStrategy (local,str)) -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 = @@ -118,7 +135,7 @@ let make_flag_constant = function | EvalVarRef id -> fVAR id | EvalConstRef sp -> fCONST sp -let make_flag f = +let make_flag env f = let red = no_red in let red = if f.rBeta then red_add red fBETA else red in let red = if f.rIota then red_add red fIOTA else red in @@ -126,7 +143,8 @@ 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.get_transp_state()) in + let red = red_add_transparent red + (Conv_oracle.get_transp_state (Environ.oracle env)) in List.fold_right (fun v red -> red_sub red (make_flag_constant v)) f.rConst red @@ -141,81 +159,90 @@ 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 +let reduction_tab = ref String.Map.empty (* table of custom reduction expressions, synchronized, filled by command Declare Reduction *) -let red_expr_tab = ref Stringmap.empty +let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction" let declare_reduction s f = - if Stringmap.mem s !reduction_tab || Stringmap.mem s !red_expr_tab + if String.Map.mem s !reduction_tab || String.Map.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 + else reduction_tab := String.Map.add s f !reduction_tab let check_custom = function | ExtraRedExpr s -> - if not (Stringmap.mem s !reduction_tab || Stringmap.mem s !red_expr_tab) + if not (String.Map.mem s !reduction_tab || String.Map.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 + if String.Map.mem s !reduction_tab || String.Map.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 + red_expr_tab := String.Map.add s e !red_expr_tab end let out_arg = function - | ArgVar _ -> anomaly "Unevaluated or_var variable" + | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable") | ArgArg x -> x -let out_with_occurrences ((b,l),c) = - ((b,List.map out_arg l), c) +let out_with_occurrences (occs,c) = + (Locusops.occurrences_map (List.map out_arg) occs, c) + +let e_red f env evm c = evm, f env evm c + +let head_style = false (* Turn to true to have a semantics where simpl + only reduce at the head when an evaluable reference is given, e.g. + 2+n would just reduce to S(1+n) instead of S(S(n)) *) + +let contextualize f g = function + | Some (occs,c) -> + let l = Locusops.occurrences_map (List.map out_arg) occs in + let b,c,h = match c with + | Inl r -> true,PRef (global_of_evaluable_reference r),f + | Inr c -> false,c,f in + e_red (contextually b (l,c) (fun _ -> h)) + | None -> e_red g -let rec reduction_of_red_expr = function +let reduction_of_red_expr env = + let make_flag = make_flag env in + 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) - (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) - | Unfold ubinds -> (unfoldn (List.map out_with_occurrences ubinds),DEFAULTcast) - | Fold cl -> (fold_commands cl,DEFAULTcast) + if internal then (e_red try_red_product,DEFAULTcast) + else (e_red red_product,DEFAULTcast) + | Hnf -> (e_red hnf_constr,DEFAULTcast) + | Simpl (f,o) -> + let whd_am = if !simplIsCbn then whd_cbn (make_flag f) else whd_simpl in + let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in + let () = + if not (!simplIsCbn || List.is_empty f.rConst) then + Pp.msg_warning (Pp.strbrk "The legacy simpl does not deal with delta flags.") in + (contextualize (if head_style then whd_am else am) am o,DEFAULTcast) + | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast) + | Cbn f -> + (e_red (strong_cbn (make_flag f)), DEFAULTcast) + | Lazy f -> (e_red (clos_norm_flags (make_flag f)),DEFAULTcast) + | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast) + | Fold cl -> (e_red (fold_commands cl),DEFAULTcast) | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast) | ExtraRedExpr s -> - (try (Stringmap.find s !reduction_tab,DEFAULTcast) + (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast) with Not_found -> - (try reduction_of_red_expr (Stringmap.find s !red_expr_tab) + (try reduction_of_red_expr (String.Map.find s !red_expr_tab) with Not_found -> error("unknown user-defined reduction \""^s^"\""))) - | CbvVm -> (cbv_vm ,VMcast) + | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast) + | CbvNative o -> (contextualize cbv_native cbv_native o, VMcast) + in + reduction_of_red_expr - -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 +let subst_red_expr subs = + Miscops.map_red_expr_gen (Mod_subst.subst_mps subs) (Mod_subst.subst_evaluable_reference subs) - (Pattern.subst_pattern subs) - e + (Patternops.subst_pattern subs) let inReduction : bool * string * red_expr -> obj = declare_object @@ -229,8 +256,3 @@ let inReduction : bool * string * red_expr -> 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