diff options
118 files changed, 1765 insertions, 1423 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 4fdbe6e818..68bb24ac77 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,7 +18,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2019-12-08-V82" + CACHEKEY: "bionic_coq-V2019-03-01-V43" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/Makefile.build b/Makefile.build index 6590f5f308..9e0a402730 100644 --- a/Makefile.build +++ b/Makefile.build @@ -555,7 +555,7 @@ $(FAKEIDEBYTE): $(FAKEIDECMO) | $(IDETOPBYTE) # votour: a small vo explorer (based on the checker) -VOTOURCMO:=clib/cObj.cmo kernel/uint63.cmo kernel/float64.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo +VOTOURCMO:=clib/cObj.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo bin/votour: $(call bestobj, $(VOTOURCMO)) $(LIBCOQRUN) $(SHOW)'OCAMLBEST -o $@' diff --git a/config/dune b/config/dune index 5f2f7b1222..bf1aa4f471 100644 --- a/config/dune +++ b/config/dune @@ -13,5 +13,7 @@ %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run %{project_root}/dev/header.c + ; Needed to generate include lists for coq_makefile + (source_tree %{project_root}/plugins) (env_var COQ_CONFIGURE_PREFIX)) (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no)))) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index b8f9d99702..41392b4b8c 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-12-08-V82" +# CACHEKEY: "bionic_coq-V2019-03-01-V43" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -37,9 +37,9 @@ ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.0 ounit.2.0.8 odoc.1.4.2" \ +ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.1 ounit.2.0.8 odoc.1.4.2" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ - BASE_ONLY_OPAM="elpi.1.8.0" + BASE_ONLY_OPAM="elpi.1.10.2" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" diff --git a/dev/ci/user-overlays/11051-gares-elpi-1.8.sh b/dev/ci/user-overlays/11051-gares-elpi-1.8.sh deleted file mode 100644 index 7845654375..0000000000 --- a/dev/ci/user-overlays/11051-gares-elpi-1.8.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11051" ] || [ "$CI_BRANCH" = "elpi-1.8" ]; then - - elpi_CI_REF="coq-master+v1.2" - elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi - -fi diff --git a/dev/ci/user-overlays/11602-herbelin-master+support-only-parsing-where-clause.sh b/dev/ci/user-overlays/11602-herbelin-master+support-only-parsing-where-clause.sh new file mode 100644 index 0000000000..8b0f86d951 --- /dev/null +++ b/dev/ci/user-overlays/11602-herbelin-master+support-only-parsing-where-clause.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "11602" ] || [ "$CI_BRANCH" = "master+support-only-parsing-where-clause" ]; then + + equations_CI_REF=master+adapt-coq-pr11602-only-parsing-where-notation + equations_CI_GITURL=https://github.com/herbelin/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/11708-gares-elpi-1.10.sh b/dev/ci/user-overlays/11708-gares-elpi-1.10.sh new file mode 100644 index 0000000000..121190e5f6 --- /dev/null +++ b/dev/ci/user-overlays/11708-gares-elpi-1.10.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "11708" ] || [ "$CI_BRANCH" = " elpi-1.10+coq-elpi-1.3" ]; then + + elpi_CI_REF="coq-master+coq-elpi-1.3" + elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi + +fi diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 3e70d6dd16..0506216541 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -46,21 +46,27 @@ of build threads `(jobs N)` and display options `(display _mode_)`. ## Running binaries [coqtop / coqide] -There are two special targets `states` and `quickide` that will -generate "shims" for running `coqtop` and `coqide` in a fast build. In -order to use them, do: +Running `coqtop` directly with `dune exec -- coqtop` won't in general +work well unless you are using `dune exec -- coqtop -noinit`. The +`coqtop` binary doesn't depend itself on Coq's prelude, so plugins / +vo files may go stale if you rebuild only `coqtop`. + +Instead, you should use the provided "shims" for running `coqtop` and +`coqide` in a fast build. In order to use them, do: ``` $ make -f Makefile.dune voboot # Only once per session $ dune exec -- dev/shim/coqtop-prelude ``` -or `quickide` / `dev/shim/coqide-prelude` for CoqIDE. These targets -enjoy quick incremental compilation thanks to `-opaque` so they tend -to be very fast while developing. +or `quickide` / `dev/shim/coqide-prelude` for CoqIDE, etc.... See +`dev/shim/dune` for a complete list of targets. These targets enjoy +quick incremental compilation thanks to `-opaque` so they tend to be +very fast while developing. Note that for a fast developer build of ML files, the `check` target -will be faster. +is faster, as it doesn't link the binaries and uses the non-optimizing +compiler. ## Targets @@ -213,3 +219,12 @@ useful to Coq, some examples are: - Cross-compilation. - Automatic Generation of OPAM files. - Multi-directory libraries. + +## FAQ + +- I get "Error: Dynlink error: Interface mismatch": + + You are likely running a partial build which doesn't include + implicitly loaded plugins / vo files. See the "Running binaries + [coqtop / coqide]" section above as to how to correctly call Coq's + binaries. diff --git a/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst b/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst new file mode 100644 index 0000000000..1d30d16664 --- /dev/null +++ b/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst @@ -0,0 +1,6 @@ +- **Added:** + Notations declared with the ``where`` clause in the declaration of + inductive types, coinductive types, record fields, fixpoints and + cofixpoints now support the ``only parsing`` modifier + (`#11602 <https://github.com/coq/coq/pull/11602>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/11429-zify-optimisation.rst b/doc/changelog/04-tactics/11429-zify-optimisation.rst new file mode 100644 index 0000000000..ce5bfa4aad --- /dev/null +++ b/doc/changelog/04-tactics/11429-zify-optimisation.rst @@ -0,0 +1,3 @@ +- **Changed** + Improve the efficiency of `zify` by rewritting the remaining Ltac code in OCaml. + (`#11429 <https://github.com/coq/coq/pull/11429>`_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst b/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst new file mode 100644 index 0000000000..3dd103b115 --- /dev/null +++ b/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst @@ -0,0 +1,6 @@ +- **Added:** + Syntax :n:`pose proof (@ident:=@term)` as an + alternative to :n:`pose proof @term as @ident`, following the model of + :n:`pose (@ident:=@term)`. See documentation of :tacn:`pose proof` + (`#11522 <https://github.com/coq/coq/pull/11522>`_, + by Hugo Herbelin). diff --git a/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst b/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst new file mode 100644 index 0000000000..d2af6a4ca7 --- /dev/null +++ b/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst @@ -0,0 +1,5 @@ +- **Deprecated:** + Deprecated the declaration of arbitrary terms as hints. Global + references are now mandatory. + (`#7791 <https://github.com/coq/coq/pull/7791>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst b/doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst new file mode 100644 index 0000000000..77fa556321 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/11618-loadpath+split_ml_handling.rst @@ -0,0 +1,9 @@ +- **Changed:** + Recursive OCaml loadpaths are not supported anymore; the command + ``Add Rec ML Path`` has been removed; :cmd:`Add ML Path` is now the + preferred one. We have also dropped support for the non-qualified + version of the :cmd:`Add LoadPath` command, that is to say, + the ``Add LoadPath dir`` version; now, + you must always specify a prefix now using ``Add Loadpath dir as Prefix.`` + (`#11618 <https://github.com/coq/coq/pull/11618>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 6c1d83b3b8..b9e181dd94 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -24,7 +24,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining record : `record_keyword` `record_body` with … with `record_body` record_keyword : Record | Inductive | CoInductive record_body : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. - field : `ident` [ `binders` ] : `type` [ where `notation` ] + field : `ident` [ `binders` ] : `type` [ `decl_notations` ] : `ident` [ `binders` ] [: `type` ] := `term` .. cmd:: {| Record | Structure } @inductive_definition {* with @inductive_definition } @@ -35,8 +35,10 @@ expressions. In this sense, the :cmd:`Record` construction allows defining the default name :n:`Build_@ident`, where :token:`ident` is the record name, is used. If :token:`sort` is omitted, the default sort is :math:`\Type`. The identifiers inside the brackets are the names of fields. For a given field :token:`ident`, its type is :n:`forall {* @binder }, @type`. - Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the - order of the fields is important. Finally, :token:`binders` are parameters of the record. + Notice that the type of a particular identifier may depend on a previously-given identifier. Thus the + order of the fields is important. The record can depend as a whole on parameters :token:`binders` + and each field can also depend on its own :token:`binders`. Finally, notations can be attached to + fields using the :n:`decl_notations` annotation. :cmd:`Record` and :cmd:`Structure` are synonyms. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 6a0ce20c79..2bfd810ea1 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1452,6 +1452,19 @@ Controlling the proof flow While :tacn:`pose proof` expects that no existential variables are generated by the tactic, :tacn:`epose proof` removes this constraint. +.. tacv:: pose proof (@ident := @term) + + This is an alternative syntax for :n:`assert (@ident := @term)` and + :n:`pose proof @term as @ident`, following the model of :n:`pose + (@ident := @term)` but dropping the value of :token:`ident`. + +.. tacv:: epose proof (@ident := @term) + + This is an alternative syntax for :n:`eassert (@ident := @term)` + and :n:`epose proof @term as @ident`, following the model of + :n:`epose (@ident := @term)` but dropping the value of + :token:`ident`. + .. tacv:: enough (@ident : @type) :name: enough @@ -3761,18 +3774,18 @@ automatically created. Local is useless since hints do not survive anyway to the closure of sections. - .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}} : @ident + .. cmdv:: Hint Resolve @qualid {? | {? @num} {? @pattern}} : @ident :name: Hint Resolve - This command adds :n:`simple apply @term` to the hint list with the head - symbol of the type of :n:`@term`. The cost of that hint is the number of - subgoals generated by :n:`simple apply @term` or :n:`@num` if specified. The + This command adds :n:`simple apply @qualid` to the hint list with the head + symbol of the type of :n:`@qualid`. The cost of that hint is the number of + subgoals generated by :n:`simple apply @qualid` or :n:`@num` if specified. The associated :n:`@pattern` is inferred from the conclusion of the type of - :n:`@term` or the given :n:`@pattern` if specified. In case the inferred type - of :n:`@term` does not start with a product the tactic added in the hint list - is :n:`exact @term`. In case this type can however be reduced to a type - starting with a product, the tactic :n:`simple apply @term` is also stored in - the hints list. If the inferred type of :n:`@term` contains a dependent + :n:`@qualid` or the given :n:`@pattern` if specified. In case the inferred type + of :n:`@qualid` does not start with a product the tactic added in the hint list + is :n:`exact @qualid`. In case this type can however be reduced to a type + starting with a product, the tactic :n:`simple apply @qualid` is also stored in + the hints list. If the inferred type of :n:`@qualid` contains a dependent quantification on a variable which occurs only in the premisses of the type and not in its conclusion, no instance could be inferred for the variable by unification with the goal. In this case, the hint is added to the hint list @@ -3780,32 +3793,32 @@ automatically created. typical example of a hint that is used only by :tacn:`eauto` is a transitivity lemma. - .. exn:: @term cannot be used as a hint + .. exn:: @qualid cannot be used as a hint - The head symbol of the type of :n:`@term` is a bound variable + The head symbol of the type of :n:`@qualid` is a bound variable such that this tactic cannot be associated to a constant. - .. cmdv:: Hint Resolve {+ @term} : @ident + .. cmdv:: Hint Resolve {+ @qualid} : @ident - Adds each :n:`Hint Resolve @term`. + Adds each :n:`Hint Resolve @qualid`. - .. cmdv:: Hint Resolve -> @term : @ident + .. cmdv:: Hint Resolve -> @qualid : @ident Adds the left-to-right implication of an equivalence as a hint (informally - the hint will be used as :n:`apply <- @term`, although as mentioned + the hint will be used as :n:`apply <- @qualid`, although as mentioned before, the tactic actually used is a restricted version of :tacn:`apply`). - .. cmdv:: Hint Resolve <- @term + .. cmdv:: Hint Resolve <- @qualid Adds the right-to-left implication of an equivalence as a hint. - .. cmdv:: Hint Immediate @term : @ident + .. cmdv:: Hint Immediate @qualid : @ident :name: Hint Immediate - This command adds :n:`simple apply @term; trivial` to the hint list associated + This command adds :n:`simple apply @qualid; trivial` to the hint list associated with the head symbol of the type of :n:`@ident` in the given database. This - tactic will fail if all the subgoals generated by :n:`simple apply @term` are + tactic will fail if all the subgoals generated by :n:`simple apply @qualid` are not solved immediately by the :tacn:`trivial` tactic (which only tries tactics with cost 0).This command is useful for theorems such as the symmetry of equality or :g:`n+1=m+1 -> n=m` that we may like to introduce with a limited @@ -3813,12 +3826,12 @@ automatically created. never generates subgoals) is always 1, so that it is not used by :tacn:`trivial` itself. - .. exn:: @term cannot be used as a hint + .. exn:: @qualid cannot be used as a hint :undocumented: - .. cmdv:: Hint Immediate {+ @term} : @ident + .. cmdv:: Hint Immediate {+ @qualid} : @ident - Adds each :n:`Hint Immediate @term`. + Adds each :n:`Hint Immediate @qualid`. .. cmdv:: Hint Constructors @qualid : @ident :name: Hint Constructors diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index a38c26c2b3..d1f3dcc309 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -745,11 +745,6 @@ the toplevel, and using them in source files is discouraged. :n:`-Q @string @dirpath`. It adds the physical directory string to the current |Coq| loadpath and maps it to the logical directory dirpath. - .. cmdv:: Add LoadPath @string - - Performs as :n:`Add LoadPath @string @dirpath` but - for the empty directory path. - .. cmd:: Add Rec LoadPath @string as @dirpath @@ -757,11 +752,6 @@ the toplevel, and using them in source files is discouraged. :n:`-R @string @dirpath`. It adds the physical directory string and all its subdirectories to the current |Coq| loadpath. - .. cmdv:: Add Rec LoadPath @string - - Works as :n:`Add Rec LoadPath @string as @dirpath` but for the empty - logical directory path. - .. cmd:: Remove LoadPath @string @@ -784,12 +774,6 @@ the toplevel, and using them in source files is discouraged. loadpath (see the command `Declare ML Module`` in Section :ref:`compiled-files`). -.. cmd:: Add Rec ML Path @string - - This command adds the directory :n:`@string` and all its subdirectories to - the current OCaml loadpath (see the command :cmd:`Declare ML Module`). - - .. cmd:: Print ML Path @string This command displays the current OCaml loadpath. This diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 9b4d7cf5fa..fd95a5cef4 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -909,10 +909,10 @@ notations are given below. The optional :production:`scope` is described in notation : [Local] Notation `string` := `term` [(`modifiers`)] [: `scope`]. : [Local] Infix `string` := `qualid` [(`modifiers`)] [: `scope`]. : [Local] Reserved Notation `string` [(`modifiers`)] . - : Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. - : CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. - : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. - : CoFixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. + : Inductive `ind_body` [`decl_notations`] with … with `ind_body` [`decl_notations`]. + : CoInductive `ind_body` [`decl_notations`] with … with `ind_body` [`decl_notations`]. + : Fixpoint `fix_body` [`decl_notations`] with … with `fix_body` [`decl_notations`]. + : CoFixpoint `fix_body` [`decl_notations`] with … with `fix_body` [`decl_notations`]. : [Local] Declare Custom Entry `ident`. modifiers : `modifier`, … , `modifier` modifier : at level `num` @@ -947,7 +947,7 @@ notations are given below. The optional :production:`scope` is described in .. prodn:: decl_notations ::= where @decl_notation {* and @decl_notation } - decl_notation ::= @string := @term1_extended {? : @ident } + decl_notation ::= @string := @term1_extended [(only parsing)] {? : @ident } .. note:: No typing of the denoted expression is performed at definition time. Type checking is done only at the time of use of the notation. diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 1caf2c2722..76d98c5ddd 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -89,12 +89,12 @@ struct let catch = fun s h -> (); fun () -> try s () with Exception e as src -> - let (src, info) = CErrors.push src in + let (src, info) = Exninfo.capture src in h (e, info) () let read_line = fun () -> try read_line () with e -> - let (e, info) = CErrors.push e in - raise (e, info) () + let (e, info) = Exninfo.capture e in + raise (e,info) () let print_char = fun c -> (); fun () -> print_char c @@ -104,8 +104,8 @@ struct let make f = (); fun () -> try f () with e when CErrors.noncritical e -> - let (e, info) = CErrors.push e in - Util.iraise (Exception e, info) + let (e, info) = Exninfo.capture e in + Exninfo.iraise (Exception e, info) (** Use the current logger. The buffer is also flushed. *) let print_debug s = make (fun _ -> Feedback.msg_debug s) @@ -115,8 +115,8 @@ struct let run = fun x -> try x () with Exception e as src -> - let (src, info) = CErrors.push src in - Util.iraise (e, info) + let (src, info) = Exninfo.capture src in + Exninfo.iraise (e, info) end (** {6 Logical layer} *) diff --git a/engine/namegen.ml b/engine/namegen.ml index bcc8c34a4d..d2c37fb716 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -259,15 +259,17 @@ let visible_ids sigma (nenv, c) = let (gseen, vseen, ids) = !accu in let g = global_of_constr c in if not (GlobRef.Set_env.mem g gseen) then - begin - try let gseen = GlobRef.Set_env.add g gseen in - let short = Nametab.shortest_qualid_of_global Id.Set.empty g in - let dir, id = repr_qualid short in - let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in + let ids = match Nametab.shortest_qualid_of_global Id.Set.empty g with + | short -> + let dir, id = repr_qualid short in + if DirPath.is_empty dir then Id.Set.add id ids else ids + | exception Not_found -> + (* This may happen if given pathological terms or when manipulating + open modules *) + ids + in accu := (gseen, vseen, ids) - with Not_found when !Flags.in_debugger || !Flags.in_toplevel -> () - end | Rel p -> let (gseen, vseen, ids) = !accu in if p > n && not (Int.Set.mem p vseen) then diff --git a/engine/proofview.ml b/engine/proofview.ml index a26ce71141..6a4e490408 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -228,7 +228,7 @@ let apply ~name ~poly env t sp = let ans = Proof.repr (Proof.run t P.{trace=false; name; poly} (sp,env)) in let ans = Logic_monad.NonLogical.run ans in match ans with - | Nil (e, info) -> iraise (TacticFailure e, info) + | Nil (e, info) -> Exninfo.iraise (TacticFailure e, info) | Cons ((r, (state, _), status, info), _) -> let (status, gaveup) = status in let status = (status, state.shelf, gaveup) in @@ -328,8 +328,8 @@ let tclEXACTLY_ONCE e t = (** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *) type 'a case = -| Fail of iexn -| Next of 'a * (iexn -> 'a tactic) +| Fail of Exninfo.iexn +| Next of 'a * (Exninfo.iexn -> 'a tactic) let tclCASE t = let open Logic_monad in let map = function @@ -1096,7 +1096,7 @@ module Goal = struct let (gl, sigma) = nf_gmake env sigma goal in tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl)) with e when catchable_exception e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in tclZERO ~info e end end @@ -1114,7 +1114,7 @@ module Goal = struct tclEVARMAP >>= fun sigma -> try f (gmake env sigma goal) with e when catchable_exception e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in tclZERO ~info e end end @@ -1127,7 +1127,7 @@ module Goal = struct tclEVARMAP >>= fun sigma -> try f (gmake env sigma goal) with e when catchable_exception e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in tclZERO ~info e end | _ -> @@ -1218,7 +1218,7 @@ module V82 = struct InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"<unknown>")) >> Pv.set { ps with solution = evd; comb = sgs; } with e when catchable_exception e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in tclZERO ~info e @@ -1261,8 +1261,8 @@ module V82 = struct let (_,final,_,_) = apply ~name ~poly (goal_env env gls.Evd.sigma gls.Evd.it) t init in { Evd.sigma = final.solution ; it = CList.map drop_state final.comb } with Logic_monad.TacticFailure e as src -> - let (_, info) = CErrors.push src in - iraise (e, info) + let (_, info) = Exninfo.capture src in + Exninfo.iraise (e, info) let put_status = Status.put @@ -1271,7 +1271,7 @@ module V82 = struct let wrap_exceptions f = try f () with e when catchable_exception e -> - let (e, info) = CErrors.push e in tclZERO ~info e + let (e, info) = Exninfo.capture e in tclZERO ~info e end diff --git a/engine/proofview.mli b/engine/proofview.mli index a92179ab5b..5bfbc6a649 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -14,7 +14,6 @@ ['a tactic] is the (abstract) type of tactics modifying the proof state and returning a value of type ['a]. *) -open Util open EConstr (** Main state of tactics *) @@ -194,18 +193,18 @@ val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic the successes of [t1] have been depleted and it failed with [e], then it behaves as [t2 e]. In other words, [tclOR] inserts a backtracking point. *) -val tclOR : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic +val tclOR : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic (** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one success or [t2 e] if [t1] fails with [e]. It is analogous to [try/with] handler of exception in that it is not a backtracking point. *) -val tclORELSE : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic +val tclORELSE : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic (** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a] succeeds at least once then it behaves as [tclBIND a s] otherwise, if [a] fails with [e], then it behaves as [f e]. *) -val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (iexn -> 'b tactic) -> 'b tactic +val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Exninfo.iexn -> 'b tactic) -> 'b tactic (** [tclONCE t] behave like [t] except it has at most one success: [tclONCE t] stops after the first success of [t]. If [t] fails @@ -227,8 +226,8 @@ val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic continuation. It is the most general primitive to control backtracking. *) type 'a case = - | Fail of iexn - | Next of 'a * (iexn -> 'a tactic) + | Fail of Exninfo.iexn + | Next of 'a * (Exninfo.iexn -> 'a tactic) val tclCASE : 'a tactic -> 'a case tactic (** [tclBREAK p t] is a generalization of [tclONCE t]. Instead of @@ -236,7 +235,7 @@ val tclCASE : 'a tactic -> 'a case tactic failure with an exception [e] such that [p e = Some e'] is raised. At which point it drops the remaining successes, failing with [e']. [tclONCE t] is equivalent to [tclBREAK (fun e -> Some e) t]. *) -val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic +val tclBREAK : (Exninfo.iexn -> Exninfo.iexn option) -> 'a tactic -> 'a tactic (** {7 Focusing tactics} *) @@ -508,8 +507,8 @@ end module UnsafeRepr : sig type state = Proofview_monad.Logical.Unsafe.state - val repr : 'a tactic -> ('a, state, state, iexn) Logic_monad.BackState.t - val make : ('a, state, state, iexn) Logic_monad.BackState.t -> 'a tactic + val repr : 'a tactic -> ('a, state, state, Exninfo.iexn) Logic_monad.BackState.t + val make : ('a, state, state, Exninfo.iexn) Logic_monad.BackState.t -> 'a tactic end (** {6 Goal-dependent tactics} *) diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 5b9ea17ba7..790b427e4c 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -21,7 +21,6 @@ let commands = [ "Add Printing Let"; "Add Printing Record"; "Add Rec LoadPath"; - "Add Rec ML Path"; "Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. "; "Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ]."; "Add Relation"; diff --git a/ide/fake_ide.ml b/ide/fake_ide.ml index dfc16d39f3..4292e91252 100644 --- a/ide/fake_ide.ml +++ b/ide/fake_ide.ml @@ -327,11 +327,7 @@ let main = { xml_printer = op; xml_parser = ip } in let init () = match base_eval_call ~print:false (Xmlprotocol.init None) coq with - | Interface.Good id -> - let dir = Filename.dirname input_file in - let phrase = Printf.sprintf "Add LoadPath \"%s\". " dir in - let eid, tip = add_sentence ~name:"initial" phrase in - after_add (base_eval_call (Xmlprotocol.add ((phrase,eid),(tip,true))) coq) + | Interface.Good id -> () | Interface.Fail _ -> error "init call failed" in let finish () = match base_eval_call (Xmlprotocol.status true) coq with diff --git a/ide/idetop.ml b/ide/idetop.ml index 9eb0b972b6..57e9792845 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -69,7 +69,7 @@ let ide_cmd_checks ~last_valid { CAst.loc; v } = let user_error s = try CErrors.user_err ?loc ~hdr:"IDE" (str s) with e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in let info = Stateid.add info ~valid:last_valid Stateid.dummy in Exninfo.iraise (e, info) in @@ -477,7 +477,7 @@ let print_xml = fun oc xml -> Mutex.lock m; try Control.protect_sigalrm (Xml_printer.print oc) xml; Mutex.unlock m - with e -> let e = CErrors.push e in Mutex.unlock m; iraise e + with e -> let e = Exninfo.capture e in Mutex.unlock m; Exninfo.iraise e let slave_feeder fmt xml_oc msg = let xml = Xmlprotocol.(of_feedback fmt msg) in diff --git a/ide/protocol/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml index a2c80ea118..2e78642f2e 100644 --- a/ide/protocol/xmlprotocol.ml +++ b/ide/protocol/xmlprotocol.ml @@ -679,7 +679,7 @@ let abstract_eval_call : type a. _ -> a call -> a value = fun handler c -> | PrintAst x -> mkGood (handler.print_ast x) | Annotate x -> mkGood (handler.annotate x) with any -> - let any = CErrors.push any in + let any = Exninfo.capture any in Fail (handler.handle_exn any) (** brain dead code, edit if protocol messages are added/removed *) diff --git a/interp/impargs.ml b/interp/impargs.ml index 78c4b21920..1365b97d82 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -77,9 +77,9 @@ let with_implicit_protection f x = implicit_args := oflags; rslt with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in let () = implicit_args := oflags in - iraise reraise + Exninfo.iraise reraise type on_trailing_implicit = Error | Info | Silent diff --git a/interp/notation.ml b/interp/notation.ml index 2086e08f79..b869cb2a36 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1959,6 +1959,6 @@ let with_notation_protection f x = let fs = freeze ~marshallable:false in try let a = f x in unfreeze fs; a with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in let () = unfreeze fs in - iraise reraise + Exninfo.iraise reraise diff --git a/kernel/inductive.ml b/kernel/inductive.ml index c6035f78ff..1be86f2bf8 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -962,7 +962,7 @@ let check_one_fix renv recpos trees def = let stack_br = push_stack_args case_spec.(k) stack' in check_rec_call renv stack_br br') with (FixGuardError _ as exn) -> - let exn = CErrors.push exn in + let exn = Exninfo.capture exn in (* we try hard to reduce the match away by looking for a constructor in c_0 (we unfold definitions too) *) let c_0 = whd_all renv.env c_0 in @@ -1007,7 +1007,7 @@ let check_one_fix renv recpos trees def = check_nested_fix_body illformed renv' (decrArg+1) arg_sp body else check_rec_call renv' [] body) with (FixGuardError _ as exn) -> - let exn = CErrors.push exn in + let exn = Exninfo.capture exn in (* we try hard to reduce the fix away by looking for a constructor in l[decrArg] (we unfold definitions too) *) if List.length l <= decrArg then Exninfo.iraise exn; @@ -1055,7 +1055,7 @@ let check_one_fix renv recpos trees def = List.iter (check_rec_call renv []) l; check_rec_call renv [] c with (FixGuardError _ as exn) -> - let exn = CErrors.push exn in + let exn = Exninfo.capture exn in (* we try hard to reduce the proj away by looking for a constructor in c (we unfold definitions too) *) let c = whd_all renv.env c in diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 86eaaddc90..3f2e63b984 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -180,8 +180,8 @@ let call_linker ?(fatal=true) env ~prefix f upds = if Dynlink.is_native then Dynlink.loadfile f else !load_obj f; register_native_file prefix with Dynlink.Error _ as exn -> - let exn = CErrors.push exn in - if fatal then iraise exn + let exn = Exninfo.capture exn in + if fatal then Exninfo.iraise exn else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn)); match upds with Some upds -> update_locations upds | _ -> () diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 8db8a044a8..d8e1b6537e 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1262,7 +1262,7 @@ let export ?except ~output_native_objects senv dir = let senv = try join_safe_environment ?except senv with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in CErrors.user_err ~hdr:"export" (CErrors.iprint e) in assert(senv.future_cst = []); diff --git a/lib/cErrors.mli b/lib/cErrors.mli index 1660a00244..ec81694177 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -14,7 +14,7 @@ (** {6 Error handling} *) val push : exn -> Exninfo.iexn -(** Alias for [Backtrace.add_backtrace]. *) +[@@ocaml.deprecated "please use [Exninfo.capture]"] (** {6 Generic errors.} diff --git a/lib/future.ml b/lib/future.ml index ddf841b7fc..e8d232ad96 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -131,7 +131,7 @@ let rec compute ck : 'a value = let data = f () in c := Val data; `Val data with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in let e = fix_exn e in match e with | (NotReady _, _) -> `Exn e diff --git a/lib/system.ml b/lib/system.ml index 2d68fd2fdf..9089eda564 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -248,9 +248,9 @@ let extern_state magic filename val_0 = marshal_out channel val_0; close_out channel with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in let () = try_remove filename in - iraise reraise + Exninfo.iraise reraise with Sys_error s -> CErrors.user_err ~hdr:"System.extern_state" (str "System error: " ++ str s) diff --git a/lib/util.mli b/lib/util.mli index 2f1a03a19c..1417d6dfcb 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -119,8 +119,10 @@ val delayed_force : 'a delayed -> 'a (** {6 Enriched exceptions} *) type iexn = Exninfo.iexn +[@@ocaml.deprecated "please use [Exninfo.iexn]"] -val iraise : iexn -> 'a +val iraise : Exninfo.iexn -> 'a +[@@ocaml.deprecated "please use [Exninfo.iraise]"] (** {6 Misc. } *) diff --git a/library/states.ml b/library/states.ml index 90303a2a5c..c656dfb952 100644 --- a/library/states.ml +++ b/library/states.ml @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Util - type state = Lib.frozen * Summary.frozen let lib_of_state = fst @@ -31,5 +29,5 @@ let with_state_protection f x = try let a = f x in unfreeze st; a with reraise -> - let reraise = CErrors.push reraise in - (unfreeze st; iraise reraise) + let reraise = Exninfo.capture reraise in + (unfreeze st; Exninfo.iraise reraise) diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index d6c6c365cb..48e6f1f213 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -17,7 +17,6 @@ open Glob_term open Constrexpr open Constrexpr_ops open Util -open Tok open Namegen open Pcoq @@ -54,48 +53,25 @@ let err () = raise Stream.Failure (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) (* admissible notation "(x t)" *) -let lpar_id_coloneq = - Pcoq.Entry.of_parser "test_lpar_id_coloneq" - (fun _ strm -> - match stream_nth 0 strm with - | KEYWORD "(" -> - (match stream_nth 1 strm with - | IDENT s -> - (match stream_nth 2 strm with - | KEYWORD ":=" -> - stream_njunk 3 strm; - Names.Id.of_string s - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) +let test_lpar_id_coloneq = + let open Pcoq.Lookahead in + to_entry "test_lpar_id_coloneq" begin + lk_kw "(" >> lk_ident >> lk_kw ":=" + end let ensure_fixannot = - Pcoq.Entry.of_parser "check_fixannot" - (fun _ strm -> - match stream_nth 0 strm with - | KEYWORD "{" -> - (match stream_nth 1 strm with - | IDENT ("wf"|"struct"|"measure") -> () - | _ -> err ()) - | _ -> err ()) + let open Pcoq.Lookahead in + to_entry "check_fixannot" begin + lk_kw "{" >> lk_kws ["wf"; "struct"; "measure"] + end -let name_colon = - Pcoq.Entry.of_parser "name_colon" - (fun _ strm -> - match stream_nth 0 strm with - | IDENT s -> - (match stream_nth 1 strm with - | KEYWORD ":" -> - stream_njunk 2 strm; - Name (Names.Id.of_string s) - | _ -> err ()) - | KEYWORD "_" -> - (match stream_nth 1 strm with - | KEYWORD ":" -> - stream_njunk 2 strm; - Anonymous - | _ -> err ()) - | _ -> err ()) +let lk_name = Pcoq.Lookahead.(lk_ident <+> lk_kw "_") + +let test_name_colon = + let open Pcoq.Lookahead in + to_entry "test_name_colon" begin + lk_name >> lk_kw ":" + end let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None @@ -266,7 +242,7 @@ GRAMMAR EXTEND Gram | "cofix"; c = cofix_decls -> { let (id,dcls) = c in CAst.make ~loc @@ CCoFix (id,dcls) } ] ] ; appl_arg: - [ [ id = lpar_id_coloneq; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByName id)) } + [ [ test_lpar_id_coloneq; "("; id = ident; ":="; c = lconstr; ")" -> { (c,Some (CAst.make ~loc @@ ExplByName id)) } | c=operconstr LEVEL "9" -> { (c,None) } ] ] ; atomic_constr: @@ -464,8 +440,8 @@ GRAMMAR EXTEND Gram [ [ "!" ; c = operconstr LEVEL "200" -> { (CAst.make ~loc Anonymous), true, c } | "{"; id = name; "}"; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" -> { id, expl, c } - | iid = name_colon ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" -> - { (CAst.make ~loc iid), expl, c } + | test_name_colon; iid = name; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" -> + { iid, expl, c } | c = operconstr LEVEL "200" -> { (CAst.make ~loc Anonymous), false, c } ] ] ; diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 020501aedf..5f61b9a047 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -31,35 +31,11 @@ let my_int_of_string loc s = with Failure _ -> CErrors.user_err ~loc (Pp.str "This number is too large.") -let rec contiguous tok n m = - n == m - || - let (_, ep) = Loc.unloc (tok n) in - let (bp, _) = Loc.unloc (tok (n + 1)) in - Int.equal ep bp && contiguous tok (succ n) m - -let rec lookahead_kwds strm n = function - | [] -> () - | x :: xs -> - let toks = Stream.npeek (n+1) strm in - match List.nth toks n with - | Tok.KEYWORD y -> - if String.equal x y then lookahead_kwds strm (succ n) xs - else raise Stream.Failure - | _ -> raise Stream.Failure - | exception (Failure _) -> raise Stream.Failure - -(* [test_nospace m] fails if the next m tokens are not contiguous keywords *) -let test_nospace m = assert(m <> []); Pcoq.Entry.of_parser "test_nospace" - (fun tok strm -> - let n = Stream.count strm in - lookahead_kwds strm 0 m; - if contiguous tok n (n + List.length m - 1) then () - else raise Stream.Failure) - -let test_nospace_pipe_closedcurly = - test_nospace ["|"; "}"] - +let test_pipe_closedcurly = + let open Pcoq.Lookahead in + to_entry "test_pipe_closedcurly" begin + lk_kw "|" >> lk_kw "}" >> check_no_space + end } @@ -155,6 +131,6 @@ GRAMMAR EXTEND Gram [ [ i = NUMERAL -> { check_int loc i } ] ] ; bar_cbrace: - [ [ test_nospace_pipe_closedcurly; "|"; "}" -> { () } ] ] + [ [ test_pipe_closedcurly; "|"; "}" -> { () } ] ] ; END diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 92c3b7c6e8..55558eaed0 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -118,6 +118,64 @@ struct end +module Lookahead = +struct + + let err () = raise Stream.Failure + + type t = Gramlib.Plexing.location_function -> int -> Tok.t Stream.t -> int option + + let rec contiguous tok n m = + n == m || + let (_, ep) = Loc.unloc (tok n) in + let (bp, _) = Loc.unloc (tok (n + 1)) in + Int.equal ep bp && contiguous tok (succ n) m + + let check_no_space tok m strm = + let n = Stream.count strm in + if contiguous tok n (n+m-1) then Some m else None + + let to_entry s (lk : t) = + let run tok strm = match lk tok 0 strm with None -> err () | Some _ -> () in + Entry.of_parser s run + + let (>>) (lk1 : t) lk2 tok n strm = match lk1 tok n strm with + | None -> None + | Some n -> lk2 tok n strm + + let (<+>) (lk1 : t) lk2 tok n strm = match lk1 tok n strm with + | None -> lk2 tok n strm + | Some n -> Some n + + let lk_empty tok n strm = Some n + + let lk_kw kw tok n strm = match stream_nth n strm with + | Tok.KEYWORD kw' | Tok.IDENT kw' -> if String.equal kw kw' then Some (n + 1) else None + | _ -> None + + let lk_kws kws tok n strm = match stream_nth n strm with + | Tok.KEYWORD kw | Tok.IDENT kw -> if List.mem_f String.equal kw kws then Some (n + 1) else None + | _ -> None + + let lk_ident tok n strm = match stream_nth n strm with + | Tok.IDENT _ -> Some (n + 1) + | _ -> None + + let lk_ident_except idents tok n strm = match stream_nth n strm with + | Tok.IDENT ident when not (List.mem_f String.equal ident idents) -> Some (n + 1) + | _ -> None + + let lk_nat tok n strm = match stream_nth n strm with + | Tok.NUMERAL { NumTok.int = _; frac = ""; exp = "" } -> Some (n + 1) + | _ -> None + + let rec lk_list lk_elem n strm = + ((lk_elem >> lk_list lk_elem) <+> lk_empty) n strm + + let lk_ident_list = lk_list lk_ident + +end + (** Grammar extensions *) (** NB: [extend_statement = @@ -627,9 +685,9 @@ let with_grammar_rule_protection f x = let fs = freeze ~marshallable:false in try let a = f x in unfreeze fs; a with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in let () = unfreeze fs in - iraise reraise + Exninfo.iraise reraise (** Registering grammar of generic arguments *) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index f2fc007a7b..6543a69b50 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -34,6 +34,21 @@ module Entry : sig val name : 'a t -> string end +module Lookahead : sig + type t + val to_entry : string -> t -> unit Entry.t + val (>>) : t -> t -> t + val (<+>) : t -> t -> t + val lk_list : t -> t + val check_no_space : t + val lk_kw : string -> t + val lk_kws : string list -> t + val lk_nat : t + val lk_ident : t + val lk_ident_except : string list -> t + val lk_ident_list : t +end + (** The parser of Coq is built from three kinds of rule declarations: - dynamic rules declared at the evaluation of Coq files (using diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index b2ee0f9370..45fafd2872 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -520,7 +520,7 @@ let funind_purify f x = let st = Vernacstate.freeze_interp_state ~marshallable:false in try f x with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in Vernacstate.unfreeze_interp_state st; Exninfo.iraise e diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index 5835d75c79..f97c291c79 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -330,18 +330,10 @@ END { let local_test_lpar_id_colon = - let err () = raise Stream.Failure in - Pcoq.Entry.of_parser "lpar_id_colon" - (fun _ strm -> - match Util.stream_nth 0 strm with - | Tok.KEYWORD "(" -> - (match Util.stream_nth 1 strm with - | Tok.IDENT _ -> - (match Util.stream_nth 2 strm with - | Tok.KEYWORD ":" -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) + let open Pcoq.Lookahead in + to_entry "lpar_id_colon" begin + lk_kw "(" >> lk_ident >> lk_kw ":" + end let pr_lpar_id_colon _ _ _ _ = mt () diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 513f5ca77b..d0c94e7903 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -670,7 +670,7 @@ let hResolve id c occ t = Pretyping.understand env sigma t_hole with | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in let loc_begin = Option.cata (fun l -> fst (Loc.unloc l)) 0 (Loc.get_loc info) in resolve_hole (subst_hole_with_term loc_begin c_raw t_hole) in diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 8344f9dae3..82c64a9857 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -114,7 +114,7 @@ END (** Eauto *) -TACTIC EXTEND prolog +TACTIC EXTEND prolog DEPRECATED { Deprecation.make ~note:"Use eauto instead" () } | [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] -> { Eauto.prolog_tac (eval_uconstrs ist l) n } END @@ -253,4 +253,3 @@ VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF (match dbnames with None -> ["core"] | Some l -> l) entry; } END - diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 7ea843ca69..c163438718 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -20,7 +20,6 @@ open Tacexpr open Namegen open Genarg open Genredexpr -open Tok (* necessary for camlp5 *) open Names open Attributes @@ -63,14 +62,10 @@ let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode (* Hack to parse "[ id" without dropping [ *) let test_bracket_ident = - Pcoq.Entry.of_parser "test_bracket_ident" - (fun _ strm -> - match stream_nth 0 strm with - | KEYWORD "[" -> - (match stream_nth 1 strm with - | IDENT _ -> () - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) + let open Pcoq.Lookahead in + to_entry "test_bracket_ident" begin + lk_kw "[" >> lk_ident + end (* Tactics grammar rules *) diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index f0d6258cd1..8e1e5559af 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -38,45 +38,24 @@ let err () = raise Stream.Failure (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) (* admissible notation "(x t)" *) let test_lpar_id_coloneq = - Pcoq.Entry.of_parser "lpar_id_coloneq" - (fun _ strm -> - match stream_nth 0 strm with - | KEYWORD "(" -> - (match stream_nth 1 strm with - | IDENT _ -> - (match stream_nth 2 strm with - | KEYWORD ":=" -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) + let open Pcoq.Lookahead in + to_entry "lpar_id_coloneq" begin + lk_kw "(" >> lk_ident >> lk_kw ":=" + end (* Hack to recognize "(x)" *) let test_lpar_id_rpar = - Pcoq.Entry.of_parser "lpar_id_coloneq" - (fun _ strm -> - match stream_nth 0 strm with - | KEYWORD "(" -> - (match stream_nth 1 strm with - | IDENT _ -> - (match stream_nth 2 strm with - | KEYWORD ")" -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) + let open Pcoq.Lookahead in + to_entry "lpar_id_coloneq" begin + lk_kw "(" >> lk_ident >> lk_kw ")" + end (* idem for (x:=t) and (1:=t) *) let test_lpar_idnum_coloneq = - Pcoq.Entry.of_parser "test_lpar_idnum_coloneq" - (fun _ strm -> - match stream_nth 0 strm with - | KEYWORD "(" -> - (match stream_nth 1 strm with - | IDENT _ | NUMERAL _ -> - (match stream_nth 2 strm with - | KEYWORD ":=" -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) + let open Pcoq.Lookahead in + to_entry "test_lpar_idnum_coloneq" begin + lk_kw "(" >> (lk_ident <+> lk_nat) >> lk_kw ":=" + end (* idem for (x:t) *) open Extraargs @@ -107,11 +86,10 @@ let check_for_coloneq = | _ -> err ()) let lookup_at_as_comma = - Pcoq.Entry.of_parser "lookup_at_as_comma" - (fun _ strm -> - match stream_nth 0 strm with - | KEYWORD (","|"at"|"as") -> () - | _ -> err ()) + let open Pcoq.Lookahead in + to_entry "lookup_at_as_comma" begin + lk_kws [",";"at";"as"] + end open Constr open Prim @@ -611,6 +589,16 @@ GRAMMAR EXTEND Gram { TacAtom (CAst.make ~loc @@ TacAssert (false,true,Some tac,ipat,c)) } | IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic -> { TacAtom (CAst.make ~loc @@ TacAssert (true,true,Some tac,ipat,c)) } + + (* Alternative syntax for "pose proof c as id by tac" *) + | IDENT "pose"; IDENT "proof"; test_lpar_id_coloneq; "("; lid = identref; ":="; + c = lconstr; ")" -> + { let { CAst.loc = loc; v = id } = lid in + TacAtom (CAst.make ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } + | IDENT "epose"; IDENT "proof"; test_lpar_id_coloneq; "("; lid = identref; ":="; + c = lconstr; ")" -> + { let { CAst.loc = loc; v = id } = lid in + TacAtom (CAst.make ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> { TacAtom (CAst.make ~loc @@ TacAssert (false,true,None,ipat,c)) } | IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 6e620b71db..1d7fe335d1 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -165,8 +165,8 @@ let catching_error call_trace fail (e, info) = let catch_error call_trace f x = try f x with e when CErrors.noncritical e -> - let e = CErrors.push e in - catching_error call_trace iraise e + let e = Exninfo.capture e in + catching_error call_trace Exninfo.iraise e let wrap_error tac k = if is_traced () then Proofview.tclORELSE tac k else tac @@ -717,13 +717,13 @@ let interp_may_eval f ist env sigma = function try f ist env sigma c with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess up with any assumption. *) Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> str"interpretation of term " ++ pr_glob_constr_env env (fst c))); - iraise reraise + Exninfo.iraise reraise (* Interprets a constr expression possibly to first evaluate *) let interp_constr_may_eval ist env sigma c = @@ -731,12 +731,12 @@ let interp_constr_may_eval ist env sigma c = try interp_may_eval interp_constr ist env sigma c with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess up with any assumption. *) Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> str"evaluation of term")); - iraise reraise + Exninfo.iraise reraise in begin (* spiwack: to avoid unnecessary modifications of tacinterp, as this diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 61234145e1..e946ffd8bc 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -413,8 +413,14 @@ let bound_monomials (sys : WithProof.t list) = (fun acc ((p, o), _) -> ISet.union (LinPoly.monomials p) acc) ISet.empty sys in + let module SetWP = Set.Make (struct + type t = int * WithProof.t + + let compare (_, x) (_, y) = WithProof.compare x y + end) in let bounds = saturate_bin + (module SetWP : Set.S with type elt = int * WithProof.t) (fun (i1, w1) (i2, w2) -> if i1 + i2 > deg then None else diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg index 2b5fac32a2..5e4a847e6b 100644 --- a/plugins/micromega/g_zify.mlg +++ b/plugins/micromega/g_zify.mlg @@ -25,7 +25,8 @@ VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF | ["Add" "UnOp" constr(t) ] -> { Zify.UnOp.register t } | ["Add" "CstOp" constr(t) ] -> { Zify.CstOp.register t } | ["Add" "BinRel" constr(t) ] -> { Zify.BinRel.register t } -| ["Add" "PropOp" constr(t) ] -> { Zify.PropOp.register t } +| ["Add" "PropOp" constr(t) ] -> { Zify.PropBinOp.register t } +| ["Add" "PropBinOp" constr(t) ] -> { Zify.PropBinOp.register t } | ["Add" "PropUOp" constr(t) ] -> { Zify.PropUnOp.register t } | ["Add" "Spec" constr(t) ] -> { Zify.Spec.register t } | ["Add" "BinOpSpec" constr(t) ] -> { Zify.Spec.register t } @@ -34,13 +35,14 @@ VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF END TACTIC EXTEND ITER -| [ "zify_iter_specs" tactic(t)] -> { Zify.iter_specs t } +| [ "zify_iter_specs"] -> { Zify.iter_specs} END TACTIC EXTEND TRANS | [ "zify_op" ] -> { Zify.zify_tac } | [ "zify_saturate" ] -> { Zify.saturate } | [ "zify_iter_let" tactic(t)] -> { Zify.iter_let t } +| [ "zify_elim_let" ] -> { Zify.elim_let } END VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 160b492d3d..51f0328e4b 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -140,24 +140,24 @@ let saturate p f sys = Printexc.print_backtrace stdout; raise x -let saturate_bin (f : 'a -> 'a -> 'a option) (l : 'a list) = - let rec map_with acc e l = +let saturate_bin (type a) (module Set : Set.S with type elt = a) + (f : a -> a -> a option) (l : a list) = + let rec map_with (acc : Set.t) e l = match l with | [] -> acc - | e' :: l' -> ( + | e' :: l -> ( match f e e' with - | None -> map_with acc e l' - | Some r -> map_with (r :: acc) e l' ) - in - let rec map2_with acc l' = - match l' with [] -> acc | e' :: l' -> map2_with (map_with acc e' l) l' + | None -> map_with acc e l + | Some r -> map_with (Set.add r acc) e l ) in + let map2_with acc l' = Set.fold (fun e' acc -> map_with acc e' l) l' acc in let rec iterate acc l' = - match map2_with [] l' with - | [] -> List.rev_append l' acc - | res -> iterate (List.rev_append l' acc) res + let res = map2_with Set.empty l' in + if Set.is_empty res then Set.union l' acc + else iterate (Set.union l' acc) res in - iterate [] l + let s0 = List.fold_left (fun acc e -> Set.add e acc) Set.empty l in + Set.elements (Set.diff (iterate Set.empty s0) s0) open Num open Big_int diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli index 5dcaf3be44..9badddc255 100644 --- a/plugins/micromega/mutils.mli +++ b/plugins/micromega/mutils.mli @@ -116,7 +116,12 @@ val simplify : ('a -> 'a option) -> 'a list -> 'a list option val saturate : ('a -> 'b option) -> ('b * 'a -> 'a -> 'a option) -> 'a list -> 'a list -val saturate_bin : ('a -> 'a -> 'a option) -> 'a list -> 'a list +val saturate_bin : + (module Set.S with type elt = 'a) + -> ('a -> 'a -> 'a option) + -> 'a list + -> 'a list + val generate : ('a -> 'b option) -> 'a list -> 'b list val app_funs : ('a -> 'b option) list -> 'a -> 'b option val command : string -> string array -> 'a -> 'b diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index b20213979b..f83b36d847 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -864,6 +864,12 @@ end module WithProof = struct type t = (LinPoly.t * op) * ProofFormat.prf_rule + (* The comparison ignores proofs on purpose *) + let compare : t -> t -> int = + fun ((lp1, o1), _) ((lp2, o2), _) -> + let c = Vect.compare lp1 lp2 in + if c = 0 then compare o1 o2 else c + let annot s (p, prf) = (p, ProofFormat.Annot (s, prf)) let output o ((lp, op), prf) = diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli index 4b56b037e0..797ff5827d 100644 --- a/plugins/micromega/polynomial.mli +++ b/plugins/micromega/polynomial.mli @@ -320,6 +320,7 @@ module WithProof : sig exception InvalidProof (** [InvalidProof] is raised if the operation is invalid. *) + val compare : t -> t -> int val annot : string -> t -> t val of_cstr : cstr * ProofFormat.prf_rule -> t diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index e71c89b4db..b3b627be14 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -12,11 +12,43 @@ open Constr open Names open Pp open Lazy +module NamedDecl = Context.Named.Declaration -(** [get_type_of] performs beta reduction ; - Is it ok for Retyping.get_type_of (Zpower_nat n q) to return (fun _ : nat => Z) q ? *) -let get_type_of env evd e = - Tacred.cbv_beta env evd (Retyping.get_type_of env evd e) +let debug = false + +(* The following [constr] are necessary for constructing the proof terms *) + +let zify str = + EConstr.of_constr + (UnivGen.constr_of_monomorphic_global + (Coqlib.lib_ref ("ZifyClasses." ^ str))) + +(* morphism like lemma *) + +let mkapp2 = lazy (zify "mkapp2") +let mkapp = lazy (zify "mkapp") +let eq_refl = lazy (zify "eq_refl") +let eq = lazy (zify "eq") +let mkrel = lazy (zify "mkrel") +let iff_refl = lazy (zify "iff_refl") +let eq_iff = lazy (zify "eq_iff") +let rew_iff = lazy (zify "rew_iff") + +(* propositional logic *) + +let op_and = lazy (zify "and") +let op_and_morph = lazy (zify "and_morph") +let op_or = lazy (zify "or") +let op_or_morph = lazy (zify "or_morph") +let op_impl_morph = lazy (zify "impl_morph") +let op_iff = lazy (zify "iff") +let op_iff_morph = lazy (zify "iff_morph") +let op_not = lazy (zify "not") +let op_not_morph = lazy (zify "not_morph") + +(* identity function *) +(*let identity = lazy (zify "identity")*) +let whd = Reductionops.clos_whd_flags CClosure.all (** [unsafe_to_constr c] returns a [Constr.t] without considering an evar_map. This is useful for calling Constr.hash *) @@ -24,6 +56,18 @@ let unsafe_to_constr = EConstr.Unsafe.to_constr let pr_constr env evd e = Printer.pr_econstr_env env evd e +let gl_pr_constr e = + let genv = Global.env () in + let evd = Evd.from_env genv in + pr_constr genv evd e + +let is_convertible env evd t1 t2 = Reductionops.(is_conv env evd t1 t2) + +(** [get_type_of] performs beta reduction ; + Is it ok for Retyping.get_type_of (Zpower_nat n q) to return (fun _ : nat => Z) q ? *) +let get_type_of env evd e = + Tacred.cbv_beta env evd (Retyping.get_type_of env evd e) + let rec find_option pred l = match l with | [] -> raise Not_found @@ -62,10 +106,7 @@ end *) let get_projections_from_constant (evd, i) = - match - EConstr.kind evd - (Reductionops.clos_whd_flags CClosure.all (Global.env ()) evd i) - with + match EConstr.kind evd (whd (Global.env ()) evd i) with | App (c, a) -> Some a | _ -> raise @@ -98,6 +139,109 @@ module EInjT = struct cstr : EConstr.t option (* forall x, pred (inj x) *) } end +(** [classify_op] classify injected operators and detect special cases. *) + +type classify_op = + | OpInj (* e.g. Z.of_nat -> \x.x *) + | OpSame (* e.g. Z.add -> Z.add *) + | OpConv (* e.g. Pos.ge == \x.y. Z.ge (Z.pos x) (Z.pos y) + \x.y. Z.pos (Pos.add x y) == \x.y. Z.add (Z.pos x) (Z.pos y) + Z.succ == (\x.x + 1) + *) + | OpOther + +(*let pp_classify_op = function + | OpInj -> Pp.str "Identity" + | OpSame -> Pp.str "Same" + | OpConv -> Pp.str "Conv" + | OpOther -> Pp.str "Other" + *) + +let name x = + Context.make_annot (Name.mk_name (Names.Id.of_string x)) Sorts.Relevant + +let mkconvert_unop i1 i2 op top = + (* fun x => inj (op x) *) + let op = + EConstr.mkLambda + ( name "x" + , i1.EInjT.source + , EConstr.mkApp (i2.EInjT.inj, [|EConstr.mkApp (op, [|EConstr.mkRel 1|])|]) + ) + in + (* fun x => top (inj x) *) + let top = + EConstr.mkLambda + ( name "x" + , i1.EInjT.source + , EConstr.mkApp + (top, [|EConstr.mkApp (i1.EInjT.inj, [|EConstr.mkRel 1|])|]) ) + in + (op, top) + +let mkconvert_binop i1 i2 i3 op top = + (* fun x y => inj (op x y) *) + let op = + EConstr.mkLambda + ( name "x" + , i1.EInjT.source + , EConstr.mkLambda + ( name "y" + , i1.EInjT.source + , EConstr.mkApp + ( i3.EInjT.inj + , [|EConstr.mkApp (op, [|EConstr.mkRel 2; EConstr.mkRel 1|])|] ) + ) ) + in + (* fun x y => top (inj x) (inj y) *) + let top = + EConstr.mkLambda + ( name "x" + , i1.EInjT.source + , EConstr.mkLambda + ( name "y" + , i2.EInjT.source + , EConstr.mkApp + ( top + , [| EConstr.mkApp (i1.EInjT.inj, [|EConstr.mkRel 2|]) + ; EConstr.mkApp (i2.EInjT.inj, [|EConstr.mkRel 1|]) |] ) ) ) + in + (op, top) + +let mkconvert_rel i r tr = + let tr = + EConstr.mkLambda + ( name "x" + , i.EInjT.source + , EConstr.mkLambda + ( name "y" + , i.EInjT.source + , EConstr.mkApp + ( tr + , [| EConstr.mkApp (i.EInjT.inj, [|EConstr.mkRel 2|]) + ; EConstr.mkApp (i.EInjT.inj, [|EConstr.mkRel 1|]) |] ) ) ) + in + (r, tr) + +(** [classify_op mkconvert op top] takes the injection [inj] for the origin operator [op] + and the destination operator [top] -- both [op] and [top] are closed terms *) +let classify_op mkconvert inj op top = + let env = Global.env () in + let evd = Evd.from_env env in + if is_convertible env evd inj op then OpInj + else if EConstr.eq_constr evd op top then OpSame + else + let op, top = mkconvert op top in + if is_convertible env evd op top then OpConv else OpOther + +(*let classify_op mkconvert tysrc op top = + let res = classify_op mkconvert tysrc op top in + Feedback.msg_debug + Pp.( + str "classify_op:" ++ gl_pr_constr op ++ str " " ++ gl_pr_constr top + ++ str " " ++ pp_classify_op res ++ fnl ()); + res + *) module EBinOpT = struct type t = { (* Op : source1 -> source2 -> source3 *) @@ -105,17 +249,23 @@ module EBinOpT = struct ; source2 : EConstr.t ; source3 : EConstr.t ; target : EConstr.t - ; inj1 : EConstr.t - ; (* InjTyp source1 target *) - inj2 : EConstr.t - ; (* InjTyp source2 target *) - inj3 : EConstr.t - ; (* InjTyp source3 target *) - tbop : EConstr.t (* TBOpInj *) } + ; inj1 : EInjT.t (* InjTyp source1 target *) + ; inj2 : EInjT.t (* InjTyp source2 target *) + ; inj3 : EInjT.t (* InjTyp source3 target *) + ; bop : EConstr.t (* BOP *) + ; tbop : EConstr.t (* TBOP *) + ; tbopinj : EConstr.t (* TBOpInj *) + ; classify_binop : classify_op } end module ECstOpT = struct - type t = {source : EConstr.t; target : EConstr.t; inj : EConstr.t} + type t = + { source : EConstr.t + ; target : EConstr.t + ; inj : EInjT.t + ; cst : EConstr.t + ; cstinj : EConstr.t + ; is_construct : bool } end module EUnOpT = struct @@ -123,28 +273,42 @@ module EUnOpT = struct { source1 : EConstr.t ; source2 : EConstr.t ; target : EConstr.t - ; inj1_t : EConstr.t - ; inj2_t : EConstr.t - ; unop : EConstr.t } + ; uop : EConstr.t + ; inj1_t : EInjT.t + ; inj2_t : EInjT.t + ; tuop : EConstr.t + ; tuopinj : EConstr.t + ; classify_unop : classify_op + ; is_construct : bool } end module EBinRelT = struct type t = - {source : EConstr.t; target : EConstr.t; inj : EConstr.t; brel : EConstr.t} + { source : EConstr.t + ; target : EConstr.t + ; inj : EInjT.t + ; brel : EConstr.t + ; tbrel : EConstr.t + ; brelinj : EConstr.t + ; classify_rel : classify_op } end module EPropBinOpT = struct - type t = EConstr.t + type t = {op : EConstr.t; op_iff : EConstr.t} end module EPropUnOpT = struct - type t = EConstr.t + type t = {op : EConstr.t; op_iff : EConstr.t} end module ESatT = struct type t = {parg1 : EConstr.t; parg2 : EConstr.t; satOK : EConstr.t} end +module ESpecT = struct + type t = {spec : EConstr.t} +end + (* Different type of declarations *) type decl_kind = | PropOp of EPropBinOpT.t decl @@ -155,16 +319,7 @@ type decl_kind = | UnOp of EUnOpT.t decl | CstOp of ECstOpT.t decl | Saturate of ESatT.t decl - -let get_decl = function - | PropOp d -> d.decl - | PropUnOp d -> d.decl - | InjTyp d -> d.decl - | BinRel d -> d.decl - | BinOp d -> d.decl - | UnOp d -> d.decl - | CstOp d -> d.decl - | Saturate d -> d.decl + | Spec of ESpecT.t decl type term_kind = Application of EConstr.constr | OtherTerm of EConstr.constr @@ -191,8 +346,10 @@ end let table = Summary.ref ~name:"zify_table" HConstr.empty let saturate = Summary.ref ~name:"zify_saturate" HConstr.empty +let specs = Summary.ref ~name:"zify_specs" HConstr.empty let table_cache = ref HConstr.empty let saturate_cache = ref HConstr.empty +let specs_cache = ref HConstr.empty (** Each type-class gives rise to a different table. They only differ on how projections are extracted. *) @@ -207,7 +364,7 @@ module EInj = struct let dest = function InjTyp x -> Some x | _ -> None let mk_elt evd i (a : EConstr.t array) = - let isid = EConstr.eq_constr evd a.(0) a.(1) in + let isid = EConstr.eq_constr_nounivs evd a.(0) a.(1) in { isid ; source = a.(0) ; target = a.(1) @@ -218,6 +375,14 @@ module EInj = struct let get_key = 0 end +let get_inj evd c = + match get_projections_from_constant (evd, c) with + | None -> + let env = Global.env () in + let t = string_of_ppcmds (pr_constr env evd c) in + failwith ("Cannot register term " ^ t) + | Some a -> EInj.mk_elt evd c a + module EBinOp = struct type elt = EBinOpT.t @@ -227,20 +392,34 @@ module EBinOp = struct let table = table let mk_elt evd i a = + let i1 = get_inj evd a.(5) in + let i2 = get_inj evd a.(6) in + let i3 = get_inj evd a.(7) in + let tbop = a.(8) in { source1 = a.(0) ; source2 = a.(1) ; source3 = a.(2) ; target = a.(3) - ; inj1 = a.(5) - ; inj2 = a.(6) - ; inj3 = a.(7) - ; tbop = a.(9) } + ; inj1 = i1 + ; inj2 = i2 + ; inj3 = i3 + ; bop = a.(4) + ; tbop = a.(8) + ; tbopinj = a.(9) + ; classify_binop = + classify_op (mkconvert_binop i1 i2 i3) i1.EInjT.inj a.(4) tbop } let get_key = 4 let cast x = BinOp x let dest = function BinOp x -> Some x | _ -> None end +(*let debug_term msg c = + let genv = Global.env () in + Feedback.msg_debug + Pp.(str msg ++ str " " ++ pr_constr genv (Evd.from_env genv) c); + c + *) module ECstOp = struct type elt = ECstOpT.t @@ -250,7 +429,15 @@ module ECstOp = struct let table = table let cast x = CstOp x let dest = function CstOp x -> Some x | _ -> None - let mk_elt evd i a = {source = a.(0); target = a.(1); inj = a.(3)} + + let mk_elt evd i a = + { source = a.(0) + ; target = a.(1) + ; inj = get_inj evd a.(3) + ; cst = a.(4) + ; cstinj = a.(5) + ; is_construct = EConstr.isConstruct evd a.(2) } + let get_key = 2 end @@ -265,12 +452,21 @@ module EUnOp = struct let dest = function UnOp x -> Some x | _ -> None let mk_elt evd i a = + let i1 = get_inj evd a.(4) in + let i2 = get_inj evd a.(5) in + let uop = a.(3) in + let tuop = a.(6) in { source1 = a.(0) ; source2 = a.(1) ; target = a.(2) - ; inj1_t = a.(4) - ; inj2_t = a.(5) - ; unop = a.(6) } + ; uop + ; inj1_t = i1 + ; inj2_t = i2 + ; tuop + ; tuopinj = a.(7) + ; is_construct = EConstr.isConstruct evd uop + ; classify_unop = classify_op (mkconvert_unop i1 i2) i1.EInjT.inj uop tuop + } let get_key = 3 end @@ -286,40 +482,48 @@ module EBinRel = struct let dest = function BinRel x -> Some x | _ -> None let mk_elt evd i a = - {source = a.(0); target = a.(1); inj = a.(3); brel = a.(4)} + let i = get_inj evd a.(3) in + let brel = a.(2) in + let tbrel = a.(4) in + { source = a.(0) + ; target = a.(1) + ; inj = get_inj evd a.(3) + ; brel + ; tbrel + ; brelinj = a.(5) + ; classify_rel = classify_op (mkconvert_rel i) i.EInjT.inj brel tbrel } let get_key = 2 end -module EPropOp = struct - type elt = EConstr.t +module EPropBinOp = struct + type elt = EPropBinOpT.t + + open EPropBinOpT let name = "PropBinOp" let table = table let cast x = PropOp x let dest = function PropOp x -> Some x | _ -> None - let mk_elt evd i a = i + let mk_elt evd i a = {op = a.(0); op_iff = a.(1)} let get_key = 0 end module EPropUnOp = struct - type elt = EConstr.t + type elt = EPropUnOpT.t + + open EPropUnOpT let name = "PropUnOp" let table = table let cast x = PropUnOp x let dest = function PropUnOp x -> Some x | _ -> None - let mk_elt evd i a = i + let mk_elt evd i a = {op = a.(0); op_iff = a.(1)} let get_key = 0 end let constr_of_term_kind = function Application c -> c | OtherTerm c -> c -let fold_declared_const f evd acc = - HConstr.fold - (fun _ (_, e) acc -> f (fst (EConstr.destConst evd (get_decl e))) acc) - !table_cache acc - module type S = sig val register : Constrexpr.constr_expr -> unit val print : unit -> unit @@ -417,118 +621,37 @@ module ESat = struct let get_key = 1 end +module ESpec = struct + open ESpecT + + type elt = ESpecT.t + + let name = "Spec" + let table = specs + let cast x = Spec x + let dest = function Spec x -> Some x | _ -> None + let mk_elt evd i a = {spec = a.(5)} + let get_key = 2 +end + module BinOp = MakeTable (EBinOp) module UnOp = MakeTable (EUnOp) module CstOp = MakeTable (ECstOp) module BinRel = MakeTable (EBinRel) -module PropOp = MakeTable (EPropOp) +module PropBinOp = MakeTable (EPropBinOp) module PropUnOp = MakeTable (EPropUnOp) module Saturate = MakeTable (ESat) +module Spec = MakeTable (ESpec) let init_cache () = table_cache := !table; - saturate_cache := !saturate - -(** The module [Spec] is used to register - the instances of [BinOpSpec], [UnOpSpec]. - They are not indexed and stored in a list. *) - -module Spec = struct - let table = Summary.ref ~name:"zify_Spec" [] - - let register_obj : Constr.constr -> Libobject.obj = - let cache_constr (_, c) = table := EConstr.of_constr c :: !table in - let subst_constr (subst, c) = Mod_subst.subst_mps subst c in - Libobject.declare_object - @@ Libobject.superglobal_object_nodischarge "register-zify-Spec" - ~cache:cache_constr ~subst:(Some subst_constr) - - let register c = - let env = Global.env () in - let evd = Evd.from_env env in - let _, c = Constrintern.interp_open_constr env evd c in - let _ = Lib.add_anonymous_leaf (register_obj (EConstr.to_constr evd c)) in - () - - let get () = !table - - let print () = - let env = Global.env () in - let evd = Evd.from_env env in - let constr_of_spec c = - let t = get_type_of env evd c in - match EConstr.kind evd t with - | App (intyp, args) -> pr_constr env evd args.(2) - | _ -> Pp.str "" - in - let l = - List.fold_left - (fun acc c -> Pp.(constr_of_spec c ++ str " " ++ acc)) - (Pp.str "") !table - in - Feedback.msg_notice l -end - -let unfold_decl evd = - let f cst acc = cst :: acc in - fold_declared_const f evd [] + saturate_cache := !saturate; + specs_cache := !specs open EInjT (** Get constr of lemma and projections in ZifyClasses. *) -let zify str = - EConstr.of_constr - (UnivGen.constr_of_monomorphic_global - (Coqlib.lib_ref ("ZifyClasses." ^ str))) - -let locate_const str = - let rf = "ZifyClasses." ^ str in - match Coqlib.lib_ref rf with - | GlobRef.ConstRef c -> c - | _ -> CErrors.anomaly Pp.(str rf ++ str " should be a constant") - -(* The following [constr] are necessary for constructing the proof terms *) -let mkapp2 = lazy (zify "mkapp2") -let mkapp = lazy (zify "mkapp") -let mkapp0 = lazy (zify "mkapp0") -let mkdp = lazy (zify "mkinjterm") -let eq_refl = lazy (zify "eq_refl") -let mkrel = lazy (zify "mkrel") -let mkprop_op = lazy (zify "mkprop_op") -let mkuprop_op = lazy (zify "mkuprop_op") -let mkdpP = lazy (zify "mkinjprop") -let iff_refl = lazy (zify "iff_refl") -let q = lazy (zify "target_prop") -let ieq = lazy (zify "injprop_ok") -let iff = lazy (zify "iff") - -(* A super-set of the previous are needed to unfold the generated proof terms. *) - -let to_unfold = - lazy - (List.rev_map locate_const - [ "source_prop" - ; "target_prop" - ; "uop_iff" - ; "op_iff" - ; "mkuprop_op" - ; "TUOp" - ; "inj_ok" - ; "TRInj" - ; "inj" - ; "source" - ; "injprop_ok" - ; "TR" - ; "TBOp" - ; "TCst" - ; "target" - ; "mkrel" - ; "mkapp2" - ; "mkapp" - ; "mkapp0" - ; "mkprop_op" ]) - (** Module [CstrTable] records terms [x] injected into [inj x] together with the corresponding type constraint. The terms are stored by side-effect during the traversal @@ -563,7 +686,10 @@ module CstrTable = struct List.iter (fun (_, (t : EConstr.types)) -> HConstr.add hyps_table t ()) (Tacmach.New.pf_hyps_types gl); - fun c -> HConstr.mem hyps_table c + fun c -> + let m = HConstr.mem hyps_table c in + if not m then HConstr.add hyps_table c (); + m in (* Add the constraint (cstr k) if it is not already present *) let gen k cstr = @@ -585,97 +711,183 @@ module CstrTable = struct Tacticals.New.tclIDTAC table) end -let mkvar red evd inj v = - ( if not red then - match inj.cstr with None -> () | Some ctr -> CstrTable.register evd v ctr ); - let iv = EConstr.mkApp (inj.inj, [|v|]) in - let iv = if red then Tacred.compute (Global.env ()) evd iv else iv in - EConstr.mkApp - ( force mkdp - , [| inj.source - ; inj.target - ; inj.inj - ; v - ; iv - ; EConstr.mkApp (force eq_refl, [|inj.target; iv|]) |] ) - -type texpr = - | Var of EInj.elt * EConstr.t - (** Var is a term that cannot be injected further *) - | Constant of EInj.elt * EConstr.t - (** Constant is a term that is solely built from constructors *) - | Injterm of EConstr.t - (** Injected is an injected term represented by a term of type [injterm] *) - -let is_constant = function Constant _ -> true | _ -> false - -let constr_of_texpr = function - | Constant (i, e) | Var (i, e) -> if i.isid then Some e else None - | _ -> None - -let inj_term_of_texpr evd = function - | Injterm e -> e - | Var (inj, e) -> mkvar false evd inj e - | Constant (inj, e) -> mkvar true evd inj e - -let mkapp2_id evd i (* InjTyp S3 T *) inj (* deriv i *) t (* S1 -> S2 -> S3 *) b - (* Binop S1 S2 S3 t ... *) dbop (* deriv b *) e1 e2 = - let default () = - let e1' = inj_term_of_texpr evd e1 in - let e2' = inj_term_of_texpr evd e2 in - EBinOpT.( - Injterm - (EConstr.mkApp - ( force mkapp2 - , [| dbop.source1 - ; dbop.source2 - ; dbop.source3 - ; dbop.target - ; t - ; dbop.inj1 - ; dbop.inj2 - ; dbop.inj3 - ; b - ; e1' - ; e2' |] ))) +type prf = + | Term (* source is built from constructors. + target = compute(inj source) + inj source == target *) + | Same (* target = source + inj source == inj target *) + | Conv of EConstr.t (* inj source == target *) + | Prf of EConstr.t * EConstr.t + +(** [eq_proof typ source target] returns (target = target : source = target) *) +let eq_proof typ source target = + EConstr.mkCast + ( EConstr.mkApp (force eq_refl, [|typ; target|]) + , DEFAULTcast + , EConstr.mkApp (force eq, [|typ; source; target|]) ) + +let interp_prf evd inj source prf = + let inj_source = + if inj.EInjT.isid then source else EConstr.mkApp (inj.EInjT.inj, [|source|]) in - if not inj.isid then default () - else - match (e1, e2) with - | Constant (_, e1), Constant (_, e2) - |Var (_, e1), Var (_, e2) - |Constant (_, e1), Var (_, e2) - |Var (_, e1), Constant (_, e2) -> - Var (inj, EConstr.mkApp (t, [|e1; e2|])) - | _, _ -> default () - -let mkapp_id evd i inj (unop, u) f e1 = - EUnOpT.( - if EConstr.eq_constr evd u.unop f then - (* Injection does nothing *) - match e1 with - | Constant (_, e) | Var (_, e) -> Var (inj, EConstr.mkApp (f, [|e|])) - | Injterm e1 -> - Injterm - (EConstr.mkApp - ( force mkapp - , [| u.source1 - ; u.source2 - ; u.target - ; f - ; u.inj1_t - ; u.inj2_t - ; unop - ; e1 |] )) + match prf with + | Term -> + let target = Tacred.compute (Global.env ()) evd inj_source in + (target, EConstr.mkApp (force eq_refl, [|inj.target; target|])) + | Same -> + (inj_source, EConstr.mkApp (force eq_refl, [|inj.target; inj_source|])) + | Conv trm -> (trm, eq_proof inj.target inj_source trm) + | Prf (target, prf) -> (target, prf) + +let pp_prf prf = + match prf with + | Term -> Pp.str "Term" + | Same -> Pp.str "Same" + | Conv t -> Pp.(str "Conv " ++ gl_pr_constr t) + | Prf (_, _) -> Pp.str "Prf " + +let interp_prf evd inj source prf = + let t, prf' = interp_prf evd inj source prf in + if debug then + Feedback.msg_debug + Pp.( + str "interp_prf " ++ gl_pr_constr inj.EInjT.inj ++ str " " + ++ gl_pr_constr source ++ str " = " ++ gl_pr_constr t ++ str " by " + ++ gl_pr_constr prf' ++ str " from " ++ pp_prf prf ++ fnl ()); + (t, prf') + +let mkvar evd inj e = + (match inj.cstr with None -> () | Some ctr -> CstrTable.register evd e ctr); + Same + +let pp_prf evd inj src prf = + let t, prf' = interp_prf evd inj src prf in + Pp.( + gl_pr_constr inj.EInjT.inj ++ str " " ++ gl_pr_constr src ++ str " = " + ++ gl_pr_constr t ++ str " by " + ++ + match prf with + | Term -> Pp.str "Term" + | Same -> Pp.str "Same" + | Conv t -> Pp.str "Conv" + | Prf (_, p) -> Pp.str "Prf " ++ gl_pr_constr p) + +let conv_of_term evd op isid arg = + Tacred.compute (Global.env ()) evd + (if isid then arg else EConstr.mkApp (op, [|arg|])) + +let app_unop evd src unop arg prf = + let cunop = unop.EUnOpT.classify_unop in + let default a' prf' = + let target = EConstr.mkApp (unop.EUnOpT.tuop, [|a'|]) in + EUnOpT.( + Prf + ( target + , EConstr.mkApp + ( force mkapp + , [| unop.source1 + ; unop.source2 + ; unop.target + ; unop.uop + ; unop.inj1_t.EInjT.inj + ; unop.inj2_t.EInjT.inj + ; unop.tuop + ; unop.tuopinj + ; arg + ; a' + ; prf' |] ) )) + in + match prf with + | Term -> ( + if unop.EUnOpT.is_construct then Term (* Keep rebuilding *) else - let e1 = inj_term_of_texpr evd e1 in - Injterm + match cunop with + | OpInj -> Conv (conv_of_term evd unop.EUnOpT.uop false arg) + | OpSame -> Same + | _ -> + let a', prf = interp_prf evd unop.EUnOpT.inj1_t arg prf in + default a' prf ) + | Same -> ( + match cunop with + | OpSame -> Same + | OpInj -> Same + | OpConv -> + Conv (EConstr.mkApp - ( force mkapp - , [|u.source1; u.source2; u.target; f; u.inj1_t; u.inj2_t; unop; e1|] - ))) - -type typed_constr = {constr : EConstr.t; typ : EConstr.t} + ( unop.EUnOpT.tuop + , [|EConstr.mkApp (unop.EUnOpT.inj1_t.EInjT.inj, [|arg|])|] )) + | OpOther -> + let a', prf' = interp_prf evd unop.EUnOpT.inj1_t arg prf in + default a' prf' ) + | Conv a' -> ( + match cunop with + | OpSame | OpConv -> Conv (EConstr.mkApp (unop.EUnOpT.tuop, [|a'|])) + | OpInj -> Conv a' + | _ -> + let a', prf = interp_prf evd unop.EUnOpT.inj1_t arg prf in + default a' prf ) + | Prf (a', prf') -> default a' prf' + +let app_unop evd src unop arg prf = + let res = app_unop evd src unop arg prf in + if debug then + Feedback.msg_debug + Pp.( + str "\napp_unop " + ++ pp_prf evd unop.EUnOpT.inj1_t arg prf + ++ str " => " + ++ pp_prf evd unop.EUnOpT.inj2_t src res); + res + +let app_binop evd src binop arg1 prf1 arg2 prf2 = + EBinOpT.( + let mkApp a1 a2 = EConstr.mkApp (binop.tbop, [|a1; a2|]) in + let to_conv inj arg = function + | Term -> conv_of_term evd inj.EInjT.inj inj.EInjT.isid arg + | Same -> + if inj.EInjT.isid then arg else EConstr.mkApp (inj.EInjT.inj, [|arg|]) + | Conv t -> t + | Prf _ -> failwith "Prf is not convertible" + in + let default a1 prf1 a2 prf2 = + let res = mkApp a1 a2 in + let prf = + EBinOpT.( + EConstr.mkApp + ( force mkapp2 + , [| binop.source1 + ; binop.source2 + ; binop.source3 + ; binop.target + ; binop.bop + ; binop.inj1.EInjT.inj + ; binop.inj2.EInjT.inj + ; binop.inj3.EInjT.inj + ; binop.tbop + ; binop.tbopinj + ; arg1 + ; a1 + ; prf1 + ; arg2 + ; a2 + ; prf2 |] )) + in + Prf (res, prf) + in + match (binop.EBinOpT.classify_binop, prf1, prf2) with + | OpSame, Same, Same -> Same + | OpSame, Term, Same | OpSame, Same, Term -> Same + | OpSame, (Term | Same | Conv _), (Term | Same | Conv _) -> + let t1 = to_conv binop.EBinOpT.inj1 arg1 prf1 in + let t2 = to_conv binop.EBinOpT.inj1 arg2 prf2 in + Conv (mkApp t1 t2) + | _, _, _ -> + let a1, prf1 = interp_prf evd binop.inj1 arg1 prf1 in + let a2, prf2 = interp_prf evd binop.inj2 arg2 prf2 in + default a1 prf1 a2 prf2) + +type typed_constr = {constr : EConstr.t; typ : EConstr.t; inj : EInjT.t} let get_injection env evd t = match snd (HConstr.find t !table_cache) with @@ -702,23 +914,68 @@ let is_prop env sigma term = let sort = Retyping.get_sort_of env sigma term in Sorts.is_prop sort -(** [get_application env evd e] expresses [e] as an application (c a) +let is_arrow env evd a p1 p2 = + is_prop env evd p1 + && is_prop + (EConstr.push_rel (Context.Rel.Declaration.LocalAssum (a, p1)) env) + evd p2 + && (a.Context.binder_name = Names.Anonymous || EConstr.Vars.noccurn evd 1 p2) + +(** [get_operator env evd e] expresses [e] as an application (c a) where c is the head symbol and [a] is the array of arguments. The function also transforms (x -> y) as (arrow x y) *) -let get_operator env evd e = - let is_arrow a p1 p2 = - is_prop env evd p1 - && is_prop - (EConstr.push_rel (Context.Rel.Declaration.LocalAssum (a, p1)) env) - evd p2 - && (a.Context.binder_name = Names.Anonymous || EConstr.Vars.noccurn evd 1 p2) - in +let get_operator barrow env evd e = match EConstr.kind evd e with - | Prod (a, p1, p2) when is_arrow a p1 p2 -> (arrow, [|p1; p2|]) + | Prod (a, p1, p2) -> + if barrow && is_arrow env evd a p1 p2 then (arrow, [|p1; p2|]) + else raise Not_found + | App (c, a) -> ( + match EConstr.kind evd c with + | Construct _ (* e.g. Z0 , Z.pos *) | Const _ (* e.g. Z.max *) | Proj _ + |Lambda _ (* e.g projections *) | Ind _ (* e.g. eq *) -> + (c, a) + | _ -> raise Not_found ) + | Construct _ -> (EConstr.whd_evar evd e, [||]) + | _ -> raise Not_found + +let decompose_app env evd e = + match EConstr.kind evd e with + | Prod (a, p1, p2) when is_arrow env evd a p1 p2 -> (arrow, [|p1; p2|]) | App (c, a) -> (c, a) - | _ -> (e, [||]) + | _ -> (EConstr.whd_evar evd e, [||]) + +type 'op propop = {op : 'op; op_constr : EConstr.t; op_iff : EConstr.t} -let is_convertible env evd k t = Reductionops.check_conv env evd k t +let mk_propop op c1 c2 = {op; op_constr = c1; op_iff = c2} + +type prop_binop = AND | OR | IFF | IMPL +type prop_unop = NOT + +type prop_op = + | BINOP of prop_binop propop * EConstr.t * EConstr.t + | UNOP of prop_unop propop * EConstr.t + | OTHEROP of EConstr.t * EConstr.t array + +let classify_prop env evd e = + match EConstr.kind evd e with + | Prod (a, p1, p2) when is_arrow env evd a p1 p2 -> + BINOP (mk_propop IMPL arrow (force op_impl_morph), p1, p2) + | App (c, a) -> ( + match Array.length a with + | 1 -> + if EConstr.eq_constr_nounivs evd (force op_not) c then + UNOP (mk_propop NOT c (force op_not_morph), a.(0)) + else OTHEROP (c, a) + | 2 -> + if EConstr.eq_constr_nounivs evd (force op_and) c then + BINOP (mk_propop AND c (force op_and_morph), a.(0), a.(1)) + else if EConstr.eq_constr_nounivs evd (force op_or) c then + BINOP (mk_propop OR c (force op_or_morph), a.(0), a.(1)) + else if EConstr.eq_constr_nounivs evd (force op_iff) c then + BINOP (mk_propop IFF c (force op_iff_morph), a.(0), a.(1)) + else OTHEROP (c, a) + | _ -> OTHEROP (c, a) ) + | _ -> OTHEROP (e, [||]) (** [match_operator env evd hd arg (t,d)] - hd is head operator of t @@ -744,223 +1001,242 @@ let match_operator env evd hd args (t, d) = | PropUnOp _ -> decomp t 1 | _ -> None ) +let pp_trans_expr env evd e res = + let {deriv = inj} = get_injection env evd e.typ in + if debug then + Feedback.msg_debug Pp.(str "\ntrans_expr " ++ pp_prf evd inj e.constr res); + res + let rec trans_expr env evd e = - (* Get the injection *) - let {decl = i; deriv = inj} = get_injection env evd e.typ in + let inj = e.inj in let e = e.constr in - if EConstr.isConstruct evd e then Constant (inj, e) (* Evaluate later *) - else - let c, a = get_operator env evd e in - try - let k, t = - find_option - (match_operator env evd c a) - (HConstr.find_all c !table_cache) + try + let c, a = get_operator false env evd e in + let k, t = + find_option (match_operator env evd c a) (HConstr.find_all c !table_cache) + in + let n = Array.length a in + match k with + | CstOp {deriv = c'} -> + ECstOpT.(if c'.is_construct then Term else Prf (c'.cst, c'.cstinj)) + | UnOp {deriv = unop} -> + let prf = + trans_expr env evd + { constr = a.(n - 1) + ; typ = unop.EUnOpT.source1 + ; inj = unop.EUnOpT.inj1_t } in - let n = Array.length a in - match k with - | CstOp {decl = c'} -> - Injterm - (EConstr.mkApp (force mkapp0, [|inj.source; inj.target; e; i; c'|])) - | UnOp {decl = unop; deriv = u} -> - let a' = - trans_expr env evd {constr = a.(n - 1); typ = u.EUnOpT.source1} - in - if is_constant a' && EConstr.isConstruct evd t then Constant (inj, e) - else mkapp_id evd i inj (unop, u) t a' - | BinOp {decl = binop; deriv = b} -> - let a0 = - trans_expr env evd {constr = a.(n - 2); typ = b.EBinOpT.source1} - in - let a1 = - trans_expr env evd {constr = a.(n - 1); typ = b.EBinOpT.source2} - in - if is_constant a0 && is_constant a1 && EConstr.isConstruct evd t then - Constant (inj, e) - else mkapp2_id evd i inj t binop b a0 a1 - | d -> Var (inj, e) - with Not_found -> Var (inj, e) + app_unop evd e unop a.(n - 1) prf + | BinOp {deriv = binop} -> + let prf1 = + trans_expr env evd + { constr = a.(n - 2) + ; typ = binop.EBinOpT.source1 + ; inj = binop.EBinOpT.inj1 } + in + let prf2 = + trans_expr env evd + { constr = a.(n - 1) + ; typ = binop.EBinOpT.source2 + ; inj = binop.EBinOpT.inj2 } + in + app_binop evd e binop a.(n - 2) prf1 a.(n - 1) prf2 + | d -> mkvar evd inj e + with Not_found -> + (* Feedback.msg_debug + Pp.(str "Not found " ++ Termops.Internal.debug_print_constr e); *) + mkvar evd inj e let trans_expr env evd e = - try trans_expr env evd e + try pp_trans_expr env evd e (trans_expr env evd e) with Not_found -> raise (CErrors.user_err ( Pp.str "Missing injection for type " ++ Printer.pr_leconstr_env env evd e.typ )) -type tprop = - | TProp of EConstr.t (** Transformed proposition *) - | IProp of EConstr.t (** Identical proposition *) - -let mk_iprop e = - EConstr.mkApp (force mkdpP, [|e; e; EConstr.mkApp (force iff_refl, [|e|])|]) - -let inj_prop_of_tprop = function TProp p -> p | IProp e -> mk_iprop e +type prfp = + | TProof of EConstr.t * EConstr.t (** Proof of tranformed proposition *) + | CProof of EConstr.t (** Transformed proposition is convertible *) + | IProof (** Transformed proposition is identical *) + +let pp_prfp = function + | TProof (t, prf) -> + Pp.str "TProof " ++ gl_pr_constr t ++ Pp.str " by " ++ gl_pr_constr prf + | CProof t -> Pp.str "CProof " ++ gl_pr_constr t + | IProof -> Pp.str "IProof" + +let trans_binrel evd src rop a1 prf1 a2 prf2 = + EBinRelT.( + match (rop.classify_rel, prf1, prf2) with + | OpSame, Same, Same -> IProof + | (OpSame | OpConv), Conv t1, Conv t2 -> + CProof (EConstr.mkApp (rop.tbrel, [|t1; t2|])) + | (OpSame | OpConv), (Same | Term | Conv _), (Same | Term | Conv _) -> + let a1', _ = interp_prf evd rop.inj a1 prf1 in + let a2', _ = interp_prf evd rop.inj a2 prf2 in + CProof (EConstr.mkApp (rop.tbrel, [|a1'; a2'|])) + | _, _, _ -> + let a1', prf1 = interp_prf evd rop.inj a1 prf1 in + let a2', prf2 = interp_prf evd rop.inj a2 prf2 in + TProof + ( EConstr.mkApp (rop.EBinRelT.tbrel, [|a1'; a2'|]) + , EConstr.mkApp + ( force mkrel + , [| rop.source + ; rop.target + ; rop.brel + ; rop.EBinRelT.inj.EInjT.inj + ; rop.EBinRelT.tbrel + ; rop.EBinRelT.brelinj + ; a1 + ; a1' + ; prf1 + ; a2 + ; a2' + ; prf2 |] ) )) + +let trans_binrel evd src rop a1 prf1 a2 prf2 = + let res = trans_binrel evd src rop a1 prf1 a2 prf2 in + if debug then Feedback.msg_debug Pp.(str "\ntrans_binrel " ++ pp_prfp res); + res + +let mkprf t p = + EConstr.( + match p with + | IProof -> (t, mkApp (force iff_refl, [|t|])) + | CProof t' -> (t', mkApp (force eq_iff, [|t; t'; eq_proof mkProp t t'|])) + | TProof (t', p) -> (t', p)) + +let mkprf t p = + let t', p = mkprf t p in + if debug then + Feedback.msg_debug + Pp.( + str "mkprf " ++ gl_pr_constr t ++ str " <-> " ++ gl_pr_constr t' + ++ str " by " ++ gl_pr_constr p); + (t', p) + +let trans_bin_prop op_constr op_iff t1 p1 t2 p2 = + match (p1, p2) with + | IProof, IProof -> IProof + | CProof t1', IProof -> CProof (EConstr.mkApp (op_constr, [|t1'; t2|])) + | IProof, CProof t2' -> CProof (EConstr.mkApp (op_constr, [|t1; t2'|])) + | CProof t1', CProof t2' -> CProof (EConstr.mkApp (op_constr, [|t1'; t2'|])) + | _, _ -> + let t1', p1 = mkprf t1 p1 in + let t2', p2 = mkprf t2 p2 in + TProof + ( EConstr.mkApp (op_constr, [|t1'; t2'|]) + , EConstr.mkApp (op_iff, [|t1; t2; t1'; t2'; p1; p2|]) ) + +let trans_bin_prop op_constr op_iff t1 p1 t2 p2 = + let prf = trans_bin_prop op_constr op_iff t1 p1 t2 p2 in + if debug then Feedback.msg_debug (pp_prfp prf); + prf + +let trans_un_prop op_constr op_iff p1 prf1 = + match prf1 with + | IProof -> IProof + | CProof p1' -> CProof (EConstr.mkApp (op_constr, [|p1'|])) + | TProof (p1', prf) -> + TProof + ( EConstr.mkApp (op_constr, [|p1'|]) + , EConstr.mkApp (op_iff, [|p1; p1'; prf|]) ) let rec trans_prop env evd e = - let c, a = get_operator env evd e in - try - let k, t = - find_option (match_operator env evd c a) (HConstr.find_all c !table_cache) - in - let n = Array.length a in - match k with - | PropOp {decl = rop} -> ( - try - let t1 = trans_prop env evd a.(n - 2) in - let t2 = trans_prop env evd a.(n - 1) in - match (t1, t2) with - | IProp _, IProp _ -> IProp e - | _, _ -> - let t1 = inj_prop_of_tprop t1 in - let t2 = inj_prop_of_tprop t2 in - TProp (EConstr.mkApp (force mkprop_op, [|t; rop; t1; t2|])) - with Not_found -> IProp e ) - | BinRel {decl = br; deriv = rop} -> ( - try + match classify_prop env evd e with + | BINOP ({op_constr; op_iff}, p1, p2) -> + let prf1 = trans_prop env evd p1 in + let prf2 = trans_prop env evd p2 in + trans_bin_prop op_constr op_iff p1 prf1 p2 prf2 + | UNOP ({op_constr; op_iff}, p1) -> + let prf1 = trans_prop env evd p1 in + trans_un_prop op_constr op_iff p1 prf1 + | OTHEROP (c, a) -> ( + try + let k, t = + find_option + (match_operator env evd c a) + (HConstr.find_all c !table_cache) + in + let n = Array.length a in + match k with + | BinRel {decl = br; deriv = rop} -> let a1 = - trans_expr env evd {constr = a.(n - 2); typ = rop.EBinRelT.source} + trans_expr env evd + { constr = a.(n - 2) + ; typ = rop.EBinRelT.source + ; inj = rop.EBinRelT.inj } in let a2 = - trans_expr env evd {constr = a.(n - 1); typ = rop.EBinRelT.source} + trans_expr env evd + { constr = a.(n - 1) + ; typ = rop.EBinRelT.source + ; inj = rop.EBinRelT.inj } in - if EConstr.eq_constr evd t rop.EBinRelT.brel then - match (constr_of_texpr a1, constr_of_texpr a2) with - | Some e1, Some e2 -> IProp (EConstr.mkApp (t, [|e1; e2|])) - | _, _ -> - let a1 = inj_term_of_texpr evd a1 in - let a2 = inj_term_of_texpr evd a2 in - TProp - (EConstr.mkApp - ( force mkrel - , [| rop.EBinRelT.source - ; rop.EBinRelT.target - ; t - ; rop.EBinRelT.inj - ; br - ; a1 - ; a2 |] )) - else - let a1 = inj_term_of_texpr evd a1 in - let a2 = inj_term_of_texpr evd a2 in - TProp - (EConstr.mkApp - ( force mkrel - , [| rop.EBinRelT.source - ; rop.EBinRelT.target - ; t - ; rop.EBinRelT.inj - ; br - ; a1 - ; a2 |] )) - with Not_found -> IProp e ) - | PropUnOp {decl = rop} -> ( - try - let t1 = trans_prop env evd a.(n - 1) in - match t1 with - | IProp _ -> IProp e - | _ -> - let t1 = inj_prop_of_tprop t1 in - TProp (EConstr.mkApp (force mkuprop_op, [|t; rop; t1|])) - with Not_found -> IProp e ) - | _ -> IProp e - with Not_found -> IProp e - -let unfold n env evd c = - let cbv l = - CClosure.RedFlags.( - Tacred.cbv_norm_flags - (mkflags - (fBETA :: fMATCH :: fFIX :: fCOFIX :: fZETA :: List.rev_map fCONST l))) - in - let unfold_decl = unfold_decl evd in - (* Unfold the let binding *) - let c = - match n with - | None -> c - | Some n -> - Tacred.unfoldn [(Locus.AllOccurrences, Names.EvalVarRef n)] env evd c - in - (* Reduce the term *) - let c = cbv (List.rev_append (force to_unfold) unfold_decl) env evd c in - c + trans_binrel evd e rop a.(n - 2) a1 a.(n - 1) a2 + | _ -> IProof + with Not_found -> IProof ) let trans_check_prop env evd t = - if is_prop env evd t then - (*let t = Tacred.unfoldn [Locus.AllOccurrences, Names.EvalConstRef coq_not] env evd t in*) - match trans_prop env evd t with IProp e -> None | TProp e -> Some e - else None + if is_prop env evd t then Some (trans_prop env evd t) else None + +let get_hyp_typ = function + | NamedDecl.LocalDef (h, _, ty) | NamedDecl.LocalAssum (h, ty) -> + (h.Context.binder_name, EConstr.of_constr ty) let trans_hyps env evd l = List.fold_left - (fun acc (h, p) -> - match trans_check_prop env evd p with + (fun acc decl -> + let h, ty = get_hyp_typ decl in + match trans_check_prop env evd ty with | None -> acc - | Some p' -> (h, p, p') :: acc) - [] (List.rev l) - -(* Only used if a direct rewrite fails *) -let trans_hyp h t = - Tactics.( + | Some p' -> (h, ty, p') :: acc) + [] l + +let trans_hyp h t0 prfp = + if debug then + Feedback.msg_debug Pp.(str "trans_hyp: " ++ pp_prfp prfp ++ fnl ()); + match prfp with + | IProof -> Tacticals.New.tclIDTAC (* Should detect before *) + | CProof t' -> + Proofview.Goal.enter (fun gl -> + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + let t' = Reductionops.nf_betaiota env evd t' in + Tactics.change_in_hyp ~check:true None + (Tactics.make_change_arg t') + (h, Locus.InHypTypeOnly)) + | TProof (t', prf) -> Tacticals.New.( Proofview.Goal.enter (fun gl -> let env = Tacmach.New.pf_env gl in - let n = - fresh_id_in_env Id.Set.empty (Names.Id.of_string "__zify") env + let evd = Tacmach.New.project gl in + let target = Reductionops.nf_betaiota env evd t' in + let h' = Tactics.fresh_id_in_env Id.Set.empty h env in + let prf = + EConstr.mkApp (force rew_iff, [|t0; target; prf; EConstr.mkVar h|]) in - let h' = fresh_id_in_env Id.Set.empty h env in - tclTHENLIST - [ letin_tac None (Names.Name n) t None - Locus.{onhyps = None; concl_occs = NoOccurrences} - ; assert_by (Name.Name h') - (EConstr.mkApp (force q, [|EConstr.mkVar n|])) - (tclTHEN - (Equality.rewriteRL - (EConstr.mkApp (force ieq, [|EConstr.mkVar n|]))) - (exact_check (EConstr.mkVar h))) - ; reduct_in_hyp ~check:true ~reorder:false (unfold (Some n)) - (h', Locus.InHyp) - ; clear [n] - ; (* [clear H] may fail if [h] has dependencies *) - tclTRY (clear [h]) ]))) - -let is_progress_rewrite evd t rew = - match EConstr.kind evd rew with - | App (c, [|lhs; rhs|]) -> - if EConstr.eq_constr evd (force iff) c then - (* This is a successful rewriting *) - not (EConstr.eq_constr evd lhs rhs) - else - CErrors.anomaly - Pp.( - str "is_progress_rewrite: not a rewrite" - ++ pr_constr (Global.env ()) evd rew) - | _ -> failwith "is_progress_rewrite: not even an application" - -let trans_hyp h t0 t = - Tacticals.New.( + tclTHEN + (Tactics.pose_proof (Name.Name h') prf) + (tclTRY + (tclTHEN (Tactics.clear [h]) (Tactics.rename_hyp [(h', h)]))))) + +let trans_concl prfp = + if debug then + Feedback.msg_debug Pp.(str "trans_concl: " ++ pp_prfp prfp ++ fnl ()); + match prfp with + | IProof -> Tacticals.New.tclIDTAC + | CProof t -> Proofview.Goal.enter (fun gl -> let env = Tacmach.New.pf_env gl in let evd = Tacmach.New.project gl in - let t' = unfold None env evd (EConstr.mkApp (force ieq, [|t|])) in - if is_progress_rewrite evd t0 (get_type_of env evd t') then - tclFIRST - [ Equality.general_rewrite_in true Locus.AllOccurrences true false h - t' false - ; trans_hyp h t ] - else tclIDTAC)) - -let trans_concl t = - Tacticals.New.( + let t' = Reductionops.nf_betaiota env evd t in + Tactics.change_concl t') + | TProof (t, prf) -> Proofview.Goal.enter (fun gl -> - let concl = Tacmach.New.pf_concl gl in - let env = Tacmach.New.pf_env gl in - let evd = Tacmach.New.project gl in - let t' = unfold None env evd (EConstr.mkApp (force ieq, [|t|])) in - if is_progress_rewrite evd concl (get_type_of env evd t') then - Equality.general_rewrite true Locus.AllOccurrences true false t' - else tclIDTAC)) + Equality.general_rewrite true Locus.AllOccurrences true false prf) let tclTHENOpt e tac tac' = match e with None -> tac' | Some e' -> Tacticals.New.tclTHEN (tac e') tac' @@ -976,6 +1252,16 @@ let assert_inj t = with Not_found -> Tacticals.New.tclFAIL 0 (Pp.str " InjTyp does not exist")) +let elim_binding x t ty = + Proofview.Goal.enter (fun gl -> + let env = Tacmach.New.pf_env gl in + let h = + Tactics.fresh_id_in_env Id.Set.empty (Nameops.add_prefix "heq_" x) env + in + Tacticals.New.tclTHEN + (Tactics.pose_proof (Name h) (eq_proof ty (EConstr.mkVar x) t)) + (Tacticals.New.tclTRY (Tactics.clear_body [x]))) + let do_let tac (h : Constr.named_declaration) = match h with | Context.Named.Declaration.LocalAssum _ -> Tacticals.New.tclIDTAC @@ -985,22 +1271,25 @@ let do_let tac (h : Constr.named_declaration) = let evd = Tacmach.New.project gl in try ignore (get_injection env evd (EConstr.of_constr ty)); - tac id.Context.binder_name t ty + tac id.Context.binder_name (EConstr.of_constr t) + (EConstr.of_constr ty) with Not_found -> Tacticals.New.tclIDTAC) -let iter_let tac = +let iter_let_aux tac = Proofview.Goal.enter (fun gl -> let env = Tacmach.New.pf_env gl in let sign = Environ.named_context env in + init_cache (); Tacticals.New.tclMAP (do_let tac) sign) let iter_let (tac : Ltac_plugin.Tacinterp.Value.t) = - init_cache (); - iter_let (fun (id : Names.Id.t) (t : Constr.types) (ty : Constr.types) -> + iter_let_aux (fun (id : Names.Id.t) t ty -> Ltac_plugin.Tacinterp.Value.apply tac [ Ltac_plugin.Tacinterp.Value.of_constr (EConstr.mkVar id) - ; Ltac_plugin.Tacinterp.Value.of_constr (EConstr.of_constr t) - ; Ltac_plugin.Tacinterp.Value.of_constr (EConstr.of_constr ty) ]) + ; Ltac_plugin.Tacinterp.Value.of_constr t + ; Ltac_plugin.Tacinterp.Value.of_constr ty ]) + +let elim_let = iter_let_aux elim_binding let zify_tac = Proofview.Goal.enter (fun gl -> @@ -1009,8 +1298,9 @@ let zify_tac = init_cache (); let evd = Tacmach.New.project gl in let env = Tacmach.New.pf_env gl in + let sign = Environ.named_context env in let concl = trans_check_prop env evd (Tacmach.New.pf_concl gl) in - let hyps = trans_hyps env evd (Tacmach.New.pf_hyps_types gl) in + let hyps = trans_hyps env evd sign in let l = CstrTable.get () in tclTHENOpt concl trans_concl (Tacticals.New.tclTHEN @@ -1018,14 +1308,101 @@ let zify_tac = (List.rev_map (fun (h, p, t) -> trans_hyp h p t) hyps)) (CstrTable.gen_cstr l))) -let iter_specs tac = - Tacticals.New.tclTHENLIST - (List.fold_left (fun acc d -> tac d :: acc) [] (Spec.get ())) +type pscript = Set of Names.Id.t * EConstr.t | Pose of Names.Id.t * EConstr.t + +type spec_env = + { map : Names.Id.t HConstr.t + ; spec_name : Names.Id.t + ; term_name : Names.Id.t + ; fresh : Nameops.Subscript.t + ; proofs : pscript list } + +let register_constr {map; spec_name; term_name; fresh; proofs} c thm = + let tname = Nameops.add_subscript term_name fresh in + let sname = Nameops.add_subscript spec_name fresh in + ( EConstr.mkVar tname + , { map = HConstr.add c tname map + ; spec_name + ; term_name + ; fresh = Nameops.Subscript.succ fresh + ; proofs = Set (tname, c) :: Pose (sname, thm) :: proofs } ) + +let fresh_subscript env = + let ctx = (Environ.named_context_val env).Environ.env_named_map in + Nameops.Subscript.succ + (Names.Id.Map.fold + (fun id _ s -> + let _, s' = Nameops.get_subscript id in + let cmp = Nameops.Subscript.compare s s' in + if cmp = 0 then s else if cmp < 0 then s' else s) + ctx Nameops.Subscript.zero) + +let init_env sname tname s = + { map = HConstr.empty + ; spec_name = sname + ; term_name = tname + ; fresh = s + ; proofs = [] } + +let rec spec_of_term env evd (senv : spec_env) t = + let get_name t env = + try EConstr.mkVar (HConstr.find t senv.map) with Not_found -> t + in + let c, a = decompose_app env evd t in + if a = [||] then (* The term cannot be decomposed. *) + (get_name t senv, senv) + else + (* recursively analyse the sub-terms *) + let a', senv' = + Array.fold_right + (fun e (l, senv) -> + let r, senv = spec_of_term env evd senv e in + (r :: l, senv)) + a ([], senv) + in + let a' = Array.of_list a' in + let t' = EConstr.mkApp (c, a') in + try (EConstr.mkVar (HConstr.find t' senv'.map), senv') + with Not_found -> ( + try + match snd (HConstr.find c !specs_cache) with + | Spec s -> + let thm = EConstr.mkApp (s.deriv.ESpecT.spec, a') in + register_constr senv' t' thm + | _ -> (get_name t' senv', senv') + with Not_found -> (t', senv') ) + +let interp_pscript s = + match s with + | Set (id, c) -> + Tacticals.New.tclTHEN + (Tactics.letin_tac None (Names.Name id) c None + {Locus.onhyps = None; Locus.concl_occs = Locus.AllOccurrences}) + (Tactics.clear_body [id]) + | Pose (id, c) -> Tactics.pose_proof (Names.Name id) c + +let rec interp_pscripts l = + match l with + | [] -> Tacticals.New.tclIDTAC + | s :: l -> Tacticals.New.tclTHEN (interp_pscript s) (interp_pscripts l) -let iter_specs (tac : Ltac_plugin.Tacinterp.Value.t) = - iter_specs (fun c -> - Ltac_plugin.Tacinterp.Value.apply tac - [Ltac_plugin.Tacinterp.Value.of_constr c]) +let spec_of_hyps = + Proofview.Goal.enter (fun gl -> + let terms = + Tacmach.New.pf_concl gl :: List.map snd (Tacmach.New.pf_hyps_types gl) + in + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + let s = fresh_subscript env in + let env = + List.fold_left + (fun acc t -> snd (spec_of_term env evd acc t)) + (init_env (Names.Id.of_string "H") (Names.Id.of_string "z") s) + terms + in + interp_pscripts (List.rev env.proofs)) + +let iter_specs = spec_of_hyps let find_hyp evd t l = try Some (fst (List.find (fun (h, t') -> EConstr.eq_constr evd t t') l)) diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli index 4930a845c9..2cec9d6f91 100644 --- a/plugins/micromega/zify.mli +++ b/plugins/micromega/zify.mli @@ -19,13 +19,14 @@ module UnOp : S module BinOp : S module CstOp : S module BinRel : S -module PropOp : S +module PropBinOp : S module PropUnOp : S module Spec : S module Saturate : S val zify_tac : unit Proofview.tactic val saturate : unit Proofview.tactic -val iter_specs : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic +val iter_specs : unit Proofview.tactic val assert_inj : EConstr.constr -> unit Proofview.tactic val iter_let : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic +val elim_let : unit Proofview.tactic diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index f95672a15d..6ff79ebb9b 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1095,11 +1095,11 @@ let tclDO n tac = try tac gl with | CErrors.UserError (l, s) as e -> - let _, info = CErrors.push e in - let e' = CErrors.UserError (l, prefix i ++ s) in - Util.iraise (e', info) + let _, info = Exninfo.capture e in + let e' = CErrors.UserError (l, prefix i ++ s) in + Exninfo.iraise (e', info) | Gramlib.Ploc.Exc(loc, CErrors.UserError (l, s)) -> - raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in + raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in let rec loop i gl = if i = n then tac_err_at i gl else (tclTHEN (tac_err_at i) (loop (i + 1))) gl in diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 3f67d55e73..cd7c7d660e 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -142,25 +142,6 @@ let add_genarg tag pr = Pptactic.declare_extra_genarg_pprule wit gen_pr gen_pr gen_pr; wit -(** Primitive parsing to avoid syntax conflicts with basic tactics. *) - -let accept_before_syms syms strm = - match Util.stream_nth 1 strm with - | Tok.KEYWORD sym when List.mem sym syms -> () - | _ -> raise Stream.Failure - -let accept_before_syms_or_any_id syms strm = - match Util.stream_nth 1 strm with - | Tok.KEYWORD sym when List.mem sym syms -> () - | Tok.IDENT _ -> () - | _ -> raise Stream.Failure - -let accept_before_syms_or_ids syms ids strm = - match Util.stream_nth 1 strm with - | Tok.KEYWORD sym when List.mem sym syms -> () - | Tok.IDENT id when List.mem id ids -> () - | _ -> raise Stream.Failure - open Ssrast let pr_id = Ppconstr.pr_id let pr_name = function Name id -> pr_id id | Anonymous -> str "_" @@ -746,13 +727,11 @@ let pushIPatNoop = function | pats :: orpat -> (IPatNoop :: pats) :: orpat | [] -> [] -let test_ident_no_do _ strm = - match Util.stream_nth 0 strm with - | Tok.IDENT s when s <> "do" -> () - | _ -> raise Stream.Failure - let test_ident_no_do = - Pcoq.Entry.of_parser "test_ident_no_do" test_ident_no_do + let open Pcoq.Lookahead in + to_entry "test_ident_no_do" begin + lk_ident_except ["do"] + end } @@ -1005,12 +984,11 @@ END { -let accept_ssrfwdid _ strm = - match stream_nth 0 strm with - | Tok.IDENT id -> accept_before_syms_or_any_id [":"; ":="; "("] strm - | _ -> raise Stream.Failure - -let test_ssrfwdid = Pcoq.Entry.of_parser "test_ssrfwdid" accept_ssrfwdid +let test_ssrfwdid = + let open Pcoq.Lookahead in + to_entry "test_ssrfwdid" begin + lk_ident >> (lk_ident <+> lk_kws [":"; ":="; "("]) + end } @@ -1589,13 +1567,12 @@ END let sq_brace_tacnames = ["first"; "solve"; "do"; "rewrite"; "have"; "suffices"; "wlog"] (* "by" is a keyword *) -let accept_ssrseqvar _ strm = - match stream_nth 0 strm with - | Tok.IDENT id when not (List.mem id sq_brace_tacnames) -> - accept_before_syms_or_ids ["["] ["first";"last"] strm - | _ -> raise Stream.Failure -let test_ssrseqvar = Pcoq.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar +let test_ssrseqvar = + let open Pcoq.Lookahead in + to_entry "test_ssrseqvar" begin + lk_ident_except sq_brace_tacnames >> (lk_kws ["[";"first";"last"]) + end let swaptacarg (loc, b) = (b, []), Some (TacId []) @@ -1985,15 +1962,11 @@ END { -let accept_ssreqid _ strm = - match Util.stream_nth 0 strm with - | Tok.IDENT _ -> accept_before_syms [":"] strm - | Tok.KEYWORD ":" -> () - | Tok.KEYWORD pat when List.mem pat ["_"; "?"; "->"; "<-"] -> - accept_before_syms [":"] strm - | _ -> raise Stream.Failure - -let test_ssreqid = Pcoq.Entry.of_parser "test_ssreqid" accept_ssreqid +let test_ssreqid = + let open Pcoq.Lookahead in + to_entry "test_ssreqid" begin + ((lk_ident <+> lk_kws ["_"; "?"; "->"; "<-"]) >> lk_kw ":") <+> lk_kw ":" + end } @@ -2614,12 +2587,11 @@ END { -let accept_idcomma _ strm = - match stream_nth 0 strm with - | Tok.IDENT _ | Tok.KEYWORD "_" -> accept_before_syms [","] strm - | _ -> raise Stream.Failure - -let test_idcomma = Pcoq.Entry.of_parser "test_idcomma" accept_idcomma +let test_idcomma = + let open Pcoq.Lookahead in + to_entry "test_idcomma" begin + (lk_ident <+> lk_kw "_") >> lk_kw "," + end } diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 55c1f41c2c..afe776dced 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -73,11 +73,11 @@ let error_wrong_numarg_inductive ?loc env c n = let list_try_compile f l = let rec aux errors = function - | [] -> if errors = [] then anomaly (str "try_find_f.") else iraise (List.last errors) + | [] -> if errors = [] then anomaly (str "try_find_f.") else Exninfo.iraise (List.last errors) | h::t -> try f h with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e -> - let e = CErrors.push e in + let e = Exninfo.capture e in aux (e::errors) t in aux [] l diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ac1a4e88ef..1269488af3 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -87,9 +87,9 @@ let search_guard ?loc env possible_indexes fixdefs = let fix = ((indexes, 0),fixdefs) in (try check_fix env fix with reraise -> - let (e, info) = CErrors.push reraise in + let (e, info) = Exninfo.capture reraise in let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in - iraise (e, info)); + Exninfo.iraise (e, info)); indexes else (* we now search recursively among all combinations *) @@ -266,8 +266,8 @@ let apply_heuristics env sigma fail_evar = let flags = default_flags_of (Typeclasses.classes_transparent_state ()) in try solve_unif_constraints_with_heuristics ~flags env sigma with e when CErrors.noncritical e -> - let e = CErrors.push e in - if fail_evar then iraise e else sigma + let e = Exninfo.capture e in + if fail_evar then Exninfo.iraise e else sigma let check_typeclasses_instances_are_solved ~program_mode env current_sigma frozen = (* Naive way, call resolution again with failure flag *) @@ -753,9 +753,9 @@ struct let cofix = (i, fixdecls) in (try check_cofix !!env (i, nf_fix sigma fixdecls) with reraise -> - let (e, info) = CErrors.push reraise in + let (e, info) = Exninfo.capture reraise in let info = Option.cata (Loc.add_loc info) info loc in - iraise (e, info)); + Exninfo.iraise (e, info)); make_judge (mkCoFix cofix) ftys.(i) in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma fixj tycon @@ -946,9 +946,9 @@ struct try judge_of_product !!env name j j' with TypeError _ as e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in let info = Option.cata (Loc.add_loc info) info loc in - iraise (e, info) in + Exninfo.iraise (e, info) in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon let pretype_letin self (name, c1, t, c2) = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 838bf22c66..b07ae8788a 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1457,12 +1457,15 @@ let pb_equal = function | Reduction.CUMUL -> Reduction.CONV | Reduction.CONV -> Reduction.CONV -let report_anomaly e = - let msg = Pp.(str "Conversion test raised an anomaly:" ++ - spc () ++ CErrors.print e) in - let e = UserError (None,msg) in - let e = CErrors.push e in - iraise e +let report_anomaly (e, info) = + let e = + if is_anomaly e then + let msg = Pp.(str "Conversion test raised an anomaly:" ++ + spc () ++ CErrors.print e) in + UserError (None, msg) + else e + in + Exninfo.iraise (e, info) let f_conv ?l2r ?reds env ?evars x y = let inj = EConstr.Unsafe.to_constr in @@ -1478,7 +1481,9 @@ let test_trans_conversion (f: constr Reduction.extended_conversion_function) red let _ = f ~reds env ~evars:(evars, Evd.universes sigma) x y in true with Reduction.NotConvertible -> false - | e when is_anomaly e -> report_anomaly e + | e -> + let e = Exninfo.capture e in + report_anomaly e let is_conv ?(reds=TransparentState.full) env sigma = test_trans_conversion f_conv reds env sigma let is_conv_leq ?(reds=TransparentState.full) env sigma = test_trans_conversion f_conv_leq reds env sigma @@ -1494,7 +1499,9 @@ let check_conv ?(pb=Reduction.CUMUL) ?(ts=TransparentState.full) env sigma x y = try f ~reds:ts env ~evars:(safe_evar_value sigma, Evd.universes sigma) x y; true with Reduction.NotConvertible -> false | Univ.UniverseInconsistency _ -> false - | e when is_anomaly e -> report_anomaly e + | e -> + let e = Exninfo.capture e in + report_anomaly e let sigma_compare_sorts env pb s0 s1 sigma = match pb with @@ -1547,7 +1554,9 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) with | Reduction.NotConvertible -> None | Univ.UniverseInconsistency _ when catch_incon -> None - | e when is_anomaly e -> report_anomaly e + | e -> + let e = Exninfo.capture e in + report_anomaly e let infer_conv = infer_conv_gen (fun pb ~l2r sigma -> Reduction.generic_conv pb ~l2r (safe_evar_value sigma)) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5b87603d54..1df377b20e 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1149,10 +1149,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e if !debug_unification then Feedback.msg_debug (str "Leaving unification with success"); a with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure"); - iraise e - + Exninfo.iraise e let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 832a749ef2..fd73ab1b5a 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -209,8 +209,8 @@ let catch_failerror (e, info) = | FailError (0,_) -> Control.check_for_interrupt () | FailError (lvl,s) -> - iraise (FailError (lvl - 1, s), info) - | e -> iraise (e, info) + Exninfo.iraise (FailError (lvl - 1, s), info) + | e -> Exninfo.iraise (e, info) (** FIXME: do we need to add a [Errors.push] here? *) (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) @@ -219,7 +219,7 @@ let tclORELSE0 t1 t2 g = t1 g with (* Breakpoint *) | e when CErrors.noncritical e -> - let e = CErrors.push e in catch_failerror e; t2 g + let e = Exninfo.capture e in catch_failerror e; t2 g (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, then applies t2 *) @@ -232,7 +232,7 @@ let tclORELSE_THEN t1 t2then t2else gls = match try Some(tclPROGRESS t1 gls) with e when CErrors.noncritical e -> - let e = CErrors.push e in catch_failerror e; None + let e = Exninfo.capture e in catch_failerror e; None with | None -> t2else gls | Some sgl -> diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index fd689602df..9eb0924bd6 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -372,7 +372,7 @@ module Make(T : Task) () = struct let with_n_workers n priority f = let q = create n priority in try let rc = f q in destroy q; rc - with e -> let e = CErrors.push e in destroy q; iraise e + with e -> let e = Exninfo.capture e in destroy q; Exninfo.iraise e let n_workers { active } = Pool.n_workers active diff --git a/stm/stm.ml b/stm/stm.ml index 95c58b9043..a5b868343d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1014,7 +1014,7 @@ end = struct (* {{{ *) if PG_compat.there_are_pending_proofs () then VCS.goals id (PG_compat.get_open_goals ()) with e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in let good_id = !cur_id in invalidate_cur_state (); VCS.reached id; @@ -1046,7 +1046,7 @@ end = struct (* {{{ *) unfreeze st; res with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in Vernacstate.invalidate_cache (); unfreeze st; Exninfo.iraise e @@ -1540,7 +1540,7 @@ end = struct (* {{{ *) RespBuiltProof(proof,time) with | e when CErrors.noncritical e || e = Stack_overflow -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in (* This can happen if the proof is broken. The error has also been * signalled as a feedback, hence we can silently recover *) let e_error_at, e_safe_id = match Stateid.get info with @@ -1687,7 +1687,7 @@ end = struct (* {{{ *) `OK proof end with e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in (try match Stateid.get info with | None -> msg_warning Pp.( @@ -2092,7 +2092,7 @@ end = struct (* {{{ *) ignore(stm_vernac_interp r_for st { r_what with verbose = true }); feedback ~id:r_for Processed with e when CErrors.noncritical e -> - let e = CErrors.push e in + let e = Exninfo.capture e in let msg = iprint e in feedback ~id:r_for (Message (Error, None, msg)) @@ -2337,7 +2337,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = else try f () with e when CErrors.noncritical e -> - let ie = CErrors.push e in + let ie = Exninfo.capture e in error_absorbing_tactic id blockname ie in (* Absorb errors from f x *) let resilient_command f x = @@ -2435,7 +2435,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x); with e when CErrors.noncritical e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in let info = Stateid.add info ~valid:prev id in Exninfo.iraise (e, info)); wall_clock_last_fork := Unix.gettimeofday () @@ -2569,28 +2569,32 @@ end (* }}} *) (********************************* STM API ************************************) (******************************************************************************) -(* Main initialization routine *) -type stm_init_options = { - (* The STM will set some internal flags differently depending on the - specified [doc_type]. This distinction should disappear at some - some point. *) - doc_type : stm_doc_type; +(** STM initialization options: *) +type stm_init_options = + { doc_type : stm_doc_type + (** The STM does set some internal flags differently depending on + the specified [doc_type]. This distinction should disappear at + some some point. *) - (* Initial load path in scope for the document. Usually extracted - from -R options / _CoqProject *) - iload_path : Loadpath.coq_path list; + ; ml_load_path : CUnix.physical_path list + (** OCaml load paths for the document. *) - (* Require [require_libs] before the initial state is + ; vo_load_path : Loadpath.vo_path list + (** [vo] load paths for the document. Usually extracted from -R + options / _CoqProject *) + + ; require_libs : (string * string option * bool option) list + (** Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, [lib,prefix,import_export] means require library [lib] from optional [prefix] and [import_export] if [Some false/Some true] is used. *) - require_libs : (string * string option * bool option) list; - (* STM options that apply to the current document. *) - stm_options : AsyncOpts.stm_opt; -} -(* fb_handler : Feedback.feedback -> unit; *) + ; stm_options : AsyncOpts.stm_opt + (** Low-level STM options *) + } + + (* fb_handler : Feedback.feedback -> unit; *) (* let doc_type_module_name (std : stm_doc_type) = @@ -2615,7 +2619,7 @@ let dirpath_of_file f = let ldir = Libnames.add_dirpath_suffix ldir0 id in ldir -let new_doc { doc_type ; iload_path; require_libs; stm_options } = +let new_doc { doc_type ; ml_load_path; vo_load_path; require_libs; stm_options } = let require_file (dir, from, exp) = let mp = Libnames.qualid_of_string dir in @@ -2633,7 +2637,8 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = (* Set load path; important, this has to happen before we declare the library below as [Declaremods/Library] will infer the module name by looking at the load path! *) - List.iter Loadpath.add_coq_path iload_path; + List.iter Mltop.add_ml_dir ml_load_path; + List.iter Loadpath.add_vo_path vo_load_path; Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff; @@ -2688,7 +2693,7 @@ let observe ~doc id = VCS.print (); doc with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in VCS.print (); VCS.restore vcs; Exninfo.iraise e @@ -2763,7 +2768,7 @@ let finish_tasks name u p (t,rcbackup as tasks) = let a, _ = List.fold_left finish_task u (info_tasks tasks) in (a,true), p with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in msg_warning (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); exit 1 @@ -2987,7 +2992,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) VCS.print (); rc with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in handle_failure e vcs let get_ast ~doc id = @@ -3197,7 +3202,7 @@ let edit_at ~doc id = VCS.print (); doc, rc with e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in match Stateid.get info with | None -> VCS.print (); diff --git a/stm/stm.mli b/stm/stm.mli index 841adcf05b..e56bac6e0f 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -52,38 +52,30 @@ type stm_doc_type = | VioDoc of string (* file path *) | Interactive of interactive_top (* module path *) -(** Coq initialization options: - - - [doc_type]: Type of document being created. - - - [require_libs]: list of libraries/modules to be pre-loaded at - startup. A tuple [(modname,modfrom,import)] is equivalent to [From - modfrom Require modname]; [import] works similarly to - [Library.require_library_from_dirpath], [Some false] will import - the module, [Some true] will additionally export it. - -*) -type stm_init_options = { - (* The STM will set some internal flags differently depending on the - specified [doc_type]. This distinction should disappear at some - some point. *) - doc_type : stm_doc_type; - - (* Initial load path in scope for the document. Usually extracted - from -R options / _CoqProject *) - iload_path : Loadpath.coq_path list; - - (* Require [require_libs] before the initial state is +(** STM initialization options: *) +type stm_init_options = + { doc_type : stm_doc_type + (** The STM does set some internal flags differently depending on + the specified [doc_type]. This distinction should disappear at + some some point. *) + + ; ml_load_path : CUnix.physical_path list + (** OCaml load paths for the document. *) + + ; vo_load_path : Loadpath.vo_path list + (** [vo] load paths for the document. Usually extracted from -R + options / _CoqProject *) + + ; require_libs : (string * string option * bool option) list + (** Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, [lib,prefix,import_export] means require library [lib] from optional [prefix] and [import_export] if [Some false/Some true] is used. *) - require_libs : (string * string option * bool option) list; - (* STM options that apply to the current document. *) - stm_options : AsyncOpts.stm_opt; -} -(* fb_handler : Feedback.feedback -> unit; *) + ; stm_options : AsyncOpts.stm_opt + (** Low-level STM options *) + } (** The type of a STM document *) type doc diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 1e18028e7b..86e6a92a22 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -97,8 +97,8 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = which is an error irrelevant to the proof system (in fact it means that [e] comes from [tac] failing to yield enough success). Hence it reraises [e]. *) - let (_, info) = CErrors.push src in - iraise (e, info) + let (_, info) = Exninfo.capture src in + Exninfo.iraise (e, info) in let body, effs = Future.force const.Declare.proof_entry_body in (* We drop the side-effects from the entry, they already exist in the ambient environment *) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 28feeecb86..e3f2f18b44 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -236,7 +236,7 @@ let unify_resolve_refine poly flags gl clenv = Tacticals.New.tclZEROMSG (str "Unable to unify") | e when CErrors.noncritical e -> Tacticals.New.tclZEROMSG (str "Unexpected error") - | _ -> iraise ie) + | _ -> Exninfo.iraise ie) (** Dealing with goals of the form A -> B and hints of the form C -> A -> B. @@ -528,9 +528,10 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = let hints = build_subclasses ~check:false env sigma (GlobRef.VarRef id) empty_hint_info in (List.map_append (fun (path,info,c) -> + let h = IsConstr (EConstr.of_constr c,Univ.ContextSet.empty) [@ocaml.warning "-3"] in make_resolves env sigma ~name:(PathHints path) (true,false,not !Flags.quiet) info ~poly:false - (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty))) + h) hints) else [] in @@ -770,7 +771,7 @@ module Search = struct (fun e' -> if CErrors.noncritical (fst e') then (pr_error e'; aux (merge_exceptions e e') tl) - else iraise e') + else Exninfo.iraise e') and aux e = function | x :: xs -> onetac e x xs | [] -> diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 9a1e6a6736..aca6b4734a 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -235,7 +235,7 @@ module SearchProblem = struct (* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *) (lgls, cost, pptac) :: aux tacl with e when CErrors.noncritical e -> - let e = CErrors.push e in + let e = Exninfo.capture e in Refiner.catch_failerror e; aux tacl in aux l diff --git a/tactics/hints.ml b/tactics/hints.ml index 86aa046586..731792e34e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1325,6 +1325,13 @@ let project_hint ~poly pri l2r r = let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in (info,false,true,PathAny, IsGlobRef (GlobRef.ConstRef c)) +let warn_deprecated_hint_constr = + CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated" + (fun () -> + Pp.strbrk + "Declaring arbitrary terms as hints is deprecated; declare a global reference instead" + ) + let interp_hints ~poly = fun h -> let env = Global.env () in @@ -1349,7 +1356,9 @@ let interp_hints ~poly = | HintsReference c -> let gr = global_with_alias c in (PathHints [gr], poly, IsGlobRef gr) - | HintsConstr c -> (PathAny, poly, f poly c) + | HintsConstr c -> + let () = warn_deprecated_hint_constr () in + (PathAny, poly, f poly c) in let fp = Constrintern.intern_constr_pattern env sigma in let fres (info, b, r) = diff --git a/tactics/hints.mli b/tactics/hints.mli index 9c9f0b7708..7bb17489bf 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -181,7 +181,7 @@ type hnf = bool type hint_term = | IsGlobRef of GlobRef.t - | IsConstr of constr * Univ.ContextSet.t + | IsConstr of constr * Univ.ContextSet.t [@ocaml.deprecated "Declare a hint constant instead"] type hints_entry = | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index dbabc4e4e0..7cdfd0637a 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -130,8 +130,8 @@ let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ctx sign ~ | _ -> CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") with reraise -> - let reraise = CErrors.push reraise in - iraise reraise + let reraise = Exninfo.capture reraise in + Exninfo.iraise reraise let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = let name = Id.of_string ("temporary_proof"^string_of_int (next())) in @@ -160,8 +160,8 @@ let refine_by_tactic ~name ~poly env sigma ty tac = try Proof.run_tactic env tac prf with Logic_monad.TacticFailure e as src -> (* Catch the inner error of the monad tactic *) - let (_, info) = CErrors.push src in - iraise (e, info) + let (_, info) = Exninfo.capture src in + Exninfo.iraise (e, info) in (* Plug back the retrieved sigma *) let Proof.{ goals; stack; shelf; given_up; sigma; entry } = Proof.data prf in diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 4b93b81d1c..5fde6d2178 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -144,7 +144,7 @@ module New : sig (** [catch_failerror e] fails and decreases the level if [e] is an Ltac error with level more than 0. Otherwise succeeds. *) - val catch_failerror : Util.iexn -> unit tactic + val catch_failerror : Exninfo.iexn -> unit tactic val tclIDTAC : unit tactic val tclTHEN : unit tactic -> unit tactic -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 8371da76b2..83423b7556 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1848,12 +1848,12 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) = let rec aux clause = try progress_with_clause flags innerclause clause with e when CErrors.noncritical e -> - let e' = CErrors.push e in + let e' = Exninfo.capture e in try aux (clenv_push_prod clause) with NotExtensibleClause -> match e with | UnableToApply -> explain_unable_to_apply_lemma ?loc env sigma thm innerclause - | _ -> iraise e' + | _ -> Exninfo.iraise e' in aux (make_clenv_binding env sigma (d,thm) lbind) @@ -1886,7 +1886,7 @@ let apply_in_once ?(respect_opaque = false) with_delta tac id ]) with e when with_destruct && CErrors.noncritical e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in (descend_in_conjunctions (Id.Set.singleton targetid) (fun b id -> aux (id::idstoclear) b (mkVar id)) (e, info) c) @@ -3155,7 +3155,7 @@ let clear_for_destruct ids = (clear_gen (fun env sigma id err inglobal -> raise (ClearDependencyError (id,err,inglobal))) ids) (function | ClearDependencyError (id,err,inglobal),_ -> warn_cannot_remove_as_expected (id,inglobal); Proofview.tclUNIT () - | e -> iraise e) + | e -> Exninfo.iraise e) (* Either unfold and clear if defined or simply clear if not a definition *) let expand_hyp id = diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differindex b3bcb5b056..046cb067c5 100644 --- a/test-suite/.csdp.cache +++ b/test-suite/.csdp.cache diff --git a/test-suite/ide/debug_ltac.fake b/test-suite/ide/debug_ltac.fake index aa68fad39e..38c610a5a6 100644 --- a/test-suite/ide/debug_ltac.fake +++ b/test-suite/ide/debug_ltac.fake @@ -1,2 +1,3 @@ +ADD { Comments "fakeide doesn't support fail as the first sentence". } FAILADD { Debug On. } ADD { Set Debug On. } diff --git a/test-suite/ide/undo002.fake b/test-suite/ide/undo002.fake index 5284c5d3a5..eb553f9dfa 100644 --- a/test-suite/ide/undo002.fake +++ b/test-suite/ide/undo002.fake @@ -3,6 +3,7 @@ # # Simple backtrack by 2 before two global definitions # +ADD initial { Comments "initial sentence". } ADD { Definition foo := 0. } ADD { Definition bar := 1. } EDIT_AT initial diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 8ff571ae55..ff2556c5dc 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -5,3 +5,5 @@ Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x Arguments foo _%type_scope Arguments Foo _%type_scope +myprod unit bool + : Set diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v index 9eec9a7dad..db1276cb6c 100644 --- a/test-suite/output/Inductive.v +++ b/test-suite/output/Inductive.v @@ -5,3 +5,11 @@ Fail Inductive list' (A:Set) : Set := (* Check printing of let-ins *) #[universes(template)] Inductive foo (A : Type) (x : A) (y := x) := Foo. Print foo. + +(* Check where clause *) +Reserved Notation "x ** y" (at level 40, left associativity). +Inductive myprod A B := + mypair : A -> B -> A ** B + where "A ** B" := (myprod A B) (only parsing). + +Check unit ** bool. diff --git a/test-suite/output/bug_8206.out b/test-suite/output/bug_8206.out new file mode 100644 index 0000000000..6015fe32f9 --- /dev/null +++ b/test-suite/output/bug_8206.out @@ -0,0 +1,5 @@ +File "stdin", line 11, characters 0-23: +Error: Signature components for label homework do not match: expected type +"forall a b : nat, bug_8206.M.add a b = bug_8206.M.add b a" but found type +"nat -> forall b : nat, bug_8206.M.add 0 b = bug_8206.M.add b 0". + diff --git a/test-suite/output/bug_8206.v b/test-suite/output/bug_8206.v new file mode 100644 index 0000000000..8d4e73dfac --- /dev/null +++ b/test-suite/output/bug_8206.v @@ -0,0 +1,11 @@ +Module Type Sig. + Parameter add: nat -> nat -> nat. + Axiom homework: forall (a b: nat), add a b = add b a. +End Sig. + +Module Impl. + Definition add(a b: nat) := plus a b. + Axiom homework: forall (a b: nat), add 0 b = add b 0. +End Impl. + +Module M : Sig := Impl. diff --git a/test-suite/success/pose.v b/test-suite/success/pose.v new file mode 100644 index 0000000000..17007915fe --- /dev/null +++ b/test-suite/success/pose.v @@ -0,0 +1,9 @@ +(* Test syntax *) + +Goal 0=0. +pose proof (a := I). +Fail clearbody a. +epose proof (b := fun _ => eq_refl). +Fail clearbody b. +exact (b a). +Qed. diff --git a/theories/micromega/Lia.v b/theories/micromega/Lia.v index e53800d07d..5d97fc46ef 100644 --- a/theories/micromega/Lia.v +++ b/theories/micromega/Lia.v @@ -14,11 +14,8 @@ (* *) (************************************************************************) -Require Import ZMicromega. -Require Import ZArith_base. -Require Import RingMicromega. -Require Import VarMap. -Require Import DeclConstant. +Require Import ZMicromega RingMicromega VarMap DeclConstant. +Require Import BinNums. Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". @@ -29,9 +26,9 @@ Ltac zchecker := (@eq_refl bool true <: @eq bool (ZTautoChecker __ff __wit) true) (@find Z Z0 __varmap)). -Ltac lia := PreOmega.zify; xlia zchecker. +Ltac lia := Zify.zify; xlia zchecker. -Ltac nia := PreOmega.zify; xnlia zchecker. +Ltac nia := Zify.zify; xnlia zchecker. (* Local Variables: *) diff --git a/theories/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v index 9bedb47371..38f3d3e0c0 100644 --- a/theories/micromega/ZMicromega.v +++ b/theories/micromega/ZMicromega.v @@ -1549,7 +1549,7 @@ Proof. apply H ; auto. unfold ltof in *. simpl in *. - PreOmega.zify. + Zify.zify. intuition subst. assumption. eapply Z.lt_le_trans. eassumption. apply Z.add_le_mono_r. assumption. diff --git a/theories/micromega/Zify.v b/theories/micromega/Zify.v index 18cd196148..494d5e5623 100644 --- a/theories/micromega/Zify.v +++ b/theories/micromega/Zify.v @@ -8,83 +8,16 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import ZifyClasses. -Require Export ZifyInst. -Require Import InitialRing. - -(** From PreOmega *) - -(** I) translation of Z.max, Z.min, Z.abs, Z.sgn into recognized equations *) - -Ltac zify_unop_core t thm a := - (* Let's introduce the specification theorem for t *) - pose proof (thm a); - (* Then we replace (t a) everywhere with a fresh variable *) - let z := fresh "z" in set (z:=t a) in *; clearbody z. - -Ltac zify_unop_var_or_term t thm a := - (* If a is a variable, no need for aliasing *) - let za := fresh "z" in - (rename a into za; rename za into a; zify_unop_core t thm a) || - (* Otherwise, a is a complex term: we alias it. *) - (remember a as za; zify_unop_core t thm za). - -Ltac zify_unop t thm a := - (* If a is a scalar, we can simply reduce the unop. *) - (* Note that simpl wasn't enough to reduce [Z.max 0 0] (#5439) *) - let isz := isZcst a in - match isz with - | true => - let u := eval compute in (t a) in - change (t a) with u in * - | _ => zify_unop_var_or_term t thm a - end. - -Ltac zify_unop_nored t thm a := - (* in this version, we don't try to reduce the unop (that can be (Z.add x)) *) - let isz := isZcst a in - match isz with - | true => zify_unop_core t thm a - | _ => zify_unop_var_or_term t thm a - end. - -Ltac zify_binop t thm a b:= - (* works as zify_unop, except that we should be careful when - dealing with b, since it can be equal to a *) - let isza := isZcst a in - match isza with - | true => zify_unop (t a) (thm a) b - | _ => - let za := fresh "z" in - (rename a into za; rename za into a; zify_unop_nored (t a) (thm a) b) || - (remember a as za; match goal with - | H : za = b |- _ => zify_unop_nored (t za) (thm za) za - | _ => zify_unop_nored (t za) (thm za) b - end) - end. - -(* end from PreOmega *) - -Ltac applySpec S := - let t := type of S in - match t with - | @BinOpSpec _ _ ?Op _ => - let Spec := (eval unfold S, BSpec in (@BSpec _ _ Op _ S)) in - repeat - match goal with - | H : context[Op ?X ?Y] |- _ => zify_binop Op Spec X Y - | |- context[Op ?X ?Y] => zify_binop Op Spec X Y - end - | @UnOpSpec _ _ ?Op _ => - let Spec := (eval unfold S, USpec in (@USpec _ _ Op _ S)) in - repeat - match goal with - | H : context[Op ?X] |- _ => zify_unop Op Spec X - | |- context[Op ?X ] => zify_unop Op Spec X - end - end. +Require Import ZifyClasses ZifyInst. +Declare ML Module "zify_plugin". (** [zify_post_hook] is there to be redefined. *) Ltac zify_post_hook := idtac. -Ltac zify := zify_op ; (zify_iter_specs applySpec) ; zify_post_hook. +Ltac iter_specs := zify_iter_specs. + +Ltac zify := intros; + zify_elim_let ; + zify_op ; + (zify_iter_specs) ; + zify_saturate ; zify_post_hook. diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v index d3f7f91074..988205a891 100644 --- a/theories/micromega/ZifyClasses.v +++ b/theories/micromega/ZifyClasses.v @@ -73,6 +73,7 @@ Class BinRel {S:Type} {T:Type} (R : S -> S -> Prop) {I : InjTyp S T} := (** [PropOp Op] declares morphisms for [<->]. This will be used to deal with e.g. [and], [or],... *) + Class PropOp (Op : Prop -> Prop -> Prop) := mkprop { op_iff : forall (p1 p2 q1 q2:Prop), (p1 <-> q1) -> (p2 <-> q2) -> (Op p1 p2 <-> Op q1 q2) @@ -80,7 +81,7 @@ Class PropOp (Op : Prop -> Prop -> Prop) := Class PropUOp (Op : Prop -> Prop) := mkuprop { - uop_iff : forall (p1 q1 :Prop), (p1 <-> q1) -> (Op p1 <-> Op q1) + uop_iff : forall (p1 q1 :Prop), (p1 <-> q1) -> (Op p1 <-> Op q1) }. @@ -131,7 +132,7 @@ Class Saturate {T: Type} (Op : T -> T -> T) := are used to store source and target expressions together with a correctness proof. *) -Record injterm {S T: Type} {I : S -> T} := +Record injterm {S T: Type} (I : S -> T) := mkinjterm { source : S ; target : T ; inj_ok : I source = target}. Record injprop := @@ -139,82 +140,104 @@ Record injprop := source_prop : Prop ; target_prop : Prop ; injprop_ok : source_prop <-> target_prop}. -(** Lemmas for building [injterm] and [injprop]. *) -Definition mkprop_op (Op : Prop -> Prop -> Prop) (POp : PropOp Op) - (p1 :injprop) (p2: injprop) : injprop := - {| source_prop := (Op (source_prop p1) (source_prop p2)) ; - target_prop := (Op (target_prop p1) (target_prop p2)) ; - injprop_ok := (op_iff (source_prop p1) (source_prop p2) (target_prop p1) (target_prop p2) - (injprop_ok p1) (injprop_ok p2)) - |}. -Definition mkuprop_op (Op : Prop -> Prop) (POp : PropUOp Op) - (p1 :injprop) : injprop := - {| source_prop := (Op (source_prop p1)) ; - target_prop := (Op (target_prop p1)) ; - injprop_ok := (uop_iff (source_prop p1) (target_prop p1) (injprop_ok p1)) - |}. +(** Lemmas for building rewrite rules. *) + +Definition PropOp_iff (Op : Prop -> Prop -> Prop) := + forall (p1 p2 q1 q2:Prop), (p1 <-> q1) -> (p2 <-> q2) -> (Op p1 p2 <-> Op q1 q2). + +Definition PropUOp_iff (Op : Prop -> Prop) := + forall (p1 q1 :Prop), (p1 <-> q1) -> (Op p1 <-> Op q1). Lemma mkapp2 (S1 S2 S3 T : Type) (Op : S1 -> S2 -> S3) - {I1 : InjTyp S1 T} {I2 : InjTyp S2 T} {I3 : InjTyp S3 T} - (B : @BinOp S1 S2 S3 T Op I1 I2 I3) - (t1 : @injterm S1 T inj) (t2 : @injterm S2 T inj) - : @injterm S3 T inj. + (I1 : S1 -> T) (I2 : S2 -> T) (I3 : S3 -> T) + (TBOP : T -> T -> T) + (TBOPINJ : forall n m, I3 (Op n m) = TBOP (I1 n) (I2 m)) + (s1 : S1) (t1 : T) (P1: I1 s1 = t1) + (s2 : S2) (t2 : T) (P2: I2 s2 = t2): I3 (Op s1 s2) = TBOP t1 t2. Proof. - apply (mkinjterm _ _ inj (Op (source t1) (source t2)) (TBOp (target t1) (target t2))). - (rewrite <- inj_ok; - rewrite <- inj_ok; - apply TBOpInj). -Defined. + subst. apply TBOPINJ. +Qed. -Lemma mkapp (S1 S2 T : Type) (Op : S1 -> S2) - {I1 : InjTyp S1 T} - {I2 : InjTyp S2 T} - (B : @UnOp S1 S2 T Op I1 I2 ) - (t1 : @injterm S1 T inj) - : @injterm S2 T inj. +Lemma mkapp (S1 S2 T : Type) (OP : S1 -> S2) + (I1 : S1 -> T) + (I2 : S2 -> T) + (TUOP : T -> T) + (TUOPINJ : forall n, I2 (OP n) = TUOP (I1 n)) + (s1: S1) (t1: T) (P1: I1 s1 = t1): I2 (OP s1) = TUOP t1. Proof. - apply (mkinjterm _ _ inj (Op (source t1)) (TUOp (target t1))). - (rewrite <- inj_ok; apply TUOpInj). -Defined. + subst. apply TUOPINJ. +Qed. + +Lemma mkrel (S T : Type) (R : S -> S -> Prop) + (I : S -> T) + (TR : T -> T -> Prop) + (TRINJ : forall n m : S, R n m <-> TR (I n) (I m)) + (s1 : S) (t1 : T) (P1 : I s1 = t1) + (s2 : S) (t2 : T) (P2 : I s2 = t2): + R s1 s2 <-> TR t1 t2. +Proof. + subst. + apply TRINJ. +Qed. + +(** Hardcoded support and lemma for propositional logic *) -Lemma mkapp0 (S T : Type) (Op : S) - {I : InjTyp S T} - (B : @CstOp S T Op I) - : @injterm S T inj. +Lemma and_morph : forall (s1 s2 t1 t2:Prop), s1 <-> t1 -> s2 <-> t2 -> ((s1 /\ s2) <-> (t1 /\ t2)). Proof. - apply (mkinjterm _ _ inj Op TCst). - (apply TCstInj). -Defined. + intros. tauto. +Qed. -Lemma mkrel (S T : Type) (R : S -> S -> Prop) - {Inj : InjTyp S T} - (B : @BinRel S T R Inj) - (t1 : @injterm S T inj) (t2 : @injterm S T inj) - : @injprop. +Lemma or_morph : forall (s1 s2 t1 t2:Prop), s1 <-> t1 -> s2 <-> t2 -> ((s1 \/ s2) <-> (t1 \/ t2)). +Proof. + intros. tauto. +Qed. + +Lemma impl_morph : forall (s1 s2 t1 t2:Prop), s1 <-> t1 -> s2 <-> t2 -> ((s1 -> s2) <-> (t1 -> t2)). +Proof. + intros. tauto. +Qed. + +Lemma iff_morph : forall (s1 s2 t1 t2:Prop), s1 <-> t1 -> s2 <-> t2 -> ((s1 <-> s2) <-> (t1 <-> t2)). +Proof. + intros. tauto. +Qed. + +Lemma not_morph : forall (s1 t1:Prop), s1 <-> t1 -> (not s1) <-> (not t1). +Proof. + intros. tauto. +Qed. + +Lemma eq_iff : forall (P Q : Prop), P = Q -> (P <-> Q). Proof. - apply (mkinjprop (R (source t1) (source t2)) (TR (target t1) (target t2))). - (rewrite <- inj_ok; rewrite <- inj_ok;apply TRInj). + intros. + rewrite H. + apply iff_refl. Defined. +Lemma rew_iff (P Q : Prop) (IFF : P <-> Q) : P -> Q. +Proof. + exact (fun H => proj1 IFF H). +Qed. + +Definition identity (A : Type) : A -> A := fun x => x. + (** Registering constants for use by the plugin *) +Register eq_iff as ZifyClasses.eq_iff. Register target_prop as ZifyClasses.target_prop. Register mkrel as ZifyClasses.mkrel. Register target as ZifyClasses.target. Register mkapp2 as ZifyClasses.mkapp2. Register mkapp as ZifyClasses.mkapp. -Register mkapp0 as ZifyClasses.mkapp0. Register op_iff as ZifyClasses.op_iff. Register uop_iff as ZifyClasses.uop_iff. Register TR as ZifyClasses.TR. Register TBOp as ZifyClasses.TBOp. Register TUOp as ZifyClasses.TUOp. Register TCst as ZifyClasses.TCst. -Register mkprop_op as ZifyClasses.mkprop_op. -Register mkuprop_op as ZifyClasses.mkuprop_op. Register injprop_ok as ZifyClasses.injprop_ok. Register inj_ok as ZifyClasses.inj_ok. Register source as ZifyClasses.source. @@ -225,8 +248,26 @@ Register TUOpInj as ZifyClasses.TUOpInj. Register not as ZifyClasses.not. Register mkinjterm as ZifyClasses.mkinjterm. Register eq_refl as ZifyClasses.eq_refl. +Register eq as ZifyClasses.eq. Register mkinjprop as ZifyClasses.mkinjprop. Register iff_refl as ZifyClasses.iff_refl. +Register rew_iff as ZifyClasses.rew_iff. Register source_prop as ZifyClasses.source_prop. Register injprop_ok as ZifyClasses.injprop_ok. Register iff as ZifyClasses.iff. +Register BinOpSpec as ZifyClasses.BinOpSpec. +Register UnOpSpec as ZifyClasses.UnOpSpec. + +(** Propositional logic *) +Register and as ZifyClasses.and. +Register and_morph as ZifyClasses.and_morph. +Register or as ZifyClasses.or. +Register or_morph as ZifyClasses.or_morph. +Register iff as ZifyClasses.iff. +Register iff_morph as ZifyClasses.iff_morph. +Register impl_morph as ZifyClasses.impl_morph. +Register not as ZifyClasses.not. +Register not_morph as ZifyClasses.not_morph. + +(** Identify function *) +Register identity as ZifyClasses.identity. diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v index edfb5a2a94..fa486f3abc 100644 --- a/theories/micromega/ZifyInst.v +++ b/theories/micromega/ZifyInst.v @@ -17,44 +17,10 @@ Require Import ZifyClasses. Declare ML Module "zify_plugin". Local Open Scope Z_scope. -(** Propositional logic *) -Instance PropAnd : PropOp and. -Proof. - constructor. - tauto. -Defined. -Add PropOp PropAnd. - -Instance PropOr : PropOp or. -Proof. - constructor. - tauto. -Defined. -Add PropOp PropOr. - -Instance PropArrow : PropOp (fun x y => x -> y). -Proof. - constructor. - intros. - tauto. -Defined. -Add PropOp PropArrow. - -Instance PropIff : PropOp iff. -Proof. - constructor. - intros. - tauto. -Defined. -Add PropOp PropIff. - -Instance PropNot : PropUOp not. -Proof. - constructor. - intros. - tauto. -Defined. -Add PropUOp PropNot. +Ltac refl := + abstract (intros ; match goal with + | |- context[@inj _ _ ?X] => unfold X, inj + end ; reflexivity). Instance Inj_Z_Z : InjTyp Z Z := @@ -162,13 +128,18 @@ Instance Op_pos_le : BinRel Pos.le := {| TR := Z.le; TRInj := fun x y => iff_refl (Z.pos x <= Z.pos y) |}. Add BinRel Op_pos_le. +Lemma eq_pos_inj : forall (x y:positive), x = y <-> Z.pos x = Z.pos y. +Proof. + intros. + apply (iff_sym (Pos2Z.inj_iff x y)). +Qed. + Instance Op_eq_pos : BinRel (@eq positive) := - {| TR := @eq Z ; TRInj := fun x y => iff_sym (Pos2Z.inj_iff x y) |}. + { TR := @eq Z ; TRInj := eq_pos_inj }. Add BinRel Op_eq_pos. (* zify_positive_op *) - Instance Op_Z_of_N : UnOp Z.of_N := { TUOp := (fun x => x) ; TUOpInj := fun x => eq_refl (Z.of_N x) }. Add UnOp Op_Z_of_N. @@ -189,8 +160,11 @@ Instance Op_pos_succ : UnOp Pos.succ := { TUOp := fun x => x + 1; TUOpInj := Pos2Z.inj_succ }. Add UnOp Op_pos_succ. + + + Instance Op_pos_pred_double : UnOp Pos.pred_double := - { TUOp := fun x => 2 * x - 1; TUOpInj := ltac:(reflexivity) }. +{ TUOp := fun x => 2 * x - 1; TUOpInj := ltac:(refl) }. Add UnOp Op_pos_pred_double. Instance Op_pos_pred : UnOp Pos.pred := @@ -217,7 +191,7 @@ Instance Op_pos_of_nat : UnOp Pos.of_nat := Add UnOp Op_pos_of_nat. Instance Op_pos_add : BinOp Pos.add := - { TBOp := Z.add ; TBOpInj := ltac: (reflexivity) }. + { TBOp := Z.add ; TBOpInj := ltac: (refl) }. Add BinOp Op_pos_add. Instance Op_pos_add_carry : BinOp Pos.add_carry := @@ -230,7 +204,7 @@ Instance Op_pos_sub : BinOp Pos.sub := Add BinOp Op_pos_sub. Instance Op_pos_mul : BinOp Pos.mul := - { TBOp := Z.mul ; TBOpInj := ltac: (reflexivity) }. + { TBOp := Z.mul ; TBOpInj := ltac: (refl) }. Add BinOp Op_pos_mul. Instance Op_pos_min : BinOp Pos.min := @@ -250,19 +224,19 @@ Instance Op_pos_square : UnOp Pos.square := Add UnOp Op_pos_square. Instance Op_xO : UnOp xO := - { TUOp := fun x => 2 * x ; TUOpInj := ltac: (reflexivity) }. + { TUOp := fun x => 2 * x ; TUOpInj := ltac: (refl) }. Add UnOp Op_xO. Instance Op_xI : UnOp xI := - { TUOp := fun x => 2 * x + 1 ; TUOpInj := ltac: (reflexivity) }. + { TUOp := fun x => 2 * x + 1 ; TUOpInj := ltac: (refl) }. Add UnOp Op_xI. Instance Op_xH : CstOp xH := - { TCst := 1%Z ; TCstInj := ltac:(reflexivity)}. + { TCst := 1%Z ; TCstInj := ltac:(refl)}. Add CstOp Op_xH. Instance Op_Z_of_nat : UnOp Z.of_nat:= - { TUOp := fun x => x ; TUOpInj := ltac:(reflexivity) }. + { TUOp := fun x => x ; TUOpInj := (fun x : nat => @eq_refl Z (Z.of_nat x)) }. Add UnOp Op_Z_of_nat. (* zify_N_rel *) @@ -287,6 +261,14 @@ Instance Op_eq_N : BinRel (@eq N) := Add BinRel Op_eq_N. (* zify_N_op *) +Instance Op_N_N0 : CstOp N0 := + { TCst := Z0 ; TCstInj := eq_refl }. +Add CstOp Op_N_N0. + +Instance Op_N_Npos : UnOp Npos := + { TUOp := (fun x => x) ; TUOpInj := ltac:(refl) }. +Add UnOp Op_N_Npos. + Instance Op_N_of_nat : UnOp N.of_nat := { TUOp := fun x => x ; TUOpInj := nat_N_Z }. Add UnOp Op_N_of_nat. @@ -296,7 +278,7 @@ Instance Op_Z_abs_N : UnOp Z.abs_N := Add UnOp Op_Z_abs_N. Instance Op_N_pos : UnOp N.pos := - { TUOp := fun x => x ; TUOpInj := ltac:(reflexivity)}. + { TUOp := fun x => x ; TUOpInj := ltac:(refl)}. Add UnOp Op_N_pos. Instance Op_N_add : BinOp N.add := @@ -360,68 +342,72 @@ Instance Op_eqZ : BinRel (@eq Z) := { TR := @eq Z ; TRInj := fun x y => iff_refl (x = y) }. Add BinRel Op_eqZ. +Instance Op_Z_Z0 : CstOp Z0 := + { TCst := Z0 ; TCstInj := eq_refl }. +Add CstOp Op_Z_Z0. + Instance Op_Z_add : BinOp Z.add := - { TBOp := Z.add ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.add ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_add. Instance Op_Z_min : BinOp Z.min := - { TBOp := Z.min ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.min ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_min. Instance Op_Z_max : BinOp Z.max := - { TBOp := Z.max ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.max ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_max. Instance Op_Z_mul : BinOp Z.mul := - { TBOp := Z.mul ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.mul ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_mul. Instance Op_Z_sub : BinOp Z.sub := - { TBOp := Z.sub ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.sub ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_sub. Instance Op_Z_div : BinOp Z.div := - { TBOp := Z.div ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.div ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_div. Instance Op_Z_mod : BinOp Z.modulo := - { TBOp := Z.modulo ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.modulo ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_mod. Instance Op_Z_rem : BinOp Z.rem := - { TBOp := Z.rem ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.rem ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_rem. Instance Op_Z_quot : BinOp Z.quot := - { TBOp := Z.quot ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.quot ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_quot. Instance Op_Z_succ : UnOp Z.succ := - { TUOp := fun x => x + 1 ; TUOpInj := ltac:(reflexivity) }. + { TUOp := fun x => x + 1 ; TUOpInj := ltac:(refl) }. Add UnOp Op_Z_succ. Instance Op_Z_pred : UnOp Z.pred := - { TUOp := fun x => x - 1 ; TUOpInj := ltac:(reflexivity) }. + { TUOp := fun x => x - 1 ; TUOpInj := ltac:(refl) }. Add UnOp Op_Z_pred. Instance Op_Z_opp : UnOp Z.opp := - { TUOp := Z.opp ; TUOpInj := ltac:(reflexivity) }. + { TUOp := Z.opp ; TUOpInj := ltac:(refl) }. Add UnOp Op_Z_opp. Instance Op_Z_abs : UnOp Z.abs := - { TUOp := Z.abs ; TUOpInj := ltac:(reflexivity) }. + { TUOp := Z.abs ; TUOpInj := ltac:(refl) }. Add UnOp Op_Z_abs. Instance Op_Z_sgn : UnOp Z.sgn := - { TUOp := Z.sgn ; TUOpInj := ltac:(reflexivity) }. + { TUOp := Z.sgn ; TUOpInj := ltac:(refl) }. Add UnOp Op_Z_sgn. Instance Op_Z_pow : BinOp Z.pow := - { TBOp := Z.pow ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.pow ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_pow. Instance Op_Z_pow_pos : BinOp Z.pow_pos := - { TBOp := Z.pow ; TBOpInj := ltac:(reflexivity) }. + { TBOp := Z.pow ; TBOpInj := ltac:(refl) }. Add BinOp Op_Z_pow_pos. Instance Op_Z_double : UnOp Z.double := diff --git a/theories/omega/PreOmega.v b/theories/omega/PreOmega.v index 34533670f8..bd9caa801c 100644 --- a/theories/omega/PreOmega.v +++ b/theories/omega/PreOmega.v @@ -573,16 +573,4 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. Require Import ZifyClasses ZifyInst. Require Zify. -(* [elim_let] replaces a let binding (x := e : t) - by an equation (x = e) if t is an injected type *) - -Ltac elim_binding x t ty := - let h := fresh "heq_" x in - pose proof (@eq_refl ty x : @eq ty x t) as h; - try clearbody x. - -Ltac elim_let := zify_iter_let elim_binding. - -Ltac zify := - intros ; elim_let ; - Zify.zify ; ZifyInst.zify_saturate. +Ltac zify := Zify.zify. diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index dceb811d66..f75a706041 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -104,7 +104,7 @@ let compile opts copts ~echo ~f_in ~f_out = |> prlist_with_sep pr_comma Names.Id.print) ++ str ".") in - let iload_path = build_load_path opts in + let ml_load_path, vo_load_path = build_load_path opts in let require_libs = require_libs opts in let stm_options = opts.config.stm_flags in let output_native_objects = match opts.config.native_compiler with @@ -129,8 +129,8 @@ let compile opts copts ~echo ~f_in ~f_out = | BuildVo | BuildVok -> let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) Stm.new_doc - Stm.{ doc_type = VoDoc long_f_dot_out; - iload_path; require_libs; stm_options; + Stm.{ doc_type = VoDoc long_f_dot_out; ml_load_path; + vo_load_path; require_libs; stm_options; } in let state = { doc; sid; proof = None; time = opts.config.time } in let state = load_init_vernaculars opts ~state in @@ -181,8 +181,8 @@ let compile opts copts ~echo ~f_in ~f_out = let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude) Stm.new_doc - Stm.{ doc_type = VioDoc long_f_dot_out; - iload_path; require_libs; stm_options; + Stm.{ doc_type = VioDoc long_f_dot_out; ml_load_path; + vo_load_path; require_libs; stm_options; } in let state = { doc; sid; proof = None; time = opts.config.time } in @@ -252,8 +252,9 @@ let do_vio opts copts = (* We must initialize the loadpath here as the vio scheduling process happens outside of the STM *) if copts.vio_files <> [] || copts.vio_tasks <> [] then - let iload_path = build_load_path opts in - List.iter Loadpath.add_coq_path iload_path; + let ml_lp, vo_lp = build_load_path opts in + List.iter Mltop.add_ml_dir ml_lp; + List.iter Loadpath.add_vo_path vo_lp; (* Vio compile pass *) if copts.vio_files <> [] then schedule_vio copts; diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 949a13974c..ef97e57a5c 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -70,8 +70,8 @@ type coqargs_pre = { load_init : bool; load_rcfile : bool; - ml_includes : Loadpath.coq_path list; - vo_includes : Loadpath.coq_path list; + ml_includes : string list; + vo_includes : Loadpath.vo_path list; vo_requires : (string * string option * bool option) list; (* None = No Import; Some false = Import; Some true = Export *) @@ -164,14 +164,13 @@ let default = { (* Functional arguments *) (******************************************************************************) let add_ml_include opts s = - Loadpath.{ opts with pre = { opts.pre with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.pre.ml_includes }} + { opts with pre = { opts.pre with ml_includes = s :: opts.pre.ml_includes }} let add_vo_include opts unix_path coq_path implicit = let open Loadpath in let coq_path = Libnames.dirpath_of_string coq_path in { opts with pre = { opts.pre with vo_includes = { - recursive = true; - path_spec = VoPath { unix_path; coq_path; has_ml = AddNoML; implicit } } :: opts.pre.vo_includes }} + unix_path; coq_path; has_ml = false; implicit; recursive = true } :: opts.pre.vo_includes }} let add_vo_require opts d p export = { opts with pre = { opts.pre with vo_requires = (d, p, export) :: opts.pre.vo_requires }} @@ -582,9 +581,11 @@ let prelude_data = "Prelude", Some "Coq", Some false let require_libs opts = if opts.pre.load_init then prelude_data :: opts.pre.vo_requires else opts.pre.vo_requires -let cmdline_load_path opts = - opts.pre.ml_includes @ opts.pre.vo_includes - let build_load_path opts = - (if opts.pre.boot then [] else Coqinit.libs_init_load_path ()) @ - cmdline_load_path opts + let ml_path, vo_path = + if opts.pre.boot then [],[] + else + let coqlib = Envars.coqlib () in + Coqinit.libs_init_load_path ~coqlib in + ml_path @ opts.pre.ml_includes , + vo_path @ opts.pre.vo_includes diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index aba6811f43..88de48967a 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -46,8 +46,8 @@ type coqargs_pre = { load_init : bool; load_rcfile : bool; - ml_includes : Loadpath.coq_path list; - vo_includes : Loadpath.coq_path list; + ml_includes : CUnix.physical_path list; + vo_includes : Loadpath.vo_path list; vo_requires : (string * string option * bool option) list; (* None = No Import; Some false = Import; Some true = Export *) @@ -83,4 +83,4 @@ val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * strin val error_wrong_arg : string -> unit val require_libs : t -> (string * string option * bool option) list -val build_load_path : t -> Loadpath.coq_path list +val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 7f3d4b570f..4041d02953 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -47,66 +47,46 @@ let load_rcfile ~rcfile ~state = " found. Skipping rcfile loading.")) *) with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in let () = Feedback.msg_info (str"Load of rcfile failed.") in - iraise reraise + Exninfo.iraise reraise -(* Recursively puts `.v` files in the LoadPath if -nois was not passed *) +(* Recursively puts `.v` files in the LoadPath *) let build_stdlib_vo_path ~unix_path ~coq_path = let open Loadpath in - { recursive = true; - path_spec = VoPath { unix_path; coq_path ; has_ml = AddNoML; implicit = true } - } - -let build_stdlib_ml_path ~dir = - let open Loadpath in - { recursive = true - ; path_spec = MlPath dir - } + { unix_path; coq_path ; has_ml = false; implicit = true; recursive = true } let build_userlib_path ~unix_path = let open Loadpath in - { recursive = true; - path_spec = VoPath { - unix_path; - coq_path = Libnames.default_root_prefix; - has_ml = AddRecML; - implicit = false; - } + { unix_path + ; coq_path = Libnames.default_root_prefix + ; has_ml = true + ; implicit = false + ; recursive = true } -let ml_path_if c p = - let open Loadpath in - let f x = { recursive = false; path_spec = MlPath x } in - if c then List.map f p else [] - -(* LoadPath for developers *) -let toplevel_init_load_path () = - let coqlib = Envars.coqlib () in - (* NOTE: These directories are searched from last to first *) - (* first, developer specific directory to open *) - ml_path_if Coq_config.local [coqlib/"dev"] - (* LoadPath for Coq user libraries *) -let libs_init_load_path () = +let libs_init_load_path ~coqlib = let open Loadpath in - let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in let coqpath = Envars.coqpath in let coq_path = Names.DirPath.make [Libnames.coq_root] in + (* ML includes *) + let plugins_dirs = System.all_subdirs ~unix_path:(coqlib/"plugins") in + List.map fst plugins_dirs, + (* current directory (not recursively!) *) - [ { recursive = false; - path_spec = VoPath { unix_path = "."; - coq_path = Libnames.default_root_prefix; - implicit = false; - has_ml = AddTopML } + [ { unix_path = "." + ; coq_path = Libnames.default_root_prefix + ; implicit = false + ; has_ml = true + ; recursive = false } ] @ (* then standard library *) - [build_stdlib_ml_path ~dir:(coqlib/"plugins")] @ [build_stdlib_vo_path ~unix_path:(coqlib/"theories") ~coq_path] @ (* then user-contrib *) @@ -116,14 +96,3 @@ let libs_init_load_path () = (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *) List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) - -(* Initialises the Ocaml toplevel before launching it, so that it can - find the "include" file in the *source* directory *) -let init_ocaml_path () = - let open Loadpath in - let lp s = { recursive = false; path_spec = MlPath s } in - let add_subdir dl = - Loadpath.add_coq_path (lp (List.fold_left (/) (Envars.coqlib()) [dl])) - in - Loadpath.add_coq_path (lp (Envars.coqlib ())); - List.iter add_subdir Coq_config.all_src_dirs diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index f3a007d987..eb6b37000e 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -14,10 +14,7 @@ val set_debug : unit -> unit val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State.t -val init_ocaml_path : unit -> unit - -(* LoadPath for toploop toplevels *) -val toplevel_init_load_path : unit -> Loadpath.coq_path list - (* LoadPath for Coq user libraries *) -val libs_init_load_path : unit -> Loadpath.coq_path list +val libs_init_load_path + : coqlib:CUnix.physical_path + -> CUnix.physical_path list * Loadpath.vo_path list diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index e4508e9bfc..7ff58039d4 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -265,7 +265,7 @@ let read_sentence ~state input = let open Vernac.State in try Stm.parse_sentence ~doc:state.doc state.sid ~entry:G_toplevel.vernac_toplevel input with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in discard_to_dot (); (* The caller of read_sentence does the error printing now, this should be re-enabled once we rely on the feedback error @@ -360,7 +360,7 @@ let top_goal_print ~doc c oldp newp = end with | exn -> - let (e, info) = CErrors.push exn in + let (e, info) = Exninfo.capture exn in let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer @@ -484,7 +484,7 @@ let read_and_execute ~state = TopErr.print_error_for_buffer Feedback.Error msg top_buffer; exit 1 | any -> - let (e, info) = CErrors.push any in + let (e, info) = Exninfo.capture any in let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer; @@ -501,10 +501,16 @@ let rec vernac_loop ~state = let state, drop = read_and_execute ~state in if drop then state else vernac_loop ~state -(* Default toplevel loop *) +(* Default toplevel loop, machinery for drop is below *) let drop_args = ref None +(* Initialises the Ocaml toplevel before launching it, so that it can + find the "include" file in the *source* directory *) +let init_ocaml_path ~coqlib = + let add_subdir dl = Mltop.add_ml_dir (Filename.concat coqlib dl) in + List.iter add_subdir ("dev" :: Coq_config.all_src_dirs) + let loop ~opts ~state = drop_args := Some opts; let open Coqargs in @@ -517,7 +523,8 @@ let loop ~opts ~state = (* Call the main loop *) let _ : Vernac.State.t = vernac_loop ~state in (* Initialise and launch the Ocaml toplevel *) - Coqinit.init_ocaml_path(); + let coqlib = Envars.coqlib () in + init_ocaml_path ~coqlib; Mltop.ocaml_toploop(); (* We delete the feeder after the OCaml toploop has ended so users of Drop can see the feedback. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 1ea48ee766..876388092d 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -155,19 +155,22 @@ let print_style_tags opts = let () = List.iter iter tags in flush_all () -let init_setup = function - | None -> Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); - | Some s -> Envars.set_user_coqlib s +let init_coqlib opts = match opts.config.coqlib with + | None when opts.pre.boot -> () + | None -> + Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); + | Some s -> + Envars.set_user_coqlib s let print_query opts = function | PrintVersion -> Usage.version () | PrintMachineReadableVersion -> Usage.machine_readable_version () | PrintWhere -> - let () = init_setup opts.config.coqlib in + let () = init_coqlib opts in print_endline (Envars.coqlib ()) | PrintHelp h -> Usage.print_usage stderr h | PrintConfig -> - let () = init_setup opts.config.coqlib in + let () = init_coqlib opts in Envars.print_config stdout Coq_config.all_src_dirs | PrintTags -> print_style_tags opts.config @@ -217,16 +220,12 @@ let init_parse parse_extra help init_opts = end; opts, customopts +(** Coq's init process, phase 2: Basic Coq environment, plugins. *) let init_execution opts custom_init = - (* Coq's init process, phase 2: - Basic Coq environment, load-path, plugins. - *) (* If we have been spawned by the Spawn module, this has to be done * early since the master waits us to connect back *) Spawned.init_channels (); if opts.post.memory_stat then at_exit print_memory_stat; - let top_lp = Coqinit.toplevel_init_load_path () in - List.iter Loadpath.add_coq_path top_lp; CoqworkmgrApi.(init opts.config.stm_flags.Stm.AsyncOpts.async_proofs_worker_priority); Mltop.init_known_plugins (); (* Configuration *) @@ -268,7 +267,7 @@ let init_toplevel custom = match opts.main with | Queries q -> List.iter (print_query opts) q; exit 0 | Run -> - let () = init_setup opts.config.coqlib in + let () = init_coqlib opts in let customstate = init_execution opts (custom.init customopts) in opts, customopts, customstate @@ -281,14 +280,14 @@ let init_document opts = *) (* Next line allows loading .vos files when in interactive mode *) Flags.load_vos_libraries := true; - let iload_path = build_load_path opts in + let ml_load_path, vo_load_path = build_load_path opts in let require_libs = require_libs opts in let stm_options = opts.config.stm_flags in let open Vernac.State in let doc, sid = Stm.(new_doc { doc_type = Interactive opts.config.logic.toplevel_name; - iload_path; require_libs; stm_options; + ml_load_path; vo_load_path; require_libs; stm_options; }) in { doc; sid; proof = None; time = opts.config.time } diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index 56fda58a25..d3768eb1e3 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -11,8 +11,6 @@ { open Pcoq open Pcoq.Prim -open Tok -open Util open Vernacexpr (* Vernaculars specific to the toplevel *) @@ -36,17 +34,10 @@ open Toplevel_ let err () = raise Stream.Failure let test_show_goal = - Pcoq.Entry.of_parser "test_show_goal" - (fun _ strm -> - match stream_nth 0 strm with - | IDENT "Show" -> - (match stream_nth 1 strm with - | IDENT "Goal" -> - (match stream_nth 2 strm with - | NUMERAL _ -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) + let open Pcoq.Lookahead in + to_entry "test_show_goal" begin + lk_kw "Show" >> lk_kw "Goal" >> lk_nat + end } diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index adcce67b0d..8e6cd8f4c7 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -69,7 +69,7 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = let new_proof = Vernacstate.Proof_global.give_me_the_proof_opt () [@ocaml.warning "-3"] in { state with doc = ndoc; sid = nsid; proof = new_proof; } with reraise -> - let (reraise, info) = CErrors.push reraise in + let (reraise, info) = Exninfo.capture reraise in (* XXX: In non-interactive mode edit_at seems to do very weird things, so we better avoid it while we investigate *) if interactive then ignore(Stm.edit_at ~doc:state.doc state.sid); @@ -77,7 +77,8 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = match Loc.get_loc info with | None -> Option.cata (Loc.add_loc info) info loc | Some _ -> info - end in iraise (reraise, info) + end in + Exninfo.iraise (reraise, info) (* Load a vernac file. CErrors are annotated with file and location *) let load_vernac_core ~echo ~check ~interactive ~state file = @@ -113,9 +114,9 @@ let load_vernac_core ~echo ~check ~interactive ~state file = in try loop state [] with any -> (* whatever the exception *) - let (e, info) = CErrors.push any in + let (e, info) = Exninfo.capture any in input_cleanup (); - iraise (e, info) + Exninfo.iraise (e, info) let process_expr ~state loc_ast = interp_vernac ~interactive:true ~check:true ~state loc_ast diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index e95ac3b02b..a0984aa2a9 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -13,7 +13,6 @@ open Pp open Util open Names -open Tok open Pcoq open Attributes open Constrexpr @@ -21,81 +20,52 @@ open Tac2expr open Tac2qexpr open Ltac_plugin -let err () = raise Stream.Failure - -type lookahead = Gramlib.Plexing.location_function -> int -> Tok.t Stream.t -> int option - -let check_no_space tok m strm = - let n = Stream.count strm in - if G_prim.contiguous tok n (n+m-1) then Some m else None - -let entry_of_lookahead s (lk : lookahead) = - let run tok strm = match lk tok 0 strm with None -> err () | Some _ -> () in - Pcoq.Entry.of_parser s run - -let (>>) (lk1 : lookahead) lk2 tok n strm = match lk1 tok n strm with -| None -> None -| Some n -> lk2 tok n strm - -let (<+>) (lk1 : lookahead) lk2 tok n strm = match lk1 tok n strm with -| None -> lk2 tok n strm -| Some n -> Some n - -let lk_empty tok n strm = Some n - -let lk_kw kw tok n strm = match stream_nth n strm with -| KEYWORD kw' | IDENT kw' -> if String.equal kw kw' then Some (n + 1) else None -| _ -> None - -let lk_ident tok n strm = match stream_nth n strm with -| IDENT _ -> Some (n + 1) -| _ -> None - -let lk_int tok n strm = match stream_nth n strm with -| NUMERAL { NumTok.int = _; frac = ""; exp = "" } -> Some (n + 1) -| _ -> None - -let lk_ident_or_anti = lk_ident <+> (lk_kw "$" >> lk_ident >> check_no_space) - -let rec lk_ident_list n strm = - ((lk_ident >> lk_ident_list) <+> lk_empty) n strm +let lk_ident_or_anti = + Pcoq.Lookahead.(lk_ident <+> (lk_kw "$" >> lk_ident >> check_no_space)) (* lookahead for (x:=t), (?x:=t) and (1:=t) *) let test_lpar_idnum_coloneq = - entry_of_lookahead "test_lpar_idnum_coloneq" begin - lk_kw "(" >> (lk_ident_or_anti <+> lk_int) >> lk_kw ":=" + let open Pcoq.Lookahead in + to_entry "test_lpar_idnum_coloneq" begin + lk_kw "(" >> (lk_ident_or_anti <+> lk_nat) >> lk_kw ":=" end (* lookahead for (x:t), (?x:t) *) let test_lpar_id_colon = - entry_of_lookahead "test_lpar_id_colon" begin + let open Pcoq.Lookahead in + to_entry "test_lpar_id_colon" begin lk_kw "(" >> lk_ident_or_anti >> lk_kw ":" end (* Hack to recognize "(x := t)" and "($x := t)" *) let test_lpar_id_coloneq = - entry_of_lookahead "test_lpar_id_coloneq" begin + let open Pcoq.Lookahead in + to_entry "test_lpar_id_coloneq" begin lk_kw "(" >> lk_ident_or_anti >> lk_kw ":=" end (* Hack to recognize "(x)" *) let test_lpar_id_rpar = - entry_of_lookahead "test_lpar_id_rpar" begin + let open Pcoq.Lookahead in + to_entry "test_lpar_id_rpar" begin lk_kw "(" >> lk_ident >> lk_kw ")" end let test_ampersand_ident = - entry_of_lookahead "test_ampersand_ident" begin + let open Pcoq.Lookahead in + to_entry "test_ampersand_ident" begin lk_kw "&" >> lk_ident >> check_no_space end let test_dollar_ident = - entry_of_lookahead "test_dollar_ident" begin + let open Pcoq.Lookahead in + to_entry "test_dollar_ident" begin lk_kw "$" >> lk_ident >> check_no_space end let test_ltac1_env = - entry_of_lookahead "test_ltac1_env" begin + let open Pcoq.Lookahead in + to_entry "test_ltac1_env" begin lk_ident_list >> lk_kw "|-" end diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 196b28b274..f66ed7b4cf 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -573,7 +573,7 @@ let () = define1 "constr_check" constr begin fun c -> Proofview.Unsafe.tclEVARS sigma >>= fun () -> return (of_result Value.of_constr (Inl c)) with e when CErrors.noncritical e -> - let e = CErrors.push e in + let e = Exninfo.capture e in return (of_result Value.of_constr (Inr e)) end end @@ -1079,7 +1079,7 @@ let interp_constr flags ist c = Proofview.Unsafe.tclEVARS sigma >>= fun () -> Proofview.tclUNIT c with e when catchable_exception e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in set_bt info >>= fun info -> match Exninfo.get info fatal_flag with | None -> Proofview.tclZERO ~info e diff --git a/vernac/classes.ml b/vernac/classes.ml index b92c9e9b71..16b9e07fb2 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -60,7 +60,9 @@ let add_instance check inst = let local = is_local_for_hint inst in add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] local inst.is_info poly; - List.iter (fun (path, pri, c) -> add_instance_hint (Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)) path + List.iter (fun (path, pri, c) -> + let h = Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) [@ocaml.warning "-3"] in + add_instance_hint h path local pri poly) (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index e57c324c9a..2b6f987fa6 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -37,9 +37,9 @@ module Hook = struct let call ?hook ?fix_exn x = try Option.iter (fun hook -> CEphemeron.get hook x) hook with e when CErrors.noncritical e -> - let e = CErrors.push e in + let e = Exninfo.capture e in let e = Option.cata (fun fix -> fix e) e fix_exn in - Util.iraise e + Exninfo.iraise e end (* Locality stuff *) diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index c816a4eb4f..e645fc552b 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -935,9 +935,9 @@ let protect_summaries f = try f fs with reraise -> (* Something wrong: undo the whole process *) - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in let () = Summary.unfreeze_summaries fs in - iraise reraise + Exninfo.iraise reraise let start_module export id args res = protect_summaries (RawModOps.start_module export id args res) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index def4ed942a..c1414c552a 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -22,7 +22,6 @@ open Extend open Decls open Declaremods open Namegen -open Tok (* necessary for camlp5 *) open Pcoq open Pcoq.Prim @@ -45,11 +44,12 @@ let quoted_attributes = Entry.create "vernac:quoted_attributes" let class_rawexpr = Entry.create "vernac:class_rawexpr" let thm_token = Entry.create "vernac:thm_token" let def_body = Entry.create "vernac:def_body" -let decl_notation = Entry.create "vernac:decl_notation" +let decl_notations = Entry.create "vernac:decl_notations" let record_field = Entry.create "vernac:record_field" let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion" let section_subset_expr = Entry.create "vernac:section_subset_expr" let scope_delimiter = Entry.create "vernac:scope_delimiter" +let only_parsing = Entry.create "vernac:only_parsing" let make_bullet s = let open Proof_bullet in @@ -177,7 +177,7 @@ let name_of_ident_decl : ident_decl -> name_decl = (* Gallina declarations *) GRAMMAR EXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion - record_field decl_notation rec_definition ident_decl univ_decl; + record_field decl_notations rec_definition ident_decl univ_decl; gallina: (* Definition, Theorem, Variable, Axiom, ... *) @@ -377,15 +377,17 @@ GRAMMAR EXTEND Gram [ [ IDENT "Eval"; r = red_expr; "in" -> { Some r } | -> { None } ] ] ; - one_decl_notation: - [ [ ntn = ne_lstring; ":="; c = constr; - scopt = OPT [ ":"; sc = IDENT -> { sc } ] -> { (ntn,c,scopt) } ] ] + decl_notation: + [ [ ntn = ne_lstring; ":="; c = constr; b = only_parsing; + scopt = OPT [ ":"; sc = IDENT -> { sc } ] -> + { { decl_ntn_string = ntn; decl_ntn_interp = c; + decl_ntn_only_parsing = b; decl_ntn_scope = scopt } } ] ] ; decl_sep: [ [ IDENT "and" -> { () } ] ] ; - decl_notation: - [ [ "where"; l = LIST1 one_decl_notation SEP decl_sep -> { l } + decl_notations: + [ [ "where"; l = LIST1 decl_notation SEP decl_sep -> { l } | -> { [] } ] ] ; (* Inductives and records *) @@ -397,7 +399,7 @@ GRAMMAR EXTEND Gram [ [ oc = opt_coercion; id = ident_decl; indpar = binders; extrapar = OPT [ "|"; p = binders -> { p } ]; c = OPT [ ":"; c = lconstr -> { c } ]; - lc=opt_constructors_or_fields; ntn = decl_notation -> + lc=opt_constructors_or_fields; ntn = decl_notations -> { (((oc,id),(indpar,extrapar),c,lc),ntn) } ] ] ; constructor_list_or_record_decl: @@ -424,14 +426,14 @@ GRAMMAR EXTEND Gram [ [ id_decl = ident_decl; bl = binders_fixannot; rtype = type_cstr; - body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notation -> + body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notations -> { let binders, rec_order = bl in {fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations} } ] ] ; corec_definition: [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr; - body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notation -> + body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notations -> { {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations} } ]] ; @@ -467,7 +469,7 @@ GRAMMAR EXTEND Gram record_field: [ [ attr = LIST0 quoted_attributes ; bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ]; - rf_notation = decl_notation -> { + rf_notation = decl_notations -> { let rf_canonical = attr |> List.flatten |> parse canonical_field in let rf_subclass, rf_decl = bd in rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ] @@ -531,16 +533,12 @@ END { -let only_starredidentrefs = - Pcoq.Entry.of_parser "test_only_starredidentrefs" - (fun _ strm -> - let rec aux n = - match Util.stream_nth n strm with - | KEYWORD "." -> () - | KEYWORD ")" -> () - | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1) - | _ -> raise Stream.Failure in - aux 0) +let test_only_starredidentrefs = + let open Pcoq.Lookahead in + to_entry "test_only_starredidentrefs" begin + lk_list (lk_ident <+> lk_kws ["Type"; "*"]) >> (lk_kws [".";")"]) + end + let starredidentreflist_to_expr l = match l with | [] -> SsEmpty @@ -670,7 +668,7 @@ GRAMMAR EXTEND Gram ; (* Proof using *) section_subset_expr: - [ [ only_starredidentrefs; l = LIST0 starredidentref -> + [ [ test_only_starredidentrefs; l = LIST0 starredidentref -> { starredidentreflist_to_expr l } | e = ssexpr -> { e } ]] ; @@ -688,9 +686,9 @@ GRAMMAR EXTEND Gram | e1 = ssexpr; "+"; e2 = ssexpr-> { SsUnion(e1,e2) } ] | "0" [ i = starredidentref -> { i } - | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"-> + | "("; test_only_starredidentrefs; l = LIST0 starredidentref; ")"-> { starredidentreflist_to_expr l } - | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" -> + | "("; test_only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" -> { SsFwdClose(starredidentreflist_to_expr l) } | "("; e = ssexpr; ")"-> { e } | "("; e = ssexpr; ")"; "*" -> { SsFwdClose e } ] ] @@ -917,10 +915,11 @@ GRAMMAR EXTEND Gram | IDENT "Locate"; l = locatable -> { VernacLocate l } (* Managing load paths *) - | IDENT "Add"; IDENT "LoadPath"; dir = ne_string; alias = as_dirpath -> - { VernacAddLoadPath (false, dir, alias) } - | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string; - alias = as_dirpath -> { VernacAddLoadPath (true, dir, alias) } + | IDENT "Add"; IDENT "LoadPath"; physical_path = ne_string; "as"; logical_path = dirpath -> + { VernacAddLoadPath { implicit = false; logical_path; physical_path } } + | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; physical_path = ne_string; "as"; logical_path = dirpath -> + { VernacAddLoadPath { implicit = true; logical_path; physical_path } } + | IDENT "Remove"; IDENT "LoadPath"; dir = ne_string -> { VernacRemoveLoadPath dir } @@ -939,9 +938,7 @@ GRAMMAR EXTEND Gram | IDENT "Inspect"; n = natural -> { VernacPrint (PrintInspect n) } | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string -> - { VernacAddMLPath (false, dir) } - | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string -> - { VernacAddMLPath (true, dir) } + { VernacAddMLPath dir } (* For acting on parameter tables *) | "Set"; table = option_table; v = option_setting -> @@ -1075,9 +1072,6 @@ GRAMMAR EXTEND Gram option_table: [ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]] ; - as_dirpath: - [ [ d = OPT [ "as"; d = dirpath -> { d } ] -> { d } ] ] - ; ne_in_or_out_modules: [ [ IDENT "inside"; l = LIST1 global -> { SearchInside l } | IDENT "outside"; l = LIST1 global -> { SearchOutside l } ] ] @@ -1154,7 +1148,7 @@ GRAMMAR EXTEND Gram (* Grammar extensions *) GRAMMAR EXTEND Gram - GLOBAL: syntax; + GLOBAL: syntax only_parsing; syntax: [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT -> diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 227d2f1554..80616ecc2a 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -118,7 +118,7 @@ let alarm what internal msg = let try_declare_scheme what f internal names kn = try f internal names kn with e -> - let e = CErrors.push e in + let e = Exninfo.capture e in let rec extract_exn = function Logic_monad.TacticFailure e -> extract_exn e | e -> e in let msg = match extract_exn (fst e) with | ParameterWithoutEquality cst -> @@ -166,11 +166,11 @@ let try_declare_scheme what f internal names kn = | e when CErrors.noncritical e -> alarm what internal (str "Unexpected error during scheme creation: " ++ CErrors.print e) - | _ -> iraise e + | _ -> Exninfo.iraise e in match msg with | None -> () - | Some msg -> iraise (UserError (None, msg), snd e) + | Some msg -> Exninfo.iraise (UserError (None, msg), snd e) let beq_scheme_msg mind = let mib = Global.lookup_mind mind in diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index f7606f4ede..68f4f55d0e 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -375,8 +375,8 @@ let finish_proved env sigma idopt po info = (* This takes care of the implicits and hook for the current constant*) process_recthms ~fix_exn ?hook env sigma universes ~udecl ~poly ~scope r impargs other_thms with e when CErrors.noncritical e -> - let e = CErrors.push e in - iraise (fix_exn e) + let e = Exninfo.capture e in + Exninfo.iraise (fix_exn e) in () | _ -> CErrors.anomaly Pp.(str "[standard_proof_terminator] close_proof returned more than one proof term") diff --git a/vernac/library.ml b/vernac/library.ml index 0f7e7d2aa0..5aff86c50c 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -440,11 +440,11 @@ let save_library_base f sum lib univs tasks proofs = System.marshal_out_segment f ch (proofs : seg_proofs); close_out ch with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in close_out ch; Feedback.msg_warning (str "Removed file " ++ str f); Sys.remove f; - iraise reraise + Exninfo.iraise reraise type ('document,'counters) todo_proofs = | ProofsTodoNone (* for .vo *) diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml index 506b3bc505..38aa42c349 100644 --- a/vernac/loadpath.ml +++ b/vernac/loadpath.ml @@ -218,24 +218,18 @@ let try_locate_absolute_library dir = (** { 5 Extending the load path } *) -(* Adds a path to the Coq and ML paths *) -type add_ml = AddNoML | AddTopML | AddRecML - -type vo_path_spec = { - unix_path : string; (* Filesystem path containing vo/ml files *) - coq_path : DP.t; (* Coq prefix for the path *) - implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *) - has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *) -} - -type coq_path_spec = - | VoPath of vo_path_spec - | MlPath of string - -type coq_path = { - path_spec: coq_path_spec; - recursive: bool; -} +type vo_path = + { unix_path : string + (** Filesystem path containing vo/ml files *) + ; coq_path : DP.t + (** Coq prefix for the path *) + ; implicit : bool + (** [implicit = true] avoids having to qualify with [coq_path] *) + ; has_ml : bool + (** If [has_ml] is true, the directory will also be added to the ml include path *) + ; recursive : bool + (** [recursive] will determine whether we explore sub-directories *) + } let warn_cannot_open_path = CWarnings.create ~name:"cannot-open-path" ~category:"filesystem" @@ -255,9 +249,10 @@ let convert_string d = warn_cannot_use_directory d; raise Exit -let add_vo_path ~recursive lp = +let add_vo_path lp = let unix_path = lp.unix_path in let implicit = lp.implicit in + let recursive = lp.recursive in if System.exists_dir unix_path then let dirs = if recursive then System.all_subdirs ~unix_path else [] in let prefix = DP.repr lp.coq_path in @@ -268,22 +263,17 @@ let add_vo_path ~recursive lp = with Exit -> None in let dirs = List.map_filter convert_dirs dirs in - let add_ml_dir = Mltop.add_ml_dir ~recursive:false in - let () = match lp.has_ml with - | AddNoML -> () - | AddTopML -> - Mltop.add_ml_dir ~recursive:false unix_path - | AddRecML -> - List.iter (fun (lp,_) -> add_ml_dir lp) dirs; - add_ml_dir unix_path in + let () = + if lp.has_ml && not lp.recursive then + Mltop.add_ml_dir unix_path + else if lp.has_ml && lp.recursive then + (List.iter (fun (lp,_) -> Mltop.add_ml_dir lp) dirs; + Mltop.add_ml_dir unix_path) + else + () + in let add (path, dir) = add_load_path path ~implicit dir in let () = List.iter add dirs in add_load_path unix_path ~implicit lp.coq_path else warn_cannot_open_path unix_path - -let add_coq_path { recursive; path_spec } = match path_spec with - | VoPath lp -> - add_vo_path ~recursive lp - | MlPath dir -> - Mltop.add_ml_dir ~recursive dir diff --git a/vernac/loadpath.mli b/vernac/loadpath.mli index 47d2d34125..68212b9a47 100644 --- a/vernac/loadpath.mli +++ b/vernac/loadpath.mli @@ -64,26 +64,17 @@ val try_locate_absolute_library : DirPath.t -> string (** {6 Extending the Load Path } *) (** Adds a path to the Coq and ML paths *) -type add_ml = AddNoML | AddTopML | AddRecML - -type vo_path_spec = { - unix_path : string; +type vo_path = + { unix_path : string (** Filesystem path containing vo/ml files *) - coq_path : Names.DirPath.t; + ; coq_path : DirPath.t (** Coq prefix for the path *) - implicit : bool; + ; implicit : bool (** [implicit = true] avoids having to qualify with [coq_path] *) - has_ml : add_ml; - (** If [has_ml] is true, the directory will also be search for plugins *) -} - -type coq_path_spec = - | VoPath of vo_path_spec - | MlPath of string - -type coq_path = { - path_spec: coq_path_spec; - recursive: bool; -} + ; has_ml : bool + (** If [has_ml] is true, the directory will also be added to the ml include path *) + ; recursive : bool + (** [recursive] will determine whether we explore sub-directories *) + } -val add_coq_path : coq_path -> unit +val add_vo_path : vo_path -> unit diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 3937f887ad..33fd14a731 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1466,9 +1466,9 @@ let with_lib_stk_protection f x = let fs = Lib.freeze () in try let a = f x in Lib.unfreeze fs; a with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in let () = Lib.unfreeze fs in - iraise reraise + Exninfo.iraise reraise let with_syntax_protection f x = with_lib_stk_protection @@ -1654,13 +1654,23 @@ let add_syntax_extension ~local ({CAst.loc;v=df},mods) = let open SynData in (* Notations with only interpretation *) -let add_notation_interpretation env ({CAst.loc;v=df},c,sc) = - let df' = add_notation_interpretation_core ~local:false df env c sc false false None in +let add_notation_interpretation env decl_ntn = + let + { decl_ntn_string = { CAst.loc ; v = df }; + decl_ntn_interp = c; + decl_ntn_only_parsing = onlyparse; + decl_ntn_scope = sc } = decl_ntn in + let df' = add_notation_interpretation_core ~local:false df env c sc onlyparse false None in Dumpglob.dump_notation (loc,df') sc true -let set_notation_for_interpretation env impls ({CAst.v=df},c,sc) = +let set_notation_for_interpretation env impls decl_ntn = + let + { decl_ntn_string = { CAst.v = df }; + decl_ntn_interp = c; + decl_ntn_only_parsing = onlyparse; + decl_ntn_scope = sc } = decl_ntn in (try ignore - (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls c sc false false None) ()); + (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls c sc onlyparse false None) ()); with NoSyntaxRule -> user_err Pp.(str "Parsing rule for this notation has to be previously declared.")); Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index e3e733a4b7..d76820b033 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -37,12 +37,12 @@ val add_class_scope : locality_flag -> scope_name -> scope_class list -> unit (** Add only the interpretation of a notation that already has pa/pp rules *) val add_notation_interpretation : - env -> (lstring * constr_expr * scope_name option) -> unit + env -> decl_notation -> unit (** Add a notation interpretation for supporting the "where" clause *) -val set_notation_for_interpretation : env -> Constrintern.internalization_env -> - (lstring * constr_expr * scope_name option) -> unit +val set_notation_for_interpretation : + env -> Constrintern.internalization_env -> decl_notation -> unit (** Add only the parsing/printing rule of a notation *) diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 5046248e11..671dae7876 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -128,11 +128,6 @@ let add_ml_dir s = | WithoutTop when has_dynlink -> keep_copy_mlpath s | _ -> () -(* For Rec Add ML Path (-R) *) -let add_ml_dir ~recursive unix_path = - let dirs = if recursive then (all_subdirs ~unix_path) else [unix_path,[]] in - List.iter (fun (lp,_) -> add_ml_dir lp) dirs - (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = if Filename.check_suffix name ".cmo" then diff --git a/vernac/mltop.mli b/vernac/mltop.mli index 271772d7ba..633a5c241d 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -32,7 +32,7 @@ val ocaml_toploop : unit -> unit (** {5 ML Dynlink} *) (** Adds a dir to the plugin search path *) -val add_ml_dir : recursive:bool -> string -> unit +val add_ml_dir : string -> unit (** Tests if we can load ML files *) val has_dynlink : bool diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 76dbf1ad5a..27eb821a6a 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -428,7 +428,7 @@ let solve_by_tac ?loc name evi t poly ctx = Some (body, entry.Declare.proof_entry_type, ctx') with | Refiner.FailError (_, s) as exn -> - let _ = CErrors.push exn in + let _ = Exninfo.capture exn in user_err ?loc ~hdr:"solve_obligation" (Lazy.force s) (* If the proof is open we absorb the error and leave the obligation open *) | Proof.OpenProof _ -> diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 314c423f65..84ae04e4cc 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -297,11 +297,6 @@ open Pputils | { v = CHole (k, Namegen.IntroAnonymous, _) } -> mt() | _ as c -> brk(0,2) ++ str" :" ++ pr_c c - let pr_decl_notation prc ({loc; v=ntn},c,scopt) = - fnl () ++ keyword "where " ++ qs ntn ++ str " := " - ++ Flags.without_option Flags.beautify prc c ++ - pr_opt (fun sc -> str ": " ++ str sc) scopt - let pr_binders_arg = let env = Global.env () in let sigma = Evd.from_env env in @@ -418,6 +413,21 @@ let string_of_theorem_kind = let open Decls in function | l -> spc() ++ hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") + let pr_only_parsing_clause onlyparsing = + pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []) + + let pr_decl_notation prc decl_ntn = + let open Vernacexpr in + let + { decl_ntn_string = {CAst.loc;v=ntn}; + decl_ntn_interp = c; + decl_ntn_only_parsing = onlyparsing; + decl_ntn_scope = scopt } = decl_ntn in + fnl () ++ keyword "where " ++ qs ntn ++ str " := " + ++ Flags.without_option Flags.beautify prc c + ++ pr_only_parsing_clause onlyparsing + ++ pr_opt (fun sc -> str ": " ++ str sc) scopt + let pr_rec_definition { fname; univs; rec_order; binders; rtype; body_def; notations } = let env = Global.env () in let sigma = Evd.from_env env in @@ -1016,22 +1026,18 @@ let string_of_definition_object_kind = let open Decls in function return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c) (* Auxiliary file and library management *) - | VernacAddLoadPath (fl,s,d) -> + | VernacAddLoadPath { implicit; physical_path; logical_path } -> return ( hov 2 (keyword "Add" ++ - (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++ - keyword "LoadPath" ++ spc() ++ qs s ++ - (match d with - | None -> mt() - | Some dir -> spc() ++ keyword "as" ++ spc() ++ DirPath.print dir)) - ) + (if implicit then spc () ++ keyword "Rec" ++ spc () else spc()) ++ + keyword "LoadPath" ++ spc() ++ qs physical_path ++ + spc() ++ keyword "as" ++ spc() ++ DirPath.print logical_path)) | VernacRemoveLoadPath s -> return (keyword "Remove LoadPath" ++ qs s) - | VernacAddMLPath (fl,s) -> + | VernacAddMLPath (s) -> return ( keyword "Add" - ++ (if fl then spc () ++ keyword "Rec" ++ spc () else spc()) ++ keyword "ML Path" ++ qs s ) @@ -1061,7 +1067,7 @@ let string_of_definition_object_kind = let open Decls in function hov 2 (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++ - pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])) + pr_only_parsing_clause onlyparsing) ) | VernacArguments (q, args, more_implicits, mods) -> return ( diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index de02f7ecfb..509c164af8 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -361,7 +361,7 @@ let in_phase ~phase f x = with exn -> let iexn = Exninfo.capture exn in default_phase := op; - Util.iraise iexn + Exninfo.iraise iexn let pr_loc loc = let fname = loc.Loc.fname in @@ -394,7 +394,7 @@ let pr_phase ?loc () = None let print_err_exn any = - let (e, info) = CErrors.push any in + let (e, info) = Exninfo.capture any in let loc = Loc.get_loc info in let pre_hdr = pr_phase ?loc () in let msg = CErrors.iprint (e, info) ++ fnl () in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 2eb1aa39b0..953faf6fdb 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -342,9 +342,9 @@ let dump_universes_gen prl g s = close (); str "Universes written to file \"" ++ str s ++ str "\"." with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in close (); - iraise reraise + Exninfo.iraise reraise let universe_subgraph ?loc g univ = let open Univ in @@ -1120,20 +1120,17 @@ let vernac_set_used_variables ~pstate e : Proof_global.t = let expand filename = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename -let vernac_add_loadpath implicit pdir ldiropt = +let vernac_add_loadpath ~implicit pdir coq_path = let open Loadpath in let pdir = expand pdir in - let alias = Option.default Libnames.default_root_prefix ldiropt in - add_coq_path { recursive = true; - path_spec = VoPath { unix_path = pdir; coq_path = alias; has_ml = AddTopML; implicit } } + add_vo_path { unix_path = pdir; coq_path; has_ml = true; implicit; recursive = true } let vernac_remove_loadpath path = Loadpath.remove_load_path (expand path) (* Coq syntax for ML or system commands *) -let vernac_add_ml_path isrec path = - let open Loadpath in - add_coq_path { recursive = isrec; path_spec = MlPath (expand path) } +let vernac_add_ml_path path = + Mltop.add_ml_dir (expand path) let vernac_declare_ml_module ~local l = let local = Option.default false local in @@ -2106,18 +2103,18 @@ let translate_vernac ~atts v = let open Vernacextend in match v with unsupported_attributes atts; vernac_solve_existential ~pstate n c) (* Auxiliary file and library management *) - | VernacAddLoadPath (isrec,s,alias) -> + | VernacAddLoadPath { implicit; physical_path; logical_path } -> VtDefault(fun () -> unsupported_attributes atts; - vernac_add_loadpath isrec s alias) + vernac_add_loadpath ~implicit physical_path logical_path) | VernacRemoveLoadPath s -> VtDefault(fun () -> unsupported_attributes atts; vernac_remove_loadpath s) - | VernacAddMLPath (isrec,s) -> + | VernacAddMLPath (s) -> VtDefault(fun () -> unsupported_attributes atts; - vernac_add_ml_path isrec s) + vernac_add_ml_path s) | VernacDeclareMLModule l -> VtDefault(fun () -> with_locality ~atts vernac_declare_ml_module l) | VernacChdir s -> diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 45018a246c..7169ea834a 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -98,7 +98,6 @@ type search_restriction = | SearchInside of qualid list | SearchOutside of qualid list -type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option @@ -129,7 +128,12 @@ type definition_expr = | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr * constr_expr option -type decl_notation = lstring * constr_expr * scope_name option +type decl_notation = + { decl_ntn_string : lstring + ; decl_ntn_interp : constr_expr + ; decl_ntn_only_parsing : bool + ; decl_ntn_scope : scope_name option + } type 'a fix_expr_gen = { fname : lident @@ -363,9 +367,13 @@ type nonrec vernac_expr = | VernacSolveExistential of int * constr_expr (* Auxiliary file and library management *) - | VernacAddLoadPath of rec_flag * string * DirPath.t option + | VernacAddLoadPath of { implicit : bool + ; physical_path : CUnix.physical_path + ; logical_path : DirPath.t + } + | VernacRemoveLoadPath of string - | VernacAddMLPath of rec_flag * string + | VernacAddMLPath of string | VernacDeclareMLModule of string list | VernacChdir of string option diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index f41df06f85..e0afb7f483 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -109,11 +109,11 @@ let type_vernac opn converted_args ~atts = phase := "Executing command"; hunk ~atts with - | reraise -> - let reraise = CErrors.push reraise in - if !Flags.debug then - Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase); - iraise reraise + | reraise -> + let reraise = Exninfo.capture reraise in + if !Flags.debug then + Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase); + Exninfo.iraise reraise (** VERNAC EXTEND registering *) diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 1ec09b6beb..8083098022 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -96,7 +96,7 @@ let with_fail f : (Pp.t, unit) result = (* Fail Timeout is a common pattern so we need to support it. *) | e when CErrors.noncritical e || e = CErrors.Timeout -> (* The error has to be printed in the failing state *) - Ok CErrors.(iprint (push e)) + Ok CErrors.(iprint (Exninfo.capture e)) (* We restore the state always *) let with_fail ~st f = @@ -262,10 +262,10 @@ let interp_gen ~verbosely ~st ~interp_fn cmd = Vernacstate.freeze_interp_state ~marshallable:false ) st with exn -> - let exn = CErrors.push exn in + let exn = Exninfo.capture exn in let exn = locate_if_not_already ?loc:cmd.CAst.loc exn in Vernacstate.invalidate_cache (); - Util.iraise exn + Exninfo.iraise exn (* Regular interp *) let interp ?(verbosely=true) ~st cmd = diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 3c70961e06..59557a60a6 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -21,7 +21,7 @@ module Parser = struct Flags.with_option Flags.we_are_parsing (fun () -> try Pcoq.Entry.parse entry pa with e when CErrors.noncritical e -> - let (e, info) = CErrors.push e in + let (e, info) = Exninfo.capture e in Exninfo.iraise (e, info)) () |