diff options
| author | Alasdair Armstrong | 2018-02-19 20:12:46 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-02-19 20:27:15 +0000 |
| commit | 5073f0e9502e5f696ff68b275310bd15187d8e1f (patch) | |
| tree | 96221d698dae97237d4fec035a555e727829a704 /lib | |
| parent | 51c122d99a1a481bc916f766ae6bd2a6a66de6d2 (diff) | |
Have generic vectors working in C backend
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/flow.sail | 2 | ||||
| -rw-r--r-- | lib/vector_dec.sail | 12 |
2 files changed, 14 insertions, 0 deletions
diff --git a/lib/flow.sail b/lib/flow.sail index 8c902803..1a0e0f2f 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -34,6 +34,8 @@ val lt_int = "lt" : (int, int) -> bool val gt_int = "lt" : (int, int) -> bool overload operator == = {eq_atom, eq_range, eq_int} +overload operator | = {or_bool} +overload operator & = {and_bool} $ifdef TEST diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index e24f5111..8a55ed61 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -13,6 +13,18 @@ val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) /* Used for creating long bitvector literals in the C backend. */ val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64) +val vector_access = { + ocaml: "access", + lem: "access_list_dec", + c: "vector_access" +} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m)) -> 'a + +val vector_update = { + ocaml: "update", + lem: "update_list_dec", + c: "vector_update" +} : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) + val add_bits = { ocaml: "add_vec", c: "add_bits" |