diff options
105 files changed, 1329 insertions, 708 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 9b208f5a24..b1709e1921 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -19,7 +19,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2020-09-17-V88" + CACHEKEY: "bionic_coq-V2020-10-12-V89" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh index 7625e4e7f7..41f204385f 100755 --- a/dev/bench/gitlab.sh +++ b/dev/bench/gitlab.sh @@ -428,6 +428,9 @@ for coq_opam_package in $sorted_coq_opam_packages; do new_base_path=$new_ocaml_switch/.opam-switch/build/$coq_opam_package.dev*/ old_base_path=$old_ocaml_switch/.opam-switch/build/$coq_opam_package.dev*/ for vo in `cd $new_opam_root/$new_base_path/; find -name '*.vo'`; do + if [ -e $old_opam_root/$old_base_path/$vo ]; then + echo "$coq_opam_package/$vo $(stat -c%s $old_opam_root/$old_base_path/$vo) $(stat -c%s $new_opam_root/$new_base_path/$vo)" >> "$log_dir/vosize.log" + fi if [ -e $old_opam_root/$old_base_path/${vo%%o}.timing -a \ -e $new_opam_root/$new_base_path/${vo%%o}.timing ]; then mkdir -p $working_dir/html/$coq_opam_package/`dirname $vo`/ diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index fcc585117b..fc8921e63d 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1204,7 +1204,7 @@ function make_elpi { make_dune make_re - if build_prep https://github.com/LPCIC/elpi/archive v1.11.0 tar.gz 1 elpi; then + if build_prep https://github.com/LPCIC/elpi/archive v1.11.4 tar.gz 1 elpi; then log2 dune build -p elpi log2 dune install elpi diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index f672ead807..c17ec502e7 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-09-17-V88" +# CACHEKEY: "bionic_coq-V2020-10-12-V89" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -43,7 +43,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ - BASE_ONLY_OPAM="elpi.1.11.0" + BASE_ONLY_OPAM="elpi.1.11.4" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0" diff --git a/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh b/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh new file mode 100644 index 0000000000..fb5947d218 --- /dev/null +++ b/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12449" ] || [ "$CI_BRANCH" = "minim-prop-toset" ]; then + + mtac2_CI_REF=janno/coq-12449 + mtac2_CI_GITURL=https://github.com/mtac2/mtac2 + +fi diff --git a/dev/ci/user-overlays/13088-gares-par-to-tactic.sh b/dev/ci/user-overlays/13088-gares-par-to-tactic.sh new file mode 100644 index 0000000000..4108a1aed1 --- /dev/null +++ b/dev/ci/user-overlays/13088-gares-par-to-tactic.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "13088" ] || [ "$CI_BRANCH" = "par-to-tactic" ]; then + + mtac2_CI_REF=par-to-tactic + mtac2_CI_GITURL=https://github.com/gares/Mtac2 + +fi diff --git a/dev/ci/user-overlays/13143-herbelin-master+drop-misleading-arg-hbox.sh b/dev/ci/user-overlays/13143-herbelin-master+drop-misleading-arg-hbox.sh new file mode 100644 index 0000000000..1b3121781b --- /dev/null +++ b/dev/ci/user-overlays/13143-herbelin-master+drop-misleading-arg-hbox.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "13143" ] || [ "$CI_BRANCH" = "master+drop-misleading-arg-hbox" ]; then + + aac_tactics_CI_REF=master+adapt-coq-pr13143-hbox-no-argument + aac_tactics_CI_GITURL=https://github.com/herbelin/aac-tactics + + equations_CI_REF=master+adapt-coq-pr13143-hbox-no-argument + equations_CI_GITURL=https://github.com/herbelin/Coq-Equations + +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 59c1623a2d..fb5d7cc244 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -10,6 +10,13 @@ git hook removed. If desired, automatic formatting can be achieved by calling the `fmt` target of the dune build system. +### Pp library + +- `Pp.h` does not take a `int` argument anymore (the argument was + not used). In general, where `h n` for `n` non zero was used, `hv n` + was instead intended. If cancelling the breaking role of cuts in the + box was intended, turn `h n c` into `h c`. + ## Changes between Coq 8.11 and Coq 8.12 ### Code formatting diff --git a/doc/changelog/02-specification-language/10331-minim-prop-toset.rst b/doc/changelog/02-specification-language/10331-minim-prop-toset.rst new file mode 100644 index 0000000000..6c442ca1aa --- /dev/null +++ b/doc/changelog/02-specification-language/10331-minim-prop-toset.rst @@ -0,0 +1,5 @@ +- **Changed:** Heuristics for universe minimization to :g:`Set`: also + use constraints ``Prop <= i`` (`#10331 + <https://github.com/coq/coq/pull/10331>`_, by Gaëtan Gilbert with + help from Maxime Dénès and Matthieu Sozeau, fixes `#12414 + <https://github.com/coq/coq/issues/12414>`_). diff --git a/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst b/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst new file mode 100644 index 0000000000..16fc91f911 --- /dev/null +++ b/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst @@ -0,0 +1,10 @@ +- **Changed:** + New model for ``only parsing`` and ``only printing`` notations with + support for at most one parsing-and-printing or only-parsing + notation per notation and scope, but an arbitrary number of + only-printing notations + (`#12950 <https://github.com/coq/coq/pull/12950>`_, + fixes `#4738 <https://github.com/coq/coq/issues/4738>`_ + and `#9682 <https://github.com/coq/coq/issues/9682>`_ + and part 2 of `#12908 <https://github.com/coq/coq/issues/12908>`_, + by Hugo Herbelin). diff --git a/doc/changelog/09-coqide/12874-show_proof_diffs.rst b/doc/changelog/09-coqide/12874-show_proof_diffs.rst new file mode 100644 index 0000000000..51bebad9be --- /dev/null +++ b/doc/changelog/09-coqide/12874-show_proof_diffs.rst @@ -0,0 +1,5 @@ +- **Added:** + Support showing diffs for :cmd:`Show Proof` in CoqIDE from the :n:`View` menu. + See :ref:`showing_proof_diffs`. + (`#12874 <https://github.com/coq/coq/pull/12874>`_, + by Jim Fehrle and Enrico Tassi) diff --git a/doc/sphinx/_static/diffs-show-proof.png b/doc/sphinx/_static/diffs-show-proof.png Binary files differnew file mode 100644 index 0000000000..62bd9cccd0 --- /dev/null +++ b/doc/sphinx/_static/diffs-show-proof.png diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index f90ebadb3a..f722ddda79 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -590,11 +590,11 @@ Requesting information constructed. Each hole is an existential variable, which appears as a question mark followed by an identifier. - Experimental: Specifying “Diffs” highlights the difference between the + Specifying “Diffs” highlights the difference between the current and previous proof step. By default, the command shows the output once with additions highlighted. Including “removed” shows the output twice: once showing removals and once showing additions. - It does not examine the :opt:`Diffs` option. See :ref:`showing_diffs`. + It does not examine the :opt:`Diffs` option. See :ref:`showing_proof_diffs`. .. cmdv:: Show Conjectures :name: Show Conjectures @@ -675,12 +675,9 @@ Requesting information Showing differences between proof steps --------------------------------------- - Coq can automatically highlight the differences between successive proof steps -and between values in some error messages. Also, as an experimental feature, -Coq can also highlight differences between proof steps shown in the :cmd:`Show Proof` -command, but only, for now, when using coqtop and Proof General. - +and between values in some error messages. Coq can also highlight differences +in the proof term. For example, the following screenshots of CoqIDE and coqtop show the application of the same :tacn:`intros` tactic. The tactic creates two new hypotheses, highlighted in green. The conclusion is entirely in pale green because although it’s changed, no tokens were added @@ -826,14 +823,37 @@ the split because it has not changed. .. image:: ../_static/diffs-coqide-multigoal.png :alt: coqide with Set Diffs on with multiple goals -This is how diffs may appear after applying a :tacn:`intro` tactic that results -in compacted hypotheses: +Diffs may appear like this after applying a :tacn:`intro` tactic that results +in a compacted hypotheses: .. .. image:: ../_static/diffs-coqide-compacted.png :alt: coqide with Set Diffs on with compacted hypotheses +.. _showing_proof_diffs: + +"Show Proof" differences +```````````````````````` + +To show differences in the proof term: + +- In coqtop and Proof General, use the :cmd:`Show Proof` `Diffs` command. + +- In CoqIDE, position the cursor on or just after a tactic to compare the proof term + after the tactic with the proof term before the tactic, then select + `View / Show Proof` from the menu or enter the associated key binding. + Differences will be shown applying the current `Show Diffs` setting + from the `View` menu. If the current setting is `Don't show diffs`, diffs + will not be shown. + + Output with the "added and removed" option looks like this: + + .. + + .. image:: ../_static/diffs-show-proof.png + :alt: coqide with Set Diffs on with compacted hypotheses + Controlling the effect of proof editing commands ------------------------------------------------ diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 5148fa84c9..d6db305300 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -57,15 +57,14 @@ to represent :g:`(and A B)`: Notations must be in double quotes, except when the abbreviation has the form of an ordinary applicative expression; see :ref:`Abbreviations`. The notation consists of *tokens* separated by -spaces. Alphanumeric strings (such as ``A`` and ``B``) are the *parameters* +spaces. Tokens which are identifiers (such as ``A``, ``x0'``, etc.) are the *parameters* of the notation. Each of them must occur at least once in the abbreviated term. The other elements of the string (such as ``/\``) are the *symbols*. -Substrings enclosed in single quotes are treated as literals. This is necessary -for substrings that would otherwise be interpreted as :n:`@ident`\s. Similarly, -every symbol of at least 3 characters and starting with a simple quote -must be quoted (then it starts by two single quotes). Here is an -example. +Identifiers enclosed in single quotes are treated as symbols and thus +lose their role of parameters. In the same vein, every symbol of at +least 3 characters and starting with a simple quote must be quoted +(then it starts with two single quotes). Here is an example. .. coqtop:: in @@ -82,7 +81,8 @@ associativity rules have to be given. The right-hand side of a notation is interpreted at the time the notation is given. In particular, disambiguation of constants, :ref:`implicit arguments <ImplicitArguments>` and other notations are resolved at the - time of the declaration of the notation. + time of the declaration of the notation. The right-hand side is + currently typed only at use time but this may change in the future. Precedences and associativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -299,12 +299,29 @@ Notations disappear when a section is closed. No typing of the denoted expression is performed at definition time. Type checking is done only at the time of use of the notation. -.. note:: Sometimes, a notation is expected only for the parser. To do - so, the option ``only parsing`` is allowed in the list of :n:`@syntax_modifier`\s - in :cmd:`Notation`. Conversely, the ``only printing`` :n:`@syntax_modifier` can be - used to declare that a notation should only be used for printing and - should not declare a parsing rule. In particular, such notations do - not modify the parser. +.. note:: + + The default for a notation is to be used both for parsing and + printing. It is possible to declare a notation only for parsing by + adding the option ``only parsing`` to the list of + :n:`@syntax_modifier`\s of :cmd:`Notation`. Symmetrically, the + ``only printing`` :n:`@syntax_modifier` can be used to declare that + a notation should only be used for printing. + + If a notation to be used both for parsing and printing is + overriden, both the parsing and printing are invalided, even if the + overriding rule is only parsing. + + If a given notation string occurs only in ``only printing`` rules, + the parser is not modified at all. + + To a given notation string and scope can be attached at most one + notation with both parsing and printing or with only + parsing. Contrastingly, an arbitrary number of ``only printing`` + notations differing in their right-hand sides but only a unique + right-hand side can be attached to a given string and + scope. Obviously, expressions printed by means of such extra + printing rules will not be reparsed to the same form. The Infix command ~~~~~~~~~~~~~~~~~~ diff --git a/engine/termops.ml b/engine/termops.ml index 0923ab6f4b..467b269e37 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -233,13 +233,13 @@ let pr_evar_universe_context ctx = if UState.is_empty ctx then mt () else (str"UNIVERSES:"++brk(0,1)++ - h 0 (Univ.pr_universe_context_set prl (UState.context_set ctx)) ++ fnl () ++ + h (Univ.pr_universe_context_set prl (UState.context_set ctx)) ++ fnl () ++ str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ - h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++ + h (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ - h 0 (UnivSubst.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++ + h (UnivSubst.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++ str "WEAK CONSTRAINTS:"++brk(0,1)++ - h 0 (UState.pr_weak prl ctx) ++ fnl ()) + h (UState.pr_weak prl ctx) ++ fnl ()) let print_env_short env sigma = let print_constr = print_kconstr in @@ -316,14 +316,14 @@ let pr_evar_list env sigma l = | Some ev' -> str " (aliased to " ++ Evar.print ev' ++ str ")" in let pr (ev, evi) = - h 0 (Evar.print ev ++ + h (Evar.print ev ++ str "==" ++ pr_evar_info env sigma evi ++ pr_alias ev ++ (if evi.evar_body == Evar_empty then str " {" ++ pr_existential_key sigma ev ++ str "}" else mt ())) in - h 0 (prlist_with_sep fnl pr l) + hv 0 (prlist_with_sep fnl pr l) let to_list d = let open Evd in diff --git a/engine/uState.ml b/engine/uState.ml index 8d1584cd95..9557111cfd 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -286,6 +286,10 @@ let process_universe_constraints ctx cstrs = if not (drop_weak_constraints ()) then weak := UPairSet.add (l,r) !weak; local | UEq (l, r) -> equalize_universes l r local in + let unify_universes cst local = + if not (UGraph.type_in_type univs) then unify_universes cst local + else try unify_universes cst local with UniverseInconsistency _ -> local + in let local = UnivProblem.Set.fold unify_universes cstrs Constraint.empty in @@ -671,7 +675,7 @@ let subst_univs_context_with_def def usubst (ctx, cst) = (LSet.diff ctx def, UnivSubst.subst_univs_constraints usubst cst) let is_trivial_leq (l,d,r) = - Level.is_prop l && (d == Le || (d == Lt && Level.is_set r)) + Level.is_prop l && (d == Le || d == Lt) && Level.is_set r (* Prop < i <-> Set+1 <= i <-> Set < i *) let translate_cstr (l,d,r as cstr) = diff --git a/engine/univMinim.ml b/engine/univMinim.ml index 1c7e716fc2..4ed6e97526 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -292,22 +292,29 @@ let is_bound l lbound = match lbound with | UGraph.Bound.Prop -> Level.is_prop l | UGraph.Bound.Set -> Level.is_set l +(* if [is_minimal u] then constraints [u <= v] may be dropped and get + used only for set_minimization. *) +let is_minimal ~lbound u = + Level.is_sprop u || Level.is_prop u || is_bound u lbound + (* TODO check is_small/sprop *) let normalize_context_set ~lbound g ctx us algs weak = let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in (* Keep the Prop/Set <= i constraints separate for minimization *) let smallles, csts = - Constraint.partition (fun (l,d,r) -> d == Le && (is_bound l lbound || Level.is_sprop l)) csts + Constraint.partition (fun (l,d,r) -> d == Le && is_minimal ~lbound l) csts in let smallles = if get_set_minimization () then Constraint.filter (fun (l,d,r) -> LMap.mem r us && not (Level.is_sprop l)) smallles else Constraint.empty in + let smallles = Constraint.map (fun (_,_,r) -> Level.set, Le, r) smallles in let csts, partition = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) + let g = UGraph.initial_universes_with g in let g = LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g) - ctx UGraph.initial_universes + ctx g in let add_soft u g = if not (Level.is_small u || LSet.mem u ctx) diff --git a/ide/.merlin.in b/ide/.merlin.in index b8d7953833..50816ae3f5 100644 --- a/ide/.merlin.in +++ b/ide/.merlin.in @@ -1,8 +1,10 @@ PKG unix laglgtk3 lablgtk3-sourceview3 -S utils -B utils -S protocol -B protocol +S coqide/utils +B coqide/utils +S coqide/protocol +B coqide/protocol +S coqide/ +B coqide/ REC diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml index 038c8b91a8..1167b8199e 100644 --- a/ide/coqide/coq.ml +++ b/ide/coqide/coq.ml @@ -512,6 +512,7 @@ let hints x = eval_call (Xmlprotocol.hints x) let search flags = eval_call (Xmlprotocol.search flags) let init x = eval_call (Xmlprotocol.init x) let stop_worker x = eval_call (Xmlprotocol.stop_worker x) +let proof_diff x = eval_call (Xmlprotocol.proof_diff x) let break_coqtop coqtop workers = if coqtop.status = Busy then @@ -579,6 +580,9 @@ struct let set (type a) (opt : a t) (v : a) = Hashtbl.replace current_state (opt_name opt) (opt_data opt v) + let get (type a) (opt : a t) = + Hashtbl.find current_state (opt_name opt) + let reset () = let init_descr d = List.iter (fun o -> set o d.init) d.opts in List.iter init_descr bool_items; diff --git a/ide/coqide/coq.mli b/ide/coqide/coq.mli index 82df36c91c..aaaf14e4d0 100644 --- a/ide/coqide/coq.mli +++ b/ide/coqide/coq.mli @@ -127,6 +127,7 @@ val hints : Interface.hints_sty -> Interface.hints_rty query val mkcases : Interface.mkcases_sty -> Interface.mkcases_rty query val search : Interface.search_sty -> Interface.search_rty query val init : Interface.init_sty -> Interface.init_rty query +val proof_diff : Interface.proof_diff_sty -> Interface.proof_diff_rty query val stop_worker: Interface.stop_worker_sty-> Interface.stop_worker_rty query @@ -144,6 +145,10 @@ sig val set : 'a t -> 'a -> unit + val get : 'a t -> Interface.option_value + + val diff : string t + val printing_unfocused: unit -> bool (** [enforce] transmits to coq the current option values. diff --git a/ide/coqide/coqOps.ml b/ide/coqide/coqOps.ml index 29ea3ce9ea..97076745a3 100644 --- a/ide/coqide/coqOps.ml +++ b/ide/coqide/coqOps.ml @@ -142,6 +142,7 @@ object method handle_reset_initial : unit task method raw_coq_query : route_id:int -> next:(query_rty value -> unit task) -> string -> unit task + method proof_diff : GText.mark -> next:(Pp.t value -> unit task) -> unit task method show_goals : unit task method backtrack_last_phrase : unit task method initialize : unit task @@ -361,6 +362,27 @@ object(self) let query = Coq.query (route_id,(phrase,sid)) in Coq.bind (Coq.seq action query) next + method proof_diff where ~next : unit Coq.task = + (* todo: would be nice to ignore comments, too *) + let rec back iter = + if iter#is_start then iter + else + let c = iter#char in + if Glib.Unichar.isspace c || c = 0 then back (iter#backward_char) + else if c = int_of_char '.' then iter#backward_char + else iter in + + let where = back (buffer#get_iter_at_mark where) in + let until _ start stop = + (buffer#get_iter_at_mark stop)#compare where >= 0 && + (buffer#get_iter_at_mark start)#compare where <= 0 in + let state_id = fst @@ self#find_id until in + let diff_opt = Interface.(match Coq.PrintOpt.(get diff) with + | StringValue diffs -> diffs + | _ -> "off") in + let proof_diff = Coq.proof_diff (diff_opt, state_id) in + Coq.bind proof_diff next + method private still_valid { edit_id = id } = try ignore(Doc.find_id document (fun _ { edit_id = id1 } -> id = id1)); true with Not_found -> false diff --git a/ide/coqide/coqOps.mli b/ide/coqide/coqOps.mli index 3a4678ae9c..84911a6aa8 100644 --- a/ide/coqide/coqOps.mli +++ b/ide/coqide/coqOps.mli @@ -20,6 +20,7 @@ object method handle_reset_initial : unit task method raw_coq_query : route_id:int -> next:(query_rty value -> unit task) -> string -> unit task + method proof_diff : GText.mark -> next:(Pp.t value -> unit task) -> unit task method show_goals : unit task method backtrack_last_phrase : unit task method initialize : unit task @@ -30,7 +31,6 @@ object method get_errors : (int * string) list method get_slaves_status : int * int * string CString.Map.t - method handle_failure : handle_exn_rty -> unit task method destroy : unit -> unit diff --git a/ide/coqide/coqide.ml b/ide/coqide/coqide.ml index b66da11e7b..f9e6e74372 100644 --- a/ide/coqide/coqide.ml +++ b/ide/coqide/coqide.ml @@ -747,6 +747,24 @@ let coq_icon () = let dir = List.find chk (Minilib.coqide_data_dirs ()) in Filename.concat dir name +let show_proof_diff where sn = + sn.messages#default_route#clear; + Coq.try_grab sn.coqtop (sn.coqops#proof_diff where + ~next:(function + | Interface.Fail (_, _, err) -> + let err = if (Pp.string_of_ppcmds err) <> "No proofs to diff." then err else + Pp.str "Put the cursor over proven lines for \"Show Proof\" diffs" + in + let err = Ideutils.validate err in + sn.messages#default_route#add err; + Coq.return () + | Interface.Good diff -> + sn.messages#default_route#add diff; + Coq.return ())) + ignore + +let show_proof_diffs _ = cb_on_current_term (show_proof_diff `INSERT) () + let about _ = let dialog = GWindow.about_dialog () in let _ = dialog#connect#response ~callback:(fun _ -> dialog#destroy ()) in @@ -1103,6 +1121,8 @@ let build_ui () = radio "Set diff" 1 ~label:"Show diffs: only _added"; radio "Set removed diff" 2 ~label:"Show diffs: added and _removed"; ]; + item "Show Proof Diffs" ~label:"_Show Proof (with diffs, if set)" ~accel:(modifier_for_display#get ^ "S") + ~callback:MiscMenu.show_proof_diffs; ]; toggle_items view_menu Coq.PrintOpt.bool_items; @@ -1352,6 +1372,11 @@ let main files = this default coqtop path *) let read_coqide_args argv = + let set_debug () = + Minilib.debug := true; + Flags.debug := true; + Exninfo.record_backtrace true + in let rec filter_coqtop coqtop project_files bindings_files out = function |"-unicode-bindings" :: sfilenames :: args -> let filenames = Str.split (Str.regexp ",") sfilenames in @@ -1371,10 +1396,12 @@ let read_coqide_args argv = |"-coqtop" :: [] -> output_string stderr "Error: missing argument after -coqtop"; exit 1 |"-debug"::args -> - Minilib.debug := true; - Flags.debug := true; - Exninfo.record_backtrace true; + set_debug (); filter_coqtop coqtop project_files bindings_files ("-debug"::out) args + |"-xml-debug"::args -> + set_debug (); + Flags.xml_debug := true; + filter_coqtop coqtop project_files bindings_files ("-xml-debug"::out) args |"-coqtop-flags" :: flags :: args-> Coq.ideslave_coqtop_flags := Some flags; filter_coqtop coqtop project_files bindings_files out args diff --git a/ide/coqide/coqide_ui.ml b/ide/coqide/coqide_ui.ml index e9ff1bbba1..6540fc6fca 100644 --- a/ide/coqide/coqide_ui.ml +++ b/ide/coqide/coqide_ui.ml @@ -89,6 +89,7 @@ let init () = \n <menuitem action='Unset diff' />\ \n <menuitem action='Set diff' />\ \n <menuitem action='Set removed diff' />\ +\n <menuitem action='Show Proof Diffs' />\ \n </menu>\ \n <menu action='Navigation'>\ \n <menuitem action='Forward' />\ diff --git a/ide/coqide/fake_ide.ml b/ide/coqide/fake_ide.ml index e1736a5fe0..034f5b4e2a 100644 --- a/ide/coqide/fake_ide.ml +++ b/ide/coqide/fake_ide.ml @@ -136,7 +136,7 @@ module Parser = struct (* {{{ *) match g with | Item (s,_) -> Printf.sprintf "%s" (clean s) | Opt g -> Printf.sprintf "[%s]" (print g) - | Alt gs -> Printf.sprintf "( %s )" (String.concat " | " (List.map print gs)) + | Alt gs -> Printf.sprintf "( %s )" (String.concat "\n| " (List.map print gs)) | Seq gs -> String.concat " " (List.map print gs) let rec print_toklist = function @@ -253,6 +253,9 @@ let eval_print l coq = after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq) | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] -> eval_call (query (0,(phrase,tip_id()))) coq + | [ Tok(_,"PDIFF"); Tok(_,id) ] -> + let to_id, _ = get_id id in + eval_call (proof_diff ("on",to_id)) coq | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] -> let to_id, _ = get_id id in eval_call (query (0,(phrase, to_id))) coq @@ -282,6 +285,7 @@ let grammar = ; Seq [Item (eat_rex "FAILADD"); Item eat_phrase] ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id] ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase] + ; Seq [Item (eat_rex "PDIFF"); Item eat_id ] ; Seq [Item (eat_rex "WAIT")] ; Seq [Item (eat_rex "JOIN")] ; Seq [Item (eat_rex "GOALS")] @@ -295,12 +299,11 @@ let grammar = let read_command inc = Parser.parse grammar inc let usage () = - error (Printf.sprintf - "A fake coqide process talking to a coqtop -toploop coqidetop.\n\ - Usage: %s (file|-) [<coqtop>]\n\ - Input syntax is the following:\n%s\n" - (Filename.basename Sys.argv.(0)) - (Parser.print grammar)) + prerr_endline (Printf.sprintf "Usage: %s ( file | - ) [ \"<coqtop arguments>\" ]\n\ + Input syntax is:\n%s\n" + (Filename.basename Sys.argv.(0)) + (Parser.print grammar)); + exit 1 module Coqide = Spawn.Sync () @@ -308,14 +311,15 @@ let main = if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe (Sys.Signal_handle (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1)); - let def_args = ["--xml_format=Ppcmds"] in let idetop_name = System.get_toplevel_path "coqidetop" in - let coqtop_args, input_file = match Sys.argv with - | [| _; f |] -> Array.of_list def_args, f - | [| _; f; ct |] -> - let ct = Str.split (Str.regexp " ") ct in - Array.of_list (def_args @ ct), f + let input_file, args = match Sys.argv with + | [| _; f |] -> f, [] + | [| _; f; args |] -> + let args = Str.split (Str.regexp " ") args in + f, args | _ -> usage () in + let def_coqtop_args = ["--xml_format=Ppcmds"] in + let coqtop_args = Array.of_list(def_coqtop_args @ args) in let inc = if input_file = "-" then stdin else open_in input_file in prerr_endline ("Running: "^idetop_name^" "^ (String.concat " " (Array.to_list coqtop_args))); diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index ad21f663e4..297dc3a706 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -367,6 +367,17 @@ let export_option_state s = { Interface.opt_value = export_option_value s.Goptions.opt_value; } +exception NotSupported of string + +let proof_diff (diff_opt, sid) = + let diff_opt = Proof_diffs.string_to_diffs diff_opt in + let doc = get_doc () in + match Stm.get_proof ~doc sid with + | None -> CErrors.user_err (Pp.str "No proofs to diff.") + | Some proof -> + let old = Stm.get_prev_proof ~doc sid in + Proof_diffs.diff_proofs ~diff_opt ?old proof + let get_options () = let table = Goptions.get_tables () in let fold key state accu = (key, export_option_state state) :: accu in @@ -455,6 +466,7 @@ let eval_call c = Interface.hints = interruptible hints; Interface.status = interruptible status; Interface.search = interruptible search; + Interface.proof_diff = interruptible proof_diff; Interface.get_options = interruptible get_options; Interface.set_options = interruptible set_options; Interface.mkcases = interruptible idetop_make_cases; @@ -479,6 +491,8 @@ let print_xml = let m = Mutex.create () in fun oc xml -> Mutex.lock m; + if !Flags.xml_debug then + Printf.printf "SENT --> %s\n%!" (Xml_printer.to_string_fmt xml); try Control.protect_sigalrm (Xml_printer.print oc) xml; Mutex.unlock m with e -> let e = Exninfo.capture e in Mutex.unlock m; Exninfo.iraise e @@ -507,7 +521,7 @@ let loop run_mode ~opts:_ state = set_doc state.doc; init_signal_handler (); catch_break := false; - let in_ch, out_ch = Spawned.get_channels () in + let in_ch, out_ch = Spawned.get_channels () in let xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in let in_lb = Lexing.from_function (fun s len -> CThread.thread_friendly_read in_ch s ~off:0 ~len) in @@ -518,7 +532,8 @@ let loop run_mode ~opts:_ state = while not !quit do try let xml_query = Xml_parser.parse xml_ic in -(* pr_with_pid (Xml_printer.to_string_fmt xml_query); *) + if !Flags.xml_debug then + pr_with_pid (Xml_printer.to_string_fmt xml_query); let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in let () = pr_debug_call q in let r = eval_call q in diff --git a/ide/coqide/protocol/interface.ml b/ide/coqide/protocol/interface.ml index 646012dcaa..86a81446e8 100644 --- a/ide/coqide/protocol/interface.ml +++ b/ide/coqide/protocol/interface.ml @@ -187,6 +187,10 @@ type status_rty = status type search_sty = search_flags type search_rty = string coq_object list +(** Diffs between the proof term at a given stateid and the previous one *) +type proof_diff_sty = string * Stateid.t +type proof_diff_rty = Pp.t + (** Retrieve the list of options of the current toplevel *) type get_options_sty = unit type get_options_rty = (option_name * option_state) list @@ -252,6 +256,7 @@ type handler = { stop_worker : stop_worker_sty -> stop_worker_rty; print_ast : print_ast_sty -> print_ast_rty; annotate : annotate_sty -> annotate_rty; + proof_diff : proof_diff_sty -> proof_diff_rty; handle_exn : handle_exn_sty -> handle_exn_rty; init : init_sty -> init_rty; quit : quit_sty -> quit_rty; diff --git a/ide/coqide/protocol/serialize.ml b/ide/coqide/protocol/serialize.ml index bdbec5b30f..6a0a3d7f5d 100644 --- a/ide/coqide/protocol/serialize.ml +++ b/ide/coqide/protocol/serialize.ml @@ -35,6 +35,11 @@ let singleton = function | l -> raise (Marshal_error ("singleton",PCData ("list of length " ^ string_of_int (List.length l)))) +let empty = function + | [] -> () + | l -> raise (Marshal_error + ("empty",PCData ("list of length " ^ string_of_int (List.length l)))) + let raw_string = function | [] -> "" | [PCData s] -> s diff --git a/ide/coqide/protocol/serialize.mli b/ide/coqide/protocol/serialize.mli index 5d88defe55..9d09b81d1e 100644 --- a/ide/coqide/protocol/serialize.mli +++ b/ide/coqide/protocol/serialize.mli @@ -16,6 +16,7 @@ val massoc: string -> (string * string) list -> string val constructor: string -> string -> xml list -> xml val do_match: string -> (string -> xml list -> 'b) -> xml -> 'b val singleton: 'a list -> 'a +val empty: 'a list -> unit val raw_string: xml list -> string val of_unit: unit -> xml val to_unit: xml -> unit diff --git a/ide/coqide/protocol/xmlprotocol.ml b/ide/coqide/protocol/xmlprotocol.ml index 6cb0cec008..6a33ff8abc 100644 --- a/ide/coqide/protocol/xmlprotocol.ml +++ b/ide/coqide/protocol/xmlprotocol.ml @@ -12,7 +12,7 @@ (** WARNING: TO BE UPDATED WHEN MODIFIED! *) -let protocol_version = "20170413" +let protocol_version = "20200911" type msg_format = Richpp of int | Ppcmds let msg_format = ref (Richpp 72) @@ -43,7 +43,7 @@ let to_search_cst = do_match "search_cst" (fun s args -> match s with | "type_pattern" -> Type_Pattern (to_string (singleton args)) | "subtype_pattern" -> SubType_Pattern (to_string (singleton args)) | "in_module" -> In_Module (to_list to_string (singleton args)) - | "include_blacklist" -> Include_Blacklist + | "include_blacklist" -> empty args; Include_Blacklist | x -> raise (Marshal_error("search",PCData x))) let of_coq_object f ans = @@ -103,14 +103,14 @@ let to_routeid = function let of_routeid i = Element ("route_id",["val",string_of_int i],[]) let of_box (ppb : Pp.block_type) = let open Pp in match ppb with - | Pp_hbox i -> constructor "ppbox" "hbox" [of_int i] + | Pp_hbox -> constructor "ppbox" "hbox" [] | Pp_vbox i -> constructor "ppbox" "vbox" [of_int i] | Pp_hvbox i -> constructor "ppbox" "hvbox" [of_int i] | Pp_hovbox i -> constructor "ppbox" "hovbox" [of_int i] let to_box = let open Pp in do_match "ppbox" (fun s args -> match s with - | "hbox" -> Pp_hbox (to_int (singleton args)) + | "hbox" -> empty args; Pp_hbox | "vbox" -> Pp_vbox (to_int (singleton args)) | "hvbox" -> Pp_hvbox (to_int (singleton args)) | "hovbox" -> Pp_hovbox (to_int (singleton args)) @@ -132,7 +132,7 @@ let rec of_pp (pp : Pp.t) = let open Pp in match Pp.repr pp with let rec to_pp xpp = let open Pp in Pp.unrepr @@ do_match "ppdoc" (fun s args -> match s with - | "empty" -> Ppcmd_empty + | "empty" -> empty args; Ppcmd_empty | "string" -> Ppcmd_string (to_string (singleton args)) | "glue" -> Ppcmd_glue (to_list to_pp (singleton args)) | "box" -> let (bt,s) = to_pair to_box to_pp (singleton args) in @@ -278,6 +278,7 @@ module ReifType : sig val state_id_t : state_id val_t val route_id_t : route_id val_t val search_cst_t : search_constraint val_t + val pp_t : Pp.t val_t val of_value_type : 'a val_t -> 'a -> xml val to_value_type : 'a val_t -> xml -> 'a @@ -314,6 +315,7 @@ end = struct | State_id : state_id val_t | Route_id : route_id val_t | Search_cst : search_constraint val_t + | Pp : Pp.t val_t type value_type = Value_type : 'a val_t -> value_type @@ -340,6 +342,7 @@ end = struct let state_id_t = State_id let route_id_t = Route_id let search_cst_t = Search_cst + let pp_t = Pp let of_value_type (ty : 'a val_t) : 'a -> xml = let rec convert : type a. a val_t -> a -> xml = function @@ -362,6 +365,7 @@ end = struct | State_id -> of_stateid | Route_id -> of_routeid | Search_cst -> of_search_cst + | Pp -> of_pp in convert ty @@ -386,6 +390,7 @@ end = struct | State_id -> to_stateid | Route_id -> to_routeid | Search_cst -> to_search_cst + | Pp -> to_pp in convert ty @@ -443,6 +448,8 @@ end = struct | In_Module s -> "In_Module " ^ String.concat "." s | Include_Blacklist -> "Include_Blacklist" + let pr_pp = Pp.string_of_ppcmds + let rec print : type a. a val_t -> a -> string = function | Unit -> pr_unit | Bool -> pr_bool @@ -463,6 +470,7 @@ end = struct | Union (t1,t2) -> (pr_union (print t1) (print t2)) | State_id -> pr_state_id | Route_id -> pr_int + | Pp -> pr_pp (* This is to break if a rename/refactoring makes the strings below outdated *) type 'a exists = bool @@ -489,6 +497,7 @@ end = struct Printf.sprintf "((%s, %s) CSig.union)" (print_val_t t1) (print_val_t t2) | State_id -> assert(true : Stateid.t exists); "Stateid.t" | Route_id -> assert(true : route_id exists); "route_id" + | Pp -> assert(true : Pp.t exists); "Pp.t" let print_type = function Value_type ty -> print_val_t ty @@ -507,6 +516,8 @@ end = struct (pr_xml (of_pair of_bool of_int (false,3))); Printf.printf "%s:\n\n%s\n\n" (print_val_t (Union (Bool,Int))) (pr_xml (of_union of_bool of_int (Inl false))); + Printf.printf "%s:\n\n%s\n\n" (print_val_t Pp) + (pr_xml (of_pp Pp.(hv 3 (str "foo" ++ spc () ++ str "bar") ))); print_endline ("All other types are records represented by a node named like the OCaml\n"^ "type which contains a flattened n-tuple. We provide one example.\n"); Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state) @@ -538,6 +549,7 @@ let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t let stop_worker_sty_t : stop_worker_sty val_t = string_t let print_ast_sty_t : print_ast_sty val_t = state_id_t let annotate_sty_t : annotate_sty val_t = string_t +let proof_diff_sty_t : proof_diff_sty val_t = pair_t string_t state_id_t let add_rty_t : add_rty val_t = pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t) @@ -563,6 +575,7 @@ let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string let stop_worker_rty_t : stop_worker_rty val_t = unit_t let print_ast_rty_t : print_ast_rty val_t = xml_t let annotate_rty_t : annotate_rty val_t = xml_t +let proof_diff_rty_t : proof_diff_rty val_t = pp_t let ($) x = erase x let calls = [| @@ -585,6 +598,7 @@ let calls = [| "StopWorker", ($)stop_worker_sty_t, ($)stop_worker_rty_t; "PrintAst", ($)print_ast_sty_t, ($)print_ast_rty_t; "Annotate", ($)annotate_sty_t, ($)annotate_rty_t; + "PDiff", ($)proof_diff_sty_t, ($)proof_diff_rty_t; |] type 'a call = @@ -609,7 +623,9 @@ type 'a call = | Interp : interp_sty -> interp_rty call | PrintAst : print_ast_sty -> print_ast_rty call | Annotate : annotate_sty -> annotate_rty call + | PDiff : proof_diff_sty -> proof_diff_rty call +(* the order of the entries must match the order in "calls" above *) let id_of_call : type a. a call -> int = function | Add _ -> 0 | Edit_at _ -> 1 @@ -630,6 +646,7 @@ let id_of_call : type a. a call -> int = function | StopWorker _ -> 16 | PrintAst _ -> 17 | Annotate _ -> 18 + | PDiff _ -> 19 let str_of_call c = pi1 calls.(id_of_call c) @@ -652,8 +669,9 @@ let init x : init_rty call = Init x let wait x : wait_rty call = Wait x let interp x : interp_rty call = Interp x let stop_worker x : stop_worker_rty call = StopWorker x -let print_ast x : print_ast_rty call = PrintAst x -let annotate x : annotate_rty call = Annotate x +let print_ast x : print_ast_rty call = PrintAst x +let annotate x : annotate_rty call = Annotate x +let proof_diff x : proof_diff_rty call = PDiff x let abstract_eval_call : type a. _ -> a call -> a value = fun handler c -> let mkGood : type a. a -> a value = fun x -> Good x in @@ -678,6 +696,7 @@ let abstract_eval_call : type a. _ -> a call -> a value = fun handler c -> | StopWorker x -> mkGood (handler.stop_worker x) | PrintAst x -> mkGood (handler.print_ast x) | Annotate x -> mkGood (handler.annotate x) + | PDiff x -> mkGood (handler.proof_diff x) with any -> let any = Exninfo.capture any in Fail (handler.handle_exn any) @@ -703,6 +722,7 @@ let of_answer : type a. a call -> a value -> xml = function | StopWorker _ -> of_value (of_value_type stop_worker_rty_t) | PrintAst _ -> of_value (of_value_type print_ast_rty_t ) | Annotate _ -> of_value (of_value_type annotate_rty_t ) + | PDiff _ -> of_value (of_value_type proof_diff_rty_t ) let of_answer msg_fmt = msg_format := msg_fmt; of_answer @@ -727,6 +747,7 @@ let to_answer : type a. a call -> xml -> a value = function | StopWorker _ -> to_value (to_value_type stop_worker_rty_t) | PrintAst _ -> to_value (to_value_type print_ast_rty_t ) | Annotate _ -> to_value (to_value_type annotate_rty_t ) + | PDiff _ -> to_value (to_value_type proof_diff_rty_t ) let of_call : type a. a call -> xml = fun q -> let mkCall x = constructor "call" (str_of_call q) [x] in @@ -750,6 +771,7 @@ let of_call : type a. a call -> xml = fun q -> | StopWorker x -> mkCall (of_value_type stop_worker_sty_t x) | PrintAst x -> mkCall (of_value_type print_ast_sty_t x) | Annotate x -> mkCall (of_value_type annotate_sty_t x) + | PDiff x -> mkCall (of_value_type proof_diff_sty_t x) let to_call : xml -> unknown_call = do_match "call" (fun s a -> @@ -774,6 +796,7 @@ let to_call : xml -> unknown_call = | "StopWorker" -> Unknown (StopWorker (mkCallArg stop_worker_sty_t a)) | "PrintAst" -> Unknown (PrintAst (mkCallArg print_ast_sty_t a)) | "Annotate" -> Unknown (Annotate (mkCallArg annotate_sty_t a)) + | "PDiff" -> Unknown (PDiff (mkCallArg proof_diff_sty_t a)) | x -> raise (Marshal_error("call",PCData x))) (** Debug printing *) @@ -805,6 +828,7 @@ let pr_full_value : type a. a call -> a value -> string = fun call value -> matc | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) value | PrintAst _ -> pr_value_gen (print print_ast_rty_t ) value | Annotate _ -> pr_value_gen (print annotate_rty_t ) value + | PDiff _ -> pr_value_gen (print proof_diff_rty_t ) value let pr_call : type a. a call -> string = fun call -> let return what x = str_of_call call ^ " " ^ print what x in match call with @@ -827,6 +851,7 @@ let pr_call : type a. a call -> string = fun call -> | StopWorker x -> return stop_worker_sty_t x | PrintAst x -> return print_ast_sty_t x | Annotate x -> return annotate_sty_t x + | PDiff x -> return proof_diff_sty_t x let document to_string_fmt = Printf.printf "=== Available calls ===\n\n"; @@ -858,11 +883,11 @@ let of_message_level = function | Error -> Serialize.constructor "message_level" "error" [] let to_message_level = Serialize.do_match "message_level" (fun s args -> match s with - | "debug" -> Debug - | "info" -> Info - | "notice" -> Notice - | "warning" -> Warning - | "error" -> Error + | "debug" -> empty args; Debug + | "info" -> empty args; Info + | "notice" -> empty args; Notice + | "warning" -> empty args; Warning + | "error" -> empty args; Error | x -> raise Serialize.(Marshal_error("error level",PCData x))) let of_message lvl loc msg = diff --git a/ide/coqide/protocol/xmlprotocol.mli b/ide/coqide/protocol/xmlprotocol.mli index 44584d44d7..4dc05c18a9 100644 --- a/ide/coqide/protocol/xmlprotocol.mli +++ b/ide/coqide/protocol/xmlprotocol.mli @@ -37,6 +37,7 @@ val wait : wait_sty -> wait_rty call val interp : interp_sty -> interp_rty call val print_ast : print_ast_sty -> print_ast_rty call val annotate : annotate_sty -> annotate_rty call +val proof_diff : proof_diff_sty -> proof_diff_rty call val abstract_eval_call : handler -> 'a call -> 'a value diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 43fef8685d..167ea3ecdf 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -551,7 +551,7 @@ and extern_notation_pattern allscopes vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> try - if is_inactive_rule keyrule then raise No_match; + if is_inactive_rule keyrule || is_printing_inactive_rule keyrule pat then raise No_match; let loc = t.loc in match DAst.get t with | PatCstr (cstr,args,na) -> @@ -568,7 +568,7 @@ let rec extern_notation_ind_pattern allscopes vars ind args = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> try - if is_inactive_rule keyrule then raise No_match; + if is_inactive_rule keyrule || is_printing_inactive_rule keyrule pat then raise No_match; apply_notation_to_pattern (GlobRef.IndRef ind) (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule with @@ -1238,7 +1238,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = | (keyrule,pat,n as _rule)::rules -> let loc = Glob_ops.loc_of_glob_constr t in try - if is_inactive_rule keyrule then raise No_match; + if is_inactive_rule keyrule || is_printing_inactive_rule keyrule pat then raise No_match; let f,args = match DAst.get t with | GApp (f,args) -> f,args diff --git a/interp/notation.ml b/interp/notation.ml index 7e90e15b72..d57c4f3abf 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -58,6 +58,31 @@ let notation_with_optional_scope_eq inscope1 inscope2 = match (inscope1,inscope2 let notation_eq (from1,ntn1) (from2,ntn2) = notation_entry_eq from1 from2 && String.equal ntn1 ntn2 +let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 + +let notation_binder_source_eq s1 s2 = match s1, s2 with +| NtnParsedAsIdent, NtnParsedAsIdent -> true +| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 +| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2 +| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false + +let ntpe_eq t1 t2 = match t1, t2 with +| NtnTypeConstr, NtnTypeConstr -> true +| NtnTypeBinder s1, NtnTypeBinder s2 -> notation_binder_source_eq s1 s2 +| NtnTypeConstrList, NtnTypeConstrList -> true +| NtnTypeBinderList, NtnTypeBinderList -> true +| (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false + +let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) = + notation_entry_level_eq entry1 entry2 && + pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 && + ntpe_eq tp1 tp2 + +let interpretation_eq (vars1, t1 as x1) (vars2, t2 as x2) = + x1 == x2 || + List.equal var_attributes_eq vars1 vars2 && + Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2 + let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntry -> mt () | InCustomEntry s -> str " in custom " ++ str s module NotationOrd = @@ -90,8 +115,21 @@ type notation_data = { not_deprecation : Deprecation.t option; } +type activation = bool + +type extra_printing_notation_data = + (activation * notation_data) list + +type parsing_notation_data = + | NoParsingData + | OnlyParsingData of activation * notation_data + | ParsingAndPrintingData of + activation (* for parsing*) * + activation (* for printing *) * + notation_data (* common data for both *) + type scope = { - notations: notation_data NotationMap.t; + notations: (parsing_notation_data * extra_printing_notation_data) NotationMap.t; delimiters: delimiters option } @@ -300,10 +338,19 @@ type notation_applicative_status = type notation_rule = interp_rule * interpretation * notation_applicative_status +let notation_rule_eq (rule1,pat1,s1 as x1) (rule2,pat2,s2 as x2) = + x1 == x2 || (rule1 = rule2 && interpretation_eq pat1 pat2 && s1 = s2) + let keymap_add key interp map = let old = try KeyMap.find key map with Not_found -> [] in + (* In case of re-import, no need to keep the previous copy *) + let old = try List.remove_first (notation_rule_eq interp) old with Not_found -> old in KeyMap.add key (interp :: old) map +let keymap_remove key interp map = + let old = try KeyMap.find key map with Not_found -> [] in + KeyMap.add key (List.remove_first (notation_rule_eq interp) old) map + let keymap_find key map = try KeyMap.find key map with Not_found -> [] @@ -1225,40 +1272,90 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function (* The mapping between notations and their interpretation *) +let pr_optional_scope = function + | LastLonelyNotation -> mt () + | NotationInScope scope -> spc () ++ strbrk "in scope" ++ spc () ++ str scope + let warn_notation_overridden = CWarnings.create ~name:"notation-overridden" ~category:"parsing" - (fun (ntn,which_scope) -> + (fun (scope,ntn) -> str "Notation" ++ spc () ++ pr_notation ntn ++ spc () - ++ strbrk "was already used" ++ which_scope ++ str ".") + ++ strbrk "was already used" ++ pr_optional_scope scope ++ str ".") -let declare_notation_interpretation ntn scopt pat df ~onlyprint deprecation = - let scope = match scopt with Some s -> s | None -> default_scope in - let sc = find_scope scope in - if not onlyprint then begin - let () = - if NotationMap.mem ntn sc.notations then - let which_scope = match scopt with - | None -> mt () - | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in - warn_notation_overridden (ntn,which_scope) - in - let notdata = { - not_interp = pat; - not_location = df; - not_deprecation = deprecation; - } in - let sc = { sc with notations = NotationMap.add ntn notdata sc.notations } in - scope_map := String.Map.add scope sc !scope_map - end; - begin match scopt with - | None -> scope_stack := LonelyNotationItem ntn :: !scope_stack - | Some _ -> () - end +let warn_deprecation_overridden = + CWarnings.create ~name:"notation-overridden" ~category:"parsing" + (fun ((scope,ntn),old,now) -> + match old, now with + | None, None -> assert false + | None, Some _ -> + (str "Notation" ++ spc () ++ pr_notation ntn ++ pr_optional_scope scope ++ spc () + ++ strbrk "is now marked as deprecated" ++ str ".") + | Some _, None -> + (str "Cancelling previous deprecation of notation" ++ spc () ++ + pr_notation ntn ++ pr_optional_scope scope ++ str ".") + | Some _, Some _ -> + (str "Amending deprecation of notation" ++ spc () ++ + pr_notation ntn ++ pr_optional_scope scope ++ str ".")) + +type notation_use = + | OnlyPrinting + | OnlyParsing + | ParsingAndPrinting + +let warn_override_if_needed (scopt,ntn) overridden data old_data = + if overridden then warn_notation_overridden (scopt,ntn) + else + if data.not_deprecation <> old_data.not_deprecation then + warn_deprecation_overridden ((scopt,ntn),old_data.not_deprecation,data.not_deprecation) + +let check_parsing_override (scopt,ntn) data = function + | OnlyParsingData (_,old_data) -> + let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in + warn_override_if_needed (scopt,ntn) overridden data old_data; + None, not overridden + | ParsingAndPrintingData (_,on_printing,old_data) -> + let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in + warn_override_if_needed (scopt,ntn) overridden data old_data; + (if on_printing then Some old_data.not_interp else None), not overridden + | NoParsingData -> None, false + +let check_printing_override (scopt,ntn) data parsingdata printingdata = + let parsing_update = match parsingdata with + | OnlyParsingData _ | NoParsingData -> parsingdata + | ParsingAndPrintingData (_,on_printing,old_data) -> + let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in + warn_override_if_needed (scopt,ntn) overridden data old_data; + if overridden then NoParsingData else parsingdata in + let exists = List.exists (fun (on_printing,old_data) -> + let exists = interpretation_eq data.not_interp old_data.not_interp in + if exists && data.not_deprecation <> old_data.not_deprecation then + warn_deprecation_overridden ((scopt,ntn),old_data.not_deprecation,data.not_deprecation); + exists) printingdata in + parsing_update, exists + +let remove_uninterpretation rule (metas,c as pat) = + let (key,n) = notation_constr_key c in + notations_key_table := keymap_remove key (rule,pat,n) !notations_key_table let declare_uninterpretation rule (metas,c as pat) = let (key,n) = notation_constr_key c in notations_key_table := keymap_add key (rule,pat,n) !notations_key_table +let update_notation_data (scopt,ntn) use data table = + let (parsingdata,printingdata) = + try NotationMap.find ntn table with Not_found -> (NoParsingData, []) in + match use with + | OnlyParsing -> + let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in + NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update, exists + | ParsingAndPrinting -> + let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in + NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update, exists + | OnlyPrinting -> + let parsingdata, exists = check_printing_override (scopt,ntn) data parsingdata printingdata in + let printingdata = if exists then printingdata else (true,data) :: printingdata in + NotationMap.add ntn (parsingdata, printingdata) table, None, exists + let rec find_interpretation ntn find = function | [] -> raise Not_found | OpenScopeItem scope :: scopes -> @@ -1273,7 +1370,9 @@ let rec find_interpretation ntn find = function find_interpretation ntn find scopes let find_notation ntn sc = - NotationMap.find ntn (find_scope sc).notations + match fst (NotationMap.find ntn (find_scope sc).notations) with + | OnlyParsingData (true,data) | ParsingAndPrintingData (true,_,data) -> data + | _ -> raise Not_found let notation_of_prim_token = function | Constrexpr.Numeral (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n @@ -1358,10 +1457,37 @@ let uninterp_cases_pattern_notations c = let uninterp_ind_pattern_notations ind = keymap_find (RefKey (canonical_gr (GlobRef.IndRef ind))) !notations_key_table +let has_active_parsing_rule_in_scope ntn sc = + try + match NotationMap.find ntn (String.Map.find sc !scope_map).notations with + | OnlyParsingData (active,_),_ | ParsingAndPrintingData (active,_,_),_ -> active + | _ -> false + with Not_found -> false + +let is_printing_active_in_scope (scope,ntn) pat = + let sc = match scope with NotationInScope sc -> sc | LastLonelyNotation -> default_scope in + let is_active extra = + try + let (_,(active,_)) = List.extract_first (fun (active,d) -> interpretation_eq d.not_interp pat) extra in + active + with Not_found -> false in + try + match NotationMap.find ntn (String.Map.find sc !scope_map).notations with + | ParsingAndPrintingData (_,active,d), extra -> + if interpretation_eq d.not_interp pat then active + else is_active extra + | _, extra -> is_active extra + with Not_found -> false + +let is_printing_inactive_rule rule pat = + match rule with + | NotationRule (scope,ntn) -> + not (is_printing_active_in_scope (scope,ntn) pat) + | SynDefRule kn -> + try let _ = Nametab.path_of_syndef kn in false with Not_found -> true + let availability_of_notation (ntn_scope,ntn) scopes = - let f scope = - NotationMap.mem ntn (String.Map.find scope !scope_map).notations in - find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes) + find_without_delimiters (has_active_parsing_rule_in_scope ntn) (ntn_scope,Some ntn) (make_current_scopes scopes) (* We support coercions from a custom entry at some level to an entry at some level (possibly the same), and from and to the constr entry. E.g.: @@ -1484,6 +1610,49 @@ let entry_has_ident = function | InCustomEntryLevel (s,n) -> try String.Map.find s !entry_has_ident_map <= n with Not_found -> false +type entry_coercion_kind = + | IsEntryCoercion of notation_entry_level + | IsEntryGlobal of string * int + | IsEntryIdent of string * int + +let declare_notation (scopt,ntn) pat df ~use coe deprecation = + (* Register the interpretation *) + let scope = match scopt with NotationInScope s -> s | LastLonelyNotation -> default_scope in + let sc = find_scope scope in + let notdata = { + not_interp = pat; + not_location = df; + not_deprecation = deprecation; + } in + let notation_update,printing_update, exists = update_notation_data (scopt,ntn) use notdata sc.notations in + if not exists then + let sc = { sc with notations = notation_update } in + scope_map := String.Map.add scope sc !scope_map; + (* Update the uninterpretation cache *) + begin match printing_update with + | Some pat -> remove_uninterpretation (NotationRule (scopt,ntn)) pat + | None -> () + end; + if not exists && use <> OnlyParsing then declare_uninterpretation (NotationRule (scopt,ntn)) pat; + (* Register visibility of lonely notations *) + if not exists then begin match scopt with + | LastLonelyNotation -> scope_stack := LonelyNotationItem ntn :: !scope_stack + | NotationInScope _ -> () + end; + (* Declare a possible coercion *) + if not exists then begin match coe with + | Some (IsEntryCoercion entry) -> + let (_,level,_) = level_of_notation ntn in + let level = match fst ntn with + | InConstrEntry -> None + | InCustomEntry _ -> Some level + in + declare_entry_coercion (scopt,ntn) level entry + | Some (IsEntryGlobal (entry,n)) -> declare_custom_entry_has_global entry n + | Some (IsEntryIdent (entry,n)) -> declare_custom_entry_has_ident entry n + | None -> () + end + let availability_of_prim_token n printer_scope local_scopes = let f scope = try @@ -1561,38 +1730,6 @@ let uninterp_prim_token_cases_pattern c local_scopes = (* Miscellaneous *) -let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 - -let notation_binder_source_eq s1 s2 = match s1, s2 with -| NtnParsedAsIdent, NtnParsedAsIdent -> true -| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 -| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2 -| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false - -let ntpe_eq t1 t2 = match t1, t2 with -| NtnTypeConstr, NtnTypeConstr -> true -| NtnTypeBinder s1, NtnTypeBinder s2 -> notation_binder_source_eq s1 s2 -| NtnTypeConstrList, NtnTypeConstrList -> true -| NtnTypeBinderList, NtnTypeBinderList -> true -| (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false - -let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) = - notation_entry_level_eq entry1 entry2 && - pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 && - ntpe_eq tp1 tp2 - -let interpretation_eq (vars1, t1) (vars2, t2) = - List.equal var_attributes_eq vars1 vars2 && - Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2 - -let exists_notation_in_scope scopt ntn onlyprint r = - let scope = match scopt with Some s -> s | None -> default_scope in - try - let sc = String.Map.find scope !scope_map in - let n = NotationMap.find ntn sc.notations in - interpretation_eq n.not_interp r - with Not_found -> false - let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) @@ -1846,38 +1983,63 @@ let pr_scope_classes sc = | _ :: ll -> let opt_s = match ll with [] -> mt () | _ -> str "es" in hov 0 (str "Bound to class" ++ opt_s ++ - spc() ++ prlist_with_sep spc pr_scope_class l) ++ fnl() + spc() ++ prlist_with_sep spc pr_scope_class l) let pr_notation_info prglob ntn c = - str "\"" ++ str ntn ++ str "\" := " ++ + str "\"" ++ str ntn ++ str "\" :=" ++ brk (1,2) ++ prglob (Notation_ops.glob_constr_of_notation_constr c) -let pr_named_scope prglob scope sc = +let pr_notation_status on_parsing on_printing = + let deactivated b = if b then [] else ["deactivated"] in + let l = match on_parsing, on_printing with + | Some on, None -> "only parsing" :: deactivated on + | None, Some on -> "only printing" :: deactivated on + | Some false, Some false -> ["deactivated"] + | Some true, Some false -> ["deactivated for printing"] + | Some false, Some true -> ["deactivated for parsing"] + | Some true, Some true -> [] + | None, None -> assert false in + match l with + | [] -> mt () + | l -> str "(" ++ prlist_with_sep pr_comma str l ++ str ")" + +let pr_non_empty spc pp = + if pp = mt () then mt () else spc ++ pp + +let pr_notation_data prglob (on_parsing,on_printing,{ not_interp = (_, r); not_location = (_, df) }) = + hov 0 (pr_notation_info prglob df r ++ pr_non_empty (brk(1,2)) (pr_notation_status on_parsing on_printing)) + +let extract_notation_data (main,extra) = + let main = match main with + | NoParsingData -> [] + | ParsingAndPrintingData (on_parsing, on_printing, d) -> + [Some on_parsing, Some on_printing, d] + | OnlyParsingData (on_parsing, d) -> + [Some on_parsing, None, d] in + let extra = List.map (fun (on_printing, d) -> (None, Some on_printing, d)) extra in + main @ extra + +let pr_named_scope prglob (scope,sc) = (if String.equal scope default_scope then match NotationMap.cardinal sc.notations with | 0 -> str "No lonely notation" | n -> str "Lonely notation" ++ (if Int.equal n 1 then mt() else str"s") else str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters) - ++ fnl () - ++ pr_scope_classes scope - ++ NotationMap.fold - (fun ntn { not_interp = (_, r); not_location = (_, df) } strm -> - pr_notation_info prglob df r ++ fnl () ++ strm) - sc.notations (mt ()) + ++ pr_non_empty (fnl ()) (pr_scope_classes scope) + ++ prlist (fun a -> fnl () ++ pr_notation_data prglob a) + (NotationMap.fold (fun ntn data l -> extract_notation_data data @ l) sc.notations []) -let pr_scope prglob scope = pr_named_scope prglob scope (find_scope scope) +let pr_scope prglob scope = pr_named_scope prglob (scope, find_scope scope) let pr_scopes prglob = - String.Map.fold - (fun scope sc strm -> pr_named_scope prglob scope sc ++ fnl () ++ strm) - !scope_map (mt ()) + let l = String.Map.bindings !scope_map in + prlist_with_sep (fun () -> fnl () ++ fnl ()) (pr_named_scope prglob) l let rec find_default ntn = function | [] -> None | OpenScopeItem scope :: scopes -> - if NotationMap.mem ntn (find_scope scope).notations then - Some scope + if has_active_parsing_rule_in_scope ntn scope then Some scope else find_default ntn scopes | LonelyNotationItem ntn' :: scopes -> if notation_eq ntn ntn' then Some default_scope @@ -1885,12 +2047,12 @@ let rec find_default ntn = function let factorize_entries = function | [] -> [] - | (ntn,c)::l -> + | (ntn,sc',c)::l -> let (ntn,l_of_ntn,rest) = List.fold_left - (fun (a',l,rest) (a,c) -> - if notation_eq a a' then (a',c::l,rest) else (a,[c],(a',l)::rest)) - (ntn,[c],[]) l in + (fun (a',l,rest) (a,sc,c) -> + if notation_eq a a' then (a',(sc,c)::l,rest) else (a,[sc,c],(a',l)::rest)) + (ntn,[sc',c],[]) l in (ntn,l_of_ntn)::rest type symbol_token = WhiteSpace of int | String of string @@ -1961,16 +2123,18 @@ let browse_notation strict ntn map = let l = String.Map.fold (fun scope_name sc -> - NotationMap.fold (fun ntn { not_interp = (_, r); not_location = df } l -> - if List.exists (find ntn) ntns then (ntn,(scope_name,r,df))::l else l) sc.notations) + NotationMap.fold (fun ntn data l -> + if List.exists (find ntn) ntns + then List.map (fun d -> (ntn,scope_name,d)) (extract_notation_data data) @ l + else l) sc.notations) map [] in - List.sort (fun x y -> String.compare (snd (fst x)) (snd (fst y))) l + List.sort (fun x y -> String.compare (snd (pi1 x)) (snd (pi1 y))) l -let global_reference_of_notation ~head test (ntn,(sc,c,_)) = +let global_reference_of_notation ~head test (ntn,sc,(on_parsing,on_printing,{not_interp = (_,c)})) = match c with - | NRef ref when test ref -> Some (ntn,sc,ref) + | NRef ref when test ref -> Some (on_parsing,on_printing,ntn,sc,ref) | NApp (NRef ref, l) when head || List.for_all isNVar_or_NHole l && test ref -> - Some (ntn,sc,ref) + Some (on_parsing,on_printing,ntn,sc,ref) | _ -> None let error_ambiguous_notation ?loc _ntn = @@ -1990,17 +2154,17 @@ let interp_notation_as_global_reference ?loc ~head test ntn sc = let ntns = browse_notation true ntn scopes in let refs = List.map (global_reference_of_notation ~head test) ntns in match Option.List.flatten refs with - | [_,_,ref] -> ref + | [Some true,_ (* why not if the only one? *),_,_,ref] -> ref | [] -> error_notation_not_reference ?loc ntn | refs -> - let f (ntn,sc,ref) = + let f (on_parsing,_,ntn,sc,ref) = let def = find_default ntn !scope_stack in match def with | None -> false - | Some sc' -> String.equal sc sc' + | Some sc' -> on_parsing = Some true && String.equal sc sc' in match List.filter f refs with - | [_,_,ref] -> ref + | [_,_,_,_,ref] -> ref | [] -> error_notation_not_reference ?loc ntn | _ -> error_ambiguous_notation ?loc ntn @@ -2010,24 +2174,25 @@ let locate_notation prglob ntn scope = match ntns with | [] -> str "Unknown notation" | _ -> - str "Notation" ++ fnl () ++ prlist_with_sep fnl (fun (ntn,l) -> let scope = find_default ntn scopes in prlist_with_sep fnl - (fun (sc,r,(_,df)) -> + (fun (sc,(on_parsing,on_printing,{ not_interp = (_, r); not_location = (_, df) })) -> hov 0 ( + str "Notation" ++ brk (1,2) ++ pr_notation_info prglob df r ++ (if String.equal sc default_scope then mt () - else (spc () ++ str ": " ++ str sc)) ++ + else (brk (1,2) ++ str ": " ++ str sc)) ++ (if Option.equal String.equal (Some sc) scope - then spc () ++ str "(default interpretation)" else mt ()))) + then brk (1,2) ++ str "(default interpretation)" else mt ()) ++ + pr_non_empty (brk (1,2)) (pr_notation_status on_parsing on_printing))) l) ntns let collect_notation_in_scope scope sc known = assert (not (String.equal scope default_scope)); NotationMap.fold - (fun ntn { not_interp = (_, r); not_location = (_, df) } (l,known as acc) -> - if List.mem_f notation_eq ntn known then acc else ((df,r)::l,ntn::known)) + (fun ntn d (l,known as acc) -> + if List.mem_f notation_eq ntn known then acc else (extract_notation_data d @ l,ntn::known)) sc.notations ([],known) let collect_notations stack = @@ -2043,13 +2208,13 @@ let collect_notations stack = if List.mem_f notation_eq ntn knownntn then (all,knownntn) else try - let { not_interp = (_, r); not_location = (_, df) } = - NotationMap.find ntn (find_scope default_scope).notations in + let datas = extract_notation_data + (NotationMap.find ntn (find_scope default_scope).notations) in let all' = match all with | (s,lonelyntn)::rest when String.equal s default_scope -> - (s,(df,r)::lonelyntn)::rest + (s,datas@lonelyntn)::rest | _ -> - (default_scope,[df,r])::all in + (default_scope,datas)::all in (all',ntn::knownntn) with Not_found -> (* e.g. if only printing *) (all,knownntn)) ([],[]) stack) @@ -2057,7 +2222,7 @@ let collect_notations stack = let pr_visible_in_scope prglob (scope,ntns) = let strm = List.fold_right - (fun (df,r) strm -> pr_notation_info prglob df r ++ fnl () ++ strm) + (fun d strm -> pr_notation_data prglob d ++ fnl () ++ strm) ntns (mt ()) in (if String.equal scope default_scope then str "Lonely notation" ++ (match ntns with [_] -> mt () | _ -> str "s") @@ -2066,9 +2231,7 @@ let pr_visible_in_scope prglob (scope,ntns) = ++ fnl () ++ strm let pr_scope_stack prglob stack = - List.fold_left - (fun strm scntns -> strm ++ pr_visible_in_scope prglob scntns ++ fnl ()) - (mt ()) (collect_notations stack) + prlist_with_sep fnl (pr_visible_in_scope prglob) (collect_notations stack) let pr_visibility prglob = function | Some scope -> pr_scope_stack prglob (push_scope scope !scope_stack) diff --git a/interp/notation.mli b/interp/notation.mli index 948831b317..d744ff41d9 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -229,12 +229,24 @@ type interp_rule = | NotationRule of specific_notation | SynDefRule of KerName.t -val declare_notation_interpretation : notation -> scope_name option -> - interpretation -> notation_location -> onlyprint:bool -> - Deprecation.t option -> unit +type notation_use = + | OnlyPrinting + | OnlyParsing + | ParsingAndPrinting val declare_uninterpretation : interp_rule -> interpretation -> unit +type entry_coercion_kind = + | IsEntryCoercion of notation_entry_level + | IsEntryGlobal of string * int + | IsEntryIdent of string * int + +val declare_notation : notation_with_optional_scope * notation -> + interpretation -> notation_location -> use:notation_use -> + entry_coercion_kind option -> + Deprecation.t option -> unit + + (** Return the interpretation bound to a notation *) val interp_notation : ?loc:Loc.t -> notation -> subscopes -> interpretation * (notation_location * scope_name option) @@ -257,16 +269,14 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list val availability_of_notation : specific_notation -> subscopes -> (scope_name option * delimiters option) option +val is_printing_inactive_rule : interp_rule -> interpretation -> bool + (** {6 Miscellaneous} *) (** If head is true, also allows applied global references. *) val interp_notation_as_global_reference : ?loc:Loc.t -> head:bool -> (GlobRef.t -> bool) -> notation_key -> delimiters option -> GlobRef.t -(** Checks for already existing notations *) -val exists_notation_in_scope : scope_name option -> notation -> - bool -> interpretation -> bool - (** Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope : bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 22531b0016..354809252e 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -27,7 +27,9 @@ open Notation_term (* helper for NVar, NVar case in eq_notation_constr *) let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None -let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with +let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = +(vars1 == vars2 && t1 == t2) || +match t1, t2 with | NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2 | NVar id1, NVar id2 -> ( match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with diff --git a/kernel/environ.ml b/kernel/environ.ml index 03c9cb4be6..dec9e1deb8 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -274,6 +274,11 @@ let is_impredicative_sort env = function let is_impredicative_univ env u = is_impredicative_sort env (Sorts.sort_of_univ u) +let is_impredicative_family env = function + | Sorts.InSProp | Sorts.InProp -> true + | Sorts.InSet -> is_impredicative_set env + | Sorts.InType -> false + let type_in_type env = not (typing_flags env).check_universes let deactivated_guard env = not (typing_flags env).check_guarded @@ -467,14 +472,22 @@ let same_flags { [@warning "+9"] let set_cumulative_sprop b = map_universes (UGraph.set_cumulative_sprop b) +let set_type_in_type b = map_universes (UGraph.set_type_in_type b) let set_typing_flags c env = if same_flags env.env_typing_flags c then env - else set_cumulative_sprop c.cumulative_sprop { env with env_typing_flags = c } + else + let env = { env with env_typing_flags = c } in + let env = set_cumulative_sprop c.cumulative_sprop env in + let env = set_type_in_type (not c.check_universes) env in + env let set_cumulative_sprop b env = set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env +let set_type_in_type b env = + set_typing_flags {env.env_typing_flags with check_universes=not b} env + let set_allow_sprop b env = { env with env_stratification = { env.env_stratification with env_sprop_allowed = b } } diff --git a/kernel/environ.mli b/kernel/environ.mli index 974e794c6b..f443ba38e1 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -122,6 +122,7 @@ val indices_matter : env -> bool val is_impredicative_sort : env -> Sorts.t -> bool val is_impredicative_univ : env -> Univ.Universe.t -> bool +val is_impredicative_family : env -> Sorts.family -> bool (** is the local context empty *) val empty_context : env -> bool @@ -320,6 +321,7 @@ val push_subgraph : Univ.ContextSet.t -> env -> env val set_engagement : engagement -> env -> env val set_typing_flags : typing_flags -> env -> env val set_cumulative_sprop : bool -> env -> env +val set_type_in_type : bool -> env -> env val set_allow_sprop : bool -> env -> env val sprop_allowed : env -> bool diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 179353d3f0..b2520b780f 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -77,7 +77,7 @@ let check_univ_leq ?(is_real_arg=false) env u info = else info in (* Inductive types provide explicit lifting from SProp to other universes, so allow SProp <= any. *) - if type_in_type env || Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ + if Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ then { info with ind_min_univ = Option.map (Universe.sup u) info.ind_min_univ } else if is_impredicative_univ env ind_univ && Option.is_empty info.ind_min_univ then { info with ind_squashed = true } diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 52e93a9e22..096e458ec4 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -29,7 +29,12 @@ module G = AcyclicGraph.Make(struct code (eg add_universe with a constraint vs G.add with no constraint) *) -type t = { graph: G.t; sprop_cumulative : bool } +type t = { + graph: G.t; + sprop_cumulative : bool; + type_in_type : bool; +} + type 'a check_function = t -> 'a -> 'a -> bool let g_map f g = @@ -39,6 +44,10 @@ let g_map f g = let set_cumulative_sprop b g = {g with sprop_cumulative=b} +let set_type_in_type b g = {g with type_in_type=b} + +let type_in_type g = g.type_in_type + let check_smaller_expr g (u,n) (v,m) = let diff = n - m in match diff with @@ -55,28 +64,33 @@ let real_check_leq g u v = Universe.for_all (fun ul -> exists_bigger g ul v) u let check_leq g u v = + type_in_type g || Universe.equal u v || (g.sprop_cumulative && Universe.is_sprop u) || (not (Universe.is_sprop u) && not (Universe.is_sprop v) && (is_type0m_univ u || real_check_leq g u v)) let check_eq g u v = + type_in_type g || Universe.equal u v || (not (Universe.is_sprop u || Universe.is_sprop v) && (real_check_leq g u v && real_check_leq g v u)) let check_eq_level g u v = u == v || + type_in_type g || (not (Level.is_sprop u || Level.is_sprop v) && G.check_eq g.graph u v) -let empty_universes = {graph=G.empty; sprop_cumulative=false} +let empty_universes = {graph=G.empty; sprop_cumulative=false; type_in_type=false} let initial_universes = let big_rank = 1000000 in let g = G.empty in let g = G.add ~rank:big_rank Level.prop g in let g = G.add ~rank:big_rank Level.set g in - {graph=G.enforce_lt Level.prop Level.set g; sprop_cumulative=false} + {empty_universes with graph=G.enforce_lt Level.prop Level.set g} + +let initial_universes_with g = {g with graph=initial_universes.graph} let enforce_constraint (u,d,v) g = match d with @@ -91,6 +105,10 @@ let enforce_constraint (u,d,v as cst) g = | true, Le, false when g.sprop_cumulative -> g | _ -> raise (UniverseInconsistency (d,Universe.make u, Universe.make v, None)) +let enforce_constraint cst g = + if not (type_in_type g) then enforce_constraint cst g + else try enforce_constraint cst g with UniverseInconsistency _ -> g + let merge_constraints csts g = Constraint.fold enforce_constraint csts g let check_constraint g (u,d,v) = @@ -103,8 +121,8 @@ let check_constraint g (u,d,v as cst) = match Level.is_sprop u, d, Level.is_sprop v with | false, _, false -> check_constraint g.graph cst | true, (Eq|Le), true -> true - | true, Le, false -> g.sprop_cumulative - | _ -> false + | true, Le, false -> g.sprop_cumulative || type_in_type g + | _ -> type_in_type g let check_constraints csts g = Constraint.for_all (check_constraint g) csts @@ -145,8 +163,10 @@ let enforce_leq_alg u v g = let enforce_leq_alg u v g = match Universe.is_sprop u, Universe.is_sprop v with | true, true -> Constraint.empty, g - | true, false | false, true -> raise (UniverseInconsistency (Le, u, v, None)) | false, false -> enforce_leq_alg u v g + | left, _ -> + if left && g.sprop_cumulative then Constraint.empty, g + else raise (UniverseInconsistency (Le, u, v, None)) (* sanity check wrapper *) let enforce_leq_alg u v g = diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index c9fbd7f694..87b3634e28 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -16,6 +16,15 @@ type t val set_cumulative_sprop : bool -> t -> t (** Makes the system incomplete. *) +val set_type_in_type : bool -> t -> t + +(** When [type_in_type], functions adding constraints do not fail and + may instead ignore inconsistent constraints. + + Checking functions such as [check_leq] always return [true]. +*) +val type_in_type : t -> bool + type 'a check_function = t -> 'a -> 'a -> bool val check_leq : Universe.t check_function @@ -25,6 +34,9 @@ val check_eq_level : Level.t check_function (** The initial graph of universes: Prop < Set *) val initial_universes : t +(** Initial universes, but keeping options such as type in type from the argument. *) +val initial_universes_with : t -> t + (** Check equality of instances w.r.t. a universe graph *) val check_eq_instances : Instance.t check_function diff --git a/kernel/univ.ml b/kernel/univ.ml index 6d8aa02dff..a2fd14025e 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -205,12 +205,6 @@ module Level = struct let pr u = str (to_string u) - let apart u v = - match data u, data v with - | SProp, _ | _, SProp - | Prop, Set | Set, Prop -> true - | _ -> false - let vars = Array.init 20 (fun i -> make (Var i)) let var n = @@ -250,7 +244,7 @@ module LMap = struct ext empty let pr f m = - h 0 (prlist_with_sep fnl (fun (u, v) -> + h (prlist_with_sep fnl (fun (u, v) -> Level.pr u ++ f v) (bindings m)) end @@ -568,16 +562,6 @@ let constraint_type_ord c1 c2 = match c1, c2 with | Eq, Eq -> 0 | Eq, _ -> 1 -(* Universe inconsistency: error raised when trying to enforce a relation - that would create a cycle in the graph of universes. *) - -type univ_inconsistency = constraint_type * universe * universe * explanation Lazy.t option - -exception UniverseInconsistency of univ_inconsistency - -let error_inconsistency o u v p = - raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p)) - (* Constraints and sets of constraints. *) type univ_constraint = Level.t * constraint_type * Level.t @@ -660,8 +644,6 @@ type 'a constraint_function = 'a -> 'a -> constraints -> constraints let enforce_eq_level u v c = (* We discard trivial constraints like u=u *) if Level.equal u v then c - else if Level.apart u v then - error_inconsistency Eq u v None else Constraint.add (u,Eq,v) c let enforce_eq u v c = @@ -684,9 +666,9 @@ let constraint_add_leq v u c = let j = m - n in if j = -1 (* n = m+1, v+1 <= u <-> v < u *) then Constraint.add (x,Lt,y) c - else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then - if Level.equal x y then (* u+(k+1) <= u *) - raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u, None)) + else if j <= -1 (* n = m+k, v+k <= u and k>0 *) then + if Level.equal x y then (* u+k <= u with k>0 *) + Constraint.add (x,Lt,x) c else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.") else if j = 0 then Constraint.add (x,Le,y) c @@ -703,8 +685,8 @@ let check_univ_leq u v = let enforce_leq u v c = match Universe.is_sprop u, Universe.is_sprop v with | true, true -> c - | true, false | false, true -> - raise (UniverseInconsistency (Le, u, v, None)) + | true, false -> Constraint.add (Level.sprop,Le,Level.prop) c + | false, true -> Constraint.add (Level.prop,Le,Level.sprop) c | false, false -> List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v @@ -961,7 +943,7 @@ struct let pr prl ?variance (univs, cst as ctx) = if is_empty ctx then mt() else - h 0 (Instance.pr prl ?variance univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) + h (Instance.pr prl ?variance univs ++ str " |= ") ++ h (v 0 (Constraint.pr prl cst)) let hcons (univs, cst) = (Instance.hcons univs, hcons_constraints cst) @@ -1076,7 +1058,7 @@ struct let pr prl (univs, cst as ctx) = if is_empty ctx then mt() else - h 0 (LSet.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) + h (LSet.pr prl univs ++ str " |= ") ++ h (v 0 (Constraint.pr prl cst)) let constraints (_univs, cst) = cst let levels (univs, _cst) = univs @@ -1232,6 +1214,14 @@ let hcons_universe_context_set (v, c) = let hcons_univ x = Universe.hcons x +(* Universe inconsistency: error raised when trying to enforce a relation + that would create a cycle in the graph of universes. *) + +type univ_inconsistency = constraint_type * universe * universe * explanation Lazy.t option + +(* Do not use in this file as we may be type-in-type *) +exception UniverseInconsistency of univ_inconsistency + let explain_universe_inconsistency prl (o,u,v,p : univ_inconsistency) = let pr_uni = Universe.pr_with prl in let pr_rel = function diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml index 74405a0105..c156a21c86 100644 --- a/kernel/vmbytecodes.ml +++ b/kernel/vmbytecodes.ml @@ -106,14 +106,14 @@ let rec pp_instr i = | Kclosure(lbl, n) -> str "closure " ++ pp_lbl lbl ++ str ", " ++ int n | Kclosurerec(fv,init,lblt,lblb) -> - h 1 (str "closurerec " ++ + hv 1 (str "closurerec " ++ int fv ++ str ", " ++ int init ++ str " types = " ++ prlist_with_sep spc pp_lbl (Array.to_list lblt) ++ str " bodies = " ++ prlist_with_sep spc pp_lbl (Array.to_list lblb)) | Kclosurecofix (fv,init,lblt,lblb) -> - h 1 (str "closurecofix " ++ + hv 1 (str "closurecofix " ++ int fv ++ str ", " ++ int init ++ str " types = " ++ prlist_with_sep spc pp_lbl (Array.to_list lblt) ++ @@ -129,7 +129,7 @@ let rec pp_instr i = str "makeswitchblock " ++ pp_lbl lblt ++ str ", " ++ pp_lbl lbls ++ str ", " ++ int sz | Kswitch(lblc,lblb) -> - h 1 (str "switch " ++ + hv 1 (str "switch " ++ prlist_with_sep spc pp_lbl (Array.to_list lblc) ++ str " | " ++ prlist_with_sep spc pp_lbl (Array.to_list lblb)) diff --git a/lib/explore.ml b/lib/explore.ml index b3ffef6ac2..139de488e2 100644 --- a/lib/explore.ml +++ b/lib/explore.ml @@ -29,7 +29,7 @@ module Make = functor(S : SearchProblem) -> struct | [i] -> int i | i :: l -> pp_rec l ++ str "." ++ int i in - Feedback.msg_debug (h 0 (pp_rec p) ++ pp) + Feedback.msg_debug (h (pp_rec p) ++ pp) (*s Depth first search. *) diff --git a/lib/flags.ml b/lib/flags.ml index 1d9d6d49bc..83733cf00d 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -47,6 +47,7 @@ let async_proofs_is_worker () = !async_proofs_worker_id <> "master" let load_vos_libraries = ref false let debug = ref false +let xml_debug = ref false let in_debugger = ref false let in_toplevel = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 30d1b5b2bd..ebd23a4d20 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -41,6 +41,7 @@ val load_vos_libraries : bool ref (** Debug flags *) val debug : bool ref +val xml_debug : bool ref val in_debugger : bool ref val in_toplevel : bool ref @@ -22,7 +22,7 @@ type pp_tag = string type block_type = - | Pp_hbox of int + | Pp_hbox | Pp_vbox of int | Pp_hvbox of int | Pp_hovbox of int @@ -131,7 +131,7 @@ let strbrk s = let ismt = function | Ppcmd_empty -> true | _ -> false (* boxing commands *) -let h n s = Ppcmd_box(Pp_hbox n,s) +let h s = Ppcmd_box(Pp_hbox,s) let v n s = Ppcmd_box(Pp_vbox n,s) let hv n s = Ppcmd_box(Pp_hvbox n,s) let hov n s = Ppcmd_box(Pp_hovbox n,s) @@ -151,7 +151,7 @@ let escape_string s = let qstring s = str "\"" ++ str (escape_string s) ++ str "\"" let qs = qstring -let quote s = h 0 (str "\"" ++ s ++ str "\"") +let quote s = h (str "\"" ++ s ++ str "\"") let rec pr_com ft s = let (s1,os) = @@ -181,7 +181,7 @@ let split_tag tag = (* pretty printing functions *) let pp_with ft pp = let cpp_open_box = function - | Pp_hbox n -> Format.pp_open_hbox ft () + | Pp_hbox -> Format.pp_open_hbox ft () | Pp_vbox n -> Format.pp_open_vbox ft n | Pp_hvbox n -> Format.pp_open_hvbox ft n | Pp_hovbox n -> Format.pp_open_hovbox ft n @@ -309,12 +309,14 @@ let db_print_pp fmt pp = let block_type fmt btype = let (bt, v) = match btype with - | Pp_hbox v -> ("Pp_hbox", v) - | Pp_vbox v -> ("Pp_vbox", v) - | Pp_hvbox v -> ("Pp_hvbox", v) - | Pp_hovbox v -> ("Pp_hovbox", v) + | Pp_hbox -> ("Pp_hbox", None) + | Pp_vbox v -> ("Pp_vbox", Some v) + | Pp_hvbox v -> ("Pp_hvbox", Some v) + | Pp_hovbox v -> ("Pp_hovbox", Some v) in - fprintf fmt "%s %d" bt v + match v with + | None -> fprintf fmt "%s" bt + | Some v -> fprintf fmt "%s %d" bt v in let rec db_print_pp_r indent pp = let ind () = fprintf fmt "%s" (String.make (2 * indent) ' ') in diff --git a/lib/pp.mli b/lib/pp.mli index b265537728..12f1ba9bb2 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -43,7 +43,7 @@ type pp_tag = string type t type block_type = - | Pp_hbox of int + | Pp_hbox | Pp_vbox of int | Pp_hvbox of int | Pp_hovbox of int @@ -99,7 +99,7 @@ val strbrk : string -> t (** {6 Boxing commands} *) -val h : int -> t -> t +val h : t -> t val v : int -> t -> t val hv : int -> t -> t val hov : int -> t -> t diff --git a/lib/pp_diff.ml b/lib/pp_diff.ml index 988e8e4303..4593bf4b07 100644 --- a/lib/pp_diff.ml +++ b/lib/pp_diff.ml @@ -109,7 +109,7 @@ let shorten_diff_span dtype diff_list = iter 0 len (<) 1; (* left to right *) iter (len-1) (-1) (>) (-1); (* right to left *) - if !changed then Array.to_list diffs else diff_list;; + if !changed then Array.to_list diffs else diff_list let has_changes diffs = let rec has_changes_r diffs added removed = @@ -118,12 +118,12 @@ let has_changes diffs = | `Removed _ :: t -> has_changes_r t added true | h :: t -> has_changes_r t added removed | [] -> (added, removed) in - has_changes_r diffs false false;; + has_changes_r diffs false false (* get the Myers diff of 2 lists of strings *) let diff_strs old_strs new_strs = let diffs = List.rev (StringDiff.diff old_strs new_strs) in - shorten_diff_span `Removed (shorten_diff_span `Added diffs);; + shorten_diff_span `Removed (shorten_diff_span `Added diffs) (* Default string tokenizer. Makes each character a separate strin. Whitespace is not ignored. Doesn't handle UTF-8 differences well. *) @@ -139,7 +139,7 @@ let def_tokenize_string s = let diff_str ?(tokenize_string=def_tokenize_string) old_str new_str = let old_toks = Array.of_list (tokenize_string old_str) and new_toks = Array.of_list (tokenize_string new_str) in - diff_strs old_toks new_toks;; + diff_strs old_toks new_toks let get_dinfo = function | `Common (_, _, s) -> (`Common, s) @@ -281,14 +281,14 @@ let add_diff_tags which pp diffs = skip (); if !diffs <> [] then raise (Diff_Failure "left-over diff info at end of Pp.t, should be impossible"); - if has_added || has_removed then wrap_in_bg diff_tag rv else rv;; + if has_added || has_removed then wrap_in_bg diff_tag rv else rv let diff_pp ?(tokenize_string=def_tokenize_string) o_pp n_pp = let open Pp in let o_str = string_of_ppcmds o_pp in let n_str = string_of_ppcmds n_pp in let diffs = diff_str ~tokenize_string o_str n_str in - (add_diff_tags `Removed o_pp diffs, add_diff_tags `Added n_pp diffs);; + (add_diff_tags `Removed o_pp diffs, add_diff_tags `Added n_pp diffs) let diff_pp_combined ?(tokenize_string=def_tokenize_string) ?(show_removed=false) o_pp n_pp = let open Pp in @@ -300,4 +300,4 @@ let diff_pp_combined ?(tokenize_string=def_tokenize_string) ?(show_removed=false if show_removed && has_removed then let removed = add_diff_tags `Removed o_pp diffs in (v 0 (removed ++ cut() ++ added)) - else added;; + else added diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml index fe6e8360c1..aab385a707 100644 --- a/parsing/ppextend.ml +++ b/parsing/ppextend.ml @@ -17,7 +17,7 @@ open Constrexpr (*s Pretty-print. *) type ppbox = - | PpHB of int + | PpHB | PpHOVB of int | PpHVB of int | PpVB of int @@ -27,7 +27,7 @@ type ppcut = | PpFnl let ppcmd_of_box = function - | PpHB n -> h n + | PpHB -> h | PpHOVB n -> hov n | PpHVB n -> hv n | PpVB n -> v n diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli index ee8180c7aa..56a3fc8e3c 100644 --- a/parsing/ppextend.mli +++ b/parsing/ppextend.mli @@ -13,7 +13,7 @@ open Constrexpr (** {6 Pretty-print. } *) type ppbox = - | PpHB of int + | PpHB | PpHOVB of int | PpHVB of int | PpVB of int diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index ee50476b10..f671860bd5 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -28,7 +28,7 @@ let keywords = "error"; "delay"; "force"; "_"; "__"] Id.Set.empty -let pp_comment s = str";; "++h 0 s++fnl () +let pp_comment s = str ";; " ++ h s ++ fnl () let pp_header_comment = function | None -> mt () diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 1ea803f561..012fcee486 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1860,13 +1860,13 @@ let do_generate_principle_aux pconstants on_error register_built let warn_cannot_define_graph = CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind" (fun (names, error) -> - Pp.(strbrk "Cannot define graph(s) for " ++ h 1 names ++ error)) + Pp.(strbrk "Cannot define graph(s) for " ++ hv 1 names ++ error)) let warn_cannot_define_principle = CWarnings.create ~name:"funind-cannot-define-principle" ~category:"funind" (fun (names, error) -> Pp.( - strbrk "Cannot define induction principle(s) for " ++ h 1 names ++ error)) + strbrk "Cannot define induction principle(s) for " ++ hv 1 names ++ error)) let warning_error names e = let e_explain e = @@ -1898,7 +1898,7 @@ let error_error names e = CErrors.user_err Pp.( str "Cannot define graph(s) for " - ++ h 1 + ++ hv 1 (prlist_with_sep (fun _ -> str "," ++ spc ()) Ppconstr.pr_id names) ++ e_explain e) | _ -> raise e diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index be0d71ad46..6cf5d30a95 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -355,28 +355,8 @@ GRAMMAR EXTEND Gram open Stdarg open Tacarg open Vernacextend -open Goptions open Libnames -let print_info_trace = - declare_intopt_option_and_ref ~depr:false ~key:["Info" ; "Level"] - -let vernac_solve ~pstate n info tcom b = - let open Goal_select in - let pstate, status = Declare.Proof.map_fold_endline ~f:(fun etac p -> - let with_end_tac = if b then Some etac else None in - let global = match n with SelectAll | SelectList _ -> true | _ -> false in - let info = Option.append info (print_info_trace ()) in - let (p,status) = - Proof.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p - in - (* in case a strict subtree was completed, - go back to the top of the prooftree *) - let p = Proof.maximal_unfocus Vernacentries.command_focus p in - p,status) pstate in - if not status then Feedback.feedback Feedback.AddedAxiom; - pstate - let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s } @@ -409,34 +389,34 @@ END { -let is_anonymous_abstract = function - | TacAbstract (_,None) -> true - | TacSolve [TacAbstract (_,None)] -> true - | _ -> false let rm_abstract = function - | TacAbstract (t,_) -> t - | TacSolve [TacAbstract (t,_)] -> TacSolve [t] - | x -> x + | TacAbstract (t,_) -> t, true + | TacSolve [TacAbstract (t,_)] -> TacSolve [t], true + | x -> x, false let is_explicit_terminator = function TacSolve _ -> true | _ -> false } VERNAC { tactic_mode } EXTEND VernacSolve STATE proof -| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => +| [ ltac_selector_opt(g) ltac_info_opt(info) tactic(t) ltac_use_default(with_end_tac) ] => { classify_as_proofstep } -> { let g = Option.default (Goal_select.get_default_goal_selector ()) g in - vernac_solve g n t def + let global = match g with Goal_select.SelectAll | Goal_select.SelectList _ -> true | _ -> false in + let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global; ast = t; }) in + ComTactic.solve g ~info t ~with_end_tac } -| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => +END + +VERNAC { tactic_mode } EXTEND VernacSolveParallel STATE proof +| [ "par" ":" ltac_info_opt(info) tactic(t) ltac_use_default(with_end_tac) ] => { - let anon_abstracting_tac = is_anonymous_abstract t in let solving_tac = is_explicit_terminator t in - let parallel = `Yes (solving_tac,anon_abstracting_tac) in let pbr = if solving_tac then Some "par" else None in - VtProofStep{ parallel = parallel; proof_block_detection = pbr } + VtProofStep{ proof_block_detection = pbr } } -> { - let t = rm_abstract t in - vernac_solve Goal_select.SelectAll n t def + let t, abstract = rm_abstract t in + let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global = true; ast = t; }) in + ComTactic.solve_parallel ~info t ~abstract ~with_end_tac } END diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 85bb901046..cbb53497d3 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -179,7 +179,7 @@ let string_of_genarg_arg (ArgumentType arg) = | ConstrTypeOf c -> hov 1 (keyword "type of" ++ spc() ++ prc env sigma c) | ConstrTerm c when test c -> - h 0 (str "(" ++ prc env sigma c ++ str ")") + h (str "(" ++ prc env sigma c ++ str ")") | ConstrTerm c -> prc env sigma c diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 0dbf16a821..9c15d24dd3 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -146,7 +146,7 @@ let header = fnl () let rec print_node ~filter all_total indent prefix (s, e) = - h 0 ( + h ( padr_with '-' 40 (prefix ^ s ^ " ") ++ padl 7 (format_ratio (e.local /. all_total)) ++ padl 7 (format_ratio (e.total /. all_total)) @@ -212,7 +212,7 @@ let to_string ~filter ?(cutoff=0.0) node = in let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in let msg = - h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++ + h (str "total time: " ++ padl 11 (format_sec (all_total))) ++ fnl () ++ fnl () ++ header ++ diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index ff6a36a049..eaeae50254 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1996,16 +1996,20 @@ let interp_tac_gen lfun avoid_ids debug t = let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t +(* MUST be marshallable! *) +type tactic_expr = { + global: bool; + ast: Tacexpr.raw_tactic_expr; +} + (* Used to hide interpretation for pretty-print, now just launch tactics *) (* [global] means that [t] should be internalized outside of goals. *) -let hide_interp global t ot = +let hide_interp {global;ast} = let hide_interp env = let ist = Genintern.empty_glob_sign env in - let te = intern_pure_tactic ist t in + let te = intern_pure_tactic ist ast in let t = eval_tactic te in - match ot with - | None -> t - | Some t' -> Tacticals.New.tclTHEN t t' + t in if global then Proofview.tclENV >>= fun env -> @@ -2015,6 +2019,8 @@ let hide_interp global t ot = hide_interp (Proofview.Goal.env gl) end +let hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp + (***************************************************************************) (** Register standard arguments *) diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index cbb17bf0fa..01d7306c9d 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -126,8 +126,12 @@ val interp_tac_gen : value Id.Map.t -> Id.Set.t -> val interp : raw_tactic_expr -> unit Proofview.tactic (** Hides interpretation for pretty-print *) +type tactic_expr = { + global: bool; + ast: Tacexpr.raw_tactic_expr; +} -val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> unit Proofview.tactic +val hide_interp : tactic_expr ComTactic.tactic_interpreter (** Internals that can be useful for syntax extensions. *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 7fcb0795bd..91c155fcce 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -883,7 +883,12 @@ and detype_binder d flags bk avoid env sigma decl c = | BLetIn -> let c = detype d { flags with flg_isgoal = false } avoid env sigma (Option.get body) in (* Heuristic: we display the type if in Prop *) - let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in + let s = + (* It can fail if ty is an evar, or if run inside ocamldebug or the + OCaml toplevel since their printers don't have access to the proper sigma/env *) + try Retyping.get_sort_family_of (snd env) sigma ty + with Retyping.RetypeError _ -> InType + in let t = if s != InProp && not !Flags.raw_print then None else Some (detype d { flags with flg_isgoal = false } avoid env sigma ty) in GLetIn (na', c, t, r) diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index f33030d6a4..eaf8c65811 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -175,10 +175,7 @@ let define_evar_as_sort env evd (ev,args) = let evd' = Evd.define ev (mkSort s) evd in Evd.set_leq_sort env evd' (Sorts.super s) (ESorts.kind evd' sort), s -(* Propagation of constraints through application and abstraction: - Given a type constraint on a functional term, returns the type - constraint on its domain and codomain. If the input constraint is - an evar instantiate it with the product of 2 new evars. *) +(* Unify with unknown array *) let rec presplit env sigma c = let c = Reductionops.whd_all env sigma c in @@ -189,25 +186,6 @@ let rec presplit env sigma c = presplit env sigma (mkApp (lam, args)) | _ -> sigma, c -let split_tycon ?loc env evd tycon = - match tycon with - | None -> evd,(make_annot Anonymous Relevant,None,None) - | Some c -> - let evd, c = presplit env evd c in - let evd, na, dom, rng = match EConstr.kind evd c with - | Prod (na,dom,rng) -> evd, na, dom, rng - | Evar ev -> - let (evd,prod) = define_evar_as_product env evd ev in - let (na,dom,rng) = destProd evd prod in - let anon = {na with binder_name = Anonymous} in - evd, anon, dom, rng - | _ -> - (* XXX no error to allow later coercion? Not sure if possible with funclass *) - error_not_product ?loc env evd c - in - evd, (na, mk_tycon dom, mk_tycon rng) - - let define_pure_evar_as_array env sigma evk = let evi = Evd.find_undefined sigma evk in let evenv = evar_env env evi in diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index e5c3f8baa1..5702e169c8 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Names open EConstr open Evd open Environ @@ -31,10 +30,6 @@ val mk_valcon : constr -> val_constraint val evar_absorb_arguments : env -> evar_map -> existential -> constr list -> evar_map * existential -val split_tycon : - ?loc:Loc.t -> env -> evar_map -> type_constraint -> - evar_map * (Name.t Context.binder_annot * type_constraint * type_constraint) - val split_as_array : env -> evar_map -> type_constraint -> evar_map * type_constraint (** If the constraint can be made to look like [array A] return [A], @@ -51,3 +46,6 @@ val define_evar_as_sort : env -> evar_map -> existential -> evar_map * Sorts.t val pr_tycon : env -> evar_map -> type_constraint -> Pp.t +(** Used for bidi heuristic when typing lambdas. Transforms an applied + evar to an evar with bigger context (ie ?X e to ?X'@{y=e}). *) +val presplit : env -> evar_map -> EConstr.t -> evar_map * EConstr.t diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b9825b6a92..7597661ca8 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -925,7 +925,32 @@ struct let sigma, ty' = Coercion.inh_coerce_to_prod ?loc ~program_mode !!env sigma ty in sigma, Some ty' in - let sigma, (name',dom,rng) = split_tycon ?loc !!env sigma tycon' in + let sigma,name',dom,rng = + match tycon' with + | None -> sigma,Anonymous, None, None + | Some ty -> + let sigma, ty = Evardefine.presplit !!env sigma ty in + match EConstr.kind sigma ty with + | Prod (na,dom,rng) -> + sigma, na.binder_name, Some dom, Some rng + | Evar ev -> + (* define_evar_as_product works badly when impredicativity + is possible but not known (#12623). OTOH if we know we + are impredicative (typically Prop) we want to keep the + information when typing the body. *) + let s = Retyping.get_sort_of !!env sigma ty in + if Environ.is_impredicative_sort !!env s + || Evd.check_leq sigma (Univ.Universe.type1) (Sorts.univ_of_sort s) + then + let sigma, prod = define_evar_as_product !!env sigma ev in + let na,dom,rng = destProd sigma prod in + sigma, na.binder_name, Some dom, Some rng + else + sigma, Anonymous, None, None + | _ -> + (* XXX no error to allow later coercion? Not sure if possible with funclass *) + error_not_product ?loc !!env sigma ty + in let dom_valcon = valcon_of_tycon dom in let sigma, j = eval_type_pretyper self ~program_mode ~poly resolve_tc dom_valcon env sigma c1 in let name = {binder_name=name; binder_relevance=Sorts.relevance_of_sort j.utj_type} in @@ -934,7 +959,7 @@ struct let var',env' = push_rel ~hypnaming sigma var env in let sigma, j' = eval_pretyper self ~program_mode ~poly resolve_tc rng env' sigma c2 in let name = get_name var' in - let resj = judge_of_abstraction !!env (orelse_name name name'.binder_name) j j' in + let resj = judge_of_abstraction !!env (orelse_name name name') j j' in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon let pretype_prod self (name, bk, c1, c2) = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index aeb18ec322..08a6db5639 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -445,7 +445,7 @@ type state_reduction_function = let pr_state env sigma (tm,sk) = let open Pp in let pr c = Termops.Internal.print_constr_env env sigma c in - h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk) + h (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk) (*************************************) (*** Reduction Functions Operators ***) @@ -705,7 +705,7 @@ let rec whd_state_gen flags env sigma = let open Pp in let pr c = Termops.Internal.print_constr_env env sigma c in Feedback.msg_debug - (h 0 (str "<<" ++ pr x ++ + (h (str "<<" ++ pr x ++ str "|" ++ cut () ++ Stack.pr pr stack ++ str ">>")) in diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index af105f4d63..267f5e0b5f 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -467,7 +467,7 @@ let tag_var = tag Tag.variable let pr_record_body_gen pr l = spc () ++ prlist_with_sep pr_semicolon - (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr ltop c)) l + (fun (id, c) -> pr_reference id ++ str" :=" ++ pr ltop c) l let pr_forall n = keyword "forall" ++ pr_com_at n ++ spc () diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 43f70dfecc..dd372ecb0f 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -252,6 +252,9 @@ let pp_of_type env sigma ty = let pr_leconstr_env ?lax ?inctx ?scope env sigma t = Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_constr ?lax ?inctx ?scope env sigma t) +let pr_econstr_env ?lax ?inctx ?scope env sigma t = + Ppconstr.pr_constr_expr env sigma (Constrextern.extern_constr ?lax ?inctx ?scope env sigma t) + let pr_lconstr_env ?lax ?inctx ?scope env sigma c = pr_leconstr_env ?lax ?inctx ?scope env sigma (EConstr.of_constr c) @@ -660,3 +663,22 @@ let make_goal_map op np = let ng_to_og = make_goal_map_i op np in (*db_goal_map op np ng_to_og;*) ng_to_og + +let diff_proofs ~diff_opt ?old proof = + let pp_proof p = + let sigma, env = Proof.get_proof_context p in + let pprf = Proof.partial_proof p in + Pp.prlist_with_sep Pp.fnl (pr_econstr_env env sigma) pprf in + match diff_opt with + | DiffOff -> pp_proof proof + | _ -> begin + try + let n_pp = pp_proof proof in + let o_pp = match old with + | None -> Pp.mt() + | Some old -> pp_proof old in + let show_removed = Some (diff_opt = DiffRemoved) in + Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp + with + | Pp_diff.Diff_Failure msg -> Pp.str msg + end diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index ea64439456..6bdd7004fb 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -25,6 +25,10 @@ val write_color_enabled : bool -> unit (** true indicates that color output is enabled *) val color_enabled : unit -> bool +type diffOpt = DiffOff | DiffOn | DiffRemoved + +val string_to_diffs : string -> diffOpt + open Evd open Environ open Constr @@ -84,3 +88,5 @@ type hyp_info = { } val diff_hyps : string list list -> hyp_info CString.Map.t -> string list list -> hyp_info CString.Map.t -> Pp.t list + +val diff_proofs : diff_opt:diffOpt -> ?old:Proof.t -> Proof.t -> Pp.t diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 31bc698830..387f0f6f5f 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -720,7 +720,7 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma (* Pretty-print *) let pr_clenv clenv = - h 0 + h (str"TEMPL: " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templval.rebus ++ str" : " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templtyp.rebus ++ fnl () ++ pr_evar_map (Some 2) clenv.env clenv.evd) diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index a8088dae36..4f04b9fe1c 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -386,3 +386,8 @@ end module MakeQueue(T : Task) () = struct include Make(T) () end module MakeWorker(T : Task) () = struct include Make(T) () end + +exception RemoteException of Pp.t +let _ = CErrors.register_handler (function + | RemoteException ppcmd -> Some ppcmd + | _ -> None) diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli index cf174d0c93..a1fa6f7268 100644 --- a/stm/asyncTaskQueue.mli +++ b/stm/asyncTaskQueue.mli @@ -220,3 +220,6 @@ module MakeWorker(T : Task) () : sig val main_loop : unit -> unit end + +(** convenience exception to marshall to master *) +exception RemoteException of Pp.t diff --git a/stm/partac.ml b/stm/partac.ml new file mode 100644 index 0000000000..8232b017f9 --- /dev/null +++ b/stm/partac.ml @@ -0,0 +1,178 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \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 Pp + +let stm_pr_err s = Format.eprintf "%s] %s\n%!" (Spawned.process_id ()) s + +module TacTask : sig + + type output = (Constr.constr * UState.t) option + type task = { + t_state : Vernacstate.t; + t_assign : output Future.assignment -> unit; + t_ast : ComTactic.interpretable; + t_goalno : int; + t_goal : Goal.goal; + t_kill : unit -> unit; + t_name : string } + + include AsyncTaskQueue.Task with type task := task + +end = struct (* {{{ *) + + let forward_feedback { Feedback.doc_id = did; span_id = id; route; contents } = + Feedback.feedback ~did ~id ~route contents + + type output = (Constr.constr * UState.t) option + + type task = { + t_state : Vernacstate.t; + t_assign : output Future.assignment -> unit; + t_ast : ComTactic.interpretable; + t_goalno : int; + t_goal : Goal.goal; + t_kill : unit -> unit; + t_name : string } + + type request = { + r_state : Vernacstate.t option; + r_ast : ComTactic.interpretable; + r_goalno : int; + r_goal : Goal.goal; + r_name : string } + + type response = + | RespBuiltSubProof of (Constr.constr * UState.t) + | RespError of Pp.t + | RespNoProgress + + let name = ref "tacticworker" + let extra_env () = [||] + type competence = unit + type worker_status = Fresh | Old of competence + + let task_match _ _ = true + + (* run by the master, on a thread *) + let request_of_task age { t_state; t_ast; t_goalno; t_goal; t_name } = + Some { + r_state = if age <> Fresh then None else Some t_state; + r_ast = t_ast; + r_goalno = t_goalno; + r_goal = t_goal; + r_name = t_name } + + let use_response _ { t_assign; t_kill } resp = + match resp with + | RespBuiltSubProof o -> t_assign (`Val (Some o)); `Stay ((),[]) + | RespNoProgress -> + t_assign (`Val None); + t_kill (); + `Stay ((),[]) + | RespError msg -> + let e = (AsyncTaskQueue.RemoteException msg, Exninfo.null) in + t_assign (`Exn e); + t_kill (); + `Stay ((),[]) + + let on_marshal_error err { t_name } = + stm_pr_err ("Fatal marshal error: " ^ t_name ); + flush_all (); exit 1 + + let on_task_cancellation_or_expiration_or_slave_death = function + | Some { t_kill } -> t_kill () + | _ -> () + + let command_focus = Proof.new_focus_kind () + let focus_cond = Proof.no_cond command_focus + + let state = ref None + let receive_state = function + | None -> () + | Some st -> state := Some st + + let perform { r_state = st; r_ast = tactic; r_goal; r_goalno } = + receive_state st; + Vernacstate.unfreeze_interp_state (Option.get !state); + try + Vernacstate.LemmaStack.with_top (Option.get (Option.get !state).Vernacstate.lemmas) ~f:(fun pstate -> + let pstate = + Declare.Proof.map pstate ~f:(Proof.focus focus_cond () r_goalno) in + let pstate = + ComTactic.solve ~pstate + Goal_select.SelectAll ~info:None tactic ~with_end_tac:false in + let { Proof.sigma } = Declare.Proof.fold pstate ~f:Proof.data in + match Evd.(evar_body (find sigma r_goal)) with + | Evd.Evar_empty -> RespNoProgress + | Evd.Evar_defined t -> + let t = Evarutil.nf_evar sigma t in + let evars = Evarutil.undefined_evars_of_term sigma t in + if Evar.Set.is_empty evars then + let t = EConstr.Unsafe.to_constr t in + RespBuiltSubProof (t, Evd.evar_universe_context sigma) + else + CErrors.user_err ~hdr:"STM" + Pp.(str"The par: selector requires a tactic that makes no progress or fully" ++ + str" solves the goal and leaves no unresolved existential variables. The following" ++ + str" existentials remain unsolved: " ++ prlist (Termops.pr_existential_key sigma) (Evar.Set.elements evars)) + ) + with e when CErrors.noncritical e -> + RespError (CErrors.print e ++ spc() ++ str "(for subgoal "++int r_goalno ++ str ")") + + let name_of_task { t_name } = t_name + let name_of_request { r_name } = r_name + +end (* }}} *) + +module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) () + +let assign_tac ~abstract res : unit Proofview.tactic = + Proofview.(Goal.enter begin fun g -> + let gid = Goal.goal g in + let g_solution = + try List.assoc gid res + with Not_found -> CErrors.anomaly(str"Partac: wrong focus.") in + if not (Future.is_over g_solution) then + tclUNIT () + else + let open Notations in + match Future.join g_solution with + | Some (pt, uc) -> + let push_state ctx = + Proofview.tclEVARMAP >>= fun sigma -> + Proofview.Unsafe.tclEVARS (Evd.merge_universe_context sigma ctx) + in + (if abstract then Abstract.tclABSTRACT None else (fun x -> x)) + (push_state uc <*> Tactics.exact_no_check (EConstr.of_constr pt)) + | None -> tclUNIT () + end) + +let enable_par ~nworkers = ComTactic.set_par_implementation + (fun ~pstate ~info t_ast ~abstract ~with_end_tac -> + let t_state = Vernacstate.freeze_interp_state ~marshallable:true in + TaskQueue.with_n_workers nworkers CoqworkmgrApi.High (fun queue -> + Declare.Proof.map pstate ~f:(fun p -> + let open TacTask in + let results = (Proof.data p).Proof.goals |> CList.map_i (fun i g -> + let g_solution, t_assign = + Future.create_delegate ~name:(Printf.sprintf "subgoal %d" i) + (fun x -> x) in + TaskQueue.enqueue_task queue + ~cancel_switch:(ref false) + { t_state; t_assign; t_ast; + t_goalno = i; t_goal = g; t_name = Goal.uid g; + t_kill = (fun () -> TaskQueue.cancel_all queue) }; + g, g_solution) 1 in + TaskQueue.join queue; + let p,_,() = + Proof.run_tactic (Global.env()) + (assign_tac ~abstract results) p in + p))) diff --git a/stm/partac.mli b/stm/partac.mli new file mode 100644 index 0000000000..a206b2e5d8 --- /dev/null +++ b/stm/partac.mli @@ -0,0 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \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) *) +(************************************************************************) + +val enable_par : nworkers:int -> unit + +module TacTask : AsyncTaskQueue.Task diff --git a/stm/stm.ml b/stm/stm.ml index 4ca0c365bf..85f889c879 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -159,9 +159,9 @@ type cmd_t = { cids : Names.Id.t list; cblock : proof_block_name option; cqueue : [ `MainQueue - | `TacQueue of solving_tac * anon_abstracting_tac * AsyncTaskQueue.cancel_switch - | `QueryQueue of AsyncTaskQueue.cancel_switch - | `SkipQueue ] } + | `QueryQueue + | `SkipQueue ]; + cancel_switch : AsyncTaskQueue.cancel_switch; } type fork_t = aast * Vcs_.Branch.t * opacity_guarantee * Names.Id.t list type qed_t = { qast : aast; @@ -190,10 +190,10 @@ type step = type visit = { step : step; next : Stateid.t } let mkTransTac cast cblock cqueue = - Cmd { ctac = true; cast; cblock; cqueue; cids = []; ceff = false } + Cmd { ctac = true; cast; cblock; cqueue; cids = []; ceff = false; cancel_switch = ref false } let mkTransCmd cast cids ceff cqueue = - Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff } + Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff; cancel_switch = ref false } type cached_state = | EmptyState @@ -742,8 +742,7 @@ end = struct (* {{{ *) Stateid.Set.iter (fun id -> match (Vcs_aux.visit old_vcs id).step with | `Qed ({ fproof = Some (_, cancel_switch) }, _) - | `Cmd { cqueue = `TacQueue (_,_,cancel_switch) } - | `Cmd { cqueue = `QueryQueue cancel_switch } -> + | `Cmd { cancel_switch } -> cancel_switch := true | _ -> ()) erased_nodes; @@ -1222,11 +1221,6 @@ let record_pb_time ?loc proof_name time = hints := Aux_file.set !hints proof_name proof_build_time end -exception RemoteException of Pp.t -let _ = CErrors.register_handler (function - | RemoteException ppcmd -> Some ppcmd - | _ -> None) - (****************** proof structure for error recovery ************************) (******************************************************************************) @@ -1429,7 +1423,7 @@ end = struct (* {{{ *) RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } -> feedback (InProgress ~-1); let info = Stateid.add ~valid Exninfo.null e_error_at in - let e = (RemoteException e_msg, info) in + let e = (AsyncTaskQueue.RemoteException e_msg, info) in t_assign (`Exn e); `Stay(t_states,[States e_safe_states]) | _ -> assert false @@ -1440,7 +1434,7 @@ end = struct (* {{{ *) | Some (BuildProof { t_start = start; t_assign }) -> let s = "Worker dies or task expired" in let info = Stateid.add ~valid:start Exninfo.null start in - let e = (RemoteException (Pp.strbrk s), info) in + let e = (AsyncTaskQueue.RemoteException (Pp.strbrk s), info) in t_assign (`Exn e); execution_error start (Pp.strbrk s); feedback (InProgress ~-1) @@ -1792,225 +1786,6 @@ end = struct (* {{{ *) end (* }}} *) -and TacTask : sig - - type output = (Constr.constr * UState.t) option - type task = { - t_state : Stateid.t; - t_state_fb : Stateid.t; - t_assign : output Future.assignment -> unit; - t_ast : int * aast; - t_goal : Goal.goal; - t_kill : unit -> unit; - t_name : string } - - include AsyncTaskQueue.Task with type task := task - -end = struct (* {{{ *) - - type output = (Constr.constr * UState.t) option - - let forward_feedback msg = Hooks.(call forward_feedback msg) - - type task = { - t_state : Stateid.t; - t_state_fb : Stateid.t; - t_assign : output Future.assignment -> unit; - t_ast : int * aast; - t_goal : Goal.goal; - t_kill : unit -> unit; - t_name : string } - - type request = { - r_state : Stateid.t; - r_state_fb : Stateid.t; - r_document : VCS.vcs option; - r_ast : int * aast; - r_goal : Goal.goal; - r_name : string } - - type response = - | RespBuiltSubProof of (Constr.constr * UState.t) - | RespError of Pp.t - | RespNoProgress - - let name = ref "tacticworker" - let extra_env () = [||] - type competence = unit - type worker_status = Fresh | Old of competence - - let task_match _ _ = true - - (* run by the master, on a thread *) - let request_of_task age { t_state; t_state_fb; t_ast; t_goal; t_name } = - try Some { - r_state = t_state; - r_state_fb = t_state_fb; - r_document = - if age <> Fresh then None - else Some (VCS.slice ~block_start:t_state ~block_stop:t_state); - r_ast = t_ast; - r_goal = t_goal; - r_name = t_name } - with VCS.Expired -> None - - let use_response _ { t_assign; t_state; t_state_fb; t_kill } resp = - match resp with - | RespBuiltSubProof o -> t_assign (`Val (Some o)); `Stay ((),[]) - | RespNoProgress -> - t_assign (`Val None); - t_kill (); - `Stay ((),[]) - | RespError msg -> - let e = (RemoteException msg, Exninfo.null) in - t_assign (`Exn e); - t_kill (); - `Stay ((),[]) - - let on_marshal_error err { t_name } = - stm_pr_err ("Fatal marshal error: " ^ t_name ); - flush_all (); exit 1 - - let on_task_cancellation_or_expiration_or_slave_death = function - | Some { t_kill } -> t_kill () - | _ -> () - - let command_focus = Proof.new_focus_kind () - let focus_cond = Proof.no_cond command_focus - - let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } = - Option.iter VCS.restore vcs; - try - Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:false id; - State.purify (fun () -> - let Proof.{sigma=sigma0} = Proof.data (PG_compat.give_me_the_proof ()) in - let g = Evd.find sigma0 r_goal in - let is_ground c = Evarutil.is_ground_term sigma0 c in - if not ( - is_ground Evd.(evar_concl g) && - List.for_all (Context.Named.Declaration.for_all is_ground) - Evd.(evar_context g)) - then - CErrors.user_err ~hdr:"STM" Pp.(strbrk("The par: goal selector does not support goals with existential variables")) - else begin - let (i, ast) = r_ast in - PG_compat.map_proof (fun p -> Proof.focus focus_cond () i p); - (* STATE SPEC: - * - start : id - * - return: id - * => captures state id in a future closure, which will - discard execution state but for the proof + univs. - *) - let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_vernac_interp r_state_fb st ast); - let Proof.{sigma} = Proof.data (PG_compat.give_me_the_proof ()) in - match Evd.(evar_body (find sigma r_goal)) with - | Evd.Evar_empty -> RespNoProgress - | Evd.Evar_defined t -> - let t = Evarutil.nf_evar sigma t in - let evars = Evarutil.undefined_evars_of_term sigma t in - if Evar.Set.is_empty evars then - let t = EConstr.Unsafe.to_constr t in - RespBuiltSubProof (t, Evd.evar_universe_context sigma) - else - CErrors.user_err ~hdr:"STM" - Pp.(str"The par: selector requires a tactic that makes no progress or fully" ++ - str" solves the goal and leaves no unresolved existential variables. The following" ++ - str" existentials remain unsolved: " ++ prlist (Termops.pr_existential_key sigma) (Evar.Set.elements evars)) - end) () - with e when CErrors.noncritical e -> - RespError (CErrors.print e ++ spc() ++ str "(for subgoal "++int (fst r_ast) ++ str ")") - - let name_of_task { t_name } = t_name - let name_of_request { r_name } = r_name - -end (* }}} *) - -and Partac : sig - - val vernac_interp : - solve:bool -> abstract:bool -> cancel_switch:AsyncTaskQueue.cancel_switch -> - int -> CoqworkmgrApi.priority -> Stateid.t -> Stateid.t -> aast -> unit - -end = struct (* {{{ *) - - module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) () - - let stm_fail ~st fail f = - if fail then - Vernacinterp.with_fail ~st f - else - f () - - let vernac_interp ~solve ~abstract ~cancel_switch nworkers priority safe_id id - { indentation; verbose; expr = e; strlen } : unit - = - let cl, time, batch, fail = - let rec find ~time ~batch ~fail cl = match cl with - | ControlTime batch :: cl -> find ~time:true ~batch ~fail cl - | ControlRedirect _ :: cl -> find ~time ~batch ~fail cl - | ControlFail :: cl -> find ~time ~batch ~fail:true cl - | cl -> cl, time, batch, fail in - find ~time:false ~batch:false ~fail:false e.CAst.v.control in - let e = CAst.map (fun cmd -> { cmd with control = cl }) e in - let st = Vernacstate.freeze_interp_state ~marshallable:false in - stm_fail ~st fail (fun () -> - (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () -> - TaskQueue.with_n_workers nworkers priority (fun queue -> - PG_compat.map_proof (fun p -> - let Proof.{goals} = Proof.data p in - let open TacTask in - let res = CList.map_i (fun i g -> - let f, assign = - Future.create_delegate - ~name:(Printf.sprintf "subgoal %d" i) - (State.exn_on id ~valid:safe_id) in - let t_ast = (i, { indentation; verbose; expr = e; strlen }) in - let t_name = Goal.uid g in - TaskQueue.enqueue_task queue - { t_state = safe_id; t_state_fb = id; - t_assign = assign; t_ast; t_goal = g; t_name; - t_kill = (fun () -> if solve then TaskQueue.cancel_all queue) } - ~cancel_switch; - g,f) - 1 goals in - TaskQueue.join queue; - let assign_tac : unit Proofview.tactic = - Proofview.(Goal.enter begin fun g -> - let gid = Goal.goal g in - let f = - try List.assoc gid res - with Not_found -> CErrors.anomaly(str"Partac: wrong focus.") in - if not (Future.is_over f) then - (* One has failed and cancelled the others, but not this one *) - if solve then Tacticals.New.tclZEROMSG - (str"Interrupted by the failure of another goal") - else tclUNIT () - else - let open Notations in - match Future.join f with - | Some (pt, uc) -> - let sigma, env = PG_compat.get_current_context () in - let push_state ctx = - Proofview.tclEVARMAP >>= fun sigma -> - Proofview.Unsafe.tclEVARS (Evd.merge_universe_context sigma ctx) - in - stm_pperr_endline (fun () -> hov 0 ( - str"g=" ++ int (Evar.repr gid) ++ spc () ++ - str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++ - str"uc=" ++ Termops.pr_evar_universe_context uc)); - (if abstract then Abstract.tclABSTRACT None else (fun x -> x)) - (push_state uc <*> - Tactics.exact_no_check (EConstr.of_constr pt)) - | None -> - if solve then Tacticals.New.tclSOLVE [] else tclUNIT () - end) - in - let p,_,() = Proof.run_tactic (Global.env()) assign_tac p in - p))) ()) - -end (* }}} *) - and QueryTask : sig type task = { t_where : Stateid.t; t_for : Stateid.t ; t_what : aast } @@ -2361,15 +2136,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = ), cache, true | `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () -> reach view.next), cache, true - | `Cmd { cast = x; cqueue = `TacQueue (solve,abstract,cancel_switch); cblock } -> - (fun () -> - resilient_tactic id cblock (fun () -> - reach ~cache:true view.next; - Partac.vernac_interp ~solve ~abstract ~cancel_switch - !cur_opt.async_proofs_n_tacworkers - !cur_opt.async_proofs_worker_priority view.next id x) - ), cache, true - | `Cmd { cast = x; cqueue = `QueryQueue cancel_switch } + | `Cmd { cast = x; cqueue = `QueryQueue; cancel_switch } when async_proofs_is_master !cur_opt -> (fun () -> reach view.next; Query.vernac_interp ~cancel_switch view.next id x @@ -2377,7 +2144,6 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | `Cmd { cast = x; ceff = eff; ctac = true; cblock } -> (fun () -> resilient_tactic id cblock (fun () -> reach view.next; - (* State resulting from reach *) let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x) ) @@ -2588,6 +2354,7 @@ let doc_type_module_name (std : stm_doc_type) = let init_core () = if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true; + if !Flags.async_proofs_worker_id = "master" then Partac.enable_par ~nworkers:!cur_opt.async_proofs_n_tacworkers; State.register_root_state () let dirpath_of_file f = @@ -2938,12 +2705,9 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) VCS.set_parsing_state id head_parsing; Backtrack.record (); `Ok - | VtProofStep { parallel; proof_block_detection = cblock } -> + | VtProofStep { proof_block_detection = cblock } -> let id = VCS.new_node ~id:newtip proof_mode () in - let queue = - match parallel with - | `Yes(solve,abstract) -> `TacQueue (solve, abstract, ref false) - | `No -> `MainQueue in + let queue = `MainQueue in VCS.commit id (mkTransTac x cblock queue); (* Static proof block detection delayed until an error really occurs. If/when and UI will make something useful with this piece of info, diff --git a/stm/stm.mli b/stm/stm.mli index 9780c96512..097bcbe0ca 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -195,7 +195,6 @@ val set_perspective : doc:doc -> Stateid.t list -> unit (** workers **************************************************************** **) module ProofTask : AsyncTaskQueue.Task -module TacTask : AsyncTaskQueue.Task module QueryTask : AsyncTaskQueue.Task (** document structure customization *************************************** **) diff --git a/stm/stm.mllib b/stm/stm.mllib index 4b254e8113..831369625f 100644 --- a/stm/stm.mllib +++ b/stm/stm.mllib @@ -6,6 +6,7 @@ WorkerPool Vernac_classifier CoqworkmgrApi AsyncTaskQueue +Partac Stm ProofBlockDelimiter Vio_checking diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f89fb9f52d..3996c64b67 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -15,11 +15,6 @@ open CAst open Vernacextend open Vernacexpr -let string_of_parallel = function - | `Yes (solve,abs) -> - "par" ^ if solve then "solve" else "" ^ if abs then "abs" else "" - | `No -> "" - let string_of_vernac_when = function | VtLater -> "Later" | VtNow -> "Now" @@ -30,9 +25,8 @@ let string_of_vernac_classification = function | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)" | VtQed (VtKeep (VtKeepOpaque | VtKeepDefined)) -> "Qed(keep)" | VtQed VtDrop -> "Qed(drop)" - | VtProofStep { parallel; proof_block_detection } -> - "ProofStep " ^ string_of_parallel parallel ^ - Option.default "" proof_block_detection + | VtProofStep { proof_block_detection } -> + "ProofStep " ^ Option.default "" proof_block_detection | VtQuery -> "Query" | VtMeta -> "Meta " | VtProofMode _ -> "Proof Mode" @@ -80,12 +74,11 @@ let classify_vernac e = | VernacCheckGuard | VernacUnfocused | VernacSolveExistential _ -> - VtProofStep { parallel = `No; proof_block_detection = None } + VtProofStep { proof_block_detection = None } | VernacBullet _ -> - VtProofStep { parallel = `No; proof_block_detection = Some "bullet" } + VtProofStep { proof_block_detection = Some "bullet" } | VernacEndSubproof -> - VtProofStep { parallel = `No; - proof_block_detection = Some "curly" } + VtProofStep { proof_block_detection = Some "curly" } (* StartProof *) | VernacDefinition ((DoDischarge,_),({v=i},_),ProveBody _) -> VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i) @@ -213,7 +206,7 @@ let classify_vernac e = (match static_classifier ~atts:v.attrs v.expr with | VtQuery | VtProofStep _ | VtSideff _ | VtMeta as x -> x - | VtQed _ -> VtProofStep { parallel = `No; proof_block_detection = None } + | VtQed _ -> VtProofStep { proof_block_detection = None } | VtStartProof _ | VtProofMode _ -> VtQuery) else static_classifier ~atts:v.attrs v.expr diff --git a/tactics/cbn.ml b/tactics/cbn.ml index 8f0966a486..0b13f4763a 100644 --- a/tactics/cbn.ml +++ b/tactics/cbn.ml @@ -543,7 +543,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let open Pp in let pr c = Termops.Internal.print_constr_env env sigma c in Feedback.msg_debug - (h 0 (str "<<" ++ pr x ++ + (h (str "<<" ++ pr x ++ str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++ str "|" ++ cut () ++ Stack.pr pr stack ++ str ">>")) diff --git a/test-suite/bugs/closed/bug_12414.v b/test-suite/bugs/closed/bug_12414.v new file mode 100644 index 0000000000..50b4b86eff --- /dev/null +++ b/test-suite/bugs/closed/bug_12414.v @@ -0,0 +1,13 @@ +Set Universe Polymorphism. +Set Printing Universes. +Inductive list {T} : Type := | cons (t : T) : list -> list. (* who needs nil anyway? *) +Arguments list : clear implicits. + +Fixpoint map {A B} (f: A -> B) (l : list A) : list B := + let '(cons t l) := l in cons (f t) (map f l). +About map@{_ _}. +(* Two universes, as expected. *) + +Definition map_Set@{} {A B : Set} := @map A B. + +Definition map_Prop@{} {A B : Prop} := @map A B. diff --git a/test-suite/bugs/closed/bug_12623.v b/test-suite/bugs/closed/bug_12623.v new file mode 100644 index 0000000000..9fdcb94e0c --- /dev/null +++ b/test-suite/bugs/closed/bug_12623.v @@ -0,0 +1,18 @@ +Set Universe Polymorphism. + +Axiom M : Type -> Prop. +Axiom raise : forall {T}, M T. + +Inductive goal : Type := +| AHyp : forall {A : Type}, goal. + +Definition gtactic@{u u0} := goal@{u} -> M@{u0} (False). + +Class Seq (C : Type) := + seq : C -> gtactic. +Arguments seq {C _} _. + +Instance seq_one : Seq@{Set _ _} (gtactic) := fun t2 => fun g => raise. + +Definition x1 : gtactic := @seq@{_ _ _} _ _ (fun g : goal => raise). +Definition x2 : gtactic := @seq@{_ _ _} _ seq_one (fun g : goal => raise). diff --git a/test-suite/bugs/closed/bug_13086.v b/test-suite/bugs/closed/bug_13086.v new file mode 100644 index 0000000000..75f842b1cf --- /dev/null +++ b/test-suite/bugs/closed/bug_13086.v @@ -0,0 +1,11 @@ +Unset Universe Checking. + +Definition bad1@{|Set < Set} := Prop. + +Set Universe Polymorphism. +Axiom ax : Type. +Inductive I@{u} : Prop := foo : ax@{u} -> I. + +Definition bad2@{v} (x:I@{v}) : I@{Set} := x. + +Definition vsdvds (f : (Prop -> Prop) -> Prop) (x : Set -> Prop) := f x. diff --git a/test-suite/bugs/closed/bug_5197.v b/test-suite/bugs/closed/bug_5197.v index 0c236e12ad..00b9e9bd9d 100644 --- a/test-suite/bugs/closed/bug_5197.v +++ b/test-suite/bugs/closed/bug_5197.v @@ -20,11 +20,11 @@ Definition Typeᶠ : TYPE := {| rel := fun _ A => (forall ω : Ω, A ω) -> Type; |}. Set Printing Universes. -Fail Definition Typeᵇ : El Typeᶠ := +Definition Typeᵇ : El Typeᶠ := mkPack _ _ (fun w => Type) (fun w A => (forall ω, A ω) -> Type). -Definition Typeᵇ : El Typeᶠ := - mkPack _ (fun _ (A : Ω -> Type) => (forall ω : Ω, A ω) -> _) (fun w => Type) (fun w A => (forall ω, A ω) -> Type). +(* Definition Typeᵇ : El Typeᶠ := *) +(* mkPack _ (fun _ (A : Ω -> Type) => (forall ω : Ω, A ω) -> _) (fun w => Type) (fun w A => (forall ω, A ω) -> Type). *) (** Bidirectional typechecking helps here *) Require Import Program.Tactics. diff --git a/test-suite/ide/proof-diffs.fake b/test-suite/ide/proof-diffs.fake new file mode 100644 index 0000000000..594ebced23 --- /dev/null +++ b/test-suite/ide/proof-diffs.fake @@ -0,0 +1,10 @@ +ADD { Goal True /\ False /\ True = False. } +ADD { split. } +GOALS +ADD here { split. } +GOALS +PDIFF here +ADD there { auto. } +GOALS +PDIFF there +ADD { Admitted. } diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index abada44da7..bd22d45059 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -231,16 +231,13 @@ fun l : list nat => match l with : list nat -> list nat Arguments foo _%list_scope -Notation -"'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope -(default interpretation) -"'exists' ! x .. y , p" := ex - (unique - (fun x => .. (ex (unique (fun y => p))) ..)) -: type_scope (default interpretation) -Notation -"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope -(default interpretation) +Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) + : type_scope (default interpretation) +Notation "'exists' ! x .. y , p" := + (ex (unique (fun x => .. (ex (unique (fun y => p))) ..))) : type_scope + (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope + (default interpretation) 1 subgoal ============================ diff --git a/test-suite/output/bug_12908.out b/test-suite/output/bug_12908.out index fca6dde704..54c4f98422 100644 --- a/test-suite/output/bug_12908.out +++ b/test-suite/output/bug_12908.out @@ -1,2 +1,7 @@ forall m n : nat, m * n = (2 * m * n)%nat : Prop +File "stdin", line 11, characters 0-31: +Warning: Notation "_ * _" was already used in scope nat_scope. +[notation-overridden,parsing] +forall m n : nat, m * n = Nat.mul (Nat.mul 2 m) n + : Prop diff --git a/test-suite/output/bug_12908.v b/test-suite/output/bug_12908.v index 558c9f9f6a..6f7be22fa0 100644 --- a/test-suite/output/bug_12908.v +++ b/test-suite/output/bug_12908.v @@ -1,6 +1,13 @@ Definition mult' m n := 2 * m * n. + Module A. (* Test hiding of a scoped notation by a lonely notation *) Infix "*" := mult'. Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n. End A. + +Module B. +(* Test that an overriden scoped notation is deactivated *) +Infix "*" := mult' : nat_scope. +Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n. +End B. diff --git a/test-suite/output/bug_13112.out b/test-suite/output/bug_13112.out new file mode 100644 index 0000000000..a8a98d6b68 --- /dev/null +++ b/test-suite/output/bug_13112.out @@ -0,0 +1,4 @@ +0 + 0 + : nat +HI + : nat diff --git a/test-suite/output/bug_13112.v b/test-suite/output/bug_13112.v new file mode 100644 index 0000000000..9fee5e09d8 --- /dev/null +++ b/test-suite/output/bug_13112.v @@ -0,0 +1,5 @@ +Reserved Notation "'HI'". +Notation "'HI'" := (O + O) (only parsing). +Check HI. (* 0 + 0 : nat *) +Notation "'HI'" := (O + O) (only printing). +Check HI. (* 0 + 0 : nat *) diff --git a/test-suite/output/bug_9180.out b/test-suite/output/bug_9180.out index ed4892b389..f035d0252a 100644 --- a/test-suite/output/bug_9180.out +++ b/test-suite/output/bug_9180.out @@ -1,4 +1,3 @@ -Notation -"n .+1" := S n : nat_scope (default interpretation) +Notation "n .+1" := (S n) : nat_scope (default interpretation) forall x : nat, x.+1 = x.+1 : Prop diff --git a/test-suite/output/bug_9682.out b/test-suite/output/bug_9682.out new file mode 100644 index 0000000000..45d9e4cad1 --- /dev/null +++ b/test-suite/output/bug_9682.out @@ -0,0 +1,9 @@ +mmatch 1 + 2 + 3 + 4 + 5 + 6 in nat as x +return M (x = x) with +| 1 +end + : unit +# + : True +## + : True diff --git a/test-suite/output/bug_9682.v b/test-suite/output/bug_9682.v new file mode 100644 index 0000000000..fa30d323ef --- /dev/null +++ b/test-suite/output/bug_9682.v @@ -0,0 +1,28 @@ +Declare Scope blafu. +Delimit Scope blafu with B. +Axiom DoesNotMatch : Type. +Axiom consumer : forall {A} (B : A -> Type) (E:Type) (x : A) (ls : list nat), unit. + +Notation "| p1 | .. | pn" := (@cons _ p1 .. (@cons _ pn nil) ..) (at level 91) : blafu. +Notation "'mmatch_do_not_write' x 'in' T 'as' y 'return' 'M' p 'with_do_not_write' ls" := + (@consumer _ (fun y : T => p%type) DoesNotMatch x ls%B) + (at level 200, ls at level 91, only parsing). +Notation "'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" := + (mmatch_do_not_write x in T as y return M p with_do_not_write ls) + (at level 200, ls at level 91, p at level 10, only parsing). +(* This should not gives a warning *) +Notation "'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" := + (@consumer _ (fun y : T => p%type) DoesNotMatch x ls%B) + (at level 200, ls at level 91, p at level 10, only printing, + format "'[ ' mmatch '/' x ']' '/' '[ ' in '/' T ']' '/' '[ ' as '/' y ']' '/' '[ ' return M p ']' with '//' '[' ls ']' '//' end" + ). +(* Check use of "mmatch" *) +Check (mmatch 1 + 2 + 3 + 4 + 5 + 6 in nat as x return M (x = x) with | 1 end). + +(* 2nd example *) +Notation "#" := I (at level 0, only parsing). +Notation "#" := I (at level 0, only printing). +Check #. +Notation "##" := I (at level 0, only printing). +Notation "##" := I (at level 0, only parsing). +Check ##. diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out index 473db2d312..93d9d6cf7b 100644 --- a/test-suite/output/locate.out +++ b/test-suite/output/locate.out @@ -1,3 +1,2 @@ -Notation -"b1 && b2" := if b1 then b2 else false (default interpretation) -"x && y" := andb x y : bool_scope +Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation) +Notation "x && y" := (andb x y) : bool_scope diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 9ab8ace39e..0796b507a1 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -457,5 +457,10 @@ Module ObligationRegression. (** Test for a regression encountered when fixing obligations for stronger restriction of universe context. *) Require Import CMorphisms. - Check trans_co_eq_inv_arrow_morphism@{_ _ _ _ _ _ _ _}. + Check trans_co_eq_inv_arrow_morphism@{_ _ _ _ _ _ _}. End ObligationRegression. + +Axiom poly@{i} : forall(A : Type@{i}) (a : A), unit. + +Definition nonpoly := @poly True Logic.I. +Definition check := nonpoly@{}. diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index f35da63fd6..e8a036bbb0 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -1401,8 +1401,8 @@ Definition mem T (pT : predType T) : pT -> mem_pred T := let: PredType toP := pT in fun A => Mem [eta toP A]. Arguments mem {T pT} A : rename, simpl never. -Notation "x \in A" := (in_mem x (mem A)) : bool_scope. -Notation "x \in A" := (in_mem x (mem A)) : bool_scope. +Notation "x \in A" := (in_mem x (mem A)) (only parsing) : bool_scope. +Notation "x \in A" := (in_mem x (mem A)) (only printing) : bool_scope. Notation "x \notin A" := (~~ (x \in A)) : bool_scope. Notation "A =i B" := (eq_mem (mem A) (mem B)) : type_scope. Notation "{ 'subset' A <= B }" := (sub_mem (mem A) (mem B)) : type_scope. @@ -1573,9 +1573,12 @@ Arguments has_quality n {T}. Lemma qualifE n T p x : (x \in @Qualifier n T p) = p x. Proof. by []. Qed. -Notation "x \is A" := (x \in has_quality 0 A) : bool_scope. -Notation "x \is 'a' A" := (x \in has_quality 1 A) : bool_scope. -Notation "x \is 'an' A" := (x \in has_quality 2 A) : bool_scope. +Notation "x \is A" := (x \in has_quality 0 A) (only parsing) : bool_scope. +Notation "x \is A" := (x \in has_quality 0 A) (only printing) : bool_scope. +Notation "x \is 'a' A" := (x \in has_quality 1 A) (only parsing) : bool_scope. +Notation "x \is 'a' A" := (x \in has_quality 1 A) (only printing) : bool_scope. +Notation "x \is 'an' A" := (x \in has_quality 2 A) (only parsing) : bool_scope. +Notation "x \is 'an' A" := (x \in has_quality 2 A) (only printing) : bool_scope. Notation "x \isn't A" := (x \notin has_quality 0 A) : bool_scope. Notation "x \isn't 'a' A" := (x \notin has_quality 1 A) : bool_scope. Notation "x \isn't 'an' A" := (x \notin has_quality 2 A) : bool_scope. diff --git a/topbin/coqtacticworker_bin.ml b/topbin/coqtacticworker_bin.ml index 252c8faa05..706554e025 100644 --- a/topbin/coqtacticworker_bin.ml +++ b/topbin/coqtacticworker_bin.ml @@ -8,6 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) () +module W = AsyncTaskQueue.MakeWorker(Partac.TacTask) () let () = WorkerLoop.start ~init:W.init_stdout ~loop:W.main_loop "coqtacticworker" diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index eb386ea3e8..d587e57fd8 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -508,6 +508,7 @@ let parse_args ~help ~init arglist : t * string list = |"-color" -> set_color oval (next ()) |"-config"|"--config" -> set_query oval PrintConfig |"-debug" -> Coqinit.set_debug (); oval + |"-xml-debug" -> Flags.xml_debug := true; Coqinit.set_debug (); oval |"-diffs" -> add_set_option oval Proof_diffs.opt_name @@ Stm.OptionSet (Some (next ())) |"-stm-debug" -> Stm.stm_debug := true; oval diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 88924160ff..6460378edc 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -371,41 +371,13 @@ let exit_on_error = declare_bool_option_and_ref ~depr:false ~key:["Coqtop";"Exit";"On";"Error"] ~value:false -(* XXX: This is duplicated with Vernacentries.show_proof , at some - point we should consolidate the code *) -let show_proof_diff_to_pp pstate = - let p = Option.get pstate in - let sigma, env = Proof.get_proof_context p in - let pprf = Proof.partial_proof p in - Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf - -let show_proof_diff_cmd ~state removed = +let show_proof_diff_cmd ~state diff_opt = let open Vernac.State in - try - let n_pp = show_proof_diff_to_pp state.proof in - if true (*Proof_diffs.show_diffs ()*) then - let doc = state.doc in - let oproof = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in - try - let o_pp = show_proof_diff_to_pp oproof in - let tokenize_string = Proof_diffs.tokenize_string in - let show_removed = Some removed in - Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp - with - | Proof.NoSuchGoal _ - | Option.IsNone -> n_pp - | Pp_diff.Diff_Failure msg -> begin - (* todo: print the unparsable string (if we know it) *) - Feedback.msg_warning Pp.(str ("Diff failure: " ^ msg) ++ cut() - ++ str "Showing results without diff highlighting" ); - n_pp - end - else - n_pp - with - | Proof.NoSuchGoal _ - | Option.IsNone -> - CErrors.user_err (str "No goals to show.") + match state.proof with + | None -> CErrors.user_err (str "No proofs to diff.") + | Some proof -> + let old = Stm.get_prev_proof ~doc:state.doc state.sid in + Proof_diffs.diff_proofs ~diff_opt ?old proof let process_toplevel_command ~state stm = let open Vernac.State in @@ -444,12 +416,12 @@ let process_toplevel_command ~state stm = Feedback.msg_notice (v 0 (goal ++ evars)); state - | VernacShowProofDiffs removed -> + | VernacShowProofDiffs diff_opt -> (* We print nothing if there are no goals left *) if not (Proof_diffs.color_enabled ()) then CErrors.user_err Pp.(str "Show Proof Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".") else - let out = show_proof_diff_cmd ~state removed in + let out = show_proof_diff_cmd ~state diff_opt in Feedback.msg_notice out; state diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index 1902103a3e..ef79f4562e 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -20,7 +20,7 @@ type vernac_toplevel = | VernacQuit | VernacControl of vernac_control | VernacShowGoal of { gid : int; sid: int } - | VernacShowProofDiffs of bool + | VernacShowProofDiffs of Proof_diffs.diffOpt module Toplevel_ : sig val vernac_toplevel : vernac_toplevel option Entry.t @@ -52,7 +52,8 @@ GRAMMAR EXTEND Gram | test_show_goal; IDENT "Show"; IDENT "Goal"; gid = natural; IDENT "at"; sid = natural; "." -> { Some (VernacShowGoal {gid; sid}) } | IDENT "Show"; IDENT "Proof"; IDENT "Diffs"; removed = OPT [ IDENT "removed" -> { () } ]; "." -> - { Some (VernacShowProofDiffs (removed <> None)) } + { Some (VernacShowProofDiffs + (if removed = None then Proof_diffs.DiffOn else Proof_diffs.DiffRemoved)) } | cmd = Pvernac.Vernac_.main_entry -> { match cmd with | None -> None diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 732ad05b26..6fb5f821ee 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -72,6 +72,7 @@ let print_usage_common co command = \n -init-file f set the rcfile to f\ \n -bt print backtraces (requires configure debug flag)\ \n -debug debug mode (implies -bt)\ +\n -xml-debug debug mode and print XML messages to/from coqide\ \n -diffs (on|off|removed) highlight differences between proof steps\ \n -stm-debug STM debug mode (will trace every transaction)\ \n -noglob do not dump globalizations\ diff --git a/vernac/comTactic.ml b/vernac/comTactic.ml new file mode 100644 index 0000000000..8a9a412362 --- /dev/null +++ b/vernac/comTactic.ml @@ -0,0 +1,82 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \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 Goptions + +module Dyn = Dyn.Make() + +module DMap = Dyn.Map(struct type 'a t = 'a -> unit Proofview.tactic end) + +let interp_map = ref DMap.empty + +type 'a tactic_interpreter = 'a Dyn.tag +type interpretable = I : 'a tactic_interpreter * 'a -> interpretable + +let register_tactic_interpreter na f = + let t = Dyn.create na in + interp_map := DMap.add t f !interp_map; + t + +let interp_tac (I (tag,t)) = + let f = DMap.find tag !interp_map in + f t + +type parallel_solver = + pstate:Declare.Proof.t -> + info:int option -> + interpretable -> + abstract:bool -> + with_end_tac:bool -> + Declare.Proof.t + +let print_info_trace = + declare_intopt_option_and_ref ~depr:false ~key:["Info" ; "Level"] + +let solve_core ~pstate n ~info t ~with_end_tac:b = + let pstate, status = Declare.Proof.map_fold_endline ~f:(fun etac p -> + let with_end_tac = if b then Some etac else None in + let info = Option.append info (print_info_trace ()) in + let (p,status) = Proof.solve n info t ?with_end_tac p in + (* in case a strict subtree was completed, + go back to the top of the prooftree *) + let p = Proof.maximal_unfocus Vernacentries.command_focus p in + p,status) pstate in + if not status then Feedback.feedback Feedback.AddedAxiom; + pstate + +let solve ~pstate n ~info t ~with_end_tac = + let t = interp_tac t in + solve_core ~pstate n ~info t ~with_end_tac + +let check_par_applicable pstate = + Declare.Proof.fold pstate ~f:(fun p -> + (Proof.data p).Proof.goals |> List.iter (fun goal -> + let is_ground = + let { Proof.sigma = sigma0 } = Declare.Proof.fold pstate ~f:Proof.data in + let g = Evd.find sigma0 goal in + let concl, hyps = Evd.evar_concl g, Evd.evar_context g in + Evarutil.is_ground_term sigma0 concl && + List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0)) hyps in + if not is_ground then + CErrors.user_err + Pp.(strbrk("The par: goal selector does not support goals with existential variables")))) + +let par_implementation = ref (fun ~pstate ~info t ~abstract ~with_end_tac -> + let t = interp_tac t in + let t = Proofview.Goal.enter (fun _ -> + if abstract then Abstract.tclABSTRACT None ~opaque:true t else t) + in + solve_core ~pstate Goal_select.SelectAll ~info t ~with_end_tac) + +let set_par_implementation f = par_implementation := f + +let solve_parallel ~pstate ~info t ~abstract ~with_end_tac = + check_par_applicable pstate; + !par_implementation ~pstate ~info t ~abstract ~with_end_tac diff --git a/vernac/comTactic.mli b/vernac/comTactic.mli new file mode 100644 index 0000000000..f1a75e1b6a --- /dev/null +++ b/vernac/comTactic.mli @@ -0,0 +1,47 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \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) *) +(************************************************************************) + +(** Tactic interpreters have to register their interpretation function *) +type 'a tactic_interpreter +type interpretable = I : 'a tactic_interpreter * 'a -> interpretable + +(** ['a] should be marshallable if ever used with [par:] *) +val register_tactic_interpreter : + string -> ('a -> unit Proofview.tactic) -> 'a tactic_interpreter + +(** Entry point for toplevel tactic expression execution. It calls Proof.solve + after having interpreted the tactic, and after the tactic runs it + unfocus as much as needed to put a goal under focus. *) +val solve : + pstate:Declare.Proof.t -> + Goal_select.t -> + info:int option -> + interpretable -> + with_end_tac:bool -> + Declare.Proof.t + +(** [par: tac] runs tac on all goals, possibly in parallel using a worker pool. + If tac is [abstract tac1], then [abstract] is passed + explicitly to the solver and [tac1] passed to worker since it is up to + master to opacify the sub proofs produced by the workers. *) +type parallel_solver = + pstate:Declare.Proof.t -> + info:int option -> + interpretable -> + abstract:bool -> (* the tactic result has to be opacified as per abstract *) + with_end_tac:bool -> + Declare.Proof.t + +(** Entry point when the goal selector is par: *) +val solve_parallel : parallel_solver + +(** By default par: is implemented with all: (sequential). + The STM and LSP document manager provide "more parallel" implementations *) +val set_par_implementation : parallel_solver -> unit diff --git a/vernac/himsg.ml b/vernac/himsg.ml index c16eaac516..a9de01bfd0 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -831,7 +831,7 @@ let pr_constraints printenv env sigma evars cstrs = (fun (ev, evi) -> fnl () ++ pr_existential_key sigma ev ++ str " : " ++ pr_leconstr_env env' sigma evi.evar_concl ++ fnl ()) l in - h 0 (pe ++ evs ++ pr_evar_constraints sigma cstrs) + h (pe ++ evs ++ pr_evar_constraints sigma cstrs) else let filter evk _ = Evar.Map.mem evk evars in pr_evar_map_filter ~with_univs:false filter env sigma @@ -973,8 +973,8 @@ let explain_not_match_error = function (UContext.instance uctx) (UContext.constraints uctx) in - str "incompatible polymorphic binders: got" ++ spc () ++ h 0 (pr_auctx got) ++ spc() ++ - str "but expected" ++ spc() ++ h 0 (pr_auctx expect) ++ + str "incompatible polymorphic binders: got" ++ spc () ++ h (pr_auctx got) ++ spc() ++ + str "but expected" ++ spc() ++ h (pr_auctx expect) ++ (if not (Int.equal (AUContext.size got) (AUContext.size expect)) then mt() else fnl() ++ str "(incompatible constraints)") | IncompatibleVariance -> diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 898a262266..8ce59c40c3 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1165,11 +1165,6 @@ let warn_non_reversible_notation = str " not occur in the right-hand side." ++ spc() ++ strbrk "The notation will not be used for printing as it is not reversible.") -type entry_coercion_kind = - | IsEntryCoercion of notation_entry_level - | IsEntryGlobal of string * int - | IsEntryIdent of string * int - let is_coercion level typs = match level, typs with | Some (custom,n,_), [e] -> @@ -1417,8 +1412,7 @@ type notation_obj = { notobj_scope : scope_name option; notobj_interp : interpretation; notobj_coercion : entry_coercion_kind option; - notobj_onlyparse : bool; - notobj_onlyprint : bool; + notobj_use : notation_use option; notobj_deprecation : Deprecation.t option; notobj_notation : notation * notation_location; notobj_specific_pp_rules : syntax_printing_extension option; @@ -1442,37 +1436,19 @@ let open_notation i (_, nobj) = let scope = nobj.notobj_scope in let (ntn, df) = nobj.notobj_notation in let pat = nobj.notobj_interp in - let onlyprint = nobj.notobj_onlyprint in let deprecation = nobj.notobj_deprecation in - let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in - let specific_ntn = (specific,ntn) in - let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in - if fresh then begin - (* Declare the interpretation *) - let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in - (* Declare the uninterpretation *) - if not nobj.notobj_onlyparse then - Notation.declare_uninterpretation (NotationRule specific_ntn) pat; - (* Declare a possible coercion *) - (match nobj.notobj_coercion with - | Some (IsEntryCoercion entry) -> - let (_,level,_) = Notation.level_of_notation ntn in - let level = match fst ntn with - | InConstrEntry -> None - | InCustomEntry _ -> Some level - in - Notation.declare_entry_coercion specific_ntn level entry - | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n - | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n - | None -> ()) - end; + let scope = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in + (* Declare the notation *) + (match nobj.notobj_use with + | Some use -> Notation.declare_notation (scope,ntn) pat df ~use nobj.notobj_coercion deprecation + | None -> ()); (* Declare specific format if any *) - match nobj.notobj_specific_pp_rules with + (match nobj.notobj_specific_pp_rules with | Some pp_sy -> - if specific_format_to_declare specific_ntn pp_sy then + if specific_format_to_declare (scope,ntn) pp_sy then Ppextend.declare_specific_notation_printing_rules - specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing - | None -> () + (scope,ntn) ~extra:pp_sy.synext_extra pp_sy.synext_unparsing + | None -> ()) end let cache_notation o = @@ -1602,6 +1578,20 @@ let make_printing_rules reserved (sd : SynData.syn_data) = let open SynData in synext_extra = sd.extra; } +let warn_unused_interpretation = + CWarnings.create ~name:"unused-notation" ~category:"parsing" + (fun b -> + strbrk "interpretation is used neither for printing nor for parsing, " ++ + (if b then strbrk "the declaration could be replaced by \"Reserved Notation\"." + else strbrk "the declaration could be removed.")) + +let make_use reserved onlyparse onlyprint = + match onlyparse, onlyprint with + | false, false -> Some ParsingAndPrinting + | true, false -> Some OnlyParsing + | false, true -> Some OnlyPrinting + | true, true -> warn_unused_interpretation reserved; None + (**********************************************************************) (* Main functions about notations *) @@ -1614,7 +1604,14 @@ let add_notation_in_scope ~local deprecation df env c mods scope = let sd = compute_syntax_data ~local deprecation df mods in (* Prepare the parsing and printing rules *) let sy_pa_rules = make_parsing_rules sd in - let sy_pp_rules = make_printing_rules false sd in + let sy_pp_rules, gen_sy_pp_rules = + match sd.only_parsing, Ppextend.has_generic_notation_printing_rule (fst sd.info) with + | true, true -> None, None + | onlyparse, has_generic -> + let rules = make_printing_rules false sd in + let _ = check_reserved_format (fst sd.info) rules in + (if onlyparse then None else rules), + (if has_generic then None else (* We use the format of this notation as the default *) rules) in (* Prepare the interpretation *) let i_vars = make_internalization_vars sd.recvars sd.mainvars sd.intern_typs in let nenv = { @@ -1626,22 +1623,18 @@ let add_notation_in_scope ~local deprecation df env c mods scope = let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in let onlyparse,coe = printability (Some sd.level) sd.subentries sd.only_parsing reversibility ac in let notation, location = sd.info in + let use = make_use true onlyparse sd.only_printing in let notation = { notobj_local = local; notobj_scope = scope; notobj_interp = (List.map_filter map i_vars, ac); (* Order is important here! *) - notobj_onlyparse = onlyparse; + notobj_use = use; notobj_coercion = coe; - notobj_onlyprint = sd.only_printing; notobj_deprecation = sd.deprecation; notobj_notation = (notation, location); notobj_specific_pp_rules = sy_pp_rules; } in - let gen_sy_pp_rules = - if Ppextend.has_generic_notation_printing_rule (fst sd.info) then None - else sy_pp_rules (* We use the format of this notation as the default *) in - let _ = check_reserved_format (fst sd.info) sy_pp_rules in (* Ready to change the global state *) List.iter (fun f -> f ()) sd.msgs; Lib.add_anonymous_leaf (inSyntaxExtension (local, (sy_pa_rules,gen_sy_pp_rules))); @@ -1673,14 +1666,14 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization let interp = make_interpretation_vars recvars plevel acvars (List.combine mainvars i_typs) in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in let onlyparse,coe = printability level i_typs onlyparse reversibility ac in + let use = make_use false onlyparse onlyprint in let notation = { notobj_local = local; notobj_scope = scope; notobj_interp = (List.map_filter map i_vars, ac); (* Order is important here! *) - notobj_onlyparse = onlyparse; + notobj_use = use; notobj_coercion = coe; - notobj_onlyprint = onlyprint; notobj_deprecation = deprecation; notobj_notation = df'; notobj_specific_pp_rules = pp_sy; diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 8b00484b4a..06f7c32cdc 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -216,7 +216,7 @@ let print_polymorphism ref = (if poly then str "universe polymorphic" else if template_poly then str "template universe polymorphic " - ++ h 0 (pr_template_variables template_variables) + ++ h (pr_template_variables template_variables) else str "not universe polymorphic") ] let print_type_in_type ref = diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 994592a88a..cd0dd5e9a6 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -43,4 +43,5 @@ Topfmt Loadpath ComArguments Vernacentries +ComTactic Vernacinterp diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index fe27d9ac8a..0d3f38d139 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1790,11 +1790,11 @@ let vernac_print ~pstate = | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s | PrintHintDb -> Hints.pr_searchtable env sigma | PrintScopes -> - Notation.pr_scopes (Constrextern.without_symbols (pr_lglob_constr_env env)) + Notation.pr_scopes (Constrextern.without_symbols (pr_glob_constr_env env)) | PrintScope s -> - Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s + Notation.pr_scope (Constrextern.without_symbols (pr_glob_constr_env env)) s | PrintVisibility s -> - Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s + Notation.pr_visibility (Constrextern.without_symbols (pr_glob_constr_env env)) s | PrintAbout (ref_or_by_not,udecl,glnumopt) -> print_about_hyp_globs ~pstate ref_or_by_not udecl glnumopt | PrintImplicit qid -> @@ -1830,7 +1830,7 @@ let vernac_locate ~pstate = let open Constrexpr in function | LocateTerm {v=ByNotation (ntn, sc)} -> let _, env = get_current_or_global_context ~pstate in Notation.locate_notation - (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc + (Constrextern.without_symbols (pr_glob_constr_env env)) ntn sc | LocateLibrary qid -> print_located_library qid | LocateModule qid -> Prettyp.print_located_module qid | LocateOther (s, qid) -> Prettyp.print_located_other s qid diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index eacb7fe6cb..ed63332861 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -30,7 +30,6 @@ type vernac_classification = | VtQed of vernac_qed_type (* A proof step *) | VtProofStep of { - parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; proof_block_detection : proof_block_name option } (* Queries are commands assumed to be "pure", that is to say, they @@ -124,7 +123,7 @@ let declare_vernac_classifier name f = let classify_as_query = VtQuery let classify_as_sideeff = VtSideff ([], VtLater) -let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None} +let classify_as_proofstep = VtProofStep { proof_block_detection = None} type (_, _) ty_sig = | TyNil : (vernac_command, vernac_classification) ty_sig diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 5ef137cfc0..e1e3b4cfe5 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -46,7 +46,6 @@ type vernac_classification = | VtQed of vernac_qed_type (* A proof step *) | VtProofStep of { - parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; proof_block_detection : proof_block_name option } (* Queries are commands assumed to be "pure", that is to say, they |
