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

chore: trace messages

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-22 11:18:48 -08:00
parent a9a27c77d8
commit b0ee140670
1 changed files with 12 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/Init/Lean/Meta/ExprDefEq.lean
View file

@ -438,21 +438,21 @@ end CheckAssignment
private def checkAssignmentFailure (mvarId : Name) (fvars : Array Expr) (v : Expr) (ex : CheckAssignment.Exception) : MetaM (Option Expr) :=
match ex with
| CheckAssignment.Exception.occursCheck => do
trace! `Meta.isDefEq.assignment.occursCheck
trace! `Meta.isDefEq.assign.occursCheck
(mkMVar mvarId ++ fvars ++ " := " ++ v);
pure none
| CheckAssignment.Exception.useFOApprox =>
pure none
| CheckAssignment.Exception.outOfScopeFVar fvarId => do
trace! `Meta.isDefEq.assignment.outOfScopeFVar
trace! `Meta.isDefEq.assign.outOfScopeFVar
(mkFVar fvarId ++ " @ " ++ mkMVar mvarId ++ fvars ++ " := " ++ v);
pure none
| CheckAssignment.Exception.readOnlyMVarWithBiggerLCtx nestedMVarId => do
trace! `Meta.isDefEq.assignment.readOnlyMVarWithBiggerLCtx
trace! `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx
(mkMVar nestedMVarId ++ " @ " ++ mkMVar mvarId ++ fvars ++ " := " ++ v);
pure none
| CheckAssignment.Exception.mvarTypeNotWellFormedInSmallerLCtx nestedMVarId => do
trace! `Meta.isDefEq.assignment.mvarTypeNotWellFormedInSmallerLCtx
trace! `Meta.isDefEq.assign.mvarTypeNotWellFormedInSmallerLCtx
(mkMVar nestedMVarId ++ " @ " ++ mkMVar mvarId ++ fvars ++ " := " ++ v);
pure none
| CheckAssignment.Exception.unknownExprMVar mvarId =>
@ -669,13 +669,13 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
| none => useFOApprox ()
| some v => do
v ← mkLambda args v;
let finalize : Unit → MetaM Bool := fun _ => do {
let finalize : Unit → MetaM Bool := fun _ => traceCtx `Meta.isDefEq.assign.checkTypes $ do {
-- must check whether types are definitionally equal or not, before assigning and returning true
mvarType ← inferType mvar;
vType ← inferType v;
condM (usingTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType)
(do assignExprMVar mvarId v; pure true)
(do trace! `Meta.isDefEq.assignment.typeMismatch (mvar ++ " : " ++ mvarType ++ " := " ++ v ++ " : " ++ vType);
(do trace! `Meta.isDefEq.assign.typeMismatch (mvar ++ " : " ++ mvarType ++ " := " ++ v ++ " : " ++ vType);
pure false)
};
if args.any (fun arg => mvarDecl.lctx.containsFVar arg) then
@ -683,7 +683,7 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
a type incorrect term. See discussion at A2 -/
condM (isTypeCorrect v)
(finalize ())
(do trace! `Meta.isDefEq.assignment.typeError (mvar ++ " := " ++ v);
(do trace! `Meta.isDefEq.assign.typeError (mvar ++ " := " ++ v);
useFOApprox ())
else
finalize ()
@ -691,9 +691,11 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
/-- Tries to solve `?m a₁ ... aₙ =?= v` by assigning `?m`.
It assumes `?m` is unassigned. -/
private def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :=
do let mvar := mvarApp.getAppFn;
mvarDecl ← getMVarDecl mvar.mvarId!;
processAssignmentAux mvar mvarDecl v 0 mvarApp.getAppArgs
traceCtx `Meta.isDefEq.assign $ do
trace! `Meta.isDefEq.assign (mvarApp ++ " := " ++ v);
let mvar := mvarApp.getAppFn;
mvarDecl ← getMVarDecl mvar.mvarId!;
processAssignmentAux mvar mvarDecl v 0 mvarApp.getAppArgs
private def isDeltaCandidate (t : Expr) : MetaM (Option ConstantInfo) :=
match t.getAppFn with