reset earlier commits to test3, that were supposed to be chosen instead of my changes in the conflict resolution but oops.

1 files changed, 10 insertions, 9 deletions

diff --git a/src/test/test3.sail b/src/test/test3.sail
index ac0c1674..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
@@ -7,7 +9,7 @@ val extern nat -> nat effect { wmem , rmem }  MEM_GPU
 val extern ( nat * nat ) -> (bit[8]) effect { wmem , rmem }  MEM_SIZE
 val extern nat -> (bit[8]) effect { wmem , rmem }  MEM_WORD
 
-(*(* XXX types are wrong *)
+(* XXX types are wrong *)
 val extern forall Type 'a . 'a -> nat effect pure to_num_inc = "to_num_inc"
 val extern forall Type 'a . 'a -> nat effect pure to_num_dec = "to_num_dec"
 val extern forall Type 'a . nat -> 'a effect pure to_vec_inc = "to_vec_inc"
@@ -19,15 +21,9 @@ function unit ignore(x) = ()
 val extern ( nat * nat ) -> nat effect pure add = "add"
 val extern ( nat * nat ) -> nat effect pure (deinfix + ) = "add"   (* infix plus *)
 
-function nat (deinfix * ) ( (nat) x, (nat) y ) = 42*)
-
-function unit ignore(x) = ()
 function nat (deinfix * ) ( (nat) x, (nat) y ) = 42
 
-function forall Type 'a . 'a ident x = x
-
 function nat main _ = {
-  ignore(0b1+ident(0b0));
   (* left-hand side function call = memory write *)
   MEM(0) := 0;
   (* memory read, thanks to effect { rmem} above *)
@@ -60,6 +56,11 @@ function nat main _ = {
   ignore(MEM_SIZE(0,2));
 
   (* extern calls *)
-  ignore(3 + 39);
-  (deinfix +)(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 *)
 }