chore: rename Stream to Std.Stream

Author: TwoFX

src/Init/Data/Stream.lean

@@ -13,6 +13,8 @@ import Init.Data.Slice.Array.Basic
 
 public section
 
+namespace Std
+
 /-!
 Remark: we considered using the following alternative design
 ```
@@ -112,3 +114,19 @@ instance : Stream Std.Range Nat where
       some (r.start, { r with start := r.start + r.step })
     else
       none
+
+end Std
+
+@[deprecated Std.Stream (since := "2025-10-01")]
+abbrev Stream := Std.Stream
+
+-- Not deprecated to avoid bootstrapping annoyances
+abbrev Stream.next? {stream : Type u} {value : outParam (Type v)} [self : Std.Stream stream value] :
+    stream → Option (value × stream) := Std.Stream.next?
+
+@[deprecated Std.ToStream (since := "2025-10-01")]
+abbrev ToStream := Std.ToStream
+
+-- Not deprecated to avoid bootstrapping annoyances
+abbrev ToStream.toStream {collection : Type u} {stream : outParam (Type u)}
+  [self : Std.ToStream collection stream] : collection → stream := Std.ToStream.toStream

src/Init/Data/String/Stream.lean

@@ -9,7 +9,7 @@ prelude
 public import Init.Data.String.Basic
 public import Init.Data.Stream
 
-public instance : Stream Substring Char where
+public instance : Std.Stream Substring Char where
   next? s :=
     if s.startPos < s.stopPos then
       some (s.str.get s.startPos, { s with startPos := s.str.next s.startPos })

src/Init/Data/Vector/Basic.lean

@@ -8,7 +8,6 @@ module
 
 prelude
 public meta import Init.Coe
--- public import Init.Data.Stream
 public import Init.Data.Array.Lemmas
 public import Init.Data.Array.MapIdx
 public import Init.Data.Array.InsertIdx

src/Init/Data/Vector/Stream.lean

@@ -14,7 +14,7 @@ namespace Vector
 /-! ### ToStream instance -/
 
 @[no_expose]
-public instance : ToStream (Vector α n) (Subarray α) where
+public instance : Std.ToStream (Vector α n) (Subarray α) where
   toStream xs := xs.toArray[*...*]
 
 end Vector

src/Lean/Elab/Do.lean

@@ -1540,9 +1540,9 @@ mutual
         ```
         into
         ```
-        let s := toStream ys
+        let s := Std.toStream ys
         for x in xs do
-          match Stream.next? s with
+          match Std.Stream.next? s with
           | none => break
           | some (y, s') =>
             s := s'
@@ -1560,11 +1560,11 @@ mutual
       withFreshMacroScope do
         /- Recall that `@` (explicit) disables `coeAtOutParam`.
            We used `@` at `Stream` functions to make sure `resultIsOutParamSupport` is not used. -/
-        let toStreamApp ← withRef ys `(@toStream _ _ _ $ys)
+        let toStreamApp ← withRef ys `(@Std.toStream _ _ _ $ys)
         let auxDo ←
           `(do let mut s := $toStreamApp:term
                for $doForDecls:doForDecl,* do
-                 match @Stream.next? _ _ _ s with
+                 match @Std.Stream.next? _ _ _ s with
                  | none => break
                  | some ($y, s') =>
                    s := s'

src/Lean/Parser/Do.lean

@@ -157,7 +157,7 @@ def doForDecl := leading_parser
 `break` and `continue` are supported inside `for` loops.
 `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
 until at least one of them is exhausted.
-The types of `e2` etc. must implement the `ToStream` typeclass.
+The types of `e2` etc. must implement the `Std.ToStream` typeclass.
 -/
 @[builtin_doElem_parser] def doFor    := leading_parser
   "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq

tests/bench/workspaceSymbolsNewRanges.lean

@@ -478,7 +478,7 @@ def consts := ["_private.«external:file:///Users/paul/code/lean4/tests/bench/wo
  "Std.Slice.casesOn",
  "_private.Init.Data.Vector.Lemmas.0.Vector.forall_mem_append._simp_1_2",
  "Std.PRange.forIn'_eq_match.match_3",
- "ToStream.casesOn",
+ "Std.ToStream.casesOn",
  "Lean.Level.PP.Result.leaf.inj",
  "Lean.PrettyPrinter.Parenthesizer.Context._sizeOf_1",
  "Std.Format.tag",

tests/lean/forErrors.lean.expected.out

@@ -1,4 +1,4 @@
 forErrors.lean:3:29-3:30: error: failed to synthesize
-  ToStream α ?m
+  Std.ToStream α ?m
 
 Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/run/1017.lean

@@ -1,6 +1,6 @@
-namespace Stream
+namespace Std.Stream
 
-variable [Stream ρ τ] (s : ρ)
+variable [Std.Stream ρ τ] (s : ρ)
 
 def take (s : ρ) : Nat → List τ × ρ
 | 0 => ([], s)
@@ -52,4 +52,4 @@ def mwe [Stream ρ τ] (acc : α) : {l : ρ // isFinite l} → α
       mwe acc ⟨xs, by sorry⟩
   termination_by l => l
 
-end Stream
+end Std.Stream

tests/lean/run/streamEqIssue.lean

@@ -1,9 +1,9 @@
-@[simp] def Stream.hasLength [Stream stream value] (n : Nat) (s : stream) : Bool :=
+@[simp] def Std.Stream.hasLength [Stream stream value] (n : Nat) (s : stream) : Bool :=
   match n, Stream.next? s with
   | 0, none => true
   | n + 1, some (_, s') => hasLength n s'
   | _, _ => false
 
-#check @Stream.hasLength.eq_1
-#check @Stream.hasLength.eq_2
-#check @Stream.hasLength.eq_3
+#check @Std.Stream.hasLength.eq_1
+#check @Std.Stream.hasLength.eq_2
+#check @Std.Stream.hasLength.eq_3