diff options
74 files changed, 452 insertions, 313 deletions
@@ -91,6 +91,7 @@ Changes from 8.8.0 to 8.8.1 Kernel - Fix a critical bug with cofixpoints and vm_compute/native_compute (#7333). +- Fix a critical bug with modules and algebraic universes (#7695) - Fix a critical bug with inlining of polymorphic constants (#7615). - Fix a critical bug with universe polymorphism and vm_compute (#7723). Was present since 8.5. @@ -100,6 +101,16 @@ Notations - Fixed unexpected collision between only-parsing and only-printing notations (issue #7462). +Windows installer + +- The Windows installer now includes external packages Ltac2 and Equations + (it included the Bignums package since 8.8+beta1). + +Many other bug fixes, documentation improvements (including fixes of +regressions due to the Sphinx migration), and user message improvements +(for details, see the 8.8.1 milestone at +https://github.com/coq/coq/milestone/13?closed=1). + Changes from 8.8+beta1 to 8.8.0 =============================== diff --git a/Makefile.build b/Makefile.build index b85418243..ed251af77 100644 --- a/Makefile.build +++ b/Makefile.build @@ -390,9 +390,10 @@ grammar/%.cmi: grammar/%.mli coqbinaries: $(TOPBIN) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) coqbyte: $(TOPBYTE) $(CHICKENBYTE) -# Special rule for coqtop +# Special rule for coqtop, we imitate `ocamlopt` can delete the target +# to avoid #7666 $(COQTOPEXE): $(TOPBIN:.opt=.$(BEST)) - cp $< $@ + rm -f $@ && cp $< $@ bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' diff --git a/dev/ci/user-overlays/7080-herbelin-master+swapping-modules-constr-context.sh b/dev/ci/user-overlays/7080-herbelin-master+swapping-modules-constr-context.sh new file mode 100644 index 000000000..b4d3d7e67 --- /dev/null +++ b/dev/ci/user-overlays/7080-herbelin-master+swapping-modules-constr-context.sh @@ -0,0 +1,7 @@ +if [ "$CI_PULL_REQUEST" = "7080" ] || [ "$CI_BRANCH" = "master+swapping-modules-constr-context" ]; then + Equations_CI_BRANCH=master+adapting-coq-pr7080 + Equations_CI_GITURL=https://github.com/herbelin/Coq-Equations.git + + Elpi_CI_BRANCH=coq-master+adapting-coq-pr7080 + Elpi_CI_GITURL=https://github.com/herbelin/coq-elpi.git +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 3e36b657d..e6d741159 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -53,6 +53,16 @@ Printer.ml API pr_subgoal and pr_goal was removed to simplify the code. It was earlierly used by PCoq. +Kernel + + The following renamings happened: + - `Context.Rel.t` into `Constr.rel_context` + - `Context.Named.t` into `Constr.named_context` + - `Context.Compacted.t` into `Constr.compacted_context` + - `Context.Rel.Declaration.t` into `Constr.rel_declaration` + - `Context.Named.Declaration.t` into `Constr.named_declaration` + - `Context.Compacted.Declaration.t` into `Constr.compacted_declaration` + Source code organization - We have eliminated / fused some redundant modules and relocated a diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex index 3867d4af9..8f9c3171d 100644 --- a/dev/doc/versions-history.tex +++ b/dev/doc/versions-history.tex @@ -395,7 +395,17 @@ Coq V8.7 beta 1 & released 6 September 2017 & \feature{bundled with Ssreflect pl Coq V8.7 beta 2 & released 6 October 2017 & \\ -Coq V8.7 & released 18 October 2016 & \\ +Coq V8.7.0 & released 18 October 2017 & \\ + +Coq V8.7.1 & released 15 December 2017 & \\ + +Coq V8.7.2 & released 17 February 2018 & \\ + +Coq V8.8 beta1 & released 19 March 2018 & \\ + +Coq V8.8.0 & released 17 April 2018 & \feature{reference manual moved to Sphinx} \\ +&& \feature{effort towards better documented, better structured ML API}\\ +&& \feature{miscellaneous changes/improvements of existing features}\\ \end{tabular} diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 811abd67f..ab679a71c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -232,7 +232,7 @@ let ppenv e = pp let ppenvwithcst e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ - str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).env_globals.env_constants (mt ()) ++ str "}") + str "{" ++ Environ.fold_constants (fun a _ s -> Constant.print a ++ spc () ++ s) e (mt ()) ++ str "}") let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x)) diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index 2562dec46..5d9324a65 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -1393,7 +1393,7 @@ Version 8.8 is the third release of |Coq| developed on a time-based development cycle. Its development spanned 6 months from the release of |Coq| 8.7 and was based on a public roadmap. The development process was coordinated by Matthieu Sozeau. Maxime Dénès was in charge of the -release process. +release process. Théo Zimmermann is the maintainer of this release. Many power users helped to improve the design of the new features via the bug tracker, the pull request system, the |Coq| development mailing diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 913825a9f..ecb36615f 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -321,7 +321,7 @@ sig val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt (** Physical identity. Does not care for defined evars. *) - val to_named_context : (t, types) Context.Named.pt -> Context.Named.t + val to_named_context : (t, types) Context.Named.pt -> Constr.named_context val to_sorts : ESorts.t -> Sorts.t (** Physical identity. Does not care for normalization. *) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 8ce1b625f..135aa73fc 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -128,7 +128,7 @@ val advance : evar_map -> Evar.t -> Evar.t option [nf_evar]. *) val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t -val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t +val undefined_evars_of_named_context : evar_map -> Constr.named_context -> Evar.Set.t val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t type undefined_evars_cache @@ -161,7 +161,7 @@ val jv_nf_evar : val tj_nf_evar : evar_map -> unsafe_type_judgment -> unsafe_type_judgment -val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t +val nf_named_context_evar : evar_map -> Constr.named_context -> Constr.named_context val nf_rel_context_evar : evar_map -> rel_context -> rel_context val nf_env_evar : evar_map -> env -> env diff --git a/engine/evd.mli b/engine/evd.mli index 64db70451..d638bb2d3 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -230,7 +230,7 @@ val existential_opt_value : evar_map -> econstr pexistential -> econstr option val existential_opt_value0 : evar_map -> existential -> constr option -val evar_instance_array : (Context.Named.Declaration.t -> 'a -> bool) -> evar_info -> +val evar_instance_array : (Constr.named_declaration -> 'a -> bool) -> evar_info -> 'a array -> (Id.t * 'a) list val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr diff --git a/engine/termops.mli b/engine/termops.mli index f9aa6ba63..80988989f 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -43,14 +43,14 @@ val it_mkProd : types -> (Name.t * types) list -> types val it_mkLambda : constr -> (Name.t * types) list -> constr val it_mkProd_or_LetIn : types -> rel_context -> types val it_mkProd_wo_LetIn : types -> rel_context -> types -val it_mkLambda_or_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr +val it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr val it_mkNamedProd_or_LetIn : types -> named_context -> types -val it_mkNamedProd_wo_LetIn : Constr.types -> Context.Named.t -> Constr.types +val it_mkNamedProd_wo_LetIn : Constr.types -> Constr.named_context -> Constr.types val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr (* Ad hoc version reinserting letin, assuming the body is defined in the context where the letins are expanded *) -val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr +val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr (** {6 Generic iterators on constr} *) @@ -225,7 +225,7 @@ val names_of_rel_context : env -> names_context (* [context_chop n Γ] returns (Γ₁,Γ₂) such that [Γ]=[Γ₂Γ₁], [Γ₁] has [n] hypotheses, excluding local definitions, and [Γ₁], if not empty, starts with an hypothesis (i.e. [Γ₁] has the form empty or [x:A;Γ₁'] *) -val context_chop : int -> Context.Rel.t -> Context.Rel.t * Context.Rel.t +val context_chop : int -> Constr.rel_context -> Constr.rel_context * Constr.rel_context (* [env_rel_context_chop n env] extracts out the [n] top declarations of the rel_context part of [env], counting both local definitions and @@ -239,19 +239,19 @@ val add_vname : Id.Set.t -> Name.t -> Id.Set.t (** other signature iterators *) val process_rel_context : (rel_declaration -> env -> env) -> env -> env val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Name.t * 't) list -val lift_rel_context : int -> Context.Rel.t -> Context.Rel.t -val substl_rel_context : Constr.constr list -> Context.Rel.t -> Context.Rel.t -val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in context *) +val lift_rel_context : int -> Constr.rel_context -> Constr.rel_context +val substl_rel_context : Constr.constr list -> Constr.rel_context -> Constr.rel_context +val smash_rel_context : Constr.rel_context -> Constr.rel_context (** expand lets in context *) val map_rel_context_in_env : - (env -> Constr.constr -> Constr.constr) -> env -> Context.Rel.t -> Context.Rel.t + (env -> Constr.constr -> Constr.constr) -> env -> Constr.rel_context -> Constr.rel_context val map_rel_context_with_binders : (int -> 'c -> 'c) -> ('c, 'c) Context.Rel.pt -> ('c, 'c) Context.Rel.pt val fold_named_context_both_sides : - ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) -> - Context.Named.t -> init:'a -> 'a + ('a -> Constr.named_declaration -> Constr.named_declaration list -> 'a) -> + Constr.named_context -> init:'a -> 'a val mem_named_context_val : Id.t -> named_context_val -> bool -val compact_named_context : Context.Named.t -> Context.Compacted.t +val compact_named_context : Constr.named_context -> Constr.compacted_context val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt @@ -313,6 +313,6 @@ val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit val print_constr : constr -> Pp.t val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t val print_named_context : env -> Pp.t -val pr_rel_decl : env -> Context.Rel.Declaration.t -> Pp.t +val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t val print_rel_context : env -> Pp.t val print_env : env -> Pp.t diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 83ad9af33..288a0bfe0 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -22,7 +22,7 @@ open Libobject open Nameops open Context.Rel.Declaration -exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *) +exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m)) module RelDecl = Context.Rel.Declaration diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index a8492095e..437fef175 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -38,14 +38,14 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits val combine_params_freevar : - Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t -> + Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> Constrexpr.constr_expr * Id.Set.t val implicit_application : Id.Set.t -> ?allow_partial:bool -> - (Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t -> + (Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> Constrexpr.constr_expr * Id.Set.t) -> constr_expr -> constr_expr * Id.Set.t (* Should be likely located elsewhere *) -exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *) -val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Context.Rel.t -> 'a +exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) +val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Constr.rel_context -> 'a diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 1d5142a5c..61ed40394 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -265,7 +265,7 @@ type 'a infos_cache = { i_repr : 'a infos -> 'a infos_tab -> constr -> 'a; i_env : env; i_sigma : existential -> constr option; - i_rels : (Context.Rel.Declaration.t * lazy_val) Range.t; + i_rels : (Constr.rel_declaration * lazy_val) Range.t; } and 'a infos = { diff --git a/kernel/clambda.ml b/kernel/clambda.ml index b722e4200..f1b6f3dff 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -814,7 +814,7 @@ let optimize_lambda lam = let lambda_of_constr ~optimize genv c = let env = Renv.make genv in - let ids = List.rev_map Context.Rel.Declaration.get_name genv.env_rel_context.env_rel_ctx in + let ids = List.rev_map Context.Rel.Declaration.get_name (rel_context genv) in Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env c in let lam = if optimize then optimize_lambda lam else lam in diff --git a/kernel/constr.ml b/kernel/constr.ml index 45812b5a1..9bf743152 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -1209,3 +1209,10 @@ let hcons = Id.hcons) (* let hcons_types = hcons_constr *) + +type rel_declaration = (constr, types) Context.Rel.Declaration.pt +type named_declaration = (constr, types) Context.Named.Declaration.pt +type compacted_declaration = (constr, types) Context.Compacted.Declaration.pt +type rel_context = rel_declaration list +type named_context = named_declaration list +type compacted_context = compacted_declaration list diff --git a/kernel/constr.mli b/kernel/constr.mli index bf7b5e87b..70acf1932 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -372,6 +372,15 @@ val eq_constr_nounivs : constr -> constr -> bool (** Total ordering compatible with [equal] *) val compare : constr -> constr -> int +(** {6 Extension of Context with declarations on constr} *) + +type rel_declaration = (constr, types) Context.Rel.Declaration.pt +type named_declaration = (constr, types) Context.Named.Declaration.pt +type compacted_declaration = (constr, types) Context.Compacted.Declaration.pt +type rel_context = rel_declaration list +type named_context = named_declaration list +type compacted_context = compacted_declaration list + (** {6 Functionals working on the immediate subterm of a construction } *) (** [fold f acc c] folds [f] on the immediate subterms of [c] diff --git a/kernel/context.ml b/kernel/context.ml index 5d4a10184..831dc850f 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -43,8 +43,6 @@ struct | LocalAssum of Name.t * 'types (** name, type *) | LocalDef of Name.t * 'constr * 'types (** name, value, type *) - type t = (Constr.constr, Constr.types) pt - (** Return the name bound by a given declaration. *) let get_name = function | LocalAssum (na,_) @@ -157,7 +155,6 @@ struct Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list (** empty rel-context *) let empty = [] @@ -241,8 +238,6 @@ struct | LocalAssum of Id.t * 'types (** identifier, type *) | LocalDef of Id.t * 'constr * 'types (** identifier, value, type *) - type t = (Constr.constr, Constr.types) pt - (** Return the identifier bound by a given declaration. *) let get_id = function | LocalAssum (id,_) -> id @@ -370,7 +365,6 @@ struct Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list (** empty named-context *) let empty = [] @@ -429,8 +423,6 @@ module Compacted = | LocalAssum of Id.t list * 'types | LocalDef of Id.t list * 'constr * 'types - type t = (Constr.constr, Constr.types) pt - let map_constr f = function | LocalAssum (ids, ty) as decl -> let ty' = f ty in @@ -454,7 +446,6 @@ module Compacted = end type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list let fold f l ~init = List.fold_right f l init end diff --git a/kernel/context.mli b/kernel/context.mli index c97db4348..957ac4b3d 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -35,8 +35,6 @@ sig | LocalAssum of Name.t * 'types (** name, type *) | LocalDef of Name.t * 'constr * 'types (** name, value, type *) - type t = (Constr.constr, Constr.types) pt - (** Return the name bound by a given declaration. *) val get_name : ('c, 't) pt -> Name.t @@ -93,7 +91,6 @@ sig Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list (** empty rel-context *) val empty : ('c, 't) pt @@ -153,8 +150,6 @@ sig | LocalAssum of Id.t * 'types (** identifier, type *) | LocalDef of Id.t * 'constr * 'types (** identifier, value, type *) - type t = (Constr.constr, Constr.types) pt - (** Return the identifier bound by a given declaration. *) val get_id : ('c, 't) pt -> Id.t @@ -220,7 +215,6 @@ sig Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list (** empty named-context *) val empty : ('c, 't) pt @@ -270,15 +264,12 @@ sig | LocalAssum of Id.t list * 'types | LocalDef of Id.t list * 'constr * 'types - type t = (Constr.constr, Constr.types) pt - val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt val of_named_decl : ('c, 't) Named.Declaration.pt -> ('c, 't) pt val to_named_context : ('c, 't) pt -> ('c, 't) Named.pt end type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list val fold : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a end diff --git a/kernel/cooking.ml b/kernel/cooking.ml index c7a84f617..521a7d890 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -157,7 +157,7 @@ type result = { cook_type : types; cook_universes : constant_universes; cook_inline : inline; - cook_context : Context.Named.t option; + cook_context : Constr.named_context option; } let on_body ml hy f = function diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 76c79335f..4c254d2ea 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -23,7 +23,7 @@ type result = { cook_type : types; cook_universes : constant_universes; cook_inline : inline; - cook_context : Context.Named.t option; + cook_context : Constr.named_context option; } val cook_constant : hcons:bool -> env -> recipe -> result diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 58fb5d66b..95078800e 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -80,7 +80,7 @@ type typing_flags = { (* some contraints are in constant_constraints, some other may be in * the OpaqueDef *) type constant_body = { - const_hyps : Context.Named.t; (** New: younger hyp at top *) + const_hyps : Constr.named_context; (** New: younger hyp at top *) const_body : constant_def; const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; @@ -138,7 +138,7 @@ type one_inductive_body = { mind_typename : Id.t; (** Name of the type: [Ii] *) - mind_arity_ctxt : Context.Rel.t; (** Arity context of [Ii] with parameters: [forall params, Ui] *) + mind_arity_ctxt : Constr.rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *) mind_arity : inductive_arity; (** Arity sort and original user arity *) @@ -196,13 +196,13 @@ type mutual_inductive_body = { mind_ntypes : int; (** Number of types in the block *) - mind_hyps : Context.Named.t; (** Section hypotheses on which the block depends *) + mind_hyps : Constr.named_context; (** Section hypotheses on which the block depends *) mind_nparams : int; (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *) mind_nparams_rec : int; (** Number of recursively uniform (i.e. ordinary) parameters *) - mind_params_ctxt : Context.Rel.t; (** The context of parameters (includes let-in declaration) *) + mind_params_ctxt : Constr.rel_context; (** The context of parameters (includes let-in declaration) *) mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) diff --git a/kernel/entries.ml b/kernel/entries.ml index 724ed9ec7..40873bea7 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -75,7 +75,7 @@ type 'a in_constant_universes_entry = 'a * constant_universes_entry type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) - const_entry_secctx : Context.Named.t option; + const_entry_secctx : Constr.named_context option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; @@ -85,7 +85,7 @@ type 'a definition_entry = { type section_def_entry = { secdef_body : constr; - secdef_secctx : Context.Named.t option; + secdef_secctx : Constr.named_context option; secdef_feedback : Stateid.t option; secdef_type : types option; } @@ -93,7 +93,7 @@ type section_def_entry = { type inline = int option (* inlining level, None for no inlining *) type parameter_entry = - Context.Named.t option * types in_constant_universes_entry * inline + Constr.named_context option * types in_constant_universes_entry * inline type 'a constant_entry = | DefinitionEntry of 'a definition_entry diff --git a/kernel/environ.ml b/kernel/environ.ml index 0e34a7165..4ab469803 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -55,7 +55,8 @@ type globals = { env_projections : projection_body Cmap_env.t; env_inductives : mind_key Mindmap_env.t; env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t} + env_modtypes : module_type_body MPmap.t; +} type stratification = { env_universes : UGraph.t; @@ -76,17 +77,17 @@ let dummy_lazy_val () = ref VKnone let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key) type named_context_val = { - env_named_ctx : Context.Named.t; - env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; + env_named_ctx : Constr.named_context; + env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t; } type rel_context_val = { - env_rel_ctx : Context.Rel.t; - env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; + env_rel_ctx : Constr.rel_context; + env_rel_map : (Constr.rel_declaration * lazy_val) Range.t; } type env = { - env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_globals : globals; env_named_context : named_context_val; (* section variables *) env_rel_context : rel_context_val; env_nb_rel : int; @@ -208,6 +209,9 @@ let lookup_named_val id env = let lookup_named_ctxt id ctxt = fst (Id.Map.find id ctxt.env_named_map) +let fold_constants f env acc = + Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc + (* Global constants *) let lookup_constant_key kn env = diff --git a/kernel/environ.mli b/kernel/environ.mli index 8928b32f1..0259dbbdd 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -46,13 +46,8 @@ type constant_key = constant_body * (link_info ref * key) type mind_key = mutual_inductive_body * link_info ref -type globals = { - env_constants : constant_key Cmap_env.t; - env_projections : projection_body Cmap_env.t; - env_inductives : mind_key Mindmap_env.t; - env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t -} +type globals +(** globals = constants + projections + inductive types + modules + module-types *) type stratification = { env_universes : UGraph.t; @@ -60,17 +55,17 @@ type stratification = { } type named_context_val = private { - env_named_ctx : Context.Named.t; - env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; + env_named_ctx : Constr.named_context; + env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t; } type rel_context_val = private { - env_rel_ctx : Context.Rel.t; - env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; + env_rel_ctx : Constr.rel_context; + env_rel_map : (Constr.rel_declaration * lazy_val) Range.t; } type env = private { - env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_globals : globals; env_named_context : named_context_val; (* section variables *) env_rel_context : rel_context_val; env_nb_rel : int; @@ -88,8 +83,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool val empty_env : env val universes : env -> UGraph.t -val rel_context : env -> Context.Rel.t -val named_context : env -> Context.Named.t +val rel_context : env -> Constr.rel_context +val named_context : env -> Constr.named_context val named_context_val : env -> named_context_val val opaque_tables : env -> Opaqueproof.opaquetab @@ -108,13 +103,13 @@ val empty_context : env -> bool (** {5 Context of de Bruijn variables ([rel_context]) } *) val nb_rel : env -> int -val push_rel : Context.Rel.Declaration.t -> env -> env -val push_rel_context : Context.Rel.t -> env -> env +val push_rel : Constr.rel_declaration -> env -> env +val push_rel_context : Constr.rel_context -> env -> env val push_rec_types : rec_declaration -> env -> env (** Looks up in the context of local vars referred by indice ([rel_context]) raises [Not_found] if the index points out of the context *) -val lookup_rel : int -> env -> Context.Rel.Declaration.t +val lookup_rel : int -> env -> Constr.rel_declaration val lookup_rel_val : int -> env -> lazy_val val evaluable_rel : int -> env -> bool val env_of_rel : int -> env -> env @@ -122,12 +117,12 @@ val env_of_rel : int -> env -> env (** {6 Recurrence on [rel_context] } *) val fold_rel_context : - (env -> Context.Rel.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a + (env -> Constr.rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a (** {5 Context of variables (section variables and goal assumptions) } *) -val named_context_of_val : named_context_val -> Context.Named.t -val val_of_named_context : Context.Named.t -> named_context_val +val named_context_of_val : named_context_val -> Constr.named_context +val val_of_named_context : Constr.named_context -> named_context_val val empty_named_context_val : named_context_val val ids_of_named_context_val : named_context_val -> Id.Set.t @@ -138,19 +133,19 @@ val ids_of_named_context_val : named_context_val -> Id.Set.t val map_named_val : (constr -> constr) -> named_context_val -> named_context_val -val push_named : Context.Named.Declaration.t -> env -> env -val push_named_context : Context.Named.t -> env -> env +val push_named : Constr.named_declaration -> env -> env +val push_named_context : Constr.named_context -> env -> env val push_named_context_val : - Context.Named.Declaration.t -> named_context_val -> named_context_val + Constr.named_declaration -> named_context_val -> named_context_val (** Looks up in the context of local vars referred by names ([named_context]) raises [Not_found] if the Id.t is not found *) -val lookup_named : variable -> env -> Context.Named.Declaration.t +val lookup_named : variable -> env -> Constr.named_declaration val lookup_named_val : variable -> env -> lazy_val -val lookup_named_ctxt : variable -> named_context_val -> Context.Named.Declaration.t +val lookup_named_ctxt : variable -> named_context_val -> Constr.named_declaration val evaluable_named : variable -> env -> bool val named_type : variable -> env -> types val named_body : variable -> env -> constr option @@ -158,13 +153,13 @@ val named_body : variable -> env -> constr option (** {6 Recurrence on [named_context]: older declarations processed first } *) val fold_named_context : - (env -> Context.Named.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a + (env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a val set_universes : env -> UGraph.t -> env (** Recurrence on [named_context] starting from younger decl *) val fold_named_context_reverse : - ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a + ('a -> Constr.named_declaration -> 'a) -> init:'a -> env -> 'a (** This forgets named and rel contexts *) val reset_context : env -> env @@ -175,6 +170,9 @@ val reset_with_named_context : named_context_val -> env -> env (** This removes the [n] last declarations from the rel context *) val pop_rel_context : int -> env -> env +(** Useful for printing *) +val fold_constants : (Constant.t -> constant_body -> 'a -> 'a) -> env -> 'a -> 'a + (** {5 Global constants } {6 Add entries to global environment } *) @@ -280,7 +278,7 @@ val vars_of_global : env -> constr -> Id.Set.t val really_needed : env -> Id.Set.t -> Id.Set.t (** like [really_needed] but computes a well ordered named context *) -val keep_hyps : env -> Id.Set.t -> Context.Named.t +val keep_hyps : env -> Id.Set.t -> Constr.named_context (** {5 Unsafe judgments. } We introduce here the pre-type of judgments, which is @@ -309,10 +307,10 @@ exception Hyp_not_found return [tail::(f head (id,_,_) (rev tail))::head]. the value associated to id should not change *) val apply_to_hyp : named_context_val -> variable -> - (Context.Named.t -> Context.Named.Declaration.t -> Context.Named.t -> Context.Named.Declaration.t) -> + (Constr.named_context -> Constr.named_declaration -> Constr.named_context -> Constr.named_declaration) -> named_context_val -val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val +val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declaration) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val @@ -320,6 +318,7 @@ open Retroknowledge (** functions manipulating the retroknowledge @author spiwack *) val retroknowledge : (retroknowledge->'a) -> env -> 'a +[@@ocaml.deprecated "Use the record projection."] val registered : env -> field -> bool diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e63f43849..61b71df31 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -425,7 +425,7 @@ let typecheck_inductive env mie = type ill_formed_ind = | LocalNonPos of int | LocalNotEnoughArgs of int - | LocalNotConstructor of Context.Rel.t * int + | LocalNotConstructor of Constr.rel_context * int | LocalNonPar of int * int * int exception IllFormedInd of ill_formed_ind diff --git a/kernel/inductive.mli b/kernel/inductive.mli index c7982f1fc..3c1464c6c 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -36,7 +36,7 @@ val lookup_mind_specif : env -> inductive -> mind_specif (** {6 Functions to build standard types related to inductive } *) val ind_subst : MutInd.t -> mutual_inductive_body -> Instance.t -> constr list -val inductive_paramdecls : mutual_inductive_body puniverses -> Context.Rel.t +val inductive_paramdecls : mutual_inductive_body puniverses -> Constr.rel_context val instantiate_inductive_constraints : mutual_inductive_body -> Instance.t -> Constraint.t @@ -87,7 +87,7 @@ val build_branches_type : constr list -> constr -> types array (** Return the arity of an inductive type *) -val mind_arity : one_inductive_body -> Context.Rel.t * Sorts.family +val mind_arity : one_inductive_body -> Constr.rel_context * Sorts.family val inductive_sort_family : one_inductive_body -> Sorts.family @@ -115,8 +115,8 @@ exception SingletonInductiveBecomesProp of Id.t val max_inductive_sort : Sorts.t array -> Universe.t -val instantiate_universes : env -> Context.Rel.t -> - template_arity -> constr Lazy.t array -> Context.Rel.t * Sorts.t +val instantiate_universes : env -> Constr.rel_context -> + template_arity -> constr Lazy.t array -> Constr.rel_context * Sorts.t (** {6 Debug} *) diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 50713b957..07a02f6ef 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -5,8 +5,8 @@ UGraph Esubst Sorts Evar -Constr Context +Constr Vars Term Mod_subst diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 74d12f3cd..1748e98a4 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1845,7 +1845,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = in let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in let auxdefs = List.fold_right get_named_val fv_named auxdefs in - let lvl = Context.Rel.length env.env_rel_context.env_rel_ctx in + let lvl = Context.Rel.length (rel_context env) in let fv_rel = List.map (fun (n,_) -> MLglobal (Grel (lvl-n))) fv_rel in let fv_named = List.map (fun (id,_) -> MLglobal (Gnamed id)) fv_named in let aux_name = fresh_lname Anonymous in @@ -1854,7 +1854,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = and compile_rel env sigma univ auxdefs n = let open Context.Rel.Declaration in let decl = lookup_rel n env in - let n = List.length env.env_rel_context.env_rel_ctx - n in + let n = List.length (rel_context env) - n in match decl with | LocalDef (_,t,_) -> let code = lambda_of_constr env sigma t in diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 244e5e0dd..5843cd543 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -659,7 +659,7 @@ let optimize lam = let lambda_of_constr env sigma c = set_global_env env; let env = Renv.make () in - let ids = List.rev_map RelDecl.get_name !global_env.env_rel_context.env_rel_ctx in + let ids = List.rev_map RelDecl.get_name (rel_context !global_env) in Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env sigma c in (* if Flags.vm_draw_opt () then begin diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index a484c08e8..f8b71e456 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -18,7 +18,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; - abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t } + abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } type proofterm = (constr * Univ.ContextSet.t) Future.computation type opaque = | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index b6ae80b46..5ea6da649 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -51,7 +51,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; - abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t } + abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } (* The type has two caveats: 1) cook_constr is defined after diff --git a/kernel/reduction.mli b/kernel/reduction.mli index e53ab6aef..581e8bd88 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -116,10 +116,10 @@ val betazeta_appvect : int -> constr -> constr array -> constr (*********************************************************************** s Recognizing products and arities modulo reduction *) -val dest_prod : env -> types -> Context.Rel.t * types -val dest_prod_assum : env -> types -> Context.Rel.t * types -val dest_lam : env -> types -> Context.Rel.t * constr -val dest_lam_assum : env -> types -> Context.Rel.t * types +val dest_prod : env -> types -> Constr.rel_context * types +val dest_prod_assum : env -> types -> Constr.rel_context * types +val dest_lam : env -> constr -> Constr.rel_context * constr +val dest_lam_assum : env -> constr -> Constr.rel_context * constr exception NotArity diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 12c82e20d..f87ec9e02 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -897,9 +897,11 @@ let typing senv = Typeops.infer (env_of_senv senv) (** {6 Retroknowledge / native compiler } *) +[@@@ocaml.warning "-3"] (** universal lifting, used for the "get" operations mostly *) let retroknowledge f senv = Environ.retroknowledge f (env_of_senv senv) +[@@@ocaml.warning "+3"] let register field value by_clause senv = (* todo : value closed, by_clause safe, by_clause of the proper type*) @@ -918,7 +920,7 @@ let register_inline kn senv = if not (evaluable_constant kn senv.env) then CErrors.user_err Pp.(str "Register inline: an evaluable constant is expected"); let env = senv.env in - let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in + let cb = lookup_constant kn env in let cb = {cb with const_inline_code = true} in let env = add_constant kn cb env in { senv with env} diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 4078a9092..aca77ccd1 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -221,6 +221,7 @@ val delta_of_senv : open Retroknowledge val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a +[@@ocaml.deprecated "Use the projection of Environ.env"] val register : field -> Retroknowledge.entry -> Constr.constr -> safe_transformer0 diff --git a/kernel/term.ml b/kernel/term.ml index 81e344e73..4851a9c0d 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -336,7 +336,7 @@ let strip_lam_n n t = snd (decompose_lam_n n t) Such a term can canonically be seen as the pair of a context of types and of a sort *) -type arity = Context.Rel.t * Sorts.t +type arity = Constr.rel_context * Sorts.t let destArity = let open Context.Rel.Declaration in diff --git a/kernel/term.mli b/kernel/term.mli index 4d340399d..181d714ed 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -25,14 +25,14 @@ val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr val mkNamedProd : Id.t -> types -> types -> types (** Constructs either [(x:t)c] or [[x=b:t]c] *) -val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types -val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types -val mkNamedProd_or_LetIn : Context.Named.Declaration.t -> types -> types -val mkNamedProd_wo_LetIn : Context.Named.Declaration.t -> types -> types +val mkProd_or_LetIn : Constr.rel_declaration -> types -> types +val mkProd_wo_LetIn : Constr.rel_declaration -> types -> types +val mkNamedProd_or_LetIn : Constr.named_declaration -> types -> types +val mkNamedProd_wo_LetIn : Constr.named_declaration -> types -> types (** Constructs either [[x:t]c] or [[x=b:t]c] *) -val mkLambda_or_LetIn : Context.Rel.Declaration.t -> constr -> constr -val mkNamedLambda_or_LetIn : Context.Named.Declaration.t -> constr -> constr +val mkLambda_or_LetIn : Constr.rel_declaration -> constr -> constr +val mkNamedLambda_or_LetIn : Constr.named_declaration -> constr -> constr (** {5 Other term constructors. } *) @@ -74,8 +74,8 @@ val to_lambda : int -> constr -> constr where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *) val to_prod : int -> constr -> constr -val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr -val it_mkProd_or_LetIn : types -> Context.Rel.t -> types +val it_mkLambda_or_LetIn : constr -> Constr.rel_context -> constr +val it_mkProd_or_LetIn : types -> Constr.rel_context -> types (** In [lambda_applist c args], [c] is supposed to have the form [λΓ.c] with [Γ] without let-in; it returns [c] with the variables @@ -126,29 +126,29 @@ val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr (** Extract the premisses and the conclusion of a term of the form "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *) -val decompose_prod_assum : types -> Context.Rel.t * types +val decompose_prod_assum : types -> Constr.rel_context * types (** Idem with lambda's and let's *) -val decompose_lam_assum : constr -> Context.Rel.t * constr +val decompose_lam_assum : constr -> Constr.rel_context * constr (** Idem but extract the first [n] premisses, counting let-ins. *) -val decompose_prod_n_assum : int -> types -> Context.Rel.t * types +val decompose_prod_n_assum : int -> types -> Constr.rel_context * types (** Idem for lambdas, _not_ counting let-ins *) -val decompose_lam_n_assum : int -> constr -> Context.Rel.t * constr +val decompose_lam_n_assum : int -> constr -> Constr.rel_context * constr (** Idem, counting let-ins *) -val decompose_lam_n_decls : int -> constr -> Context.Rel.t * constr +val decompose_lam_n_decls : int -> constr -> Constr.rel_context * constr (** Return the premisses/parameters of a type/term (let-in included) *) -val prod_assum : types -> Context.Rel.t -val lam_assum : constr -> Context.Rel.t +val prod_assum : types -> Constr.rel_context +val lam_assum : constr -> Constr.rel_context (** Return the first n-th premisses/parameters of a type (let included and counted) *) -val prod_n_assum : int -> types -> Context.Rel.t +val prod_n_assum : int -> types -> Constr.rel_context (** Return the first n-th premisses/parameters of a term (let included but not counted) *) -val lam_n_assum : int -> constr -> Context.Rel.t +val lam_n_assum : int -> constr -> Constr.rel_context (** Remove the premisses/parameters of a type/term *) val strip_prod : types -> types @@ -167,7 +167,7 @@ val strip_lam_assum : constr -> constr Such a term can canonically be seen as the pair of a context of types and of a sort *) -type arity = Context.Rel.t * Sorts.t +type arity = Constr.rel_context * Sorts.t (** Build an "arity" from its canonical form *) val mkArity : arity -> types diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 3b2abc777..57acdfe4b 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -28,7 +28,7 @@ val infer_v : env -> constr array -> unsafe_judgment array val infer_type : env -> types -> unsafe_type_judgment val infer_local_decls : - env -> (Id.t * local_entry) list -> (env * Context.Rel.t) + env -> (Id.t * local_entry) list -> (env * Constr.rel_context) (** {6 Basic operations of the typing machine. } *) @@ -102,4 +102,4 @@ val judge_of_case : env -> case_info val type_of_constant_in : env -> pconstant -> types (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit +val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Constr.named_context -> unit diff --git a/kernel/vars.mli b/kernel/vars.mli index a0c7ba4bd..fdddbdb34 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -70,10 +70,10 @@ type substl = constr list as if usable in [applist] while the substitution is represented the other way round, i.e. ending with either [u₁] or [c₁], as if usable for [substl]. *) -val subst_of_rel_context_instance : Context.Rel.t -> constr list -> substl +val subst_of_rel_context_instance : Constr.rel_context -> constr list -> substl (** For compatibility: returns the substitution reversed *) -val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list +val adjust_subst_to_rel_context : Constr.rel_context -> constr list -> constr list (** Take an index in an instance of a context and returns its index wrt to the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *) @@ -97,13 +97,13 @@ val subst1 : constr -> constr -> constr accordingly indexes in [a₁],...,[an] and [c]. In terms of typing, if Γ ⊢ a{_n}..a₁ : Δ and Γ, Δ, Γ', Ω ⊢ with |Γ'|=[k], then Γ, Γ', [substnl_decl [a₁;...;an]] k Ω ⊢. *) -val substnl_decl : substl -> int -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t +val substnl_decl : substl -> int -> Constr.rel_declaration -> Constr.rel_declaration (** [substl_decl σ Ω] is a short-hand for [substnl_decl σ 0 Ω] *) -val substl_decl : substl -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t +val substl_decl : substl -> Constr.rel_declaration -> Constr.rel_declaration (** [subst1_decl a Ω] is a short-hand for [substnl_decl [a] 0 Ω] *) -val subst1_decl : constr -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t +val subst1_decl : constr -> Constr.rel_declaration -> Constr.rel_declaration (** [replace_vars k [(id₁,c₁);...;(idn,cn)] t] substitutes [Var idj] by [cj] in [t]. *) @@ -134,8 +134,8 @@ open Univ (** Level substitutions for polymorphism. *) val subst_univs_level_constr : universe_level_subst -> constr -> constr -val subst_univs_level_context : Univ.universe_level_subst -> Context.Rel.t -> Context.Rel.t +val subst_univs_level_context : Univ.universe_level_subst -> Constr.rel_context -> Constr.rel_context (** Instance substitution for polymorphism. *) val subst_instance_constr : Instance.t -> constr -> constr -val subst_instance_context : Instance.t -> Context.Rel.t -> Context.Rel.t +val subst_instance_context : Instance.t -> Constr.rel_context -> Constr.rel_context diff --git a/library/global.mli b/library/global.mli index 57e173cb9..b2a191cee 100644 --- a/library/global.mli +++ b/library/global.mli @@ -23,7 +23,7 @@ val env_is_initial : unit -> bool val universes : unit -> UGraph.t val named_context_val : unit -> Environ.named_context_val -val named_context : unit -> Context.Named.t +val named_context : unit -> Constr.named_context (** {6 Enriching the global environment } *) @@ -79,7 +79,7 @@ val add_module_parameter : (** {6 Queries in the global environment } *) -val lookup_named : variable -> Context.Named.Declaration.t +val lookup_named : variable -> Constr.named_declaration val lookup_constant : Constant.t -> Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body diff --git a/library/lib.ml b/library/lib.ml index 128b27e75..a20de55bf 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -405,7 +405,7 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind +type variable_info = Constr.named_declaration * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = { diff --git a/library/lib.mli b/library/lib.mli index 1d77212e9..5abfccfc7 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -9,6 +9,7 @@ (************************************************************************) open Names + (** Lib: record of operations, backtrack, low-level sections *) (** This module provides a general mechanism to keep a trace of all operations @@ -153,7 +154,7 @@ val unfreeze : frozen -> unit val init : unit -> unit (** {6 Section management for discharge } *) -type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind +type variable_info = Constr.named_declaration * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = private { abstr_ctx : variable_context; @@ -165,7 +166,7 @@ type abstr_info = private { } val instance_from_variable_context : variable_context -> Id.t array -val named_of_variable_context : variable_context -> Context.Named.t +val named_of_variable_context : variable_context -> Constr.named_context val section_segment_of_constant : Constant.t -> abstr_info val section_segment_of_mutual_inductive: MutInd.t -> abstr_info @@ -179,9 +180,9 @@ val is_in_section : GlobRef.t -> bool val add_section_variable : Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit val add_section_context : Univ.ContextSet.t -> unit val add_section_constant : Decl_kinds.polymorphic -> - Constant.t -> Context.Named.t -> unit + Constant.t -> Constr.named_context -> unit val add_section_kn : Decl_kinds.polymorphic -> - MutInd.t -> Context.Named.t -> unit + MutInd.t -> Constr.named_context -> unit val replacement_context : unit -> Opaqueproof.work_list (** {6 Discharge: decrease the section level if in the current section } *) diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index e9ce306e8..4ea0b30bd 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -29,11 +29,6 @@ TACTIC EXTEND protect_fv [ protect_tac map ] END -TACTIC EXTEND closed_term - [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] -> - [ closed_term t l ] -END - open Pptactic open Ppconstr diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index e4d17f250..8e0ca877a 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -96,34 +96,36 @@ let protect_tac_in map id = (****************************************************************************) -let closed_term t l = - let open Quote_plugin in +let rec closed_under sigma cset t = + try + let (gr, _) = Termops.global_of_constr sigma t in + Refset_env.mem gr cset + with Not_found -> + match EConstr.kind sigma t with + | Cast(c,_,_) -> closed_under sigma cset c + | App(f,l) -> closed_under sigma cset f && Array.for_all (closed_under sigma cset) l + | _ -> false + +let closed_term args _ = match args with +| [t; l] -> + let t = Option.get (Value.to_constr t) in + let l = List.map (fun c -> Value.cast (Genarg.topwit Stdarg.wit_ref) c) (Option.get (Value.to_list l)) in Proofview.tclEVARMAP >>= fun sigma -> - let l = List.map UnivGen.constr_of_global l in - let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in - if Quote.closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt()) - -(* TACTIC EXTEND echo -| [ "echo" constr(t) ] -> - [ Pp.msg (Termops.print_constr t); Tacinterp.eval_tactic (TacId []) ] -END;;*) + let cs = List.fold_right Refset_env.add l Refset_env.empty in + if closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt()) +| _ -> assert false -(* -let closed_term_ast l = - TacFun([Some(Id.of_string"t")], - TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term", - [Genarg.in_gen Constrarg.wit_constr (mkVar(Id.of_string"t")); - Genarg.in_gen (Genarg.wit_list Constrarg.wit_ref) l]))) -*) -let closed_term_ast l = +let closed_term_ast = let tacname = { mltac_plugin = "newring_plugin"; mltac_tactic = "closed_term"; } in + let () = Tacenv.register_ml_tactic tacname [|closed_term|] in let tacname = { mltac_name = tacname; mltac_index = 0; } in + fun l -> let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in TacFun([Name(Id.of_string"t")], TacML(Loc.tag (tacname, diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index 0e056a472..fcd04a2e7 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -18,8 +18,6 @@ val protect_tac_in : string -> Id.t -> unit Proofview.tactic val protect_tac : string -> unit Proofview.tactic -val closed_term : EConstr.constr -> GlobRef.t list -> unit Proofview.tactic - val add_theory : Id.t -> constr_expr -> diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 347a1e4e2..6b183dab1 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -962,6 +962,7 @@ END (* the default simpl and unfold tactics would erase blindly. *) open Ssrmatching_plugin.Ssrmatching +open Ssrmatching_plugin.G_ssrmatching let pr_wgen = function | (clr, Some((id,k),None)) -> spc() ++ pr_clear mt clr ++ str k ++ pr_hoi id diff --git a/plugins/ssrmatching/g_ssrmatching.ml4 b/plugins/ssrmatching/g_ssrmatching.ml4 new file mode 100644 index 000000000..746c368aa --- /dev/null +++ b/plugins/ssrmatching/g_ssrmatching.ml4 @@ -0,0 +1,101 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Ltac_plugin +open Genarg +open Pcoq +open Pcoq.Constr +open Ssrmatching +open Ssrmatching.Internal + +(* Defining grammar rules with "xx" in it automatically declares keywords too, + * we thus save the lexer to restore it at the end of the file *) +let frozen_lexer = CLexer.get_keyword_state () ;; + +DECLARE PLUGIN "ssrmatching_plugin" + +let pr_rpattern _ _ _ = pr_rpattern + +ARGUMENT EXTEND rpattern + TYPED AS rpatternty + PRINTED BY pr_rpattern + INTERPRETED BY interp_rpattern + GLOBALIZED BY glob_rpattern + SUBSTITUTED BY subst_rpattern + | [ lconstr(c) ] -> [ mk_rpattern (T (mk_lterm c None)) ] + | [ "in" lconstr(c) ] -> [ mk_rpattern (In_T (mk_lterm c None)) ] + | [ lconstr(x) "in" lconstr(c) ] -> + [ mk_rpattern (X_In_T (mk_lterm x None, mk_lterm c None)) ] + | [ "in" lconstr(x) "in" lconstr(c) ] -> + [ mk_rpattern (In_X_In_T (mk_lterm x None, mk_lterm c None)) ] + | [ lconstr(e) "in" lconstr(x) "in" lconstr(c) ] -> + [ mk_rpattern (E_In_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) ] + | [ lconstr(e) "as" lconstr(x) "in" lconstr(c) ] -> + [ mk_rpattern (E_As_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) ] +END + +let pr_ssrterm _ _ _ = pr_ssrterm + +ARGUMENT EXTEND cpattern + PRINTED BY pr_ssrterm + INTERPRETED BY interp_ssrterm + GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm + RAW_PRINTED BY pr_ssrterm + GLOB_PRINTED BY pr_ssrterm +| [ "Qed" constr(c) ] -> [ mk_lterm c None ] +END + +let input_ssrtermkind strm = match Util.stream_nth 0 strm with + | Tok.KEYWORD "(" -> '(' + | Tok.KEYWORD "@" -> '@' + | _ -> ' ' +let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind + +GEXTEND Gram + GLOBAL: cpattern; + cpattern: [[ k = ssrtermkind; c = constr -> + let pattern = mk_term k c None in + if loc_of_cpattern pattern <> Some !@loc && k = '(' + then mk_term 'x' c None + else pattern ]]; +END + +ARGUMENT EXTEND lcpattern + TYPED AS cpattern + PRINTED BY pr_ssrterm + INTERPRETED BY interp_ssrterm + GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm + RAW_PRINTED BY pr_ssrterm + GLOB_PRINTED BY pr_ssrterm +| [ "Qed" lconstr(c) ] -> [ mk_lterm c None ] +END + +GEXTEND Gram + GLOBAL: lcpattern; + lcpattern: [[ k = ssrtermkind; c = lconstr -> + let pattern = mk_term k c None in + if loc_of_cpattern pattern <> Some !@loc && k = '(' + then mk_term 'x' c None + else pattern ]]; +END + +ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY pr_rpattern +| [ rpattern(pat) ] -> [ pat ] +END + +TACTIC EXTEND ssrinstoftpat +| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof arg) ] +END + +(* We wipe out all the keywords generated by the grammar rules we defined. *) +(* The user is supposed to Require Import ssreflect or Require ssreflect *) +(* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) +(* consequence the extended ssreflect grammar. *) +let () = CLexer.set_keyword_state frozen_lexer ;; diff --git a/plugins/ssrmatching/g_ssrmatching.mli b/plugins/ssrmatching/g_ssrmatching.mli new file mode 100644 index 000000000..bb5161a0e --- /dev/null +++ b/plugins/ssrmatching/g_ssrmatching.mli @@ -0,0 +1,17 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) + +open Genarg +open Ssrmatching + +(** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *) +val cpattern : cpattern Pcoq.Gram.entry +val wit_cpattern : cpattern uniform_genarg_type + +(** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *) +val lcpattern : cpattern Pcoq.Gram.entry +val wit_lcpattern : cpattern uniform_genarg_type + +(** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *) +val rpattern : rpattern Pcoq.Gram.entry +val wit_rpattern : rpattern uniform_genarg_type diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml index 9d9b1b2e8..05eda14e9 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml @@ -10,10 +10,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -(* Defining grammar rules with "xx" in it automatically declares keywords too, - * we thus save the lexer to restore it at the end of the file *) -let frozen_lexer = CLexer.get_keyword_state () ;; - open Ltac_plugin open Names open Pp @@ -22,8 +18,6 @@ open Stdarg open Term module CoqConstr = Constr open CoqConstr -open Pcoq -open Pcoq.Constr open Vars open Libnames open Tactics @@ -46,8 +40,6 @@ open Evar_kinds open Constrexpr open Constrexpr_ops -DECLARE PLUGIN "ssrmatching_plugin" - let errorstrm = CErrors.user_err ~hdr:"ssrmatching" let loc_error loc msg = CErrors.user_err ?loc ~hdr:msg (str msg) let ppnl = Feedback.msg_info @@ -907,7 +899,6 @@ let pr_pattern_aux pr_constr = function let pp_pattern (sigma, p) = pr_pattern_aux (fun t -> pr_constr_pat (EConstr.Unsafe.to_constr (pi3 (nf_open_term sigma sigma (EConstr.of_constr t))))) p let pr_cpattern = pr_term -let pr_rpattern _ _ _ = pr_pattern let wit_rpatternty = add_genarg "rpatternty" pr_pattern @@ -987,27 +978,7 @@ let interp_rpattern s = function | E_As_X_In_T(e,x,t) -> E_As_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t) -let interp_rpattern ist gl t = Tacmach.project gl, interp_rpattern ist t - -ARGUMENT EXTEND rpattern - TYPED AS rpatternty - PRINTED BY pr_rpattern - INTERPRETED BY interp_rpattern - GLOBALIZED BY glob_rpattern - SUBSTITUTED BY subst_rpattern - | [ lconstr(c) ] -> [ T (mk_lterm c None) ] - | [ "in" lconstr(c) ] -> [ In_T (mk_lterm c None) ] - | [ lconstr(x) "in" lconstr(c) ] -> - [ X_In_T (mk_lterm x None, mk_lterm c None) ] - | [ "in" lconstr(x) "in" lconstr(c) ] -> - [ In_X_In_T (mk_lterm x None, mk_lterm c None) ] - | [ lconstr(e) "in" lconstr(x) "in" lconstr(c) ] -> - [ E_In_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None) ] - | [ lconstr(e) "as" lconstr(x) "in" lconstr(c) ] -> - [ E_As_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None) ] -END - - +let interp_rpattern0 ist gl t = Tacmach.project gl, interp_rpattern ist t type cpattern = char * glob_constr_and_expr * Geninterp.interp_sign option let tag_of_cpattern = pi1 @@ -1051,52 +1022,9 @@ let interp_wit wit ist gl x = let interp_open_constr ist gl gc = interp_wit wit_open_constr ist gl gc let pf_intern_term gl (_, c, ist) = glob_constr ist (pf_env gl) (project gl) c -let pr_ssrterm _ _ _ = pr_term -let input_ssrtermkind strm = match stream_nth 0 strm with - | Tok.KEYWORD "(" -> '(' - | Tok.KEYWORD "@" -> '@' - | _ -> ' ' -let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind let interp_ssrterm ist gl t = Tacmach.project gl, interp_ssrterm ist t -ARGUMENT EXTEND cpattern - PRINTED BY pr_ssrterm - INTERPRETED BY interp_ssrterm - GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm - RAW_PRINTED BY pr_ssrterm - GLOB_PRINTED BY pr_ssrterm -| [ "Qed" constr(c) ] -> [ mk_lterm c None ] -END - -GEXTEND Gram - GLOBAL: cpattern; - cpattern: [[ k = ssrtermkind; c = constr -> - let pattern = mk_term k c None in - if loc_ofCG pattern <> Some !@loc && k = '(' - then mk_term 'x' c None - else pattern ]]; -END - -ARGUMENT EXTEND lcpattern - TYPED AS cpattern - PRINTED BY pr_ssrterm - INTERPRETED BY interp_ssrterm - GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm - RAW_PRINTED BY pr_ssrterm - GLOB_PRINTED BY pr_ssrterm -| [ "Qed" lconstr(c) ] -> [ mk_lterm c None ] -END - -GEXTEND Gram - GLOBAL: lcpattern; - lcpattern: [[ k = ssrtermkind; c = lconstr -> - let pattern = mk_term k c None in - if loc_ofCG pattern <> Some !@loc && k = '(' - then mk_term 'x' c None - else pattern ]]; -END - let interp_term gl = function | (_, c, Some ist) -> on_snd EConstr.Unsafe.to_constr (interp_open_constr ist gl c) @@ -1416,10 +1344,6 @@ let is_wildcard ((_, (l, r), _) : cpattern) : bool = match DAst.get l, r with (* "ssrpattern" *) -ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY pr_rpattern -| [ rpattern(pat) ] -> [ pat ] -END - let pr_rpattern = pr_pattern let pf_merge_uc uc gl = @@ -1428,6 +1352,9 @@ let pf_merge_uc uc gl = let pf_unsafe_merge_uc uc gl = re_sig (sig_it gl) (Evd.set_universe_context (project gl) uc) +(** All the pattern types reuse the same dynamic toplevel tag *) +let wit_ssrpatternarg = wit_rpatternty + let interp_rpattern = interp_rpattern ~wit_ssrpatternarg let ssrpatterntac _ist arg gl = @@ -1479,14 +1406,20 @@ let ssrinstancesof arg gl = done; raise NoMatch with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl -TACTIC EXTEND ssrinstoftpat -| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof arg) ] -END - -(* We wipe out all the keywords generated by the grammar rules we defined. *) -(* The user is supposed to Require Import ssreflect or Require ssreflect *) -(* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) -(* consequence the extended ssreflect grammar. *) -let () = CLexer.set_keyword_state frozen_lexer ;; +module Internal = +struct + let wit_rpatternty = wit_rpatternty + let glob_rpattern = glob_rpattern + let subst_rpattern = subst_rpattern + let interp_rpattern = interp_rpattern0 + let pr_rpattern = pr_rpattern + let mk_rpattern x = x + let mk_lterm = mk_lterm + let mk_term = mk_term + let glob_cpattern = glob_cpattern + let subst_ssrterm = subst_ssrterm + let interp_ssrterm = interp_ssrterm + let pr_ssrterm = pr_term +end (* vim: set filetype=ocaml foldmethod=marker: *) diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index c55081e0f..f478d48ea 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -2,7 +2,6 @@ (* Distributed under the terms of CeCILL-B. *) open Goal -open Genarg open Environ open Evd open Constr @@ -19,24 +18,12 @@ open Tacexpr type cpattern val pr_cpattern : cpattern -> Pp.t -(** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *) -val cpattern : cpattern Pcoq.Gram.entry -val wit_cpattern : cpattern uniform_genarg_type - -(** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *) -val lcpattern : cpattern Pcoq.Gram.entry -val wit_lcpattern : cpattern uniform_genarg_type - (** The type of rewrite patterns, the patterns of the [rewrite] tactic. These patterns also include patterns that identify all the subterms of a context (i.e. "in" prefix) *) type rpattern val pr_rpattern : rpattern -> Pp.t -(** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *) -val rpattern : rpattern Pcoq.Gram.entry -val wit_rpattern : rpattern uniform_genarg_type - (** Pattern interpretation and matching *) exception NoMatch @@ -238,4 +225,25 @@ val debug : bool -> unit * "Unset SsrMatchingProfiling" to get timings *) val profile : bool -> unit +val ssrinstancesof : cpattern -> Tacmach.tactic + +(** Functions used for grammar extensions. Do not use. *) + +module Internal : +sig + val wit_rpatternty : (rpattern, rpattern, rpattern) Genarg.genarg_type + val glob_rpattern : Genintern.glob_sign -> rpattern -> rpattern + val subst_rpattern : Mod_subst.substitution -> rpattern -> rpattern + val interp_rpattern : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> rpattern -> Evd.evar_map * rpattern + val pr_rpattern : rpattern -> Pp.t + val mk_rpattern : (cpattern, cpattern) ssrpattern -> rpattern + val mk_lterm : Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern + val mk_term : char -> Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern + + val glob_cpattern : Genintern.glob_sign -> cpattern -> cpattern + val subst_ssrterm : Mod_subst.substitution -> cpattern -> cpattern + val interp_ssrterm : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> cpattern -> Evd.evar_map * cpattern + val pr_ssrterm : cpattern -> Pp.t +end + (* eof *) diff --git a/plugins/ssrmatching/ssrmatching_plugin.mlpack b/plugins/ssrmatching/ssrmatching_plugin.mlpack index 5fb1f1567..02c75f14e 100644 --- a/plugins/ssrmatching/ssrmatching_plugin.mlpack +++ b/plugins/ssrmatching/ssrmatching_plugin.mlpack @@ -1 +1,2 @@ Ssrmatching +G_ssrmatching diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index efb205182..576073344 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -303,7 +303,7 @@ type constructor_summary = { cs_cstr : pconstructor; cs_params : constr list; cs_nargs : int; - cs_args : Context.Rel.t; + cs_args : Constr.rel_context; cs_concl_realargs : constr array } diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index aa53f7e67..8eaef24c4 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -93,12 +93,12 @@ val inductive_nparamdecls : inductive -> int val inductive_nparamdecls_env : env -> inductive -> int (** @return params context *) -val inductive_paramdecls : pinductive -> Context.Rel.t -val inductive_paramdecls_env : env -> pinductive -> Context.Rel.t +val inductive_paramdecls : pinductive -> Constr.rel_context +val inductive_paramdecls_env : env -> pinductive -> Constr.rel_context (** @return full arity context, hence with letin *) -val inductive_alldecls : pinductive -> Context.Rel.t -val inductive_alldecls_env : env -> pinductive -> Context.Rel.t +val inductive_alldecls : pinductive -> Constr.rel_context +val inductive_alldecls_env : env -> pinductive -> Constr.rel_context (** {7 Extract information from a constructor name} *) @@ -141,7 +141,7 @@ type constructor_summary = { cs_cstr : pconstructor; (* internal name of the constructor plus universes *) cs_params : constr list; (* parameters of the constructor in current ctx *) cs_nargs : int; (* length of arguments signature (letin included) *) - cs_args : Context.Rel.t; (* signature of the arguments (letin included) *) + cs_args : Constr.rel_context; (* signature of the arguments (letin included) *) cs_concl_realargs : constr array; (* actual realargs in the concl of cstr *) } val lift_constructor : int -> constructor_summary -> constructor_summary @@ -154,7 +154,7 @@ val get_projections : env -> inductive_family -> Constant.t array option (** [get_arity] returns the arity of the inductive family instantiated with the parameters; if recursively non-uniform parameters are not part of the inductive family, they appears in the arity *) -val get_arity : env -> inductive_family -> Context.Rel.t * Sorts.family +val get_arity : env -> inductive_family -> Constr.rel_context * Sorts.family val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 7319846fb..16d003f67 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -123,7 +123,7 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs = try if const then let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(0)) params in - retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkInd ind) tag, ctyp + Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkInd ind) tag, ctyp else raise Not_found with Not_found -> diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d3aa7ac64..efb3c339a 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -74,10 +74,10 @@ type typeclass = { cl_impl : GlobRef.t; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *) - cl_context : GlobRef.t option list * Context.Rel.t; + cl_context : GlobRef.t option list * Constr.rel_context; (* Context of definitions and properties on defs, will not be shared *) - cl_props : Context.Rel.t; + cl_props : Constr.rel_context; (* The method implementaions as projections. *) cl_projs : (Name.t * (direction * hint_info) option diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index e4a56960c..80c6d8239 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -35,10 +35,10 @@ type typeclass = { (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The global reference gives a direct link to the class itself. *) - cl_context : GlobRef.t option list * Context.Rel.t; + cl_context : GlobRef.t option list * Constr.rel_context; (** Context of definitions and properties on defs, will not be shared *) - cl_props : Context.Rel.t; + cl_props : Constr.rel_context; (** The methods implementations of the typeclass as projections. Some may be undefinable due to sorting restrictions or simply undefined if diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 14c9f49b1..bd6062824 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -79,7 +79,7 @@ let construct_of_constr const env tag typ = (* spiwack : here be a branch for specific decompilation handled by retroknowledge *) try if const then - ((retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkIndU indu) tag), + ((Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkIndU indu) tag), typ) (*spiwack: this may need to be changed in case there are parameters in the type which may cause a constant value to have an arity. (type_constructor seems to be all about parameters actually) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f926e8275..fd7135b6a 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -40,7 +40,7 @@ type object_pr = { print_syntactic_def : env -> KerName.t -> Pp.t; print_module : bool -> ModPath.t -> Pp.t; print_modtype : ModPath.t -> Pp.t; - print_named_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t; + print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 8dd729610..1668bce29 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -89,7 +89,7 @@ type object_pr = { print_syntactic_def : env -> KerName.t -> Pp.t; print_module : bool -> ModPath.t -> Pp.t; print_modtype : ModPath.t -> Pp.t; - print_named_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t; + print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; diff --git a/printing/printer.ml b/printing/printer.ml index d76bd1e2b..92224c992 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -852,7 +852,7 @@ type axiom = type context_object = | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of axiom * (Label.t * Context.Rel.t * types) list + | Axiom of axiom * (Label.t * Constr.rel_context * types) list | Opaque of Constant.t (* An opaque constant. *) | Transparent of Constant.t diff --git a/printing/printer.mli b/printing/printer.mli index 7a8b963d2..eddfef6fa 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -152,13 +152,13 @@ val get_compact_context : unit -> bool val pr_context_unlimited : env -> evar_map -> Pp.t val pr_ne_context_of : Pp.t -> env -> evar_map -> Pp.t -val pr_named_decl : env -> evar_map -> Context.Named.Declaration.t -> Pp.t -val pr_compacted_decl : env -> evar_map -> Context.Compacted.Declaration.t -> Pp.t -val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> Pp.t +val pr_named_decl : env -> evar_map -> Constr.named_declaration -> Pp.t +val pr_compacted_decl : env -> evar_map -> Constr.compacted_declaration -> Pp.t +val pr_rel_decl : env -> evar_map -> Constr.rel_declaration -> Pp.t -val pr_named_context : env -> evar_map -> Context.Named.t -> Pp.t +val pr_named_context : env -> evar_map -> Constr.named_context -> Pp.t val pr_named_context_of : env -> evar_map -> Pp.t -val pr_rel_context : env -> evar_map -> Context.Rel.t -> Pp.t +val pr_rel_context : env -> evar_map -> Constr.rel_context -> Pp.t val pr_rel_context_of : env -> evar_map -> Pp.t val pr_context_of : env -> evar_map -> Pp.t @@ -210,7 +210,7 @@ type axiom = type context_object = | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of axiom * (Label.t * Context.Rel.t * types) list + | Axiom of axiom * (Label.t * Constr.rel_context * types) list | Opaque of Constant.t (* An opaque constant. *) | Transparent of Constant.t diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 47c9c51ee..7e250faa8 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -93,7 +93,7 @@ type pstate = { pid : Id.t; (* the name of the theorem whose proof is being constructed *) terminator : proof_terminator CEphemeron.key; endline_tactic : Genarg.glob_generic_argument option; - section_vars : Context.Named.t option; + section_vars : Constr.named_context option; proof : Proof.t; strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 9e07ed2d0..854ceaa41 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -126,8 +126,8 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit * (w.r.t. type dependencies and let-ins covered by it) + a list of * ids to be cleared *) val set_used_variables : - Names.Id.t list -> Context.Named.t * Names.lident list -val get_used_variables : unit -> Context.Named.t option + Names.Id.t list -> Constr.named_context * Names.lident list +val get_used_variables : unit -> Constr.named_context option (** Get the universe declaration associated to the current proof. *) val get_universe_decl : unit -> UState.universe_decl diff --git a/test-suite/bugs/closed/7712.v b/test-suite/bugs/closed/7712.v new file mode 100644 index 000000000..a4e9697fa --- /dev/null +++ b/test-suite/bugs/closed/7712.v @@ -0,0 +1,4 @@ +(* This used to raise an anomaly *) + +Fail Reserved Notation "'[tele_arg' x ';' .. ';' z ]" + (format "[tele_arg '[hv' x .. z ']' ]"). diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 996af5927..5ab616160 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -241,3 +241,8 @@ Notation Notation "( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope (default interpretation) +1 subgoal + + ============================ + ##@% + ^^^ diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 3cf0c913f..876aaa394 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -385,3 +385,17 @@ Module LocateNotations. Locate "exists". Locate "( _ , _ , .. , _ )". End LocateNotations. + +Module Issue7731. + +Axiom (P : nat -> Prop). +Parameter (X : nat). +Notation "## @ E ^^^" := (P E) (at level 20, E at level 1, format "'[ ' ## '/' @ E '/' ^^^ ']'"). +Notation "%" := X. + +Set Printing Width 7. +Goal ## @ % ^^^. +Show. +Abort. + +End Issue7731. diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli index 0e2b0c80e..751e79d89 100644 --- a/vernac/assumptions.mli +++ b/vernac/assumptions.mli @@ -23,7 +23,7 @@ open Printer val traverse : Label.t -> constr -> (Refset_env.t * Refset_env.t Refmap_env.t * - (Label.t * Context.Rel.t * types) list Refmap_env.t) + (Label.t * Constr.rel_context * types) list Refmap_env.t) (** Collects all the assumptions (optionally including opaque definitions) on which a term relies (together with their type). The above warning of diff --git a/vernac/classes.mli b/vernac/classes.mli index bd30b2d60..9c37364cb 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -16,9 +16,9 @@ open Libnames (** Errors *) -val mismatched_params : env -> constr_expr list -> Context.Rel.t -> 'a +val mismatched_params : env -> constr_expr list -> Constr.rel_context -> 'a -val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a +val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a (** Instance declaration *) diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index f51bfbad5..b1a9c8a5a 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -82,12 +82,12 @@ val interp_fixpoint : val declare_fixpoint : locality -> polymorphic -> recursive_preentry * UState.universe_decl * UState.t * - (Context.Rel.t * Impargs.manual_implicits * int option) list -> + (Constr.rel_context * Impargs.manual_implicits * int option) list -> Proof_global.lemma_possible_guards -> decl_notation list -> unit val declare_cofixpoint : locality -> polymorphic -> recursive_preentry * UState.universe_decl * UState.t * - (Context.Rel.t * Impargs.manual_implicits * int option) list -> + (Constr.rel_context * Impargs.manual_implicits * int option) list -> decl_notation list -> unit (** Very private function, do not use *) diff --git a/vernac/himsg.mli b/vernac/himsg.mli index 1d3807502..91caddcf1 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -25,7 +25,7 @@ val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t val explain_inductive_error : inductive_error -> Pp.t -val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Context.Rel.t -> Pp.t +val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.t val explain_typeclass_error : env -> typeclass_error -> Pp.t diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index da14358ef..240147c8d 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -487,6 +487,15 @@ and check_no_ldots_in_box = function let error_not_same ?loc () = user_err ?loc Pp.(str "The format is not the same on the right- and left-hand sides of the special token \"..\".") +let find_prod_list_loc sfmt fmt = + (* [fmt] is some [UnpTerminal x :: sfmt @ UnpTerminal ".." :: sfmt @ UnpTerminal y :: rest] *) + if List.is_empty sfmt then + (* No separators; we highlight the sequence "x .." *) + Loc.merge_opt (fst (List.hd fmt)) (fst (List.hd (List.tl fmt))) + else + (* A separator; we highlight the separating sequence *) + Loc.merge_opt (fst (List.hd sfmt)) (fst (List.last sfmt)) + let skip_var_in_recursive_format = function | (_,UnpTerminal s) :: sl (* skip first var *) when not (List.for_all (fun c -> c = " ") (String.explode s)) -> (* To do, though not so important: check that the names match @@ -496,6 +505,8 @@ let skip_var_in_recursive_format = function | [] -> assert false let read_recursive_format sl fmt = + (* Turn [[UnpTerminal s :: some-list @ UnpTerminal ".." :: same-some-list @ UnpTerminal s' :: rest] *) + (* into [(some-list,rest)] *) let get_head fmt = let sl = skip_var_in_recursive_format fmt in try split_format_at_ldots [] sl with Exit -> error_not_same ?loc:(fst (List.last (if sl = [] then fmt else sl))) () in @@ -528,10 +539,10 @@ let hunks_of_format (from,(vars,typs)) symfmt = let i = index_id m vars in let typ = List.nth typs (i-1) in let _,prec = precedence_of_entry_type from typ in - let slfmt,fmt = read_recursive_format sl fmt in - let sl, slfmt = aux (sl,slfmt) in - if not (List.is_empty sl) then error_format ?loc:(fst (List.last fmt)) (); - let symbs, l = aux (symbs,fmt) in + let loc_slfmt,rfmt = read_recursive_format sl fmt in + let sl, slfmt = aux (sl,loc_slfmt) in + if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) (); + let symbs, l = aux (symbs,rfmt) in let hunk = match typ with | ETConstr _ -> UnpListMetaVar (i,prec,slfmt) | ETBinder isopen -> @@ -1312,8 +1323,15 @@ let make_pa_rule level (typs,symbols) ntn need_squash = let make_pp_rule level (typs,symbols) fmt = match fmt with - | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols level)] - | Some fmt -> hunks_of_format (level, List.split typs) (symbols, parse_format fmt) + | None -> + let hunks = make_hunks typs symbols level in + if List.exists (function _,(UnpCut (PpBrk _) | UnpListMetaVar _) -> true | _ -> false) hunks then + [UnpBox (PpHOVB 0,hunks)] + else + (* Optimization to work around what seems an ocaml Format bug (see Mantis #7804/#7807) *) + List.map snd hunks (* drop locations which are dummy *) + | Some fmt -> + hunks_of_format (level, List.split typs) (symbols, parse_format fmt) (* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *) let make_syntax_rules (sd : SynData.syn_data) = let open SynData in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index fa6a9adf1..1f401b4e1 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -40,7 +40,7 @@ let check_evars env evm = type oblinfo = { ev_name: int * Id.t; - ev_hyps: Context.Named.t; + ev_hyps: Constr.named_context; ev_status: bool * Evar_kinds.obligation_definition_status; ev_chop: int option; ev_src: Evar_kinds.t Loc.located; diff --git a/vernac/record.mli b/vernac/record.mli index 7cf7da1e2..567f2b313 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -22,7 +22,7 @@ val declare_projections : bool list -> UnivNames.universe_binders -> Impargs.manual_implicits list -> - Context.Rel.t -> + Constr.rel_context -> (Name.t * bool) list * Constant.t option list val definition_structure : diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 43c974846..6d1abeca1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -263,15 +263,13 @@ let print_namespace ns = let matches mp = match match_modulepath ns mp with | Some [] -> true | _ -> false in - let constants = (Global.env ()).Environ.env_globals.Environ.env_constants in let constants_in_namespace = - Cmap_env.fold (fun c (body,_) acc -> - let kn = Constant.user c in - if matches (KerName.modpath kn) then - acc++fnl()++hov 2 (print_constant kn body) - else - acc - ) constants (str"") + Environ.fold_constants (fun c body acc -> + let kn = Constant.user c in + if matches (KerName.modpath kn) + then acc++fnl()++hov 2 (print_constant kn body) + else acc) + (Global.env ()) (str"") in (print_list Id.print ns)++str":"++fnl()++constants_in_namespace |