diff options
| -rw-r--r-- | doc/sphinx/credits.rst | 60 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 3 | ||||
| -rw-r--r-- | gramlib/gramext.ml | 67 | ||||
| -rw-r--r-- | gramlib/gramext.mli | 5 | ||||
| -rw-r--r-- | gramlib/grammar.ml | 271 | ||||
| -rw-r--r-- | gramlib/grammar.mli | 76 | ||||
| -rw-r--r-- | gramlib/plexing.ml | 198 | ||||
| -rw-r--r-- | gramlib/plexing.mli | 71 | ||||
| -rw-r--r-- | gramlib/ploc.ml | 113 | ||||
| -rw-r--r-- | gramlib/ploc.mli | 36 | ||||
| -rw-r--r-- | plugins/ssr/ssrast.mli | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssripats.ml | 11 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 6 | ||||
| -rw-r--r-- | plugins/ssr/ssrprinters.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_8544.v | 6 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 4 |
17 files changed, 78 insertions, 855 deletions
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index 4f5064839b..909af6e2f2 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -557,7 +557,7 @@ Pierre Courtieu, Julien Forest and Yves Bertot added extra support to reason on the inductive structure of recursively defined functions. Jean-Marc Notin significantly contributed to the general maintenance of -the system. He also took care of `coqdoc`. +the system. He also took care of ``coqdoc``. Pierre Castéran contributed to the documentation of (co-)inductive types and suggested improvements to the libraries. @@ -642,7 +642,7 @@ improvements, Jean-Marc Notin provided help in debugging, general maintenance and coqdoc support, Vincent Siles contributed extensions of the Scheme command and of injection. -Bruno Barras implemented the `coqchk` tool: this is a stand-alone +Bruno Barras implemented the ``coqchk`` tool: this is a stand-alone type checker that can be used to certify .vo files. Especially, as this verifier runs in a separate process, it is granted not to be “hijacked” by virtually malicious extensions added to |Coq|. @@ -817,12 +817,12 @@ expressions occurring in the goal by pattern in tactics such as set or destruct. Hugo Herbelin also relied on ideas from Chung-Kil Hur’s Heq plugin to introduce automatic computation of occurrences to generalize when using destruct and induction on types with indices. Stéphane Glondu -introduced new tactics constr\_eq, is\_evar and has\_evar to be used +introduced new tactics :tacn:`constr_eq`, :tacn:`is_evar`, and :tacn:`has_evar`, to be used when writing complex tactics. Enrico Tassi added support to fine-tuning -the behavior of simpl. Enrico Tassi added the ability to specify over +the behavior of :tacn:`simpl`. Enrico Tassi added the ability to specify over which variables of a section a lemma has to be exactly generalized. Pierre Letouzey added a tactic timeout and the interruptibility of -vm\_compute. Bug fixes and miscellaneous improvements of the tactic +:tacn:`vm_compute`. Bug fixes and miscellaneous improvements of the tactic language came from Hugo Herbelin, Pierre Letouzey and Matthieu Sozeau. Regarding decision tactics, Loïc Pottier maintained nsatz, moving in @@ -866,7 +866,7 @@ Pierre Courtieu and Arnaud Spiwack contributed new features for using Coq through Proof General. The Dp plugin has been removed. Use the plugin provided with Why 3 -instead (http://why3.lri.fr). +instead (http://why3.lri.fr/). Under the hood, the |Coq| architecture benefited from improvements in terms of efficiency and robustness, especially regarding universes @@ -982,7 +982,7 @@ working at the IAS in Princeton. The guard condition has been made compliant with extensional equality principles such as propositional extensionality and univalence, thanks to Maxime Dénès and Bruno Barras. To ensure compatibility with the -univalence axiom, a new flag “-indices-matter” has been implemented, +univalence axiom, a new flag ``-indices-matter`` has been implemented, taking into account the universe levels of indices when computing the levels of inductive types. This supports using |Coq| as a tool to explore the relations between homotopy theory and type theory. @@ -997,7 +997,7 @@ and improvements regarding the different components of the system. We shall only list a few of them. Pierre Boutillier developed an improved tactic for simplification of -expressions called cbn. +expressions called :tacn:`cbn`. Maxime Dénès maintained the bytecode-based reduction machine. Pierre Letouzey maintained the extraction mechanism. @@ -1069,7 +1069,7 @@ over 100 contributions integrated. The main user visible changes are: document. - More access to the proof engine features from Ltac: goal management - primitives, range selectors and a ``typeclasses eauto`` engine handling + primitives, range selectors and a :tacn:`typeclasses eauto` engine handling multiple goals and multiple successes, by Cyprien Mangin, Matthieu Sozeau and Arnaud Spiwack. @@ -1199,25 +1199,25 @@ Credits: version 8.7 and cleanups of the internals of the system along with a few new features. The main user visible changes are: -- New tactics: variants of tactics supporting existential variables eassert, - eenough, etc... by Hugo Herbelin. Tactics extensionality in H and - inversion_sigma by Jason Gross, specialize with ... accepting partial bindings +- New tactics: variants of tactics supporting existential variables :tacn:`eassert`, + :tacn:`eenough`, etc... by Hugo Herbelin. Tactics ``extensionality in H`` and + :tacn:`inversion_sigma` by Jason Gross, ``specialize with ...`` accepting partial bindings by Pierre Courtieu. -- Cumulative Polymorphic Inductive Types, allowing cumulativity of universes to +- ``Cumulative Polymorphic Inductive`` types, allowing cumulativity of universes to go through applied inductive types, by Amin Timany and Matthieu Sozeau. - Integration of the SSReflect plugin and its documentation in the reference manual, by Enrico Tassi, Assia Mahboubi and Maxime Dénès. -- The coq_makefile tool was completely redesigned to improve its maintainability - and the extensibility of generated Makefiles, and to make `_CoqProject` files +- The ``coq_makefile`` tool was completely redesigned to improve its maintainability + and the extensibility of generated Makefiles, and to make ``_CoqProject`` files more palatable to IDEs by Enrico Tassi. |Coq| 8.7 involved a large amount of work on cleaning and speeding up the code base, notably the work of Pierre-Marie Pédrot on making the tactic-level system insensitive to existential variable expansion, providing a safer API to plugin -writers and making the code more robust. The `dev/doc/changes.txt` file +writers and making the code more robust. The ``dev/doc/changes.txt`` file documents the numerous changes to the implementation and improvements of interfaces. An effort to provide an official, streamlined API to plugin writers is in progress, thanks to the work of Matej Košík. @@ -1238,8 +1238,8 @@ The BigN, BigZ, BigQ libraries are no longer part of the |Coq| standard library, they are now provided by a separate repository https://github.com/coq/bignums, maintained by Pierre Letouzey. -In the Reals library, `IZR` has been changed to produce a compact representation -of integers and real constants are now represented using `IZR` (work by +In the Reals library, ``IZR`` has been changed to produce a compact representation +of integers and real constants are now represented using ``IZR`` (work by Guillaume Melquiond). Standard library additions and improvements by Jason Gross, Pierre Letouzey and @@ -1346,7 +1346,7 @@ with a few new features. The main user visible changes are: Laurence Rideau, Matthieu Sozeau, Paul Steckler, Enrico Tassi, Laurent Théry, Nikita Zyuzin. -- Tools: experimental ``-mangle-names`` option to coqtop/coqc for +- Tools: experimental ``-mangle-names`` option to ``coqtop``/``coqc`` for linting proof scripts, by Jasper Hugunin. On the implementation side, the ``dev/doc/changes.md`` file @@ -1370,7 +1370,7 @@ maintaining and improving the continuous integration system. The OPAM repository for |Coq| packages has been maintained by Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many -users. A list of packages is available at https://coq.inria.fr/opam/www. +users. A list of packages is available at https://coq.inria.fr/opam/www/. The 44 contributors for this version are Yves Bertot, Joachim Breitner, Tej Chajed, Arthur Charguéraud, Jacques-Pascal Deplaix, Maxime Dénès, Jim Fehrle, @@ -1421,8 +1421,8 @@ changes: - Notations: - - Support for autonomous grammars of terms called "custom entries", by - Hugo Herbelin (see section :ref:`custom-entries` of the reference + - Support for autonomous grammars of terms called “custom entries”, by + Hugo Herbelin (see Section :ref:`custom-entries` of the reference manual). - Deprecated notations of the standard library will be removed in the @@ -1449,9 +1449,9 @@ changes: - SSReflect: the implementation of delayed clear was simplified by Enrico Tassi: the variables are always renamed using inaccessible names when the clear switch is processed and finally cleared at the - end of the intro pattern. In addition to that the use-and-discard flag - `{}` typical of rewrite rules can now be also applied to views, - e.g. `=> {}/v` applies `v` and then clears `v`. See section + end of the intro pattern. In addition to that, the use-and-discard flag + ``{}`` typical of rewrite rules can now be also applied to views, + e.g. ``=> {}/v`` applies ``v`` and then clears ``v``. See Section :ref:`introduction_ssr`. - Vernacular: @@ -1476,10 +1476,10 @@ changes: - Multiple sections with the same name are now allowed, by Jasper Hugunin. -- Library: additions and changes in the ``VectorDef``, ``Ascii`` and - ``String`` library. Syntax notations are now available only when using +- Library: additions and changes in the ``VectorDef``, ``Ascii``, and + ``String`` libraries. Syntax notations are now available only when using ``Import`` of libraries and not merely ``Require``, by various - contributors (source of incompatibility, see `CHANGES.md` for details). + contributors (source of incompatibility, see ``CHANGES.md`` for details). - Toplevels: ``coqtop`` and ``coqide`` can now display diffs between proof steps in color, using the :opt:`Diffs` option, by Jim Fehrle. @@ -1515,7 +1515,7 @@ continuous integration system. The OPAM repository for |Coq| packages has been maintained by Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many -users. A list of packages is available at https://coq.inria.fr/opam/www. +users. A list of packages is available at https://coq.inria.fr/opam/www/. The 54 contributors for this version are Léo Andrès, Rin Arakaki, Benjamin Barenblat, Langston Barrett, Siddharth Bhat, Martin Bodin, @@ -1548,6 +1548,6 @@ result of ~2,000 commits and ~500 PRs merged, closing 75+ issues. The |Coq| development team welcomed Vincent Laporte, a new |Coq| engineer working with Maxime Dénès in the |Coq| consortium. -| Paris, October 2018, +| Paris, November 2018, | Matthieu Sozeau for the |Coq| development team | diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 26f4ec6242..457f9b2efa 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2226,6 +2226,7 @@ and an explanation of the underlying technique. :n:`inversion @ident using @ident`. .. tacv:: inversion_sigma + :name: inversion_sigma This tactic turns equalities of dependent pairs (e.g., :g:`existT P x p = existT P y q`, frequently left over by inversion on @@ -2369,7 +2370,7 @@ and an explanation of the underlying technique. assumption. Qed. -.. tacn:: fix ident num +.. tacn:: fix @ident @num :name: fix This tactic is a primitive tactic to start a proof by induction. In diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml index 8960d4f257..72468b540e 100644 --- a/gramlib/gramext.ml +++ b/gramlib/gramext.ml @@ -27,8 +27,6 @@ and 'te g_level = lprefix : 'te g_tree } and g_assoc = NonA | RightA | LeftA and 'te g_symbol = - Sfacto of 'te g_symbol - | Smeta of string * 'te g_symbol list * Obj.t | Snterm of 'te g_entry | Snterml of 'te g_entry * string | Slist0 of 'te g_symbol @@ -36,13 +34,10 @@ and 'te g_symbol = | Slist1 of 'te g_symbol | Slist1sep of 'te g_symbol * 'te g_symbol * bool | Sopt of 'te g_symbol - | Sflag of 'te g_symbol | Sself | Snext - | Scut | Stoken of Plexing.pattern | Stree of 'te g_tree - | Svala of string list * 'te g_symbol and g_action = Obj.t and 'te g_tree = Node of 'te g_node @@ -66,12 +61,10 @@ let rec derive_eps = function Slist0 _ -> true | Slist0sep (_, _, _) -> true - | Sopt _ | Sflag _ -> true - | Sfacto s -> derive_eps s + | Sopt _ -> true | Stree t -> tree_derive_eps t - | Svala (_, s) -> derive_eps s - | Smeta (_, _, _) | Slist1 _ | Slist1sep (_, _, _) | Snterm _ | - Snterml (_, _) | Snext | Sself | Scut | Stoken _ -> + | Slist1 _ | Slist1sep (_, _, _) | Snterm _ | + Snterml (_, _) | Snext | Sself | Stoken _ -> false and tree_derive_eps = function @@ -90,38 +83,11 @@ let rec eq_symbol s1 s2 = | 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 - | Sflag s1, Sflag s2 -> eq_symbol s1 s2 | Sopt s1, Sopt s2 -> eq_symbol s1 s2 - | Svala (ls1, s1), Svala (ls2, s2) -> ls1 = ls2 && eq_symbol s1 s2 | Stree _, Stree _ -> false - | Sfacto (Stree t1), Sfacto (Stree t2) -> - (* The only goal of the node 'Sfacto' is to allow tree comparison - (therefore factorization) without looking at the semantic - actions; allow factorization of rules like "SV foo" which are - actually expanded into a tree. *) - let rec eq_tree t1 t2 = - match t1, t2 with - Node n1, Node n2 -> - eq_symbol n1.node n2.node && eq_tree n1.son n2.son && - eq_tree n1.brother n2.brother - | LocAct (_, _), LocAct (_, _) -> true - | DeadEnd, DeadEnd -> true - | _ -> false - in - eq_tree t1 t2 | _ -> s1 = s2 let is_before s1 s2 = - let s1 = - match s1 with - Svala (_, s) -> s - | _ -> s1 - in - let s2 = - match s2 with - Svala (_, s) -> s - | _ -> s2 - in match s1, s2 with Stoken ("ANY", _), _ -> false | _, Stoken ("ANY", _) -> true @@ -158,9 +124,6 @@ let insert_tree entry_name gsymbols action tree = if eq_symbol s s1 then let t = Node {node = s1; son = insert sl son; brother = bro} in Some t - else if s = Scut then - try_insert s sl (Node {node = s; son = tree; brother = DeadEnd}) - else if s1 = Scut then try_insert s1 (s :: sl) tree else if is_before s1 s || derive_eps s && not (derive_eps s1) then let bro = match try_insert s sl bro with @@ -203,8 +166,6 @@ and token_exists_in_tree f = | LocAct (_, _) | DeadEnd -> false and token_exists_in_symbol f = function - Sfacto sy -> token_exists_in_symbol f sy - | Smeta (_, syl, _) -> List.exists (token_exists_in_symbol f) syl | Slist0 sy -> token_exists_in_symbol f sy | Slist0sep (sy, sep, _) -> token_exists_in_symbol f sy || token_exists_in_symbol f sep @@ -212,11 +173,9 @@ and token_exists_in_symbol f = | Slist1sep (sy, sep, _) -> token_exists_in_symbol f sy || token_exists_in_symbol f sep | Sopt sy -> token_exists_in_symbol f sy - | Sflag sy -> token_exists_in_symbol f sy | Stoken tok -> f tok | Stree t -> token_exists_in_tree f t - | Svala (_, sy) -> token_exists_in_symbol f sy - | Snterm _ | Snterml (_, _) | Snext | Sself | Scut -> false + | Snterm _ | Snterml (_, _) | Snext | Sself -> false let insert_level entry_name e1 symbols action slev = match e1 with @@ -341,17 +300,13 @@ Error: entries \"%s\" and \"%s\" do not belong to the same grammar.\n" flush stderr; failwith "Grammar.extend error" end - | Sfacto s -> check_gram entry s - | Smeta (_, sl, _) -> List.iter (check_gram entry) sl | Slist0sep (s, t, _) -> check_gram entry t; check_gram entry s | Slist1sep (s, t, _) -> check_gram entry t; check_gram entry s | Slist0 s -> check_gram entry s | Slist1 s -> check_gram entry s | Sopt s -> check_gram entry s - | Sflag s -> check_gram entry s | Stree t -> tree_check_gram entry t - | Svala (_, s) -> check_gram entry s - | Snext | Sself | Scut | Stoken _ -> () + | Snext | Sself | Stoken _ -> () and tree_check_gram entry = function Node {node = n; brother = bro; son = son} -> @@ -371,16 +326,12 @@ let get_initial entry = let insert_tokens gram symbols = let rec insert = function - Sfacto s -> insert s - | Smeta (_, sl, _) -> List.iter insert sl | 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 - | Sflag s -> insert s | Stree t -> tinsert t - | Svala (_, s) -> insert s | Stoken ("ANY", _) -> () | Stoken tok -> gram.glexer.Plexing.tok_using tok; @@ -389,7 +340,7 @@ let insert_tokens gram symbols = Not_found -> let r = ref 0 in Hashtbl.add gram.gtokens tok r; r in incr r - | Snterm _ | Snterml (_, _) | Snext | Sself | Scut -> () + | Snterm _ | Snterml (_, _) | Snext | Sself -> () and tinsert = function Node {node = s; brother = bro; son = son} -> @@ -507,17 +458,13 @@ let rec decr_keyw_use gram = Hashtbl.remove gram.gtokens tok; gram.glexer.Plexing.tok_removing tok end - | Sfacto s -> decr_keyw_use gram s - | Smeta (_, sl, _) -> List.iter (decr_keyw_use gram) sl | 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 - | Sflag s -> decr_keyw_use gram s | Stree t -> decr_keyw_use_in_tree gram t - | Svala (_, s) -> decr_keyw_use gram s - | Sself | Snext | Scut | Snterm _ | Snterml (_, _) -> () + | Sself | Snext | Snterm _ | Snterml (_, _) -> () and decr_keyw_use_in_tree gram = function DeadEnd | LocAct (_, _) -> () diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli index a76b7da9a2..e888508277 100644 --- a/gramlib/gramext.mli +++ b/gramlib/gramext.mli @@ -25,8 +25,6 @@ and 'te g_level = lprefix : 'te g_tree } and g_assoc = NonA | RightA | LeftA and 'te g_symbol = - Sfacto of 'te g_symbol - | Smeta of string * 'te g_symbol list * Obj.t | Snterm of 'te g_entry | Snterml of 'te g_entry * string | Slist0 of 'te g_symbol @@ -34,13 +32,10 @@ and 'te g_symbol = | Slist1 of 'te g_symbol | Slist1sep of 'te g_symbol * 'te g_symbol * bool | Sopt of 'te g_symbol - | Sflag of 'te g_symbol | Sself | Snext - | Scut | Stoken of Plexing.pattern | Stree of 'te g_tree - | Svala of string list * 'te g_symbol and g_action = Obj.t and 'te g_tree = Node of 'te g_node diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 04ec1049ed..760410894a 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -41,8 +41,6 @@ let print_str ppf s = fprintf ppf "\"%s\"" (string_escaped s) let rec print_symbol ppf = function - Sfacto s -> print_symbol ppf s - | Smeta (n, sl, _) -> print_meta ppf n sl | Slist0 s -> fprintf ppf "LIST0 %a" print_symbol1 s | Slist0sep (s, t, osep) -> fprintf ppf "LIST0 %a SEP %a%s" print_symbol1 s print_symbol1 t @@ -52,42 +50,23 @@ let rec print_symbol ppf = fprintf ppf "LIST1 %a SEP %a%s" print_symbol1 s print_symbol1 t (if osep then " OPT_SEP" else "") | Sopt s -> fprintf ppf "OPT %a" print_symbol1 s - | Sflag s -> fprintf ppf "FLAG %a" print_symbol1 s | Stoken (con, prm) when con <> "" && prm <> "" -> fprintf ppf "%s@ %a" con print_str prm - | Svala (_, s) -> fprintf ppf "V %a" print_symbol s | Snterml (e, l) -> fprintf ppf "%s%s@ LEVEL@ %a" e.ename (if e.elocal then "*" else "") print_str l - | Snterm _ | Snext | Sself | Scut | Stoken _ | Stree _ as s -> + | Snterm _ | Snext | Sself | Stoken _ | Stree _ as s -> print_symbol1 ppf s -and print_meta ppf n sl = - let rec loop i = - function - [] -> () - | s :: sl -> - let j = - try String.index_from n i ' ' with Not_found -> String.length n - in - fprintf ppf "%s %a" (String.sub n i (j - i)) print_symbol1 s; - if sl = [] then () - else - begin fprintf ppf " "; loop (min (j + 1) (String.length n)) sl end - in - loop 0 sl and print_symbol1 ppf = function - Sfacto s -> print_symbol1 ppf s | Snterm e -> fprintf ppf "%s%s" e.ename (if e.elocal then "*" else "") | Sself -> pp_print_string ppf "SELF" | Snext -> pp_print_string ppf "NEXT" - | Scut -> pp_print_string ppf "/" | Stoken ("", s) -> print_str ppf s | Stoken (con, "") -> pp_print_string ppf con | Stree t -> print_level ppf pp_print_space (flatten_tree t) - | Smeta (_, _, _) | Snterml (_, _) | Slist0 _ | Slist0sep (_, _, _) | - Slist1 _ | Slist1sep (_, _, _) | Sopt _ | Sflag _ | Stoken _ | - Svala (_, _) as s -> + | Snterml (_, _) | Slist0 _ | Slist0sep (_, _, _) | + Slist1 _ | Slist1sep (_, _, _) | Sopt _ | Stoken _ as s -> fprintf ppf "(%a)" print_symbol s and print_rule ppf symbols = fprintf ppf "@[<hov 0>"; @@ -162,31 +141,24 @@ let name_of_symbol entry = let rec get_token_list entry rev_tokl last_tok tree = match tree with Node {node = Stoken tok; son = son; brother = DeadEnd} -> - get_token_list entry (last_tok :: rev_tokl) (tok, None) son - | Node {node = Svala (ls, Stoken tok); son = son; brother = DeadEnd} -> - get_token_list entry (last_tok :: rev_tokl) (tok, Some ls) son + get_token_list entry (last_tok :: rev_tokl) tok son | _ -> if rev_tokl = [] then None else Some (rev_tokl, last_tok, tree) let rec name_of_symbol_failed entry = function - Sfacto s -> name_of_symbol_failed entry s | Slist0 s -> name_of_symbol_failed entry s | Slist0sep (s, _, _) -> name_of_symbol_failed entry s | Slist1 s -> name_of_symbol_failed entry s | Slist1sep (s, _, _) -> name_of_symbol_failed entry s | Sopt s -> name_of_symbol_failed entry s - | Sflag s -> name_of_symbol_failed entry s | Stree t -> name_of_tree_failed entry t - | Svala (_, s) -> name_of_symbol_failed entry s - | Smeta (_, s :: _, _) -> name_of_symbol_failed entry s | s -> name_of_symbol entry s and name_of_tree_failed entry = function Node {node = s; brother = bro; son = son} -> let tokl = match s with - Stoken tok -> get_token_list entry [] (tok, None) son - | Svala (ls, Stoken tok) -> get_token_list entry [] (tok, Some ls) son + Stoken tok -> get_token_list entry [] tok son | _ -> None in begin match tokl with @@ -205,7 +177,7 @@ and name_of_tree_failed entry = txt | Some (rev_tokl, last_tok, son) -> List.fold_left - (fun s (tok, _) -> + (fun s tok -> (if s = "" then "" else s ^ " ") ^ entry.egram.glexer.Plexing.tok_text tok) "" (List.rev (last_tok :: rev_tokl)) @@ -318,7 +290,7 @@ 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 _ | Sflag _ | Stree _ | Svala (_, _) -> txt ^ " expected" + | Sopt _ | Stree _ -> txt ^ " expected" | _ -> txt ^ " expected after " ^ name_of_symbol_failed entry prev_symb in if !error_verbose then @@ -426,29 +398,9 @@ let call_and_push ps al strm = let a = ps strm in let al = if !item_skipped then al else a :: al in item_skipped := false; al -let token_ematch gram (tok, vala) = +let token_ematch gram tok = let tematch = gram.glexer.Plexing.tok_match tok in - match vala with - Some al -> - let pa = - match al with - [] -> - let t = "V " ^ fst tok in gram.glexer.Plexing.tok_match (t, "") - | al -> - let rec loop = - function - a :: al -> - let pa = gram.glexer.Plexing.tok_match ("V", a) in - let pal = loop al in - (fun tok -> try pa tok with Stream.Failure -> pal tok) - | [] -> fun tok -> raise Stream.Failure - in - loop al - in - (fun tok -> - try Obj.repr (Ploc.VaAnt (Obj.magic (pa tok : string))) with - Stream.Failure -> Obj.repr (Ploc.VaVal (tematch tok))) - | None -> fun tok -> Obj.repr (tematch tok : string) + fun tok -> Obj.repr (tematch tok : string) let rec parser_of_tree entry nlevn alevn = function @@ -457,8 +409,6 @@ let rec parser_of_tree entry nlevn alevn = | Node {node = Sself; son = LocAct (act, _); brother = DeadEnd} -> (fun (strm__ : _ Stream.t) -> let a = entry.estart alevn strm__ in app act a) - | Node {node = Scut; son = son; brother = _} -> - parser_of_tree entry nlevn alevn son | Node {node = Sself; son = LocAct (act, _); brother = bro} -> let p2 = parser_of_tree entry nlevn alevn bro in (fun (strm__ : _ Stream.t) -> @@ -470,8 +420,7 @@ let rec parser_of_tree entry nlevn alevn = | Node {node = s; son = son; brother = DeadEnd} -> let tokl = match s with - Stoken tok -> get_token_list entry [] (tok, None) son - | Svala (ls, Stoken tok) -> get_token_list entry [] (tok, Some ls) son + Stoken tok -> get_token_list entry [] tok son | _ -> None in begin match tokl with @@ -488,24 +437,18 @@ let rec parser_of_tree entry nlevn alevn = raise (Stream.Error (tree_failed entry a s son)) in app act a) - | Some (rev_tokl, (last_tok, svala), son) -> - let lt = - let t = Stoken last_tok in - match svala with - Some l -> Svala (l, t) - | None -> t - in + | Some (rev_tokl, last_tok, son) -> + 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 (fun (strm__ : _ Stream.t) -> raise Stream.Failure) rev_tokl - (last_tok, svala) + last_tok end | Node {node = s; son = son; brother = bro} -> let tokl = match s with - Stoken tok -> get_token_list entry [] (tok, None) son - | Svala (ls, Stoken tok) -> get_token_list entry [] (tok, Some ls) son + Stoken tok -> get_token_list entry [] tok son | _ -> None in match tokl with @@ -525,18 +468,13 @@ let rec parser_of_tree entry nlevn alevn = | None -> raise (Stream.Error (tree_failed entry a s son)) end | None -> p2 strm) - | Some (rev_tokl, (last_tok, vala), son) -> - let lt = - let t = Stoken last_tok in - match vala with - Some ls -> Svala (ls, t) - | None -> t - in + | Some (rev_tokl, last_tok, son) -> + 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, vala) + parser_of_token_list entry lt son p1 p2 rev_tokl last_tok in fun (strm__ : _ Stream.t) -> try p1 strm__ with Stream.Failure -> p2 strm__ @@ -592,13 +530,6 @@ and parser_of_token_list entry s son p1 p2 rev_tokl last_tok = let a = ps strm__ in let act = p1 strm__ in app act a and parser_of_symbol entry nlevn = function - Sfacto s -> parser_of_symbol entry nlevn s - | Smeta (_, symbl, act) -> - let act = Obj.magic act entry symbl in - Obj.magic - (List.fold_left - (fun act symb -> Obj.magic act (parser_of_symbol entry nlevn symb)) - act symbl) | Slist0 s -> let ps = call_and_push (parser_of_symbol entry nlevn s) in let rec loop al (strm__ : _ Stream.t) = @@ -705,12 +636,6 @@ and parser_of_symbol entry nlevn = match try Some (ps strm__) with Stream.Failure -> None with Some a -> Obj.repr (Some a) | _ -> Obj.repr None) - | Sflag 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 _ -> Obj.repr true - | _ -> Obj.repr false) | Stree t -> let pt = parser_of_tree entry 1 0 t in (fun (strm__ : _ Stream.t) -> @@ -718,46 +643,11 @@ and parser_of_symbol entry nlevn = let a = pt strm__ in let ep = Stream.count strm__ in let loc = loc_of_token_interval bp ep in app a loc) - | Svala (al, s) -> - let pa = - match al with - [] -> - let t = - match s with - Sflag _ -> Some "V FLAG" - | Sopt _ -> Some "V OPT" - | Slist0 _ | Slist0sep (_, _, _) -> Some "V LIST" - | Slist1 _ | Slist1sep (_, _, _) -> Some "V LIST" - | Stoken (con, "") -> Some ("V " ^ con) - | _ -> None - in - begin match t with - Some t -> parser_of_token entry (t, "") - | None -> fun (strm__ : _ Stream.t) -> raise Stream.Failure - end - | al -> - let rec loop = - function - a :: al -> - let pa = parser_of_token entry ("V", a) in - let pal = loop al in - (fun (strm__ : _ Stream.t) -> - try pa strm__ with Stream.Failure -> pal strm__) - | [] -> fun (strm__ : _ Stream.t) -> raise Stream.Failure - in - loop al - in - let ps = parser_of_symbol entry nlevn s in - (fun (strm__ : _ Stream.t) -> - match try Some (pa strm__) with Stream.Failure -> None with - Some a -> Obj.repr (Ploc.VaAnt (Obj.magic a : string)) - | _ -> let a = ps strm__ in Obj.repr (Ploc.VaVal a)) | 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__) - | Scut -> (fun (strm__ : _ Stream.t) -> Obj.repr ()) | Stoken tok -> parser_of_token entry tok and parser_of_token entry tok = let f = entry.egram.glexer.Plexing.tok_match tok in @@ -891,13 +781,6 @@ let delete_rule entry sl = (* Normal interface *) -type token = string * string -type g = token Gramext.grammar - -type ('self, 'a) ty_symbol = token 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 create_toktab () = Hashtbl.create 301 let gcreate glexer = {gtokens = create_toktab (); glexer = glexer } @@ -916,12 +799,6 @@ type 'te gen_parsable = pa_tok_strm : 'te Stream.t; pa_loc_func : Plexing.location_function } -type parsable = token gen_parsable - -let parsable g cs = - let (ts, lf) = g.glexer.Plexing.tok_func cs in - {pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf} - let parse_parsable entry p = let efun = entry.estart 0 in let ts = p.pa_tok_strm in @@ -953,105 +830,6 @@ let parse_parsable entry p = let loc = Stream.count cs, Stream.count cs + 1 in restore (); Ploc.raise (Ploc.make_unlined loc) exc -let find_entry e s = - let rec find_levels = - function - [] -> None - | lev :: levs -> - match find_tree lev.lsuffix with - None -> - begin match find_tree lev.lprefix with - None -> find_levels levs - | x -> x - end - | x -> x - and find_symbol = - function - Sfacto s -> find_symbol s - | Snterm e -> if e.ename = s then Some e else None - | Snterml (e, _) -> if e.ename = s then Some e else None - | Smeta (_, sl, _) -> find_symbol_list sl - | Slist0 s -> find_symbol s - | Slist0sep (s, _, _) -> find_symbol s - | Slist1 s -> find_symbol s - | Slist1sep (s, _, _) -> find_symbol s - | Sopt s -> find_symbol s - | Sflag s -> find_symbol s - | Stree t -> find_tree t - | Svala (_, s) -> find_symbol s - | Sself | Snext | Scut | Stoken _ -> None - and find_symbol_list = - function - s :: sl -> - begin match find_symbol s with - None -> find_symbol_list sl - | x -> x - end - | [] -> None - and find_tree = - function - Node {node = s; brother = bro; son = son} -> - begin match find_symbol s with - None -> - begin match find_tree bro with - None -> find_tree son - | x -> x - end - | x -> x - end - | LocAct (_, _) | DeadEnd -> None - in - match e.edesc with - Dlevels levs -> - begin match find_levels levs with - Some e -> e - | None -> raise Not_found - end - | Dparser _ -> raise Not_found -module Entry = - struct - type te = token - type 'a e = te g_entry - let create g n = - {egram = g; ename = n; elocal = false; estart = empty_entry n; - econtinue = (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure); - edesc = Dlevels []} - let parse_parsable (entry : 'a e) p : 'a = - Obj.magic (parse_parsable entry p : Obj.t) - let parse (entry : 'a e) cs : 'a = - let parsable = parsable entry.egram cs in parse_parsable entry parsable - let parse_parsable_all (entry : 'a e) p : 'a = - begin try Obj.magic [(parse_parsable entry p : Obj.t)] with - Stream.Failure | Stream.Error _ -> [] - end - let parse_all (entry : 'a e) cs : 'a = - let parsable = parsable entry.egram cs in - parse_parsable_all entry parsable - let parse_token_stream (entry : 'a e) ts : 'a = - Obj.magic (entry.estart 0 ts : Obj.t) - let _warned_using_parse_token = ref false - let parse_token (entry : 'a e) ts : 'a = - (* commented: too often warned in Coq... - if not warned_using_parse_token.val then do { - eprintf "<W> use of Grammar.Entry.parse_token "; - eprintf "deprecated since 2017-06-16\n%!"; - eprintf "use Grammar.Entry.parse_token_stream instead\n%! "; - warned_using_parse_token.val := True - } - else (); - *) - parse_token_stream entry ts - let name e = e.ename - let of_parser g n (p : te Stream.t -> 'a) : 'a e = - {egram = g; ename = n; elocal = false; - estart = (fun _ -> (Obj.magic p : te Stream.t -> Obj.t)); - econtinue = (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure); - edesc = Dparser (Obj.magic p : te Stream.t -> Obj.t)} - external obj : 'a e -> te Gramext.g_entry = "%identity" - let print ppf e = fprintf ppf "%a@." print_entry (obj e) - let find e s = find_entry (obj e) s - end - (* Unsafe *) let clear_entry e = @@ -1063,12 +841,6 @@ let clear_entry e = let gram_reinit g glexer = Hashtbl.clear g.gtokens; g.glexer <- glexer -module Unsafe = - struct - let gram_reinit = gram_reinit - let clear_entry = clear_entry - end - (* Functorial interface *) module type GLexerType = sig type te val lexer : te Plexing.lexer end @@ -1095,7 +867,6 @@ module type S = type ('self, 'a) ty_symbol type ('self, 'f, 'r) ty_rule type 'a ty_production - val s_facto : ('self, 'a) ty_symbol -> ('self, 'a) ty_symbol 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 @@ -1107,18 +878,14 @@ module type S = ('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_flag : ('self, 'a) ty_symbol -> ('self, bool) 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 : 'a ty_production list -> ('self, 'a) ty_symbol - val s_vala : - string list -> ('self, 'a) ty_symbol -> ('self, 'a Ploc.vala) 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 r_cut : ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule val production : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f -> 'a ty_production module Unsafe : sig @@ -1187,7 +954,6 @@ module GMake (L : GLexerType) = 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_facto s = Sfacto s let s_nterm e = Snterm e let s_nterml e l = Snterml (e, l) let s_list0 s = Slist0 s @@ -1195,15 +961,12 @@ module GMake (L : GLexerType) = let s_list1 s = Slist1 s let s_list1sep s sep b = Slist1sep (s, sep, b) let s_opt s = Sopt s - let s_flag s = Sflag s let s_self = Sself let s_next = Snext let s_token tok = Stoken tok let s_rules (t : Obj.t ty_production list) = Gramext.srules (Obj.magic t) - let s_vala sl s = Svala (sl, s) let r_stop = [] let r_next r s = r @ [s] - let r_cut r = r @ [Scut] let production (p : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f) : 'a ty_production = Obj.magic p diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 54b7eb5539..244ab710dc 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -8,77 +8,6 @@ Grammars entries can be extended using the [EXTEND] statement, added by loading the Camlp5 [pa_extend.cmo] file. *) -type g - (** The type for grammars, holding entries. *) -type token = string * string - -type parsable -val parsable : g -> char Stream.t -> parsable - (** Type and value allowing to keep the same token stream between - several calls of entries of the same grammar, to prevent possible - loss of tokens. To be used with [Entry.parse_parsable] below *) - -module Entry : - sig - type 'a e - val create : g -> string -> 'a e - val parse : 'a e -> char Stream.t -> 'a - val parse_all : 'a e -> char Stream.t -> 'a list - val parse_parsable : 'a e -> parsable -> 'a - val name : 'a e -> string - val of_parser : g -> string -> (token Stream.t -> 'a) -> 'a e - val parse_token_stream : 'a e -> token Stream.t -> 'a - val print : Format.formatter -> 'a e -> unit - val find : 'a e -> string -> Obj.t e - external obj : 'a e -> token Gramext.g_entry = "%identity" - val parse_token : 'a e -> token Stream.t -> 'a - end - (** Module to handle entries. -- [Entry.e] is the type for entries returning values of type ['a]. -- [Entry.create g n] creates a new entry named [n] in the grammar [g]. -- [Entry.parse e] returns the stream parser of the entry [e]. -- [Entry.parse_all e] returns the stream parser returning all possible - values while parsing with the entry [e]: may return more than one - value when the parsing algorithm is [Backtracking] -- [Entry.parse_all e] returns the parser returning all possible values. -- [Entry.parse_parsable e] returns the parsable parser of the entry [e]. -- [Entry.name e] returns the name of the entry [e]. -- [Entry.of_parser g n p] makes an entry from a token stream parser. -- [Entry.parse_token_stream e] returns the token stream parser of the - entry [e]. -- [Entry.print e] displays the entry [e] using [Format]. -- [Entry.find e s] finds the entry named [s] in the rules of [e]. -- [Entry.obj e] converts an entry into a [Gramext.g_entry] allowing - to see what it holds. -- [Entry.parse_token]: deprecated since 2017-06-16; old name for - [Entry.parse_token_stream] *) - -type ('self, 'a) ty_symbol -(** Type of grammar symbols. A type-safe wrapper around Gramext.symbol. The - first type argument is the type of the ambient entry, the second one is the - type of the produced value. *) - -type ('self, 'f, 'r) ty_rule - -type 'a ty_production - -(** {6 Clearing grammars and entries} *) - -module Unsafe : - sig - val gram_reinit : g -> token Plexing.lexer -> unit - val clear_entry : 'a Entry.e -> unit - end - (** Module for clearing grammars and entries. To be manipulated with - care, because: 1) reinitializing a grammar destroys all tokens - and there may have problems with the associated lexer if there - are keywords; 2) clearing an entry does not destroy the tokens - used only by itself. -- [Unsafe.reinit_gram g lex] removes the tokens of the grammar -- and sets [lex] as a new lexer for [g]. Warning: the lexer -- itself is not reinitialized. -- [Unsafe.clear_entry e] removes all rules of the entry [e]. *) - (** {6 Functorial interface} *) (** Alternative for grammars use. Grammars are no more Ocaml values: @@ -112,7 +41,6 @@ module type S = type ('self, 'a) ty_symbol type ('self, 'f, 'r) ty_rule type 'a ty_production - val s_facto : ('self, 'a) ty_symbol -> ('self, 'a) ty_symbol 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 @@ -124,18 +52,14 @@ module type S = ('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_flag : ('self, 'a) ty_symbol -> ('self, bool) 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 : 'a ty_production list -> ('self, 'a) ty_symbol - val s_vala : - string list -> ('self, 'a) ty_symbol -> ('self, 'a Ploc.vala) 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 r_cut : ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule val production : ('a, 'f, Ploc.t -> 'a) ty_rule * 'f -> 'a ty_production module Unsafe : diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml index beebcd016e..986363ec1f 100644 --- a/gramlib/plexing.ml +++ b/gramlib/plexing.ml @@ -17,201 +17,3 @@ type 'te lexer = mutable tok_match : pattern -> 'te -> string; tok_text : pattern -> string; mutable tok_comm : location list option } - -let make_loc = Ploc.make_unlined -let dummy_loc = Ploc.dummy - -let lexer_text (con, prm) = - if con = "" then "'" ^ prm ^ "'" - else if prm = "" then con - else con ^ " '" ^ prm ^ "'" - -let locerr () = failwith "Lexer: location function" -let loct_create () = ref (Array.make 1024 None), ref false -let loct_func (loct, ov) i = - match - if i < 0 || i >= Array.length !loct then - if !ov then Some dummy_loc else None - else Array.unsafe_get !loct i - with - Some loc -> loc - | None -> locerr () -let loct_add (loct, ov) i loc = - if i >= Array.length !loct then - let new_tmax = Array.length !loct * 2 in - if new_tmax < Sys.max_array_length then - let new_loct = Array.make new_tmax None in - Array.blit !loct 0 new_loct 0 (Array.length !loct); - loct := new_loct; - !loct.(i) <- Some loc - else ov := true - else !loct.(i) <- Some loc - -let make_stream_and_location next_token_loc = - let loct = loct_create () in - let ts = - Stream.from - (fun i -> - let (tok, loc) = next_token_loc () in loct_add loct i loc; Some tok) - in - ts, loct_func loct - -let lexer_func_of_parser next_token_loc cs = - let line_nb = ref 1 in - let bolpos = ref 0 in - make_stream_and_location (fun () -> next_token_loc (cs, line_nb, bolpos)) - -let lexer_func_of_ocamllex lexfun cs = - let lb = - Lexing.from_function - (fun s n -> - try Bytes.set s 0 (Stream.next cs); 1 with Stream.Failure -> 0) - in - let next_token_loc _ = - let tok = lexfun lb in - let loc = make_loc (Lexing.lexeme_start lb, Lexing.lexeme_end lb) in - tok, loc - in - make_stream_and_location next_token_loc - -(* Char and string tokens to real chars and string *) - -let buff = ref (Bytes.create 80) -let store len x = - if len >= Bytes.length !buff then - buff := Bytes.(cat !buff (create (length !buff))); - Bytes.set !buff len x; - succ len -let get_buff len = Bytes.sub !buff 0 len - -let valch x = Char.code x - Char.code '0' -let valch_a x = Char.code x - Char.code 'a' + 10 -let valch_A x = Char.code x - Char.code 'A' + 10 - -let rec backslash s i = - if i = String.length s then raise Not_found - else - match s.[i] with - 'n' -> '\n', i + 1 - | 'r' -> '\r', i + 1 - | 't' -> '\t', i + 1 - | 'b' -> '\b', i + 1 - | '\\' -> '\\', i + 1 - | '"' -> '"', i + 1 - | '\'' -> '\'', i + 1 - | '0'..'9' as c -> backslash1 (valch c) s (i + 1) - | 'x' -> backslash1h s (i + 1) - | _ -> raise Not_found -and backslash1 cod s i = - if i = String.length s then '\\', i - 1 - else - match s.[i] with - '0'..'9' as c -> backslash2 (10 * cod + valch c) s (i + 1) - | _ -> '\\', i - 1 -and backslash2 cod s i = - if i = String.length s then '\\', i - 2 - else - match s.[i] with - '0'..'9' as c -> Char.chr (10 * cod + valch c), i + 1 - | _ -> '\\', i - 2 -and backslash1h s i = - if i = String.length s then '\\', i - 1 - else - match s.[i] with - '0'..'9' as c -> backslash2h (valch c) s (i + 1) - | 'a'..'f' as c -> backslash2h (valch_a c) s (i + 1) - | 'A'..'F' as c -> backslash2h (valch_A c) s (i + 1) - | _ -> '\\', i - 1 -and backslash2h cod s i = - if i = String.length s then '\\', i - 2 - else - match s.[i] with - '0'..'9' as c -> Char.chr (16 * cod + valch c), i + 1 - | 'a'..'f' as c -> Char.chr (16 * cod + valch_a c), i + 1 - | 'A'..'F' as c -> Char.chr (16 * cod + valch_A c), i + 1 - | _ -> '\\', i - 2 - -let rec skip_indent s i = - if i = String.length s then i - else - match s.[i] with - ' ' | '\t' -> skip_indent s (i + 1) - | _ -> i - -let skip_opt_linefeed s i = - if i = String.length s then i else if s.[i] = '\010' then i + 1 else i - -let eval_char s = - if String.length s = 1 then s.[0] - else if String.length s = 0 then failwith "invalid char token" - else if s.[0] = '\\' then - if String.length s = 2 && s.[1] = '\'' then '\'' - else - try - let (c, i) = backslash s 1 in - if i = String.length s then c else raise Not_found - with Not_found -> failwith "invalid char token" - else failwith "invalid char token" - -let eval_string loc s = - let rec loop len i = - if i = String.length s then get_buff len - else - let (len, i) = - if s.[i] = '\\' then - let i = i + 1 in - if i = String.length s then failwith "invalid string token" - else if s.[i] = '"' then store len '"', i + 1 - else - match s.[i] with - '\010' -> len, skip_indent s (i + 1) - | '\013' -> len, skip_indent s (skip_opt_linefeed s (i + 1)) - | c -> - try let (c, i) = backslash s i in store len c, i with - Not_found -> store (store len '\\') c, i + 1 - else store len s.[i], i + 1 - in - loop len i - in - Bytes.to_string (loop 0 0) - -let default_match = - function - "ANY", "" -> (fun (con, prm) -> prm) - | "ANY", v -> - (fun (con, prm) -> if v = prm then v else raise Stream.Failure) - | p_con, "" -> - (fun (con, prm) -> if con = p_con then prm else raise Stream.Failure) - | p_con, p_prm -> - fun (con, prm) -> - if con = p_con && prm = p_prm then prm else raise Stream.Failure - -let input_file = ref "" -let line_nb = ref (ref 0) -let bol_pos = ref (ref 0) -let restore_lexing_info = ref None - -(* The lexing buffer used by pa_lexer.cmo *) - -let rev_implode l = - let s = Bytes.create (List.length l) in - let rec loop i = - function - c :: l -> Bytes.unsafe_set s i c; loop (i - 1) l - | [] -> s - in - Bytes.to_string (loop (Bytes.length s - 1) l) - -module Lexbuf : - sig - type t - val empty : t - val add : char -> t -> t - val get : t -> string - end = - struct - type t = char list - let empty = [] - let add c l = c :: l - let get = rev_implode - end diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli index 6b5f718bc3..96b432a8ad 100644 --- a/gramlib/plexing.mli +++ b/gramlib/plexing.mli @@ -35,74 +35,3 @@ and 'te lexer_func = char Stream.t -> 'te Stream.t * location_function and location_function = int -> Ploc.t (** The type of a function giving the location of a token in the source from the token number in the stream (starting from zero). *) - -val lexer_text : pattern -> string - (** A simple [tok_text] function. *) - -val default_match : pattern -> string * string -> string - (** A simple [tok_match] function, appling to the token type - [(string * string)] *) - -(** Lexers from parsers or ocamllex - - The functions below create lexer functions either from a [char stream] - parser or for an [ocamllex] function. With the returned function [f], - it is possible to get a simple lexer (of the type [Plexing.glexer] above): - {[ - { Plexing.tok_func = f; - Plexing.tok_using = (fun _ -> ()); - Plexing.tok_removing = (fun _ -> ()); - Plexing.tok_match = Plexing.default_match; - Plexing.tok_text = Plexing.lexer_text; - Plexing.tok_comm = None } - ]} - Note that a better [tok_using] function should check the used tokens - and raise [Plexing.Error] for incorrect ones. The other functions - [tok_removing], [tok_match] and [tok_text] may have other implementations - as well. *) - -val lexer_func_of_parser : - (char Stream.t * int ref * int ref -> 'te * Ploc.t) -> 'te lexer_func - (** A lexer function from a lexer written as a char stream parser - returning the next token and its location. The two references - with the char stream contain the current line number and the - position of the beginning of the current line. *) -val lexer_func_of_ocamllex : (Lexing.lexbuf -> 'te) -> 'te lexer_func - (** A lexer function from a lexer created by [ocamllex] *) - -(** Function to build a stream and a location function *) - -val make_stream_and_location : - (unit -> 'te * Ploc.t) -> 'te Stream.t * location_function - (** General function *) - -(** Useful functions and values *) - -val eval_char : string -> char -val eval_string : Ploc.t -> string -> string - (** Convert a char or a string token, where the backslashes had not - been interpreted into a real char or string; raise [Failure] if - bad backslash sequence found; [Plexing.eval_char (Char.escaped c)] - would return [c] and [Plexing.eval_string (String.escaped s)] would - return [s] *) - -val restore_lexing_info : (int * int) option ref -val input_file : string ref -val line_nb : int ref ref -val bol_pos : int ref ref - (** Special variables used to reinitialize line numbers and position - of beginning of line with their correct current values when a parser - is called several times with the same character stream. Necessary - for directives (e.g. #load or #use) which interrupt the parsing. - Without usage of these variables, locations after the directives - can be wrong. *) - -(** The lexing buffer used by streams lexers *) - -module Lexbuf : - sig - type t - val empty : t - val add : char -> t -> t - val get : t -> string - end diff --git a/gramlib/ploc.ml b/gramlib/ploc.ml index cb71f72678..082686db01 100644 --- a/gramlib/ploc.ml +++ b/gramlib/ploc.ml @@ -55,122 +55,9 @@ let sub loc sh len = {loc with bp = loc.bp + sh; ep = loc.bp + sh + len} let after loc sh len = {loc with bp = loc.ep + sh; ep = loc.ep + sh + len} let with_comment loc comm = {loc with comm = comm} -let name = ref "loc" - -let from_file fname loc = - let (bp, ep) = first_pos loc, last_pos loc in - try - let ic = open_in_bin fname in - let strm = Stream.of_channel ic in - let rec loop fname lin = - let rec not_a_line_dir col (strm__ : _ Stream.t) = - let cnt = Stream.count strm__ in - match Stream.peek strm__ with - Some c -> - Stream.junk strm__; - let s = strm__ in - if cnt < bp then - if c = '\n' then loop fname (lin + 1) - else not_a_line_dir (col + 1) s - else let col = col - (cnt - bp) in fname, lin, col, col + ep - bp - | _ -> fname, lin, col, col + 1 - in - let rec a_line_dir str n col (strm__ : _ Stream.t) = - match Stream.peek strm__ with - Some '\n' -> Stream.junk strm__; loop str n - | Some _ -> Stream.junk strm__; a_line_dir str n (col + 1) strm__ - | _ -> raise Stream.Failure - in - let rec spaces col (strm__ : _ Stream.t) = - match Stream.peek strm__ with - Some ' ' -> Stream.junk strm__; spaces (col + 1) strm__ - | _ -> col - in - let rec check_string str n col (strm__ : _ Stream.t) = - match Stream.peek strm__ with - Some '"' -> - Stream.junk strm__; - let col = - try spaces (col + 1) strm__ with - Stream.Failure -> raise (Stream.Error "") - in - a_line_dir str n col strm__ - | Some c when c <> '\n' -> - Stream.junk strm__; - check_string (str ^ String.make 1 c) n (col + 1) strm__ - | _ -> not_a_line_dir col strm__ - in - let check_quote n col (strm__ : _ Stream.t) = - match Stream.peek strm__ with - Some '"' -> Stream.junk strm__; check_string "" n (col + 1) strm__ - | _ -> not_a_line_dir col strm__ - in - let rec check_num n col (strm__ : _ Stream.t) = - match Stream.peek strm__ with - Some ('0'..'9' as c) -> - Stream.junk strm__; - check_num (10 * n + Char.code c - Char.code '0') (col + 1) strm__ - | _ -> let col = spaces col strm__ in check_quote n col strm__ - in - let begin_line (strm__ : _ Stream.t) = - match Stream.peek strm__ with - Some '#' -> - Stream.junk strm__; - let col = - try spaces 1 strm__ with - Stream.Failure -> raise (Stream.Error "") - in - check_num 0 col strm__ - | _ -> not_a_line_dir 0 strm__ - in - begin_line strm - in - let r = - try loop fname 1 with - Stream.Failure -> - let bol = bol_pos loc in fname, line_nb loc, bp - bol, ep - bol - in - close_in ic; r - with Sys_error _ -> fname, 1, bp, ep - -let second_line fname ep0 (line, bp) ep = - let ic = open_in fname in - seek_in ic bp; - let rec loop line bol p = - if p = ep then - begin close_in ic; if bol = bp then line, ep0 else line, ep - bol end - else - let (line, bol) = - match input_char ic with - '\n' -> line + 1, p + 1 - | _ -> line, bol - in - loop line bol (p + 1) - in - loop line bp bp - -let get loc = - if loc.fname = "" || loc.fname = "-" then - loc.line_nb, loc.bp - loc.bol_pos, loc.line_nb, loc.ep - loc.bol_pos, - loc.ep - loc.bp - else - let (bl, bc, ec) = - loc.line_nb, loc.bp - loc.bol_pos, loc.ep - loc.bol_pos - in - let (el, eep) = second_line loc.fname ec (bl, loc.bp) loc.ep in - bl, bc, el, eep, ec - bc - -let call_with r v f a = - let saved = !r in - try r := v; let b = f a in r := saved; b with e -> r := saved; raise e - exception Exc of t * exn let raise loc exc = match exc with Exc (_, _) -> raise exc | _ -> raise (Exc (loc, exc)) - -type 'a vala = - VaAnt of string - | VaVal of 'a diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli index d2ab62db06..2ce6382183 100644 --- a/gramlib/ploc.mli +++ b/gramlib/ploc.mli @@ -84,39 +84,3 @@ val after : t -> int -> int -> t [len]. *) val with_comment : t -> string -> t (** Change the comment part of the given location *) - -(* miscellaneous *) - -val name : string ref - (** [Ploc.name.val] is the name of the location variable used in grammars - and in the predefined quotations for OCaml syntax trees. Default: - ["loc"] *) - -val get : t -> int * int * int * int * int - (** [Ploc.get loc] returns in order: 1/ the line number of the begin - of the location, 2/ its column, 3/ the line number of the first - character not in the location, 4/ its column and 5/ the length - of the location. The file where the location occurs (if any) may - be read during this operation. *) - -val from_file : string -> t -> string * int * int * int - (** [Ploc.from_file fname loc] reads the file [fname] up to the - location [loc] and returns the real input file, the line number - and the characters location in the line; the real input file - can be different from [fname] because of possibility of line - directives typically generated by /lib/cpp. *) - -(* pervasives *) - -type 'a vala = - VaAnt of string - | VaVal of 'a - (** Encloser of many abstract syntax tree nodes types, in "strict" mode. - This allow the system of antiquotations of abstract syntax tree - quotations to work when using the quotation kit [q_ast.cmo]. *) - -val call_with : 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c - (** [Ploc.call_with r v f a] sets the reference [r] to the value [v], - then call [f a], and resets [r] to its initial value. If [f a] raises - an exception, its initial value is also reset and the exception is - re-raised. The result is the result of [f a]. *) diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 6ba937a2ff..a786b9953d 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -84,7 +84,7 @@ type ssripat = | IPatId of (*TODO id_mod option * *) Id.t | IPatAnon of anon_iter (* inaccessible name *) (* TODO | IPatClearMark *) - | IPatDispatch of ssripatss (* /[..|..] *) + | IPatDispatch of bool (* ssr exception: accept a dispatch on the empty list even when there are subgoals *) * ssripatss (* (..|..) *) | IPatCase of (* ipats_mod option * *) ssripatss (* this is not equivalent to /case /[..|..] if there are already multiple goals *) | IPatInj of ssripatss | IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 5d75b28539..ebe4aac213 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -800,7 +800,7 @@ let rec is_name_in_ipats name = function | IPatId id :: tl -> id = name || is_name_in_ipats name tl | IPatAbstractVars ids :: tl -> CList.mem_f Id.equal name ids || is_name_in_ipats name tl - | (IPatCase l | IPatDispatch l | IPatInj l) :: tl -> + | (IPatCase l | IPatDispatch (_,l) | IPatInj l) :: tl -> List.exists (is_name_in_ipats name) l || is_name_in_ipats name tl | (IPatView _ | IPatAnon _ | IPatSimpl _ | IPatRewrite _ | IPatTac _ | IPatNoop) :: tl -> is_name_in_ipats name tl | [] -> false diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index ce439d0497..0553260472 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -216,8 +216,11 @@ let rec ipat_tac1 ipat : unit tactic = | IPatView (clear_if_id,l) -> Ssrview.tclIPAT_VIEWS ~views:l ~clear_if_id ~conclusion:(fun ~to_clear:clr -> intro_clear clr) - | IPatDispatch ipatss -> - tclEXTEND (List.map ipat_tac ipatss) (tclUNIT ()) [] + + | IPatDispatch(true,[[]]) -> + tclUNIT () + | IPatDispatch(_,ipatss) -> + tclDISPATCH (List.map ipat_tac ipatss) | IPatId id -> Ssrcommon.tclINTRO_ID id @@ -275,7 +278,7 @@ let split_at_first_case ipats = loop [] ipats let ssr_exception is_on = function - | Some (IPatCase l) when is_on -> Some (IPatDispatch l) + | Some (IPatCase l) when is_on -> Some (IPatDispatch(true, l)) | x -> x let option_to_list = function None -> [] | Some x -> [x] @@ -285,7 +288,7 @@ let elaborate_ipats l = let rec elab = function | [] -> [] | (IPatClear _ as p1) :: (IPatView _ as p2) :: rest -> p2 :: p1 :: elab rest - | IPatDispatch p :: rest -> IPatDispatch (List.map elab p) :: elab rest + | IPatDispatch(s,p) :: rest -> IPatDispatch (s,List.map elab p) :: elab rest | IPatCase p :: rest -> IPatCase (List.map elab p) :: elab rest | IPatInj p :: rest -> IPatInj (List.map elab p) :: elab rest | (IPatTac _ | IPatId _ | IPatSimpl _ | IPatClear _ | diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 8699b62c39..52240f5896 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -632,7 +632,7 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function | IPatAbstractVars l -> IPatAbstractVars (List.map map_id l) | IPatClear clr -> IPatClear (List.map map_ssrhyp clr) | IPatCase iorpat -> IPatCase (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) - | IPatDispatch iorpat -> IPatDispatch (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) + | IPatDispatch (s,iorpat) -> IPatDispatch (s,List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) | IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v) | IPatTac _ -> assert false (*internal usage only *) @@ -697,8 +697,8 @@ let interp_ipat ist gl = check_hyps_uniq [] clr'; IPatClear clr' | IPatCase(iorpat) -> IPatCase(List.map (List.map interp) iorpat) - | IPatDispatch(iorpat) -> - IPatDispatch(List.map (List.map interp) iorpat) + | IPatDispatch(s,iorpat) -> + IPatDispatch(s,List.map (List.map interp) iorpat) | IPatInj iorpat -> IPatInj (List.map (List.map interp) iorpat) | IPatAbstractVars l -> IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist gl) l)) diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 8f4b2179e1..824666ba9c 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -101,7 +101,7 @@ let rec pr_ipat p = | IPatSimpl sim -> pr_simpl sim | IPatClear clr -> pr_clear mt clr | IPatCase iorpat -> hov 1 (str "[" ++ pr_iorpat iorpat ++ str "]") - | IPatDispatch iorpat -> hov 1 (str "/[" ++ pr_iorpat iorpat ++ str "]") + | IPatDispatch(_,iorpat) -> hov 1 (str "/[" ++ pr_iorpat iorpat ++ str "]") | IPatInj iorpat -> hov 1 (str "[=" ++ pr_iorpat iorpat ++ str "]") | IPatRewrite (occ, dir) -> pr_occ occ ++ pr_dir dir | IPatAnon All -> str "*" diff --git a/test-suite/bugs/closed/bug_8544.v b/test-suite/bugs/closed/bug_8544.v new file mode 100644 index 0000000000..674d112595 --- /dev/null +++ b/test-suite/bugs/closed/bug_8544.v @@ -0,0 +1,6 @@ +Require Import ssreflect. +Goal True \/ True -> False. +Proof. +(* the following should fail: 2 subgoals, but only one intro pattern *) +Fail case => [a]. +Abort. diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index f94da14cd0..84850e7158 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -175,8 +175,10 @@ let pp_vo_dep dir fmt vo = let deps = List.map (fun s -> bpath [sdir;s]) (edep @ vo.deps) in (* The source file is also corrected as we will call coqtop from the top dir *) let source = bpath (dir @ [Filename.(remove_extension vo.target) ^ ".v"]) in + (* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *) + let libflag = "-coqlib %{project_root}" in (* The final build rule *) - let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s -compile %s))" eflag cflag source in + let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s %s -compile %s))" libflag eflag cflag source in pp_rule fmt [vo.target] deps action let pp_ml4_dep _dir fmt ml = |