Fixing None and Some

src/sail_lean_backend/pretty_print_lean.ml

@@ -398,6 +398,11 @@ and doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
   | E_app (Id_aux (Id "internal_pick", _), _) ->
       (* TODO replace by actual implementation of internal_pick *)
       string "sorry"
+  | E_app (Id_aux (Id "None", _), _) -> string "none"
+  | E_app (Id_aux (Id "Some", _), args) ->
+      let d_id = string "some" in
+      let d_args = List.map d_of_arg args in
+      nest 2 (parens (flow (break 1) (d_id :: d_args)))
   | E_internal_plet (pat, e1, e2) ->
       let e0 = doc_pat pat in
       let e1_pp = doc_exp false ctx e1 in

test/lean/option.expected.lean

@@ -0,0 +1,19 @@
+import Out.Sail.Sail
+
+open Sail
+
+abbrev SailM := StateM Unit
+
+def match_option (x : (Option (BitVec 1))) : (BitVec 1) :=
+  match x with
+  | some x => x
+  | none => 0#1
+
+def option_match (x : (Option Unit)) (y : (BitVec 1)) : (Option (BitVec 1)) :=
+  match x with
+  | some () => (some y)
+  | none => none
+
+def initialize_registers (lit : Unit) : Unit :=
+  ()
+

test/lean/option.sail

@@ -0,0 +1,17 @@
+default Order dec
+
+$include <prelude.sail>
+
+function match_option(x : option(bit)) -> bit = {
+  match x {
+    Some(x) => x,
+    None() => bitzero,
+  }
+}
+
+function option_match(x : option(unit), y : bit) -> option(bit) = {
+    match x {
+        Some(()) => Some(y),
+        None() => None()
+    }
+}