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_sim/state.ml.html
Source file state.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 73module Value = Runtime.Value module IO = Runtime.Sim.Io (* The state consists of: - current evaluation context - current arch - list of transmissions to perform *) type s = Value.t * Value.t * IO.tx list (* State monad with failure *) type 'a state = s -> 'a option * s (* Get, Put, Modify: state manipulation functions *) let get : s state = fun s -> (Some s, s) let put (x : s) : unit state = fun _ -> (Some (), x) let modify (f : s -> s) : unit state = fun s -> (Some (), f s) (* Return: wrap a value into the monad *) let return (a : 'a) : 'a state = fun s -> (Some a, s) (* Bind: sequence two computations in the monad *) let bind (m : 'a state) (f : 'a -> 'b state) s = match m s with Some a, s -> f a s | None, s -> (None, s) let ( >> ) (ma : 'a state) (mb : 'b state) = bind ma (fun _ -> mb) let ( let* ) = bind (* Map: apply a function to the result of a computation in the monad *) let map (m : 'a state) (f : 'a -> 'b) = bind m (fun a -> return (f a)) let ( let+ ) = map (* Sequence: run each state action from left to right and return accumulated result *) let sequence (ms : 'a state list) : 'a list state = let rec seq acc = function | [] -> return (List.rev acc) | m :: ms -> let* x = m in seq (x :: acc) ms in seq [] ms (* Combinators *) (* If computation succeeds, run `some`. Otherwise, run `none` *) let on_result (m : 'a state) ~(some : 'a -> 'b state) ~(none : unit -> 'b state) : 'b state = fun s -> let result, s' = m s in match result with Some x -> some x s' | None -> none () s' (* Apply: apply a function to the current context and arch, updating them *) let apply (f : Value.t -> Value.t -> Value.t * Value.t * 'a) : 'a state = let* value_ctx, value_arch, txs = get in let value_ctx, value_arch, result = f value_ctx value_arch in let+ () = put (value_ctx, value_arch, txs) in result (* Guard: fail the computation if the condition is false *) let guard (cond : bool) : unit state = if cond then return () else fun s -> (None, s) let empty : 'a state = fun s -> (None, s) let run (m : 'a state) (s : s) : 'a option * s = m s
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>