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 resume : 'a checkpoint -> 'a checkpoint
val lexer_lexbuf_to_supplier : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> supplier
val loop : 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
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 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_WITH : unit terminal
  3. | T_WHEN : unit terminal
  4. | T_VARIABLE : unit terminal
  5. | T_UNDERSCORE : unit terminal
  6. | T_TZ : Big_int.big_int terminal
  7. | T_TRUE : unit terminal
  8. | T_TRANSITION : unit terminal
  9. | T_TRANSFER : unit terminal
  10. | T_TO : unit terminal
  11. | T_THEOREM : unit terminal
  12. | T_THEN : unit terminal
  13. | T_STRING : string terminal
  14. | T_STATES : unit terminal
  15. | T_SPECIFICATION : unit terminal
  16. | T_SORTED : unit terminal
  17. | T_SOME : unit terminal
  18. | T_SEMI_COLON : unit terminal
  19. | T_SECURITY : unit terminal
  20. | T_RPAREN : unit terminal
  21. | T_RETURN : unit terminal
  22. | T_REQUIRE : unit terminal
  23. | T_REFUSE_TRANSFER : unit terminal
  24. | T_REF : unit terminal
  25. | T_RECORD : unit terminal
  26. | T_RBRACKET : unit terminal
  27. | T_RBRACE : unit terminal
  28. | T_RATIONAL : (Big_int.big_int * Big_int.big_int) terminal
  29. | T_PREDICATE : unit terminal
  30. | T_POSTCONDITION : unit terminal
  31. | T_PLUSEQUAL : unit terminal
  32. | T_PLUS : unit terminal
  33. | T_PIPE : unit terminal
  34. | T_PERCENTRBRACKET : unit terminal
  35. | T_PERCENT : unit terminal
  36. | T_PARTITION : unit terminal
  37. | T_OTHERWISE : unit terminal
  38. | T_OREQUAL : unit terminal
  39. | T_OR : unit terminal
  40. | T_OPTION : unit terminal
  41. | T_ON : unit terminal
  42. | T_OF : unit terminal
  43. | T_NUMBER : Big_int.big_int terminal
  44. | T_NOT : unit terminal
  45. | T_NONE : unit terminal
  46. | T_NEQUAL : unit terminal
  47. | T_NAMESPACE : unit terminal
  48. | T_MULTEQUAL : unit terminal
  49. | T_MULT : unit terminal
  50. | T_MTZ : Big_int.big_int terminal
  51. | T_MINUSEQUAL : unit terminal
  52. | T_MINUS : unit terminal
  53. | T_MATCH : unit terminal
  54. | T_LPAREN : unit terminal
  55. | T_LET : unit terminal
  56. | T_LESSEQUAL : unit terminal
  57. | T_LESS : unit terminal
  58. | T_LEMMA : unit terminal
  59. | T_LBRACKETPERCENT : unit terminal
  60. | T_LBRACKET : unit terminal
  61. | T_LBRACE : unit terminal
  62. | T_ITER : unit terminal
  63. | T_INVARIANT : unit terminal
  64. | T_INVALID_EXPR : unit terminal
  65. | T_INVALID_EFFECT : unit terminal
  66. | T_INVALID_DECL : unit terminal
  67. | T_INSTANCE : unit terminal
  68. | T_INITIALIZED : unit terminal
  69. | T_INITIAL : unit terminal
  70. | T_IN : unit terminal
  71. | T_IMPLY : unit terminal
  72. | T_IF : unit terminal
  73. | T_IDENTIFIED : unit terminal
  74. | T_IDENT : string terminal
  75. | T_GREATEREQUAL : unit terminal
  76. | T_GREATER : unit terminal
  77. | T_FUNCTION : unit terminal
  78. | T_FROM : unit terminal
  79. | T_FORALL : unit terminal
  80. | T_FOR : unit terminal
  81. | T_FALSE : unit terminal
  82. | T_FAILIF : unit terminal
  83. | T_EXTENSION : unit terminal
  84. | T_EXISTS : unit terminal
  85. | T_EQUIV : unit terminal
  86. | T_EQUAL : unit terminal
  87. | T_EOF : unit terminal
  88. | T_ENUM : unit terminal
  89. | T_END : unit terminal
  90. | T_ELSE : unit terminal
  91. | T_EFFECT : unit terminal
  92. | T_DURATION : string terminal
  93. | T_DOT : unit terminal
  94. | T_DIVEQUAL : unit terminal
  95. | T_DIV : unit terminal
  96. | T_DEFINITION : unit terminal
  97. | T_DATE : string terminal
  98. | T_CONTRACT : unit terminal
  99. | T_CONSTANT : unit terminal
  100. | T_COMMA : unit terminal
  101. | T_COLONEQUAL : unit terminal
  102. | T_COLONCOLON : unit terminal
  103. | T_COLON : unit terminal
  104. | T_COLLECTION : unit terminal
  105. | T_CALLED : unit terminal
  106. | T_BY : unit terminal
  107. | T_BUT : unit terminal
  108. | T_BREAK : unit terminal
  109. | T_BACK : unit terminal
  110. | T_AT_UPDATE : unit terminal
  111. | T_AT_REMOVE : unit terminal
  112. | T_AT_ADD : unit terminal
  113. | T_AT : unit terminal
  114. | T_ASSET : unit terminal
  115. | T_ASSERT : unit terminal
  116. | T_ARCHETYPE : unit terminal
  117. | T_ANDEQUAL : unit terminal
  118. | T_AND : unit terminal
  119. | T_ADDRESS : string terminal
  120. | T_ACTION : unit terminal
  121. | T_ACCEPT_TRANSFER : unit terminal
