package libsail

  1. Overview
  2. Docs
module Big_int = Nat_big_num
val opt_type_grouped_regstate : bool Stdlib.ref
val is_defined : 'a Ast.def list -> string -> bool
val get_bitfield_typ_id : Type_check.Env.t -> Ast.typ -> Ast.id option
val is_bitfield_typ : Type_check.Env.t -> Ast.typ -> bool
val regval_base_typ : Type_check.Env.t -> Ast.typ -> Ast.typ
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 -> Ast.typ -> Ast.id
val regstate_field : Ast.typ -> Ast.id
val generate_regstate : Type_check.Env.t -> (Ast.typ * Ast.id) list -> Ast_util.uannot Ast.def list
val generate_initial_regstate : Type_check.Env.t -> Type_check.tannot Ast.def list -> Ast_util.uannot Ast.def list list
val regval_constr_id : Ast.typ -> Ast.id
val register_base_types : Type_check.Env.t -> Ast.typ list -> Ast.typ Ast_util.Bindings.t
val register_bitfield_types : Type_check.Env.t -> Ast.typ list -> Ast.typ Ast_util.Bindings.t
val generate_regval_typ : 'a -> Ast.typ Ast_util.Bindings.t -> Ast_util.uannot Ast.def list list
val regval_class_typs_lem : (string * string) list
val regval_instance_lem : PPrint.document
val regval_base_convs : Ast.typ -> string * string
val add_regval_conv : Type_check.Env.t -> 'a -> Ast.typ -> Ast_util.uannot Ast.def list -> Ast_util.uannot Ast.def list
val regval_convs : (string -> string) -> Ast.typ -> string * string
val regval_convs_lem : Ast.typ -> string * string
val regval_convs_isa : Ast.typ -> string * string
val register_refs_lem : (Ast.typ -> PPrint.document) -> Type_check.Env.t -> (Ast.typ * Ast.id) list -> PPrint.document
val generate_isa_lemmas : Type_check.Env.t -> Type_check.tannot Ast.def list -> PPrint.document
val regval_convs_coq : 'a -> Ast.typ -> string * string
val register_refs_coq : ('a -> PPrint.document) -> 'b -> (Ast.typ * 'c) list -> PPrint.document
val generate_regstate_defs : Type_check.Env.t -> Type_check.tannot Ast.def list -> Ast_util.uannot Ast.def list