From 67d4ad39c9361d9ebdfc2acb14901beb78fe8bb0 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Wed, 12 Feb 2025 12:14:33 +0000
Subject: [PATCH] omit type abbreviations

---
 src/sail_lean_backend/pretty_print_lean.ml | 3 +--
 test/lean/bitfield.expected.lean           | 2 +-
 test/lean/register_vector.expected.lean    | 2 +-
 test/lean/typedef.expected.lean            | 4 +++-
 test/lean/typedef.sail                     | 2 ++
 5 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
index 4491de58d..fc11c4465 100644
--- a/src/sail_lean_backend/pretty_print_lean.ml
+++ b/src/sail_lean_backend/pretty_print_lean.ml
@@ -618,8 +618,7 @@ let doc_typdef ctx (TD_aux (td, tannot) as full_typdef) =
         | _ -> [string "structure"; string id; separate space rectyp; string "where"]
       in
       doc_typ_quant_in_comment ctx tq ^^ hardline ^^ nest 2 (flow (break 1) decl_start ^^ hardline ^^ fields_doc)
-  | 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, tq, A_aux (A_typ t, _)) -> string "/- Type abbreviation omitted: " ^^ doc_id_ctor id ^^ string " -/"
   | TD_abbrev (Id_aux (Id id, _), tq, A_aux (A_nexp ne, _)) ->
       nest 2 (flow (break 1) [string "abbrev"; string id; colon; string "Int"; coloneq; doc_nexp ctx ne])
   | TD_variant (Id_aux (Id id, _), tq, ar, _) ->
diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean
index b9d8ea7ec..834676448 100644
--- a/test/lean/bitfield.expected.lean
+++ b/test/lean/bitfield.expected.lean
@@ -2,7 +2,7 @@ import Out.Sail.Sail
 
 open Sail
 
-abbrev cr_type := (BitVec 8)
+/- Type abbreviation omitted: cr_type -/
 
 inductive Register : Type where
   | R
diff --git a/test/lean/register_vector.expected.lean b/test/lean/register_vector.expected.lean
index b23b8b842..d8859c14a 100644
--- a/test/lean/register_vector.expected.lean
+++ b/test/lean/register_vector.expected.lean
@@ -2,7 +2,7 @@ import Out.Sail.Sail
 
 open Sail
 
-abbrev reg_index := Nat
+/- Type abbreviation omitted: reg_index -/
 
 inductive Register : Type where
   | R0
diff --git a/test/lean/typedef.expected.lean b/test/lean/typedef.expected.lean
index 0ad927948..9356b72e8 100644
--- a/test/lean/typedef.expected.lean
+++ b/test/lean/typedef.expected.lean
@@ -6,7 +6,9 @@ abbrev xlen : Int := 64
 
 abbrev xlen_bytes : Int := 8
 
-abbrev xlenbits := (BitVec 64)
+/- Type abbreviation omitted: xlenbits -/
+
+/- Type abbreviation omitted: bits2 -/
 
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
diff --git a/test/lean/typedef.sail b/test/lean/typedef.sail
index dcc805d94..279cc8a41 100644
--- a/test/lean/typedef.sail
+++ b/test/lean/typedef.sail
@@ -11,3 +11,5 @@ function EXTZ(m, v) = sail_zero_extend(v, m)
 val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
 function EXTS(m, v) = sail_sign_extend(v, m)
 
+type bits2('n) = bitvector('n)
+