feat: top-down heuristic delaboration
This commit is contained in:
Daniel Selsam
Sebastian Ullrich
parent
ea37a29e4c
commit
89364b802b
33 changed files with 992 additions and 272 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 "<input>"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -169,6 +169,7 @@ end MessageData
|
|||
|
||||
structure Message where
|
||||
fileName : String
|
||||
rawPos : Nat
|
||||
pos : Position
|
||||
endPos : Option Position := none
|
||||
severity : MessageSeverity := MessageSeverity.error
|
||||
|
|
|
|||
|
|
@ -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) :=
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
107
src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
Normal file
107
src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
Normal file
|
|
@ -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
|
||||
370
src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
Normal file
370
src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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 := "<ignored>", pos := ⟨0, 0⟩, data := e.toString }
|
||||
let msgs := MessageLog.empty.add { fileName := "<ignored>", rawPos := 0, pos := ⟨0, 0⟩, data := e.toString }
|
||||
pure (← mkEmptyEnvironment, msgs)
|
||||
publishMessages m msgLog hOut
|
||||
let cmdState := Elab.Command.mkState headerEnv msgLog opts
|
||||
|
|
|
|||
|
|
@ -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
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 }
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -1,2 +1,2 @@
|
|||
(fun (this : Unit) => this) Unit.unit : Unit
|
||||
(fun (this : Unit) => this) () : Unit
|
||||
commandPrefix.lean:3:0: error: expected command
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 ()
|
||||
|
|
|
|||
236
tests/lean/run/PPTopDownAnalyze.lean
Normal file
236
tests/lean/run/PPTopDownAnalyze.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ variable {α : Type}
|
|||
|
||||
#print f
|
||||
|
||||
set_option pp.safe_shadowing false
|
||||
set_option pp.safeShadowing false
|
||||
|
||||
#check fun {α} (a : α) => a
|
||||
|
||||
|
|
|
|||
|
|
@ -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"}
|
||||
"jsonrpc": "2.0"}
|
||||
|
|
|
|||
|
|
@ -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"}
|
||||
"jsonrpc": "2.0"}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue