Add testing code for Lean lazy infinite lists

Changes

1 changed files (+324/-0)

• lazy.lean (new)
  • @@ -0,0 +1,324 @@
    + -- Want: + -- def ints := LazyList.cons 1 <| ints.map (· + 1) + -- Problem: This is recursive, bad! + -- Idea: use dependent types to encode promise that recursion won't exceed certain depth? Bake that into cons + -- Problem: memoization? + -- Like let's say I take 10 then take 20, the initial elements will have different types + -- Well let's try implementing this first + + -- inductive Vect (α : Type u) : Nat → Type u where + -- | nil : Vect α 0 + -- | cons : α → Vect α n → Vect α (n + 1) + + -- def Vect.map (f : α → β) : Vect α n → Vect β n + -- | nil => nil + -- | cons x xs => cons (f x) <| xs.map f + + -- -- def Vect.map (f : α → β) : Vect α (n + 1) → Vect β n := + -- -- match n with + -- -- | 0 => λ _ => nil + -- -- | _ + 1 => λ v => match v with + -- -- | cons x xs => cons (f x) <| xs.map f + + -- def a := Vect.cons 1 (Vect.cons 2 Vect.nil) + + -- #eval a.map (· + 1) + + -- def ints (n : Nat) : Vect Nat n + -- | 0 => Vect.nil + -- | n + 1 => Vect.cons 1 <| (ints n).map (· + 1) + + -- -- #eval ints 10 + + + + + + inductive LazyList (α : Type u) where + | nil + | cons : α → Thunk (LazyList α) → LazyList α + + def LazyList.take : Nat → LazyList α → List α + | 0, _ => .nil + | _, .nil => .nil + | n + 1, .cons x xs => .cons x <| xs.get.take n + + def LazyList.map (f: α → β) : LazyList α → LazyList β + | .nil => .nil + | .cons x xs => .cons (f x) <| xs.get.map f + + def LazyList.zipWith (f: α → β → γ) : LazyList α → LazyList β → LazyList γ + | .nil, _ => .nil + | _, .nil => .nil + | .cons x xs, .cons y ys => .cons (f x y) <| zipWith f xs.get ys.get + + unsafe def ints := LazyList.cons 1.0 <| ints.map (· + 1) + + #eval ints.take 10 + + -- Doesn't work? + -- unsafe def integrate s (c : Float) := LazyList.cons c <| LazyList.zipWith (· / ·) s ints + + notation s "integrate" c => LazyList.cons c <| LazyList.zipWith (· / ·) s ints + + unsafe def pows := LazyList.cons 1.0 <| LazyList.zipWith (· + ·) pows pows + + #eval pows.take 10 + + unsafe def expSeries := expSeries integrate 1.0 + + #eval expSeries.take 10 + + def evalAt n (s : LazyList Float) x := (s.take n).foldr (λ a acc => a + acc * x) 0 + + mutual + unsafe def sine := cosine integrate 0.0 + unsafe def cosine := (sine integrate -1.0).map (-·) + end + + #eval sine.take 10 + + #eval evalAt 100 sine 2.0 + #eval 2.0.sin + + -- inductive LazyList (α : Type u) where + -- | nil + -- | cons : α → Thunk (LazyList α) → LazyList α + -- | delayed : Thunk (LazyList α) → LazyList α + + -- def LazyList.take : Nat → LazyList α → List α + -- | 0, _ => .nil + -- | _, .nil => .nil + -- | n + 1, .cons x xs => .cons x <| xs.get.take n + -- | n + 1, .delayed xs => xs.get.take n + + -- def LazyList.map (f: α → β) : LazyList α → LazyList β + -- | .nil => .nil + -- | .cons x xs => .cons (f x) <| xs.get.map f + -- | .delayed xs => xs.get.map f + + -- def LazyList.zipWith (f: α → β → γ) : LazyList α → LazyList β → LazyList γ + -- | .nil, _ => .nil + -- | _, .nil => .nil + -- | .cons x xs, .cons y ys => .cons (f x y) <| zipWith f xs.get ys.get + -- | .delayed xs, y => zipWith f xs.get y + -- | x, .delayed ys => zipWith f x ys.get + + -- unsafe def ints := LazyList.cons 1 <| ints.map (· + 1) + + -- #eval ints.take 10 + + -- def hi := LazyList.delayed LazyList + + -- unsafe def integrate s c := LazyList.cons c <| LazyList.delayed <| LazyList.zipWith (· / ·) s ints + + -- unsafe def expSeries := integrate expSeries 1 + + -- #eval expSeries.take 10 + + -- inductive LazyList (α : Type u) where + -- | nil + -- | cons : α → LazyList α → LazyList α + -- | delayed : Thunk (LazyList α) → LazyList α + + -- unsafe def LazyList.map (f: α → β) : LazyList α → Thunk (LazyList β) + -- | nil => Thunk.pure nil + -- | cons x xs => cons (f x) <| delayed <| xs.map f + -- | delayed xs => xs.bind <| λ l => l.map f + + -- -- def LazyList.take : Nat → LazyList α → LazyList α + -- -- | 0, _ => .nil + -- -- | _, .nil => .nil + -- -- | n + 1, .cons x xs => .cons x <| .delayed <| take n xs + -- -- | n + 1, .delayed xs => .delayed <| take (n + 1) xs.get + + -- def LazyList.take : Nat → LazyList α → List α + -- | 0, _ => .nil + -- | _, .nil => .nil + -- | n + 1, .cons x xs => .cons x <| xs.take n + -- | n + 1, .delayed xs => take (n + 1) xs.get + + -- -- def LazyList.toList : LazyList α → List α + -- -- | .nil => [] + -- -- | .cons x xs => x :: xs.toList + -- -- | .delayed xs => xs.get.toList + + -- unsafe def ints := LazyList.cons 1 <| LazyList.delayed <| ints.map (· + 1) + + -- -- #eval ints.take 10 + + + + -- inductive LazyList (α : Type u) : Type u + -- /-- The empty lazy list. -/ + -- | nil : LazyList α + -- /-- Construct a lazy list from an element and a tail inside a thunk. -/ + -- | cons (hd : α) (tl : Thunk <| LazyList α) : LazyList α + + + -- namespace LazyList + + + -- instance : Inhabited (LazyList α) := + -- ⟨nil⟩ + + -- /-- The singleton lazy list. -/ + -- def singleton : α → LazyList α + -- | a => cons a <| Thunk.pure nil + + -- /-- Constructs a lazy list from a list. -/ + -- def ofList : List α → LazyList α + -- | [] => nil + -- | h :: t => cons h (ofList t) + + -- /-- Converts a lazy list to a list. + -- If the lazy list is infinite, + -- then this function does not terminate. + -- -/ + -- def toList : LazyList α → List α + -- | nil => [] + -- | cons h t => h :: toList (t.get) + + -- /-- Returns the first element of the lazy list, + -- or `default` if the lazy list is empty. + -- -/ + -- def headI [Inhabited α] : LazyList α → α + -- | nil => default + -- | cons h _ => h + + -- /-- Removes the first element of the lazy list. + -- -/ + -- def tail : LazyList α → LazyList α + -- | nil => nil + -- | cons _ t => t.get + + -- /-- Appends two lazy lists. -/ + -- def append : LazyList α → Thunk (LazyList α) → LazyList α + -- | nil, l => l.get + -- | cons h t, l => cons h (append (t.get) l) + + -- /-- Maps a function over a lazy list. -/ + -- def map (f : α → β) : LazyList α → LazyList β + -- | nil => nil + -- | cons h t => cons (f h) (map f t.get) + + -- /-- Maps a binary function over two lazy list. + -- Like `LazyList.zip`, the result is only as long as the smaller input. + -- -/ + -- def map₂ (f : α → β → δ) : LazyList α → LazyList β → LazyList δ + -- | nil, _ => nil + -- | _, nil => nil + -- | cons h₁ t₁, cons h₂ t₂ => cons (f h₁ h₂) (Thunk.pure (map₂ f t₁.get t₂.get)) + + -- /-- Zips two lazy lists. -/ + -- def zip : LazyList α → LazyList β → LazyList (α × β) := + -- map₂ Prod.mk + + -- /-- The monadic join operation for lazy lists. -/ + -- def join : LazyList (LazyList α) → LazyList α + -- | nil => nil + -- | cons h t => append h (join (t.get)) + + -- /-- The list containing the first `n` elements of a lazy list. -/ + -- def take : Nat → LazyList α → List α + -- | 0, _ => [] + -- | _, nil => [] + -- | a + 1, cons h t => h :: take a (t.get) + + -- /-- The lazy list of all elements satisfying the predicate. + -- If the lazy list is infinite and none of the elements satisfy the predicate, + -- then this function will not terminate. + -- -/ + -- def filter (p : α → Prop) [DecidablePred p] : LazyList α → LazyList α + -- | nil => nil + -- | cons h t => if p h then cons h (filter p t.get) else filter p (t.get) + + -- /-- The nth element of a lazy list as an option (like `List.get?`). -/ + -- def get? : LazyList α → Nat → Option α + -- | nil, _ => none + -- | cons a _, 0 => some a + -- | cons _ l, n + 1 => get? (l.get) n + + -- /-- The infinite lazy list `[x, f x, f (f x), ...]` of iterates of a function. + -- This definition is partial because it creates an infinite list. + -- -/ + -- partial def iterates (f : α → α) : α → LazyList α + -- | x => cons x (iterates f (f x)) + + -- /-- The infinite lazy list `[i, i+1, i+2, ...]` -/ + -- partial def iota (i : Nat) : LazyList Nat := + -- iterates Nat.succ i + + -- end LazyList + + -- unsafe def ints := LazyList.cons 1 (ints.map λ x => x + 1) + + -- #eval ints.take 13 + + -- unsafe def integrate f c := LazyList.cons c <| LazyList.map₂ (λ a b => a / b) f ints + + -- unsafe def expSeries := integrate expSeries 1 + + -- -- #eval expSeries.take 13 + + + + -- structure FibStream : Type where + -- x₁ : ℕ + -- x₂ : ℕ + -- deriving Repr + + -- namespace FibStream + -- def next? (s : FibStream) : Option (ℕ × FibStream) := + -- match s with + -- | ⟨x₁, x₂⟩ => + -- let x₃ := x₁ + x₂ + -- some (x₃, ⟨x₂, x₃⟩) + + -- instance : Stream FibStream ℕ where + -- next? := next? + + -- def init : FibStream := ⟨0, 1⟩ + + -- end FibStream + + -- namespace Stream + -- variable {Stream_α : Type} {α : Type} [Stream Stream_α α] + + -- def take (n : Nat) (s : Stream_α) : List α := + -- match n with + -- | 0 => [] + -- | n+1 => + -- let next? := Stream.next? s + -- match next? with + -- | none => [] + -- | some (next, s') => next :: take n s' + + -- structure Filter (Stream_α : Type) [Stream Stream_α α] where + -- stream : Stream_α + -- filter_by : α → Bool + + + -- partial def Filter.next? (s : Filter Stream_α) : Option (α × Filter Stream_α) := + -- let next? := Stream.next? s.stream + -- match next? with + -- | none => none + -- | some (next, s') => + -- let next_filtered : Filter Stream_α := { stream := s', filter_by := s.filter_by : Filter Stream_α } + -- if s.filter_by next then + -- some (next, next_filtered) + -- else + -- Filter.next? next_filtered + + -- def filter (p : α → Bool) (s : Stream_α) : Filter Stream_α := + -- { stream := s, filter_by := p } + + -- instance : Stream (Filter Stream_α) α where + -- next? := Filter.next? + -- end Stream + + + -- -- def natOrStringThree (b : Bool) : if b then Nat else String := + -- -- match b with + -- -- | true => (3 : Nat) + -- -- | false => "three"