Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
387 lines (261 sloc) 10.6 KB

Archetype grammar

{% hint style="info" %} The view below is generated by obelisk from parser.mly {% endhint %}

<loc(X)> ::= X

<snl(separator, X)> ::= X
                      | X separator
                      | X separator <snl(separator, X)>

<snl2(separator, X)> ::= X separator X
                       | X separator <snl2(separator, X)>

<paren(X)> ::= LPAREN X RPAREN

<braced(X)> ::= LBRACE X RBRACE

<bracket(X)> ::= LBRACKET X RBRACKET

<start_expr> ::= <expr> EOF
               | <loc(error)>

<main> ::= <loc(<archetype_r>)>
         | <loc(error)>

<archetype_r> ::= <implementation_archetype> EOF
                | <archetype_extension> EOF

<archetype_extension> ::= ARCHETYPE EXTENSION <ident> <paren(<declarations>)>
                          EQUAL <braced(<declarations>)>

<implementation_archetype> ::= <declarations>

<declarations> ::= <declaration>+

<declaration> ::= <loc(<declaration_r>)>

<declaration_r> ::= <archetype>
                  | <constant>
                  | <variable>
                  | <enum>
                  | <states>
                  | <asset>
                  | <action>
                  | <transition>
                  | <dextension>
                  | <namespace>
                  | <contract>
                  | <function_decl>
                  | <verification_decl>

<archetype> ::= ARCHETYPE [<extensions>] <ident>

<vc_decl(X)> ::= X [<extensions>] <ident> <type_t> [<value_options>]
                 [<default_value>]

<constant> ::= <vc_decl(CONSTANT)>

<variable> ::= <vc_decl(VARIABLE)>

<value_options> ::= <value_option>+

<value_option> ::= <from_value>
                 | <to_value>

<default_value> ::= EQUAL <expr>

<from_value> ::= FROM <qualid>

<to_value> ::= TO <qualid>

<dextension> ::= PERCENT <ident> [nonempty_list(<simple_expr>)]

<extensions> ::= <extension>+

<extension> ::= <loc(<extension_r>)>

<extension_r> ::= LBRACKETPERCENT <ident> [<simple_expr>+] RBRACKET

<namespace> ::= NAMESPACE <ident> <braced(<declarations>)>

<contract> ::= CONTRACT [<extensions>] <ident> EQUAL <braced(<signatures>)>
               [<default_value>]

<signatures> ::= <signature>+

<signature> ::= ACTION <ident>
              | ACTION <ident> COLON <types>

<fun_effect> ::= EFFECT <braced(<expr>)>

<fun_body> ::= <expr>
             | <verification_fun> <fun_effect>

<function_gen> ::= FUNCTION <ident> <function_args> [<function_return>] EQUAL
                   LBRACE <fun_body> RBRACE

<function_item> ::= <loc(<function_gen>)>

<function_decl> ::= <function_gen>

<verif_predicate> ::= PREDICATE <ident> <function_args> EQUAL
                      <braced(<expr>)>

<verif_definition> ::= DEFINITION <ident> EQUAL LBRACE <ident> COLON <type_t>
                       PIPE <expr> RBRACE

<verif_axiom> ::= AXIOM <ident> EQUAL <braced(<expr>)>

<verif_theorem> ::= THEOREM <ident> EQUAL <braced(<expr>)>

<verif_variable> ::= VARIABLE <ident> <type_t> [<default_value>]

<verif_invariant> ::= INVARIANT <ident> EQUAL <braced(<expr>)>

<verif_effect> ::= EFFECT <braced(<expr>)>

<verif_specification> ::= SPECIFICATION <braced(<expr>)>

<verif_item> ::= <verif_predicate>
               | <verif_definition>
               | <verif_axiom>
               | <verif_theorem>
               | <verif_variable>
               | <verif_invariant>
               | <verif_effect>

<verification(spec)> ::= <loc(spec)>
                       | VERIFICATION [<extensions>] LBRACE
                         <loc(<verif_item>)>* <loc(<verif_specification>)>
                         RBRACE

<verification_fun> ::= <loc(<verification(<verif_specification>)>)>

