summaryrefslogtreecommitdiff
path: root/src/test/test3.sail
diff options
context:
space:
mode:
authorKathy Gray2014-02-15 16:01:33 +0000
committerKathy Gray2014-02-15 16:05:20 +0000
commitbe133edd6eef4a775085df4aa658670d8737b315 (patch)
tree1ddbbde5bb4e045134028fe6730e8a521f7585c8 /src/test/test3.sail
parent6be9047cff82cdbb1c52135e80b373c9c44d36f2 (diff)
Full type checker. No constraint checking in place.
Diffstat (limited to 'src/test/test3.sail')
-rw-r--r--src/test/test3.sail9
1 files changed, 4 insertions, 5 deletions
diff --git a/src/test/test3.sail b/src/test/test3.sail
index 0ffab6ae..ed30d243 100644
--- a/src/test/test3.sail
+++ b/src/test/test3.sail
@@ -2,11 +2,10 @@
register nat dummy_reg
(* a function to read from memory; wmem serves no purpose currently,
memory-writing functions are figured out syntactically. *)
-val nat -> nat effect { wmem , rmem } MEM
-val nat -> nat effect { wmem , rmem } MEM_GPU
-val ( nat * nat ) -> (bit[8]) effect { wmem , rmem } MEM_SIZE
-
-val nat -> (bit[8]) effect { wmem , rmem } MEM_WORD
+val extern nat -> nat effect { wmem , rmem } MEM
+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 *)
val extern forall Type 'a . 'a -> nat effect pure to_num_inc = "to_num_inc"