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;