libsail 0.17.1 (latest) · OCaml Package

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 * bool) 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 * 'a) list ->
  Ast_util.uannot Ast.def list

val generate_initial_regstate : 
  Type_check.Env.t ->
  Type_check.tannot Ast_defs.ast ->
  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 * 'a) 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 * 'd) list ->
  PPrint.document

val generate_regstate_defs : 
  Type_check.Env.t ->
  Type_check.tannot Ast_defs.ast ->
  Ast_util.uannot Ast.def list

val add_regstate_defs : 
  'a ->
  Type_check.Env.t ->
  Type_check.tannot Ast_defs.ast ->
  Type_check.Env.t * Type_check.tannot Ast_defs.ast

package libsail