package sail

You can search for identifiers within the package.

in-package search v0.2.0

package sail

sail
- Anf
- Ast
- Ast_defs
- Ast_util
  - BE
  - BESet
  - Bindings
  - Id
  - IdSet
  - KBindings
  - KOpt
  - KOptMap
  - KOptSet
  - Kid
  - KidSet
  - Kind
  - NC
  - NCMap
  - Nexp
  - NexpMap
  - NexpSet
  - Typ
  - TypMap
- Bitfield
- C_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
- Slice
  - Node
- Smtlib
- Spec_analysis
- Specialize
- Splice
- 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

type mut =

| Immutable
| Mutable

type !'a lvar =

| Register of Ast.effect * Ast.effect * 'a
| Enum of 'a
| Local of mut * 'a
| Unbound

val lvar_typ : 'a lvar -> 'a

val no_annot : unit Ast.annot

val gen_loc : Parse_ast.l -> Parse_ast.l

val mk_id : string -> Ast.id

val mk_kid : string -> Ast.kid

val mk_ord : Ast.order_aux -> Ast.order

val mk_nc : Ast.n_constraint_aux -> Ast.n_constraint

val mk_nexp : Ast.nexp_aux -> Ast.nexp

val mk_exp : ?loc:Ast.l -> unit Ast.exp_aux -> unit Ast.exp

val mk_pat : unit Ast.pat_aux -> unit Ast.pat

val mk_mpat : unit Ast.mpat_aux -> unit Ast.mpat

val mk_pexp : ?loc:Ast.l -> unit Ast.pexp_aux -> unit Ast.pexp

val mk_mpexp : unit Ast.mpexp_aux -> unit Ast.mpexp

val mk_lexp : unit Ast.lexp_aux -> unit Ast.lexp

val mk_lit : Ast.lit_aux -> Ast.lit

val mk_lit_exp : Ast.lit_aux -> unit Ast.exp

val mk_typ_pat : Ast.typ_pat_aux -> Ast.typ_pat

val mk_funcl : Ast.id -> unit Ast.pat -> unit Ast.exp -> unit Ast.funcl

val mk_fundef : unit Ast.funcl list -> unit Ast.def

val mk_val_spec : Ast.val_spec_aux -> unit Ast.def

val mk_typschm : Ast.typquant -> Ast.typ -> Ast.typschm

val mk_typquant : Ast.quant_item list -> Ast.typquant

val mk_qi_id : Ast.kind_aux -> Ast.kid -> Ast.quant_item

val mk_qi_nc : Ast.n_constraint -> Ast.quant_item

val mk_qi_kopt : Ast.kinded_id -> Ast.quant_item

val mk_fexp : Ast.id -> unit Ast.exp -> unit Ast.fexp

val mk_letbind : unit Ast.pat -> unit Ast.exp -> unit Ast.letbind

val mk_kopt : Ast.kind_aux -> Ast.kid -> Ast.kinded_id

val inc_ord : Ast.order

val dec_ord : Ast.order

val unaux_exp : 'a Ast.exp -> 'a Ast.exp_aux

val unaux_pat : 'a Ast.pat -> 'a Ast.pat_aux

val unaux_nexp : Ast.nexp -> Ast.nexp_aux

val unaux_order : Ast.order -> Ast.order_aux

val unaux_typ : Ast.typ -> Ast.typ_aux

val unaux_kind : Ast.kind -> Ast.kind_aux

val unaux_constraint : Ast.n_constraint -> Ast.n_constraint_aux

val untyp_pat : 'a Ast.pat -> 'a Ast.pat * Ast.typ option

val uncast_exp : 'a Ast.exp -> 'a Ast.exp * Ast.typ option

val kopt_kid : Ast.kinded_id -> Ast.kid

val kopt_kind : Ast.kinded_id -> Ast.kind

val is_int_kopt : Ast.kinded_id -> bool

val is_order_kopt : Ast.kinded_id -> bool

val is_typ_kopt : Ast.kinded_id -> bool

