Lean: add support for range types

src/sail_lean_backend/pretty_print_lean.ml

@@ -102,6 +102,10 @@ let string_of_typ_con (Typ_aux (t, _)) =
   | Typ_internal_unknown -> "Typ_internal_unknown"
   | Typ_id _ -> "Typ_id"
 
+let clearly_negative (Nexp_aux (n, _)) =
+  Printf.printf "hi there\n";
+  match n with Nexp_neg _ -> true | Nexp_constant n -> Nat_big_num.(less n zero) | _ -> false
+
 let rec doc_typ (Typ_aux (t, _) as typ) =
   match t with
   | Typ_id (Id_aux (Id "unit", _)) -> string "Unit"
@@ -113,6 +117,10 @@ 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, _)]) ->
+      (* The heuristics is that 99% of rages are positive, so we try to
+         translate them to Nat. *)
+      if clearly_negative low then string "Int" else string "Nat"
   | _ -> 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) : Nat :=
+  0
+
+def f_negvar (x : Int) : Int :=
+  x
+
+def f_nnegvar (x : Int) : Nat :=
+  x
+
+def f_unkn (x : Int) : Nat :=
+  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
+}