diff options
42 files changed, 1095 insertions, 931 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 77e34d4e00..f434b63d74 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -596,7 +596,7 @@ plugin:ci-elpi: plugin:ci-equations: <<: *ci-template -plugin:ci-fiat-parsers: +plugin:ci-fiat_parsers: <<: *ci-template plugin:ci-ltac2: diff --git a/Makefile.ci b/Makefile.ci index b8bff98f5f..0307d39d54 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -25,7 +25,7 @@ CI_TARGETS= \ ci-fcsl-pcm \ ci-fiat-crypto \ ci-fiat-crypto-legacy \ - ci-fiat-parsers \ + ci-fiat_parsers \ ci-flocq \ ci-geocoq \ ci-coqhammer \ diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat_parsers.sh index ac74ebf667..ac74ebf667 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat_parsers.sh diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index 277e9ee08f..94e0a666e2 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -39,11 +39,21 @@ let corn = (coqPackages.corn.override { inherit coq bignums math-classes; }) src = fetchTarball "https://github.com/coq-community/corn/archive/master.tar.gz"; }); in +let stdpp = coqPackages.stdpp.overrideAttrs (o: { + src = fetchTarball "https://gitlab.mpi-sws.org/iris/stdpp/-/archive/master/stdpp-master.tar.bz2"; + }); in + +let iris = (coqPackages.iris.override { inherit coq stdpp; }) + .overrideAttrs (o: { + src = fetchTarball "https://gitlab.mpi-sws.org/iris/iris/-/archive/master/iris-master.tar.bz2"; + propagatedBuildInputs = [ stdpp ]; + }); in + let unicoq = callPackage ./unicoq { inherit coq; }; in let callPackage = newScope { inherit coq - bignums coq-ext-lib coqprime corn math-classes - mathcomp simple-io ssreflect unicoq; + bignums coq-ext-lib coqprime corn iris math-classes + mathcomp simple-io ssreflect stdpp unicoq; }; in # Environments for building CI libraries with this Coq @@ -62,6 +72,8 @@ let projects = { formal-topology = callPackage ./formal-topology.nix {}; GeoCoq = callPackage ./GeoCoq.nix {}; HoTT = callPackage ./HoTT.nix {}; + iris = callPackage ./iris.nix {}; + lambda-rust = callPackage ./lambda-rust.nix {}; math_classes = callPackage ./math_classes.nix {}; mathcomp = {}; mtac2 = callPackage ./mtac2.nix {}; diff --git a/dev/ci/nix/iris.nix b/dev/ci/nix/iris.nix new file mode 100644 index 0000000000..b55cccc7c6 --- /dev/null +++ b/dev/ci/nix/iris.nix @@ -0,0 +1,4 @@ +{ stdpp }: +{ + coqBuildInputs = [ stdpp ]; +} diff --git a/dev/ci/nix/lambda-rust.nix b/dev/ci/nix/lambda-rust.nix new file mode 100644 index 0000000000..0d07c3028a --- /dev/null +++ b/dev/ci/nix/lambda-rust.nix @@ -0,0 +1,4 @@ +{ iris }: +{ + coqBuildInputs = [ iris ]; +} diff --git a/dev/ci/nix/unicoq/META b/dev/ci/nix/unicoq/META deleted file mode 100644 index 30dd8b5559..0000000000 --- a/dev/ci/nix/unicoq/META +++ /dev/null @@ -1,2 +0,0 @@ -archive(native) = "unicoq.cmxa" -plugin(native) = "unicoq.cmxs" diff --git a/dev/ci/nix/unicoq/default.nix b/dev/ci/nix/unicoq/default.nix index 36f40dbe33..54c67ac0fd 100644 --- a/dev/ci/nix/unicoq/default.nix +++ b/dev/ci/nix/unicoq/default.nix @@ -1,4 +1,10 @@ -{ stdenv, coq }: +{ stdenv, writeText, coq }: + +let META = writeText "META" '' + archive(native) = "unicoq.cmxa" + plugin(native) = "unicoq.cmxs" +''; in + stdenv.mkDerivation { name = "coq${coq.coq-version}-unicoq-0.0-git"; @@ -12,8 +18,9 @@ stdenv.mkDerivation { installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; postInstall = '' + cp ${META} META install -d $OCAMLFIND_DESTDIR ln -s $out/lib/coq/${coq.coq-version}/user-contrib/Unicoq $OCAMLFIND_DESTDIR/ - install -m 0644 ${./META} src/unicoq.a $OCAMLFIND_DESTDIR/Unicoq + install -m 0644 META src/unicoq.a $OCAMLFIND_DESTDIR/Unicoq ''; } diff --git a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh b/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh deleted file mode 100644 index 6e89741e29..0000000000 --- a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6914" ] || [ "$CI_BRANCH" = "primitive-bool-list" ]; then - - bignums_CI_REF=primitive-integers - bignums_CI_GITURL=https://github.com/vbgl/bignums - - mtac2_CI_REF=primitive-integers - mtac2_CI_GITURL=https://github.com/vbgl/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh deleted file mode 100644 index 2df8affd14..0000000000 --- a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9102" ] || [ "$CI_BRANCH" = "ltac+remove_aliases" ]; then - - elpi_CI_REF=ltac+remove_aliases - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - -fi diff --git a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh b/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh deleted file mode 100644 index f2a113b118..0000000000 --- a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9150" ] || [ "$CI_BRANCH" = "build+warn_50" ]; then - - mtac2_CI_REF=build+warn_50 - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh deleted file mode 100644 index f532fdfc52..0000000000 --- a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9172" ] || [ "$CI_BRANCH" = "proof_rework" ]; then - - ltac2_CI_REF=proof_rework - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - mtac2_CI_REF=proof_rework - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh new file mode 100644 index 0000000000..23eb24c304 --- /dev/null +++ b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "9173" ] || [ "$CI_BRANCH" = "proofview+proof_info" ]; then + + ltac2_CI_REF=proofview+proof_info + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + fiat_parsers_CI_REF=proofview+proof_info + fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat + +fi diff --git a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh b/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh deleted file mode 100644 index efcdd2e97f..0000000000 --- a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9220" ] || [ "$CI_BRANCH" = "stm-shallow-logic" ]; then - - paramcoq_CI_REF=stm-shallow-logic - paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq - -fi diff --git a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh deleted file mode 100644 index ebd1b524da..0000000000 --- a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9263" ] || [ "$CI_BRANCH" = "parsing-state" ]; then - - mtac2_CI_REF=proof-mode - mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2 - - ltac2_CI_REF=proof-mode - ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - equations_CI_REF=proof-mode - equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/09410-maximedenes-thread-program.sh b/dev/ci/user-overlays/09410-maximedenes-thread-program.sh deleted file mode 100644 index 985c2db74e..0000000000 --- a/dev/ci/user-overlays/09410-maximedenes-thread-program.sh +++ /dev/null @@ -1,13 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9410" ] || [ "$CI_BRANCH" = "thread-program" ]; then - - math_classes_CI_REF=program-mode-flag - math_classes_CI_GITURL=https://github.com/maximedenes/math-classes - - ltac2_CI_REF=program-mode-flag - ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - - equations_CI_REF=thread-program - equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - -fi diff --git a/dev/core_dune.dbg b/dev/core_dune.dbg index cf9c5bd39a..4e1035f7b6 100644 --- a/dev/core_dune.dbg +++ b/dev/core_dune.dbg @@ -1,10 +1,10 @@ load_printer threads.cma load_printer str.cma -load_printer gramlib.cma load_printer config.cma load_printer clib.cma load_printer dynlink.cma load_printer lib.cma +load_printer gramlib.cma load_printer byterun.cma load_printer kernel.cma load_printer library.cma diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index e5b41be691..d15aacad44 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -37,7 +37,7 @@ In addition to these user-defined classes, we have two built-in classes: * ``Funclass``, the class of functions; its objects are all the terms with a functional type, i.e. of form :g:`forall x:A,B`. -Formally, the syntax of a classes is defined as: +Formally, the syntax of classes is defined as: .. productionlist:: class: `qualid` @@ -289,7 +289,7 @@ by extending the existing :cmd:`Record` macro. Its new syntax is: The first identifier :token:`ident` is the name of the defined record and :token:`sort` is its type. The optional identifier after ``:=`` is the name - of the constuctor (it will be :n:`Build_@ident` if not given). + of the constructor (it will be :n:`Build_@ident` if not given). The other identifiers are the names of the fields, and :token:`term` are their respective types. If ``:>`` is used instead of ``:`` in the declaration of a field, then the name of this field is automatically @@ -365,7 +365,7 @@ We first give an example of coercion between atomic inductive types .. warning:: - Note that ``Check true=O`` would fail. This is "normal" behavior of + Note that ``Check (true = O)`` would fail. This is "normal" behavior of coercions. To validate ``true=O``, the coercion is searched from ``nat`` to ``bool``. There is none. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 5788ae19e6..0bcfce2322 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3406,129 +3406,140 @@ Automation This tactic implements a Prolog-like resolution procedure to solve the current goal. It first tries to solve the goal using the :tacn:`assumption` - tactic, then it reduces the goal to an atomic one using intros and + tactic, then it reduces the goal to an atomic one using :tacn:`intros` and introduces the newly generated hypotheses as hints. Then it looks at the list of tactics associated to the head symbol of the goal and tries to apply one of them (starting from the tactics with lower cost). This process is recursively applied to the generated subgoals. - By default, auto only uses the hypotheses of the current goal and the - hints of the database named core. + By default, :tacn:`auto` only uses the hypotheses of the current goal and + the hints of the database named ``core``. -.. tacv:: auto @num + .. warning:: - Forces the search depth to be :token:`num`. The maximal search depth - is 5 by default. + :tacn:`auto` uses a weaker version of :tacn:`apply` that is closer to + :tacn:`simple apply` so it is expected that sometimes :tacn:`auto` will + fail even if applying manually one of the hints would succeed. -.. tacv:: auto with {+ @ident} + .. tacv:: auto @num - Uses the hint databases :n:`{+ @ident}` in addition to the database core. + Forces the search depth to be :token:`num`. The maximal search depth + is 5 by default. + + .. tacv:: auto with {+ @ident} + + Uses the hint databases :n:`{+ @ident}` in addition to the database ``core``. + + .. note:: + + Use the fake database `nocore` if you want to *not* use the `core` + database. + + .. tacv:: auto with * + + Uses all existing hint databases. Using this variant is highly discouraged + in finished scripts since it is both slower and less robust than the variant + where the required databases are explicitly listed. .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of pre-defined databases and the way to create or extend a database. -.. tacv:: auto with * + .. tacv:: auto using {+ @ident__i} {? with {+ @ident } } - Uses all existing hint databases. + Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an + inductive type, it is the collection of its constructors which are added + as hints. - .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + .. note:: -.. tacv:: auto using {+ @ident__i} {? with {+ @ident } } + The hints passed through the `using` clause are used in the same + way as if they were passed through a hint database. Consequently, + they use a weaker version of :tacn:`apply` and :n:`auto using @ident` + may fail where :n:`apply @ident` succeeds. - Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an - inductive type, it is the collection of its constructors which are added - as hints. + Given that this can be seen as counter-intuitive, it could be useful + to have an option to use full-blown :tacn:`apply` for lemmas passed + through the `using` clause. Contributions welcome! -.. tacv:: info_auto + .. tacv:: info_auto - Behaves like auto but shows the tactics it uses to solve the goal. This - variant is very useful for getting a better understanding of automation, or - to know what lemmas/assumptions were used. + Behaves like :tacn:`auto` but shows the tactics it uses to solve the goal. This + variant is very useful for getting a better understanding of automation, or + to know what lemmas/assumptions were used. -.. tacv:: debug auto - :name: debug auto + .. tacv:: debug auto + :name: debug auto - Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, - including failing paths. + Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, + including failing paths. -.. tacv:: {? info_}auto {? @num} {? using {+ @lemma}} {? with {+ @ident}} + .. tacv:: {? info_}auto {? @num} {? using {+ @lemma}} {? with {+ @ident}} - This is the most general form, combining the various options. + This is the most general form, combining the various options. .. tacv:: trivial :name: trivial - This tactic is a restriction of auto that is not recursive + This tactic is a restriction of :tacn:`auto` that is not recursive and tries only hints that cost `0`. Typically it solves trivial equalities like :g:`X=X`. -.. tacv:: trivial with {+ @ident} - :undocumented: - -.. tacv:: trivial with * - :undocumented: - -.. tacv:: trivial using {+ @lemma} - :undocumented: - -.. tacv:: debug trivial - :name: debug trivial - :undocumented: - -.. tacv:: info_trivial - :name: info_trivial - :undocumented: - -.. tacv:: {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}} - :undocumented: + .. tacv:: trivial with {+ @ident} + trivial with * + trivial using {+ @lemma} + debug trivial + info_trivial + {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}} + :name: _; _; _; debug trivial; info_trivial; _ + :undocumented: .. note:: - :tacn:`auto` either solves completely the goal or else leaves it - intact. :tacn:`auto` and :tacn:`trivial` never fail. - -The following options enable printing of informative or debug information for -the :tacn:`auto` and :tacn:`trivial` tactics: + :tacn:`auto` and :tacn:`trivial` either solve completely the goal or + else succeed without changing the goal. Use :g:`solve [ auto ]` and + :g:`solve [ trivial ]` if you would prefer these tactics to fail when + they do not manage to solve the goal. .. flag:: Info Auto Debug Auto Info Trivial Debug Trivial - :undocumented: -.. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + These options enable printing of informative or debug information for + the :tacn:`auto` and :tacn:`trivial` tactics. .. tacn:: eauto :name: eauto This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try resolution hints which would leave existential variables in the goal, - :tacn:`eauto` does try them (informally speaking, it usessimple :tacn:`eapply` - where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto` + :tacn:`eauto` does try them (informally speaking, it internally uses a tactic + close to :tacn:`simple eapply` instead of a tactic close to :tacn:`simple apply` + in the case of :tacn:`auto`). As a consequence, :tacn:`eauto` can solve such a goal: .. example:: .. coqtop:: all - Hint Resolve ex_intro. + Hint Resolve ex_intro : core. Goal forall P:nat -> Prop, P 0 -> exists n, P n. eauto. Note that ``ex_intro`` should be declared as a hint. -.. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}} + .. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}} - The various options for :tacn:`eauto` are the same as for :tacn:`auto`. + The various options for :tacn:`eauto` are the same as for :tacn:`auto`. -:tacn:`eauto` also obeys the following options: + :tacn:`eauto` also obeys the following options: -.. flag:: Info Eauto - Debug Eauto - :undocumented: + .. flag:: Info Eauto + Debug Eauto + :undocumented: -.. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` .. tacn:: autounfold with {+ @ident} diff --git a/engine/proofview.ml b/engine/proofview.ml index d4ad53ff5f..a725444e81 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -223,9 +223,9 @@ module Proof = Logical type +'a tactic = 'a Proof.t (** Applies a tactic to the current proofview. *) -let apply env t sp = +let apply ~name ~poly env t sp = let open Logic_monad in - let ans = Proof.repr (Proof.run t false (sp,env)) in + 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) @@ -993,7 +993,10 @@ let tclTIME s t = tclOR (tclUNIT x) (fun e -> aux (n+1) (k e)) in aux 0 t - +let tclProofInfo = + let open Proof in + Logical.current >>= fun P.{name; poly} -> + tclUNIT (name, poly) (** {7 Unsafe primitives} *) @@ -1275,7 +1278,8 @@ module V82 = struct let of_tactic t gls = try let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in - let (_,final,_,_) = apply (goal_env gls.Evd.sigma gls.Evd.it) t init in + let name, poly = Names.Id.of_string "legacy_pe", false in + let (_,final,_,_) = apply ~name ~poly (goal_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 diff --git a/engine/proofview.mli b/engine/proofview.mli index 286703c0dc..680a93f0cc 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -156,10 +156,15 @@ type +'a tactic tactic has given up. In case of multiple success the first one is selected. If there is no success, fails with {!Logic_monad.TacticFailure}*) -val apply : Environ.env -> 'a tactic -> proofview -> 'a - * proofview - * (bool*Evar.t list*Evar.t list) - * Proofview_monad.Info.tree +val apply + : name:Names.Id.t + -> poly:bool + -> Environ.env + -> 'a tactic + -> proofview + -> 'a * proofview + * (bool*Evar.t list*Evar.t list) + * Proofview_monad.Info.tree (** {7 Monadic primitives} *) @@ -407,6 +412,10 @@ val tclTIMEOUT : int -> 'a tactic -> 'a tactic identifying annotation if present *) val tclTIME : string option -> 'a tactic -> 'a tactic +(** Internal, don't use. *) +val tclProofInfo : (Names.Id.t * bool) tactic +[@@ocaml.deprecated "internal, don't use"] + (** {7 Unsafe primitives} *) (** The primitives in the [Unsafe] module should be avoided as much as diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml index 69341d97df..80eb9d0124 100644 --- a/engine/proofview_monad.ml +++ b/engine/proofview_monad.ml @@ -177,7 +177,7 @@ module P = struct type s = proofview * Environ.env (** Recording info trace (true) or not. *) - type e = bool + type e = { trace: bool; name : Names.Id.t; poly : bool } (** Status (safe/unsafe) * shelved goals * given up *) type w = bool * goal list @@ -254,13 +254,16 @@ end (** Lens and utilies pertaining to the info trace *) module InfoL = struct - let recording = Logical.current + let recording = Logical.(map (fun {P.trace} -> trace) current) let if_recording t = let open Logical in recording >>= fun r -> if r then t else return () - let record_trace t = Logical.local true t + let record_trace t = + Logical.( + current >>= fun s -> + local {s with P.trace = true} t) let raw_update = Logical.update let update f = if_recording (raw_update f) diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index a08cab3bf6..3437b6ce77 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -98,7 +98,7 @@ module P : sig val wprod : w -> w -> w (** Recording info trace (true) or not. *) - type e = bool + type e = { trace: bool; name : Names.Id.t; poly : bool } type u = Info.state diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml index 46c2688f05..c396bbab34 100644 --- a/gramlib/gramext.ml +++ b/gramlib/gramext.ml @@ -2,51 +2,6 @@ (* gramext.ml,v *) (* Copyright (c) INRIA 2007-2017 *) -open Printf - -type 'a parser_t = 'a Stream.t -> Obj.t - -type 'te grammar = - { gtokens : (Plexing.pattern, int ref) Hashtbl.t; - glexer : 'te Plexing.lexer } - -type 'te g_entry = - { egram : 'te grammar; - ename : string; - elocal : bool; - mutable estart : int -> 'te parser_t; - mutable econtinue : int -> int -> Obj.t -> 'te parser_t; - mutable edesc : 'te g_desc } -and 'te g_desc = - Dlevels of 'te g_level list - | Dparser of 'te parser_t -and 'te g_level = - { assoc : g_assoc; - lname : string option; - lsuffix : 'te g_tree; - lprefix : 'te g_tree } -and g_assoc = NonA | RightA | LeftA -and 'te g_symbol = - | Snterm of 'te g_entry - | Snterml of 'te g_entry * string - | Slist0 of 'te g_symbol - | Slist0sep of 'te g_symbol * 'te g_symbol * bool - | Slist1 of 'te g_symbol - | Slist1sep of 'te g_symbol * 'te g_symbol * bool - | Sopt of 'te g_symbol - | Sself - | Snext - | Stoken of Plexing.pattern - | Stree of 'te g_tree -and g_action = Obj.t -and 'te g_tree = - Node of 'te g_node - | LocAct of g_action * g_action list - | DeadEnd -and 'te g_node = - { node : 'te g_symbol; son : 'te g_tree; brother : 'te g_tree } -and err_fun = unit -> string - type position = First | Last @@ -54,408 +9,4 @@ type position = | After of string | Level of string -let rec derive_eps = - function - Slist0 _ -> true - | Slist0sep (_, _, _) -> true - | Sopt _ -> true - | Stree t -> tree_derive_eps t - | Slist1 _ | Slist1sep (_, _, _) | Snterm _ | - Snterml (_, _) | Snext | Sself | Stoken _ -> - false -and tree_derive_eps = - function - LocAct (_, _) -> true - | Node {node = s; brother = bro; son = son} -> - derive_eps s && tree_derive_eps son || tree_derive_eps bro - | DeadEnd -> false - -let rec eq_symbol s1 s2 = - match s1, s2 with - Snterm e1, Snterm e2 -> e1 == e2 - | Snterml (e1, l1), Snterml (e2, l2) -> e1 == e2 && l1 = l2 - | Slist0 s1, Slist0 s2 -> eq_symbol s1 s2 - | Slist0sep (s1, sep1, b1), Slist0sep (s2, sep2, b2) -> - eq_symbol s1 s2 && eq_symbol sep1 sep2 && b1 = b2 - | Slist1 s1, Slist1 s2 -> eq_symbol s1 s2 - | Slist1sep (s1, sep1, b1), Slist1sep (s2, sep2, b2) -> - eq_symbol s1 s2 && eq_symbol sep1 sep2 && b1 = b2 - | Sopt s1, Sopt s2 -> eq_symbol s1 s2 - | Stree _, Stree _ -> false - | _ -> s1 = s2 - -let is_before s1 s2 = - match s1, s2 with - Stoken ("ANY", _), _ -> false - | _, Stoken ("ANY", _) -> true - | Stoken (_, s), Stoken (_, "") when s <> "" -> true - | Stoken _, Stoken _ -> false - | Stoken _, _ -> true - | _ -> false - -let insert_tree ~warning entry_name gsymbols action tree = - let rec insert symbols tree = - match symbols with - s :: sl -> insert_in_tree s sl tree - | [] -> - match tree with - Node {node = s; son = son; brother = bro} -> - Node {node = s; son = son; brother = insert [] bro} - | LocAct (old_action, action_list) -> - begin match warning with - | None -> () - | Some warn_fn -> - let msg = - "<W> Grammar extension: " ^ - (if entry_name <> "" then "" else "in ["^entry_name^"%s], ") ^ - "some rule has been masked" in - warn_fn msg - end; - LocAct (action, old_action :: action_list) - | DeadEnd -> LocAct (action, []) - and insert_in_tree s sl tree = - match try_insert s sl tree with - Some t -> t - | None -> Node {node = s; son = insert sl DeadEnd; brother = tree} - and try_insert s sl tree = - match tree with - Node {node = s1; son = son; brother = bro} -> - if eq_symbol s s1 then - let t = Node {node = s1; son = insert sl son; brother = bro} in - Some t - else if is_before s1 s || derive_eps s && not (derive_eps s1) then - let bro = - match try_insert s sl bro with - Some bro -> bro - | None -> Node {node = s; son = insert sl DeadEnd; brother = bro} - in - let t = Node {node = s1; son = son; brother = bro} in Some t - else - begin match try_insert s sl bro with - Some bro -> - let t = Node {node = s1; son = son; brother = bro} in Some t - | None -> None - end - | LocAct (_, _) | DeadEnd -> None - in - insert gsymbols tree - -let srules ~warning rl = - let t = - List.fold_left - (fun tree (symbols, action) -> insert_tree ~warning "" symbols action tree) - DeadEnd rl - in - Stree t - -let is_level_labelled n lev = - match lev.lname with - Some n1 -> n = n1 - | None -> false - -let insert_level ~warning entry_name e1 symbols action slev = - match e1 with - true -> - {assoc = slev.assoc; lname = slev.lname; - lsuffix = insert_tree ~warning entry_name symbols action slev.lsuffix; - lprefix = slev.lprefix} - | false -> - {assoc = slev.assoc; lname = slev.lname; lsuffix = slev.lsuffix; - lprefix = insert_tree ~warning entry_name symbols action slev.lprefix} - -let empty_lev lname assoc = - let assoc = - match assoc with - Some a -> a - | None -> LeftA - in - {assoc = assoc; lname = lname; lsuffix = DeadEnd; lprefix = DeadEnd} - -let change_lev ~warning lev n lname assoc = - let a = - match assoc with - None -> lev.assoc - | Some a -> - if a <> lev.assoc then - begin - match warning with - | None -> () - | Some warn_fn -> - warn_fn ("<W> Changing associativity of level \""^n^"\"") - end; - a - in - begin match lname with - Some n -> - if lname <> lev.lname then - begin match warning with - | None -> () - | Some warn_fn -> - warn_fn ("<W> Level label \""^n^"\" ignored") - end; - | None -> () - end; - {assoc = a; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = lev.lprefix} - -let get_level ~warning entry position levs = - match position with - Some First -> [], empty_lev, levs - | Some Last -> levs, empty_lev, [] - | Some (Level n) -> - let rec get = - function - [] -> - eprintf "No level labelled \"%s\" in entry \"%s\"\n" n - entry.ename; - flush stderr; - failwith "Grammar.extend" - | lev :: levs -> - if is_level_labelled n lev then [], change_lev ~warning lev n, levs - else - let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2 - in - get levs - | Some (Before n) -> - let rec get = - function - [] -> - eprintf "No level labelled \"%s\" in entry \"%s\"\n" n - entry.ename; - flush stderr; - failwith "Grammar.extend" - | lev :: levs -> - if is_level_labelled n lev then [], empty_lev, lev :: levs - else - let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2 - in - get levs - | Some (After n) -> - let rec get = - function - [] -> - eprintf "No level labelled \"%s\" in entry \"%s\"\n" n - entry.ename; - flush stderr; - failwith "Grammar.extend" - | lev :: levs -> - if is_level_labelled n lev then [lev], empty_lev, levs - else - let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2 - in - get levs - | None -> - match levs with - lev :: levs -> [], change_lev ~warning lev "<top>", levs - | [] -> [], empty_lev, [] - -let change_to_self entry = - function - Snterm e when e == entry -> Sself - | x -> x - -let get_initial entry = - function - Sself :: symbols -> true, symbols - | symbols -> false, symbols - -let insert_tokens gram symbols = - let rec insert = - function - | Slist0 s -> insert s - | Slist1 s -> insert s - | Slist0sep (s, t, _) -> insert s; insert t - | Slist1sep (s, t, _) -> insert s; insert t - | Sopt s -> insert s - | Stree t -> tinsert t - | Stoken ("ANY", _) -> () - | Stoken tok -> - gram.glexer.Plexing.tok_using tok; - let r = - try Hashtbl.find gram.gtokens tok with - Not_found -> let r = ref 0 in Hashtbl.add gram.gtokens tok r; r - in - incr r - | Snterm _ | Snterml (_, _) | Snext | Sself -> () - and tinsert = - function - Node {node = s; brother = bro; son = son} -> - insert s; tinsert bro; tinsert son - | LocAct (_, _) | DeadEnd -> () - in - List.iter insert symbols - -let levels_of_rules ~warning entry position rules = - let elev = - match entry.edesc with - Dlevels elev -> elev - | Dparser _ -> - eprintf "Error: entry not extensible: \"%s\"\n" entry.ename; - flush stderr; - failwith "Grammar.extend" - in - if rules = [] then elev - else - let (levs1, make_lev, levs2) = get_level ~warning entry position elev in - let (levs, _) = - List.fold_left - (fun (levs, make_lev) (lname, assoc, level) -> - let lev = make_lev lname assoc in - let lev = - List.fold_left - (fun lev (symbols, action) -> - let symbols = List.map (change_to_self entry) symbols in - let (e1, symbols) = get_initial entry symbols in - insert_tokens entry.egram symbols; - insert_level ~warning entry.ename e1 symbols action lev) - lev level - in - lev :: levs, empty_lev) - ([], make_lev) rules - in - levs1 @ List.rev levs @ levs2 - -let logically_eq_symbols entry = - let rec eq_symbols s1 s2 = - match s1, s2 with - Snterm e1, Snterm e2 -> e1.ename = e2.ename - | Snterm e1, Sself -> e1.ename = entry.ename - | Sself, Snterm e2 -> entry.ename = e2.ename - | Snterml (e1, l1), Snterml (e2, l2) -> e1.ename = e2.ename && l1 = l2 - | Slist0 s1, Slist0 s2 -> eq_symbols s1 s2 - | Slist0sep (s1, sep1, b1), Slist0sep (s2, sep2, b2) -> - eq_symbols s1 s2 && eq_symbols sep1 sep2 && b1 = b2 - | Slist1 s1, Slist1 s2 -> eq_symbols s1 s2 - | Slist1sep (s1, sep1, b1), Slist1sep (s2, sep2, b2) -> - eq_symbols s1 s2 && eq_symbols sep1 sep2 && b1 = b2 - | Sopt s1, Sopt s2 -> eq_symbols s1 s2 - | Stree t1, Stree t2 -> eq_trees t1 t2 - | _ -> s1 = s2 - and eq_trees t1 t2 = - match t1, t2 with - Node n1, Node n2 -> - eq_symbols n1.node n2.node && eq_trees n1.son n2.son && - eq_trees n1.brother n2.brother - | (LocAct (_, _) | DeadEnd), (LocAct (_, _) | DeadEnd) -> true - | _ -> false - in - eq_symbols - -(* [delete_rule_in_tree] returns - [Some (dsl, t)] if success - [dsl] = - Some (list of deleted nodes) if branch deleted - None if action replaced by previous version of action - [t] = remaining tree - [None] if failure *) - -let delete_rule_in_tree entry = - let rec delete_in_tree symbols tree = - match symbols, tree with - s :: sl, Node n -> - if logically_eq_symbols entry s n.node then delete_son sl n - else - begin match delete_in_tree symbols n.brother with - Some (dsl, t) -> - Some (dsl, Node {node = n.node; son = n.son; brother = t}) - | None -> None - end - | s :: sl, _ -> None - | [], Node n -> - begin match delete_in_tree [] n.brother with - Some (dsl, t) -> - Some (dsl, Node {node = n.node; son = n.son; brother = t}) - | None -> None - end - | [], DeadEnd -> None - | [], LocAct (_, []) -> Some (Some [], DeadEnd) - | [], LocAct (_, action :: list) -> Some (None, LocAct (action, list)) - and delete_son sl n = - match delete_in_tree sl n.son with - Some (Some dsl, DeadEnd) -> Some (Some (n.node :: dsl), n.brother) - | Some (Some dsl, t) -> - let t = Node {node = n.node; son = t; brother = n.brother} in - Some (Some (n.node :: dsl), t) - | Some (None, t) -> - let t = Node {node = n.node; son = t; brother = n.brother} in - Some (None, t) - | None -> None - in - delete_in_tree - -let rec decr_keyw_use gram = - function - Stoken tok -> - let r = Hashtbl.find gram.gtokens tok in - decr r; - if !r == 0 then - begin - Hashtbl.remove gram.gtokens tok; - gram.glexer.Plexing.tok_removing tok - end - | Slist0 s -> decr_keyw_use gram s - | Slist1 s -> decr_keyw_use gram s - | Slist0sep (s1, s2, _) -> decr_keyw_use gram s1; decr_keyw_use gram s2 - | Slist1sep (s1, s2, _) -> decr_keyw_use gram s1; decr_keyw_use gram s2 - | Sopt s -> decr_keyw_use gram s - | Stree t -> decr_keyw_use_in_tree gram t - | Sself | Snext | Snterm _ | Snterml (_, _) -> () -and decr_keyw_use_in_tree gram = - function - DeadEnd | LocAct (_, _) -> () - | Node n -> - decr_keyw_use gram n.node; - decr_keyw_use_in_tree gram n.son; - decr_keyw_use_in_tree gram n.brother - -let rec delete_rule_in_suffix entry symbols = - function - lev :: levs -> - begin match delete_rule_in_tree entry symbols lev.lsuffix with - Some (dsl, t) -> - begin match dsl with - Some dsl -> List.iter (decr_keyw_use entry.egram) dsl - | None -> () - end; - begin match t with - DeadEnd when lev.lprefix == DeadEnd -> levs - | _ -> - let lev = - {assoc = lev.assoc; lname = lev.lname; lsuffix = t; - lprefix = lev.lprefix} - in - lev :: levs - end - | None -> - let levs = delete_rule_in_suffix entry symbols levs in lev :: levs - end - | [] -> raise Not_found - -let rec delete_rule_in_prefix entry symbols = - function - lev :: levs -> - begin match delete_rule_in_tree entry symbols lev.lprefix with - Some (dsl, t) -> - begin match dsl with - Some dsl -> List.iter (decr_keyw_use entry.egram) dsl - | None -> () - end; - begin match t with - DeadEnd when lev.lsuffix == DeadEnd -> levs - | _ -> - let lev = - {assoc = lev.assoc; lname = lev.lname; lsuffix = lev.lsuffix; - lprefix = t} - in - lev :: levs - end - | None -> - let levs = delete_rule_in_prefix entry symbols levs in lev :: levs - end - | [] -> raise Not_found - -let delete_rule_in_level_list entry symbols levs = - match symbols with - Sself :: symbols -> delete_rule_in_suffix entry symbols levs - | Snterm e :: symbols when e == entry -> - delete_rule_in_suffix entry symbols levs - | _ -> delete_rule_in_prefix entry symbols levs +type g_assoc = NonA | RightA | LeftA diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli index f1e294fb4c..f9daf5bf10 100644 --- a/gramlib/gramext.mli +++ b/gramlib/gramext.mli @@ -2,49 +2,6 @@ (* gramext.mli,v *) (* Copyright (c) INRIA 2007-2017 *) -type 'a parser_t = 'a Stream.t -> Obj.t - -type 'te grammar = - { gtokens : (Plexing.pattern, int ref) Hashtbl.t; - glexer : 'te Plexing.lexer } - -type 'te g_entry = - { egram : 'te grammar; - ename : string; - elocal : bool; - mutable estart : int -> 'te parser_t; - mutable econtinue : int -> int -> Obj.t -> 'te parser_t; - mutable edesc : 'te g_desc } -and 'te g_desc = - Dlevels of 'te g_level list - | Dparser of 'te parser_t -and 'te g_level = - { assoc : g_assoc; - lname : string option; - lsuffix : 'te g_tree; - lprefix : 'te g_tree } -and g_assoc = NonA | RightA | LeftA -and 'te g_symbol = - | Snterm of 'te g_entry - | Snterml of 'te g_entry * string - | Slist0 of 'te g_symbol - | Slist0sep of 'te g_symbol * 'te g_symbol * bool - | Slist1 of 'te g_symbol - | Slist1sep of 'te g_symbol * 'te g_symbol * bool - | Sopt of 'te g_symbol - | Sself - | Snext - | Stoken of Plexing.pattern - | Stree of 'te g_tree -and g_action = Obj.t -and 'te g_tree = - Node of 'te g_node - | LocAct of g_action * g_action list - | DeadEnd -and 'te g_node = - { node : 'te g_symbol; son : 'te g_tree; brother : 'te g_tree } -and err_fun = unit -> string - type position = First | Last @@ -52,14 +9,4 @@ type position = | After of string | Level of string -val levels_of_rules : warning:(string -> unit) option -> - 'te g_entry -> position option -> - (string option * g_assoc option * ('te g_symbol list * g_action) list) - list -> - 'te g_level list - -val srules : warning:(string -> unit) option -> ('te g_symbol list * g_action) list -> 'te g_symbol -val eq_symbol : 'a g_symbol -> 'a g_symbol -> bool - -val delete_rule_in_level_list : - 'te g_entry -> 'te g_symbol list -> 'te g_level list -> 'te g_level list +type g_assoc = NonA | RightA | LeftA diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index e959e9b9e6..e313f2e648 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -5,14 +5,644 @@ open Gramext open Format -external gramext_action : 'a -> g_action = "%identity" +type ('a, 'b) eq = Refl : ('a, 'a) eq -let rec flatten_tree = +(* Functorial interface *) + +module type GLexerType = sig type te val lexer : te Plexing.lexer end + +module type S = + sig + type te + type parsable + val parsable : char Stream.t -> parsable + val tokens : string -> (string * int) list + module Entry : + sig + type 'a e + val create : string -> 'a e + val parse : 'a e -> parsable -> 'a + val name : 'a e -> string + val of_parser : string -> (te Stream.t -> 'a) -> 'a e + val parse_token_stream : 'a e -> te Stream.t -> 'a + val print : Format.formatter -> 'a e -> unit + end + type ('self, 'a) ty_symbol + type ('self, 'f, 'r) ty_rule + type 'a ty_production + val s_nterm : 'a Entry.e -> ('self, 'a) ty_symbol + val s_nterml : 'a Entry.e -> string -> ('self, 'a) ty_symbol + val s_list0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol + val s_list0sep : + ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool -> + ('self, 'a list) ty_symbol + val s_list1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol + val s_list1sep : + ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool -> + ('self, 'a list) ty_symbol + val s_opt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol + val s_self : ('self, 'self) ty_symbol + val s_next : ('self, 'self) ty_symbol + val s_token : Plexing.pattern -> ('self, string) ty_symbol + val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol + val r_stop : ('self, 'r, 'r) ty_rule + val r_next : + ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol -> + ('self, 'b -> 'a, 'r) ty_rule + val production : ('a, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production + module Unsafe : + sig + val clear_entry : 'a Entry.e -> unit + end + val safe_extend : warning:(string -> unit) option -> + 'a Entry.e -> Gramext.position option -> + (string option * Gramext.g_assoc option * 'a ty_production list) + list -> + unit + val safe_delete_rule : 'a Entry.e -> ('a, 'r, 'f) ty_rule -> unit + end + +(* Implementation *) + +module GMake (L : GLexerType) = +struct + +type te = L.te + +type 'a parser_t = L.te Stream.t -> 'a + +type grammar = + { gtokens : (Plexing.pattern, int ref) Hashtbl.t; + glexer : L.te Plexing.lexer } + +let egram = + {gtokens = Hashtbl.create 301; glexer = L.lexer } + +let tokens con = + let list = ref [] in + Hashtbl.iter + (fun (p_con, p_prm) c -> if p_con = con then list := (p_prm, !c) :: !list) + egram.gtokens; + !list + +type 'a ty_entry = { + ename : string; + mutable estart : int -> 'a parser_t; + mutable econtinue : int -> int -> 'a -> 'a parser_t; + mutable edesc : 'a ty_desc; +} + +and 'a ty_desc = +| Dlevels of 'a ty_level list +| Dparser of 'a parser_t + +and 'a ty_level = { + assoc : g_assoc; + lname : string option; + lsuffix : ('a, 'a -> Loc.t -> 'a) ty_tree; + lprefix : ('a, Loc.t -> 'a) ty_tree; +} + +and ('self, 'a) ty_symbol = +| Stoken : Plexing.pattern -> ('self, string) ty_symbol +| Slist1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol +| Slist1sep : ('self, 'a) ty_symbol * ('self, _) ty_symbol * bool -> ('self, 'a list) ty_symbol +| Slist0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol +| Slist0sep : ('self, 'a) ty_symbol * ('self, _) ty_symbol * bool -> ('self, 'a list) ty_symbol +| Sopt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol +| Sself : ('self, 'self) ty_symbol +| Snext : ('self, 'self) ty_symbol +| Snterm : 'a ty_entry -> ('self, 'a) ty_symbol +| Snterml : 'a ty_entry * string -> ('self, 'a) ty_symbol +| Stree : ('self, Loc.t -> 'a) ty_tree -> ('self, 'a) ty_symbol + +and ('self, _, 'r) ty_rule = +| TStop : ('self, 'r, 'r) ty_rule +| TNext : ('self, 'a, 'r) ty_rule * ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule + +and ('self, 'a) ty_tree = +| Node : ('self, 'b, 'a) ty_node -> ('self, 'a) ty_tree +| LocAct : 'k * 'k list -> ('self, 'k) ty_tree +| DeadEnd : ('self, 'k) ty_tree + +and ('self, 'a, 'r) ty_node = { + node : ('self, 'a) ty_symbol; + son : ('self, 'a -> 'r) ty_tree; + brother : ('self, 'r) ty_tree; +} + +type 'a ty_production = +| TProd : ('a, 'act, Loc.t -> 'a) ty_rule * 'act -> 'a ty_production + +let rec derive_eps : type s a. (s, a) ty_symbol -> bool = + function + Slist0 _ -> true + | Slist0sep (_, _, _) -> true + | Sopt _ -> true + | Stree t -> tree_derive_eps t + | Slist1 _ -> false + | Slist1sep (_, _, _) -> false + | Snterm _ | Snterml (_, _) -> false + | Snext -> false + | Sself -> false + | Stoken _ -> false +and tree_derive_eps : type s a. (s, a) ty_tree -> bool = + function + LocAct (_, _) -> true + | Node {node = s; brother = bro; son = son} -> + derive_eps s && tree_derive_eps son || tree_derive_eps bro + | DeadEnd -> false + +(** FIXME: find a way to do that type-safely *) +let eq_entry : type a1 a2. a1 ty_entry -> a2 ty_entry -> (a1, a2) eq option = fun e1 e2 -> + if (Obj.magic e1) == (Obj.magic e2) then Some (Obj.magic Refl) + else None + +let rec eq_symbol : type s a1 a2. (s, a1) ty_symbol -> (s, a2) ty_symbol -> (a1, a2) eq option = fun s1 s2 -> + match s1, s2 with + Snterm e1, Snterm e2 -> eq_entry e1 e2 + | Snterml (e1, l1), Snterml (e2, l2) -> + if String.equal l1 l2 then eq_entry e1 e2 else None + | Slist0 s1, Slist0 s2 -> + begin match eq_symbol s1 s2 with None -> None | Some Refl -> Some Refl end + | Slist0sep (s1, sep1, b1), Slist0sep (s2, sep2, b2) -> + if b1 = b2 then match eq_symbol s1 s2 with + | None -> None + | Some Refl -> + match eq_symbol sep1 sep2 with + | None -> None + | Some Refl -> Some Refl + else None + | Slist1 s1, Slist1 s2 -> + begin match eq_symbol s1 s2 with None -> None | Some Refl -> Some Refl end + | Slist1sep (s1, sep1, b1), Slist1sep (s2, sep2, b2) -> + if b1 = b2 then match eq_symbol s1 s2 with + | None -> None + | Some Refl -> + match eq_symbol sep1 sep2 with + | None -> None + | Some Refl -> Some Refl + else None + | Sopt s1, Sopt s2 -> + begin match eq_symbol s1 s2 with None -> None | Some Refl -> Some Refl end + | Stree _, Stree _ -> None + | Sself, Sself -> Some Refl + | Snext, Snext -> Some Refl + | Stoken p1, Stoken p2 -> if p1 = p2 then Some Refl else None + | _ -> None + +let is_before : type s1 s2 a1 a2. (s1, a1) ty_symbol -> (s2, a2) ty_symbol -> bool = fun s1 s2 -> + match s1, s2 with + Stoken ("ANY", _), _ -> false + | _, Stoken ("ANY", _) -> true + | Stoken (_, s), Stoken (_, "") when s <> "" -> true + | Stoken _, Stoken _ -> false + | Stoken _, _ -> true + | _ -> false + +(** Ancilliary datatypes *) + +type ('self, _) ty_symbols = +| TNil : ('self, unit) ty_symbols +| TCns : ('self, 'a) ty_symbol * ('self, 'b) ty_symbols -> ('self, 'a * 'b) ty_symbols + +(** ('i, 'p, 'f, 'r) rel_prod0 ~ + ∃ α₁ ... αₙ. + p ≡ αₙ * ... α₁ * 'i ∧ + f ≡ α₁ -> ... -> αₙ -> 'r +*) +type ('i, _, 'f, _) rel_prod0 = +| Rel0 : ('i, 'i, 'f, 'f) rel_prod0 +| RelS : ('i, 'p, 'f, 'a -> 'r) rel_prod0 -> ('i, 'a * 'p, 'f, 'r) rel_prod0 + +type ('p, 'k, 'r) rel_prod = (unit, 'p, 'k, 'r) rel_prod0 + +type ('s, 'i, 'k, 'r) any_symbols = +| AnyS : ('s, 'p) ty_symbols * ('i, 'p, 'k, 'r) rel_prod0 -> ('s, 'i, 'k, 'r) any_symbols + +(** FIXME *) +let rec symbols : type s p k r. (s, p) ty_symbols -> (s, k, r) ty_rule -> (s, unit, k, r) any_symbols = + fun accu r -> match r with + | TStop -> AnyS (Obj.magic accu, Rel0) + | TNext (r, s) -> + let AnyS (r, pf) = symbols (TCns (s, accu)) r in + AnyS (Obj.magic r, RelS (Obj.magic pf)) + +let get_symbols : type s k r. (s, k, r) ty_rule -> (s, unit, k, r) any_symbols = + fun r -> symbols TNil r + +let insert_tree (type s p k a) ~warning entry_name (gsymbols : (s, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, a) ty_tree) = + let rec insert : type p f k. (s, p) ty_symbols -> (p, k, f) rel_prod -> (s, f) ty_tree -> k -> (s, f) ty_tree = + fun symbols pf tree action -> + match symbols, pf with + TCns (s, sl), RelS pf -> insert_in_tree s sl pf tree action + | TNil, Rel0 -> + match tree with + Node {node = s; son = son; brother = bro} -> + Node {node = s; son = son; brother = insert TNil Rel0 bro action} + | LocAct (old_action, action_list) -> + begin match warning with + | None -> () + | Some warn_fn -> + let msg = + "<W> Grammar extension: " ^ + (if entry_name <> "" then "" else "in ["^entry_name^"%s], ") ^ + "some rule has been masked" in + warn_fn msg + end; + LocAct (action, old_action :: action_list) + | DeadEnd -> LocAct (action, []) + and insert_in_tree : type a p f k. (s, a) ty_symbol -> (s, p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, f) ty_tree -> k -> (s, f) ty_tree = + fun s sl pf tree action -> + match try_insert s sl pf tree action with + Some t -> t + | None -> Node {node = s; son = insert sl pf DeadEnd action; brother = tree} + and try_insert : type a p f k. (s, a) ty_symbol -> (s, p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, f) ty_tree -> k -> (s, f) ty_tree option = + fun s sl pf tree action -> + match tree with + Node {node = s1; son = son; brother = bro} -> + begin match eq_symbol s s1 with + | Some Refl -> + let t = Node {node = s1; son = insert sl pf son action; brother = bro} in + Some t + | None -> + if is_before s1 s || derive_eps s && not (derive_eps s1) then + let bro = + match try_insert s sl pf bro action with + Some bro -> bro + | None -> Node {node = s; son = insert sl pf DeadEnd action; brother = bro} + in + let t = Node {node = s1; son = son; brother = bro} in Some t + else + begin match try_insert s sl pf bro action with + Some bro -> + let t = Node {node = s1; son = son; brother = bro} in Some t + | None -> None + end + end + | LocAct (_, _) | DeadEnd -> None + in + insert gsymbols pf tree action + +let srules (type self a) ~warning (rl : a ty_production list) = + let t = + List.fold_left + (fun tree (TProd (symbols, action)) -> + let AnyS (symbols, pf) = get_symbols symbols in + insert_tree ~warning "" symbols pf action tree) + DeadEnd rl + in + (* FIXME: use an universal self type to ensure well-typedness *) + (Obj.magic (Stree t) : (self, a) ty_symbol) + +let is_level_labelled n lev = + match lev.lname with + Some n1 -> n = n1 + | None -> false + +let insert_level (type s p k) ~warning entry_name (symbols : (s, p) ty_symbols) (pf : (p, k, Loc.t -> s) rel_prod) (action : k) (slev : s ty_level) : s ty_level = + match symbols with + | TCns (Sself, symbols) -> + let RelS pf = pf in + {assoc = slev.assoc; lname = slev.lname; + lsuffix = insert_tree ~warning entry_name symbols pf action slev.lsuffix; + lprefix = slev.lprefix} + | _ -> + {assoc = slev.assoc; lname = slev.lname; lsuffix = slev.lsuffix; + lprefix = insert_tree ~warning entry_name symbols pf action slev.lprefix} + +let empty_lev lname assoc = + let assoc = + match assoc with + Some a -> a + | None -> LeftA + in + {assoc = assoc; lname = lname; lsuffix = DeadEnd; lprefix = DeadEnd} + +let change_lev ~warning lev n lname assoc = + let a = + match assoc with + None -> lev.assoc + | Some a -> + if a <> lev.assoc then + begin + match warning with + | None -> () + | Some warn_fn -> + warn_fn ("<W> Changing associativity of level \""^n^"\"") + end; + a + in + begin match lname with + Some n -> + if lname <> lev.lname then + begin match warning with + | None -> () + | Some warn_fn -> + warn_fn ("<W> Level label \""^n^"\" ignored") + end; + | None -> () + end; + {assoc = a; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = lev.lprefix} + +let get_level ~warning entry position levs = + match position with + Some First -> [], empty_lev, levs + | Some Last -> levs, empty_lev, [] + | Some (Level n) -> + let rec get = + function + [] -> + eprintf "No level labelled \"%s\" in entry \"%s\"\n" n + entry.ename; + flush stderr; + failwith "Grammar.extend" + | lev :: levs -> + if is_level_labelled n lev then [], change_lev ~warning lev n, levs + else + let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2 + in + get levs + | Some (Before n) -> + let rec get = + function + [] -> + eprintf "No level labelled \"%s\" in entry \"%s\"\n" n + entry.ename; + flush stderr; + failwith "Grammar.extend" + | lev :: levs -> + if is_level_labelled n lev then [], empty_lev, lev :: levs + else + let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2 + in + get levs + | Some (After n) -> + let rec get = + function + [] -> + eprintf "No level labelled \"%s\" in entry \"%s\"\n" n + entry.ename; + flush stderr; + failwith "Grammar.extend" + | lev :: levs -> + if is_level_labelled n lev then [lev], empty_lev, levs + else + let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2 + in + get levs + | None -> + match levs with + lev :: levs -> [], change_lev ~warning lev "<top>", levs + | [] -> [], empty_lev, [] + +let change_to_self0 (type s) (type a) (entry : s ty_entry) : (s, a) ty_symbol -> (s, a) ty_symbol = + function + | Snterm e -> + begin match eq_entry e entry with + | None -> Snterm e + | Some Refl -> Sself + end + | x -> x + +let rec change_to_self : type s a r. s ty_entry -> (s, a, r) ty_rule -> (s, a, r) ty_rule = fun e r -> match r with +| TStop -> TStop +| TNext (r, t) -> TNext (change_to_self e r, change_to_self0 e t) + +let insert_tokens gram symbols = + let rec insert : type s a. (s, a) ty_symbol -> unit = + function + | Slist0 s -> insert s + | Slist1 s -> insert s + | Slist0sep (s, t, _) -> insert s; insert t + | Slist1sep (s, t, _) -> insert s; insert t + | Sopt s -> insert s + | Stree t -> tinsert t + | Stoken ("ANY", _) -> () + | Stoken tok -> + gram.glexer.Plexing.tok_using tok; + let r = + try Hashtbl.find gram.gtokens tok with + Not_found -> let r = ref 0 in Hashtbl.add gram.gtokens tok r; r + in + incr r + | Snterm _ | Snterml (_, _) -> () + | Snext -> () + | Sself -> () + and tinsert : type s a. (s, a) ty_tree -> unit = + function + Node {node = s; brother = bro; son = son} -> + insert s; tinsert bro; tinsert son + | LocAct (_, _) | DeadEnd -> () + and linsert : type s p. (s, p) ty_symbols -> unit = function + | TNil -> () + | TCns (s, r) -> insert s; linsert r + in + linsert symbols + +let levels_of_rules ~warning entry position rules = + let elev = + match entry.edesc with + Dlevels elev -> elev + | Dparser _ -> + eprintf "Error: entry not extensible: \"%s\"\n" entry.ename; + flush stderr; + failwith "Grammar.extend" + in + match rules with + | [] -> elev + | _ -> + let (levs1, make_lev, levs2) = get_level ~warning entry position elev in + let (levs, _) = + List.fold_left + (fun (levs, make_lev) (lname, assoc, level) -> + let lev = make_lev lname assoc in + let lev = + List.fold_left + (fun lev (TProd (symbols, action)) -> + let symbols = change_to_self entry symbols in + let AnyS (symbols, pf) = get_symbols symbols in + insert_tokens egram symbols; + insert_level ~warning entry.ename symbols pf action lev) + lev level + in + lev :: levs, empty_lev) + ([], make_lev) rules + in + levs1 @ List.rev levs @ levs2 + +let logically_eq_symbols entry = + let rec eq_symbols : type s1 s2 a1 a2. (s1, a1) ty_symbol -> (s2, a2) ty_symbol -> bool = fun s1 s2 -> + match s1, s2 with + Snterm e1, Snterm e2 -> e1.ename = e2.ename + | Snterm e1, Sself -> e1.ename = entry.ename + | Sself, Snterm e2 -> entry.ename = e2.ename + | Snterml (e1, l1), Snterml (e2, l2) -> e1.ename = e2.ename && l1 = l2 + | Slist0 s1, Slist0 s2 -> eq_symbols s1 s2 + | Slist0sep (s1, sep1, b1), Slist0sep (s2, sep2, b2) -> + eq_symbols s1 s2 && eq_symbols sep1 sep2 && b1 = b2 + | Slist1 s1, Slist1 s2 -> eq_symbols s1 s2 + | Slist1sep (s1, sep1, b1), Slist1sep (s2, sep2, b2) -> + eq_symbols s1 s2 && eq_symbols sep1 sep2 && b1 = b2 + | Sopt s1, Sopt s2 -> eq_symbols s1 s2 + | Stree t1, Stree t2 -> eq_trees t1 t2 + | Stoken p1, Stoken p2 -> p1 = p2 + | Sself, Sself -> true + | Snext, Snext -> true + | _ -> false + and eq_trees : type s1 s2 a1 a2. (s1, a1) ty_tree -> (s2, a2) ty_tree -> bool = fun t1 t2 -> + match t1, t2 with + Node n1, Node n2 -> + eq_symbols n1.node n2.node && eq_trees n1.son n2.son && + eq_trees n1.brother n2.brother + | (LocAct (_, _) | DeadEnd), (LocAct (_, _) | DeadEnd) -> true + | _ -> false + in + eq_symbols + +(* [delete_rule_in_tree] returns + [Some (dsl, t)] if success + [dsl] = + Some (list of deleted nodes) if branch deleted + None if action replaced by previous version of action + [t] = remaining tree + [None] if failure *) + +type 's ex_symbols = +| ExS : ('s, 'p) ty_symbols -> 's ex_symbols + +let delete_rule_in_tree entry = + let rec delete_in_tree : + type s p r. (s, p) ty_symbols -> (s, r) ty_tree -> (s ex_symbols option * (s, r) ty_tree) option = + fun symbols tree -> + match symbols, tree with + | TCns (s, sl), Node n -> + if logically_eq_symbols entry s n.node then delete_son sl n + else + begin match delete_in_tree symbols n.brother with + Some (dsl, t) -> + Some (dsl, Node {node = n.node; son = n.son; brother = t}) + | None -> None + end + | TCns (s, sl), _ -> None + | TNil, Node n -> + begin match delete_in_tree TNil n.brother with + Some (dsl, t) -> + Some (dsl, Node {node = n.node; son = n.son; brother = t}) + | None -> None + end + | TNil, DeadEnd -> None + | TNil, LocAct (_, []) -> Some (Some (ExS TNil), DeadEnd) + | TNil, LocAct (_, action :: list) -> Some (None, LocAct (action, list)) + and delete_son : + type s p a r. (s, p) ty_symbols -> (s, a, r) ty_node -> (s ex_symbols option * (s, r) ty_tree) option = + fun sl n -> + match delete_in_tree sl n.son with + Some (Some (ExS dsl), DeadEnd) -> Some (Some (ExS (TCns (n.node, dsl))), n.brother) + | Some (Some (ExS dsl), t) -> + let t = Node {node = n.node; son = t; brother = n.brother} in + Some (Some (ExS (TCns (n.node, dsl))), t) + | Some (None, t) -> + let t = Node {node = n.node; son = t; brother = n.brother} in + Some (None, t) + | None -> None + in + delete_in_tree + +let rec decr_keyw_use : type s a. _ -> (s, a) ty_symbol -> unit = fun gram -> + function + Stoken tok -> + let r = Hashtbl.find gram.gtokens tok in + decr r; + if !r == 0 then + begin + Hashtbl.remove gram.gtokens tok; + gram.glexer.Plexing.tok_removing tok + end + | Slist0 s -> decr_keyw_use gram s + | Slist1 s -> decr_keyw_use gram s + | Slist0sep (s1, s2, _) -> decr_keyw_use gram s1; decr_keyw_use gram s2 + | Slist1sep (s1, s2, _) -> decr_keyw_use gram s1; decr_keyw_use gram s2 + | Sopt s -> decr_keyw_use gram s + | Stree t -> decr_keyw_use_in_tree gram t + | Sself -> () + | Snext -> () + | Snterm _ | Snterml (_, _) -> () +and decr_keyw_use_in_tree : type s a. _ -> (s, a) ty_tree -> unit = fun gram -> + function + DeadEnd | LocAct (_, _) -> () + | Node n -> + decr_keyw_use gram n.node; + decr_keyw_use_in_tree gram n.son; + decr_keyw_use_in_tree gram n.brother +and decr_keyw_use_in_list : type s p. _ -> (s, p) ty_symbols -> unit = fun gram -> + function + | TNil -> () + | TCns (s, l) -> decr_keyw_use gram s; decr_keyw_use_in_list gram l + +let rec delete_rule_in_suffix entry symbols = + function + lev :: levs -> + begin match delete_rule_in_tree entry symbols lev.lsuffix with + Some (dsl, t) -> + begin match dsl with + Some (ExS dsl) -> decr_keyw_use_in_list egram dsl + | None -> () + end; + begin match t with + DeadEnd when lev.lprefix == DeadEnd -> levs + | _ -> + let lev = + {assoc = lev.assoc; lname = lev.lname; lsuffix = t; + lprefix = lev.lprefix} + in + lev :: levs + end + | None -> + let levs = delete_rule_in_suffix entry symbols levs in lev :: levs + end + | [] -> raise Not_found + +let rec delete_rule_in_prefix entry symbols = + function + lev :: levs -> + begin match delete_rule_in_tree entry symbols lev.lprefix with + Some (dsl, t) -> + begin match dsl with + Some (ExS dsl) -> decr_keyw_use_in_list egram dsl + | None -> () + end; + begin match t with + DeadEnd when lev.lsuffix == DeadEnd -> levs + | _ -> + let lev = + {assoc = lev.assoc; lname = lev.lname; lsuffix = lev.lsuffix; + lprefix = t} + in + lev :: levs + end + | None -> + let levs = delete_rule_in_prefix entry symbols levs in lev :: levs + end + | [] -> raise Not_found + +let delete_rule_in_level_list (type s p) (entry : s ty_entry) (symbols : (s, p) ty_symbols) levs = + match symbols with + TCns (Sself, symbols) -> delete_rule_in_suffix entry symbols levs + | TCns (Snterm e, symbols') -> + begin match eq_entry e entry with + | None -> delete_rule_in_prefix entry symbols levs + | Some Refl -> + delete_rule_in_suffix entry symbols' levs + end + | _ -> delete_rule_in_prefix entry symbols levs + +let rec flatten_tree : type s a. (s, a) ty_tree -> s ex_symbols list = function DeadEnd -> [] - | LocAct (_, _) -> [[]] + | LocAct (_, _) -> [ExS TNil] | Node {node = n; brother = b; son = s} -> - List.map (fun l -> n :: l) (flatten_tree s) @ flatten_tree b + List.map (fun (ExS l) -> ExS (TCns (n, l))) (flatten_tree s) @ flatten_tree b let utf8_print = ref true @@ -41,7 +671,8 @@ let string_escaped s = let print_str ppf s = fprintf ppf "\"%s\"" (string_escaped s) -let rec print_symbol ppf = +let rec print_symbol : type s r. formatter -> (s, r) ty_symbol -> unit = + fun ppf -> function | Slist0 s -> fprintf ppf "LIST0 %a" print_symbol1 s | Slist0sep (s, t, osep) -> @@ -55,36 +686,38 @@ let rec print_symbol ppf = | Stoken (con, prm) when con <> "" && prm <> "" -> fprintf ppf "%s@ %a" con print_str prm | Snterml (e, l) -> - fprintf ppf "%s%s@ LEVEL@ %a" e.ename (if e.elocal then "*" else "") + fprintf ppf "%s%s@ LEVEL@ %a" e.ename "" print_str l - | Snterm _ | Snext | Sself | Stoken _ | Stree _ as s -> - print_symbol1 ppf s -and print_symbol1 ppf = + | s -> print_symbol1 ppf s +and print_symbol1 : type s r. formatter -> (s, r) ty_symbol -> unit = + fun ppf -> function - | Snterm e -> fprintf ppf "%s%s" e.ename (if e.elocal then "*" else "") + | Snterm e -> fprintf ppf "%s%s" e.ename "" | Sself -> pp_print_string ppf "SELF" | Snext -> pp_print_string ppf "NEXT" | Stoken ("", s) -> print_str ppf s | Stoken (con, "") -> pp_print_string ppf con | Stree t -> print_level ppf pp_print_space (flatten_tree t) - | Snterml (_, _) | Slist0 _ | Slist0sep (_, _, _) | - Slist1 _ | Slist1sep (_, _, _) | Sopt _ | Stoken _ as s -> + | s -> fprintf ppf "(%a)" print_symbol s -and print_rule ppf symbols = +and print_rule : type s p. formatter -> (s, p) ty_symbols -> unit = + fun ppf symbols -> fprintf ppf "@[<hov 0>"; - let _ = - List.fold_left - (fun sep symbol -> - fprintf ppf "%t%a" sep print_symbol symbol; - fun ppf -> fprintf ppf ";@ ") - (fun ppf -> ()) symbols + let rec fold : type s p. _ -> (s, p) ty_symbols -> unit = + fun sep symbols -> match symbols with + | TNil -> () + | TCns (symbol, symbols) -> + fprintf ppf "%t%a" sep print_symbol symbol; + fold (fun ppf -> fprintf ppf ";@ ") symbols in + let () = fold (fun ppf -> ()) symbols in fprintf ppf "@]" -and print_level ppf pp_print_space rules = +and print_level : type s. _ -> _ -> s ex_symbols list -> _ = + fun ppf pp_print_space rules -> fprintf ppf "@[<hov 0>[ "; let _ = List.fold_left - (fun sep rule -> + (fun sep (ExS rule) -> fprintf ppf "%t%a" sep print_rule rule; fun ppf -> fprintf ppf "%a| " pp_print_space ()) (fun ppf -> ()) rules @@ -96,7 +729,7 @@ let print_levels ppf elev = List.fold_left (fun sep lev -> let rules = - List.map (fun t -> Sself :: t) (flatten_tree lev.lsuffix) @ + List.map (fun (ExS t) -> ExS (TCns (Sself, t))) (flatten_tree lev.lsuffix) @ flatten_tree lev.lprefix in fprintf ppf "%t@[<hov 2>" sep; @@ -132,21 +765,32 @@ let loc_of_token_interval bp ep = else let loc1 = !floc bp in let loc2 = !floc (pred ep) in Loc.merge loc1 loc2 -let name_of_symbol entry = +let name_of_symbol : type s a. s ty_entry -> (s, a) ty_symbol -> string = + fun entry -> function Snterm e -> "[" ^ e.ename ^ "]" | Snterml (e, l) -> "[" ^ e.ename ^ " level " ^ l ^ "]" - | Sself | Snext -> "[" ^ entry.ename ^ "]" - | Stoken tok -> entry.egram.glexer.Plexing.tok_text tok + | Sself -> "[" ^ entry.ename ^ "]" + | Snext -> "[" ^ entry.ename ^ "]" + | Stoken tok -> egram.glexer.Plexing.tok_text tok | _ -> "???" -let rec get_token_list entry rev_tokl last_tok tree = +type ('r, 'f) tok_list = +| TokNil : ('f, 'f) tok_list +| TokCns : ('r, 'f) tok_list -> (string -> 'r, 'f) tok_list + +type ('s, 'f) tok_tree = TokTree : ('s, string -> 'r) ty_tree * ('r, 'f) tok_list -> ('s, 'f) tok_tree + +let rec get_token_list : type s r f. + s ty_entry -> _ -> _ -> _ -> (r, f) tok_list -> (s, string -> r) ty_tree -> (_ * _ * _ * (s, f) tok_tree) option = + fun entry first_tok rev_tokl last_tok pf tree -> match tree with Node {node = Stoken tok; son = son; brother = DeadEnd} -> - get_token_list entry (last_tok :: rev_tokl) tok son - | _ -> if rev_tokl = [] then None else Some (rev_tokl, last_tok, tree) + get_token_list entry first_tok (last_tok :: rev_tokl) tok (TokCns pf) son + | _ -> if rev_tokl = [] then None else Some (first_tok, rev_tokl, last_tok, TokTree (tree, pf)) -let rec name_of_symbol_failed entry = +let rec name_of_symbol_failed : type s a. s ty_entry -> (s, a) ty_symbol -> _ = + fun entry -> function | Slist0 s -> name_of_symbol_failed entry s | Slist0sep (s, _, _) -> name_of_symbol_failed entry s @@ -155,12 +799,13 @@ let rec name_of_symbol_failed entry = | Sopt s -> name_of_symbol_failed entry s | Stree t -> name_of_tree_failed entry t | s -> name_of_symbol entry s -and name_of_tree_failed entry = +and name_of_tree_failed : type s a. s ty_entry -> (s, a) ty_tree -> _ = + fun entry -> function Node {node = s; brother = bro; son = son} -> let tokl = match s with - Stoken tok -> get_token_list entry [] tok son + Stoken tok -> get_token_list entry tok [] tok TokNil son | _ -> None in begin match tokl with @@ -177,16 +822,16 @@ and name_of_tree_failed entry = | Node _ -> txt ^ " or " ^ name_of_tree_failed entry bro in txt - | Some (rev_tokl, last_tok, son) -> + | Some (_, rev_tokl, last_tok, _) -> List.fold_left (fun s tok -> (if s = "" then "" else s ^ " ") ^ - entry.egram.glexer.Plexing.tok_text tok) + egram.glexer.Plexing.tok_text tok) "" (List.rev (last_tok :: rev_tokl)) end | DeadEnd | LocAct (_, _) -> "???" -let tree_failed entry prev_symb_result prev_symb tree = +let tree_failed (type s a) (entry : s ty_entry) (prev_symb_result : a) (prev_symb : (s, a) ty_symbol) tree = let txt = name_of_tree_failed entry tree in let txt = match prev_symb with @@ -197,7 +842,7 @@ let tree_failed entry prev_symb_result prev_symb tree = let txt1 = name_of_symbol_failed entry s in txt1 ^ " or " ^ txt ^ " expected" | Slist0sep (s, sep, _) -> - begin match Obj.magic prev_symb_result with + begin match prev_symb_result with [] -> let txt1 = name_of_symbol_failed entry s in txt1 ^ " or " ^ txt ^ " expected" @@ -206,7 +851,7 @@ let tree_failed entry prev_symb_result prev_symb tree = txt1 ^ " or " ^ txt ^ " expected" end | Slist1sep (s, sep, _) -> - begin match Obj.magic prev_symb_result with + begin match prev_symb_result with [] -> let txt1 = name_of_symbol_failed entry s in txt1 ^ " or " ^ txt ^ " expected" @@ -214,7 +859,8 @@ let tree_failed entry prev_symb_result prev_symb tree = let txt1 = name_of_symbol_failed entry sep in txt1 ^ " or " ^ txt ^ " expected" end - | Sopt _ | Stree _ -> txt ^ " expected" + | Sopt _ -> txt ^ " expected" + | Stree _ -> txt ^ " expected" | _ -> txt ^ " expected after " ^ name_of_symbol_failed entry prev_symb in txt ^ " (in [" ^ entry.ename ^ "])" @@ -223,8 +869,6 @@ let symb_failed entry prev_symb_result prev_symb symb = let tree = Node {node = symb; brother = DeadEnd; son = DeadEnd} in tree_failed entry prev_symb_result prev_symb tree -external app : Obj.t -> 'a = "%identity" - let is_level_labelled n lev = match lev.lname with Some n1 -> n = n1 @@ -241,28 +885,33 @@ let level_number entry lab = Dlevels elev -> lookup 0 elev | Dparser _ -> raise Not_found -let rec top_symb entry = +let rec top_symb : type s a. s ty_entry -> (s, a) ty_symbol -> (s, a) ty_symbol = + fun entry -> function - Sself | Snext -> Snterm entry + Sself -> Snterm entry + | Snext -> Snterm entry | Snterml (e, _) -> Snterm e | Slist1sep (s, sep, b) -> Slist1sep (top_symb entry s, sep, b) | _ -> raise Stream.Failure -let entry_of_symb entry = +let entry_of_symb : type s a. s ty_entry -> (s, a) ty_symbol -> a ty_entry = + fun entry -> function - Sself | Snext -> entry + Sself -> entry + | Snext -> entry | Snterm e -> e | Snterml (e, _) -> e | _ -> raise Stream.Failure -let top_tree entry = +let top_tree : type s a. s ty_entry -> (s, a) ty_tree -> (s, a) ty_tree = + fun entry -> function Node {node = s; brother = bro; son = son} -> Node {node = top_symb entry s; brother = bro; son = son} | LocAct (_, _) | DeadEnd -> raise Stream.Failure let skip_if_empty bp p strm = - if Stream.count strm == bp then gramext_action (fun a -> p strm) + if Stream.count strm == bp then fun a -> p strm else raise Stream.Failure let continue entry bp a s son p1 (strm__ : _ Stream.t) = @@ -271,7 +920,7 @@ let continue entry bp a s son p1 (strm__ : _ Stream.t) = try p1 strm__ with Stream.Failure -> raise (Stream.Error (tree_failed entry a s son)) in - gramext_action (fun _ -> app act a) + fun _ -> act a let do_recover parser_of_tree entry nlevn alevn bp a s son (strm__ : _ Stream.t) = @@ -309,27 +958,28 @@ let call_and_push ps al strm = let token_ematch gram tok = let tematch = gram.glexer.Plexing.tok_match tok in - fun tok -> Obj.repr (tematch tok : string) + fun tok -> tematch tok -let rec parser_of_tree entry nlevn alevn = +let rec parser_of_tree : type s r. s ty_entry -> int -> int -> (s, r) ty_tree -> r parser_t = + fun entry nlevn alevn -> function DeadEnd -> (fun (strm__ : _ Stream.t) -> raise Stream.Failure) | LocAct (act, _) -> (fun (strm__ : _ Stream.t) -> act) | Node {node = Sself; son = LocAct (act, _); brother = DeadEnd} -> (fun (strm__ : _ Stream.t) -> - let a = entry.estart alevn strm__ in app act a) + let a = entry.estart alevn strm__ in act a) | Node {node = Sself; son = LocAct (act, _); brother = bro} -> let p2 = parser_of_tree entry nlevn alevn bro in (fun (strm__ : _ Stream.t) -> match try Some (entry.estart alevn strm__) with Stream.Failure -> None with - Some a -> app act a + Some a -> act a | _ -> p2 strm__) | Node {node = s; son = son; brother = DeadEnd} -> let tokl = match s with - Stoken tok -> get_token_list entry [] tok son + Stoken tok -> get_token_list entry tok [] tok TokNil son | _ -> None in begin match tokl with @@ -345,19 +995,20 @@ let rec parser_of_tree entry nlevn alevn = Stream.Failure -> raise (Stream.Error (tree_failed entry a s son)) in - app act a) - | Some (rev_tokl, last_tok, son) -> + act a) + | Some (first_tok, rev_tokl, last_tok, TokTree (son, pf)) -> + let s = Stoken first_tok in let lt = Stoken last_tok in let p1 = parser_of_tree entry nlevn alevn son in let p1 = parser_cont p1 entry nlevn alevn lt son in - parser_of_token_list entry s son p1 + parser_of_token_list entry s son pf p1 (fun (strm__ : _ Stream.t) -> raise Stream.Failure) rev_tokl last_tok end | Node {node = s; son = son; brother = bro} -> let tokl = match s with - Stoken tok -> get_token_list entry [] tok son + Stoken tok -> get_token_list entry tok [] tok TokNil son | _ -> None in match tokl with @@ -373,71 +1024,81 @@ let rec parser_of_tree entry nlevn alevn = begin match (try Some (p1 bp a strm) with Stream.Failure -> None) with - Some act -> app act a + Some act -> act a | None -> raise (Stream.Error (tree_failed entry a s son)) end | None -> p2 strm) - | Some (rev_tokl, last_tok, son) -> + | Some (first_tok, rev_tokl, last_tok, TokTree (son, pf)) -> let lt = Stoken last_tok in let p2 = parser_of_tree entry nlevn alevn bro in let p1 = parser_of_tree entry nlevn alevn son in let p1 = parser_cont p1 entry nlevn alevn lt son in let p1 = - parser_of_token_list entry lt son p1 p2 rev_tokl last_tok + parser_of_token_list entry lt son pf p1 p2 rev_tokl last_tok in fun (strm__ : _ Stream.t) -> try p1 strm__ with Stream.Failure -> p2 strm__ -and parser_cont p1 entry nlevn alevn s son bp a (strm__ : _ Stream.t) = +and parser_cont : type s a r. + (a -> r) parser_t -> s ty_entry -> int -> int -> (s, a) ty_symbol -> (s, a -> r) ty_tree -> int -> a -> (a -> r) parser_t = + fun p1 entry nlevn alevn s son bp a (strm__ : _ Stream.t) -> try p1 strm__ with Stream.Failure -> recover parser_of_tree entry nlevn alevn bp a s son strm__ -and parser_of_token_list entry s son p1 p2 rev_tokl last_tok = - let plast = +and parser_of_token_list : type s r f. + s ty_entry -> (s, string) ty_symbol -> (s, string -> r) ty_tree -> + (r, f) tok_list -> (int -> string -> (string -> r) parser_t) -> f parser_t -> _ -> _ -> f parser_t = + fun entry s son pf p1 p2 rev_tokl last_tok -> + let plast : r parser_t = let n = List.length rev_tokl + 1 in - let tematch = token_ematch entry.egram last_tok in + let tematch = token_ematch egram last_tok in let ps strm = match peek_nth n strm with Some tok -> let r = tematch tok in - for _i = 1 to n do Stream.junk strm done; Obj.repr r + for _i = 1 to n do Stream.junk strm done; r | None -> raise Stream.Failure in fun (strm : _ Stream.t) -> let bp = Stream.count strm in let a = ps strm in match try Some (p1 bp a strm) with Stream.Failure -> None with - Some act -> app act a + Some act -> act a | None -> raise (Stream.Error (tree_failed entry a s son)) in - match List.rev rev_tokl with - [] -> (fun (strm__ : _ Stream.t) -> plast strm__) - | tok :: tokl -> - let tematch = token_ematch entry.egram tok in + match List.rev rev_tokl, pf with + [], TokNil -> (fun (strm__ : _ Stream.t) -> plast strm__) + | tok :: tokl, TokCns pf -> + let tematch = token_ematch egram tok in let ps strm = match peek_nth 1 strm with Some tok -> tematch tok | None -> raise Stream.Failure in let p1 = - let rec loop n = - function - [] -> plast - | tok :: tokl -> - let tematch = token_ematch entry.egram tok in + let rec loop : type s f. _ -> _ -> (s, f) tok_list -> (string -> s) parser_t -> (string -> f) parser_t = + fun n tokl pf plast -> + match tokl, pf with + [], TokNil -> plast + | tok :: tokl, TokCns pf -> + let tematch = token_ematch egram tok in let ps strm = match peek_nth n strm with Some tok -> tematch tok | None -> raise Stream.Failure in - let p1 = loop (n + 1) tokl in + let p1 = loop (n + 1) tokl pf (Obj.magic plast) in (* FIXME *) fun (strm__ : _ Stream.t) -> - let a = ps strm__ in let act = p1 strm__ in app act a + let a = ps strm__ in let act = p1 strm__ in (Obj.magic act a) (* FIXME *) + | _ -> assert false in - loop 2 tokl + loop 2 tokl pf plast in fun (strm__ : _ Stream.t) -> - let a = ps strm__ in let act = p1 strm__ in app act a -and parser_of_symbol entry nlevn = + let a = ps strm__ in let act = p1 strm__ in act a + | _ -> assert false +and parser_of_symbol : type s a. + s ty_entry -> int -> (s, a) ty_symbol -> a parser_t = + fun entry nlevn -> function | Slist0 s -> let ps = call_and_push (parser_of_symbol entry nlevn s) in @@ -447,7 +1108,7 @@ and parser_of_symbol entry nlevn = | _ -> al in (fun (strm__ : _ Stream.t) -> - let a = loop [] strm__ in Obj.repr (List.rev a)) + let a = loop [] strm__ in List.rev a) | Slist0sep (symb, sep, false) -> let ps = call_and_push (parser_of_symbol entry nlevn symb) in let pt = parser_of_symbol entry nlevn sep in @@ -464,8 +1125,8 @@ and parser_of_symbol entry nlevn = in (fun (strm__ : _ Stream.t) -> match try Some (ps [] strm__) with Stream.Failure -> None with - Some al -> let a = kont al strm__ in Obj.repr (List.rev a) - | _ -> Obj.repr []) + Some al -> let a = kont al strm__ in List.rev a + | _ -> []) | Slist0sep (symb, sep, true) -> let ps = call_and_push (parser_of_symbol entry nlevn symb) in let pt = parser_of_symbol entry nlevn sep in @@ -482,8 +1143,8 @@ and parser_of_symbol entry nlevn = in (fun (strm__ : _ Stream.t) -> match try Some (ps [] strm__) with Stream.Failure -> None with - Some al -> let a = kont al strm__ in Obj.repr (List.rev a) - | _ -> Obj.repr []) + Some al -> let a = kont al strm__ in List.rev a + | _ -> []) | Slist1 s -> let ps = call_and_push (parser_of_symbol entry nlevn s) in let rec loop al (strm__ : _ Stream.t) = @@ -493,7 +1154,7 @@ and parser_of_symbol entry nlevn = in (fun (strm__ : _ Stream.t) -> let al = ps [] strm__ in - let a = loop al strm__ in Obj.repr (List.rev a)) + let a = loop al strm__ in List.rev a) | Slist1sep (symb, sep, false) -> let ps = call_and_push (parser_of_symbol entry nlevn symb) in let pt = parser_of_symbol entry nlevn sep in @@ -515,7 +1176,7 @@ and parser_of_symbol entry nlevn = in (fun (strm__ : _ Stream.t) -> let al = ps [] strm__ in - let a = kont al strm__ in Obj.repr (List.rev a)) + let a = kont al strm__ in List.rev a) | Slist1sep (symb, sep, true) -> let ps = call_and_push (parser_of_symbol entry nlevn symb) in let pt = parser_of_symbol entry nlevn sep in @@ -538,33 +1199,37 @@ and parser_of_symbol entry nlevn = in (fun (strm__ : _ Stream.t) -> let al = ps [] strm__ in - let a = kont al strm__ in Obj.repr (List.rev a)) + let a = kont al strm__ in List.rev a) | Sopt s -> let ps = parser_of_symbol entry nlevn s in (fun (strm__ : _ Stream.t) -> match try Some (ps strm__) with Stream.Failure -> None with - Some a -> Obj.repr (Some a) - | _ -> Obj.repr None) + Some a -> Some a + | _ -> None) | Stree t -> let pt = parser_of_tree entry 1 0 t in (fun (strm__ : _ Stream.t) -> let bp = Stream.count strm__ in let a = pt strm__ in let ep = Stream.count strm__ in - let loc = loc_of_token_interval bp ep in app a loc) + let loc = loc_of_token_interval bp ep in a loc) | Snterm e -> (fun (strm__ : _ Stream.t) -> e.estart 0 strm__) | Snterml (e, l) -> (fun (strm__ : _ Stream.t) -> e.estart (level_number e l) strm__) | Sself -> (fun (strm__ : _ Stream.t) -> entry.estart 0 strm__) | Snext -> (fun (strm__ : _ Stream.t) -> entry.estart nlevn strm__) | Stoken tok -> parser_of_token entry tok -and parser_of_token entry tok = - let f = entry.egram.glexer.Plexing.tok_match tok in +and parser_of_token : type s. + s ty_entry -> Plexing.pattern -> string parser_t = + fun entry tok -> + let f = egram.glexer.Plexing.tok_match tok in fun strm -> match Stream.peek strm with - Some tok -> let r = f tok in Stream.junk strm; Obj.repr r + Some tok -> let r = f tok in Stream.junk strm; r | None -> raise Stream.Failure -and parse_top_symb entry symb = parser_of_symbol entry 0 (top_symb entry symb) +and parse_top_symb : type s a. s ty_entry -> (s, a) ty_symbol -> a parser_t = + fun entry symb -> + parser_of_symbol entry 0 (top_symb entry symb) let rec start_parser_of_levels entry clevn = function @@ -594,7 +1259,7 @@ let rec start_parser_of_levels entry clevn = let bp = Stream.count strm__ in let act = p2 strm__ in let ep = Stream.count strm__ in - let a = app act (loc_of_token_interval bp ep) in + let a = act (loc_of_token_interval bp ep) in entry.econtinue levn bp a strm) | _ -> fun levn strm -> @@ -605,7 +1270,7 @@ let rec start_parser_of_levels entry clevn = match try Some (p2 strm__) with Stream.Failure -> None with Some act -> let ep = Stream.count strm__ in - let a = app act (loc_of_token_interval bp ep) in + let a = act (loc_of_token_interval bp ep) in entry.econtinue levn bp a strm | _ -> p1 levn strm__ @@ -631,7 +1296,7 @@ let rec continue_parser_of_levels entry clevn = Stream.Failure -> let act = p2 strm__ in let ep = Stream.count strm__ in - let a = app act a (loc_of_token_interval bp ep) in + let a = act a (loc_of_token_interval bp ep) in entry.econtinue levn bp a strm let continue_parser_of_entry entry = @@ -663,7 +1328,7 @@ let init_entry_functions entry = entry.econtinue <- f; f lev bp a strm) let extend_entry ~warning entry position rules = - let elev = Gramext.levels_of_rules ~warning entry position rules in + let elev = levels_of_rules ~warning entry position rules in entry.edesc <- Dlevels elev; init_entry_functions entry (* Deleting a rule *) @@ -671,7 +1336,7 @@ let extend_entry ~warning entry position rules = let delete_rule entry sl = match entry.edesc with Dlevels levs -> - let levs = Gramext.delete_rule_in_level_list entry sl levs in + let levs = delete_rule_in_level_list entry sl levs in entry.edesc <- Dlevels levs; entry.estart <- (fun lev strm -> @@ -685,20 +1350,9 @@ let delete_rule entry sl = (* Normal interface *) -let create_toktab () = Hashtbl.create 301 -let gcreate glexer = - {gtokens = create_toktab (); glexer = glexer } - -let tokens g con = - let list = ref [] in - Hashtbl.iter - (fun (p_con, p_prm) c -> if p_con = con then list := (p_prm, !c) :: !list) - g.gtokens; - !list - -type 'te gen_parsable = +type parsable = { pa_chr_strm : char Stream.t; - pa_tok_strm : 'te Stream.t; + pa_tok_strm : L.te Stream.t; pa_loc_func : Plexing.location_function } let parse_parsable entry p = @@ -741,95 +1395,30 @@ let clear_entry e = Dlevels _ -> e.edesc <- Dlevels [] | Dparser _ -> () -(* Functorial interface *) - -module type GLexerType = sig type te val lexer : te Plexing.lexer end - -module type S = - sig - type te - type parsable - val parsable : char Stream.t -> parsable - val tokens : string -> (string * int) list - module Entry : - sig - type 'a e - val create : string -> 'a e - val parse : 'a e -> parsable -> 'a - val name : 'a e -> string - val of_parser : string -> (te Stream.t -> 'a) -> 'a e - val parse_token_stream : 'a e -> te Stream.t -> 'a - val print : Format.formatter -> 'a e -> unit - end - type ('self, 'a) ty_symbol - type ('self, 'f, 'r) ty_rule - type 'a ty_production - val s_nterm : 'a Entry.e -> ('self, 'a) ty_symbol - val s_nterml : 'a Entry.e -> string -> ('self, 'a) ty_symbol - val s_list0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol - val s_list0sep : - ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool -> - ('self, 'a list) ty_symbol - val s_list1 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol - val s_list1sep : - ('self, 'a) ty_symbol -> ('self, 'b) ty_symbol -> bool -> - ('self, 'a list) ty_symbol - val s_opt : ('self, 'a) ty_symbol -> ('self, 'a option) ty_symbol - val s_self : ('self, 'self) ty_symbol - val s_next : ('self, 'self) ty_symbol - val s_token : Plexing.pattern -> ('self, string) ty_symbol - val s_rules : warning:(string -> unit) option -> 'a ty_production list -> ('self, 'a) ty_symbol - val r_stop : ('self, 'r, 'r) ty_rule - val r_next : - ('self, 'a, 'r) ty_rule -> ('self, 'b) ty_symbol -> - ('self, 'b -> 'a, 'r) ty_rule - val production : ('a, 'f, Loc.t -> 'a) ty_rule * 'f -> 'a ty_production - module Unsafe : - sig - val clear_entry : 'a Entry.e -> unit - end - val safe_extend : warning:(string -> unit) option -> - 'a Entry.e -> Gramext.position option -> - (string option * Gramext.g_assoc option * 'a ty_production list) - list -> - unit - val safe_delete_rule : 'a Entry.e -> ('a, 'r, 'f) ty_rule -> unit - end - -module GMake (L : GLexerType) = - struct - type te = L.te - type parsable = te gen_parsable - let gram = gcreate L.lexer let parsable cs = let (ts, lf) = L.lexer.Plexing.tok_func cs in {pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf} - let tokens = tokens gram module Entry = struct - type 'a e = te g_entry + type 'a e = 'a ty_entry let create n = - {egram = gram; ename = n; elocal = false; estart = empty_entry n; + { ename = n; estart = empty_entry n; econtinue = (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure); edesc = Dlevels []} - external obj : 'a e -> te Gramext.g_entry = "%identity" let parse (e : 'a e) p : 'a = - Obj.magic (parse_parsable e p : Obj.t) + parse_parsable e p let parse_token_stream (e : 'a e) ts : 'a = - Obj.magic (e.estart 0 ts : Obj.t) + e.estart 0 ts let name e = e.ename let of_parser n (p : te Stream.t -> 'a) : 'a e = - {egram = gram; ename = n; elocal = false; - estart = (fun _ -> (Obj.magic p : te Stream.t -> Obj.t)); + { ename = n; + estart = (fun _ -> p); econtinue = (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure); - edesc = Dparser (Obj.magic p : te Stream.t -> Obj.t)} - let print ppf e = fprintf ppf "%a@." print_entry (obj e) + edesc = Dparser p} + let print ppf e = fprintf ppf "%a@." print_entry e end - type ('self, 'a) ty_symbol = te Gramext.g_symbol - type ('self, 'f, 'r) ty_rule = ('self, Obj.t) ty_symbol list - type 'a ty_production = ('a, Obj.t, Obj.t) ty_rule * Gramext.g_action let s_nterm e = Snterm e let s_nterml e l = Snterml (e, l) let s_list0 s = Slist0 s @@ -840,20 +1429,21 @@ module GMake (L : GLexerType) = let s_self = Sself let s_next = Snext let s_token tok = Stoken tok - let s_rules ~warning (t : Obj.t ty_production list) = Gramext.srules ~warning (Obj.magic t) - let r_stop = [] - let r_next r s = r @ [s] - let production - (p : ('a, 'f, Loc.t -> 'a) ty_rule * 'f) : 'a ty_production = - Obj.magic p + let s_rules ~warning (t : 'a ty_production list) = srules ~warning t + let r_stop = TStop + let r_next r s = TNext (r, s) + let production (p, act) = TProd (p, act) module Unsafe = struct let clear_entry = clear_entry end - let safe_extend ~warning e pos + let safe_extend ~warning (e : 'a Entry.e) pos (r : - (string option * Gramext.g_assoc option * Obj.t ty_production list) + (string option * Gramext.g_assoc option * 'a ty_production list) list) = - extend_entry ~warning e pos (Obj.magic r) - let safe_delete_rule e r = delete_rule (Entry.obj e) r - end + extend_entry ~warning e pos r + let safe_delete_rule e r = + let AnyS (symbols, _) = get_symbols r in + delete_rule e symbols + +end diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 525ff7fd0f..62906303a4 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -530,7 +530,15 @@ let interp_gen kind ist pattern_mode flags env sigma c = invariant that running the tactic returned by push_trace does not modify sigma. *) let (_, dummy_proofview) = Proofview.init sigma [] in - let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in + + (* Again this is called at times with no open proof! *) + let name, poly = + try + let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in + name, poly + with | Proof_global.NoCurrentProof -> Id.of_string "tacinterp", false + in + let (trace,_,_,_) = Proofview.apply ~name ~poly env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in let (evd,c) = catch_error trace (understand_ltac flags env sigma vars kind) term in @@ -2041,7 +2049,16 @@ let _ = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun = lfun; extra; } in let tac = interp_tactic ist tac in - let name, poly = Id.of_string "ltac_sub", false in + (* XXX: This depends on the global state which is bad; the hooking + mechanism should be modified. *) + let name, poly = + try + let (_, poly, _) = Proof_global.get_current_persistence () in + let name = Proof_global.get_current_proof_name () in + name, poly + with | Proof_global.NoCurrentProof -> + Id.of_string "ltac_gen", false + in let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in (EConstr.of_constr c, sigma) in diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 9ce9250a43..0897d3b45b 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -137,6 +137,9 @@ type 'tac ssrhint = bool * 'tac option list type 'tac fwdbinders = bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint)) +type 'tac ffwbinders = + (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint)) + type clause = (ssrclear * ((ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) option) diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 3fb21e5ef6..2a2cd73df2 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -591,10 +591,8 @@ END GRAMMAR EXTEND Gram GLOBAL: ssrfwdview; ssrfwdview: [ - [ test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr -> - { [mk_ast_closure_term `None c] } - | test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr; w = ssrfwdview -> - { (mk_ast_closure_term `None c) :: w } ]]; + [ test_not_ssrslashnum; "/"; c = ast_closure_term -> { [c] } + | test_not_ssrslashnum; "/"; c = ast_closure_term; w = ssrfwdview -> { c :: w } ]]; END (* ipats *) diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index a2cbd3c9c8..7844050272 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -32,6 +32,19 @@ type ssrfwdview = ast_closure_term list type ssreqid = ssripat option type ssrarg = ssrfwdview * (ssreqid * (cpattern ssragens * ssripats)) +val wit_ssrseqdir : ssrdir Genarg.uniform_genarg_type +val wit_ssrseqarg : (Tacexpr.raw_tactic_expr ssrseqarg, Tacexpr.glob_tactic_expr ssrseqarg, Geninterp.Val.t ssrseqarg) Genarg.genarg_type + +val wit_ssrintrosarg : + (Tacexpr.raw_tactic_expr * ssripats, + Tacexpr.glob_tactic_expr * ssripats, + Geninterp.Val.t * ssripats) Genarg.genarg_type + +val wit_ssrsufffwd : + (Tacexpr.raw_tactic_expr ffwbinders, + Tacexpr.glob_tactic_expr ffwbinders, + Geninterp.Val.t ffwbinders) Genarg.genarg_type + val wit_ssripatrep : ssripat Genarg.uniform_genarg_type val wit_ssrarg : ssrarg Genarg.uniform_genarg_type val wit_ssrrwargs : ssrrwarg list Genarg.uniform_genarg_type @@ -47,3 +60,43 @@ val wit_ssrhintarg : (Tacexpr.raw_tactic_expr ssrhint, Tacexpr.glob_tactic_expr ssrhint, Tacinterp.Value.t ssrhint) Genarg.genarg_type + +val wit_ssrexactarg : ssrapplyarg Genarg.uniform_genarg_type +val wit_ssrcongrarg : ((int * ssrterm) * cpattern ssragens) Genarg.uniform_genarg_type +val wit_ssrfwdid : Names.Id.t Genarg.uniform_genarg_type + +val wit_ssrsetfwd : + ((ssrfwdfmt * (cpattern * ast_closure_term option)) * ssrdocc) Genarg.uniform_genarg_type + +val wit_ssrdoarg : + (Tacexpr.raw_tactic_expr ssrdoarg, + Tacexpr.glob_tactic_expr ssrdoarg, + Tacinterp.Value.t ssrdoarg) Genarg.genarg_type + +val wit_ssrhint : + (Tacexpr.raw_tactic_expr ssrhint, + Tacexpr.glob_tactic_expr ssrhint, + Tacinterp.Value.t ssrhint) Genarg.genarg_type + +val wit_ssrhpats : ssrhpats Genarg.uniform_genarg_type +val wit_ssrhpats_nobs : ssrhpats Genarg.uniform_genarg_type +val wit_ssrhpats_wtransp : ssrhpats_wtransp Genarg.uniform_genarg_type + +val wit_ssrposefwd : (ssrfwdfmt * ast_closure_term) Genarg.uniform_genarg_type + +val wit_ssrrpat : ssripat Genarg.uniform_genarg_type +val wit_ssrterm : ssrterm Genarg.uniform_genarg_type +val wit_ssrunlockarg : (ssrocc * ssrterm) Genarg.uniform_genarg_type +val wit_ssrunlockargs : (ssrocc * ssrterm) list Genarg.uniform_genarg_type + +val wit_ssrwgen : clause Genarg.uniform_genarg_type +val wit_ssrwlogfwd : (clause list * (ssrfwdfmt * ast_closure_term)) Genarg.uniform_genarg_type + +val wit_ssrfixfwd : (Names.Id.t * (ssrfwdfmt * ast_closure_term)) Genarg.uniform_genarg_type +val wit_ssrfwd : (ssrfwdfmt * ast_closure_term) Genarg.uniform_genarg_type +val wit_ssrfwdfmt : ssrfwdfmt Genarg.uniform_genarg_type + +val wit_ssrcpat : ssripat Genarg.uniform_genarg_type +val wit_ssrdgens : cpattern ssragens Genarg.uniform_genarg_type +val wit_ssrdgens_tl : cpattern ssragens Genarg.uniform_genarg_type +val wit_ssrdir : ssrdir Genarg.uniform_genarg_type diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 7f1ae6d12b..9509c36ec0 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -70,11 +70,6 @@ let get_current_context ?p () = let evd = Proof.in_proof p (fun x -> x) in (evd, Global.env ()) -let current_proof_statement () = - match Proof_global.V82.get_current_initial_conclusions () with - | (id,([concl],strength)) -> id,strength,concl - | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement.") - let solve ?with_end_tac gi info_lvl tac pr = try let tac = match with_end_tac with diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 5699320af5..29ab00876a 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -34,11 +34,6 @@ val get_current_goal_context : unit -> Evd.evar_map * env val get_current_context : ?p:Proof.t -> unit -> Evd.evar_map * env -(** [current_proof_statement] *) - -val current_proof_statement : - unit -> Id.t * goal_kind * EConstr.types - (** {6 ... } *) (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th diff --git a/proofs/proof.ml b/proofs/proof.ml index 4ce932b93d..e40940f652 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -415,8 +415,9 @@ let run_tactic env tac pr = Proofview.Unsafe.tclEVARS sigma >>= fun () -> Proofview.tclUNIT retrieved in + let { name; poly } = pr in let (retrieved,proofview,(status,to_shelve,give_up),info_trace) = - Proofview.apply env tac sp + Proofview.apply ~name ~poly env tac sp in let sigma = Proofview.return proofview in let to_shelve = undef sigma to_shelve in @@ -498,7 +499,8 @@ module V82 = struct let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in Proofview.Unsafe.tclEVARS sigma end in - let ((), proofview, _, _) = Proofview.apply env tac pr.proofview in + let { name; poly } = pr in + let ((), proofview, _, _) = Proofview.apply ~name ~poly env tac pr.proofview in let shelf = List.filter begin fun g -> Evd.is_undefined (Proofview.return proofview) g diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 9ee9e7ae2c..0cfc010c1a 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -66,12 +66,6 @@ let pstates = ref ([] : pstate list) (* combinators for the current_proof lists *) let push a l = l := a::!l -exception NoSuchProof -let () = CErrors.register_handler begin function - | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.") - | _ -> raise CErrors.Unhandled -end - exception NoCurrentProof let () = CErrors.register_handler begin function | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).") @@ -91,6 +85,7 @@ let cur_pstate () = let give_me_the_proof () = (cur_pstate ()).proof let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None let get_current_proof_name () = (Proof.data (cur_pstate ()).proof).Proof.name +let get_current_persistence () = (cur_pstate ()).strength let with_current_proof f = match !pstates with @@ -386,15 +381,6 @@ let set_terminator hook = | [] -> raise NoCurrentProof | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps -module V82 = struct - let get_current_initial_conclusions () = - let { proof; strength } = cur_pstate () in - let Proof.{ name; entry } = Proof.data proof in - let initial = Proofview.initial_goals entry in - let goals = List.map (fun (o, c) -> c) initial in - name, (goals, strength) -end - let freeze ~marshallable = if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.") else !pstates diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 40920f51a3..38e234eaee 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -17,6 +17,7 @@ val there_are_pending_proofs : unit -> bool val check_no_pending_proof : unit -> unit val get_current_proof_name : unit -> Names.Id.t +val get_current_persistence : unit -> Decl_kinds.goal_kind val get_all_proof_names : unit -> Names.Id.t list val discard : Names.lident -> unit @@ -104,8 +105,6 @@ val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> val get_terminator : unit -> proof_terminator val set_terminator : proof_terminator -> unit -exception NoSuchProof - val get_open_goals : unit -> int (** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is @@ -129,11 +128,6 @@ val get_used_variables : unit -> Constr.named_context option (** Get the universe declaration associated to the current proof. *) val get_universe_decl : unit -> UState.universe_decl -module V82 : sig - val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list * - Decl_kinds.goal_kind) -end - val freeze : marshallable:bool -> t val unfreeze : t -> unit val proof_of_state : t -> Proof.t diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 3a687a6b41..c3e3a62e26 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -11,7 +11,6 @@ module CVars = Vars open Util -open Names open Termops open EConstr open Decl_kinds @@ -87,10 +86,26 @@ let shrink_entry sign const = } in (const, args) -let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = +let name_op_to_name ~name_op ~name ~goal_kind suffix = + match name_op with + | Some s -> s, goal_kind + | None -> Nameops.add_suffix name suffix, goal_kind + +let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let open Tacticals.New in let open Tacmach.New in let open Proofview.Notations in + Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (name, poly) -> + (* This is important: The [Global] and [Proof Theorem] parts of the + goal_kind are not relevant here as build_constant_by_tactic does + use the noop terminator; but beware if some day we remove the + redundancy on constrant declaration. This opens up an interesting + question, how does abstract behave when discharge is local for example? + *) + let goal_kind, suffix = if opaque + then (Global,poly,Proof Theorem), "_subproof" + else (Global,poly,DefinitionBody Definition), "_subterm" in + let id, goal_kind = name_op_to_name ~name_op ~name ~goal_kind suffix in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in @@ -126,7 +141,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in let ectx = Evd.evar_universe_context evd in let (const, safe, ectx) = - try Pfedit.build_constant_by_tactic ~goal_kind:gk id ectx secsign concl solve_tac + try Pfedit.build_constant_by_tactic ~goal_kind id ectx secsign concl solve_tac with Logic_monad.TacticFailure e as src -> (* if the tactic [tac] fails, it reports a [TacticFailure e], which is an error irrelevant to the proof system (in fact it @@ -170,26 +185,8 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) tac end -let abstract_subproof ~opaque id gk tac = - cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> Tactics.exact_no_check (applist (lem, args))) - -let anon_id = Id.of_string "anonymous" - -let name_op_to_name name_op object_kind suffix = - let open Proof_global in - let default_gk = (Global, false, object_kind) in - let name, gk = match Proof_global.V82.get_current_initial_conclusions () with - | (id, (_, gk)) -> Some id, gk - | exception NoCurrentProof -> None, default_gk - in - match name_op with - | Some s -> s, gk - | None -> - let name = Option.default anon_id name in - Nameops.add_suffix name suffix, gk +let abstract_subproof ~opaque tac = + cache_term_by_tactic_then ~opaque tac (fun lem args -> Tactics.exact_no_check (applist (lem, args))) let tclABSTRACT ?(opaque=true) name_op tac = - let s, gk = if opaque - then name_op_to_name name_op (Proof Theorem) "_subproof" - else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in - abstract_subproof ~opaque s gk tac + abstract_subproof ~opaque ~name_op tac diff --git a/tactics/abstract.mli b/tactics/abstract.mli index 7fb671fbf8..9d4f3cfb27 100644 --- a/tactics/abstract.mli +++ b/tactics/abstract.mli @@ -11,6 +11,12 @@ open Names open EConstr -val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic +val cache_term_by_tactic_then + : opaque:bool + -> name_op:Id.t option + -> ?goal_type:(constr option) + -> unit Proofview.tactic + -> (constr -> constr list -> unit Proofview.tactic) + -> unit Proofview.tactic val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index ba7645446d..e505bb3a42 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -930,8 +930,16 @@ module Search = struct let _, pv = Proofview.init evm [] in let pv = Proofview.unshelve goals pv in try + (* Instance may try to call this before a proof is set up! + Thus, give_me_the_proof will fail. Beware! *) + let name, poly = try + let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in + name, poly + with | Proof_global.NoCurrentProof -> + Id.of_string "instance", false + in let (), pv', (unsafe, shelved, gaveup), _ = - Proofview.apply env tac pv + Proofview.apply ~name ~poly env tac pv in if not (List.is_empty gaveup) then CErrors.anomaly (Pp.str "run_on_evars not assumed to apply tactics generating given up goals."); diff --git a/test-suite/ssr/autoclean.v b/test-suite/ssr/autoclean.v new file mode 100644 index 0000000000..db80a62259 --- /dev/null +++ b/test-suite/ssr/autoclean.v @@ -0,0 +1,4 @@ +Require Import ssreflect. + +Lemma view_disappears A B (AB : A -> B) : A -> False. +Proof. move=> {}/(AB). have := AB. Abort. diff --git a/test-suite/stm/arg_filter_1.v b/test-suite/stm/arg_filter_1.v index 1cf66d6b43..ed87d67405 100644 --- a/test-suite/stm/arg_filter_1.v +++ b/test-suite/stm/arg_filter_1.v @@ -1,4 +1,4 @@ (* coq-prog-args: ("-async-proofs-tac-j" "1") *) -Lemma foo : True. -Proof. now auto. Qed. +Lemma foo (A B : Prop) n : n + 0 = n /\ (A -> B -> A). +Proof. split. par: now auto. Qed. diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index b549f22119..c110f3831e 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -13,6 +13,9 @@ let fatal_error exn = let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in exit exit_code +let error_wrong_arg msg = + prerr_endline msg; exit 1 + let error_missing_arg s = prerr_endline ("Error: extra argument expected after option "^s); prerr_endline "See -help for the syntax of supported options"; @@ -169,7 +172,8 @@ let set_color opts = function | "yes" | "on" -> { opts with color = `ON } | "no" | "off" -> { opts with color = `OFF } | "auto" -> { opts with color = `AUTO } -| _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1 +| _ -> + error_wrong_arg ("Error: on/off/auto expected after option color") let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" @@ -187,26 +191,26 @@ let exitcode opts = if opts.filter_opts then 2 else 0 let get_bool opt = function | "yes" | "on" -> true | "no" | "off" -> false - | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1 + | _ -> + error_wrong_arg ("Error: yes/no expected after option "^opt) let get_int opt n = try int_of_string n with Failure _ -> - prerr_endline ("Error: integer expected after option "^opt); exit 1 + error_wrong_arg ("Error: integer expected after option "^opt) let get_float opt n = try float_of_string n with Failure _ -> - prerr_endline ("Error: float expected after option "^opt); exit 1 + error_wrong_arg ("Error: float expected after option "^opt) let get_host_port opt s = match String.split_on_char ':' s with | [host; portr; portw] -> - Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) + Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) | ["stdfds"] -> Some Spawned.AnonPipe | _ -> - prerr_endline ("Error: host:portr:portw or stdfds expected after option "^opt); - exit 1 + error_wrong_arg ("Error: host:portr:portw or stdfds expected after option "^opt) let get_error_resilience opt = function | "on" | "all" | "yes" -> `All @@ -216,17 +220,20 @@ let get_error_resilience opt = function let get_priority opt s = try CoqworkmgrApi.priority_of_string s with Invalid_argument _ -> - prerr_endline ("Error: low/high expected after "^opt); exit 1 + error_wrong_arg ("Error: low/high expected after "^opt) let get_async_proofs_mode opt = let open Stm.AsyncOpts in function | "no" | "off" -> APoff | "yes" | "on" -> APon | "lazy" -> APonLazy - | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1 + | _ -> + error_wrong_arg ("Error: on/off/lazy expected after "^opt) let get_cache opt = function | "force" -> Some Stm.AsyncOpts.Force - | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 + | _ -> + error_wrong_arg ("Error: force expected after "^opt) + let get_native_name s = (* We ignore even critical errors because this mode has to be super silent *) @@ -311,8 +318,12 @@ let parse_args ~help ~init arglist : t * string list = }} |"-async-proofs-tac-j" -> + let j = get_int opt (next ()) in + if j <= 0 then begin + error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1") + end; { oval with stm_flags = { oval.stm_flags with - Stm.AsyncOpts.async_proofs_n_tacworkers = (get_int opt (next ())) + Stm.AsyncOpts.async_proofs_n_tacworkers = j }} |"-async-proofs-worker-priority" -> @@ -431,7 +442,8 @@ let parse_args ~help ~init arglist : t * string list = | ("yes" | "on") -> NativeOn {ondemand=false} | "ondemand" -> NativeOn {ondemand=true} | ("no" | "off") -> NativeOff - | _ -> prerr_endline ("Error: (yes|no|ondemand) expected after option -native-compiler"); exit 1 + | _ -> + error_wrong_arg ("Error: (yes|no|ondemand) expected after option -native-compiler") in { oval with native_compiler } @@ -456,7 +468,7 @@ let parse_args ~help ~init arglist : t * string list = if List.exists (fun x -> opt = x) ["off"; "on"; "removed"] then Proof_diffs.write_diffs_option opt else - (prerr_endline ("Error: on|off|removed expected after -diffs"); exit 1); + error_wrong_arg "Error: on|off|removed expected after -diffs"; { oval with diffs_set = true } |"-stm-debug" -> Stm.stm_debug := true; oval |"-emacs" -> set_emacs oval diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 4635883dc2..79182a3f9d 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -481,7 +481,14 @@ let save_proof ?proof = function Admitted(id, k, (sec_vars, (typ, ctx), None), universes) | None -> let pftree = Proof_global.give_me_the_proof () in - let id, k, typ = Pfedit.current_proof_statement () in + let gk = Proof_global.get_current_persistence () in + let Proof.{ name; poly; entry } = Proof.data pftree in + let typ = match Proofview.initial_goals entry with + | [typ] -> snd typ + | _ -> + CErrors.anomaly + ~label:"Lemmas.save_proof" (Pp.str "more than one statement.") + in let typ = EConstr.Unsafe.to_constr typ in let universes = Proof.((data pftree).initial_euctx) in (* This will warn if the proof is complete *) @@ -491,16 +498,15 @@ let save_proof ?proof = function if not !keep_admitted_vars then None else match Proof_global.get_used_variables(), pproofs with | Some _ as x, _ -> x - | None, (pproof, _) :: _ -> + | None, (pproof, _) :: _ -> let env = Global.env () in let ids_typ = Environ.global_vars_set env typ in let ids_def = Environ.global_vars_set env pproof in Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def)) | _ -> None in let decl = Proof_global.get_universe_decl () in - let poly = pi2 k in let ctx = UState.check_univ_decl ~poly universes decl in - Admitted(id,k,(sec_vars, (typ, ctx), None), universes) + Admitted(name,gk,(sec_vars, (typ, ctx), None), universes) in Proof_global.apply_terminator (Proof_global.get_terminator ()) pe | Vernacexpr.Proved (opaque,idopt) -> |