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/Sli/Boot/index.html
Module Sli.Boot
val boot_param : Lang.Sl.param -> Runtime.Value.tval boot_params : Lang.Sl.param list -> Runtime.Value.tval boot_iterinstr : Lang.Sl.iterinstr -> Runtime.Value.tval boot_iterinstrs : Lang.Sl.iterinstr list -> Runtime.Value.tval boot_iterexps : Lang.Sl.iterexp list -> Runtime.Value.tval boot_instr : Lang.Sl.instr -> Runtime.Value.tval boot_if_instr :
Util.Source.region ->
Lang.Sl.exp ->
Lang.Sl.iterexp list ->
Lang.Sl.block ->
Runtime.Value.tval boot_holdcase : Lang.Sl.holdcase -> Runtime.Value.tval boot_hold_instr :
Util.Source.region ->
Lang.Sl.id ->
Lang.Sl.notexp ->
Lang.Sl.iterexp list ->
Lang.Sl.holdcase ->
Runtime.Value.tval boot_guard : Lang.Sl.guard -> Runtime.Value.tval boot_case : Lang.Sl.case -> Runtime.Value.tval boot_cases : Lang.Sl.case list -> Runtime.Value.tval boot_case_instr :
Util.Source.region ->
Lang.Sl.exp ->
Lang.Sl.case list ->
Runtime.Value.tval boot_group_instr :
Util.Source.region ->
Lang.Sl.id ->
Lang.Sl.nottyp ->
Lang.Hints.Input.t ->
Lang.Sl.exp list ->
Lang.Sl.block ->
Runtime.Value.tval boot_let_instr :
Util.Source.region ->
Lang.Sl.exp ->
Lang.Sl.exp ->
Lang.Sl.iterinstr list ->
Lang.Sl.block ->
Runtime.Value.tval boot_rule_instr :
Util.Source.region ->
Lang.Sl.id ->
Lang.Sl.notexp ->
Lang.Hints.Input.t ->
Lang.Sl.iterinstr list ->
Lang.Sl.block ->
Runtime.Value.tval boot_result_instr :
Util.Source.region ->
Lang.Sl.nottyp ->
Lang.Hints.Input.t ->
Lang.Sl.exp list ->
Runtime.Value.tval boot_return_instr : Util.Source.region -> Lang.Sl.exp -> Runtime.Value.tval boot_debug_instr :
Util.Source.region ->
Lang.Sl.exp ->
Lang.Sl.instr ->
Runtime.Value.tval boot_instrs : Lang.Sl.block -> Runtime.Value.tval boot_block : Lang.Sl.block -> Runtime.Value.tval boot_elsblock_opt : Lang.Sl.elseblock option -> Runtime.Value.tval boot_tablerow : Lang.Sl.tablerow -> Runtime.Value.tval boot_tablerows : Lang.Sl.tablerow list -> Runtime.Value.tval boot_def : Lang.Sl.def -> Runtime.Value.t optionval boot_extern_typ_def : Util.Source.region -> Lang.Sl.id -> Runtime.Value.tval boot_typ_def :
Util.Source.region ->
Lang.Sl.id ->
Lang.Sl.tparam list ->
Lang.Sl.deftyp ->
Runtime.Value.tval boot_extern_rel_def :
Util.Source.region ->
Lang.Sl.id ->
Lang.Sl.nottyp ->
Lang.Hints.Input.t ->
Lang.Sl.exp list ->
Runtime.Value.tval boot_rel_def :
Util.Source.region ->
Lang.Sl.id ->
Lang.Sl.nottyp ->
Lang.Hints.Input.t ->
Lang.Sl.exp list ->
Lang.Sl.block ->
Lang.Sl.elseblock option ->
Runtime.Value.tval boot_extern_func_def :
Util.Source.region ->
Lang.Sl.id ->
Lang.Sl.tparam list ->
Lang.Sl.param list ->
Lang.Sl.typ ->
Runtime.Value.tval boot_builtin_func_def :
Util.Source.region ->
Lang.Sl.id ->
Lang.Sl.tparam list ->
Lang.Sl.param list ->
Lang.Sl.typ ->
Runtime.Value.tval boot_table_func_def :
Util.Source.region ->
Lang.Sl.id ->
Lang.Sl.param list ->
Lang.Sl.typ ->
Lang.Sl.tablerow list ->
Runtime.Value.tval boot_func_def :
Util.Source.region ->
Lang.Sl.id ->
Lang.Sl.tparam list ->
Lang.Sl.param list ->
Lang.Sl.typ ->
Lang.Sl.block ->
Lang.Sl.elseblock option ->
Runtime.Value.tval boot_spec : Lang.Sl.spec -> Runtime.Value.t