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

val opt_sequential : bool Stdlib.ref

val opt_mwords : bool Stdlib.ref

type context = {

early_ret : bool;
bound_nexps : Ast_util.NexpSet.t;
top_env : Type_check.Env.t;

}

val empty_ctxt : context

val print_to_from_interp_value : bool Stdlib.ref

val langlebar : PPrint.document

val ranglebar : PPrint.document

val anglebars : PPrint.document -> PPrint.document

val doc_var : Ast.kid -> PPrint.document

val is_number_char : char -> bool

val fix_id : bool -> string -> string

val doc_id_lem : Ast.id -> PPrint.document

val doc_id_lem_type : Ast.id -> PPrint.document

val doc_id_lem_ctor : Ast.id -> PPrint.document

val deinfix : Ast.id -> Ast.id

val doc_var_lem : Ast.kid -> PPrint.document

val doc_docstring_lem : (Parse_ast.l * 'a) -> PPrint.document

val simple_annot : 
  Parse_ast.l ->
  'a ->
  Parse_ast.l * (Type_check.Env.t * 'a * Ast.effect) option

val simple_num : 
  Parse_ast.l ->
  Nat_big_num.num ->
  (Type_check.Env.t * Ast.typ * Ast.effect) option Ast.exp

val effectful_set : 'a list -> bool

val effectful : Ast.effect -> bool

val is_regtyp : Ast.typ -> 'a -> bool

val lemnum : 
  (Pretty_print_common.Big_int.num -> string) ->
  Pretty_print_common.Big_int.num ->
  string

val doc_nexp_lem : Ast.nexp -> PPrint.document

val orig_nexp : Ast.nexp -> Ast.nexp

val lem_nexps_of_typ : Ast.typ -> Ast_util.NexpSet.t

val lem_nexps_of_typ_arg : Ast.typ_arg -> Ast_util.NexpSet.t

val lem_tyvars_of_typ : Ast.typ -> Ast_util.KidSet.t

val doc_typ_lem : Type_check.Env.t -> Ast.typ -> PPrint.document

val doc_atomic_typ_lem : bool -> Ast.typ -> PPrint.document

val contains_t_pp_var : 'a -> Ast.typ -> bool

val replace_typ_size : context -> Type_check.Env.t -> Ast.typ -> Ast.typ option

val replace_typ_arg_size : 
  context ->
  Type_check.Env.t ->
  Ast.typ_arg ->
  Ast.typ_arg option

val make_printable_type : 
  context ->
  Type_check.Env.t ->
  Ast.typ ->
  Ast.typ option

val doc_tannot_lem : 
  context ->
  Type_check.Env.t ->
  bool ->
  Ast.typ ->
  PPrint.document

val min_int32 : Pretty_print_common.Big_int.num

val max_int32 : Pretty_print_common.Big_int.num

val doc_lit_lem : Ast.lit -> PPrint.document

val kid_nexps_of_typquant : Ast.typquant -> Ast.nexp list

val doc_typquant_items_lem : Ast.nexp list -> PPrint.document

val typeclass_nexps : Ast.typ -> Ast_util.NexpSet.t

val doc_typclasses_lem : Ast.typ -> PPrint.document * Ast_util.NexpSet.t

val doc_typschm_lem : 
  Type_check.Env.t ->
  bool ->
  Ast.typschm ->
  PPrint.document

val is_ctor : Type_check.Env.t -> Ast.id -> bool

val doc_pat_lem : 
  context ->
  bool ->
  Type_check.tannot Ast.pat ->
  PPrint.document

val typ_needs_printed : Ast.typ -> bool

val typ_needs_printed_arg : Ast.typ_arg -> bool

val contains_early_return : 'a Ast.exp -> bool

type is_bitvector_cast =

| BVC_yes
| BVC_allowed
| BVC_not

val is_bitvector_cast_out : 'a Ast.exp -> bool

val replace_env_for_cast_out : 
  Type_check.Env.t ->
  Type_check.tannot Ast.pat ->
  Type_check.tannot Ast.pat

val find_e_ids : 'a Ast.exp -> Ast_util.IdSet.t

val typ_id_of : Ast.typ -> Ast.id

val prefix_recordtype : bool

val report : Parse_ast.l -> (string * int * int * int) -> string -> exn

val doc_exp_lem : 
  context ->
  bool ->
  Type_check.tannot Ast.exp ->
  PPrint.document

val doc_let_lem : context -> Type_check.tannot Ast.letbind -> PPrint.document

val doc_type_union_lem : Type_check.Env.t -> Ast.type_union -> PPrint.document

val doc_typquant_sorts : PPrint.document -> Ast.typquant -> PPrint.document

val doc_sia_id : Ast.id -> PPrint.document

val doc_typdef_lem : Type_check.Env.t -> 'a Ast.type_def -> PPrint.document

val args_of_typs : 
  Ast.l ->
  Type_check.Env.t ->
  Ast.typ list ->
  Type_check.tannot Ast.pat list * Type_check.tannot Ast.exp list

val untuple_args_pat : 
  Type_check.tannot Ast.pat ->
  Ast.typ list ->
  Type_check.tannot Ast.pat list
  * (Type_check.tannot Ast.exp ->
  Type_check.tannot Ast.exp)

val doc_tannot_opt_lem : Type_check.Env.t -> Ast.tannot_opt -> PPrint.document

val doc_fun_body_lem : context -> Type_check.tannot Ast.exp -> PPrint.document

val doc_funcl_lem : 
  Type_check.Env.t ->
  Type_check.tannot Ast.funcl ->
  PPrint.document

val get_id : 'a Ast.funcl list -> Ast.id

module StringSet : sig ... end

val doc_fundef_rhs_lem : 
  Type_check.Env.t ->
  Type_check.tannot Ast.fundef ->
  PPrint.document

val doc_mutrec_lem : 
  Type_check.Env.t ->
  Type_check.tannot Ast.fundef list ->
  PPrint.document

val doc_fundef_lem : 
  Type_check.Env.t ->
  Type_check.tannot Ast.fundef ->
  PPrint.document

val doc_dec_lem : Type_check.tannot Ast.dec_spec -> PPrint.document

val doc_spec_lem : Type_check.Env.t -> 'a Ast.val_spec -> PPrint.document

val is_field_accessor : 
  (string * ('a * 'b * ('c * Ast.id) list)) list ->
  'd Ast.fundef ->
  bool

val int_of_field_index : string -> Ast.id -> Ast.nexp -> Ast_util.Big_int.num

val doc_regtype_fields : 
  (string * (Ast.nexp * Ast.nexp * (Ast.index_range * Ast.id) list)) ->
  PPrint.document

val doc_def_lem : 
  Type_check.Env.t ->
  Type_check.tannot Ast.def ->
  PPrint.document

val find_exc_typ : 'a Ast.def list -> string

val pp_defs_lem : 
  (PPrint.ToChannel.channel * string list) ->
  (PPrint.ToChannel.channel * string list) ->
  Type_check.Env.t ->
  Type_check.tannot Ast.defs ->
  string ->
  unit