Lean: derive Inhabited for structs (#950)

This closes #949
rems-project · Feb 4, 2025 · ba1ae75 · ba1ae75
1 parent a5dbda8
commit ba1ae75
Show file tree

Hide file tree

Showing 6 changed files with 21 additions and 9 deletions.
diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
@@ -571,22 +571,27 @@ let string_of_type_def_con (TD_aux (td, _)) =
 let doc_typdef ctx (TD_aux (td, tannot) as full_typdef) =
   match td with
   | TD_enum (Id_aux (Id id, _), fields, _) ->
-      let derivers = if List.length fields > 0 then [string "Inhabited"] else [] in
       let fields = List.map doc_id_ctor fields in
       let fields = List.map (fun i -> space ^^ pipe ^^ space ^^ i) fields in
+      let derivers =
+        if List.length fields == 0 then [string "DecidableEq"] else [string "Inhabited"; string "DecidableEq"]
+      in
       let enums_doc = concat fields in
       nest 2
         (flow (break 1) [string "inductive"; string id; string "where"]
-        ^^ enums_doc ^^ hardline ^^ string "deriving" ^^ space
-        ^^ separate (comma ^^ space) derivers
+        ^^ enums_doc ^^ hardline ^^ string "deriving" ^^ space ^^ separate comma_sp derivers
         )
-      ^^ hardline ^^ string "open " ^^ string id
+      ^^ hardline ^^ hardline ^^ string "open " ^^ string id
   | TD_record (Id_aux (Id id, _), TypQ_aux (tq, _), fields, _) ->
       let fields = List.map (doc_typ_id ctx) fields in
-      let enums_doc = separate hardline fields in
+      let fields_doc = separate hardline fields in
       let rectyp = doc_typ_quant ctx tq in
       (* TODO don't ignore type quantifiers *)
-      nest 2 (flow (break 1) [string "structure"; string id; string "where"] ^^ hardline ^^ enums_doc)
+      nest 2
+        (flow (break 1) [string "structure"; string id; string "where"]
+        ^^ hardline ^^ fields_doc ^^ hardline ^^ string "deriving" ^^ space
+        ^^ nest 2 (flow comma_sp [string "Inhabited"; string "DecidableEq"])
+        )
   | TD_abbrev (Id_aux (Id id, _), tq, A_aux (A_typ t, _)) ->
       nest 2 (flow (break 1) [string "abbrev"; string id; coloneq; doc_typ ctx t])
   | TD_abbrev (Id_aux (Id id, _), tq, A_aux (A_nexp ne, _)) ->

diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean
@@ -3,7 +3,8 @@ import Out.Sail.Sail
 open Sail
 
 inductive E where | A | B | C
-  deriving Inhabited
+  deriving Inhabited, DecidableEq
+
 open E
 
 abbrev SailM := StateM Unit

diff --git a/test/lean/match.expected.lean b/test/lean/match.expected.lean
@@ -3,7 +3,8 @@ import Out.Sail.Sail
 open Sail
 
 inductive E where | A | B | C
-  deriving Inhabited
+  deriving Inhabited, DecidableEq
+
 open E
 
 inductive Register : Type where

diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean
@@ -5,6 +5,7 @@ open Sail
 structure My_struct where
   field1 : Int
   field2 : (BitVec 1)
+  deriving Inhabited, DecidableEq
 
 abbrev SailM := StateM Unit
 

diff --git a/test/lean/struct_of_enum.expected.lean b/test/lean/struct_of_enum.expected.lean
@@ -3,11 +3,13 @@ import Out.Sail.Sail
 open Sail
 
 inductive e_test where | VAL
-  deriving Inhabited
+  deriving Inhabited, DecidableEq
+
 open e_test
 
 structure s_test where
   f : e_test
+  deriving Inhabited, DecidableEq
 
 abbrev SailM := StateM Unit
 

diff --git a/test/lean/union.expected.lean b/test/lean/union.expected.lean
@@ -5,9 +5,11 @@ open Sail
 structure rectangle where
   width : Int
   height : Int
+  deriving Inhabited, DecidableEq
 
 structure circle where
   radius : Int
+  deriving Inhabited, DecidableEq
 
 inductive shape where
   | Rectangle (_ : rectangle)