package p4spectec
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
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/p4spectec.backend_boot/config.ml.html
Source file config.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 66module Run = Runtime.Dynamic_Runner.Signature (* Kind of interface, currently offering three: P4, SL, and AL *) type interface = P4_interface | AL_interface | SL_interface (* Layers *) type layer = { specdir : string; rel : string } type target = { includes : string list; path : string } (* Tower is an alternation of a layer and an interface *) type level = { layer : layer; interface : interface } type tower = { mode : Run.mode; level_boot : level; levels_interm : level list; level_target : level; target : target; } (* Load a tower from a JSON file. JSON schema: { "mode": "al"|"sl", "levels": [ { "specdir": "...", "rel": "...", "interface": "p4"|"al"|"sl" }, ... ] } First level = boot, last = target, middle = intermediates. `target` is supplied separately (from CLI -p/-i flags). *) let tower_of_file path target = let json = Yojson.Basic.from_file path in let open Yojson.Basic.Util in let mode = match json |> member "mode" |> to_string with | "al" -> Run.AL_mode | "sl" -> Run.SL_mode | s -> failwith (Format.sprintf "tower: unknown mode %S" s) in let level_of_json json = let interface = match json |> member "interface" |> to_string with | "p4" -> P4_interface | "al" -> AL_interface | "sl" -> SL_interface | s -> failwith (Format.sprintf "tower: unknown interface %S" s) in { layer = { specdir = json |> member "specdir" |> to_string; rel = json |> member "rel" |> to_string; }; interface; } in let levels = json |> member "levels" |> to_list |> List.map level_of_json in match levels with | [] | [ _ ] -> failwith "tower: at least two levels required (boot + target)" | _ -> let level_boot = List.hd levels in let levels_interm = levels |> List.tl |> List.rev |> List.tl |> List.rev in let level_target = levels |> List.rev |> List.hd in { mode; level_boot; levels_interm; level_target; target }
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>