Lean: implement struct patterns

src/sail_lean_backend/pretty_print_lean.ml

@@ -434,6 +434,9 @@ let rec doc_pat ?(in_vector = false) (P_aux (p, (l, annot)) as pat) =
   | P_app (cons, pats) -> doc_id_ctor (fixup_match_id cons) ^^ space ^^ separate_map (string ", ") doc_pat pats
   | P_var (p, _) -> doc_pat p
   | P_as (pat, id) -> doc_pat pat
+  | P_struct (pats, _) ->
+      let pats = List.map (fun (id, pat) -> separate space [doc_id_ctor id; coloneq; doc_pat pat]) pats in
+      braces (space ^^ separate (comma ^^ space) pats ^^ space)
   | _ -> failwith ("Doc Pattern " ^ string_of_pat_con pat ^ " " ^ string_of_pat pat ^ " not translatable yet.")
 
 (* Copied from the Coq PP *)

test/lean/struct.expected.lean

@@ -119,6 +119,14 @@ def mk_struct (i : Int) (b : (BitVec 1)) : My_struct :=
 def undef_struct (x : (BitVec 1)) : SailM My_struct := do
   ((undefined_My_struct ()) : SailM My_struct)
 
+def match_struct (value : My_struct) : SailM Int := do
+  match value with
+  | { field2 := 0#1, field1 := g__0 } => (pure 0)
+  | { field1 := field1, field2 := 1#1 } => (pure field1)
+  | _ =>
+    assert false "Pattern match failure at struct.sail:39.4-42.5"
+    throw Error.Exit
+
 def initialize_registers (_ : Unit) : Unit :=
   ()
 

test/lean/struct.sail

@@ -35,6 +35,13 @@ function undef_struct (x) = {
   (undefined_My_struct(): My_struct)
 }
 
+function match_struct(value : My_struct) -> int = {
+    match value {
+        struct { _, field2 = bitzero } => 0,
+        struct { field1, field2 = bitone } => field1
+    }
+}
+
 struct Mem_write_request('n : Int, 'vasize : Int, 'pa : Type, 'ts : Type,
                          'arch_ak : Type), 'n > 0 & 'vasize >= 0 = {
   va : option(bits('vasize)),