From 091cc48901dcfc20cec17a6b47b50be8656bc634 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Jan 2020 10:29:10 -0800 Subject: [PATCH] feat: expose old pretty printer in Lean --- src/Init/Lean/Util/Message.lean | 6 +++++- src/frontends/lean/pp.cpp | 9 +++++++++ 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/src/Init/Lean/Util/Message.lean b/src/Init/Lean/Util/Message.lean index b75975e5b1..4e40aad34f 100644 --- a/src/Init/Lean/Util/Message.lean +++ b/src/Init/Lean/Util/Message.lean @@ -52,6 +52,10 @@ registerOption `syntaxMaxDepth { defValue := (2 : Nat), group := "", descr := "m def getSyntaxMaxDepth (opts : Options) : Nat := opts.getNat `syntaxMaxDepth 2 +/- TODO: delete after we implement the new pretty printer in Lean -/ +@[extern "lean_pp_expr"] +constant ppOld : Environment → MetavarContext → LocalContext → Options → Expr → Format := arbitrary _ + partial def formatAux : Option MessageDataContext → MessageData → Format | _, ofFormat fmt => fmt | _, ofLevel u => fmt u @@ -59,7 +63,7 @@ partial def formatAux : Option MessageDataContext → MessageData → Format | some ctx, ofSyntax s => s.formatStx (getSyntaxMaxDepth ctx.opts) | none, ofSyntax s => s.formatStx | none, ofExpr e => format (toString e) -| some ctx, ofExpr e => format (toString (ctx.mctx.instantiateMVars e).1) -- TODO: invoke pretty printer +| some ctx, ofExpr e => ppOld ctx.env ctx.mctx ctx.lctx ctx.opts e -- TODO: replace with new pretty printer | _, withContext ctx d => formatAux (some ctx) d | ctx, tagged cls d => Format.sbracket (format cls) ++ " " ++ formatAux ctx d | ctx, nest n d => Format.nest n (formatAux ctx d) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 76cf06ba1b..dcb3797649 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -1753,4 +1753,13 @@ formatter_factory mk_pretty_formatter_factory() { }); }; } + +format pp(environment const & env, metavar_context const & mctx, local_context const & lctx, options const & opts, expr const & e) { + type_context_old ctx(env, opts, mctx, lctx, transparency_mode::All); + return pretty_fn(env, opts, ctx)(e); +} + +extern "C" object * lean_pp_expr(object * env, object * mctx, object * lctx, object * opts, object * e) { + return pp(environment(env), metavar_context(mctx), local_context(lctx), options(opts), expr(e)).steal(); +} }