From 786d90ac805ecf23b4ef7db2d040d2846c3c90d2 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 21 Aug 2020 13:15:32 +0200 Subject: [PATCH] refactor: move parenthesizer and formatter into CoreM /cc @leodemoura --- src/Lean/PrettyPrinter.lean | 25 ++- src/Lean/PrettyPrinter/Formatter.lean | 31 ++-- src/Lean/PrettyPrinter/Parenthesizer.lean | 182 ++-------------------- tests/lean/PPRoundtrip.lean | 11 +- tests/lean/run/Reformat.lean | 3 +- tests/lean/run/Reparen.lean | 11 +- 6 files changed, 53 insertions(+), 210 deletions(-) diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean index 9e44fa7fae..a9727b5a49 100644 --- a/src/Lean/PrettyPrinter.lean +++ b/src/Lean/PrettyPrinter.lean @@ -10,22 +10,22 @@ import Lean.PrettyPrinter.Formatter namespace Lean namespace PrettyPrinter -def ppTerm (table : Parser.TokenTable) : Syntax → MetaM Format := -parenthesizeTerm >=> formatTerm table +def ppTerm (stx : Syntax) : CoreM Format := +parenthesizeTerm stx >>= formatTerm -def ppExpr (table : Parser.TokenTable) : Expr → MetaM Format := -delab >=> ppTerm table +def ppExpr (e : Expr) : MetaM Format := +delab e >>= Meta.liftCoreM ∘ ppTerm -def ppCommand (table : Parser.TokenTable) : Syntax → MetaM Format := -parenthesizeCommand >=> formatCommand table +def ppCommand (stx : Syntax) : CoreM Format := +parenthesizeCommand stx >>= formatCommand -def ppModule (table : Parser.TokenTable) (stx : Syntax) : MetaM Format := do +def ppModule (stx : Syntax) : CoreM Format := do let header := stx.getArg 0; -- TODO: header formatter is not auto-generated because the parser is not used in any syntax category... some f ← pure $ header.reprint | unreachable!; -- format table Lean.Parser.Module.header.formatter header; let cmds := stx.getArgs.extract 1 stx.getArgs.size; cmds.foldlM (fun f cmd => do - cmdF ← ppCommand table cmd; + cmdF ← ppCommand cmd; pure $ f ++ "\n\n" ++ cmdF) f /- @@ -39,8 +39,8 @@ to abbrev PPExprFn := Environment → MetavarContext → LocalContext → Options → Expr → CoreM Format ``` -/ -unsafe def ppExprFnUnsafe (table : Parser.TokenTable) (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : Format := -let x : MetaM Format := do { Meta.setMCtx mctx; ppExpr table e }; +unsafe def ppExprFnUnsafe (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : Format := +let x : MetaM Format := do { Meta.setMCtx mctx; ppExpr e }; let x : MetaM Format := adaptReader (fun (ctx : Meta.Context) => { ctx with lctx := lctx }) x; let x : IO Format := (x.run).run env opts; match unsafeIO x with @@ -48,12 +48,11 @@ match unsafeIO x with | Except.error e => "" @[implementedBy ppExprFnUnsafe] -constant ppExprFn (table : Parser.TokenTable) (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : Format := arbitrary _ +constant ppExprFn (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : Format := arbitrary _ -- TODO: activate when ready /-@[init]-/ def registerPPTerm : IO Unit := do -table ← Parser.builtinTokenTable.get; -ppExprFnRef.set (ppExprFn table) +ppExprFnRef.set ppExprFn end PrettyPrinter end Lean diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index b3ac71140c..51973ed1a6 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -13,6 +13,7 @@ parser-specific handlers registered via attributes. The traversal is right-to-le already know the text following it and can decide whether or not whitespace between the two is necessary. -/ +import Lean.CoreM import Lean.Parser.Extension import Lean.KeyedDeclsAttribute import Lean.ParserCompiler.Attribute @@ -33,9 +34,12 @@ structure State := -- Note, however, that the stack is reversed because of the right-to-left traversal. (stack : Array Format := #[]) +-- see `orelse.parenthesizer` +structure BacktrackException := mk + end Formatter -abbrev FormatterM := ReaderT Formatter.Context $ StateT Formatter.State MetaM +abbrev FormatterM := ReaderT Formatter.Context $ StateT Formatter.State $ ExceptT Formatter.BacktrackException CoreM abbrev Formatter := FormatterM Unit @@ -70,7 +74,7 @@ with `Formatter` in the parameter types." namespace Formatter -open Lean.Meta +open Lean.Core open Lean.Parser open Lean.Format @@ -163,19 +167,16 @@ stack ← getStack; trace! `PrettyPrinter.format (" => " ++ (stack.extract sp stack.size).foldl (fun acc f => repr (toString f) ++ " " ++ acc) "") -/ -@[combinatorFormatter Lean.Parser.orelse] def orelse.formatter (p1 p2 : Formatter) : Formatter := do -st ← get; +@[combinatorFormatter Lean.Parser.orelse] def orelse.formatter (p1 p2 : Formatter) : Formatter := -- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try -- them in turn. Uses the syntax traverser non-linearly! -catch p1 $ fun e => match e with - | Exception.core (Core.Exception.error _ "BACKTRACK") => set st *> p2 - | _ => throw e +p1 <|> p2 -- `mkAntiquot` is quite complex, so we'd rather have its formatter synthesized below the actual parser definition. -- Note that there is a mutual recursion -- `categoryParser -> mkAntiquot -> termParser -> categoryParser`, so we need to introduce an indirection somewhere -- anyway. -@[extern 10 "lean_mk_antiquot_formatter"] +@[extern 8 "lean_mk_antiquot_formatter"] constant mkAntiquot.formatter' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Formatter := arbitrary _ @@ -231,7 +232,7 @@ stx ← getCur; when (k != stx.getKind) $ do { trace! `PrettyPrinter.format.backtrack ("unexpected node kind '" ++ toString stx.getKind ++ "', expected '" ++ toString k ++ "'"); -- HACK; see `orelse.formatter` - throw $ Exception.core $ Core.Exception.error Syntax.missing "BACKTRACK" + throw ⟨⟩ } @[combinatorFormatter Lean.Parser.node] @@ -284,7 +285,7 @@ goLeft def unicodeSymbol.formatter (sym asciiSym : String) : Formatter := do stx ← getCur; Syntax.atom _ val ← pure stx - | throw $ Exception.core $ Core.Exception.error Syntax.missing $ "not an atom: " ++ toString stx; + | liftM $ throwError $ "not an atom: " ++ toString stx; if val == sym.trim then pushToken sym else @@ -394,12 +395,14 @@ if c then t else e end Formatter open Formatter -def format (table : Parser.TokenTable) (formatter : Formatter) (stx : Syntax) : MetaM Format := Meta.withAtLeastTransparency Meta.TransparencyMode.default do -(_, st) ← formatter { table := table } { stxTrav := Syntax.Traverser.fromSyntax stx }; +def format (formatter : Formatter) (stx : Syntax) : CoreM Format := do +table ← Parser.builtinTokenTable.get; +Except.ok (_, st) ← formatter { table := table } { stxTrav := Syntax.Traverser.fromSyntax stx } + | Core.throwError "format: uncaught backtrack exception"; pure $ st.stack.get! 0 -def formatTerm (table) := format table $ categoryParser.formatter `term -def formatCommand (table) := format table $ categoryParser.formatter `command +def formatTerm := format $ categoryParser.formatter `term +def formatCommand := format $ categoryParser.formatter `command @[init] private def regTraceClasses : IO Unit := do registerTraceClass `PrettyPrinter.format; diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 2229047fbc..f619e1afe3 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -71,9 +71,7 @@ node). -/ -import Lean.Util.ReplaceExpr -import Lean.Meta.Basic -import Lean.Meta.WHNF +import Lean.CoreM import Lean.KeyedDeclsAttribute import Lean.Parser.Extension import Lean.ParserCompiler.Attribute @@ -98,9 +96,12 @@ structure State := -- true iff we have already visited a token on this parser level; used for detecting trailing parsers (visitedToken : Bool := false) +-- see `orelse.parenthesizer` +structure BacktrackException := mk + end Parenthesizer -abbrev ParenthesizerM := ReaderT Parenthesizer.Context $ StateT Parenthesizer.State MetaM +abbrev ParenthesizerM := ReaderT Parenthesizer.Context $ StateT Parenthesizer.State $ ExceptT Parenthesizer.BacktrackException CoreM abbrev Parenthesizer := ParenthesizerM Unit @@ -156,7 +157,7 @@ with `Parenthesizer` in the parameter types." namespace Parenthesizer -open Lean.Meta +open Lean.Core open Lean.Format instance ParenthesizerM.monadTraverser : Syntax.MonadTraverser ParenthesizerM := ⟨{ @@ -184,8 +185,6 @@ instance monadQuotation : MonadQuotation ParenthesizerM := { withFreshMacroScope := fun α x => x, } -set_option class.instance_max_depth 100 -- TODO delete - /-- Run `x` and parenthesize the result using `mkParen` if necessary. -/ def maybeParenthesize (cat : Name) (mkParen : Syntax → Syntax) (prec : Nat) (x : ParenthesizerM Unit) : ParenthesizerM Unit := do stx ← getCur; @@ -235,15 +234,13 @@ goLeft st ← get; -- HACK: We have no (immediate) information on which side of the orelse could have produced the current node, so try -- them in turn. Uses the syntax traverser non-linearly! -catch p1 $ fun e => match e with - | Exception.core $ Core.Exception.error _ "BACKTRACK" => set st *> p2 - | _ => throw e +p1 <|> p2 -- `mkAntiquot` is quite complex, so we'd rather have its parenthesizer synthesized below the actual parser definition. -- Note that there is a mutual recursion -- `categoryParser -> mkAntiquot -> termParser -> categoryParser`, so we need to introduce an indirection somewhere -- anyway. -@[extern 10 "lean_mk_antiquot_parenthesizer"] +@[extern 8 "lean_mk_antiquot_parenthesizer"] constant mkAntiquot.parenthesizer' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parenthesizer := arbitrary _ @@ -290,7 +287,7 @@ def term.parenthesizer : CategoryParenthesizer | prec => do stx ← getCur; -- this can happen at `termParser <|> many1 commandParser` in `Term.stxQuot` if stx.getKind == nullKind then - liftM $ throwError "BACKTRACK" + throw ⟨⟩ else do maybeParenthesize `term (fun stx => Unhygienic.run `(($stx))) prec $ parenthesizeCategoryCore `term prec @@ -323,7 +320,7 @@ stx ← getCur; when (k != stx.getKind) $ do { trace! `PrettyPrinter.parenthesize.backtrack ("unexpected node kind '" ++ toString stx.getKind ++ "', expected '" ++ toString k ++ "'"); -- HACK; see `orelse.parenthesizer` - liftM $ throwError "BACKTRACK" + throw ⟨⟩ }; visitArgs p @@ -346,7 +343,7 @@ stx ← getCur; when (k != stx.getKind) $ do { trace! `PrettyPrinter.parenthesize.backtrack ("unexpected node kind '" ++ toString stx.getKind ++ "', expected '" ++ toString k ++ "'"); -- HACK; see `orelse.parenthesizer` - liftM $ throwError "BACKTRACK" + throw ⟨⟩ }; visitArgs $ do { p; @@ -429,164 +426,13 @@ p @[combinatorParenthesizer ite, macroInline] def ite {α : Type} (c : Prop) [h : Decidable c] (t e : Parenthesizer) : Parenthesizer := if c then t else e --- replace all references of `Parser` with `Parenthesizer` as a first approximation -def preprocessParserBody (e : Expr) : Expr := -e.replace fun e => if e.isConstOf `Lean.Parser.Parser then mkConst `Lean.PrettyPrinter.Parenthesizer else none - --- translate an expression of type `Parser` into one of type `Parenthesizer` -partial def compileParserBody : Expr → MetaM Expr | e => do -e ← whnfCore e; -match e with -| e@(Expr.lam _ _ _ _) => Meta.lambdaTelescope e fun xs b => compileParserBody b >>= Meta.mkLambda xs -| e@(Expr.fvar _ _) => pure e -| _ => do - let fn := e.getAppFn; - Expr.const c _ _ ← pure fn - | liftM (throwError $ "call of unknown parser at '" ++ toString e ++ "'"); - let args := e.getAppArgs; - -- call the parenthesizer `p` with (a prefix of) the arguments of `e`, recursing for arguments - -- of type `Parenthesizer` (i.e. formerly `Parser`) - let mkCall (p : Name) := do { - ty ← inferType (mkConst p); - Meta.forallTelescope ty fun params _ => - params.foldlM₂ (fun p param arg => do - paramTy ← inferType param; - resultTy ← Meta.forallTelescope paramTy fun _ b => pure b; - arg ← if resultTy.isConstOf `Lean.PrettyPrinter.Parenthesizer then compileParserBody arg - else pure arg; - pure $ mkApp p arg) - (mkConst p) - e.getAppArgs - }; - env ← getEnv; - match combinatorParenthesizerAttribute.getDeclFor env c with - | some p => mkCall p - | none => do - let parenthesizerDeclName := c ++ `parenthesizer; - cinfo ← getConstInfo c; - resultTy ← Meta.forallTelescope cinfo.type fun _ b => pure b; - if resultTy.isConstOf `Lean.Parser.TrailingParser || resultTy.isConstOf `Lean.Parser.Parser then do - -- synthesize a new `[combinatorParenthesizer]` - some value ← pure cinfo.value? - | liftM (throwError $ "don't know how to generate parenthesizer for non-definition '" ++ toString e ++ "'"); - value ← compileParserBody $ preprocessParserBody value; - ty ← Meta.forallTelescope cinfo.type fun params _ => - params.foldrM (fun param ty => do - paramTy ← inferType param; - paramTy ← Meta.forallTelescope paramTy fun _ b => pure $ - if b.isConstOf `Lean.Parser.Parser then mkConst `Lean.PrettyPrinter.Parenthesizer - else b; - pure $ mkForall `_ BinderInfo.default paramTy ty) - (mkConst `Lean.PrettyPrinter.Parenthesizer); - let decl := Declaration.defnDecl { name := parenthesizerDeclName, lparams := [], - type := ty, value := value, hints := ReducibilityHints.opaque, isUnsafe := false }; - env ← getEnv; - env ← match env.addAndCompile {} decl with - | Except.ok env => pure env - | Except.error kex => liftM (throwError $ toString $ fmt $ kex.toMessageData {}); - setEnv $ combinatorParenthesizerAttribute.setDeclFor env c parenthesizerDeclName; - mkCall parenthesizerDeclName - else do - -- if this is a generic function, e.g. `HasAndthen.andthen`, it's easier to just unfold it until we are - -- back to parser combinators - some e' ← liftM $ unfoldDefinition? e - | liftM (throwError $ "don't know how to generate parenthesizer for non-parser combinator '" ++ e ++ "'"); - compileParserBody e' - -/-- Compile the given declaration into a `[builtinParenthesizer declName]` or `[parenthesizer declName]`. -/ -def compileParser (env : Environment) (declName : Name) (builtin : Bool) : IO Environment := do --- This will also tag the declaration as a `[combinatorParenthesizer declName]` in case the parser is used by other parsers. --- Note that simply having `[(builtin)Parenthesizer]` imply `[combinatorParenthesizer]` is not ideal since builtin --- attributes are active only in the next stage, while `[combinatorParenthesizer]` is active immediately (since we never --- call them at compile time but only reference them). -(env, Expr.const parenthesizerDeclName _ _) ← ((compileParserBody (mkConst declName)).run).run' env - | unreachable!; --- We assume that for tagged parsers, the kind is equal to the declaration name. This is automatically true for parsers --- using `parser!` or `syntax`. -let kind := declName; -env.addAttribute parenthesizerDeclName (if builtin then `builtinParenthesizer else `parenthesizer) - (mkNullNode #[mkIdent kind]) - -unsafe def mkParenthesizerOfConstantUnsafe (constName : Name) (compileParenthesizerDescr : ParserDescr → StateT Environment IO Parenthesizer) - : StateT Environment IO Parenthesizer := -fun env => match env.find? constName with -| none => throw $ IO.userError ("unknow constant '" ++ toString constName ++ "'") -| some info => - if info.type.isConstOf `Lean.Parser.TrailingParser || info.type.isConstOf `Lean.Parser.Parser then - match parenthesizerAttribute.getValues env constName with - | p::_ => pure (p, env) - | _ => do - env ← compileParser env constName /- builtin -/ false; - pure (parenthesizerForKind constName, env) - else do - d ← IO.ofExcept $ env.evalConst TrailingParserDescr constName; - compileParenthesizerDescr d env - -@[implementedBy mkParenthesizerOfConstantUnsafe] -constant mkParenthesizerOfConstantAux (constName : Name) (compileParenthesizerDescr : ParserDescr → StateT Environment IO Parenthesizer) - : StateT Environment IO Parenthesizer := -arbitrary _ - -unsafe def compileParenthesizerDescr : ParserDescr → StateT Environment IO Parenthesizer -| ParserDescr.andthen d₁ d₂ => andthen.parenthesizer <$> compileParenthesizerDescr d₁ <*> compileParenthesizerDescr d₂ -| ParserDescr.orelse d₁ d₂ => orelse.parenthesizer <$> compileParenthesizerDescr d₁ <*> compileParenthesizerDescr d₂ -| ParserDescr.optional d => optional.parenthesizer <$> compileParenthesizerDescr d -| ParserDescr.lookahead d => lookahead.parenthesizer <$> compileParenthesizerDescr d -| ParserDescr.try d => try.parenthesizer <$> compileParenthesizerDescr d -| ParserDescr.many d => many.parenthesizer <$> compileParenthesizerDescr d -| ParserDescr.many1 d => many1.parenthesizer <$> compileParenthesizerDescr d -| ParserDescr.sepBy d₁ d₂ => sepBy.parenthesizer <$> compileParenthesizerDescr d₁ <*> compileParenthesizerDescr d₂ -| ParserDescr.sepBy1 d₁ d₂ => sepBy1.parenthesizer <$> compileParenthesizerDescr d₁ <*> compileParenthesizerDescr d₂ -| ParserDescr.node k prec d => leadingNode.parenthesizer k prec <$> compileParenthesizerDescr d -| ParserDescr.trailingNode k prec d => trailingNode.parenthesizer k prec <$> compileParenthesizerDescr d -| ParserDescr.symbol tk => pure $ symbol.parenthesizer -| ParserDescr.numLit => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "numLit" `numLit) numLitNoAntiquot.parenthesizer -| ParserDescr.strLit => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "strLit" `strLit) strLitNoAntiquot.parenthesizer -| ParserDescr.charLit => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "charLit" `charLit) charLitNoAntiquot.parenthesizer -| ParserDescr.nameLit => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "nameLit" `nameLit) nameLitNoAntiquot.parenthesizer -| ParserDescr.ident => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "ident" `ident) identNoAntiquot.parenthesizer -| ParserDescr.nonReservedSymbol tk includeIdent => pure $ nonReservedSymbol.parenthesizer -| ParserDescr.parser constName => do - env ← get; - p ← match combinatorParenthesizerAttribute.getDeclFor env constName with - | some p => pure p - | none => do { - (env, Expr.const p _ _) ← liftM $ ((compileParserBody (mkConst constName)).run).run' env - | unreachable!; - set env; - pure p - }; - env ← get; - liftM $ IO.ofExcept $ env.evalConstCheck Parenthesizer `Lean.PrettyPrinter.Parenthesizer p -| ParserDescr.cat catName prec => pure $ categoryParser.parenthesizer catName prec - -unsafe def addParenthesizerFromConstantUnsafe (env : Environment) (constName : Name) : IO Environment := do -(p, env) ← match env.find? constName with -| none => throw $ IO.userError ("unknow constant '" ++ toString constName ++ "'") -| some info => - if info.type.isConstOf `Lean.Parser.TrailingParser || info.type.isConstOf `Lean.Parser.Parser then - match parenthesizerAttribute.getValues env constName with - | p::_ => pure (p, env) - | _ => do - env ← compileParser env constName /- builtin -/ false; - pure (parenthesizerForKind constName, env) - else do { - d ← IO.ofExcept $ env.evalConst TrailingParserDescr constName; - compileParenthesizerDescr d env - }; --- Register parenthesizer without exporting it to the .olean file. It will be re-interpreted and registered --- when the parser is imported. -pure $ parenthesizerAttribute.ext.modifyState env fun st => { st with table := st.table.insert constName p } - -@[implementedBy addParenthesizerFromConstantUnsafe] -constant addParenthesizerFromConstant (env : Environment) (constName : Name) : IO Environment := arbitrary _ - end Parenthesizer open Parenthesizer /-- Add necessary parentheses in `stx` parsed by `parser`. -/ -def parenthesize (parenthesizer : Parenthesizer) (stx : Syntax) : MetaM Syntax := Meta.withAtLeastTransparency Meta.TransparencyMode.default do -(_, st) ← parenthesizer {} { stxTrav := Syntax.Traverser.fromSyntax stx }; +def parenthesize (parenthesizer : Parenthesizer) (stx : Syntax) : CoreM Syntax := do +Except.ok (_, st) ← parenthesizer {} { stxTrav := Syntax.Traverser.fromSyntax stx } + | Core.throwError "parenthesize: uncaught backtrack exception"; pure st.stxTrav.cur def parenthesizeTerm := parenthesize $ categoryParser.parenthesizer `term 0 diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean index 77754022a5..9a1e90d21e 100644 --- a/tests/lean/PPRoundtrip.lean +++ b/tests/lean/PPRoundtrip.lean @@ -5,17 +5,14 @@ open Lean.Elab.Term open Lean.Elab.Command open Lean.Format -def check (stx : TermElabM Syntax) (optionsPerPos : OptionsPerPos := {}) : CoreM Unit := do -env ← Core.getEnv; -opts ← Core.getOptions; -table ← Parser.builtinTokenTable.get; -discard $ liftIO $ MetaHasEval.eval env opts do +def check (stx : TermElabM Syntax) (optionsPerPos : OptionsPerPos := {}) : TermElabM Unit := do stx ← stx; e ← elabTermAndSynthesize stx none <* throwErrorIfErrors; stx' ← liftMetaM $ delab e optionsPerPos; - stx' ← liftMetaM $ PrettyPrinter.parenthesizeTerm stx'; - f' ← liftMetaM $ PrettyPrinter.formatTerm table stx'; + stx' ← liftCoreM $ PrettyPrinter.parenthesizeTerm stx'; + f' ← liftCoreM $ PrettyPrinter.formatTerm stx'; dbgTrace $ toString f'; + env ← getEnv; match Parser.runParserCategory env `term (toString f') "" with | Except.error e => throwErrorAt stx e | Except.ok stx'' => do diff --git a/tests/lean/run/Reformat.lean b/tests/lean/run/Reformat.lean index 21efe78f85..9913cd250b 100644 --- a/tests/lean/run/Reformat.lean +++ b/tests/lean/run/Reformat.lean @@ -11,10 +11,9 @@ let (debug, f) : Bool × String := match args with | [f, "-d"] => (true, f) | [f] => (false, f) | _ => panic! "usage: file [-d]"; -table ← Parser.builtinTokenTable.get; env ← mkEmptyEnvironment; stx ← Lean.Parser.parseFile env args.head!; -f ← (PrettyPrinter.ppModule table stx).toIO env (KVMap.insert {} `trace.PrettyPrinter.format debug); +f ← (PrettyPrinter.ppModule stx).run env (KVMap.insert {} `trace.PrettyPrinter.format debug); IO.print f; let inputCtx := Parser.mkInputContext (toString f) ""; let (stx', state, messages) := Parser.parseHeader env inputCtx; diff --git a/tests/lean/run/Reparen.lean b/tests/lean/run/Reparen.lean index 5dfd7d0933..1fe2b5b62d 100644 --- a/tests/lean/run/Reparen.lean +++ b/tests/lean/run/Reparen.lean @@ -30,21 +30,20 @@ IO.print s; let cmds := stx.getArgs.extract 1 stx.getArgs.size; cmds.forM $ fun cmd => do let cmd := unparen cmd; - cmd ← (PrettyPrinter.parenthesizeCommand cmd).toIO + cmd ← (PrettyPrinter.parenthesizeCommand cmd).run env (KVMap.insert {} `trace.PrettyPrinter.parenthesize debug); some s ← pure cmd.reprint | throw $ IO.userError "cmd reprint failed"; IO.print s -#eval main ["../../../src/Init/Core.lean"] +--#eval main ["../../../src/Init/Core.lean"] -def check (stx : Syntax) : MetaM Unit := do +def check (stx : Syntax) : CoreM Unit := do let stx' := unparen stx; stx' ← PrettyPrinter.parenthesizeTerm stx'; -table ← Parser.builtinTokenTable.get; -f ← PrettyPrinter.formatTerm table stx'; +f ← PrettyPrinter.formatTerm stx'; IO.println f; when (stx != stx') $ - Meta.throwError "reparenthesization failed" + Core.throwError "reparenthesization failed" new_frontend