Module `Libsail.State`Source

module Big_int = Nat_big_num

Sourceval opt_type_grouped_regstate : bool ref

Sourceval is_defined : ('a, 'b) Ast.def list -> string -> bool

Sourceval get_bitfield_typ_id : Type_check.Env.t -> Ast.typ -> Ast.id option

Sourceval is_bitfield_typ : Type_check.Env.t -> Ast.typ -> bool

Sourceval regval_base_typ : Type_check.Env.t -> Ast.typ -> Ast.typ

Sourceval has_default_order : ('a, 'b) Ast.def list -> bool

val find_registers : 
  (Type_check.tannot, 'a) Ast.def list ->
  (Ast.typ * Ast.id * bool) list

Sourceval generate_register_id_enum : ('a * Ast.id) list -> string list

Sourceval id_of_nexp : Ast.nexp -> string

Sourceval id_of_nexp_aux : Ast.nexp_aux -> string

Sourceval id_of_regtyp : Ast_util.IdSet.t -> Ast.typ -> Ast.id

Sourceval regstate_field : Ast.typ -> Ast.id

Source

val generate_regstate : 
  Type_check.Env.t ->
  (Ast.typ * Ast.id * 'a) list ->
  (Ast_util.uannot, unit) Ast.def list

Source

val generate_initial_regstate : 
  Initial_check.ctx ->
  Type_check.env ->
  Type_check.typed_ast ->
  Ast_util.untyped_def list list

Sourceval regval_constr_id : Ast.typ -> Ast.id

Source

val register_base_types : 
  Type_check.Env.t ->
  Ast.typ list ->
  Ast.typ Ast_util.Bindings.t

Source

val register_bitfield_types : 
  Type_check.Env.t ->
  Ast.typ list ->
  Ast.typ Ast_util.Bindings.t

Source

val generate_regval_typ : 
  Initial_check.ctx ->
  'a ->
  Ast.typ Ast_util.Bindings.t ->
  Ast_util.untyped_def list * Initial_check.ctx

Sourceval regval_class_typs_lem : (string * string) list

Sourceval regval_instance_lem : PPrint.document

Sourceval regval_base_convs : Ast.typ -> string * string

Source

val add_regval_conv : 
  Initial_check.ctx ->
  Type_check.Env.t ->
  'a ->
  Ast.typ ->
  (Ast_util.uannot, unit) Ast.def list ->
  (Ast_util.uannot, unit) Ast.def list

Sourceval regval_convs : (string -> string) -> Ast.typ -> string * string

Sourceval regval_convs_lem : Ast.typ -> string * string

Sourceval regval_convs_isa : Ast.typ -> string * string

Source

val register_refs_lem : 
  (Ast.typ -> PPrint.document) ->
  Type_check.Env.t ->
  (Ast.typ * Ast.id * 'a) list ->
  PPrint.document

Source

val generate_isa_lemmas : 
  Type_check.Env.t ->
  (Type_check.tannot, 'a) Ast.def list ->
  PPrint.document

Sourceval regval_convs_coq : 'a -> Ast.typ -> string * string

Source

val register_refs_coq : 
  ('a -> PPrint.document) ->
  bool ->
  'b ->
  (Ast.typ * 'a * 'c) list ->
  PPrint.document

Source

val generate_regstate_defs : 
  Initial_check.ctx ->
  Type_check.Env.t ->
  (Type_check.tannot, Type_check.env) Ast_defs.ast ->
  (Ast_util.uannot, unit) Ast.def list * Initial_check.ctx

Source

val add_regstate_defs : 
  'a ->
  Initial_check.ctx ->
  Type_check.Env.t ->
  (Type_check.tannot, Type_check.env) Ast_defs.ast ->
  Initial_check.ctx
  * Type_check.Env.t
  * (Type_check.tannot, Type_check.env) Ast_defs.ast

Source

val add_register_init_function : 
  'a ->
  Type_check.Env.t ->
  (Type_check.tannot, Type_check.env) Ast_defs.ast ->
  (Type_check.tannot, Type_check.env) Ast_defs.ast * 'a * Type_check.Env.t

package libsail

Module Libsail.StateSource

Module `Libsail.State`Source