From 4cff135ec301136acc6231a4db0fe7935f97753c Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 19 Mar 2020 16:42:11 +0100
Subject: [PATCH] feat: #eval: auto-hide `()` output for `m Unit` chained
 instances

---
 src/Init/Lean/Elab/Term.lean        |  4 ++--
 src/Init/Lean/Eval.lean             | 10 +++++-----
 src/Init/Lean/Meta/Message.lean     |  2 +-
 src/Init/System/IO.lean             | 17 +++++++++--------
 src/frontends/lean/builtin_cmds.cpp | 10 +++++-----
 5 files changed, 22 insertions(+), 21 deletions(-)

diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 2032351026..f35c18a14a 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -1152,7 +1152,7 @@ fun stx _ =>
   | none     => throwError stx "ill-formed syntax"
 
 instance MetaHasEval {α} [MetaHasEval α] : MetaHasEval (TermElabM α) :=
-⟨fun env opts x => do
+⟨fun env opts x _ => do
   let ctx : Context := {
     config        := { opts := opts },
     fileName      := "<TermElabM>",
@@ -1177,7 +1177,7 @@ instance MetaHasEval {α} [MetaHasEval α] : MetaHasEval (TermElabM α) :=
     throw (IO.userError "error: unsupported syntax")
   | EStateM.Result.error Exception.postpone s => do
     showMessages s;
-    throw (IO.userError "error: elaborator posponed")⟩
+    throw (IO.userError "error: elaborator postponed")⟩
 
 end Term
 
diff --git a/src/Init/Lean/Eval.lean b/src/Init/Lean/Eval.lean
index a58779b2d8..508d9c52a6 100644
--- a/src/Init/Lean/Eval.lean
+++ b/src/Init/Lean/Eval.lean
@@ -16,10 +16,10 @@ universe u
     The basic `HasEval` class is in the prelude and should not depend on these
     types. -/
 class MetaHasEval (α : Type u) :=
-(eval : Environment → Options → α → IO Unit)
+(eval : Environment → Options → α → forall (hideUnit : optParam Bool true), IO Unit)
 
-instance MetaHasEvalOfHasEval {α : Type u} [HasEval α] : MetaHasEval α :=
-⟨fun env opts a => HasEval.eval a⟩
+instance metaHasEvalOfHasEval {α : Type u} [HasEval α] : MetaHasEval α :=
+⟨fun env opts a hideUnit => HasEval.eval a hideUnit⟩
 
 abbrev MetaIO := ReaderT (Environment × Options) IO
 
@@ -29,8 +29,8 @@ ctx ← read; pure ctx.1
 def MetaIO.getOptions : MetaIO Options := do
 ctx ← read; pure ctx.2
 
-instance MetaIO.metaHasEval : MetaHasEval (MetaIO Unit) :=
-⟨fun env opts x => x (env, opts)⟩
+instance MetaIO.metaHasEval {α} [MetaHasEval α] : MetaHasEval (MetaIO α) :=
+⟨fun env opts x _ => x (env, opts) >>= MetaHasEval.eval env opts⟩
 
 instance MetaIO.monadIO : MonadIO MetaIO :=
 ⟨fun _ x _ => x⟩
diff --git a/src/Init/Lean/Meta/Message.lean b/src/Init/Lean/Meta/Message.lean
index fde90ecc32..2f22a50731 100644
--- a/src/Init/Lean/Meta/Message.lean
+++ b/src/Init/Lean/Meta/Message.lean
@@ -85,7 +85,7 @@ def toMessageData : Exception → MessageData
 end Exception
 
 instance MetaHasEval {α} [MetaHasEval α] : MetaHasEval (MetaM α) :=
-⟨fun env opts x => do
+⟨fun env opts x _ => do
    match x { config := { opts := opts }, currRecDepth := 0, maxRecDepth := getMaxRecDepth opts } { env := env } with
    | EStateM.Result.ok a s    => do
      s.traceState.traces.forM $ fun m => IO.println $ format m;
diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 92dffbaa5c..903be6b018 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -308,16 +308,17 @@ namespace Lean
 
 /-- Typeclass used for presenting the output of an `#eval` command. -/
 class HasEval (α : Type u) :=
-(eval : α → IO Unit)
+-- We default `hideUnit` to `true`, but set it to `false` in the direct call from `#eval`
+-- so that `()` output is hidden in chained instances such as for some `m Unit`.
+(eval : α → forall (hideUnit : optParam Bool true), IO Unit)
 
-instance HasRepr.HasEval {α : Type u} [HasRepr α] : HasEval α :=
-⟨fun a => IO.println (repr a)⟩
+instance HasRepr.hasEval {α : Type u} [HasRepr α] : HasEval α :=
+⟨fun a _ => IO.println (repr a)⟩
+
+instance Unit.hasEval : HasEval Unit :=
+⟨fun u hideUnit => if hideUnit then pure () else IO.println (repr u)⟩
 
 instance IO.HasEval {α : Type} [HasEval α] : HasEval (IO α) :=
-⟨fun x => do a ← x; HasEval.eval a⟩
-
--- special case: do not print `()`
-instance IOUnit.HasEval : HasEval (IO Unit) :=
-⟨fun x => x⟩
+⟨fun x _ => do a ← x; HasEval.eval a⟩
 
 end Lean
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 3b31593497..0b39432212 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -349,12 +349,12 @@ static environment eval_cmd(parser & p) {
     } catch (exception &) {}
 
     if (meta_eval_instance) {
-        /* Modify the 'program' to (fun env opts => MetaHasEval.eval env opts e) */
+        /* Modify the 'program' to (fun env opts => MetaHasEval.eval (hideUnit := false) env opts e) */
         expr env = tc.push_local("env", mk_const({"Lean", "Environment"}));
         expr opts = tc.push_local("opts", mk_const({"Lean", "Options"}));
         e = tc.mk_lambda(env, tc.mk_lambda(opts,
-                                           mk_app(tc, {"Lean", "MetaHasEval", "eval"}, 5,
-                                                  {type, *meta_eval_instance, env, opts, e})));
+                                           mk_app(tc, {"Lean", "MetaHasEval", "eval"}, 6,
+                                                  {type, *meta_eval_instance, env, opts, e, mk_bool_false()})));
         // run `Environment -> Options -> IO Unit`
         args = { p.env().to_obj_arg(), p.get_options().to_obj_arg(), io_mk_world() };
     } else {
@@ -365,8 +365,8 @@ static environment eval_cmd(parser & p) {
         } catch (exception &) {}
 
         if (eval_instance) {
-            /* Modify the 'program' to (HasEval.eval e) */
-            e = mk_app(tc, {"Lean", "HasEval", "eval"}, 3, type, *eval_instance, e);
+            /* Modify the 'program' to (HasEval.eval (hideUnit := false) e) */
+            e = mk_app(tc, {"Lean", "HasEval", "eval"}, 4, {type, *eval_instance, e, mk_bool_false()});
             // run `IO Unit`
             args = { io_mk_world() };
         } else {