package sail

  1. Overview
  2. Docs
package sail
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Big_int = Nat_big_num
val opt_trace_ocaml : bool ref
val opt_ocaml_nobuild : bool ref
val opt_ocaml_coverage : bool ref
val opt_ocaml_build_dir : string ref
type ctx = {
  1. register_inits : Type_check.tannot Ast.exp list;
  2. externs : Ast.id Ast_util.Bindings.t;
  3. val_specs : Ast.typ Ast_util.Bindings.t;
}
val empty_ctx : ctx
val gensym_counter : int ref
val gensym : unit -> PPrint.document
val zencode_upper : ctx -> Ast_util.Bindings.key -> PPrint.document
val zencode_kid : Ast.kid -> PPrint.document
val ocaml_string_of : Ast.id -> PPrint.document
val ocaml_string_parens : PPrint.document -> PPrint.document
val ocaml_string_comma : PPrint.document
val ocaml_string_typ : Ast.typ -> PPrint.document -> PPrint.document
val ocaml_typ_id : ctx -> Ast_util.Bindings.key -> PPrint.document
val ocaml_typ : ctx -> Ast.typ -> PPrint.document
val ocaml_typ_arg : ctx -> Ast.typ_arg -> PPrint.document
val ocaml_typquant : Ast.typquant -> PPrint.document
val string_lit : string -> PPrint.document
val ocaml_lit : Ast.lit -> PPrint.document
val begin_end : PPrint.document -> PPrint.document
val is_passed_by_name : Ast.typ -> bool
val ocaml_pexps : ctx -> Type_check.tannot Ast.pexp list -> PPrint.document
val ocaml_block : ctx -> Type_check.tannot Ast.exp list -> PPrint.document
val ocaml_atomic_exp : ctx -> Type_check.tannot Ast.exp -> PPrint.document
val ocaml_atomic_lexp : ctx -> Type_check.tannot Ast.lexp -> PPrint.document
val get_initialize_registers : 'a Ast.def list -> 'a Ast.exp list
val initial_value_for : Ast.id -> 'a Ast.exp list -> 'a Ast.exp
val first_function : bool ref
val function_header : unit -> PPrint.document
val funcls_id : 'a Ast.funcl list -> Ast.id
val ocaml_funcl_match : ctx -> Type_check.tannot Ast.funcl -> PPrint.document
val ocaml_funcl_matches : ctx -> Type_check.tannot Ast.funcl list -> PPrint.document
val ocaml_funcls : ctx -> Type_check.tannot Ast.funcl list -> PPrint.document
val ocaml_fields : ctx -> (Ast.typ * Ast_util.Bindings.key) list -> PPrint.document
val ocaml_cases : ctx -> Ast.type_union list -> PPrint.document
val ocaml_exceptions : ctx -> Ast.type_union list -> PPrint.document
val ocaml_enum : ctx -> Ast_util.Bindings.key list -> PPrint.document
val ocaml_def_end : PPrint.document
val ocaml_string_of_enum : ctx -> Ast.id -> Ast_util.Bindings.key list -> PPrint.document
val ocaml_string_of_struct : ctx -> Ast_util.Bindings.key -> Ast.typquant -> (Ast.typ * Ast_util.Bindings.key) list -> PPrint.document
val ocaml_string_of_abbrev : ctx -> Ast_util.Bindings.key -> 'a -> Ast.typ -> PPrint.document
val ocaml_string_of_variant : 'a -> Ast.id -> 'b -> 'c -> PPrint.document
val ocaml_typedef : ctx -> 'a Ast.type_def -> PPrint.document
val get_externs : 'a Ast.def list -> Ast.id Ast_util.Bindings.t
val val_spec_typs : 'a Ast.def list -> Ast.typ Ast_util.Bindings.t
val orig_types_for_ocaml_generator : 'a Ast.def list -> 'a Ast.type_def list
val ocaml_pp_generators : ctx -> 'a -> 'b Ast.type_def list -> Ast_util.IdSet.elt list -> PPrint.document
val ocaml_ast : Type_check.tannot Ast_defs.ast -> ('a Ast.type_def list * string list) option -> PPrint.document
val ocaml_main : string -> string -> string
val ocaml_pp_ast : PPrint.ToChannel.channel -> Type_check.tannot Ast_defs.ast -> ('a Ast.type_def list * string list) option -> unit
val system_checked : string -> unit
val ocaml_compile : string -> Type_check.tannot Ast_defs.ast -> ('a Ast.type_def list * string list) option -> unit