Type abbrevs to abbrev

rems-project · Jan 28, 2025 · cad2ca9 · cad2ca9
1 parent 65fe108
commit cad2ca9
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 8 deletions.
diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
@@ -529,9 +529,9 @@ let doc_typdef ctx (TD_aux (td, tannot) as full_typdef) =
       (* TODO don't ignore type quantifiers *)
       nest 2 (flow (break 1) [string "structure"; string id; string "where"] ^^ hardline ^^ enums_doc)
   | TD_abbrev (Id_aux (Id id, _), tq, A_aux (A_typ t, _)) ->
-      nest 2 (flow (break 1) [string "def"; string id; coloneq; doc_typ ctx 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, _)) ->
-      nest 2 (flow (break 1) [string "def"; string id; colon; string "Int"; coloneq; doc_nexp ctx ne])
+      nest 2 (flow (break 1) [string "abbrev"; string id; colon; string "Int"; coloneq; doc_nexp ctx ne])
   | _ -> failwith ("Type definition " ^ string_of_type_def_con full_typdef ^ " not translatable yet.")
 
 (* Copied from the Coq PP *)

diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean
@@ -2,7 +2,7 @@ import Out.Sail.Sail
 
 open Sail
 
-def cr_type := (BitVec 8)
+abbrev cr_type := (BitVec 8)
 
 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
 
-def reg_index := Nat
+abbrev reg_index := Nat
 
 inductive Register : Type where
   | R0
@@ -41,7 +41,7 @@ inductive Register : Type where
 open Register
 
 abbrev RegisterType : Register → Type
-  | .R0 => (BitVec 64)Reg
+  | .R0 => (BitVec 64)
   | .R1 => (BitVec 64)
   | .R2 => (BitVec 64)
   | .R3 => (BitVec 64)

diff --git a/test/lean/typedef.expected.lean b/test/lean/typedef.expected.lean
@@ -2,11 +2,11 @@ import Out.Sail.Sail
 
 open Sail
 
-def xlen : Int := 64
+abbrev xlen : Int := 64
 
-def xlen_bytes : Int := 8
+abbrev xlen_bytes : Int := 8
 
-def xlenbits := (BitVec 64)
+abbrev xlenbits := (BitVec 64)
 
 /-- Type quantifiers: k_n : Int, m : Int, m ≥ k_n -/
 def EXTZ {m : _} (v : (BitVec k_n)) : (BitVec m) :=