Lean: Translate function bodies that only consist of literals or vari…

…ables (#745)

* create doc_exp and doc_funcl_body functions
* implement doc_lit
* add trivial test file with expected output

src/sail_lean_backend/pretty_print_lean.ml

@@ -65,7 +65,34 @@ let rec untuple_args_pat typs (P_aux (paux, ((l, _) as annot)) as pat) =
   | _, _ -> unreachable l __POS__ "Unexpected pattern/type combination"
 
 let doc_typ (Typ_aux (t, _) as typ) =
-  match t with Typ_id (Id_aux (Id "unit", _)) -> string "Unit" | _ -> failwith "Type not translatable yet."
+  match t with
+  | Typ_id (Id_aux (Id "unit", _)) -> string "Unit"
+  | Typ_id (Id_aux (Id "int", _)) -> string "Int"
+  | _ -> failwith "Type not translatable yet."
+
+let lean_escape_string s = Str.global_replace (Str.regexp "\"") "\"\"" s
+
+let doc_lit (L_aux (lit, l)) =
+  match lit with
+  | L_unit -> string "()"
+  | L_zero -> string "0"
+  | L_one -> string "1"
+  | L_false -> string "false"
+  | L_true -> string "true"
+  | L_num i ->
+      let s = Big_int.to_string i in
+      string s
+  | L_hex n -> utf8string ("Ox" ^ n)
+  | L_bin n -> utf8string ("Ob" ^ n)
+  | L_undef -> utf8string "(Fail \"undefined value of unsupported type\")"
+  | L_string s -> utf8string ("\"" ^ lean_escape_string s ^ "\"")
+  | L_real s -> utf8string s (* TODO test if this is really working *)
+
+let doc_exp (E_aux (e, (l, annot)) as full_exp) =
+  match e with
+  | E_id id -> string (string_of_id id) (* TODO replace by a translating via a binding map *)
+  | E_lit l -> doc_lit l
+  | _ -> failwith "Expression not translatable yet"
 
 let doc_funcl_init (FCL_aux (FCL_funcl (id, pexp), annot)) =
   let env = env_of_tannot (snd annot) in
@@ -91,11 +118,15 @@ let doc_funcl_init (FCL_aux (FCL_funcl (id, pexp), annot)) =
            )
       in
       let binders : document list =
-        binders |> List.map (fun (i, t) -> separate space [string (string_of_id i); string ":"; doc_typ t] |> parens)
+        binders |> List.map (fun (i, t) -> separate space [string (string_of_id i); colon; doc_typ t] |> parens)
       in
-      separate space ([string "def"; string (string_of_id id)] @ binders @ [string ":"; doc_typ ret_typ; string ":="])
+      separate space ([string "def"; string (string_of_id id)] @ binders @ [colon; doc_typ ret_typ; coloneq])
+
+let doc_funcl_body (FCL_aux (FCL_funcl (id, pexp), annot)) =
+  let _, _, exp, _ = destruct_pexp pexp in
+  doc_exp exp
 
-let doc_funcl funcl = separate hardline [doc_funcl_init funcl; string "  _"] ^^ hardline
+let doc_funcl funcl = nest 2 (doc_funcl_init funcl ^^ hardline ^^ doc_funcl_body funcl)
 
 let doc_fundef (FD_aux (FD_function (r, typa, fcls), fannot)) =
   match fcls with

test/lean/trivial.expected.lean

@@ -0,0 +1,6 @@
+def foo (y : Unit) : Unit :=
+  y
+
+def initialize_registers : Unit :=
+  ()
+

test/lean/trivial.sail

@@ -0,0 +1,4 @@
+function foo(y : unit) -> unit = {
+  return y
+}
+