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

feat: add throwError! macro and improve trace[..]! macro

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-13 12:31:11 -07:00
parent 39f6aae306
commit bdb92ce7a4
7 changed files with 66 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -13,10 +13,10 @@ open Term
private def addAndCompilePartial (preDefs : Array PreDefinition) : TermElabM Unit := do
for preDef in preDefs do
trace[Elab.definition]! msg!"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]! msg!"inhabitant for {preDef.declName}"
trace[Elab.definition]! "inhabitant for {preDef.declName}"
addNonRec { preDef with
kind := DefKind.«opaque»,
value := inh }
@ -53,7 +53,7 @@ if ← logUnassignedUsingErrorInfos pendingMVarIds then
def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := do
for preDef in preDefs do
trace[Elab.definition.body]! msg!"{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

2
src/Lean/Elab/PreDefinition/MkInhabitant.lean
View file

@ -39,6 +39,6 @@ match ← findAssumption? xs type with
| none =>
match ← mkFnInhabitant? xs type with
| some val => pure val
| none => throwError msg!"failed to compile partial definition '{declName}', failed to show that type is inhabited"
| none => throwError! "failed to compile partial definition '{declName}', failed to show that type is inhabited"
end Lean.Elab

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

@ -85,11 +85,11 @@ let rec loop (i : Nat) : MetaM α := do
let indIndices := indArgs.extract indInfo.nparams indArgs.size
if !indIndices.all Expr.isFVar then
orelseMergeErrors
(throwError msg!"argument #{i+1} was not used because its type is an inductive family and indices are not variables{indentExpr xType}")
(throwError! "argument #{i+1} was not used because its type is an inductive family and indices are not variables{indentExpr xType}")
(loop (i+1))
else if !indIndices.allDiff then
orelseMergeErrors
(throwError msg!"argument #{i+1} was not used because its type is an inductive family and indices are not pairwise distinct{indentExpr xType}")
(throwError! "argument #{i+1} was not used because its type is an inductive family and indices are not pairwise distinct{indentExpr xType}")
(loop (i+1))
else
let indexMinPos := getIndexMinPos xs indIndices
@ -99,13 +99,13 @@ let rec loop (i : Nat) : MetaM α := do
match ← hasBadIndexDep? ys indIndices with
| some (index, y) =>
orelseMergeErrors
(throwError msg!"argument #{i+1} was not used because its type is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}")
(throwError! "argument #{i+1} was not used because its type is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}")
(loop (i+1))
| none =>
match ← hasBadParamDep? ys indParams with
| some (indParam, y) =>
orelseMergeErrors
(throwError msg!"argument #{i+1} was not used because its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}")
(throwError! "argument #{i+1} was not used because its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}")
(loop (i+1))
| none =>
let indicesPos := indIndices.map fun index => match ys.indexOf? index with | some i => i.val | none => unreachable!
@ -129,7 +129,7 @@ private def ensureNoRecFn (recFnName : Name) (e : Expr) : MetaM Expr := do
if containsRecFn recFnName e then
Meta.forEachExpr e fun e => do
if e.isAppOf recFnName then
throwError msg!"unexpected occurrence of recursive application{indentExpr e}"
throwError! "unexpected occurrence of recursive application{indentExpr e}"
pure e
else
pure e
@ -141,7 +141,7 @@ throwError "toBelow failed"
private partial def toBelowAux (C : Expr) : Expr → Expr → Expr → MetaM Expr
| belowDict, arg, F => do
belowDict ← whnf belowDict
trace[Elab.definition.structural]! msg!"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]))
@ -167,10 +167,10 @@ 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]! msg!"belowType: {belowType}"
trace[Elab.definition.structural]! "belowType: {belowType}"
belowType.withApp fun f args => do
let motivePos := numIndParams + 1
unless motivePos < args.size do throwError msg!"unexpected 'below' type{indentExpr belowType}"
unless motivePos < args.size do throwError! "unexpected 'below' type{indentExpr belowType}"
let pre := mkAppN f (args.extract 0 numIndParams)
let preType ← inferType pre
forallBoundedTelescope preType (some 1) fun x _ => do
@ -225,9 +225,9 @@ let rec loop : Expr → Expr → MetaM Expr
let numFixed := recArgInfo.fixedParams.size
let recArgPos := recArgInfo.fixedParams.size + recArgInfo.pos
if recArgPos >= args.size then
throwError msg!"insufficient number of parameters at recursive application {indentExpr e}"
throwError! "insufficient number of parameters at recursive application {indentExpr e}"
let recArg := args[recArgPos]
let f ← try toBelow below recArgInfo.indParams.size recArg catch _ => throwError msg!"failed to eliminate recursive application{indentExpr e}"
let f ← try toBelow below recArgInfo.indParams.size recArg catch _ => throwError! "failed to eliminate recursive application{indentExpr e}"
-- Recall that the fixed parameters are not in the scope of the `brecOn`. So, we skip them.
let argsNonFixed := args.extract numFixed args.size
-- The function `f` does not explicitly take `recArg` and its indices as arguments. So, we skip them too.
@ -279,9 +279,9 @@ let rec loop : Expr → Expr → MetaM Expr
do let matcherApp ← mapError (matcherApp.addArg below) (fun msg => "failed to add `below` argument to 'matcher' application" ++ indentD msg)
let altsNew ← (Array.zip matcherApp.alts matcherApp.altNumParams).mapM fun (alt, numParams) =>
lambdaTelescope alt fun xs altBody => do
trace[Elab.definition.structural]! msg!"altNumParams: {numParams}, xs: {xs}"
trace[Elab.definition.structural]! "altNumParams: {numParams}, xs: {xs}"
unless xs.size >= numParams do
throwError msg!"unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
throwError! "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
let belowForAlt := xs[numParams - 1]
mkLambdaFVars xs (← loop belowForAlt altBody)
pure { matcherApp with alts := altsNew }.toExpr
@ -295,12 +295,12 @@ let major := recArgInfo.ys[recArgInfo.pos]
let otherArgs := recArgInfo.ys.filter fun y => y != major && !recArgInfo.indIndices.contains y
let motive ← mkForallFVars otherArgs type
let brecOnUniv ← getLevel motive
trace[Elab.definition.structural]! msg!"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]! msg!"brecOn motive: {motive}"
trace[Elab.definition.structural]! "brecOn motive: {motive}"
let brecOn :=
if useBInductionOn then
Lean.mkConst (mkBInductionOnFor recArgInfo.indName) recArgInfo.indLevels
@ -312,8 +312,8 @@ let brecOn := mkAppN brecOn recArgInfo.indIndices
let brecOn := mkApp brecOn major
check brecOn
let brecOnType ← inferType brecOn
trace[Elab.definition.structural]! msg!"brecOn {brecOn}"
trace[Elab.definition.structural]! msg!"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
@ -334,13 +334,13 @@ forallBoundedTelescope brecOnType (some 1) fun F _ => do
private def elimRecursion (preDef : PreDefinition) : MetaM PreDefinition :=
withoutModifyingEnv do lambdaTelescope preDef.value fun xs value => do
addAsAxiom preDef
trace[Elab.definition.structural]! msg!"{preDef.declName} {xs} :=\n{value}"
trace[Elab.definition.structural]! "{preDef.declName} {xs} :=\n{value}"
let numFixed := getFixedPrefix preDef.declName xs value
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]! msg!"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 }

