Fix grammar element "terms" (tamarin-prover#678)

* updates script, new keys * fix directory * github workflow * make pdf * add * deploy to manual repo, not to code repo * set key before checking out * directory * Properly nest term types in grammar.js * fixed latex template * update pandoc version * MANUAL+syntax: update "term" and co. * Syntax: Removed `\w` for its definition because of pandoc/latex --------- Co-authored-by: Jannik Dreier <[email protected]> Co-authored-by: jdreier <[email protected]> Co-authored-by: Robert Künnemann <[email protected]>
rkunnema · Sep 9, 2024 · d48f3cb · d48f3cb
1 parent 0396410
commit d48f3cb
Show file tree

Hide file tree

Showing 3 changed files with 48 additions and 48 deletions.
diff --git a/manual/grammar/grammar.ebnf b/manual/grammar/grammar.ebnf
@@ -137,14 +137,14 @@ rules:
   chain_goal  ::=  '(' temporal_var ',' natural ')' '~~>' '(' temporal_var ',' natural ')'
   disjunction_split_goal  ::=  CHAIN_GOAL((_formula: formula) (('||' | '∥') (_formula: formula))+)
   eq_split_goal  ::=  'splitEqs' '(' natural ')'
-  _term  ::=  tuple_term | mset_term | nat_term | xor_term | mul_term | exp_term | nested_term | nullary_fun | binary_app | nary_app | _literal
-  tuple_term  ::=  TUPLE('<' ((_term): term) (',' (_term: term))* '>')
-  mset_term  ::=  <MUL_SET((_term: left) ('++' | '+') (_term: right))
-  nat_term  ::=  <ADD((_term: left) '%+' (_term: right))
-  xor_term  ::=  <EXCLUSIVE_OR((_term: left) ('XOR' | '⊕') (_term: right))
-  mul_term  ::=  <MULTIPLY((_term: left) '*' (_term: right))
+  _term  ::=  tuple_term | mset_term | nested_term | nullary_fun | binary_app | nary_app | _literal
+  tuple_term  ::=  TUPLE('<' ((mset_term): term) (',' (mset_term: term))* '>')
+  mset_term  ::=  <MUL_SET((nat_term: left) ('++' | '+') (nat_term: right))
+  nat_term  ::=  <ADD((xor_term: left) '%+' (xor_term: right))
+  xor_term  ::=  <EXCLUSIVE_OR((mult_term: left) ('XOR' | '⊕') (mult_term: right))
+  mult_term  ::=  <MULTIPLY((exp_term: left) '*' (exp_term: right))
   exp_term  ::=  >EXPONENTIAL((_term: base) '^' (_term: exponent))
-  nested_term  ::=  NESTED('(' _term ')')
+  nested_term  ::=  NESTED('(' mset_term ')')
   nullary_fun  ::=  NULLARY_FUN((ident: function_identifier) | ((ident: function_identifier) '(' ')'))
   binary_app  ::=  FUNCTION((ident: function_identifier) '{' (_term: argument) (',' (_term: argument))*? '}' (_term: argument))
   nary_app  ::=  FUNCTION((ident: function_identifier) '(' arguments ')')
@@ -183,7 +183,7 @@ rules:
   predicate_ref  ::=  FUNCTION((ident: predicate_identifier) '(' arguments? ')')
   pre_defined  ::=  NULLARY_FUN(ident)
   hexcolor  ::=  (''' @('#')? @(/[0-9a-fA-F]{1,6}/) ''') | (@('#')? @(/[0-9a-fA-F]{1,6}/))
-  ident  ::=  /[A-Za-z0-9]\w*/
+  ident  ::=  /[A-Za-z0-9][a-zA-Z0-9_*]*/
   param  ::=  /[^"]*/
   export_query  ::=  /(\\"|[^"])*/
   natural  ::=  /[0-9]+/

diff --git a/manual/src/016_syntax_description.md b/manual/src/016_syntax_description.md
@@ -135,35 +135,37 @@ symbols, there is no need to write `nullary()`. Note that the number of
 arguments of an n-ary function application must agree with the arity given in
 the function definition.
 
-TODO
-~~~~ {.tamarin grammar="grammar/grammar.ebnf" rules="_term,tupleterm,mset_term,natterm,"}
-~~~~
-    tupleterm := '<' msetterm (',' msetterm)* '>'
-    msetterm  := natterm (('++' | '+') natterm)*
-    natterm   := xorterm ('%+' xorterm)*
-    xorterm   := multterm (('XOR' | ⊕) multterm)*
-    multterm  := expterm ('*' expterm)*
-    expterm   := term    ('^' term   )*
-    term      := tupleterm             // n-ary right-associative pairing
-               | '(' msetterm ')'      // a nested term
-               | nullary_fun
-               | binary_app
-               | nary_app
-               | literal
+~~~~ {.tamarin grammar="grammar/grammar.ebnf" rules="tupleterm,mset_term,nat_term,xor_term,mult_term,exp_term,_term"}
+~~~~
+
+Tamarin's parser checks that functions were previously defined and are used with the correct arity.
 
+~~~~
     nullary_fun := <all-nullary-functions-defined-up-to-here>
     binary_app  := binary_fun '{' tupleterm '}' term
     binary_fun  := <all-binary-functions-defined-up-to-here>
     nary_app    := nary_fun '(' multterm* ')'
+~~~~
+
+External tools may instead use the following grammar and check these conditions after parsing.
+
+~~~~ {.tamarin grammar="grammar/grammar.ebnf" rules="nulllary_fun,binary_app,binary_fun,nary_app"}
+~~~~
+
+Literals and variables appear in many forms.
 
-    literal     := "'"  ident "'" // a fixed, public name
-                 | "~'" ident "'" // a fixed, fresh name
-                 | nonnode_var    // a non-temporal variable
-    nonnode_var := ['$'] ident ['.' natural]         // 'pub' sort prefix
-                 | ident ['.' natural] ':' 'pub'     // 'pub' sort suffix
-                 | ['~'] ident ['.' natural]         // 'fresh' sort prefix
-                 | ident ['.' natural] ':' 'fresh'   // 'fresh' sort suffix
-                 | msg_var                                // 'msg' sort
+~~~~ {.tamarin grammar="grammar/grammar.ebnf" rules="_literal,_non_temporal_var"}
+~~~~
+
+When appearing in formulas or rules, they have an identifier and a sort.
+
+~~~~ {.tamarin grammar="grammar/grammar.ebnf" rules="fresh_name,_non_temporal_var,pub_var,fresh_var,msg_var_or_nullary_fun,nat_var"}
+~~~~
+
+SAPIC processes also have (optional) types. Moreover, literals in pattern can signify with a `=` if they are matched or bound.
+
+~~~~ {.tamarin grammar="grammar/grammar.ebnf" rules="comp_var,_custom_type_var,custom_var"}
+~~~~
 
 Facts do not have to be defined up-front. This will probably change once we
 implement user-defined sorts. Facts prefixed with `!` are persistent facts.

diff --git a/tree-sitter/tree-sitter-spthy/grammar.js b/tree-sitter/tree-sitter-spthy/grammar.js
@@ -1057,10 +1057,6 @@ module.exports = grammar({
       _term: $ => choice(
           $.tuple_term,
           $.mset_term,
-          $.nat_term,
-          $.xor_term,
-          $.mul_term,
-          $.exp_term,
           $.nested_term,
           $.nullary_fun,
           $.binary_app,
@@ -1070,36 +1066,38 @@ module.exports = grammar({
 
       tuple_term: $ => prec('TUPLE', seq(
           '<',
-          field('term', choice($._term)),
+          field('term', choice($.mset_term)),
           repeat(seq(
               ',',
-              field('term', $._term)
+              field('term', $.mset_term)
           )),
           '>'
       )),
 
+      // Not represented here, but taken from the code:
+      // only allow if multiset is enabled and we do not parse an equation
       mset_term: $ => prec.left('MUL_SET', seq(
-          field('left', $._term),
+          field('left', $.nat_term),
           choice('++', '+'),
-          field('right', $._term)
+          field('right', $.nat_term)
       )),
 
       nat_term: $ => prec.left('ADD', seq(
-          field('left', $._term),
+          field('left', $.xor_term),
           '%+',
-          field('right', $._term)
+          field('right', $.xor_term)
       )),
 
       xor_term: $ => prec.left('EXCLUSIVE_OR', seq(
-          field('left', $._term),
+          field('left', $.mult_term),
           choice('XOR', '⊕'),
-          field('right', $._term)
+          field('right', $.mult_term)
       )),
 
-      mul_term: $ => prec.left('MULTIPLY', seq(
-          field('left', $._term),
+      mult_term: $ => prec.left('MULTIPLY', seq(
+          field('left', $.exp_term),
           '*',
-          field('right', $._term)
+          field('right', $.exp_term)
       )),
 
       exp_term: $ => prec.right('EXPONENTIAL', seq(
@@ -1109,7 +1107,7 @@ module.exports = grammar({
       )),
 
       nested_term: $ => prec('NESTED', seq(
-          '(', $._term, ')'
+          '(', $.mset_term, ')'
       )),
 
       nullary_fun: $ => prec('NULLARY_FUN', choice(
@@ -1425,7 +1423,7 @@ module.exports = grammar({
           )
       ),
 
-      ident: $ => /[A-Za-z0-9]\w*/,
+      ident: $ => /[A-Za-z0-9][a-zA-Z0-9_*]*/,
 
       param: $ => /[^"]*/,