More tests for implicit casts

The last test added in vectors.sail fails.

2 files changed, 18 insertions, 2 deletions

diff --git a/src/test/test3.sail b/src/test/test3.sail
index b07ffb7d..778d323a 100644
--- a/src/test/test3.sail
+++ b/src/test/test3.sail
@@ -1,5 +1,7 @@
 (* a register containing nat numbers *)
 register nat dummy_reg
+(* and one containing a byte *)
+register (bit[8]) dummy_reg2
 (* a function to read from memory; wmem serves no purpose currently,
    memory-writing functions are figured out syntactically. *)
 val extern nat -> nat effect { wmem , rmem }  MEM
@@ -54,6 +56,11 @@ function nat main _ = {
   ignore(MEM_SIZE(0,2));
 
   (* extern calls *)
-  ignore(3 + 39);
-  add(5, 37);
+  dummy_reg := 3 + 39;
+  dummy_reg := add(5, 37);
+  (* casts and external calls *)
+  dummy_reg := 0b01 + 0b01;
+  dummy_reg2 := dummy_reg;               (* cast from nat to bit[8] *)
+  dummy_reg2 := dummy_reg2 + dummy_reg2; (* cast to nat for add call *)
+  dummy_reg2;                            (* cast again and return 4 *)
 }
diff --git a/src/test/vectors.sail b/src/test/vectors.sail
index c7fd6d77..94132d25 100644
--- a/src/test/vectors.sail
+++ b/src/test/vectors.sail
@@ -5,6 +5,9 @@ register (bit[32]) i
 let (bit[10]) v3 = 0b0101010111
 register (bit[10]) slice_check
 register (bit[10]) slice_check_copy
+register nat result
+
+function forall Type 'a . 'a id ( x ) = x
 
 register nat match_success
 
@@ -21,6 +24,12 @@ function bit main _ = {
 
   gpr_small[1] := v3; (*Writes to slice_check*)
   slice_check_copy := gpr_small[1];
+  (* check that cast are still inserted for function calls *)
+  result := gpr_small[1] + gpr_small[1];
+  (* idem with type inference for return type *)
+  fresh_var := gpr_small[1] + gpr_small[1];
+  (* id function call - prevents the correct cast currently *)
+  result := gpr_small[1] + id(gpr_small[1]);
  
   i := [bitzero, bitzero, bitone, bitzero];