From d48f3cbfc98c12c11483f9c0017c80a42c36c486 Mon Sep 17 00:00:00 2001 From: rkunnema Date: Mon, 9 Sep 2024 14:35:52 +0200 Subject: [PATCH] Fix grammar element "terms" (#678) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * 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 Co-authored-by: jdreier Co-authored-by: Robert Künnemann --- manual/grammar/grammar.ebnf | 16 ++++---- manual/src/016_syntax_description.md | 48 ++++++++++++------------ tree-sitter/tree-sitter-spthy/grammar.js | 32 ++++++++-------- 3 files changed, 48 insertions(+), 48 deletions(-) diff --git a/manual/grammar/grammar.ebnf b/manual/grammar/grammar.ebnf index ea5426273..9e601c01d 100644 --- 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 ::= ') + mset_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 index 3ddd49db2..9cfddcde4 100644 --- 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 := binary_app := binary_fun '{' tupleterm '}' term binary_fun := 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 index b3af9b7d5..63cd8dafe 100644 --- 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: $ => /[^"]*/,