chore(tests/playground): fix playground tests
This commit is contained in:
Leonardo de Moura
parent
452d5107ac
commit
548e7c5436
9 changed files with 147 additions and 147 deletions
|
|
@ -1,4 +1,4 @@
|
|||
import init.Lean.Message init.Lean.Parser.Syntax init.Lean.Parser.Trie init.Lean.Parser.basic
|
||||
import init.lean.message init.lean.parser.syntax init.lean.parser.trie init.lean.parser.basic
|
||||
|
||||
namespace Lean
|
||||
namespace flatParser
|
||||
|
|
@ -26,17 +26,17 @@ private def fromStringAux (s : String) : Nat → Nat → Nat → pos → Array N
|
|||
else fromStringAux k offset line i offsets lines
|
||||
|
||||
def fromString (s : String) : FileMap :=
|
||||
fromStringAux s s.length 0 1 0 (Array.nil.push 0) (Array.nil.push 1)
|
||||
fromStringAux s s.length 0 1 0 (Array.empty.push 0) (Array.empty.push 1)
|
||||
|
||||
/- Remark: `offset is in [(offsets.get b), (offsets.get e)]` and `b < e` -/
|
||||
private def toPositionAux (offsets : Array Nat) (lines : Array Nat) (offset : Nat) : Nat → Nat → Nat → Position
|
||||
| 0 b e := ⟨offset, 1⟩ -- unreachable
|
||||
| (k+1) b e :=
|
||||
let offsetB := offsets.read' b in
|
||||
if e = b + 1 then ⟨offset - offsetB, lines.read' b⟩
|
||||
let offsetB := offsets.get b in
|
||||
if e = b + 1 then ⟨offset - offsetB, lines.get b⟩
|
||||
else let m := (b + e) / 2 in
|
||||
let offsetM := offsets.read' m in
|
||||
if offset = offsetM then ⟨0, lines.read' m⟩
|
||||
let offsetM := offsets.get m in
|
||||
if offset = offsetM then ⟨0, lines.get m⟩
|
||||
else if offset > offsetM then toPositionAux k m e
|
||||
else toPositionAux k b m
|
||||
|
||||
|
|
@ -86,7 +86,7 @@ False.elim (errorIsNotOk h)
|
|||
|
||||
def resultOk := {r : Result Unit // r.IsOk}
|
||||
|
||||
@[inline] def mkResultOk (i : pos) (cache : ParserCache) (State : ParserState) (eps := tt) : resultOk :=
|
||||
@[inline] def mkResultOk (i : pos) (cache : ParserCache) (State : ParserState) (eps := true) : resultOk :=
|
||||
⟨Result.ok () i cache State eps, Result.IsOk.mk _ _ _ _ _⟩
|
||||
|
||||
def parserCoreM (α : Type) :=
|
||||
|
|
@ -107,7 +107,7 @@ abbreviation trailingParser := Syntax → Parser
|
|||
@[inline] def parserM.pure {α : Type} (a : α) : parserM α :=
|
||||
λ _ _ r,
|
||||
match r with
|
||||
| ⟨Result.ok _ it c s _, h⟩ := Result.ok a it c s tt
|
||||
| ⟨Result.ok _ it c s _, h⟩ := Result.ok a it c s true
|
||||
| ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h
|
||||
|
||||
@[inlineIfReduce] def eagerOr (b₁ b₂ : Bool) := b₁ || b₂
|
||||
|
|
@ -130,14 +130,14 @@ instance : Monad parserM :=
|
|||
match r with
|
||||
| ⟨Result.ok _ i₁ _ s₁ _, _⟩ :=
|
||||
(match p ps cfg r with
|
||||
| Result.error msg₁ i₂ c₂ stx₁ tt := q ps cfg (mkResultOk i₁ c₂ s₁)
|
||||
| Result.error msg₁ i₂ c₂ stx₁ true := q ps cfg (mkResultOk i₁ c₂ s₁)
|
||||
| other := other)
|
||||
| ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h
|
||||
|
||||
@[inline] protected def failure {α : Type} : parserM α :=
|
||||
λ _ _ r,
|
||||
match r with
|
||||
| ⟨Result.ok _ i c s _, h⟩ := Result.error "failure" i c Syntax.missing tt
|
||||
| ⟨Result.ok _ i c s _, h⟩ := Result.error "failure" i c Syntax.missing true
|
||||
| ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h
|
||||
|
||||
instance : Alternative parserM :=
|
||||
|
|
@ -146,7 +146,7 @@ instance : Alternative parserM :=
|
|||
..flatParser.Monad }
|
||||
|
||||
def setSilentError {α : Type} : Result α → Result α
|
||||
| (Result.error i c msg stx _) := Result.error i c msg stx tt
|
||||
| (Result.error i c msg stx _) := Result.error i c msg stx true
|
||||
| other := other
|
||||
|
||||
/--
|
||||
|
|
@ -176,7 +176,7 @@ cfg.input.length
|
|||
| ⟨Result.ok _ _ _ s _, _⟩ := s
|
||||
| ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h
|
||||
|
||||
def mkError {α : Type} (r : resultOk) (msg : String) (stx : Syntax := Syntax.missing) (eps := tt) : Result α :=
|
||||
def mkError {α : Type} (r : resultOk) (msg : String) (stx : Syntax := Syntax.missing) (eps := true) : Result α :=
|
||||
match r with
|
||||
| ⟨Result.ok _ i c s _, _⟩ := Result.error msg i c stx eps
|
||||
| ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h
|
||||
|
|
@ -187,12 +187,12 @@ match r with
|
|||
| ⟨Result.ok _ i ch st e, _⟩ :=
|
||||
if atEnd cfg i then mkError r "end of input"
|
||||
else let c := curr cfg i in
|
||||
if p c then Result.ok c (next cfg i) ch st ff
|
||||
if p c then Result.ok c (next cfg i) ch st false
|
||||
else mkError r "unexpected character"
|
||||
| ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h
|
||||
|
||||
def any : parserM Char :=
|
||||
satisfy (λ _, tt)
|
||||
satisfy (λ _, true)
|
||||
|
||||
@[specialize] def takeUntilAux (p : Char → Bool) (cfg : ParserConfig) : Nat → resultOk → Result Unit
|
||||
| 0 r := r.val
|
||||
|
|
@ -202,7 +202,7 @@ satisfy (λ _, tt)
|
|||
if atEnd cfg i then r.val
|
||||
else let c := curr cfg i in
|
||||
if p c then r.val
|
||||
else takeUntilAux n (mkResultOk (next cfg i) ch st tt)
|
||||
else takeUntilAux n (mkResultOk (next cfg i) ch st true)
|
||||
| ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h
|
||||
|
||||
@[specialize] def takeUntil (p : Char → Bool) : parserM Unit :=
|
||||
|
|
@ -224,9 +224,9 @@ def strAux (cfg : ParserConfig) (str : String) (error : String) : Nat → result
|
|||
else
|
||||
match r with
|
||||
| ⟨Result.ok _ i ch st e, _⟩ :=
|
||||
if atEnd cfg i then Result.error error i ch Syntax.missing tt
|
||||
else if curr cfg i = str.utf8Get j then strAux n (mkResultOk (next cfg i) ch st tt) (str.utf8Next j)
|
||||
else Result.error error i ch Syntax.missing tt
|
||||
if atEnd cfg i then Result.error error i ch Syntax.missing true
|
||||
else if curr cfg i = str.utf8Get j then strAux n (mkResultOk (next cfg i) ch st true) (str.utf8Next j)
|
||||
else Result.error error i ch Syntax.missing true
|
||||
| ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h
|
||||
|
||||
-- #exit
|
||||
|
|
@ -240,11 +240,11 @@ def strAux (cfg : ParserConfig) (str : String) (error : String) : Nat → result
|
|||
let i₀ := currPos r in
|
||||
let s₀ := currState r in
|
||||
match p ps cfg r with
|
||||
| Result.ok a i c s _ := manyAux k ff ps cfg (mkResultOk i c s)
|
||||
| Result.ok a i c s _ := manyAux k false ps cfg (mkResultOk i c s)
|
||||
| Result.error _ _ c _ _ := Result.ok () i₀ c s₀ fst
|
||||
|
||||
@[inline] def many (p : parserM Unit) : parserM Unit :=
|
||||
λ ps cfg r, manyAux p (inputSize cfg) tt ps cfg r
|
||||
λ ps cfg r, manyAux p (inputSize cfg) true ps cfg r
|
||||
|
||||
@[inline] def many1 (p : parserM Unit) : parserM Unit :=
|
||||
p *> many p
|
||||
|
|
@ -256,7 +256,7 @@ def testParser {α : Type} (x : parserM α) (input : String) : String :=
|
|||
let r :=
|
||||
x { cmdParser := dummyParserCore, termParser := λ _, dummyParserCore }
|
||||
{ filename := "test", input := input, FileMap := FileMap.fromString input, tokens := Lean.Parser.Trie.mk }
|
||||
(mkResultOk 0 {} {messages := MessageLog.Empty}) in
|
||||
(mkResultOk 0 {} {messages := MessageLog.empty}) in
|
||||
match r with
|
||||
| Result.ok _ i _ _ _ := "Ok at " ++ toString i
|
||||
| Result.error msg i _ _ _ := "Error at " ++ toString i ++ ": " ++ msg
|
||||
|
|
|
|||
|
|
@ -25,7 +25,7 @@ False.elim (errorIsNotOk h)
|
|||
|
||||
def input (σ δ μ : Type) : Type := { r : Result σ δ μ Unit // r.IsOk }
|
||||
|
||||
@[inline] def mkInput {σ δ μ : Type} (i : pos) (st : σ) (bst : δ) (eps := tt) : input σ δ μ :=
|
||||
@[inline] def mkInput {σ δ μ : Type} (i : pos) (st : σ) (bst : δ) (eps := true) : input σ δ μ :=
|
||||
⟨Result.ok () i st bst eps, Result.IsOk.mk _ _ _ _ _⟩
|
||||
|
||||
def parserM (σ δ μ α : Type) :=
|
||||
|
|
@ -39,7 +39,7 @@ p s (mkInput 0 st bst)
|
|||
@[inline] def parserM.pure (a : α) : parserM σ δ μ α :=
|
||||
λ _ inp,
|
||||
match inp with
|
||||
| ⟨Result.ok _ it st bst _, h⟩ := Result.ok a it st bst tt
|
||||
| ⟨Result.ok _ it st bst _, h⟩ := Result.ok a it st bst true
|
||||
| ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h
|
||||
|
||||
@[inlineIfReduce] def strictOr (b₁ b₂ : Bool) := b₁ || b₂
|
||||
|
|
@ -57,7 +57,7 @@ p s (mkInput 0 st bst)
|
|||
instance parserMIsMonad : Monad (parserM σ δ μ) :=
|
||||
{pure := @parserM.pure _ _ _, bind := @parserM.bind _ _ _}
|
||||
|
||||
def mkError (r : input σ δ μ) (msg : String) (eps := tt) : Result σ δ μ α :=
|
||||
def mkError (r : input σ δ μ) (msg : String) (eps := true) : Result σ δ μ α :=
|
||||
match r with
|
||||
| ⟨Result.ok _ i c s _, _⟩ := Result.error msg i c none eps
|
||||
| ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h
|
||||
|
|
@ -80,7 +80,7 @@ instance : Alternative (parserM σ δ μ) :=
|
|||
.. Parser.parserMIsMonad }
|
||||
|
||||
def setSilentError : Result σ δ μ α → Result σ δ μ α
|
||||
| (Result.error msg i st ext _) := Result.error msg i st ext tt
|
||||
| (Result.error msg i st ext _) := Result.error msg i st ext true
|
||||
| other := other
|
||||
|
||||
@[inline] def curr (str : String) (i : pos) : Char := str.utf8Get i
|
||||
|
|
@ -100,7 +100,7 @@ namespace Prim
|
|||
match inp with
|
||||
| ⟨Result.ok _ i _ bst _, _⟩ :=
|
||||
(match p str inp with
|
||||
| Result.ok a _ st _ _ := Result.ok a i st bst tt
|
||||
| Result.ok a _ st _ _ := Result.ok a i st bst true
|
||||
| other := other)
|
||||
| ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h
|
||||
|
||||
|
|
@ -110,7 +110,7 @@ namespace Prim
|
|||
| ⟨Result.ok _ i st bst _, _⟩ :=
|
||||
if atEnd str i then mkError inp "end of input"
|
||||
else let c := curr str i in
|
||||
if p c then Result.ok c (next str i) st bst ff
|
||||
if p c then Result.ok c (next str i) st bst false
|
||||
else mkError inp "unexpected character"
|
||||
| ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h
|
||||
|
||||
|
|
@ -122,7 +122,7 @@ namespace Prim
|
|||
if atEnd str i then inp.val
|
||||
else let c := curr str i in
|
||||
if p c then inp.val
|
||||
else takeUntilAux n str (mkInput (next str i) st bst ff)
|
||||
else takeUntilAux n str (mkInput (next str i) st bst false)
|
||||
| ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h
|
||||
|
||||
@[inline] def takeUntil (p : Char → Bool) : parserM σ δ μ Unit :=
|
||||
|
|
@ -136,7 +136,7 @@ def strAux (inS : String) (s : String) (errorMsg : String) : Nat → input σ δ
|
|||
match inp with
|
||||
| ⟨Result.ok _ i st bst e, _⟩ :=
|
||||
if atEnd inS i then mkError inp errorMsg
|
||||
else if curr inS i = curr s j then strAux n (mkInput (next inS i) st bst ff) (next s j)
|
||||
else if curr inS i = curr s j then strAux n (mkInput (next inS i) st bst false) (next s j)
|
||||
else mkError inp errorMsg
|
||||
| ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h
|
||||
|
||||
|
|
@ -149,13 +149,13 @@ def strAux (inS : String) (s : String) (errorMsg : String) : Nat → input σ δ
|
|||
match inp with
|
||||
| ⟨Result.ok _ i₀ _ bst₀ _, _⟩ :=
|
||||
(match p str inp with
|
||||
| Result.ok _ i st bst _ := manyLoop k ff str (mkInput i st bst)
|
||||
| Result.ok _ i st bst _ := manyLoop k false str (mkInput i st bst)
|
||||
| Result.error _ _ st _ _ := Result.ok a i₀ st bst₀ fst)
|
||||
| ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h
|
||||
|
||||
-- Auxiliary Function used to lift manyAux
|
||||
@[inline] def manyAux (a : α) (p : parserM σ δ μ α) : parserM σ δ μ α :=
|
||||
λ str inp, manyLoop a p str.length tt str inp
|
||||
λ str inp, manyLoop a p str.length true str inp
|
||||
|
||||
@[inline] def many (p : parserM σ δ μ Unit) : parserM σ δ μ Unit :=
|
||||
manyAux () p
|
||||
|
|
|
|||
|
|
@ -4,41 +4,41 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import init.data.Ordering.basic init.coe init.data.Option.basic init.IO
|
||||
import init.data.ordering.basic init.coe init.data.option.basic init.io
|
||||
|
||||
universes u v w w'
|
||||
|
||||
inductive color
|
||||
| Red | Black
|
||||
|
||||
inductive Node
|
||||
| Leaf {} : Node
|
||||
| Node (color : color) (lchild : Node) (key : Nat) (val : Bool) (rchild : Node) : Node
|
||||
inductive Tree
|
||||
| Leaf {} : Tree
|
||||
| Node (color : color) (lchild : Tree) (key : Nat) (val : Bool) (rchild : Tree) : Tree
|
||||
|
||||
variables {σ : Type w}
|
||||
open color Nat Node
|
||||
open color Nat Tree
|
||||
|
||||
def fold (f : Nat → Bool → σ → σ) : Node → σ → σ
|
||||
def fold (f : Nat → Bool → σ → σ) : Tree → σ → σ
|
||||
| Leaf b := b
|
||||
| (Node _ l k v r) b := fold r (f k v (fold l b))
|
||||
|
||||
def balance1 : Node → Node → Node
|
||||
def balance1 : Tree → Tree → Tree
|
||||
| (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
|
||||
|
||||
def balance2 : Node → Node → Node
|
||||
def balance2 : Tree → Tree → Tree
|
||||
| (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
|
||||
|
||||
def isRed : Node → Bool
|
||||
| (Node Red _ _ _ _) := tt
|
||||
| _ := ff
|
||||
def isRed : Tree → Bool
|
||||
| (Node Red _ _ _ _) := true
|
||||
| _ := false
|
||||
|
||||
def ins : Node → Nat → Bool → Node
|
||||
def ins : Tree → Nat → Bool → Tree
|
||||
| Leaf kx vx := Node Red Leaf kx vx Leaf
|
||||
| (Node Red a ky vy b) kx vx :=
|
||||
(if kx < ky then Node Red (ins a kx vx) ky vy b
|
||||
|
|
@ -52,15 +52,15 @@ def ins : Node → Nat → Bool → Node
|
|||
else 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 : Node → Node
|
||||
def setBlack : Tree → Tree
|
||||
| (Node _ l k v r) := Node Black l k v r
|
||||
| e := e
|
||||
|
||||
def insert (t : Node) (k : Nat) (v : Bool) : Node :=
|
||||
def insert (t : Tree) (k : Nat) (v : Bool) : Tree :=
|
||||
if isRed t then setBlack (ins t k v)
|
||||
else ins t k v
|
||||
|
||||
def mkMapAux : Nat → Node → Node
|
||||
def mkMapAux : Nat → Tree → Tree
|
||||
| 0 m := m
|
||||
| (n+1) m := mkMapAux n (insert m n (n % 10 = 0))
|
||||
|
||||
|
|
|
|||
|
|
@ -49,11 +49,11 @@ protected def max : Rbnode α β → Option (Σ k : α, β k)
|
|||
| (Node _ l k v r) b := revFold l (f k v (revFold r b))
|
||||
|
||||
@[specialize] def all (p : Π k : α, β k → Bool) : Rbnode α β → Bool
|
||||
| leaf := tt
|
||||
| leaf := true
|
||||
| (Node _ l k v r) := p k v && all l && all r
|
||||
|
||||
@[specialize] def any (p : Π k : α, β k → Bool) : Rbnode α β → Bool
|
||||
| leaf := ff
|
||||
| leaf := false
|
||||
| (Node _ l k v r) := p k v || any l || any r
|
||||
|
||||
def balance (rb : Rbcolor) (t1 : Rbnode α β) (k : α) (vk : β k) (t2 : Rbnode α β) :=
|
||||
|
|
@ -78,7 +78,7 @@ match t with
|
|||
| Node _ a x vx b := Node black a x vx b
|
||||
|
||||
section insert
|
||||
variables (lt : α → α → Prop) [decidableRel lt]
|
||||
variables (lt : α → α → Prop) [DecidableRel lt]
|
||||
|
||||
def ins (x : α) (vx : β x) : Rbnode α β → Rbnode α β
|
||||
| leaf := Node red leaf x vx leaf
|
||||
|
|
@ -95,7 +95,7 @@ end insert
|
|||
section membership
|
||||
variable (lt : α → α → Prop)
|
||||
|
||||
variable [decidableRel lt]
|
||||
variable [DecidableRel lt]
|
||||
|
||||
def findCore : Rbnode α β → Π k : α, Option (Σ k : α, β k)
|
||||
| leaf x := none
|
||||
|
|
@ -124,7 +124,7 @@ end membership
|
|||
|
||||
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
|
||||
|
||||
|
|
@ -153,12 +153,12 @@ t.val.depth f
|
|||
@[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
|
||||
| ⟨leaf, _⟩ := tt
|
||||
| _ := ff
|
||||
@[inline] def empty : Rbmap α β lt → Bool
|
||||
| ⟨leaf, _⟩ := true
|
||||
| _ := false
|
||||
|
||||
@[specialize] def toList : Rbmap α β lt → List (α × β)
|
||||
| ⟨t, _⟩ := t.revFold (λ k v ps, (k, v)::ps) []
|
||||
|
|
@ -178,7 +178,7 @@ t.mfold (λ k v _, f k v *> pure ⟨⟩) ⟨⟩
|
|||
instance [HasRepr α] [HasRepr β] : HasRepr (Rbmap α β lt) :=
|
||||
⟨λ t, "rbmapOf " ++ repr t.toList⟩
|
||||
|
||||
variables [decidableRel lt]
|
||||
variables [DecidableRel lt]
|
||||
|
||||
def insert : Rbmap α β lt → α → β → Rbmap α β lt
|
||||
| ⟨t, w⟩ k v := ⟨t.insert lt k v, WellFormed.insertWff w rfl⟩
|
||||
|
|
@ -201,7 +201,7 @@ def lowerBound : Rbmap α β lt → α → Option (Σ k : α, β)
|
|||
@[inline] def contains (t : Rbmap α β lt) (a : α) : Bool :=
|
||||
(t.find a).isSome
|
||||
|
||||
def fromList (l : List (α × β)) (lt : α → α → Prop) [decidableRel lt] : Rbmap α β 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
|
||||
|
|
@ -212,7 +212,7 @@ l.foldl (λ r p, r.insert p.1 p.2) (mkRbmap α β lt)
|
|||
|
||||
end Rbmap
|
||||
|
||||
def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (lt : α → α → Prop) [decidableRel lt] : Rbmap α β lt :=
|
||||
def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (lt : α → α → Prop) [DecidableRel lt] : Rbmap α β lt :=
|
||||
Rbmap.fromList l lt
|
||||
|
||||
end tst
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
prelude
|
||||
import init.core init.IO init.data.Ordering
|
||||
import init.core init.io init.data.ordering
|
||||
|
||||
universes u v w
|
||||
|
||||
|
|
@ -43,20 +43,20 @@ protected def max : Rbnode α β → Option (Σ k : α, β k)
|
|||
| (Node _ l k v r) b := revFold l (f k v (revFold r b))
|
||||
|
||||
@[specialize] def all (p : Π k : α, β k → Bool) : Rbnode α β → Bool
|
||||
| leaf := tt
|
||||
| leaf := true
|
||||
| (Node _ l k v r) := p k v && all l && all r
|
||||
|
||||
@[specialize] def any (p : Π k : α, β k → Bool) : Rbnode α β → Bool
|
||||
| leaf := ff
|
||||
| leaf := false
|
||||
| (Node _ l k v r) := p k v || any l || any r
|
||||
|
||||
def isRed : Rbnode α β → Bool
|
||||
| (Node red _ _ _ _) := tt
|
||||
| _ := ff
|
||||
| (Node red _ _ _ _) := true
|
||||
| _ := false
|
||||
|
||||
def rotateLeft : Π (n : Rbnode α β), n ≠ leaf → Rbnode α β
|
||||
| n@(Node hc hl hk hv (Node red xl xk xv xr)) _ :=
|
||||
if not (isRed hl)
|
||||
if !isRed hl
|
||||
then (Node hc (Node red hl hk hv xl) xk xv xr)
|
||||
else n
|
||||
| leaf h := absurd rfl h
|
||||
|
|
@ -114,7 +114,7 @@ def setBlack : Rbnode α β → Rbnode α β
|
|||
| n := n
|
||||
|
||||
section insert
|
||||
variables (lt : α → α → Prop) [decidableRel lt]
|
||||
variables (lt : α → α → Prop) [DecidableRel lt]
|
||||
|
||||
def ins (x : α) (vx : β x) : Rbnode α β → Rbnode α β
|
||||
| leaf := Node red leaf x vx leaf
|
||||
|
|
@ -131,7 +131,7 @@ end insert
|
|||
section membership
|
||||
variable (lt : α → α → Prop)
|
||||
|
||||
variable [decidableRel lt]
|
||||
variable [DecidableRel lt]
|
||||
|
||||
def findCore : Rbnode α β → Π k : α, Option (Σ k : α, β k)
|
||||
| leaf x := none
|
||||
|
|
@ -161,7 +161,7 @@ end membership
|
|||
|
||||
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
|
||||
|
||||
|
|
@ -187,9 +187,9 @@ t.val.depth f
|
|||
@[inline] def revFold (f : α → β → σ → σ) : Rbmap α β lt → σ → σ
|
||||
| ⟨t, _⟩ b := t.revFold f b
|
||||
|
||||
@[inline] def Empty : Rbmap α β lt → Bool
|
||||
| ⟨leaf, _⟩ := tt
|
||||
| _ := ff
|
||||
@[inline] def empty : Rbmap α β lt → Bool
|
||||
| ⟨leaf, _⟩ := true
|
||||
| _ := false
|
||||
|
||||
@[specialize] def toList : Rbmap α β lt → List (α × β)
|
||||
| ⟨t, _⟩ := t.revFold (λ k v ps, (k, v)::ps) []
|
||||
|
|
@ -209,7 +209,7 @@ t.val.depth f
|
|||
instance [HasRepr α] [HasRepr β] : HasRepr (Rbmap α β lt) :=
|
||||
⟨λ t, "rbmapOf " ++ repr t.toList⟩
|
||||
|
||||
variables [decidableRel lt]
|
||||
variables [DecidableRel lt]
|
||||
|
||||
def insert : Rbmap α β lt → α → β → Rbmap α β lt
|
||||
| ⟨t, w⟩ k v := ⟨t.insert lt k v, WellFormed.insertWff w rfl⟩
|
||||
|
|
@ -232,7 +232,7 @@ def lowerBound : Rbmap α β lt → α → Option (Σ k : α, β)
|
|||
@[inline] def contains (t : Rbmap α β lt) (a : α) : Bool :=
|
||||
(t.find a).isSome
|
||||
|
||||
def fromList (l : List (α × β)) (lt : α → α → Prop) [decidableRel lt] : Rbmap α β 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
|
||||
|
|
@ -243,7 +243,7 @@ l.foldl (λ r p, r.insert p.1 p.2) (mkRbmap α β lt)
|
|||
|
||||
end Rbmap
|
||||
|
||||
def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (lt : α → α → Prop) [decidableRel lt] : Rbmap α β lt :=
|
||||
def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (lt : α → α → Prop) [DecidableRel lt] : Rbmap α β lt :=
|
||||
Rbmap.fromList l lt
|
||||
|
||||
/- Test -/
|
||||
|
|
|
|||
|
|
@ -1,15 +1,15 @@
|
|||
def inc (r : IO.ref Nat) : IO Unit :=
|
||||
do v ← r.read,
|
||||
r.write (v+1),
|
||||
def inc (r : IO.Ref Nat) : IO Unit :=
|
||||
do v ← r.get,
|
||||
r.set (v+1),
|
||||
IO.println (">> " ++ toString v)
|
||||
|
||||
def initArray (r : IO.ref (Array Nat)) (n : Nat) : IO Unit :=
|
||||
def initArray (r : IO.Ref (Array Nat)) (n : Nat) : IO Unit :=
|
||||
n.mrepeat $ λ i, do
|
||||
r.modify $ λ a, a.push (2*i)
|
||||
|
||||
def showArrayRef (r : IO.ref (Array Nat)) : IO Unit :=
|
||||
do a ← r.swap Array.nil,
|
||||
a.size.mrepeat (λ i, IO.println ("[" ++ toString i ++ "]: " ++ toString (a.read' i))),
|
||||
def showArrayRef (r : IO.Ref (Array Nat)) : IO Unit :=
|
||||
do a ← r.swap ∅,
|
||||
a.size.mrepeat (λ i, IO.println ("[" ++ toString i ++ "]: " ++ toString (a.get i))),
|
||||
r.swap a,
|
||||
pure ()
|
||||
|
||||
|
|
@ -17,6 +17,6 @@ def main (xs : List String) : IO Unit :=
|
|||
do let n := xs.head.toNat,
|
||||
r₁ ← IO.mkRef 0,
|
||||
n.mrepeat (λ _, inc r₁),
|
||||
r₂ ← IO.mkRef (Array.nil : Array Nat),
|
||||
r₂ ← IO.mkRef (∅ : Array Nat),
|
||||
initArray r₂ n,
|
||||
showArrayRef r₂
|
||||
|
|
|
|||
|
|
@ -1,11 +1,11 @@
|
|||
def initX : IO (IO.ref Nat) :=
|
||||
def initX : IO (IO.Ref Nat) :=
|
||||
IO.mkRef 0
|
||||
|
||||
@[init initX] constant x : IO.ref Nat := default _
|
||||
@[init initX] constant x : IO.Ref Nat := default _
|
||||
|
||||
def inc : IO Unit :=
|
||||
do v ← x.read,
|
||||
x.write (v+1),
|
||||
do v ← x.get,
|
||||
x.set (v+1),
|
||||
IO.println (">> " ++ toString v)
|
||||
|
||||
def main (xs : List String) : IO Unit :=
|
||||
|
|
|
|||
|
|
@ -1,34 +1,34 @@
|
|||
def StateT (m : Type → Type) (σ : Type) (α : Type) := (Unit × σ) → m (α × σ)
|
||||
namespace StateT
|
||||
def StateT' (m : Type → Type) (σ : Type) (α : Type) := (Unit × σ) → m (α × σ)
|
||||
namespace StateT'
|
||||
variables {m : Type → Type} [Monad m] {σ : Type} {α β : Type}
|
||||
@[inline] protected def pure (a : α) : StateT m σ α := λ ⟨_, s⟩, pure (a, s)
|
||||
@[inline] protected def bind (x : StateT m σ α) (f : α → StateT m σ β) : StateT m σ β := λ p, do (a, s') ← x p, f a ((), s')
|
||||
@[inline] def read : StateT m σ σ := λ ⟨_, s⟩, pure (s, s)
|
||||
@[inline] def write (s' : σ) : StateT m σ Unit := λ ⟨_, s⟩, pure ((), s')
|
||||
@[inline] def updt (f : σ → σ) : StateT m σ Unit := λ ⟨_, s⟩, pure ((), f s)
|
||||
instance : Monad (StateT m σ) :=
|
||||
{pure := @StateT.pure _ _ _, bind := @StateT.bind _ _ _}
|
||||
end StateT
|
||||
@[inline] protected def pure (a : α) : StateT' m σ α := λ ⟨_, s⟩, pure (a, s)
|
||||
@[inline] protected def bind (x : StateT' m σ α) (f : α → StateT' m σ β) : StateT' m σ β := λ p, do (a, s') ← x p, f a ((), s')
|
||||
@[inline] def read : StateT' m σ σ := λ ⟨_, s⟩, pure (s, s)
|
||||
@[inline] def write (s' : σ) : StateT' m σ Unit := λ ⟨_, s⟩, pure ((), s')
|
||||
@[inline] def updt (f : σ → σ) : StateT' m σ Unit := λ ⟨_, s⟩, pure ((), f s)
|
||||
instance : Monad (StateT' m σ) :=
|
||||
{pure := @StateT'.pure _ _ _, bind := @StateT'.bind _ _ _}
|
||||
end StateT'
|
||||
|
||||
def ExceptT (m : Type → Type) (ε : Type) (α : Type) := Except Unit Unit → m (Except ε α)
|
||||
namespace ExceptT
|
||||
def ExceptT' (m : Type → Type) (ε : Type) (α : Type) := Except Unit Unit → m (Except ε α)
|
||||
namespace ExceptT'
|
||||
variables {m : Type → Type} [Monad m] {ε : Type} {α β : Type}
|
||||
@[inline] protected def pure (a : α) : ExceptT m ε α :=
|
||||
@[inline] protected def pure (a : α) : ExceptT' m ε α :=
|
||||
λ e, match e with
|
||||
| Except.ok _ := pure (Except.ok a)
|
||||
| Except.error _ := pure (Except.ok a)
|
||||
@[inline] protected def bind (x : ExceptT m ε α) (f : α → ExceptT m ε β) : ExceptT m ε β :=
|
||||
@[inline] protected def bind (x : ExceptT' m ε α) (f : α → ExceptT' m ε β) : ExceptT' m ε β :=
|
||||
λ e, do v ← x e, match v with
|
||||
| Except.error e := pure (Except.error e)
|
||||
| Except.ok a := f a (Except.ok ())
|
||||
@[inline] def error (e : ε) : ExceptT m ε α :=
|
||||
@[inline] def error (e : ε) : ExceptT' m ε α :=
|
||||
λ e', match e' with
|
||||
| Except.ok _ := pure (Except.error e)
|
||||
| Except.error _ := pure (Except.error e)
|
||||
@[inline] def lift (x : m α) : ExceptT m ε α := λ e, do {a ← x, pure (Except.ok a)}
|
||||
instance : Monad (ExceptT m ε) :=
|
||||
{pure := @ExceptT.pure _ _ _, bind := @ExceptT.bind _ _ _}
|
||||
end ExceptT
|
||||
@[inline] def lift (x : m α) : ExceptT' m ε α := λ e, do {a ← x, pure (Except.ok a)}
|
||||
instance : Monad (ExceptT' m ε) :=
|
||||
{pure := @ExceptT'.pure _ _ _, bind := @ExceptT'.bind _ _ _}
|
||||
end ExceptT'
|
||||
|
||||
abbreviation Node := Nat
|
||||
|
||||
|
|
@ -37,12 +37,12 @@ structure nodeData :=
|
|||
|
||||
abbreviation ufData := Array nodeData
|
||||
|
||||
abbreviation M (α : Type) := ExceptT (StateT id ufData) String α
|
||||
@[inline] def read : M ufData := ExceptT.lift StateT.read
|
||||
@[inline] def write (s : ufData) : M Unit := ExceptT.lift (StateT.write s)
|
||||
@[inline] def updt (f : ufData → ufData) : M Unit := ExceptT.lift (StateT.updt f)
|
||||
@[inline] def error {α : Type} (e : String) : M α := ExceptT.error e
|
||||
def run {α : Type} (x : M α) (s : ufData := Array.nil) : Except String α × ufData :=
|
||||
abbreviation M (α : Type) := ExceptT' (StateT' id ufData) String α
|
||||
@[inline] def read : M ufData := ExceptT'.lift StateT'.read
|
||||
@[inline] def write (s : ufData) : M Unit := ExceptT'.lift (StateT'.write s)
|
||||
@[inline] def updt (f : ufData → ufData) : M Unit := ExceptT'.lift (StateT'.updt f)
|
||||
@[inline] def error {α : Type} (e : String) : M α := ExceptT'.error e
|
||||
def run {α : Type} (x : M α) (s : ufData := ∅) : Except String α × ufData :=
|
||||
x (Except.ok ()) ((), s)
|
||||
|
||||
def capacity : M Nat :=
|
||||
|
|
@ -53,10 +53,10 @@ def findEntryAux : Nat → Node → M nodeData
|
|||
| (i+1) n :=
|
||||
do s ← read,
|
||||
if h : n < s.size then
|
||||
do { let e := s.read ⟨n, h⟩,
|
||||
do { let e := s.index ⟨n, h⟩,
|
||||
if e.find = n then pure e
|
||||
else do e₁ ← findEntryAux i e.find,
|
||||
updt (λ s, s.write' n e₁),
|
||||
updt (λ s, s.set n e₁),
|
||||
pure e₁ }
|
||||
else error "invalid Node"
|
||||
|
||||
|
|
@ -77,11 +77,11 @@ do r₁ ← findEntry n₁,
|
|||
r₂ ← findEntry n₂,
|
||||
if r₁.find = r₂.find then pure ()
|
||||
else updt $ λ s,
|
||||
if r₁.rank < r₂.rank then s.write' r₁.find { find := r₂.find }
|
||||
if r₁.rank < r₂.rank then s.set r₁.find { find := r₂.find }
|
||||
else if r₁.rank = r₂.rank then
|
||||
let s₁ := s.write' r₁.find { find := r₂.find } in
|
||||
s₁.write' r₂.find { rank := r₂.rank + 1, .. r₂}
|
||||
else s.write' r₂.find { find := r₁.find }
|
||||
let s₁ := s.set r₁.find { find := r₂.find } in
|
||||
s₁.set r₂.find { rank := r₂.rank + 1, .. r₂}
|
||||
else s.set r₂.find { find := r₁.find }
|
||||
|
||||
|
||||
def mkNodes : Nat → M Unit
|
||||
|
|
|
|||
|
|
@ -1,28 +1,28 @@
|
|||
def StateT (m : Type → Type) (σ : Type) (α : Type) := σ → m (α × σ)
|
||||
namespace StateT
|
||||
def StateT' (m : Type → Type) (σ : Type) (α : Type) := σ → m (α × σ)
|
||||
namespace StateT'
|
||||
variables {m : Type → Type} [Monad m] {σ : Type} {α β : Type}
|
||||
@[inline] protected def pure (a : α) : StateT m σ α := λ s, pure (a, s)
|
||||
@[inline] protected def bind (x : StateT m σ α) (f : α → StateT m σ β) : StateT m σ β := λ s, do (a, s') ← x s, f a s'
|
||||
@[inline] def read : StateT m σ σ := λ s, pure (s, s)
|
||||
@[inline] def write (s' : σ) : StateT m σ Unit := λ s, pure ((), s')
|
||||
@[inline] def updt (f : σ → σ) : StateT m σ Unit := λ s, pure ((), f s)
|
||||
instance : Monad (StateT m σ) :=
|
||||
{pure := @StateT.pure _ _ _, bind := @StateT.bind _ _ _}
|
||||
end StateT
|
||||
@[inline] protected def pure (a : α) : StateT' m σ α := λ s, pure (a, s)
|
||||
@[inline] protected def bind (x : StateT' m σ α) (f : α → StateT' m σ β) : StateT' m σ β := λ s, do (a, s') ← x s, f a s'
|
||||
@[inline] def read : StateT' m σ σ := λ s, pure (s, s)
|
||||
@[inline] def write (s' : σ) : StateT' m σ Unit := λ s, pure ((), s')
|
||||
@[inline] def updt (f : σ → σ) : StateT' m σ Unit := λ s, pure ((), f s)
|
||||
instance : Monad (StateT' m σ) :=
|
||||
{pure := @StateT'.pure _ _ _, bind := @StateT'.bind _ _ _}
|
||||
end StateT'
|
||||
|
||||
def ExceptT (m : Type → Type) (ε : Type) (α : Type) := m (Except ε α)
|
||||
namespace ExceptT
|
||||
def ExceptT' (m : Type → Type) (ε : Type) (α : Type) := m (Except ε α)
|
||||
namespace ExceptT'
|
||||
variables {m : Type → Type} [Monad m] {ε : Type} {α β : Type}
|
||||
@[inline] protected def pure (a : α) : ExceptT m ε α := (pure (Except.ok a) : m (Except ε α))
|
||||
@[inline] protected def bind (x : ExceptT m ε α) (f : α → ExceptT m ε β) : ExceptT m ε β :=
|
||||
@[inline] protected def pure (a : α) : ExceptT' m ε α := (pure (Except.ok a) : m (Except ε α))
|
||||
@[inline] protected def bind (x : ExceptT' m ε α) (f : α → ExceptT' m ε β) : ExceptT' m ε β :=
|
||||
(do { v ← x, match v with
|
||||
| Except.error e := pure (Except.error e)
|
||||
| Except.ok a := f a } : m (Except ε β))
|
||||
@[inline] def error (e : ε) : ExceptT m ε α := (pure (Except.error e) : m (Except ε α))
|
||||
@[inline] def lift (x : m α) : ExceptT m ε α := (do {a ← x, pure (Except.ok a) } : m (Except ε α))
|
||||
instance : Monad (ExceptT m ε) :=
|
||||
{pure := @ExceptT.pure _ _ _, bind := @ExceptT.bind _ _ _}
|
||||
end ExceptT
|
||||
@[inline] def error (e : ε) : ExceptT' m ε α := (pure (Except.error e) : m (Except ε α))
|
||||
@[inline] def lift (x : m α) : ExceptT' m ε α := (do {a ← x, pure (Except.ok a) } : m (Except ε α))
|
||||
instance : Monad (ExceptT' m ε) :=
|
||||
{pure := @ExceptT'.pure _ _ _, bind := @ExceptT'.bind _ _ _}
|
||||
end ExceptT'
|
||||
|
||||
abbreviation Node := Nat
|
||||
|
||||
|
|
@ -31,12 +31,12 @@ structure nodeData :=
|
|||
|
||||
abbreviation ufData := Array nodeData
|
||||
|
||||
abbreviation M (α : Type) := ExceptT (StateT id ufData) String α
|
||||
@[inline] def read : M ufData := ExceptT.lift StateT.read
|
||||
@[inline] def write (s : ufData) : M Unit := ExceptT.lift (StateT.write s)
|
||||
@[inline] def updt (f : ufData → ufData) : M Unit := ExceptT.lift (StateT.updt f)
|
||||
@[inline] def error {α : Type} (e : String) : M α := ExceptT.error e
|
||||
def run {α : Type} (x : M α) (s : ufData := Array.nil) : Except String α × ufData :=
|
||||
abbreviation M (α : Type) := ExceptT' (StateT' id ufData) String α
|
||||
@[inline] def read : M ufData := ExceptT'.lift StateT'.read
|
||||
@[inline] def write (s : ufData) : M Unit := ExceptT'.lift (StateT'.write s)
|
||||
@[inline] def updt (f : ufData → ufData) : M Unit := ExceptT'.lift (StateT'.updt f)
|
||||
@[inline] def error {α : Type} (e : String) : M α := ExceptT'.error e
|
||||
def run {α : Type} (x : M α) (s : ufData := ∅) : Except String α × ufData :=
|
||||
x s
|
||||
|
||||
def capacity : M Nat :=
|
||||
|
|
@ -47,10 +47,10 @@ def findEntryAux : Nat → Node → M nodeData
|
|||
| (i+1) n :=
|
||||
do s ← read,
|
||||
if h : n < s.size then
|
||||
do { let e := s.read ⟨n, h⟩,
|
||||
do { let e := s.index ⟨n, h⟩,
|
||||
if e.find = n then pure e
|
||||
else do e₁ ← findEntryAux i e.find,
|
||||
updt (λ s, s.write' n e₁),
|
||||
updt (λ s, s.set n e₁),
|
||||
pure e₁ }
|
||||
else error "invalid Node"
|
||||
|
||||
|
|
@ -71,11 +71,11 @@ do r₁ ← findEntry n₁,
|
|||
r₂ ← findEntry n₂,
|
||||
if r₁.find = r₂.find then pure ()
|
||||
else updt $ λ s,
|
||||
if r₁.rank < r₂.rank then s.write' r₁.find { find := r₂.find }
|
||||
if r₁.rank < r₂.rank then s.set r₁.find { find := r₂.find }
|
||||
else if r₁.rank = r₂.rank then
|
||||
let s₁ := s.write' r₁.find { find := r₂.find } in
|
||||
s₁.write' r₂.find { rank := r₂.rank + 1, .. r₂}
|
||||
else s.write' r₂.find { find := r₁.find }
|
||||
let s₁ := s.set r₁.find { find := r₂.find } in
|
||||
s₁.set r₂.find { rank := r₂.rank + 1, .. r₂}
|
||||
else s.set r₂.find { find := r₁.find }
|
||||
|
||||
|
||||
def mkNodes : Nat → M Unit
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue