Description of the syntax is out of date

[lovasoa]

Hi,
I'm writing an LBNF grammar for .ph files.
For this, I use this description of the format: http://loicpauleve.name/pint/doc/syntax.html
And I test my grammar against the example files you provide.
But the format they use seems to be slightly different from the one that is described.
For instance, COOPERATIVITY seems to have a different syntax, and there are new directives.

[MFolschette]

Hi,
Indeed, these syntaxes do not seem to be referenced in the documentation. In fact, the COOPERATIVITY macro comes in two different forms and only one appears in the documentation.
For the exact syntax, please refer to the source code of Pint or contact Loïc Paulevé.

[pauleve]

Hi,
Thanks for pushing on having up-to-date docs :-)
I've add the documentation on the alternate COOPERATIVITY usage.
Note that I moved the syntax page as Pint progressively migrates to a new file format.
http://loicpauleve.name/pint/doc/syntax-ph.html

If you want the actual grammar of ph files, you can have a look at the second-half of
https://github.com/pauleve/pint/blob/master/phlib/ph_parser.mly
and
https://github.com/pauleve/pint/blob/master/phlib/ph_lexer.mll

Regarding the directive "sample" it is no longer used, so it should be silently ignored.

[lovasoa]

I'm closing the issue since you added the missing doc.

However, I still have questions:

• What is the use of the named cooperations? Where is the name used ? Why does it have to be "enforced" ? Is it defined elsewhere?
• What is the priority of the "and" and "or" operators ? Are parenthesis supported for overriding priority ?
• Is "[a;b] in [[0;1]]" the same as "[a] in [[0]] and [b] in [[1]]" ?
• Why are there so many square brackets? Why couldn't we write "a in 0 and b in 1" ? I understand their use with the other COOPERATIVITY syntax, but not here.
• The description of the second COOPERATIVY syntax specifies that the sort bounces back to its original state whenever the condition is false. Is it also the case when the cooperativity is defined using the other syntax ?

[pauleve]

COOPERATIVITY creates additional automata - by default, if your cooperation is not nested, the created automaton takes as name the concatenation of the automata in the condition. If it is nested, then some will be named by concatenation of the inputs, others with arbirtrary names like __coop1. The only use of enforcing the name is for making reference to this automatically created automaton in further macros/actions.

You can use the phc command to see the effect of the macros : phc -i file.ph -l dump will output the same model without the use of macros (only simple actions).

Regarding the priority, it is the classical one : and has higher priority than or - and yes, you can use parenthesis.

Regarding your question on "[a;b] in [[0;1]]" and "[a] in [[0]] and [b] in [[1]]" - in this case it is strictly the same (a cooperative automaton ab will be created). But in the general case, one cooperative automaton is created for each logical operator ; hence the global dynamics is equivalent if the matching is equivalent, but you can have different way to implement it using the cooperative automata.

The main goal was to help splitting large cooperative automata: if you use
[a;b;c;d;e;f] in [[1;1;1;1;1;1]] it will create one cooperative automaton with 2^6 local states.
But if you use ['a';b';'c'] in [[1;1;1]] and ['d';'e';'f'] in [[1;1;1]] it will create 3 cooperative automata : one for abc with 2^3 states, one for def with 2^3 states and one for the "and" with 2^2 states; which helps the scalability of the static analysis we develop.
If you use only ['a'] in [[1]], no cooperative automaton is created, that's why in your question, the encodings are equivalent.

The brackets are here to encode lists, the "in" operators check for a matching of the state of the automata list on the left in the state list on the right. Some syntax sugar like "=" operators could remove some brackets, but well, that's not a very crucial point.

For your last question, no the first COOPERATIVITY macro only specifies the condition for one bounce; while the other one for symmetric bounces. This latter helps to encode Boolean functions.