From 62f6fb862ce4f3eec46200d11e503aa5d6d051db Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 13 Nov 2019 17:18:06 +0100 Subject: Documenting plugin/tactic/stdlib keywords in corresponding chapters. Incidentally removing "discriminated", "(bfs)" and "(dfs)" from keywords. It is enough to make them normal identifiers. Note: - keywords reserved by the tactics are: ** [= _eqn |- by using - keywords reserved by ltac are: lazymatch multimatch || --- doc/sphinx/language/core/basic.rst | 8 ++++---- plugins/ltac/g_class.mlg | 15 +++++++++++---- vernac/g_proofs.mlg | 2 +- 3 files changed, 16 insertions(+), 9 deletions(-) diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 9473cc5a15..3940242bb3 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -134,7 +134,7 @@ Keywords used as identifiers:: _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop - SProp Set Theorem Type Variable as at cofix discriminated else end + SProp Set Theorem Type Variable as at cofix else end fix for forall fun if in let match return then where with Note that notations and plugins may define additional keywords. @@ -150,10 +150,10 @@ Other tokens Here are the character sequences that |Coq| directly defines as tokens without using :cmd:`Notation`:: - ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - -> + ! #[ % & ' ( () ) * + , - -> . .( .. ... / : ::= := :> :>> ; < <+ <- <: - <<: <= = => > >-> >= ? @ @{ [ [= ] _ - `( `{ { {| | |- || } + <<: <= = => > >-> >= ? @ @{ [ ] _ + `( `{ { {| | } When multiple tokens match the beginning of a sequence of characters, the longest matching token is used. diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 0f0341f123..81e745b714 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -54,16 +54,23 @@ END { +let pr_search_strategy_name _prc _prlc _prt = function + | Dfs -> Pp.str "dfs" + | Bfs -> Pp.str "bfs" + let pr_search_strategy _prc _prlc _prt = function - | Some Dfs -> Pp.str "dfs" - | Some Bfs -> Pp.str "bfs" + | Some s -> pr_search_strategy_name _prc _prlc _prt s | None -> Pp.mt () } +ARGUMENT EXTEND eauto_search_strategy_name PRINTED BY { pr_search_strategy_name } +| [ "bfs" ] -> { Bfs } +| [ "dfs" ] -> { Dfs } +END + ARGUMENT EXTEND eauto_search_strategy PRINTED BY { pr_search_strategy } -| [ "(bfs)" ] -> { Some Bfs } -| [ "(dfs)" ] -> { Some Dfs } +| [ "(" eauto_search_strategy_name(s) ")" ] -> { Some s } | [ ] -> { None } END diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index e84fce5504..f2a1dce01d 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -98,7 +98,7 @@ GRAMMAR EXTEND Gram | IDENT "Guarded" -> { VernacCheckGuard } (* Hints for Auto and EAuto *) | IDENT "Create"; IDENT "HintDb" ; - id = IDENT ; b = [ "discriminated" -> { true } | -> { false } ] -> + id = IDENT ; b = [ IDENT "discriminated" -> { true } | -> { false } ] -> { VernacCreateHintDb (id, b) } | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> { VernacRemoveHints (dbnames, ids) } -- cgit v1.2.3 From 259162be000a8a66bf4f551be64d6a5d61edce05 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 13 Nov 2019 18:19:44 +0100 Subject: Mention keywords used in tactics from g_tactic.mlg. --- doc/sphinx/proof-engine/tactics.rst | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 8989dd29ab..78ac7d00dd 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -36,6 +36,18 @@ language will be described in Chapter :ref:`ltac`. Common elements of tactics -------------------------- +Reserved keywords +~~~~~~~~~~~~~~~~~ + +The tactics described in this chapter reserve the following keywords:: + + by using + +Thus, these keywords cannot be used as identifiers. It also declares +the following character sequences as tokens:: + + ** [= |- + .. _invocation-of-tactics: Invocation of tactics -- cgit v1.2.3 From 986bfd1ff69231f1b17efda2fa5d13b88a39caee Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 13 Nov 2019 20:54:52 +0100 Subject: Mention keywords from g_ltac.mlg used in Ltac. --- doc/sphinx/proof-engine/ltac.rst | 3 +++ 1 file changed, 3 insertions(+) diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index b184311bef..dc994fe863 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -57,6 +57,9 @@ mode but it can also be used in toplevel definitions as shown below. .. note:: + - The grammar reserves the keywords ``lazymatch`` and + ``multimatch`` as well as the token ``||``. + - The infix tacticals  ``… || …`` ,  ``… + …`` , and  ``… ; …``  are associative. .. example:: -- cgit v1.2.3 From 86cdd51c4e25fceb12854863419fbdc3f19e44aa Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 16 Nov 2019 11:03:49 +0100 Subject: Stop keeping outdated static list of keywords. The real list is computed by tok_using in CLexer. --- parsing/g_constr.mlg | 10 ---------- parsing/g_prim.mlg | 4 ---- plugins/ltac/g_tactic.mlg | 3 --- vernac/g_vernac.mlg | 3 --- 4 files changed, 20 deletions(-) diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 963f029766..c19dd00b38 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -26,16 +26,6 @@ open Pcoq.Constr (* TODO: avoid this redefinition without an extra dep to Notation_ops *) let ldots_var = Id.of_string ".." -let constr_kw = - [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; - "end"; "as"; "let"; "if"; "then"; "else"; "return"; - "SProp"; "Prop"; "Set"; "Type"; - ":="; "=>"; "->"; ".."; "<:"; "<<:"; ":>"; - ".("; "()"; "`{"; "`("; "@{"; "{|"; - "_"; "@"; "+"; "!"; "?"; ";"; ","; ":" ] - -let _ = List.iter CLexer.add_keyword constr_kw - let mk_cast = function (c,(_,None)) -> c | (c,(_,Some ty)) -> diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 9c50109bb3..1b5b5c91ca 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -15,10 +15,6 @@ open Libnames open Pcoq.Prim -let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"; "%"; "|"] -let _ = List.iter CLexer.add_keyword prim_kw - - let local_make_qualid loc l id = make_qualid ~loc (DirPath.make l) id let my_int_of_string ?loc s = diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 6a158bde17..e51b1f051d 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -30,9 +30,6 @@ open Pcoq let all_with delta = Redops.make_red_flag [FBeta;FMatch;FFix;FCofix;FZeta;delta] -let tactic_kw = [ "->"; "<-" ; "by" ] -let _ = List.iter CLexer.add_keyword tactic_kw - let err () = raise Stream.Failure (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 13145d3757..5b68a41c6a 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -30,9 +30,6 @@ open Pcoq.Module open Pvernac.Vernac_ open Attributes -let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ] -let _ = List.iter CLexer.add_keyword vernac_kw - (* Rem: do not join the different GEXTEND into one, it breaks native *) (* compilation on PowerPC and Sun architectures *) -- cgit v1.2.3 From 20f0e2efb87541e511cf31e220a44e4376c44550 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 2 May 2020 23:22:48 +0200 Subject: Moving lazymatch and multimatch to simple identifiers. --- doc/sphinx/proof-engine/ltac.rst | 3 +-- plugins/ltac/g_ltac.mlg | 4 ++-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index dc994fe863..90173d65bf 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -57,8 +57,7 @@ mode but it can also be used in toplevel definitions as shown below. .. note:: - - The grammar reserves the keywords ``lazymatch`` and - ``multimatch`` as well as the token ``||``. + - The grammar reserves the token ``||``. - The infix tacticals  ``… || …`` ,  ``… + …`` , and  ``… ; …``  are associative. diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 5baa23b3e9..0dea4fcc43 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -216,8 +216,8 @@ GRAMMAR EXTEND Gram ; match_key: [ [ "match" -> { Once } - | "lazymatch" -> { Select } - | "multimatch" -> { General } ] ] + | IDENT "lazymatch" -> { Select } + | IDENT "multimatch" -> { General } ] ] ; input_fun: [ [ "_" -> { Name.Anonymous } -- cgit v1.2.3 From 037c8d299ca1a5aef9813133dca07ad6f35e1e75 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 6 May 2020 16:59:19 +0200 Subject: Keywords: Applying suggestions from Jim Fehrle and Théo Zimmermann. --- doc/sphinx/language/coq-library.rst | 8 ++++---- doc/sphinx/language/core/basic.rst | 31 +++++++++++++++++++------------ 2 files changed, 23 insertions(+), 16 deletions(-) diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index acdd4408ed..899173a83a 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -9,11 +9,11 @@ The |Coq| library The |Coq| library has two parts: - * **The basic library**: definitions and theorems for + * The :gdef:`prelude`: definitions and theorems for the most commonly used elementary logical notions and data types. |Coq| normally loads these files automatically when it starts. - * **The standard library**: general-purpose libraries with + * The :gdef:`standard library`: general-purpose libraries with definitions and theorems for sets, lists, sorting, arithmetic, etc. To use these files, users must load them explicitly with the ``Require`` command (see :ref:`compiled-files`) @@ -28,8 +28,8 @@ also be browsed at http://coq.inria.fr/stdlib/. -The basic library ------------------ +The prelude +----------- This section lists the basic notions and results which are directly available in the standard |Coq| system. Most of these constructions diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 3940242bb3..aa93b4d21f 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -130,31 +130,38 @@ Strings identified with :production:`string`. Keywords - The following character sequences are reserved keywords that cannot be - used as identifiers:: + The following character sequences are keywords defined in the main Coq grammar + that cannot be used as identifiers (even when starting Coq with the `-noinit` + command-line flag):: _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop SProp Set Theorem Type Variable as at cofix else end fix for forall fun if in let match return then where with - Note that notations and plugins may define additional keywords. + The following are keywords defined in notations or plugins loaded in the :term:`prelude`:: -Other tokens - The set of - tokens defined at any given time can vary because the :cmd:`Notation` - command can define new tokens. A :cmd:`Require` command may load more notation definitions, - while the end of a :cmd:`Section` may remove notations. Some notations - are defined in the standard library (see :ref:`thecoqlibrary`) and are generally - loaded automatically at startup time. + IF by exists exists2 using + + Note that loading additional modules or plugins may expand the set of reserved + keywords. - Here are the character sequences that |Coq| directly defines as tokens - without using :cmd:`Notation`:: +Other tokens + The following character sequences are tokens defined in the main Coq grammar + (even when starting Coq with the `-noinit` command-line flag):: ! #[ % & ' ( () ) * + , - -> . .( .. ... / : ::= := :> :>> ; < <+ <- <: <<: <= = => > >-> >= ? @ @{ [ ] _ `( `{ { {| | } + The following character sequences are tokens defined in notations or plugins + loaded in the :term:`prelude`:: + + ** [= |- || -> + + Note that loading additional modules or plugins may expand the set of defined + tokens. + When multiple tokens match the beginning of a sequence of characters, the longest matching token is used. Occasionally you may need to insert spaces to separate tokens. For example, -- cgit v1.2.3