diff options
| author | Alasdair Armstrong | 2017-06-24 19:06:22 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-06-24 19:06:22 +0100 |
| commit | 7691516974eaaa7c41179818e1d76d073c72cc18 (patch) | |
| tree | d64c7305733b3729d4d6fe3eac37f09297c22efc /test | |
| parent | 98a20e197ef086bd294e157f4eaf75f9f025ff69 (diff) | |
Added implicit casting
Added support for implicit casting to the bi-directional type
checker. The casts can be any user-specified function, and in princple
don't have to be hardcoded. This allows us to typecheck definitions such as
function bit[64] rGPR idx = {
if idx == 0 then 0 else GPR[idx]
}
in the MIPS spec, which involves lots of casting from integers to
bitvectors, as well as casting from a named register to it's value
(implicit dereferencing).
Diffstat (limited to 'test')
| -rw-r--r-- | test/typecheck/pass/vector_access.sail | 3 | ||||
| -rw-r--r-- | test/typecheck/pass/vector_append.sail | 3 |
2 files changed, 2 insertions, 4 deletions
diff --git a/test/typecheck/pass/vector_access.sail b/test/typecheck/pass/vector_access.sail index 9346f5fe..c7c1b502 100644 --- a/test/typecheck/pass/vector_access.sail +++ b/test/typecheck/pass/vector_access.sail @@ -1,5 +1,6 @@ -val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec +val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc default Order inc diff --git a/test/typecheck/pass/vector_append.sail b/test/typecheck/pass/vector_append.sail index d2f1ca47..af83c44d 100644 --- a/test/typecheck/pass/vector_append.sail +++ b/test/typecheck/pass/vector_append.sail @@ -1,5 +1,4 @@ -val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0. (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append @@ -10,8 +9,6 @@ val (bit[4], bit[4]) -> bit[8] effect pure test function bit[8] test (v1, v2) = { - z := vector_access(v1, 3); - z := v1[0]; zv := vector_append(v1, v2); zv := v1 : v2; zv |