summaryrefslogtreecommitdiff
path: root/lib/vector_dec.sail
blob: 84493f734282020bd408938f6296fa3c2c581bc9 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
$ifndef _VECTOR_DEC
$define _VECTOR_DEC

type bits ('n : Int) = vector('n, dec, bit)

val "zeros" : forall 'n. atom('n) -> bits('n)

val "print_bits" : forall 'n. (string, bits('n)) -> unit

val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)

val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64)

val add_bits = {
  ocaml: "add_vec",
  c: "add_bits"
} : forall 'n. (bits('n), bits('n)) -> bits('n)

val add_bits_int = {
  ocaml: "add_vec_int",
  c: "add_bits_int"
} : forall 'n. (bits('n), int) -> bits('n)

$endif