val is_bool_kopt : Ast.kinded_id -> bool

val mk_typ : Ast.typ_aux -> Ast.typ

val mk_typ_arg : Ast.typ_arg_aux -> Ast.typ_arg

val mk_id_typ : Ast.id -> Ast.typ

val unknown_typ : Ast.typ

val int_typ : Ast.typ

val nat_typ : Ast.typ

val atom_typ : Ast.nexp -> Ast.typ

val implicit_typ : Ast.nexp -> Ast.typ

val range_typ : Ast.nexp -> Ast.nexp -> Ast.typ

val bit_typ : Ast.typ

val bool_typ : Ast.typ

val atom_bool_typ : Ast.n_constraint -> Ast.typ

val app_typ : Ast.id -> Ast.typ_arg list -> Ast.typ

val register_typ : Ast.typ -> Ast.typ

val unit_typ : Ast.typ

val string_typ : Ast.typ

val real_typ : Ast.typ

val vector_typ : Ast.nexp -> Ast.order -> Ast.typ -> Ast.typ

val bitvector_typ : Ast.nexp -> Ast.order -> Ast.typ

val list_typ : Ast.typ -> Ast.typ

val exc_typ : Ast.typ

val tuple_typ : Ast.typ list -> Ast.typ

val function_typ : Ast.typ list -> Ast.typ -> Ast.effect -> Ast.typ

val is_unit_typ : Ast.typ -> bool

val is_number : Ast.typ -> bool

val is_ref_typ : Ast.typ -> bool

val is_vector_typ : Ast.typ -> bool

val is_bit_typ : Ast.typ -> bool

val is_bitvector_typ : Ast.typ -> bool

val nexp_simp : Ast.nexp -> Ast.nexp

val constraint_simp : Ast.n_constraint -> Ast.n_constraint

val constraint_conj : Ast.n_constraint -> Ast.n_constraint list

val constraint_disj : Ast.n_constraint -> Ast.n_constraint list

module Id : sig ... end

module Kid : sig ... end

module Kind : sig ... end

module KOpt : sig ... end

module Nexp : sig ... end

module BE : sig ... end

module NC : sig ... end

module Typ : sig ... end

module IdSet : sig ... end

module NexpSet : sig ... end

module NexpMap : sig ... end

module KOptSet : sig ... end

module KOptMap : sig ... end

module BESet : sig ... end

module KidSet : sig ... end

module KBindings : sig ... end

module Bindings : sig ... end

module NCMap : sig ... end

module TypMap : sig ... end

val no_effect : Ast.effect

val mk_effect : Ast.base_effect_aux list -> Ast.effect

val has_effect : Ast.effect -> Ast.base_effect_aux -> bool

val effect_set : Ast.effect -> BESet.t

val equal_effects : Ast.effect -> Ast.effect -> bool

val subseteq_effects : Ast.effect -> Ast.effect -> bool

val union_effects : Ast.effect -> Ast.effect -> Ast.effect

val nconstant : Big_int.num -> Ast.nexp

val nint : int -> Ast.nexp

val nminus : Ast.nexp -> Ast.nexp -> Ast.nexp

val nsum : Ast.nexp -> Ast.nexp -> Ast.nexp

val ntimes : Ast.nexp -> Ast.nexp -> Ast.nexp

val npow2 : Ast.nexp -> Ast.nexp

val nvar : Ast.kid -> Ast.nexp

val napp : Ast.id -> Ast.nexp list -> Ast.nexp

val nid : Ast.id -> Ast.nexp

val nc_eq : Ast.nexp -> Ast.nexp -> Ast.n_constraint

val nc_neq : Ast.nexp -> Ast.nexp -> Ast.n_constraint

val nc_lteq : Ast.nexp -> Ast.nexp -> Ast.n_constraint

val nc_gteq : Ast.nexp -> Ast.nexp -> Ast.n_constraint

val nc_lt : Ast.nexp -> Ast.nexp -> Ast.n_constraint

val nc_gt : Ast.nexp -> Ast.nexp -> Ast.n_constraint

