omit type abbreviations

rems-project · Feb 12, 2025 · 67d4ad3 · 67d4ad3
1 parent 6c0caba
commit 67d4ad3
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 5 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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)
+
Original file line number	Diff line number	Diff line change
Expand Up		@@ -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)