package p4spectec

  1. Overview
  2. Docs
P4-SpecTec: A mechanization toolchain for the P4 Programming Language

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (2)

Authors

  1. K
    KAIST PLRG

Maintainers

  1. 9
    99jaehyunlee@kaist.ac.kr

Sources

v0.1.2.tar.gz
md5=1a3bc0a385fe1ecf403c019f49aa6de6
sha512=5d20b5821f33e2a3a5419b208606f27c01511994c2b3b1e1cdf4c077056dfd0aa81682af0720e1060ee2bfb0341918fcc4c53159820205a2bc32b725e5c1a714

doc/p4/P4/Parser/MenhirInterpreter/index.html

Module Parser.MenhirInterpreterSource

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:??? -> '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:??? -> 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
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
Sourcetype _ terminal =
  1. | T_error : unit terminal
  2. | T_VOID : unit terminal
  3. | T_VARBIT : unit terminal
  4. | T_VALUE_SET : unit terminal
  5. | T_UNEXPECTED_TOKEN : Lang.Il.value terminal
  6. | T_TYPENAME : unit terminal
  7. | T_TYPEDEF : unit terminal
  8. | T_TYPE : unit terminal
  9. | T_TUPLE : unit terminal
  10. | T_TRUE : unit terminal
  11. | T_TRANSITION : unit terminal
  12. | T_THIS : unit terminal
  13. | T_TABLE : unit terminal
  14. | T_SWITCH : unit terminal
  15. | T_STRUCT : unit terminal
  16. | T_STRING_LITERAL : Lang.Il.value terminal
  17. | T_STRING : unit terminal
  18. | T_STATE : unit terminal
  19. | T_SHR_ASSIGN : unit terminal
  20. | T_SHL_ASSIGN : unit terminal
  21. | T_SHL : unit terminal
  22. | T_SEMICOLON : unit terminal
  23. | T_SELECT : unit terminal
  24. | T_R_PAREN : unit terminal
  25. | T_R_BRACKET : unit terminal
  26. | T_R_BRACE : unit terminal
  27. | T_R_ANGLE_SHIFT : unit terminal
  28. | T_R_ANGLE : unit terminal
  29. | T_RETURN : unit terminal
  30. | T_RANGE : unit terminal
  31. | T_QUESTION : unit terminal
  32. | T_PRIORITY : unit terminal
  33. | T_PRAGMA_END : unit terminal
  34. | T_PRAGMA : unit terminal
  35. | T_PLUS_SAT_ASSIGN : unit terminal
  36. | T_PLUS_SAT : unit terminal
  37. | T_PLUS_ASSIGN : unit terminal
  38. | T_PLUSPLUS : unit terminal
  39. | T_PLUSCOLON : unit terminal
  40. | T_PLUS : unit terminal
  41. | T_PARSER : unit terminal
  42. | T_PACKAGE : unit terminal
  43. | T_OUT : unit terminal
  44. | T_OR : unit terminal
  45. | T_NUMBER_INT : (Lang.Il.value * string) terminal
  46. | T_NUMBER : (Lang.Il.value * string) terminal
  47. | T_NOT : unit terminal
  48. | T_NE : unit terminal
  49. | T_NAME : Lang.Il.value terminal
  50. | T_MUL_ASSIGN : unit terminal
  51. | T_MUL : unit terminal
  52. | T_MOD_ASSIGN : unit terminal
  53. | T_MOD : unit terminal
  54. | T_MINUS_SAT_ASSIGN : unit terminal
  55. | T_MINUS_SAT : unit terminal
  56. | T_MINUS_ASSIGN : unit terminal
  57. | T_MINUS : unit terminal
  58. | T_MATCH_KIND : unit terminal
  59. | T_MASK : unit terminal
  60. | T_L_PAREN : unit terminal
  61. | T_L_BRACKET : unit terminal
  62. | T_L_BRACE : unit terminal
  63. | T_L_ANGLE_ARGS : unit terminal
  64. | T_L_ANGLE : unit terminal
  65. | T_LIST : unit terminal
  66. | T_LE : unit terminal
  67. | T_KEY : unit terminal
  68. | T_INVALID : unit terminal
  69. | T_INT : unit terminal
  70. | T_INOUT : unit terminal
  71. | T_IN : unit terminal
  72. | T_IF : unit terminal
  73. | T_IDENTIFIER : unit terminal
  74. | T_HEADER_UNION : unit terminal
  75. | T_HEADER : unit terminal
  76. | T_GE : unit terminal
  77. | T_FOR : unit terminal
  78. | T_FALSE : unit terminal
  79. | T_EXTERN : unit terminal
  80. | T_EXIT : unit terminal
  81. | T_ERROR : unit terminal
  82. | T_EQ : unit terminal
  83. | T_ENUM : unit terminal
  84. | T_ENTRIES : unit terminal
  85. | T_END : unit terminal
  86. | T_ELSE : unit terminal
  87. | T_DOTS : unit terminal
  88. | T_DOT : unit terminal
  89. | T_DONTCARE : unit terminal
  90. | T_DIV_ASSIGN : unit terminal
  91. | T_DIV : unit terminal
  92. | T_DEFAULT : unit terminal
  93. | T_CONTROL : unit terminal
  94. | T_CONTINUE : unit terminal
  95. | T_CONST : unit terminal
  96. | T_COMPLEMENT : unit terminal
  97. | T_COMMA : unit terminal
  98. | T_COLON : unit terminal
  99. | T_BREAK : unit terminal
  100. | T_BOOL : unit terminal
  101. | T_BIT_XOR_ASSIGN : unit terminal
  102. | T_BIT_XOR : unit terminal
  103. | T_BIT_OR_ASSIGN : unit terminal
  104. | T_BIT_OR : unit terminal
  105. | T_BIT_AND_ASSIGN : unit terminal
  106. | T_BIT_AND : unit terminal
  107. | T_BIT : unit terminal
  108. | T_AT : unit terminal
  109. | T_ASSIGN : unit terminal
  110. | T_APPLY : unit terminal
  111. | T_AND : unit terminal
  112. | T_ACTIONS : unit terminal
  113. | T_ACTION : unit terminal
  114. | T_ABSTRACT : unit terminal
