diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 16e0ee09ff..4a6c3aee89 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -93,6 +93,18 @@ macro "Σ'" xs:explicitBinders ", " b:term : term => expandExplicitBinders `PSig
macro:35 xs:bracketedExplicitBinders " × " b:term:35 : term => expandBrackedBinders `Sigma xs b
macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBinders `PSigma xs b
+@[appUnexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
+ | `(Unit.unit) => `(())
+ | _ => throw ()
+
+@[appUnexpander Eq.ndrec] def unexpandEqNDRec : Lean.PrettyPrinter.Unexpander
+ | `(Eq.ndrec $m $h) => `($h ▸ $m)
+ | _ => throw ()
+
+@[appUnexpander Eq.rec] def unexpandEqRec : Lean.PrettyPrinter.Unexpander
+ | `(Eq.rec $m $h) => `($h ▸ $m)
+ | _ => throw ()
+
@[appUnexpander Exists] def unexpandExists : Lean.PrettyPrinter.Unexpander
| `(Exists fun $x:ident => ∃ $xs:binderIdent*, $b) => `(∃ $x:ident $xs:binderIdent*, $b)
| `(Exists fun $x:ident => $b) => `(∃ $x:ident, $b)
@@ -139,7 +151,7 @@ macro_rules
attribute [instance] C.mk
```
-/
-syntax declModifiers "class " "abbrev " declId bracketedBinder* (":" term)?
+syntax declModifiers "class " "abbrev " declId bracketedBinder* (":" term)?
":=" withPosition(group(colGe term ","?)*) : command
macro_rules
diff --git a/src/Lean/Elab/Exception.lean b/src/Lean/Elab/Exception.lean
index f1e49c6829..80d788bdce 100644
--- a/src/Lean/Elab/Exception.lean
+++ b/src/Lean/Elab/Exception.lean
@@ -59,8 +59,8 @@ def isAbortTacticException (ex : Exception) : Bool :=
def isAbortExceptionId (id : InternalExceptionId) : Bool :=
id == abortCommandExceptionId || id == abortTermExceptionId || id == abortTacticExceptionId
-def mkMessageCore (fileName : String) (fileMap : FileMap) (msgData : MessageData) (severity : MessageSeverity) (pos : String.Pos) : Message :=
- let pos := fileMap.toPosition pos
- { fileName := fileName, pos := pos, data := msgData, severity := severity }
+def mkMessageCore (fileName : String) (fileMap : FileMap) (msgData : MessageData) (severity : MessageSeverity) (rawPos : String.Pos) : Message :=
+ let pos := fileMap.toPosition rawPos
+ { fileName := fileName, rawPos := rawPos, pos := pos, data := msgData, severity := severity }
end Lean.Elab
diff --git a/src/Lean/Elab/Import.lean b/src/Lean/Elab/Import.lean
index 18cab54e25..cbee37a3e3 100644
--- a/src/Lean/Elab/Import.lean
+++ b/src/Lean/Elab/Import.lean
@@ -23,7 +23,7 @@ def processHeader (header : Syntax) (opts : Options) (messages : MessageLog) (in
let env ← mkEmptyEnvironment
let spos := header.getPos?.getD 0
let pos := inputCtx.fileMap.toPosition spos
- pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos })
+ pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, rawPos := spos, pos := pos })
def parseImports (input : String) (fileName : Option String := none) : IO (List Import × Position × MessageLog) := do
let fileName := fileName.getD ""
diff --git a/src/Lean/Elab/Log.lean b/src/Lean/Elab/Log.lean
index 14ff6f7176..4dc107fbd8 100644
--- a/src/Lean/Elab/Log.lean
+++ b/src/Lean/Elab/Log.lean
@@ -39,7 +39,7 @@ def logAt (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity :=
let endPos := ref.getTailPos?.getD pos
let fileMap ← getFileMap
let msgData ← addMessageContext msgData
- logMessage { fileName := (← getFileName), pos := fileMap.toPosition pos, endPos := fileMap.toPosition endPos, data := msgData, severity := severity }
+ logMessage { fileName := (← getFileName), rawPos := pos, pos := fileMap.toPosition pos, endPos := fileMap.toPosition endPos, data := msgData, severity := severity }
def logErrorAt (ref : Syntax) (msgData : MessageData) : m Unit :=
logAt ref msgData MessageSeverity.error
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 39b3e0bf3d..a9e952bf66 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1330,7 +1330,7 @@ def isLocalIdent? (stx : Syntax) : TermElabM (Option Expr) :=
def mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM Expr := do
let cinfo ← getConstInfo constName
if explicitLevels.length > cinfo.levelParams.length then
- throwError "too many explicit universe levels"
+ throwError "too many explicit universe levels for '{constName}'"
else
let numMissingLevels := cinfo.levelParams.length - explicitLevels.length
let us ← mkFreshLevelMVars numMissingLevels
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 4698888d79..5245df8149 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -169,6 +169,7 @@ end MessageData
structure Message where
fileName : String
+ rawPos : Nat
pos : Position
endPos : Option Position := none
severity : MessageSeverity := MessageSeverity.error
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index fb46c1cf98..79e46315f5 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -826,13 +826,13 @@ def getParamNames (declName : Name) : MetaM (Array Name) := do
-- `kind` specifies the metavariable kind for metavariables not corresponding to instance implicit `[ ... ]` arguments.
private partial def forallMetaTelescopeReducingAux
- (e : Expr) (reducing : Bool) (maxMVars? : Option Nat) (kind : MetavarKind) : MetaM (Array Expr × Array BinderInfo × Expr) :=
+ (e : Expr) (reducing : Bool) (maxMVars? : Option Nat) (kind : MetavarKind) (instsSynthetic : Bool) : MetaM (Array Expr × Array BinderInfo × Expr) :=
let rec process (mvars : Array Expr) (bis : Array BinderInfo) (j : Nat) (type : Expr) : MetaM (Array Expr × Array BinderInfo × Expr) := do
match type with
| Expr.forallE n d b c =>
let cont : Unit → MetaM (Array Expr × Array BinderInfo × Expr) := fun _ => do
let d := d.instantiateRevRange j mvars.size mvars
- let k := if c.binderInfo.isInstImplicit then MetavarKind.synthetic else kind
+ let k := if c.binderInfo.isInstImplicit && instsSynthetic then MetavarKind.synthetic else kind
let mvar ← mkFreshExprMVar d k n
let mvars := mvars.push mvar
let bis := bis.push c.binderInfo
@@ -859,11 +859,16 @@ private partial def forallMetaTelescopeReducingAux
/-- Similar to `forallTelescope`, but creates metavariables instead of free variables. -/
def forallMetaTelescope (e : Expr) (kind := MetavarKind.natural) : MetaM (Array Expr × Array BinderInfo × Expr) :=
- forallMetaTelescopeReducingAux e (reducing := false) (maxMVars? := none) kind
+ forallMetaTelescopeReducingAux e (reducing := false) (maxMVars? := none) (instsSynthetic := true) kind
/-- Similar to `forallTelescopeReducing`, but creates metavariables instead of free variables. -/
def forallMetaTelescopeReducing (e : Expr) (maxMVars? : Option Nat := none) (kind := MetavarKind.natural) : MetaM (Array Expr × Array BinderInfo × Expr) :=
- forallMetaTelescopeReducingAux e (reducing := true) maxMVars? kind
+ forallMetaTelescopeReducingAux e (reducing := true) maxMVars? kind (instsSynthetic := true)
+
+/-- Similar to `forallMetaTelescopeReducing`, stops constructing the telescope when
+ it reaches size `maxMVars`. -/
+def forallMetaBoundedTelescope (e : Expr) (maxMVars : Nat) (kind : MetavarKind := MetavarKind.natural) (instsSynthetic : Bool := true) : MetaM (Array Expr × Array BinderInfo × Expr) :=
+ forallMetaTelescopeReducingAux e (reducing := true) (maxMVars? := some maxMVars) (kind := kind) (instsSynthetic := instsSynthetic)
/-- Similar to `forallMetaTelescopeReducingAux` but for lambda expressions. -/
partial def lambdaMetaTelescope (e : Expr) (maxMVars? : Option Nat := none) : MetaM (Array Expr × Array BinderInfo × Expr) :=
diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean
index f12cd4929f..a59ae1c630 100644
--- a/src/Lean/Parser/Module.lean
+++ b/src/Lean/Parser/Module.lean
@@ -33,9 +33,9 @@ structure ModuleParserState where
recovering : Bool := false
deriving Inhabited
-private def mkErrorMessage (c : ParserContext) (pos : String.Pos) (errorMsg : String) : Message :=
- let pos := c.fileMap.toPosition pos
- { fileName := c.fileName, pos := pos, data := errorMsg }
+private def mkErrorMessage (c : ParserContext) (rawPos : String.Pos) (errorMsg : String) : Message :=
+ let pos := c.fileMap.toPosition rawPos
+ { fileName := c.fileName, rawPos := rawPos, pos := pos, data := errorMsg }
def parseHeader (inputCtx : InputContext) : IO (Syntax × ModuleParserState × MessageLog) := do
let dummyEnv ← mkEmptyEnvironment
diff --git a/src/Lean/PrettyPrinter/Delaborator.lean b/src/Lean/PrettyPrinter/Delaborator.lean
index 41be185991..20501b95ca 100644
--- a/src/Lean/PrettyPrinter/Delaborator.lean
+++ b/src/Lean/PrettyPrinter/Delaborator.lean
@@ -3,5 +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.SubExpr
+import Lean.PrettyPrinter.Delaborator.TopDownAnalyze
import Lean.PrettyPrinter.Delaborator.Basic
import Lean.PrettyPrinter.Delaborator.Builtins
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index fdef10b5d6..9d65b08a35 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -30,6 +30,8 @@ import Lean.ProjFns
import Lean.Syntax
import Lean.Meta.Match
import Lean.Elab.Term
+import Lean.PrettyPrinter.Delaborator.SubExpr
+import Lean.PrettyPrinter.Delaborator.TopDownAnalyze
namespace Lean
@@ -54,29 +56,29 @@ register_builtin_option pp.universes : Bool := {
group := "pp"
descr := "(pretty printer) display universe"
}
-register_builtin_option pp.full_names : Bool := {
+register_builtin_option pp.fullNames : Bool := {
defValue := false
group := "pp"
descr := "(pretty printer) display fully qualified names"
}
-register_builtin_option pp.private_names : Bool := {
+register_builtin_option pp.privateNames : Bool := {
defValue := false
group := "pp"
descr := "(pretty printer) display internal names assigned to private declarations"
}
-register_builtin_option pp.binder_types : Bool := {
- defValue := false
+register_builtin_option pp.binderTypes : Bool := {
+ defValue := true
group := "pp"
descr := "(pretty printer) display types of lambda and Pi parameters"
}
-register_builtin_option pp.structure_instances : Bool := {
+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.structure_projections : Bool := {
+register_builtin_option pp.structureProjections : Bool := {
defValue := true
group := "pp"
descr := "(pretty printer) display structure projections using field notation"
@@ -86,12 +88,12 @@ register_builtin_option pp.explicit : Bool := {
group := "pp"
descr := "(pretty printer) display implicit arguments"
}
-register_builtin_option pp.structure_instance_type : Bool := {
+register_builtin_option pp.structureInstanceTypes : Bool := {
defValue := false
group := "pp"
descr := "(pretty printer) display type of structure instances"
}
-register_builtin_option pp.safe_shadowing : Bool := {
+register_builtin_option pp.safeShadowing : Bool := {
defValue := true
group := "pp"
descr := "(pretty printer) allow variable shadowing if there is no collision"
@@ -170,37 +172,29 @@ register_builtin_option g_pp_compact_let : Bool := {
}
-/
-def getPPAll (o : Options) : Bool := o.get `pp.all false
-def getPPBinderTypes (o : Options) : Bool := o.get `pp.binder_types true
-def getPPCoercions (o : Options) : Bool := o.get `pp.coercions (!getPPAll o)
-def getPPExplicit (o : Options) : Bool := o.get `pp.explicit (getPPAll o)
-def getPPNotation (o : Options) : Bool := o.get `pp.notation (!getPPAll o)
-def getPPStructureProjections (o : Options) : Bool := o.get `pp.structure_projections (!getPPAll o)
-def getPPStructureInstances (o : Options) : Bool := o.get `pp.structure_instances (!getPPAll o)
-def getPPStructureInstanceType (o : Options) : Bool := o.get `pp.structure_instance_type (getPPAll o)
-def getPPUniverses (o : Options) : Bool := o.get `pp.universes (getPPAll o)
-def getPPFullNames (o : Options) : Bool := o.get `pp.full_names (getPPAll o)
-def getPPPrivateNames (o : Options) : Bool := o.get `pp.private_names (getPPAll o)
-def getPPUnicode (o : Options) : Bool := o.get `pp.unicode true
-def getPPSafeShadowing (o : Options) : Bool := o.get `pp.safe_shadowing true
-def getPPProofs (o : Options) : Bool := o.get pp.proofs.name (getPPAll o)
-def getPPProofsWithType (o : Options) : Bool := o.get pp.proofs.withType.name true
+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 || getPPAnalyze 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 getPPSafeShadowing (o : Options) : Bool := o.get pp.safeShadowing.name pp.safeShadowing.defValue
+def getPPProofs (o : Options) : Bool := o.get pp.proofs.name (getPPAll o || getPPAnalyze 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
-/-- Associate pretty printer options to a specific subterm using a synthetic position. -/
-abbrev OptionsPerPos := Std.RBMap Nat Options compare
-
namespace PrettyPrinter
namespace Delaborator
-open Lean.Meta
+open Lean.Meta SubExpr
structure Context where
- -- In contrast to other systems like the elaborator, we do not pass the current term explicitly as a
- -- parameter, but store it in the monad so that we can keep it in sync with `pos`.
- expr : Expr
- pos : Nat := 1
defaultOptions : Options
optionsPerPos : OptionsPerPos
currNamespace : Name
@@ -211,7 +205,7 @@ structure Context where
-- the delaborator was able to produce a Syntax object.
builtin_initialize delabFailureId : InternalExceptionId ← registerInternalExceptionId `delabFailure
-abbrev DelabM := ReaderT Context MetaM
+abbrev DelabM := ReaderT Context (ReaderT SubExpr MetaM)
abbrev Delab := DelabM Syntax
instance {α} : Inhabited (DelabM α) where
@@ -251,10 +245,6 @@ unsafe def mkDelabAttribute : IO (KeyedDeclsAttribute Delab) :=
} `Lean.PrettyPrinter.Delaborator.delabAttribute
@[builtinInit mkDelabAttribute] constant delabAttribute : KeyedDeclsAttribute Delab
-def getExpr : DelabM Expr := do
- let ctx ← read
- pure ctx.expr
-
def getExprKind : DelabM Name := do
let e ← getExpr
pure $ match e with
@@ -277,14 +267,17 @@ def getExprKind : DelabM Name := do
| _ => `mdata
| Expr.proj _ _ _ _ => `proj
-/-- Evaluate option accessor, using subterm-specific options if set. -/
-def getPPOption (opt : Options → Bool) : DelabM Bool := do
+def getOptionsAtCurrPos : DelabM Options := do
let ctx ← read
let mut opts := ctx.defaultOptions
- if let some opts' ← ctx.optionsPerPos.find? ctx.pos then
+ if let some opts' ← ctx.optionsPerPos.find? (← getPos) then
for (k, v) in opts' do
opts := opts.insert k v
- return opt opts
+ opts
+
+/-- Evaluate option accessor, using subterm-specific options if set. -/
+def getPPOption (opt : Options → Bool) : DelabM Bool := do
+ return opt (← getOptionsAtCurrPos)
def whenPPOption (opt : Options → Bool) (d : Delab) : Delab := do
let b ← getPPOption opt
@@ -294,50 +287,6 @@ def whenNotPPOption (opt : Options → Bool) (d : Delab) : Delab := do
let b ← getPPOption opt
if b then failure else d
-/--
-Descend into `child`, the `childIdx`-th subterm of the current term, and update position.
-
-Because `childIdx < 3` in the case of `Expr`, we can injectively map a path
-`childIdxs` to a natural number by computing the value of the 3-ary representation
-`1 :: childIdxs`, since n-ary representations without leading zeros are unique.
-Note that `pos` is initialized to `1` (case `childIdxs == []`).
--/
-def descend {α} (child : Expr) (childIdx : Nat) (d : DelabM α) : DelabM α :=
- withReader (fun cfg => { cfg with expr := child, pos := cfg.pos * 3 + childIdx }) d
-
-def withAppFn {α} (d : DelabM α) : DelabM α := do
- let Expr.app fn _ _ ← getExpr | unreachable!
- descend fn 0 d
-
-def withAppArg {α} (d : DelabM α) : DelabM α := do
- let Expr.app _ arg _ ← getExpr | unreachable!
- descend arg 1 d
-
-partial def withAppFnArgs {α} : DelabM α → (α → DelabM α) → DelabM α
- | fnD, argD => do
- let Expr.app fn arg _ ← getExpr | fnD
- let a ← withAppFn (withAppFnArgs fnD argD)
- withAppArg (argD a)
-
-def withBindingDomain {α} (d : DelabM α) : DelabM α := do
- let e ← getExpr
- descend e.bindingDomain! 0 d
-
-def withBindingBody {α} (n : Name) (d : DelabM α) : DelabM α := do
- let e ← getExpr
- withLocalDecl n e.binderInfo e.bindingDomain! fun fvar =>
- let b := e.bindingBody!.instantiate1 fvar
- descend b 1 d
-
-def withProj {α} (d : DelabM α) : DelabM α := do
- let Expr.proj _ _ e _ ← getExpr | unreachable!
- descend e 0 d
-
-def withMDataExpr {α} (d : DelabM α) : DelabM α := do
- let Expr.mdata _ e _ ← getExpr | unreachable!
- -- do not change position so that options on an mdata are automatically forwarded to the child
- withReader ({ · with expr := e }) d
-
partial def annotatePos (pos : Nat) : Syntax → Syntax
| stx@(Syntax.ident _ _ _ _) => stx.setInfo (SourceInfo.synthetic pos pos)
-- app => annotate function
@@ -348,8 +297,7 @@ partial def annotatePos (pos : Nat) : Syntax → Syntax
| none => stx
def annotateCurPos (stx : Syntax) : Delab := do
- let ctx ← read
- pure $ annotatePos ctx.pos stx
+ annotatePos (← getPos) stx
def getUnusedName (suggestion : Name) (body : Expr) : DelabM Name := do
-- Use a nicer binder name than `[anonymous]`. We probably shouldn't do this in all LocalContext use cases, so do it here.
@@ -387,6 +335,7 @@ partial def delabFor : Name → Delab
delabFor k.getRoot
partial def delab : Delab := do
+ checkMaxHeartbeats "delab"
unless (← getPPOption getPPProofs) do
let e ← getExpr
-- no need to hide atomic proofs
@@ -400,7 +349,11 @@ partial def delab : Delab := do
return ← ``(_)
catch _ => pure ()
let k ← getExprKind
- delabFor k <|> (liftM $ show MetaM Syntax from throwError "don't know how to delaborate '{k}'")
+ let stx ← delabFor k <|> (liftM $ show MetaM Syntax from throwError "don't know how to delaborate '{k}'")
+ if ← getPPOption getPPAnalyzeTypeAscriptions <&&> getPPOption getPPAnalysisNeedsType <&&> (pure (← getExpr).isApp) then
+ let typeStx ← withAppType delab
+ `(show $typeStx:term from $stx:term) >>= annotateCurPos
+ else stx
unsafe def mkAppUnexpanderAttribute : IO (KeyedDeclsAttribute Unexpander) :=
KeyedDeclsAttribute.init {
@@ -416,6 +369,8 @@ to true or `pp.notation` is set to false, it will not be called at all.",
end Delaborator
+open Delaborator (OptionsPerPos topDownAnalyze)
+
/-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/
def delab (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM Syntax := do
trace[PrettyPrinter.delab.input] "{Std.format e}"
@@ -427,8 +382,12 @@ def delab (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (options
if ← Meta.isProp ty then
opts := pp.proofs.set opts true
catch _ => pure ()
+ let optionsPerPos ←
+ if getPPAnalyze opts && optionsPerPos.isEmpty then
+ topDownAnalyze e
+ else optionsPerPos
catchInternalId Delaborator.delabFailureId
- (Delaborator.delab.run { expr := e, defaultOptions := opts, optionsPerPos := optionsPerPos, currNamespace := currNamespace, openDecls := openDecls })
+ (Delaborator.delab.run { defaultOptions := opts, optionsPerPos := optionsPerPos, currNamespace := currNamespace, openDecls := openDecls } (Delaborator.SubExpr.mkRoot e))
(fun _ => unreachable!)
builtin_initialize registerTraceClass `PrettyPrinter.delab
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 13645a5b86..ed3a5618af 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -5,11 +5,14 @@ Authors: Sebastian Ullrich
-/
import Lean.PrettyPrinter.Delaborator.Basic
+import Lean.PrettyPrinter.Delaborator.SubExpr
+import Lean.PrettyPrinter.Delaborator.TopDownAnalyze
import Lean.Parser
namespace Lean.PrettyPrinter.Delaborator
open Lean.Meta
open Lean.Parser.Term
+open SubExpr
@[builtinDelab fvar]
def delabFVar : Delab := do
@@ -55,38 +58,65 @@ private def unresolveQualifiedName (ns : Name) (c : Name) : DelabM Name := do
guard $ c' != c && !c'.isAnonymous && (!c'.isAtomic || !isProtected env c)
pure c'
-private def unresolveUsingNamespace (c : Name) : Name → DelabM Name
- | ns@(Name.str p _ _) => unresolveQualifiedName ns c <|> unresolveUsingNamespace c p
- | _ => failure
+private def checkForNameClash (nsOrig nsPfix candidate : Name) : DelabM Unit := do
+ -- Suppose the current namespace is `Foo.Bar`, we are delaborating `Foo.rig`, and `Foo.Bar.rig`
+ -- already exists. This function will detect the clash and fail.
+ let rest := nsOrig.components.drop nsPfix.components.length
+ let mut nsPfix := nsPfix
+ for component in rest do
+ nsPfix := nsPfix ++ component
+ let candidate := nsPfix ++ candidate
+ -- TODO: what are the elab rules for 'protected' declarations?
+ guard ((← getEnv).find? candidate |>.isNone)
+
+private partial def unresolveUsingNamespace (c ns : Name) : DelabM Name := core ns where
+ core
+ | nsPfix@(Name.str p _ _) =>
+ (do let candidate ← unresolveQualifiedName nsPfix c; checkForNameClash ns nsPfix candidate; candidate)
+ <|> core p
+ | _ => failure
private def unresolveOpenDecls (c : Name) : List OpenDecl → DelabM Name
| [] => failure
| OpenDecl.simple ns exs :: openDecls =>
let c' := c.replacePrefix ns Name.anonymous
- if c' != c && exs.elem c' then unresolveOpenDecls c openDecls
- else
- unresolveQualifiedName ns c <|> unresolveOpenDecls c openDecls
+ if c' == c || exs.elem c' then unresolveOpenDecls c openDecls
+ else unresolveQualifiedName ns c <|> unresolveOpenDecls c openDecls
| OpenDecl.explicit openedId resolvedId :: openDecls =>
- guard (c == resolvedId) *> pure openedId <|> unresolveOpenDecls c openDecls
+ (guard (c == resolvedId) *> pure openedId) <|> unresolveOpenDecls c openDecls
-- NOTE: not a registered delaborator, as `const` is never called (see [delab] description)
def delabConst : Delab := do
let Expr.const c ls _ ← getExpr | unreachable!
let c₀ := c
- let mut c ← if (← getPPOption getPPFullNames) then pure c else
- let ctx ← read
+ let ctx ← read
+ let maybeAddRoot (c : Name) : DelabM Name := do
+ (do checkForNameClash ctx.currNamespace Name.anonymous c
+ pure c)
+ <|>
+ (do guard (c == c₀)
+ guard (! (← read).inPattern)
+ guard ((← getEnv).contains c)
+ pure (`_root_ ++ c))
+ <|> (pure c₀)
+
+ let mut c ← if (← getPPOption getPPFullNames) then maybeAddRoot c else
let env ← getEnv
let as := getRevAliases env c
-- might want to use a more clever heuristic such as selecting the shortest alias...
let c := as.headD c
- unresolveUsingNamespace c ctx.currNamespace <|> unresolveOpenDecls c ctx.openDecls <|> pure c
+ unresolveUsingNamespace c ctx.currNamespace
+ <|> unresolveOpenDecls c ctx.openDecls
+ <|> maybeAddRoot c
+
unless (← getPPOption getPPPrivateNames) do
c := (privateToUserName? c).getD c
+
let ppUnivs ← getPPOption getPPUniverses
if ls.isEmpty || !ppUnivs then
if (← getLCtx).usesUserName c then
-- `c` is also a local declaration
- if c == c₀ then
+ if c == c₀ && !(← read).inPattern then
-- `c` is the fully qualified named. So, we append the `_root_` prefix
c := `_root_ ++ c
else
@@ -115,7 +145,7 @@ def getParamKinds (e : Expr) : MetaM (Array ParamKind) := do
pure ParamKind.explicit
@[builtinDelab app]
-def delabAppExplicit : Delab := do
+def delabAppExplicit : Delab := whenPPOption getPPExplicit do
let (fnStx, argStxs) ← withAppFnArgs
(do
let fn ← getExpr
@@ -128,24 +158,67 @@ def delabAppExplicit : Delab := do
pure (fnStx, argStxs.push argStx))
Syntax.mkApp fnStx argStxs
-def shouldShowMotive (motive : Expr) (opts : Options) : Bool :=
+def shouldShowMotive (motive : Expr) (opts : Options) : MetaM Bool := do
getPPMotivesAll opts
- || (getPPMotivesPi opts && returnsPi motive)
- || (getPPMotivesNonConst opts && isNonConstFun motive)
- where
- returnsPi (motive : Expr) : Bool := do
- match motive with
- | Expr.lam name d b _ => returnsPi b
- | Expr.forallE .. => true
- | _ => false
-
- isNonConstFun (motive : Expr) : Bool := do
- match motive with
- | Expr.lam name d b _ => isNonConstFun b
- | _ => motive.hasLooseBVars
+ <||> (← getPPMotivesPi opts <&&> returnsPi motive)
+ <||> (← getPPMotivesNonConst opts <&&> isNonConstFun motive)
+
+def isRegularApp : DelabM Bool := do
+ let e ← getExpr
+ if not e.getAppFn.isConst then return false
+ if ← withNaryFn (getPPOption getPPUniverses <||> getPPOption getPPExplicit) then return false
+ for i in [:e.getAppNumArgs] do
+ if ← withNaryArg i (getPPOption getPPAnalysisNamedArg) then return false
+ return true
+
+def unexpandRegularApp (stx : Syntax) : Delab := do
+ let Expr.const c .. ← pure (← getExpr).getAppFn | unreachable!
+ let fs ← appUnexpanderAttribute.getValues (← getEnv) c
+ fs.firstM fun f =>
+ match f stx |>.run () with
+ | EStateM.Result.ok stx _ => pure stx
+ | _ => failure
+
+-- abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β
+-- abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a
+def unexpandCoe (stx : Syntax) : Delab := whenPPOption getPPCoercions do
+ if not (← isCoe) then failure
+ let e ← getExpr
+ match stx with
+ | `($fn $arg) => arg
+ | `($fn $args*) => `($(args.get! 0) $(args.eraseIdx 0)*)
+ | _ => failure
+where
+ isCoe : DelabM Bool := do
+ let e ← getExpr
+ e.isAppOfArity `coe 4 || e.isAppOfArity `coeFun 4
+
+def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStructureInstances do
+ let env ← getEnv
+ let e ← getExpr
+ let some s ← pure $ e.isConstructorApp? env | failure
+ guard $ isStructure env s.induct;
+ /- If implicit arguments should be shown, and the structure has parameters, we should not
+ pretty print using { ... }, because we will not be able to see the parameters. -/
+ let fieldNames := getStructureFields env s.induct
+ let mut fields := #[]
+ guard $ fieldNames.size == stx[1].getNumArgs
+ for idx in [:fieldNames.size] do
+ let field ← `(structInstField|$(mkIdent <| fieldNames.get! idx):ident := $(stx[1][idx]):term)
+ fields := fields.push field
+ let lastField := fields.back
+ fields := fields.pop
+ let tyStx ← withAppType do
+ if (← getPPOption getPPStructureInstanceType) then delab >>= pure ∘ some else pure none
+ `({ $[$fields, ]* $lastField $[: $tyStx]? })
@[builtinDelab app]
-def delabAppImplicit : Delab := whenNotPPOption getPPExplicit do
+def delabAppImplicit : Delab := do
+ -- TODO: always call the unexpanders, make them guard on the right # args?
+ if ← getPPOption getPPExplicit then
+ let paramKinds ← liftM <| getParamKinds (← getExpr).getAppFn <|> pure #[]
+ if paramKinds.any (fun | ParamKind.explicit => false | _ => true) then failure
+
let (fnStx, _, argStxs) ← withAppFnArgs
(do
let fn ← getExpr
@@ -157,44 +230,57 @@ def delabAppImplicit : Delab := whenNotPPOption getPPExplicit do
let opts ← getOptions
let mkNamedArg (name : Name) (argStx : Syntax) : DelabM Syntax := do
`(Parser.Term.namedArgument| ($(← mkIdent name):ident := $argStx:term))
- let stx ← delab
- let argStx? : Option Syntax ← match paramKinds with
- | [ParamKind.implicit _ (some v)] =>
- if !v.hasLooseBVars && v == arg then none else stx
- | ParamKind.implicit name none :: _ => do
- if name == `motive && shouldShowMotive arg opts
- then mkNamedArg name stx
- else none
- | _ => some stx
+ let argStx? : Option Syntax ←
+ if ← getPPOption getPPAnalysisSkip then pure none
+ else if ← getPPOption getPPAnalysisHole then `(_)
+ else
+ match paramKinds with
+ | [ParamKind.implicit _ (some v)] =>
+ if !v.hasLooseBVars && v == arg then none else delab
+ | ParamKind.implicit name none :: _ =>
+ if ← getPPOption getPPAnalysisNamedArg <||> (name == `motive <&&> shouldShowMotive arg opts)
+ then mkNamedArg name (← delab)
+ else none
+ | _ => delab
let argStxs := match argStx? with
| none => argStxs
| some stx => argStxs.push stx
pure (fnStx, paramKinds.tailD [], argStxs))
- Syntax.mkApp fnStx argStxs
+ let stx := Syntax.mkApp fnStx argStxs
+ if ← isRegularApp then
+ unexpandRegularApp stx
+ <|> unexpandStructureInstance stx
+ <|> unexpandCoe stx
+ <|> pure stx
+ else pure stx
/-- State for `delabAppMatch` and helpers. -/
structure AppMatchState where
- info : MatcherInfo
- matcherTy : Expr
- params : Array Expr := #[]
- motive : Option (Syntax × Expr) := none
- discrs : Array Syntax := #[]
- varNames : Array (Array Name) := #[]
- rhss : Array Syntax := #[]
+ info : MatcherInfo
+ matcherTy : Expr
+ params : Array Expr := #[]
+ motive : Option (Syntax × Expr) := none
+ motiveNamed : Bool := false
+ discrs : Array Syntax := #[]
+ varNames : Array (Array Name) := #[]
+ rhss : Array Syntax := #[]
-- additional arguments applied to the result of the `match` expression
- moreArgs : Array Syntax := #[]
+ moreArgs : Array Syntax := #[]
/--
Extract arguments of motive applications from the matcher type.
For the example below: `#[#[`([])], #[`(a::as)]]` -/
private partial def delabPatterns (st : AppMatchState) : DelabM (Array (Array Syntax)) :=
- withReader (fun ctx => { ctx with inPattern := true }) do
+ withReader (fun ctx => { ctx with inPattern := true, optionsPerPos := {} }) do
let ty ← instantiateForall st.matcherTy st.params
forallTelescope ty fun params _ => do
-- skip motive and discriminators
- let alts := Array.ofSubarray $ params[1 + st.discrs.size:]
+ let alts := Array.ofSubarray params[1 + st.discrs.size:]
alts.mapIdxM fun idx alt => do
let ty ← inferType alt
- withReader ({ · with expr := ty }) $
+ -- TODO: this is a hack; we are accessing the expression out-of-sync with the position
+ -- Currently, we reset `optionsPerPos` at the beginning of `delabPatterns` to avoid
+ -- incorrectly considering annotations.
+ withTheReader SubExpr ({ · with expr := ty }) $
usingNames st.varNames[idx] do
withAppFnArgs (pure #[]) (fun pats => do pure $ pats.push (← delab))
where
@@ -237,7 +323,7 @@ where
mkLambdaFVars xs (mkApp e (mkConst ``Unit.unit))
else
mkLambdaFVars xs (mkAppN e xs)
- withReader (fun ctx => { ctx with expr := e }) visitLambda
+ withTheReader SubExpr (fun ctx => { ctx with expr := e }) visitLambda
/--
Delaborate applications of "matchers" such as
@@ -262,8 +348,9 @@ def delabAppMatch : Delab := whenPPOption getPPNotation do
-- store motive argument separately
let lamMotive ← getExpr
let piMotive ← lambdaTelescope lamMotive fun xs body => mkForallFVars xs body
- let piStx ← withReader (fun cfg => { cfg with expr := piMotive }) delab
- pure { st with motive := (piStx, lamMotive) }
+ let piStx ← withTheReader SubExpr (fun cfg => { cfg with expr := piMotive }) delab
+ let named ← getPPOption getPPAnalysisNamedArg
+ pure { st with motive := (piStx, lamMotive), motiveNamed := named }
else if st.discrs.size < st.info.numDiscrs then
pure { st with discrs := st.discrs.push (← delab) }
else if st.rhss.size < st.info.altNumParams.size then
@@ -290,7 +377,8 @@ def delabAppMatch : Delab := whenPPOption getPPNotation do
let stx ← do
let (piStx, lamMotive) := st.motive.get!
let opts ← getOptions
- if shouldShowMotive lamMotive opts then
+ -- TODO: disable the match if other implicits are needed?
+ if ← st.motiveNamed <||> shouldShowMotive lamMotive opts then
`(match $[$st.discrs:term],* : $piStx with $[| $pats,* => $st.rhss]*)
else
`(match $[$st.discrs:term],* with $[| $pats,* => $st.rhss]*)
@@ -308,7 +396,7 @@ def delabMData : Delab := do
-- only interpret `pp.` values by default
let Expr.mdata m _ _ ← getExpr | unreachable!
let mut posOpts := (← read).optionsPerPos
- let pos := (← read).pos
+ let pos ← getPos
for (k, v) in m do
if (`pp).isPrefixOf k then
let opts := posOpts.find? pos |>.getD {}
@@ -331,7 +419,7 @@ Return `true` iff current binder should be merged with the nested
binder, if any, into a single binder group:
* both binders must have same binder info and domain
* they cannot be inst-implicit (`[a b : A]` is not valid syntax)
-* `pp.binder_types` must be the same value for both terms
+* `pp.binderTypes` must be the same value for both terms
* prefer `fun a b` over `fun (a b)`
-/
private def shouldGroupWithNext : DelabM Bool := do
@@ -369,14 +457,21 @@ def delabLam : Delab :=
let stxT ← withBindingDomain delab
let ppTypes ← getPPOption getPPBinderTypes
let expl ← getPPOption getPPExplicit
+ let usedDownstream ← curNames.any (fun n => hasIdent n.getId stxBody)
+
-- leave lambda implicit if possible
- let blockImplicitLambda := expl ||
+ -- TODO: for now we just always block implicit lambdas. Once other things work, we can revisit.
+ -- Note: the current issue is that it requires state, i.e. if *any* previous binder was implicit,
+ -- it doesn't seem like we can leave a subsequent binder implicit.
+ let blockImplicitLambda := true ||
+ expl ||
e.binderInfo == BinderInfo.default ||
-- Note: the following restriction fixes many issues with roundtripping,
-- but this condition may still not be perfectly in sync with the elaborator.
e.binderInfo == BinderInfo.instImplicit ||
Elab.Term.blockImplicitLambda stxBody ||
- curNames.any (fun n => hasIdent n.getId stxBody);
+ usedDownstream
+
if !blockImplicitLambda then
pure stxBody
else
@@ -393,7 +488,9 @@ def delabLam : Delab :=
| BinderInfo.default, false => pure curNames.back -- here `curNames.size == 1`
| BinderInfo.implicit, true => `(funBinder| {$curNames* : $stxT})
| BinderInfo.implicit, false => `(funBinder| {$curNames*})
- | BinderInfo.instImplicit, _ => `(funBinder| [$curNames.back : $stxT]) -- here `curNames.size == 1`
+ | BinderInfo.instImplicit, _ =>
+ if usedDownstream then `(funBinder| [$curNames.back : $stxT]) -- here `curNames.size == 1`
+ else `(funBinder| [$stxT])
| _ , _ => unreachable!;
match stxBody with
| `(fun $binderGroups* => $stxBody) => `(fun $group $binderGroups* => $stxBody)
@@ -432,12 +529,14 @@ def delabForall : Delab :=
def delabLetE : Delab := do
let Expr.letE n t v b _ ← getExpr | unreachable!
let n ← getUnusedName n b
- let stxT ← descend t 0 delab
let stxV ← descend v 1 delab
let stxB ← withLetDecl n t v fun fvar =>
let b := b.instantiate1 fvar
descend b 2 delab
- `(let $(mkIdent n) : $stxT := $stxV; $stxB)
+ if ← getPPOption getPPAnalysisLetVarType then
+ let stxT ← descend t 0 delab
+ `(let $(mkIdent n) : $stxT := $stxV; $stxB)
+ else `(let $(mkIdent n) := $stxV; $stxB)
@[builtinDelab lit]
def delabLit : Delab := do
@@ -507,61 +606,6 @@ def delabProjectionApp : Delab := whenPPOption getPPStructureProjections $ do
let appStx ← withAppArg delab
`($(appStx).$(mkIdent f):ident)
-@[builtinDelab app]
-def delabStructureInstance : Delab := whenPPOption getPPStructureInstances do
- let env ← getEnv
- let e ← getExpr
- let some s ← pure $ e.isConstructorApp? env | failure
- guard $ isStructure env s.induct;
- /- If implicit arguments should be shown, and the structure has parameters, we should not
- pretty print using { ... }, because we will not be able to see the parameters. -/
- let explicit ← getPPOption getPPExplicit
- guard !(explicit && s.numParams > 0)
- let fieldNames := getStructureFields env s.induct
- let (_, fields) ← withAppFnArgs (pure (0, #[])) fun ⟨idx, fields⟩ => do
- if idx < s.numParams then
- pure (idx + 1, fields)
- else
- let val ← delab
- let field ← `(structInstField|$(mkIdent <| fieldNames.get! (idx - s.numParams)):ident := $val)
- pure (idx + 1, fields.push field)
- let lastField := fields[fields.size - 1]
- let fields := fields.pop
- let ty ←
- if (← getPPOption getPPStructureInstanceType) then
- let ty ← inferType e
- -- `ty` is not actually part of `e`, but since `e` must be an application or constant, we know that
- -- index 2 is unused.
- pure <| some (← descend ty 2 delab)
- else pure <| none
- `({ $[$fields, ]* $lastField $[: $ty]? })
-
-@[builtinDelab app]
-def delabAppWithUnexpander : Delab := whenPPOption getPPNotation do
- let Expr.const c _ _ ← pure (← getExpr).getAppFn | failure
- let fs@(f::_) ← pure <| appUnexpanderAttribute.getValues (← getEnv) c | failure
- /-
- Note: the following example will take exponential time:
- ```
- def foo (k : Nat → Nat) (n : Nat) : Nat := k (n+1)
-
- @[appUnexpander foo] def unexpandFooApp : Lean.PrettyPrinter.Unexpander
- | `(foo $k $a) => `(My.foo $k $a)
- | _ => throw ()
-
- #check foo $ foo $ foo $ foo $ foo $ foo $ foo id -- exp-time
- ```
- -/
- let stx ← delabAppImplicit
- match stx with
- | `($cPP:ident $args*) => do go fs stx
- | `($cPP:ident) => do go fs stx
- | _ => pure stx
-where
- go fs stx := fs.firstM fun f =>
- match f stx |>.run () with
- | EStateM.Result.ok stx _ => pure stx
- | _ => failure
@[builtinDelab app.Prod.mk]
def delabTuple : Delab := whenPPOption getPPNotation do
@@ -573,22 +617,6 @@ def delabTuple : Delab := whenPPOption getPPNotation do
| `(($b, $bs,*)) => `(($a, $b, $bs,*))
| _ => `(($a, $b))
--- abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β
-@[builtinDelab app.coe]
-def delabCoe : Delab := whenPPOption getPPCoercions do
- let e ← getExpr
- guard $ e.getAppNumArgs >= 4
- -- delab as application, then discard function
- let stx ← delabAppImplicit
- match stx with
- | `($fn $arg) => arg
- | `($fn $args*) => `($(args.get! 0) $(args.eraseIdx 0)*)
- | _ => failure
-
--- abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a
-@[builtinDelab app.coeFun]
-def delabCoeFun : Delab := delabCoe
-
@[builtinDelab app.List.nil]
def delabNil : Delab := whenPPOption getPPNotation do
guard $ (← getExpr).getAppNumArgs == 1
@@ -646,6 +674,7 @@ partial def delabDoElems : DelabM (List Syntax) := do
let e ← getExpr
if e.isAppOfArity `Bind.bind 6 then
-- Bind.bind.{u, v} : {m : Type u → Type v} → [self : Bind m] → {α β : Type u} → m α → (α → m β) → m β
+ let α := e.getAppArgs[2]
let ma ← withAppFn $ withAppArg delab
withAppArg do
match (← getExpr) with
@@ -653,8 +682,10 @@ partial def delabDoElems : DelabM (List Syntax) := do
withBindingBodyUnusedName fun n => do
if body.hasLooseBVars then
prependAndRec `(doElem|let $n:term ← $ma:term)
- else
+ else if α.isConstOf `Unit || α.isConstOf `PUnit then
prependAndRec `(doElem|$ma:term)
+ else
+ prependAndRec `(doElem|let _ ← $ma:term)
| _ => failure
else if e.isLet then
let Expr.letE n t v b _ ← getExpr | unreachable!
@@ -683,19 +714,6 @@ def delabSorryAx : Delab := whenPPOption getPPNotation do
guard <| (← getExpr).isAppOfArity ``sorryAx 2
`(sorry)
-@[builtinDelab app.Eq.ndrec]
-def delabEqNDRec : Delab := whenPPOption getPPNotation do
- guard <| (← getExpr).getAppNumArgs == 6
- -- Eq.ndrec.{u1, u2} : {α : Sort u2} → {a : α} → {motive : α → Sort u1} → (m : motive a) → {b : α} → (h : a = b) → motive b
- let m ← withAppFn <| withAppFn <| withAppArg delab
- let h ← withAppArg delab
- `($h ▸ $m)
-
-@[builtinDelab app.Eq.rec]
-def delabEqRec : Delab :=
- -- relevant signature parts as in `Eq.ndrec`
- delabEqNDRec
-
def reifyName : Expr → DelabM Name
| Expr.const ``Lean.Name.anonymous .. => Name.anonymous
| Expr.app (Expr.app (Expr.const ``Lean.Name.mkStr ..) n _) (Expr.lit (Literal.strVal s) _) _ => do
diff --git a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
new file mode 100644
index 0000000000..d143c58d95
--- /dev/null
+++ b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Daniel Selsam
+-/
+
+/-!
+This file defines utilities for `MetaM` computations to traverse subexpressions
+of an expression in sync with the `Nat` "position" values that refers to them.
+We use a simple encoding scheme: every `Expr` constructor has at most 3 direct
+expression children. We can injectively map a path of `childIdxs` to a natural
+number by computing the value of the 3-ary representation `1 :: childIdxs`,
+since n-ary representations without leading zeros are unique.
+Note that `pos` is initialized to `1` (case `childIdxs == []`).
+-/
+import Lean.Meta.Basic
+import Std.Data.RBMap
+
+namespace Lean.PrettyPrinter.Delaborator
+
+abbrev Pos := Nat
+
+abbrev OptionsPerPos := Std.RBMap Pos Options compare
+
+structure SubExpr where
+ expr : Expr
+ pos : Pos
+
+namespace SubExpr
+
+variable {α : Type} [Inhabited α]
+variable {m : Type → Type} [Monad m]
+variable [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m]
+variable [MonadLiftT MetaM m] [MonadControlT MetaM m]
+variable [MonadLiftT IO m]
+
+abbrev maxChildren : Pos := 3
+
+def mkRoot (e : Expr) : SubExpr := ⟨e, 1⟩
+
+def getExpr : m Expr := do (← readThe SubExpr).expr
+def getPos : m Pos := do (← readThe SubExpr).pos
+
+def descend (child : Expr) (childIdx : Pos) (x : m α) : m α :=
+ withTheReader SubExpr (fun cfg => { cfg with expr := child, pos := cfg.pos * maxChildren + childIdx }) x
+
+def withAppFn (x : m α) : m α := do descend (← getExpr).appFn! 0 x
+def withAppArg (x : m α) : m α := do descend (← getExpr).appArg! 1 x
+
+def withAppType (x : m α) : m α := do
+ descend (← Meta.inferType (← getExpr)) 2 x -- phantom positions for types
+
+def withFVarType (x : m α) : m α := do
+ let e@(Expr.fvar ..) ← getExpr | unreachable!
+ descend (← Meta.inferType e) 0 x -- phantom positions for types
+
+partial def withAppFnArgs (xf : m α) (xa : α → m α) : m α := do
+ if (← getExpr).isApp then
+ let acc ← withAppFn (withAppFnArgs xf xa)
+ withAppArg (xa acc)
+ else xf
+
+def withBindingDomain (x : m α) : m α := do descend (← getExpr).bindingDomain! 0 x
+
+def withBindingBody (n : Name) (x : m α) : m α := do
+ let e ← getExpr
+ Meta.withLocalDecl n e.binderInfo e.bindingDomain! fun fvar =>
+ descend (e.bindingBody!.instantiate1 fvar) 1 x
+
+def withProj (x : m α) : m α := do
+ let Expr.proj _ _ e _ ← getExpr | unreachable!
+ descend e 0 x
+
+def withMDataExpr (x : m α) : m α := do
+ let Expr.mdata _ e _ ← getExpr | unreachable!
+ -- do not change position so that options on an mdata are automatically forwarded to the child
+ withReader ({ · with expr := e }) x
+
+def withLetVarType (x : m α) : m α := do
+ let Expr.letE _ t _ _ _ ← getExpr | unreachable!
+ descend t 0 x
+
+def withLetValue (x : m α) : m α := do
+ let Expr.letE _ _ v _ _ ← getExpr | unreachable!
+ descend v 1 x
+
+def withLetBody (x : m α) : m α := do
+ let Expr.letE n t v b _ ← getExpr | unreachable!
+ Meta.withLetDecl n t v fun fvar =>
+ let b := b.instantiate1 fvar
+ descend b 2 x
+
+def withNaryFn (x : m α) : m α := do
+ let e ← getExpr
+ let n := e.getAppNumArgs
+ let newPos := (← getPos) * (maxChildren ^ n)
+ withTheReader SubExpr (fun cfg => { cfg with expr := e.getAppFn, pos := newPos }) x
+
+def withNaryArg (argIdx : Nat) (x : m α) : m α := do
+ let e ← getExpr
+ let args := e.getAppArgs
+ let newPos := (← getPos) * (maxChildren ^ (args.size - argIdx)) + 1
+ withTheReader SubExpr (fun cfg => { cfg with expr := args[argIdx], pos := newPos }) x
+
+end SubExpr
+
+end Lean.PrettyPrinter.Delaborator
diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
new file mode 100644
index 0000000000..9cb413f87e
--- /dev/null
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -0,0 +1,370 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Daniel Selsam
+-/
+
+/-!
+The top-down analyzer is an optional preprocessor to the delaborator that aims
+to determine the minimal annotations necessary to ensure that the delaborated
+expression can be re-elaborated correctly. Currently, the top-down analyzer
+is neither sound nor complete: there may be edge-cases in which the expression
+can still not be re-elaborated correctly, and it may also add many annotations
+that are not strictly necessary.
+-/
+
+import Lean.Meta
+import Lean.Util.CollectLevelParams
+import Lean.Util.ReplaceLevel
+import Lean.PrettyPrinter.Delaborator.SubExpr
+import Std.Data.RBMap
+
+namespace Lean
+
+open Lean.Meta
+open Std (RBMap)
+
+register_builtin_option pp.analyze : Bool := {
+ defValue := false
+ group := "pp.analyze"
+ descr := "(pretty printer analyzer) determine annotations sufficient to ensure round-tripping"
+}
+
+register_builtin_option pp.analyze.checkInstances : Bool := {
+ defValue := true
+ group := "pp.analyze"
+ descr := "(pretty printer analyzer) confirm that instances can be re-synthesized"
+}
+
+register_builtin_option pp.analyze.typeAscriptions : Bool := {
+ defValue := true
+ group := "pp.analyze"
+ descr := "(pretty printer analyzer) add type ascriptions when deemed necessary"
+}
+
+register_builtin_option pp.analyze.trustSubst : Bool := {
+ defValue := false
+ group := "pp.analyze"
+ descr := "(pretty printer analyzer) always 'pretend' applications that can delab to ▸ are 'regular'"
+}
+
+register_builtin_option pp.analyze.trustOfNat : Bool := {
+ defValue := true
+ group := "pp.analyze"
+ descr := "(pretty printer analyzer) always 'pretend' `OfNat.ofNat` applications can elab bottom-up"
+}
+
+register_builtin_option pp.analyze.trustSimpleHOFuns : Bool := {
+ defValue := false
+ group := "pp.analyze"
+ descr := "(pretty printer analyzer) omit constant higher-order functions returning non-Pi types"
+}
+
+register_builtin_option pp.analyze.trustKnownType2TypeHOFuns : Bool := {
+ defValue := true
+ group := "pp.analyze"
+ descr := "(pretty printer analyzer) omit higher-order functions whose values seem to be knownType2Type"
+}
+
+def getPPAnalyze (o : Options) : Bool := o.get pp.analyze.name pp.analyze.defValue
+def getPPAnalyzeCheckInstances (o : Options) : Bool := o.get pp.analyze.checkInstances.name pp.analyze.checkInstances.defValue
+def getPPAnalyzeTypeAscriptions (o : Options) : Bool := o.get pp.analyze.typeAscriptions.name pp.analyze.typeAscriptions.defValue
+def getPPAnalyzeTrustSubst (o : Options) : Bool := o.get pp.analyze.trustSubst.name pp.analyze.trustSubst.defValue
+def getPPAnalyzeTrustOfNat (o : Options) : Bool := o.get pp.analyze.trustOfNat.name pp.analyze.trustOfNat.defValue
+def getPPAnalyzeTrustSimpleHOFuns (o : Options) : Bool := o.get pp.analyze.trustSimpleHOFuns.name pp.analyze.trustSimpleHOFuns.defValue
+def getPPAnalyzeTrustKnownType2TypeHOFuns (o : Options) : Bool := o.get pp.analyze.trustKnownType2TypeHOFuns.name pp.analyze.trustKnownType2TypeHOFuns.defValue
+
+def getPPAnalysisSkip (o : Options) : Bool := o.get `pp.analysis.skip false
+def getPPAnalysisHole (o : Options) : Bool := o.get `pp.analysis.hole false
+def getPPAnalysisNamedArg (o : Options) : Bool := o.get `pp.analysis.namedArg false
+def getPPAnalysisLetVarType (o : Options) : Bool := o.get `pp.analysis.letVarType true
+def getPPAnalysisNeedsType (o : Options) : Bool := o.get `pp.analysis.needsType false
+
+namespace PrettyPrinter.Delaborator
+
+-- TODO: elsewhere
+deriving instance Repr for BinderInfo
+
+def returnsPi (motive : Expr) : MetaM Bool := do
+ lambdaTelescope motive fun xs b => b.isForall
+
+def isNonConstFun (motive : Expr) : MetaM Bool := do
+ match motive with
+ | Expr.lam name d b _ => isNonConstFun b
+ | _ => motive.hasLooseBVars
+
+def isSimpleHOFun (motive : Expr) : MetaM Bool := do
+ not (← returnsPi motive) && not (← isNonConstFun motive)
+
+def isType2Type (motive : Expr) : MetaM Bool := do
+ match ← inferType motive with
+ | Expr.forallE _ (Expr.sort ..) (Expr.sort ..) .. =>
+ -- TODO: change the name
+ -- we really want something "monad-like", so no lambda
+ motive.isApp || motive.isConst || motive.isFVar
+ | _ => false
+
+namespace TopDownAnalyze
+
+def replaceLPsWithVars (e : Expr) : MetaM Expr := do
+ let lps := collectLevelParams {} e |>.params
+ let mut replaceMap : Std.HashMap Name Level := {}
+ for lp in lps do replaceMap := replaceMap.insert lp (← mkFreshLevelMVar)
+ return e.replaceLevel fun
+ | Level.param n .. => replaceMap.find! n
+ | l => if !l.hasParam then some l else none
+
+def tryUnify (t s : Expr) : MetaM Unit := do
+ try
+ let r ← Meta.isExprDefEqAux t s
+ if !r then
+ trace[pp.analyze.tryUnify] "nonDefEq\n\n{fmt t}\n\n=?=\n\n{fmt s}\n"
+ pure ()
+ catch ex =>
+ trace[pp.analyze.tryUnify] "{← ex.toMessageData.toString}\n\n{fmt t}\n\n=?=\n\n{fmt s}\n"
+ pure ()
+
+structure BottomUpKind where
+ needsType : Bool
+ needsLevel : Bool
+ deriving Inhabited, Repr, BEq
+
+def BottomUpKind.safe : BottomUpKind := ⟨false, false⟩
+def BottomUpKind.unsafe : BottomUpKind := ⟨true, true⟩
+
+def BottomUpKind.isSafe : BottomUpKind → Bool := (· == BottomUpKind.safe)
+def BottomUpKind.isUnsafe : BottomUpKind → Bool := (· == BottomUpKind.unsafe)
+
+partial def inspectOutParams (arg mvar : Expr) : MetaM Unit := do
+ let argType ← inferType arg -- HAdd α α α
+ let mvarType ← inferType mvar
+ let fType ← inferType argType.getAppFn -- Type → Type → outParam Type
+ let mType ← inferType mvarType.getAppFn
+ inspectAux fType mType 0 argType.getAppArgs mvarType.getAppArgs
+where
+ inspectAux (fType mType : Expr) (i : Nat) (args mvars : Array Expr) := do
+ let fType ← whnf fType
+ let mType ← whnf mType
+ if not (i < args.size) then return ()
+ match fType, mType with
+ | Expr.forallE _ fd fb _, Expr.forallE _ md mb _ => do
+ -- TODO: do I need to check (← okBottomUp? args[i] mvars[i] fuel).isSafe here?
+ -- if so, I'll need to take a callback
+ if isOutParam fd then
+ tryUnify (args[i]) (mvars[i])
+ inspectAux (fb.instantiate1 args[i]) (mb.instantiate1 mvars[i]) (i+1) args mvars
+ | _, _ => return ()
+
+partial def okBottomUp? (e : Expr) (mvar? : Option Expr := none) (fuel : Nat := 10) : MetaM BottomUpKind := do
+ -- Here we check if `e` can be safely elaborated without its expected type.
+ -- These are incomplete (and possibly unsound) heuristics.
+ match fuel with
+ | 0 => BottomUpKind.unsafe
+ | fuel + 1 =>
+ if e.isFVar then return BottomUpKind.safe
+ if getPPAnalyzeTrustOfNat (← getOptions) && e.isAppOfArity `OfNat.ofNat 3 then return BottomUpKind.safe
+ if e.isApp || e.isConst then
+ match e.getAppFn with
+ | Expr.const .. =>
+ let args := e.getAppArgs
+ let fType ← replaceLPsWithVars (← inferType e.getAppFn)
+ let ⟨mvars, bInfos, resultType⟩ ← forallMetaBoundedTelescope fType e.getAppArgs.size (instsSynthetic := false)
+ for i in [:mvars.size] do
+ if bInfos[i] == BinderInfo.instImplicit then
+ inspectOutParams args[i] mvars[i]
+ else if bInfos[i] == BinderInfo.default then
+ match ← okBottomUp? args[i] mvars[i] fuel with
+ | ⟨false, false⟩ => tryUnify args[i] mvars[i]
+ | _ => pure ()
+ if mvar?.isSome then tryUnify resultType (← inferType mvar?.get!)
+ let resultType ← instantiateMVars resultType
+ pure ⟨resultType.hasExprMVar, resultType.hasLevelMVar⟩
+ | _ => BottomUpKind.unsafe
+ else BottomUpKind.unsafe
+
+def isHigherOrder (type : Expr) : MetaM Bool := do
+ withTransparency TransparencyMode.all do forallTelescopeReducing type fun xs b => xs.size > 0 && b.isSort
+
+def isFunLike (e : Expr) : MetaM Bool := do
+ withTransparency TransparencyMode.all do forallTelescopeReducing (← inferType e) fun xs b => xs.size > 0
+
+def isSubstLike (e : Expr) : Bool :=
+ e.isAppOfArity `Eq.ndrec 6
+
+open SubExpr
+
+structure Context where
+ knowsType : Bool
+ knowsLevel : Bool -- only constants look at this
+ inBottomUp : Bool := false
+ deriving Inhabited, Repr
+
+structure State where
+ annotations : RBMap Pos Options compare := {}
+
+abbrev AnalyzeM := ReaderT Context (ReaderT SubExpr (StateRefT State MetaM))
+
+def withKnowing (knowsType knowsLevel : Bool) (x : AnalyzeM α) : AnalyzeM α := do
+ withReader (fun ctx => { ctx with knowsType := knowsType, knowsLevel := knowsLevel }) x
+
+builtin_initialize analyzeFailureId : InternalExceptionId ← registerInternalExceptionId `analyzeFailure
+
+def checkKnowsType : AnalyzeM Unit := do
+ if not (← read).knowsType then
+ throw $ Exception.internal analyzeFailureId
+
+def annotateBool (n : Name) (b : Bool) : AnalyzeM Unit := do
+ let pos ← getPos
+ let opts := (← get).annotations.findD pos {} |>.setBool n b
+ trace[pp.analyze.annotate] "{pos} {n} {b}"
+ modify fun s => { s with annotations := s.annotations.insert pos opts }
+
+def annotateName (n : Name) (v : Name) : AnalyzeM Unit := do
+ let pos ← getPos
+ let opts := (← get).annotations.findD pos {} |>.setName n v
+ modify fun s => { s with annotations := s.annotations.insert pos opts }
+
+partial def analyze : AnalyzeM Unit := do
+ checkMaxHeartbeats "Delaborator.topDownAnalyze"
+ trace[pp.analyze] "{(← read).knowsType}.{(← read).knowsLevel} {← getExpr}"
+ 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 .. => unreachable!
+where
+ analyzeApp := do
+ withKnowing true true $ analyzeAppStaged (← getExpr).getAppFn (← getExpr).getAppArgs
+ if !(← read).knowsType && !(← okBottomUp? (← getExpr)).isSafe then
+ annotateBool `pp.analysis.needsType true
+ withAppType $ withKnowing true false $ analyze
+
+ analyzeAppStaged (f : Expr) (args : Array Expr) : AnalyzeM Unit := do
+ let fType ← replaceLPsWithVars (← inferType f)
+ let ⟨mvars, bInfos, resultType⟩ ← forallMetaBoundedTelescope fType args.size (instsSynthetic := false)
+ let rest := args.extract mvars.size args.size
+ let args := args.shrink mvars.size
+
+ -- Unify with the expected type
+ tryUnify (← inferType (mkAppN f args)) resultType
+
+ -- Collect explicit arguments that can be elaborated without expected type
+ -- TODO: try before *and* after HO?
+ let mut bottomUps := mkArray args.size false
+ for i in [:args.size] do
+ if bInfos[i] == BinderInfo.default then
+ if (← valUnknown mvars[i]) && (← okBottomUp? args[i] mvars[i]).isSafe then
+ tryUnify args[i] mvars[i]
+ bottomUps := bottomUps.set! i true
+ else if bInfos[i] == BinderInfo.instImplicit then
+ inspectOutParams args[i] mvars[i]
+
+ -- Collect implicit higher-order arguments
+ let mut higherOrders := mkArray args.size false
+ for i in [:args.size] do
+ -- TODO: determine more conditions under which we can safely omit higher-order arguments
+ if not (← bInfos[i] == BinderInfo.implicit) then continue
+ if not (← isHigherOrder (← inferType args[i])) then continue
+
+ if getPPAnalyzeTrustSimpleHOFuns (← getOptions) && (← isSimpleHOFun args[i]) then continue
+
+ tryUnify args[i] mvars[i]
+
+ -- TODO: the following check seems to bring scores down significantly, but I am not sure why yet
+ -- Guess: the elaborator may not always proceed in the same order that we do
+ if getPPAnalyzeTrustKnownType2TypeHOFuns (← getOptions) && not (← valUnknown args[i]) && (← isType2Type (args[i])) then continue
+ higherOrders := higherOrders.set! i true
+
+ -- Now, if this is the first staging, analyze the n-ary function without expected type
+ if !f.isApp then withKnowing false !(← instantiateMVars fType).hasLevelMVar $ withNaryFn analyze
+
+ let disableNamedImplicits : Bool := getPPAnalyzeTrustSubst (← getOptions) && isSubstLike (← getExpr)
+
+ for i in [:args.size] do
+ let arg := args[i]
+ let argType ← inferType arg
+
+ withNaryArg (f.getAppNumArgs + i) do
+ withReader (fun ctx => { ctx with inBottomUp := ctx.inBottomUp || bottomUps[i] }) do
+ match bInfos[i] with
+ | BinderInfo.default =>
+ if !(← valUnknown mvars[i]) && !(← read).inBottomUp && !(← isFunLike arg) then annotateBool `pp.analysis.hole true
+ | BinderInfo.implicit =>
+ if (← valUnknown mvars[i] <||> higherOrders[i]) && !disableNamedImplicits then annotateBool `pp.analysis.namedArg true
+ else annotateBool `pp.analysis.skip true
+ | BinderInfo.instImplicit =>
+ -- Note: apparently checking valUnknown here is not sound, because the elaborator
+ -- will not happily assign instImplicits that it cannot synthesize
+ if getPPAnalyzeCheckInstances (← getOptions) then
+ let instResult ← try trySynthInstance argType catch _ => LOption.undef
+ match instResult with
+ | LOption.some inst =>
+ if ← isDefEq inst arg then annotateBool `pp.analysis.skip true
+ else annotateBool `pp.analysis.namedArg true
+ | _ => annotateBool `pp.analysis.namedArg true
+ | BinderInfo.auxDecl => pure ()
+ | BinderInfo.strictImplicit => unreachable!
+ withKnowing (not (← typeUnknown mvars[i])) true analyze
+ tryUnify mvars[i] args[i]
+
+ if not rest.isEmpty then analyzeAppStaged (mkAppN f args) rest
+
+ analyzeConst : AnalyzeM Unit := do
+ -- TODO: currently, the analyzer never uses @,
+ -- even though named arguments do not work for inaccessible names
+ let Expr.const n ls .. ← getExpr | unreachable!
+ annotateBool `pp.universes (!(← read).knowsLevel && !ls.isEmpty)
+
+ analyzePi : AnalyzeM Unit := do
+ annotateBool `pp.binderTypes true
+ withBindingDomain $ withKnowing true false analyze
+ withBindingBody Name.anonymous analyze
+
+ analyzeLam : AnalyzeM Unit := do
+ annotateBool `pp.binderTypes !(← read).knowsType
+ withBindingDomain $ withKnowing true false analyze
+ withBindingBody Name.anonymous analyze
+
+ analyzeLet : AnalyzeM Unit := do
+ let Expr.letE n t v body .. ← getExpr | unreachable!
+ let needsType := (← okBottomUp? v).needsType
+ annotateBool `pp.analysis.letVarType needsType
+ withLetValue $ withKnowing true true analyze
+ withLetVarType $ withKnowing true false analyze
+ withLetBody analyze
+
+ analyzeSort : AnalyzeM Unit := pure ()
+ analyzeProj : AnalyzeM Unit := withProj analyze
+ analyzeFVar : AnalyzeM Unit := pure ()
+ analyzeMData : AnalyzeM Unit := withMDataExpr analyze
+
+ valUnknown (e : Expr) : AnalyzeM Bool := do
+ (← instantiateMVars e).hasMVar
+
+ typeUnknown (e : Expr) : AnalyzeM Bool := do
+ (← instantiateMVars (← inferType e)).hasMVar
+
+end TopDownAnalyze
+
+open TopDownAnalyze SubExpr
+
+def topDownAnalyze (e : Expr) : MetaM OptionsPerPos := do
+ traceCtx `pp.analyze do
+ withReader (fun ctx => { ctx with config := Lean.Elab.Term.setElabConfig ctx.config }) do
+ let ϕ : AnalyzeM OptionsPerPos := do analyze; (← get).annotations
+ ϕ { knowsType := true, knowsLevel := true } (mkRoot e) |>.run' {}
+
+builtin_initialize
+ registerTraceClass `pp.analyze
+ registerTraceClass `pp.analyze.annotate
+ registerTraceClass `pp.analyze.tryUnify
+
+end Lean.PrettyPrinter.Delaborator
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index a4037fb021..fb124d7cbb 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -164,7 +164,7 @@ section Initialization
srcSearchPath := srcSearchPath ++ pkgSearchPath
Elab.processHeader headerStx opts msgLog inputCtx
catch e => -- should be from `leanpkg print-paths`
- let msgs := MessageLog.empty.add { fileName := "", pos := ⟨0, 0⟩, data := e.toString }
+ let msgs := MessageLog.empty.add { fileName := "", rawPos := 0, pos := ⟨0, 0⟩, data := e.toString }
pure (← mkEmptyEnvironment, msgs)
publishMessages m msgLog hOut
let cmdState := Elab.Command.mkState headerEnv msgLog opts
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index 208f650721..049b3b1970 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -113,6 +113,7 @@ def compileNextCmd (contents : String) (snap : Snapshot) : IO (Sum Snapshot Mess
messages := postCmdState.messages.add {
fileName := inputCtx.fileName
severity := MessageSeverity.information
+ rawPos := snap.endPos
pos := inputCtx.fileMap.toPosition snap.endPos
data := output
}
diff --git a/tests/compiler/partial.lean b/tests/compiler/partial.lean
index d52201249d..43ac3fb675 100644
--- a/tests/compiler/partial.lean
+++ b/tests/compiler/partial.lean
@@ -1,6 +1,6 @@
set_option pp.explicit true
-set_option pp.binder_types false
+set_option pp.binderTypes false
-- set_option trace.compiler.boxed true
partial def contains : String → Char → Nat → Bool
diff --git a/tests/lean/236.lean b/tests/lean/236.lean
index 6f6dc59f10..178d5613af 100644
--- a/tests/lean/236.lean
+++ b/tests/lean/236.lean
@@ -7,5 +7,7 @@ structure Foo where
set_option pp.all true
#check { x := 10, b := true : Foo }
-set_option pp.structure_instances true
+set_option pp.universes false
+set_option pp.explicit false
+set_option pp.structureInstances true
#check { x := 10, b := true : Foo }
diff --git a/tests/lean/236.lean.expected.out b/tests/lean/236.lean.expected.out
index 7f1b8c1794..226d08e3ac 100644
--- a/tests/lean/236.lean.expected.out
+++ b/tests/lean/236.lean.expected.out
@@ -1,3 +1,3 @@
{ x := 10, b := true } : Foo
Foo.mk (@OfNat.ofNat.{0} Nat 10 (instOfNatNat 10)) Bool.true : Foo
-{ x := @OfNat.ofNat.{0} Nat 10 (instOfNatNat 10), b := Bool.true : Foo } : Foo
+{ x := OfNat.ofNat 10, b := Bool.true : Foo } : Foo
diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean
index 8845aeb24d..e1439c7c06 100644
--- a/tests/lean/PPRoundtrip.lean
+++ b/tests/lean/PPRoundtrip.lean
@@ -6,6 +6,7 @@ open Lean.Elab.Term
open Lean.Elab.Command
open Std.Format open Std
open Lean.PrettyPrinter
+open Lean.PrettyPrinter.Delaborator
open Lean.Meta
@@ -77,7 +78,7 @@ end
#eval checkM `({α : Type} → [ToString α] → α)
#eval checkM `(∀ x : Nat, x = x)
#eval checkM `(∀ {x : Nat} [ToString Nat], x = x)
-set_option pp.binder_types false in
+set_option pp.binderTypes false in
#eval checkM `(∀ x : Nat, x = x)
-- TODO: hide `ofNat`
@@ -86,7 +87,7 @@ set_option pp.binder_types false in
#eval checkM `(42)
#eval checkM `("hi")
-set_option pp.structure_instance_type true in
+set_option pp.structureInstanceTypes true in
#eval checkM `({ type := Nat, val := 0 : PointedType })
#eval checkM `((1,2,3))
#eval checkM `((1,2).fst)
diff --git a/tests/lean/commandPrefix.lean.expected.out b/tests/lean/commandPrefix.lean.expected.out
index c439d23468..34d12cbad3 100644
--- a/tests/lean/commandPrefix.lean.expected.out
+++ b/tests/lean/commandPrefix.lean.expected.out
@@ -1,2 +1,2 @@
-(fun (this : Unit) => this) Unit.unit : Unit
+(fun (this : Unit) => this) () : Unit
commandPrefix.lean:3:0: error: expected command
diff --git a/tests/lean/delabUnexpand.lean b/tests/lean/delabUnexpand.lean
index 4a8de8c1c0..eea0f8505f 100644
--- a/tests/lean/delabUnexpand.lean
+++ b/tests/lean/delabUnexpand.lean
@@ -22,5 +22,4 @@ def foo (k : Nat → Nat) (n : Nat) : Nat := k (n+1)
| `(foo $k $a) => `(My.foo $k $a)
| _ => throw ()
--- The following would take exponential time without the `delabCache`.
-#check foo $ foo $ foo $ foo $ foo $ foo $ id
+#check foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ foo $ id
diff --git a/tests/lean/delabUnexpand.lean.expected.out b/tests/lean/delabUnexpand.lean.expected.out
index 8a21845bbd..370aa772ae 100644
--- a/tests/lean/delabUnexpand.lean.expected.out
+++ b/tests/lean/delabUnexpand.lean.expected.out
@@ -1,2 +1,9 @@
3 ♬ 4 : Foo
-foo (foo (foo (foo (foo (foo id))))) : Nat → Nat
+foo
+ (foo
+ (foo
+ (foo
+ (foo
+ (foo
+ (foo
+ (foo (foo (foo (foo (foo (foo (foo (foo (foo (foo (foo (foo (foo (foo id)))))))))))))))))))) : Nat → Nat
diff --git a/tests/lean/holes.lean.expected.out b/tests/lean/holes.lean.expected.out
index f7d555a925..ebdec58509 100644
--- a/tests/lean/holes.lean.expected.out
+++ b/tests/lean/holes.lean.expected.out
@@ -26,7 +26,7 @@ holes.lean:19:0-19:3: error: don't know how to synthesize implicit argument
@f Nat (?m a) a
context:
a : Nat
-f : {α : Type} → {β : ?m a} → α → α := fun {α : Type} (a : α) => a
+f : {α : Type} → {β : ?m a} → α → α := fun {α : Type} {β : ?m a} (a : α) => a
⊢ ?m a
holes.lean:18:7-18:10: error: failed to infer binder type
holes.lean:21:25-22:4: error: failed to infer definition type
diff --git a/tests/lean/matchApp.lean b/tests/lean/matchApp.lean
index e417810740..5b9faf42c7 100644
--- a/tests/lean/matchApp.lean
+++ b/tests/lean/matchApp.lean
@@ -8,4 +8,4 @@ def f (xs ys : List α) : Nat :=
(h1 : Unit → motive [] [])
(h2 : (x : List α) → motive x [])
(h3 : (x x_1 : List α) → motive x x_1)
- => f.match_1 motive [] [] h1 h2 h3
+ => f.match_1 (motive := motive) [] [] h1 h2 h3
diff --git a/tests/lean/matchApp.lean.expected.out b/tests/lean/matchApp.lean.expected.out
index 6eb45ac9e1..de40fb5583 100644
--- a/tests/lean/matchApp.lean.expected.out
+++ b/tests/lean/matchApp.lean.expected.out
@@ -1,7 +1,7 @@
fun {α : Type} (motive : List α → List α → Type) (h1 : Unit → motive [] []) (h2 : (x : List α) → motive x [])
(h3 : (x x_1 : List α) → motive x x_1) =>
match [], [] with
- | [], [] => h1 Unit.unit
+ | [], [] => h1 ()
| x, [] => h2 x
| x, x_1 =>
h3 x
diff --git a/tests/lean/ppNotationCode.lean.expected.out b/tests/lean/ppNotationCode.lean.expected.out
index c334099948..b6cf14899c 100644
--- a/tests/lean/ppNotationCode.lean.expected.out
+++ b/tests/lean/ppNotationCode.lean.expected.out
@@ -36,15 +36,15 @@ fun (x : Lean.Syntax) =>
let lhs : Lean.Syntax := discr;
do
let info ← Lean.MonadRef.mkInfoFromRefPos
- Lean.getCurrMacroScope
- Lean.getMainModule
+ let _ ← Lean.getCurrMacroScope
+ let _ ← Lean.getMainModule
pure (Lean.Syntax.node `«term_+++_» #[lhs, Lean.Syntax.atom info "+++", rhs])
else
let discr : Lean.Syntax := Lean.Syntax.getArg discr 1;
- throw Unit.unit)
+ throw ())
(let discr_2 : Lean.Syntax := Lean.Syntax.getArg discr 0;
let discr : Lean.Syntax := Lean.Syntax.getArg discr 1;
- throw Unit.unit)
+ throw ())
else
let discr : Lean.Syntax := x;
- throw Unit.unit
+ throw ()
diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean
new file mode 100644
index 0000000000..bef64470bf
--- /dev/null
+++ b/tests/lean/run/PPTopDownAnalyze.lean
@@ -0,0 +1,236 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Daniel Selsam
+-/
+import Lean
+
+open Lean Lean.Meta Lean.Elab Lean.Elab.Term Lean.Elab.Command
+open Lean.PrettyPrinter
+
+def checkDelab (e : Expr) (tgt? : Option Syntax) (name? : Option Name := none) : TermElabM Unit := do
+ if e.hasMVar then throwError "[checkDelab] term has mvars, {e}"
+ let stx ← delab (← getCurrNamespace) (← getOpenDecls) e
+ match tgt? with
+ | some tgt =>
+ if toString (← PrettyPrinter.ppTerm stx) != toString (← PrettyPrinter.ppTerm tgt?.get!) then
+ throwError "[checkDelab] missed target\n{← PrettyPrinter.ppTerm stx}\n!=\n{← PrettyPrinter.ppTerm tgt}\n\nExpr: {e}\nType: {← inferType e}"
+ | _ => pure ()
+
+ let e' ←
+ try
+ let e' ← elabTerm stx (some (← inferType e))
+ synthesizeSyntheticMVarsNoPostponing
+ let e' ← instantiateMVars e'
+ -- let ⟨e', _⟩ ← levelMVarToParam e'
+ throwErrorIfErrors
+ e'
+ catch ex => throwError "[checkDelab] failed to re-elaborate,\n{stx}\n{← ex.toMessageData.toString}"
+
+ withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `pp.all true }) do
+ if not (← isDefEq e e') then
+ println! "[checkDelab] {← inferType e} {← inferType e'}"
+ throwError "[checkDelab] roundtrip not structurally equal\n\nOriginal: {e}\n\nSyntax: {stx}\n\nNew: {e'}"
+
+ let e' ← instantiateMVars e'
+ if e'.hasMVar then throwError "[checkDelab] elaborated term still has mvars\n\nSyntax: {stx}\n\nExpression: {e'}"
+
+
+syntax (name := testDelabTD) "#testDelab " term " expecting " term : command
+
+@[commandElab testDelabTD] def elabTestDelabTD : CommandElab
+ | `(#testDelab $stx:term expecting $tgt:term) => liftTermElabM `delabTD do
+ let e ← elabTerm stx none
+ let ⟨e, _⟩ ← levelMVarToParam e
+ let e ← instantiateMVars e
+ checkDelab e (some tgt)
+ | _ => throwUnsupportedSyntax
+
+syntax (name := testDelabTDN) "#testDelabN " ident : command
+
+@[commandElab testDelabTDN] def elabTestDelabTDN : CommandElab
+ | `(#testDelabN $name:ident) => liftTermElabM `delabTD do
+ let name := name.getId
+ let [name] ← resolveGlobalConst name | throwError "cannot resolve name"
+ let some cInfo ← (← getEnv).find? name | throwError "no decl for name"
+ let some value ← pure cInfo.value? | throwError "decl has no value"
+ modify fun s => { s with levelNames := cInfo.levelParams }
+ withTheReader Core.Context (fun ctx => { ctx with currNamespace := name.getPrefix, openDecls := [] }) do
+ checkDelab value none
+ | _ => throwUnsupportedSyntax
+
+-------------------------------------------------
+-------------------------------------------------
+-------------------------------------------------
+
+universe u v
+
+set_option pp.analyze true
+
+#testDelab @Nat.brecOn (fun x => Nat) 0 (fun x ih => x)
+ expecting Nat.brecOn (motive := fun x => Nat) 0 fun x ih => x
+
+#testDelab @Nat.brecOn (fun x => Nat → Nat) 0 (fun x ih => fun y => y + x)
+ expecting Nat.brecOn (motive := fun x => Nat → Nat) 0 fun x ih y => y + x
+
+#testDelab @Nat.brecOn (fun x => Nat → Nat) 0 (fun x ih => fun y => y + x) 0
+ expecting Nat.brecOn (motive := fun x => Nat → Nat) 0 (fun x ih y => y + x) 0
+
+#testDelab let xs := #[]; xs.push (5 : Nat)
+ expecting let xs : Array Nat := #[]; Array.push xs 5
+
+#testDelab let x := Nat.zero; x + Nat.zero
+ expecting let x := Nat.zero; x + Nat.zero
+
+def fHole (α : Type) (x : α) : α := x
+
+#testDelab fHole Nat Nat.zero
+ expecting fHole _ Nat.zero
+
+def fPoly {α : Type u} (x : α) : α := x
+
+#testDelab fPoly Nat.zero
+ expecting fPoly Nat.zero
+
+#testDelab fPoly (id Nat.zero)
+ expecting fPoly (id Nat.zero)
+
+def fPoly2 {α : Type u} {β : Type v} (x : α) : α := x
+
+#testDelab @fPoly2 _ (Type 3) Nat.zero
+ expecting fPoly2 (β := Type 3) Nat.zero
+
+def fPolyInst {α : Type u} [Add α] : α → α → α := Add.add
+
+#testDelab @fPolyInst Nat ⟨Nat.add⟩
+ expecting fPolyInst
+
+def fPolyNotInst {α : Type u} (inst : Add α) : α → α → α := Add.add
+
+#testDelab @fPolyNotInst Nat ⟨Nat.add⟩
+ expecting fPolyNotInst { add := Nat.add : Add Nat }
+
+#testDelab (fun (x : Nat) => x) Nat.zero
+ expecting (fun (x : Nat) => x) Nat.zero
+
+#testDelab (fun (α : Type) (x : α) => x) Nat Nat.zero
+ expecting (fun (α : Type) (x : α) => x) _ Nat.zero
+
+#testDelab (fun {α : Type} (x : α) => x) Nat.zero
+ expecting (fun {α : Type} (x : α) => x) Nat.zero
+
+#testDelab ((@Add.mk Nat Nat.add).1 : Nat → Nat → Nat)
+ expecting Add.add
+
+class Foo (α : Type v) where foo : α
+
+instance : Foo Bool := ⟨true⟩
+
+#testDelab @Foo.foo Bool ⟨true⟩
+ expecting Foo.foo
+
+#testDelab @Foo.foo Bool ⟨false⟩
+ expecting Foo.foo (self := { foo := false : Foo Bool })
+
+axiom wild {α : Type u} {f : α → Type v} {x : α} [_inst_1 : Foo (f x)] : Nat
+
+abbrev nat2bool : Nat → Type := fun _ => Bool
+
+#testDelab @wild Nat nat2bool Nat.zero ⟨false⟩
+ expecting wild (f := nat2bool) (x := Nat.zero) (_inst_1 := { foo := false : Foo (nat2bool Nat.zero) })
+
+#testDelab @wild Nat (fun (n : Nat) => Bool) Nat.zero ⟨false⟩
+ expecting wild (f := fun n => Bool) (x := Nat.zero) (_inst_1 := { foo := false : Foo Bool })
+
+#testDelab (fun {α : Type u} (x : α) => x : ∀ {α : Type u}, α → α)
+ expecting fun {α} x => x
+
+#testDelab (fun {α : Type} (x : α) => x) Nat.zero
+ expecting (fun {α : Type} (x : α) => x) Nat.zero
+
+#testDelab (fun {α : Type} [Add α] (x : α) => x + x) (0 : Nat)
+ expecting (fun {α : Type} [Add α] (x : α) => x + x) 0
+
+#testDelab (fun {α : Type} [Add α] (x : α) => x + x) Nat.zero
+ expecting (fun {α : Type} [Add α] (x : α) => x + x) Nat.zero
+
+#testDelab id id id id Nat.zero
+ expecting id id id id Nat.zero
+
+def zzz : Unit := ()
+def Z1.zzz : Unit := ()
+def Z1.Z2.zzz : Unit := ()
+
+namespace Z1.Z2
+
+#testDelab _root_.zzz
+ expecting _root_.zzz
+
+#testDelab Z1.zzz
+ expecting Z1.zzz
+
+#testDelab zzz
+ expecting zzz
+
+end Z1.Z2
+
+#testDelab fun {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (f : σ → α × σ) (s : σ) => pure (f := m) (f s)
+ expecting fun {σ} {m} [Monad m] {α} f s => pure (f s)
+
+set_option pp.analyze.trustSubst false in
+#testDelab (fun (x y z : Nat) (hxy : x = y) (hyz : x = z) => hxy ▸ hyz : ∀ (x y z : Nat), x = y → x = z → y = z)
+ expecting fun x y z hxy hyz => Eq.ndrec (a := x) (motive := fun x => x = z) hyz hxy
+
+set_option pp.analyze.trustSubst true in
+#testDelab (fun (x y z : Nat) (hxy : x = y) (hyz : x = z) => hxy ▸ hyz : ∀ (x y z : Nat), x = y → x = z → y = z)
+ expecting fun x y z hxy hyz => hxy ▸ hyz
+
+def fooReadGetModify : ReaderT Unit (StateT Unit IO) Unit := do
+ let _ ← read
+ let _ ← get
+ modify fun s => s
+
+#testDelab
+ (do discard read
+ pure () : ReaderT Bool IO Unit)
+ expecting
+ do discard read
+ pure ()
+
+#testDelab
+ ((do let ctx ← read
+ let s ← get
+ modify fun s => s : ReaderT Bool (StateT Bool IO) Unit))
+ expecting
+ do let _ ← read
+ let _ ← get
+ modify fun s => s
+
+#testDelabN Nat.brecOn
+#testDelabN Nat.below
+#testDelabN Nat.mod_lt
+#testDelabN Array.qsort
+#testDelabN List.partition
+#testDelabN List.partitionAux
+#testDelabN StateT.modifyGet
+#testDelabN Nat.gcd_one_left
+#testDelabN List.hasDecidableLt
+#testDelabN Lean.Xml.parse
+#testDelabN Add.noConfusionType
+#testDelabN List.filterMapM.loop
+
+#testDelabN instInhabitedPUnit
+#testDelabN Lean.Syntax.getOptionalIdent?
+#testDelabN Lean.Meta.ppExpr
+#testDelabN Eq.mprProp
+
+-- TODO: this test is broken because of the inability to solve structural max constraints
+-- #testDelabN Lean.PrefixTree.empty
+
+-- TODO: this is broken because it is printing inaccessible names
+-- #testDelabN Std.ShareCommon.ObjectMap.find?
+
+-- TODO: these all fail currently for undiagnosed reasons
+--#testDelabN MonadLift.noConfusion
+--#testDelabN instMonadReaderOf
+--#testDelabN MonadLift.noConfusionType
diff --git a/tests/lean/run/new_compiler.lean b/tests/lean/run/new_compiler.lean
index 9e2c2668a2..75db267656 100644
--- a/tests/lean/run/new_compiler.lean
+++ b/tests/lean/run/new_compiler.lean
@@ -4,7 +4,7 @@ universe u v w r s
set_option trace.compiler.stage1 true
-- set_option pp.explicit true
-set_option pp.binder_types false
+set_option pp.binderTypes false
-- set_option pp.proofs true
def foo (n : Nat) : Nat :=
diff --git a/tests/lean/run/rc_tests.lean b/tests/lean/run/rc_tests.lean
index e5ccb3e9ee..de32d5bdb1 100644
--- a/tests/lean/run/rc_tests.lean
+++ b/tests/lean/run/rc_tests.lean
@@ -1,7 +1,7 @@
universe u v
--- set_option pp.binder_types false
+-- set_option pp.binderTypes false
set_option pp.explicit true
set_option trace.compiler.llnf true
-- set_option trace.compiler.boxed true
diff --git a/tests/lean/safeShadowing.lean b/tests/lean/safeShadowing.lean
index 0c12946503..f42792b5b2 100644
--- a/tests/lean/safeShadowing.lean
+++ b/tests/lean/safeShadowing.lean
@@ -13,7 +13,7 @@ variable {α : Type}
#print f
-set_option pp.safe_shadowing false
+set_option pp.safeShadowing false
#check fun {α} (a : α) => a
diff --git a/tests/lean/server/content_diag.json b/tests/lean/server/content_diag.json
index 8e8a5837ea..2db75f3322 100644
--- a/tests/lean/server/content_diag.json
+++ b/tests/lean/server/content_diag.json
@@ -49,9 +49,9 @@
"range":
{"start": {"line": 24, "character": 0},
"end": {"line": 24, "character": 6}},
- "message": "def MyNs.u : Unit :=\nUnit.unit",
+ "message": "def MyNs.u : Unit :=\n()",
"fullRange":
{"start": {"line": 24, "character": 0},
"end": {"line": 24, "character": 6}}}]},
"method": "textDocument/publishDiagnostics",
- "jsonrpc": "2.0"}
\ No newline at end of file
+ "jsonrpc": "2.0"}
diff --git a/tests/lean/server/edits_diag.json b/tests/lean/server/edits_diag.json
index 7a65571146..1d4260cc3d 100644
--- a/tests/lean/server/edits_diag.json
+++ b/tests/lean/server/edits_diag.json
@@ -34,7 +34,7 @@
"range":
{"start": {"line": 16, "character": 0},
"end": {"line": 16, "character": 6}},
- "message": "def α : Unit :=\nUnit.unit",
+ "message": "def α : Unit :=\n()",
"code": null}]},
"method": "textDocument/publishDiagnostics",
- "jsonrpc": "2.0"}
\ No newline at end of file
+ "jsonrpc": "2.0"}
diff --git a/tests/playground/mapVShmap.lean b/tests/playground/mapVShmap.lean
index 11e49d1c5c..ef663940ca 100644
--- a/tests/playground/mapVShmap.lean
+++ b/tests/playground/mapVShmap.lean
@@ -3,7 +3,7 @@ def mkBigPairs : Nat → Array (Nat × Nat) → Array (Nat × Nat)
| (n+1) ps := mkBigPairs n (ps.push (n, n))
set_option pp.implicit true
-set_option pp.binder_types false
+set_option pp.binderTypes false
-- set_option trace.compiler.specialize true
-- set_option trace.compiler.boxed true