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 ----------- 6 files changed, 169 deletions(-) delete mode 100644 interp/genredexpr.ml delete mode 100644 interp/redops.ml delete mode 100644 interp/redops.mli (limited to 'interp') 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 -- cgit v1.2.3