diff --git a/src/Lean/PrettyPrinter/Delaborator.lean b/src/Lean/PrettyPrinter/Delaborator.lean index 20501b95ca..d4fa0a3e51 100644 --- a/src/Lean/PrettyPrinter/Delaborator.lean +++ b/src/Lean/PrettyPrinter/Delaborator.lean @@ -3,6 +3,7 @@ Copyright (c) 2020 Sebastian Ullrich. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich -/ +import Lean.PrettyPrinter.Delaborator.Options import Lean.PrettyPrinter.Delaborator.SubExpr import Lean.PrettyPrinter.Delaborator.TopDownAnalyze import Lean.PrettyPrinter.Delaborator.Basic diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index fb6aa93d23..84427a4d2c 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -30,174 +30,12 @@ import Lean.ProjFns import Lean.Syntax import Lean.Meta.Match import Lean.Elab.Term +import Lean.PrettyPrinter.Delaborator.Options import Lean.PrettyPrinter.Delaborator.SubExpr import Lean.PrettyPrinter.Delaborator.TopDownAnalyze -namespace Lean +namespace Lean.PrettyPrinter.Delaborator -register_builtin_option pp.all : Bool := { - defValue := false - group := "pp" - descr := "(pretty printer) display coercions, implicit parameters, proof terms, fully qualified names, universe, " ++ - "and disable beta reduction and notations during pretty printing" -} -register_builtin_option pp.notation : Bool := { - defValue := true - group := "pp" - descr := "(pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)" -} -register_builtin_option pp.coercions : Bool := { - defValue := true - group := "pp" - descr := "(pretty printer) hide coercion applications" -} -register_builtin_option pp.universes : Bool := { - defValue := false - group := "pp" - descr := "(pretty printer) display universe" -} -register_builtin_option pp.fullNames : Bool := { - defValue := false - group := "pp" - descr := "(pretty printer) display fully qualified names" -} -register_builtin_option pp.privateNames : Bool := { - defValue := false - group := "pp" - descr := "(pretty printer) display internal names assigned to private declarations" -} -register_builtin_option pp.binderTypes : Bool := { - defValue := false - group := "pp" - descr := "(pretty printer) display types of lambda and Pi parameters" -} -register_builtin_option pp.instantiateMVars : Bool := { - defValue := false -- TODO: default to true? - group := "pp" - descr := "(pretty printer) instantiate mvars before delaborating" -} -register_builtin_option pp.structureInstances : Bool := { - defValue := true - group := "pp" - -- TODO: implement second part - descr := "(pretty printer) display structure instances using the '{ fieldName := fieldValue, ... }' notation " ++ - "or '⟨fieldValue, ... ⟩' if structure is tagged with [pp_using_anonymous_constructor] attribute" -} -register_builtin_option pp.structureProjections : Bool := { - defValue := true - group := "pp" - descr := "(pretty printer) display structure projections using field notation" -} -register_builtin_option pp.explicit : Bool := { - defValue := false - group := "pp" - descr := "(pretty printer) display implicit arguments" -} -register_builtin_option pp.structureInstanceTypes : Bool := { - defValue := false - group := "pp" - descr := "(pretty printer) display type of structure instances" -} -register_builtin_option pp.safeShadowing : Bool := { - defValue := true - group := "pp" - descr := "(pretty printer) allow variable shadowing if there is no collision" -} -register_builtin_option pp.proofs : Bool := { - defValue := false - group := "pp" - descr := "(pretty printer) if set to false, replace proofs appearing as an argument to a function with a placeholder" -} -register_builtin_option pp.proofs.withType : Bool := { - defValue := true - group := "pp" - descr := "(pretty printer) when eliding a proof (see `pp.proofs`), show its type instead" -} -register_builtin_option pp.motives.pi : Bool := { - defValue := true - group := "pp" - descr := "(pretty printer) print all motives that return pi types" -} -register_builtin_option pp.motives.nonConst : Bool := { - defValue := false - group := "pp" - descr := "(pretty printer) print all motives that are not constant functions" -} -register_builtin_option pp.motives.all : Bool := { - defValue := false - group := "pp" - descr := "(pretty printer) print all motives" -} --- TODO: -/- -register_builtin_option g_pp_max_depth : Nat := { - defValue := false - group := "pp" - descr := "(pretty printer) maximum expression depth, after that it will use ellipsis" -} -register_builtin_option g_pp_max_steps : Nat := { - defValue := false - group := "pp" - descr := "(pretty printer) maximum number of visited expressions, after that it will use ellipsis" -} -register_builtin_option g_pp_locals_full_names : Bool := { - defValue := false - group := "pp" - descr := "(pretty printer) show full names of locals" -} -register_builtin_option g_pp_beta : Bool := { - defValue := false - group := "pp" - descr := "(pretty printer) apply beta-reduction when pretty printing" -} -register_builtin_option g_pp_goal_compact : Bool := { - defValue := false - group := "pp" - descr := "(pretty printer) try to display goal in a single line when possible" -} -register_builtin_option g_pp_goal_max_hyps : Nat := { - defValue := false - group := "pp" - descr := "(pretty printer) maximum number of hypotheses to be displayed" -} -register_builtin_option g_pp_instantiate_mvars : Bool := { - defValue := false - group := "pp" - descr := "(pretty printer) instantiate assigned metavariables before pretty printing terms and goals" -} -register_builtin_option g_pp_annotations : Bool := { - defValue := false - group := "pp" - descr := "(pretty printer) display internal annotations (for debugging purposes only)" -} -register_builtin_option g_pp_compact_let : Bool := { - defValue := false - group := "pp" - descr := "(pretty printer) minimal indentation at `let`-declarations" -} --/ - -def getPPAll (o : Options) : Bool := o.get pp.all.name false -def getPPBinderTypes (o : Options) : Bool := o.get pp.binderTypes.name pp.binderTypes.defValue -def getPPCoercions (o : Options) : Bool := o.get pp.coercions.name (!getPPAll o) -def getPPExplicit (o : Options) : Bool := o.get pp.explicit.name (getPPAll o) -def getPPNotation (o : Options) : Bool := o.get pp.notation.name (!getPPAll o) -def getPPStructureProjections (o : Options) : Bool := o.get pp.structureProjections.name (!getPPAll o) -def getPPStructureInstances (o : Options) : Bool := o.get pp.structureInstances.name (!getPPAll o) -def getPPStructureInstanceType (o : Options) : Bool := o.get pp.structureInstanceTypes.name (getPPAll o) -def getPPUniverses (o : Options) : Bool := o.get pp.universes.name (getPPAll o) -def getPPFullNames (o : Options) : Bool := o.get pp.fullNames.name (getPPAll o) -def getPPPrivateNames (o : Options) : Bool := o.get pp.privateNames.name (getPPAll o) -def getPPInstantiateMVars (o : Options) : Bool := o.get pp.instantiateMVars.name pp.instantiateMVars.defValue -def getPPSafeShadowing (o : Options) : Bool := o.get pp.safeShadowing.name pp.safeShadowing.defValue -def getPPProofs (o : Options) : Bool := o.get pp.proofs.name (getPPAll o) -def getPPProofsWithType (o : Options) : Bool := o.get pp.proofs.withType.name pp.proofs.withType.defValue -def getPPMotivesPi (o : Options) : Bool := o.get pp.motives.pi.name pp.motives.pi.defValue -def getPPMotivesNonConst (o : Options) : Bool := o.get pp.motives.nonConst.name pp.motives.nonConst.defValue -def getPPMotivesAll (o : Options) : Bool := o.get pp.motives.all.name pp.motives.all.defValue - -namespace PrettyPrinter -namespace Delaborator open Lean.Meta SubExpr structure Context where @@ -342,20 +180,14 @@ partial def delabFor : Name → Delab partial def delab : Delab := do checkMaxHeartbeats "delab" - unless (← getPPOption getPPProofs) do - let e ← getExpr - -- no need to hide atomic proofs - unless e.isAtomic do - try - let ty ← Meta.inferType (← getExpr) - if ← Meta.isProp ty then - -- TODO: make sure the type is analyzed before this delab - let stx ← withType delab - if ← getPPOption getPPProofsWithType then - return ← ``((_ : $stx)) - else - return ← ``(_) - catch _ => pure () + let e ← getExpr + -- no need to hide atomic proofs + if ← !e.isAtomic <&&> !(← getPPOption getPPProofs) <&&> (try Meta.isProof e catch ex => false) then + if ← getPPOption getPPProofsWithType then + let stx ← withType delab + return ← ``((_ : $stx)) + else + return ← ``(_) let k ← getExprKind let stx ← delabFor k <|> (liftM $ show MetaM Syntax from throwError "don't know how to delaborate '{k}'") if ← getPPOption getPPAnalyzeTypeAscriptions <&&> getPPOption getPPAnalysisNeedsType then @@ -385,15 +217,12 @@ def delab (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (options let mut opts ← MonadOptions.getOptions -- default `pp.proofs` to `true` if `e` is a proof if pp.proofs.get? opts == none then - try - let ty ← Meta.inferType e - if ← Meta.isProp ty then - opts := pp.proofs.set opts true + try if ← Meta.isProof e then opts := pp.proofs.set opts true catch _ => pure () let e ← if getPPInstantiateMVars opts then ← Meta.instantiateMVars e else e let optionsPerPos ← if !getPPAll opts && getPPAnalyze opts && optionsPerPos.isEmpty then - topDownAnalyze e + withTheReader Core.Context (fun ctx => { ctx with options := opts }) do topDownAnalyze e else optionsPerPos catchInternalId Delaborator.delabFailureId (Delaborator.delab.run { defaultOptions := opts, optionsPerPos := optionsPerPos, currNamespace := currNamespace, openDecls := openDecls } (Delaborator.SubExpr.mkRoot e)) @@ -401,5 +230,4 @@ def delab (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (options builtin_initialize registerTraceClass `PrettyPrinter.delab -end PrettyPrinter -end Lean +end Lean.PrettyPrinter diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean new file mode 100644 index 0000000000..39683c8a74 --- /dev/null +++ b/src/Lean/PrettyPrinter/Delaborator/Options.lean @@ -0,0 +1,166 @@ +/- +Copyright (c) 2020 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Ullrich +-/ +import Lean.Data.Options + +namespace Lean + +register_builtin_option pp.all : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) display coercions, implicit parameters, proof terms, fully qualified names, universe, " ++ + "and disable beta reduction and notations during pretty printing" +} +register_builtin_option pp.notation : Bool := { + defValue := true + group := "pp" + descr := "(pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)" +} +register_builtin_option pp.coercions : Bool := { + defValue := true + group := "pp" + descr := "(pretty printer) hide coercion applications" +} +register_builtin_option pp.universes : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) display universe" +} +register_builtin_option pp.fullNames : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) display fully qualified names" +} +register_builtin_option pp.privateNames : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) display internal names assigned to private declarations" +} +register_builtin_option pp.binderTypes : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) display types of lambda and Pi parameters" +} +register_builtin_option pp.instantiateMVars : Bool := { + defValue := false -- TODO: default to true? + group := "pp" + descr := "(pretty printer) instantiate mvars before delaborating" +} +register_builtin_option pp.structureInstances : Bool := { + defValue := true + group := "pp" + -- TODO: implement second part + descr := "(pretty printer) display structure instances using the '{ fieldName := fieldValue, ... }' notation " ++ + "or '⟨fieldValue, ... ⟩' if structure is tagged with [pp_using_anonymous_constructor] attribute" +} +register_builtin_option pp.structureProjections : Bool := { + defValue := true + group := "pp" + descr := "(pretty printer) display structure projections using field notation" +} +register_builtin_option pp.explicit : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) display implicit arguments" +} +register_builtin_option pp.structureInstanceTypes : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) display type of structure instances" +} +register_builtin_option pp.safeShadowing : Bool := { + defValue := true + group := "pp" + descr := "(pretty printer) allow variable shadowing if there is no collision" +} +register_builtin_option pp.proofs : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) if set to false, replace proofs appearing as an argument to a function with a placeholder" +} +register_builtin_option pp.proofs.withType : Bool := { + defValue := true + group := "pp" + descr := "(pretty printer) when eliding a proof (see `pp.proofs`), show its type instead" +} +register_builtin_option pp.motives.pi : Bool := { + defValue := true + group := "pp" + descr := "(pretty printer) print all motives that return pi types" +} +register_builtin_option pp.motives.nonConst : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) print all motives that are not constant functions" +} +register_builtin_option pp.motives.all : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) print all motives" +} +-- TODO: +/- +register_builtin_option g_pp_max_depth : Nat := { + defValue := false + group := "pp" + descr := "(pretty printer) maximum expression depth, after that it will use ellipsis" +} +register_builtin_option g_pp_max_steps : Nat := { + defValue := false + group := "pp" + descr := "(pretty printer) maximum number of visited expressions, after that it will use ellipsis" +} +register_builtin_option g_pp_locals_full_names : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) show full names of locals" +} +register_builtin_option g_pp_beta : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) apply beta-reduction when pretty printing" +} +register_builtin_option g_pp_goal_compact : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) try to display goal in a single line when possible" +} +register_builtin_option g_pp_goal_max_hyps : Nat := { + defValue := false + group := "pp" + descr := "(pretty printer) maximum number of hypotheses to be displayed" +} +register_builtin_option g_pp_annotations : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) display internal annotations (for debugging purposes only)" +} +register_builtin_option g_pp_compact_let : Bool := { + defValue := false + group := "pp" + descr := "(pretty printer) minimal indentation at `let`-declarations" +} +-/ + +def getPPAll (o : Options) : Bool := o.get pp.all.name false +def getPPBinderTypes (o : Options) : Bool := o.get pp.binderTypes.name pp.binderTypes.defValue +def getPPCoercions (o : Options) : Bool := o.get pp.coercions.name (!getPPAll o) +def getPPExplicit (o : Options) : Bool := o.get pp.explicit.name (getPPAll o) +def getPPNotation (o : Options) : Bool := o.get pp.notation.name (!getPPAll o) +def getPPStructureProjections (o : Options) : Bool := o.get pp.structureProjections.name (!getPPAll o) +def getPPStructureInstances (o : Options) : Bool := o.get pp.structureInstances.name (!getPPAll o) +def getPPStructureInstanceType (o : Options) : Bool := o.get pp.structureInstanceTypes.name (getPPAll o) +def getPPUniverses (o : Options) : Bool := o.get pp.universes.name (getPPAll o) +def getPPFullNames (o : Options) : Bool := o.get pp.fullNames.name (getPPAll o) +def getPPPrivateNames (o : Options) : Bool := o.get pp.privateNames.name (getPPAll o) +def getPPInstantiateMVars (o : Options) : Bool := o.get pp.instantiateMVars.name pp.instantiateMVars.defValue +def getPPSafeShadowing (o : Options) : Bool := o.get pp.safeShadowing.name pp.safeShadowing.defValue +def getPPProofs (o : Options) : Bool := o.get pp.proofs.name (getPPAll o) +def getPPProofsWithType (o : Options) : Bool := o.get pp.proofs.withType.name pp.proofs.withType.defValue +def getPPMotivesPi (o : Options) : Bool := o.get pp.motives.pi.name pp.motives.pi.defValue +def getPPMotivesNonConst (o : Options) : Bool := o.get pp.motives.nonConst.name pp.motives.nonConst.defValue +def getPPMotivesAll (o : Options) : Bool := o.get pp.motives.all.name pp.motives.all.defValue + +end Lean diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index 82485f5f55..d900c01b75 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -16,6 +16,7 @@ that are not strictly necessary. import Lean.Meta import Lean.Util.CollectLevelParams import Lean.Util.ReplaceLevel +import Lean.PrettyPrinter.Delaborator.Options import Lean.PrettyPrinter.Delaborator.SubExpr import Std.Data.RBMap @@ -312,20 +313,28 @@ def annotateNamedArg (n : Name) (appPos : Pos) : AnalyzeM Bool := do partial def analyze (parentIsApp : Bool := false) : AnalyzeM Unit := do checkMaxHeartbeats "Delaborator.topDownAnalyze" trace[pp.analyze] "{(← read).knowsType}.{(← read).knowsLevel}" - withReader (fun ctx => { ctx with parentIsApp := parentIsApp }) do - match (← getExpr) with - | Expr.app .. => analyzeApp - | Expr.forallE .. => analyzePi - | Expr.lam .. => analyzeLam - | Expr.const .. => analyzeConst - | Expr.sort .. => analyzeSort - | Expr.proj .. => analyzeProj - | Expr.fvar .. => analyzeFVar - | Expr.mdata .. => analyzeMData - | Expr.letE .. => analyzeLet - | Expr.lit .. => pure () - | Expr.mvar .. => pure () - | Expr.bvar .. => pure () + let e ← getExpr + let opts ← getOptions + + if ← !e.isAtomic <&&> !(getPPProofs opts) <&&> (try Meta.isProof e catch ex => false) then + if getPPProofsWithType opts then + withType $ withKnowing true true $ analyze + else pure () + else + withReader (fun ctx => { ctx with parentIsApp := parentIsApp }) do + match (← getExpr) with + | Expr.app .. => analyzeApp + | Expr.forallE .. => analyzePi + | Expr.lam .. => analyzeLam + | Expr.const .. => analyzeConst + | Expr.sort .. => analyzeSort + | Expr.proj .. => analyzeProj + | Expr.fvar .. => analyzeFVar + | Expr.mdata .. => analyzeMData + | Expr.letE .. => analyzeLet + | Expr.lit .. => pure () + | Expr.mvar .. => pure () + | Expr.bvar .. => pure () where analyzeApp := do let couldBottomUp ← canBottomUp (← getExpr) diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean index 4c6649dfaa..d711d2366c 100644 --- a/tests/lean/run/PPTopDownAnalyze.lean +++ b/tests/lean/run/PPTopDownAnalyze.lean @@ -252,6 +252,18 @@ structure S2 where x : Unit #testDelab (fun (u : Unit) => Eq.refl True) () expecting (fun (u : Unit) => Eq.refl True) () +inductive NeedsAnalysis {α : Type} : Prop + | mk : NeedsAnalysis + +set_option pp.proofs false in +#testDelab @NeedsAnalysis.mk Unit + expecting (_ : NeedsAnalysis (α := Unit)) + +set_option pp.proofs false in +set_option pp.proofs.withType false in +#testDelab @NeedsAnalysis.mk Unit + expecting _ + #testDelabN Nat.brecOn #testDelabN Nat.below #testDelabN Nat.mod_lt