package p4spectec

  1. Overview
  2. Docs
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/p4spectec.lang/Lang/Il/index.html

Module Lang.Il

type num = Xl.Num.t
val num_to_yojson : num -> Yojson.Safe.t
type text = string
val text_to_yojson : text -> Yojson.Safe.t
and id' = string
val id_to_yojson : id -> Yojson.Safe.t
val id'_to_yojson : id' -> Yojson.Safe.t
and atom' = Domain.Atom.t
val atom_to_yojson : atom -> Yojson.Safe.t
val atom'_to_yojson : atom' -> Yojson.Safe.t
type mixop = Domain.Mixfix.mixop
val mixop_to_yojson : mixop -> Yojson.Safe.t
type iter =
  1. | Opt
  2. | List
val iter_to_yojson : iter -> Yojson.Safe.t
type var = id * typ * iter list
and typ' =
  1. | BoolT
  2. | NumT of Xl.Num.typ
  3. | TextT
  4. | VarT of id * targ list
  5. | TupleT of typ list
  6. | IterT of typ * iter
  7. | FuncT of tparam list * typ list * typ
and nottyp' = typ Domain.Mixfix.t
and deftyp' =
  1. | PlainT of typ
  2. | StructT of typfield list
  3. | VariantT of typcase list
and typfield = atom * typ
and typorigin' = id * targ list
and typcase = nottyp * typorigin * hint list
and vid = int
and vnote = {
  1. vid : vid;
  2. typ : typ';
  3. vhash : int;
}
and value' =
  1. | BoolV of bool
  2. | NumV of Xl.Num.t
  3. | TextV of string
  4. | StructV of valuefield list
  5. | CaseV of valuecase
  6. | TupleV of value list
  7. | OptV of value option
  8. | ListV of value list
  9. | FuncV of id
  10. | ExternV of Yojson.Safe.t
and valuefield = atom * value
and valuecase = value Domain.Mixfix.t
and numop = [
  1. | `DecOp
  2. | `HexOp
]
and unop = [
  1. | Xl.Bool.unop
  2. | Xl.Num.unop
]
and binop = [
  1. | Xl.Bool.binop
  2. | Xl.Num.binop
]
and cmpop = [
  1. | Xl.Bool.cmpop
  2. | Xl.Num.cmpop
]
and optyp = [
  1. | Xl.Bool.typ
  2. | Xl.Num.typ
]
and exp' =
  1. | BoolE of bool
  2. | NumE of num
  3. | TextE of text
  4. | VarE of id
  5. | UnE of unop * optyp * exp
  6. | BinE of binop * optyp * exp * exp
  7. | CmpE of cmpop * optyp * exp * exp
  8. | UpCastE of typ * exp
  9. | DownCastE of typ * exp
  10. | SubE of exp * typ
  11. | MatchE of exp * pattern
  12. | TupleE of exp list
  13. | CaseE of notexp
  14. | StrE of (atom * exp) list
  15. | OptE of exp option
  16. | ListE of exp list
  17. | ConsE of exp * exp
  18. | CatE of exp * exp
  19. | MemE of exp * exp
  20. | LenE of exp
  21. | DotE of exp * atom
  22. | IdxE of exp * exp
  23. | SliceE of exp * exp * exp
  24. | UpdE of exp * path * exp
  25. | CallE of id * targ list * arg list
  26. | IterE of exp * iterexp
