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

feat: save checkAssignment failures as trace messages

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-13 12:42:01 -08:00
parent cace9304ec
commit 46d817135e
2 changed files with 30 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
library/Init/Lean/Message.lean
View file

@ -59,9 +59,10 @@ instance : HasAppend MessageData := ⟨compose⟩
instance : HasFormat MessageData := ⟨fun d => formatAux none d⟩
instance coeOfFormat : HasCoe Format MessageData := ⟨ofFormat⟩
instance coeOfLevel : HasCoe Level MessageData := ⟨ofLevel⟩
instance coeOfExpr : HasCoe Expr MessageData := ⟨ofExpr⟩
instance coeOfFormat : HasCoe Format MessageData := ⟨ofFormat⟩
instance coeOfLevel : HasCoe Level MessageData := ⟨ofLevel⟩
instance coeOfExpr : HasCoe Expr MessageData := ⟨ofExpr⟩
instance coeOfArrayExpr : HasCoe (Array Expr) MessageData := ⟨fun es => node $ es.map $ fun e => ofExpr e⟩
end MessageData

34
library/Init/Lean/Meta/ExprDefEq.lean
View file

@ -539,6 +539,30 @@ partial def check : Expr → CheckAssignmentM Expr
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.checkAssignment.occursCheck
(Expr.mvar mvarId ++ fvars ++ " := " ++ v);
pure none
| CheckAssignment.Exception.useFOApprox =>
pure none
| CheckAssignment.Exception.outOfScopeFVar fvarId => do
trace! `Meta.isDefEq.checkAssignment.outOfScopeFVar
(Expr.fvar fvarId ++ " @ " ++ Expr.mvar mvarId ++ fvars ++ " := " ++ v);
pure none
| CheckAssignment.Exception.readOnlyMVarWithBiggerLCtx nestedMVarId => do
trace! `Meta.isDefEq.checkAssignment.readOnlyMVarWithBiggerLCtx
(Expr.mvar nestedMVarId ++ " @ " ++ Expr.mvar mvarId ++ fvars ++ " := " ++ v);
pure none
| CheckAssignment.Exception.mvarTypeNotWellFormedInSmallerLCtx nestedMVarId => do
trace! `Meta.isDefEq.checkAssignment.mvarTypeNotWellFormedInSmallerLCtx
(Expr.mvar nestedMVarId ++ " @ " ++ Expr.mvar mvarId ++ fvars ++ " := " ++ v);
pure none
| CheckAssignment.Exception.unknownExprMVar mvarId =>
-- This case can only happen if the MetaM API is being misused
throwEx $ Exception.unknownExprMVar mvarId
/--
Auxiliary function for handling constraints of the form `?m a₁ ... aₙ =?= v`.
It will check whether we can perform the assignment
@ -561,14 +585,8 @@ fun ctx s => if !v.hasExprMVar && !v.hasFVar then EStateM.Result.ok (some v) s e
hasCtxLocals := hasCtxLocals
};
match (CheckAssignment.check v checkCtx).run { mctx := s.mctx, ngen := s.ngen } with
| EStateM.Result.ok e newS =>
EStateM.Result.ok (some e) { mctx := newS.mctx, ngen := newS.ngen, .. s }
| EStateM.Result.error (CheckAssignment.Exception.unknownExprMVar mvarId) newS =>
-- This case can only happen if the MetaM API is being misused
EStateM.Result.error (Exception.unknownExprMVar mvarId { env := s.env, mctx := s.mctx, lctx := ctx.lctx }) { ngen := newS.ngen, .. s }
| EStateM.Result.error ex newS =>
-- TODO: save other exceptions as trace message
EStateM.Result.ok none { ngen := newS.ngen, .. s }
| EStateM.Result.ok e newS => EStateM.Result.ok (some e) { mctx := newS.mctx, ngen := newS.ngen, .. s }
| EStateM.Result.error ex newS => checkAssignmentFailure mvarId fvars v ex ctx { ngen := newS.ngen, .. s }
end Meta
end Lean