syntax.bnf

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

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

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

<definibility> ::= 'injective'
                 | 'private'
                 | 'private' 'injective'
                 | 'def'

<ilist(x)> ::= [x+]

<line> ::= <rule>+ '.'
         | 'def' <ident> <ilist(<param>)> [<of_ty>] ':=' <term> '.'
         | 'thm' <ident> <ilist(<param>)> [<of_ty>] ':=' <term> '.'
         | [<definibility>] <ident> <ilist(<param>)> <of_ty> '.'
         | 'def'AC <ident> '[' <term> ']' '.'
         | 'private' 'def'AC <ident> '[' <term> ']' '.'
         | 'def'ACU <ident> '[' <term> ',' <term> ']' '.'
         | 'private' 'def'ACU <ident> '[' <term> ',' <term> ']' '.'
         | '#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' '.'
         | PRAGMA
         | EOF

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

<of_ty> ::= ':' <term>

<param> ::= '(' <pid> ':' <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>*
                | '(' <top_pattern> ')' <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>
         | '(' <pid> ':' <aterm> ')' '->' <term>
         | <aterm> '->' <term>
         | <pid> '=>' <term>
         | <pid> ':' <aterm> '=>' <term>
         | '(' <pid> ':' <aterm> ':=' <aterm> ')' '=>' <term>