diff options
| author | Kathy Gray | 2014-02-15 16:01:33 +0000 |
|---|---|---|
| committer | Kathy Gray | 2014-02-15 16:05:20 +0000 |
| commit | be133edd6eef4a775085df4aa658670d8737b315 (patch) | |
| tree | 1ddbbde5bb4e045134028fe6730e8a521f7585c8 /src/test | |
| parent | 6be9047cff82cdbb1c52135e80b373c9c44d36f2 (diff) | |
Full type checker. No constraint checking in place.
Diffstat (limited to 'src/test')
| -rw-r--r-- | src/test/pattern.sail | 2 | ||||
| -rw-r--r-- | src/test/test3.sail | 9 |
2 files changed, 5 insertions, 6 deletions
diff --git a/src/test/pattern.sail b/src/test/pattern.sail index 8cdc7a3c..bc04590d 100644 --- a/src/test/pattern.sail +++ b/src/test/pattern.sail @@ -11,7 +11,7 @@ function nat main _ = { (switch n { case 0 -> { x := 21; x } case 1 -> { x := 42; x } - case x -> { x := 99; x } + case z -> { x := 99; x } }); (* doesn't work - main returns 1 instead of 99 *) 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" |