From 3176943750e6d6f853644fbe9fc097664aade7ca Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 7 Jul 2022 12:36:02 +0200 Subject: [PATCH] refactor: use computed fields for Level --- src/Lean/Elab/Inductive.lean | 18 +- src/Lean/Elab/MutualDef.lean | 6 +- src/Lean/Elab/Structure.lean | 2 +- src/Lean/Level.lean | 175 +++++++++--------- src/Lean/Meta/AbstractMVars.lean | 12 +- src/Lean/Meta/Basic.lean | 2 +- src/Lean/Meta/Closure.lean | 8 +- src/Lean/Meta/DecLevel.lean | 14 +- src/Lean/Meta/InferType.lean | 4 +- src/Lean/Meta/LevelDefEq.lean | 22 +-- src/Lean/Meta/RecursorInfo.lean | 4 +- src/Lean/Meta/SizeOf.lean | 2 +- src/Lean/Meta/SynthInstance.lean | 8 +- src/Lean/MetavarContext.lean | 42 ++--- .../PrettyPrinter/Delaborator/Builtins.lean | 4 +- src/Lean/Server/Rpc/Deriving.lean | 2 +- src/Lean/Util/CollectLevelParams.lean | 8 +- src/Lean/Util/FindLevelMVar.lean | 12 +- src/Lean/Util/ReplaceLevel.lean | 8 +- src/kernel/level.h | 4 +- tests/lean/run/998Export.lean | 12 +- 21 files changed, 185 insertions(+), 184 deletions(-) diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 4d2792e823..490e7d26c8 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -397,7 +397,7 @@ def shouldInferResultUniverse (u : Level) : TermElabM (Option MVarId) := do let u ← instantiateLevelMVars u if u.hasMVar then match u.getLevelOffset with - | Level.mvar mvarId _ => return some mvarId + | Level.mvar mvarId => return some mvarId | _ => throwError "cannot infer resulting universe level of inductive datatype, given level contains metavariables {mkSort u}, provide universe explicitly" else @@ -447,11 +447,11 @@ def accLevel (u : Level) (r : Level) (rOffset : Nat) : OptionT (StateT (Array Le where go (u : Level) (rOffset : Nat) : OptionT (StateT (Array Level) Id) Unit := do match u, rOffset with - | .max u v _, rOffset => go u rOffset; go v rOffset - | .imax u v _, rOffset => go u rOffset; go v rOffset - | .zero _, _ => return () - | .succ u _, rOffset+1 => go u rOffset - | u, rOffset => + | .max u v, rOffset => go u rOffset; go v rOffset + | .imax u v, rOffset => go u rOffset; go v rOffset + | .zero, _ => return () + | .succ u, rOffset+1 => go u rOffset + | u, rOffset => if rOffset == 0 && u == r then return () else if r.occurs u then @@ -546,8 +546,8 @@ private def checkResultingUniverses (views : Array InductiveView) (numParams : N let v := (← instantiateLevelMVars (← getLevel type)).normalize let rec check (v' : Level) (u' : Level) : TermElabM Unit := match v', u' with - | .succ v' _, .succ u' _ => check v' u' - | .mvar id _, .param .. => + | .succ v', .succ u' => check v' u' + | .mvar id, .param .. => /- Special case: The constructor parameter `v` is at unverse level `?v+k` and the resulting inductive universe level is `u'+k`, where `u'` is a parameter (or zero). @@ -563,7 +563,7 @@ private def checkResultingUniverses (views : Array InductiveView) (numParams : N ----------------------------------------------------------- -/ assignLevelMVar id u' - | .mvar id _, .zero _ => assignLevelMVar id u' -- TODO: merge with previous case + | .mvar id, .zero => assignLevelMVar id u' -- TODO: merge with previous case | _, _ => unless u.geq v do let mut msg := m!"invalid universe level in constructor '{ctor.name}', parameter" diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 834a3b3c9b..d8f152faf3 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -740,9 +740,9 @@ partial def checkForHiddenUnivLevels (allUserLevelNames : List Name) (preDefs : -- Otherwise, we try to produce an error message containing the expression with the offending universe let rec visitLevel (u : Level) : ReaderT Expr TermElabM Unit := do match u with - | .succ u _ => visitLevel u - | .imax u v _ | .max u v _ => visitLevel u; visitLevel v - | .param n _ => + | .succ u => visitLevel u + | .imax u v | .max u v => visitLevel u; visitLevel v + | .param n => unless sTypes.visitedLevel.contains u || allUserLevelNames.contains n do let parent ← withOptions (fun o => pp.universes.set o true) do addMessageContext m!"{indentExpr (← read)}" let body ← withOptions (fun o => pp.letVarTypes.setIfNotSet (pp.funBinderTypes.setIfNotSet o true) true) do addMessageContext m!"{indentExpr preDef.value}" diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 535e20c685..6d9cd8b34c 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -642,7 +642,7 @@ private def updateResultingUniverse (fieldInfos : Array StructFieldInfo) (type : let rOffset : Nat := r.getOffset let r : Level := r.getLevelOffset match r with - | Level.mvar mvarId _ => + | Level.mvar mvarId => let us ← collectUniversesFromFields r rOffset fieldInfos let rNew := mkResultUniverse us rOffset assignLevelMVar mvarId rNew diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean index 0b0d76603a..c5efb8df8e 100644 --- a/src/Lean/Level.lean +++ b/src/Lean/Level.lean @@ -83,24 +83,27 @@ instance : Inhabited (MVarIdMap α) where default := {} inductive Level where - | zero : Data → Level - | succ : Level → Data → Level - | max : Level → Level → Data → Level - | imax : Level → Level → Data → Level - | param : Name → Data → Level - | mvar : MVarId → Data → Level - deriving Inhabited, Repr + | zero : Level + | succ : Level → Level + | max : Level → Level → Level + | imax : Level → Level → Level + | param : Name → Level + | mvar : MVarId → Level +with + @[computedField] data : Level → Data + | .zero => mkData 2221 0 false false + | .mvar mvarId => mkData (mixHash 2237 <| hash mvarId) 0 true false + | .param name => mkData (mixHash 2239 <| hash name) 0 false true + | .succ u => mkData (mixHash 2243 <| u.data.hash) (u.data.depth.toNat + 1) u.data.hasMVar u.data.hasParam + | .max u v => mkData (mixHash 2251 <| mixHash (u.data.hash) (v.data.hash)) (Nat.max u.data.depth.toNat v.data.depth.toNat + 1) + (u.data.hasMVar || v.data.hasMVar) (u.data.hasParam || v.data.hasParam) + | .imax u v => mkData (mixHash 2267 <| mixHash (u.data.hash) (v.data.hash)) (Nat.max u.data.depth.toNat v.data.depth.toNat + 1) + (u.data.hasMVar || v.data.hasMVar) (u.data.hasParam || v.data.hasParam) + +deriving Inhabited, Repr namespace Level -@[inline] def data : Level → Data - | zero d => d - | mvar _ d => d - | param _ d => d - | succ _ d => d - | max _ _ d => d - | imax _ _ d => d - protected def hash (u : Level) : UInt64 := u.data.hash @@ -123,26 +126,22 @@ def hasParam (u : Level) : Bool := end Level def levelZero := - Level.zero <| mkData 2221 0 false false + Level.zero def mkLevelMVar (mvarId : MVarId) := - Level.mvar mvarId <| mkData (mixHash 2237 <| hash mvarId) 0 true false + Level.mvar mvarId def mkLevelParam (name : Name) := - Level.param name <| mkData (mixHash 2239 <| hash name) 0 false true + Level.param name def mkLevelSucc (u : Level) := - Level.succ u <| mkData (mixHash 2243 <| hash u) (u.depth + 1) u.hasMVar u.hasParam + Level.succ u def mkLevelMax (u v : Level) := - Level.max u v <| mkData (mixHash 2251 <| mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1) - (u.hasMVar || v.hasMVar) - (u.hasParam || v.hasParam) + Level.max u v def mkLevelIMax (u v : Level) := - Level.imax u v <| mkData (mixHash 2267 <| mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1) - (u.hasMVar || v.hasMVar) - (u.hasParam || v.hasParam) + Level.imax u v def levelOne := mkLevelSucc levelZero @@ -156,7 +155,7 @@ def levelOne := mkLevelSucc levelZero namespace Level def isZero : Level → Bool - | zero _ => true + | zero => true | _ => false def isSucc : Level → Bool @@ -185,18 +184,18 @@ def isMVar : Level → Bool | _ => false def mvarId! : Level → MVarId - | mvar mvarId _ => mvarId - | _ => panic! "metavariable expected" + | mvar mvarId => mvarId + | _ => panic! "metavariable expected" /-- If result is true, then forall assignments `A` which assigns all parameters and metavariables occuring in `l`, `l[A] != zero` -/ def isNeverZero : Level → Bool - | zero _ => false + | zero => false | param .. => false | mvar .. => false | succ .. => true - | max l₁ l₂ _ => isNeverZero l₁ || isNeverZero l₂ - | imax _ l₂ _ => isNeverZero l₂ + | max l₁ l₂ => isNeverZero l₁ || isNeverZero l₂ + | imax _ l₂ => isNeverZero l₂ def ofNat : Nat → Level | 0 => levelZero @@ -210,24 +209,24 @@ def addOffset (u : Level) (n : Nat) : Level := u.addOffsetAux n def isExplicit : Level → Bool - | zero _ => true - | succ u _ => !u.hasMVar && !u.hasParam && isExplicit u + | zero => true + | succ u => !u.hasMVar && !u.hasParam && isExplicit u | _ => false def getOffsetAux : Level → Nat → Nat - | succ u _, r => getOffsetAux u (r+1) + | succ u , r => getOffsetAux u (r+1) | _, r => r def getOffset (lvl : Level) : Nat := getOffsetAux lvl 0 def getLevelOffset : Level → Level - | succ u _ => getLevelOffset u + | succ u => getLevelOffset u | u => u def toNat (lvl : Level) : Option Nat := match lvl.getLevelOffset with - | zero _ => lvl.getOffset + | zero => lvl.getOffset | _ => none @[extern "lean_level_eq"] @@ -237,9 +236,9 @@ instance : BEq Level := ⟨Level.beq⟩ /-- `occurs u l` return `true` iff `u` occurs in `l`. -/ def occurs : Level → Level → Bool - | u, v@(succ v₁ _) => u == v || occurs u v₁ - | u, v@(max v₁ v₂ _) => u == v || occurs u v₁ || occurs u v₂ - | u, v@(imax v₁ v₂ _) => u == v || occurs u v₁ || occurs u v₂ + | u, v@(succ v₁ ) => u == v || occurs u v₁ + | u, v@(max v₁ v₂ ) => u == v || occurs u v₁ || occurs u v₂ + | u, v@(imax v₁ v₂ ) => u == v || occurs u v₁ || occurs u v₂ | u, v => u == v def ctorToNat : Level → Nat @@ -252,24 +251,24 @@ def ctorToNat : Level → Nat /- TODO: use well founded recursion. -/ partial def normLtAux : Level → Nat → Level → Nat → Bool - | succ l₁ _, k₁, l₂, k₂ => normLtAux l₁ (k₁+1) l₂ k₂ - | l₁, k₁, succ l₂ _, k₂ => normLtAux l₁ k₁ l₂ (k₂+1) - | l₁@(max l₁₁ l₁₂ _), k₁, l₂@(max l₂₁ l₂₂ _), k₂ => + | succ l₁, k₁, l₂, k₂ => normLtAux l₁ (k₁+1) l₂ k₂ + | l₁, k₁, succ l₂, k₂ => normLtAux l₁ k₁ l₂ (k₂+1) + | l₁@(max l₁₁ l₁₂), k₁, l₂@(max l₂₁ l₂₂), k₂ => if l₁ == l₂ then k₁ < k₂ else if l₁₁ != l₂₁ then normLtAux l₁₁ 0 l₂₁ 0 else normLtAux l₁₂ 0 l₂₂ 0 - | l₁@(imax l₁₁ l₁₂ _), k₁, l₂@(imax l₂₁ l₂₂ _), k₂ => + | l₁@(imax l₁₁ l₁₂), k₁, l₂@(imax l₂₁ l₂₂), k₂ => if l₁ == l₂ then k₁ < k₂ else if l₁₁ != l₂₁ then normLtAux l₁₁ 0 l₂₁ 0 else normLtAux l₁₂ 0 l₂₂ 0 - | param n₁ _, k₁, param n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.lt n₁ n₂ -- use `Name.lt` because it is lexicographical + | param n₁, k₁, param n₂, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.lt n₁ n₂ -- use `Name.lt` because it is lexicographical /- We also use `Name.lt` in the following case to make sure universe parameters in a declaration are not affected by shifted indices. We used to use `Name.quickLt` which is not stable over shifted indices (the hashcodes change), and changes to the elaborator could affect the universe parameters and break code that relies on an explicit order. Example: test `tests/lean/343.lean`. -/ - | mvar n₁ _, k₁, mvar n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.lt n₁.name n₂.name + | mvar n₁, k₁, mvar n₂, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.lt n₁.name n₂.name | l₁, k₁, l₂, k₂ => if l₁ == l₂ then k₁ < k₂ else ctorToNat l₁ < ctorToNat l₂ /-- @@ -281,21 +280,21 @@ def normLt (l₁ l₂ : Level) : Bool := normLtAux l₁ 0 l₂ 0 private def isAlreadyNormalizedCheap : Level → Bool - | zero _ => true - | param _ _ => true - | mvar _ _ => true - | succ u _ => isAlreadyNormalizedCheap u - | _ => false + | zero => true + | param _ => true + | mvar _ => true + | succ u => isAlreadyNormalizedCheap u + | _ => false /- Auxiliary function used at `normalize` -/ private def mkIMaxAux : Level → Level → Level - | _, u@(zero _) => u - | zero _, u => u - | u₁, u₂ => if u₁ == u₂ then u₁ else mkLevelIMax u₁ u₂ + | _, zero => zero + | zero, u => u + | u₁, u₂ => if u₁ == u₂ then u₁ else mkLevelIMax u₁ u₂ /- Auxiliary function used at `normalize` -/ @[specialize] private partial def getMaxArgsAux (normalize : Level → Level) : Level → Bool → Array Level → Array Level - | max l₁ l₂ _, alreadyNormalized, lvls => getMaxArgsAux normalize l₂ alreadyNormalized (getMaxArgsAux normalize l₁ alreadyNormalized lvls) + | max l₁ l₂, alreadyNormalized, lvls => getMaxArgsAux normalize l₂ alreadyNormalized (getMaxArgsAux normalize l₁ alreadyNormalized lvls) | l, false, lvls => getMaxArgsAux normalize (normalize l) true lvls | l, true, lvls => lvls.push l @@ -360,7 +359,7 @@ partial def normalize (l : Level) : Level := let k := l.getOffset let u := l.getLevelOffset match u with - | max l₁ l₂ _ => + | max l₁ l₂ => let lvls := getMaxArgsAux normalize l₁ false #[] let lvls := getMaxArgsAux normalize l₂ false lvls let lvls := lvls.qsort normLt @@ -370,7 +369,7 @@ partial def normalize (l : Level) : Level := let prev := lvl₁.getLevelOffset let prevK := lvl₁.getOffset mkMaxAux lvls k (i+1) prev prevK levelZero - | imax l₁ l₂ _ => + | imax l₁ l₂ => if l₂.isNeverZero then addOffset (normalize (mkLevelMax l₁ l₂)) k else let l₁ := normalize l₁ @@ -385,14 +384,14 @@ def isEquiv (u v : Level) : Bool := /-- Reduce (if possible) universe level by 1 -/ def dec : Level → Option Level - | zero _ => none - | param _ _ => none - | mvar _ _ => none - | succ l _ => l - | max l₁ l₂ _ => return mkLevelMax (← dec l₁) (← dec l₂) + | zero => none + | param _ => none + | mvar _ => none + | succ l => l + | max l₁ l₂ => return mkLevelMax (← dec l₁) (← dec l₂) /- Remark: `mkLevelMax` in the following line is not a typo. If `dec l₂` succeeds, then `imax l₁ l₂` is equivalent to `max l₁ l₂`. -/ - | imax l₁ l₂ _ => return mkLevelMax (← dec l₁) (← dec l₂) + | imax l₁ l₂ => return mkLevelMax (← dec l₁) (← dec l₂) /- Level to Format/Syntax -/ @@ -418,12 +417,12 @@ def Result.imax : Result → Result → Result | f₁, f₂ => Result.imaxNode [f₁, f₂] def toResult : Level → Result - | zero _ => Result.num 0 - | succ l _ => Result.succ (toResult l) - | max l₁ l₂ _ => Result.max (toResult l₁) (toResult l₂) - | imax l₁ l₂ _ => Result.imax (toResult l₁) (toResult l₂) - | param n _ => Result.leaf n - | mvar n _ => + | zero => Result.num 0 + | succ l => Result.succ (toResult l) + | max l₁ l₂ => Result.max (toResult l₁) (toResult l₂) + | imax l₁ l₂ => Result.imax (toResult l₁) (toResult l₂) + | param n => Result.leaf n + | mvar n => let n := n.name.replacePrefix `_uniq (Name.mkSimple "?u"); Result.leaf n @@ -481,7 +480,7 @@ end Level let subsumes (u v : Level) : Bool := if v.isExplicit && u.getOffset ≥ v.getOffset then true else match u with - | Level.max u₁ u₂ _ => v == u₁ || v == u₂ + | Level.max u₁ u₂ => v == u₁ || v == u₂ | _ => false if u == v then u else if u.isZero then v @@ -564,11 +563,11 @@ def mkNaryMax : List Level → Level /- Level to Format -/ @[specialize] def instantiateParams (s : Name → Option Level) : Level → Level - | u@(zero _) => u - | u@(succ v _) => if u.hasParam then u.updateSucc! (instantiateParams s v) else u - | u@(max v₁ v₂ _) => if u.hasParam then u.updateMax! (instantiateParams s v₁) (instantiateParams s v₂) else u - | u@(imax v₁ v₂ _) => if u.hasParam then u.updateIMax! (instantiateParams s v₁) (instantiateParams s v₂) else u - | u@(param n _) => match s n with + | u@(zero) => u + | u@(succ v) => if u.hasParam then u.updateSucc! (instantiateParams s v) else u + | u@(max v₁ v₂) => if u.hasParam then u.updateMax! (instantiateParams s v₁) (instantiateParams s v₂) else u + | u@(imax v₁ v₂) => if u.hasParam then u.updateIMax! (instantiateParams s v₁) (instantiateParams s v₂) else u + | u@(param n) => match s n with | some u' => u' | none => u | u => u @@ -579,12 +578,12 @@ where go (u v : Level) : Bool := u == v || match u, v with - | _, zero _ => true - | u, max v₁ v₂ _ => go u v₁ && go u v₂ - | max u₁ u₂ _, v => go u₁ v || go u₂ v - | u, imax v₁ v₂ _ => go u v₁ && go u v₂ - | imax _ u₂ _, v => go u₂ v - | succ u _, succ v _ => go u v + | _, zero => true + | u, max v₁ v₂ => go u v₁ && go u v₂ + | max u₁ u₂, v => go u₁ v || go u₂ v + | u, imax v₁ v₂ => go u v₁ && go u v₂ + | imax _ u₂, v => go u₂ v + | succ u, succ v => go u v | _, _ => let v' := v.getLevelOffset (u.getLevelOffset == v' || v'.isZero) @@ -603,20 +602,20 @@ abbrev PLevelSet := PersistentLevelSet def Level.collectMVars (u : Level) (s : MVarIdSet := {}) : MVarIdSet := match u with - | succ v _ => collectMVars v s - | max u v _ => collectMVars u (collectMVars v s) - | imax u v _ => collectMVars u (collectMVars v s) - | mvar n _ => s.insert n - | _ => s + | succ v => collectMVars v s + | max u v => collectMVars u (collectMVars v s) + | imax u v => collectMVars u (collectMVars v s) + | mvar n => s.insert n + | _ => s def Level.find? (u : Level) (p : Level → Bool) : Option Level := let rec visit (u : Level) : Option Level := if p u then return u else match u with - | succ v _ => visit v - | max u v _ => visit u <|> visit v - | imax u v _ => visit u <|> visit v + | succ v => visit v + | max u v => visit u <|> visit v + | imax u v => visit u <|> visit v | _ => failure visit u diff --git a/src/Lean/Meta/AbstractMVars.lean b/src/Lean/Meta/AbstractMVars.lean index 69421bf8a3..d09ded902e 100644 --- a/src/Lean/Meta/AbstractMVars.lean +++ b/src/Lean/Meta/AbstractMVars.lean @@ -47,12 +47,12 @@ private partial def abstractLevelMVars (u : Level) : M Level := do return u else match u with - | Level.zero _ => return u - | Level.param _ _ => return u - | Level.succ v _ => return u.updateSucc! (← abstractLevelMVars v) - | Level.max v w _ => return u.updateMax! (← abstractLevelMVars v) (← abstractLevelMVars w) - | Level.imax v w _ => return u.updateIMax! (← abstractLevelMVars v) (← abstractLevelMVars w) - | Level.mvar mvarId _ => + | Level.zero => return u + | Level.param _ => return u + | Level.succ v => return u.updateSucc! (← abstractLevelMVars v) + | Level.max v w => return u.updateMax! (← abstractLevelMVars v) (← abstractLevelMVars w) + | Level.imax v w => return u.updateIMax! (← abstractLevelMVars v) (← abstractLevelMVars w) + | Level.mvar mvarId => let s ← get let depth := s.mctx.getLevelDepth mvarId; if depth != s.mctx.depth then diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 43e970fcc9..c693e38a1e 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -1360,7 +1360,7 @@ private def mkLeveErrorMessageCore (header : String) (entry : PostponedEntry) : withLCtx ctx.lctx ctx.localInstances do let s := entry.lhs.collectMVars entry.rhs.collectMVars /- `p u` is true if it contains a universe metavariable in `s` -/ - let p (u : Level) := u.any fun | Level.mvar m _ => s.contains m | _ => false + let p (u : Level) := u.any fun | Level.mvar m => s.contains m | _ => false let lhs := exposeRelevantUniverses (← instantiateMVars ctx.lhs) p let rhs := exposeRelevantUniverses (← instantiateMVars ctx.rhs) p try diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean index ff7667cf9b..fb188a86f5 100644 --- a/src/Lean/Meta/Closure.lean +++ b/src/Lean/Meta/Closure.lean @@ -152,12 +152,12 @@ def mkNewLevelParam (u : Level) : ClosureM Level := do pure $ mkLevelParam p partial def collectLevelAux : Level → ClosureM Level - | u@(Level.succ v _) => return u.updateSucc! (← visitLevel collectLevelAux v) - | u@(Level.max v w _) => return u.updateMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w) - | u@(Level.imax v w _) => return u.updateIMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w) + | u@(Level.succ v) => return u.updateSucc! (← visitLevel collectLevelAux v) + | u@(Level.max v w) => return u.updateMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w) + | u@(Level.imax v w) => return u.updateIMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w) | u@(Level.mvar ..) => mkNewLevelParam u | u@(Level.param ..) => mkNewLevelParam u - | u@(Level.zero _) => pure u + | u@(Level.zero) => pure u def collectLevel (u : Level) : ClosureM Level := do -- u ← instantiateLevelMVars u diff --git a/src/Lean/Meta/DecLevel.lean b/src/Lean/Meta/DecLevel.lean index a3e36db58d..c535289d52 100644 --- a/src/Lean/Meta/DecLevel.lean +++ b/src/Lean/Meta/DecLevel.lean @@ -16,9 +16,9 @@ structure DecLevelContext where canAssignMVars : Bool := true private partial def decAux? : Level → ReaderT DecLevelContext MetaM (Option Level) - | Level.zero _ => return none - | Level.param _ _ => return none - | Level.mvar mvarId _ => do + | Level.zero => return none + | Level.param _ => return none + | Level.mvar mvarId => do match (← getLevelMVarAssignment? mvarId) with | some u => decAux? u | none => @@ -29,7 +29,7 @@ private partial def decAux? : Level → ReaderT DecLevelContext MetaM (Option Le trace[Meta.isLevelDefEq.step] "decAux?, {mkLevelMVar mvarId} := {mkLevelSucc u}" assignLevelMVar mvarId (mkLevelSucc u) return u - | Level.succ u _ => return u + | Level.succ u => return u | u => let processMax (u v : Level) : ReaderT DecLevelContext MetaM (Option Level) := do /- Remark: this code uses the fact that `max (u+1) (v+1) = (max u v)+1`. @@ -45,10 +45,10 @@ private partial def decAux? : Level → ReaderT DecLevelContext MetaM (Option Le | none => return none | some v => return mkLevelMax' u v match u with - | Level.max u v _ => processMax u v + | Level.max u v => processMax u v /- Remark: If `decAux? v` returns `some ...`, then `imax u v` is equivalent to `max u v`. -/ - | Level.imax u v _ => processMax u v - | _ => unreachable! + | Level.imax u v => processMax u v + | _ => unreachable! def decLevel? (u : Level) : MetaM (Option Level) := do let mctx ← getMCtx diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index 8aa6edb5f0..3fd5a54115 100644 --- a/src/Lean/Meta/InferType.lean +++ b/src/Lean/Meta/InferType.lean @@ -206,8 +206,8 @@ private def isAlwaysZero : Level → Bool | .mvar .. => false | .param .. => false | .succ .. => false - | .max u v _ => isAlwaysZero u && isAlwaysZero v - | .imax _ u _ => isAlwaysZero u + | .max u v => isAlwaysZero u && isAlwaysZero v + | .imax _ u => isAlwaysZero u /-- `isArrowProp type n` is an "approximate" predicate which returns `LBool.true` diff --git a/src/Lean/Meta/LevelDefEq.lean b/src/Lean/Meta/LevelDefEq.lean index c0e906a10e..65f7396bc2 100644 --- a/src/Lean/Meta/LevelDefEq.lean +++ b/src/Lean/Meta/LevelDefEq.lean @@ -14,17 +14,17 @@ namespace Lean.Meta Return true iff `lvl` occurs in `max u_1 ... u_n` and `lvl != u_i` for all `i in [1, n]`. That is, `lvl` is a proper level subterm of some `u_i`. -/ private def strictOccursMax (lvl : Level) : Level → Bool - | Level.max u v _ => visit u || visit v + | Level.max u v => visit u || visit v | _ => false where visit : Level → Bool - | Level.max u v _ => visit u || visit v + | Level.max u v => visit u || visit v | u => u != lvl && lvl.occurs u /-- `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 - | l@(Level.mvar id _), acc => if id != mvarId then mkLevelMax' acc l else 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 /-- @@ -43,14 +43,14 @@ private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : MetaM Unit := do private def isMVarWithGreaterDepth (v : Level) (mvarId : MVarId) : MetaM Bool := match v with - | Level.mvar mvarId' _ => return (← getLevelMVarDepth mvarId') > (← getLevelMVarDepth mvarId) + | Level.mvar mvarId' => return (← getLevelMVarDepth mvarId') > (← getLevelMVarDepth mvarId) | _ => return false mutual private partial def solve (u v : Level) : MetaM LBool := do match u, v with - | Level.mvar mvarId _, _ => + | Level.mvar mvarId, _ => if (← isReadOnlyLevelMVar mvarId) then return LBool.undef else if (← getConfig).ignoreLevelMVarDepth && (← isMVarWithGreaterDepth v mvarId) then @@ -67,12 +67,12 @@ mutual else return LBool.undef | _, Level.mvar .. => return LBool.undef -- Let `solve v u` to handle this case - | Level.zero _, Level.max v₁ v₂ _ => + | Level.zero, Level.max v₁ v₂ => Bool.toLBool <$> (isLevelDefEqAux levelZero v₁ <&&> isLevelDefEqAux levelZero v₂) - | Level.zero _, Level.imax _ v₂ _ => + | Level.zero, Level.imax _ v₂ => Bool.toLBool <$> isLevelDefEqAux levelZero v₂ - | Level.zero _, Level.succ .. => return LBool.false - | Level.succ u _, v => + | Level.zero, Level.succ .. => return LBool.false + | Level.succ u, v => if v.isParam then return LBool.false else if u.isMVar && u.occurs v then @@ -85,7 +85,7 @@ mutual @[export lean_is_level_def_eq] partial def isLevelDefEqAuxImpl : Level → Level → MetaM Bool - | Level.succ lhs _, Level.succ rhs _ => isLevelDefEqAux lhs rhs + | Level.succ lhs, Level.succ rhs => isLevelDefEqAux lhs rhs | lhs, rhs => do if lhs.getLevelOffset == rhs.getLevelOffset then return lhs.getOffset == rhs.getOffset diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean index 24da9eff8c..5fa4fd757e 100644 --- a/src/Lean/Meta/RecursorInfo.lean +++ b/src/Lean/Meta/RecursorInfo.lean @@ -160,8 +160,8 @@ private def getIndicesPos (declName : Name) (xs : Array Expr) (majorPos numIndic private def getMotiveLevel (declName : Name) (motiveResultType : Expr) : MetaM Level := match motiveResultType with - | Expr.sort u@(Level.zero _) _ => pure u - | Expr.sort u@(Level.param _ _) _ => pure u + | Expr.sort u@(Level.zero) _ => pure u + | Expr.sort u@(Level.param _) _ => pure u | _ => throwError "invalid user defined recursor '{declName}', motive result sort must be Prop or (Sort u) where u is a universe level parameter" diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean index a9ae724a9b..3cb1d16864 100644 --- a/src/Lean/Meta/SizeOf.lean +++ b/src/Lean/Meta/SizeOf.lean @@ -340,7 +340,7 @@ mutual | none => throwFailed | some (fName, us) => let thmLevelParams ← us.mapM fun - | Level.param n _ => return n + | Level.param n => return n | _ => throwFailed let thmName := fName.appendAfter "_eq" if (← getEnv).contains thmName then diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 5b1ee1b2af..b6a8dc9323 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -98,10 +98,10 @@ partial def normLevel (u : Level) : M Level := do if !u.hasMVar then return u else match u with - | Level.succ v _ => return u.updateSucc! (← normLevel v) - | Level.max v w _ => return u.updateMax! (← normLevel v) (← normLevel w) - | Level.imax v w _ => return u.updateIMax! (← normLevel v) (← normLevel w) - | Level.mvar mvarId _ => + | Level.succ v => return u.updateSucc! (← normLevel v) + | Level.max v w => return u.updateMax! (← normLevel v) (← normLevel w) + | Level.imax v w => return u.updateIMax! (← normLevel v) (← normLevel w) + | Level.mvar mvarId => if !(← isLevelMVarAssignable mvarId) then return u else diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index c30ce08a19..53b52d4c66 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -365,12 +365,12 @@ def isExprMVarAssignable [Monad m] [MonadMCtx m] (mvarId : MVarId) : m Bool := d /-- Return true iff the given level contains an assigned metavariable. -/ def hasAssignedLevelMVar [Monad m] [MonadMCtx m] : Level → m Bool - | Level.succ lvl _ => pure lvl.hasMVar <&&> hasAssignedLevelMVar lvl - | Level.max lvl₁ lvl₂ _ => (pure lvl₁.hasMVar <&&> hasAssignedLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignedLevelMVar lvl₂) - | Level.imax lvl₁ lvl₂ _ => (pure lvl₁.hasMVar <&&> hasAssignedLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignedLevelMVar lvl₂) - | Level.mvar mvarId _ => isLevelMVarAssigned mvarId - | Level.zero _ => pure false - | Level.param _ _ => pure false + | Level.succ lvl => pure lvl.hasMVar <&&> hasAssignedLevelMVar lvl + | Level.max lvl₁ lvl₂ => (pure lvl₁.hasMVar <&&> hasAssignedLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignedLevelMVar lvl₂) + | Level.imax lvl₁ lvl₂ => (pure lvl₁.hasMVar <&&> hasAssignedLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignedLevelMVar lvl₂) + | Level.mvar mvarId => isLevelMVarAssigned mvarId + | Level.zero => pure false + | Level.param _ => pure false /-- Return `true` iff expression contains assigned (level/expr) metavariables or delayed assigned mvars -/ def hasAssignedMVar [Monad m] [MonadMCtx m] : Expr → m Bool @@ -389,12 +389,12 @@ def hasAssignedMVar [Monad m] [MonadMCtx m] : Expr → m Bool /-- Return true iff the given level contains a metavariable that can be assigned. -/ def hasAssignableLevelMVar [Monad m] [MonadMCtx m] : Level → m Bool - | Level.succ lvl _ => pure lvl.hasMVar <&&> hasAssignableLevelMVar lvl - | Level.max lvl₁ lvl₂ _ => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂) - | Level.imax lvl₁ lvl₂ _ => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂) - | Level.mvar mvarId _ => isLevelMVarAssignable mvarId - | Level.zero _ => return false - | Level.param _ _ => return false + | Level.succ lvl => pure lvl.hasMVar <&&> hasAssignableLevelMVar lvl + | Level.max lvl₁ lvl₂ => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂) + | Level.imax lvl₁ lvl₂ => (pure lvl₁.hasMVar <&&> hasAssignableLevelMVar lvl₁) <||> (pure lvl₂.hasMVar <&&> hasAssignableLevelMVar lvl₂) + | Level.mvar mvarId => isLevelMVarAssignable mvarId + | Level.zero => return false + | Level.param _ => return false /-- Return `true` iff expression contains a metavariable that can be assigned. -/ def hasAssignableMVar [Monad m] [MonadMCtx m] : Expr → m Bool @@ -445,10 +445,10 @@ To avoid this term eta-expanded term, we apply beta-reduction when instantiating This operation is performed at `instantiateExprMVars`, `elimMVarDeps`, and `levelMVarToParam`. -/ partial def instantiateLevelMVars [Monad m] [MonadMCtx m] : Level → m Level - | lvl@(Level.succ lvl₁ _) => return Level.updateSucc! lvl (← instantiateLevelMVars lvl₁) - | lvl@(Level.max lvl₁ lvl₂ _) => return Level.updateMax! lvl (← instantiateLevelMVars lvl₁) (← instantiateLevelMVars lvl₂) - | lvl@(Level.imax lvl₁ lvl₂ _) => return Level.updateIMax! lvl (← instantiateLevelMVars lvl₁) (← instantiateLevelMVars lvl₂) - | lvl@(Level.mvar mvarId _) => do + | lvl@(Level.succ lvl₁) => return Level.updateSucc! lvl (← instantiateLevelMVars lvl₁) + | lvl@(Level.max lvl₁ lvl₂) => return Level.updateMax! lvl (← instantiateLevelMVars lvl₁) (← instantiateLevelMVars lvl₂) + | lvl@(Level.imax lvl₁ lvl₂) => return Level.updateIMax! lvl (← instantiateLevelMVars lvl₁) (← instantiateLevelMVars lvl₂) + | lvl@(Level.mvar mvarId) => do match (← getLevelMVarAssignment? mvarId) with | some newLvl => if !newLvl.hasMVar then pure newLvl @@ -1219,12 +1219,12 @@ partial def mkParamName : M Name := do partial def visitLevel (u : Level) : M Level := do match u with - | Level.succ v _ => return u.updateSucc! (← visitLevel v) - | Level.max v₁ v₂ _ => return u.updateMax! (← visitLevel v₁) (← visitLevel v₂) - | Level.imax v₁ v₂ _ => return u.updateIMax! (← visitLevel v₁) (← visitLevel v₂) - | Level.zero _ => return u + | Level.succ v => return u.updateSucc! (← visitLevel v) + | Level.max v₁ v₂ => return u.updateMax! (← visitLevel v₁) (← visitLevel v₂) + | Level.imax v₁ v₂ => return u.updateIMax! (← visitLevel v₁) (← visitLevel v₂) + | Level.zero => return u | Level.param .. => return u - | Level.mvar mvarId _ => + | Level.mvar mvarId => match (← getLevelMVarAssignment? mvarId) with | some v => visitLevel v | none => diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 1e66d7d614..3a07ce20e4 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -52,8 +52,8 @@ def delabMVar : Delab := do def delabSort : Delab := do let Expr.sort l _ ← getExpr | unreachable! match l with - | Level.zero _ => `(Prop) - | Level.succ (Level.zero _) _ => `(Type) + | Level.zero => `(Prop) + | Level.succ .zero => `(Type) | _ => match l.dec with | some l' => `(Type $(Level.quote l' max_prec)) | none => `(Sort $(Level.quote l max_prec)) diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean index 1efe10e094..c106b84d07 100644 --- a/src/Lean/Server/Rpc/Deriving.lean +++ b/src/Lean/Server/Rpc/Deriving.lean @@ -103,7 +103,7 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr let mut fieldTp := fieldTp if isOptField fieldName then if !fieldTp.isAppOf ``Option then - throwError "optional field '{fieldName}' has type{indentD m!"{fieldTp}"}\nbut is expected to have type{indentD "Option _"}" + throwError "optional field '{fieldName}' has type{indentD m!"{fieldTp}"}\nbut is expected to have type{indentD "Option _"}" --" fieldTp := fieldTp.getArg! 0 -- postulate that the field has an encoding and remember the encoding's binder name diff --git a/src/Lean/Util/CollectLevelParams.lean b/src/Lean/Util/CollectLevelParams.lean index 590491592a..95416efbdd 100644 --- a/src/Lean/Util/CollectLevelParams.lean +++ b/src/Lean/Util/CollectLevelParams.lean @@ -24,10 +24,10 @@ mutual else collect u { s with visitedLevel := s.visitedLevel.insert u } partial def collect : Level → Visitor - | Level.succ v _ => visitLevel v - | Level.max u v _ => visitLevel v ∘ visitLevel u - | Level.imax u v _ => visitLevel v ∘ visitLevel u - | Level.param n _ => fun s => { s with params := s.params.push n } + | Level.succ v => visitLevel v + | Level.max u v => visitLevel v ∘ visitLevel u + | Level.imax u v => visitLevel v ∘ visitLevel u + | Level.param n => fun s => { s with params := s.params.push n } | _ => id end diff --git a/src/Lean/Util/FindLevelMVar.lean b/src/Lean/Util/FindLevelMVar.lean index 7d410c9cd1..f1c07488de 100644 --- a/src/Lean/Util/FindLevelMVar.lean +++ b/src/Lean/Util/FindLevelMVar.lean @@ -30,12 +30,12 @@ mutual if s.isSome || !l.hasMVar then s else mainLevel p l s partial def mainLevel (p : MVarId → Bool) : Level → Visitor - | Level.zero _ => id - | Level.succ l _ => visitLevel p l - | Level.max l₁ l₂ _ => visitLevel p l₁ ∘ visitLevel p l₂ - | Level.imax l₁ l₂ _ => visitLevel p l₁ ∘ visitLevel p l₂ - | Level.param _ _ => id - | Level.mvar mvarId _ => fun s => if p mvarId then some mvarId else s + | Level.zero => id + | Level.succ l => visitLevel p l + | Level.max l₁ l₂ => visitLevel p l₁ ∘ visitLevel p l₂ + | Level.imax l₁ l₂ => visitLevel p l₁ ∘ visitLevel p l₂ + | Level.param _ => id + | Level.mvar mvarId => fun s => if p mvarId then some mvarId else s end end FindLevelMVar diff --git a/src/Lean/Util/ReplaceLevel.lean b/src/Lean/Util/ReplaceLevel.lean index ca117e5473..15226c75e0 100644 --- a/src/Lean/Util/ReplaceLevel.lean +++ b/src/Lean/Util/ReplaceLevel.lean @@ -12,10 +12,10 @@ partial def replace (f? : Level → Option Level) (u : Level) : Level := match f? u with | some v => v | none => match u with - | max v₁ v₂ _ => mkLevelMax' (replace f? v₁) (replace f? v₂) - | imax v₁ v₂ _ => mkLevelIMax' (replace f? v₁) (replace f? v₂) - | succ v _ => mkLevelSucc (replace f? v) - | _ => u + | max v₁ v₂ => mkLevelMax' (replace f? v₁) (replace f? v₂) + | imax v₁ v₂ => mkLevelIMax' (replace f? v₁) (replace f? v₂) + | succ v => mkLevelSucc (replace f? v) + | _ => u end Level diff --git a/src/kernel/level.h b/src/kernel/level.h index cedabf02fb..e31402458b 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -45,7 +45,9 @@ public: explicit level(b_obj_arg o, bool b):object_ref(o, b) {} level(level const & other):object_ref(other) {} level(level && other):object_ref(other) {} - level_kind kind() const { return static_cast(lean_ptr_tag(raw())); } + level_kind kind() const { + return lean_is_scalar(raw()) ? level_kind::Zero : static_cast(lean_ptr_tag(raw())); + } unsigned hash() const; level & operator=(level const & other) { object_ref::operator=(other); return *this; } diff --git a/tests/lean/run/998Export.lean b/tests/lean/run/998Export.lean index f3ef2af967..c48d70ffed 100644 --- a/tests/lean/run/998Export.lean +++ b/tests/lean/run/998Export.lean @@ -65,15 +65,15 @@ def exportLevel (L : Level) : ExportM Nat := do match (← get).levels.map.find? L with | some i => pure i | none => match L with - | Level.zero _ => pure 0 - | Level.succ l _ => + | Level.zero => pure 0 + | Level.succ l => let i ← alloc L; IO.println s!"{i} #US {← exportLevel l}"; pure i - | Level.max l₁ l₂ _ => + | Level.max l₁ l₂ => let i ← alloc L; IO.println s!"{i} #UM {← exportLevel l₁} {← exportLevel l₂}"; pure i - | Level.imax l₁ l₂ _ => + | Level.imax l₁ l₂ => let i ← alloc L; IO.println s!"{i} #UIM {← exportLevel l₁} {← exportLevel l₂}"; pure i - | Level.param n _ => + | Level.param n => let i ← alloc L; IO.println s!"{i} #UP {← exportName n}"; pure i - | Level.mvar n _ => unreachable! + | Level.mvar n => unreachable! attribute [simp] exportLevel