Sourcetype _ nonterminal =
  1. | N_variableDeclaration : Value.t nonterminal
  2. | N_valueSetType : Value.t nonterminal
  3. | N_valueSetDeclaration : Value.t nonterminal
  4. | N_typedefDeclaration : Value.t nonterminal
  5. | N_typedef : Value.t nonterminal
  6. | N_typeRef : Value.t nonterminal
  7. | N_typeParameterListOpt : Value.t nonterminal
  8. | N_typeParameterList : Value.t nonterminal
  9. | N_typeParameter : Value.t nonterminal
  10. | N_typeOrVoid : Value.t nonterminal
  11. | N_typeName : Value.t nonterminal
  12. | N_typeIdentifier : Value.t nonterminal
  13. | N_typeFieldList : Value.t nonterminal
  14. | N_typeField : Value.t nonterminal
  15. | N_typeDeclaration : Value.t nonterminal
  16. | N_typeArgumentList : Value.t nonterminal
  17. | N_typeArgument : Value.t nonterminal
  18. | N_tupleType : Value.t nonterminal
  19. | N_tupleKeysetExpression : Value.t nonterminal
  20. | N_transitionStatement : Value.t nonterminal
  21. | N_trailingCommaOpt : Value.t nonterminal
  22. | N_tablePropertyList : Value.t nonterminal
  23. | N_tableProperty : Value.t nonterminal
  24. | N_tableKeyList : Value.t nonterminal
  25. | N_tableKey : Value.t nonterminal
  26. | N_tableEntryPriority : Value.t nonterminal
  27. | N_tableEntryList : Value.t nonterminal
  28. | N_tableEntry : Value.t nonterminal
  29. | N_tableDeclaration : Value.t nonterminal
  30. | N_tableCustomName : Value.t nonterminal
  31. | N_tableActionReference : Value.t nonterminal
  32. | N_tableActionList : Value.t nonterminal
  33. | N_tableAction : Value.t nonterminal
  34. | N_switchStatement : Value.t nonterminal
  35. | N_switchLabel : Value.t nonterminal
  36. | N_switchCaseList : Value.t nonterminal
  37. | N_switchCase : Value.t nonterminal
  38. | N_structuredAnnotationBody : Value.t nonterminal
  39. | N_structTypeDeclaration : Value.t nonterminal
  40. | N_stringLiteral : Value.t nonterminal
  41. | N_statement : Value.t nonterminal
  42. | N_stateExpression : Value.t nonterminal
  43. | N_specializedType : Value.t nonterminal
  44. | N_simpleKeysetExpressionList : Value.t nonterminal
  45. | N_simpleKeysetExpression : Value.t nonterminal
  46. | N_set_parent_namespace : unit nonterminal
  47. | N_selectExpression : Value.t nonterminal
  48. | N_selectCaseList : Value.t nonterminal
  49. | N_selectCase : Value.t nonterminal
  50. | N_returnStatement : Value.t nonterminal
  51. | N_realTypeArgumentList : Value.t nonterminal
  52. | N_realTypeArgument : Value.t nonterminal
  53. | N_push_scope : unit nonterminal
  54. | N_push_name : Value.t nonterminal
  55. | N_push_externName : Value.t nonterminal
  56. | N_prefixedTypeName : Value.t nonterminal
  57. | N_prefixedNonTypeName : Value.t nonterminal
  58. | N_pop_scope : Context.namespace nonterminal
  59. | N_parserTypeDeclaration : Value.t nonterminal
  60. | N_parserStatement : Value.t nonterminal
  61. | N_parserStateList : Value.t nonterminal
  62. | N_parserState : Value.t nonterminal
  63. | N_parserLocalDeclarationList : Value.t nonterminal
  64. | N_parserLocalDeclaration : Value.t nonterminal
  65. | N_parserDeclaration : Value.t nonterminal
  66. | N_parserConditionalStatement : Value.t nonterminal
  67. | N_parserBlockStatement : Value.t nonterminal
  68. | N_parserBlockElementStatementList : Value.t nonterminal
  69. | N_parserBlockElementStatement : Value.t nonterminal
  70. | N_parameterList : Value.t nonterminal
  71. | N_parameter : Value.t nonterminal
  72. | N_packageTypeDeclaration : Value.t nonterminal
  73. | N_p4program : Value.t nonterminal
  74. | N_objectInitializer : Value.t nonterminal
  75. | N_objectDeclarationList : Value.t nonterminal
  76. | N_objectDeclaration : Value.t nonterminal
  77. | N_nonTypeName : Value.t nonterminal
  78. | N_nonEmptyParameterList : Value.t nonterminal
  79. | N_namedType : Value.t nonterminal
  80. | N_namedExpressionList : Value.t nonterminal
  81. | N_namedExpression : Value.t nonterminal
  82. | N_nameList : Value.t nonterminal
  83. | N_name : Value.t nonterminal
  84. | N_member : Value.t nonterminal
  85. | N_matchKindDeclaration : Value.t nonterminal
  86. | N_lvalue : Value.t nonterminal
  87. | N_listType : Value.t nonterminal
  88. | N_keysetExpression : Value.t nonterminal
  89. | N_integerLiteral : Value.t nonterminal
  90. | N_int : Value.t nonterminal
  91. | N_instantiation : Value.t nonterminal
  92. | N_initializerOpt : Value.t nonterminal
  93. | N_initialValue : Value.t nonterminal
  94. | N_identifier : Value.t nonterminal
  95. | N_headerUnionTypeDeclaration : Value.t nonterminal
  96. | N_headerTypeDeclaration : Value.t nonterminal
  97. | N_go_toplevel : unit nonterminal
  98. | N_go_local : unit nonterminal
  99. | N_functionPrototype : Value.t nonterminal
  100. | N_functionDeclaration : Value.t nonterminal
  101. | N_forUpdateStatementListNonEmpty : Value.t nonterminal
  102. | N_forUpdateStatementList : Value.t nonterminal
  103. | N_forUpdateStatement : Value.t nonterminal
  104. | N_forStatement : Value.t nonterminal
  105. | N_forInitStatementListNonEmpty : Value.t nonterminal
  106. | N_forInitStatementList : Value.t nonterminal
  107. | N_forInitStatement : Value.t nonterminal
  108. | N_forCollectionExpression : Value.t nonterminal
  109. | N_externObjectDeclaration : Value.t nonterminal
  110. | N_externName : Value.t nonterminal
  111. | N_externFunctionDeclaration : Value.t nonterminal
  112. | N_externDeclaration : Value.t nonterminal
  113. | N_externConstructorOrMethodPrototypeList : Value.t nonterminal
  114. | N_externConstructorOrMethodPrototype : Value.t nonterminal
  115. | N_expressionNonBrace : Value.t nonterminal
  116. | N_expressionList : Value.t nonterminal
  117. | N_expression : Value.t nonterminal
  118. | N_exitStatement : Value.t nonterminal
  119. | N_errorDeclaration : Value.t nonterminal
  120. | N_enumTypeDeclaration : Value.t nonterminal
  121. | N_emptyStatement : Value.t nonterminal
  122. | N_direction : Value.t nonterminal
  123. | N_directApplicationStatement : Value.t nonterminal
  124. | N_derivedTypeDeclaration : Value.t nonterminal
  125. | N_declarationList : Value.t nonterminal
  126. | N_declaration : Value.t nonterminal
  127. | N_controlTypeDeclaration : Value.t nonterminal
  128. | N_controlLocalDeclarationList : Value.t nonterminal
  129. | N_controlLocalDeclaration : Value.t nonterminal
  130. | N_controlDeclaration : Value.t nonterminal
  131. | N_controlBody : Value.t nonterminal
  132. | N_continueStatement : Value.t nonterminal
  133. | N_constructorParameterListOpt : Value.t nonterminal
  134. | N_constantDeclaration : Value.t nonterminal
  135. | N_constOpt : Value.t nonterminal
  136. | N_conditionalStatement : Value.t nonterminal
  137. | N_clear_parent_namespace : unit nonterminal
  138. | N_callStatement : Value.t nonterminal
  139. | N_breakStatement : Value.t nonterminal
  140. | N_blockStatement : Value.t nonterminal
  141. | N_blockElementStatementList : Value.t nonterminal
  142. | N_blockElementStatement : Value.t nonterminal
  143. | N_baseType : Value.t nonterminal
  144. | N_assignop : Value.t nonterminal
  145. | N_assignmentStatement : Value.t nonterminal
  146. | N_arrayType : Value.t nonterminal
  147. | N_argumentListNonEmpty : Value.t nonterminal
  148. | N_argumentList : Value.t nonterminal
  149. | N_argument : Value.t nonterminal
  150. | N_annotationToken : Value.t nonterminal
  151. | N_annotationListNonEmpty : Value.t nonterminal
  152. | N_annotationBody : Value.t nonterminal
  153. | N_annotation : Value.t nonterminal
  154. | N_actionDeclaration : Value.t 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