diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/typecheck/pass/ex_cast.sail | 2 | ||||
| -rw-r--r-- | test/typecheck/pass/exint.sail | 4 | ||||
| -rw-r--r-- | test/typecheck/pass/lexp_memory.sail | 2 | ||||
| -rw-r--r-- | test/typecheck/pass/mips_CP0Cause_BD_assign1.sail | 2 | ||||
| -rw-r--r-- | test/typecheck/pass/mips_CP0Cause_BD_assign2.sail | 2 |
5 files changed, 6 insertions, 6 deletions
diff --git a/test/typecheck/pass/ex_cast.sail b/test/typecheck/pass/ex_cast.sail index 5ea22d14..964bfa72 100644 --- a/test/typecheck/pass/ex_cast.sail +++ b/test/typecheck/pass/ex_cast.sail @@ -3,7 +3,7 @@ default Order dec val cast int -> exist 'n. [:'n:] effect pure ex_int -val [:'n:] -> bit['n] effect pure zeros +val forall 'n. [:'n:] -> bit['n] effect pure zeros val int -> unit effect pure test diff --git a/test/typecheck/pass/exint.sail b/test/typecheck/pass/exint.sail index dfe51eb9..1239fa44 100644 --- a/test/typecheck/pass/exint.sail +++ b/test/typecheck/pass/exint.sail @@ -1,9 +1,9 @@ typedef Int = exist 'n. [:'n:] -val ([:'n:], [:'m:]) -> exist 'o, 'o = 'n + 'm. [:'o:] effect pure add +val forall 'n, 'm. ([:'n:], [:'m:]) -> exist 'o, 'o = 'n + 'm. [:'o:] effect pure add -val ([:'n:], [:'m:]) -> exist 'o, 'o = 'n * 'm. [:'o:] effect pure mult +val forall 'n, 'm. ([:'n:], [:'m:]) -> exist 'o, 'o = 'n * 'm. [:'o:] effect pure mult overload (deinfix +) [add] diff --git a/test/typecheck/pass/lexp_memory.sail b/test/typecheck/pass/lexp_memory.sail index cc84130f..321fb315 100644 --- a/test/typecheck/pass/lexp_memory.sail +++ b/test/typecheck/pass/lexp_memory.sail @@ -48,7 +48,7 @@ val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'or overload (deinfix ==) [eq_vec] -val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec +val extern forall Num 'l, 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) diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail index 0160dd8a..54ae354f 100644 --- a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail @@ -1,7 +1,7 @@ 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 +val extern forall Num 'l, 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) diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail index 847bca60..2e80f538 100644 --- a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail @@ -1,7 +1,7 @@ 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 +val extern forall Num 'l, 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) |