summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/typecheck/fail/exist1.sail30
-rw-r--r--test/typecheck/pass/exint.sail22
-rw-r--r--test/typecheck/pass/exist1.sail30
-rw-r--r--test/typecheck/pass/exist2.sail46
-rw-r--r--test/typecheck/pass/exist_pattern.sail38
-rw-r--r--test/typecheck/pass/exist_simple.sail15
-rw-r--r--test/typecheck/pass/exist_tlb.sail94
-rw-r--r--test/typecheck/pass/return_simple4.sail (renamed from test/typecheck/fail/return_simple1.sail)0
-rw-r--r--test/typecheck/pass/varity.sail15
9 files changed, 290 insertions, 0 deletions
diff --git a/test/typecheck/fail/exist1.sail b/test/typecheck/fail/exist1.sail
new file mode 100644
index 00000000..3fab1366
--- /dev/null
+++ b/test/typecheck/fail/exist1.sail
@@ -0,0 +1,30 @@
+
+let (exist 'n, 'n in {0, 1}. [:'n:]) v1 = 0
+
+val bool -> exist 'n, 'n in {0, 1}. [:'n:] effect pure test
+
+function test flag =
+{
+ if flag then 0 else 1
+}
+
+let ([|0:1|]) v2 = test(true)
+
+val forall 'a, 'b. ([:'a:], [:'b:]) -> [:'a + 'b:] effect pure add
+
+let (exist 'k, 'k in {3, 4}. [:'k:]) v3 = 3
+
+let (exist 'q, 'q in {0, 1}. [:'q + 3:]) v4 = v3
+
+let v5 = add(test(true), 4)
+
+let ([:4:]) v6 = 4
+
+function unit unit_fn (([:4:]) x) = ()
+
+val forall 'a. ([:'a:], [:'a:]) -> [:'a + 'a:] effect pure s_add
+
+let (exist 'k, 'k = 4. [:'k:]) v7 = 4
+
+let v8 = s_add(test(true), 4)
+
diff --git a/test/typecheck/pass/exint.sail b/test/typecheck/pass/exint.sail
new file mode 100644
index 00000000..dfe51eb9
--- /dev/null
+++ b/test/typecheck/pass/exint.sail
@@ -0,0 +1,22 @@
+
+typedef Int = exist 'n. [:'n:]
+
+val ([:'n:], [:'m:]) -> exist 'o, 'o = 'n + 'm. [:'o:] effect pure add
+
+val ([:'n:], [:'m:]) -> exist 'o, 'o = 'n * 'm. [:'o:] effect pure mult
+
+overload (deinfix +) [add]
+
+overload (deinfix * ) [mult]
+
+let x = 3 + 4
+
+let y = x + x * x
+
+let ([:7 * 8:]) z = y
+
+typedef Range = forall Num 'n, Num 'm, 'n <= 'm. exist 'o, 'n <= 'o & 'o <= 'm. [:'o:]
+
+let (Range<3,4>) a = 3
+
+let (Range<2,5>) b = a + 1 \ No newline at end of file
diff --git a/test/typecheck/pass/exist1.sail b/test/typecheck/pass/exist1.sail
new file mode 100644
index 00000000..31968f36
--- /dev/null
+++ b/test/typecheck/pass/exist1.sail
@@ -0,0 +1,30 @@
+
+let (exist 'n, 'n in {0, 1}. [:'n:]) v1 = 0
+
+val bool -> exist 'n, 'n in {0, 1}. [:'n:] effect pure test
+
+function test flag =
+{
+ if flag then 0 else 1
+}
+
+let ([|0:1|]) v2 = test(true)
+
+val forall 'a, 'b. ([:'a:], [:'b:]) -> [:'a + 'b:] effect pure add
+
+let (exist 'k, 'k in {3, 4}. [:'k:]) v3 = 3
+
+let (exist 'q, 'q in {0, 1}. [:'q + 3:]) v4 = v3
+
+let v5 = add(test(true), 4)
+
+let ([:4:]) v6 = 4
+
+function unit unit_fn (([:4:]) x) = ()
+
+val forall 'a. ([:'a:], [:'a:]) -> [:'a + 'a:] effect pure s_add
+
+let (exist 'k, 'k = 4. [:'k:]) v7 = 4
+
+let v8 = s_add(v7, 4)
+
diff --git a/test/typecheck/pass/exist2.sail b/test/typecheck/pass/exist2.sail
new file mode 100644
index 00000000..04ccb57b
--- /dev/null
+++ b/test/typecheck/pass/exist2.sail
@@ -0,0 +1,46 @@
+
+let (exist 'n, 'n in {0, 1}. [:'n:]) v1 = 0
+
+val bool -> exist 'n, 'n in {0, 1}. [:'n:] effect pure test
+
+function test flag =
+{
+ if flag then 0 else 1
+}
+
+let ([|0:1|]) v2 = test(true)
+
+val forall 'a, 'b. ([:'a:], [:'b:]) -> [:'a + 'b:] effect pure add
+
+let (exist 'k, 'k in {3, 4}. [:'k:]) v3 = 3
+
+let (exist 'q, 'q in {0, 1}. [:'q + 3:]) v4 = v3
+
+let v5 = add(test(true), 4)
+
+let ([:4:]) v6 = 4
+
+function unit unit_fn (([:4:]) x) = ()
+
+val forall 'a. ([:'a:], [:'a:]) -> [:'a + 'a:] effect pure s_add
+
+let (exist 'k, 'k = 4. [:'k:]) v7 = 4
+
+(* let v8 = s_add(test(true), 4) *)
+
+let (exist 'n, 0 = 0. [:'n:]) v9 = 100
+
+let (int) v10 = v9
+
+typedef Int = exist 'n, 0 = 0. [:'n:]
+
+val int -> Int effect pure existential_int
+val forall 'n, 'm. range<'n,'m> -> exist 'e, 'n <= 'e & 'e <= 'm. [:'e:] effect pure existential_range
+
+overload existential [existential_int; existential_range]
+
+let (exist 'n, 0 = 0. [:'n:]) v11 = existential(v10)
+
+let (exist 'e, 0 <= 'e & 'e <= 3. [:'e:]) v12 = existential(([|0:3|]) 2)
+
+let (Int) v13 = existential(v10)
diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail
new file mode 100644
index 00000000..46913de4
--- /dev/null
+++ b/test/typecheck/pass/exist_pattern.sail
@@ -0,0 +1,38 @@
+default Order inc
+
+register nat n
+register nat x
+register nat y
+
+typedef wordsize = exist 'n, 'n IN {8,16,32}. [|'n|]
+let (wordsize) word = ([|8|]) 8
+
+function nat main () = {
+
+ (* works - x and y are set to 42 *)
+ n := 1;
+ y :=
+ (switch n {
+ case 0 -> { x := 21; x }
+ case 1 -> { x := 42; x }
+ case z -> { x := 99; x }
+ });
+
+ switch word {
+ case ([|8|]) 8 -> { x:= 32; }
+ case ([|16|]) 16 -> { x:= 64; }
+ case ([|32|]) 32 -> { x:= 128; }
+ };
+
+ switch 0b010101 {
+ case (0b01:(bit[1]) _:0b101) -> n:= 42
+ case _ -> n:=0
+ };
+
+ n := 3;
+ switch n {
+ case 0 -> { 21 }
+ case 1 -> { 42 }
+ case u -> { 99 }
+ };
+}
diff --git a/test/typecheck/pass/exist_simple.sail b/test/typecheck/pass/exist_simple.sail
new file mode 100644
index 00000000..87e62b13
--- /dev/null
+++ b/test/typecheck/pass/exist_simple.sail
@@ -0,0 +1,15 @@
+
+register bool reg
+
+let (exist 'n, 0 <= 'n & 'n <= 4. [:'n:]) A = 4
+
+let ([|0:4|]) B = A
+
+val unit -> exist 'n, 'n in {0, 1}. [:'n:] effect {rreg} test
+
+function test () =
+{
+ if reg
+ then 0
+ else 1
+}
diff --git a/test/typecheck/pass/exist_tlb.sail b/test/typecheck/pass/exist_tlb.sail
new file mode 100644
index 00000000..525d29c6
--- /dev/null
+++ b/test/typecheck/pass/exist_tlb.sail
@@ -0,0 +1,94 @@
+
+(* Minimal prelude *)
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord.
+ vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure extz
+
+val forall Num 'n, Num 'm, Num 'o, Num 'p, Order 'ord.
+ vector<'o, 'n, 'ord, bit> -> vector<'p, 'm, 'ord, bit> effect pure exts
+
+overload EXTZ [extz]
+overload EXTS [exts]
+
+val forall Num 'n, Num 'o, Order 'ord.
+ (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure add_vec
+
+overload (deinfix +) [add_vec]
+
+val bool -> bool effect pure bool_not
+overload ~ [bool_not]
+
+(* MIPS spec subset *)
+
+default Order dec
+
+register (bit[1]) CP0LLBit
+register (bit[64]) CP0LLAddr
+
+typedef MemAccessType = enumerate {Instruction; LoadData; StoreData}
+
+typedef regno = bit[5] (* a register number *)
+typedef imm16 = bit[16] (* 16-bit immediate *)
+
+typedef Exception = enumerate
+{
+ Int; TLBMod; TLBL; TLBS; AdEL; AdES; Sys; Bp; ResI; CpU; Ov; Tr; C2E; C2Trap;
+ XTLBRefillL; XTLBRefillS; XTLBInvL; XTLBInvS; MCheck
+}
+
+typedef WordType = enumerate {B; H; W; D}
+
+val bit[5] -> bit[64] effect {rreg} rGPR
+val (bit[64], WordType) -> bool effect pure isAddressAligned
+val forall Type 'o. (Exception, bit[64]) -> 'o effect pure SignalExceptionBadAddr
+
+val WordType -> exist 'r, 'r in {1,2,4,8}. [:'r:] effect pure wordWidthBytes
+
+function wordWidthBytes w = switch w {
+ case B -> 1
+ case H -> 2
+ case W -> 4
+ case D -> 8
+}
+
+val forall Nat 'n. (bit[64], [:'n:]) -> bit[8 * 'n] effect {rmem} MEMr_reserve_wrapper
+val forall Nat 'n. (bit[64], [:'n:]) -> bit[8 * 'n] effect {rmem} MEMr_wrapper
+val (bit[5], bit[64]) -> unit effect {wreg} wGPR
+
+function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) = addr
+
+function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = vAddr
+
+scattered typedef ast = const union
+
+val ast -> unit effect {rmem, rreg, wreg} execute
+
+scattered function unit execute
+
+union ast member (WordType, bool, bool, regno, regno, imm16) Load
+
+function clause execute (Load(width, signed, linked, base, rt, offset)) =
+ {
+ (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, width);
+ if ~ (isAddressAligned(vAddr, width)) then
+ (SignalExceptionBadAddr(AdEL, vAddr)) (* unaligned access *)
+ else
+ let pAddr = (TLBTranslate(vAddr, LoadData)) in
+ {
+ (exist 't, 't in {1,2,4,8}. bit[8 * 't]) memResult := if linked then
+ {
+ CP0LLBit := 0b1;
+ CP0LLAddr := pAddr;
+ MEMr_reserve_wrapper(pAddr, wordWidthBytes(width));
+ }
+ else
+ MEMr_wrapper(pAddr, wordWidthBytes(width));
+ if (signed) then
+ wGPR(rt) := EXTS(memResult)
+ else
+ wGPR(rt) := EXTZ(memResult)
+ }
+ }
+
+end ast
+end execute
diff --git a/test/typecheck/fail/return_simple1.sail b/test/typecheck/pass/return_simple4.sail
index 1bbc0e73..1bbc0e73 100644
--- a/test/typecheck/fail/return_simple1.sail
+++ b/test/typecheck/pass/return_simple4.sail
diff --git a/test/typecheck/pass/varity.sail b/test/typecheck/pass/varity.sail
new file mode 100644
index 00000000..d196f777
--- /dev/null
+++ b/test/typecheck/pass/varity.sail
@@ -0,0 +1,15 @@
+
+val int -> unit effect pure f1
+val (int, int) -> unit effect pure f2
+val (int, int, int) -> unit effect pure f3
+
+overload f [f1; f2; f3]
+
+val unit -> unit effect pure test
+
+function test () =
+{
+ f(1);
+ f(2, 3);
+ f(4, 5, 6);
+}
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 23:13:24 +0000