package p4spectec
P4-SpecTec: A mechanization toolchain for the P4 Programming Language
Install
dune-project
Dependency
Authors
Maintainers
Sources
v0.1.2.tar.gz
md5=1a3bc0a385fe1ecf403c019f49aa6de6
sha512=5d20b5821f33e2a3a5419b208606f27c01511994c2b3b1e1cdf4c077056dfd0aa81682af0720e1060ee2bfb0341918fcc4c53159820205a2bc32b725e5c1a714
doc/src/p4/extract.ml.html
Source file extract.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221(* * Helper functions for context management * * - id_of : extracts identifiers from CaseV values * - has_type_params : checks for type parameters in CaseV values *) open Lang open Il module Value = Runtime.Value open Util.Error open Util.Source module F = Format let error = error_parse (* Identifier extraction *) let id_of_name (value : value) : string = Value.Get.mtch value [ ("_ID text", fun values -> values |> Value.Get.nth 0 |> Value.Get.text); ("APPLY", fun _ -> "apply"); ("KEY", fun _ -> "key"); ("ACTIONS", fun _ -> "actions"); ("STATE", fun _ -> "state"); ("ENTRIES", fun _ -> "entries"); ("TYPE", fun _ -> "type"); ("PRIORITY", fun _ -> "priority"); ("_TID text", fun values -> values |> Value.Get.nth 0 |> Value.Get.text); ("LIST", fun _ -> "list"); ] (fun _ -> error no_region "@id_of_name: unexpected value") let id_of_function_prototype (value : value) : string = Value.Get.mtch value [ ( "typeOrVoid name typeParameterListOpt `( parameterList `)", fun values -> values |> Value.Get.nth 1 |> id_of_name ); ] (fun _ -> error no_region "@id_of_function_prototype: unexpected value") let id_of_declaration (value : value) : string = Value.Get.mtch value [ ( "annotationList CONST type name initializer ';'", fun values -> values |> Value.Get.nth 2 |> id_of_name ); ( "annotationList type `( argumentList `) name ';'", fun values -> values |> Value.Get.nth 3 |> id_of_name ); ( "annotationList type `( argumentList `) name objectInitializer ';'", fun values -> values |> Value.Get.nth 3 |> id_of_name ); ( "annotationList functionPrototype blockStatement", fun values -> values |> Value.Get.nth 1 |> id_of_function_prototype ); ( "annotationList ACTION name `( parameterList `) blockStatement", fun values -> values |> Value.Get.nth 1 |> id_of_name ); ( "annotationList EXTERN functionPrototype ';'", fun values -> values |> Value.Get.nth 1 |> id_of_function_prototype ); ( "annotationList EXTERN nonTypeName typeParameterListOpt `{ \ externConstructorOrMethodPrototypeList `}", fun values -> values |> Value.Get.nth 1 |> id_of_name ); ( "annotationList PARSER name typeParameterListOpt `( parameterList `) \ constructorParameterListOpt `{ parserLocalDeclarationList \ parserStateList `}", fun values -> values |> Value.Get.nth 1 |> id_of_name ); ( "annotationList CONTROL name typeParameterListOpt `( parameterList `) \ constructorParameterListOpt `{ controlLocalDeclarationList APPLY \ controlBody `}", fun values -> values |> Value.Get.nth 1 |> id_of_name ); ( "annotationList ENUM name `{ nameList trailingCommaOpt `}", fun values -> values |> Value.Get.nth 1 |> id_of_name ); ( "annotationList ENUM type name `{ namedExpressionList trailingCommaOpt \ `}", fun values -> values |> Value.Get.nth 2 |> id_of_name ); ( "annotationList STRUCT name typeParameterListOpt `{ typeFieldList `}", fun values -> values |> Value.Get.nth 1 |> id_of_name ); ( "annotationList HEADER name typeParameterListOpt `{ typeFieldList `}", fun values -> values |> Value.Get.nth 1 |> id_of_name ); ( "annotationList HEADER_UNION name typeParameterListOpt `{ \ typeFieldList `}", fun values -> values |> Value.Get.nth 1 |> id_of_name ); ( "annotationList TYPEDEF typedef name ';'", fun values -> values |> Value.Get.nth 2 |> id_of_name ); ( "annotationList TYPE type name ';'", fun values -> values |> Value.Get.nth 2 |> id_of_name ); ( "annotationList PARSER name typeParameterListOpt `( parameterList `) ';'", fun values -> values |> Value.Get.nth 1 |> id_of_name ); ( "annotationList CONTROL name typeParameterListOpt `( parameterList `) \ ';'", fun values -> values |> Value.Get.nth 1 |> id_of_name ); ( "annotationList PACKAGE name typeParameterListOpt `( parameterList `) \ ';'", fun values -> values |> Value.Get.nth 1 |> id_of_name ); ( "annotationList TABLE name `{ tablePropertyList `}", fun values -> values |> Value.Get.nth 1 |> id_of_name ); ] (fun _ -> error no_region "@id_of_declaration: unexpected value") let id_of_parameter (value : value) : string = Value.Get.mtch value [ ( "annotationList direction type name initializerOpt", fun values -> values |> Value.Get.nth 3 |> id_of_name ); ] (fun _ -> error no_region "@id_of_parameter: unexpected value") (* Type identifier extraction *) let rec tid_of_typeRef (value : value) : Context.tid = Value.Get.mtch value [ ("BOOL", fun _ -> Context.Empty); ("ERROR", fun _ -> Context.Empty); ("MATCH_KIND", fun _ -> Context.Empty); ("STRING", fun _ -> Context.Empty); ("INT", fun _ -> Context.Empty); ("INT `< int `>", fun _ -> Context.Empty); ("INT `< `( expression `) `>", fun _ -> Context.Empty); ("BIT", fun _ -> Context.Empty); ("BIT `< int `>", fun _ -> Context.Empty); ("BIT `< `( expression `) `>", fun _ -> Context.Empty); ("VARBIT `< int `>", fun _ -> Context.Empty); ("VARBIT `< `( expression `) `>", fun _ -> Context.Empty); ( "_TID text", fun values -> let s = values |> Value.Get.nth 0 |> Value.Get.text in Context.Local s ); ( "_TID '.' typeName", fun values -> let value = values |> Value.Get.nth 0 in match tid_of_typeRef value with | Context.Local s -> Context.Global s | _ -> error no_region "@tid_of_typeRef: unreachable" ); ( "prefixedTypeName `< typeArgumentList `>", fun values -> let prefixedTypeName = values |> Value.Get.nth 0 in tid_of_typeRef prefixedTypeName ); ("namedType `[ expression `]", fun _ -> Context.Empty); ("LIST `< typeArgument `>", fun _ -> Context.Empty); ("TUPLE `< typeArgumentList `>", fun _ -> Context.Empty); ] (fun _ -> error no_region "@tid_of_typeRef: unexpected value") let tid_of_declaration (value : value) : Context.tid = Value.Get.mtch value [ ( "annotationList CONST type name initializer ';'", fun values -> values |> Value.Get.nth 1 |> tid_of_typeRef ); ( "annotationList type `( argumentList `) name ';'", fun values -> values |> Value.Get.nth 1 |> tid_of_typeRef ); ( "annotationList type `( argumentList `) name objectInitializer ';'", fun values -> values |> Value.Get.nth 1 |> tid_of_typeRef ); ] (fun _ -> error no_region "@tid_of_declaration: unexpected value") (* Type parameter extraction *) let has_type_params (value : value) : bool = Value.Get.mtch value [ ("_EMPTY", fun _ -> false); ("`< typeParameterList `>", fun _ -> true) ] (fun _ -> error no_region "@has_type_params: unexpected value") let has_type_params_function_prototype (value : value) : bool = Value.Get.mtch value [ ( "typeOrVoid name typeParameterListOpt `( parameterList `)", fun values -> values |> Value.Get.nth 2 |> has_type_params ); ] (fun _ -> error no_region "@has_type_params_function_prototype: unexpected value") let has_type_params_declaration (value : value) : bool = Value.Get.mtch value [ ("annotationList CONST type name initializer ';'", fun _ -> false); ("annotationList type `( argumentList `) name ';'", fun _ -> false); ( "annotationList type `( argumentList `) name objectInitializer ';'", fun _ -> false ); ( "annotationList functionPrototype blockStatement", fun values -> values |> Value.Get.nth 1 |> has_type_params_function_prototype ); ( "annotationList ACTION name `( parameterList `) blockStatement", fun _ -> false ); ( "annotationList EXTERN functionPrototype ';'", fun values -> values |> Value.Get.nth 1 |> has_type_params_function_prototype ); ( "annotationList EXTERN nonTypeName typeParameterListOpt `{ \ externConstructorOrMethodPrototypeList `}", fun values -> values |> Value.Get.nth 2 |> has_type_params ); ( "annotationList PARSER name typeParameterListOpt `( parameterList `) \ constructorParameterListOpt `{ parserLocalDeclarationList \ parserStateList `}", fun values -> values |> Value.Get.nth 2 |> has_type_params ); ( "annotationList CONTROL name typeParameterListOpt `( parameterList `) \ constructorParameterListOpt `{ controlLocalDeclarationList APPLY \ controlBody `}", fun values -> values |> Value.Get.nth 2 |> has_type_params ); ( "annotationList ENUM name `{ nameList trailingCommaOpt `}", fun _ -> false ); ( "annotationList ENUM type name `{ namedExpressionList trailingCommaOpt \ `}", fun _ -> false ); ( "annotationList STRUCT name typeParameterListOpt `{ typeFieldList `}", fun values -> values |> Value.Get.nth 2 |> has_type_params ); ( "annotationList HEADER name typeParameterListOpt `{ typeFieldList `}", fun values -> values |> Value.Get.nth 2 |> has_type_params ); ( "annotationList HEADER_UNION name typeParameterListOpt `{ \ typeFieldList `}", fun values -> values |> Value.Get.nth 2 |> has_type_params ); ("annotationList TYPEDEF typedef name ';'", fun _ -> false); ("annotationList TYPE type name ';'", fun _ -> false); ( "annotationList PARSER name typeParameterListOpt `( parameterList `) ';'", fun values -> values |> Value.Get.nth 2 |> has_type_params ); ( "annotationList CONTROL name typeParameterListOpt `( parameterList `) \ ';'", fun values -> values |> Value.Get.nth 2 |> has_type_params ); ( "annotationList PACKAGE name typeParameterListOpt `( parameterList `) \ ';'", fun values -> values |> Value.Get.nth 2 |> has_type_params ); ("annotationList TABLE name `{ tablePropertyList `}", fun _ -> false); ] (fun _ -> error no_region "@has_type_params_declaration: unexpected value")