/* Content from riscv_xlen64.sail */
default Order dec

/* $include <smt.sail> */
$include <option.sail>
/* $include <arith.sail> */
$include <string.sail>
$include <vector_dec.sail>
/* $include <regfp.sail> */

type xlen       : Int = 64
type xlen_bytes : Int = 8
type xlenbits         = bits(xlen)

/* Content from prelude.sail */

val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
val EXTZ : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)

function EXTS(m, v) = sail_sign_extend(v, m)
function EXTZ(m, v) = sail_zero_extend(v, m)

val string_length = "string_length" : string -> nat
val string_startswith = "string_startswith" : (string, string) -> bool
val string_drop = "string_drop" : (string, nat) -> string
val string_take = "string_take" : (string, nat) -> string
val string_length = "string_length" : string -> nat
val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string
/* Content from riscv_reg_type.sail*/

/* default register type */
type regtype = xlenbits

/* default zero register */
let zero_reg : regtype = EXTZ(0x0)

/* default register printer */
/* val RegStr : regtype -> string */
/* function RegStr(r) = BitStr(r) */

/* conversions */

val regval_from_reg : regtype -> xlenbits
function regval_from_reg(r) = r

val regval_into_reg : xlenbits -> regtype
function regval_into_reg(v) = v

/* register file indexing */

type regno ('n : Int), 0 <= 'n < 32 = atom('n)

/* val regidx_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)} */
/* function regidx_to_regno b = let 'r = unsigned(b) in r */

/* register identifiers */

type regidx  = bits(5)
type cregidx = bits(3)    /* identifiers in RVC instructions */
type csreg   = bits(12)   /* CSR addressing */