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>
| <record>
| <entry>
| <entry_simple>
| <transition>
| <dextension>
| <namespace>
| <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>)>
<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>
<type_s> ::= <loc(<type_s_unloc>)>
<type_s_unloc> ::= <ident>
| <container> LESS <type_t> GREATER
| PKEY LESS <type_t> GREATER
| OPTION LESS <type_t> GREATER
| LIST LESS <type_t> GREATER
| SET LESS <type_t> GREATER
| MAP LESS <type_t> COMMA <type_s> GREATER
| ENTRYSIG LESS <type_t> GREATER
| <paren(<type_r>)>
<type_tuples> ::= <type_tuple>+
<type_tuple> ::= MULT <type_s>
<container> ::= AGGREGATE
| PARTITION
| VIEW
<shadow_asset_fields> ::= [SHADOW <asset_fields>]
<record> ::= RECORD [<extensions>] <ident> [<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 LBRACE <record_expr> (SEMI_COLON
<record_expr>)* RBRACE
<record_expr> ::= <loc(<record_expr_unloc>)>
<record_expr_unloc> ::= LBRACE <record_item> (SEMI_COLON <record_item>)*
RBRACE
<asset_post_options> ::= <asset_post_option>*
<asset_fields> ::= <braced(<fields>)>
<asset_options> ::= <asset_option>+
<asset_option> ::= IDENTIFIED BY <ident>+
| SORTED BY <ident>
| TO <ident>
<fields> ::= <sl(SEMI_COLON, <field>)>
<field_r> ::= <ident> [<extensions>] COLON <type_t> [REF] [<default_value>]
<field> ::= <loc(<field_r>)>
<ident> ::= <loc(IDENT)>
<entry> ::= ENTRY [<extensions>] <ident> <function_args> <transitems_eq>
<entry_simple> ::= ENTRY [<extensions>] <ident> <function_args>
<braced(<block>)>
<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 <entry_properties> FROM <expr>
<transitions> RBRACE
<transitems_eq> ::= [LBRACE <entry_properties> [<effect>] RBRACE]
<accept_transfer> ::= epsilon
| REFUSE_TRANSFER
| ACCEPT_TRANSFER
<entry_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
| AMPEQUAL
| PIPEEQUAL
<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>]
<for_ident_unloc> ::= <ident>
| LPAREN <ident> COMMA <ident> RPAREN
<for_ident> ::= <loc(<for_ident_unloc>)>
<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> <for_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>
| TRANSFER <simple_expr> TO <simple_expr> CALL <ident> LESS
<type_t> GREATER <paren(<expr>)>
| TRANSFER <simple_expr> TO ENTRY <ident> <simple_expr>
| TRANSFER <simple_expr> TO ENTRY SELF DOT <ident>
<paren(<sl(COMMA, <simple_expr>)>)>
| DOREQUIRE <simple_expr>
| DOFAILIF <simple_expr>
| FAIL <paren(<simple_expr>)>
| RETURN <simple_expr>
| SOME <paren(<simple_expr>)>
| NONE
| UNPACK LESS <type_t> GREATER <paren(<expr>)>
| SELF DOT <ident>
| ENTRYPOINT LESS <type_t> GREATER LPAREN <expr> COMMA <expr>
RPAREN
| <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>
<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> LBRACKET <expr> RBRACKET
| <simple_expr> DOT <ident> <app_args>
| LBRACKET RBRACKET
| LBRACKET <expr> RBRACKET
| LBRACE [<record_item> (SEMI_COLON <record_item>)*] RBRACE
| <literal>
| <vt> <ident>
| ANY
| INVALID_EXPR
| <paren(<block_r>)>
<vt_vset> ::= ADDED
| UNMOVED
| REMOVED
<vt_lbl> ::= BEFORE
| AT LPAREN <ident> RPAREN
<vt> ::= [<postfix(<vt_vset>, DOT)>] [<postfix(<vt_lbl>, 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> ::= NUMBERINT
| NUMBERNAT
| DECIMAL
| TZ
| MTZ
| UTZ
| STRING
| ADDRESS
| <bool_value>
| DURATION
| DATE
| BYTES
| PERCENT_LIT
<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
Edit on GitHub