max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: move parenthesizer and formatter into CoreM

Browse source 
/cc @leodemoura
This commit is contained in:
Sebastian Ullrich 2020-08-21 13:15:32 +02:00
parent 2a1d9b392f
commit 786d90ac80
6 changed files with 53 additions and 210 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/Lean/PrettyPrinter.lean
View file

@ -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 => "<pretty printer error: " ++ toString 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

31
src/Lean/PrettyPrinter/Formatter.lean
View file

@ -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;

182
src/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -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

11
tests/lean/PPRoundtrip.lean
View file

@ -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') "<input>" with
| Except.error e => throwErrorAt stx e
| Except.ok stx'' => do

3
tests/lean/run/Reformat.lean
View file

@ -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) "<foo>";
let (stx', state, messages) := Parser.parseHeader env inputCtx;

11
tests/lean/run/Reparen.lean
View file

@ -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