feat: update

Author: Serhii Khoma

Glob/Data/NonEmptyList.lean

@@ -1,11 +1,11 @@
+import Batteries.Data.List.Basic
+import Init.System.IO
 import Lean
 import Lean.Data.RBMap
-import Std.Data.HashSet
 import Lean.Data.RBTree
-import Init.System.IO
 import Lean.Elab.Term
 import Lean.Parser.Term
-import Batteries.Data.List.Basic
+import Std.Data.HashSet
 
 structure NonEmptyList (α : Type u) where
   toList : List α
@@ -19,7 +19,7 @@ instance [BEq α] : BEq (NonEmptyList α) where
   beq a b := a.toList == b.toList
 
 instance [ToString α] : ToString (NonEmptyList α) where
-  toString a := toString a.toList
+  toString a := "nel!" ++ toString a.toList
 
 instance [Inhabited α] : Inhabited (NonEmptyList α) where
   default := ⟨[default], List.cons_ne_nil default []⟩

Glob/Utils/Other.lean

@@ -16,8 +16,8 @@ open System (FilePath)
 private abbrev LNES := List NonEmptyString
 private abbrev NELNES := NonEmptyList NonEmptyString
 
--- \f<< \-> \f>>
-@[inline] def FilePath.Lax.«→LNES» (p : FilePath) : LNES := ToNE.FilterMap.«LS->LNES» p.components
-@[inline] def FilePath.Lax.«→NELNES»  (p : FilePath) : Option NELNES := ToNE.FilterMap.«LS->NELNES» p.components
-@[inline] def FilePath.Strict.«→LNES» (p : FilePath) : Option LNES := ToNE.Traverse.«LS->LNES» p.components
-@[inline] def FilePath.Strict.«→NELNES» (p : FilePath) : Option NELNES := ToNE.Traverse.«LS->NELNES» p.components
+-- \f<< -> \f>>
+@[inline] def FilePath.Lax.«->LNES» (p : FilePath) : LNES := ToNE.FilterMap.«LS->LNES» p.components
+@[inline] def FilePath.Lax.«->NELNES»  (p : FilePath) : Option NELNES := ToNE.FilterMap.«LS->NELNES» p.components
+@[inline] def FilePath.Strict.«->LNES» (p : FilePath) : Option LNES := ToNE.Traverse.«LS->LNES» p.components
+@[inline] def FilePath.Strict.«->NELNES» (p : FilePath) : Option NELNES := ToNE.Traverse.«LS->NELNES» p.components

Test/GlobSpec.lean

@@ -1,4 +1,5 @@
 import Glob
+import Glob.Data.NonEmptyList
 import Glob.Data.Tree
 import Glob.WF.IO
 import Glob.WF.Tree
@@ -23,26 +24,26 @@ def glob (pattern : PatternValidated) (tree : Tree) : Option Tree := none
 def globMany (patterns : NonEmptyList PatternValidated) (tree : Tree) : Option Tree := none
 
 -- Helper to assert glob results match expected Tree
-def assertGlobResult (name : String) (pattern : String) (tree : Tree) (expected : Option Tree) : IO Unit := do
+def assertGlobResult (pattern : String) (tree : Tree) (expected : Option Tree) : IO Unit := do
   let patternValidated ← PatternValidated.patternStrictIO! pattern
   let actual := glob patternValidated tree
   unless actual == expected do
-    IO.println s!"❌ {name} failed:"
+    IO.println s!"❌ {pattern} failed:"
     IO.println s!"  Pattern: {pattern}"
     IO.println s!"  Expected: {reprStr expected}"
     IO.println s!"  Actual: {reprStr actual}"
-    throw <| IO.Error.userError s!"Assertion failed: {name}"
+    throw <| IO.Error.userError s!"Assertion failed: {pattern}"
 
 -- Helper to assert globMany results match expected Tree
-def assertGlobManyResult (name : String) (patternsNel : NonEmptyList String) (tree : Tree) (expected : Option Tree) : IO Unit := do
+def assertGlobManyResult (patternsNel : NonEmptyList String) (tree : Tree) (expected : Option Tree) : IO Unit := do
   let patternsNel' ← patternsNel.mapM PatternValidated.patternStrictIO!
   let actual := globMany patternsNel' tree
   unless actual == expected do
