Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Lean: add support for register definitions #894

Merged
merged 24 commits into from
Jan 27, 2025
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
fixing lean arrows
lfrenot committed Jan 22, 2025
commit 5e1c0181e549f671a5a68c07bf7aa9ab3def1472
8 changes: 4 additions & 4 deletions src/sail_lean_backend/Sail/Sail.lean
Original file line number Diff line number Diff line change
@@ -10,16 +10,16 @@ structure SequentialSate ( Regs : Type ) where

abbrev PreSailM ( Regs: Type ) := EStateM Error (SequentialSate Regs)

structure RegisterRef (Register : Type -> Type) (T : Type) where
structure RegisterRef (Register : Type Type) (T : Type) where
reg : Register T

def read_reg {Register : Type -> Type} (register_lookup : ∀ T, Register T -> Regstate -> T) (reg : Register S) : PreSailM Regstate S := do
def read_reg {Register : Type Type} (register_lookup : ∀ T, Register T Regstate T) (reg : Register T) : PreSailM Regstate T := do
let r ← get
return register_lookup _ reg r.regs

def write_reg {Register : Type -> Type} (register_set : ∀ T, Register T -> T -> Regstate -> Regstate) (reg : Register S) (s : S) : PreSailM Regstate Unit := do
def write_reg {Register : Type Type} (register_set : ∀ T, Register T T Regstate Regstate) (reg : Register T) (t : T) : PreSailM Regstate Unit := do
let r ← get
set { r with regs := register_set _ reg s r.regs }
set { r with regs := register_set _ reg t r.regs }
return ()

