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

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct