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

chore: trace[...]! ==> trace[...]

Browse source 
@Kha I think this one is a good change, there is no real reason for
using the `!` suffix here.
This commit is contained in:
Leonardo de Moura 2021-03-10 16:29:06 -08:00
parent 55157a3108
commit 68143ca8ba
41 changed files with 183 additions and 194 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Lean/Elab/App.lean
View file

@ -292,13 +292,13 @@ private def propagateExpectedType (arg : Arg) : M Unit := do
modify fun s => { s with propagateExpected := false }
else
let numRemainingArgs := s.args.length
trace[Elab.app.propagateExpectedType]! "etaArgs.size: {s.etaArgs.size}, numRemainingArgs: {numRemainingArgs}, fType: {s.fType}"
trace[Elab.app.propagateExpectedType] "etaArgs.size: {s.etaArgs.size}, numRemainingArgs: {numRemainingArgs}, fType: {s.fType}"
match getForallBody s.explicit numRemainingArgs s.namedArgs s.fType with
| none => pure ()
| some fTypeBody =>
unless fTypeBody.hasLooseBVars do
unless (← hasOptAutoParams fTypeBody) do
trace[Elab.app.propagateExpectedType]! "{expectedType} =?= {fTypeBody}"
trace[Elab.app.propagateExpectedType] "{expectedType} =?= {fTypeBody}"
if (← isDefEq expectedType fTypeBody) then
/- Note that we only set `propagateExpected := false` when propagation has succeeded. -/
modify fun s => { s with propagateExpected := false }
@ -319,7 +319,7 @@ private def finalize : M Expr := do
let s ← get
let mut e := s.f
-- all user explicit arguments have been consumed
trace[Elab.app.finalize]! e
trace[Elab.app.finalize] e
let ref ← getRef
-- Register the error context of implicits
for mvarId in s.toSetErrorCtx do
@ -331,11 +331,11 @@ private def finalize : M Expr := do
`s.etaArgs.isEmpty`. Reason: it may have been unfolded.
-/
let eType ← inferType e
trace[Elab.app.finalize]! "after etaArgs, {e} : {eType}"
trace[Elab.app.finalize] "after etaArgs, {e} : {eType}"
match s.expectedType? with
| none => pure ()
| some expectedType =>
trace[Elab.app.finalize]! "expected type: {expectedType}"
trace[Elab.app.finalize] "expected type: {expectedType}"
-- Try to propagate expected type. Ignore if types are not definitionally equal, caller must handle it.
discard <| isDefEq expectedType eType
synthesizeAppInstMVars
@ -485,7 +485,7 @@ def elabAppArgs (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg)
(expectedType? : Option Expr) (explicit ellipsis : Bool) : TermElabM Expr := do
let fType ← inferType f
let fType ← instantiateMVars fType
trace[Elab.app.args]! "explicit: {explicit}, {f} : {fType}"
trace[Elab.app.args] "explicit: {explicit}, {f} : {fType}"
unless namedArgs.isEmpty && args.isEmpty do
tryPostponeIfMVar fType
ElabAppArgs.main.run' {

4
src/Lean/Elab/Binders.lean
View file

@ -64,7 +64,7 @@ def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
let tactic ← quoteAutoTactic tactic
let val ← elabTerm tactic type
let val ← instantiateMVars val
trace[Elab.autoParam]! val
trace[Elab.autoParam] val
let decl := Declaration.defnDecl { name := name, levelParams := [], type := type, value := val, hints := ReducibilityHints.opaque,
safety := DefinitionSafety.safe }
addDecl decl
@ -518,7 +518,7 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
let type ← mkForallFVars xs type
let val ← mkLambdaFVars xs val
pure (type, val, xs.size)
trace[Elab.let.decl]! "{id.getId} : {type} := {val}"
trace[Elab.let.decl] "{id.getId} : {type} := {val}"
let result ←
if useLetExpr then
withLetDecl id.getId type val fun x => do

1
src/Lean/Elab/BuiltinNotation.lean
View file

@ -154,7 +154,6 @@ private def getPropToDecide (expectedType? : Option Expr) : TermElabM Expr := do
@[builtinTermElab Lean.Parser.Term.decide] def elabDecide : TermElab := fun stx expectedType? => do
let p ← getPropToDecide expectedType?
trace[Meta.debug]! "elabDecide: {p}"
let d ← mkDecide p
let d ← instantiateMVars d
let r ← withDefault <| whnf d

2
src/Lean/Elab/Deriving/BEq.lean
View file

@ -94,7 +94,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
private def mkBEqInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
let ctx ← mkContext "beq" declNames[0]
let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `BEq declNames)
trace[Elab.Deriving.beq]! "\n{cmds}"
trace[Elab.Deriving.beq] "\n{cmds}"
return cmds
open Command

2
src/Lean/Elab/Deriving/DecEq.lean
View file

@ -90,7 +90,7 @@ def mkAuxFunction (ctx : Context) : TermElabM Syntax := do
def mkDecEqCmds (indVal : InductiveVal) : TermElabM (Array Syntax) := do
let ctx ← mkContext "decEq" indVal.name
let cmds := #[← mkAuxFunction ctx] ++ (← mkInstanceCmds ctx `DecidableEq #[indVal.name] (useAnonCtor := false))
trace[Elab.Deriving.decEq]! "\n{cmds}"
trace[Elab.Deriving.decEq] "\n{cmds}"
return cmds
open Command

10
src/Lean/Elab/Deriving/Inhabited.lean
View file

