package sail

You can search for identifiers within the package.

in-package search v0.2.0

package sail

sail
- Anf
- Ast
- Ast_util
  - BE
  - BESet
  - Bindings
  - Id
  - IdSet
  - KBindings
  - KOpt
  - KOptMap
  - KOptSet
  - Kid
  - KidSet
  - Kind
  - NC
  - NCMap
  - Nexp
  - NexpMap
  - NexpSet
  - Typ
  - TypMap
- Bitfield
- C_backend
- Cgen_backend
- Constant_fold
  - StringMap
- Constant_propagation
- Constant_propagation_mutrec
- Constraint
- Elf_loader
- Error_format
- Graph
  - Make
    
    Ord
  - OrderedType
  - S
- Initial_check
- Interactive
- Interpreter
- Jib
- Jib_compile
  - Config
  - Make
    
    C
- Jib_interactive
- Jib_ir
  - Flat_ir_config
  - Flat_ir_formatter
  - Ir_formatter
    
    Config
    
    Make
    
    C
  - StringMap
- Jib_optimize
- Jib_smt
  - EventMap
  - IntSet
  - Make_optimizer
    
    S
  - Sequence
- Jib_ssa
  - IntSet
- Jib_util
  - CT
  - CTMap
  - CTSet
  - Name
  - NameCT
  - NameCTMap
  - NameCTSet
  - NameMap
  - NameSet
  - UBindings
  - UId
- Latex
  - StringSet
- Lexer
  - M
- Manifest
- Monomorphise
- Nl_flow
- Ocaml_backend
- Optimize
- Parse_ast
- Parser
- Parser_combinators
- Pattern_completeness
- Pretty_print
- Pretty_print_common
- Pretty_print_coq
  - StringSet
- Pretty_print_lem
  - StringSet
- Pretty_print_sail
- Process_file
- Profile
- Property
  - Event
- Reporting
- Rewriter
- Rewrites
- Sail2_values
- Sail_lib
  - BitType
  - Mem
- Scattered
- Smtlib
- Spec_analysis
- Specialize
- State
- ToFromInterp_backend
- ToFromInterp_lib_bitlist
  - Make
    
    BitT
- ToFromInterp_lib_mword
- Type_check
  - Env
- Type_error
- Util
- Value
  - StringMap

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Big_int = Nat_big_num

val opt_trace_ocaml : bool Stdlib.ref

val opt_ocaml_nobuild : bool Stdlib.ref

val opt_ocaml_coverage : bool Stdlib.ref

val opt_ocaml_build_dir : string Stdlib.ref

type ctx = {

register_inits : Type_check.tannot Ast.exp list;
externs : Ast.id Ast_util.Bindings.t;
val_specs : Ast.typ Ast_util.Bindings.t;

}

val empty_ctx : ctx

val gensym_counter : int Stdlib.ref

val gensym : unit -> PPrint.document

val zencode : ctx -> Ast_util.Bindings.key -> 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 ocaml_pat : ctx -> Type_check.tannot Ast.pat -> PPrint.document

val begin_end : PPrint.document -> PPrint.document

val is_passed_by_name : Ast.typ -> bool

val ocaml_exp : ctx -> Type_check.tannot Ast.exp -> PPrint.document

val ocaml_letbind : ctx -> Type_check.tannot Ast.letbind -> PPrint.document

val ocaml_pexps : ctx -> Type_check.tannot Ast.pexp list -> PPrint.document

val ocaml_pexp : ctx -> Type_check.tannot Ast.pexp -> PPrint.document

val ocaml_block : ctx -> Type_check.tannot Ast.exp list -> PPrint.document

val ocaml_fexp : ctx -> Type_check.tannot Ast.fexp -> PPrint.document

val ocaml_atomic_exp : ctx -> Type_check.tannot Ast.exp -> PPrint.document

val ocaml_assignment : 
  ctx ->
  Type_check.tannot Ast.lexp ->
  Type_check.tannot Ast.exp ->
  PPrint.document

val ocaml_lexp : ctx -> Type_check.tannot Ast.lexp -> 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 ocaml_dec_spec : ctx -> Type_check.tannot Ast.dec_spec -> PPrint.document

val first_function : bool Stdlib.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_fundef : ctx -> Type_check.tannot Ast.fundef -> 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.defs -> Ast.id Ast_util.Bindings.t

val nf_group : PPrint.document -> PPrint.document

val ocaml_def : ctx -> Type_check.tannot Ast.def -> PPrint.document

val val_spec_typs : 'a Ast.defs -> Ast.typ Ast_util.Bindings.t

val orig_types_for_ocaml_generator : 'a Ast.defs -> '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_defs : 
  Type_check.tannot Ast.defs ->
  ('a Ast.type_def list * string list) option ->
  PPrint.document

val ocaml_main : string -> string -> string

val ocaml_pp_defs : 
  PPrint.ToChannel.channel ->
  Type_check.tannot Ast.defs ->
  ('a Ast.type_def list * string list) option ->
  unit

val system_checked : string -> unit

val ocaml_compile : 
  string ->
  Type_check.tannot Ast.defs ->
  ('a Ast.type_def list * string list) option ->
  unit