From 91dca5327410c2d5731b4e795eaa3867bff731df Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 18 Nov 2020 17:55:03 -0800 Subject: [PATCH] refactor: remove `MonadIO` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit There is no reason for having `MonadIO` anymore. The `MonadLift` type class is well behaved in the new frontend, the `MonadFinally` solves the problem at monad stacks such as `ExcepT e IO`. This commit also changes the type of the IO printing functions. For example, the type of `IO.println` was ``` def IO.println {m} [MonadIO m] {α} [ToString α] (s : α) : m Unit ``` and now it is just ``` def IO.println {α} [ToString α] (s : α) : IO Unit ``` We rely on the new frontend auto-lifting feature. That is, if there is an instance `[MonadLiftT IO m]`, then a term of type `IO a` is automatically coerced to `m a` We also want a simpler `IO.println` for writing tests. For example, ``` ``` doesn't work because there isn't sufficient information for inferring the parameter `m` in the previous `IO.println`. The shortest workaround looked very weird ``` ``` I considered adding `IO` as a default value for `m` when we have `MonadIO m`, as we use `Nat` as the default for `ofNat a`, but it felt like uncessary complexity. @Kha The commit seems to work well. The auto-lifting featuring has been working great for me. There is still room for improvement. For example, given `MonadLiftT m n`, it doesn't automatically lift `a -> m b` into `a -> n b`. So, code such as `foo >>= IO.println` had to be rewritten as `foo >>= fun x => IO.println x` I will add this feature later. If you have time, please try to play with this feature and figure out if it is stable enough for making it the default. That is, if it roboust enough, we can stop using the following idiom for writing functions that can be lifted automatically. ``` def instantiateLevelMVarsImp (u : Level) : MetaM Level := ... def instantiateLevelMVars {m} [MonadLiftT MetaM m] (u : Level) : m Level := liftMetaM $ instantiateLevelMVarsImp u ``` I think we only need this idiom when using `MonadControlT` which is not as common as `MonadLiftT`. --- src/Init/Control/StateRef.lean | 1 - src/Init/System/IO.lean | 72 ++++++++++------------- src/Lean/Attributes.lean | 2 +- src/Lean/CoreM.lean | 4 +- src/Lean/Elab/Command.lean | 6 +- src/Lean/Elab/Log.lean | 4 +- src/Lean/Elab/Syntax.lean | 8 +-- src/Lean/Elab/Term.lean | 5 +- src/Lean/KeyedDeclsAttribute.lean | 2 +- src/Lean/Meta/Basic.lean | 14 ++--- src/Lean/Meta/Instances.lean | 4 +- src/Lean/Meta/Tactic/Util.lean | 2 +- src/Lean/Parser/Extension.lean | 4 +- src/Lean/ParserCompiler.lean | 2 +- src/Lean/PrettyPrinter/Formatter.lean | 6 +- src/Lean/PrettyPrinter/Parenthesizer.lean | 6 +- src/Lean/Util/MonadCache.lean | 1 - src/Lean/Util/Trace.lean | 6 +- tests/lean/ppExpr.lean | 4 +- tests/lean/ppSyntax.lean | 4 +- tests/lean/run/evalconst.lean | 2 +- tests/lean/run/frontend1.lean | 4 +- tests/lean/run/termParserAttr.lean | 4 +- tests/lean/typeMismatch.lean.expected.out | 2 +- 24 files changed, 76 insertions(+), 93 deletions(-) diff --git a/src/Init/Control/StateRef.lean b/src/Init/Control/StateRef.lean index 38fd9d2115..65bdfbc82a 100644 --- a/src/Init/Control/StateRef.lean +++ b/src/Init/Control/StateRef.lean @@ -31,7 +31,6 @@ variables {ω σ : Type} {m : Type → Type} {α : Type} instance [Monad m] : Monad (StateRefT' ω σ m) := inferInstanceAs (Monad (ReaderT _ _)) instance : MonadLift m (StateRefT' ω σ m) := ⟨StateRefT'.lift⟩ -instance [Monad m] [MonadIO m] : MonadIO (StateRefT' ω σ m) := inferInstanceAs (MonadIO (ReaderT _ _)) instance (σ m) [Monad m] : MonadFunctor m (StateRefT' ω σ m) := inferInstanceAs (MonadFunctor m (ReaderT _ _)) @[inline] protected def get [Monad m] [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ := diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 226eb83227..4e031b3231 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -73,17 +73,6 @@ set_option compiler.extract_closed false in The action `initializing` returns `true` iff it is invoked during initialization. -/ @[extern "lean_io_initializing"] constant IO.initializing : IO Bool -class MonadIO (m : Type → Type) := - { liftIO {α} : IO α → m α } - -export MonadIO (liftIO) - -instance (m n) [MonadIO m] [MonadLift m n] : MonadIO n := - { liftIO := fun x => liftM (liftIO x : m _) } - -instance : MonadIO IO := -{ liftIO := id } - namespace IO def ofExcept {ε α : Type} [ToString ε] (e : Except ε α) : IO α := @@ -190,10 +179,10 @@ def fopenFlags (m : FS.Mode) (b : Bool) : String := end Prim namespace FS -variables {m : Type → Type} [Monad m] [MonadIO m] +variables {m : Type → Type} [Monad m] [MonadLiftT IO m] def Handle.mk (s : String) (Mode : Mode) (bin : Bool := true) : m Handle := - liftIO (Prim.Handle.mk s (Prim.fopenFlags Mode bin)) + liftM (Prim.Handle.mk s (Prim.fopenFlags Mode bin)) @[inline] def withFile {α} (fn : String) (mode : Mode) (f : Handle → m α) : m α := @@ -203,15 +192,15 @@ def withFile {α} (fn : String) (mode : Mode) (f : Handle → m α) : m α := `h.isEof` returns true /after/ the first attempt at reading past the end of `h`. Once `h.isEof` is true, the reading `h` raises `IO.Error.eof`. -/ -def Handle.isEof : Handle → m Bool := liftIO ∘ Prim.Handle.isEof -def Handle.flush : Handle → m Unit := liftIO ∘ Prim.Handle.flush -def Handle.read (h : Handle) (bytes : Nat) : m ByteArray := liftIO (Prim.Handle.read h (USize.ofNat bytes)) -def Handle.write (h : Handle) (s : ByteArray) : m Unit := liftIO (Prim.Handle.write h s) +def Handle.isEof : Handle → m Bool := liftM ∘ Prim.Handle.isEof +def Handle.flush : Handle → m Unit := liftM ∘ Prim.Handle.flush +def Handle.read (h : Handle) (bytes : Nat) : m ByteArray := liftM (Prim.Handle.read h (USize.ofNat bytes)) +def Handle.write (h : Handle) (s : ByteArray) : m Unit := liftM (Prim.Handle.write h s) -def Handle.getLine : Handle → m String := liftIO ∘ Prim.Handle.getLine +def Handle.getLine : Handle → m String := liftM ∘ Prim.Handle.getLine def Handle.putStr (h : Handle) (s : String) : m Unit := - liftIO $ Prim.Handle.putStr h s + liftM $ Prim.Handle.putStr h s def Handle.putStrLn (h : Handle) (s : String) : m Unit := h.putStr (s.push '\n') @@ -246,27 +235,27 @@ partial def lines (fname : String) : m (Array String) := do namespace Stream def putStrLn (strm : FS.Stream) (s : String) : m Unit := - liftIO (strm.putStr (s.push '\n')) + liftM (strm.putStr (s.push '\n')) end Stream end FS section -variables {m : Type → Type} [Monad m] [MonadIO m] +variables {m : Type → Type} [Monad m] [MonadLiftT IO m] -def getStdin : m FS.Stream := liftIO Prim.getStdin -def getStdout : m FS.Stream := liftIO Prim.getStdout -def getStderr : m FS.Stream := liftIO Prim.getStderr +def getStdin : m FS.Stream := liftM Prim.getStdin +def getStdout : m FS.Stream := liftM Prim.getStdout +def getStderr : m FS.Stream := liftM Prim.getStderr /-- Replaces the stdin stream of the current thread and returns its previous value. -/ -def setStdin : FS.Stream → m FS.Stream := liftIO ∘ Prim.setStdin +def setStdin : FS.Stream → m FS.Stream := liftM ∘ Prim.setStdin /-- Replaces the stdout stream of the current thread and returns its previous value. -/ -def setStdout : FS.Stream → m FS.Stream := liftIO ∘ Prim.setStdout +def setStdout : FS.Stream → m FS.Stream := liftM ∘ Prim.setStdout /-- Replaces the stderr stream of the current thread and returns its previous value. -/ -def setStderr : FS.Stream → m FS.Stream := liftIO ∘ Prim.setStderr +def setStderr : FS.Stream → m FS.Stream := liftM ∘ Prim.setStderr def withStdin [MonadFinally m] {α} (h : FS.Stream) (x : m α) : m α := do let prev ← setStdin h @@ -280,32 +269,35 @@ def withStderr [MonadFinally m] {α} (h : FS.Stream) (x : m α) : m α := do let prev ← setStderr h try x finally discard $ setStderr prev -def print {α} [ToString α] (s : α) : m Unit := do +def print {α} [ToString α] (s : α) : IO Unit := do let out ← getStdout - liftIO $ out.putStr $ toString s + out.putStr $ toString s -def println {α} [ToString α] (s : α) : m Unit := print ((toString s).push '\n') +def println {α} [ToString α] (s : α) : IO Unit := + print ((toString s).push '\n') -def eprint {α} [ToString α] (s : α) : m Unit := do +def eprint {α} [ToString α] (s : α) : IO Unit := do let out ← getStderr - liftIO $ out.putStr $ toString s + liftM $ out.putStr $ toString s -def eprintln {α} [ToString α] (s : α) : m Unit := eprint ((toString s).push '\n') +def eprintln {α} [ToString α] (s : α) : IO Unit := + eprint ((toString s).push '\n') @[export lean_io_eprintln] -private def eprintlnAux (s : String) : IO Unit := eprintln s +private def eprintlnAux (s : String) : IO Unit := + eprintln s -def getEnv : String → m (Option String) := liftIO ∘ Prim.getEnv -def realPath : String → m String := liftIO ∘ Prim.realPath -def isDir : String → m Bool := liftIO ∘ Prim.isDir -def fileExists : String → m Bool := liftIO ∘ Prim.fileExists -def appPath : m String := liftIO Prim.appPath +def getEnv : String → m (Option String) := liftM ∘ Prim.getEnv +def realPath : String → m String := liftM ∘ Prim.realPath +def isDir : String → m Bool := liftM ∘ Prim.isDir +def fileExists : String → m Bool := liftM ∘ Prim.fileExists +def appPath : m String := liftM Prim.appPath def appDir : m String := do let p ← appPath realPath (System.FilePath.dirName p) -def currentDir : m String := liftIO Prim.currentDir +def currentDir : m String := liftM Prim.currentDir end diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index dc319c9d04..65034a591a 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -27,7 +27,7 @@ structure Attr.Context := abbrev AttrM := ReaderT Attr.Context CoreM instance : MonadLift ImportM AttrM := { - monadLift := fun x => do liftIO (x { env := (← getEnv), opts := (← getOptions) }) + monadLift := fun x => do liftM (m := IO) (x { env := (← getEnv), opts := (← getOptions) }) } instance : MonadResolveName AttrM := { diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 09e2686a69..d30b40a304 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -64,8 +64,8 @@ instance : MonadRecDepth CoreM := { let ref ← getRef IO.toEIO (fun (err : IO.Error) => Exception.error ref (toString err)) x -instance : MonadIO CoreM := { - liftIO := @liftIOCore +instance : MonadLift IO CoreM := { + monadLift := liftIOCore } instance : MonadTrace CoreM := { diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 88658c853b..64079a535c 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -125,7 +125,7 @@ private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : M let ctx ← read IO.toEIO (fun (ex : IO.Error) => Exception.error ctx.ref ex.toString) x -instance : MonadIO CommandElabM := { liftIO := liftIO } +instance : MonadLiftT IO CommandElabM := { monadLift := liftIO } def getScope : CommandElabM Scope := do pure (← get).scopes.head! @@ -573,7 +573,7 @@ unsafe def elabEvalUnsafe : CommandElab := fun stx => do let env ← getEnv let opts ← getOptions let act ← try addAndCompile e; evalConst (Environment → Options → IO (String × Except IO.Error Environment)) n finally setEnv env - let (out, res) ← MonadIO.liftIO $ act env opts -- we execute `act` using the environment + let (out, res) ← act env opts -- we execute `act` using the environment logInfo out match res with | Except.error e => throwError e.toString @@ -587,7 +587,7 @@ unsafe def elabEvalUnsafe : CommandElab := fun stx => do let e ← mkAppM `Lean.runEval #[e] let env ← getEnv let act ← try addAndCompile e; evalConst (IO (String × Except IO.Error Unit)) n finally setEnv env - let (out, res) ← MonadIO.liftIO act + let (out, res) ← liftM (m := IO) act logInfo out match res with | Except.error e => throwError e.toString diff --git a/src/Lean/Elab/Log.lean b/src/Lean/Elab/Log.lean index ea611b48ac..3f7e3a607b 100644 --- a/src/Lean/Elab/Log.lean +++ b/src/Lean/Elab/Log.lean @@ -62,12 +62,12 @@ def logWarning (msgData : MessageData) : m Unit := def logInfo (msgData : MessageData) : m Unit := log msgData MessageSeverity.information -def logException [MonadIO m] (ex : Exception) : m Unit := do +def logException [MonadLiftT IO m] (ex : Exception) : m Unit := do match ex with | Exception.error ref msg => logErrorAt ref msg | Exception.internal id => unless id == abortExceptionId do - let name ← liftIO $ id.getName + let name ← id.getName logError ("internal exception: " ++ name) def logTrace (cls : Name) (msgData : MessageData) : m Unit := do diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index cc4a6d5c92..6a294dfd35 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -82,20 +82,20 @@ partial def toParserDescrAux (stx : Syntax) : ToParserDescrM Syntax := withRef s toParserDescrAux stx[1] else if kind == `Lean.Parser.Syntax.unary then let aliasName := (stx[0].getId).eraseMacroScopes - liftIO $ Parser.ensureUnaryParserAlias aliasName + Parser.ensureUnaryParserAlias aliasName let d ← withNestedParser $ toParserDescrAux stx[2] `(ParserDescr.unary $(quote aliasName) $d) else if kind == `Lean.Parser.Syntax.binary then let aliasName := (stx[0].getId).eraseMacroScopes - liftIO $ Parser.ensureBinaryParserAlias aliasName + Parser.ensureBinaryParserAlias aliasName let d₁ ← withNestedParser $ toParserDescrAux stx[2] let d₂ ← withNestedParser $ toParserDescrAux stx[4] `(ParserDescr.binary $(quote aliasName) $d₁ $d₂) else if kind == `Lean.Parser.Syntax.cat then let cat := stx[0].getId.eraseMacroScopes let prec? : Option Nat := expandOptPrecedence stx[1] - if (← liftIO $ Parser.isParserAlias cat) then - liftIO $ Parser.ensureConstantParserAlias cat + if (← Parser.isParserAlias cat) then + Parser.ensureConstantParserAlias cat if prec?.isSome then throwErrorAt! stx[1] "unexpected precedence in atomic parser" `(ParserDescr.const $(quote cat)) diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 6c7f7b10c2..497a18bda6 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -201,9 +201,6 @@ def applyResult (result : TermElabResult) : TermElabM Expr := | EStateM.Result.ok e r => do r.restore; pure e | EStateM.Result.error ex r => do r.restore; throw ex -instance : MonadIO TermElabM := -{ liftIO := fun x => liftMetaM $ liftIO x } - @[inline] protected def liftMetaM {α} (x : MetaM α) : TermElabM α := liftM x @@ -1264,7 +1261,7 @@ instance {α} [MetaEval α] : MetaEval (TermElabM α) := let x : TermElabM α := do try x finally let s ← get - liftIO $ s.messages.forM fun msg => msg.toString >>= IO.println + s.messages.forM fun msg => do IO.println (← msg.toString) MetaEval.eval env opts (hideUnit := true) $ x.run' mkSomeContext⟩ end Term diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean index 50e390a9c3..7f91e8de10 100644 --- a/src/Lean/KeyedDeclsAttribute.lean +++ b/src/Lean/KeyedDeclsAttribute.lean @@ -142,7 +142,7 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDe if c != df.valueTypeName then throwError! "unexpected type at '{declName}', '{df.valueTypeName}' expected" else let env ← getEnv - let env ← liftIO $ declareBuiltin df attrDeclName env key declName + let env ← declareBuiltin df attrDeclName env key declName setEnv env | _ => throwError! "unexpected type at '{declName}', '{df.valueTypeName}' expected", applicationTime := AttributeApplicationTime.afterCompilation diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 01135df4ea..22ef4c9fa2 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -113,10 +113,6 @@ structure Context := abbrev MetaM := ReaderT Context $ StateRefT State CoreM -instance : MonadIO MetaM := { - liftIO := fun x => liftM (liftIO x : CoreM _) -} - instance {α} : Inhabited (MetaM α) := { default := fun _ _ => arbitrary _ } @@ -191,20 +187,20 @@ builtin_initialize isExprDefEqAuxRef : IO.Ref (Expr → Expr → MetaM Bool) ← builtin_initialize synthPendingRef : IO.Ref (MVarId → MetaM Bool) ← IO.mkRef fun _ => pure false def whnf (e : Expr) : m Expr := - liftMetaM $ withIncRecDepth do (← liftIO whnfRef.get) e + liftMetaM $ withIncRecDepth do (← whnfRef.get) e def whnfForall [Monad m] (e : Expr) : m Expr := do let e' ← whnf e if e'.isForall then pure e' else pure e def inferType (e : Expr) : m Expr := - liftMetaM $ withIncRecDepth do (← liftIO inferTypeRef.get) e + liftMetaM $ withIncRecDepth do (← inferTypeRef.get) e protected def isExprDefEqAux (t s : Expr) : MetaM Bool := - withIncRecDepth do (← liftIO isExprDefEqAuxRef.get) t s + withIncRecDepth do (← isExprDefEqAuxRef.get) t s protected def synthPending (mvarId : MVarId) : MetaM Bool := - withIncRecDepth do (← liftIO synthPendingRef.get) mvarId + withIncRecDepth do (← synthPendingRef.get) mvarId -- withIncRecDepth for a monad `n` such that `[MonadControlT MetaM n]` protected def withIncRecDepth {α} (x : n α) : n α := @@ -982,7 +978,7 @@ def ppExprImp (e : Expr) : MetaM Format := do let mctx ← getMCtx let lctx ← getLCtx let opts ← getOptions - liftIO $ Lean.ppExpr { env := env, mctx := mctx, lctx := lctx, opts := opts } e + Lean.ppExpr { env := env, mctx := mctx, lctx := lctx, opts := opts } e def ppExpr (e : Expr) : m Format := liftMetaM $ ppExprImp e diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index bc9329de72..8c84db4b47 100644 --- a/src/Lean/Meta/Instances.lean +++ b/src/Lean/Meta/Instances.lean @@ -38,9 +38,9 @@ def addGlobalInstanceImp (env : Environment) (constName : Name) : IO Environment let (keys, s, _) ← (mkInstanceKey c).toIO {} { env := env } {} {} pure $ instanceExtension.addEntry s.env { keys := keys, val := c } -def addGlobalInstance {m} [Monad m] [MonadEnv m] [MonadIO m] (declName : Name) : m Unit := do +def addGlobalInstance {m} [Monad m] [MonadEnv m] [MonadLiftT IO m] (declName : Name) : m Unit := do let env ← getEnv - let env ← liftIO $ Meta.addGlobalInstanceImp env declName + let env ← Meta.addGlobalInstanceImp env declName setEnv env builtin_initialize diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean index e00498dd93..100dcdfa9e 100644 --- a/src/Lean/Meta/Tactic/Util.lean +++ b/src/Lean/Meta/Tactic/Util.lean @@ -40,7 +40,7 @@ def getMVarType (mvarId : MVarId) : MetaM Expr := do pure (← getMVarDecl mvarId).type def ppGoal (mvarId : MVarId) : MetaM Format := do - liftIO $ Lean.ppGoal { env := (← getEnv), mctx := (← getMCtx), opts := (← getOptions) } mvarId + Lean.ppGoal { env := (← getEnv), mctx := (← getMCtx), opts := (← getOptions) } mvarId builtin_initialize registerTraceClass `Meta.Tactic diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 8e332c2deb..5745efe975 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -476,10 +476,10 @@ private def BuiltinParserAttribute.add (attrName : Name) (catName : Name) let env ← getEnv match decl.type with | Expr.const `Lean.Parser.TrailingParser _ _ => do - let env ← liftIO $ declareTrailingBuiltinParser env catName declName prio + let env ← declareTrailingBuiltinParser env catName declName prio setEnv env | Expr.const `Lean.Parser.Parser _ _ => do - let env ← liftIO $ declareLeadingBuiltinParser env catName declName prio + let env ← declareLeadingBuiltinParser env catName declName prio setEnv env | _ => throwError! "unexpected parser type at '{declName}' (`Parser` or `TrailingParser` expected)" runParserAttributeHooks catName declName (builtin := true) diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index c02254ab82..7364637ff5 100644 --- a/src/Lean/ParserCompiler.lean +++ b/src/Lean/ParserCompiler.lean @@ -87,7 +87,7 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do let env ← getEnv let env ← match env.addAndCompile {} decl with | Except.ok env => pure env - | Except.error kex => do throwError (← liftIO $ (kex.toMessageData {}).toString) + | Except.error kex => do throwError (← (kex.toMessageData {}).toString) setEnv $ ctx.combinatorAttr.setDeclFor env c c' mkCall c' else diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index aea98a6c08..0097b62e02 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -438,9 +438,9 @@ builtin_initialize @[export lean_pretty_printer_formatter_interpret_parser_descr] unsafe def interpretParserDescr : ParserDescr → CoreM Formatter - | ParserDescr.const n => liftIO $ getConstAlias formatterAliasesRef n - | ParserDescr.unary n d => return (← liftIO $ getUnaryAlias formatterAliasesRef n) (← interpretParserDescr d) - | ParserDescr.binary n d₁ d₂ => return (← liftIO $ getBinaryAlias formatterAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂) + | ParserDescr.const n => getConstAlias formatterAliasesRef n + | ParserDescr.unary n d => return (← getUnaryAlias formatterAliasesRef n) (← interpretParserDescr d) + | ParserDescr.binary n d₁ d₂ => return (← getBinaryAlias formatterAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂) | ParserDescr.node k prec d => return node.formatter k (← interpretParserDescr d) | ParserDescr.nodeWithAntiquot _ k d => return node.formatter k (← interpretParserDescr d) | ParserDescr.trailingNode k prec d => return trailingNode.formatter k prec (← interpretParserDescr d) diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index f406a8acd3..328c3a67a6 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -517,9 +517,9 @@ builtin_initialize @[export lean_pretty_printer_parenthesizer_interpret_parser_descr] unsafe def interpretParserDescr : ParserDescr → CoreM Parenthesizer - | ParserDescr.const n => liftIO $ getConstAlias parenthesizerAliasesRef n - | ParserDescr.unary n d => return (← liftIO $ getUnaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d) - | ParserDescr.binary n d₁ d₂ => return (← liftIO $ getBinaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂) + | ParserDescr.const n => getConstAlias parenthesizerAliasesRef n + | ParserDescr.unary n d => return (← getUnaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d) + | ParserDescr.binary n d₁ d₂ => return (← getBinaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂) | ParserDescr.node k prec d => return leadingNode.parenthesizer k prec (← interpretParserDescr d) | ParserDescr.nodeWithAntiquot _ k d => return node.parenthesizer k (← interpretParserDescr d) | ParserDescr.trailingNode k prec d => return trailingNode.parenthesizer k prec (← interpretParserDescr d) diff --git a/src/Lean/Util/MonadCache.lean b/src/Lean/Util/MonadCache.lean index 07e717cf4c..7a71e13bf1 100644 --- a/src/Lean/Util/MonadCache.lean +++ b/src/Lean/Util/MonadCache.lean @@ -71,7 +71,6 @@ instance : MonadHashMapCacheAdapter α β (MonadCacheT α β m) := { instance : Monad (MonadCacheT α β m) := inferInstanceAs (Monad (StateRefT' _ _ _)) instance : MonadLift m (MonadCacheT α β m) := inferInstanceAs (MonadLift m (StateRefT' _ _ _)) -instance [MonadIO m] : MonadIO (MonadCacheT α β m) := inferInstanceAs (MonadIO (StateRefT' _ _ _)) instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (MonadCacheT α β m) := inferInstanceAs (MonadExceptOf ε (StateRefT' _ _ _)) instance : MonadControl m (MonadCacheT α β m) := inferInstanceAs (MonadControl m (StateRefT' _ _ _)) instance [MonadFinally m] : MonadFinally (MonadCacheT α β m) := inferInstanceAs (MonadFinally (StateRefT' _ _ _)) diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index f678dc7fe0..a92e1e062c 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -47,11 +47,11 @@ instance (m n) [MonadTrace m] [MonadLift m n] : MonadTrace n := variables {α : Type} {m : Type → Type} [Monad m] [MonadTrace m] -def printTraces {m} [Monad m] [MonadTrace m] [MonadIO m] : m Unit := do +def printTraces {m} [Monad m] [MonadTrace m] [MonadLiftT IO m] : m Unit := do let traceState ← getTraceState traceState.traces.forM fun m => do - let d ← liftIO m.msg.format - liftIO $ IO.println d + let d ← m.msg.format + IO.println d def resetTraceState {m} [MonadTrace m] : m Unit := modifyTraceState (fun _ => {}) diff --git a/tests/lean/ppExpr.lean b/tests/lean/ppExpr.lean index edf393c0dd..642569acef 100644 --- a/tests/lean/ppExpr.lean +++ b/tests/lean/ppExpr.lean @@ -5,8 +5,8 @@ import Lean open Lean -def test (e : Expr) : MetaM Unit := -PrettyPrinter.ppExpr Name.anonymous [] e >>= IO.println +def test (e : Expr) : MetaM Unit := do + IO.println (← PrettyPrinter.ppExpr Name.anonymous [] e) -- loose bound variable #eval test (mkBVar 0) diff --git a/tests/lean/ppSyntax.lean b/tests/lean/ppSyntax.lean index 76c4d66c46..cc02000351 100644 --- a/tests/lean/ppSyntax.lean +++ b/tests/lean/ppSyntax.lean @@ -2,8 +2,8 @@ import Lean open Lean -def test (stx : Unhygienic Syntax) : MetaM Unit := - PrettyPrinter.ppTerm stx.run >>= IO.println +def test (stx : Unhygienic Syntax) : MetaM Unit := do + IO.println (← PrettyPrinter.ppTerm stx.run) -- test imported `ParserDescr` #eval test `(s!"hi!") diff --git a/tests/lean/run/evalconst.lean b/tests/lean/run/evalconst.lean index 43f1a962ae..697caa6f26 100644 --- a/tests/lean/run/evalconst.lean +++ b/tests/lean/run/evalconst.lean @@ -14,7 +14,7 @@ def f (x : Nat) := x + 1 unsafe def tst2 : CoreM Unit := do let env ← getEnv -let f ← liftIO $ IO.ofExcept $ env.evalConst (Nat → Nat) {} `f +let f ← IO.ofExcept $ env.evalConst (Nat → Nat) {} `f IO.println $ (f 10) #eval tst2 diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean index d7aa814e93..261aeabc56 100644 --- a/tests/lean/run/frontend1.lean +++ b/tests/lean/run/frontend1.lean @@ -6,8 +6,8 @@ open Lean.Elab def runM (input : String) (failIff : Bool := true) : CoreM Unit := do let env ← getEnv; let opts ← getOptions; -let (env, messages) ← liftIO $ process input env opts; -messages.forM $ fun msg => (liftIO msg.toString) >>= IO.println; +let (env, messages) ← process input env opts; +messages.forM fun msg => do IO.println (← msg.toString) when (failIff && messages.hasErrors) $ throwError "errors have been found"; when (!failIff && !messages.hasErrors) $ throwError "there are no errors"; pure () diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean index ebee6a09e9..48c64ea052 100644 --- a/tests/lean/run/termParserAttr.lean +++ b/tests/lean/run/termParserAttr.lean @@ -6,8 +6,8 @@ open Lean.Elab def runCore (input : String) (failIff : Bool := true) : CoreM Unit := do let env ← getEnv; let opts ← getOptions; -let (env, messages) ← liftIO $ process input env opts; -messages.toList.forM $ fun msg => liftIO (msg.toString >>= IO.println); +let (env, messages) ← process input env opts; +messages.toList.forM fun msg => do IO.println (← msg.toString) when (failIff && messages.hasErrors) $ throwError "errors have been found"; when (!failIff && !messages.hasErrors) $ throwError "there are no errors"; pure () diff --git a/tests/lean/typeMismatch.lean.expected.out b/tests/lean/typeMismatch.lean.expected.out index fa2d061a67..a0a68e83f4 100644 --- a/tests/lean/typeMismatch.lean.expected.out +++ b/tests/lean/typeMismatch.lean.expected.out @@ -1,7 +1,7 @@ typeMismatch.lean:7:0: error: type mismatch IO.println "" has type - EIO IO.Error Unit + IO Unit but is expected to have type IO Nat typeMismatch.lean:12:0: error: type mismatch