From 913ccc7fb4a987ddd7c591d3c7d75579dc502a95 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 6 Dec 2018 08:07:32 +0100 Subject: [api] Move reduction modules to `tactics` These modules do actually belong there. We have to slightly reorganize printers, removing a couple of duplicated ones in the way. --- interp/genredexpr.ml | 65 ---------- interp/interp.mllib | 2 - interp/redops.ml | 64 --------- interp/redops.mli | 20 --- interp/stdarg.ml | 5 - interp/stdarg.mli | 13 -- plugins/btauto/refl_btauto.ml | 7 +- plugins/firstorder/g_ground.mlg | 2 +- plugins/ltac/extraargs.mlg | 2 +- plugins/ltac/pptactic.ml | 14 +- plugins/ltac/pptactic.mli | 3 +- plugins/ltac/tacexpr.ml | 5 +- plugins/ltac/tacexpr.mli | 5 +- printing/ppconstr.ml | 15 --- printing/ppconstr.mli | 5 - printing/pputils.ml | 99 +++----------- printing/pputils.mli | 24 +--- proofs/proofs.mllib | 1 - proofs/redexpr.ml | 278 ---------------------------------------- proofs/redexpr.mli | 48 ------- proofs/tacmach.ml | 6 - proofs/tacmach.mli | 4 - tactics/genredexpr.ml | 79 ++++++++++++ tactics/ppred.ml | 83 ++++++++++++ tactics/ppred.mli | 19 +++ tactics/redexpr.ml | 278 ++++++++++++++++++++++++++++++++++++++++ tactics/redexpr.mli | 48 +++++++ tactics/redops.ml | 64 +++++++++ tactics/redops.mli | 20 +++ tactics/tactics.ml | 2 +- tactics/tactics.mllib | 4 + vernac/ppvernac.ml | 6 +- vernac/pvernac.ml | 2 +- 33 files changed, 633 insertions(+), 659 deletions(-) delete mode 100644 interp/genredexpr.ml delete mode 100644 interp/redops.ml delete mode 100644 interp/redops.mli delete mode 100644 proofs/redexpr.ml delete mode 100644 proofs/redexpr.mli create mode 100644 tactics/genredexpr.ml create mode 100644 tactics/ppred.ml create mode 100644 tactics/ppred.mli create mode 100644 tactics/redexpr.ml create mode 100644 tactics/redexpr.mli create mode 100644 tactics/redops.ml create mode 100644 tactics/redops.mli diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml deleted file mode 100644 index 607f2258fd..0000000000 --- a/interp/genredexpr.ml +++ /dev/null @@ -1,65 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* red - | FBeta :: lf -> add_flag { red with rBeta = true } lf - | FMatch :: lf -> add_flag { red with rMatch = true } lf - | FFix :: lf -> add_flag { red with rFix = true } lf - | FCofix :: lf -> add_flag { red with rCofix = true } lf - | FZeta :: lf -> add_flag { red with rZeta = true } lf - | FConst l :: lf -> - if red.rDelta then - CErrors.user_err Pp.(str - "Cannot set both constants to unfold and constants not to unfold"); - add_flag { red with rConst = union_consts red.rConst l } lf - | FDeltaBut l :: lf -> - if red.rConst <> [] && not red.rDelta then - CErrors.user_err Pp.(str - "Cannot set both constants to unfold and constants not to unfold"); - add_flag - { red with rConst = union_consts red.rConst l; rDelta = true } - lf - in - add_flag - {rBeta = false; rMatch = false; rFix = false; rCofix = false; - rZeta = false; rDelta = false; rConst = []} - l - - -let all_flags = - {rBeta = true; rMatch = true; rFix = true; rCofix = true; - rZeta = true; rDelta = true; rConst = []} - -(** Mapping [red_expr_gen] *) - -let map_flags f flags = - { flags with rConst = List.map f flags.rConst } - -let map_occs f (occ,e) = (occ,f e) - -let map_red_expr_gen f g h = function - | Fold l -> Fold (List.map f l) - | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l) - | Simpl (flags,occs_o) -> - Simpl (map_flags g flags, Option.map (map_occs (Util.map_union g h)) occs_o) - | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l) - | Cbv flags -> Cbv (map_flags g flags) - | Lazy flags -> Lazy (map_flags g flags) - | CbvVm occs_o -> CbvVm (Option.map (map_occs (Util.map_union g h)) occs_o) - | CbvNative occs_o -> CbvNative (Option.map (map_occs (Util.map_union g h)) occs_o) - | Cbn flags -> Cbn (map_flags g flags) - | ExtraRedExpr _ | Red _ | Hnf as x -> x diff --git a/interp/redops.mli b/interp/redops.mli deleted file mode 100644 index 7254f29b25..0000000000 --- a/interp/redops.mli +++ /dev/null @@ -1,20 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 'a glob_red_flag - -val all_flags : 'a glob_red_flag - -(** Mapping [red_expr_gen] *) - -val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) -> - ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 7b01b6dc1c..bf3a8fe215 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -11,8 +11,6 @@ open Genarg open Geninterp -type 'a and_short_name = 'a * Names.lident option - let make0 ?dyn name = let wit = Genarg.make0 name in let () = register_val0 wit dyn in @@ -53,8 +51,6 @@ let wit_uconstr = make0 "uconstr" let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr" -let wit_red_expr = make0 "redexpr" - let wit_clause_dft_concl = make0 "clause_dft_concl" @@ -65,4 +61,3 @@ let wit_preident = wit_pre_ident let wit_reference = wit_ref let wit_global = wit_ref let wit_clause = wit_clause_dft_concl -let wit_redexpr = wit_red_expr diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 5e5e43ed38..c974a4403c 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -14,15 +14,11 @@ open Loc open Names open EConstr open Libnames -open Genredexpr -open Pattern open Constrexpr open Genarg open Genintern open Locus -type 'a and_short_name = 'a * lident option - val wit_unit : unit uniform_genarg_type val wit_bool : bool uniform_genarg_type @@ -52,11 +48,6 @@ val wit_uconstr : (constr_expr , glob_constr_and_expr, Ltac_pretype.closed_glob_ val wit_open_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type -val wit_red_expr : - ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen, - (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, - (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type - val wit_clause_dft_concl : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type (** Aliases for compatibility *) @@ -66,7 +57,3 @@ val wit_preident : string uniform_genarg_type val wit_reference : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_global : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type -val wit_redexpr : - ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen, - (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, - (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 07f50f6cd5..4d817625f5 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -164,11 +164,12 @@ module Btauto = struct let reify env t = lapp eval [|convert_env env; convert t|] - let print_counterexample p env gl = + let print_counterexample p penv gl = let var = lapp witness [|p|] in let var = EConstr.of_constr var in (* Compute an assignment that dissatisfies the goal *) - let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in + let redfun, _ = Redexpr.reduction_of_red_expr (Refiner.pf_env gl) Genredexpr.(CbvVm None) in + let _, var = redfun Refiner.(pf_env gl) Refiner.(project gl) var in let var = EConstr.Unsafe.to_constr var in let rec to_list l = match decomp_term (Tacmach.project gl) l with | App (c, _) @@ -192,7 +193,7 @@ module Btauto = struct let msg = try let var = to_list var in - let assign = List.combine env var in + let assign = List.combine penv var in let map_msg (key, v) = let b = if v then str "true" else str "false" in let sigma, env = Pfedit.get_current_context () in diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 37fc81ee38..ea86a4b514 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -132,7 +132,7 @@ let normalize_evaluables= open Ppconstr open Printer let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid -let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x))) +let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (Pputils.pr_or_var (fun x -> pr_global (snd x))) let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global let warn_deprecated_syntax = diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index 156ee94a66..5d5d45c58f 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -314,7 +314,7 @@ END let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c -let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Ppconstr.pr_lident cl +let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Pputils.pr_lident cl let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl let in_clause' = Pltac.in_clause diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 55e58187b0..8bf1855fe0 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -22,8 +22,8 @@ open Tactypes open Locus open Decl_kinds open Genredexpr -open Pputils open Ppconstr +open Pputils open Printer open Genintern @@ -159,8 +159,8 @@ let string_of_genarg_arg (ArgumentType arg) = end | _ -> default - let pr_with_occurrences pr c = pr_with_occurrences pr keyword c - let pr_red_expr pr c = pr_red_expr pr keyword c + let pr_with_occurrences pr c = Ppred.pr_with_occurrences pr keyword c + let pr_red_expr pr c = Ppred.pr_red_expr pr keyword c let pr_may_eval test prc prlc pr2 pr3 = function | ConstrEval (r,c) -> @@ -186,12 +186,6 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_and_short_name pr (c,_) = pr c - let pr_or_by_notation f = CAst.with_val (function - | AN v -> f v - | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc) - - let pr_located pr (_,x) = pr x - let pr_evaluable_reference = function | EvalVarRef id -> pr_id id | EvalConstRef sp -> pr_global (Globnames.ConstRef sp) @@ -694,7 +688,7 @@ let pr_goal_selector ~toplevel s = (* match t with | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal | _ ->*) - let s = prlist_with_sep spc Ppconstr.pr_lname nal ++ str ":" ++ pr.pr_lconstr t in + let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in spc() ++ hov 1 (str"(" ++ s ++ str")") in let pr_fix_tac (id,n,c) = diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 0ab9e501bc..bc47036d92 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -98,8 +98,7 @@ val pr_may_eval : ('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) -> ('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t -val pr_and_short_name : ('a -> Pp.t) -> 'a Stdarg.and_short_name -> Pp.t -val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t +val pr_and_short_name : ('a -> Pp.t) -> 'a Genredexpr.and_short_name -> Pp.t val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 2bd21f9d7a..b99f956ce0 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -270,7 +270,7 @@ constraint 'a = < type g_trm = Genintern.glob_constr_and_expr type g_pat = Genintern.glob_constr_pattern_and_expr -type g_cst = evaluable_global_reference Stdarg.and_short_name or_var +type g_cst = evaluable_global_reference Genredexpr.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident @@ -296,9 +296,6 @@ type glob_tactic_arg = (** Raw tactics *) -type r_trm = constr_expr -type r_pat = constr_pattern_expr -type r_cst = qualid or_by_notation type r_ref = qualid type r_nam = lident type r_lev = rlevel diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 0c27f3bfe2..bd080bf4f0 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -269,7 +269,7 @@ constraint 'a = < type g_trm = Genintern.glob_constr_and_expr type g_pat = Genintern.glob_constr_pattern_and_expr -type g_cst = evaluable_global_reference Stdarg.and_short_name or_var +type g_cst = evaluable_global_reference Genredexpr.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident @@ -295,9 +295,6 @@ type glob_tactic_arg = (** Raw tactics *) -type r_trm = constr_expr -type r_pat = constr_pattern_expr -type r_cst = qualid or_by_notation type r_ref = qualid type r_nam = lident type r_lev = rlevel diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 6d53349fa1..26202ef4ca 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -14,7 +14,6 @@ open Util open Pp open CAst open Names -open Nameops open Libnames open Pputils open Ppextend @@ -230,20 +229,6 @@ let tag_var = tag Tag.variable | { CAst.v = CHole (_,IntroAnonymous,_) } -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t - let pr_lident {loc; v=id} = - match loc with - | None -> pr_id id - | Some loc -> let (b,_) = Loc.unloc loc in - pr_located pr_id (Some (Loc.make_loc (b,b + String.length (Id.to_string id))), id) - - let pr_lname = function - | {CAst.loc; v=Name id} -> pr_lident CAst.(make ?loc id) - | x -> pr_ast Name.print x - - let pr_or_var pr = function - | Locus.ArgArg x -> pr x - | Locus.ArgVar id -> pr_lident id - let pr_prim_token = function | Numeral (n,s) -> str (if s then n else "-"^n) | String s -> qs s diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index e7f71849a5..1cb3aa6d7a 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -21,11 +21,6 @@ val prec_less : precedence -> tolerability -> bool val pr_tight_coma : unit -> Pp.t -val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t - -val pr_lident : lident -> Pp.t -val pr_lname : lname -> Pp.t - val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t val pr_com_at : int -> Pp.t val pr_sep_com : diff --git a/printing/pputils.ml b/printing/pputils.ml index 59e5f68f22..e6daf9544c 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -12,7 +12,6 @@ open Util open Pp open Genarg open Locus -open Genredexpr let beautify_comments = ref [] @@ -39,91 +38,25 @@ let pr_located pr (loc, x) = let pr_ast pr { CAst.loc; v } = pr_located pr (loc, v) -let pr_or_var pr = function - | ArgArg x -> pr x - | ArgVar {CAst.v=s} -> Names.Id.print s - -let pr_with_occurrences pr keyword (occs,c) = - match occs with - | AllOccurrences -> - pr c - | NoOccurrences -> - failwith "pr_with_occurrences: no occurrences" - | OnlyOccurrences nl -> - hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++ - hov 0 (prlist_with_sep spc (pr_or_var int) nl)) - | AllOccurrencesBut nl -> - hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++ - hov 0 (prlist_with_sep spc (pr_or_var int) nl)) - -exception ComplexRedFlag - -let pr_short_red_flag pr r = - if not r.rBeta || not r.rMatch || not r.rFix || not r.rCofix || not r.rZeta then - raise ComplexRedFlag - else if List.is_empty r.rConst then - if r.rDelta then mt () else raise ComplexRedFlag - else (if r.rDelta then str "-" else mt ()) ++ - hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]") - -let pr_red_flag pr r = - try pr_short_red_flag pr r - with ComplexRedFlag -> - (if r.rBeta then pr_arg str "beta" else mt ()) ++ - (if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else - (if r.rMatch then pr_arg str "match" else mt ()) ++ - (if r.rFix then pr_arg str "fix" else mt ()) ++ - (if r.rCofix then pr_arg str "cofix" else mt ())) ++ - (if r.rZeta then pr_arg str "zeta" else mt ()) ++ - (if List.is_empty r.rConst then - if r.rDelta then pr_arg str "delta" - else mt () - else - pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++ - hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")) - -let pr_union pr1 pr2 = function - | Inl a -> pr1 a - | Inr b -> pr2 b - -let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function - | Red false -> keyword "red" - | Hnf -> keyword "hnf" - | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f) - ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o - | Cbv f -> - if f.rBeta && f.rMatch && f.rFix && f.rCofix && - f.rZeta && f.rDelta && List.is_empty f.rConst then - keyword "compute" - else - hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f) - | Lazy f -> - hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f) - | Cbn f -> - hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f) - | Unfold l -> - hov 1 (keyword "unfold" ++ spc() ++ - prlist_with_sep pr_comma (pr_with_occurrences pr_ref keyword) l) - | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l) - | Pattern l -> - hov 1 (keyword "pattern" ++ - pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr keyword)) l) +let pr_lident { CAst.loc; v=id } = + let open Names.Id in + match loc with + | None -> print id + | Some loc -> let (b,_) = Loc.unloc loc in + pr_located print + (Some (Loc.make_loc (b,b + String.length (to_string id))), id) - | Red true -> - CErrors.user_err Pp.(str "Shouldn't be accessible from user.") - | ExtraRedExpr s -> - str s - | CbvVm o -> - keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o - | CbvNative o -> - keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o +let pr_lname = let open Names in function + | {CAst.loc; v=Name id} -> pr_lident CAst.(make ?loc id) + | x -> pr_ast Name.print x -let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) = - pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma) +let pr_or_var pr = function + | ArgArg x -> pr x + | ArgVar id -> pr_lident id -let pr_or_by_notation f = let open Constrexpr in function - | {CAst.loc; v=AN v} -> f v - | {CAst.loc; v=ByNotation (s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc +let pr_or_by_notation f = let open Constrexpr in CAst.with_val (function + | AN v -> f v + | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc) let hov_if_not_empty n p = if Pp.ismt p then p else hov n p diff --git a/printing/pputils.mli b/printing/pputils.mli index 5b1969e232..ea554355bc 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -8,33 +8,17 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open Genarg -open Locus -open Genredexpr val pr_located : ('a -> Pp.t) -> 'a Loc.located -> Pp.t val pr_ast : ('a -> Pp.t) -> 'a CAst.t -> Pp.t (** Prints an object surrounded by its commented location *) -val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t +val pr_lident : lident -> Pp.t +val pr_lname : lname -> Pp.t +val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t val pr_or_by_notation : ('a -> Pp.t) -> 'a Constrexpr.or_by_notation -> Pp.t -val pr_with_occurrences : - ('a -> Pp.t) -> (string -> Pp.t) -> 'a with_occurrences -> Pp.t - -val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t -val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t - -val pr_red_expr : - ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> - (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t - -val pr_red_expr_env : Environ.env -> Evd.evar_map -> - (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * - (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * - ('b -> Pp.t) * - (Environ.env -> Evd.evar_map -> 'c -> Pp.t) -> - (string -> Pp.t) -> - ('a,'b,'c) red_expr_gen -> Pp.t val pr_raw_generic : Environ.env -> rlevel generic_argument -> Pp.t val pr_glb_generic : Environ.env -> glevel generic_argument -> Pp.t diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index dbd5be23ab..0ce726db25 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -7,7 +7,6 @@ Logic Goal_select Proof_bullet Proof_global -Redexpr Refiner Tacmach Pfedit diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml deleted file mode 100644 index 6658c37f41..0000000000 --- a/proofs/redexpr.ml +++ /dev/null @@ -1,278 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* - strbrk "native_compute disabled at configure time; falling back to vm_compute.") - -let cbv_native env sigma c = - if Coq_config.native_compiler then - let ctyp = Retyping.get_type_of env sigma c in - Nativenorm.native_norm env sigma c ctyp - else - (warn_native_compute_disabled (); - cbv_vm env sigma c) - -let whd_cbn flags env sigma t = - let (state,_) = - (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t,Reductionops.Stack.empty)) - in - Reductionops.Stack.zip ~refold:true sigma state - -let strong_cbn flags = - strong_with_flags whd_cbn flags - -let simplIsCbn = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optname = - "Plug the simpl tactic to the new cbn mechanism"; - optkey = ["SimplIsCbn"]; - optread = (fun () -> !simplIsCbn); - 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 - Global.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 - (match cb.const_body with - | OpaqueDef _ -> - user_err ~hdr:"set_transparent_const" - (str "Cannot make" ++ spc () ++ - Nametab.pr_global_env Id.Set.empty (GlobRef.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,(local,obj)) = - local, - List.Smart.map - (fun (k,ql as entry) -> - let ql' = List.Smart.map (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 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 - -let disch_ref ref = - match ref with - EvalConstRef c -> Some ref - | EvalVarRef id -> if Lib.is_in_section (GlobRef.VarRef id) then None else Some ref - -let discharge_strategy (_,(local,obj)) = - if local then None else - map_strategy disch_ref obj - -type strategy_obj = - bool * (Conv_oracle.level * evaluable_global_reference list) list - -let inStrategy : strategy_obj -> obj = - 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 } - - -let set_strategy local str = - Lib.add_anonymous_leaf (inStrategy (local,str)) - -(* Generic reduction: reduction functions used in reduction tactics *) - -type red_expr = - (constr, evaluable_global_reference, constr_pattern) red_expr_gen - -let make_flag_constant = function - | EvalVarRef id -> fVAR id - | EvalConstRef sp -> fCONST sp - -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.rMatch then red_add red fMATCH else red in - let red = if f.rFix then red_add red fFIX else red in - let red = if f.rCofix then red_add red fCOFIX else red in - let red = if f.rZeta then red_add red fZETA else red in - 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 (Environ.oracle env)) in - List.fold_right - (fun v red -> red_sub red (make_flag_constant v)) - f.rConst red - else (* Only rConst *) - let red = red_add_transparent (red_add red fDELTA) TransparentState.empty in - List.fold_right - (fun v red -> red_add red (make_flag_constant v)) - f.rConst red - in red - -(* table of custom reductino fonctions, not synchronized, - filled via ML calls to [declare_reduction] *) -let reduction_tab = ref String.Map.empty - -(* table of custom reduction expressions, synchronized, - filled by command Declare Reduction *) -let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction" - -let declare_reduction s f = - if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then user_err ~hdr:"Redexpr.declare_reduction" - (str "There is already a reduction expression of name " ++ str s) - else reduction_tab := String.Map.add s f !reduction_tab - -let check_custom = function - | ExtraRedExpr s -> - if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab) - then user_err ~hdr:"Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s) - |_ -> () - -let decl_red_expr s e = - if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then user_err ~hdr:"Redexpr.decl_red_expr" - (str "There is already a reduction expression of name " ++ str s) - else begin - check_custom e; - red_expr_tab := String.Map.add s e !red_expr_tab - end - -let out_arg = function - | Locus.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.") - | Locus.ArgArg x -> x - -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 warn_simpl_unfolding_modifiers = - CWarnings.create ~name:"simpl-unfolding-modifiers" ~category:"tactics" - (fun () -> - Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.") - -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 (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 - warn_simpl_unfolding_modifiers () 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 (e_red (String.Map.find s !reduction_tab),DEFAULTcast) - with Not_found -> - (try reduction_of_red_expr (String.Map.find s !red_expr_tab) - with Not_found -> - user_err ~hdr:"Redexpr.reduction_of_red_expr" - (str "unknown user-defined reduction \"" ++ str s ++ str "\""))) - | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast) - | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast) - in - reduction_of_red_expr - -let subst_mps subst c = - EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c)) - -let subst_red_expr subs = - Redops.map_red_expr_gen - (subst_mps subs) - (Mod_subst.subst_evaluable_reference subs) - (Patternops.subst_pattern subs) - -let inReduction : bool * string * red_expr -> obj = - 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)) diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli deleted file mode 100644 index 1e59f436c3..0000000000 --- a/proofs/redexpr.mli +++ /dev/null @@ -1,48 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* occurrences * 'a - -val reduction_of_red_expr : - Environ.env -> red_expr -> e_reduction_function * cast_kind - -(** [true] if we should use the vm to verify the reduction *) - -(** Adding a custom reduction (function to be use at the ML level) - NB: the effect is permanent. *) -val declare_reduction : string -> reduction_function -> unit - -(** Adding a custom reduction (function to be called a vernac command). - The boolean flag is the locality. *) -val declare_red_expr : bool -> string -> red_expr -> unit - -(** Opaque and Transparent commands. *) - -(** 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 diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 64d7630d55..eed68b058b 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -15,7 +15,6 @@ open Environ open Reductionops open Evd open Typing -open Redexpr open Tacred open Logic open Context.Named.Declaration @@ -71,11 +70,6 @@ let pf_global gls id = let sigma = project gls in Evd.fresh_global env sigma (Constrintern.construct_reference (pf_hyps gls) id) -let pf_reduction_of_red_expr gls re c = - let (redfun, _) = reduction_of_red_expr (pf_env gls) re in - let sigma = project gls in - redfun (pf_env gls) sigma c - let pf_apply f gls = f (pf_env gls) (project gls) let pf_eapply f gls x = on_sig gls (fun evm -> f (pf_env gls) evm x) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index ef6a1544e4..213ed7bfda 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -12,7 +12,6 @@ open Names open Constr open Environ open EConstr -open Redexpr open Locus (** Operations for handling terms under a local typing context. *) @@ -44,9 +43,6 @@ val pf_get_hyp_typ : Goal.goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> Goal.goal sigma -> Id.t -val pf_reduction_of_red_expr : Goal.goal sigma -> red_expr -> constr -> evar_map * constr - - val pf_apply : (env -> evar_map -> 'a) -> Goal.goal sigma -> 'a val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) -> Goal.goal sigma -> 'a -> Goal.goal sigma * 'b diff --git a/tactics/genredexpr.ml b/tactics/genredexpr.ml new file mode 100644 index 0000000000..8209684c37 --- /dev/null +++ b/tactics/genredexpr.ml @@ -0,0 +1,79 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + str s + | CbvVm o -> + keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o + | CbvNative o -> + keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o + +let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) = + pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma) diff --git a/tactics/ppred.mli b/tactics/ppred.mli new file mode 100644 index 0000000000..b3a306a36f --- /dev/null +++ b/tactics/ppred.mli @@ -0,0 +1,19 @@ +open Genredexpr + +val pr_with_occurrences : + ('a -> Pp.t) -> (string -> Pp.t) -> 'a Locus.with_occurrences -> Pp.t + +val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t +val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t + +val pr_red_expr : + ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> + (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t + +val pr_red_expr_env : Environ.env -> Evd.evar_map -> + (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * + (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * + ('b -> Pp.t) * + (Environ.env -> Evd.evar_map -> 'c -> Pp.t) -> + (string -> Pp.t) -> + ('a,'b,'c) red_expr_gen -> Pp.t diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml new file mode 100644 index 0000000000..aabfae444e --- /dev/null +++ b/tactics/redexpr.ml @@ -0,0 +1,278 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + strbrk "native_compute disabled at configure time; falling back to vm_compute.") + +let cbv_native env sigma c = + if Coq_config.native_compiler then + let ctyp = Retyping.get_type_of env sigma c in + Nativenorm.native_norm env sigma c ctyp + else + (warn_native_compute_disabled (); + cbv_vm env sigma c) + +let whd_cbn flags env sigma t = + let (state,_) = + (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t,Reductionops.Stack.empty)) + in + Reductionops.Stack.zip ~refold:true sigma state + +let strong_cbn flags = + strong_with_flags whd_cbn flags + +let simplIsCbn = ref (false) +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = + "Plug the simpl tactic to the new cbn mechanism"; + optkey = ["SimplIsCbn"]; + optread = (fun () -> !simplIsCbn); + 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 + Global.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 + (match cb.const_body with + | OpaqueDef _ -> + user_err ~hdr:"set_transparent_const" + (str "Cannot make" ++ spc () ++ + Nametab.pr_global_env Id.Set.empty (GlobRef.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,(local,obj)) = + local, + List.Smart.map + (fun (k,ql as entry) -> + let ql' = List.Smart.map (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 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 + +let disch_ref ref = + match ref with + EvalConstRef c -> Some ref + | EvalVarRef id -> if Lib.is_in_section (GlobRef.VarRef id) then None else Some ref + +let discharge_strategy (_,(local,obj)) = + if local then None else + map_strategy disch_ref obj + +type strategy_obj = + bool * (Conv_oracle.level * evaluable_global_reference list) list + +let inStrategy : strategy_obj -> obj = + 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 } + + +let set_strategy local str = + Lib.add_anonymous_leaf (inStrategy (local,str)) + +(* Generic reduction: reduction functions used in reduction tactics *) + +type red_expr = + (constr, evaluable_global_reference, constr_pattern) red_expr_gen + +let make_flag_constant = function + | EvalVarRef id -> fVAR id + | EvalConstRef sp -> fCONST sp + +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.rMatch then red_add red fMATCH else red in + let red = if f.rFix then red_add red fFIX else red in + let red = if f.rCofix then red_add red fCOFIX else red in + let red = if f.rZeta then red_add red fZETA else red in + 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 (Environ.oracle env)) in + List.fold_right + (fun v red -> red_sub red (make_flag_constant v)) + f.rConst red + else (* Only rConst *) + let red = red_add_transparent (red_add red fDELTA) TransparentState.empty in + List.fold_right + (fun v red -> red_add red (make_flag_constant v)) + f.rConst red + in red + +(* table of custom reductino fonctions, not synchronized, + filled via ML calls to [declare_reduction] *) +let reduction_tab = ref String.Map.empty + +(* table of custom reduction expressions, synchronized, + filled by command Declare Reduction *) +let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction" + +let declare_reduction s f = + if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab + then user_err ~hdr:"Redexpr.declare_reduction" + (str "There is already a reduction expression of name " ++ str s) + else reduction_tab := String.Map.add s f !reduction_tab + +let check_custom = function + | ExtraRedExpr s -> + if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab) + then user_err ~hdr:"Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s) + |_ -> () + +let decl_red_expr s e = + if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab + then user_err ~hdr:"Redexpr.decl_red_expr" + (str "There is already a reduction expression of name " ++ str s) + else begin + check_custom e; + red_expr_tab := String.Map.add s e !red_expr_tab + end + +let out_arg = function + | Locus.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.") + | Locus.ArgArg x -> x + +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 warn_simpl_unfolding_modifiers = + CWarnings.create ~name:"simpl-unfolding-modifiers" ~category:"tactics" + (fun () -> + Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.") + +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 (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 + warn_simpl_unfolding_modifiers () 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 (e_red (String.Map.find s !reduction_tab),DEFAULTcast) + with Not_found -> + (try reduction_of_red_expr (String.Map.find s !red_expr_tab) + with Not_found -> + user_err ~hdr:"Redexpr.reduction_of_red_expr" + (str "unknown user-defined reduction \"" ++ str s ++ str "\""))) + | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast) + | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast) + in + reduction_of_red_expr + +let subst_mps subst c = + EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c)) + +let subst_red_expr subs = + Redops.map_red_expr_gen + (subst_mps subs) + (Mod_subst.subst_evaluable_reference subs) + (Patternops.subst_pattern subs) + +let inReduction : bool * string * red_expr -> obj = + 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)) diff --git a/tactics/redexpr.mli b/tactics/redexpr.mli new file mode 100644 index 0000000000..1f65862701 --- /dev/null +++ b/tactics/redexpr.mli @@ -0,0 +1,48 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* occurrences * 'a + +val reduction_of_red_expr : + Environ.env -> red_expr -> e_reduction_function * cast_kind + +(** [true] if we should use the vm to verify the reduction *) + +(** Adding a custom reduction (function to be use at the ML level) + NB: the effect is permanent. *) +val declare_reduction : string -> reduction_function -> unit + +(** Adding a custom reduction (function to be called a vernac command). + The boolean flag is the locality. *) +val declare_red_expr : bool -> string -> red_expr -> unit + +(** Opaque and Transparent commands. *) + +(** 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 diff --git a/tactics/redops.ml b/tactics/redops.ml new file mode 100644 index 0000000000..6f83ea9a34 --- /dev/null +++ b/tactics/redops.ml @@ -0,0 +1,64 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* red + | FBeta :: lf -> add_flag { red with rBeta = true } lf + | FMatch :: lf -> add_flag { red with rMatch = true } lf + | FFix :: lf -> add_flag { red with rFix = true } lf + | FCofix :: lf -> add_flag { red with rCofix = true } lf + | FZeta :: lf -> add_flag { red with rZeta = true } lf + | FConst l :: lf -> + if red.rDelta then + CErrors.user_err Pp.(str + "Cannot set both constants to unfold and constants not to unfold"); + add_flag { red with rConst = union_consts red.rConst l } lf + | FDeltaBut l :: lf -> + if red.rConst <> [] && not red.rDelta then + CErrors.user_err Pp.(str + "Cannot set both constants to unfold and constants not to unfold"); + add_flag + { red with rConst = union_consts red.rConst l; rDelta = true } + lf + in + add_flag + {rBeta = false; rMatch = false; rFix = false; rCofix = false; + rZeta = false; rDelta = false; rConst = []} + l + + +let all_flags = + {rBeta = true; rMatch = true; rFix = true; rCofix = true; + rZeta = true; rDelta = true; rConst = []} + +(** Mapping [red_expr_gen] *) + +let map_flags f flags = + { flags with rConst = List.map f flags.rConst } + +let map_occs f (occ,e) = (occ,f e) + +let map_red_expr_gen f g h = function + | Fold l -> Fold (List.map f l) + | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l) + | Simpl (flags,occs_o) -> + Simpl (map_flags g flags, Option.map (map_occs (Util.map_union g h)) occs_o) + | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l) + | Cbv flags -> Cbv (map_flags g flags) + | Lazy flags -> Lazy (map_flags g flags) + | CbvVm occs_o -> CbvVm (Option.map (map_occs (Util.map_union g h)) occs_o) + | CbvNative occs_o -> CbvNative (Option.map (map_occs (Util.map_union g h)) occs_o) + | Cbn flags -> Cbn (map_flags g flags) + | ExtraRedExpr _ | Red _ | Hnf as x -> x diff --git a/tactics/redops.mli b/tactics/redops.mli new file mode 100644 index 0000000000..7254f29b25 --- /dev/null +++ b/tactics/redops.mli @@ -0,0 +1,20 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* 'a glob_red_flag + +val all_flags : 'a glob_red_flag + +(** Mapping [red_expr_gen] *) + +val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) -> + ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b3ea13cf4f..9bd4a29a69 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -889,7 +889,7 @@ let reduce redexp cl = let trace env sigma = let open Printer in let pr = (pr_econstr_env, pr_leconstr_env, pr_evaluable_reference, pr_constr_pattern_env) in - Pp.(hov 2 (Pputils.pr_red_expr_env env sigma pr str redexp)) + Pp.(hov 2 (Ppred.pr_red_expr_env env sigma pr str redexp)) in let trace () = let sigma, env = Pfedit.get_current_context () in diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 5afec74fae..1861c5b99b 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -6,6 +6,10 @@ Hipattern Ind_tables Eqschemes Elimschemes +Genredexpr +Redops +Redexpr +Ppred Tactics Abstract Elim diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index e7c1e29beb..46854b7f5d 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -700,7 +700,7 @@ open Pputils | None -> mt() | Some r -> keyword "Eval" ++ spc() ++ - pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++ + Ppred.pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) keyword r ++ keyword " in" ++ spc() in let pr_def_body = function @@ -1134,7 +1134,7 @@ open Pputils let pr_mayeval r c = match r with | Some r0 -> hov 2 (keyword "Eval" ++ spc() ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++ + Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r0 ++ spc() ++ keyword "in" ++ spc () ++ pr_lconstr c) | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) in @@ -1146,7 +1146,7 @@ open Pputils | VernacDeclareReduction (s,r) -> return ( keyword "Declare Reduction" ++ spc () ++ str s ++ str " := " ++ - pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r + Ppred.pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) keyword r ) | VernacPrint p -> return (pr_printable p) diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index f26e0d0885..a647b2ef73 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -52,4 +52,4 @@ let set_command_entry e = Vernac_.command_entry_ref := e let get_command_entry () = !Vernac_.command_entry_ref let () = - register_grammar Stdarg.wit_red_expr (Vernac_.red_expr); + register_grammar Genredexpr.wit_red_expr (Vernac_.red_expr); -- cgit v1.2.3 From 1d0e7063fe10fbf27a1b0a8296c69ed6b661d70e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 6 Dec 2018 18:43:49 +0100 Subject: [ci] Clean overlay folder. --- .../user-overlays/07925-ppedrot-clean-transp-state.sh | 14 -------------- .../08705-ejgallego-vernac+remove_empty_hooks.sh | 18 ------------------ dev/ci/user-overlays/08850-poly-local-univs.sh | 9 --------- dev/ci/user-overlays/08889-mattam-program-obl-subst.sh | 6 ------ .../08902-ejgallego-ltac+use_atts_in_ast.sh | 15 --------------- .../08914-ejgallego-lib+better_boot_coqproject.sh | 6 ------ .../08933-solve-remaining-evars-initial-arg.sh | 6 ------ .../08985-ejgallego-build+pack_gramlib.sh | 6 ------ .../08998-ejgallego-legacy_proof_eng_clean.sh | 6 ------ .../09003-ejgallego-vernac+move_extend_ast.sh | 6 ------ .../09051-ppedrot-camlp5-safe-api-strikes-back.sh | 9 --------- .../user-overlays/09065-ejgallego-gramlib+no_ploc.sh | 6 ------ 12 files changed, 107 deletions(-) delete mode 100644 dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh delete mode 100644 dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh delete mode 100644 dev/ci/user-overlays/08850-poly-local-univs.sh delete mode 100644 dev/ci/user-overlays/08889-mattam-program-obl-subst.sh delete mode 100644 dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh delete mode 100644 dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh delete mode 100644 dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh delete mode 100644 dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh delete mode 100644 dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh delete mode 100644 dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh delete mode 100644 dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh delete mode 100644 dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh diff --git a/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh b/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh deleted file mode 100644 index b05d02c5be..0000000000 --- a/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh +++ /dev/null @@ -1,14 +0,0 @@ -_OVERLAY_BRANCH=clean-transp-state - -if [ "$CI_PULL_REQUEST" = "7925" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then - - unicoq_CI_REF="$_OVERLAY_BRANCH" - unicoq_CI_GITURL=https://github.com/ppedrot/unicoq - - equations_CI_REF="$_OVERLAY_BRANCH" - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - - mtac2_CI_REF="$_OVERLAY_BRANCH" - mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 - -fi diff --git a/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh b/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh deleted file mode 100644 index 3600f1cd3e..0000000000 --- a/dev/ci/user-overlays/08705-ejgallego-vernac+remove_empty_hooks.sh +++ /dev/null @@ -1,18 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8705" ] || [ "$CI_BRANCH" = "vernac+remove_empty_hooks" ]; then - - elpi_CI_REF=vernac+remove_empty_hooks - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - equations_CI_REF=vernac+remove_empty_hooks - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - paramcoq_CI_REF=vernac+remove_empty_hooks - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - plugin_tutorial_CI_REF=vernac+remove_empty_hooks - plugin_tutorial_CI_GITURL=https://github.com/ejgallego/plugin_tutorials - - mtac2_CI_REF=vernac+remove_empty_hooks - mtac2_CI_GITURL=https://github.com/ejgallego/mtac2 - -fi diff --git a/dev/ci/user-overlays/08850-poly-local-univs.sh b/dev/ci/user-overlays/08850-poly-local-univs.sh deleted file mode 100644 index 482792d7cd..0000000000 --- a/dev/ci/user-overlays/08850-poly-local-univs.sh +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8850" ] || [ "$CI_BRANCH" = "poly-local-univs" ]; then - formal_topology_CI_REF=poly-local-univs - formal_topology_CI_GITURL=https://github.com/SkySkimmer/topology - - paramcoq_CI_REF=poly-local-univs - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq -fi diff --git a/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh b/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh deleted file mode 100644 index 17eb5fffae..0000000000 --- a/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8889" ] || [ "$CI_BRANCH" = "program-hook-obligation-subst" ]; then - - Equations_CI_REF=program-hook-obligation-subst - Equations_CI_GITURL=https://github.com/mattam82/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh b/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh deleted file mode 100644 index 08112d3054..0000000000 --- a/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8902" ] || [ "$CI_BRANCH" = "ltac+use_atts_in_ast" ]; then - - aactactics_CI_REF=ltac+use_atts_in_ast - aactactics_CI_GITURL=https://github.com/ejgallego/aac-tactics - - coqhammer_CI_REF=ltac+use_atts_in_ast - coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer - - Equations_CI_REF=ltac+use_atts_in_ast - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - mtac2_CI_REF=ltac+use_atts_in_ast - mtac2_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh b/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh deleted file mode 100644 index 1c5157ba12..0000000000 --- a/dev/ci/user-overlays/08914-ejgallego-lib+better_boot_coqproject.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8914" ] || [ "$CI_BRANCH" = "lib+better_boot_coqproject" ]; then - - quickchick_CI_REF=lib+better_boot_coqproject - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh b/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh deleted file mode 100644 index e74e53fa40..0000000000 --- a/dev/ci/user-overlays/08933-solve-remaining-evars-initial-arg.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "8933" ] || [ "$CI_BRANCH" = "solve-remaining-evars-initial-arg" ]; then - plugin_tutorial_CI_REF=solve-remaining-evars-initial-arg - plugin_tutorial_CI_GITURL=https://github.com/SkySkimmer/plugin_tutorials -fi diff --git a/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh b/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh deleted file mode 100644 index d7130cc67a..0000000000 --- a/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8985" ] || [ "$CI_BRANCH" = "build+pack_gramlib" ]; then - - elpi_CI_REF=use_coq_gramlib - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - -fi diff --git a/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh deleted file mode 100644 index c8bea0c868..0000000000 --- a/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8998" ] || [ "$CI_BRANCH" = "legacy_proof_eng_clean" ]; then - - equations_CI_REF=legacy_proof_eng_clean - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh b/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh deleted file mode 100644 index 61ffa4a197..0000000000 --- a/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9003" ] || [ "$CI_BRANCH" = "vernac+move_extend_ast" ]; then - - ltac2_CI_REF=vernac+move_extend_ast - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - -fi diff --git a/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh b/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh deleted file mode 100644 index 14e7c0d7f0..0000000000 --- a/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9051" ] || [ "$CI_BRANCH" = "camlp5-safe-api-strikes-back" ]; then - - equations_CI_REF=camlp5-safe-api-strikes-back - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - - ltac2_CI_REF=camlp5-safe-api-strikes-back - ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 - -fi diff --git a/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh b/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh deleted file mode 100644 index e9daa7a44e..0000000000 --- a/dev/ci/user-overlays/09065-ejgallego-gramlib+no_ploc.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9065" ] || [ "$CI_BRANCH" = "gramlib+no_ploc" ]; then - - elpi_CI_REF=gramlib+no_ploc - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - -fi -- cgit v1.2.3