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

type !'a aexp =

| AE_aux of 'a aexp_aux * Type_check.Env.t * Ast.l

and !'a aexp_aux =

| AE_val of 'a aval
| AE_app of Ast.id * 'a aval list * 'a
| AE_cast of 'a aexp * 'a
| AE_assign of 'a alexp * 'a aexp
| AE_let of Ast_util.mut * Ast.id * 'a * 'a aexp * 'a aexp * 'a
| AE_block of 'a aexp list * 'a aexp * 'a
| AE_return of 'a aval * 'a
| AE_throw of 'a aval * 'a
| AE_if of 'a aval * 'a aexp * 'a aexp * 'a
| AE_field of 'a aval * Ast.id * 'a
| AE_case of 'a aval * ('a apat * 'a aexp * 'a aexp) list * 'a
| AE_try of 'a aexp * ('a apat * 'a aexp * 'a aexp) list * 'a
| AE_record_update of 'a aval * 'a aval Ast_util.Bindings.t * 'a
| AE_for of Ast.id * 'a aexp * 'a aexp * 'a aexp * Ast.order * 'a aexp
| AE_loop of Ast.loop * 'a aexp * 'a aexp
| AE_short_circuit of sc_op * 'a aval * 'a aexp

and sc_op =

| SC_and
| SC_or

and !'a apat =

| AP_aux of 'a apat_aux * Type_check.Env.t * Ast.l

and !'a apat_aux =

| AP_tup of 'a apat list
| AP_id of Ast.id * 'a
| AP_global of Ast.id * 'a
| AP_app of Ast.id * 'a apat * 'a
| AP_cons of 'a apat * 'a apat
| AP_as of 'a apat * Ast.id * 'a
| AP_nil of 'a
| AP_wild of 'a

and !'a aval =

| AV_lit of Ast.lit * 'a
| AV_id of Ast.id * 'a Ast_util.lvar
| AV_ref of Ast.id * 'a Ast_util.lvar
| AV_tuple of 'a aval list
| AV_list of 'a aval list * 'a
| AV_vector of 'a aval list * 'a
| AV_record of 'a aval Ast_util.Bindings.t * 'a
| AV_cval of Jib.cval * 'a

and !'a alexp =

| AL_id of Ast.id * 'a
| AL_addr of Ast.id * 'a
| AL_field of 'a alexp * Ast.id

val reset_anf_counter : unit -> unit

val aexp_loc : 'a aexp -> Parse_ast.l

val aval_typ : Ast.typ aval -> Ast.typ

val aexp_typ : Ast.typ aexp -> Ast.typ

val map_aval : 
  (Type_check.Env.t -> Ast.l -> 'a aval -> 'a aval) ->
  'a aexp ->
  'a aexp

val map_functions : 
  (Type_check.Env.t -> Ast.l -> Ast.id -> 'a aval list -> 'a -> 'a aexp_aux) ->
  'a aexp ->
  'a aexp

val fold_aexp : ('a aexp -> 'a aexp) -> 'a aexp -> 'a aexp

val no_shadow : Ast_util.IdSet.t -> 'a aexp -> 'a aexp

val apat_globals : 'a apat -> (Ast.id * 'a) list

val apat_types : 'a apat -> 'a Ast_util.Bindings.t

val is_dead_aexp : 'a aexp -> bool

val anf_pat : ?global:bool -> Type_check.tannot Ast.pat -> Ast.typ apat

val anf : Type_check.tannot Ast.exp -> Ast.typ aexp

val pp_aval : Ast.typ aval -> PPrint.document

val pp_aexp : Ast.typ aexp -> PPrint.document