Skip to content

Commit 7376fae

Browse files
datokratdatokrat
committed
wip
1 parent 21e3116 commit 7376fae

File tree

4 files changed

+80
-89
lines changed

4 files changed

+80
-89
lines changed

‎src/Std/Data/Ranges/Array.lean‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
prelude
2+
import Std.Data.Ranges.Slice
3+
4+
instance : Sliceable shape (Array α) Nat α where
5+
6+
instance : SliceIter ⟨.none, .none⟩ (Array α) Nat :=
7+
.of (·.collection.iter)
8+
9+
instance : SliceIter ⟨.closed, .none⟩ (Array α) Nat :=
10+
.of (fun s => s.collection.iter.drop s.range.lower)
11+
12+
instance : SliceIter ⟨.open, .none⟩ (Array α) Nat :=
13+
.of (fun s => s.collection.iter.drop (s.range.lower + 1))
14+
15+
instance : SliceIter ⟨.none, .closed⟩ (Array α) Nat :=
16+
.of (fun s => s.collection.iter.take (s.range.upper + 1))
17+
18+
instance : SliceIter ⟨.closed, .closed⟩ (Array α) Nat :=
19+
.of (fun s => s.collection.iter.take (s.range.upper + 1) |>.drop s.range.lower)
20+
21+
instance : SliceIter ⟨.open, .closed⟩ (Array α) Nat :=
22+
.of (fun s => s.collection.iter.take (s.range.upper + 1) |>.drop (s.range.lower + 1))
23+
24+
instance : SliceIter ⟨.none, .open⟩ (Array α) Nat :=
25+
.of (fun s => s.collection.iter.take s.range.upper)
26+
27+
instance : SliceIter ⟨.closed, .open⟩ (Array α) Nat :=
28+
.of (fun s => s.collection.iter.take s.range.upper |>.drop s.range.lower)
29+
30+
instance : SliceIter ⟨.open, .open⟩ (Array α) Nat :=
31+
.of (fun s => s.collection.iter.take s.range.upper |>.drop (s.range.lower + 1))
32+
33+
def testArray : Array Nat := #[0, 1, 2, 3, 4, 5, 6]
34+
35+
#eval testArray[[2<,,]].iter.toList

‎src/Std/Data/Ranges/Basic.lean‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,6 +98,20 @@ instance {State : PRange shape α → Type u} {r : PRange shape α}
9898
IteratorCollectPartial (RangeIter.State r) Id m :=
9999
inferInstanceAs <| IteratorCollectPartial (State r) Id m
100100

101+
instance {State : PRange shape α → Type u} {r : PRange shape α}
102+
[Iterator (State r) Id α] [IteratorLoop (State r) Id m]
103+
{iter : (r : PRange shape α) → Iter (α := State r) α} :
104+
letI : RangeIter shape α := RangeIter.of iter
105+
IteratorLoop (RangeIter.State r) Id m :=
106+
inferInstanceAs <| IteratorLoop (State r) Id m
107+
108+
instance {State : PRange shape α → Type u} {r : PRange shape α}
109+
[Iterator (State r) Id α] [IteratorLoopPartial (State r) Id m]
110+
{iter : (r : PRange shape α) → Iter (α := State r) α} :
111+
letI : RangeIter shape α := RangeIter.of iter
112+
IteratorLoopPartial (RangeIter.State r) Id m :=
113+
inferInstanceAs <| IteratorLoopPartial (State r) Id m
114+
101115
@[always_inline, inline]
102116
def PRange.size [RangeSize shape α] (r : PRange shape α) : Nat :=
103117
RangeSize.size r

‎src/Std/Data/Ranges/General.lean‎

Lines changed: 13 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
prelude
22
import Std.Data.Ranges.Basic
33
import Std.Data.Ranges.Slice
4+
open Std.Iterators
45

56
-- Have: `LE`, `LT`, `HAdd`
67
-- Perhaps need: `Succ`
@@ -68,7 +69,6 @@ instance [LE α] [DecidableLE α] (r : PRange ⟨.closed, .closed⟩ α) : Decid
6869

6970

7071
section Iterator
71-
open Std.Iterators
7272

