Lean: translate type parameters of record types (#951)

This fixes part of #939 as the type Mem_write_request is now well defined.

A follow up PR will add type annotations to the let bindings to instantiate these parameters.

src/sail_lean_backend/pretty_print_lean.ml

@@ -238,14 +238,31 @@ let rec captured_typ_var ((i, Typ_aux (t, _)) as typ) =
 
 let doc_typ_id ctx (typ, fid) = flow (break 1) [doc_id_ctor fid; colon; doc_typ ctx typ]
 
-let doc_kind (K_aux (k, _)) = match k with K_int -> string "Int" | K_bool -> string "Bool" | K_type -> string "Type"
+let doc_kind ctx (kid : kid) (K_aux (k, _)) =
+  match k with
+  | K_int -> if provably_nneg ctx (Nexp_aux (Nexp_var kid, Unknown)) then string "Nat" else string "Int"
+  | K_bool -> string "Bool"
+  | K_type -> string "Type"
 
-let doc_quant_item ctx (QI_aux (qi, _)) =
+let doc_quant_item_all ctx (QI_aux (qi, _)) =
   match qi with
-  | QI_id (KOpt_aux (KOpt_kind (k, ki), _)) -> flow (break 1) [doc_kid ctx ki; colon; doc_kind k]
+  | QI_id (KOpt_aux (KOpt_kind (k, ki), _)) -> flow (break 1) [doc_kid ctx ki; colon; doc_kind ctx ki k]
   | QI_constraint c -> doc_nconstraint ctx c
 
-let doc_typ_quant ctx tq = match tq with TypQ_tq qs -> List.map (doc_quant_item ctx) qs | TypQ_no_forall -> []
+(* Used to annotate types with the original constraints *)
+let doc_typ_quant_all ctx tq = match tq with TypQ_tq qs -> List.map (doc_quant_item_all ctx) qs | TypQ_no_forall -> []
+
+let doc_quant_item_relevant ctx (QI_aux (qi, annot)) =
+  match qi with
+  | QI_id (KOpt_aux (KOpt_kind (k, ki), _)) -> Some (flow (break 1) [doc_kid ctx ki; colon; doc_kind ctx ki k])
+  | QI_constraint c -> None
+
+(* Used to translate type parameters of types, so we drop the constraints *)
+let doc_typ_quant_relevant ctx (TypQ_aux (tq, _) as tq_full) =
+  (* We go through the type variables with an environment that contains all the constraints,
+     in order to detect when we can translate the Kind as Nat *)
+  let ctx = initial_context (Type_check.Env.add_typquant Unknown tq_full ctx.env) ctx.global in
+  match tq with TypQ_tq qs -> List.filter_map (doc_quant_item_relevant ctx) qs | TypQ_no_forall -> []
 
 let lean_escape_string s = Str.global_replace (Str.regexp "\"") "\"\"" s
 
@@ -520,7 +537,7 @@ let doc_funcl_init global (FCL_aux (FCL_funcl (id, pexp), annot)) =
       )
       (ctx, []) binders
   in
-  let typ_quants = doc_typ_quant ctx tq in
+  let typ_quants = doc_typ_quant_all ctx tq in
   let typ_quant_comment =
     if List.length typ_quants > 0 then
       string "/-- Type quantifiers: " ^^ nest 2 (flow comma_sp typ_quants) ^^ string " -/" ^^ hardline
@@ -582,16 +599,16 @@ let doc_typdef ctx (TD_aux (td, tannot) as full_typdef) =
         ^^ enums_doc ^^ hardline ^^ string "deriving" ^^ space ^^ separate comma_sp derivers
         )
       ^^ hardline ^^ hardline ^^ string "open " ^^ string id
-  | TD_record (Id_aux (Id id, _), TypQ_aux (tq, _), fields, _) ->
+  | TD_record (Id_aux (Id id, _), tq, fields, _) ->
       let fields = List.map (doc_typ_id ctx) 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 ^^ fields_doc ^^ hardline ^^ string "deriving" ^^ space
