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

feat: add trace messages

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-19 17:41:27 -08:00
parent 87e109aeba
commit 2bc6d8568b
2 changed files with 41 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -25,6 +25,7 @@ inductive MessageData
| ofSyntax : Syntax → MessageData
| ofExpr : Expr → MessageData
| ofLevel : Level → MessageData
| ofName : Name → MessageData
/- `context env mctx lctx d` specifies the pretty printing context `(env, mctx, lctx)` for the nested expressions in `d`. -/
| context : Environment → MetavarContext → LocalContext → MessageData → MessageData
/- Lifted `Format.nest` -/
@ -46,6 +47,7 @@ partial def formatAux : Option (Environment × MetavarContext × LocalContext)
| _, ofFormat fmt => fmt
| _, ofSyntax s => s.formatStx
| _, ofLevel u => fmt u
| _, ofName n => fmt n
| none, ofExpr e => "<expr>"
| some (env, mctx, lctx), ofExpr e => "<expr>" -- TODO: invoke pretty printer
| _, context env mctx lctx d => formatAux (some (env, mctx, lctx)) d
@ -62,6 +64,7 @@ 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 coeOfName : HasCoe Name MessageData := ⟨ofName⟩
instance coeOfArrayExpr : HasCoe (Array Expr) MessageData := ⟨fun es => node $ es.map $ fun e => ofExpr e⟩
end MessageData

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

@ -704,49 +704,70 @@ match t.getAppFn, s.getAppFn with
(synthesizePending : Expr → MetaM Bool)
(t s : Expr) : MetaM LBool :=
do let isDefEqL (t s : Expr) : MetaM LBool := toLBoolM $ isDefEq t s;
let isDefEqLeft (fn : Name) (t s : Expr) : MetaM LBool := do {
trace! `Meta.isDefEq.delta.unfoldLeft fn;
toLBoolM $ isDefEq t s
};
let isDefEqRight (fn : Name) (t s : Expr) : MetaM LBool := do {
trace! `Meta.isDefEq.delta.unfoldRight fn;
toLBoolM $ isDefEq t s
};
let isDefEqLeftRight (fn : Name) (t s : Expr) : MetaM LBool := do {
trace! `Meta.isDefEq.delta.unfoldLeftRight fn;
toLBoolM $ isDefEq t s
};
let isListLevelDefEqL (us vs : List Level) : MetaM LBool := toLBoolM $ isListLevelDefEq us vs;
let unfold {α} (e failK successK) : MetaM α := unfoldDefinitionAux whnf (inferTypeAux whnf) isDefEq synthesizePending e failK successK;
let unfold (e failK successK) : MetaM LBool := unfoldDefinitionAux whnf (inferTypeAux whnf) isDefEq synthesizePending e failK successK;
let tryHeuristic : MetaM Bool :=
/- Try to solve `f a₁ ... aₙ =?= f b₁ ... bₙ` by solving `a₁ =?= b₁, ..., aₙ =?= bₙ` -/
let tFn := t.getAppFn;
let sFn := s.getAppFn;
traceCtx `Meta.isDefEq.delta $
try $
isDefEqArgs whnf isDefEq synthesizePending tFn t.getAppArgs s.getAppArgs
<&&>
isListLevelDefEq tFn.constLevels! sFn.constLevels!;
tInfo? ← isDeltaCandidate t.getAppFn;
sInfo? ← isDeltaCandidate s.getAppFn;
match tInfo?, sInfo? with
| none, none => pure LBool.undef
| some _, none => unfold t (pure LBool.undef) $ fun t => isDefEqL t s
| none, some _ => unfold s (pure LBool.undef) $ fun s => isDefEqL t s
| some tInfo, none => unfold t (pure LBool.undef) $ fun t => isDefEqLeft tInfo.name t s
| none, some sInfo => unfold s (pure LBool.undef) $ fun s => isDefEqRight sInfo.name t s
| some tInfo, some sInfo =>
let isDefEqLeft (t s) := isDefEqLeft tInfo.name t s;
let isDefEqRight (t s) := isDefEqRight sInfo.name t s;
let isDefEqLeftRight (t s) := isDefEqLeftRight tInfo.name t s;
if tInfo.name == sInfo.name then
match t, s with
| Expr.const _ ls₁ _, Expr.const _ ls₂ _ => isListLevelDefEqL ls₁ ls₂
| Expr.app _ _ _, Expr.app _ _ _ =>
let tFn := t.getAppFn;
let sFn := s.getAppFn;
condM (try (isDefEqArgs whnf isDefEq synthesizePending tFn t.getAppArgs s.getAppArgs
<&&> isListLevelDefEq tFn.constLevels! sFn.constLevels!))
condM tryHeuristic
(pure LBool.true)
(unfold t
(unfold s (pure LBool.undef) (fun s => isDefEqL t s))
(fun t => unfold s (isDefEqL t s) (fun s => isDefEqL t s)))
(unfold s (pure LBool.undef) (fun s => isDefEqRight t s))
(fun t => unfold s (isDefEqLeft t s) (fun s => isDefEqLeftRight t s)))
| _, _ => pure LBool.false
else
let unfoldComparingHeads : Unit → MetaM LBool := fun _ =>
unfold t
(unfold s
(pure LBool.undef)
(fun s => isDefEqL t s))
(fun s => isDefEqRight t s))
(fun tNew =>
if sameHeadSymbol tNew s then
isDefEqL tNew s
isDefEqLeft tNew s
else
unfold s
(isDefEqL tNew s)
(fun sNew => if sameHeadSymbol t sNew then isDefEqL t sNew else isDefEqL tNew sNew));
(isDefEqLeft tNew s)
(fun sNew => if sameHeadSymbol t sNew then isDefEqRight t sNew else isDefEqLeftRight tNew sNew));
let kernelLikeUnfolding : Unit → MetaM LBool := fun _ =>
if !t.hasExprMVar && !s.hasExprMVar then
/- If `t` and `s` do not contain metavariables,
we simulate strategy used in the kernel. -/
if tInfo.hints.lt sInfo.hints then
unfold t (unfoldComparingHeads ()) $ fun t => isDefEqL t s
unfold t (unfoldComparingHeads ()) $ fun t => isDefEqLeft t s
else if sInfo.hints.lt tInfo.hints then
unfold s (unfoldComparingHeads ()) $ fun s => isDefEqL t s
unfold s (unfoldComparingHeads ()) $ fun s => isDefEqRight t s
else
unfoldComparingHeads ()
else
@ -760,9 +781,9 @@ do let isDefEqL (t s : Expr) : MetaM LBool := toLBoolM $ isDefEq t s;
tReducible ← isReducible tInfo.name;
sReducible ← isReducible sInfo.name;
if tReducible && !sReducible then
unfold t (kernelLikeUnfolding ()) $ fun t => isDefEqL t s
unfold t (kernelLikeUnfolding ()) $ fun t => isDefEqLeft t s
else if !tReducible && sReducible then
unfold s (kernelLikeUnfolding ()) $ fun s => isDefEqL t s
unfold s (kernelLikeUnfolding ()) $ fun s => isDefEqRight t s
else
kernelLikeUnfolding ())