diff options
| author | Kathy Gray | 2014-03-27 14:20:51 +0000 |
|---|---|---|
| committer | Kathy Gray | 2014-03-27 14:20:51 +0000 |
| commit | 70d8fd00c326f928bf0300b006b2c3a79d09cd10 (patch) | |
| tree | f781fee882027302bd3368ddd33e13826769b310 /src/test/test3.sail | |
| parent | 9549b13972f5c3173bc7d11ea1b62b490f673166 (diff) | |
Check simple constraints (i.e. ones using only constants).
Changes syntax of tuple type from * to , so that nexps of the form 8 * 'n can be supported in the parser, which was apparently not true before.
Diffstat (limited to 'src/test/test3.sail')
| -rw-r--r-- | src/test/test3.sail | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/test/test3.sail b/src/test/test3.sail index 778d323a..78d60513 100644 --- a/src/test/test3.sail +++ b/src/test/test3.sail @@ -6,7 +6,7 @@ register (bit[8]) dummy_reg2 memory-writing functions are figured out syntactically. *) 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 forall Nat 'n . ( nat, [|'n|] ) -> (bit['n * 8]) effect { wmem , rmem } MEM_SIZE val extern nat -> (bit[8]) effect { wmem , rmem } MEM_WORD (* XXX types are wrong *) @@ -18,8 +18,8 @@ val extern forall Type 'a . nat -> 'a effect pure to_vec_dec = "to_vec_dec" function unit ignore(x) = () (* extern functions *) -val extern ( nat * nat ) -> nat effect pure add = "add" -val extern ( nat * nat ) -> nat effect pure (deinfix + ) = "add" (* infix plus *) +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 |