12
src/Lean/Elab/Tactic/Basic.lean
View file

@ -20,7 +20,7 @@ def goalsToMessageData (goals : List MVarId) : MessageData :=
MessageData.joinSep (goals.map $ MessageData.ofGoal) (Format.line ++ Format.line)
def Term.reportUnsolvedGoals (goals : List MVarId) : TermElabM Unit := do
throwError msg!"unsolved goals\n{goalsToMessageData goals}"
throwError! "unsolved goals\n{goalsToMessageData goals}"
namespace Tactic
@ -93,7 +93,7 @@ mkElabAttribute Tactic `Lean.Elab.Tactic.tacticElabAttribute `builtinTactic `tac
private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List Tactic) : TacticM Unit := do
let rec loop : List Tactic → TacticM Unit
| [] => throwErrorAt stx msg!"unexpected syntax {indentD stx}"
| [] => throwErrorAt! stx "unexpected syntax {indentD stx}"
| evalFn::evalFns => do
try
evalFn stx
@ -117,7 +117,7 @@ mutual
partial def expandTacticMacroFns (stx : Syntax) (macros : List Macro) : TacticM Unit :=
let rec loop : List Macro → TacticM Unit
| [] => throwErrorAt stx msg!"tactic '{stx.getKind}' has not been implemented"
| [] => throwErrorAt! stx "tactic '{stx.getKind}' has not been implemented"
| m::ms => do
let scp ← getCurrMacroScope
try
@ -177,7 +177,7 @@ let e ← instantiateMVars e
let pendingMVars ← getMVars e
Term.logUnassignedUsingErrorInfos pendingMVars
if e.hasExprMVar then
throwError msg!"tactic failed, resulting expression contains metavariables{indentExpr e}"
throwError! "tactic failed, resulting expression contains metavariables{indentExpr e}"
def withMainMVarContext {α} (x : TacticM α) : TacticM α := do
let (mvarId, _) ← getMainGoal
@ -286,7 +286,7 @@ fun stx => pure ()
fun stx => do
let tactic := stx.getArg 1
if (← do try evalTactic tactic; pure true catch _ => pure false) then
throwError ("tactic succeeded")
throwError "tactic succeeded"
@[builtinTactic traceState] def evalTraceState : Tactic :=
fun stx => do
@ -345,7 +345,7 @@ withRef id do
let fvar? ← liftTermElabM $ Term.isLocalIdent? id;
match fvar? with
| some fvar => pure fvar.fvarId!
| none => throwError msg!"unknown variable '{id.getId}'"
| none => throwError! "unknown variable '{id.getId}'"
def getFVarIds (ids : Array Syntax) : TacticM (Array FVarId) := do
withMainMVarContext $ ids.mapM getFVarId

18
src/Lean/Elab/Tactic/Induction.lean
View file

@ -96,9 +96,9 @@ private def getAltRHS (alt : Syntax) : Syntax := alt.getArg 3
private def checkAltCtorNames (alts : Array Syntax) (ctorNames : List Name) : TacticM Unit := do
for alt in alts do
let n := getAltName alt
withRef alt $ trace[Elab.checkAlt]! msg!"{n} , {alt}"
withRef alt $ trace[Elab.checkAlt]! "{n} , {alt}"
unless n == `_ || ctorNames.any (fun ctorName => n.isSuffixOf ctorName) do
throwErrorAt (alt.getArg 0) msg!"invalid constructor name '{n}'"
throwErrorAt! (alt.getArg 0) "invalid constructor name '{n}'"
structure RecInfo :=
(recName : Name)
@ -143,7 +143,7 @@ match ← getRecFromUsingLoop baseRecName (← inferType major) with
try
liftMetaMAtMain fun _ => Meta.mkRecursorInfo recName
catch _ =>
throwError msg!"invalid recursor name '{baseRecName}'"
throwError! "invalid recursor name '{baseRecName}'"
/- Create `RecInfo` assuming builtin recursor -/
private def getRecInfoDefault (major : Expr) (withAlts : Syntax) (allowMissingAlts : Bool) : TacticM (RecInfo × Array Name) := do
@ -183,7 +183,7 @@ else
altVars := altVars.push []
altRHSs := altRHSs.push Syntax.missing
else
throwError msg!"alternative for constructor '{ctorName}' is missing"
throwError! "alternative for constructor '{ctorName}' is missing"
unless remainingAlts.isEmpty do
throwErrorAt remainingAlts[0] "unused alternative"
pure ({ recName := recName, altVars := altVars, altRHSs := altRHSs }, ctorNames.toArray)
@ -238,7 +238,7 @@ else
altVars := altVars.push (getAltVarNames alt).toList
altRHSs := altRHSs.push (getAltRHS alt)
| none =>
throwError msg!"alternative for minor premise '{paramName}' is missing"
throwError! "alternative for minor premise '{paramName}' is missing"
unless remainingAlts.isEmpty do
throwErrorAt remainingAlts[0] "unused alternative"
pure { recName := recName, altVars := altVars, altRHSs := altRHSs }
@ -252,7 +252,7 @@ if altRHSs.isEmpty then
setGoals $ result.toList.map fun s => s.mvarId
else
unless altRHSs.size == result.size do
throwError msg!"mistmatch on the number of subgoals produced ({result.size}) and alternatives provided ({altRHSs.size})"
throwError! "mistmatch on the number of subgoals produced ({result.size}) and alternatives provided ({altRHSs.size})"
let gs := []
for i in [:result.size] do
let subgoal := result[i]
@ -299,12 +299,12 @@ let rec loop (i j : Nat) : TacticM Unit :=
if ctorName == subgoal.ctorName then
loop (i+1) (j+1)
else
throwError msg!"alternative for '{subgoal.ctorName}' has not been provided"
throwError! "alternative for '{subgoal.ctorName}' has not been provided"
else
throwError msg!"alternative for '{ctorName}' is not needed"
throwError! "alternative for '{ctorName}' is not needed"
else if h : i < casesResult.size then
let subgoal := casesResult.get ⟨i, h⟩
throwError msg!"alternative for '{subgoal.ctorName}' has not been provided"
throwError! "alternative for '{subgoal.ctorName}' has not been provided"
else
pure ()
unless altRHSs.isEmpty do