def reg_deref {Register : Type → Type} (read_reg : ∀ T, Register T → PreSailM Regstate T) (reg_ref : RegisterRef Register T) : PreSailM Regstate T := do
14 changes: 7 additions & 7 deletions src/sail_lean_backend/pretty_print_lean.ml
Original file line number Diff line number Diff line change
@@ -585,14 +585,14 @@ let type_enum ctxt env type_map =
| _ ->
separate hardline
[
string "inductive Register : Type -> Type where";
string "inductive Register : Type Type where";
separate_map hardline
(fun (typ_id, typ) ->
string " | "
^^ doc_id_ctor (reg_case_name typ_id)
^^ space ^^ colon ^^ space
^^ doc_id_ctor (reg_type_name typ_id)
^^ string " -> Register " ^^ doc_typ ctxt typ
^^ string " Register " ^^ doc_typ ctxt typ
)
type_map;
empty;
@@ -623,7 +623,7 @@ let regstate ctxt env type_map =
^^ doc_id_ctor (state_field_name typ_id)
^^ string " : "
^^ doc_id_ctor (reg_type_name typ_id)
^^ string " -> " ^^ doc_typ ctxt typ
^^ string " " ^^ doc_typ ctxt typ
)
type_map;
string "";
@@ -643,7 +643,7 @@ let reg_accessors ctxt env type_map =
separate hardline
[
string "def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg";
string "def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()";
string "def register_set {T : Type} (_ : Register T) : T Regstate Regstate := fun _ _ => ()";
]
| _ ->
separate hardline
@@ -660,7 +660,7 @@ let reg_accessors ctxt env type_map =
)
type_map;
empty;
string "def register_set {T : Type} (reg : Register T) : T -> Regstate -> Regstate :=";
string "def register_set {T : Type} (reg : Register T) : T Regstate Regstate :=";
string " match reg with";
separate_map hardline
(fun (typ_id, _typ) ->
@@ -698,8 +698,8 @@ let doc_reg_info env registers =
regstate bare_ctxt env type_map;
reg_accessors bare_ctxt env type_map;
string "abbrev SailM := PreSailM Regstate";
string "def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup";
string "def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set";
string "def read_reg {T : Type} : Register T SailM T := @Sail.read_reg _ T _ @register_lookup";
string "def write_reg {T : Type} : Register T T SailM Unit := @Sail.write_reg _ T _ @register_set";
string "def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg";
(* string

6 changes: 3 additions & 3 deletions test/lean/bitfield.expected.lean
Original file line number Diff line number Diff line change
@@ -8,10 +8,10 @@ def cr_type := (BitVec 8)
def Register (T : Type) := T
abbrev Regstate := Unit
def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
def register_set {T : Type} (_ : Register T) : T Regstate Regstate := fun _ _ => ()
abbrev SailM := PreSailM Regstate
def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
def read_reg {T : Type} : Register T SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T T SailM Unit := @Sail.write_reg _ T _ @register_set
def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg

def undefined_cr_type (lit : Unit) : SailM (BitVec 8) := do
6 changes: 3 additions & 3 deletions test/lean/bitvec_operation.expected.lean
Original file line number Diff line number Diff line change
@@ -6,10 +6,10 @@ open Sail
def Register (T : Type) := T
abbrev Regstate := Unit
def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
def register_set {T : Type} (_ : Register T) : T Regstate Regstate := fun _ _ => ()
abbrev SailM := PreSailM Regstate
def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
def read_reg {T : Type} : Register T SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T T SailM Unit := @Sail.write_reg _ T _ @register_set
def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg

def bitvector_eq (x : (BitVec 16)) (y : (BitVec 16)) : Bool :=
6 changes: 3 additions & 3 deletions test/lean/enum.expected.lean
Original file line number Diff line number Diff line change
@@ -9,10 +9,10 @@ inductive E where | A | B | C
def Register (T : Type) := T
abbrev Regstate := Unit
def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
def register_set {T : Type} (_ : Register T) : T Regstate Regstate := fun _ _ => ()
abbrev SailM := PreSailM Regstate
def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
def read_reg {T : Type} : Register T SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T T SailM Unit := @Sail.write_reg _ T _ @register_set
def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg

def undefined_E : SailM E := do
6 changes: 3 additions & 3 deletions test/lean/extern.expected.lean
Original file line number Diff line number Diff line change
@@ -6,10 +6,10 @@ open Sail
def Register (T : Type) := T
abbrev Regstate := Unit
def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
def register_set {T : Type} (_ : Register T) : T Regstate Regstate := fun _ _ => ()
abbrev SailM := PreSailM Regstate
def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
def read_reg {T : Type} : Register T SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T T SailM Unit := @Sail.write_reg _ T _ @register_set
def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg

def extern_add : Int :=
6 changes: 3 additions & 3 deletions test/lean/extern_bitvec.expected.lean
Original file line number Diff line number Diff line change
@@ -6,10 +6,10 @@ open Sail
def Register (T : Type) := T
abbrev Regstate := Unit
def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
def register_set {T : Type} (_ : Register T) : T Regstate Regstate := fun _ _ => ()
abbrev SailM := PreSailM Regstate
def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
def read_reg {T : Type} : Register T SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T T SailM Unit := @Sail.write_reg _ T _ @register_set
def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg

def extern_const : (BitVec 64) :=
6 changes: 3 additions & 3 deletions test/lean/let.expected.lean
Original file line number Diff line number Diff line change
@@ -6,10 +6,10 @@ open Sail
def Register (T : Type) := T
abbrev Regstate := Unit
def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
def register_set {T : Type} (_ : Register T) : T Regstate Regstate := fun _ _ => ()
abbrev SailM := PreSailM Regstate
def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
def read_reg {T : Type} : Register T SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T T SailM Unit := @Sail.write_reg _ T _ @register_set
def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg

def foo : (BitVec 16) :=
6 changes: 3 additions & 3 deletions test/lean/range.expected.lean
Original file line number Diff line number Diff line change
@@ -6,10 +6,10 @@ open Sail
def Register (T : Type) := T
abbrev Regstate := Unit
def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
def register_set {T : Type} (_ : Register T) : T Regstate Regstate := fun _ _ => ()
abbrev SailM := PreSailM Regstate
def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
def read_reg {T : Type} : Register T SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T T SailM Unit := @Sail.write_reg _ T _ @register_set
def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg

/-- Type quantifiers: x : Int, 0 ≤ x ∧ x ≤ 31 -/
28 changes: 14 additions & 14 deletions test/lean/registers.expected.lean
Original file line number Diff line number Diff line change
@@ -29,12 +29,12 @@ deriving DecidableEq
open register_nat


inductive Register : Type -> Type where
| R_bit : register_bit -> Register (BitVec 1)
| R_bitvector_64 : register_bitvector_64 -> Register (BitVec 64)
| R_bool : register_bool -> Register Bool
| R_int : register_int -> Register Int
| R_nat : register_nat -> Register Nat
inductive Register : Type Type where
| R_bit : register_bit Register (BitVec 1)
| R_bitvector_64 : register_bitvector_64 Register (BitVec 64)
| R_bool : register_bool Register Bool
| R_int : register_int Register Int
| R_nat : register_nat Register Nat

instance : Coe register_bit (Register (BitVec 1)) where
coe r := Register.R_bit r
@@ -48,11 +48,11 @@ instance : Coe register_nat (Register Nat) where
coe r := Register.R_nat r

structure Regstate where
bit_s : register_bit -> (BitVec 1)
bitvector_64_s : register_bitvector_64 -> (BitVec 64)
bool_s : register_bool -> Bool
int_s : register_int -> Int
nat_s : register_nat -> Nat
bit_s : register_bit (BitVec 1)
bitvector_64_s : register_bitvector_64 (BitVec 64)
bool_s : register_bool Bool
int_s : register_int Int
nat_s : register_nat Nat


def register_lookup {T : Type} (reg : Register T) (rs : Regstate) : T :=
@@ -63,7 +63,7 @@ def register_lookup {T : Type} (reg : Register T) (rs : Regstate) : T :=
| Register.R_int r => rs.int_s r
| Register.R_nat r => rs.nat_s r

def register_set {T : Type} (reg : Register T) : T -> Regstate -> Regstate :=
def register_set {T : Type} (reg : Register T) : T Regstate Regstate :=
match reg with
| Register.R_bit r => fun v rs => { rs with bit_s := fun r' => if r' = r then v else rs.bit_s r' }
| Register.R_bitvector_64 r => fun v rs => { rs with bitvector_64_s := fun r' => if r' = r then v else rs.bitvector_64_s r' }
@@ -73,8 +73,8 @@ def register_set {T : Type} (reg : Register T) : T -> Regstate -> Regstate :=


abbrev SailM := PreSailM Regstate
def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
def read_reg {T : Type} : Register T SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T T SailM Unit := @Sail.write_reg _ T _ @register_set
def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg

def initialize_registers : SailM Unit := do
6 changes: 3 additions & 3 deletions test/lean/struct.expected.lean
Original file line number Diff line number Diff line change
@@ -10,10 +10,10 @@ structure My_struct where
def Register (T : Type) := T
abbrev Regstate := Unit
def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
def register_set {T : Type} (_ : Register T) : T Regstate Regstate := fun _ _ => ()
abbrev SailM := PreSailM Regstate
def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
def read_reg {T : Type} : Register T SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T T SailM Unit := @Sail.write_reg _ T _ @register_set
def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg

def undefined_My_struct (lit : Unit) : SailM My_struct := do
6 changes: 3 additions & 3 deletions test/lean/trivial.expected.lean
Original file line number Diff line number Diff line change
@@ -6,10 +6,10 @@ open Sail
def Register (T : Type) := T
abbrev Regstate := Unit
def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
def register_set {T : Type} (_ : Register T) : T Regstate Regstate := fun _ _ => ()
abbrev SailM := PreSailM Regstate
def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
def read_reg {T : Type} : Register T SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T T SailM Unit := @Sail.write_reg _ T _ @register_set
def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg

def foo (y : Unit) : Unit :=
6 changes: 3 additions & 3 deletions test/lean/tuples.expected.lean
Original file line number Diff line number Diff line change
@@ -6,10 +6,10 @@ open Sail
def Register (T : Type) := T
abbrev Regstate := Unit
def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
def register_set {T : Type} (_ : Register T) : T Regstate Regstate := fun _ _ => ()
abbrev SailM := PreSailM Regstate
def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
def read_reg {T : Type} : Register T SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T T SailM Unit := @Sail.write_reg _ T _ @register_set
def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg

def tuple1 : (Int × Int × ((BitVec 2) × Unit)) :=
6 changes: 3 additions & 3 deletions test/lean/typedef.expected.lean
Original file line number Diff line number Diff line change
@@ -12,10 +12,10 @@ def xlenbits := (BitVec 64)
def Register (T : Type) := T
abbrev Regstate := Unit
def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
def register_set {T : Type} (_ : Register T) : T Regstate Regstate := fun _ _ => ()
abbrev SailM := PreSailM Regstate
def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
def read_reg {T : Type} : Register T SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T T SailM Unit := @Sail.write_reg _ T _ @register_set
def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg

/-- Type quantifiers: k_n : Int, m : Int, m ≥ k_n -/
6 changes: 3 additions & 3 deletions test/lean/typquant.expected.lean
Original file line number Diff line number Diff line change
@@ -6,10 +6,10 @@ open Sail
def Register (T : Type) := T
abbrev Regstate := Unit
def register_lookup {T : Type} (reg : Register T) (_ : Regstate) : T := reg
def register_set {T : Type} (_ : Register T) : T -> Regstate -> Regstate := fun _ _ => ()
def register_set {T : Type} (_ : Register T) : T Regstate Regstate := fun _ _ => ()
abbrev SailM := PreSailM Regstate
def read_reg {T : Type} : Register T -> SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T -> T -> SailM Unit := @Sail.write_reg _ T _ @register_set
def read_reg {T : Type} : Register T SailM T := @Sail.read_reg _ T _ @register_lookup
def write_reg {T : Type} : Register T T SailM Unit := @Sail.write_reg _ T _ @register_set
def reg_deref {T : Type} : RegisterRef Register T → SailM T := @Sail.reg_deref _ T _ @read_reg

/-- Type quantifiers: n : Int -/