summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-03-13 17:32:58 +0000
committerAlasdair Armstrong2018-03-13 17:37:12 +0000
commitf063a1e71d90368c04cf1f8eb2ba36cd16592e01 (patch)
tree2e79ad03a62a85a7c7427da099452a59bf0b88ba /test
parent0da6c4482f2a68d8cde54c5261be6d715d5ce63c (diff)
Polymorphic option types now compile to C
Fixed an issue whereby an option constructor that was never constructed, but only matched on, would cause compilation to fail. Temporarily fixed an issue where union types that can be entirely stack-allocated were not being treated as such, by simply heap-allocating all unions. Need to adapt the code generator to handle this case properly. Fixed a further small issue whereby multiple union types would confuse the type specialisation pass. Added a test case for compiling option types. RISCV now generates C code, but there are still some bugs that need to be squashed before it compile and work.
Diffstat (limited to 'test')
-rw-r--r--test/c/option.expect3
-rw-r--r--test/c/option.sail40
-rw-r--r--test/c/sail.h4
3 files changed, 47 insertions, 0 deletions
diff --git a/test/c/option.expect b/test/c/option.expect
new file mode 100644
index 00000000..f099c714
--- /dev/null
+++ b/test/c/option.expect
@@ -0,0 +1,3 @@
+a = 5
+b = 0xF
+c = 0xA
diff --git a/test/c/option.sail b/test/c/option.sail
new file mode 100644
index 00000000..1ca59372
--- /dev/null
+++ b/test/c/option.sail
@@ -0,0 +1,40 @@
+default Order dec
+
+val print = "print_endline" : string -> unit
+
+val "print_int" : (string, int) -> unit
+val "print_bits" : forall 'n. (string, vector('n, dec, bit)) -> unit
+
+union option ('a : Type) = {
+ None : unit,
+ Some : 'a
+}
+
+union soption ('a : Type) = {
+ sNone : unit,
+ sSome : 'a
+}
+
+val main : unit -> unit
+
+function main () = {
+ let x : option(int) = Some(5);
+ let y : option(int) = None();
+ let z : option(vector(4, dec, bit)) = Some(0xF);
+
+ match x {
+ Some(a) => print_int("a = ", 5),
+ None() => print("None")
+ };
+
+ match z {
+ Some(b) => print_bits("b = ", b),
+ None() => print("None")
+ };
+
+ let q : soption(vector(4, dec, bit)) = sSome(0xA);
+
+ match q {
+ sSome(c) => print_bits("c = ", c)
+ }
+}
diff --git a/test/c/sail.h b/test/c/sail.h
index b29e9535..c0f2674b 100644
--- a/test/c/sail.h
+++ b/test/c/sail.h
@@ -12,6 +12,10 @@ typedef int unit;
#define UNIT 0
+unit undefined_unit(const unit u) {
+ return UNIT;
+}
+
typedef struct {
mp_bitcnt_t len;
mpz_t *bits;