Archetype grammar

The view below is generated by obelisk from parser.mly

<loc(X)> ::= X
<sl(separator, X)> ::= [<snl(separator, 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
<main> ::= <loc(<archetype_r>)>
<archetype_r> ::= <implementation_archetype> EOF
| <archetype_extension> EOF
<archetype_extension> ::= ARCHETYPE EXTENSION <ident> <paren(<declarations>)>
<braced(<declarations>)>
<implementation_archetype> ::= <declarations>
<declarations> ::= <declaration>+
<declaration> ::= <loc(<declaration_r>)>
<declaration_r> ::= <archetype>
| <constant>
| <variable>
| <enum>
| <asset>
| <action>
| <transition>
| <dextension>
| <namespace>
| <contract>
| <function_decl>
| <specification_decl>
| <security_decl>
| INVALID_DECL
<archetype> ::= ARCHETYPE [<extensions>] <ident>
<invariants> ::= [WITH <braced(<label_exprs>)>]
<vc_decl(X)> ::= X [<extensions>] <ident> COLON <type_t> [<default_value>]
<invariants>
<constant> ::= <vc_decl(CONSTANT)>
<variable> ::= <vc_decl(VARIABLE)>
<default_value> ::= EQUAL <expr>
<ext_args> ::= [LPAREN <snl(COMMA, <simple_expr>)> RPAREN]
<dextension> ::= PERCENT <ident> <ext_args>
<extensions> ::= <extension>+
<extension> ::= <loc(<extension_r>)>
<extension_r> ::= LBRACKETPERCENT <ident> <ext_args> PERCENTRBRACKET
<namespace> ::= NAMESPACE <ident> <braced(<declarations>)>
<contract> ::= CONTRACT [<extensions>] <ident> <braced(<signatures>)>
<signatures> ::= <signature>+
<sig_arg> ::= <ident> COLON <type_t>
<sig_args> ::= LPAREN <sl(COMMA, <sig_arg>)> RPAREN
<signature> ::= ACTION <ident> <sig_args>
<fun_body> ::= <expr>
| <specification_fun> EFFECT <braced(<expr>)>
<function_gen> ::= FUNCTION <ident> <function_args> [<function_return>]
LBRACE <fun_body> RBRACE
<function_item> ::= <loc(<function_gen>)>
<function_decl> ::= <function_gen>
<spec_predicate> ::= PREDICATE <ident> <function_args> <braced(<expr>)>
<spec_definition> ::= DEFINITION <ident> LBRACE <ident> COLON <type_t> PIPE
<expr> RBRACE
<spec_variable> ::= VARIABLE <ident> COLON <type_t> [<default_value>]
<spec_effect> ::= SHADOW EFFECT <braced(<block>)>
<invars> ::= INVARIANT FOR <ident> <braced(<expr>)>
<uses> ::= [USE COLON <ident>+ SEMI_COLON]
<spec_body> ::= <expr> <invars>* <uses>
<spec_assert> ::= ASSERT <ident> <braced(<spec_body>)>
<spec_postcondition> ::= POSTCONDITION <ident> <braced(<spec_body>)>
<spec_contract_invariant> ::= CONTRACT INVARIANT <ident>
<braced(<spec_body>)>
<spec_items> ::= <loc(<spec_definition>)>* <loc(<spec_predicate>)>*
<loc(<spec_variable>)>* <loc(<spec_effect>)>*
<loc(<spec_assert>)>* <loc(<spec_postcondition>)>*
<loc(<spec_contract_invariant>)>*
<specification> ::= SPECIFICATION [<extensions>] LBRACE <spec_items> RBRACE
| SPECIFICATION [<extensions>] LBRACE
<label_exprs_non_empty> RBRACE
<specification_fun> ::= <loc(<specification>)>
<specification_decl> ::= <loc(<specification>)>
<security_item_unloc> ::= <ident> COLON <ident> <security_args>
<security_item> ::= <loc(<security_item_unloc>)>
<security_decl_unloc> ::= SECURITY [<extensions>] LBRACE <sl(SEMI_COLON,
<security_item>)> RBRACE
<security_decl> ::= <loc(<security_decl_unloc>)>
<enum> ::= STATES [<extensions>] <equal_enum_values>
| ENUM [<extensions>] <ident> <equal_enum_values>
<equal_enum_values> ::= [EQUAL <enum_values>]
<enum_values> ::= [<pipe_idents>]
<pipe_idents> ::= <pipe_ident>+
<pipe_ident> ::= PIPE <ident> <enum_options>
<enum_options> ::= [<enum_option>+]
<enum_option> ::= INITIAL
| WITH <braced(<label_exprs>)>
<type_t> ::= <loc(<type_r>)>
<type_r> ::= <type_s> <type_tuples>
| <type_s_unloc>
| PKEY OF <type_s>
<type_s> ::= <loc(<type_s_unloc>)>
<type_s_unloc> ::= <ident>
| <ident> RECORD
| <type_s> <container>
| <type_s> OPTION
| <type_s> LIST
| <paren(<type_r>)>
<type_tuples> ::= <type_tuple>+
<type_tuple> ::= MULT <type_s>
<container> ::= COLLECTION
| PARTITION
<shadow_asset_fields> ::= [SHADOW <asset_fields>]
<asset> ::= ASSET [<extensions>] [<bracket(<asset_operation>)>] <ident>
[<asset_options>] [<asset_fields>] <shadow_asset_fields>
<asset_post_options>
<asset_post_option> ::= WITH STATES <ident>
| WITH <braced(<label_exprs>)>
| INITIALIZED BY <simple_expr>
<asset_post_options> ::= <asset_post_option>*
<asset_fields> ::= <braced(<fields>)>
<asset_options> ::= <asset_option>+
<asset_option> ::= IDENTIFIED BY <ident>
| SORTED BY <ident>
<fields> ::= <sl(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 LPAREN <ident> COLON <type_t> RPAREN
<transition> ::= TRANSITION [<extensions>] <ident> <function_args>
[<on_value>] LBRACE <action_properties> FROM <expr>
<transitions> RBRACE
<transitems_eq> ::= [LBRACE <action_properties> [<effect>] RBRACE]
<accept_transfer> ::= epsilon
| REFUSE_TRANSFER
| ACCEPT_TRANSFER
<action_properties> ::= [<specification_fun>] <accept_transfer> [<calledby>]
[<require>] [<failif>] <function_item>*
<calledby> ::= CALLED BY [<extensions>] <expr>
<require> ::= REQUIRE [<extensions>] <braced(<label_exprs>)>
<failif> ::= FAILIF [<extensions>] <braced(<label_exprs>)>
<require_value> ::= WHEN [<extensions>] <braced(<expr>)>
<with_effect> ::= WITH <effect>
<effect> ::= EFFECT [<extensions>] <braced(<block>)>
| INVALID_EFFECT
<function_return> ::= COLON <type_t>
<function_args> ::= LPAREN <sl(COMMA, <function_arg>)> RPAREN
<function_arg> ::= <ident> [<extensions>] COLON <type_t>
<assignment_operator_record> ::= EQUAL
| <assignment_operator_extra>
<assignment_operator_expr> ::= COLONEQUAL
| <assignment_operator_extra>
<assignment_operator_extra> ::= PLUSEQUAL
| MINUSEQUAL
| MULTEQUAL
| DIVEQUAL
<branchs> ::= <branch>+
<branch> ::= <patterns> IMPLY <expr>
<patterns> ::= <loc(<pattern>)>+
<pattern> ::= PIPE UNDERSCORE
| PIPE <ident>
<expr> ::= <loc(<expr_r>)>
<ident_typ_q_item> ::= LPAREN <ident>+ <quant_kind> RPAREN
<ident_typ_q> ::= <ident_typ_q_item>+
<colon_type_opt> ::= [COLON <type_s>]
<colon_ident> ::= [COLON <ident>]
<from_expr> ::= [FROM <expr>]
<expr_r> ::= LPAREN RPAREN
| <quantifier> <ident> <quant_kind> COMMA <expr>
| <quantifier> <ident_typ_q> COMMA <expr>
| LET SOME <ident> <colon_type_opt> EQUAL <expr> IN <expr>
OTHERWISE <expr>
| LET <ident> <colon_type_opt> EQUAL <expr> IN <expr>
| VAR <ident> <colon_type_opt> EQUAL <expr>
| <expr> SEMI_COLON <expr>
| ASSERT <ident>
| LABEL <ident>
| BREAK
| FOR <colon_ident> <ident> IN <expr> DO <block> DONE
| ITER <colon_ident> <ident> <from_expr> TO <expr> DO <block> DONE
| IF <expr> THEN <expr>
| IF <expr> THEN <expr> ELSE <expr>
| <paren(<snl2(COMMA, <simple_expr>)>)>
| <expr> <assignment_operator_expr> <expr>
| TRANSFER <simple_expr> TO <simple_expr> <with_call_r>
| REQUIRE <simple_expr>
| FAILIF <simple_expr>
| RETURN <simple_expr>
| SOME <paren(<simple_expr>)>
| NONE
| <order_operations>
| <expr> <loc(<bin_operator>)> <expr>
| <loc(<un_operator>)> <expr>
| <simple_expr_r>
<block> ::= <loc(<block_r>)>
<block_r> ::= <expr_r> [SEMI_COLON]
<order_operation> ::= <expr> <loc(<ord_operator>)> <expr>
<with_call_r> ::= [CALL <ident> <paren(<sl(COMMA, <simple_expr>)>)>]
<order_operations> ::= <order_operation>
| <loc(<order_operations>)> <loc(<ordering_operator>)>
<expr>
<app_args> ::= LPAREN RPAREN
| LPAREN <snl(COMMA, <expr>)> RPAREN
<simple_expr> ::= <loc(<simple_expr_r>)>
<simple_expr_r> ::= MATCH <expr> WITH <branchs> END
| <ident> <app_args>
| <simple_expr> DOT <ident>
| <simple_expr> DOT <ident> <app_args>
| LBRACKET RBRACKET
| LBRACKET <expr> RBRACKET
| LBRACE <record_item> (SEMI_COLON <record_item>)* RBRACE
| <literal>
| <vt_dot> <ident>
| ANY
| INVALID_EXPR
| <paren(<block_r>)>
<vt_dot> ::= epsilon
| BEFORE DOT
| AT LPAREN <ident> RPAREN DOT
<label_exprs> ::= [<label_exprs_non_empty>]
<label_exprs_non_empty> ::= <snl(SEMI_COLON, <label_expr>)>
<label_expr> ::= <loc(<label_expr_unloc>)>
<label_expr_unloc> ::= <ident> COLON <expr>
<quant_kind> ::= COLON <type_s>
| IN <simple_expr>
<literal> ::= NUMBER
| DECIMAL
| TZ
| MTZ
| UTZ
| STRING
| ADDRESS
| <bool_value>
| DURATION
| DATE
| BYTES
<bool_value> ::= TRUE
| FALSE
<record_item> ::= <simple_expr>
| <ident> <assignment_operator_record> <simple_expr>
<quantifier> ::= FORALL
| EXISTS
<logical_operator> ::= AND
| OR
| IMPLY
| EQUIV
<comparison_operator> ::= EQUAL
| NEQUAL
<ordering_operator> ::= LESS
| LESSEQUAL
| GREATER
| GREATEREQUAL
<arithmetic_operator> ::= PLUS
| MINUS
| MULT
| SLASH
| DIV
| PERCENT
<unary_operator> ::= PLUS
| MINUS
| NOT
<bin_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>]
<security_args> ::= <paren([<security_arg> (COMMA <security_arg>)*])>
<security_arg> ::= <loc(<security_arg_unloc>)>
<security_arg_unloc> ::= <ident>
| <ident> DOT <ident>
| <bracket(<snl2(OR, <security_arg>)>)>
| <ident> <paren(<sl(COMMA, <security_arg>)>)>
| <ident> BUT <security_arg>
| <ident> TO <security_arg>
| <paren(<security_arg_unloc>)>
<postfix(X, P)> ::= X P