type _ nonterminal =
  1. | N_vc_decl_VARIABLE_ : (ParseTree.lident * ParseTree.type_t * ParseTree.value_option list option * ParseTree.expr option * ParseTree.exts) nonterminal
  2. | N_vc_decl_CONSTANT_ : (ParseTree.lident * ParseTree.type_t * ParseTree.value_option list option * ParseTree.expr option * ParseTree.exts) nonterminal
  3. | N_variable : ParseTree.declaration_unloc nonterminal
  4. | N_value_option : ParseTree.value_option nonterminal
  5. | N_types : ParseTree.type_t list nonterminal
  6. | N_type_s_unloc : ParseTree.type_r nonterminal
  7. | N_type_r : ParseTree.type_r nonterminal
  8. | N_transition_to_item : (ParseTree.lident * (ParseTree.expr * ParseTree.exts) option * (ParseTree.expr * ParseTree.exts) option) nonterminal
  9. | N_transition : ParseTree.declaration_unloc nonterminal
  10. | N_start_expr : ParseTree.expr nonterminal
  11. | N_specification_fun : ParseTree.specification nonterminal
  12. | N_specification_decl : ParseTree.declaration_unloc nonterminal
  13. | N_spec_items : ParseTree.specification_item list nonterminal
  14. | N_snl2_OR_security_arg_ : ParseTree.security_arg list nonterminal
  15. | N_snl2_COMMA_simple_expr_ : ParseTree.expr list nonterminal
  16. | N_simple_expr_r : ParseTree.expr_unloc nonterminal
  17. | N_signature : ParseTree.signature nonterminal
  18. | N_separated_nonempty_list_SEMI_COLON_record_item_ : ParseTree.record_item list nonterminal
  19. | N_separated_nonempty_list_COMMA_type_t_ : ParseTree.type_t list nonterminal
  20. | N_security_decl_unloc : ParseTree.security_unloc nonterminal
  21. | N_security_decl : ParseTree.declaration_unloc nonterminal
  22. | N_security_arg_unloc : ParseTree.security_arg_unloc nonterminal
  23. | N_security_arg_ext_unloc : ParseTree.security_arg_unloc nonterminal
  24. | N_require : (ParseTree.label_exprs * ParseTree.exts) nonterminal
  25. | N_record_item : ParseTree.record_item nonterminal
  26. | N_pattern : ParseTree.pattern_unloc nonterminal
  27. | N_order_operations : ParseTree.expr_unloc nonterminal
  28. | N_order_operation : ParseTree.expr_unloc nonterminal
  29. | N_option_with_effect_ : (ParseTree.expr * ParseTree.exts) option nonterminal
  30. | N_option_value_options_ : ParseTree.value_option list option nonterminal
  31. | N_option_specification_fun_ : ParseTree.specification option nonterminal
  32. | N_option_simple_expr_ : ParseTree.expr option nonterminal
  33. | N_option_require_value_ : (ParseTree.expr * ParseTree.exts) option nonterminal
  34. | N_option_require_ : (ParseTree.label_exprs * ParseTree.exts) option nonterminal
  35. | N_option_on_value_ : (ParseTree.lident * ParseTree.lident) option nonterminal
  36. | N_option_function_return_ : ParseTree.type_t option nonterminal
  37. | N_option_failif_ : (ParseTree.label_exprs * ParseTree.exts) option nonterminal
  38. | N_option_extensions_ : ParseTree.exts nonterminal
  39. | N_option_effect_ : (ParseTree.expr * ParseTree.exts) option nonterminal
  40. | N_option_default_value_ : ParseTree.expr option nonterminal
  41. | N_option_calledby_ : (ParseTree.expr * ParseTree.exts) option nonterminal
  42. | N_option_bracket_asset_operation__ : ParseTree.asset_operation option nonterminal
  43. | N_option_asset_options_ : ParseTree.asset_option list option nonterminal
  44. | N_option_asset_fields_ : ParseTree.field_unloc Location.loced list option nonterminal
  45. | N_on_value : (ParseTree.lident * ParseTree.lident) nonterminal
  46. | N_nonempty_list_value_option_ : ParseTree.value_option list nonterminal
  47. | N_nonempty_list_type_tuple_ : ParseTree.type_t list nonterminal
  48. | N_nonempty_list_transition_to_item_ : ParseTree.transition nonterminal
  49. | N_nonempty_list_terminated_field_SEMI_COLON__ : ParseTree.field_unloc Location.loced list nonterminal
  50. | N_nonempty_list_signature_ : ParseTree.signature list nonterminal
  51. | N_nonempty_list_security_item_ : ParseTree.security_item list nonterminal
  52. | N_nonempty_list_security_arg_ : ParseTree.security_arg list nonterminal
  53. | N_nonempty_list_pipe_ident_ : (ParseTree.lident * ParseTree.enum_option list) list nonterminal
  54. | N_nonempty_list_loc_pattern__ : ParseTree.pattern list nonterminal
  55. | N_nonempty_list_label_expr_ : ParseTree.label_exprs nonterminal
  56. | N_nonempty_list_ident_typ_q_item_ : (string Location.loced * ParseTree.quantifier_kind) list list nonterminal
  57. | N_nonempty_list_ident_ : ParseTree.lident list nonterminal
  58. | N_nonempty_list_function_arg_ : ParseTree.args nonterminal
  59. | N_nonempty_list_extension_ : ParseTree.extension list nonterminal
  60. | N_nonempty_list_enum_option_ : ParseTree.enum_option list nonterminal
  61. | N_nonempty_list_declaration_ : ParseTree.declaration list nonterminal
  62. | N_nonempty_list_branch_ : (ParseTree.pattern list * ParseTree.expr) list nonterminal
  63. | N_nonempty_list_asset_option_ : ParseTree.asset_option list nonterminal
  64. | N_nonempty_list_asset_operation_enum_ : ParseTree.asset_operation_enum list nonterminal
  65. | N_namespace : ParseTree.declaration_unloc nonterminal
  66. | N_main : ParseTree.archetype nonterminal
  67. | N_literal : ParseTree.literal nonterminal
  68. | N_list_loc_spec_variable__ : ParseTree.specification_item_unloc Location.loced list nonterminal
  69. | N_list_loc_spec_theorem__ : ParseTree.specification_item_unloc Location.loced list nonterminal
  70. | N_list_loc_spec_predicate__ : ParseTree.specification_item_unloc Location.loced list nonterminal
  71. | N_list_loc_spec_postcondition__ : ParseTree.specification_item_unloc Location.loced list nonterminal
  72. | N_list_loc_spec_lemma__ : ParseTree.specification_item_unloc Location.loced list nonterminal
  73. | N_list_loc_spec_effect__ : ParseTree.specification_item_unloc Location.loced list nonterminal
  74. | N_list_loc_spec_definition__ : ParseTree.specification_item_unloc Location.loced list nonterminal
  75. | N_list_loc_spec_assert__ : ParseTree.specification_item_unloc Location.loced list nonterminal
  76. | N_list_invars_ : ParseTree.invariants nonterminal
  77. | N_list_function_item_ : ParseTree.s_function Location.loced list nonterminal
  78. | N_list_asset_post_option_ : ParseTree.asset_post_option list nonterminal
  79. | N_instance : ParseTree.declaration_unloc nonterminal
  80. | N_implementation_archetype : ParseTree.archetype_unloc nonterminal
  81. | N_ident_typ_q : (string Location.loced * ParseTree.quantifier_kind) list nonterminal
  82. | N_function_item : ParseTree.s_function Location.loced nonterminal
  83. | N_function_decl : ParseTree.declaration_unloc nonterminal
  84. | N_field_r : ParseTree.field_unloc nonterminal
  85. | N_failif : (ParseTree.label_exprs * ParseTree.exts) nonterminal
  86. | N_extension_r : ParseTree.extension_unloc nonterminal
  87. | N_expr_r : ParseTree.expr_unloc nonterminal
  88. | N_equal_enum_values : (ParseTree.lident * ParseTree.enum_option list) list nonterminal
  89. | N_enum_values : (ParseTree.lident * ParseTree.enum_option list) list nonterminal
  90. | N_enum_option : ParseTree.enum_option nonterminal
  91. | N_enum : ParseTree.declaration_unloc nonterminal
  92. | N_effect : (ParseTree.expr * ParseTree.exts) nonterminal
  93. | N_dextension : ParseTree.declaration_unloc nonterminal
  94. | N_declaration_r : ParseTree.declaration_unloc nonterminal
  95. | N_contract : ParseTree.declaration_unloc nonterminal
  96. | N_constant : ParseTree.declaration_unloc nonterminal
  97. | N_calledby : (ParseTree.expr * ParseTree.exts) nonterminal
  98. | N_branch : (ParseTree.pattern list * ParseTree.expr) nonterminal
  99. | N_boption_REF_ : bool nonterminal
  100. | N_boption_BACK_ : bool nonterminal
  101. | N_asset_post_option : ParseTree.asset_post_option nonterminal
  102. | N_asset_option : ParseTree.asset_option nonterminal
  103. | N_asset : ParseTree.declaration_unloc nonterminal
  104. | N_archetype_r : ParseTree.archetype_unloc nonterminal
  105. | N_archetype_extension : ParseTree.archetype_unloc nonterminal
  106. | N_archetype : ParseTree.declaration_unloc nonterminal
  107. | N_action_properties : ParseTree.action_properties nonterminal
  108. | N_action : 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