-        ^^ nest 2 (flow comma_sp [string "Inhabited"; string "DecidableEq"])
-        )
+      let rectyp = doc_typ_quant_relevant ctx tq in
+      let rectyp = List.map (fun d -> parens d) rectyp in
+      let decl_start =
+        if List.is_empty rectyp then [string "structure"; string id; string "where"]
+        else [string "structure"; string id; separate space rectyp; string "where"]
+      in
+      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_aux (Id id, _), tq, A_aux (A_nexp ne, _)) ->

test/lean/bitvec_operation.expected.lean

@@ -52,7 +52,7 @@ def bitvector_unsigned (x : (BitVec 16)) : Nat :=
 def bitvector_signed (x : (BitVec 16)) : Int :=
   (BitVec.toInt x)
 
-/-- Type quantifiers: i : Int, 0 ≤ i ∧ i ≤ 15 -/
+/-- Type quantifiers: i : Nat, 0 ≤ i ∧ i ≤ 15 -/
 def bitvector_access' (x : (BitVec 16)) (i : Nat) : (BitVec 1) :=
   (BitVec.access x i)
 

test/lean/enum.expected.lean

@@ -12,7 +12,7 @@ abbrev SailM := StateM Unit
 def undefined_E (lit : Unit) : SailM E := do
   sorry
 
-/-- Type quantifiers: arg_ : Int, 0 ≤ arg_ ∧ arg_ ≤ 2 -/
+/-- Type quantifiers: arg_ : Nat, 0 ≤ arg_ ∧ arg_ ≤ 2 -/
 def E_of_num (arg_ : Nat) : E :=
   match arg_ with
   | 0 => A

test/lean/ite.expected.lean

@@ -19,22 +19,22 @@ instance : Inhabited (RegisterRef RegisterType Nat) where
   default := .Reg R
 abbrev SailM := PreSailM RegisterType
 
-/-- Type quantifiers: n : Int, 0 ≤ n -/
+/-- Type quantifiers: n : Nat, 0 ≤ n -/
 def elif (n : Nat) : (BitVec 1) :=
   if (Eq n 0)
   then 1#1
   else if (Eq n 1)
        then 1#1
        else 0#1
 
-/-- Type quantifiers: n : Int, 0 ≤ n -/
+/-- Type quantifiers: n : Nat, 0 ≤ n -/
 def monadic_in_out (n : Nat) : SailM Nat := do
   if (← readReg B)
     then writeReg R n
     else (pure ())
   readReg R
 
-/-- Type quantifiers: n : Int, 0 ≤ n -/
+/-- Type quantifiers: n : Nat, 0 ≤ n -/
 def monadic_lines (n : Nat) : SailM Unit := do
   let b := (Eq n 0)
   if b

test/lean/range.expected.lean

@@ -4,19 +4,19 @@ open Sail
 
 abbrev SailM := StateM Unit
 
-/-- Type quantifiers: x : Int, 0 ≤ x ∧ x ≤ 31 -/
+/-- Type quantifiers: x : Nat, 0 ≤ x ∧ x ≤ 31 -/
 def f_int (x : Nat) : Int :=
   0
 
-/-- Type quantifiers: x : Int, 0 ≤ x ∧ x ≤ 31 -/
+/-- Type quantifiers: x : Nat, 0 ≤ x ∧ x ≤ 31 -/
 def f_nat (x : Nat) : Nat :=
   0
 
-/-- Type quantifiers: x : Int, k_n : Int, 0 ≤ x ∧ x ≤ k_n -/
+/-- Type quantifiers: x : Nat, k_n : Nat, 0 ≤ x ∧ x ≤ k_n -/
 def f_negvar (x : Nat) : Int :=
   x
 
-/-- Type quantifiers: x : Int, k_n : Int, 0 ≤ x ∧ x ≤ k_n -/
+/-- Type quantifiers: x : Nat, k_n : Nat, 0 ≤ x ∧ x ≤ k_n -/
 def f_nnegvar (x : Nat) : Nat :=
   x
 

