From 2a69be9e8243fa67d5c7ef5f10e623b02a0a3e2f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 21 May 2018 19:21:26 +0200 Subject: [api] Move `Constrexpr` to the `interp` module. Continuing the interface cleanup we place `Constrexpr` in the internalization module, which is the one that eliminates it. This slims down `pretyping` considerably, including removing the `Univdecls` module which existed only due to bad dependency ordering in the first place. Thanks to @ Skyskimmer we also remove a duplicate `univ_decl` definition among `Misctypes` and `UState`. This is mostly a proof of concept yet as it depends on quite a few patches of the tree. For sure some tweaks will be necessary, but it should be good for review now. IMO the tree is now in a state where we can could easy eliminate more than 10 modules without any impact, IMHO this is a net saving API-wise and would help people to understand the structure of the code better. --- pretyping/constrexpr.ml | 153 --------------------------------------- pretyping/genredexpr.ml | 66 ----------------- pretyping/miscops.ml | 21 ------ pretyping/miscops.mli | 6 -- pretyping/pretyping.mllib | 4 - pretyping/redops.ml | 44 ----------- pretyping/redops.mli | 15 ---- pretyping/typeclasses_errors.ml | 4 - pretyping/typeclasses_errors.mli | 4 - pretyping/univdecls.ml | 52 ------------- pretyping/univdecls.mli | 21 ------ 11 files changed, 390 deletions(-) delete mode 100644 pretyping/constrexpr.ml delete mode 100644 pretyping/genredexpr.ml delete mode 100644 pretyping/redops.ml delete mode 100644 pretyping/redops.mli delete mode 100644 pretyping/univdecls.ml delete mode 100644 pretyping/univdecls.mli (limited to 'pretyping') diff --git a/pretyping/constrexpr.ml b/pretyping/constrexpr.ml deleted file mode 100644 index 1443dfb51..000000000 --- a/pretyping/constrexpr.ml +++ /dev/null @@ -1,153 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Names.Id.equal id1 id2 | _ -> false -(** 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 (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 (map_union g h)) occs_o) - | CbvNative occs_o -> CbvNative (Option.map (map_occs (map_union g h)) occs_o) - | Cbn flags -> Cbn (map_flags g flags) - | ExtraRedExpr _ | Red _ | Hnf as x -> x - (** Mapping bindings *) let map_explicit_bindings f l = diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli index 1d4504541..6a84fb9eb 100644 --- a/pretyping/miscops.mli +++ b/pretyping/miscops.mli @@ -9,7 +9,6 @@ (************************************************************************) open Misctypes -open Genredexpr (** Mapping [cast_type] *) @@ -25,11 +24,6 @@ val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool val intro_pattern_naming_eq : intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool -(** 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 - (** Mapping bindings *) val map_bindings : ('a -> 'b) -> 'a bindings -> 'b bindings diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index c48decdb0..3d9b5d3cf 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -16,13 +16,10 @@ Evarsolve Recordops Evarconv Typing -Constrexpr -Genredexpr Miscops Glob_term Ltac_pretype Glob_ops -Redops Pattern Patternops Constr_matching @@ -37,4 +34,3 @@ Indrec Cases Pretyping Unification -Univdecls diff --git a/pretyping/redops.ml b/pretyping/redops.ml deleted file mode 100644 index 90c3bdfae..000000000 --- a/pretyping/redops.ml +++ /dev/null @@ -1,44 +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 = []} diff --git a/pretyping/redops.mli b/pretyping/redops.mli deleted file mode 100644 index 285931ecd..000000000 --- a/pretyping/redops.mli +++ /dev/null @@ -1,15 +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 diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 89c5d7e7b..a1ac53c73 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -12,7 +12,6 @@ open Names open EConstr open Environ -open Constrexpr (*i*) type contexts = Parameters | Properties @@ -20,7 +19,6 @@ type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr | UnboundMethod of GlobRef.t * Misctypes.lident (* Class name, method *) - | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (* found, expected *) exception TypeClassError of env * typeclass_error @@ -29,5 +27,3 @@ let typeclass_error env err = raise (TypeClassError (env, err)) let not_a_class env c = typeclass_error env (NotAClass c) let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id)) - -let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m)) diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 4aabc0aee..1003f2ae1 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -11,14 +11,12 @@ open Names open EConstr open Environ -open Constrexpr type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr | UnboundMethod of GlobRef.t * Misctypes.lident (** Class name, method *) - | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (** found, expected *) exception TypeClassError of env * typeclass_error @@ -26,5 +24,3 @@ val not_a_class : env -> constr -> 'a val unbound_method : env -> GlobRef.t -> Misctypes.lident -> 'a -val mismatched_ctx_inst : env -> contexts -> constr_expr list -> Context.Rel.t -> 'a - diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml deleted file mode 100644 index 8864be576..000000000 --- a/pretyping/univdecls.ml +++ /dev/null @@ -1,52 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* - user_err ~hdr:"interp_constraint" - (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e) - in - List.fold_left interp (evd,Univ.Constraint.empty) cstrs - -let interp_univ_decl env decl = - let open Misctypes in - let pl : lident list = decl.univdecl_instance in - let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in - let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in - let decl = { univdecl_instance = pl; - univdecl_extensible_instance = decl.univdecl_extensible_instance; - univdecl_constraints = cstrs; - univdecl_extensible_constraints = decl.univdecl_extensible_constraints } - in evd, decl - -let interp_univ_decl_opt env l = - match l with - | None -> Evd.from_env env, default_univ_decl - | Some decl -> interp_univ_decl env decl diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli deleted file mode 100644 index 305d045b1..000000000 --- a/pretyping/univdecls.mli +++ /dev/null @@ -1,21 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Constrexpr.universe_decl_expr -> - Evd.evar_map * universe_decl - -val interp_univ_decl_opt : Environ.env -> Constrexpr.universe_decl_expr option -> - Evd.evar_map * universe_decl -- cgit v1.2.3