-    IO.println s!"❌ {name} failed:"
+    IO.println s!"❌ {toString patternsNel} failed:"
     IO.println s!"  Patterns: {patternsNel}"
     IO.println s!"  Expected: {reprStr expected}"
     IO.println s!"  Actual: {reprStr actual}"
-    throw <| IO.Error.userError s!"Assertion failed: {name}"
+    throw <| IO.Error.userError s!"Assertion failed: {toString patternsNel}"
 
 -- Test data
 def globTestExample1 := tree! "Glob" { "A" { "X" { } }, "B" { "Y" { } } }
@@ -58,198 +59,185 @@ def globTestExample2 := tree! "Root" {
 def testBasicGlob : IO Unit := do
   IO.println "Testing basic glob patterns..."
 
-  assertGlobResult "Glob root match" "Glob"
+  assertGlobResult "Glob"
     (tree! "Glob" { "A" { } })
     (some (tree! "Glob" {}))
 
-  assertGlobResult "Glob/A match" "Glob/A"
+  assertGlobResult "Glob/A"
     (tree! "Glob" { "A" { } })
     (some (tree! "Glob" { "A" { } }))
 
-  assertGlobResult "Glob/A match without children" "Glob/A"
+  assertGlobResult "Glob/A"
     (tree! "Glob" { "A" })
     (some (tree! "Glob" { "A" }))
 
-  assertGlobResult "Glob/B no match" "Glob/B"
+  assertGlobResult "Glob/B"
     (tree! "Glob" { "A" { } })
     none
 
 -- Wildcard tests
 def testWildcardGlob : IO Unit := do
   IO.println "Testing wildcard patterns..."
 
-  assertGlobResult "Double star match" "**"
+  assertGlobResult "**"
     globTestExample1
     (some (tree! "Glob" { "A" { "X" {} }, "B" { "Y" {} } }))
 
-  assertGlobResult "**/X recursive match" "**/X"
+  assertGlobResult "**/X"
     globTestExample1
     (some (tree! "Glob" { "A" { "X" {} } }))
 
-  assertGlobResult "**/Y recursive match" "**/Y"
+  assertGlobResult "**/Y"
     globTestExample1
     (some (tree! "Glob" { "B" { "Y" {} } }))
 
-  assertGlobResult "**/Z no match" "**/Z"
+  assertGlobResult "**/Z"
     globTestExample1
     none
 
-  assertGlobResult "Glob/* single level" "Glob/*"
+  assertGlobResult "Glob/*"
     globTestExample1
     (some (tree! "Glob" { "A" {}, "B" {} }))
 
-  assertGlobResult "Glob/** recursive" "Glob/**"
+  assertGlobResult "Glob/**"
     globTestExample1
     (some globTestExample1)
 
 -- Specific path tests
 def testSpecificPaths : IO Unit := do
   IO.println "Testing specific path patterns..."
 
-  assertGlobResult "Glob/A/* match" "Glob/A/*"
+  assertGlobResult "Glob/A/*"
     globTestExample1
     (some (tree! "Glob" { "A" { "X" {} } }))
 
-  assertGlobResult "Glob/A/** recursive" "Glob/A/**"
+  assertGlobResult "Glob/A/**"
     globTestExample1
     (some (tree! "Glob" { "A" { "X" { } } }))
 
-  assertGlobResult "Glob/A/X exact match" "Glob/A/X"
+  assertGlobResult "Glob/A/X"
     globTestExample1
     (some (tree! "Glob" { "A" { "X" {} } }))
 
-  assertGlobResult "Glob/B/** recursive" "Glob/B/**"
+  assertGlobResult "Glob/B/**"
     globTestExample1
     (some (tree! "Glob" { "B" { "Y" {} } }))
 
-  assertGlobResult "Glob/C no match" "Glob/C"
+  assertGlobResult "Glob/C"
     globTestExample1
     none
 
 -- Simple tree tests
 def testSimpleTrees : IO Unit := do
   IO.println "Testing simple tree patterns..."
 
-  assertGlobResult "Single star match" "*"
+  assertGlobResult "*"
     (tree! "foo" {})
     (some (tree! "foo" {}))
 
-  assertGlobResult "Double star on simple tree" "**"
+  assertGlobResult "**"
     (tree! "root" {})
     (some (tree! "root" {}))
 
 -- Complex tree tests
 def testComplexTree : IO Unit := do
   IO.println "Testing complex tree patterns..."
 
-  assertGlobResult "**/baz.txt deep search" "**/baz.txt"
+  assertGlobResult "**/baz.txt"
     globTestExample2
     (some (tree! "Root" { "foo" { "bar" { "baz.txt"  } } }))
 
-  assertGlobResult "**/delta.txt deep search" "**/delta.txt"
+  assertGlobResult "**/delta.txt"
     globTestExample2
     (some (tree! "Root" { "alpha" { "beta" { "gamma" { "delta.txt"  } } } }))
 
-  assertGlobResult "**/file.txt search" "**/file.txt"
+  assertGlobResult "**/file.txt"
     globTestExample2
     (some (tree! "Root" { "foo" { "file.txt"  } }))
 
-  assertGlobResult "**/qux.md search" "**/qux.md"
+  assertGlobResult "**/qux.md"
     globTestExample2
     (some (tree! "Root" { "foo" { "bar" { "qux.md" } } }))
 
-  assertGlobResult "Root exact match" "Root"
+  assertGlobResult "Root"
     globTestExample2
     (some (tree! "Root" {}))
 
-  assertGlobResult "Root/* first level" "Root/*"
+  assertGlobResult "Root/*"
     globTestExample2
     (some (Tree.dir "Root" [Tree.dir "foo" [], Tree.dir "foo2" [], Tree.dir "alpha" [], Tree.dir "zeta" []]))
 
-  assertGlobResult "Root/** full tree" "Root/**"
+  assertGlobResult "Root/**"
     globTestExample2
     (some globTestExample2)
 
 -- Multi-level pattern tests
 def testMultiLevelPatterns : IO Unit := do
   IO.println "Testing multi-level patterns..."
 
-  assertGlobResult "Root/**/bar/* nested wildcard" "Root/**/bar/*"
+  assertGlobResult "Root/**/bar/*"
     globTestExample2
     (some (tree! "Root" { "foo" { "bar" { "baz.txt", "qux.md" } }, "foo2" { "bar" { "baz2.txt", "qux2.md" } } }))
 
-  assertGlobResult "Root/**/delta.txt deep nested" "Root/**/delta.txt"
+  assertGlobResult "Root/**/delta.txt"
     globTestExample2
     (some (tree! "Root" { "alpha" { "beta" { "gamma" { "delta.txt"  } } } }))
 
-  assertGlobResult "Root/**/file.txt nested search" "Root/**/file.txt"
+  assertGlobResult "Root/**/file.txt"
     globTestExample2
     (some (tree! "Root" { "foo" { "file.txt"  } }))
 
-  assertGlobResult "Root/*/*/*/delta.txt exact depth" "Root/*/*/*/delta.txt"
+  assertGlobResult "Root/*/*/*/delta.txt"
     globTestExample2
     (some (tree! "Root" { "alpha" { "beta" { "gamma" { "delta.txt"  } } } }))
 
 -- Specific path combinations
 def testSpecificCombinations : IO Unit := do
   IO.println "Testing specific path combinations..."
 
-  assertGlobResult "Root/foo/**/baz.txt" "Root/foo/**/baz.txt"
+  assertGlobResult "Root/foo/**/baz.txt"
     globTestExample2
     (some (tree! "Root" { "foo" { "bar" { "baz.txt"  } } }))
 
-  assertGlobResult "Root/foo/*/baz.txt" "Root/foo/*/baz.txt"
+  assertGlobResult "Root/foo/*/baz.txt"
     globTestExample2
     (some (tree! "Root" { "foo" { "bar" { "baz.txt"  } } }))
 
-  assertGlobResult "Root/foo/*/doesntexist.txt no match" "Root/foo/*/doesntexist.txt"
+  assertGlobResult "Root/foo/*/doesntexist.txt"
     globTestExample2
     none
 
-  assertGlobResult "Root/foo/bar/baz.txt exact" "Root/foo/bar/baz.txt"
+  assertGlobResult "Root/foo/bar/baz.txt"
     globTestExample2
     (some (tree! "Root" { "foo" { "bar" { "baz.txt"  } } }))
 
-  assertGlobResult "Root/foo/bar/baz.txt/extra invalid" "Root/foo/bar/baz.txt/extra"
+  assertGlobResult "Root/foo/bar/baz.txt/extra"
     globTestExample2
     none
 
-  assertGlobResult "Root/foo/bar/notfound.txt no match" "Root/foo/bar/notfound.txt"
+  assertGlobResult "Root/foo/bar/notfound.txt"
     globTestExample2
     none
 
 -- GlobMany tests using assertGlobManyResult
 def testGlobMany : IO Unit := do
   IO.println "Testing globMany patterns..."
 
-  assertGlobManyResult "GlobMany test 1" nel!["Glob/A", "Glob/B"]
-    (tree! "Glob" { "A" {}, "B" {} })
-    (some (tree! "Glob" { "A" {}, "B" {} }))
-
-  assertGlobManyResult "GlobMany test 2" nel!["Glob/A", "Glob/C"]
-    (tree! "Glob" { "A" {}, "B" {} })
-    (some (tree! "Glob" { "A" {} }))
-
-  assertGlobManyResult "GlobMany test 3" nel!["**/X", "**/Y"]
-    globTestExample1
-    (some (tree! "Glob" { "A" { "X" {} }, "B" { "Y" {} } }))
-
-  assertGlobManyResult "GlobMany test 4" nel!["**/baz.txt", "**/delta.txt"]
+  assertGlobManyResult nel!["Glob/A", "Glob/B"] (tree! "Glob" { "A" {}, "B" {} }) (some (tree! "Glob" { "A" {}, "B" {} }))
+  assertGlobManyResult nel!["Glob/A", "Glob/C"] (tree! "Glob" { "A" {}, "B" {} }) (some (tree! "Glob" { "A" {} }))
+  assertGlobManyResult nel!["**/X", "**/Y"] globTestExample1 (some (tree! "Glob" { "A" { "X" {} }, "B" { "Y" {} } }))
+  assertGlobManyResult nel!["**/baz.txt", "**/delta.txt"]
     globTestExample2
     (some (tree! "Root" {
       "foo"   { "bar" { "baz.txt" } },
       "alpha" { "beta" { "gamma" { "delta.txt" } } }
     }))
 
-  assertGlobManyResult "GlobMany test 5" nel!["**/file.txt", "**/qux.md"]
-    globTestExample2
-    (some (tree! "Root" { "foo" { "file.txt", "bar" { "qux.md" } } }))
+  assertGlobManyResult nel!["**/file.txt", "**/qux.md"] globTestExample2 (some (tree! "Root" { "foo" { "file.txt", "bar" { "qux.md" } } }))
 
-  assertGlobManyResult "GlobMany test 6" nel!["**/doesntexist.txt", "**/missing.txt"]
-    globTestExample2
-    none
+  assertGlobManyResult nel!["**/doesntexist.txt", "**/missing.txt"] globTestExample2 none
 
-  assertGlobManyResult "GlobMany test 7" nel!["Root/foo/bar/baz.txt", "Root/foo2/bar/qux2.md"]
+  assertGlobManyResult nel!["Root/foo/bar/baz.txt", "Root/foo2/bar/qux2.md"]
     globTestExample2
     (some (tree! "Root" {
       "foo"  { "bar" { "baz.txt" } },
@@ -275,4 +263,4 @@ def runGlobTests : IO Unit := do
     IO.println s!"❌ Glob tests failed: {e}"
     throw e
 
-end
+end GlobSpec

Test/Main.lean

@@ -23,6 +23,8 @@ open System (FilePath)
 `mkTestGlob pat t expected` returns a pair
 ```lean
   (testName, IO Unit)
+```
+
 where testName is derived from pat, and the IO Unit runs runGlobTest.
 
 pat is the pattern string (the first argument to #testGlob)
@@ -31,8 +33,9 @@ t is the Tree to search in
 
 expected is the Option Tree you expect back
 -/
+
 -- def main : IO Unit := return
 def main : IO Unit := do
   GlobSpec.runGlobTests
   -- runTests #[
-    -- ("FindRecursive", fun (currentTmpDir : FilePath) => do -- TODO: this is a limitation of glob-posix, no support of recursion
+  -- ("FindRecursive", fun (currentTmpDir : FilePath) => do -- TODO: this is a limitation of glob-posix, no support of recursion