Lean: support for implicit arguments in function application (#955)

This closes #948.

src/sail_lean_backend/pretty_print_lean.ml

@@ -398,6 +398,14 @@ let wrap_with_pure (needs_return : bool) (d : document) =
 let wrap_with_left_arrow (needs_return : bool) (d : document) =
   if needs_return then parens (nest 2 (flow space [string "←"; d])) else d
 
+let get_fn_implicits (Typ_aux (t, _)) : bool list =
+  let arg_implicit arg =
+    match arg with
+    | Typ_aux (Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp (Nexp_aux (Nexp_var ki, _)), _)]), _) -> true
+    | _ -> false
+  in
+  match t with Typ_fn (args, cod) -> List.map arg_implicit args | _ -> []
+
 let rec doc_match_clause (as_monadic : bool) ctx (Pat_aux (cl, l)) =
   match cl with
   | Pat_exp (pat, branch) -> string "| " ^^ doc_pat pat ^^ string " =>" ^^ space ^^ doc_exp as_monadic ctx branch
@@ -446,11 +454,14 @@ and doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
       in
       nest 2 (e0_pp ^^ e1_pp) ^^ hardline ^^ e2_pp
   | E_app (f, args) ->
+      let _, f_typ = Env.get_val_spec f env in
+      let implicits = get_fn_implicits f_typ in
       let d_id =
         if Env.is_extern f env "lean" then string (Env.get_extern f env "lean")
         else doc_exp false ctx (E_aux (E_id f, (l, annot)))
       in
       let d_args = List.map d_of_arg args in
+      let d_args = List.map snd (List.filter (fun x -> not (fst x)) (List.combine implicits d_args)) in
       let fn_monadic = not (Effects.function_is_pure f ctx.global.effect_info) in
       nest 2
         (wrap_with_left_arrow ((not as_monadic) && fn_monadic)

test/lean/implicit.expected.lean

@@ -0,0 +1,16 @@
+import Out.Sail.Sail
+
+open Sail
+
+abbrev SailM := StateM Unit
+
+/-- Type quantifiers: k_n : Int, m : Int, m ≥ k_n -/
+def EXTZ {m : _} (v : (BitVec k_n)) : (BitVec m) :=
+  (Sail.BitVec.zeroExtend v m)
+
+def foo (x : (BitVec 8)) : (BitVec 16) :=
+  (EXTZ x)
+
+def initialize_registers (lit : Unit) : Unit :=
+  ()
+

test/lean/implicit.sail

@@ -0,0 +1,11 @@
+default Order dec
+
+$include <prelude.sail>
+
+val EXTZ : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
+function EXTZ(m, v) = sail_zero_extend(v, m)
+
+val foo : bits(8) -> bits(16)
+function foo x = {
+  EXTZ(x)
+}