7373
def Range.succIteratorInternal [Succ? α] (init : α) (stepSize : Nat) (Predicate : α → Bool) :=
7474
Iter.repeatUntilNone (init := init) (Succ?.succAtIdx? stepSize) |>.takeWhile Predicate
@@ -106,25 +106,29 @@ instance [Monad m] [MonadLiftT Id m] [Succ? α] (stepSize : Nat) (Predicate : α
106106
unfold Range.SuccIterator
107107
infer_instance
108108

109+
-- TODO: Should we hide the ≤ or < predicates behind some identifier to avoid accidental rewriting?
109110
instance [Succ? α] [LE α] [DecidableLE α] : RangeIter ⟨.closed, .closed⟩ α :=
110111
.of fun r => Range.succIterator r.lower 1 (fun a => a ≤ r.upper) (by omega)
111112

112113
instance [Succ? α] [LT α] [DecidableLT α] : RangeIter ⟨.closed, .open⟩ α :=
113114
.of fun r => Range.succIterator r.lower 1 (fun a => a < r.upper) (by omega)
114115

115-
instance [Succ? α] [LE α] [DecidableLE α] : RangeIter ⟨.closed, .closed⟩ α :=
116-
.of fun r => Range.succIterator (Succ?.succ? 1 r.lower) 1 (fun a => a ≤ r.upper) (by omega)
116+
instance [Succ? α] [LT α] [DecidableLT α] : RangeIter ⟨.closed, .none⟩ α :=
117+
.of fun r => Range.succIterator r.lower 1 (fun _ => True) (by omega)
117118

118-
end Iterator
119+
instance [Succ? α] [LE α] [DecidableLE α] : RangeIter ⟨.open, .closed⟩ α :=
120+
.of fun r => Range.succIterator r.lower 1 (fun a => a ≤ r.upper) (by omega) |>.drop 1
119121

122+
instance [Succ? α] [LT α] [DecidableLT α] : RangeIter ⟨.open, .open⟩ α :=
123+
.of fun r => Range.succIterator r.lower 1 (fun a => a < r.upper) (by omega) |>.drop 1
120124

121-
section Examples
125+
instance [Succ? α] [LT α] [DecidableLT α] : RangeIter ⟨.open, .none⟩ α :=
126+
.of fun r => Range.succIterator r.lower 1 (fun _ => True) (by omega) |>.drop 1
122127

123-
instance : Succ? Nat where
124-
succ? n := some (n + 1)
128+
-- TODO: iterators for ranges that are unbounded downwards
125129

126-
#eval "b" ∈ ("a",,"c")
130+
end Iterator
127131

128-
#eval (1,,<4).iter.allowNontermination.toList
132+
section Examples
129133

130134
end Examples

‎src/Std/Data/Ranges/Nat.lean‎

Lines changed: 18 additions & 80 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
prelude
22
import Std.Data.Ranges.Basic
3+
import Std.Data.Ranges.General
34
import Std.Data.Ranges.Slice
45
import Std.Data.Iterators.Combinators.Monadic.Lineage
56

@@ -23,100 +24,37 @@ instance : RangeSize ⟨.none, .closed⟩ Nat where
2324
instance : RangeSize ⟨.none, .open⟩ Nat where
2425
size r := r.upper + 1
2526

26-
instance : RangeIter ⟨.closed, .closed⟩ Nat :=
27-
.of fun r => Iter.repeat (init := r.lower) (· + 1) |>.take r.size
27+
instance : Succ? Nat where
28+
succ? n := some (n + 1)
2829

29-
instance : RangeIter ⟨.closed, .open⟩ Nat :=
30-
.of fun r => Iter.repeat (init := r.lower) (· + 1) |>.take r.size
30+
instance (stepSize : Nat) (h) :
31+
Finite (Range.SuccIterator (α := Nat) stepSize (· ≤ n) h) Id := by
32+
unfold Range.SuccIterator
33+
sorry
3134

32-
instance : RangeIter ⟨.closed, .none⟩ Nat :=
33-
.of fun r => Iter.repeat (init := r.lower) (· + 1)
35+
instance (stepSize : Nat) (h) :
36+
Finite (Range.SuccIterator (α := Nat) stepSize (· < n) h) Id := by
37+
unfold Range.SuccIterator
38+
sorry
3439

35-
instance : RangeIter ⟨.open, .closed⟩ Nat :=
36-
.of fun r => Iter.repeat (init := r.lower) (· + 1) |>.take r.size
40+
#eval "b" ∈ ("a",,"c")
3741

38-
instance : RangeIter ⟨.open, .open⟩ Nat :=
39-
.of fun r => Iter.repeat (init := r.lower + 1) (· + 1) |>.take r.size
42+
#eval "a"
4043

41-
instance : RangeIter ⟨.open, .none⟩ Nat :=
42-
.of fun r => Iter.repeat (init := r.lower + 1) (· + 1)
43-
44-
instance : RangeIter ⟨.none, .closed⟩ Nat :=
45-
.of fun r => Iter.repeat (init := 0) (· + 1) |>.take r.size
46-
47-
instance : RangeIter ⟨.none, .open⟩ Nat :=
48-
.of fun r => Iter.repeat (init := 0) (· + 1) |>.take r.size
49-
50-
instance : RangeIter ⟨.none, .none⟩ Nat :=
51-
.of fun r => Iter.repeat (init := 0) (· + 1)
52-
53-
instance : Membership Nat (PRange shape Nat) where
54-
mem r n := match shape with
55-
| ⟨sl, su, ss⟩ => (match sl with
56-
| .open => r.lower < n
57-
| .closed => r.lower ≤ n
58-
| .none => True) ∧
59-
(match su with
60-
| .open => n < r.upper
61-
| .closed => n ≤ r.upper
62-
| .none => True)
63-
64-
instance {n : Nat} {r : PRange shape Nat} : Decidable (n ∈ r) := by
65-
simp only [Membership.mem]
66-
split <;> split <;> infer_instance
44+
#eval! (1<,,<4).iter.toList
6745

6846
#eval (2<,,<5).size
6947

70-
#eval (2,,→0→,,10).iter.toList
71-
72-
#eval (,,<5).iter.toList
48+
-- #eval (,,<5).iter.toList
7349

7450
#eval 1 ∈ (1,,5)
7551

76-
#eval 1 ∈ (1,,→2→,,5)
52+
-- TODO:
53+
instance [Pure m] : MonadLiftT Id m where
54+
monadLift := pure
7755

7856
def f : IO Unit := do
7957
for x in ((2 : Nat),,8) do -- ugly: For some reason, we need a type hint here
8058
IO.println x
8159

8260
#synth ForIn IO (type_of% (2,,8)) _ -- Note that we don't need the type hint this time
83-
84-
-- Slices
85-
86-
87-
instance : Sliceable shape (Array α) Nat α where
88-
89-
instance [i : SliceIter ⟨sl, su, .custom Nat⟩ (Array α) Nat] : SliceIter ⟨sl, su, .default⟩ (Array α) Nat where
90-
State s := i.State ⟨s.collection, ⟨s.range.lower, s.range.upper, 1⟩⟩
91-
iter s := i.iter ⟨s.collection, ⟨s.range.lower, s.range.upper, 1⟩⟩
92-
93-
instance : SliceIter ⟨.none, .none, .default⟩ (Array α) Nat :=
94-
.of (·.collection.iter)
95-
96-
instance : SliceIter ⟨.closed, .none, .default⟩ (Array α) Nat :=
97-
.of (fun s => s.collection.iter.drop s.range.lower)
98-
99-
instance : SliceIter ⟨.open, .none, .default⟩ (Array α) Nat :=
100-
.of (fun s => s.collection.iter.drop (s.range.lower + 1))
101-
102-
instance : SliceIter ⟨.none, .closed, .default⟩ (Array α) Nat :=
103-
.of (fun s => s.collection.iter.take (s.range.upper + 1))
104-
105-
instance : SliceIter ⟨.closed, .closed, .default⟩ (Array α) Nat :=
106-
.of (fun s => s.collection.iter.take (s.range.upper + 1) |>.drop s.range.lower)
107-
108-
instance : SliceIter ⟨.open, .closed, .default⟩ (Array α) Nat :=
109-
.of (fun s => s.collection.iter.take (s.range.upper + 1) |>.drop (s.range.lower + 1))
110-
111-
instance : SliceIter ⟨.none, .open, .default⟩ (Array α) Nat :=
112-
.of (fun s => s.collection.iter.take s.range.upper)
113-
114-
instance : SliceIter ⟨.closed, .open, .default⟩ (Array α) Nat :=
115-
.of (fun s => s.collection.iter.take s.range.upper |>.drop s.range.lower)
116-
117-
instance : SliceIter ⟨.open, .open, .default⟩ (Array α) Nat :=
118-
.of (fun s => s.collection.iter.take s.range.upper |>.drop (s.range.lower + 1))
119-
120-
def testArray := (0,,<10).iter.toArray
121-
122-
#eval testArray[[2<,,]].iter.toList

0 commit comments

Comments
 (0)