diff --git a/library/Init/Lean/Level.lean b/library/Init/Lean/Level.lean index 8e998b8ff7..5259f00770 100644 --- a/library/Init/Lean/Level.lean +++ b/library/Init/Lean/Level.lean @@ -10,6 +10,9 @@ import Init.Lean.Format import Init.Data.HashMap import Init.Data.PersistentHashMap +def Nat.imax (n m : Nat) : Nat := +if m = 0 then 0 else Nat.max n m + namespace Lean inductive Level @@ -26,69 +29,93 @@ attribute [extern "level_mk_imax"] Level.imax attribute [extern "level_mk_param"] Level.param attribute [extern "level_mk_mvar"] Level.mvar -instance levelIsInhabited : Inhabited Level := -⟨Level.zero⟩ +namespace Level -def Level.one : Level := Level.succ Level.zero +instance : Inhabited Level := ⟨zero⟩ -def Level.hasParam : Level → Bool -| Level.param _ => true -| Level.succ l => Level.hasParam l -| Level.max l₁ l₂ => Level.hasParam l₁ || Level.hasParam l₂ -| Level.imax l₁ l₂ => Level.hasParam l₁ || Level.hasParam l₂ -| _ => false +def isZero : Level → Bool +| zero => true +| _ => false -def Level.hasMVar : Level → Bool -| Level.mvar _ => true -| Level.succ l => Level.hasMVar l -| Level.max l₁ l₂ => Level.hasMVar l₁ || Level.hasMVar l₂ -| Level.imax l₁ l₂ => Level.hasMVar l₁ || Level.hasMVar l₂ -| _ => false +def isSucc : Level → Bool +| succ _ => true +| _ => false -def Level.ofNat : Nat → Level -| 0 => Level.zero -| n+1 => Level.succ (Level.ofNat n) +def isMax : Level → Bool +| max _ _ => true +| _ => false -def Level.addOffsetAux : Nat → Level → Level +def isIMax : Level → Bool +| imax _ _ => true +| _ => false + +def isParam : Level → Bool +| param _ => true +| _ => false + +def isMVar : Level → Bool +| mvar _ => true +| _ => false + +def one : Level := succ zero + +@[extern "lean_level_has_param"] +def hasParam : Level → Bool +| param _ => true +| succ l => hasParam l +| max l₁ l₂ => hasParam l₁ || hasParam l₂ +| imax l₁ l₂ => hasParam l₁ || hasParam l₂ +| _ => false + +@[extern "lean_level_has_mvar"] +def hasMVar : Level → Bool +| mvar _ => true +| succ l => hasMVar l +| max l₁ l₂ => hasMVar l₁ || hasMVar l₂ +| imax l₁ l₂ => hasMVar l₁ || hasMVar l₂ +| _ => false + +def ofNat : Nat → Level +| 0 => zero +| n+1 => succ (ofNat n) + +def addOffsetAux : Nat → Level → Level | 0, l => l -| (n+1), l => Level.addOffsetAux n (Level.succ l) +| (n+1), l => addOffsetAux n (Level.succ l) -def Level.addOffset (l : Level) (n : Nat) : Level := +def addOffset (l : Level) (n : Nat) : Level := l.addOffsetAux n -def Nat.imax (n m : Nat) : Nat := -if m = 0 then 0 else Nat.max n m +def toNat : Level → Option Nat +| zero => some 0 +| succ l => Nat.succ <$> toNat l +| max l₁ l₂ => Nat.max <$> toNat l₁ <*> toNat l₂ +| imax l₁ l₂ => Nat.imax <$> toNat l₁ <*> toNat l₂ +| _ => none -def Level.toNat : Level → Option Nat -| Level.zero => some 0 -| Level.succ l => Nat.succ <$> Level.toNat l -| Level.max l₁ l₂ => Nat.max <$> Level.toNat l₁ <*> Level.toNat l₂ -| Level.imax l₁ l₂ => Nat.imax <$> Level.toNat l₁ <*> Level.toNat l₂ -| _ => none +def toOffset : Level → Level × Nat +| zero => (zero, 0) +| succ l => let (l', k) := toOffset l; (l', k+1) +| l => (l, 0) -def Level.toOffset : Level → Level × Nat -| Level.zero => (Level.zero, 0) -| Level.succ l => let (l', k) := Level.toOffset l; (l', k+1) -| l => (l, 0) - -def Level.instantiate (s : Name → Option Level) : Level → Level -| Level.zero => Level.zero -| Level.succ l => Level.succ (Level.instantiate l) -| Level.max l₁ l₂ => Level.max (Level.instantiate l₁) (Level.instantiate l₂) -| Level.imax l₁ l₂ => Level.imax (Level.instantiate l₁) (Level.instantiate l₂) -| l@(Level.param n) => +def instantiate (s : Name → Option Level) : Level → Level +| zero => zero +| succ l => succ (instantiate l) +| max l₁ l₂ => max (instantiate l₁) (instantiate l₂) +| imax l₁ l₂ => imax (instantiate l₁) (instantiate l₂) +| l@(param n) => match s n with | some l' => l' | none => l -| l => l +| l => l @[extern "lean_level_hash"] -constant Level.hash (n : @& Level) : USize := default USize +protected constant hash (n : @& Level) : USize := default USize -instance Level.hashable : Hashable Level := ⟨Level.hash⟩ +instance hashable : Hashable Level := ⟨Level.hash⟩ @[extern "lean_level_eq"] -constant Level.beq (a : @& Level) (b : @& Level) : Bool := default _ +protected constant beq (a : @& Level) (b : @& Level) : Bool := default _ instance : HasBeq Level := ⟨Level.beq⟩ @@ -96,7 +123,7 @@ instance : HasBeq Level := ⟨Level.beq⟩ Check is currently incomplete. TODO: implement in Lean. -/ @[extern "lean_level_eqv"] -constant Level.isEquiv (a : @& Level) (b : @& Level) : Bool := default _ +constant isEquiv (a : @& Level) (b : @& Level) : Bool := default _ /- Level to Format -/ namespace LevelToFormat @@ -138,21 +165,60 @@ partial def Result.format : Result → Bool → Format | Result.maxNode fs, r => parenIfFalse (Format.group $ "max" ++ formatLst (fun r => Result.format r false) fs) r | Result.imaxNode fs, r => parenIfFalse (Format.group $ "imax" ++ formatLst (fun r => Result.format r false) fs) r -def Level.toResult : Level → Result -| Level.zero => Result.num 0 -| Level.succ l => Result.succ (Level.toResult l) -| Level.max l₁ l₂ => Result.max (Level.toResult l₁) (Level.toResult l₂) -| Level.imax l₁ l₂ => Result.imax (Level.toResult l₁) (Level.toResult l₂) -| Level.param n => Result.leaf (fmt n) -| Level.mvar n => Result.leaf (fmt n) +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 (fmt n) +| mvar n => Result.leaf (fmt n) -def Level.format (l : Level) : Format := -(Level.toResult l).format true - -instance levelHasFormat : HasFormat Level := ⟨Level.format⟩ -instance levelHasToString : HasToString Level := ⟨Format.pretty ∘ Level.format⟩ end LevelToFormat +protected def format (l : Level) : Format := +(LevelToFormat.toResult l).format true + +instance : HasFormat Level := ⟨Level.format⟩ +instance : HasToString Level := ⟨Format.pretty ∘ Level.format⟩ + +/- The update functions here are defined using C code. They will try to avoid + allocating new values using pointer equality. + The hypotheses `(h : e.is... = true)` are used to ensure Lean will not crash + at runtime. + The `update*!` functions are inlined and provide a convenient way of using the + update proofs without providing proofs. + Note that if they are used under a match-expression, the compiler will eliminate + the double-match. -/ + +@[extern "lean_level_update_succ"] +def updateSucc (lvl : Level) (newLvl : Level) (h : lvl.isSucc = true) : Level := +succ newLvl + +@[inline] def updateSucc! (lvl : Level) (newLvl : Level) : Level := +match lvl with +| succ lvl => updateSucc (succ lvl) newLvl rfl +| _ => panic! "succ level expected" + +@[extern "lean_level_update_max"] +def updateMax (lvl : Level) (newLhs : Level) (newRhs : Level) (h : lvl.isMax = true) : Level := +max newLhs newRhs + +@[inline] def updateMax! (lvl : Level) (newLhs : Level) (newRhs : Level) : Level := +match lvl with +| max lhs rhs => updateMax (max lhs rhs) newLhs newRhs rfl +| _ => panic! "max level expected" + +@[extern "lean_level_update_imax"] +def updateIMax (lvl : Level) (newLhs : Level) (newRhs : Level) (h : lvl.isIMax = true) : Level := +imax newLhs newRhs + +@[inline] def updateIMax! (lvl : Level) (newLhs : Level) (newRhs : Level) : Level := +match lvl with +| max lhs rhs => updateIMax (imax lhs rhs) newLhs newRhs rfl +| _ => panic! "imax level expected" + +end Level + abbrev LevelMap (α : Type) := HashMap Level α abbrev PersistentLevelMap (α : Type) := PHashMap Level α diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 1cc6260e01..a0975c7b0e 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -377,7 +377,7 @@ expr mk_app(expr const & f, expr const & a) { extern "C" object * lean_expr_mk_sort(obj_arg l) { object * r = alloc_cnstr(static_cast(expr_kind::Sort), 1, expr_scalar_size(expr_kind::Sort)); cnstr_set(r, 0, l); - set_scalar(r, level::hash(l), false, level_has_mvar(l), false, level_has_param(l)); + set_scalar(r, level::hash(l), false, lean_level_has_mvar(l), false, lean_level_has_param(l)); return r; } diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index c23700a366..8048a19d8c 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -63,7 +63,7 @@ unsigned level_depth(b_obj_arg l) { extern "C" object * lean_level_depth(b_obj_arg l) { return mk_nat_obj(level_depth(l)); } -bool level_has_param(b_obj_arg l) { +extern "C" uint8 lean_level_has_param(b_obj_arg l) { switch (get_level_kind(l)) { case level_kind::Zero: case level_kind::MVar: return false; @@ -77,7 +77,7 @@ bool level_has_param(b_obj_arg l) { lean_unreachable(); // LCOV_EXCL_LINE } -bool level_has_mvar(b_obj_arg l) { +extern "C" uint8 lean_level_has_mvar(b_obj_arg l) { switch (get_level_kind(l)) { case level_kind::Zero: case level_kind::Param: return false; @@ -94,7 +94,7 @@ bool level_has_mvar(b_obj_arg l) { extern "C" object * level_mk_succ(obj_arg l) { object * r = alloc_cnstr(static_cast(level_kind::Succ), 1, g_level_num_scalars); cnstr_set(r, 0, l); - set_level_scalar_fields(r, 1, hash(level::hash(l), 17u), level_depth(l)+1, level_has_param(l), level_has_mvar(l)); + set_level_scalar_fields(r, 1, hash(level::hash(l), 17u), level_depth(l)+1, lean_level_has_param(l), lean_level_has_mvar(l)); return r; } @@ -105,8 +105,8 @@ template object * level_mk_max_imax(obj_arg l1, obj_arg l2) { set_level_scalar_fields(r, 2, hash(level::hash(l1), level::hash(l2)), std::max(level_depth(l1), level_depth(l2)) + 1, - level_has_param(l1) || level_has_param(l2), - level_has_mvar(l1) || level_has_mvar(l2)); + lean_level_has_param(l1) || lean_level_has_param(l2), + lean_level_has_mvar(l1) || lean_level_has_mvar(l2)); return r; } @@ -156,8 +156,8 @@ level mk_univ_mvar(name const & n) { } unsigned get_depth(level const & l) { return level_depth(l.raw()); } -bool has_param(level const & l) { return level_has_param(l.raw()); } -bool has_mvar(level const & l) { return level_has_mvar(l.raw()); } +bool has_param(level const & l) { return lean_level_has_param(l.raw()); } +bool has_mvar(level const & l) { return lean_level_has_mvar(l.raw()); } bool is_explicit(level const & l) { switch (kind(l)) { @@ -320,7 +320,7 @@ bool is_lt(levels const & as, levels const & bs, bool use_hash) { bool levels_has_param(b_obj_arg ls) { while (!is_scalar(ls)) { - if (level_has_param(cnstr_get(ls, 0))) return true; + if (lean_level_has_param(cnstr_get(ls, 0))) return true; ls = cnstr_get(ls, 1); } return false; @@ -328,7 +328,7 @@ bool levels_has_param(b_obj_arg ls) { bool levels_has_mvar(b_obj_arg ls) { while (!is_scalar(ls)) { - if (level_has_mvar(cnstr_get(ls, 0))) return true; + if (lean_level_has_mvar(cnstr_get(ls, 0))) return true; ls = cnstr_get(ls, 1); } return false; @@ -407,6 +407,36 @@ level update_max(level const & l, level const & new_lhs, level const & new_rhs) return mk_imax(new_lhs, new_rhs); } +extern "C" object * lean_level_update_succ(obj_arg l, obj_arg new_arg) { + if (succ_of(TO_REF(level, l)).raw() == new_arg) { + lean_dec(new_arg); + return l; + } else { + lean_dec_ref(l); + return level_mk_succ(new_arg); + } +} + +extern "C" object * lean_level_update_max(obj_arg l, obj_arg new_lhs, obj_arg new_rhs) { + if (max_lhs(TO_REF(level, l)).raw() == new_lhs && max_rhs(TO_REF(level, l)).raw() == new_rhs) { + lean_dec(new_lhs); lean_dec(new_rhs); + return l; + } else { + lean_dec_ref(l); + return level_mk_max(new_lhs, new_rhs); + } +} + +extern "C" object * lean_level_update_imax(obj_arg l, obj_arg new_lhs, obj_arg new_rhs) { + if (imax_lhs(TO_REF(level, l)).raw() == new_lhs && imax_rhs(TO_REF(level, l)).raw() == new_rhs) { + lean_dec(new_lhs); lean_dec(new_rhs); + return l; + } else { + lean_dec_ref(l); + return level_mk_imax(new_lhs, new_rhs); + } +} + level instantiate(level const & l, names const & ps, levels const & ls) { lean_assert(length(ps) == length(ls)); return replace(l, [=](level const & l) { diff --git a/src/kernel/level.h b/src/kernel/level.h index 8ef4fbfa64..3bb391ae04 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -129,10 +129,8 @@ bool is_explicit(level const & l); unsigned to_explicit(level const & l); /** \brief Return true iff \c l contains placeholder (aka meta parameters). */ bool has_mvar(level const & l); -bool level_has_mvar(b_obj_arg l); /** \brief Return true iff \c l contains parameters */ bool has_param(level const & l); -bool level_has_param(b_obj_arg l); /** \brief Return a new level expression based on l == succ(arg), where \c arg is replaced with \c new_arg. @@ -162,6 +160,8 @@ bool levels_has_mvar(object * ls); bool has_mvar(levels const & ls); bool levels_has_param(object * ls); bool has_param(levels const & ls); +extern "C" uint8 lean_level_has_mvar(b_obj_arg l); +extern "C" uint8 lean_level_has_param(b_obj_arg l); /** \brief An arbitrary (monotonic) total order on universe level terms. */ bool is_lt(level const & l1, level const & l2, bool use_hash);