<verification_decl> ::= <loc(<verification(<verif_specification>)>)>

<enum> ::= ENUM [<extensions>] <ident> EQUAL <pipe_idents>

<states> ::= STATES [<extensions>] [<ident>] [<states_values>]

<states_values> ::= EQUAL <pipe_ident_options>

<types> ::= <type_t> (COMMA <type_t>)*

<type_t> ::= <loc(<type_r>)>

<type_r> ::= <type_s> <type_tuples>
           | <type_s_unloc>
           | <type_t> IMPLY <type_t>

<type_s> ::= <loc(<type_s_unloc>)>

<type_s_unloc> ::= <ident>
                 | <type_s> <container>
                 | <ident> <type_s>
                 | <paren(<type_r>)>

<type_tuples> ::= <type_tuple>+

<type_tuple> ::= MULT <type_s>

<container> ::= COLLECTION
              | QUEUE
              | STACK
              | SET
              | PARTITION

<pipe_idents> ::= [PIPE] <ident> (PIPE <ident>)*

<pipe_ident_options> ::= [PIPE] <pipe_ident_option> (PIPE
                         <pipe_ident_option>)*

<pipe_ident_option> ::= <ident> [<state_options>]

<state_options> ::= <state_option>+

<state_option> ::= INITIAL
                 | WITH <braced(<expr>)>

<asset> ::= ASSET [<extensions>] [<bracket(<asset_operation>)>] <ident>
            [<asset_options>] [<asset_fields>] <asset_post_options>

<asset_post_option> ::= WITH STATES <ident>
                      | WITH <braced(<expr>)>
                      | INITIALIZED BY <simple_expr>

<asset_post_options> ::= <asset_post_option>*

<asset_fields> ::= EQUAL <braced(<fields>)>

<asset_options> ::= <asset_option>+

<asset_option> ::= AS <ident>
                 | IDENTIFIED BY <ident>
                 | SORTED BY <ident>

<fields> ::= <snl(SEMI_COLON, <field>)>

<field_r> ::= <ident> [<extensions>] COLON <type_t> [REF] [<default_value>]

<field> ::= <loc(<field_r>)>

<ident> ::= <loc(IDENT)>

<action> ::= ACTION [<extensions>] <ident> <function_args> <transitems_eq>

<transition_to_item> ::= TO <ident> [<require_value>] [<with_effect>]

<transitions> ::= <transition_to_item>+

<on_value> ::= ON <ident> COLON <ident>

<transition> ::= TRANSITION [<extensions>] <ident> <function_args>
                 [<on_value>] FROM <expr> EQUAL LBRACE <action_properties>
                 <transitions> RBRACE

<transitems_eq> ::= [EQUAL LBRACE <action_properties> [<effect>] RBRACE]

<action_properties> ::= [<calledby>] [ACCEPT_TRANSFER] [<require>]
                        [<verification_fun>] <function_item>*

<calledby> ::= CALLED BY [<extensions>] <expr>

<require> ::= REQUIRE [<extensions>] <braced(<expr>)>

<require_value> ::= WHEN [<extensions>] <braced(<expr>)>

<with_effect> ::= WITH EFFECT [<extensions>] <braced(<expr>)>

<effect> ::= EFFECT [<extensions>] <braced(<expr>)>

<function_return> ::= COLON <type_t>

<function_args> ::= [<function_arg>+]

<function_arg> ::= <ident> [<extensions>]
                 | LPAREN <ident> [<extensions>] COLON <type_t> RPAREN

<assignment_operator_record> ::= EQUAL
                               | <assignment_operator_extra>

<assignment_operator_expr> ::= COLONEQUAL
                             | <assignment_operator_extra>

<assignment_operator_extra> ::= PLUSEQUAL
                              | MINUSEQUAL
                              | MULTEQUAL
                              | DIVEQUAL
                              | ANDEQUAL
                              | OREQUAL

<qualid> ::= <ident> (DOT <ident>)*

<branchs> ::= <branch>+

<branch> ::= <patterns> IMPLY <expr>

<patterns> ::= <loc(<pattern>)>+

