syntax.bnf

<ident> ::= [a-zA-Z0-9_!?] [a-zA-Z0-9_!?']*
          | '{|' <string> '|}'

<mident> ::= [a-zA-Z0-9_]*

<qident> ::= <mident> '.' <ident>

<line> ::= <ident> <param>* ':' <term> '.'
         | 'private' <ident> <param>* ':' <term> '.'
         | 'def' <ident> ':' <term> '.'
         | 'private' 'def' <ident> ':' <term> '.'
         | 'injective' <ident> ':' <term> '.'
         | 'private' 'injective' <ident> ':' <term> '.'
         | 'def'AC <ident> '[' <term> ']' '.'
         | 'private' 'def'AC <ident> '[' <term> ']' '.'
         | 'def'ACU <ident> '[' <term> ',' <term> ']' '.'
         | 'private' 'def'ACU <ident> '[' <term> ',' <term> ']' '.'
         | 'def' <ident> ':' <term> ':=' <term> '.'
         | 'def' <ident> ':=' <term> '.'
         | 'def' <ident> <param>+ ':' <term> ':=' <term> '.'
         | 'def' <ident> <param>+ ':=' <term> '.'
         | 'private' 'def' <ident> ':' <term> ':=' <term> '.'
         | 'private' 'def' <ident> ':=' <term> '.'
         | 'private' 'def' <ident> <param>+ ':' <term> ':=' <term> '.'
         | 'private' 'def' <ident> <param>+ ':=' <term> '.'
         | 'thm' <ident> ':' <term> ':=' <term> '.'
         | 'thm' <ident> <param>+ ':' <term> ':=' <term> '.'
         | <rule>+ '.'
         | '#EVAL' <term> '.'
         | '#EVAL' <eval_config> <term> '.'
         | '#INFER' <term> '.'
         | '#INFER' <eval_config> <term> '.'
         | '#CHECK' <aterm> ':' <term> '.'
         | '#CHECKNOT' <aterm> ':' <term> '.'
         | '#ASSERT' <aterm> ':' <term> '.'
         | '#ASSERTNOT' <aterm> ':' <term> '.'
         | '#CHECK' <aterm> '=' <term> '.'
         | '#CHECKNOT' <aterm> '=' <term> '.'
         | '#ASSERT' <aterm> '=' <term> '.'
         | '#ASSERTNOT' <aterm> '=' <term> '.'
         | '#PRINT' '"' <string> '"' '.'
         | '#GDT' <ident> '.'
         | '#GDT' <qident> '.'
         | '#NAME' '.'
         | '#REQUIRE' '.'
         | EOF

<eval_config> ::= '[' <ident> (',' <ident>)* ']'

<param> ::= '(' <ident> ':' <term> ')'

<rule> ::= '[' <context> ']' <top_pattern> '-->' <term>
         | '{' <ident> '}'  '[' <context> ']' <top_pattern>
           '-->' <term>
         | '{' <qident> '}'  '[' <context> ']' <top_pattern>
           '-->' <term>

<decl> ::= <ident> ':' <term>
         | <ident>

<context> ::= [<decl> (',' <decl>)*]

<top_pattern> ::= <ident> <pattern_wp>*
                | <qident> <pattern_wp>*

<pid> ::= '_'
        | <ident>

<pattern_wp> ::= <ident>
               | <qident>
               | '_'
               | '{' <term> '}' 
               | '(' <pattern> ')'

<pattern> ::= <pid> '=>' <pattern>
            | <pattern_wp>+

<sterm> ::= <qident>
          | <ident>
          | '(' <term> ')'
          | 'Type'

<aterm> ::= <sterm> <sterm>*

<term> ::= <aterm>
         | <pid> ':' <aterm> '->' <term>
         | '(' <ident> ':' <aterm> ')' '->' <term>
         | <aterm> '->' <term>
         | <pid> '=>' <term>
         | <pid> ':' <aterm> '=>' <term>
         | '(' <pid> ':' <aterm> ':=' <aterm> ')' '=>' <term>