From 87e109aebaa5e7bb6ec243af461bbab0f2749fac Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 19 Nov 2019 17:11:20 -0800 Subject: [PATCH] feat: add `isDefEqDelta` --- library/Init/Lean/Declaration.lean | 13 ++++ library/Init/Lean/Meta/Basic.lean | 4 +- library/Init/Lean/Meta/ExprDefEq.lean | 91 +++++++++++++++++++++++++- library/Init/Lean/Meta/LevelDefEq.lean | 7 +- library/Init/Lean/Meta/WHNF.lean | 2 +- 5 files changed, 111 insertions(+), 6 deletions(-) diff --git a/library/Init/Lean/Declaration.lean b/library/Init/Lean/Declaration.lean index 701b54669e..e702c5993d 100644 --- a/library/Init/Lean/Declaration.lean +++ b/library/Init/Lean/Declaration.lean @@ -36,6 +36,19 @@ inductive ReducibilityHints | «abbrev» : ReducibilityHints | regular : UInt32 → ReducibilityHints +namespace ReducibilityHints + +instance : Inhabited ReducibilityHints := ⟨opaque⟩ + +def lt : ReducibilityHints → ReducibilityHints → Bool +| «abbrev», «abbrev» => false +| «abbrev», _ => true +| regular d₁, regular d₂ => d₁ < d₂ +| regular _, opaque => true +| _, _ => false + +end ReducibilityHints + /-- Base structure for `AxiomVal`, `DefinitionVal`, `TheoremVal`, `InductiveVal`, `ConstructorVal`, `RecursorVal` and `QuotVal`. -/ structure ConstantVal := (name : Name) (lparams : List Name) (type : Expr) diff --git a/library/Init/Lean/Meta/Basic.lean b/library/Init/Lean/Meta/Basic.lean index 78fa117725..e2a3ba1734 100644 --- a/library/Init/Lean/Meta/Basic.lean +++ b/library/Init/Lean/Meta/Basic.lean @@ -152,10 +152,10 @@ do s ← get; modify $ fun s => { ngen := s.ngen.next, .. s }; pure id -@[inline] private def reduceAll? : MetaM Bool := +@[inline] def reduceAll? : MetaM Bool := do ctx ← read; pure $ ctx.config.transparency == TransparencyMode.all -@[inline] private def reduceReducibleOnly? : MetaM Bool := +@[inline] def reduceReducibleOnly? : MetaM Bool := do ctx ← read; pure $ ctx.config.transparency == TransparencyMode.reducible @[inline] def getTransparency : MetaM TransparencyMode := diff --git a/library/Init/Lean/Meta/ExprDefEq.lean b/library/Init/Lean/Meta/ExprDefEq.lean index a409268e16..f67e5dcb03 100644 --- a/library/Init/Lean/Meta/ExprDefEq.lean +++ b/library/Init/Lean/Meta/ExprDefEq.lean @@ -9,6 +9,7 @@ import Init.Lean.Meta.InferType import Init.Lean.Meta.FunInfo import Init.Lean.Meta.LevelDefEq import Init.Lean.Meta.Check +import Init.Lean.Meta.Offset namespace Lean namespace Meta @@ -669,8 +670,8 @@ do arg ← if arg.getAppFn.hasExprMVar then instantiateMVars arg else pure arg; else finalize () - /-- Tries to solve `?m a₁ ... aₙ =?= v` by assigning `?m`. - It assumes `?m` is unassigned. -/ +/-- Tries to solve `?m a₁ ... aₙ =?= v` by assigning `?m`. + It assumes `?m` is unassigned. -/ @[specialize] private def processAssignment (whnf : Expr → MetaM Expr) (isDefEq : Expr → Expr → MetaM Bool) @@ -679,5 +680,91 @@ do arg ← if arg.getAppFn.hasExprMVar then instantiateMVars arg else pure arg; do mvarDecl ← getMVarDecl mvar.mvarId!; processAssignmentAux whnf isDefEq synthesizePending mvar mvarDecl v 0 args +@[specialize] private def unfold {α} + (whnf : Expr → MetaM Expr) + (isDefEq : Expr → Expr → MetaM Bool) + (synthesizePending : Expr → MetaM Bool) + (e : Expr) + (failK : MetaM α) (successK : Expr → MetaM α) : MetaM α := +unfoldDefinitionAux whnf (inferTypeAux whnf) isDefEq synthesizePending e failK successK + +private def isDeltaCandidate (t : Expr) : MetaM (Option ConstantInfo) := +match t.getAppFn with +| Expr.const c _ _ => getConst c +| _ => pure none + +private def sameHeadSymbol (t s : Expr) : Bool := +match t.getAppFn, s.getAppFn with +| Expr.const c₁ _ _, Expr.const c₂ _ _ => true +| _, _ => false + +@[specialize] private def isDefEqDelta + (whnf : Expr → MetaM Expr) + (isDefEq : Expr → Expr → MetaM Bool) + (synthesizePending : Expr → MetaM Bool) + (t s : Expr) : MetaM LBool := +do let isDefEqL (t s : Expr) : MetaM LBool := 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; + 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, some sInfo => + 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!)) + (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))) + | _, _ => pure LBool.false + else + let unfoldComparingHeads : Unit → MetaM LBool := fun _ => + unfold t + (unfold s + (pure LBool.undef) + (fun s => isDefEqL t s)) + (fun tNew => + if sameHeadSymbol tNew s then + isDefEqL tNew s + else + unfold s + (isDefEqL tNew s) + (fun sNew => if sameHeadSymbol t sNew then isDefEqL t sNew else isDefEqL 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 + else if sInfo.hints.lt tInfo.hints then + unfold s (unfoldComparingHeads ()) $ fun s => isDefEqL t s + else + unfoldComparingHeads () + else + unfoldComparingHeads (); + condM reduceReducibleOnly? + (kernelLikeUnfolding ()) + (do + /- TransparencyMode is set to `default` or `all`. + If `t` is reducible and `s` is not ==> reduce `t` + If `s` is reducible and `t` is not ==> reduce `s` -/ + tReducible ← isReducible tInfo.name; + sReducible ← isReducible sInfo.name; + if tReducible && !sReducible then + unfold t (kernelLikeUnfolding ()) $ fun t => isDefEqL t s + else if !tReducible && sReducible then + unfold s (kernelLikeUnfolding ()) $ fun s => isDefEqL t s + else + kernelLikeUnfolding ()) + end Meta end Lean diff --git a/library/Init/Lean/Meta/LevelDefEq.lean b/library/Init/Lean/Meta/LevelDefEq.lean index aeb24b5d93..b6063a56cc 100644 --- a/library/Init/Lean/Meta/LevelDefEq.lean +++ b/library/Init/Lean/Meta/LevelDefEq.lean @@ -145,7 +145,7 @@ modify $ fun s => { env := env, mctx := mctx, postponed := postponed, .. s } Remark: postponed universe level constraints must be solved before returning. Otherwise, we don't know whether `x` really succeeded. -/ -@[inline] def try (x : MetaM Bool) : MetaM Bool := +@[specialize] def try (x : MetaM Bool) : MetaM Bool := do s ← get; let env := s.env; let mctx := s.mctx; @@ -167,5 +167,10 @@ try $ do if !r then pure false else processPostponed false +def isListLevelDefEq : List Level → List Level → MetaM Bool +| [], [] => pure true +| u::us, v::vs => isLevelDefEq u v <&&> isListLevelDefEq us vs +| _, _ => pure false + end Meta end Lean diff --git a/library/Init/Lean/Meta/WHNF.lean b/library/Init/Lean/Meta/WHNF.lean index b1646dc3ee..35ebcf1d83 100644 --- a/library/Init/Lean/Meta/WHNF.lean +++ b/library/Init/Lean/Meta/WHNF.lean @@ -14,7 +14,7 @@ namespace Meta private def isAuxDef? (constName : Name) : MetaM Bool := do env ← getEnv; pure (isAuxRecursor env constName || isNoConfusion env constName) -@[specialize] partial def unfoldDefinitionAux {α} +@[specialize] def unfoldDefinitionAux {α} (whnf : Expr → MetaM Expr) (inferType : Expr → MetaM Expr) (isDefEq : Expr → Expr → MetaM Bool)