From 6a89a811ce1970e63125014f7e8dd922d4e4170c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Jan 2021 07:57:59 -0800 Subject: [PATCH] chore: cleanup --- src/Lean/Meta/LevelDefEq.lean | 173 +++++++++++++++++----------------- 1 file changed, 87 insertions(+), 86 deletions(-) diff --git a/src/Lean/Meta/LevelDefEq.lean b/src/Lean/Meta/LevelDefEq.lean index 454c470489..f40d63ed57 100644 --- a/src/Lean/Meta/LevelDefEq.lean +++ b/src/Lean/Meta/LevelDefEq.lean @@ -9,28 +9,28 @@ import Lean.Meta.InferType namespace Lean.Meta private partial def decAux? : Level → MetaM (Option Level) - | Level.zero _ => pure none - | Level.param _ _ => pure none + | Level.zero _ => return none + | Level.param _ _ => return none | Level.mvar mvarId _ => do let mctx ← getMCtx match mctx.getLevelAssignment? mvarId with | some u => decAux? u | none => if (← isReadOnlyLevelMVar mvarId) then - pure none + return none else let u ← mkFreshLevelMVar assignLevelMVar mvarId (mkLevelSucc u) - pure u - | Level.succ u _ => pure u + return u + | Level.succ u _ => return u | u => let process (u v : Level) : MetaM (Option Level) := do match (← decAux? u) with - | none => pure none + | none => return none | some u => do match (← decAux? v) with - | none => pure none - | some v => pure $ mkLevelMax' u v + | none => return none + | some v => return mkLevelMax' u v match u with | Level.max u v _ => process u v /- Remark: If `decAux? v` returns `some ...`, then `imax u v` is equivalent to `max u v`. -/ @@ -40,22 +40,21 @@ private partial def decAux? : Level → MetaM (Option Level) def decLevel? (u : Level) : MetaM (Option Level) := do let mctx ← getMCtx match (← decAux? u) with - | some v => pure $ some v + | some v => return some v | none => do modify fun s => { s with mctx := mctx } - pure none + return none def decLevel (u : Level) : MetaM Level := do match (← decLevel? u) with - | some u => pure u + | some u => return u | none => throwError! "invalid universe level, {u} is not greater than 0" /- This method is useful for inferring universe level parameters for function that take arguments such as `{α : Type u}`. Recall that `Type u` is `Sort (u+1)` in Lean. Thus, given `α`, we must infer its universe level, and then decrement 1 to obtain `u`. -/ def getDecLevel (type : Expr) : MetaM Level := do - let u ← getLevel type - decLevel u + decLevel (← getLevel type) private def strictOccursMaxAux (lvl : Level) : Level → Bool | Level.max u v _ => strictOccursMaxAux lvl u || strictOccursMaxAux lvl v @@ -70,7 +69,7 @@ private def strictOccursMax (lvl : Level) : Level → Bool /-- `mkMaxArgsDiff mvarId (max u_1 ... (mvar mvarId) ... u_n) v` => `max v u_1 ... u_n` -/ private def mkMaxArgsDiff (mvarId : MVarId) : Level → Level → Level - | Level.max u v _, acc => mkMaxArgsDiff mvarId v $ mkMaxArgsDiff mvarId u acc + | Level.max u v _, acc => mkMaxArgsDiff mvarId v <| mkMaxArgsDiff mvarId u acc | l@(Level.mvar id _), acc => if id != mvarId then mkLevelMax' acc l else acc | l, acc => mkLevelMax' acc l @@ -79,84 +78,86 @@ private def mkMaxArgsDiff (mvarId : MVarId) : Level → Level → Level and assigning `?m := max ?n v` -/ private def solveSelfMax (mvarId : MVarId) (v : Level) : MetaM Unit := do let n ← mkFreshLevelMVar - assignLevelMVar mvarId $ mkMaxArgsDiff mvarId v n + assignLevelMVar mvarId <| mkMaxArgsDiff mvarId v n private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : MetaM Unit := modifyPostponed fun postponed => postponed.push { lhs := lhs, rhs := rhs } mutual -private partial def solve (u v : Level) : MetaM LBool := do - match u, v with - | Level.mvar mvarId _, _ => - if (← isReadOnlyLevelMVar mvarId) then - pure LBool.undef - else if !u.occurs v then - assignLevelMVar u.mvarId! v - pure LBool.true - else if !strictOccursMax u v then - solveSelfMax u.mvarId! v - pure LBool.true - else - pure LBool.undef - | Level.zero _, Level.max v₁ v₂ _ => - Bool.toLBool <$> (isLevelDefEqAux levelZero v₁ <&&> isLevelDefEqAux levelZero v₂) - | Level.zero _, Level.imax _ v₂ _ => - Bool.toLBool <$> isLevelDefEqAux levelZero v₂ - | Level.zero _, Level.succ .. => pure LBool.false - | Level.succ u _, v => - match (← Meta.decLevel? v) with - | some v => Bool.toLBool <$> isLevelDefEqAux u v - | none => pure LBool.undef - | _, _ => pure LBool.undef -partial def isLevelDefEqAux : Level → Level → MetaM Bool - | Level.succ lhs _, Level.succ rhs _ => isLevelDefEqAux lhs rhs - | lhs, rhs => do - if lhs == rhs then - pure true - else - trace[Meta.isLevelDefEq.step]! "{lhs} =?= {rhs}" - let lhs' ← instantiateLevelMVars lhs - let lhs' := lhs'.normalize - let rhs' ← instantiateLevelMVars rhs - let rhs' := rhs'.normalize - if lhs != lhs' || rhs != rhs' then - isLevelDefEqAux lhs' rhs' + private partial def solve (u v : Level) : MetaM LBool := do + match u, v with + | Level.mvar mvarId _, _ => + if (← isReadOnlyLevelMVar mvarId) then + return LBool.undef + else if !u.occurs v then + assignLevelMVar u.mvarId! v + return LBool.true + else if !strictOccursMax u v then + solveSelfMax u.mvarId! v + return LBool.true else - let r ← solve lhs rhs; - if r != LBool.undef then - pure $ r == LBool.true + return LBool.undef + | Level.zero _, Level.max v₁ v₂ _ => + Bool.toLBool <$> (isLevelDefEqAux levelZero v₁ <&&> isLevelDefEqAux levelZero v₂) + | Level.zero _, Level.imax _ v₂ _ => + Bool.toLBool <$> isLevelDefEqAux levelZero v₂ + | Level.zero _, Level.succ .. => return LBool.false + | Level.succ u _, v => + match (← Meta.decLevel? v) with + | some v => Bool.toLBool <$> isLevelDefEqAux u v + | none => return LBool.undef + | _, _ => return LBool.undef + + partial def isLevelDefEqAux : Level → Level → MetaM Bool + | Level.succ lhs _, Level.succ rhs _ => isLevelDefEqAux lhs rhs + | lhs, rhs => do + if lhs == rhs then + return true + else + trace[Meta.isLevelDefEq.step]! "{lhs} =?= {rhs}" + let lhs' ← instantiateLevelMVars lhs + let lhs' := lhs'.normalize + let rhs' ← instantiateLevelMVars rhs + let rhs' := rhs'.normalize + if lhs != lhs' || rhs != rhs' then + isLevelDefEqAux lhs' rhs' else - let r ← solve rhs lhs; + let r ← solve lhs rhs; if r != LBool.undef then - pure $ r == LBool.true - else do - let mctx ← getMCtx - if !mctx.hasAssignableLevelMVar lhs && !mctx.hasAssignableLevelMVar rhs then - let ctx ← read - if ctx.config.isDefEqStuckEx && (lhs.isMVar || rhs.isMVar) then do - trace[Meta.isLevelDefEq.stuck]! "{lhs} =?= {rhs}" - Meta.throwIsDefEqStuck + return r == LBool.true + else + let r ← solve rhs lhs; + if r != LBool.undef then + return r == LBool.true + else do + let mctx ← getMCtx + if !mctx.hasAssignableLevelMVar lhs && !mctx.hasAssignableLevelMVar rhs then + let ctx ← read + if ctx.config.isDefEqStuckEx && (lhs.isMVar || rhs.isMVar) then do + trace[Meta.isLevelDefEq.stuck]! "{lhs} =?= {rhs}" + Meta.throwIsDefEqStuck + else + return false else - pure false - else - postponeIsLevelDefEq lhs rhs; pure true + postponeIsLevelDefEq lhs rhs + return true end def isListLevelDefEqAux : List Level → List Level → MetaM Bool - | [], [] => pure true + | [], [] => return true | u::us, v::vs => isLevelDefEqAux u v <&&> isListLevelDefEqAux us vs - | _, _ => pure false + | _, _ => return false private def getNumPostponed : MetaM Nat := do - pure (← getPostponed).size + return (← getPostponed).size open Std (PersistentArray) private def getResetPostponed : MetaM (PersistentArray PostponedEntry) := do let ps ← getPostponed setPostponed {} - pure ps + return ps private def processPostponedStep : MetaM Bool := traceCtx `Meta.isLevelDefEq.postponed.step do @@ -168,26 +169,26 @@ private def processPostponedStep : MetaM Bool := private partial def processPostponed (mayPostpone : Bool := true) : MetaM Bool := do if (← getNumPostponed) == 0 then - pure true + return true else traceCtx `Meta.isLevelDefEq.postponed do let rec loop : MetaM Bool := do let numPostponed ← getNumPostponed if numPostponed == 0 then - pure true + return true else trace[Meta.isLevelDefEq.postponed]! "processing #{numPostponed} postponed is-def-eq level constraints" if !(← processPostponedStep) then - pure false + return false else let numPostponed' ← getNumPostponed if numPostponed' == 0 then - pure true + return true else if numPostponed' < numPostponed then loop else trace[Meta.isLevelDefEq.postponed]! "no progress solving pending is-def-eq level constraints" - pure mayPostpone + return mayPostpone loop private def restore (env : Environment) (mctx : MetavarContext) (postponed : PersistentArray PostponedEntry) : MetaM Unit := do @@ -208,13 +209,13 @@ private def restore (env : Environment) (mctx : MetavarContext) (postponed : Per try if (← x) then if (← processPostponed mayPostpone) then - pure true + return true else restore env mctx postponed - pure false + return false else restore env mctx postponed - pure false + return false catch ex => restore env mctx postponed throw ex @@ -223,7 +224,7 @@ private def postponedToMessageData (ps : PersistentArray PostponedEntry) : Messa let mut r := MessageData.nil for p in ps do r := m!"{r}\n{p.lhs} =?= {p.rhs}" - pure r + return r @[specialize] def withoutPostponingUniverseConstraintsImp {α} (x : MetaM α) : MetaM α := do let postponed ← getResetPostponed @@ -232,31 +233,31 @@ private def postponedToMessageData (ps : PersistentArray PostponedEntry) : Messa unless (← processPostponed (mayPostpone := false)) do throwError! "stuck at solving universe constraints{MessageData.nestD (postponedToMessageData (← getPostponed))}" setPostponed postponed - pure a + return a catch ex => setPostponed postponed throw ex @[inline] def withoutPostponingUniverseConstraints {α m} [MonadControlT MetaM m] [Monad m] : m α → m α := - mapMetaM $ withoutPostponingUniverseConstraintsImp + mapMetaM <| withoutPostponingUniverseConstraintsImp def isLevelDefEq (u v : Level) : MetaM Bool := traceCtx `Meta.isLevelDefEq do - let b ← commitWhen (mayPostpone := true) $ Meta.isLevelDefEqAux u v + let b ← commitWhen (mayPostpone := true) <| Meta.isLevelDefEqAux u v trace[Meta.isLevelDefEq]! "{u} =?= {v} ... {if b then "success" else "failure"}" - pure b + return b def isExprDefEq (t s : Expr) : MetaM Bool := traceCtx `Meta.isDefEq do - let b ← commitWhen (mayPostpone := true) $ Meta.isExprDefEqAux t s + let b ← commitWhen (mayPostpone := true) <| Meta.isExprDefEqAux t s trace[Meta.isDefEq]! "{t} =?= {s} ... {if b then "success" else "failure"}" - pure b + return b abbrev isDefEq (t s : Expr) : MetaM Bool := isExprDefEq t s def isExprDefEqGuarded (a b : Expr) : MetaM Bool := do - try isExprDefEq a b catch _ => pure false + try isExprDefEq a b catch _ => return false abbrev isDefEqGuarded (t s : Expr) : MetaM Bool := isExprDefEqGuarded t s