package archetype

  1. Overview
  2. Docs
include MenhirLib.IncrementalEngine.INCREMENTAL_ENGINE with type token = token
type token = token
type production
type 'a env
type !'a checkpoint = private
  1. | InputNeeded of 'a env
  2. | Shifting of 'a env * 'a env * bool
  3. | AboutToReduce of 'a env * production
  4. | HandlingError of 'a env
  5. | Accepted of 'a
  6. | Rejected
val offer : 'a checkpoint -> (token * MenhirLib.IncrementalEngine.position * MenhirLib.IncrementalEngine.position) -> 'a checkpoint
type strategy = [
  1. | `Legacy
  2. | `Simplified
]
val resume : ?strategy:strategy -> 'a checkpoint -> 'a checkpoint
type supplier = unit -> token * MenhirLib.IncrementalEngine.position * MenhirLib.IncrementalEngine.position
val lexer_lexbuf_to_supplier : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> supplier
val loop : ?strategy:strategy -> supplier -> 'a checkpoint -> 'a
val loop_handle : ('a -> 'answer) -> ('a checkpoint -> 'answer) -> supplier -> 'a checkpoint -> 'answer
val loop_handle_undo : ('a -> 'answer) -> ('a checkpoint -> 'a checkpoint -> 'answer) -> supplier -> 'a checkpoint -> 'answer
val shifts : 'a checkpoint -> 'a env option
val acceptable : 'a checkpoint -> token -> MenhirLib.IncrementalEngine.position -> bool
type 'a lr1state
val number : 'a lr1state -> int
val production_index : production -> int
val find_production : int -> production
type element =
  1. | Element : 'a lr1state * 'a * MenhirLib.IncrementalEngine.position * MenhirLib.IncrementalEngine.position -> element
type stack = element MenhirLib.General.stream
val stack : 'a env -> stack
val top : 'a env -> element option
val pop_many : int -> 'a env -> 'a env option
val get : int -> 'a env -> element option
val current_state_number : 'a env -> int
val equal : 'a env -> 'a env -> bool
val positions : 'a env -> MenhirLib.IncrementalEngine.position * MenhirLib.IncrementalEngine.position
val env_has_default_reduction : 'a env -> bool
val state_has_default_reduction : 'a lr1state -> bool
val pop : 'a env -> 'a env option
val force_reduction : production -> 'a env -> 'a env
val input_needed : 'a env -> 'a checkpoint
type _ terminal =
  1. | T_error : unit terminal
  2. | T_XOR : unit terminal
  3. | T_WITH : unit terminal
  4. | T_WHILE : unit terminal
  5. | T_WHEN : unit terminal
  6. | T_VIEW : unit terminal
  7. | T_VARIABLE : unit terminal
  8. | T_VAR : unit terminal
  9. | T_UTZ : Big_int.big_int terminal
  10. | T_USE : unit terminal
  11. | T_UNPACK : unit terminal
  12. | T_UNMOVED : unit terminal
  13. | T_UNDERSCORE : unit terminal
  14. | T_TZ : Big_int.big_int terminal
  15. | T_TRUE : unit terminal
  16. | T_TRANSITION : unit terminal
  17. | T_TRANSFER : unit terminal
  18. | T_TO : unit terminal
  19. | T_THEN : unit terminal
  20. | T_STRING : string terminal
  21. | T_STATES : unit terminal
  22. | T_SPECIFICATION : unit terminal
  23. | T_SORTED : unit terminal
  24. | T_SOME : unit terminal
  25. | T_SLASH : unit terminal
  26. | T_SHADOW : unit terminal
  27. | T_SET : unit terminal
  28. | T_SEMI_COLON : unit terminal
  29. | T_SELF : unit terminal
  30. | T_SECURITY : unit terminal
  31. | T_RPAREN : unit terminal
  32. | T_RETURN : unit terminal
  33. | T_REQUIRE : unit terminal
  34. | T_REMOVED : unit terminal
  35. | T_REFUSE_TRANSFER : unit terminal
  36. | T_REF : unit terminal
  37. | T_RECORD : unit terminal
  38. | T_RBRACKET : unit terminal
  39. | T_RBRACE : unit terminal
  40. | T_PREDICATE : unit terminal
  41. | T_POSTCONDITION : unit terminal
  42. | T_PLUSEQUAL : unit terminal
  43. | T_PLUS : unit terminal
  44. | T_PKEY : unit terminal
  45. | T_PIPEEQUAL : unit terminal
  46. | T_PIPE : unit terminal
  47. | T_PERCENT_LIT : Big_int.big_int terminal
  48. | T_PERCENTRBRACKET : unit terminal
  49. | T_PERCENT : unit terminal
  50. | T_PARTITION : unit terminal
  51. | T_OTHERWISE : unit terminal
  52. | T_OR : unit terminal
  53. | T_OPTION : unit terminal
  54. | T_ON : unit terminal
  55. | T_NUMBERNAT : Big_int.big_int terminal
  56. | T_NUMBERINT : Big_int.big_int terminal
  57. | T_NOT : unit terminal
  58. | T_NONE : unit terminal
  59. | T_NEQUAL : unit terminal
  60. | T_NAMESPACE : unit terminal
  61. | T_MULTEQUAL : unit terminal
  62. | T_MULT : unit terminal
  63. | T_MTZ : Big_int.big_int terminal
  64. | T_MINUSEQUAL : unit terminal
  65. | T_MINUS : unit terminal
  66. | T_MATCH : unit terminal
  67. | T_MAP : unit terminal
  68. | T_LPAREN : unit terminal
  69. | T_LIST : unit terminal
  70. | T_LET : unit terminal
  71. | T_LESSEQUAL : unit terminal
  72. | T_LESS : unit terminal
  73. | T_LBRACKETPERCENT : unit terminal
  74. | T_LBRACKET : unit terminal
  75. | T_LBRACE : unit terminal
  76. | T_LABEL : unit terminal
  77. | T_ITER : unit terminal
  78. | T_INVARIANT : unit terminal
  79. | T_INVALID_EXPR : unit terminal
  80. | T_INVALID_EFFECT : unit terminal
  81. | T_INVALID_DECL : unit terminal
  82. | T_INITIALIZED : unit terminal
  83. | T_INITIAL : unit terminal
  84. | T_IN : unit terminal
  85. | T_IMPLY : unit terminal
  86. | T_IF : unit terminal
  87. | T_IDENTIFIED : unit terminal
  88. | T_IDENT : string terminal
  89. | T_GREATEREQUAL : unit terminal
  90. | T_GREATER : unit terminal
  91. | T_GETTER : unit terminal
  92. | T_FUNCTION : unit terminal
  93. | T_FROM : unit terminal
  94. | T_FORALL : unit terminal
  95. | T_FOR : unit terminal
  96. | T_FALSE : unit terminal
  97. | T_FAILS : unit terminal
  98. | T_FAILIF : unit terminal
  99. | T_FAIL : unit terminal
  100. | T_EXTENSION : unit terminal
  101. | T_EXISTS : unit terminal
  102. | T_EQUIV : unit terminal
  103. | T_EQUAL : unit terminal
  104. | T_EOF : unit terminal
  105. | T_ENUM : unit terminal
  106. | T_ENTRYPOINT : unit terminal
  107. | T_ENTRY : unit terminal
  108. | T_END : unit terminal
  109. | T_ELSE : unit terminal
  110. | T_EFFECT : unit terminal
  111. | T_DURATION : string terminal
  112. | T_DOT : unit terminal
  113. | T_DOREQUIRE : unit terminal
  114. | T_DONE : unit terminal
  115. | T_DOFAILIF : unit terminal
  116. | T_DO : unit terminal
  117. | T_DIVEQUAL : unit terminal
  118. | T_DIV : unit terminal
  119. | T_DEFINITION : unit terminal
  120. | T_DECIMAL : string terminal
  121. | T_DATE : string terminal
  122. | T_CONTRACT : unit terminal
  123. | T_CONSTANT : unit terminal
  124. | T_COMMA : unit terminal
  125. | T_COLONEQUAL : unit terminal
  126. | T_COLON : unit terminal
  127. | T_CALLED : unit terminal
  128. | T_CALL : unit terminal
  129. | T_BYTES : string terminal
  130. | T_BY : unit terminal
  131. | T_BUT : unit terminal
  132. | T_BEFORE : unit terminal
  133. | T_AT_UPDATE : unit terminal
  134. | T_AT_REMOVE : unit terminal
  135. | T_AT_ADD : unit terminal
  136. | T_AT : unit terminal
  137. | T_ASSET : unit terminal
  138. | T_ASSERT : unit terminal
  139. | T_ARCHETYPE : unit terminal
  140. | T_ANY : unit terminal
  141. | T_AND : unit terminal
  142. | T_AMPEQUAL : unit terminal
  143. | T_AGGREGATE : unit terminal
  144. | T_ADDRESS : string terminal
  145. | T_ADDED : unit terminal
  146. | T_ACCEPT_TRANSFER : unit terminal
type _ nonterminal =
  1. | N_vc_decl_VARIABLE_ : (ParseTree.lident * ParseTree.type_t * ParseTree.expr option * ParseTree.label_exprs * ParseTree.exts) nonterminal
  2. | N_vc_decl_CONSTANT_ : (ParseTree.lident * ParseTree.type_t * ParseTree.expr option * ParseTree.label_exprs * ParseTree.exts) nonterminal
  3. | N_variable : ParseTree.declaration_unloc nonterminal
  4. | N_type_s_unloc : ParseTree.type_r nonterminal
  5. | N_type_r : ParseTree.type_r nonterminal
  6. | N_transition_to_item : (ParseTree.lident * (ParseTree.expr * ParseTree.exts) option * (ParseTree.expr * ParseTree.exts) option) nonterminal
  7. | N_transition : ParseTree.declaration_unloc nonterminal
  8. | N_start_expr : ParseTree.expr nonterminal
  9. | N_specvariable : ParseTree.declaration_unloc nonterminal
  10. | N_specification_fun : ParseTree.specification nonterminal
  11. | N_specification_decl : ParseTree.declaration_unloc nonterminal
  12. | N_specgetter : ParseTree.declaration_unloc nonterminal
  13. | N_specfun_gen_GETTER_ : (ParseTree.lident * ParseTree.args * ParseTree.specification) nonterminal
  14. | N_specfun_gen_FUNCTION_ : (ParseTree.lident * ParseTree.args * ParseTree.specification) nonterminal
  15. | N_specfun_gen_ENTRY_ : (ParseTree.lident * ParseTree.args * ParseTree.specification) nonterminal
  16. | N_specfun : ParseTree.declaration_unloc nonterminal
  17. | N_specentry : ParseTree.declaration_unloc nonterminal
  18. | N_specasset : ParseTree.declaration_unloc nonterminal
  19. | N_spec_items : ParseTree.specification_item list nonterminal
  20. | N_snl2_OR_security_arg_ : ParseTree.security_arg list nonterminal
  21. | N_snl2_COMMA_simple_expr_ : ParseTree.expr list nonterminal
  22. | N_snl_SEMI_COLON_security_item_ : ParseTree.security_item list nonterminal
  23. | N_snl_SEMI_COLON_rf_WITH__ : (ParseTree.lident * ParseTree.expr * ParseTree.expr option) list nonterminal
  24. | N_snl_SEMI_COLON_rf_OTHERWISE__ : (ParseTree.lident * ParseTree.expr * ParseTree.expr option) list nonterminal
  25. | N_snl_SEMI_COLON_label_expr_ : ParseTree.label_exprs nonterminal
  26. | N_snl_SEMI_COLON_field_ : ParseTree.field list nonterminal
  27. | N_snl_COMMA_simple_expr_ : ParseTree.expr list nonterminal
  28. | N_snl_COMMA_security_arg_ : ParseTree.security_arg list nonterminal
  29. | N_snl_COMMA_function_arg_ : ParseTree.args nonterminal
  30. | N_snl_COMMA_expr_ : ParseTree.expr list nonterminal
  31. | N_sl_SEMI_COLON_security_item_ : ParseTree.security_item list nonterminal
  32. | N_sl_SEMI_COLON_field_ : ParseTree.field list nonterminal
  33. | N_sl_COMMA_simple_expr_ : ParseTree.expr list nonterminal
  34. | N_sl_COMMA_security_arg_ : ParseTree.security_arg list nonterminal
  35. | N_sl_COMMA_function_arg_ : ParseTree.args nonterminal
  36. | N_simple_expr_r : ParseTree.expr_unloc nonterminal
  37. | N_separated_nonempty_list_SEMI_COLON_recupdate_item_ : (ParseTree.lident * ParseTree.expr) list nonterminal
  38. | N_separated_nonempty_list_SEMI_COLON_record_item_ : ParseTree.record_item list nonterminal
  39. | N_separated_nonempty_list_SEMI_COLON_record_expr_ : ParseTree.expr list nonterminal
  40. | N_separated_nonempty_list_COMMA_security_arg_ : ParseTree.security_arg list nonterminal
  41. | N_security_decl_unloc : ParseTree.security_unloc nonterminal
  42. | N_security_decl : ParseTree.declaration_unloc nonterminal
  43. | N_security_arg_unloc : ParseTree.security_arg_unloc nonterminal
  44. | N_rf_WITH_ : (ParseTree.lident * ParseTree.expr * ParseTree.expr option) nonterminal
  45. | N_rf_OTHERWISE_ : (ParseTree.lident * ParseTree.expr * ParseTree.expr option) nonterminal
  46. | N_recupdate_item : (ParseTree.lident * ParseTree.expr) nonterminal
  47. | N_record_item : ParseTree.record_item nonterminal
  48. | N_record : ParseTree.declaration_unloc nonterminal
  49. | N_pattern : ParseTree.pattern_unloc nonterminal
  50. | N_order_operations : ParseTree.expr_unloc nonterminal
  51. | N_order_operation : ParseTree.expr_unloc nonterminal
  52. | N_option_with_effect_ : (ParseTree.expr * ParseTree.exts) option nonterminal
  53. | N_option_specification_fun_ : ParseTree.specification option nonterminal
  54. | N_option_simple_expr_ : ParseTree.expr option nonterminal
  55. | N_option_rfi_WITH__ : ParseTree.expr option nonterminal
  56. | N_option_rfi_OTHERWISE__ : ParseTree.expr option nonterminal
  57. | N_option_require_value_ : (ParseTree.expr * ParseTree.exts) option nonterminal
  58. | N_option_require_ : ((ParseTree.lident * ParseTree.expr * ParseTree.expr option) list * ParseTree.exts) option nonterminal
  59. | N_option_on_value_ : (ParseTree.lident * ParseTree.type_t) option nonterminal
  60. | N_option_function_return_ : ParseTree.type_t option nonterminal
  61. | N_option_failif_ : ((ParseTree.lident * ParseTree.expr * ParseTree.expr option) list * ParseTree.exts) option nonterminal
  62. | N_option_extensions_ : ParseTree.exts nonterminal
  63. | N_option_effect_ : (ParseTree.expr * ParseTree.exts) option nonterminal
  64. | N_option_default_value_ : ParseTree.expr option nonterminal
  65. | N_option_calledby_ : (ParseTree.expr * ParseTree.exts) option nonterminal
  66. | N_option_bracket_asset_operation__ : ParseTree.asset_operation option nonterminal
  67. | N_option_asset_options_ : ParseTree.asset_option list option nonterminal
  68. | N_option_asset_fields_ : ParseTree.field list option nonterminal
  69. | N_option_SEMI_COLON_ : unit option nonterminal
  70. | N_on_value : (ParseTree.lident * ParseTree.type_t) nonterminal
  71. | N_nonempty_list_type_tuple_ : ParseTree.type_t list nonterminal
  72. | N_nonempty_list_transition_to_item_ : ParseTree.transition nonterminal
  73. | N_nonempty_list_spec_fail_item_ : (ParseTree.lident * ParseTree.lident * ParseTree.type_t * ParseTree.expr) list nonterminal
  74. | N_nonempty_list_pipe_ident_ : (ParseTree.lident * ParseTree.enum_option list) list nonterminal
  75. | N_nonempty_list_loc_pattern__ : ParseTree.pattern list nonterminal
  76. | N_nonempty_list_ident_typ_q_item_ : (string Location.loced * ParseTree.quantifier_kind) list list nonterminal
  77. | N_nonempty_list_ident_ : ParseTree.lident list nonterminal
  78. | N_nonempty_list_extension_ : ParseTree.extension list nonterminal
  79. | N_nonempty_list_enum_option_ : ParseTree.enum_option list nonterminal
  80. | N_nonempty_list_declaration_ : ParseTree.declaration list nonterminal
  81. | N_nonempty_list_branch_ : ParseTree.branch list nonterminal
  82. | N_nonempty_list_asset_option_ : ParseTree.asset_option list nonterminal
  83. | N_nonempty_list_asset_operation_enum_ : ParseTree.asset_operation_enum list nonterminal
  84. | N_namespace : ParseTree.declaration_unloc nonterminal
  85. | N_main : ParseTree.archetype nonterminal
  86. | N_loption_separated_nonempty_list_SEMI_COLON_recupdate_item__ : (ParseTree.lident * ParseTree.expr) list nonterminal
  87. | N_loption_separated_nonempty_list_SEMI_COLON_record_item__ : ParseTree.record_item list nonterminal
  88. | N_loption_separated_nonempty_list_COMMA_security_arg__ : ParseTree.security_arg list nonterminal
  89. | N_literal : ParseTree.literal nonterminal
  90. | N_list_loc_spec_variable__ : ParseTree.specification_item_unloc Location.loced list nonterminal
  91. | N_list_loc_spec_predicate__ : ParseTree.specification_item_unloc Location.loced list nonterminal
  92. | N_list_loc_spec_postcondition__ : ParseTree.specification_item_unloc Location.loced list nonterminal
  93. | N_list_loc_spec_fails__ : ParseTree.specification_item_unloc Location.loced list nonterminal
  94. | N_list_loc_spec_effect__ : ParseTree.specification_item_unloc Location.loced list nonterminal
  95. | N_list_loc_spec_definition__ : ParseTree.specification_item_unloc Location.loced list nonterminal
  96. | N_list_loc_spec_contract_invariant__ : ParseTree.specification_item_unloc Location.loced list nonterminal
  97. | N_list_loc_spec_assert__ : ParseTree.specification_item_unloc Location.loced list nonterminal
  98. | N_list_invars_ : ParseTree.invariants nonterminal
  99. | N_list_function_item_ : ParseTree.s_function Location.loced list nonterminal
  100. | N_list_asset_post_option_ : ParseTree.asset_post_option list nonterminal
  101. | N_label_expr_unloc : (ParseTree.lident * ParseTree.expr) nonterminal
  102. | N_implementation_archetype : ParseTree.archetype_unloc nonterminal
  103. | N_ident_typ_q : (string Location.loced * ParseTree.quantifier_kind) list nonterminal
  104. | N_getter_decl : ParseTree.declaration_unloc nonterminal
  105. | N_function_item : ParseTree.s_function Location.loced nonterminal
  106. | N_function_decl : ParseTree.declaration_unloc nonterminal
  107. | N_field_r : ParseTree.field_unloc nonterminal
  108. | N_extension_r : ParseTree.extension_unloc nonterminal
  109. | N_expr_r : ParseTree.expr_unloc nonterminal
  110. | N_equal_enum_values : (ParseTree.lident * ParseTree.enum_option list) list nonterminal
  111. | N_enum_values : (ParseTree.lident * ParseTree.enum_option list) list nonterminal
  112. | N_enum_option : ParseTree.enum_option nonterminal
  113. | N_enum : ParseTree.declaration_unloc nonterminal
  114. | N_entry_simple : ParseTree.declaration_unloc nonterminal
  115. | N_entry_properties : ParseTree.entry_properties nonterminal
  116. | N_entry : ParseTree.declaration_unloc nonterminal
  117. | N_effect : (ParseTree.expr * ParseTree.exts) nonterminal
  118. | N_dextension : ParseTree.declaration_unloc nonterminal
  119. | N_declaration_r : ParseTree.declaration_unloc nonterminal
  120. | N_constant : ParseTree.declaration_unloc nonterminal
  121. | N_calledby : (ParseTree.expr * ParseTree.exts) nonterminal
  122. | N_branch : ParseTree.branch nonterminal
  123. | N_boption_REF_ : bool nonterminal
  124. | N_asset_post_option : ParseTree.asset_post_option nonterminal
  125. | N_asset_option : ParseTree.asset_option nonterminal
  126. | N_asset : ParseTree.declaration_unloc nonterminal
  127. | N_archetype_r : ParseTree.archetype_unloc nonterminal
  128. | N_archetype_extension : ParseTree.archetype_unloc nonterminal
  129. | N_archetype : ParseTree.declaration_unloc nonterminal
include MenhirLib.IncrementalEngine.INSPECTION with type 'a lr1state := 'a lr1state with type production := production with type 'a terminal := 'a terminal with type 'a nonterminal := 'a nonterminal with type 'a env := 'a env
type !'a1 symbol =
  1. | T : 'a terminal -> 'a symbol
  2. | N : 'a0 nonterminal -> 'a0 symbol
type xsymbol =
  1. | X : 'a symbol -> xsymbol
type item = production * int
val compare_terminals : 'a terminal -> 'b terminal -> int
val compare_nonterminals : 'a nonterminal -> 'b nonterminal -> int
val compare_symbols : xsymbol -> xsymbol -> int
val compare_productions : production -> production -> int
val compare_items : item -> item -> int
val incoming_symbol : 'a lr1state -> 'a symbol
val items : 'a lr1state -> item list
val lhs : production -> xsymbol
val rhs : production -> xsymbol list
val nullable : 'a nonterminal -> bool
val first : 'a nonterminal -> 'b terminal -> bool
val xfirst : xsymbol -> 'a terminal -> bool
val foreach_terminal : (xsymbol -> 'a -> 'a) -> 'a -> 'a
val foreach_terminal_but_error : (xsymbol -> 'a -> 'a) -> 'a -> 'a
val feed : 'a symbol -> MenhirLib.IncrementalEngine.position -> 'a -> MenhirLib.IncrementalEngine.position -> 'b env -> 'b env
OCaml

Innovation. Community. Security.