package p4spectec

  1. Overview
  2. Docs
package p4spectec
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Interface.SpecTec_SLSource

include module type of struct include Spectec.Common.Boot end
val boot_iters : Spectec.Caches.Il.iter list -> Runtime.Value.t
val boot_vars : Spectec.Caches.Il.var list -> Runtime.Value.t
val boot_typs : Spectec.Caches.Il.typ list -> Runtime.Value.t
val boot_bool_typ : Util.Source.region -> Runtime.Value.t
val boot_text_typ : Util.Source.region -> Runtime.Value.t
val boot_func_typ : Util.Source.region -> Runtime.Value.t
val boot_typfields : Spectec.Caches.Il.typfield list -> Runtime.Value.t
val boot_typcases : Spectec.Caches.Il.typcase list -> Runtime.Value.t
val boot_variant_deftyp : Util.Source.region -> Spectec.Caches.Il.typcase list -> Runtime.Value.t
val boot_value_opt : Spectec.Caches.Il.value option -> Runtime.Value.t
val boot_values : Spectec.Caches.Il.value list -> Runtime.Value.t
val boot_bool_value : Util.Source.region -> bool -> Runtime.Value.t
val boot_text_value : Util.Source.region -> string -> Runtime.Value.t
val boot_valuefields : Spectec.Caches.Il.valuefield list -> Runtime.Value.t
val boot_extern_value : Util.Source.region -> Yojson.Safe.t -> Runtime.Value.t
val boot_unop_bool : Lang.Xl.Bool.unop -> Runtime.Value.t
val boot_unop_num : Lang.Xl.Num.unop -> Runtime.Value.t
val boot_binop_bool : Lang.Xl.Bool.binop -> Runtime.Value.t
val boot_binop_num : Lang.Xl.Num.binop -> Runtime.Value.t
val boot_cmpop_bool : Lang.Xl.Bool.cmpop -> Runtime.Value.t
val boot_cmpop_num : Lang.Xl.Num.cmpop -> Runtime.Value.t
val boot_targs : Spectec.Caches.Il.targ list -> Runtime.Value.t
val boot_tparams : Spectec.Caches.Il.tparam list -> Runtime.Value.t
val boot_args : Spectec.Caches.Il.arg list -> Runtime.Value.t
val boot_bool_exp : Util.Source.region -> bool -> Runtime.Value.t
val boot_text_exp : Util.Source.region -> Spectec.Caches.Il.text -> Runtime.Value.t
val boot_exps : Spectec.Caches.Il.exp list -> Runtime.Value.t
val boot_exp_opt : Spectec.Caches.Il.exp option -> Runtime.Value.t
include module type of struct include Spectec.Common.Unboot end
val error : string -> 'a
val unboot_iters : Runtime.Value.t -> Spectec.Caches.Il.iter list
val unboot_varis : Runtime.Value.t -> Spectec.Caches.Il.var list
val unboot_typs : Runtime.Value.t -> Spectec.Caches.Il.typ list
val unboot_num_typ_nat : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.typ
val unboot_num_typ_int : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.typ
val unboot_text_typ : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.typ
val unboot_tuple_typ : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.typ
val unboot_targs : Runtime.Value.t -> Spectec.Caches.Il.targ list
val unboot_tparams : Runtime.Value.t -> Spectec.Caches.Il.tparam list
val unboot_plain_deftyp : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.deftyp
val unboot_typfields : Runtime.Value.t -> Spectec.Caches.Il.typfield list
val unboot_struct_deftyp : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.deftyp
val unboot_typcases : Runtime.Value.t -> Spectec.Caches.Il.typcase list
val unboot_variant_deftyp : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.deftyp
val unboot_values : Runtime.Value.t -> Lang.Il.value list
val unboot_num_value_nat : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.value
val unboot_num_value_int : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.value
val unboot_text_value : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.value
val unboot_valuefields : Runtime.Value.t -> Lang.Il.valuefield list
val unboot_struct_value : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.value
val unboot_variant_value : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.value
val unboot_tuple_value : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.value
val unboot_value_opt : Runtime.Value.t -> Lang.Il.value option
val unboot_extern_value : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.value
val unboot_minus_unop : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.unop
val unboot_equiv_binop : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.binop
val unboot_args : Runtime.Value.t -> Spectec.Caches.Il.arg list
val unboot_exps : Runtime.Value.t -> Spectec.Caches.Il.exp list
val unboot_exp_opt : Runtime.Value.t -> Spectec.Caches.Il.exp option
val unboot_num_exp_nat : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.exp
val unboot_num_exp_int : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.exp
val unboot_text_exp : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.exp
val unboot_upcast_exp : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.exp
val unboot_downcast_exp : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.exp
val unboot_match_exp : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.exp
val unboot_tuple_exp : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.exp
val unboot_slice_exp : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.exp
val unboot_slice_path : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.path
val unboot_cons_pattern : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.pattern
val unboot_fixed_pattern : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.pattern
val unboot_some_pattern : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.pattern
val unboot_none_pattern : Util.Source.region -> Runtime.Value.t list -> Spectec.Caches.Il.pattern
val unboot_iterexps : Runtime.Value.t -> Spectec.Caches.Il.iterexp list
include module type of struct include Spectec.Sli.Boot end
val boot_param : Lang.Sl.param -> Runtime.Value.t
val boot_params : Lang.Sl.param list -> Runtime.Value.t
val boot_iterinstr : Lang.Sl.iterinstr -> Runtime.Value.t
val boot_iterinstrs : Lang.Sl.iterinstr list -> Runtime.Value.t
val boot_iterexps : Lang.Sl.iterexp list -> Runtime.Value.t
val boot_instr : Lang.Sl.instr -> Runtime.Value.t
val boot_holdcase : Lang.Sl.holdcase -> Runtime.Value.t
val boot_guard : Lang.Sl.guard -> Runtime.Value.t
val boot_case : Lang.Sl.case -> Runtime.Value.t
val boot_cases : Lang.Sl.case list -> Runtime.Value.t
val boot_case_instr : Util.Source.region -> Lang.Sl.exp -> Lang.Sl.case list -> Runtime.Value.t
val boot_return_instr : Util.Source.region -> Lang.Sl.exp -> Runtime.Value.t
val boot_instrs : Lang.Sl.block -> Runtime.Value.t
val boot_block : Lang.Sl.block -> Runtime.Value.t
val boot_elsblock_opt : Lang.Sl.elseblock option -> Runtime.Value.t
val boot_tablerow : Lang.Sl.tablerow -> Runtime.Value.t
val boot_tablerows : Lang.Sl.tablerow list -> Runtime.Value.t
val boot_def : Lang.Sl.def -> Runtime.Value.t option
val boot_extern_typ_def : Util.Source.region -> Lang.Sl.id -> Runtime.Value.t
val boot_extern_func_def : Util.Source.region -> Lang.Sl.id -> Lang.Sl.tparam list -> Lang.Sl.param list -> Lang.Sl.typ -> Runtime.Value.t
val boot_builtin_func_def : Util.Source.region -> Lang.Sl.id -> Lang.Sl.tparam list -> Lang.Sl.param list -> Lang.Sl.typ -> Runtime.Value.t
val boot_table_func_def : Util.Source.region -> Lang.Sl.id -> Lang.Sl.param list -> Lang.Sl.typ -> Lang.Sl.tablerow list -> Runtime.Value.t
val boot_spec : Lang.Sl.spec -> Runtime.Value.t
include module type of struct include Spectec.Sli.Unboot end
val unboot_param_mtchtbl : Lang.Sl.param Runtime.Value.Get.mtchtbl ref
val unboot_holdcase_mtchtbl : Lang.Sl.holdcase Runtime.Value.Get.mtchtbl ref
val unboot_guard_mtchtbl : Lang.Sl.guard Runtime.Value.Get.mtchtbl ref
val unboot_instr_mtchtbl : Lang.Sl.instr Runtime.Value.Get.mtchtbl ref
val unboot_def_mtchtbl : Lang.Sl.def Runtime.Value.Get.mtchtbl ref
val unboot_iterinstr : Runtime.Value.t -> Lang.Sl.iterinstr
val unboot_iterinstrs : Runtime.Value.t -> Lang.Sl.iterinstr list
val unboot_param : Runtime.Value.t -> Lang.Sl.param
val unboot_exp_param : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.param
val unboot_def_param : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.param
val unboot_params : Runtime.Value.t -> Lang.Sl.param list
val unboot_instr : Runtime.Value.t -> Lang.Sl.instr
val unboot_if_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_holdcase : Runtime.Value.t -> Lang.Sl.holdcase
val unboot_both_holdcase : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.holdcase
val unboot_hold_holdcase : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.holdcase
val unboot_nothold_holdcase : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.holdcase
val unboot_hold_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_guard : Runtime.Value.t -> Lang.Sl.guard
val unboot_bool_guard : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.guard
val unboot_cmp_guard : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.guard
val unboot_sub_guard : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.guard
val unboot_match_guard : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.guard
val unboot_mem_guard : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.guard
val unboot_case : Runtime.Value.t -> Lang.Sl.case
val unboot_cases : Runtime.Value.t -> Lang.Sl.case list
val unboot_case_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_group_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_let_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_rule_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_result_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_return_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_debug_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_instrs : Runtime.Value.t -> Lang.Sl.block
val unboot_block : Runtime.Value.t -> Lang.Sl.block
val unboot_block_opt : Runtime.Value.t -> Lang.Sl.block option
val unboot_tablerow : Runtime.Value.t -> Lang.Sl.tablerow
val unboot_tablerows : Runtime.Value.t -> Lang.Sl.tablerow list
val unboot_def : Runtime.Value.t -> Lang.Sl.def
val unboot_extern_typ_def : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.def
val unboot_typ_def : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.def
val unboot_extern_rel_def : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.def
val unboot_rel_def : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.def
val unboot_extern_func_def : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.def
val unboot_builtin_func_def : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.def
val unboot_table_func_def : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.def
val unboot_func_def : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.def
val unboot_script : Runtime.Value.t -> Lang.Sl.spec
include module type of struct include Spectec.Caches end
module Il = Spectec.Caches.Il
module VCache = Spectec.Caches.VCache
module MCache = Spectec.Caches.MCache
type cache = Spectec.Caches.cache = {
  1. mutable enabled : bool;
  2. boot_mixop : Il.value MCache.t;
  3. boot_value : Il.value VCache.t;
  4. boot_value_pingpong : Il.value VCache.t;
  5. unboot_mixop : Il.mixop VCache.t;
  6. unboot_typ : Il.typ VCache.t;
  7. unboot_value : Il.value VCache.t;
  8. unboot_value_pingpong : Il.value VCache.t;
}
val find_boot_mixop_cache : (Il.mixop -> Il.value option) ref
val add_boot_mixop_cache : (Il.mixop -> Il.value -> unit) ref
val find_boot_value_cache : (Il.value -> Il.value option) ref
val add_boot_value_cache : (Il.value -> Il.value -> unit) ref
val find_boot_value_pingpong_cache : (Il.value -> Il.value option) ref
val add_boot_value_pingpong_cache : (Il.value -> Il.value -> unit) ref
val find_unboot_mixop_cache : (Il.value -> Il.mixop option) ref
val add_unboot_mixop_cache : (Il.value -> Il.mixop -> unit) ref
val find_unboot_typ_cache : (Il.value -> Il.typ option) ref
val add_unboot_typ_cache : (Il.value -> Il.typ -> unit) ref
val find_unboot_value_cache : (Il.value -> Il.value option) ref
val add_unboot_value_cache : (Il.value -> Il.value -> unit) ref
val find_unboot_value_pingpong_cache : (Il.value -> Il.value option) ref
val add_unboot_value_pingpong_cache : (Il.value -> Il.value -> unit) ref
val make_cache : unit -> cache
val cache_enable : cache -> unit
val cache_disable_reset : cache -> unit
val cache_clear : cache -> unit
val stack : cache option list ref
val curr : cache option ref
val install_none : unit -> unit
val install_some : cache -> unit
val install : cache option -> unit
val push_cache : cache -> unit
val pop_cache : unit -> unit
Sourceval parse_program : string list -> string list -> Run.parse_result
Sourceval parse_string : string -> string -> Run.parse_result
Sourceval unparse_program : Value.t -> string
module Builtin_SpecTec : sig ... end
Sourceval call_builtin : (Lang.Il.value -> unit) -> Lang.Il.id -> Lang.Il.targ list -> Lang.Il.value list -> Lang.Il.value
Sourceval checkpoint : unit -> int
Sourceval seff : int -> int -> bool
Sourceval init : Run.spec -> unit