From 24a31ab50ef1f932176c1b512fdff1c3c52cb3bf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 1 Dec 2019 11:48:58 -0800 Subject: [PATCH] feat: improve `Level.instantiate` --- src/Init/Lean/Level.lean | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/src/Init/Lean/Level.lean b/src/Init/Lean/Level.lean index 6c3da4e1f0..edd88224a0 100644 --- a/src/Init/Lean/Level.lean +++ b/src/Init/Lean/Level.lean @@ -198,17 +198,6 @@ match lvl.getLevelOffset with | zero _ => lvl.getOffset | _ => none -def instantiate (s : Name → Option Level) : Level → Level -| u@(zero _) => u -| succ u _ => mkLevelSucc (instantiate u) -| max u₁ u₂ _ => mkLevelMax (instantiate u₁) (instantiate u₂) -| imax u₁ u₂ _ => mkLevelIMax (instantiate u₁) (instantiate u₂) -| u@(param n _) => - match s n with - | some u' => u' - | none => u -| u => u - @[extern "lean_level_eq"] protected constant beq (a : @& Level) (b : @& Level) : Bool := arbitrary _ @@ -429,6 +418,16 @@ match lvl with | max lhs rhs d => updateIMax (imax lhs rhs d) newLhs newRhs rfl | _ => panic! "imax level expected" +@[specialize] def instantiate (s : Name → Option Level) : Level → Level +| u@(zero _) => u +| u@(succ v _) => if u.hasParam then u.updateSucc (instantiate v) rfl else u +| u@(max v₁ v₂ _) => if u.hasParam then u.updateMax (instantiate v₁) (instantiate v₂) rfl else u +| u@(imax v₁ v₂ _) => if u.hasParam then u.updateIMax (instantiate v₁) (instantiate v₂) rfl else u +| u@(param n _) => match s n with + | some u' => u' + | none => u +| u => u + end Level abbrev LevelMap (α : Type) := HashMap Level α