val nc_and : Ast.n_constraint -> Ast.n_constraint -> Ast.n_constraint

val nc_or : Ast.n_constraint -> Ast.n_constraint -> Ast.n_constraint

val nc_not : Ast.n_constraint -> Ast.n_constraint

val nc_true : Ast.n_constraint

val nc_false : Ast.n_constraint

val nc_set : Ast.kid -> Big_int.num list -> Ast.n_constraint

val nc_int_set : Ast.kid -> int list -> Ast.n_constraint

val nc_var : Ast.kid -> Ast.n_constraint

val arg_nexp : ?loc:Ast.l -> Ast.nexp -> Ast.typ_arg

val arg_order : ?loc:Ast.l -> Ast.order -> Ast.typ_arg

val arg_typ : ?loc:Ast.l -> Ast.typ -> Ast.typ_arg

val arg_bool : ?loc:Ast.l -> Ast.n_constraint -> Ast.typ_arg

val arg_kopt : Ast.kinded_id -> Ast.typ_arg

val quant_add : Ast.quant_item -> Ast.typquant -> Ast.typquant

val quant_items : Ast.typquant -> Ast.quant_item list

val quant_kopts : Ast.typquant -> Ast.kinded_id list

val quant_split : Ast.typquant -> Ast.kinded_id list * Ast.n_constraint list

val quant_map_items : 
  (Ast.quant_item -> Ast.quant_item) ->
  Ast.typquant ->
  Ast.typquant

val is_quant_kopt : Ast.quant_item -> bool

val is_quant_constraint : Ast.quant_item -> bool

val map_exp_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.exp -> 'b Ast.exp

val map_pat_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.pat -> 'b Ast.pat

val map_pexp_annot : 
  ('a Ast.annot -> 'b Ast.annot) ->
  'a Ast.pexp ->
  'b Ast.pexp

val map_lexp_annot : 
  ('a Ast.annot -> 'b Ast.annot) ->
  'a Ast.lexp ->
  'b Ast.lexp

val map_letbind_annot : 
  ('a Ast.annot -> 'b Ast.annot) ->
  'a Ast.letbind ->
  'b Ast.letbind

val map_mpat_annot : 
  ('a Ast.annot -> 'b Ast.annot) ->
  'a Ast.mpat ->
  'b Ast.mpat

val map_mpexp_annot : 
  ('a Ast.annot -> 'b Ast.annot) ->
  'a Ast.mpexp ->
  'b Ast.mpexp

val map_mapcl_annot : 
  ('a Ast.annot -> 'b Ast.annot) ->
  'a Ast.mapcl ->
  'b Ast.mapcl

val map_typedef_annot : 
  ('a Ast.annot -> 'b Ast.annot) ->
  'a Ast.type_def ->
  'b Ast.type_def

val map_fundef_annot : 
  ('a Ast.annot -> 'b Ast.annot) ->
  'a Ast.fundef ->
  'b Ast.fundef

val map_funcl_annot : 
  ('a Ast.annot -> 'b Ast.annot) ->
  'a Ast.funcl ->
  'b Ast.funcl

val map_mapdef_annot : 
  ('a Ast.annot -> 'b Ast.annot) ->
  'a Ast.mapdef ->
  'b Ast.mapdef

val map_valspec_annot : 
  ('a Ast.annot -> 'b Ast.annot) ->
  'a Ast.val_spec ->
  'b Ast.val_spec

val map_scattered_annot : 
  ('a Ast.annot -> 'b Ast.annot) ->
  'a Ast.scattered_def ->
  'b Ast.scattered_def

val map_def_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.def -> 'b Ast.def

val map_ast_annot : 
  ('a Ast.annot -> 'b Ast.annot) ->
  'a Ast_defs.ast ->
  'b Ast_defs.ast

val id_loc : Ast.id -> Parse_ast.l

val kid_loc : Ast.kid -> Parse_ast.l

val typ_loc : Ast.typ -> Parse_ast.l

val pat_loc : 'a Ast.pat -> Parse_ast.l

