Keywords vs. identifiers in the parser

[jfehrle]

Strings that the parser identifies as keywords can't be used as identifiers, for example Theorem, but other significant strings such as Lemma can. While I expect we want to be conservative in defining keywords, it's hard to see much of a pattern. Have these strings been made keywords or identifiers with care or arbitrarily? The current description of keywords in the doc is incomplete, I'm trying to figure what I can say that's more complete/useful.

Some examples: (with IDENT = an identifier, without = a reserved word):

  thm_token:
    [ [ "Theorem" -> { Theorem }
      | IDENT "Lemma" -> { Lemma }
      | IDENT "Fact" -> { Fact }
      | IDENT "Remark" -> { Remark }
      | IDENT "Corollary" -> { Corollary }
      | IDENT "Proposition" -> { Proposition }
      | IDENT "Property" -> { Property } ] ]
  ;
  def_token:
    [ [ "Definition" -> { (NoDischarge,Definition) }
      | IDENT "Example" -> { (NoDischarge,Example) }
      | IDENT "SubClass" -> { (NoDischarge,SubClass) } ] ]
  ;
  assumption_token:
    [ [ "Hypothesis" -> { (DoDischarge, Logical) }
      | "Variable" -> { (DoDischarge, Definitional) }
      | "Axiom" -> { (NoDischarge, Logical) }
      | "Parameter" -> { (NoDischarge, Definitional) }
      | IDENT "Conjecture" -> { (NoDischarge, Conjectural) } ] ]
  ;
  assumptions_token:
    [ [ IDENT "Hypotheses" -> { ("Hypotheses", (DoDischarge, Logical)) }
      | IDENT "Variables" -> { ("Variables", (DoDischarge, Definitional)) }
      | IDENT "Axioms" -> { ("Axioms", (NoDischarge, Logical)) }
      | IDENT "Parameters" -> { ("Parameters", (NoDischarge, Definitional)) }
      | IDENT "Conjectures" -> { ("Conjectures", (NoDischarge, Conjectural)) } ] ]
  ;

The current set of keywords is:

'Axiom' 'CoFixpoint' 'Definition' 'Fixpoint' 'Hypothesis' 'IF' 'Parameter' 'Prop'
 'SProp'  'Set'  'Theorem' 'Type' 'Variable' 'as''at' 'by' 'cofix' 'discriminated' 'else'
'end' 'exists' 'exists2' 'fix' 'for' 'forall' 'fun' 'if' 'in' 'lazymatch' 'let' 'match'
'multimatch' 'return' 'then' 'using' 'where' 'with'

[SkySkimmer]

see also https://github.com/coq/coq/pull/616

Gaëtan Gilbert

On 23/07/2019 22:29, Jim Fehrle wrote:

Strings that the parser identifies as keywords can't be used as identifiers, for example |Theorem|, but other significant strings such as |Lemma| can. While I expect we want to be conservative in defining keywords, it's hard to see much of a pattern. Have these strings been made keywords or identifiers with care or arbitrarily? The current description of keywords in the doc is incomplete, I'm trying to figure what I can say that's more complete/useful.

Some examples: (with |IDENT| = an identifier, without = a reserved word):

|thm_token: [ [ "Theorem" -> { Theorem } | IDENT "Lemma" -> { Lemma } | IDENT "Fact" -> { Fact } | IDENT "Remark" -> { Remark } | IDENT "Corollary" -> { Corollary } | IDENT "Proposition" -> { Proposition } | IDENT "Property" -> { Property } ] ] ; def_token: [ [ "Definition" -> { (NoDischarge,Definition) } | IDENT "Example" -> { (NoDischarge,Example) } | IDENT "SubClass" -> { (NoDischarge,SubClass) } ] ] ; assumption_token: [ [ "Hypothesis" -> { (DoDischarge, Logical) } | "Variable" -> { (DoDischarge, Definitional) } | "Axiom" -> { (NoDischarge, Logical) } | "Parameter" -> { (NoDischarge, Definitional) } | IDENT "Conjecture" -> { (NoDischarge, Conjectural) } ] ] ; assumptions_token: [ [ IDENT "Hypotheses" -> { ("Hypotheses", (DoDischarge, Logical)) } | IDENT "Variables" -> { ("Variables", (DoDischarge, Definitional)) } | IDENT "Axioms" -> { ("Axioms", (NoDischarge, Logical)) } | IDENT "Parameters" -> { ("Parameters", (NoDischarge, Definitional)) } | IDENT "Conjectures" -> { ("Conjectures", (NoDischarge, Conjectural)) } ] ] ; |

The current set of keywords is:

|'Axiom' 'CoFixpoint' 'Definition' 'Fixpoint' 'Hypothesis' 'IF' 'Parameter' 'Prop' 'SProp' 'Set' 'Theorem' 'Type' 'Variable' 'as''at' 'by' 'cofix' 'discriminated' 'else' 'end' 'exists' 'exists2' 'fix' 'for' 'forall' 'fun' 'if' 'in' 'lazymatch' 'let' 'match' 'multimatch' 'return' 'then' 'using' 'where' 'with' |

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/coq/coq/issues/10558?email_source=notifications&email_token=AASZB3FW3KNDXFJ6DXFM6Y3QA5S4BA5CNFSM4IGI6Q7KYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4HBBADGQ, or mute the thread https://github.com/notifications/unsubscribe-auth/AASZB3CSFCZPPZ4CIEQXYGDQA5S4BANCNFSM4IGI6Q7A.

[Zimmi48]

Related as well: #5464. But indeed, this discussion has already happened (including in WGs I think), and the status quo did not change because we could just not agree on a solution, with some people wanting more keywords and some people wanting less.

[jfehrle]

Thanks, guys. The status quo is not surprising. I've added code to doc_grammar to print the list of all keywords. Perhaps that info can later be used to make it more visible when new keywords are added.