refactor: pp.analyze needs pp options

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

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

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

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)

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