chore(library): s/Punit/PUnit/g etc
This commit is contained in:
Sebastian Ullrich
Leonardo de Moura
parent
4b3ca1f679
commit
97e5aa2411
19 changed files with 258 additions and 257 deletions
|
|
@ -19,12 +19,12 @@ def List.mmap {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f :
|
|||
| (h :: t) := do h' ← f h, t' ← List.mmap t, pure (h' :: t')
|
||||
|
||||
@[specialize]
|
||||
def List.mmap' {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m Punit
|
||||
def List.mmap' {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit
|
||||
| [] := pure ⟨⟩
|
||||
| (h :: t) := f h *> List.mmap' t
|
||||
|
||||
@[specialize]
|
||||
def List.mfor {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m Punit :=
|
||||
def List.mfor {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit :=
|
||||
List.mmap' f
|
||||
|
||||
def mjoin {m : Type u → Type u} [Monad m] {α : Type u} (a : m (m α)) : m α :=
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@ prelude
|
|||
import init.control.state init.control.except
|
||||
universes u v
|
||||
|
||||
namespace Estate
|
||||
namespace EState
|
||||
|
||||
inductive Result (ε σ α : Type u)
|
||||
| ok {} : α → σ → Result
|
||||
|
|
@ -44,57 +44,57 @@ protected def Result.repr [HasRepr ε] [HasRepr α] : Result ε σ α → String
|
|||
instance [HasToString ε] [HasToString α] : HasToString (Result ε σ α) := ⟨Result.toString⟩
|
||||
instance [HasRepr ε] [HasRepr α] : HasRepr (Result ε σ α) := ⟨Result.repr⟩
|
||||
|
||||
end Estate
|
||||
end EState
|
||||
|
||||
def Estate (ε σ α : Type u) := Estate.resultOk Punit σ Punit → Estate.Result ε σ α
|
||||
def EState (ε σ α : Type u) := EState.resultOk PUnit σ PUnit → EState.Result ε σ α
|
||||
|
||||
namespace Estate
|
||||
namespace EState
|
||||
|
||||
variables {ε σ α β : Type u}
|
||||
|
||||
instance [Inhabited ε] : Inhabited (Estate ε σ α) :=
|
||||
instance [Inhabited ε] : Inhabited (EState ε σ α) :=
|
||||
⟨λ r, match r with
|
||||
| ⟨Result.ok _ s, _⟩ := Result.error (default ε) s
|
||||
| ⟨Result.error _ _, h⟩ := unreachableError h⟩
|
||||
|
||||
@[inline] protected def pure (a : α) : Estate ε σ α :=
|
||||
@[inline] protected def pure (a : α) : EState ε σ α :=
|
||||
λ r, match r with
|
||||
| ⟨Result.ok _ s, _⟩ := Result.ok a s
|
||||
| ⟨Result.error _ _, h⟩ := unreachableError h
|
||||
|
||||
@[inline] protected def put (s : σ) : Estate ε σ Punit :=
|
||||
@[inline] protected def put (s : σ) : EState ε σ PUnit :=
|
||||
λ r, match r with
|
||||
| ⟨Result.ok _ _, _⟩ := Result.ok ⟨⟩ s
|
||||
| ⟨Result.error _ _, h⟩ := unreachableError h
|
||||
|
||||
@[inline] protected def get : Estate ε σ σ :=
|
||||
@[inline] protected def get : EState ε σ σ :=
|
||||
λ r, match r with
|
||||
| ⟨Result.ok _ s, _⟩ := Result.ok s s
|
||||
| ⟨Result.error _ _, h⟩ := unreachableError h
|
||||
|
||||
@[inline] protected def modify (f : σ → σ) : Estate ε σ Punit :=
|
||||
@[inline] protected def modify (f : σ → σ) : EState ε σ PUnit :=
|
||||
λ r, match r with
|
||||
| ⟨Result.ok _ s, _⟩ := Result.ok ⟨⟩ (f s)
|
||||
| ⟨Result.error _ _, h⟩ := unreachableError h
|
||||
|
||||
@[inline] protected def throw (e : ε) : Estate ε σ α :=
|
||||
@[inline] protected def throw (e : ε) : EState ε σ α :=
|
||||
λ r, match r with
|
||||
| ⟨Result.ok _ s, _⟩ := Result.error e s
|
||||
| ⟨Result.error _ _, h⟩ := unreachableError h
|
||||
|
||||
@[inline] protected def catch (x : Estate ε σ α) (handle : ε → Estate ε σ α) : Estate ε σ α :=
|
||||
@[inline] protected def catch (x : EState ε σ α) (handle : ε → EState ε σ α) : EState ε σ α :=
|
||||
λ r, match x r with
|
||||
| Result.error e s := handle e (resultOk.mk ⟨⟩ s)
|
||||
| ok := ok
|
||||
|
||||
@[inline] protected def orelse (x₁ x₂ : Estate ε σ α) : Estate ε σ α :=
|
||||
@[inline] protected def orelse (x₁ x₂ : EState ε σ α) : EState ε σ α :=
|
||||
λ r, match x₁ r with
|
||||
| Result.error _ s := x₂ (resultOk.mk ⟨⟩ s)
|
||||
| ok := ok
|
||||
|
||||
/-- Alternative orelse operator that allows to select which exception should be used.
|
||||
The default is to use the first exception since the standard `orelse` uses the second. -/
|
||||
@[inline] protected def orelse' (x₁ x₂ : Estate ε σ α) (useFirstEx := true) : Estate ε σ α :=
|
||||
@[inline] protected def orelse' (x₁ x₂ : EState ε σ α) (useFirstEx := true) : EState ε σ α :=
|
||||
λ r, match x₁ r with
|
||||
| Result.error e₁ s₁ :=
|
||||
(match x₂ (resultOk.mk ⟨⟩ s₁) with
|
||||
|
|
@ -102,31 +102,31 @@ instance [Inhabited ε] : Inhabited (Estate ε σ α) :=
|
|||
| ok := ok)
|
||||
| ok := ok
|
||||
|
||||
@[inline] def adaptExcept {ε' : Type u} [HasLift ε ε'] (x : Estate ε σ α) : Estate ε' σ α :=
|
||||
@[inline] def adaptExcept {ε' : Type u} [HasLift ε ε'] (x : EState ε σ α) : EState ε' σ α :=
|
||||
λ r, match x r with
|
||||
| Result.error e s := Result.error (lift e) s
|
||||
| Result.ok a s := Result.ok a s
|
||||
|
||||
@[inline] protected def bind (x : Estate ε σ α) (f : α → Estate ε σ β) : Estate ε σ β :=
|
||||
@[inline] protected def bind (x : EState ε σ α) (f : α → EState ε σ β) : EState ε σ β :=
|
||||
λ r, match x r with
|
||||
| Result.ok a s := f a (resultOk.mk ⟨⟩ s)
|
||||
| Result.error e s := Result.error e s
|
||||
|
||||
@[inline] protected def map (f : α → β) (x : Estate ε σ α) : Estate ε σ β :=
|
||||
@[inline] protected def map (f : α → β) (x : EState ε σ α) : EState ε σ β :=
|
||||
λ r, match x r with
|
||||
| Result.ok a s := Result.ok (f a) s
|
||||
| Result.error e s := Result.error e s
|
||||
|
||||
instance : Monad (Estate ε σ) :=
|
||||
{ bind := @Estate.bind _ _, pure := @Estate.pure _ _, map := @Estate.map _ _ }
|
||||
instance : Monad (EState ε σ) :=
|
||||
{ bind := @EState.bind _ _, pure := @EState.pure _ _, map := @EState.map _ _ }
|
||||
|
||||
instance : HasOrelse (Estate ε σ) :=
|
||||
{ orelse := @Estate.orelse _ _ }
|
||||
instance : HasOrelse (EState ε σ) :=
|
||||
{ orelse := @EState.orelse _ _ }
|
||||
|
||||
instance : MonadState σ (Estate ε σ) :=
|
||||
{ put := @Estate.put _ _, get := @Estate.get _ _, modify := @Estate.modify _ _ }
|
||||
instance : MonadState σ (EState ε σ) :=
|
||||
{ put := @EState.put _ _, get := @EState.get _ _, modify := @EState.modify _ _ }
|
||||
|
||||
instance : MonadExcept ε (Estate ε σ) :=
|
||||
{ throw := @Estate.throw _ _, catch := @Estate.catch _ _}
|
||||
instance : MonadExcept ε (EState ε σ) :=
|
||||
{ throw := @EState.throw _ _, catch := @EState.catch _ _}
|
||||
|
||||
end Estate
|
||||
end EState
|
||||
|
|
|
|||
|
|
@ -52,11 +52,11 @@ section
|
|||
@[inline] protected def get : StateT σ m σ :=
|
||||
λ s, pure (s, s)
|
||||
|
||||
@[inline] protected def put : σ → StateT σ m Punit :=
|
||||
λ s' s, pure (Punit.star, s')
|
||||
@[inline] protected def put : σ → StateT σ m PUnit :=
|
||||
λ s' s, pure (PUnit.star, s')
|
||||
|
||||
@[inline] protected def modify (f : σ → σ) : StateT σ m Punit :=
|
||||
λ s, pure (Punit.star, f s)
|
||||
@[inline] protected def modify (f : σ → σ) : StateT σ m PUnit :=
|
||||
λ s, pure (PUnit.star, f s)
|
||||
|
||||
@[inline] protected def lift {α : Type u} (t : m α) : StateT σ m α :=
|
||||
λ s, do a ← t, pure (a, s)
|
||||
|
|
@ -86,12 +86,12 @@ class MonadState (σ : outParam (Type u)) (m : Type u → Type v) :=
|
|||
/- Obtain the top-most State of a Monad stack. -/
|
||||
(get {} : m σ)
|
||||
/- Set the top-most State of a Monad stack. -/
|
||||
(put {} : σ → m Punit)
|
||||
(put {} : σ → m PUnit)
|
||||
/- Map the top-most State of a Monad stack.
|
||||
|
||||
Note: `modify f` may be preferable to `f <$> get >>= put` because the latter
|
||||
does not use the State linearly (without sufficient inlining). -/
|
||||
(modify {} : (σ → σ) → m Punit)
|
||||
(modify {} : (σ → σ) → m PUnit)
|
||||
|
||||
export MonadState (get put modify)
|
||||
|
||||
|
|
@ -152,7 +152,7 @@ section
|
|||
variables {σ σ' : Type u} {m m' : Type u → Type v}
|
||||
|
||||
def MonadStateAdapter.adaptState' [MonadStateAdapter σ σ' m m'] {α : Type u} (toSigma : σ' → σ) (fromSigma : σ → σ') : m α → m' α :=
|
||||
adaptState (λ st, (toSigma st, Punit.star)) (λ st _, fromSigma st)
|
||||
adaptState (λ st, (toSigma st, PUnit.star)) (λ st _, fromSigma st)
|
||||
export MonadStateAdapter (adaptState')
|
||||
|
||||
instance monadStateAdapterTrans {n n' : Type u → Type v} [MonadFunctor m m' n n'] [MonadStateAdapter σ σ' m m'] : MonadStateAdapter σ σ' n n' :=
|
||||
|
|
|
|||
|
|
@ -127,15 +127,15 @@ a
|
|||
issues when proving equational lemmas. The equation Compiler uses it as a marker. -/
|
||||
@[macroInline] abbrev idRhs (α : Sort u) (a : α) : α := a
|
||||
|
||||
inductive Punit : Sort u
|
||||
| star : Punit
|
||||
inductive PUnit : Sort u
|
||||
| star : PUnit
|
||||
|
||||
/-- An abbreviation for `Punit.{0}`, its most common instantiation.
|
||||
This Type should be preferred over `Punit` where possible to avoid
|
||||
/-- An abbreviation for `PUnit.{0}`, its most common instantiation.
|
||||
This Type should be preferred over `PUnit` where possible to avoid
|
||||
unnecessary universe parameters. -/
|
||||
abbrev Unit : Type := Punit
|
||||
abbrev Unit : Type := PUnit
|
||||
|
||||
@[pattern] abbrev Unit.star : Unit := Punit.star
|
||||
@[pattern] abbrev Unit.star : Unit := PUnit.star
|
||||
|
||||
/- Remark: thunks have an efficient implementation in the runtime. -/
|
||||
structure Thunk (α : Type u) : Type u :=
|
||||
|
|
@ -219,7 +219,7 @@ structure Prod (α : Type u) (β : Type v) :=
|
|||
|
||||
/-- Similar to `Prod`, but α and β can be propositions.
|
||||
We use this Type internally to automatically generate the brecOn recursor. -/
|
||||
structure Pprod (α : Sort u) (β : Sort v) :=
|
||||
structure PProd (α : Sort u) (β : Sort v) :=
|
||||
(fst : α) (snd : β)
|
||||
|
||||
structure And (a b : Prop) : Prop :=
|
||||
|
|
@ -265,9 +265,9 @@ inductive Sum (α : Type u) (β : Type v)
|
|||
| inl {} (val : α) : Sum
|
||||
| inr {} (val : β) : Sum
|
||||
|
||||
inductive Psum (α : Sort u) (β : Sort v)
|
||||
| inl {} (val : α) : Psum
|
||||
| inr {} (val : β) : Psum
|
||||
inductive PSum (α : Sort u) (β : Sort v)
|
||||
| inl {} (val : α) : PSum
|
||||
| inr {} (val : β) : PSum
|
||||
|
||||
inductive Or (a b : Prop) : Prop
|
||||
| inl {} (h : a) : Or
|
||||
|
|
@ -282,7 +282,7 @@ Or.inr hb
|
|||
structure Sigma {α : Type u} (β : α → Type v) :=
|
||||
mk :: (fst : α) (snd : β fst)
|
||||
|
||||
structure Psigma {α : Sort u} (β : α → Sort v) :=
|
||||
structure PSigma {α : Sort u} (β : α → Sort v) :=
|
||||
mk :: (fst : α) (snd : β fst)
|
||||
|
||||
inductive Bool : Type
|
||||
|
|
@ -296,7 +296,7 @@ structure Subtype {α : Sort u} (p : α → Prop) :=
|
|||
inductive Exists {α : Sort u} (p : α → Prop) : Prop
|
||||
| intro (w : α) (h : p w) : Exists
|
||||
|
||||
attribute [ppAnonymousCtor] Sigma Psigma Subtype Pprod And
|
||||
attribute [ppAnonymousCtor] Sigma PSigma Subtype PProd And
|
||||
|
||||
class inductive Decidable (p : Prop)
|
||||
| isFalse (h : ¬p) : Decidable
|
||||
|
|
@ -358,10 +358,10 @@ class HasAppend (α : Type u) := (append : α → α → α)
|
|||
class HasAndthen (α : Type u) (β : Type v) (σ : outParam $ Type w) := (andthen : α → β → σ)
|
||||
class HasUnion (α : Type u) := (union : α → α → α)
|
||||
class HasInter (α : Type u) := (inter : α → α → α)
|
||||
class HasSdiff (α : Type u) := (sdiff : α → α → α)
|
||||
class HasSDiff (α : Type u) := (sdiff : α → α → α)
|
||||
class HasEquiv (α : Sort u) := (equiv : α → α → Prop)
|
||||
class HasSubset (α : Type u) := (subset : α → α → Prop)
|
||||
class HasSsubset (α : Type u) := (ssubset : α → α → Prop)
|
||||
class HasSSubset (α : Type u) := (ssubset : α → α → Prop)
|
||||
/- Type classes HasEmptyc and HasInsert are
|
||||
used to implement polymorphic notation for collections.
|
||||
Example: {a, b, c}. -/
|
||||
|
|
@ -399,8 +399,8 @@ notation `∅` := HasEmptyc.emptyc _
|
|||
infix ∪ := HasUnion.union
|
||||
infix ∩ := HasInter.inter
|
||||
infix ⊆ := HasSubset.subset
|
||||
infix ⊂ := HasSsubset.ssubset
|
||||
infix \ := HasSdiff.sdiff
|
||||
infix ⊂ := HasSSubset.ssubset
|
||||
infix \ := HasSDiff.sdiff
|
||||
infix ≈ := HasEquiv.equiv
|
||||
infixr ^ := HasPow.pow
|
||||
infixr /\ := And
|
||||
|
|
@ -422,7 +422,7 @@ infix ≥ := ge
|
|||
infix > := gt
|
||||
|
||||
@[reducible] def superset {α : Type u} [HasSubset α] (a b : α) : Prop := HasSubset.subset b a
|
||||
@[reducible] def ssuperset {α : Type u} [HasSsubset α] (a b : α) : Prop := HasSsubset.ssubset b a
|
||||
@[reducible] def ssuperset {α : Type u} [HasSSubset α] (a b : α) : Prop := HasSSubset.ssubset b a
|
||||
|
||||
infix ⊇ := superset
|
||||
infix ⊃ := ssuperset
|
||||
|
|
@ -518,12 +518,12 @@ protected def Sum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof
|
|||
instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Sum α β) :=
|
||||
⟨Sum.sizeof⟩
|
||||
|
||||
protected def Psum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (Psum α β) → Nat
|
||||
| (Psum.inl a) := 1 + sizeof a
|
||||
| (Psum.inr b) := 1 + sizeof b
|
||||
protected def PSum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (PSum α β) → Nat
|
||||
| (PSum.inl a) := 1 + sizeof a
|
||||
| (PSum.inr b) := 1 + sizeof b
|
||||
|
||||
instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Psum α β) :=
|
||||
⟨Psum.sizeof⟩
|
||||
instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (PSum α β) :=
|
||||
⟨PSum.sizeof⟩
|
||||
|
||||
protected def Sigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [∀ a, HasSizeof (β a)] : Sigma β → Nat
|
||||
| ⟨a, b⟩ := 1 + sizeof a + sizeof b
|
||||
|
|
@ -531,16 +531,16 @@ protected def Sigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [
|
|||
instance (α : Type u) (β : α → Type v) [HasSizeof α] [∀ a, HasSizeof (β a)] : HasSizeof (Sigma β) :=
|
||||
⟨Sigma.sizeof⟩
|
||||
|
||||
protected def Psigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [∀ a, HasSizeof (β a)] : Psigma β → Nat
|
||||
protected def PSigma.sizeof {α : Type u} {β : α → Type v} [HasSizeof α] [∀ a, HasSizeof (β a)] : PSigma β → Nat
|
||||
| ⟨a, b⟩ := 1 + sizeof a + sizeof b
|
||||
|
||||
instance (α : Type u) (β : α → Type v) [HasSizeof α] [∀ a, HasSizeof (β a)] : HasSizeof (Psigma β) :=
|
||||
⟨Psigma.sizeof⟩
|
||||
instance (α : Type u) (β : α → Type v) [HasSizeof α] [∀ a, HasSizeof (β a)] : HasSizeof (PSigma β) :=
|
||||
⟨PSigma.sizeof⟩
|
||||
|
||||
protected def Punit.sizeof : Punit → Nat
|
||||
protected def PUnit.sizeof : PUnit → Nat
|
||||
| u := 1
|
||||
|
||||
instance : HasSizeof Punit := ⟨Punit.sizeof⟩
|
||||
instance : HasSizeof PUnit := ⟨PUnit.sizeof⟩
|
||||
|
||||
protected def Bool.sizeof : Bool → Nat
|
||||
| b := 1
|
||||
|
|
@ -1420,7 +1420,7 @@ instance : Inhabited True := ⟨trivial⟩
|
|||
|
||||
instance : Inhabited Nat := ⟨0⟩
|
||||
|
||||
instance : Inhabited PointedType := ⟨{type := Punit, val := ⟨⟩}⟩
|
||||
instance : Inhabited PointedType := ⟨{type := PUnit, val := ⟨⟩}⟩
|
||||
|
||||
class inductive nonempty (α : Sort u) : Prop
|
||||
| intro (val : α) : nonempty
|
||||
|
|
@ -1667,7 +1667,7 @@ def {u₁ u₂ v₁ v₂} Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β
|
|||
/- Dependent products -/
|
||||
|
||||
notation `Σ` binders `, ` r:(scoped p, Sigma p) := r
|
||||
notation `Σ'` binders `, ` r:(scoped p, Psigma p) := r
|
||||
notation `Σ'` binders `, ` r:(scoped p, PSigma p) := r
|
||||
|
||||
theorem exOfPsig {α : Type u} {p : α → Prop} : (Σ' x, p x) → ∃ x, p x
|
||||
| ⟨x, hx⟩ := ⟨x, hx⟩
|
||||
|
|
@ -1682,25 +1682,25 @@ end
|
|||
section
|
||||
variables {α : Sort u} {β : α → Sort v}
|
||||
|
||||
protected theorem Psigma.Eq : ∀ {p₁ p₂ : Psigma β} (h₁ : p₁.1 = p₂.1), (Eq.recOn h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
|
||||
protected theorem PSigma.Eq : ∀ {p₁ p₂ : PSigma β} (h₁ : p₁.1 = p₂.1), (Eq.recOn h₁ p₁.2 : β p₂.1) = p₂.2 → p₁ = p₂
|
||||
| ⟨a, b⟩ ⟨.(a), .(b)⟩ rfl rfl := rfl
|
||||
end
|
||||
|
||||
/- Universe polymorphic unit -/
|
||||
|
||||
theorem punitEq (a b : Punit) : a = b :=
|
||||
Punit.recOn a (Punit.recOn b rfl)
|
||||
theorem punitEq (a b : PUnit) : a = b :=
|
||||
PUnit.recOn a (PUnit.recOn b rfl)
|
||||
|
||||
theorem punitEqPunit (a : Punit) : a = () :=
|
||||
theorem punitEqPUnit (a : PUnit) : a = () :=
|
||||
punitEq a ()
|
||||
|
||||
instance : subsingleton Punit :=
|
||||
instance : subsingleton PUnit :=
|
||||
subsingleton.intro punitEq
|
||||
|
||||
instance : Inhabited Punit :=
|
||||
instance : Inhabited PUnit :=
|
||||
⟨()⟩
|
||||
|
||||
instance : DecidableEq Punit :=
|
||||
instance : DecidableEq PUnit :=
|
||||
{decEq := λ a b, isTrue (punitEq a b)}
|
||||
|
||||
/- Setoid -/
|
||||
|
|
@ -1800,13 +1800,13 @@ variable {β : Quot r → Sort v}
|
|||
local notation `⟦`:max a `⟧` := Quot.mk r a
|
||||
|
||||
@[reducible, macroInline]
|
||||
protected def indep (f : Π a, β ⟦a⟧) (a : α) : Psigma β :=
|
||||
protected def indep (f : Π a, β ⟦a⟧) (a : α) : PSigma β :=
|
||||
⟨⟦a⟧, f a⟩
|
||||
|
||||
protected theorem indepCoherent (f : Π a, β ⟦a⟧)
|
||||
(h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦b⟧) = f b)
|
||||
: ∀ a b, r a b → Quot.indep f a = Quot.indep f b :=
|
||||
λ a b e, Psigma.Eq (sound e) (h a b e)
|
||||
λ a b e, PSigma.Eq (sound e) (h a b e)
|
||||
|
||||
protected theorem liftIndepPr1
|
||||
(f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (Eq.rec (f a) (sound p) : β ⟦b⟧) = f b)
|
||||
|
|
|
|||
|
|
@ -11,62 +11,62 @@ universes u v w w'
|
|||
inductive Rbcolor
|
||||
| red | black
|
||||
|
||||
inductive Rbnode (α : Type u) (β : α → Type v)
|
||||
| leaf {} : Rbnode
|
||||
| Node (color : Rbcolor) (lchild : Rbnode) (key : α) (val : β key) (rchild : Rbnode) : Rbnode
|
||||
inductive RBNode (α : Type u) (β : α → Type v)
|
||||
| leaf {} : RBNode
|
||||
| Node (color : Rbcolor) (lchild : RBNode) (key : α) (val : β key) (rchild : RBNode) : RBNode
|
||||
|
||||
namespace Rbnode
|
||||
namespace RBNode
|
||||
variables {α : Type u} {β : α → Type v} {σ : Type w}
|
||||
|
||||
open Rbcolor Nat
|
||||
|
||||
def depth (f : Nat → Nat → Nat) : Rbnode α β → Nat
|
||||
def depth (f : Nat → Nat → Nat) : RBNode α β → Nat
|
||||
| leaf := 0
|
||||
| (Node _ l _ _ r) := succ (f (depth l) (depth r))
|
||||
|
||||
protected def min : Rbnode α β → Option (Σ k : α, β k)
|
||||
protected def min : RBNode α β → Option (Σ k : α, β k)
|
||||
| leaf := none
|
||||
| (Node _ leaf k v _) := some ⟨k, v⟩
|
||||
| (Node _ l k v _) := min l
|
||||
|
||||
protected def max : Rbnode α β → Option (Σ k : α, β k)
|
||||
protected def max : RBNode α β → Option (Σ k : α, β k)
|
||||
| leaf := none
|
||||
| (Node _ _ k v leaf) := some ⟨k, v⟩
|
||||
| (Node _ _ k v r) := max r
|
||||
|
||||
@[specialize] def fold (f : Π (k : α), β k → σ → σ) : Rbnode α β → σ → σ
|
||||
@[specialize] def fold (f : Π (k : α), β k → σ → σ) : RBNode α β → σ → σ
|
||||
| leaf b := b
|
||||
| (Node _ l k v r) b := fold r (f k v (fold l b))
|
||||
|
||||
@[specialize] def mfold {m : Type w → Type w'} [Monad m] (f : Π (k : α), β k → σ → m σ) : Rbnode α β → σ → m σ
|
||||
@[specialize] def mfold {m : Type w → Type w'} [Monad m] (f : Π (k : α), β k → σ → m σ) : RBNode α β → σ → m σ
|
||||
| leaf b := pure b
|
||||
| (Node _ l k v r) b := do b₁ ← mfold l b, b₂ ← f k v b₁, mfold r b₂
|
||||
|
||||
@[specialize] def revFold (f : Π (k : α), β k → σ → σ) : Rbnode α β → σ → σ
|
||||
@[specialize] def revFold (f : Π (k : α), β k → σ → σ) : RBNode α β → σ → σ
|
||||
| leaf b := b
|
||||
| (Node _ l k v r) b := revFold l (f k v (revFold r b))
|
||||
|
||||
@[specialize] def all (p : Π k : α, β k → Bool) : Rbnode α β → Bool
|
||||
@[specialize] def all (p : Π k : α, β k → Bool) : RBNode α β → Bool
|
||||
| leaf := true
|
||||
| (Node _ l k v r) := p k v && all l && all r
|
||||
|
||||
@[specialize] def any (p : Π k : α, β k → Bool) : Rbnode α β → Bool
|
||||
@[specialize] def any (p : Π k : α, β k → Bool) : RBNode α β → Bool
|
||||
| leaf := false
|
||||
| (Node _ l k v r) := p k v || any l || any r
|
||||
|
||||
def balance1 : Rbnode α β → Rbnode α β → Rbnode α β
|
||||
def balance1 : RBNode α β → RBNode α β → RBNode α β
|
||||
| (Node _ _ kv vv t) (Node _ (Node red l kx vx r₁) ky vy r₂) := Node red (Node black l kx vx r₁) ky vy (Node black r₂ kv vv t)
|
||||
| (Node _ _ kv vv t) (Node _ l₁ ky vy (Node red l₂ kx vx r)) := Node red (Node black l₁ ky vy l₂) kx vx (Node black r kv vv t)
|
||||
| (Node _ _ kv vv t) (Node _ l ky vy r) := Node black (Node red l ky vy r) kv vv t
|
||||
| _ _ := leaf -- unreachable
|
||||
|
||||
def balance2 : Rbnode α β → Rbnode α β → Rbnode α β
|
||||
def balance2 : RBNode α β → RBNode α β → RBNode α β
|
||||
| (Node _ t kv vv _) (Node _ (Node red l kx₁ vx₁ r₁) ky vy r₂) := Node red (Node black t kv vv l) kx₁ vx₁ (Node black r₁ ky vy r₂)
|
||||
| (Node _ t kv vv _) (Node _ l₁ ky vy (Node red l₂ kx₂ vx₂ r₂)) := Node red (Node black t kv vv l₁) ky vy (Node black l₂ kx₂ vx₂ r₂)
|
||||
| (Node _ t kv vv _) (Node _ l ky vy r) := Node black t kv vv (Node red l ky vy r)
|
||||
| _ _ := leaf -- unreachable
|
||||
|
||||
def isRed : Rbnode α β → Bool
|
||||
def isRed : RBNode α β → Bool
|
||||
| (Node red _ _ _ _) := true
|
||||
| _ := false
|
||||
|
||||
|
|
@ -74,7 +74,7 @@ section insert
|
|||
|
||||
variables (lt : α → α → Prop) [DecidableRel lt]
|
||||
|
||||
def ins : Rbnode α β → Π k : α, β k → Rbnode α β
|
||||
def ins : RBNode α β → Π k : α, β k → RBNode α β
|
||||
| leaf kx vx := Node red leaf kx vx leaf
|
||||
| (Node red a ky vy b) kx vx :=
|
||||
(match cmpUsing lt kx ky with
|
||||
|
|
@ -91,11 +91,11 @@ def ins : Rbnode α β → Π k : α, β k → Rbnode α β
|
|||
if isRed b then balance2 (Node black a ky vy leaf) (ins b kx vx)
|
||||
else Node black a ky vy (ins b kx vx)
|
||||
|
||||
def setBlack : Rbnode α β → Rbnode α β
|
||||
def setBlack : RBNode α β → RBNode α β
|
||||
| (Node _ l k v r) := Node black l k v r
|
||||
| e := e
|
||||
|
||||
def insert (t : Rbnode α β) (k : α) (v : β k) : Rbnode α β :=
|
||||
def insert (t : RBNode α β) (k : α) (v : β k) : RBNode α β :=
|
||||
if isRed t then setBlack (ins lt t k v)
|
||||
else ins lt t k v
|
||||
|
||||
|
|
@ -106,7 +106,7 @@ variable (lt : α → α → Prop)
|
|||
|
||||
variable [DecidableRel lt]
|
||||
|
||||
def findCore : Rbnode α β → Π k : α, Option (Σ k : α, β k)
|
||||
def findCore : RBNode α β → Π k : α, Option (Σ k : α, β k)
|
||||
| leaf x := none
|
||||
| (Node _ a ky vy b) x :=
|
||||
(match cmpUsing lt x ky with
|
||||
|
|
@ -114,7 +114,7 @@ def findCore : Rbnode α β → Π k : α, Option (Σ k : α, β k)
|
|||
| Ordering.Eq := some ⟨ky, vy⟩
|
||||
| Ordering.gt := findCore b x)
|
||||
|
||||
def find {β : Type v} : Rbnode α (λ _, β) → α → Option β
|
||||
def find {β : Type v} : RBNode α (λ _, β) → α → Option β
|
||||
| leaf x := none
|
||||
| (Node _ a ky vy b) x :=
|
||||
(match cmpUsing lt x ky with
|
||||
|
|
@ -122,7 +122,7 @@ def find {β : Type v} : Rbnode α (λ _, β) → α → Option β
|
|||
| Ordering.Eq := some vy
|
||||
| Ordering.gt := find b x)
|
||||
|
||||
def lowerBound : Rbnode α β → α → Option (Sigma β) → Option (Sigma β)
|
||||
def lowerBound : RBNode α β → α → Option (Sigma β) → Option (Sigma β)
|
||||
| leaf x lb := lb
|
||||
| (Node _ a ky vy b) x lb :=
|
||||
(match cmpUsing lt x ky with
|
||||
|
|
@ -132,95 +132,95 @@ def lowerBound : Rbnode α β → α → Option (Sigma β) → Option (Sigma β)
|
|||
|
||||
end membership
|
||||
|
||||
inductive WellFormed (lt : α → α → Prop) : Rbnode α β → Prop
|
||||
inductive WellFormed (lt : α → α → Prop) : RBNode α β → Prop
|
||||
| leafWff : WellFormed leaf
|
||||
| insertWff {n n' : Rbnode α β} {k : α} {v : β k} [DecidableRel lt] : WellFormed n → n' = insert lt n k v → WellFormed n'
|
||||
| insertWff {n n' : RBNode α β} {k : α} {v : β k} [DecidableRel lt] : WellFormed n → n' = insert lt n k v → WellFormed n'
|
||||
|
||||
end Rbnode
|
||||
end RBNode
|
||||
|
||||
open Rbnode
|
||||
open RBNode
|
||||
|
||||
/- TODO(Leo): define dRbmap -/
|
||||
/- TODO(Leo): define dRBMap -/
|
||||
|
||||
def Rbmap (α : Type u) (β : Type v) (lt : α → α → Prop) : Type (max u v) :=
|
||||
{t : Rbnode α (λ _, β) // t.WellFormed lt }
|
||||
def RBMap (α : Type u) (β : Type v) (lt : α → α → Prop) : Type (max u v) :=
|
||||
{t : RBNode α (λ _, β) // t.WellFormed lt }
|
||||
|
||||
@[inline] def mkRbmap (α : Type u) (β : Type v) (lt : α → α → Prop) : Rbmap α β lt :=
|
||||
@[inline] def mkRBMap (α : Type u) (β : Type v) (lt : α → α → Prop) : RBMap α β lt :=
|
||||
⟨leaf, WellFormed.leafWff lt⟩
|
||||
|
||||
namespace Rbmap
|
||||
namespace RBMap
|
||||
variables {α : Type u} {β : Type v} {σ : Type w} {lt : α → α → Prop}
|
||||
|
||||
def depth (f : Nat → Nat → Nat) (t : Rbmap α β lt) : Nat :=
|
||||
def depth (f : Nat → Nat → Nat) (t : RBMap α β lt) : Nat :=
|
||||
t.val.depth f
|
||||
|
||||
@[inline] def fold (f : α → β → σ → σ) : Rbmap α β lt → σ → σ
|
||||
@[inline] def fold (f : α → β → σ → σ) : RBMap α β lt → σ → σ
|
||||
| ⟨t, _⟩ b := t.fold f b
|
||||
|
||||
@[inline] def revFold (f : α → β → σ → σ) : Rbmap α β lt → σ → σ
|
||||
@[inline] def revFold (f : α → β → σ → σ) : RBMap α β lt → σ → σ
|
||||
| ⟨t, _⟩ b := t.revFold f b
|
||||
|
||||
@[inline] def mfold {m : Type w → Type w'} [Monad m] (f : α → β → σ → m σ) : Rbmap α β lt → σ → m σ
|
||||
@[inline] def mfold {m : Type w → Type w'} [Monad m] (f : α → β → σ → m σ) : RBMap α β lt → σ → m σ
|
||||
| ⟨t, _⟩ b := t.mfold f b
|
||||
|
||||
@[inline] def mfor {m : Type w → Type w'} [Monad m] (f : α → β → m σ) (t : Rbmap α β lt) : m Punit :=
|
||||
@[inline] def mfor {m : Type w → Type w'} [Monad m] (f : α → β → m σ) (t : RBMap α β lt) : m PUnit :=
|
||||
t.mfold (λ k v _, f k v *> pure ⟨⟩) ⟨⟩
|
||||
|
||||
@[inline] def Empty : Rbmap α β lt → Bool
|
||||
@[inline] def Empty : RBMap α β lt → Bool
|
||||
| ⟨leaf, _⟩ := true
|
||||
| _ := false
|
||||
|
||||
@[specialize] def toList : Rbmap α β lt → List (α × β)
|
||||
@[specialize] def toList : RBMap α β lt → List (α × β)
|
||||
| ⟨t, _⟩ := t.revFold (λ k v ps, (k, v)::ps) []
|
||||
|
||||
@[inline] protected def min : Rbmap α β lt → Option (α × β)
|
||||
@[inline] protected def min : RBMap α β lt → Option (α × β)
|
||||
| ⟨t, _⟩ :=
|
||||
match t.min with
|
||||
| some ⟨k, v⟩ := some (k, v)
|
||||
| none := none
|
||||
|
||||
@[inline] protected def max : Rbmap α β lt → Option (α × β)
|
||||
@[inline] protected def max : RBMap α β lt → Option (α × β)
|
||||
| ⟨t, _⟩ :=
|
||||
match t.max with
|
||||
| some ⟨k, v⟩ := some (k, v)
|
||||
| none := none
|
||||
|
||||
instance [HasRepr α] [HasRepr β] : HasRepr (Rbmap α β lt) :=
|
||||
instance [HasRepr α] [HasRepr β] : HasRepr (RBMap α β lt) :=
|
||||
⟨λ t, "rbmapOf " ++ repr t.toList⟩
|
||||
|
||||
variables [DecidableRel lt]
|
||||
|
||||
def insert : Rbmap α β lt → α → β → Rbmap α β lt
|
||||
def insert : RBMap α β lt → α → β → RBMap α β lt
|
||||
| ⟨t, w⟩ k v := ⟨t.insert lt k v, WellFormed.insertWff w rfl⟩
|
||||
|
||||
@[specialize] def ofList : List (α × β) → Rbmap α β lt
|
||||
| [] := mkRbmap _ _ _
|
||||
@[specialize] def ofList : List (α × β) → RBMap α β lt
|
||||
| [] := mkRBMap _ _ _
|
||||
| (⟨k,v⟩::xs) := (ofList xs).insert k v
|
||||
|
||||
def findCore : Rbmap α β lt → α → Option (Σ k : α, β)
|
||||
def findCore : RBMap α β lt → α → Option (Σ k : α, β)
|
||||
| ⟨t, _⟩ x := t.findCore lt x
|
||||
|
||||
def find : Rbmap α β lt → α → Option β
|
||||
def find : RBMap α β lt → α → Option β
|
||||
| ⟨t, _⟩ x := t.find lt x
|
||||
|
||||
/-- (lowerBound k) retrieves the kv pair of the largest key smaller than or equal to `k`,
|
||||
if it exists. -/
|
||||
def lowerBound : Rbmap α β lt → α → Option (Σ k : α, β)
|
||||
def lowerBound : RBMap α β lt → α → Option (Σ k : α, β)
|
||||
| ⟨t, _⟩ x := t.lowerBound lt x none
|
||||
|
||||
@[inline] def contains (t : Rbmap α β lt) (a : α) : Bool :=
|
||||
@[inline] def contains (t : RBMap α β lt) (a : α) : Bool :=
|
||||
(t.find a).isSome
|
||||
|
||||
def fromList (l : List (α × β)) (lt : α → α → Prop) [DecidableRel lt] : Rbmap α β lt :=
|
||||
l.foldl (λ r p, r.insert p.1 p.2) (mkRbmap α β lt)
|
||||
def fromList (l : List (α × β)) (lt : α → α → Prop) [DecidableRel lt] : RBMap α β lt :=
|
||||
l.foldl (λ r p, r.insert p.1 p.2) (mkRBMap α β lt)
|
||||
|
||||
@[inline] def all : Rbmap α β lt → (α → β → Bool) → Bool
|
||||
@[inline] def all : RBMap α β lt → (α → β → Bool) → Bool
|
||||
| ⟨t, _⟩ p := t.all p
|
||||
|
||||
@[inline] def any : Rbmap α β lt → (α → β → Bool) → Bool
|
||||
@[inline] def any : RBMap α β lt → (α → β → Bool) → Bool
|
||||
| ⟨t, _⟩ p := t.any p
|
||||
|
||||
end Rbmap
|
||||
end RBMap
|
||||
|
||||
def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (lt : α → α → Prop) [DecidableRel lt] : Rbmap α β lt :=
|
||||
Rbmap.fromList l lt
|
||||
def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (lt : α → α → Prop) [DecidableRel lt] : RBMap α β lt :=
|
||||
RBMap.fromList l lt
|
||||
|
|
|
|||
|
|
@ -7,82 +7,82 @@ prelude
|
|||
import init.data.rbmap.basic
|
||||
universes u v w
|
||||
|
||||
def Rbtree (α : Type u) (lt : α → α → Prop) : Type u :=
|
||||
Rbmap α Unit lt
|
||||
def RBTree (α : Type u) (lt : α → α → Prop) : Type u :=
|
||||
RBMap α Unit lt
|
||||
|
||||
@[inline] def mkRbtree (α : Type u) (lt : α → α → Prop) : Rbtree α lt :=
|
||||
mkRbmap α Unit lt
|
||||
@[inline] def mkRBTree (α : Type u) (lt : α → α → Prop) : RBTree α lt :=
|
||||
mkRBMap α Unit lt
|
||||
|
||||
namespace Rbtree
|
||||
namespace RBTree
|
||||
variables {α : Type u} {β : Type v} {lt : α → α → Prop}
|
||||
|
||||
@[inline] def depth (f : Nat → Nat → Nat) (t : Rbtree α lt) : Nat :=
|
||||
Rbmap.depth f t
|
||||
@[inline] def depth (f : Nat → Nat → Nat) (t : RBTree α lt) : Nat :=
|
||||
RBMap.depth f t
|
||||
|
||||
@[inline] def fold (f : α → β → β) (t : Rbtree α lt) (b : β) : β :=
|
||||
Rbmap.fold (λ a _ r, f a r) t b
|
||||
@[inline] def fold (f : α → β → β) (t : RBTree α lt) (b : β) : β :=
|
||||
RBMap.fold (λ a _ r, f a r) t b
|
||||
|
||||
@[inline] def revFold (f : α → β → β) (t : Rbtree α lt) (b : β) : β :=
|
||||
Rbmap.revFold (λ a _ r, f a r) t b
|
||||
@[inline] def revFold (f : α → β → β) (t : RBTree α lt) (b : β) : β :=
|
||||
RBMap.revFold (λ a _ r, f a r) t b
|
||||
|
||||
@[inline] def mfold {m : Type v → Type w} [Monad m] (f : α → β → m β) (t : Rbtree α lt) (b : β) : m β :=
|
||||
Rbmap.mfold (λ a _ r, f a r) t b
|
||||
@[inline] def mfold {m : Type v → Type w} [Monad m] (f : α → β → m β) (t : RBTree α lt) (b : β) : m β :=
|
||||
RBMap.mfold (λ a _ r, f a r) t b
|
||||
|
||||
@[inline] def mfor {m : Type v → Type w} [Monad m] (f : α → m β) (t : Rbtree α lt) : m Punit :=
|
||||
@[inline] def mfor {m : Type v → Type w} [Monad m] (f : α → m β) (t : RBTree α lt) : m PUnit :=
|
||||
t.mfold (λ a _, f a *> pure ⟨⟩) ⟨⟩
|
||||
|
||||
@[inline] def Empty (t : Rbtree α lt) : Bool :=
|
||||
Rbmap.Empty t
|
||||
@[inline] def Empty (t : RBTree α lt) : Bool :=
|
||||
RBMap.Empty t
|
||||
|
||||
@[specialize] def toList (t : Rbtree α lt) : List α :=
|
||||
@[specialize] def toList (t : RBTree α lt) : List α :=
|
||||
t.revFold (::) []
|
||||
|
||||
@[inline] protected def min (t : Rbtree α lt) : Option α :=
|
||||
match Rbmap.min t with
|
||||
@[inline] protected def min (t : RBTree α lt) : Option α :=
|
||||
match RBMap.min t with
|
||||
| some ⟨a, _⟩ := some a
|
||||
| none := none
|
||||
|
||||
@[inline] protected def max (t : Rbtree α lt) : Option α :=
|
||||
match Rbmap.max t with
|
||||
@[inline] protected def max (t : RBTree α lt) : Option α :=
|
||||
match RBMap.max t with
|
||||
| some ⟨a, _⟩ := some a
|
||||
| none := none
|
||||
|
||||
instance [HasRepr α] : HasRepr (Rbtree α lt) :=
|
||||
instance [HasRepr α] : HasRepr (RBTree α lt) :=
|
||||
⟨λ t, "rbtreeOf " ++ repr t.toList⟩
|
||||
|
||||
variables [DecidableRel lt]
|
||||
|
||||
@[inline] def insert (t : Rbtree α lt) (a : α) : Rbtree α lt :=
|
||||
Rbmap.insert t a ()
|
||||
@[inline] def insert (t : RBTree α lt) (a : α) : RBTree α lt :=
|
||||
RBMap.insert t a ()
|
||||
|
||||
@[specialize] def ofList : List α → Rbtree α lt
|
||||
| [] := mkRbtree _ _
|
||||
@[specialize] def ofList : List α → RBTree α lt
|
||||
| [] := mkRBTree _ _
|
||||
| (x::xs) := (ofList xs).insert x
|
||||
|
||||
def find (t : Rbtree α lt) (a : α) : Option α :=
|
||||
match Rbmap.findCore t a with
|
||||
def find (t : RBTree α lt) (a : α) : Option α :=
|
||||
match RBMap.findCore t a with
|
||||
| some ⟨a, _⟩ := some a
|
||||
| none := none
|
||||
|
||||
@[inline] def contains (t : Rbtree α lt) (a : α) : Bool :=
|
||||
@[inline] def contains (t : RBTree α lt) (a : α) : Bool :=
|
||||
(t.find a).isSome
|
||||
|
||||
def fromList (l : List α) (lt : α → α → Prop) [DecidableRel lt] : Rbtree α lt :=
|
||||
l.foldl insert (mkRbtree α lt)
|
||||
def fromList (l : List α) (lt : α → α → Prop) [DecidableRel lt] : RBTree α lt :=
|
||||
l.foldl insert (mkRBTree α lt)
|
||||
|
||||
@[inline] def all (t : Rbtree α lt) (p : α → Bool) : Bool :=
|
||||
Rbmap.all t (λ a _, p a)
|
||||
@[inline] def all (t : RBTree α lt) (p : α → Bool) : Bool :=
|
||||
RBMap.all t (λ a _, p a)
|
||||
|
||||
@[inline] def any (t : Rbtree α lt) (p : α → Bool) : Bool :=
|
||||
Rbmap.any t (λ a _, p a)
|
||||
@[inline] def any (t : RBTree α lt) (p : α → Bool) : Bool :=
|
||||
RBMap.any t (λ a _, p a)
|
||||
|
||||
def subset (t₁ t₂ : Rbtree α lt) : Bool :=
|
||||
def subset (t₁ t₂ : RBTree α lt) : Bool :=
|
||||
t₁.all $ λ a, (t₂.find a).toBool
|
||||
|
||||
def seteq (t₁ t₂ : Rbtree α lt) : Bool :=
|
||||
def seteq (t₁ t₂ : RBTree α lt) : Bool :=
|
||||
subset t₁ t₂ && subset t₂ t₁
|
||||
|
||||
end Rbtree
|
||||
end RBTree
|
||||
|
||||
def rbtreeOf {α : Type u} (l : List α) (lt : α → α → Prop) [DecidableRel lt] : Rbtree α lt :=
|
||||
Rbtree.fromList l lt
|
||||
def rbtreeOf {α : Type u} (l : List α) (lt : α → α → Prop) [DecidableRel lt] : RBTree α lt :=
|
||||
RBTree.fromList l lt
|
||||
|
|
|
|||
|
|
@ -18,10 +18,10 @@ constant IO.RealWorld : Type := Unit
|
|||
```
|
||||
-/
|
||||
@[derive Monad MonadExcept]
|
||||
def EIO (ε : Type) : Type → Type := Estate ε IO.RealWorld
|
||||
def EIO (ε : Type) : Type → Type := EState ε IO.RealWorld
|
||||
|
||||
instance {ε : Type} {α : Type} [Inhabited ε] : Inhabited (EIO ε α) :=
|
||||
inferInstanceAs (Inhabited (Estate ε IO.RealWorld α))
|
||||
inferInstanceAs (Inhabited (EState ε IO.RealWorld α))
|
||||
|
||||
/-
|
||||
In the future, we may want to give more concrete data
|
||||
|
|
|
|||
|
|
@ -57,26 +57,26 @@ open Expander
|
|||
local attribute [instance] Name.hasLtQuick
|
||||
|
||||
-- TODO(Sebastian): move
|
||||
/-- An Rbmap that remembers the insertion order. -/
|
||||
structure OrderedRbmap (α β : Type) (lt : α → α → Prop) :=
|
||||
/-- An RBMap that remembers the insertion order. -/
|
||||
structure OrderedRBMap (α β : Type) (lt : α → α → Prop) :=
|
||||
(entries : List (α × β))
|
||||
(map : Rbmap α (Nat × β) lt)
|
||||
(map : RBMap α (Nat × β) lt)
|
||||
(size : Nat)
|
||||
|
||||
namespace OrderedRbmap
|
||||
variables {α β : Type} {lt : α → α → Prop} [DecidableRel lt] (m : OrderedRbmap α β lt)
|
||||
namespace OrderedRBMap
|
||||
variables {α β : Type} {lt : α → α → Prop} [DecidableRel lt] (m : OrderedRBMap α β lt)
|
||||
|
||||
def Empty : OrderedRbmap α β lt := {entries := [], map := mkRbmap _ _ _, size := 0}
|
||||
def Empty : OrderedRBMap α β lt := {entries := [], map := mkRBMap _ _ _, size := 0}
|
||||
|
||||
def insert (k : α) (v : β) : OrderedRbmap α β lt :=
|
||||
def insert (k : α) (v : β) : OrderedRBMap α β lt :=
|
||||
{entries := (k, v)::m.entries, map := m.map.insert k (m.size, v), size := m.size + 1}
|
||||
|
||||
def find (a : α) : Option (Nat × β) :=
|
||||
m.map.find a
|
||||
|
||||
def ofList (l : List (α × β)) : OrderedRbmap α β lt :=
|
||||
l.foldl (λ m p, OrderedRbmap.insert m (Prod.fst p) (Prod.snd p)) OrderedRbmap.Empty
|
||||
end OrderedRbmap
|
||||
def ofList (l : List (α × β)) : OrderedRBMap α β lt :=
|
||||
l.foldl (λ m p, OrderedRBMap.insert m (Prod.fst p) (Prod.snd p)) OrderedRBMap.Empty
|
||||
end OrderedRBMap
|
||||
|
||||
structure ElaboratorConfig extends FrontendConfig :=
|
||||
(initialParserCfg : ModuleParserConfig)
|
||||
|
|
@ -93,11 +93,11 @@ structure Scope :=
|
|||
(notations : List NotationMacro := [])
|
||||
/- The set of local universe variables.
|
||||
We remember their insertion order so that we can keep the order when copying them to declarations. -/
|
||||
(univs : OrderedRbmap Name Level (<) := OrderedRbmap.Empty)
|
||||
(univs : OrderedRBMap Name Level (<) := OrderedRBMap.Empty)
|
||||
/- The set of local variables. -/
|
||||
(vars : OrderedRbmap Name SectionVar (<) := OrderedRbmap.Empty)
|
||||
(vars : OrderedRBMap Name SectionVar (<) := OrderedRBMap.Empty)
|
||||
/- The subset of `vars` that is tagged as always included. -/
|
||||
(includeVars : Rbtree Name (<) := mkRbtree _ _)
|
||||
(includeVars : RBTree Name (<) := mkRBTree _ _)
|
||||
/- The stack of nested active `namespace` commands. -/
|
||||
(nsStack : List Name := [])
|
||||
/- The set of active `open` declarations. -/
|
||||
|
|
@ -364,9 +364,9 @@ do cfg ← read,
|
|||
..st},
|
||||
match st' with
|
||||
| some st' := do modifyCurrentScope $ λ sc, {sc with
|
||||
univs := OrderedRbmap.ofList st'.univs,
|
||||
vars := OrderedRbmap.ofList st'.vars,
|
||||
includeVars := Rbtree.ofList st'.includeVars,
|
||||
univs := OrderedRBMap.ofList st'.univs,
|
||||
vars := OrderedRBMap.ofList st'.vars,
|
||||
includeVars := RBTree.ofList st'.includeVars,
|
||||
Options := st'.Options,
|
||||
},
|
||||
modify $ λ st, {..st', ..st}
|
||||
|
|
@ -423,7 +423,7 @@ match dl with
|
|||
match dl.oldUnivParams with
|
||||
| some uparams :=
|
||||
modifyCurrentScope $ λ sc, {sc with univs :=
|
||||
(uparams.ids.map mangleIdent).foldl (λ m id, OrderedRbmap.insert m id (Level.Param id)) sc.univs}
|
||||
(uparams.ids.map mangleIdent).foldl (λ m id, OrderedRBMap.insert m id (Level.Param id)) sc.univs}
|
||||
| none := pure (),
|
||||
-- do we actually need this??
|
||||
let uparams := namesToPexpr $ match dl.oldUnivParams with
|
||||
|
|
@ -500,7 +500,7 @@ def Declaration.elaborate : Elaborator :=
|
|||
match ind.oldUnivParams with
|
||||
| some uparams :=
|
||||
modifyCurrentScope $ λ sc, {sc with univs :=
|
||||
(uparams.ids.map mangleIdent).foldl (λ m id, OrderedRbmap.insert m id (Level.Param id)) sc.univs}
|
||||
(uparams.ids.map mangleIdent).foldl (λ m id, OrderedRBMap.insert m id (Level.Param id)) sc.univs}
|
||||
| none := pure (),
|
||||
let uparams := namesToPexpr $ match ind.oldUnivParams with
|
||||
| some uparams := uparams.ids.map mangleIdent
|
||||
|
|
@ -531,7 +531,7 @@ def Declaration.elaborate : Elaborator :=
|
|||
match s.oldUnivParams with
|
||||
| some uparams :=
|
||||
modifyCurrentScope $ λ sc, {sc with univs :=
|
||||
(uparams.ids.map mangleIdent).foldl (λ m id, OrderedRbmap.insert m id (Level.Param id)) sc.univs}
|
||||
(uparams.ids.map mangleIdent).foldl (λ m id, OrderedRBMap.insert m id (Level.Param id)) sc.univs}
|
||||
| none := pure (),
|
||||
let uparams := namesToPexpr $ match s.oldUnivParams with
|
||||
| some uparams := uparams.ids.map mangleIdent
|
||||
|
|
@ -600,7 +600,7 @@ def include.elaborate : Elaborator :=
|
|||
modifyCurrentScope $ λ sc, {sc with includeVars :=
|
||||
v.ids.foldl (λ vars v, vars.insert $ mangleIdent v) sc.includeVars}
|
||||
|
||||
-- TODO: Rbmap.remove
|
||||
-- TODO: RBMap.remove
|
||||
/-
|
||||
def omit.elaborate : Elaborator :=
|
||||
λ stx, do
|
||||
|
|
@ -893,7 +893,7 @@ def eoi.elaborate : Elaborator :=
|
|||
error cmd "invalid end of input, expected 'end'"
|
||||
|
||||
-- TODO(Sebastian): replace with attribute
|
||||
def elaborators : Rbmap Name Elaborator (<) := Rbmap.fromList [
|
||||
def elaborators : RBMap Name Elaborator (<) := RBMap.fromList [
|
||||
(Module.header.name, Module.header.elaborate),
|
||||
(notation.name, notation.elaborate),
|
||||
(reserveNotation.name, reserveNotation.elaborate),
|
||||
|
|
|
|||
|
|
@ -471,7 +471,7 @@ def sorry.transform : transformer :=
|
|||
local attribute [instance] Name.hasLtQuick
|
||||
|
||||
-- TODO(Sebastian): replace with attribute
|
||||
def builtinTransformers : Rbmap Name transformer (<) := Rbmap.fromList [
|
||||
def builtinTransformers : RBMap Name transformer (<) := RBMap.fromList [
|
||||
(mixfix.name, mixfix.transform),
|
||||
(reserveMixfix.name, reserveMixfix.transform),
|
||||
(bracketedBinders.name, bracketedBinders.transform),
|
||||
|
|
@ -497,7 +497,7 @@ structure ExpanderState :=
|
|||
(nextScope : MacroScope)
|
||||
|
||||
structure ExpanderConfig extends TransformerConfig :=
|
||||
(transformers : Rbmap Name transformer (<))
|
||||
(transformers : RBMap Name transformer (<))
|
||||
|
||||
instance ExpanderConfig.HasLift : HasLift ExpanderConfig TransformerConfig :=
|
||||
⟨ExpanderConfig.toTransformerConfig⟩
|
||||
|
|
|
|||
|
|
@ -22,8 +22,8 @@ def DataValue.beq : DataValue → DataValue → Bool
|
|||
|
||||
instance DataValue.HasBeq : HasBeq DataValue := ⟨DataValue.beq⟩
|
||||
|
||||
/- Remark: we do not use Rbmap here because we need to manipulate Kvmap objects in
|
||||
C++ and Rbmap is implemented in Lean. So, we use just a List until we can
|
||||
/- Remark: we do not use RBMap here because we need to manipulate Kvmap objects in
|
||||
C++ and RBMap is implemented in Lean. So, we use just a List until we can
|
||||
generate C++ code from Lean code. -/
|
||||
structure Kvmap :=
|
||||
(entries : List (Name × DataValue) := [])
|
||||
|
|
|
|||
|
|
@ -157,27 +157,27 @@ end Name
|
|||
|
||||
section
|
||||
local attribute [instance] Name.hasLtQuick
|
||||
def NameMap (α : Type) := Rbmap Name α (<)
|
||||
def NameMap (α : Type) := RBMap Name α (<)
|
||||
variable {α : Type}
|
||||
@[inline] def mkNameMap : NameMap α :=
|
||||
mkRbmap Name α (<)
|
||||
mkRBMap Name α (<)
|
||||
def NameMap.insert (m : NameMap α) (n : Name) (a : α) :=
|
||||
Rbmap.insert m n a
|
||||
RBMap.insert m n a
|
||||
def NameMap.contains (m : NameMap α) (n : Name) : Bool :=
|
||||
Rbmap.contains m n
|
||||
RBMap.contains m n
|
||||
@[inline] def NameMap.find (m : NameMap α) (n : Name) : Option α :=
|
||||
Rbmap.find m n
|
||||
RBMap.find m n
|
||||
end
|
||||
|
||||
section
|
||||
local attribute [instance] Name.hasLtQuick
|
||||
def NameSet := Rbtree Name (<)
|
||||
def NameSet := RBTree Name (<)
|
||||
@[inline] def mkNameSet : NameSet :=
|
||||
mkRbtree Name (<)
|
||||
mkRBTree Name (<)
|
||||
def NameSet.insert (s : NameSet) (n : Name) :=
|
||||
Rbtree.insert s n
|
||||
RBTree.insert s n
|
||||
def NameSet.contains (s : NameSet) (n : Name) : Bool :=
|
||||
Rbmap.contains s n
|
||||
RBMap.contains s n
|
||||
end
|
||||
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -84,7 +84,7 @@ local attribute [reducible] BasicParserM ParserT parserCoreT
|
|||
@[inline] def getCache : BasicParserM ParserCache :=
|
||||
monadLift (get : StateT ParserCache id _)
|
||||
|
||||
@[inline] def putCache : ParserCache → BasicParserM Punit :=
|
||||
@[inline] def putCache : ParserCache → BasicParserM PUnit :=
|
||||
λ c, monadLift (put c : StateT ParserCache id _)
|
||||
end
|
||||
|
||||
|
|
@ -192,7 +192,7 @@ instance trailingTermParserCoe : HasCoe termParser trailingTermParser :=
|
|||
|
||||
local attribute [instance] Name.hasLtQuick
|
||||
/-- A multimap indexed by tokens. Used for indexing parsers by their leading token. -/
|
||||
def TokenMap (α : Type) := Rbmap Name (List α) (<)
|
||||
def TokenMap (α : Type) := RBMap Name (List α) (<)
|
||||
|
||||
def TokenMap.insert {α : Type} (map : TokenMap α) (k : Name) (v : α) : TokenMap α :=
|
||||
match map.find k with
|
||||
|
|
@ -200,7 +200,7 @@ match map.find k with
|
|||
| some vs := map.insert k (v::vs)
|
||||
|
||||
def TokenMap.ofList {α : Type} : List (Name × α) → TokenMap α
|
||||
| [] := mkRbmap _ _ _
|
||||
| [] := mkRBMap _ _ _
|
||||
| (⟨k,v⟩::xs) := (TokenMap.ofList xs).insert k v
|
||||
|
||||
instance tokenMapNil.tokens : Parser.HasTokens $ @TokenMap.ofList ρ [] :=
|
||||
|
|
@ -215,8 +215,8 @@ structure CommandParserConfig extends ParserConfig :=
|
|||
(leadingTermParsers : TokenMap termParser)
|
||||
(trailingTermParsers : TokenMap trailingTermParser)
|
||||
-- local Term parsers (such as from `local notation`) hide previous parsers instead of overloading them
|
||||
(localLeadingTermParsers : TokenMap termParser := mkRbmap _ _ _)
|
||||
(localTrailingTermParsers : TokenMap trailingTermParser := mkRbmap _ _ _)
|
||||
(localLeadingTermParsers : TokenMap termParser := mkRBMap _ _ _)
|
||||
(localTrailingTermParsers : TokenMap trailingTermParser := mkRBMap _ _ _)
|
||||
|
||||
instance commandParserConfigCoeParserConfig : HasCoe CommandParserConfig ParserConfig :=
|
||||
⟨CommandParserConfig.toParserConfig⟩
|
||||
|
|
|
|||
|
|
@ -13,19 +13,19 @@ namespace Lean
|
|||
namespace Parser
|
||||
|
||||
inductive Trie (α : Type)
|
||||
| Node : Option α → Rbnode Char (λ _, Trie) → Trie
|
||||
| Node : Option α → RBNode Char (λ _, Trie) → Trie
|
||||
|
||||
namespace Trie
|
||||
variables {α : Type}
|
||||
|
||||
protected def mk : Trie α :=
|
||||
⟨none, Rbnode.leaf⟩
|
||||
⟨none, RBNode.leaf⟩
|
||||
|
||||
private def insertAux (val : α) : Nat → Trie α → String.Iterator → Trie α
|
||||
| 0 (Trie.Node _ map) _ := Trie.Node (some val) map -- NOTE: overrides old value
|
||||
| (n+1) (Trie.Node val map) it :=
|
||||
let t' := (Rbnode.find (<) map it.curr).getOrElse Trie.mk in
|
||||
Trie.Node val (Rbnode.insert (<) map it.curr (insertAux n t' it.next))
|
||||
let t' := (RBNode.find (<) map it.curr).getOrElse Trie.mk in
|
||||
Trie.Node val (RBNode.insert (<) map it.curr (insertAux n t' it.next))
|
||||
|
||||
def insert (t : Trie α) (s : String) (val : α) : Trie α :=
|
||||
insertAux val s.length t s.mkIterator
|
||||
|
|
@ -33,7 +33,7 @@ insertAux val s.length t s.mkIterator
|
|||
private def findAux : Nat → Trie α → String.Iterator → Option α
|
||||
| 0 (Trie.Node val _) _ := val
|
||||
| (n+1) (Trie.Node val map) it := do
|
||||
t' ← Rbnode.find (<) map it.curr,
|
||||
t' ← RBNode.find (<) map it.curr,
|
||||
findAux n t' it.next
|
||||
|
||||
def find (t : Trie α) (s : String) : Option α :=
|
||||
|
|
@ -43,7 +43,7 @@ private def matchPrefixAux : Nat → Trie α → String.Iterator → Option (Str
|
|||
| 0 (Trie.Node val map) it Acc := Prod.mk it <$> val <|> Acc
|
||||
| (n+1) (Trie.Node val map) it Acc :=
|
||||
let Acc' := Prod.mk it <$> val <|> Acc in
|
||||
match Rbnode.find (<) map it.curr with
|
||||
match RBNode.find (<) map it.curr with
|
||||
| some t := matchPrefixAux n t it.next Acc'
|
||||
| none := Acc'
|
||||
|
||||
|
|
@ -51,7 +51,7 @@ def matchPrefix {α : Type} (t : Trie α) (it : String.Iterator) : Option (Strin
|
|||
matchPrefixAux it.remaining t it none
|
||||
|
||||
private def toStringAux {α : Type} : Trie α → List Format
|
||||
| (Trie.Node val map) := flip Rbnode.fold map (λ c t Fs,
|
||||
| (Trie.Node val map) := flip RBNode.fold map (λ c t Fs,
|
||||
toFormat (repr c) :: (Format.group $ Format.nest 2 $ flip Format.joinSep Format.line $ toStringAux t) :: Fs) []
|
||||
|
||||
instance {α : Type} : HasToString (Trie α) :=
|
||||
|
|
|
|||
|
|
@ -37,7 +37,7 @@ end Position
|
|||
/-- A precomputed cache for quickly mapping Char offsets to positionitions. -/
|
||||
structure FileMap :=
|
||||
-- A mapping from Char offset of line start to line index
|
||||
(lines : Rbmap Nat Nat (<))
|
||||
(lines : RBMap Nat Nat (<))
|
||||
|
||||
namespace FileMap
|
||||
private def fromStringAux : Nat → String.Iterator → Nat → List (Nat × Nat)
|
||||
|
|
@ -49,7 +49,7 @@ private def fromStringAux : Nat → String.Iterator → Nat → List (Nat × Nat
|
|||
| other := fromStringAux k it.next line
|
||||
|
||||
def fromString (s : String) : FileMap :=
|
||||
{lines := Rbmap.ofList $ fromStringAux s.length s.mkIterator 1}
|
||||
{lines := RBMap.ofList $ fromStringAux s.length s.mkIterator 1}
|
||||
|
||||
def toPosition (m : FileMap) (off : Nat) : Position :=
|
||||
match m.lines.lowerBound off with
|
||||
|
|
|
|||
|
|
@ -25,7 +25,7 @@ fmt ++ Format.nest 2 (Format.join $ subtraces.map (λ t, Format.line ++ t.pp))
|
|||
|
||||
namespace Trace
|
||||
|
||||
def TraceMap := Rbmap Position Trace (<)
|
||||
def TraceMap := RBMap Position Trace (<)
|
||||
|
||||
structure TraceState :=
|
||||
(opts : Options)
|
||||
|
|
@ -77,7 +77,7 @@ instance (m) [Monad m] : MonadTracer (TraceT m) :=
|
|||
}
|
||||
|
||||
unsafe def TraceT.run {m α} [Monad m] (opts : Options) (x : TraceT m α) : m (α × TraceMap) :=
|
||||
do (a, st) ← StateT.run x {opts := opts, roots := mkRbmap _ _ _, curPos := none, curTraces := []},
|
||||
do (a, st) ← StateT.run x {opts := opts, roots := mkRBMap _ _ _, curPos := none, curTraces := []},
|
||||
pure (a, st.roots)
|
||||
|
||||
end Trace
|
||||
|
|
|
|||
|
|
@ -203,14 +203,14 @@ instance HasWellFounded {α : Type u} {β : Type v} [s₁ : HasWellFounded α] [
|
|||
|
||||
end Prod
|
||||
|
||||
namespace Psigma
|
||||
namespace PSigma
|
||||
section
|
||||
variables {α : Sort u} {β : α → Sort v}
|
||||
variable (r : α → α → Prop)
|
||||
variable (s : ∀ a, β a → β a → Prop)
|
||||
|
||||
-- Lexicographical order based on r and s
|
||||
inductive Lex : Psigma β → Psigma β → Prop
|
||||
inductive Lex : PSigma β → PSigma β → Prop
|
||||
| left : ∀ {a₁ : α} (b₁ : β a₁) {a₂ : α} (b₂ : β a₂), r a₁ a₂ → Lex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
|
||||
| right : ∀ (a : α) {b₁ b₂ : β a}, s a b₁ b₂ → Lex ⟨a, b₁⟩ ⟨a, b₂⟩
|
||||
end
|
||||
|
|
@ -229,7 +229,7 @@ Acc.ndrecOn aca
|
|||
(ihb : ∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩),
|
||||
Acc.intro ⟨xa, xb⟩ (λ p (lt : p ≺ ⟨xa, xb⟩),
|
||||
have aux : xa = xa → xb ≅ xb → Acc (Lex r s) p, from
|
||||
@Psigma.Lex.recOn α β r s (λ p₁ p₂ _, p₂.1 = xa → p₂.2 ≅ xb → Acc (Lex r s) p₁)
|
||||
@PSigma.Lex.recOn α β r s (λ p₁ p₂ _, p₂.1 = xa → p₂.2 ≅ xb → Acc (Lex r s) p₁)
|
||||
p ⟨xa, xb⟩ lt
|
||||
(λ (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂) (h : r a₁ a₂) (Eq₂ : a₂ = xa) (Eq₃ : b₂ ≅ xb),
|
||||
have aux : (∀ (y : α), r y xa → ∀ (b : β y), Acc (Lex r s) ⟨y, b⟩) →
|
||||
|
|
@ -269,7 +269,7 @@ section
|
|||
variables {α : Sort u} {β : Sort v}
|
||||
|
||||
-- Reverse lexicographical order based on r and s
|
||||
inductive RevLex (r : α → α → Prop) (s : β → β → Prop) : @Psigma α (λ a, β) → @Psigma α (λ a, β) → Prop
|
||||
inductive RevLex (r : α → α → Prop) (s : β → β → Prop) : @PSigma α (λ a, β) → @PSigma α (λ a, β) → Prop
|
||||
| left : ∀ {a₁ a₂ : α} (b : β), r a₁ a₂ → RevLex ⟨a₁, b⟩ ⟨a₂, b⟩
|
||||
| right : ∀ (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β}, s b₁ b₂ → RevLex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
|
||||
end
|
||||
|
|
@ -305,7 +305,7 @@ WellFounded.intro $ λ ⟨a, b⟩, revLexAccessible (apply hb b) (WellFounded.ap
|
|||
end
|
||||
|
||||
section
|
||||
def skipLeft (α : Type u) {β : Type v} (s : β → β → Prop) : @Psigma α (λ a, β) → @Psigma α (λ a, β) → Prop :=
|
||||
def skipLeft (α : Type u) {β : Type v} (s : β → β → Prop) : @PSigma α (λ a, β) → @PSigma α (λ a, β) → Prop :=
|
||||
RevLex emptyRelation s
|
||||
|
||||
def skipLeftWf (α : Type u) {β : Type v} {s : β → β → Prop} (hb : WellFounded s) : WellFounded (skipLeft α s) :=
|
||||
|
|
@ -316,10 +316,10 @@ def mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → P
|
|||
RevLex.right _ _ _ h
|
||||
end
|
||||
|
||||
instance HasWellFounded {α : Type u} {β : α → Type v} [s₁ : HasWellFounded α] [s₂ : ∀ a, HasWellFounded (β a)] : HasWellFounded (Psigma β) :=
|
||||
instance HasWellFounded {α : Type u} {β : α → Type v} [s₁ : HasWellFounded α] [s₂ : ∀ a, HasWellFounded (β a)] : HasWellFounded (PSigma β) :=
|
||||
{r := Lex s₁.r (λ a, (s₂ a).r), wf := lexWf s₁.wf (λ a, (s₂ a).wf)}
|
||||
|
||||
end Psigma
|
||||
end PSigma
|
||||
|
||||
/- Temporary hack for bootstrapping Lean.
|
||||
TODO: DELETE!!!!
|
||||
|
|
|
|||
|
|
@ -495,14 +495,14 @@ void initialize_constants() {
|
|||
g_out_param = new name{"outParam"};
|
||||
g_pexpr = new name{"pexpr"};
|
||||
g_pexpr_subst = new name{"pexpr", "subst"};
|
||||
g_punit = new name{"Punit"};
|
||||
g_punit_cases_on = new name{"Punit", "casesOn"};
|
||||
g_punit_star = new name{"Punit", "star"};
|
||||
g_punit = new name{"PUnit"};
|
||||
g_punit_cases_on = new name{"PUnit", "casesOn"};
|
||||
g_punit_star = new name{"PUnit", "star"};
|
||||
g_prod_mk = new name{"Prod", "mk"};
|
||||
g_pprod = new name{"Pprod"};
|
||||
g_pprod_mk = new name{"Pprod", "mk"};
|
||||
g_pprod_fst = new name{"Pprod", "fst"};
|
||||
g_pprod_snd = new name{"Pprod", "snd"};
|
||||
g_pprod = new name{"PProd"};
|
||||
g_pprod_mk = new name{"PProd", "mk"};
|
||||
g_pprod_fst = new name{"PProd", "fst"};
|
||||
g_pprod_snd = new name{"PProd", "snd"};
|
||||
g_propext = new name{"propext"};
|
||||
g_to_pexpr = new name{"toPexpr"};
|
||||
g_quot_mk = new name{"Quot", "mk"};
|
||||
|
|
@ -513,11 +513,11 @@ void initialize_constants() {
|
|||
g_rfl = new name{"rfl"};
|
||||
g_scope_trace = new name{"scopeTrace"};
|
||||
g_set_of = new name{"setOf"};
|
||||
g_psigma = new name{"Psigma"};
|
||||
g_psigma_cases_on = new name{"Psigma", "casesOn"};
|
||||
g_psigma_mk = new name{"Psigma", "mk"};
|
||||
g_psigma_fst = new name{"Psigma", "fst"};
|
||||
g_psigma_snd = new name{"Psigma", "snd"};
|
||||
g_psigma = new name{"PSigma"};
|
||||
g_psigma_cases_on = new name{"PSigma", "casesOn"};
|
||||
g_psigma_mk = new name{"PSigma", "mk"};
|
||||
g_psigma_fst = new name{"PSigma", "fst"};
|
||||
g_psigma_snd = new name{"PSigma", "snd"};
|
||||
g_singleton = new name{"singleton"};
|
||||
g_sizeof = new name{"sizeof"};
|
||||
g_sorry_ax = new name{"sorryAx"};
|
||||
|
|
@ -537,10 +537,10 @@ void initialize_constants() {
|
|||
g_subtype_mk = new name{"Subtype", "mk"};
|
||||
g_subtype_val = new name{"Subtype", "val"};
|
||||
g_subtype_rec = new name{"Subtype", "rec"};
|
||||
g_psum = new name{"Psum"};
|
||||
g_psum_cases_on = new name{"Psum", "casesOn"};
|
||||
g_psum_inl = new name{"Psum", "inl"};
|
||||
g_psum_inr = new name{"Psum", "inr"};
|
||||
g_psum = new name{"PSum"};
|
||||
g_psum_cases_on = new name{"PSum", "casesOn"};
|
||||
g_psum_inl = new name{"PSum", "inl"};
|
||||
g_psum_inr = new name{"PSum", "inr"};
|
||||
g_tactic = new name{"tactic"};
|
||||
g_tactic_try = new name{"tactic", "try"};
|
||||
g_tactic_triv = new name{"tactic", "triv"};
|
||||
|
|
|
|||
|
|
@ -206,14 +206,14 @@ Or
|
|||
outParam
|
||||
pexpr
|
||||
pexpr.subst
|
||||
Punit
|
||||
Punit.casesOn
|
||||
Punit.star
|
||||
PUnit
|
||||
PUnit.casesOn
|
||||
PUnit.star
|
||||
Prod.mk
|
||||
Pprod
|
||||
Pprod.mk
|
||||
Pprod.fst
|
||||
Pprod.snd
|
||||
PProd
|
||||
PProd.mk
|
||||
PProd.fst
|
||||
PProd.snd
|
||||
propext
|
||||
toPexpr
|
||||
Quot.mk
|
||||
|
|
@ -224,11 +224,11 @@ repr
|
|||
rfl
|
||||
scopeTrace
|
||||
setOf
|
||||
Psigma
|
||||
Psigma.casesOn
|
||||
Psigma.mk
|
||||
Psigma.fst
|
||||
Psigma.snd
|
||||
PSigma
|
||||
PSigma.casesOn
|
||||
PSigma.mk
|
||||
PSigma.fst
|
||||
PSigma.snd
|
||||
singleton
|
||||
sizeof
|
||||
sorryAx
|
||||
|
|
@ -248,10 +248,10 @@ Subtype
|
|||
Subtype.mk
|
||||
Subtype.val
|
||||
Subtype.rec
|
||||
Psum
|
||||
Psum.casesOn
|
||||
Psum.inl
|
||||
Psum.inr
|
||||
PSum
|
||||
PSum.casesOn
|
||||
PSum.inl
|
||||
PSum.inr
|
||||
tactic
|
||||
tactic.try
|
||||
tactic.triv
|
||||
|
|
|
|||
|
|
@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#pragma clang diagnostic ignored "-Wreturn-std-move"
|
||||
#include <utility>
|
||||
#include <algorithm>
|
||||
#include "runtime/optional.h"
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue