Difference between the syntax description chapter and the Tamarin parser

[aeyno]

While programming a parser for the Tamarin theory files, I came across some problems in the Syntax Description chapter of the manual where the grammar seems different from what Tamarin could parse :

• In the rule lemma, proof_skeleton should probably be optional

• The grammar says that the list of facts between brackets must be non-empty but in Tamarin it is possible to have rules without facts

   simple_rule := 'rule' [modulo] ident [rule_attrs] ':'
       				[let_block]
       				'[' facts ']' ( '-->' | '--[' facts ']->') '[' facts ']'

  Is probably something like

   simple_rule := 'rule' [modulo] ident [rule_attrs] ':'
   	[let_block]
   	'[' [facts] ']' ( '-->' | '--[' [facts] ']->') '[' [facts] ']'

  Or facts could be rewritten as

   facts := [ fact (',' fact)* ]

• No description of hexcolor : (done in Add hexcolor to syntax description #105 ✅)
  hexcolor which is used in the rule rule_attr is not defined explicitly in EBNF style.
  The manual only says A color is represented as a triplet of 8 bit hexadecimal values optionally preceded by '#'
  but after some testing I found out that Tamarin seems to accept some files where hexcolor is between simple quotes,
  making all #ffffff, #FFFFFF, 'ffffff, 'FFFFFF', '#ffffff' and '#FFFFFF' valid syntaxes.
  Maybe consider adding something like this to the manual

   hexcolor := "'" ["#"] hex "'"
   	| ["#"] hex

• multterm is used instead of tupleterm in nary_app

• No description of preprocessor directives :
  Tamarin has some preprocessing capabilities (support for #ifdef, #else, #endif, #include) but those are not present in the grammar

• No description of predicates :
  The syntax description for predicates and _restrict() is also not present in the grammar

• There are some missing built-in names (eg. locations-report)

[cascremers]

Hi, thanks for this -- you are right, the grammar isn't completely accurate, and we want to update it in the near future. Your observations are very helpful. Do let us know if you spot more differences!

[aeyno]

I found new problems in the grammar :

• macros doesn't appear in any grammar rule, I believe it should be in signature_spec (@ValentinYuri)
• The macro rule uses var which is not defined in the grammar
• According to the manual, rule_attrs could not be equal to [] but Tamarin is able to parse the following rule :

  rule empty_attrs[]:
      []-->[]
  

• No syntax description of tactic goals ranking {.} which is described in the advanced features