From 79ff2bc044aa86a5ce30f0c24647db8c8e2544fa Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 2 Apr 2018 04:26:09 +0200 Subject: [api] Remove dependency of library on Vernacexpr. Morally, `library` should not depend on the vernacular definition. This will also create problems when trying to modularize the codebase due to the cycle [vernacs depend for example on constrexprs]. The fix is fortunately easy. --- .../user-overlays/07152-ejgallego-api+vernac_expr_iso.sh | 12 ++++++++++++ intf/vernacexpr.ml | 12 +++++++----- library/declaremods.ml | 16 +++++++++++++++- library/declaremods.mli | 16 +++++++++++++++- parsing/g_vernac.ml4 | 1 + printing/ppvernac.ml | 7 ++++--- vernac/classes.ml | 2 +- vernac/comAssumption.ml | 3 +-- vernac/comAssumption.mli | 4 ++-- vernac/vernacentries.ml | 2 +- 10 files changed, 59 insertions(+), 16 deletions(-) create mode 100644 dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh diff --git a/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh b/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh new file mode 100644 index 000000000..7e554684e --- /dev/null +++ b/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "7152" ] || [ "$CI_BRANCH" = "api+vernac_expr_iso" ]; then + + # Equations_CI_BRANCH=ssr+correct_packing + # Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + # ltac2_CI_BRANCH=ssr+correct_packing + # ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Elpi_CI_BRANCH=api+vernac_expr_iso + Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git + +fi diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 06f969f19..4e1c986f1 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -281,20 +281,22 @@ type bullet = (** Rigid / flexible module signature *) -type 'a module_signature = +type 'a module_signature = 'a Declaremods.module_signature = | Enforce of 'a (** ... : T *) | Check of 'a list (** ... <: T1 <: T2, possibly empty *) +[@@ocaml.deprecated "please use [Declaremods.module_signature]."] (** Which module inline annotations should we honor, either None or the ones whose level is less or equal to the given integer *) -type inline = +type inline = Declaremods.inline = | NoInline | DefaultInline | InlineAt of int +[@@ocaml.deprecated "please use [Declaremods.inline]."] -type module_ast_inl = module_ast * inline +type module_ast_inl = module_ast * Declaremods.inline type module_binder = bool option * lident list * module_ast_inl (** [Some b] if locally enabled/disabled according to [b], [None] if @@ -333,7 +335,7 @@ type nonrec vernac_expr = | VernacEndProof of proof_end | VernacExactProof of constr_expr | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) * - inline * (ident_decl list * constr_expr) with_coercion list + Declaremods.inline * (ident_decl list * constr_expr) with_coercion list | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list @@ -373,7 +375,7 @@ type nonrec vernac_expr = | VernacDeclareModule of bool option * lident * module_binder list * module_ast_inl | VernacDefineModule of bool option * lident * module_binder list * - module_ast_inl module_signature * module_ast_inl list + module_ast_inl Declaremods.module_signature * module_ast_inl list | VernacDeclareModuleType of lident * module_binder list * module_ast_inl list * module_ast_inl list | VernacInclude of module_ast_inl list diff --git a/library/declaremods.ml b/library/declaremods.ml index 762efc5e3..1d5df49cf 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -17,11 +17,25 @@ open Entries open Libnames open Libobject open Mod_subst -open Vernacexpr open Misctypes (** {6 Inlining levels} *) +(** Rigid / flexible module signature *) + +type 'a module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) + +(** Which module inline annotations should we honor, + either None or the ones whose level is less or equal + to the given integer *) + +type inline = + | NoInline + | DefaultInline + | InlineAt of int + let default_inline () = Some (Flags.get_inline_level ()) let inl2intopt = function diff --git a/library/declaremods.mli b/library/declaremods.mli index fd8d29614..4aee7feae 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -9,10 +9,24 @@ (************************************************************************) open Names -open Vernacexpr (** {6 Modules } *) +(** Rigid / flexible module signature *) + +type 'a module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) + +(** Which module inline annotations should we honor, + either None or the ones whose level is less or equal + to the given integer *) + +type inline = + | NoInline + | DefaultInline + | InlineAt of int + type 'modast module_interpretor = Environ.env -> Misctypes.module_kind -> 'modast -> Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 593dcbf58..2dbd624c2 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -17,6 +17,7 @@ open Constrexpr open Constrexpr_ops open Extend open Decl_kinds +open Declaremods open Declarations open Misctypes open Tok (* necessary for camlp5 *) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 7eb8396ac..83c875707 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -16,12 +16,13 @@ open Util open CAst open Extend -open Vernacexpr -open Pputils open Libnames +open Decl_kinds open Constrexpr open Constrexpr_ops -open Decl_kinds +open Vernacexpr +open Declaremods +open Pputils open Ppconstr diff --git a/vernac/classes.ml b/vernac/classes.ml index 76d427add..ae653974a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -425,7 +425,7 @@ let context poly l = let nstatus = match b with | None -> pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl - Vernacexpr.NoInline (CAst.make id)) + Declaremods.NoInline (CAst.make id)) | Some b -> let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~univs ~types:t b in diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 6a590758f..26a46a752 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -20,7 +20,6 @@ open Constrintern open Impargs open Decl_kinds open Pretyping -open Vernacexpr open Entries (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) @@ -66,7 +65,7 @@ match local with | Global | Local | Discharge -> let do_instance = should_axiom_into_instance local in let local = DeclareDef.get_locality ident ~kind:"axiom" local in - let inl = match nl with + let inl = let open Declaremods in match nl with | NoInline -> None | DefaultInline -> Some (Flags.get_inline_level()) | InlineAt i -> Some i diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 56e324376..a2d20a1d1 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -19,7 +19,7 @@ open Decl_kinds (** {6 Parameters/Assumptions} *) val do_assumptions : locality * polymorphic * assumption_object_kind -> - Vernacexpr.inline -> (ident_decl list * constr_expr) with_coercion list -> bool + Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list -> bool (************************************************************************) (** Internal API *) @@ -32,5 +32,5 @@ val do_assumptions : locality * polymorphic * assumption_object_kind -> val declare_assumption : coercion_flag -> assumption_kind -> types in_constant_universes_entry -> Universes.universe_binders -> Impargs.manual_implicits -> - bool (** implicit *) -> Vernacexpr.inline -> variable CAst.t -> + bool (** implicit *) -> Declaremods.inline -> variable CAst.t -> global_reference * Univ.Instance.t * bool diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index b44c7cccb..11e9dc16c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -672,7 +672,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast = else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_module_ast - id binders_ast (Enforce mty_ast) [] + id binders_ast (Declaremods.Enforce mty_ast) [] in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared"); -- cgit v1.2.3