Lean: fix formatting and arguments for matches (#913)

rems-project · Jan 27, 2025 · 4e52b82 · 4e52b82
1 parent 49d5bed
commit 4e52b82
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 9 deletions.
diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean
@@ -38,6 +38,9 @@ def reg_deref (reg_ref : @RegisterRef Register RegisterType α) := readRegRef re
 
 end Regs
 
+/- TODO: Remove when #911 is merged -/
+abbrev SailM := StateM Unit
+
 namespace BitVec
 
 def length {w : Nat} (_ : BitVec w) : Nat := w

diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
@@ -306,7 +306,8 @@ let rec doc_pat (P_aux (p, (l, annot)) as pat) =
   | P_id id -> fixup_match_id id |> doc_id_ctor
   | P_tuple pats -> separate (string ", ") (List.map doc_pat pats) |> parens
   | P_list pats -> separate (string ", ") (List.map doc_pat pats) |> brackets
-  | P_app (cons, pats) -> doc_id_ctor cons ^^ space ^^ separate_map (string ", ") doc_pat pats
+  | P_app (Id_aux (Id "None", _), p) -> string "none"
+  | P_app (cons, pats) -> doc_id_ctor (fixup_match_id cons) ^^ space ^^ separate_map (string ", ") doc_pat pats
   | _ -> failwith ("Pattern " ^ string_of_pat_con pat ^ " " ^ string_of_pat pat ^ " not translatable yet.")
 
 (* Copied from the Coq PP *)
@@ -419,8 +420,8 @@ and doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
       wrap_with_pure as_monadic
         (braces (space ^^ doc_exp false ctx exp ^^ string " with " ^^ separate (comma ^^ space) args ^^ space))
   | E_match (discr, brs) ->
-      let cases = hardline ^^ separate_map hardline (fun br -> doc_match_clause ctx br) brs ^^ hardline in
-      string "match " ^^ doc_exp (effectful (effect_of discr)) ctx discr ^^ string " with" ^^ cases
+      let cases = separate_map hardline (fun br -> doc_match_clause ctx br) brs in
+      string "match " ^^ doc_exp (effectful (effect_of discr)) ctx discr ^^ string " with" ^^ hardline ^^ cases
   | E_assign ((LE_aux (le_act, tannot) as le), e) -> (
       match le_act with
       | LE_id id | LE_typ (_, id) -> string "writeReg " ^^ doc_id_ctor id ^^ space ^^ doc_exp false ctx e

diff --git a/test/lean/match.expected.lean b/test/lean/match.expected.lean
@@ -15,26 +15,22 @@ def match_enum (x : E) : (BitVec 1) :=
   | B => 1#1
   | C => 0#1
 
-
 def match_option (x : (Option (BitVec 1))) : (BitVec 1) :=
   match x with
-  | Some x => x
-  | None () => 0#1
-
+  | some x => x
+  | none => 0#1
 
 /-- Type quantifiers: y : Int, x : Int -/
 def match_pair_pat (x : Int) (y : Int) : Int :=
   match (x, y) with
   | (a, b) => (HAdd.hAdd a b)
 
-
 /-- Type quantifiers: arg1 : Int, arg0 : Int -/
 def match_pair (arg0 : Int) (arg1 : Int) : Int :=
   let x := (arg0, arg1)
   match x with
   | (a, b) => (HAdd.hAdd a b)
 
-
 def initialize_registers : Unit :=
   ()