diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/typecheck/pass/lexp_memory.sail | 5 | ||||
| -rw-r--r-- | test/typecheck/pass/mips_CP0Cause_BD_assign1.sail | 9 | ||||
| -rw-r--r-- | test/typecheck/pass/mips_CP0Cause_BD_assign2.sail | 9 | ||||
| -rw-r--r-- | test/typecheck/pass/set_mark.sail | 7 | ||||
| -rw-r--r-- | test/typecheck/pass/set_mark2.sail | 8 | ||||
| -rw-r--r-- | test/typecheck/pass/varity.sail | 4 | ||||
| -rw-r--r-- | test/typecheck/pass/vector_synonym_cast.sail | 2 |
7 files changed, 36 insertions, 8 deletions
diff --git a/test/typecheck/pass/lexp_memory.sail b/test/typecheck/pass/lexp_memory.sail index 83313ac7..cc84130f 100644 --- a/test/typecheck/pass/lexp_memory.sail +++ b/test/typecheck/pass/lexp_memory.sail @@ -48,7 +48,10 @@ val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'or overload (deinfix ==) [eq_vec] -val cast forall Nat 'n, Nat 'l, Order 'ord. [|0:1|] -> vector<'n,'l,'ord,bit> effect pure cast_01_vec +val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +val cast forall Nat 'n, Nat 'l. [|0:1|] -> vector<'n,'l,dec,bit> effect pure cast_01_vec +function forall Num 'n, Num 'l. (vector<'n,'l,dec,bit>) cast_01_vec i = to_vec_dec (sizeof 'n, sizeof 'l, i) val cast forall Nat 'n, Nat 'm, Order 'ord. vector<'n,'m,'ord,bit> -> [|0:2**'m - 1|] effect pure unsigned val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail index 7808b2c0..0160dd8a 100644 --- a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail @@ -1,5 +1,10 @@ -val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_1_vec -val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_0_vec +val cast forall Num 'n. [:1:] -> vector<'n,1,dec,bit> effect pure cast_1_vec +val cast forall Num 'n. [:0:] -> vector<'n,1,dec,bit> effect pure cast_0_vec + +val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +function forall Num 'n. (vector<'n,1,dec,bit>) cast_1_vec i = to_vec_dec (sizeof 'n, 1, i) +function forall Num 'n. (vector<'n,1,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, 1, i) default Order dec diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail index 26f161e2..847bca60 100644 --- a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail @@ -1,6 +1,11 @@ -val cast forall Nat 'n, Order 'ord. [:1:] -> vector<'n,1,'ord,bit> effect pure cast_1_vec -val cast forall Nat 'n, Order 'ord. [:0:] -> vector<'n,1,'ord,bit> effect pure cast_0_vec +val cast forall Num 'n. [:1:] -> vector<'n,1,dec,bit> effect pure cast_1_vec +val cast forall Num 'n. [:0:] -> vector<'n,1,dec,bit> effect pure cast_0_vec +val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +function forall Num 'n. (vector<'n,1,dec,bit>) cast_1_vec i = to_vec_dec (sizeof 'n, 1, i) +function forall Num 'n. (vector<'n,1,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, 1, i) + default Order dec typedef CauseReg = register bits [ 31 : 0 ] { diff --git a/test/typecheck/pass/set_mark.sail b/test/typecheck/pass/set_mark.sail index 7bc7370b..af0b5ba2 100644 --- a/test/typecheck/pass/set_mark.sail +++ b/test/typecheck/pass/set_mark.sail @@ -1,5 +1,10 @@ -val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_0_vec +val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +val cast forall Num 'n, Num 'm. [:0:] -> vector<'n,'m,dec,bit> effect pure cast_0_vec +function forall Num 'n, Num 'm. (vector<'n,'m,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, sizeof 'm, i) + +default Order dec function forall Num 'N, 'N IN {32}. bit['N] Foo32( (bit['N]) x) = x diff --git a/test/typecheck/pass/set_mark2.sail b/test/typecheck/pass/set_mark2.sail index cabfb1af..591c17ad 100644 --- a/test/typecheck/pass/set_mark2.sail +++ b/test/typecheck/pass/set_mark2.sail @@ -1,4 +1,10 @@ -val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_0_vec + +val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec + +val cast forall Num 'n, Num 'm. [:0:] -> vector<'n,'m,dec,bit> effect pure cast_0_vec +function forall Num 'n, Num 'm. (vector<'n,'m,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, sizeof 'm, i) + +default Order dec function forall Nat 'N, 'N IN {32, 64}. bit['N] Foo32( (bit['N]) x) = x diff --git a/test/typecheck/pass/varity.sail b/test/typecheck/pass/varity.sail index d196f777..750d70eb 100644 --- a/test/typecheck/pass/varity.sail +++ b/test/typecheck/pass/varity.sail @@ -3,6 +3,10 @@ val int -> unit effect pure f1 val (int, int) -> unit effect pure f2 val (int, int, int) -> unit effect pure f3 +function f1 (i1) = () +function f2 (i1, i2) = () +function f3 (i1, i2, i3) = () + overload f [f1; f2; f3] val unit -> unit effect pure test diff --git a/test/typecheck/pass/vector_synonym_cast.sail b/test/typecheck/pass/vector_synonym_cast.sail index f1de42e9..bd0acaa6 100644 --- a/test/typecheck/pass/vector_synonym_cast.sail +++ b/test/typecheck/pass/vector_synonym_cast.sail @@ -1,7 +1,7 @@ typedef vecsyn = vector<0,1,dec,bit> -val cast vector<1,1,dec,bit> -> vector<0,1,dec,bit> effect pure adjust_dec +val cast vector<1,1,dec,bit> -> vector<0,1,dec,bit> effect pure norm_dec val vector<1,1,dec,bit> -> vecsyn effect pure test |