val exp_loc : 'a Ast.exp -> Parse_ast.l

val def_loc : 'a Ast.def -> Parse_ast.l

val string_of_id : Ast.id -> string

val string_of_kid : Ast.kid -> string

val string_of_base_effect_aux : Ast.base_effect_aux -> string

val string_of_kind_aux : Ast.kind_aux -> string

val string_of_kind : Ast.kind -> string

val string_of_base_effect : Ast.base_effect -> string

val string_of_effect : Ast.effect -> string

val string_of_order : Ast.order -> string

val string_of_nexp : Ast.nexp -> string

val string_of_typ : Ast.typ -> string

val string_of_typ_arg : Ast.typ_arg -> string

val string_of_typ_pat : Ast.typ_pat -> string

val string_of_n_constraint : Ast.n_constraint -> string

val string_of_kinded_id : Ast.kinded_id -> string

val string_of_quant_item : Ast.quant_item -> string

val string_of_typquant : Ast.typquant -> string

val string_of_typschm : Ast.typschm -> string

val string_of_lit : Ast.lit -> string

val string_of_exp : 'a Ast.exp -> string

val string_of_pexp : 'a Ast.pexp -> string

val string_of_lexp : 'a Ast.lexp -> string

val string_of_pat : 'a Ast.pat -> string

val string_of_mpat : 'a Ast.mpat -> string

val string_of_letbind : 'a Ast.letbind -> string

val string_of_index_range : Ast.index_range -> string

val id_of_fundef : 'a Ast.fundef -> Ast.id

val id_of_type_def : 'a Ast.type_def -> Ast.id

val id_of_val_spec : 'a Ast.val_spec -> Ast.id

val id_of_dec_spec : 'a Ast.dec_spec -> Ast.id

val id_of_kid : Ast.kid -> Ast.id

val kid_of_id : Ast.id -> Ast.kid

val prepend_id : string -> Ast.id -> Ast.id

val append_id : Ast.id -> string -> Ast.id

val prepend_kid : string -> Ast.kid -> Ast.kid

val nexp_frees : Ast.nexp -> KidSet.t

val nexp_identical : Ast.nexp -> Ast.nexp -> bool

val is_nexp_constant : Ast.nexp -> bool

val int_of_nexp_opt : Ast.nexp -> Big_int.num option

val lexp_to_exp : 'a Ast.lexp -> 'a Ast.exp

val typ_app_args_of : Ast.typ -> string * Ast.typ_arg_aux list * Ast.l

val vector_typ_args_of : Ast.typ -> Ast.nexp * Ast.order * Ast.typ

val vector_start_index : Ast.typ -> Ast.nexp

val is_order_inc : Ast.order -> bool

val kopts_of_order : Ast.order -> KOptSet.t

val kopts_of_nexp : Ast.nexp -> KOptSet.t

val kopts_of_typ : Ast.typ -> KOptSet.t

val kopts_of_typ_arg : Ast.typ_arg -> KOptSet.t

val kopts_of_constraint : Ast.n_constraint -> KOptSet.t

val kopts_of_quant_item : Ast.quant_item -> KOptSet.t

val tyvars_of_nexp : Ast.nexp -> KidSet.t

val tyvars_of_typ : Ast.typ -> KidSet.t

val tyvars_of_constraint : Ast.n_constraint -> KidSet.t

val tyvars_of_quant_item : Ast.quant_item -> KidSet.t

val is_kid_generated : Ast.kid -> bool

val undefined_of_typ : 
  bool ->
  Ast.l ->
  (Ast.typ -> 'annot) ->
  Ast.typ ->
  'annot Ast.exp

val destruct_pexp : 
  'a Ast.pexp ->
  'a Ast.pat * 'a Ast.exp option * 'a Ast.exp * (Ast.l * 'a)

val construct_pexp : 
  ('a Ast.pat * 'a Ast.exp option * 'a Ast.exp * (Ast.l * 'a)) ->
  'a Ast.pexp