test/lean/register_vector.expected.lean

@@ -84,13 +84,13 @@ def GPRs : (Vector (RegisterRef RegisterType (BitVec 64)) 31) :=
     Reg R20, Reg R19, Reg R18, Reg R17, Reg R16, Reg R15, Reg R14, Reg R13, Reg R12, Reg R11,
     Reg R10, Reg R9, Reg R8, Reg R7, Reg R6, Reg R5, Reg R4, Reg R3, Reg R2, Reg R1, Reg R0]
 
-/-- Type quantifiers: n : Int, 0 ≤ n ∧ n ≤ 31 -/
+/-- Type quantifiers: n : Nat, 0 ≤ n ∧ n ≤ 31 -/
 def wX (n : Nat) (value : (BitVec 64)) : SailM Unit := do
   if (Ne n 31)
   then writeRegRef (vectorAccess GPRs n) value
   else (pure ())
 
-/-- Type quantifiers: n : Int, 0 ≤ n ∧ n ≤ 31 -/
+/-- Type quantifiers: n : Nat, 0 ≤ n ∧ n ≤ 31 -/
 def rX (n : Nat) : SailM (BitVec 64) := do
   if (Ne n 31)
   then (reg_deref (vectorAccess GPRs n))
@@ -102,7 +102,7 @@ def rPC (lit : Unit) : SailM (BitVec 64) := do
 def wPC (pc : (BitVec 64)) : SailM Unit := do
   writeReg _PC pc
 
-/-- Type quantifiers: r : Int, 0 ≤ r ∧ r ≤ 31 -/
+/-- Type quantifiers: r : Nat, 0 ≤ r ∧ r ≤ 31 -/
 def monad_test (r : Nat) : SailM (BitVec 1) := do
   if (Eq (← (rX r)) (0x0000000000000000 : (BitVec 64)))
   then (pure 1#1)

test/lean/struct.expected.lean

@@ -5,7 +5,15 @@ open Sail
 structure My_struct where
   field1 : Int
   field2 : (BitVec 1)
-  deriving Inhabited, DecidableEq
+
+structure Mem_write_request
+  (k_n : Nat) (k_vasize : Nat) (k_pa : Type) (k_ts : Type) (k_arch_ak : Type) where
+  va : (Option (BitVec k_vasize))
+  pa : k_pa
+  translation : k_ts
+  size : Int
+  value : (Option (BitVec (8 * k_n)))
+  tag : (Option Bool)
 
 abbrev SailM := StateM Unit
 

test/lean/struct.sail

@@ -34,3 +34,13 @@ val undef_struct : bit -> My_struct
 function undef_struct (x) = {
   (undefined_My_struct(): My_struct)
 }
+
+struct Mem_write_request('n : Int, 'vasize : Int, 'pa : Type, 'ts : Type,
+                         'arch_ak : Type), 'n > 0 & 'vasize >= 0 = {
+  va : option(bits('vasize)),
+  pa : 'pa,
+  translation : 'ts,
+  size : int('n),
+  value : option(bits(8 * 'n)),
+  tag : option(bool),
+}

test/lean/struct_of_enum.expected.lean

@@ -9,14 +9,13 @@ open e_test
 
 structure s_test where
   f : e_test
-  deriving Inhabited, DecidableEq
 
 abbrev SailM := StateM Unit
 
 def undefined_e_test (lit : Unit) : SailM e_test := do
   sorry
 
-/-- Type quantifiers: arg_ : Int, 0 ≤ arg_ ∧ arg_ ≤ 0 -/
+/-- Type quantifiers: arg_ : Nat, 0 ≤ arg_ ∧ arg_ ≤ 0 -/
 def e_test_of_num (arg_ : Nat) : e_test :=
   match arg_ with
   | _ => VAL

test/lean/union.expected.lean

@@ -5,11 +5,9 @@ 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)