and notexp = exp Domain.Mixfix.t
and iterexp = iter * var list
and pattern =
  1. | CaseP of mixop
  2. | ListP of [ `Cons | `Fixed of int | `Nil ]
  3. | OptP of [ `Some | `None ]
and path' =
  1. | RootP
  2. | IdxP of path * exp
  3. | SliceP of path * exp * exp
  4. | DotP of path * atom
and param' =
  1. | ExpP of typ
  2. | DefP of id * tparam list * param list * typ
and tparam' = id'
and arg' =
  1. | ExpA of exp
  2. | DefA of id
and targ' = typ'
and prem' =
  1. | RulePr of id * notexp * Hints.Input.t
  2. | IfPr of exp
  3. | IfHoldPr of id * notexp
  4. | IfNotHoldPr of id * notexp
  5. | LetPr of exp * exp
  6. | IterPr of prem * iterprem
  7. | DebugPr of exp
and iterprem = iter * var list * var list
and rule' = id * notexp * prem list
and rulegroup' = id * rule list
and elsegroup' = id * rule
and clause' = arg list * exp * prem list
and elseclause = clause
and elseclause' = clause'
and tablerow' = arg list * exp
and hint = El.hint
val var_to_yojson : var -> Yojson.Safe.t
val typ_to_yojson : typ -> Yojson.Safe.t
val typ'_to_yojson : typ' -> Yojson.Safe.t
val nottyp_to_yojson : nottyp -> Yojson.Safe.t
val nottyp'_to_yojson : nottyp' -> Yojson.Safe.t
val deftyp_to_yojson : deftyp -> Yojson.Safe.t
val deftyp'_to_yojson : deftyp' -> Yojson.Safe.t
val typfield_to_yojson : typfield -> Yojson.Safe.t
val typorigin_to_yojson : typorigin -> Yojson.Safe.t
val typorigin'_to_yojson : typorigin' -> Yojson.Safe.t
val typcase_to_yojson : typcase -> Yojson.Safe.t
val vid_to_yojson : vid -> Yojson.Safe.t
val vnote_to_yojson : vnote -> Yojson.Safe.t
val value_to_yojson : value -> Yojson.Safe.t
val value'_to_yojson : value' -> Yojson.Safe.t
val valuefield_to_yojson : valuefield -> Yojson.Safe.t
val valuecase_to_yojson : valuecase -> Yojson.Safe.t
val numop_to_yojson : numop -> Yojson.Safe.t
val unop_to_yojson : unop -> Yojson.Safe.t
val binop_to_yojson : binop -> Yojson.Safe.t
val cmpop_to_yojson : cmpop -> Yojson.Safe.t
val optyp_to_yojson : optyp -> Yojson.Safe.t
val exp_to_yojson : exp -> Yojson.Safe.t
val exp'_to_yojson : exp' -> Yojson.Safe.t
val notexp_to_yojson : notexp -> Yojson.Safe.t
val iterexp_to_yojson : iterexp -> Yojson.Safe.t
val pattern_to_yojson : pattern -> Yojson.Safe.t
val path_to_yojson : path -> Yojson.Safe.t
val path'_to_yojson : path' -> Yojson.Safe.t
val param_to_yojson : param -> Yojson.Safe.t
val param'_to_yojson : param' -> Yojson.Safe.t
val tparam_to_yojson : tparam -> Yojson.Safe.t
val tparam'_to_yojson : tparam' -> Yojson.Safe.t
val arg_to_yojson : arg -> Yojson.Safe.t
val arg'_to_yojson : arg' -> Yojson.Safe.t
val targ_to_yojson : targ -> Yojson.Safe.t
val targ'_to_yojson : targ' -> Yojson.Safe.t
val prem_to_yojson : prem -> Yojson.Safe.t
val prem'_to_yojson : prem' -> Yojson.Safe.t
val iterprem_to_yojson : iterprem -> Yojson.Safe.t
val rule_to_yojson : rule -> Yojson.Safe.t
val rule'_to_yojson : rule' -> Yojson.Safe.t
val rulegroup_to_yojson : rulegroup -> Yojson.Safe.t
val rulegroup'_to_yojson : rulegroup' -> Yojson.Safe.t
val elsegroup_to_yojson : elsegroup -> Yojson.Safe.t
val elsegroup'_to_yojson : elsegroup' -> Yojson.Safe.t
val clause_to_yojson : clause -> Yojson.Safe.t
val clause'_to_yojson : clause' -> Yojson.Safe.t
val elseclause_to_yojson : elseclause -> Yojson.Safe.t
val elseclause'_to_yojson : elseclause' -> Yojson.Safe.t
val tablerow_to_yojson : tablerow -> Yojson.Safe.t
val tablerow'_to_yojson : tablerow' -> Yojson.Safe.t
val hint_to_yojson : hint -> Yojson.Safe.t
and def' =
  1. | ExternTypD of id * hint list
  2. | TypD of id * tparam list * deftyp * hint list
  3. | VarD of id * typ * hint list
  4. | ExternRelD of id * nottyp * Hints.Input.t * hint list
  5. | RelD of id * nottyp * Hints.Input.t * rulegroup list * elsegroup option * hint list
  6. | ExternDecD of id * tparam list * param list * typ * hint list
  7. | BuiltinDecD of id * tparam list * param list * typ * hint list
  8. | TableDecD of id * param list * typ * tablerow list * hint list
  9. | FuncDecD of id * tparam list * param list * typ * clause list * elseclause option * hint list
type spec = def list
module Eq : sig ... end
module Free : sig ... end
module Fresh : sig ... end
module Var : sig ... end
module Print : sig ... end