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

feat: expose old pretty printer in Lean

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-07 10:29:10 -08:00
parent 477d53f2dd
commit 091cc48901
2 changed files with 14 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Lean/Util/Message.lean
View file

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

9
src/frontends/lean/pp.cpp
View file

@ -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();
}
}