<pattern> ::= PIPE UNDERSCORE
            | PIPE <ident>

<expr> ::= <loc(<expr_r>)>

<ident_typ_q_item> ::= LPAREN <ident>+ COLON <type_t> RPAREN

<ident_typ_q> ::= <ident_typ_q_item>+

<expr_r> ::= <quantifier> <ident_typ1> COMMA <expr>
           | <quantifier> <ident_typ_q> COMMA <expr>
           | LET <ident_typ1> EQUAL <expr> IN <expr> OTHERWISE <expr>
           | LET <ident_typ1> EQUAL <expr> IN <expr>
           | <expr> SEMI_COLON <expr>
           | <ident> COLON <expr>
           | FUN <ident_typs> EQUALGREATER <expr>
           | ASSERT <paren(<expr>)>
           | BREAK
           | FOR LPAREN <ident> IN <expr> RPAREN <expr>
           | IF <expr> THEN <expr>
           | IF <expr> THEN <expr> ELSE <expr>
           | MATCH <expr> WITH <branchs> END
           | <snl2(COMMA, <simple_expr>)>
           | <expr> <assignment_operator_expr> <expr>
           | TRANSFER [BACK] <simple_expr> [<to_value>]
           | REQUIRE <simple_expr>
           | FAILIF <simple_expr>
           | <order_operations>
           | <expr> <loc(<bin_operator>)> <expr>
           | <loc(<un_operator>)> <expr>
           | <ident> <app_args>
           | <simple_expr> DOT <ident> <app_args>
           | <simple_expr_r>

<order_operation> ::= <expr> <loc(<ord_operator>)> <expr>

<order_operations> ::= <order_operation>
                     | <loc(<order_operations>)> <loc(<ord_operator>)> <expr>

<app_args> ::= LPAREN RPAREN
             | <simple_expr>+

<simple_expr> ::= <loc(<simple_expr_r>)>

<simple_expr_r> ::= <simple_expr> DOT <ident>
                  | LBRACKET RBRACKET
                  | LBRACKET <expr> RBRACKET
                  | LBRACE <record_item> (SEMI_COLON <record_item>)* RBRACE
                  | <literal>
                  | <ident> COLONCOLON <ident>
                  | <ident>
                  | LPAREN <ident> COLONCOLON <ident> AT <ident> RPAREN
                  | LPAREN <ident> AT <ident> RPAREN
                  | <paren(<expr_r>)>

<ident_typs> ::= <ident>+ COLON <type_t>
               | <ident_typ>+

<ident_typ> ::= <ident>
              | LPAREN <ident>+ COLON <type_t> RPAREN

<ident_typ1> ::= <ident> [COLON <type_t>]

<literal> ::= NUMBER
            | RATIONAL
            | TZ
            | STRING
            | ADDRESS
            | <bool_value>
            | DURATION
            | DATE

<bool_value> ::= TRUE
               | FALSE

<record_item> ::= <simple_expr>
                | <ident> <assignment_operator_record> <simple_expr>

<quantifier> ::= FORALL
               | EXISTS

<spec_operator> ::= OP_SPEC1
                  | OP_SPEC2
                  | OP_SPEC3
                  | OP_SPEC4

<logical_operator> ::= AND
                     | OR
                     | IMPLY
                     | EQUIV

<comparison_operator> ::= EQUAL
                        | NEQUAL

<ordering_operator> ::= LESS
                      | LESSEQUAL
                      | GREATER
                      | GREATEREQUAL

<arithmetic_operator> ::= PLUS
                        | MINUS
                        | MULT
                        | DIV
                        | PERCENT

<unary_operator> ::= PLUS
                   | MINUS
                   | NOT

<bin_operator> ::= <spec_operator>
                 | <logical_operator>
                 | <comparison_operator>
                 | <arithmetic_operator>

<un_operator> ::= <unary_operator>

<ord_operator> ::= <ordering_operator>

<asset_operation_enum> ::= AT_ADD
                         | AT_REMOVE
                         | AT_UPDATE

<asset_operation> ::= <asset_operation_enum>+ [<simple_expr>+]
You can’t perform that action at this time.