diff options
71 files changed, 472 insertions, 496 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index c3e59a6d89..73b979c6a3 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -749,6 +749,9 @@ plugin:plugin-tutorial: plugin:ci-quickchick: extends: .ci-template-flambda +plugin:ci-reduction_effects: + extends: .ci-template + plugin:ci-relation_algebra: extends: .ci-template diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index a0139e422d..8cff8f66b7 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -43,6 +43,7 @@ well. - [Reviewing pull requests](#reviewing-pull-requests) - [Merging pull requests](#merging-pull-requests) - [Additional notes for pull request reviewers and assignees](#additional-notes-for-pull-request-reviewers-and-assignees) + - [Joining / leaving maintainer teams](#joining--leaving-maintainer-teams) - [Core development team](#core-development-team) - [Release management](#release-management) - [Packaging Coq](#packaging-coq) @@ -60,6 +61,7 @@ well. - [Merge script dependencies](#merge-script-dependencies) - [Coqbot](#coqbot) - [Online forum and chat to talk to developers](#online-forum-and-chat-to-talk-to-developers) + - [Coq calls](#coq-calls) - [Coq remote working groups](#coq-remote-working-groups) - [Coq Users and Developers Workshops](#coq-users-and-developers-workshops) @@ -746,12 +748,15 @@ member of a team that was requested a review should self-assign the PR, and will act as its shepherd from then on. The PR assignee is responsible for making sure that all the proposed -changes have been reviewed by relevant maintainers, that change -requests have been implemented, that CI is passing, and eventually -will be the one who merges the PR. +changes have been reviewed by relevant maintainers (at least one +reviewer for each component that is significantly affected), that +change requests have been implemented, that CI is passing, and +eventually will be the one who merges the PR. *If you have already frequently contributed to a component, we would -be happy to have you join one of the maintainer teams.* +be happy to have you join one of the maintainer teams.* See the +[section below](#joining--leaving-maintainer-teams) on joining / +leaving maintainer teams. The complete list of maintainer teams is available [here][coq-pushers] (link only accessible to people who are already members of the Coq @@ -768,9 +773,20 @@ organization, because of a limitation of GitHub). they contributed to. However, reviewers may push small fixes to the PR branch to facilitate the PR integration. +- PRs are merged when there is consensus. Consensus is defined by an + explicit approval from at least one maintainer for each component + that is significantly affected and an absence of dissent. As soon + as a developer opposes a PR, it should not be merged without being + discussed first (usually in a call or working group). + +- Sometimes (especially for large or potentially controversial PRs), + it is a good practice to announce the intent to merge, one or + several days in advance, when unsure that everyone had a chance to + voice their opinion, or to finish reviewing the PR. + - Only PRs targetting the `master` branch can be merged by a maintainer. For PRs targetting a release branch, the assignee - should always be the RM. + should always be the release manager. - Before merging, the assignee must also select a milestone for the PR (see also Section [Release management](#release-management)). @@ -782,10 +798,6 @@ organization, because of a limitation of GitHub).  -- Sometimes, it is a good practice to announce the intent to merge one - or several days in advance when unsure that everyone had a chance to - voice their opinion, or to finish reviewing the PR. - - When a PR has [overlays][user-overlays], then: - the overlays that are backward-compatible (normally the case for @@ -798,6 +810,16 @@ organization, because of a limitation of GitHub). maintainers of the affected projects to ask them to merge the overlays). +#### Joining / leaving maintainer teams #### + +We are always happy to have more people involved in the PR reviewing +and merging process, so do not hesitate to propose yourself if you +already have experience on a component. + +Maintainers can leave teams at any time (and core members can also +join any team where they feel able to help) but you should always +announce it to other maintainers when you do join or leave a team. + ### Core development team ### The core developers are the active developers with a lengthy and @@ -1110,6 +1132,14 @@ Obviously, the issue tracker is also a good place to ask questions, especially if the development processes are unclear, or the developer documentation should be improved. +### Coq calls ### + +We try to gather every week for one hour through video-conference to +discuss current and urgent matters. When longer discussions are +needed, topics are left out for the next working group. See the +[wiki][wiki-calls] for more information about Coq calls, as well as +notes of past ones. + ### Coq remote working groups ### We semi-regularly (up to every month) organize remote working groups, @@ -1219,6 +1249,7 @@ can be found [on the wiki][wiki-CUDW]. [user-changelog]: doc/changelog [user-overlays]: dev/ci/user-overlays [wiki]: https://github.com/coq/coq/wiki +[wiki-calls]: https://github.com/coq/coq/wiki/Coq-Calls [wiki-CUDW]: https://github.com/coq/coq/wiki/CoqImplementorsWorkshop [wiki-WG]: https://github.com/coq/coq/wiki/Coq-Working-Groups [YouTube]: https://www.youtube.com/channel/UCbJo6gYYr0OF18x01M4THdQ diff --git a/Makefile.ci b/Makefile.ci index 8315c16c64..4fc0e69748 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -38,6 +38,7 @@ CI_TARGETS= \ ci-paramcoq \ ci-perennial \ ci-quickchick \ + ci-reduction_effects \ ci-relation_algebra \ ci-rewriter \ ci-sf \ diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index e606d60d96..a2cf44389e 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -144,10 +144,16 @@ let check_inductive env mind mb = = (* Locally set typing flags for further typechecking *) let mb_flags = mb.mind_typing_flags in - let env = Environ.set_typing_flags {env.env_typing_flags with check_guarded = mb_flags.check_guarded; - check_positive = mb_flags.check_positive; - check_universes = mb_flags.check_universes; - conv_oracle = mb_flags.conv_oracle} env in + let env = Environ.set_typing_flags + {env.env_typing_flags with + check_guarded = mb_flags.check_guarded; + check_positive = mb_flags.check_positive; + check_universes = mb_flags.check_universes; + check_template = mb_flags.check_template; + conv_oracle = mb_flags.conv_oracle; + } + env + in Indtypes.check_inductive env ~sec_univs:None mind entry in let check = check mind in diff --git a/checker/check_stat.ml b/checker/check_stat.ml index a67945ae94..d115744707 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -56,6 +56,9 @@ let pr_nonpositive env = let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_positive then MutInd.to_string c :: acc else acc) env [] in pr_assumptions "Inductives whose positivity is assumed" inds +let pr_unsafe_template env = + let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_template then MutInd.to_string c :: acc else acc) env [] in + pr_assumptions "Inductives using unchecked template polymorphism" inds let print_context env = if !output_context then begin @@ -67,7 +70,8 @@ let print_context env = str "* " ++ hov 0 (pr_axioms env ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++ - str "* " ++ hov 0 (pr_nonpositive env))) + str "* " ++ hov 0 (pr_nonpositive env ++ fnl()) ++ fnl() ++ + str "* " ++ hov 0 (pr_unsafe_template env))) end let stats env = diff --git a/clib/backtrace.ml b/clib/backtrace.ml deleted file mode 100644 index 81803a81a5..0000000000 --- a/clib/backtrace.ml +++ /dev/null @@ -1,119 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <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) *) -(************************************************************************) -[@@@ocaml.warning "-37"] - -type raw_frame = -| Known_location of bool (* is_raise *) - * string (* filename *) - * int (* line number *) - * int (* start char *) - * int (* end char *) -| Unknown_location of bool (*is_raise*) - -type location = { - loc_filename : string; - loc_line : int; - loc_start : int; - loc_end : int; -} - -type frame = { frame_location : location option; frame_raised : bool; } - -external get_exception_backtrace: unit -> raw_frame array option - = "caml_get_exception_backtrace" - -type t = raw_frame array list -(** List of partial raw stack frames, in reverse order *) - -let empty = [] - -let of_raw = function -| Unknown_location r -> - { frame_location = None; frame_raised = r; } -| Known_location (r, file, line, st, en) -> - let loc = { - loc_filename = file; - loc_line = line; - loc_start = st; - loc_end = en; - } in - { frame_location = Some loc; frame_raised = r; } - -let rec repr_aux accu = function -| [] -> accu -| fragment :: stack -> - let len = Array.length fragment in - let rec append accu i = - if i = len then accu - else append (of_raw fragment.(i) :: accu) (succ i) - in - repr_aux (append accu 0) stack - -let repr bt = repr_aux [] (List.rev bt) - -let push stack = match get_exception_backtrace () with -| None -> [] -| Some frames -> frames :: stack - -(** Utilities *) - -let print_frame frame = - let raise = if frame.frame_raised then "raise" else "frame" in - match frame.frame_location with - | None -> Printf.sprintf "%s @ unknown" raise - | Some loc -> - Printf.sprintf "%s @ file \"%s\", line %d, characters %d-%d" - raise loc.loc_filename loc.loc_line loc.loc_start loc.loc_end - -(** Exception manipulation *) - -let backtrace : t Exninfo.t = Exninfo.make () - -let is_recording = ref false - -let record_backtrace b = - let () = Printexc.record_backtrace b in - is_recording := b - -let get_backtrace e = - Exninfo.get e backtrace - -let add_backtrace e = - if !is_recording then - (* This must be the first function call, otherwise the stack may be - destroyed *) - let current = get_exception_backtrace () in - let info = Exninfo.info e in - begin match current with - | None -> (e, info) - | Some fragment -> - let bt = match get_backtrace info with - | None -> [] - | Some bt -> bt - in - let bt = fragment :: bt in - (e, Exninfo.add info backtrace bt) - end - else - let info = Exninfo.info e in - (e, info) - -let app_backtrace ~src ~dst = - if !is_recording then - match get_backtrace src with - | None -> dst - | Some bt -> - match get_backtrace dst with - | None -> - Exninfo.add dst backtrace bt - | Some nbt -> - let bt = bt @ nbt in - Exninfo.add dst backtrace bt - else dst diff --git a/clib/backtrace.mli b/clib/backtrace.mli deleted file mode 100644 index 55c60e5483..0000000000 --- a/clib/backtrace.mli +++ /dev/null @@ -1,98 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <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) *) -(************************************************************************) - -(** * Low-level management of OCaml backtraces. - - Currently, OCaml manages its backtraces in a very imperative way. That is to - say, it only keeps track of the stack destroyed by the last raised exception. - So we have to be very careful when using this module not to do silly things. - - Basically, you need to manually handle the reraising of exceptions. In order - to do so, each time the backtrace is lost, you must [push] the stack fragment. - This essentially occurs whenever a [with] handler is crossed. - -*) - -(** {5 Backtrace information} *) - -type location = { - loc_filename : string; - loc_line : int; - loc_start : int; - loc_end : int; -} -(** OCaml debugging information for function calls. *) - -type frame = { frame_location : location option; frame_raised : bool; } -(** A frame contains two informations: its optional physical location, and - whether it raised the exception or let it pass through. *) - -type t -(** Type of backtraces. They're essentially stack of frames. *) - -val empty : t -(** Empty frame stack. *) - -val push : t -> t -(** Add the current backtrace information to a given backtrace. *) - -val repr : t -> frame list -(** Represent a backtrace as a list of frames. Leftmost element is the outermost - call. *) - -(** {5 Utilities} *) - -val print_frame : frame -> string -(** Represent a frame. *) - -(** {5 Exception handling} *) - -val record_backtrace : bool -> unit -(** Whether to activate the backtrace recording mechanism. Note that it will - only work whenever the program was compiled with the [debug] flag. *) - -val get_backtrace : Exninfo.info -> t option -(** Retrieve the optional backtrace coming with the exception. *) - -val add_backtrace : exn -> Exninfo.iexn -(** Add the current backtrace information to the given exception. - - The intended use case is of the form: {[ - - try foo - with - | Bar -> bar - | err -> let err = add_backtrace err in baz - - ]} - - WARNING: any intermediate code between the [with] and the handler may - modify the backtrace. Yes, that includes [when] clauses. Ideally, what you - should do is something like: {[ - - try foo - with err -> - let err = add_backtrace err in - match err with - | Bar -> bar - | err -> baz - - ]} - - I admit that's a bit heavy, but there is not much to do... - -*) - -val app_backtrace : src:Exninfo.info -> dst:Exninfo.info -> Exninfo.info -(** Append the backtrace from [src] to [dst]. The returned exception is [dst] - except for its backtrace information. This is targeted at container - exceptions, that is, exceptions that contain exceptions. This way, one can - transfer the backtrace from the container to the underlying exception, as if - the latter was the one originally raised. *) diff --git a/clib/cArray.ml b/clib/cArray.ml index be59ae57d0..0f57204cc1 100644 --- a/clib/cArray.ml +++ b/clib/cArray.ml @@ -392,18 +392,30 @@ let iter2_i f v1 v2 = let () = if not (Int.equal len2 len1) then invalid_arg "Array.iter2" in for i = 0 to len1 - 1 do f i (uget v1 i) (uget v2 i) done -let pure_functional = false +let map_right f a = + let l = length a in + if l = 0 then [||] else begin + let r = Array.make l (f (unsafe_get a (l-1))) in + for i = l-2 downto 0 do + unsafe_set r i (f (unsafe_get a i)) + done; + r + end + +let map2_right f a b = + let l = length a in + if l <> length b then invalid_arg "CArray.map2_right: length mismatch"; + if l = 0 then [||] else begin + let r = Array.make l (f (unsafe_get a (l-1)) (unsafe_get b (l-1))) in + for i = l-2 downto 0 do + unsafe_set r i (f (unsafe_get a i) (unsafe_get b i)) + done; + r + end let fold_right_map f v e = -if pure_functional then - let (l,e) = - Array.fold_right - (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) - v ([],e) in - (Array.of_list l,e) -else let e' = ref e in - let v' = Array.map (fun x -> let (y,e) = f x !e' in e' := e; y) v in + let v' = map_right (fun x -> let (y,e) = f x !e' in e' := e; y) v in (v',!e') let fold_left_map f e v = @@ -414,7 +426,7 @@ let fold_left_map f e v = let fold_right2_map f v1 v2 e = let e' = ref e in let v' = - map2 (fun x1 x2 -> let (y,e) = f x1 x2 !e' in e' := e; y) v1 v2 + map2_right (fun x1 x2 -> let (y,e) = f x1 x2 !e' in e' := e; y) v1 v2 in (v',!e') diff --git a/clib/cArray.mli b/clib/cArray.mli index f94af26515..94390a369f 100644 --- a/clib/cArray.mli +++ b/clib/cArray.mli @@ -107,7 +107,7 @@ sig (** Same than [fold_left2_map] but passing the index of the array *) val fold_right2_map : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c - (** Same with two arrays, folding on the left *) + (** Same with two arrays, folding on the right *) val distinct : 'a array -> bool (** Return [true] if every element of the array is unique (for default diff --git a/clib/cEphemeron.ml b/clib/cEphemeron.ml index a2a6933e36..78aa8266e4 100644 --- a/clib/cEphemeron.ml +++ b/clib/cEphemeron.ml @@ -103,8 +103,4 @@ let default (typ, boxkey) default = try (EHashtbl.find values boxkey).get typ with Not_found -> default -let iter_opt (typ, boxkey) f = - try f ((EHashtbl.find values boxkey).get typ) - with Not_found -> () - let clean () = EHashtbl.clean values diff --git a/clib/cEphemeron.mli b/clib/cEphemeron.mli index 4c10a3d66f..e567e9b2c5 100644 --- a/clib/cEphemeron.mli +++ b/clib/cEphemeron.mli @@ -43,12 +43,12 @@ type 'a key val create : 'a -> 'a key -(* May raise InvalidKey *) exception InvalidKey + val get : 'a key -> 'a +(** May raise InvalidKey *) -(* These never fail. *) val default : 'a key -> 'a -> 'a -val iter_opt : 'a key -> ('a -> unit) -> unit +(** Never fails. *) val clean : unit -> unit diff --git a/clib/exninfo.ml b/clib/exninfo.ml index 34f76a2edd..ee998c2f17 100644 --- a/clib/exninfo.ml +++ b/clib/exninfo.ml @@ -57,12 +57,29 @@ let rec find_and_remove_assoc (i : int) = function if rem == ans then (r, l) else (r, (j, v) :: ans) -let iraise e = +type backtrace = Printexc.raw_backtrace +let backtrace_to_string = Printexc.raw_backtrace_to_string + +let backtrace_info : backtrace t = make () + +let is_recording = ref false + +let record_backtrace b = + let () = Printexc.record_backtrace b in + is_recording := b + +let get_backtrace e = get e backtrace_info + +let iraise (e,i) = let () = Mutex.lock lock in let id = Thread.id (Thread.self ()) in - let () = current := (id, e) :: remove_assoc id !current in + let () = current := (id, (e,i)) :: remove_assoc id !current in let () = Mutex.unlock lock in - raise (fst e) + match get i backtrace_info with + | None -> + raise e + | Some bt -> + Printexc.raise_with_backtrace e bt let raise ?info e = match info with | None -> @@ -72,11 +89,7 @@ let raise ?info e = match info with let () = Mutex.unlock lock in raise e | Some i -> - let () = Mutex.lock lock in - let id = Thread.id (Thread.self ()) in - let () = current := (id, (e, i)) :: remove_assoc id !current in - let () = Mutex.unlock lock in - raise e + iraise (e,i) let find_and_remove () = let () = Mutex.lock lock in @@ -104,3 +117,13 @@ let info e = (* Mismatch: the raised exception is not the one stored, either because the previous raise was not instrumented, or because something went wrong. *) Store.empty + +let capture e = + if !is_recording then + (* This must be the first function call, otherwise the stack may be + destroyed *) + let bt = Printexc.get_raw_backtrace () in + let info = info e in + e, add info backtrace_info bt + else + e, info e diff --git a/clib/exninfo.mli b/clib/exninfo.mli index 30803e3e6a..36cc44cf82 100644 --- a/clib/exninfo.mli +++ b/clib/exninfo.mli @@ -34,6 +34,49 @@ val get : info -> 'a t -> 'a option val info : exn -> info (** Retrieve the information of the last exception raised. *) +type backtrace + +val get_backtrace : info -> backtrace option +(** [get_backtrace info] does get the backtrace associated to info *) + +val backtrace_to_string : backtrace -> string +(** [backtrace_to_string info] does get the backtrace associated to info *) + +val record_backtrace : bool -> unit + +val capture : exn -> iexn +(** Add the current backtrace information to the given exception. + + The intended use case is of the form: {[ + + try foo + with + | Bar -> bar + | exn -> + let exn = Exninfo.capture err in + baz + + ]} + + where [baz] should re-raise using [iraise] below. + + WARNING: any intermediate code between the [with] and the handler may + modify the backtrace. Yes, that includes [when] clauses. Ideally, what you + should do is something like: {[ + + try foo + with exn -> + let exn = Exninfo.capture exn in + match err with + | Bar -> bar + | err -> baz + + ]} + + I admit that's a bit heavy, but there is not much to do... + +*) + val iraise : iexn -> 'a (** Raise the given enriched exception. *) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 9e9e3b4cfa..7342bc72e7 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -259,6 +259,13 @@ : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" ######################################################################## +# reduction-effects +######################################################################## +: "${reduction_effects_CI_REF:=master}" +: "${reduction_effects_CI_GITURL:=https://github.com/coq-community/reduction-effects}" +: "${reduction_effects_CI_ARCHIVEURL:=${reduction_effects_CI_GITURL}/archive}" + +######################################################################## # menhirlib ######################################################################## : "${menhirlib_CI_REF:=master}" diff --git a/dev/ci/ci-reduction_effects.sh b/dev/ci/ci-reduction_effects.sh new file mode 100755 index 0000000000..6b6de3fa2f --- /dev/null +++ b/dev/ci/ci-reduction_effects.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download reduction_effects + +( cd "${CI_BUILD_DIR}/reduction_effects" && make && make test && make install) diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 04b20c6889..3bc92e6aee 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,13 @@ ### ML API +Exception handling: + +- Coq's custom `Backtrace` module has been removed in favor of OCaml's + native backtrace implementation. Please use the functions in + `Exninfo.capture` and `iraise` when re-raising inside an exception + handler. + Printers: - Functions such as Printer.pr_lconstr_goal_style_env have been diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 835c20a4f7..f640a33773 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -254,7 +254,9 @@ let ppenvwithcst e = pp let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x)) -let ppobj obj = Format.print_string (Libobject.object_tag obj) +let ppobj obj = + let Libobject.Dyn.Dyn (tag, _) = obj in + Format.print_string (Libobject.Dyn.repr tag) let cnt = ref 0 diff --git a/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst b/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst new file mode 100644 index 0000000000..db433ad64c --- /dev/null +++ b/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst @@ -0,0 +1,5 @@ +- **Removed:** + The `-load-ml-source` and `-load-ml-object` command line options + have been removed; their use was very limited, you can achieve the same adding + additional object files in the linking step or using a plugin. + (`#11409 <https://github.com/coq/coq/pull/11409>`_, by Emilio Jesus Gallego Arias). diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index ba43128bdc..98d222e317 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -157,8 +157,6 @@ and ``coqtop``, unless stated otherwise: loading the default resource file from the standard configuration directories. :-q: Do not to load the default resource file. -:-load-ml-source *file*: Load the OCaml source file *file*. -:-load-ml-object *file*: Load the OCaml object file *file*. :-l *file*, -load-vernac-source *file*: Load and execute the |Coq| script from *file.v*. :-lv *file*, -load-vernac-source-verbose *file*: Load and execute the diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 853ddfd6dc..46215f16a6 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2222,14 +2222,14 @@ tactics to *permute* the subgoals generated by a tactic. If :token:`num`\'s value is :math:`k`, this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n` - in focus. The first subgoal becomes :math:`G_{n + 1 − k}` and the + in focus. Subgoal :math:`G_{n + 1 − k}` becomes the first, and the circular order of subgoals remains unchanged. .. tacn:: first @num last If :token:`num`\'s value is :math:`k`, this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n` - in focus. The first subgoal becomes :math:`G_k` and the circular order + in focus. Subgoal :math:`G_{k + 1 \bmod n}` becomes the first, and the circular order of subgoals remains unchanged. Finally, the tactics ``last`` and ``first`` combine with the branching syntax diff --git a/engine/evd.ml b/engine/evd.ml index 8e7d942c37..70f58163fd 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -902,14 +902,14 @@ let make_nonalgebraic_variable evd u = let fresh_sort_in_family ?loc ?(rigid=univ_flexible) evd s = with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family s) -let fresh_constant_instance ?loc env evd c = - with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c) +let fresh_constant_instance ?loc ?(rigid=univ_flexible) env evd c = + with_context_set ?loc rigid evd (UnivGen.fresh_constant_instance env c) -let fresh_inductive_instance ?loc env evd i = - with_context_set ?loc univ_flexible evd (UnivGen.fresh_inductive_instance env i) +let fresh_inductive_instance ?loc ?(rigid=univ_flexible) env evd i = + with_context_set ?loc rigid evd (UnivGen.fresh_inductive_instance env i) -let fresh_constructor_instance ?loc env evd c = - with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c) +let fresh_constructor_instance ?loc ?(rigid=univ_flexible) env evd c = + with_context_set ?loc rigid evd (UnivGen.fresh_constructor_instance env c) let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr = with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr) diff --git a/engine/evd.mli b/engine/evd.mli index 8843adc853..82e1003a65 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -653,10 +653,14 @@ val update_sigma_env : evar_map -> env -> evar_map (** Polymorphic universes *) -val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> evar_map -> Sorts.family -> evar_map * Sorts.t -val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant -val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive -val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor +val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid + -> evar_map -> Sorts.family -> evar_map * Sorts.t +val fresh_constant_instance : ?loc:Loc.t -> ?rigid:rigid + -> env -> evar_map -> Constant.t -> evar_map * pconstant +val fresh_inductive_instance : ?loc:Loc.t -> ?rigid:rigid + -> env -> evar_map -> inductive -> evar_map * pinductive +val fresh_constructor_instance : ?loc:Loc.t -> ?rigid:rigid + -> env -> evar_map -> constructor -> evar_map * pconstructor val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> GlobRef.t -> evar_map * econstr diff --git a/engine/univGen.ml b/engine/univGen.ml index 1fe09270ba..b270f9dc0b 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -48,8 +48,6 @@ let fresh_instance_from ?loc ctx = function (** Fresh universe polymorphic construction *) -open Globnames - let fresh_global_instance ?loc ?names env gr = let auctx = Environ.universes_of_global env gr in let u, ctx = fresh_instance_from ?loc auctx names in @@ -78,10 +76,6 @@ let constr_of_monomorphic_global gr = Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ str " would forget universes.") -let fresh_global_or_constr_instance env = function - | IsConstr c -> c, ContextSet.empty - | IsGlobal gr -> fresh_global_instance env gr - let fresh_sort_in_family = function | InSProp -> Sorts.sprop, ContextSet.empty | InProp -> Sorts.prop, ContextSet.empty diff --git a/engine/univGen.mli b/engine/univGen.mli index 1b351c61c4..bbde9d4e30 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -46,9 +46,6 @@ val fresh_constructor_instance : env -> constructor -> val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t -> constr in_universe_context_set -val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> - constr in_universe_context_set - (** Get fresh variables for the universe context. Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) val fresh_universe_context_set_instance : ContextSet.t -> diff --git a/ide/coqide.ml b/ide/coqide.ml index d7e155f6bb..e0347d3c5f 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1366,7 +1366,7 @@ let read_coqide_args argv = |"-debug"::args -> Minilib.debug := true; Flags.debug := true; - Backtrace.record_backtrace true; + Exninfo.record_backtrace true; filter_coqtop coqtop project_files bindings_files ("-debug"::out) args |"-coqtop-flags" :: flags :: args-> Coq.ideslave_coqtop_flags := Some flags; diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 33336079bb..4d15ce741c 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -128,7 +128,7 @@ let enforce_leq_alg u v g = | exception (UniverseInconsistency _ as e) -> Inr e) in (* max(us) <= max(vs) <-> forall u in us, exists v in vs, u <= v *) - let c = Universe.map (fun u -> Universe.map (fun v -> (u,v)) v) u in + let c = List.map (fun u -> List.map (fun v -> (u,v)) (Universe.repr v)) (Universe.repr u) in let c = List.cartesians enforce_one (Inl (Constraint.empty,g)) c in (* We pick a best constraint: smallest number of constraints, not an error if possible. *) let order x y = match x, y with diff --git a/kernel/univ.ml b/kernel/univ.ml index 0712774576..94f7076c02 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -42,6 +42,8 @@ struct let make dp i = (DirPath.hcons dp,i) + let repr x : t = x + let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i' let hash (d,i) = Hashset.Combine.combine i (DirPath.hash d) @@ -320,8 +322,9 @@ struct if u == v then 0 else let (x, n) = u and (x', n') = v in - if Int.equal n n' then Level.compare x x' - else n - n' + let c = Int.compare n n' in + if Int.equal 0 c then Level.compare x x' + else c let sprop = hcons (Level.sprop, 0) let prop = hcons (Level.prop, 0) @@ -427,6 +430,10 @@ struct let hcons = Hashcons.recursive_hcons Huniv.generate Huniv.hcons Expr.hcons + module Self = struct type nonrec t = t let compare = compare end + module Map = CMap.Make(Self) + module Set = CSet.Make(Self) + let make l = tip (Expr.make l) let tip x = tip x @@ -524,15 +531,10 @@ struct Used to type the products. *) let sup x y = merge_univs x y - let empty = [] - let exists = List.exists let for_all = List.for_all - - let smart_map = List.Smart.map - - let map = List.map + let repr x : t = x end type universe = Universe.t @@ -550,8 +552,6 @@ let pr_uni = Universe.pr let sup = Universe.sup let super = Universe.super -open Universe - let universe_level = Universe.level @@ -576,7 +576,7 @@ type univ_inconsistency = constraint_type * universe * universe * explanation La exception UniverseInconsistency of univ_inconsistency let error_inconsistency o u v p = - raise (UniverseInconsistency (o,make u,make v,p)) + raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p)) (* Constraints and sets of constraints. *) @@ -677,7 +677,7 @@ let enforce_eq u v c = let constraint_add_leq v u c = (* We just discard trivial constraints like u<=u *) - if Expr.equal v u then c + if Universe.Expr.equal v u then c else match v, u with | (x,n), (y,m) -> @@ -695,13 +695,13 @@ let constraint_add_leq v u c = else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *) else Constraint.add (x,Le,y) c (* u <= v implies u <= v+k *) -let check_univ_leq_one u v = Universe.exists (Expr.leq u) v +let check_univ_leq_one u v = Universe.exists (Universe.Expr.leq u) v let check_univ_leq u v = Universe.for_all (fun u -> check_univ_leq_one u v) u let enforce_leq u v c = - match is_sprop u, is_sprop v with + match Universe.is_sprop u, Universe.is_sprop v with | true, true -> c | true, false | false, true -> raise (UniverseInconsistency (Le, u, v, None)) @@ -925,7 +925,7 @@ let subst_instance_instance s i = let subst_instance_universe s u = let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in - let u' = Universe.smart_map f u in + let u' = List.Smart.map f u in if u == u' then u else Universe.sort u' @@ -1108,7 +1108,7 @@ let subst_univs_level_level subst l = let subst_univs_level_universe subst u = let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in - let u' = Universe.smart_map f u in + let u' = List.Smart.map f u in if u == u' then u else Universe.sort u' @@ -1150,7 +1150,7 @@ let subst_univs_universe fn ul = if CList.is_empty subst then ul else let substs = - List.fold_left Universe.merge_univs Universe.empty subst + List.fold_left Universe.merge_univs [] subst in List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u)) substs nosubst diff --git a/kernel/univ.mli b/kernel/univ.mli index f7c984870f..94e57b9efc 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -16,6 +16,7 @@ sig type t val make : Names.DirPath.t -> int -> t + val repr : t -> Names.DirPath.t * int val equal : t -> t -> bool val hash : t -> int val compare : t -> t -> int @@ -138,8 +139,10 @@ sig val exists : (Level.t * int -> bool) -> t -> bool val for_all : (Level.t * int -> bool) -> t -> bool + val repr : t -> (Level.t * int) list - val map : (Level.t * int -> 'a) -> t -> 'a list + module Set : CSet.S with type elt = t + module Map : CMap.ExtS with type key = t and module Set := Set end diff --git a/lib/cErrors.ml b/lib/cErrors.ml index b9735d0579..9f496f5845 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -12,7 +12,7 @@ open Pp (** Aliases *) -let push = Backtrace.add_backtrace +let push = Exninfo.capture (* Errors *) @@ -51,12 +51,10 @@ let raw_anomaly e = match e with | _ -> str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." -let print_backtrace e = match Backtrace.get_backtrace e with +let print_backtrace e = match Exninfo.get_backtrace e with | None -> mt () | Some bt -> - let bt = Backtrace.repr bt in - let pr_frame f = str (Backtrace.print_frame f) in - let bt = prlist_with_sep fnl pr_frame bt in + let bt = str (Exninfo.backtrace_to_string bt) in fnl () ++ hov 0 bt let print_anomaly askreport e = diff --git a/lib/control.ml b/lib/control.ml index 7d54838df8..e67e88ee95 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -38,7 +38,7 @@ let unix_timeout n f x e = restore_timeout (); res with e -> - let e = Backtrace.add_backtrace e in + let e = Exninfo.capture e in restore_timeout (); Exninfo.iraise e @@ -76,7 +76,7 @@ let windows_timeout n f x e = else raise e | e -> let () = killed := true in - let e = Backtrace.add_backtrace e in + let e = Exninfo.capture e in Exninfo.iraise e type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b } @@ -102,7 +102,7 @@ let protect_sigalrm f x = | true, Sys.Signal_handle f -> f Sys.sigalrm; res | _, _ -> res with e -> - let e = Backtrace.add_backtrace e in + let e = Exninfo.capture e in Sys.set_signal Sys.sigalrm old_handler; Exninfo.iraise e with Invalid_argument _ -> (* This happens on Windows, as handling SIGALRM does not seem supported *) diff --git a/lib/flags.ml b/lib/flags.ml index b87ba46634..ad48024761 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -19,7 +19,7 @@ let with_modified_ref ?(restore=true) r nf f x = if restore || pre == !r then r := old_ref; res with reraise -> - let reraise = Backtrace.add_backtrace reraise in + let reraise = Exninfo.capture reraise in r := old_ref; Exninfo.iraise reraise @@ -37,7 +37,7 @@ let with_options ol f x = let r = f x in let () = List.iter2 (:=) ol vl in r with reraise -> - let reraise = Backtrace.add_backtrace reraise in + let reraise = Exninfo.capture reraise in let () = List.iter2 (:=) ol vl in Exninfo.iraise reraise @@ -203,7 +203,7 @@ let pp_with ft pp = in try pp_cmd pp with reraise -> - let reraise = Backtrace.add_backtrace reraise in + let reraise = Exninfo.capture reraise in let () = Format.pp_print_flush ft () in Exninfo.iraise reraise diff --git a/library/globnames.ml b/library/globnames.ml index acb05f9ac0..63cb2c69bd 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -123,7 +123,3 @@ module ExtRefOrdered = struct | SynDef kn -> combinesmall 2 (KerName.hash kn) end - -type global_reference_or_constr = - | IsGlobal of GlobRef.t - | IsConstr of constr diff --git a/library/globnames.mli b/library/globnames.mli index 48cbb11b66..d61cdd2b64 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -59,7 +59,3 @@ module ExtRefOrdered : sig val equal : t -> t -> bool val hash : t -> int end - -type global_reference_or_constr = - | IsGlobal of GlobRef.t - | IsConstr of constr diff --git a/library/lib.ml b/library/lib.ml index 9cce9b92ad..7f96adeecf 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -500,7 +500,7 @@ let close_section () = type frozen = lib_state -let freeze ~marshallable = !lib_state +let freeze () = !lib_state let unfreeze st = lib_state := st diff --git a/library/lib.mli b/library/lib.mli index 0d03046dc2..1fe72389f6 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -151,7 +151,7 @@ val close_section : unit -> unit type frozen -val freeze : marshallable:bool -> frozen +val freeze : unit -> frozen val unfreeze : frozen -> unit (** Keep only the libobject structure, not the objects themselves *) diff --git a/library/libobject.ml b/library/libobject.ml index c9ea6bcff8..28d0654444 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -82,8 +82,6 @@ and objects = (Names.Id.t * t) list and substitutive_objects = MBId.t list * algebraic_objects -let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t - module DynMap = Dyn.Map (struct type 'a t = 'a object_declaration end) let cache_tab = ref DynMap.empty @@ -92,14 +90,12 @@ let declare_object_full odecl = let na = odecl.object_name in let tag = Dyn.create na in let () = cache_tab := DynMap.add tag odecl !cache_tab in - let infun v = Dyn.Dyn (tag, v) in - let outfun v = match Dyn.Easy.prj v tag with - | None -> assert false - | Some v -> v - in - (infun,outfun) + tag -let declare_object odecl = fst (declare_object_full odecl) +let declare_object odecl = + let tag = declare_object_full odecl in + let infun v = Dyn.Dyn (tag, v) in + infun let cache_object (sp, Dyn.Dyn (tag, v)) = let decl = DynMap.find tag !cache_tab in diff --git a/library/libobject.mli b/library/libobject.mli index 146ccc293f..c25345994a 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -101,7 +101,9 @@ val ident_subst_function : substitution * 'a -> 'a will hand back two functions, the "injection" and "projection" functions for dynamically typed library-objects. *) -type obj +module Dyn : Dyn.S + +type obj = Dyn.t type algebraic_objects = | Objs of objects @@ -120,13 +122,11 @@ and objects = (Names.Id.t * t) list and substitutive_objects = Names.MBId.t list * algebraic_objects val declare_object_full : - 'a object_declaration -> ('a -> obj) * (obj -> 'a) + 'a object_declaration -> 'a Dyn.tag val declare_object : 'a object_declaration -> ('a -> obj) -val object_tag : obj -> string - val cache_object : object_name * obj -> unit val load_object : int -> object_name * obj -> unit val open_object : int -> object_name * obj -> unit diff --git a/library/states.ml b/library/states.ml index 0be153d96a..90303a2a5c 100644 --- a/library/states.ml +++ b/library/states.ml @@ -18,7 +18,7 @@ let replace_summary (lib,_) st = lib, st let replace_lib (_,st) lib = lib, st let freeze ~marshallable = - (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable) + (Lib.freeze (), Summary.freeze_summaries ~marshallable) let unfreeze (fl,fs) = Lib.unfreeze fl; diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 35110552ab..2dc3e8a934 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -26,19 +26,29 @@ open Common (*S Part I: computing Coq environment. *) (***************************************) +(* FIXME: this is a Libobject hack that should be removed. *) +module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> (Label.t * structure_field_body) option end) + +let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with +| f -> f o +| exception Not_found -> None + let toplevel_env () = let get_reference = function - | (_,kn), Lib.Leaf Libobject.AtomicObject o -> - let mp,l = KerName.repr kn in - begin match Libobject.object_tag o with - | "CONSTANT" -> + | (_,kn), Lib.Leaf Libobject.AtomicObject o -> + let mp,l = KerName.repr kn in + let handler = + DynHandle.add Declare.Internal.objConstant begin fun _ -> let constant = Global.lookup_constant (Constant.make1 kn) in Some (l, SFBconst constant) - | "INDUCTIVE" -> + end @@ + DynHandle.add DeclareInd.Internal.objInductive begin fun _ -> let inductive = Global.lookup_mind (MutInd.make1 kn) in Some (l, SFBmind inductive) - | _ -> None - end + end @@ + DynHandle.empty + in + handle handler o | (_,kn), Lib.Leaf Libobject.ModuleObject _ -> let mp,l = KerName.repr kn in let modl = Global.lookup_module (MPdot (mp, l)) in diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 70c1077106..f6fbdaa958 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -164,7 +164,7 @@ let rawnum_of_r c = match DAst.get c with let s, i = if is_pos_or_zero i then SPlus, i else SMinus, neg i in let i = Bigint.to_string i in let se = if is_gr md glob_Rdiv then "-" else "" in - let e = se ^ Bigint.to_string e in + let e = "e" ^ se ^ Bigint.to_string e in s, { NumTok.int = i; frac = ""; exp = e } | _ -> raise Non_closed_number end diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 037006bc47..b042437a22 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -696,7 +696,7 @@ let detype_universe sigma u = if Univ.Level.is_set l then GSet else GType (hack_qualid_of_univ_level sigma l) in (s, n) in - Univ.Universe.map fn u + List.map fn (Univ.Universe.repr u) let detype_sort sigma = function | SProp -> UNamed [GSProp,0] diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 909804d0c9..fd689602df 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -138,7 +138,7 @@ module Make(T : Task) () = struct set_slave_opt tl (* We need to pass some options with one argument *) | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" | "-compat" - | "-load-ml-object" | "-load-ml-source" | "-require" | "-w" | "-color" | "-init-file" + | "-require" | "-w" | "-color" | "-init-file" | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names" | "-set" | "-unset" | "-diffs" | "-mangle-name" | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl -> x :: a :: set_slave_opt tl diff --git a/stm/stm.ml b/stm/stm.ml index eff2403eca..4c539684e3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2362,7 +2362,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in - st, Lib.freeze ~marshallable:false in + st, Lib.freeze () in let inject_non_pstate (s,l) = Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env () diff --git a/tactics/declare.ml b/tactics/declare.ml index 9a14f4d40f..c7581fb0e0 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -130,8 +130,8 @@ let dummy_constant cst = { let classify_constant cst = Substitute (dummy_constant cst) -let (inConstant : constant_obj -> obj) = - declare_object { (default_object "CONSTANT") with +let (objConstant : constant_obj Libobject.Dyn.tag) = + declare_object_full { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; open_function = open_constant; @@ -139,6 +139,8 @@ let (inConstant : constant_obj -> obj) = subst_function = ident_subst_function; discharge_function = discharge_constant } +let inConstant v = Libobject.Dyn.Easy.inj v objConstant + let update_tables c = Impargs.declare_constant_implicits c; Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstRef c) @@ -357,10 +359,12 @@ type variable_declaration = (* This object is only for things which iterate over objects to find variables (only Prettyp.print_context AFAICT) *) -let inVariable : unit -> obj = - declare_object { (default_object "VARIABLE") with +let objVariable : unit Libobject.Dyn.tag = + declare_object_full { (default_object "VARIABLE") with classify_function = (fun () -> Dispose)} +let inVariable v = Libobject.Dyn.Easy.inj v objVariable + let declare_variable ~name ~kind d = (* Variables are distinguished by only short names *) if Decls.variable_exists name then @@ -497,4 +501,9 @@ module Internal = struct ; proof_entry_type = Some typ }, args + type nonrec constant_obj = constant_obj + + let objVariable = objVariable + let objConstant = objConstant + end diff --git a/tactics/declare.mli b/tactics/declare.mli index c646d2f85b..00c1e31717 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -131,7 +131,8 @@ val check_exists : Id.t -> unit (* Used outside this module only in indschemes *) exception AlreadyDeclared of (string option * Id.t) -(* For legacy support, do not use *) +(** {6 For legacy support, do not use} *) + module Internal : sig val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry @@ -145,4 +146,9 @@ module Internal : sig val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list + type constant_obj + + val objConstant : constant_obj Libobject.Dyn.tag + val objVariable : unit Libobject.Dyn.tag + end diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index d6fda00ad8..6cdb24965d 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -49,14 +49,14 @@ let optimize_non_type_induction_scheme kind dep sort ind = let sigma = Evd.minimize_universes sigma in (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma) else - let sigma, pind = Evd.fresh_inductive_instance env sigma ind in + let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in (c, Evd.evar_universe_context sigma) let build_induction_scheme_in_type dep sort ind = let env = Global.env () in let sigma = Evd.from_env env in - let sigma, pind = Evd.fresh_inductive_instance env sigma ind in + let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in c, Evd.evar_universe_context sigma diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v index 75b2a56169..fbd9c8bcba 100644 --- a/test-suite/failure/Template.v +++ b/test-suite/failure/Template.v @@ -1,4 +1,4 @@ -(* + Module TestUnsetTemplateCheck. Unset Template Check. @@ -15,18 +15,14 @@ Module TestUnsetTemplateCheck. (* Can only succeed if no template check is performed *) Check myind True : Prop. - Print Assumptions myind. - (* - Axioms: - myind is template polymorphic on all its universe parameters. - *) About myind. -(* -myind : Type@{Top.60} -> Type@{Top.60} -myind is assumed template universe polymorphic on Top.60 -Argument scope is [type_scope] -Expands to: Inductive Top.TestUnsetTemplateCheck.myind -*) + (* test discharge puts things in the right order (by using the + checker on the result) *) + Section S. + + Variables (A:Type) (a:A). + Inductive bb (B:Type) := BB : forall a', a = a' -> B -> bb B. + End S. + End TestUnsetTemplateCheck. -*) diff --git a/test-suite/output/QArithSyntax.out b/test-suite/output/QArithSyntax.out new file mode 100644 index 0000000000..6bc04f1cef --- /dev/null +++ b/test-suite/output/QArithSyntax.out @@ -0,0 +1,14 @@ +eq_refl : 102e-2 = 102e-2 + : 102e-2 = 102e-2 +eq_refl : 102e-1 = 102e-1 + : 102e-1 = 102e-1 +eq_refl : 1020 = 1020 + : 1020 = 1020 +eq_refl : 102 = 102 + : 102 = 102 +eq_refl : 102e-2 = 102e-2 + : 102e-2 = 102e-2 +eq_refl : -1e-4 = -1e-4 + : -1e-4 = -1e-4 +eq_refl : -50e-2 = -50e-2 + : -50e-2 = -50e-2 diff --git a/test-suite/success/QArithSyntax.v b/test-suite/output/QArithSyntax.v index 2f2ee0134a..2f2ee0134a 100644 --- a/test-suite/success/QArithSyntax.v +++ b/test-suite/output/QArithSyntax.v diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out index e6f7556d96..2d877bd813 100644 --- a/test-suite/output/RealSyntax.out +++ b/test-suite/output/RealSyntax.out @@ -2,3 +2,17 @@ : R (-31)%R : R +eq_refl : 102e-2 = 102e-2 + : 102e-2 = 102e-2 +eq_refl : 102e-1 = 102e-1 + : 102e-1 = 102e-1 +eq_refl : 102e1 = 102e1 + : 102e1 = 102e1 +eq_refl : 102 = 102 + : 102 = 102 +eq_refl : 102e-2 = 102e-2 + : 102e-2 = 102e-2 +eq_refl : -1e-4 = -1e-4 + : -1e-4 = -1e-4 +eq_refl : -50e-2 = -50e-2 + : -50e-2 = -50e-2 diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v index 44e8c7a50c..cb3bce70d4 100644 --- a/test-suite/output/RealSyntax.v +++ b/test-suite/output/RealSyntax.v @@ -1,3 +1,25 @@ Require Import Reals.Rdefinitions. Check 32%R. Check (-31)%R. + +Open Scope R_scope. + +Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)). +Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)). +Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)). +Check (eq_refl : 1.02e+02 = IZR 102). +Check (eq_refl : 10.2e-1 = 1.02). +Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)). +Check (eq_refl : -0.50 = IZR (-50) / IZR (Z.pow_pos 10 2)). + +Require Import Reals. + +Goal 254e3 = 2540 * 10 ^ 2. +ring. +Qed. + +Require Import Psatz. + +Goal 254e3 = 2540 * 10 ^ 2. +lra. +Qed. diff --git a/test-suite/success/RealSyntax.v b/test-suite/success/RealSyntax.v deleted file mode 100644 index 2765200991..0000000000 --- a/test-suite/success/RealSyntax.v +++ /dev/null @@ -1,19 +0,0 @@ -Require Import Reals. -Open Scope R_scope. -Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)). -Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)). -Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)). -Check (eq_refl : 1.02e+02 = IZR 102). -Check (eq_refl : 10.2e-1 = 1.02). -Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)). -Check (eq_refl : -0.5 = IZR (-5) / IZR (Z.pow_pos 10 1)). - -Goal 254e3 = 2540 * 10 ^ 2. -ring. -Qed. - -Require Import Psatz. - -Goal 254e3 = 2540 * 10 ^ 2. -lra. -Qed. diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v index 855f26698c..4b928007cf 100644 --- a/test-suite/success/Scheme.v +++ b/test-suite/success/Scheme.v @@ -25,3 +25,8 @@ Check myeq_rew_fwd_r_dep. Set Rewriting Schemes. Inductive myeq_true : bool -> Prop := myrefl_true : myeq_true true. Unset Rewriting Schemes. + +(* check that the scheme doesn't minimize itself into something non general *) +Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= . +Lemma bla@{u v|u < v} : foo@{u v} -> False. +Proof. induction 1. Qed. diff --git a/topbin/coqtop_byte_bin.ml b/topbin/coqtop_byte_bin.ml index aaabd90370..604c6e251a 100644 --- a/topbin/coqtop_byte_bin.ml +++ b/topbin/coqtop_byte_bin.ml @@ -8,6 +8,14 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(* We register this handler for lower-level toplevel loading code *) +let _ = CErrors.register_handler (function + | Symtable.Error e -> + Pp.str (Format.asprintf "%a" Symtable.report_error e) + | _ -> + raise CErrors.Unhandled + ) + let drop_setup () = begin try (* Enable rectypes in the toplevel if it has the directive #rectypes *) @@ -23,7 +31,6 @@ let drop_setup () = { load_obj = (fun f -> if not (Topdirs.load_file ppf f) then CErrors.user_err Pp.(str ("Could not load plugin "^f)) ); - use_file = Topdirs.dir_use ppf; add_dir = Topdirs.dir_directory; ml_loop = (fun () -> Toploop.loop ppf); }) diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 56a6312b61..74d9c113d6 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -198,14 +198,6 @@ let set_query opts q = | Queries queries -> Queries (queries@[q]) } -let warn_depr_load_ml_object = - CWarnings.create ~name:"deprecated-mlobject" ~category:"deprecated" - (fun () -> Pp.strbrk "The -load-ml-object option is deprecated, see the changelog for more details.") - -let warn_depr_ml_load_source = - CWarnings.create ~name:"deprecated-mlsource" ~category:"deprecated" - (fun () -> Pp.strbrk "The -load-ml-source option is deprecated, see the changelog for more details.") - let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") @@ -403,14 +395,6 @@ let parse_args ~help ~init arglist : t * string list = |"-inputstate"|"-is" -> set_inputstate oval (next ()) - |"-load-ml-object" -> - warn_depr_load_ml_object (); - Mltop.dir_ml_load (next ()); oval - - |"-load-ml-source" -> - warn_depr_ml_load_source (); - Mltop.dir_ml_use (next ()); oval - |"-load-vernac-object" -> add_vo_require oval (next ()) None None @@ -513,7 +497,7 @@ let parse_args ~help ~init arglist : t * string list = }}} |"-test-mode" -> Vernacinterp.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval - |"-bt" -> Backtrace.record_backtrace true; oval + |"-bt" -> Exninfo.record_backtrace true; oval |"-color" -> set_color oval (next ()) |"-config"|"--config" -> set_query oval PrintConfig |"-debug" -> Coqinit.set_debug (); oval diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index ae37e40101..ac348b9646 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -14,7 +14,7 @@ open Pp let ( / ) s1 s2 = Filename.concat s1 s2 let set_debug () = - let () = Backtrace.record_backtrace true in + let () = Exninfo.record_backtrace true in Flags.debug := true (* Loading of the resource file. diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index e1748d5c1c..977cae6254 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -469,6 +469,16 @@ let rec vernac_loop ~state = (* Exception printing should be done by the feedback listener, however this is not yet ready so we rely on the exception for now. *) + | Sys_blocked_io -> + (* the parser doesn't like nonblocking mode, cf #10918 *) + let msg = + Pp.(strbrk "Coqtop needs the standard input to be in blocking mode." ++ spc() + ++ str "One way of clearing the non-blocking flag is through python:" ++ fnl() + ++ str " import os" ++ fnl() + ++ str " os.set_blocking(0, True)") + in + TopErr.print_error_for_buffer Feedback.Error msg top_buffer; + exit 1 | any -> let (e, info) = CErrors.push any in let loc = Loc.get_loc info in diff --git a/toplevel/usage.ml b/toplevel/usage.ml index b17ca71f4c..051638d53c 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -36,8 +36,6 @@ let print_usage_common co command = \n -nois (idem)\ \n -compat X.Y provides compatibility support for Coq version X.Y\ \n\ -\n -load-ml-object f load ML object file f\ -\n -load-ml-source f load ML file f\ \n -load-vernac-source f load Coq file f.v (Load \"f\".)\ \n -l f (idem)\ \n -load-vernac-source-verbose f load Coq file f.v (Load Verbose \"f\".)\ diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index bca6b48499..adcce67b0d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -69,10 +69,10 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = let new_proof = Vernacstate.Proof_global.give_me_the_proof_opt () [@ocaml.warning "-3"] in { state with doc = ndoc; sid = nsid; proof = new_proof; } with reraise -> + let (reraise, info) = CErrors.push reraise in (* XXX: In non-interactive mode edit_at seems to do very weird things, so we better avoid it while we investigate *) if interactive then ignore(Stm.edit_at ~doc:state.doc state.sid); - let (reraise, info) = CErrors.push reraise in let info = begin match Loc.get_loc info with | None -> Option.cata (Loc.add_loc info) info loc diff --git a/vernac/classes.ml b/vernac/classes.ml index c9b5144299..77bc4e4f8a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -42,13 +42,10 @@ let () = Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state let add_instance_hint inst path local info poly = - let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) - | IsGlobal gr -> Hints.IsGlobRef gr - in Flags.silently (fun () -> Hints.add_hints ~local [typeclasses_db] (Hints.HintsResolveEntry - [info, poly, false, Hints.PathHints path, inst'])) () + [info, poly, false, Hints.PathHints path, inst])) () let is_local_for_hint i = match i.is_global with @@ -61,9 +58,9 @@ let is_local_for_hint i = let add_instance check inst = let poly = Global.is_polymorphic inst.is_impl in let local = is_local_for_hint inst in - add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] local + add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] local inst.is_info poly; - List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path + List.iter (fun (path, pri, c) -> add_instance_hint (Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)) path local pri poly) (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml index 2375028541..7dd53564cc 100644 --- a/vernac/declareInd.ml +++ b/vernac/declareInd.ml @@ -60,9 +60,9 @@ let cache_inductive ((sp, kn), names) = let discharge_inductive ((sp, kn), names) = Some names -let inInductive : inductive_obj -> Libobject.obj = +let objInductive : inductive_obj Libobject.Dyn.tag = let open Libobject in - declare_object {(default_object "INDUCTIVE") with + declare_object_full {(default_object "INDUCTIVE") with cache_function = cache_inductive; load_function = load_inductive; open_function = open_inductive; @@ -71,6 +71,7 @@ let inInductive : inductive_obj -> Libobject.obj = discharge_function = discharge_inductive; } +let inInductive v = Libobject.Dyn.Easy.inj v objInductive let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c @@ -212,3 +213,9 @@ let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie p if mie.mind_entry_private == None then Indschemes.declare_default_schemes mind; mind + +module Internal = +struct + type nonrec inductive_obj = inductive_obj + let objInductive = objInductive +end diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli index df8895a999..17647d50aa 100644 --- a/vernac/declareInd.mli +++ b/vernac/declareInd.mli @@ -21,3 +21,12 @@ val declare_mutual_inductive_with_eliminations -> UnivNames.universe_binders -> one_inductive_impls list -> Names.MutInd.t + +(** {6 For legacy support, do not use} *) +module Internal : +sig + +type inductive_obj +val objInductive : inductive_obj Libobject.Dyn.tag + +end diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ba7ae5069b..eb39564fed 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1364,7 +1364,6 @@ let explain_exn_default = function | Sys_error msg -> hov 0 (str "System error: " ++ quote (str msg)) | Out_of_memory -> hov 0 (str "Out of memory.") | Stack_overflow -> hov 0 (str "Stack overflow.") - | Dynlink.Error e -> hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e)) | CErrors.Timeout -> hov 0 (str "Timeout!") | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") (* Otherwise, not handled here *) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 222e9eb825..05e23164b1 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1346,7 +1346,7 @@ let inNotation : notation_obj -> obj = (**********************************************************************) let with_lib_stk_protection f x = - let fs = Lib.freeze ~marshallable:false in + let fs = Lib.freeze () in try let a = f x in Lib.unfreeze fs; a with reraise -> let reraise = CErrors.push reraise in diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 9c18441d9c..2bac35b08f 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -56,7 +56,6 @@ let keep_copy_mlpath path = (* If there is a toplevel under Coq *) type toplevel = { load_obj : string -> unit; - use_file : string -> unit; add_dir : string -> unit; ml_loop : unit -> unit } @@ -94,43 +93,26 @@ let ocaml_toploop () = | WithTop t -> Printexc.catch t.ml_loop () | _ -> () -(* Try to interpret load_obj's (internal) errors *) -let report_on_load_obj_error exc = - let x = Obj.repr exc in - (* Try an horrible (fragile) hack to report on Symtable dynlink errors *) - (* (we follow ocaml's Printexc.to_string decoding of exceptions) *) - if Obj.is_block x && String.equal (Obj.magic (Obj.field (Obj.field x 0) 0)) "Symtable.Error" - then - let err_block = Obj.field x 1 in - if Int.equal (Obj.tag err_block) 0 then - (* Symtable.Undefined_global of string *) - str "reference to undefined global " ++ - str (Obj.magic (Obj.field err_block 0)) - else str (Printexc.to_string exc) - else str (Printexc.to_string exc) - (* Dynamic loading of .cmo/.cma *) +(* We register errors at least for Dynlink, it is possible to do so Symtable + too, as we do in the bytecode init code. +*) +let _ = CErrors.register_handler (function + | Dynlink.Error e -> + hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e)) + | _ -> + raise CErrors.Unhandled + ) + let ml_load s = - match !load with - | WithTop t -> - (try t.load_obj s; s - with - | e when CErrors.noncritical e -> - let e = CErrors.push e in - match fst e with - | (UserError _ | Failure _ | Not_found as u) -> Exninfo.iraise (u, snd e) - | exc -> - let msg = report_on_load_obj_error exc in - user_err ~hdr:"Mltop.load_object" (str"Cannot link ml-object " ++ - str s ++ str" to Coq code (" ++ msg ++ str ").")) - | WithoutTop -> - try - Dynlink.loadfile s; s - with Dynlink.Error a -> - user_err ~hdr:"Mltop.load_object" - (strbrk "while loading " ++ str s ++ - strbrk ": " ++ str (Dynlink.error_message a)) + (match !load with + | WithTop t -> + t.load_obj s + | WithoutTop -> + Dynlink.loadfile s + ); + s let dir_ml_load s = match !load with @@ -140,17 +122,6 @@ let dir_ml_load s = let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in ml_load gname -(* Dynamic interpretation of .ml *) -let dir_ml_use s = - match !load with - | WithTop t -> t.use_file s - | _ -> - let moreinfo = - if Sys.(backend_type = Native) then " Loading ML code works only in bytecode." - else "" - in - user_err ~hdr:"Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo) - (* Adds a path to the ML paths *) let add_ml_dir s = match !load with @@ -275,7 +246,6 @@ let load_ml_object mname ?path fname= init_ml_object mname; path -let dir_ml_load m = ignore(dir_ml_load m) let add_known_module m = add_known_module m None (* Summary of declared ML Modules *) diff --git a/vernac/mltop.mli b/vernac/mltop.mli index 56a28b64b0..271772d7ba 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -14,7 +14,6 @@ record. *) type toplevel = { load_obj : string -> unit; - use_file : string -> unit; add_dir : string -> unit; ml_loop : unit -> unit } @@ -38,12 +37,6 @@ val add_ml_dir : recursive:bool -> string -> unit (** Tests if we can load ML files *) val has_dynlink : bool -(** Dynamic loading of .cmo *) -val dir_ml_load : string -> unit - -(** Dynamic interpretation of .ml *) -val dir_ml_use : string -> unit - (** List of modules linked to the toplevel *) val add_known_module : string -> unit val module_is_known : string -> bool diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index b999ce9f3f..2cd1cf7c65 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -670,25 +670,35 @@ let gallina_print_syntactic_def env kn = Constrextern.without_specific_symbols [Notation.SynDefRule kn] (pr_glob_constr_env env) c) -let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = +module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> Pp.t option end) + +let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with +| f -> f o +| exception Not_found -> None + +(* TODO: this kind of feature should not rely on the Libobject stack. There is + no reason that an object in the stack corresponds to a user-facing + declaration. It may have been so at the time this was written, but this + needs to be done in a more principled way. *) +let gallina_print_leaf_entry env sigma with_values ((sp, kn),lobj) = let sep = if with_values then " = " else " : " in match lobj with | AtomicObject o -> - let tag = object_tag o in - begin match (oname,tag) with - | (_,"VARIABLE") -> + let handler = + DynHandle.add Declare.Internal.objVariable begin fun _ -> (* Outside sections, VARIABLES still exist but only with universes constraints *) (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) - | (_,"CONSTANT") -> + end @@ + DynHandle.add Declare.Internal.objConstant begin fun _ -> Some (print_constant with_values sep (Constant.make1 kn) None) - | (_,"INDUCTIVE") -> + end @@ + DynHandle.add DeclareInd.Internal.objInductive begin fun _ -> Some (gallina_print_inductive (MutInd.make1 kn) None) - | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| - "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None - (* To deal with forgotten cases... *) - | (_,s) -> None - end + end @@ + DynHandle.empty + in + handle handler o | ModuleObject _ -> let (mp,l) = KerName.repr kn in Some (print_module with_values ~mod_ops:Declaremods.mod_ops (MPdot (mp,l))) @@ -777,11 +787,18 @@ let print_full_context env sigma = let print_full_context_typ env sigma = print_context env sigma false None (Lib.contents ()) +module DynHandleF = Libobject.Dyn.Map(struct type 'a t = 'a -> Pp.t end) + +let handleF h (Libobject.Dyn.Dyn (tag, o)) = match DynHandleF.find tag h with +| f -> f o +| exception Not_found -> mt () + +(* TODO: see the comment for {!gallina_print_leaf_entry} *) let print_full_pure_context env sigma = let rec prec = function | ((_,kn),Lib.Leaf AtomicObject lobj)::rest -> - let pp = match object_tag lobj with - | "CONSTANT" -> + let handler = + DynHandleF.add Declare.Internal.objConstant begin fun _ -> let con = Global.constant_of_delta_kn kn in let cb = Global.lookup_constant con in let typ = cb.const_type in @@ -804,12 +821,16 @@ let print_full_pure_context env sigma = str "Primitive " ++ print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ) ++ str "." ++ fnl () ++ fnl () - | "INDUCTIVE" -> + end @@ + DynHandleF.add DeclareInd.Internal.objInductive begin fun _ -> let mind = Global.mind_of_delta_kn kn in let mib = Global.lookup_mind mind in pr_mutual_inductive_body (Global.env()) mind mib None ++ str "." ++ fnl () ++ fnl () - | _ -> mt () in + end @@ + DynHandleF.empty + in + let pp = handleF handler lobj in prec rest ++ pp | ((_,kn),Lib.Leaf ModuleObject _)::rest -> (* TODO: make it reparsable *) diff --git a/vernac/search.ml b/vernac/search.ml index 364dae7152..b8825c3b29 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -71,6 +71,14 @@ let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> env -> constr -> unit) = let pfctxt = named_context e in iter_named_context_name_type iter_hyp pfctxt +(* FIXME: this is a Libobject hack that should be replaced with a proper + registration mechanism. *) +module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> unit end) + +let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with +| f -> f o +| exception Not_found -> () + (* General search over declarations *) let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = let env = Global.env () in @@ -78,13 +86,14 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = (Environ.named_context env); let iter_obj (sp, kn) lobj = match lobj with | AtomicObject o -> - begin match object_tag o with - | "CONSTANT" -> + let handler = + DynHandle.add Declare.Internal.objConstant begin fun _ -> let cst = Global.constant_of_delta_kn kn in let gr = GlobRef.ConstRef cst in let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in fn gr env typ - | "INDUCTIVE" -> + end @@ + DynHandle.add DeclareInd.Internal.objInductive begin fun _ -> let mind = Global.mind_of_delta_kn kn in let mib = Global.lookup_mind mind in let iter_packet i mip = @@ -97,8 +106,10 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = iter_constructors ind u fn env len in Array.iteri iter_packet mib.mind_packets - | _ -> () - end + end @@ + DynHandle.empty + in + handle handler o | _ -> () in try Declaremods.iter_all_segments iter_obj diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 45f40b1258..de02f7ecfb 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -359,7 +359,7 @@ let in_phase ~phase f x = default_phase := op; res with exn -> - let iexn = Backtrace.add_backtrace exn in + let iexn = Exninfo.capture exn in default_phase := op; Util.iraise iexn @@ -415,7 +415,7 @@ let with_output_to_file fname func input = close_out channel; output with reraise -> - let reraise = Backtrace.add_backtrace reraise in + let reraise = Exninfo.capture reraise in std_ft := Util.pi1 old_fmt; err_ft := Util.pi2 old_fmt; deep_ft := Util.pi3 old_fmt; diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 7b4924eaed..6e398d87ca 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -19,11 +19,9 @@ DeclareObl Canonical RecLemmas Library -Prettyp Lemmas ComCoercion Auto_ind_decl -Search Indschemes Obligations ComDefinition @@ -31,6 +29,8 @@ Classes ComPrimitive ComAssumption DeclareInd +Search +Prettyp ComInductive ComFixpoint ComProgramFixpoint |