val destruct_mpexp : 
  'a Ast.mpexp ->
  'a Ast.mpat * 'a Ast.exp option * (Ast.l * 'a)

val construct_mpexp : 
  ('a Ast.mpat * 'a Ast.exp option * (Ast.l * 'a)) ->
  'a Ast.mpexp

val is_valspec : Ast.id -> 'a Ast.def -> bool

val is_fundef : Ast.id -> 'a Ast.def -> bool

val rename_valspec : Ast.id -> 'a Ast.val_spec -> 'a Ast.val_spec

val rename_fundef : Ast.id -> 'a Ast.fundef -> 'a Ast.fundef

val split_defs : 
  ('a Ast.def -> bool) ->
  'a Ast.def list ->
  ('a Ast.def list * 'a Ast.def * 'a Ast.def list) option

val append_ast : 'a Ast_defs.ast -> 'a Ast_defs.ast -> 'a Ast_defs.ast

val append_ast_defs : 'a Ast_defs.ast -> 'a Ast.def list -> 'a Ast_defs.ast

val concat_ast : 'a Ast_defs.ast list -> 'a Ast_defs.ast

val type_union_id : Ast.type_union -> Ast.id

val ids_of_def : 'a Ast.def -> IdSet.t

val ids_of_defs : 'a Ast.def list -> IdSet.t

val ids_of_ast : 'a Ast_defs.ast -> IdSet.t

val val_spec_ids : 'a Ast.def list -> IdSet.t

val pat_ids : 'a Ast.pat -> IdSet.t

val subst : Ast.id -> 'a Ast.exp -> 'a Ast.exp -> 'a Ast.exp

val hex_to_bin : string -> string

val vector_string_to_bit_list : Ast.lit -> Ast.lit list

val locate : (Ast.l -> Ast.l) -> 'a Ast.exp -> 'a Ast.exp

val locate_pat : (Ast.l -> Ast.l) -> 'a Ast.pat -> 'a Ast.pat

val locate_lexp : (Ast.l -> Ast.l) -> 'a Ast.lexp -> 'a Ast.lexp

val locate_typ : (Ast.l -> Ast.l) -> Ast.typ -> Ast.typ

val unique : Ast.l -> Ast.l

val extern_assoc : string -> (string * string) list -> string option

val find_annot_ast : 
  (Stdlib.Lexing.position * Stdlib.Lexing.position) option ->
  'a Ast_defs.ast ->
  (Ast.l * 'a) option

val nexp_subst : Ast.kid -> Ast.typ_arg -> Ast.nexp -> Ast.nexp

val constraint_subst : 
  Ast.kid ->
  Ast.typ_arg ->
  Ast.n_constraint ->
  Ast.n_constraint

val order_subst : Ast.kid -> Ast.typ_arg -> Ast.order -> Ast.order

val typ_subst : Ast.kid -> Ast.typ_arg -> Ast.typ -> Ast.typ

val typ_arg_subst : Ast.kid -> Ast.typ_arg -> Ast.typ_arg -> Ast.typ_arg

val subst_kid : 
  (Ast.kid -> Ast.typ_arg -> 'a -> 'a) ->
  Ast.kid ->
  Ast.kid ->
  'a ->
  'a

val subst_kids_nexp : Ast.nexp KBindings.t -> Ast.nexp -> Ast.nexp

val subst_kids_nc : 
  Ast.nexp KBindings.t ->
  Ast.n_constraint ->
  Ast.n_constraint

val subst_kids_typ : Ast.nexp KBindings.t -> Ast.typ -> Ast.typ

val subst_kids_typ_arg : Ast.nexp KBindings.t -> Ast.typ_arg -> Ast.typ_arg

val quant_item_subst_kid : 
  Ast.kid ->
  Ast.kid ->
  Ast.quant_item ->
  Ast.quant_item

val typquant_subst_kid : Ast.kid -> Ast.kid -> Ast.typquant -> Ast.typquant

val simple_string_of_loc : Parse_ast.l -> string

val attach_comments : Lexer.comment list -> 'a Ast.def list -> 'a Ast.def list