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_type_grouped_regstate : bool ref
val defs_of_string : string -> unit Ast.def list
val is_defined : 'a Ast.def list -> string -> bool
val has_default_order : 'a Ast.def list -> bool
val find_registers : Type_check.tannot Ast.def list -> (Ast.typ * Ast.id) list
val generate_register_id_enum : ('a * Ast.id) list -> string list
val id_of_regtyp : Ast_util.IdSet.t -> bool -> Ast.typ -> Ast.id
val regstate_field : Ast.typ -> Ast.id
val generate_regstate : (Ast.typ * Ast.id) list -> unit Ast.def list
val generate_initial_regstate : Type_check.tannot Ast.def list -> unit Ast.def list list
val regval_constr_id : bool -> Ast.typ -> Ast.id
val register_base_types : bool -> Ast.typ list -> Ast.typ Ast_util.Bindings.t
val generate_regval_typ : Ast.typ Ast_util.Bindings.t -> unit Ast.def list list
val add_regval_conv : Ast.id -> Ast.typ -> unit Ast.def list -> unit Ast.def list
val regval_convs_lem : bool -> Ast.typ -> string * string
val register_refs_lem : bool -> (Ast.typ * Ast.id) list -> PPrint.document
val generate_isa_lemmas : bool -> Type_check.tannot Ast.def list -> PPrint.document
val regval_convs_coq : Ast.typ -> string * string
val register_refs_coq : (Ast.typ * Ast.id) list -> PPrint.document
val generate_regstate_defs : bool -> Type_check.tannot Ast.def list -> unit Ast.def list