@ -30,7 +30,7 @@ where
let instType ← mkAppM `Inhabited #[x]
if (← isTypeCorrect instType) then
withLocalDeclD (← mkFreshUserName `inst) instType fun inst => do
trace[Elab.Deriving.inhabited]! "adding local instance {instType}"
trace[Elab.Deriving.inhabited] "adding local instance {instType}"
addLocalInstancesForParamsAux k xs (i+1) (map.insert inst.fvarId! i)
else
addLocalInstancesForParamsAux k xs (i+1) map
@ -89,20 +89,20 @@ where
for i in [ctorVal.numParams:xs.size] do
let x := xs[i]
let instType ← mkAppM `Inhabited #[(← inferType x)]
trace[Elab.Deriving.inhabited]! "checking {instType} for '{ctorName}'"
trace[Elab.Deriving.inhabited] "checking {instType} for '{ctorName}'"
match (← trySynthInstance instType) with
| LOption.some e =>
usedInstIdxs ← collectUsedLocalsInsts usedInstIdxs localInst2Index e
| _ =>
trace[Elab.Deriving.inhabited]! "failed to generate instance using '{ctorName}' {if addHypotheses then "(assuming parameters are inhabited)" else ""} because of field with type{indentExpr (← inferType x)}"
trace[Elab.Deriving.inhabited] "failed to generate instance using '{ctorName}' {if addHypotheses then "(assuming parameters are inhabited)" else ""} because of field with type{indentExpr (← inferType x)}"
ok := false
break
if !ok then
return none
else
trace[Elab.Deriving.inhabited]! "inhabited instance using '{ctorName}' {if addHypotheses then "(assuming parameters are inhabited)" else ""} {usedInstIdxs.toList}"
trace[Elab.Deriving.inhabited] "inhabited instance using '{ctorName}' {if addHypotheses then "(assuming parameters are inhabited)" else ""} {usedInstIdxs.toList}"
let cmd ← mkInstanceCmdWith usedInstIdxs
trace[Elab.Deriving.inhabited]! "\n{cmd}"
trace[Elab.Deriving.inhabited] "\n{cmd}"
return some cmd
private def mkInhabitedInstance (declName : Name) : CommandElabM Unit := do

2
src/Lean/Elab/Deriving/Repr.lean
View file

@ -108,7 +108,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
private def mkReprInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
let ctx ← mkContext "repr" declNames[0]
let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Repr declNames)
trace[Elab.Deriving.repr]! "\n{cmds}"
trace[Elab.Deriving.repr] "\n{cmds}"
return cmds
open Command

3
src/Lean/Elab/Deriving/Util.lean
View file

@ -61,7 +61,7 @@ def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do
match typeName.eraseMacroScopes with
| Name.str _ t _ => auxFunNames := auxFunNames.push (← mkFreshUserName <| Name.mkSimple <| fnPrefix ++ t)
| _ => auxFunNames := auxFunNames.push (← mkFreshUserName `instFn)
trace[Elab.Deriving.beq]! "{auxFunNames}"
trace[Elab.Deriving.beq] "{auxFunNames}"
let usePartial := indVal.isNested || typeInfos.size > 1
return {
typeInfos := typeInfos
@ -104,7 +104,6 @@ def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) (
let type ← `($(mkIdent className) $indType)
let val ← if useAnonCtor then `(⟨$(mkIdent auxFunName)⟩) else pure <| mkIdent auxFunName
let instCmd ← `(instance $binders:implicitBinder* : $type := $val)
trace[Meta.debug]! "\n{instCmd}"
instances := instances.push instCmd
return instances

2
src/Lean/Elab/Do.lean
View file

@ -1541,7 +1541,7 @@ def elabDo : TermElab := fun stx expectedType? => do
let m ← mkMonadAlias bindInfo.m
let codeBlock ← ToCodeBlock.run stx m
let stxNew ← liftMacroM $ ToTerm.run codeBlock.code m
trace[Elab.do]! stxNew
trace[Elab.do] stxNew
withMacroExpansion stx stxNew $ elabTermEnsuringType stxNew bindInfo.expectedType
end Do

3
src/Lean/Elab/Inductive.lean
View file

@ -215,7 +215,6 @@ private def elabCtors (indFVars : Array Expr) (indFVar : Expr) (params : Array E
let ctorParams ← Term.addAutoBoundImplicits ctorParams
let type ← mkForallFVars ctorParams type
let type ← mkForallFVars params type
trace[Meta.debug]! "{ctorView.declName} : {type}"
return { name := ctorView.declName, type := type }
where
checkParamOccs (ctorType : Expr) : MetaM Expr :=
@ -339,7 +338,7 @@ private def updateResultingUniverse (numParams : Nat) (indTypes : List Inductive
unless r.isParam do
throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly"
let us ← collectUniverses r rOffset numParams indTypes
trace[Elab.inductive]! "updateResultingUniverse us: {us}, r: {r}, rOffset: {rOffset}"
trace[Elab.inductive] "updateResultingUniverse us: {us}, r: {r}, rOffset: {rOffset}"
let rNew := mkResultUniverse us rOffset
let updateLevel (e : Expr) : Expr := e.replaceLevel fun u => if u == tmpIndParam then some rNew else none
return indTypes.map fun indType =>

18
src/Lean/Elab/Match.lean
View file

@ -47,7 +47,7 @@ private def elabDiscrsWitMatchType (discrStxs : Array Syntax) (matchType : Expr)
match matchType with
| Expr.forallE _ d b _ =>
let discr ← fullApproxDefEq <| elabTermEnsuringType discrStx[1] d
trace[Elab.match]! "discr #{i} {discr} : {d}"
trace[Elab.match] "discr #{i} {discr} : {d}"
if b.hasLooseBVars then
isDep := true
matchType ← b.instantiate1 discr
@ -473,7 +473,7 @@ where
def main (alt : MatchAltView) : M MatchAltView := do
let patterns ← alt.patterns.mapM fun p => do
trace[Elab.match]! "collecting variables at pattern: {p}"
trace[Elab.match] "collecting variables at pattern: {p}"
collect p
return { alt with patterns := patterns }
@ -552,13 +552,13 @@ def finalizePatternDecls (patternVarDecls : Array PatternVarDecl) : TermElabM (A
decls := decls.push decl
| PatternVarDecl.anonymousVar mvarId fvarId =>
let e ← instantiateMVars (mkMVar mvarId);
trace[Elab.match]! "finalizePatternDecls: mvarId: {mvarId} := {e}, fvar: {mkFVar fvarId}"
trace[Elab.match] "finalizePatternDecls: mvarId: {mvarId} := {e}, fvar: {mkFVar fvarId}"
match e with
| Expr.mvar newMVarId _ =>
/- Metavariable was not assigned, or assigned to another metavariable. So,
we assign to the auxiliary free variable we created at `withPatternVars` to `newMVarId`. -/
assignExprMVar newMVarId (mkFVar fvarId)
trace[Elab.match]! "finalizePatternDecls: {mkMVar newMVarId} := {mkFVar fvarId}"
trace[Elab.match] "finalizePatternDecls: {mkMVar newMVarId} := {mkFVar fvarId}"
let decl ← getLocalDecl fvarId
let decl ← instantiateLocalDeclMVars decl
decls := decls.push decl
@ -683,13 +683,13 @@ private def withElaboratedLHS {α} (ref : Syntax) (patternVarDecls : Array Patte
def elabMatchAltView (alt : MatchAltView) (matchType : Expr) : TermElabM (AltLHS × Expr) := withRef alt.ref do
let (patternVars, alt) ← collectPatternVars alt
trace[Elab.match]! "patternVars: {patternVars}"
trace[Elab.match] "patternVars: {patternVars}"
withPatternVars patternVars fun patternVarDecls => do
withElaboratedLHS alt.ref patternVarDecls alt.patterns matchType fun altLHS matchType => do
let rhs ← elabTermEnsuringType alt.rhs matchType
let xs := altLHS.fvarDecls.toArray.map LocalDecl.toExpr
let rhs ← if xs.isEmpty then pure <| mkSimpleThunk rhs else mkLambdaFVars xs rhs
trace[Elab.match]! "rhs: {rhs}"
trace[Elab.match] "rhs: {rhs}"
return (altLHS, rhs)
def mkMatcher (elimName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss : List AltLHS) : TermElabM MatcherResult :=
@ -730,7 +730,7 @@ private def elabMatchAux (discrStxs : Array Syntax) (altViews : Array MatchAltVi
let (discrs, matchType, altLHSS, isDep, rhss) ← commitIfDidNotPostpone do
let ⟨discrs, matchType, isDep, altViews⟩ ← elabMatchTypeAndDiscrs discrStxs matchOptType altViews expectedType
let matchAlts ← liftMacroM <| expandMacrosInPatterns altViews
trace[Elab.match]! "matchType: {matchType}"
trace[Elab.match] "matchType: {matchType}"
let alts ← matchAlts.mapM fun alt => elabMatchAltView alt matchType
/-
We should not use `synthesizeSyntheticMVarsNoPostponing` here. Otherwise, we will not be
@ -796,7 +796,7 @@ private def elabMatchAux (discrStxs : Array Syntax) (altViews : Array MatchAltVi
let r := mkApp matcherResult.matcher motive
let r := mkAppN r discrs
let r := mkAppN r rhss
trace[Elab.match]! "result: {r}"
trace[Elab.match] "result: {r}"
return r
private def getDiscrs (matchStx : Syntax) : Array Syntax :=
@ -852,7 +852,7 @@ private def tryPostponeIfDiscrTypeIsMVar (matchStx : Syntax) : TermElabM Unit :=
| none => throwErrorAt discr "unexpected discriminant" -- see `expandNonAtomicDiscrs?
| some d =>
let dType ← inferType d
trace[Elab.match]! "discr {d} : {dType}"
trace[Elab.match] "discr {d} : {dType}"
tryPostponeIfMVar dType
/-

2
src/Lean/Elab/MutualDef.lean
View file

@ -438,7 +438,7 @@ private partial def mkClosureForAux (toProcess : Array FVarId) : StateRefT Closu
match pickMaxFVar? lctx toProcess with
| none => pure ()
| some fvarId =>
trace[Elab.definition.mkClosure]! "toProcess: {toProcess.map mkFVar}, maxVar: {mkFVar fvarId}"
trace[Elab.definition.mkClosure] "toProcess: {toProcess.map mkFVar}, maxVar: {mkFVar fvarId}"
let toProcess := toProcess.erase fvarId
let localDecl ← getLocalDecl fvarId
match localDecl with

8
src/Lean/Elab/PreDefinition/Main.lean
View file

@ -12,10 +12,10 @@ open Term
private def addAndCompilePartial (preDefs : Array PreDefinition) : TermElabM Unit := do
for preDef in preDefs do
trace[Elab.definition]! "processing {preDef.declName}"
trace[Elab.definition] "processing {preDef.declName}"
forallTelescope preDef.type fun xs type => do
let inh ← liftM $ mkInhabitantFor preDef.declName xs type
trace[Elab.definition]! "inhabitant for {preDef.declName}"
trace[Elab.definition] "inhabitant for {preDef.declName}"
addNonRec { preDef with
kind := DefKind.«opaque»,
value := inh
@ -53,11 +53,11 @@ private def ensureNoUnassignedMVarsAtPreDef (preDef : PreDefinition) : TermElabM
def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := do
for preDef in preDefs do
trace[Elab.definition.body]! "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
for preDef in preDefs do
ensureNoUnassignedMVarsAtPreDef preDef
for preDefs in partitionPreDefs preDefs do
trace[Elab.definition.scc]! "{preDefs.map (·.declName)}"
trace[Elab.definition.scc] "{preDefs.map (·.declName)}"
if preDefs.size == 1 && isNonRecursive preDefs[0] then
let preDef := preDefs[0]
if preDef.modifiers.isNoncomputable then

26
src/Lean/Elab/PreDefinition/Structural.lean
View file

@ -183,7 +183,7 @@ private def throwToBelowFailed {α} : MetaM α :=
private partial def toBelowAux (C : Expr) : Expr → Expr → Expr → MetaM Expr
| belowDict, arg, F => do
let belowDict ← whnf belowDict
trace[Elab.definition.structural]! "belowDict: {belowDict}, arg: {arg}"
trace[Elab.definition.structural] "belowDict: {belowDict}, arg: {arg}"
match belowDict with
| Expr.app (Expr.app (Expr.const `PProd _ _) d1 _) d2 _ =>
(do toBelowAux C d1 arg (← mkAppM `PProd.fst #[F]))
@ -209,7 +209,7 @@ private partial def toBelowAux (C : Expr) : Expr → Expr → Expr → MetaM Exp
/- See toBelow -/
private def withBelowDict {α} (below : Expr) (numIndParams : Nat) (k : Expr → Expr → MetaM α) : MetaM α := do
let belowType ← inferType below
trace[Elab.definition.structural]! "belowType: {belowType}"
trace[Elab.definition.structural] "belowType: {belowType}"
belowType.withApp fun f args => do
let motivePos := numIndParams + 1
unless motivePos < args.size do throwError! "unexpected 'below' type{indentExpr belowType}"
@ -321,12 +321,12 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
To make it work, users have to write the third alternative as `| zs => g zs + 2`
If this is too annoying in practice, we may replace `ys` with the matching term, but
this may generate weird error messages, when it doesn't work. -/
trace[Elab.definition.structural]! "below before matcherApp.addArg: {below} : {← inferType below}"
trace[Elab.definition.structural] "below before matcherApp.addArg: {below} : {← inferType below}"
let matcherApp ← mapError (matcherApp.addArg below) (fun msg => "failed to add `below` argument to 'matcher' application" ++ indentD msg)
modify fun s => { s with matcherBelowDep := s.matcherBelowDep.insert matcherApp.matcherName }
let altsNew ← (Array.zip matcherApp.alts matcherApp.altNumParams).mapM fun (alt, numParams) =>
lambdaTelescope alt fun xs altBody => do
trace[Elab.definition.structural]! "altNumParams: {numParams}, xs: {xs}"
trace[Elab.definition.structural] "altNumParams: {numParams}, xs: {xs}"
unless xs.size >= numParams do
throwError! "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
let belowForAlt := xs[numParams - 1]
@ -340,15 +340,15 @@ private def mkBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr)
let type := (← inferType value).headBeta
let major := recArgInfo.ys[recArgInfo.pos]
let otherArgs := recArgInfo.ys.filter fun y => y != major && !recArgInfo.indIndices.contains y
trace[Elab.definition.structural]! "fixedParams: {recArgInfo.fixedParams}, otherArgs: {otherArgs}"
trace[Elab.definition.structural] "fixedParams: {recArgInfo.fixedParams}, otherArgs: {otherArgs}"
let motive ← mkForallFVars otherArgs type
let mut brecOnUniv ← getLevel motive
trace[Elab.definition.structural]! "brecOn univ: {brecOnUniv}"
trace[Elab.definition.structural] "brecOn univ: {brecOnUniv}"
let useBInductionOn := recArgInfo.reflexive && brecOnUniv == levelZero
if recArgInfo.reflexive && brecOnUniv != levelZero then
brecOnUniv ← decLevel brecOnUniv
let motive ← mkLambdaFVars (recArgInfo.indIndices.push major) motive
trace[Elab.definition.structural]! "brecOn motive: {motive}"
trace[Elab.definition.structural] "brecOn motive: {motive}"
let brecOn :=
if useBInductionOn then
Lean.mkConst (mkBInductionOnName recArgInfo.indName) recArgInfo.indLevels
@ -360,12 +360,12 @@ private def mkBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr)
let brecOn := mkApp brecOn major
check brecOn
let brecOnType ← inferType brecOn
trace[Elab.definition.structural]! "brecOn {brecOn}"
trace[Elab.definition.structural]! "brecOnType {brecOnType}"
trace[Elab.definition.structural] "brecOn {brecOn}"
trace[Elab.definition.structural] "brecOnType {brecOnType}"
forallBoundedTelescope brecOnType (some 1) fun F _ => do
let F := F[0]
let FType ← inferType F
trace[Elab.definition.structural]! "FType: {FType}"
trace[Elab.definition.structural] "FType: {FType}"
let FType ← instantiateForall FType recArgInfo.indIndices
let FType ← instantiateForall FType #[major]
forallBoundedTelescope FType (some 1) fun below _ => do
@ -378,14 +378,14 @@ private def mkBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr)
private def elimRecursion (preDef : PreDefinition) : M PreDefinition :=
withoutModifyingEnv do lambdaTelescope preDef.value fun xs value => do
addAsAxiom preDef
trace[Elab.definition.structural]! "{preDef.declName} {xs} :=\n{value}"
trace[Elab.definition.structural] "{preDef.declName} {xs} :=\n{value}"
let numFixed ← getFixedPrefix preDef.declName xs value
trace[Elab.definition.structural]! "numFixed: {numFixed}"
trace[Elab.definition.structural] "numFixed: {numFixed}"
findRecArg numFixed xs fun recArgInfo => do
-- when (recArgInfo.indName == `Nat) throwStructuralFailed -- HACK to skip Nat argument
let valueNew ← mkBRecOn preDef.declName recArgInfo value
let valueNew ← mkLambdaFVars xs valueNew
trace[Elab.definition.structural]! "result: {valueNew}"
trace[Elab.definition.structural] "result: {valueNew}"
-- Recursive applications may still occur in expressions that were not visited by replaceRecApps (e.g., in types)
let valueNew ← ensureNoRecFn preDef.declName valueNew
pure { preDef with value := valueNew }

4
src/Lean/Elab/Quotation.lean
View file

@ -403,7 +403,7 @@ private def deduplicate (floatedLetDecls : Array Syntax) : Alt → TermElabM (Ar
(floatedLetDecls.push (← `(letDecl|rhs $vars:ident* := $rhs)), (pats, rhs'))
private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : TermElabM Syntax := do
trace[Elab.match_syntax]! "match {discrs} with {alts}"
trace[Elab.match_syntax] "match {discrs} with {alts}"
match discrs, alts with
| [], ([], rhs)::_ => pure rhs -- nothing left to match
| _, [] => throwError "non-exhaustive 'match_syntax'"
@ -461,7 +461,7 @@ def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
-- no quotations => fall back to regular `match`
throwUnsupportedSyntax
let stx ← compileStxMatch discrs.toList (patss.map (·.toList) |>.zip rhss).toList
trace[Elab.match_syntax.result]! "{stx}"
trace[Elab.match_syntax.result] "{stx}"
stx
| _ => throwUnsupportedSyntax

8
src/Lean/Elab/StructInst.lean
View file

@ -127,9 +127,9 @@ private def elabModifyOp (stx modifyOp source : Syntax) (expectedType? : Option
let idx := lval[1]
let self := source[0]
let stxNew ← `($(self).modifyOp (idx := $idx) (fun s => $val))
trace[Elab.struct.modifyOp]! "{stx}\n===>\n{stxNew}"
trace[Elab.struct.modifyOp] "{stx}\n===>\n{stxNew}"
withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
trace[Elab.struct.modifyOp]! "{modifyOp}\nSource: {source}"
trace[Elab.struct.modifyOp] "{modifyOp}\nSource: {source}"
let rest := modifyOp[0][1]
if rest.isNone then
cont modifyOp[2]
@ -143,7 +143,7 @@ private def elabModifyOp (stx modifyOp source : Syntax) (expectedType? : Option
let valSource := source.modifyArg 0 fun _ => s
let val := stx.setArg 1 valSource
let val := val.setArg 2 <| mkNullNode #[mkNullNode #[valField, mkNullNode]]
trace[Elab.struct.modifyOp]! "{stx}\nval: {val}"
trace[Elab.struct.modifyOp] "{stx}\nval: {val}"
cont val
/- Get structure name and elaborate explicit source (if available) -/
@ -789,7 +789,7 @@ private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sour
| Except.error ex => throwError ex
| Except.ok struct =>
let struct ← expandStruct struct
trace[Elab.struct]! "{struct}"
trace[Elab.struct] "{struct}"
let (r, struct) ← elabStruct struct expectedType?
DefaultFields.propagate struct
pure r

4
src/Lean/Elab/Structure.lean
View file

@ -431,7 +431,6 @@ private def mkCtor (view : StructView) (levelParams : List Name) (params : Array
let type ← addCtorFields fieldInfos fieldInfos.size type
let type ← mkForallFVars params type
let type ← instantiateMVars type
trace[Meta.debug]! "ctor type: {type}"
let type := type.inferImplicit params.size !view.ctor.inferMod
pure { name := view.ctor.declName, type := type }
@ -488,7 +487,7 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
else
checkResultingUniverse (← getResultUniverse type)
pure type
trace[Elab.structure]! "type: {type}"
trace[Elab.structure] "type: {type}"
let usedLevelNames ← collectLevelParamsInStructure type scopeVars view.params fieldInfos
match sortDeclLevelParams view.scopeLevelNames view.allUserLevelNames usedLevelNames with
| Except.error msg => withRef view.ref <| throwError msg
@ -497,7 +496,6 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
let ctor ← mkCtor view levelParams params fieldInfos
let type ← mkForallFVars params type
let type ← instantiateMVars type
trace[Meta.debug]! "type: {type}"
let indType := { name := view.declName, type := type, ctors := [ctor] : InductiveType }
let decl := Declaration.inductDecl levelParams params.size [indType] view.modifiers.isUnsafe
Term.ensureNoUnassignedMVars decl

6
src/Lean/Elab/SyntheticMVars.lean
View file

@ -101,14 +101,14 @@ private def tryToSynthesizeUsingDefaultInstance (mvarId : MVarId) (defaultInstan
let candidate := Lean.mkConst defaultInstance (← mkFreshLevelMVars constInfo.levelParams.length)
let (mvars, bis, _) ← forallMetaTelescopeReducing (← inferType candidate)
let candidate := mkAppN candidate mvars
trace[Elab.resume]! "trying default instance for {mkMVar mvarId} := {candidate}"
trace[Elab.resume] "trying default instance for {mkMVar mvarId} := {candidate}"
if (← isDefEqGuarded (mkMVar mvarId) candidate) then
-- Succeeded. Collect new TC problems
let mut result := []
for i in [:bis.size] do
if bis[i] == BinderInfo.instImplicit then
result := { mvarId := mvars[i].mvarId!, stx := (← getRef), kind := SyntheticMVarKind.typeClass } :: result
trace[Elab.resume]! "worked"
trace[Elab.resume] "worked"
return some result
else
return none
@ -239,7 +239,7 @@ mutual
-- We use `traceM` because we want to make sure the metavar local context is used to trace the message
traceM `Elab.postpone (withMVarContext mvarDecl.mvarId do addMessageContext m!"resuming {mkMVar mvarDecl.mvarId}")
let succeeded ← synthesizeSyntheticMVar mvarDecl postponeOnError runTactics
trace[Elab.postpone]! if succeeded then fmt "succeeded" else fmt "not ready yet"
trace[Elab.postpone] if succeeded then fmt "succeeded" else fmt "not ready yet"
pure !succeeded
-- Merge new synthetic metavariables with `remainingSyntheticMVars`, i.e., metavariables that still couldn't be synthesized
modify fun s => { s with syntheticMVars := s.syntheticMVars ++ remainingSyntheticMVars }

10
src/Lean/Elab/Term.lean
View file

@ -876,7 +876,7 @@ def tryPostponeIfHasMVars (expectedType? : Option Expr) (msg : String) : TermEla
pure expectedType
private def postponeElabTerm (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
trace[Elab.postpone]! "{stx} : {expectedType?}"
trace[Elab.postpone] "{stx} : {expectedType?}"
let mvar ← mkFreshExprMVar expectedType? MetavarKind.syntheticOpaque
let ctx ← read
registerSyntheticMVar stx mvar.mvarId! (SyntheticMVarKind.postponed ctx.macroStack ctx.declName?)
@ -980,7 +980,7 @@ private def elabImplicitLambdaAux (stx : Syntax) (catchExPostpone : Bool) (expec
let body ← elabUsingElabFns stx expectedType catchExPostpone
let body ← ensureHasType expectedType body
let r ← mkLambdaFVars fvars body
trace[Elab.implicitForall]! r
trace[Elab.implicitForall] r
pure r
private partial def elabImplicitLambda (stx : Syntax) (catchExPostpone : Bool) : Expr → Array Expr → TermElabM Expr
@ -998,7 +998,7 @@ private partial def elabImplicitLambda (stx : Syntax) (catchExPostpone : Bool) :
/- Main loop for `elabTerm` -/
private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone : Bool) (implicitLambda : Bool) : Syntax → TermElabM Expr
| stx => withFreshMacroScope <| withIncRecDepth do
trace[Elab.step]! "expected type: {expectedType?}, term\n{stx}"
trace[Elab.step] "expected type: {expectedType?}, term\n{stx}"
checkMaxHeartbeats "elaborator"
withNestedTraces do
let env ← getEnv
@ -1157,9 +1157,9 @@ builtin_initialize registerTraceClass `Elab.letrec
/- Return true if mvarId is an auxiliary metavariable created for compiling `let rec` or it
is delayed assigned to one. -/
def isLetRecAuxMVar (mvarId : MVarId) : TermElabM Bool := do
trace[Elab.letrec]! "mvarId: {mkMVar mvarId} letrecMVars: {(← get).letRecsToLift.map (mkMVar $ ·.mvarId)}"
trace[Elab.letrec] "mvarId: {mkMVar mvarId} letrecMVars: {(← get).letRecsToLift.map (mkMVar $ ·.mvarId)}"
let mvarId := (← getMCtx).getDelayedRoot mvarId
trace[Elab.letrec]! "mvarId root: {mkMVar mvarId}"
trace[Elab.letrec] "mvarId root: {mkMVar mvarId}"
return (← get).letRecsToLift.any (·.mvarId == mvarId)
/- =======================================

10
src/Lean/Meta/AppBuilder.lean
View file

@ -51,14 +51,14 @@ def mkHEqRefl (a : Expr) : MetaM Expr := do
return mkApp2 (mkConst ``HEq.refl [u]) aType a
def mkAbsurd (e : Expr) (hp hnp : Expr) : MetaM Expr := do
let p ← inferType hp
let u ← getLevel e
return mkApp4 (mkConst ``absurd [u]) p e hp hnp
let p ← inferType hp
let u ← getLevel e
return mkApp4 (mkConst ``absurd [u]) p e hp hnp
def mkFalseElim (e : Expr) (h : Expr) : MetaM Expr := do
let u ← getLevel e
return mkApp2 (mkConst ``False.elim [u]) e h
private def infer (h : Expr) : MetaM Expr := do
let hType ← inferType h
whnfD hType
@ -243,7 +243,7 @@ def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := do
traceCtx `Meta.appBuilder <| withNewMCtxDepth do
let (f, fType) ← mkFun constName
let r ← mkAppMArgs f fType xs
trace[Meta.appBuilder]! "constName: {constName}, xs: {xs}, result: {r}"
trace[Meta.appBuilder] "constName: {constName}, xs: {xs}, result: {r}"
return r
private partial def mkAppOptMAux (f : Expr) (xs : Array (Option Expr)) : Nat → Array Expr → Nat → Array MVarId → Expr → MetaM Expr

2
src/Lean/Meta/Check.lean
View file

@ -186,7 +186,7 @@ def isTypeCorrect (e : Expr) : MetaM Bool := do
check e
pure true
catch ex =>
trace[Meta.typeError]! ex.toMessageData
trace[Meta.typeError] ex.toMessageData
pure false
builtin_initialize

4
src/Lean/Meta/Closure.lean
View file

@ -347,7 +347,7 @@ end Closure
returned where `u_i`s are universe parameters and metavariables `type` and `value` depend on,
and `t_j`s are free and meta variables `type` and `value` depend on. -/
def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := false) (compile : Bool := true) : MetaM Expr := do
trace[Meta.debug]! "{name} : {type} := {value}"
trace[Meta.debug] "{name} : {type} := {value}"
let result ← Closure.mkValueTypeClosure type value zeta
let env ← getEnv
let decl := Declaration.defnDecl {
@ -358,7 +358,7 @@ def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := f
hints := ReducibilityHints.regular (getMaxHeight env result.value + 1),
safety := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe
}
trace[Meta.debug]! "{name} : {result.type} := {result.value}"
trace[Meta.debug] "{name} : {result.type} := {result.value}"
addDecl decl
if compile then
compileDecl decl

34
src/Lean/Meta/ExprDefEq.lean
View file

@ -229,18 +229,18 @@ private partial def isDefEqBindingAux (lctx : LocalContext) (fvars : Array Expr)
private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
traceCtx `Meta.isDefEq.assign.checkTypes do
if !mvar.isMVar then
trace[Meta.isDefEq.assign.final]! "metavariable expected at {mvar} := {v}"
trace[Meta.isDefEq.assign.final] "metavariable expected at {mvar} := {v}"
return false
else
-- must check whether types are definitionally equal or not, before assigning and returning true
let mvarType ← inferType mvar
let vType ← inferType v
if (← withTransparency TransparencyMode.default <| Meta.isExprDefEqAux mvarType vType) then
trace[Meta.isDefEq.assign.final]! "{mvar} := {v}"
trace[Meta.isDefEq.assign.final] "{mvar} := {v}"
assignExprMVar mvar.mvarId! v
pure true
else
trace[Meta.isDefEq.assign.typeMismatch]! "{mvar} : {mvarType} := {v} : {vType}"
trace[Meta.isDefEq.assign.typeMismatch] "{mvar} : {mvarType} := {v} : {vType}"
pure false
/--
@ -278,7 +278,7 @@ private partial def mkLambdaFVarsWithLetDeps (xs : Array Expr) (v : Expr) : Meta
mkLambdaFVars xs v
else
let ys ← addLetDeps
trace[Meta.debug]! "ys: {ys}, v: {v}"
trace[Meta.debug] "ys: {ys}, v: {v}"
mkLambdaFVars ys v
where
@ -834,7 +834,7 @@ private partial def processAssignmentFOApprox (mvar : Expr) (args : Array Expr)
if !cfg.foApprox then
pure false
else
trace[Meta.isDefEq.foApprox]! "{mvar} {args} := {v}"
trace[Meta.isDefEq.foApprox] "{mvar} {args} := {v}"
let v := v.headBeta
if (← commitWhen <| processAssignmentFOApproxAux mvar args v) then
pure true
@ -872,7 +872,7 @@ private def assignConst (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM Bool :=
match (← checkAssignment mvar.mvarId! #[] v) with
| none => pure false
| some v =>
trace[Meta.isDefEq.constApprox]! "{mvar} := {v}"
trace[Meta.isDefEq.constApprox] "{mvar} := {v}"
checkTypesAndAssign mvar v
private def processConstApprox (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM Bool := do
@ -888,7 +888,7 @@ private def processConstApprox (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM
It assumes `?m` is unassigned. -/
private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :=
traceCtx `Meta.isDefEq.assign do
trace[Meta.isDefEq.assign]! "{mvarApp} := {v}"
trace[Meta.isDefEq.assign] "{mvarApp} := {v}"
let mvar := mvarApp.getAppFn
let mvarDecl ← getMVarDecl mvar.mvarId!
let rec process (i : Nat) (args : Array Expr) (v : Expr) := do
@ -919,7 +919,7 @@ private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :
match (← checkAssignment mvarId args v) with
| none => useFOApprox args
| some v => do
trace[Meta.isDefEq.assign.beforeMkLambda]! "{mvar} {args} := {v}"
trace[Meta.isDefEq.assign.beforeMkLambda] "{mvar} {args} := {v}"
let some v ← mkLambdaFVarsWithLetDeps args v | return false
if args.any (fun arg => mvarDecl.lctx.containsFVar arg) then
/- We need to type check `v` because abstraction using `mkLambdaFVars` may have produced
@ -927,7 +927,7 @@ private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :
if (← isTypeCorrect v) then
checkTypesAndAssign mvar v
else
trace[Meta.isDefEq.assign.typeError]! "{mvar} := {v}"
trace[Meta.isDefEq.assign.typeError] "{mvar} := {v}"
useFOApprox args
else
checkTypesAndAssign mvar v
@ -968,17 +968,17 @@ private def isListLevelDefEq (us vs : List Level) : MetaM LBool :=
/-- Auxiliary method for isDefEqDelta -/
private def isDefEqLeft (fn : Name) (t s : Expr) : MetaM LBool := do
trace[Meta.isDefEq.delta.unfoldLeft]! fn
trace[Meta.isDefEq.delta.unfoldLeft] fn
toLBoolM <| Meta.isExprDefEqAux t s
/-- Auxiliary method for isDefEqDelta -/
private def isDefEqRight (fn : Name) (t s : Expr) : MetaM LBool := do
trace[Meta.isDefEq.delta.unfoldRight]! fn
trace[Meta.isDefEq.delta.unfoldRight] fn
toLBoolM <| Meta.isExprDefEqAux t s
/-- Auxiliary method for isDefEqDelta -/
private def isDefEqLeftRight (fn : Name) (t s : Expr) : MetaM LBool := do
trace[Meta.isDefEq.delta.unfoldLeftRight]! fn
trace[Meta.isDefEq.delta.unfoldLeftRight] fn
toLBoolM <| Meta.isExprDefEqAux t s
/-- Try to solve `f a₁ ... aₙ =?= f b₁ ... bₙ` by solving `a₁ =?= b₁, ..., aₙ =?= bₙ`.
@ -1012,7 +1012,7 @@ private def tryHeuristic (t s : Expr) : MetaM Bool :=
<&&>
isListLevelDefEqAux tFn.constLevels! sFn.constLevels!
unless b do
trace[Meta.isDefEq.delta]! "heuristic failed {t} =?= {s}"
trace[Meta.isDefEq.delta] "heuristic failed {t} =?= {s}"
pure b
/-- Auxiliary method for isDefEqDelta -/
@ -1288,7 +1288,7 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do
let tAssign? ← isAssignable tFn
let sAssign? ← isAssignable sFn
let assignableMsg (b : Bool) := if b then "[assignable]" else "[nonassignable]"
trace[Meta.isDefEq]! "{t} {assignableMsg tAssign?} =?= {s} {assignableMsg sAssign?}"
trace[Meta.isDefEq] "{t} {assignableMsg tAssign?} =?= {s} {assignableMsg sAssign?}"
if tAssign? && !sAssign? then
toLBoolM <| processAssignment' t s
else if !tAssign? && sAssign? then
@ -1297,7 +1297,7 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do
if tFn.isMVar || sFn.isMVar then
let ctx ← read
if ctx.config.isDefEqStuckEx then do
trace[Meta.isDefEq.stuck]! "{t} =?= {s}"
trace[Meta.isDefEq.stuck] "{t} =?= {s}"
Meta.throwIsDefEqStuck
else
pure LBool.false
@ -1337,7 +1337,7 @@ end
@[specialize] private def unstuckMVar (e : Expr) (successK : Expr → MetaM Bool) (failK : MetaM Bool): MetaM Bool := do
match (← getStuckMVar? e) with
| some mvarId =>
trace[Meta.isDefEq.stuckMVar]! "found stuck MVar {mkMVar mvarId} : {← inferType (mkMVar mvarId)}"
trace[Meta.isDefEq.stuckMVar] "found stuck MVar {mkMVar mvarId} : {← inferType (mkMVar mvarId)}"
if (← Meta.synthPending mvarId) then
let e ← instantiateMVars e
successK e
@ -1373,7 +1373,7 @@ private def isDefEqApp (t s : Expr) : MetaM Bool := do
isDefEqOnFailure t s
partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := do
trace[Meta.isDefEq.step]! "{t} =?= {s}"
trace[Meta.isDefEq.step] "{t} =?= {s}"
checkMaxHeartbeats "isDefEq"
withNestedTraces do
whenUndefDo (isDefEqQuick t s) do

12
src/Lean/Meta/LevelDefEq.lean
View file

@ -119,7 +119,7 @@ mutual
if lhs.getLevelOffset == rhs.getLevelOffset then
return lhs.getOffset == rhs.getOffset
else
trace[Meta.isLevelDefEq.step]! "{lhs} =?= {rhs}"
trace[Meta.isLevelDefEq.step] "{lhs} =?= {rhs}"
let lhs' ← instantiateLevelMVars lhs
let lhs' := lhs'.normalize
let rhs' ← instantiateLevelMVars rhs
@ -139,7 +139,7 @@ mutual
if !mctx.hasAssignableLevelMVar lhs && !mctx.hasAssignableLevelMVar rhs then
let ctx ← read
if ctx.config.isDefEqStuckEx && (lhs.isMVar || rhs.isMVar) then do
trace[Meta.isLevelDefEq.stuck]! "{lhs} =?= {rhs}"
trace[Meta.isLevelDefEq.stuck] "{lhs} =?= {rhs}"
Meta.throwIsDefEqStuck
else
return false
@ -181,7 +181,7 @@ else
if numPostponed == 0 then
return true
else
trace[Meta.isLevelDefEq.postponed]! "processing #{numPostponed} postponed is-def-eq level constraints"
trace[Meta.isLevelDefEq.postponed] "processing #{numPostponed} postponed is-def-eq level constraints"
if !(← processPostponedStep) then
return false
else
@ -191,7 +191,7 @@ else
else if numPostponed' < numPostponed then
loop
else
trace[Meta.isLevelDefEq.postponed]! "no progress solving pending is-def-eq level constraints"
trace[Meta.isLevelDefEq.postponed] "no progress solving pending is-def-eq level constraints"
return mayPostpone
loop
@ -257,13 +257,13 @@ private def postponedToMessageData (ps : PersistentArray PostponedEntry) : Messa
def isLevelDefEq (u v : Level) : MetaM Bool :=
traceCtx `Meta.isLevelDefEq do
let b ← commitWhen (mayPostpone := true) <| Meta.isLevelDefEqAux u v
trace[Meta.isLevelDefEq]! "{u} =?= {v} ... {if b then "success" else "failure"}"
trace[Meta.isLevelDefEq] "{u} =?= {v} ... {if b then "success" else "failure"}"
return b
def isExprDefEq (t s : Expr) : MetaM Bool :=
traceCtx `Meta.isDefEq do
let b ← commitWhen (mayPostpone := true) <| Meta.isExprDefEqAux t s
trace[Meta.isDefEq]! "{t} =?= {s} ... {if b then "success" else "failure"}"
trace[Meta.isDefEq] "{t} =?= {s} ... {if b then "success" else "failure"}"
return b
abbrev isDefEq (t s : Expr) : MetaM Bool :=

6
src/Lean/Meta/Match/CaseValues.lean
View file

@ -45,11 +45,11 @@ def caseValueAux (mvarId : MVarId) (fvarId : FVarId) (value : Expr) (hName : Nam
let clearH := false
let (thenSubst, thenMVarId) ← substCore thenMVarId thenH symm subst clearH
withMVarContext thenMVarId do
trace[Meta]! "subst domain: {thenSubst.domain}"
trace[Meta] "subst domain: {thenSubst.domain}"
let thenH := (thenSubst.get thenH).fvarId!
trace[Meta]! "searching for decl"
trace[Meta] "searching for decl"
let decl ← getLocalDecl thenH
trace[Meta]! "found decl"
trace[Meta] "found decl"
let thenSubgoal := { mvarId := thenMVarId, newH := (thenSubst.get thenH).fvarId!, subst := thenSubst : CaseValueSubgoal }
pure (thenSubgoal, elseSubgoal)

35
src/Lean/Meta/Match/Match.lean
View file

@ -41,7 +41,7 @@ where
let (minorType, minorNumParams) := if !xs.isEmpty then (minorType, xs.size) else (mkSimpleThunkType minorType, 1)
let idx := alts.length
let minorName := (`h).appendIndexAfter (idx+1)
trace[Meta.Match.debug]! "minor premise {minorName} : {minorType}"
trace[Meta.Match.debug] "minor premise {minorName} : {minorType}"
withLocalDeclD minorName minorType fun minor => do
let rhs := if xs.isEmpty then mkApp minor (mkConst `Unit.unit) else mkAppN minor xs
let minors := minors.push (minor, minorNumParams)
@ -202,20 +202,20 @@ def occurs (fvarId : FVarId) (v : Expr) : Bool :=
def assign (fvarId : FVarId) (v : Expr) : M Bool := do
if occurs fvarId v then
trace[Meta.Match.unify]! "assign occurs check failed, {mkFVar fvarId} := {v}"
trace[Meta.Match.unify] "assign occurs check failed, {mkFVar fvarId} := {v}"
pure false
else
let ctx ← read
if (← isAltVar fvarId) then
trace[Meta.Match.unify]! "{mkFVar fvarId} := {v}"
trace[Meta.Match.unify] "{mkFVar fvarId} := {v}"
modify fun s => { s with fvarSubst := s.fvarSubst.insert fvarId v }
pure true
else
trace[Meta.Match.unify]! "assign failed variable is not local, {mkFVar fvarId} := {v}"
trace[Meta.Match.unify] "assign failed variable is not local, {mkFVar fvarId} := {v}"
pure false
partial def unify (a : Expr) (b : Expr) : M Bool := do
trace[Meta.Match.unify]! "{a} =?= {b}"
trace[Meta.Match.unify] "{a} =?= {b}"
if (← isDefEq a b) then
pure true
else
@ -292,7 +292,7 @@ def processInaccessibleAsCtor (alt : Alt) (ctorName : Name) : MetaM (Option Alt)
let env ← getEnv
match alt.patterns with
| p@(Pattern.inaccessible e) :: ps =>
trace[Meta.Match.match]! "inaccessible in ctor step {e}"
trace[Meta.Match.match] "inaccessible in ctor step {e}"
withExistingLocalDecls alt.fvarDecls do
-- Try to push inaccessible annotations.
let e ← whnfD e
@ -308,7 +308,7 @@ def processInaccessibleAsCtor (alt : Alt) (ctorName : Name) : MetaM (Option Alt)
| _ => unreachable!
private def processConstructor (p : Problem) : MetaM (Array Problem) := do
trace[Meta.Match.match]! "constructor step"
trace[Meta.Match.match] "constructor step"
let env ← getEnv
match p.vars with
| [] => unreachable!
@ -395,7 +395,7 @@ private def isFirstPatternVar (alt : Alt) : Bool :=
| _ => false
private def processValue (p : Problem) : MetaM (Array Problem) := do
trace[Meta.Match.match]! "value step"
trace[Meta.Match.match] "value step"
match p.vars with
| [] => unreachable!
| x :: xs => do
@ -449,7 +449,7 @@ private def expandVarIntoArrayLit (alt : Alt) (fvarId : FVarId) (arrayElemType :
loop arraySize #[]
private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
trace[Meta.Match.match]! "array literal step"
trace[Meta.Match.match] "array literal step"
match p.vars with
| [] => unreachable!
| x :: xs => do
@ -490,7 +490,7 @@ private def expandNatValuePattern (p : Problem) : Problem := do
{ p with alts := alts }
private def traceStep (msg : String) : StateRefT State MetaM Unit :=
trace[Meta.Match.match]! "{msg} step"
trace[Meta.Match.match] "{msg} step"
private def traceState (p : Problem) : MetaM Unit :=
withGoalOf p (traceM `Meta.Match.match p.toMessageData)
@ -579,7 +579,7 @@ builtin_initialize matcherExt : EnvExtension (Std.PHashMap (Expr × Bool) Name)
/- Similar to `mkAuxDefinition`, but uses the cache `matcherExt`.
It also returns an Boolean that indicates whether a new matcher function was added to the environment or not. -/
def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (Bool × Expr) := do
trace[Meta.debug]! "{name} : {type} := {value}"
trace[Meta.debug] "{name} : {type} := {value}"
let compile := bootstrap.genMatcherCode.get (← getOptions)
let result ← Closure.mkValueTypeClosure type value (zeta := false)
let env ← getEnv
@ -594,7 +594,7 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (B
hints := ReducibilityHints.regular (getMaxHeight env result.value + 1),
safety := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe
}
trace[Meta.debug]! "{name} : {result.type} := {result.value}"
trace[Meta.debug] "{name} : {result.type} := {result.value}"
addDecl decl
if compile then
compileDecl decl
@ -621,9 +621,9 @@ def mkMatcher (matcherName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss :
let uElimGen ← if uElim == levelZero then pure levelZero else mkFreshLevelMVar
let motiveType ← mkForallFVars majors (mkSort uElimGen)
withLocalDeclD `motive motiveType fun motive => do
trace[Meta.Match.debug]! "motiveType: {motiveType}"
trace[Meta.Match.debug] "motiveType: {motiveType}"
let mvarType := mkAppN motive majors
trace[Meta.Match.debug]! "target: {mvarType}"
trace[Meta.Match.debug] "target: {mvarType}"
withAlts motive lhss fun alts minors => do
let mvar ← mkFreshExprMVar mvarType
let examples := majors.toList.map fun major => Example.var major.fvarId!
@ -631,7 +631,7 @@ def mkMatcher (matcherName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss :
let args := #[motive] ++ majors ++ minors.map Prod.fst
let type ← mkForallFVars args mvarType
let val ← mkLambdaFVars args mvar
trace[Meta.Match.debug]! "matcher value: {val}\ntype: {type}"
trace[Meta.Match.debug] "matcher value: {val}\ntype: {type}"
/- The option `bootstrap.gen_matcher_code` is a helper hack. It is useful, for example,
for compiling `src/Init/Data/Int`. It is needed because the compiler uses `Int.decLt`
for generating code for `Int.casesOn` applications, but `Int.casesOn` is used to
@ -644,13 +644,13 @@ def mkMatcher (matcherName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss :
```
which is defined **before** `Int.decLt` -/
let (isNewMatcher, matcher) ← mkMatcherAuxDefinition matcherName type val
trace[Meta.Match.debug]! "matcher levels: {matcher.getAppFn.constLevels!}, uElim: {uElimGen}"
trace[Meta.Match.debug] "matcher levels: {matcher.getAppFn.constLevels!}, uElim: {uElimGen}"
let uElimPos? ← getUElimPos? matcher.getAppFn.constLevels! uElimGen
discard <| isLevelDefEq uElimGen uElim
if isNewMatcher then
addMatcherInfo matcherName { numParams := matcher.getAppNumArgs, numDiscrs := numDiscrs, altNumParams := minors.map Prod.snd, uElimPos? := uElimPos? }
setInlineAttribute matcherName
trace[Meta.Match.debug]! "matcher: {matcher}"
trace[Meta.Match.debug] "matcher: {matcher}"
let unusedAltIdxs := lhss.length.fold (init := []) fun i r =>
if s.used.contains i then r else i::r
pure { matcher := matcher, counterExamples := s.counterExamples, unusedAltIdxs := unusedAltIdxs.reverse }
@ -709,7 +709,6 @@ def MatcherApp.addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp :=
let aux := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) matcherApp.params
let aux := mkApp aux motive
let aux := mkAppN aux matcherApp.discrs
trace! `Meta.debug aux
check aux
unless (← isTypeCorrect aux) do
throwError "failed to add argument to matcher application, type error when constructing the new motive"

18
src/Lean/Meta/SizeOf.lean
View file

@ -68,7 +68,7 @@ where
let type ← inferType motiveFVars[i]
let motive ← forallTelescopeReducing type fun xs _ => do
mkLambdaFVars xs <| mkConst ``Nat
trace[Meta.sizeOf]! "motive: {motive}"
trace[Meta.sizeOf] "motive: {motive}"
loop (i+1) (motives.push motive)
else
k motives
@ -89,7 +89,7 @@ where
| some idx => minor ← mkAdd minor xs'[idx]
| none => minor ← mkAdd minor (← mkAppM ``SizeOf.sizeOf #[x'])
minor ← mkLambdaFVars xs' minor
trace[Meta.sizeOf]! "minor: {minor}"
trace[Meta.sizeOf] "minor: {minor}"
loop (i+1) (minors.push minor)
else
k minors
@ -98,7 +98,7 @@ where
Create a "sizeOf" function with name `declName` using the recursor `recName`.
-/
partial def mkSizeOfFn (recName : Name) (declName : Name): MetaM Unit := do
trace[Meta.sizeOf]! "recName: {recName}"
trace[Meta.sizeOf] "recName: {recName}"
let recInfo : RecursorVal ← getConstInfoRec recName
forallTelescopeReducing recInfo.type fun xs type =>
let levelParams := recInfo.levelParams.tail! -- universe parameters for declaration being defined
@ -118,7 +118,7 @@ partial def mkSizeOfFn (recName : Name) (declName : Name): MetaM Unit := do
let sizeOfParams := params ++ localInsts ++ indices ++ #[major]
let sizeOfType ← mkForallFVars sizeOfParams nat
let val := mkAppN val (minors ++ indices ++ #[major])
trace[Meta.sizeOf]! "val: {val}"
trace[Meta.sizeOf] "val: {val}"
let sizeOfValue ← mkLambdaFVars sizeOfParams val
addDecl <| Declaration.defnDecl {
name := declName
@ -205,7 +205,7 @@ private def recToSizeOf (e : Expr) : M Expr := do
mutual
/-- Construct minor premise proof for `mkSizeOfAuxLemmaProof`. `ys` contains fields and inductive hypotheses for the minor premise. -/
private partial def mkMinorProof (ys : Array Expr) (lhs rhs : Expr) : M Expr := do
trace[Meta.sizeOf.minor]! "{lhs} =?= {rhs}"
trace[Meta.sizeOf.minor] "{lhs} =?= {rhs}"
if (← isDefEq lhs rhs) then
mkEqRefl rhs
else
@ -228,7 +228,7 @@ mutual
mkEqRefl rhs
else
let lhs ← recToSizeOf lhs
trace[Meta.sizeOf.minor.step]! "{lhs} =?= {rhs}"
trace[Meta.sizeOf.minor.step] "{lhs} =?= {rhs}"
let target ← mkEq lhs rhs
for y in ys do
if (← isDefEq (← inferType y) target) then
@ -317,7 +317,7 @@ mutual
`Expr._sizeOf_1 args` is **not** definitionally equal to `sizeOf args`. We need a proof by induction.
-/
private partial def mkSizeOfAuxLemma (lhs rhs : Expr) : M Expr := do
trace[Meta.sizeOf.aux]! "{lhs} =?= {rhs}"
trace[Meta.sizeOf.aux] "{lhs} =?= {rhs}"
match lhs.getAppFn.const? with
| none => throwFailed
| some (fName, us) =>
@ -347,7 +347,7 @@ mutual
let thmType ← mkForallFVars thmParams eq
let thmValue ← mkSizeOfAuxLemmaProof info lhsNew rhsNew
let thmValue ← mkLambdaFVars thmParams thmValue
trace[Meta.sizeOf]! "thmValue: {thmValue}"
trace[Meta.sizeOf] "thmValue: {thmValue}"
addDecl <| Declaration.thmDecl {
name := thmName
levelParams := thmLevelParams
@ -369,7 +369,7 @@ partial def main (lhs rhs : Expr) : M Expr := do
loop lhs rhs
where
loop (lhs rhs : Expr) : M Expr := do
trace[Meta.sizeOf.loop]! "{lhs} =?= {rhs}"
trace[Meta.sizeOf.loop] "{lhs} =?= {rhs}"
if (← isDefEq lhs rhs) then
mkEqRefl rhs
else

32
src/Lean/Meta/SynthInstance.lean
View file

@ -199,7 +199,7 @@ def getInstances (type : Expr) : MetaM (Array Expr) := do
let result ← result.mapM fun e => match e.val with
| Expr.const constName us _ => return e.val.updateConst! (← us.mapM (fun _ => mkFreshLevelMVar))
| _ => panic! "global instance is not a constant"
trace[Meta.synthInstance.globalInstances]! "{type}, {result}"
trace[Meta.synthInstance.globalInstances] "{type}, {result}"
let result := localInstances.foldl (init := result) fun (result : Array Expr) linst =>
if linst.className == className then result.push linst.fvar else result
pure result
@ -224,7 +224,7 @@ def mkGeneratorNode? (key mvar : Expr) : MetaM (Option GeneratorNode) := do
`key` must be `mkTableKey mctx mvarType`. -/
def newSubgoal (mctx : MetavarContext) (key : Expr) (mvar : Expr) (waiter : Waiter) : SynthM Unit :=
withMCtx mctx do
trace[Meta.synthInstance.newSubgoal]! key
trace[Meta.synthInstance.newSubgoal] key
match (← mkGeneratorNode? key mvar) with
| none => pure ()
| some node =>
@ -316,17 +316,17 @@ def tryResolveCore (mvar : Expr) (inst : Expr) : MetaM (Option (MetavarContext
let localInsts ← getLocalInstances
forallTelescopeReducing mvarType fun xs mvarTypeBody => do
let ⟨subgoals, instVal, instTypeBody⟩ ← getSubgoals lctx localInsts xs inst
trace[Meta.synthInstance.tryResolve]! "{mvarTypeBody} =?= {instTypeBody}"
trace[Meta.synthInstance.tryResolve] "{mvarTypeBody} =?= {instTypeBody}"
if (← isDefEq mvarTypeBody instTypeBody) then
let instVal ← mkLambdaFVars xs instVal
if (← isDefEq mvar instVal) then
trace[Meta.synthInstance.tryResolve]! "success"
trace[Meta.synthInstance.tryResolve] "success"
pure (some ((← getMCtx), subgoals))
else
trace[Meta.synthInstance.tryResolve]! "failure assigning"
trace[Meta.synthInstance.tryResolve] "failure assigning"
pure none
else
trace[Meta.synthInstance.tryResolve]! "failure"
trace[Meta.synthInstance.tryResolve] "failure"
pure none
/--
@ -355,7 +355,7 @@ def wakeUp (answer : Answer) : Waiter → SynthM Unit
modify fun s => { s with result := answer.result.expr }
else
let (_, _, answerExpr) ← openAbstractMVarsResult answer.result
trace[Meta.synthInstance]! "skip answer containing metavariables {answerExpr}"
trace[Meta.synthInstance] "skip answer containing metavariables {answerExpr}"
pure ()
| Waiter.consumerNode cNode =>
modify fun s => { s with resumeStack := s.resumeStack.push (cNode, answer) }
@ -370,7 +370,7 @@ private def mkAnswer (cNode : ConsumerNode) : MetaM Answer :=
withMCtx cNode.mctx do
traceM `Meta.synthInstance.newAnswer do m!"size: {cNode.size}, {← inferType cNode.mvar}"
let val ← instantiateMVars cNode.mvar
trace[Meta.synthInstance.newAnswer]! "val: {val}"
trace[Meta.synthInstance.newAnswer] "val: {val}"
let result ← abstractMVars val -- assignable metavariables become parameters
let resultType ← inferType result.expr
pure { result := result, resultType := resultType, size := cNode.size + 1 }
@ -425,7 +425,7 @@ def generate : SynthM Unit := do
let inst := gNode.instances.get! idx
let mctx := gNode.mctx
let mvar := gNode.mvar
trace[Meta.synthInstance.generate]! "instance {inst}"
trace[Meta.synthInstance.generate] "instance {inst}"
modifyTop fun gNode => { gNode with currInstanceIdx := idx }
match (← tryResolve mctx mvar inst) with
| none => pure ()
@ -475,12 +475,12 @@ partial def synth : SynthM (Option Expr) := do
| none => synth
| some result => pure result
else
trace[Meta.synthInstance]! "failed"
trace[Meta.synthInstance] "failed"
pure none
def main (type : Expr) (maxResultSize : Nat) : MetaM (Option Expr) :=
withCurrHeartbeats <| traceCtx `Meta.synthInstance do
trace[Meta.synthInstance]! "main goal {type}"
trace[Meta.synthInstance] "main goal {type}"
let mvar ← mkFreshExprMVar type
let mctx ← getMCtx
let key := mkTableKey mctx type
@ -577,27 +577,27 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
| none =>
let result? ← withNewMCtxDepth do
let normType ← preprocessOutParam type
trace[Meta.synthInstance]! "{type} ==> {normType}"
trace[Meta.synthInstance] "{type} ==> {normType}"
match (← SynthInstance.main normType maxResultSize) with
| none => pure none
| some result =>
trace[Meta.synthInstance]! "FOUND result {result}"
trace[Meta.synthInstance] "FOUND result {result}"
let result ← instantiateMVars result
if (← hasAssignableMVar result) then
trace[Meta.synthInstance]! "Failed has assignable mvar {result.setOption `pp.all true}"
trace[Meta.synthInstance] "Failed has assignable mvar {result.setOption `pp.all true}"
pure none
else
pure (some result)
let result? ← match result? with
| none => pure none
| some result => do
trace[Meta.synthInstance]! "result {result}"
trace[Meta.synthInstance] "result {result}"
let resultType ← inferType result
if (← withConfig (fun _ => inputConfig) <| isDefEq type resultType) then
let result ← instantiateMVars result
pure (some result)
else
trace[Meta.synthInstance]! "result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
trace[Meta.synthInstance] "result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
pure none
if type.hasMVar then
pure result?

2
src/Lean/Meta/Tactic/Cases.lean
View file

@ -296,7 +296,7 @@ def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNam
inductionCasesOn mvarId majorFVarId givenNames ctx
else
let s₁ ← generalizeIndices mvarId majorFVarId
trace[Meta.Tactic.cases]! "after generalizeIndices\n{MessageData.ofGoal s₁.mvarId}"
trace[Meta.Tactic.cases] "after generalizeIndices\n{MessageData.ofGoal s₁.mvarId}"
let s₂ ← inductionCasesOn s₁.mvarId s₁.fvarId givenNames ctx
let s₂ ← elimAuxIndices s₁ s₂
unifyCasesEqs s₁.numEqs s₂

4
src/Lean/Meta/Tactic/Induction.lean
View file

@ -124,7 +124,7 @@ private def throwUnexpectedMajorType {α} (mvarId : MVarId) (majorType : Expr) :
def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (givenNames : Array AltVarNames := #[]) : MetaM (Array InductionSubgoal) :=
withMVarContext mvarId do
trace[Meta.Tactic.induction]! "initial\n{MessageData.ofGoal mvarId}"
trace[Meta.Tactic.induction] "initial\n{MessageData.ofGoal mvarId}"
checkNotAssigned mvarId `induction
let majorLocalDecl ← getLocalDecl majorFVarId
let recursorInfo ← mkRecursorInfo recursorName
@ -168,7 +168,7 @@ def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (gi
subst := subst.insert index.fvarId! (mkFVar indices'[i])
i := i + 1
pure subst
trace[Meta.Tactic.induction]! "after revert&intro\n{MessageData.ofGoal mvarId}"
trace[Meta.Tactic.induction] "after revert&intro\n{MessageData.ofGoal mvarId}"
-- Update indices and major
let indices := indices'.map mkFVar
let majorFVarId := majorFVarId'

1
src/Lean/Meta/Tactic/Injection.lean
View file

@ -93,7 +93,6 @@ def injection (mvarId : MVarId) (fvarId : FVarId) (newNames : List Name := []) (
match (← injectionCore mvarId fvarId) with
| InjectionResultCore.solved => pure InjectionResult.solved
| InjectionResultCore.subgoal mvarId numEqs =>
trace[Meta.debug]! "before injectionIntro\n{MessageData.ofGoal mvarId}"
injectionIntro numEqs mvarId #[] newNames
end Lean.Meta

2
src/Lean/Meta/Tactic/Simp/CongrLemmas.lean
View file

@ -90,7 +90,7 @@ def mkCongrLemma (declName : Name) (prio : Nat) : MetaM CongrLemma := withReduci
foundMVars := foundMVars.insert x.mvarId! |>.insert rhsFn.mvarId!
hypothesesPos := hypothesesPos.push i
i := i + 1
trace[Meta.debug]! "c: {c} : {type}"
trace[Meta.debug] "c: {c} : {type}"
return {
theoremName := declName
funName := lhsFn.constName!

21
src/Lean/Meta/Tactic/Simp/Main.lean
View file

@ -57,7 +57,6 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
match (← getProjectionFnInfo? cinfo.name) with
| none => return none
| some projInfo =>
trace[Meta.debug]! "reduceProjFn? {projInfo.fromClass}, {cinfo.name}, {e}"
if projInfo.fromClass then
if (← read).toUnfold.contains cinfo.name then
-- We only unfold class projections when the user explicitly requested them to be unfolded.
@ -103,7 +102,7 @@ private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
-- TODO: eta reduction
if cfg.proj then
match (← reduceProjFn? e) with
| some e => trace[Meta.debug]! "reduceProjFn? result {e}"; return (← reduce e)
| some e => return (← reduce e)
| none => pure ()
if cfg.iota then
match (← reduceRecMatcher? e) with
@ -168,7 +167,7 @@ where
let mut r ← simp f
let mut i := 0
for arg in args do
trace[Debug.Meta.Tactic.simp]! "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i].hasFwdDeps}"
trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i].hasFwdDeps}"
if i < infos.size && !infos[i].hasFwdDeps then
r ← mkCongr r (← simp arg)
else
@ -192,7 +191,7 @@ where
/- Try to rewrite `e` children using the given congruence lemma -/
tryCongrLemma? (c : CongrLemma) (e : Expr) : M (Option Result) := withNewMCtxDepth do
trace[Debug.Meta.Tactic.simp.congr]! "{c.theoremName}, {e}"
trace[Debug.Meta.Tactic.simp.congr] "{c.theoremName}, {e}"
let info ← getConstInfo c.theoremName
let lemma := mkConst c.theoremName (← info.levelParams.mapM fun _ => mkFreshLevelMVar)
let (xs, bis, type) ← forallMetaTelescopeReducing (← inferType lemma)
@ -208,13 +207,13 @@ where
if (← processCongrHypothesis x) then
modified := true
catch _ =>
trace[Meta.Tactic.simp.congr]! "processCongrHypothesis {c.theoremName} failed {← inferType x}"
trace[Meta.Tactic.simp.congr] "processCongrHypothesis {c.theoremName} failed {← inferType x}"
return none
unless modified do
trace[Meta.Tactic.simp.congr]! "{c.theoremName} not modified"
trace[Meta.Tactic.simp.congr] "{c.theoremName} not modified"
return none
unless (← synthesizeArgs c.theoremName xs bis (← read).discharge?) do
trace[Meta.Tactic.simp.congr]! "{c.theoremName} synthesizeArgs failed"
trace[Meta.Tactic.simp.congr] "{c.theoremName} synthesizeArgs failed"
return none
let eNew ← instantiateMVars rhs
let proof ← instantiateMVars (mkAppN lemma xs)
@ -272,13 +271,13 @@ where
return { expr := eNew, proof? := p }
simpArrow (e : Expr) : M Result := do
trace[Debug.Meta.Tactic.simp]! "arrow {e}"
trace[Debug.Meta.Tactic.simp] "arrow {e}"
let p := e.bindingDomain!
let q := e.bindingBody!
let rp ← simp p
trace[Debug.Meta.Tactic.simp]! "arrow [{(← getConfig).contextual}] {p} [{← isProp p}] -> {q} [{← isProp q}]"
trace[Debug.Meta.Tactic.simp] "arrow [{(← getConfig).contextual}] {p} [{← isProp p}] -> {q} [{← isProp q}]"
if (← (← getConfig).contextual <&&> isProp p <&&> isProp q) then
trace[Debug.Meta.Tactic.simp]! "ctx arrow {rp.expr} -> {q}"
trace[Debug.Meta.Tactic.simp] "ctx arrow {rp.expr} -> {q}"
withLocalDeclD e.bindingName! rp.expr fun h => do
let s ← getSimpLemmas
let s ← s.add h
@ -293,7 +292,7 @@ where
mkImpCongr rp (← simp q)
simpForall (e : Expr) : M Result := withParent e do
trace[Debug.Meta.Tactic.simp]! "forall {e}"
trace[Debug.Meta.Tactic.simp] "forall {e}"
if e.isArrow then
simpArrow e
else if (← isProp e) then

16
src/Lean/Meta/Tactic/Simp/Rewrite.lean
View file

@ -15,19 +15,19 @@ def synthesizeArgs (lemmaName : Name) (xs : Array Expr) (bis : Array BinderInfo)
match ← trySynthInstance type with
| LOption.some val =>
unless (← isDefEq x val) do
trace[Meta.Tactic.simp.discharge]! "{lemmaName}, failed to assign instance{indentExpr type}"
trace[Meta.Tactic.simp.discharge] "{lemmaName}, failed to assign instance{indentExpr type}"
return false
| _ =>
trace[Meta.Tactic.simp.discharge]! "{lemmaName}, failed to synthesize instance{indentExpr type}"
trace[Meta.Tactic.simp.discharge] "{lemmaName}, failed to synthesize instance{indentExpr type}"
return false
else if (← isProp type <&&> (← instantiateMVars x).isMVar) then
match ← discharge? type with
| some proof =>
unless (← isDefEq x proof) do
trace[Meta.Tactic.simp.discharge]! "{lemmaName}, failed to assign proof{indentExpr type}"
trace[Meta.Tactic.simp.discharge] "{lemmaName}, failed to assign proof{indentExpr type}"
return false
| none =>
trace[Meta.Tactic.simp.discharge]! "{lemmaName}, failed to discharge hypotheses{indentExpr type}"
trace[Meta.Tactic.simp.discharge] "{lemmaName}, failed to discharge hypotheses{indentExpr type}"
return false
return true
@ -37,7 +37,7 @@ Remark: the parameter tag is used for creating trace messages. It is irrelevant
def rewrite (e : Expr) (s : DiscrTree SimpLemma) (erased : SimpLemmaNameSet) (discharge? : Expr → SimpM (Option Expr)) (tag : String) : SimpM Result := do
let lemmas ← s.getMatch e
if lemmas.isEmpty then
trace[Debug.Meta.Tactic.simp]! "no lemmas found for {tag}-rewriting {e}"
trace[Debug.Meta.Tactic.simp] "no lemmas found for {tag}-rewriting {e}"
return { expr := e }
else
let lemmas := lemmas.insertionSort fun e₁ e₂ => e₁.priority < e₂.priority
@ -69,16 +69,16 @@ where
if e == rhs then
return none
if lemma.perm && !Expr.lt rhs e then
trace[Meta.Tactic.simp.rewrite]! "{lemma}, perm rejected {e} ==> {rhs}"
trace[Meta.Tactic.simp.rewrite] "{lemma}, perm rejected {e} ==> {rhs}"
return none
trace[Meta.Tactic.simp.rewrite]! "{lemma}, {e} ==> {rhs}"
trace[Meta.Tactic.simp.rewrite] "{lemma}, {e} ==> {rhs}"
return some { expr := rhs, proof? := proof }
else
unless lhs.isMVar do
-- We do not report unification failures when `lhs` is a metavariable
-- Example: `x = ()`
-- TODO: reconsider if we want lemmas such as `(x : Unit) → x = ()`
trace[Meta.Tactic.simp.unify]! "{lemma}, failed to unify {lhs} with {e}"
trace[Meta.Tactic.simp.unify] "{lemma}, failed to unify {lhs} with {e}"
return none
def rewriteCtorEq? (e : Expr) : MetaM (Option Result) := withReducibleAndInstances do

10
src/Lean/Meta/Tactic/Subst.lean
View file

@ -29,16 +29,16 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
match a with
| Expr.fvar aFVarId _ => do
let aFVarIdOriginal := aFVarId
trace[Meta.Tactic.subst]! "substituting {a} (id: {aFVarId}) with {b}"
trace[Meta.Tactic.subst] "substituting {a} (id: {aFVarId}) with {b}"
let mctx ← getMCtx
if mctx.exprDependsOn b aFVarId then
throwTacticEx `subst mvarId m!"'{a}' occurs at{indentExpr b}"
let aLocalDecl ← getLocalDecl aFVarId
let (vars, mvarId) ← revert mvarId #[aFVarId, hFVarId] true
trace[Meta.Tactic.subst]! "after revert {MessageData.ofGoal mvarId}"
trace[Meta.Tactic.subst] "after revert {MessageData.ofGoal mvarId}"
let (twoVars, mvarId) ← introNP mvarId 2
trace[Meta.Tactic.subst]! "after intro2 {MessageData.ofGoal mvarId}"
trace[Meta.Tactic.subst]! "reverted variables {vars}"
trace[Meta.Tactic.subst] "after intro2 {MessageData.ofGoal mvarId}"
trace[Meta.Tactic.subst] "reverted variables {vars}"
let aFVarId := twoVars[0]
let a := mkFVar aFVarId
let hFVarId := twoVars[1]
@ -83,7 +83,7 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
else
pure mvarId
let (newFVars, mvarId) ← introNP mvarId (vars.size - 2)
trace[Meta.Tactic.subst]! "after intro rest {vars.size - 2} {MessageData.ofGoal mvarId}"
trace[Meta.Tactic.subst] "after intro rest {vars.size - 2} {MessageData.ofGoal mvarId}"
let fvarSubst ← newFVars.size.foldM (init := fvarSubst) fun i (fvarSubst : FVarSubst) =>
let var := vars[i+2]
let newFVar := newFVars[i]

8
src/Lean/Meta/UnificationHint.lean
View file

@ -79,7 +79,7 @@ def addUnificationHint (declName : Name) (kind : AttributeKind) : MetaM Unit :=
let keys ← DiscrTree.mkPath hint.pattern.lhs
validateHint declName hint
unificationHintExtension.add { keys := keys, val := declName } kind
trace[Meta.debug]! "addUnificationHint: {unificationHintExtension.getState (← getEnv)}"
trace[Meta.debug] "addUnificationHint: {unificationHintExtension.getState (← getEnv)}"
builtin_initialize
registerBuiltinAttribute {
@ -91,7 +91,7 @@ builtin_initialize
}
def tryUnificationHints (t s : Expr) : MetaM Bool := do
trace[Meta.isDefEq.hint]! "{t} =?= {s}"
trace[Meta.isDefEq.hint] "{t} =?= {s}"
unless (← read).config.unificationHints do
return false
if t.isMVar then
@ -108,7 +108,7 @@ where
tryCandidate candidate : MetaM Bool :=
traceCtx `Meta.isDefEq.hint <| commitWhen do
trace[Meta.isDefEq.hint]! "trying hint {candidate} at {t} =?= {s}"
trace[Meta.isDefEq.hint] "trying hint {candidate} at {t} =?= {s}"
let cinfo ← getConstInfo candidate
let us ← cinfo.levelParams.mapM fun _ => mkFreshLevelMVar
let val := cinfo.instantiateValueLevelParams us
@ -124,7 +124,7 @@ where
match hint? with
| none => return false
| some hint =>
trace[Meta.isDefEq.hint]! "{candidate} succeeded, applying constraints"
trace[Meta.isDefEq.hint] "{candidate} succeeded, applying constraints"
for c in hint.constraints do
unless (← Meta.isExprDefEqAux c.lhs c.rhs) do
return false

4
src/Lean/Meta/WHNF.lean
View file

@ -337,7 +337,7 @@ private def whnfDelayedAssigned? (f' : Expr) (e : Expr) : MetaM (Option Expr) :=
expand let-expressions, expand assigned meta-variables. -/
partial def whnfCore (e : Expr) : MetaM Expr :=
whnfEasyCases e fun e => do
trace[Meta.whnf]! e
trace[Meta.whnf] e
match e with
| Expr.const .. => pure e
| Expr.letE _ _ v b _ => whnfCore $ b.instantiate1 v
@ -519,7 +519,7 @@ def reduceUnaryNatOp (f : Nat → Nat) (a : Expr) : MetaM (Option Expr) :=
def reduceBinNatOp (f : Nat → Nat → Nat) (a b : Expr) : MetaM (Option Expr) :=
withNatValue a fun a =>
withNatValue b fun b => do
trace[Meta.isDefEq.whnf.reduceBinOp]! "{a} op {b}"
trace[Meta.isDefEq.whnf.reduceBinOp] "{a} op {b}"
return mkNatLit <| f a b
def reduceBinNatPred (f : Nat → Nat → Bool) (a b : Expr) : MetaM (Option Expr) := do

2
src/Lean/PrettyPrinter/Delaborator/Basic.lean
View file

@ -380,7 +380,7 @@ end Delaborator
/-- "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]! "{fmt e}"
trace[PrettyPrinter.delab.input] "{fmt e}"
let opts ← MonadOptions.getOptions
catchInternalId Delaborator.delabFailureId
(Delaborator.delab.run { expr := e, defaultOptions := opts, optionsPerPos := optionsPerPos, currNamespace := currNamespace, openDecls := openDecls })

8
src/Lean/PrettyPrinter/Formatter.lean
View file

@ -187,7 +187,7 @@ def tokenWithAntiquot.formatter (p : Formatter) : Formatter := do
@[combinatorFormatter Lean.Parser.categoryParser]
def categoryParser.formatter (cat : Name) : Formatter := group $ indent do
let stx ← getCur
trace[PrettyPrinter.format]! "formatting {indentD (fmt stx)}"
trace[PrettyPrinter.format] "formatting {indentD (fmt stx)}"
if stx.getKind == `choice then
visitArgs do
-- format only last choice
@ -226,7 +226,7 @@ def andthen.formatter (p1 p2 : Formatter) : Formatter := p2 *> p1
def checkKind (k : SyntaxNodeKind) : FormatterM Unit := do
let stx ← getCur
if k != stx.getKind then
trace[PrettyPrinter.format.backtrack]! "unexpected node kind '{stx.getKind}', expected '{k}'"
trace[PrettyPrinter.format.backtrack] "unexpected node kind '{stx.getKind}', expected '{k}'"
throwBacktrack
@[combinatorFormatter Lean.Parser.node]
@ -314,7 +314,7 @@ def symbolNoAntiquot.formatter (sym : String) : Formatter := do
pushToken info sym
goLeft
else do
trace[PrettyPrinter.format.backtrack]! "unexpected syntax '{fmt stx}', expected symbol '{sym}'"
trace[PrettyPrinter.format.backtrack] "unexpected syntax '{fmt stx}', expected symbol '{sym}'"
throwBacktrack
@[combinatorFormatter Lean.Parser.nonReservedSymbolNoAntiquot] def nonReservedSymbolNoAntiquot.formatter := symbolNoAntiquot.formatter
@ -478,7 +478,7 @@ end Formatter
open Formatter
def format (formatter : Formatter) (stx : Syntax) : CoreM Format := do
trace[PrettyPrinter.format.input]! "{fmt stx}"
trace[PrettyPrinter.format.input] "{fmt stx}"
let options ← getOptions
let table ← Parser.builtinTokenTable.get
catchInternalId backtrackExceptionId

12
src/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -204,11 +204,11 @@ def maybeParenthesize (cat : Name) (canJuxtapose : Bool) (mkParen : Syntax → S
let st ← get
-- reset precs for the recursive call
set { stxTrav := st.stxTrav : State }
trace[PrettyPrinter.parenthesize]! "parenthesizing (cont := {(st.contPrec, st.contCat)}){indentD (fmt stx)}"
trace[PrettyPrinter.parenthesize] "parenthesizing (cont := {(st.contPrec, st.contCat)}){indentD (fmt stx)}"
x
let { minPrec := some minPrec, trailPrec := trailPrec, trailCat := trailCat, .. } ← get
| panic! s!"maybeParenthesize: visited a syntax tree without precedences?!{line ++ fmt stx}"
trace[PrettyPrinter.parenthesize]! ("...precedences are {prec} >? {minPrec}" ++ if canJuxtapose then m!", {(trailPrec, trailCat)} <=? {(st.contPrec, st.contCat)}" else "")
trace[PrettyPrinter.parenthesize] ("...precedences are {prec} >? {minPrec}" ++ if canJuxtapose then m!", {(trailPrec, trailCat)} <=? {(st.contPrec, st.contCat)}" else "")
-- Should we parenthesize?
if (prec > minPrec || canJuxtapose && match trailPrec, st.contPrec with | some trailPrec, some contPrec => trailCat == st.contCat && trailPrec <= contPrec | _, _ => false) then
-- The recursive `visit` call, by the invariant, has moved to the preceding node. In order to parenthesize
@ -226,7 +226,7 @@ def maybeParenthesize (cat : Name) (canJuxtapose : Bool) (mkParen : Syntax → S
stx' := stx'.setHeadInfo (SourceInfo.original lead pos "".toSubstring)
if let SourceInfo.original _ pos trail := stx.getTailInfo then
stx' := stx'.setTailInfo (SourceInfo.original "".toSubstring pos trail)
trace! `PrettyPrinter.parenthesize m!"parenthesized: {stx'.formatStx none}"
trace[PrettyPrinter.parenthesize] "parenthesized: {stx'.formatStx none}"
setCur stx'
goLeft
-- after parenthesization, there is no more trailing parser
@ -377,7 +377,7 @@ def andthen.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer :=
def node.parenthesizer (k : SyntaxNodeKind) (p : Parenthesizer) : Parenthesizer := do
let stx ← getCur
if k != stx.getKind then
trace[PrettyPrinter.parenthesize.backtrack]! "unexpected node kind '{stx.getKind}', expected '{k}'"
trace[PrettyPrinter.parenthesize.backtrack] "unexpected node kind '{stx.getKind}', expected '{k}'"
-- HACK; see `orelse.parenthesizer`
throwBacktrack
visitArgs p
@ -399,7 +399,7 @@ def leadingNode.parenthesizer (k : SyntaxNodeKind) (prec : Nat) (p : Parenthesiz
def trailingNode.parenthesizer (k : SyntaxNodeKind) (prec : Nat) (p : Parenthesizer) : Parenthesizer := do
let stx ← getCur
if k != stx.getKind then
trace[PrettyPrinter.parenthesize.backtrack]! "unexpected node kind '{stx.getKind}', expected '{k}'"
trace[PrettyPrinter.parenthesize.backtrack] "unexpected node kind '{stx.getKind}', expected '{k}'"
-- HACK; see `orelse.parenthesizer`
throwBacktrack
visitArgs do
@ -530,7 +530,7 @@ open Parenthesizer
/-- Add necessary parentheses in `stx` parsed by `parser`. -/
def parenthesize (parenthesizer : Parenthesizer) (stx : Syntax) : CoreM Syntax := do
trace[PrettyPrinter.parenthesize.input]! "{fmt stx}"
trace[PrettyPrinter.parenthesize.input] "{fmt stx}"
catchInternalId backtrackExceptionId
(do
let (_, st) ← (parenthesizer {}).run { stxTrav := Syntax.Traverser.fromSyntax stx }

7
src/Lean/Util/Trace.lean
View file

@ -135,13 +135,10 @@ end
def registerTraceClass (traceClassName : Name) : IO Unit :=
registerOption (`trace ++ traceClassName) { group := "trace", defValue := false, descr := "enable/disable tracing for the given module and submodules" }
macro:max "trace!" id:term:max msg:term : term =>
`(trace $id fun _ => ($msg : MessageData))
syntax "trace[" ident "]!" (interpolatedStr(term) <|> term) : term
syntax "trace[" ident "]" (interpolatedStr(term) <|> term) : term
macro_rules
| `(trace[$id]! $s) =>
| `(trace[$id] $s) =>
if s.getKind == interpolatedStrKind then
`(Lean.trace $(quote id.getId) fun _ => m! $s)
else