From 548e7c5436de67dc53dec6b236395ab40f72b49a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Mar 2019 18:28:01 -0700 Subject: [PATCH] chore(tests/playground): fix playground tests --- tests/playground/flat_parser.lean | 42 ++++++++++----------- tests/playground/parser.lean | 20 +++++----- tests/playground/rbmap.lean | 30 +++++++-------- tests/playground/rbmap2.lean | 24 ++++++------ tests/playground/rbmap3.lean | 30 +++++++-------- tests/playground/ref1.lean | 16 ++++---- tests/playground/ref2.lean | 8 ++-- tests/playground/unionfind1.lean | 62 +++++++++++++++---------------- tests/playground/unionfind2.lean | 62 +++++++++++++++---------------- 9 files changed, 147 insertions(+), 147 deletions(-) diff --git a/tests/playground/flat_parser.lean b/tests/playground/flat_parser.lean index b6a15db3f5..9e36630ad9 100644 --- a/tests/playground/flat_parser.lean +++ b/tests/playground/flat_parser.lean @@ -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 diff --git a/tests/playground/parser.lean b/tests/playground/parser.lean index a10e4d0050..b5982e79cd 100644 --- a/tests/playground/parser.lean +++ b/tests/playground/parser.lean @@ -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 diff --git a/tests/playground/rbmap.lean b/tests/playground/rbmap.lean index 0f11a2e3a5..9a191ee426 100644 --- a/tests/playground/rbmap.lean +++ b/tests/playground/rbmap.lean @@ -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)) diff --git a/tests/playground/rbmap2.lean b/tests/playground/rbmap2.lean index fa9594193d..2ff59a0f0c 100644 --- a/tests/playground/rbmap2.lean +++ b/tests/playground/rbmap2.lean @@ -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 diff --git a/tests/playground/rbmap3.lean b/tests/playground/rbmap3.lean index 3bc5aca103..24406a6398 100644 --- a/tests/playground/rbmap3.lean +++ b/tests/playground/rbmap3.lean @@ -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 -/ diff --git a/tests/playground/ref1.lean b/tests/playground/ref1.lean index ba9c5b554f..ed54e0416b 100644 --- a/tests/playground/ref1.lean +++ b/tests/playground/ref1.lean @@ -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₂ diff --git a/tests/playground/ref2.lean b/tests/playground/ref2.lean index 701caf6a64..cfee291ac8 100644 --- a/tests/playground/ref2.lean +++ b/tests/playground/ref2.lean @@ -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 := diff --git a/tests/playground/unionfind1.lean b/tests/playground/unionfind1.lean index 36363db9d4..91b6302a5b 100644 --- a/tests/playground/unionfind1.lean +++ b/tests/playground/unionfind1.lean @@ -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 diff --git a/tests/playground/unionfind2.lean b/tests/playground/unionfind2.lean index 798cf2b702..9d03dade01 100644 --- a/tests/playground/unionfind2.lean +++ b/tests/playground/unionfind2.lean @@ -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