Lean: add support for range types

src/sail_lean_backend/pretty_print_lean.ml

@@ -113,6 +113,7 @@ let rec doc_typ (Typ_aux (t, _) as typ) =
   | Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]) -> string "Int"
   | Typ_tuple ts -> parens (separate_map (space ^^ string "×" ^^ space) doc_typ ts)
   | Typ_id (Id_aux (Id id, _)) -> string id
+  | Typ_app (Id_aux (Id "range", _), [A_aux (A_nexp low, _); A_aux (A_nexp high, _)]) -> string "Int"
   | _ -> failwith ("Type " ^ string_of_typ_con typ ^ " " ^ string_of_typ typ ^ " not translatable yet.")
 
 let doc_typ_id (typ, fid) = concat [doc_id_ctor fid; space; colon; space; doc_typ typ; hardline]

test/lean/range.expected.lean

@@ -0,0 +1,20 @@
+import Out.Sail.Sail
+
+def f_int (x : Int) : Int :=
+  0
+
+def f_nat (x : Int) : Int :=
+  0
+
+def f_negvar (x : Int) : Int :=
+  x
+
+def f_nnegvar (x : Int) : Int :=
+  x
+
+def f_unkn (x : Int) : Int :=
+  x
+
+def initialize_registers : Unit :=
+  ()
+

test/lean/range.sail

@@ -0,0 +1,28 @@
+default Order dec
+$include <prelude.sail>
+
+
+val f_int : range(0, 31) -> range(-2, 2)
+function f_int(x) = {
+  0
+}
+
+val f_nat : range(0, 31) -> range(0, 2)
+function f_nat(x) = {
+  0
+}
+
+val f_negvar : forall 'n. range(0, 'n) -> range(- 'n, 'n)
+function f_negvar(x) = {
+  x
+}
+
+val f_nnegvar : forall 'n. range(0, 'n) -> range(0, 'n)
+function f_nnegvar(x) = {
+  x
+}
+
+val f_unkn : forall 'n 'm. range('n, 'm) -> range('n, 'm)
+function f_unkn(x) = {
+  x
+}