23
src/Lean/Exception.lean
View file

@ -103,3 +103,26 @@ when (curr == max) $ throwError maxRecDepthErrorMessage;
MonadRecDepth.withRecDepth (curr+1) x
end Lean
new_frontend
namespace Lean
syntax "throwError! " ((interpolatedStr term) <|> term) : term
syntax "throwErrorAt! " term:max ((interpolatedStr term) <|> term) : term
macro_rules
| `(throwError! $msg) =>
if msg.getKind == interpolatedStrKind then
`(throwError (msg! $msg))
else
`(throwError $msg)
macro_rules
| `(throwErrorAt! $ref $msg) =>
if msg.getKind == interpolatedStrKind then
`(throwErrorAt $ref (msg! $msg))
else
`(throwErrorAt $ref $msg)
end Lean

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

@ -135,9 +135,13 @@ namespace Lean
macro:max "trace!" id:term:max msg:term : term => `(trace $id fun _ => ($msg : MessageData))
syntax "trace[" ident "]!" term : term
syntax "trace[" ident "]!" ((interpolatedStr term) <|> term) : term
macro_rules
| `(trace[$id]! $s) => `(Lean.trace $(quote id.getId) fun _ => ($s : MessageData))
| `(trace[$id]! $s) =>
if s.getKind == interpolatedStrKind then
`(Lean.trace $(quote id.getId) fun _ => msg! $s)
else
`(Lean.trace $(quote id.getId) fun _ => ($s : MessageData))
end Lean