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/spectec/Spectec/Ali/Boot/index.html
Module Ali.Boot
val boot_param : Lang.Il.param -> Runtime.Value.tval boot_params : Lang.Il.param list -> Runtime.Value.tval boot_iterprem : Lang.Il.iterprem -> Runtime.Value.tval boot_prem : Lang.Il.prem -> Runtime.Value.tval boot_rel_prem :
Util.Source.region ->
Lang.Il.id ->
Lang.Il.notexp ->
Lang.Hints.Input.t ->
Runtime.Value.tval boot_if_prem : Util.Source.region -> Lang.Il.exp -> Runtime.Value.tval boot_if_hold_prem :
Util.Source.region ->
Lang.Il.id ->
Lang.Il.notexp ->
Runtime.Value.tval boot_if_nothold_prem :
Util.Source.region ->
Lang.Il.id ->
Lang.Il.notexp ->
Runtime.Value.tval boot_let_prem :
Util.Source.region ->
Lang.Il.exp ->
Lang.Il.exp ->
Runtime.Value.tval boot_iter_prem :
Util.Source.region ->
Lang.Il.prem ->
Lang.Il.iterprem ->
Runtime.Value.tval boot_debug_prem : Util.Source.region -> Lang.Il.exp -> Runtime.Value.tval boot_prems : Lang.Il.prem list -> Runtime.Value.tval boot_rulmatch : Lang.Al.rulematch -> Runtime.Value.tval boot_rulpath : Lang.Al.rulepath -> Runtime.Value.tval boot_rulpaths : Lang.Al.rulepath list -> Runtime.Value.tval boot_rulgroup : Lang.Al.rulegroup -> Runtime.Value.tval boot_rulgroups : Lang.Al.rulegroup list -> Runtime.Value.tval boot_elsgroup : Lang.Al.elsegroup -> Runtime.Value.tval boot_elsgroup_opt : Lang.Al.elsegroup option -> Runtime.Value.tval boot_clause : Lang.Il.clause -> Runtime.Value.tval boot_clauses : Lang.Il.clause list -> Runtime.Value.tval boot_elsclause : Lang.Il.elseclause -> Runtime.Value.tval boot_elsclause_opt : Lang.Il.elseclause option -> Runtime.Value.tval boot_tablerow : Lang.Al.tablerow -> Runtime.Value.tval boot_tablerows : Lang.Al.tablerow list -> Runtime.Value.tval boot_def : Lang.Al.def -> Runtime.Value.t optionval boot_extern_typ_def : Util.Source.region -> Lang.Il.id -> Runtime.Value.tval boot_typ_def :
Util.Source.region ->
Lang.Il.id ->
Lang.Il.tparam list ->
Lang.Il.deftyp ->
Runtime.Value.tval boot_extern_rel_def :
Util.Source.region ->
Lang.Il.id ->
Lang.Il.nottyp ->
Lang.Hints.Input.t ->
Runtime.Value.tval boot_rel_def :
Util.Source.region ->
Lang.Il.id ->
Lang.Il.nottyp ->
Lang.Hints.Input.t ->
Lang.Al.rulegroup list ->
Lang.Al.elsegroup option ->
Runtime.Value.tval boot_extern_func_def :
Util.Source.region ->
Lang.Il.id ->
Lang.Il.tparam list ->
Lang.Il.param list ->
Lang.Il.typ ->
Runtime.Value.tval boot_builtin_func_def :
Util.Source.region ->
Lang.Il.id ->
Lang.Il.tparam list ->
Lang.Il.param list ->
Lang.Il.typ ->
Runtime.Value.tval boot_table_func_def :
Util.Source.region ->
Lang.Il.id ->
Lang.Il.param list ->
Lang.Il.typ ->
Lang.Al.tablerow list ->
Runtime.Value.tval boot_func_def :
Util.Source.region ->
Lang.Il.id ->
Lang.Il.tparam list ->
Lang.Il.param list ->
Lang.Il.typ ->
Lang.Il.clause list ->
Lang.Il.elseclause option ->
Runtime.Value.tval boot_spec : Lang.Al.spec -> Runtime.Value.t