fdd5aec172
This refactors and improves the `#eval` command, introducing some new
features.
* Now evaluated results can be represented using `ToExpr` and pretty
printing. This means **hoverable output**. If `ToExpr` fails, it then
tries `Repr` and then `ToString`. The `eval.pp` option controls whether
or not to try `ToExpr`.
* There is now **auto-derivation** of `Repr` instances, enabled with the
`pp.derive.repr` option (default to **true**). For example:
```lean
inductive Baz
| a | b
#eval Baz.a
-- Baz.a
```
It simply does `deriving instance Repr for Baz` when there's no way to
represent `Baz`. If core Lean gets `ToExpr` derive handlers, they could
be used here as well.
* The option `eval.type` controls whether or not to include the type in
the output. For now the default is false.
* Now things like `#eval do return 2` work. It tries using
`CommandElabM`, `TermElabM`, or `IO` when the monad is unknown.
* Now there is no longer `Lean.Eval` or `Lean.MetaEval`. These each used
to be responsible for both adapting monads and printing results. The
concerns have been split into two. (1) The `MonadEval` class is
responsible for adapting monads for evaluation (it is similar to
`MonadLift`, but instances are allowed to use default data when
initializing state) and (2) finding a way to represent results is
handled separately.
* Error messages about failed instance synthesis are now more precise.
Once it detects that a `MonadEval` class applies, then the error message
will be specific about missing `ToExpr`/`Repr`/`ToString` instances.
* Fixes a bug where `Repr`/`ToString` instances can't be found by
unfolding types "under the monad". For example, this works now:
```lean
def Foo := List Nat
def Foo.mk (l : List Nat) : Foo := l
#eval show Lean.CoreM Foo from do return Foo.mk [1,2,3]
```
* Elaboration errors now abort evaluation. This eliminates some
not-so-relevant error messages.
* Now evaluating a value of type `m Unit` never prints a blank message.
* Fixes bugs where evaluating `MetaM` and `CoreM` wouldn't collect log
messages.
The `run_cmd`, `run_elab`, and `run_meta` commands are now frontends for
`#eval`.
179 lines
3.3 KiB
Text
179 lines
3.3 KiB
Text
import Lean
|
|
/-!
|
|
# Tests of the `#eval` command
|
|
-/
|
|
|
|
set_option eval.type true
|
|
|
|
/-!
|
|
Basic values
|
|
-/
|
|
/-- info: 2 : Nat -/
|
|
#guard_msgs in #eval 2
|
|
/-- info: some 2 : Option Nat -/
|
|
#guard_msgs in #eval some 2
|
|
/-- info: [2, 3, 4] : List Nat -/
|
|
#guard_msgs in #eval [1,2,3].map (· + 1)
|
|
|
|
/-!
|
|
Deciding a proposition
|
|
-/
|
|
/-- info: true : Bool -/
|
|
#guard_msgs in #eval True
|
|
|
|
/-!
|
|
Can't evaluate proofs
|
|
-/
|
|
/-- error: cannot evaluate, proofs are not computationally relevant -/
|
|
#guard_msgs in #eval trivial
|
|
|
|
/-!
|
|
Can't evaluate types
|
|
-/
|
|
/-- error: cannot evaluate, types are not computationally relevant -/
|
|
#guard_msgs in #eval Nat
|
|
|
|
|
|
/-!
|
|
Capturing `dbg_trace` output
|
|
-/
|
|
def Nat.choose : Nat → Nat → Nat
|
|
| _, 0 => dbg_trace "(_, 0)"; 1
|
|
| 0, _ + 1 => dbg_trace "(0, _ + 1)"; 0
|
|
| n + 1, k + 1 => dbg_trace "(_ + 1, _ + 1)"; choose n k + choose n (k + 1)
|
|
/--
|
|
info: (_ + 1, _ + 1)
|
|
(_ + 1, _ + 1)
|
|
(_, 0)
|
|
(0, _ + 1)
|
|
(_ + 1, _ + 1)
|
|
(0, _ + 1)
|
|
(0, _ + 1)
|
|
---
|
|
info: 1 : Nat
|
|
-/
|
|
#guard_msgs in #eval Nat.choose 2 2
|
|
|
|
/-!
|
|
Custom monad
|
|
-/
|
|
|
|
abbrev MyMonad := ReaderT Nat IO
|
|
/--
|
|
error: unable to synthesize 'MonadEval' instance to adapt
|
|
MyMonad Nat
|
|
to 'IO' or 'Lean.Elab.Command.CommandElabM'.
|
|
-/
|
|
#guard_msgs in #eval (pure 2 : MyMonad Nat)
|
|
|
|
-- Note that there is no "this is due to..." diagonostic in this case.
|
|
/--
|
|
error: could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type
|
|
MyMonad (Nat → Nat)
|
|
-/
|
|
#guard_msgs in #eval (pure id : MyMonad (Nat → _))
|
|
|
|
instance : MonadEval MyMonad IO where
|
|
monadEval m := m.run 0
|
|
|
|
/-- info: 2 : Nat -/
|
|
#guard_msgs in #eval (pure 2 : MyMonad Nat)
|
|
|
|
-- Note that now we have a MonadEval instance, it doesn't mention MyMonad in the error.
|
|
/--
|
|
error: could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type
|
|
Nat → Nat
|
|
-/
|
|
#guard_msgs in #eval (pure id : MyMonad (Nat → _))
|
|
|
|
/-!
|
|
Elaboration error, does not attempt to evaluate.
|
|
-/
|
|
/-- error: unknown identifier 'x' -/
|
|
#guard_msgs in #eval 2 + x
|
|
|
|
/-!
|
|
Defaulting to the CommandElabM monad
|
|
-/
|
|
/-- info: 2 : Nat -/
|
|
#guard_msgs in #eval do pure 2
|
|
/-- info: true : Bool -/
|
|
#guard_msgs in #eval do return (← Lean.getEnv).contains ``Lean.MessageData
|
|
|
|
/-!
|
|
Defaulting does not affect postponed elaborators.
|
|
-/
|
|
/-- info: 1 : Nat -/
|
|
#guard_msgs in #eval if True then 1 else 2
|
|
|
|
/-!
|
|
Testing that dbg_trace and logs carry over from all the major meta monads.
|
|
-/
|
|
/--
|
|
info: hi
|
|
---
|
|
info: dbg
|
|
-/
|
|
#guard_msgs in #eval show Lean.Elab.Term.TermElabM Unit from do dbg_trace "dbg"; Lean.logInfo m!"hi"
|
|
/--
|
|
info: hi
|
|
---
|
|
info: dbg
|
|
-/
|
|
#guard_msgs in #eval show Lean.MetaM Unit from do dbg_trace "dbg"; Lean.logInfo m!"hi"
|
|
/--
|
|
info: hi
|
|
---
|
|
info: dbg
|
|
-/
|
|
#guard_msgs in #eval show Lean.CoreM Unit from do dbg_trace "dbg"; Lean.logInfo m!"hi"
|
|
|
|
/-!
|
|
Testing delta deriving
|
|
-/
|
|
def Foo := List Nat
|
|
def Foo.mk (l : List Nat) : Foo := l
|
|
|
|
/-- info: [1, 2, 3] : Foo -/
|
|
#guard_msgs in #eval Foo.mk [1,2,3]
|
|
|
|
/-- info: [1, 2, 3] : Foo -/
|
|
#guard_msgs in #eval do return Foo.mk [1,2,3]
|
|
|
|
/-!
|
|
Testing auto-deriving
|
|
-/
|
|
|
|
inductive Baz
|
|
| a | b
|
|
|
|
/-- info: Baz.a : Baz -/
|
|
#guard_msgs in #eval Baz.a
|
|
|
|
/-!
|
|
Returning after printing
|
|
-/
|
|
def returns : Lean.CoreM Nat := do
|
|
IO.println "hi"
|
|
return 2
|
|
|
|
/--
|
|
info: hi
|
|
---
|
|
info: 2 : Nat
|
|
-/
|
|
#guard_msgs in #eval returns
|
|
|
|
/-!
|
|
Throwing an exception after printing
|
|
-/
|
|
def throwsEx : Lean.CoreM Nat := do
|
|
IO.println "hi"
|
|
throwError "ex"
|
|
|
|
/--
|
|
info: hi
|
|
---
|
|
error: ex
|
|
-/
|
|
#guard_msgs in #eval throwsEx
|