Skip to content

Commit 40db458

Browse files
author
Serhii Khoma
committed
feat: tests
1 parent 5f17897 commit 40db458

File tree

15 files changed

+592
-181
lines changed

15 files changed

+592
-181
lines changed

Glob/Data/NonEmptyList.lean

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -24,9 +24,6 @@ instance [ToString α] : ToString (NonEmptyList α) where
2424
instance [Inhabited α] : Inhabited (NonEmptyList α) where
2525
default := ⟨[default], List.cons_ne_nil default []⟩
2626

27-
-- ToExpr instance for compile-time evaluation
28-
open Lean Elab Term Meta
29-
3027
namespace NonEmptyList
3128

3229
@[inline] def fromList? (l : List α) : Option (NonEmptyList α) :=
@@ -68,8 +65,14 @@ namespace NonEmptyList
6865
let allInits := nel.toList.inits.drop 1 -- drop the initial empty list
6966
fromList! (allInits.map fromList!)
7067

68+
@[inline] def mapM {α : Type u} /- {β : Type v} {m : Type v → Type w} -/ [Monad m] [Inhabited β] (f : α → m β) (as : NonEmptyList α) : m (NonEmptyList β) := do
69+
let bs ← as.toList.mapM f
70+
pure (NonEmptyList.fromList! bs)
71+
7172
end NonEmptyList
7273

74+
section
75+
7376
open Lean Macro Parser Term Elab Term
7477

7578
instance {α : Type u} [ToLevel.{u}] [ToExpr α] : ToExpr (NonEmptyList α) :=
@@ -105,6 +108,8 @@ example : NonEmptyList Nat := nel![10]
105108
#guard (nel![1, 2, 3]).tail = [2, 3] -- Should output [2, 3]
106109
#guard (nel![1, 2, 3]).length = 3 -- Should output 3
107110

111+
end
112+
108113
-- #eval (toExpr $ nel![1]) -- Should output 1
109114

110115
-- Elaborator-based version for compile-time evaluation

Glob/Data/Tree.lean

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ def Tree.toString : Tree → String
2121
def Tree.toStringMacro (t : Tree) : String := "tree! " ++ Tree.toString t
2222

2323
open Std.Format in
24-
partial def Tree.toFormat : Tree → Format
24+
def Tree.toFormat : Tree → Format
2525
| Tree.file name =>
2626
-- Just the filename in quotes, e.g. `"foo"`
2727
text "\"" ++ text name ++ text "\""
@@ -38,7 +38,6 @@ partial def Tree.toFormat : Tree → Format
3838
) ++
3939
line
4040
group (
41-
text "tree! " ++
4241
text "\"" ++ text name ++ text "\"" ++
4342
text " {" ++
4443
childrenFmt ++

Glob/NonWF/Types.lean

Lines changed: 21 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,23 @@ def PatternSegmentNonWF.fromNES (nes : NonEmptyString) : PatternSegmentNonWF :=
4747
| "*" => .oneStar
4848
| _ => .lit nes
4949

50+
/--
51+
Match a single pattern segment against a tree dir name.
52+
- `lit s` matches if `s = name`.
53+
- `oneStar` matches any single name.
54+
- `doubleStar` is handled at pattern list level, not here.
55+
-/
56+
def PatternSegmentNonWF.matchNES (seg : PatternSegmentNonWF) (name : NonEmptyString) : Bool :=
57+
match seg with
58+
| .lit s => s == name
59+
| .oneStar => true
60+
| .doubleStar => false
61+
62+
def PatternSegmentNonWF.matchS (seg : PatternSegmentNonWF) (name : String) : Bool :=
63+
match NonEmptyString.fromString? name with
64+
| none => false
65+
| some name' => PatternSegmentNonWF.matchNES seg name'
66+
5067
open Lean Meta
5168

5269
-- set_option diagnostics true
@@ -77,20 +94,16 @@ def PatternNonWF'.fromStringLax (s : String) : PatternNonWF' :=
7794
|> ToNE.FilterMap.«LS->LNES»
7895
|>.map PatternSegmentNonWF.fromNES
7996

80-
def PatternNonWF.toString (ps : PatternNonWF) : String := PatternNonWF'.toString ps.toList
81-
def PatternNonWF.fromStringStrict (s : String) : Option PatternNonWF := PatternNonWF'.fromStringStrict s >>= NonEmptyList.fromList?
82-
83-
set_option diagnostics.threshold 50
97+
def PatternNonWF.toString : PatternNonWF -> String := (PatternNonWF'.toString ·.toList)
98+
def PatternNonWF.fromStringStrict : String -> Option PatternNonWF := (PatternNonWF'.fromStringStrict · >>= NonEmptyList.fromList?)
8499

85-
elab "patternNonWFLax" pat:str : term => do
86-
let s := pat.getString
87-
return (Lean.toExpr (PatternNonWF'.fromStringLax s))
100+
elab "patternNonWFLax" pat:str : term => return Lean.toExpr (PatternNonWF'.fromStringLax pat.getString)
88101

89102
elab "patternNonWFStrict" pat:str : term => do
90103
let s := pat.getString
91104
match PatternNonWF.fromStringStrict s with
92105
| some (p : NonEmptyList PatternSegmentNonWF) => return (Lean.toExpr p)
93-
| none => throwError s!"invalid non-well-formed pattern: {s}"
106+
| none => throwError s!"invalid non-well-formed pattern: {s}"
94107

95108
#guard nel![PatternSegmentNonWF.oneStar] = nel![PatternSegmentNonWF.oneStar]
96109
#guard PatternNonWF.fromStringStrict "*" = .some nel![PatternSegmentNonWF.oneStar]

Glob/WF/Elab.lean

Lines changed: 3 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -23,15 +23,10 @@ elab "patternLax" pat:str : term => do
2323
| .error e => throwError e.toHumanReadable
2424
| .ok pat => return (Lean.toExpr pat)
2525

26-
-- (normalize:Bool = false)
2726
elab "patternStrict" pat:str : term => do
28-
let s := pat.getString
29-
match PatternNonWF'.fromStringStrict s with
30-
| .none => throwError "did some segment was empty? e.g. `foo//bar` should be `foo/bar`"
31-
| .some pat => match (PatternValidated.mk? pat) with
32-
| .error .invalidEmpty => throwError PatternValidatedError.invalidEmpty.toHumanReadable
33-
| .error .invalidWrongOrdering => throwError (s!"Probably You wanted to write {PatternNonWF'.toString $ normalizeSegments pat}\n{PatternValidatedError.invalidWrongOrdering.toHumanReadable}")
34-
| .ok pat => return (Lean.toExpr pat)
27+
match PatternValidated.patternStrict? pat.getString with
28+
| .error e => throwError e
29+
| .ok pat => return (Lean.toExpr pat)
3530

3631
#check_failure patternLax ""
3732
#guard (patternLax "**" |>.pattern) == patternNonWFLax "**"

Glob/WF/IO.lean

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
import Init.System.IO
2+
import Lean
3+
import Lean.Data.RBMap
4+
import Std.Data.HashSet
5+
import Lean.Data.RBTree
6+
import Init.System.IO
7+
import Lean.Elab.Term
8+
import Init.Meta
9+
import Lean.Parser.Term
10+
import Glob.Data.NonEmptyString
11+
import Glob.Data.NonEmptyList
12+
import Glob.Utils.NEFromTo
13+
-- import Mathlib.Data.List.Induction
14+
-- import Aesop
15+
-- import LeanCopilot
16+
import Glob.NonWF.Types
17+
import Glob.WF.Types
18+
import Glob.WF.Elab
19+
20+
open IO.FS
21+
open IO.FS (DirEntry FileType Metadata)
22+
open System (FilePath)
23+
24+
-- partial def walkDir
25+
-- (p : FilePath)
26+
-- (enter : String → Bool)
27+
-- (shouldAddFileToListOfFilepaths : String → Bool) : IO (Array FilePath) :=
28+
-- go p
29+
-- where
30+
-- go (p : FilePath) : IO (Array FilePath) := do
31+
-- if !enter p.fileName then
32+
-- return #[]
33+
--
34+
-- let entries ← p.readDir
35+
-- let results ← entries.mapM fun d => do
36+
-- let root := d.root
37+
-- let fileName := d.fileName
38+
-- let path := d.path
39+
-- let includeSelf := if shouldAddFileToListOfFilepaths fileName then #[path] else #[]
40+
--
41+
-- match (← path.metadata.toBaseIO) with
42+
-- | .ok { type := .symlink, .. } =>
43+
-- let real ← IO.FS.realPath path
44+
-- if (← real.isDir) then
45+
-- -- don't call enter on symlink again
46+
-- if enter p.fileName then
47+
-- let sub ← go real
48+
-- return includeSelf ++ sub
49+
-- else
50+
-- return includeSelf
51+
-- else
52+
-- return includeSelf
53+
-- | .ok { type := .dir, .. } =>
54+
-- let sub ← go path
55+
-- return includeSelf ++ sub
56+
-- | .ok => return includeSelf
57+
-- | .error (.noFileOrDirectory ..) => return #[]
58+
-- | .error e => throw e
59+
-- return results.join

Glob/WF/Tree.lean

Lines changed: 4 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -5,23 +5,6 @@ import Lean.Elab.Command
55

66
open Tree
77

8-
/--
9-
Match a single pattern segment against a tree dir name.
10-
- `lit s` matches if `s = name`.
11-
- `oneStar` matches any single name.
12-
- `doubleStar` is handled at pattern list level, not here.
13-
-/
14-
def PatternSegmentNonWF.matchNES (seg : PatternSegmentNonWF) (name : NonEmptyString) : Bool :=
15-
match seg with
16-
| .lit s => s == name
17-
| .oneStar => true
18-
| .doubleStar => false
19-
20-
def PatternSegmentNonWF.matchS (seg : PatternSegmentNonWF) (name : String) : Bool :=
21-
match NonEmptyString.fromString? name with
22-
| none => false
23-
| some name' => PatternSegmentNonWF.matchNES seg name'
24-
258
mutual
269
def globList : List PatternSegmentNonWF → Tree → Option Tree
2710
| [], t => some (match t with
@@ -102,6 +85,8 @@ instance : TreeGlobForPattern PatternValidated where
10285
glob := globValidated
10386
globMany := globManyValidated
10487

88+
namespace Tests
89+
10590
open TreeGlobForPattern
10691

10792
open Lean Elab Command Meta
@@ -183,3 +168,5 @@ def globTestExample2 := tree! "Root" {
183168
"foo" { "bar" { "baz.txt" } },
184169
"foo2" { "bar" { "qux2.md" } }
185170
})
171+
172+
end Tests

Glob/WF/Types.lean

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ import Lean.Parser.Term
44
import Glob.Data.NonEmptyString
55
import Glob.Data.NonEmptyList
66
import Glob.NonWF.Types
7+
import Glob.NonWF.Normalize
78

89
--------------------------------------
910

@@ -48,6 +49,9 @@ structure PatternValidated : Type where
4849
valid_sequence : isValidSequence pattern
4950
deriving Repr, Ord, Hashable, DecidableEq
5051

52+
instance : Inhabited PatternValidated where
53+
default := ⟨[.oneStar], by simp [isValidSequence]⟩
54+
5155
open Lean Meta Elab
5256

5357
-- Helper function to create decidable proofs (same as in the regex library)
@@ -115,3 +119,18 @@ def PatternValidated.mk? (segments : List PatternSegmentNonWF) : Except PatternV
115119

116120
-- ✅ "**/foo/**/bar/**"
117121
#guard (PatternValidated.mk? [.doubleStar, nes!"foo", .doubleStar, nes!"bar", .doubleStar]).isOk
122+
123+
-----------------------------
124+
125+
def PatternValidated.patternStrict? (str : String) : Except String PatternValidated :=
126+
match PatternNonWF'.fromStringStrict str with
127+
| .none => throw "Did some segment was empty? `foo//bar` should be `foo/bar`"
128+
| .some pat => match (PatternValidated.mk? pat) with
129+
| .error .invalidEmpty => throw PatternValidatedError.invalidEmpty.toHumanReadable
130+
| .error .invalidWrongOrdering => throw (s!"Probably You wanted to write {PatternNonWF'.toString $ normalizeSegments pat}\n{PatternValidatedError.invalidWrongOrdering.toHumanReadable}")
131+
| .ok pat => return pat
132+
133+
def PatternValidated.patternStrictIO! (str : String) : IO PatternValidated := do
134+
match PatternValidated.patternStrict? str with
135+
| .ok pat => pure pat
136+
| .error err => throw <| IO.userError err

Test/GlobRealSpec.lean

Lines changed: 126 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,126 @@
1+
-- runTests #[
2+
-- ("FindRecursive", fun (currentTmpDir : FilePath) => do -- TODO: this is a limitation of glob-posix, no support of recursion
3+
-- writeFile "foo.txt" "content"
4+
-- createDir "subdir"
5+
-- writeFile "subdir/bar.txt" "content"
6+
-- writeFile "subdir/foo.txt" "content"
7+
-- createDir "subdir/another_subdir"
8+
-- writeFile "subdir/another_subdir/bar.txt" "content"
9+
-- writeFile "subdir/another_subdir/foo.txt" "content"
10+
-- assertGlob nel![PatternSegment.doubleStar, nes!"foo.txt"] #["foo.txt", "subdir/foo.txt", "subdir/another_subdir/foo.txt"]
11+
-- assertGlob nel![nes!"foo.txt"]] #["foo.txt"]
12+
-- assertGlob nel![PatternSegment.oneStar, nes!"foo.txt"] #["subdir/foo.txt"]
13+
-- ]
14+
-- -- ("BasicWildcard", fun (_tmpDir : FilePath) => do
15+
-- -- writeFile "file1.txt" "content"
16+
-- -- writeFile "file2.txt" "content"
17+
-- -- writeFile "image.png" "content"
18+
-- -- createDir "subdir"
19+
-- -- writeFile "subdir/file3.txt" "content"
20+
-- -- createDir "empty_dir"
21+
--
22+
-- -- let results ← glob "*.txt"
23+
-- -- assertEq "Basic wildcard *.txt" #["file1.txt", "file2.txt"] results
24+
--
25+
-- -- let allFiles ← glob "*"
26+
-- -- assertEq "All files *" #["file1.txt", "file2.txt", "image.png", "empty_dir", "subdir"] allFiles),
27+
-- -- ("QuestionMark", fun (_tmpDir : FilePath) => do
28+
-- -- writeFile "doc1" "content"
29+
-- -- writeFile "doc2" "content"
30+
-- -- writeFile "doc_long" "content"
31+
--
32+
-- -- let results ← glob "doc?"
33+
-- -- assertEq "Question mark doc?" #["doc1", "doc2"] results),
34+
-- -- ("CharacterClass", fun (_tmpDir : FilePath) => do
35+
-- -- writeFile "apple" "content"
36+
-- -- writeFile "apricot" "content"
37+
-- -- writeFile "banana" "content"
38+
-- -- assertEq "Character class a[p-r]*" #["apple", "apricot"] (← glob "a[p-r]*")),
39+
-- -- ("GlobWithDirMark", fun (_tmpDir : FilePath) => do
40+
-- -- writeFile "file.txt" "content"
41+
-- -- createDir "mydir"
42+
-- -- createDir "another_dir"
43+
-- -- let expected := #["file.txt", "mydir/", "another_dir/"]
44+
-- -- assertEq "globWithDirMark *" expected (← globWithDirMark "*")),
45+
-- -- ("GlobUnsorted", fun (_tmpDir : FilePath) => do
46+
-- -- writeFile "c.txt" "c"
47+
-- -- writeFile "a.txt" "a"
48+
-- -- writeFile "b.txt" "b"
49+
-- -- -- We can't assert a specific order, just that all are present and count is correct
50+
-- -- assertEq "globUnsorted *.txt" #["a.txt", "b.txt", "c.txt"] (← globUnsorted "*.txt")),
51+
-- -- ("CheckPattern", fun (_tmpDir : FilePath) => do
52+
-- -- writeFile "existing.txt" "content"
53+
-- -- writeFile "another.md" "content"
54+
-- -- assertBool "checkPattern *.txt (true)" true (← checkPattern "*.txt")
55+
-- -- assertBool "checkPattern *.xyz (false)" false (← checkPattern "*.xyz")
56+
-- -- assertBool "checkPattern existing.txt (true)" true (← checkPattern "existing.txt")
57+
-- -- assertBool "checkPattern non_existing.txt (false)" false (← checkPattern "non_existing.txt")),
58+
-- -- ("GlobMany", fun (_tmpDir : FilePath) => do
59+
-- -- writeFile "file.txt" "content"
60+
-- -- writeFile "doc.md" "content"
61+
-- -- writeFile "image.jpg" "content"
62+
-- -- writeFile "data.csv" "content"
63+
-- -- assertEq "globMany multiple extensions" #["file.txt", "doc.md", "data.csv"] (← globMany #["*.txt", "*.md", "*.csv"])
64+
-- -- assertEq "globMany mixed (some match, some no match)" #["file.txt"] (← globMany #["*.xyz", "*.txt"])
65+
-- -- assertIsEmpty "globMany all no match" (← globMany #["*.xyz", "*.abc"])),
66+
-- -- ("GlobWithBraces", fun (_tmpDir : FilePath) => do
67+
-- -- writeFile "config.json" "content"
68+
-- -- writeFile "config.yaml" "content"
69+
-- -- writeFile "config.txt" "content"
70+
-- -- writeFile "data.json" "content"
71+
-- -- assertEq "globWithBraces config.{json,yaml}" #["config.json", "config.yaml"] (← globWithBraces "config.{json,yaml}")),
72+
-- -- ("GlobWithTilde", fun (_tmpDir : FilePath) => do
73+
-- -- -- Tilde expansion is highly environment-dependent. This test primarily checks
74+
-- -- -- that the flag is passed and doesn't cause a crash. A true functional test
75+
-- -- -- would require setting up a controlled home directory, which is non-trivial.
76+
-- -- let homeDirFile := "~/.profile"
77+
-- -- let results ← globWithTilde homeDirFile
78+
-- -- if results.isEmpty then
79+
-- -- IO.println s!"Warning: {homeDirFile} not found or tilde expansion failed. (This might be normal depending on environment/config)"
80+
-- -- pure ()
81+
-- -- else
82+
-- -- assertIsNotEmpty "globWithTilde ~/" results
83+
-- -- IO.println s!"Found {results.size} files with tilde expansion, e.g., {results[0]!}"),
84+
-- -- ("GlobDirsOnly", fun (tmpDir : FilePath) => do
85+
-- -- writeFile "file.txt" "content"
86+
-- -- createDir "dir1"
87+
-- -- createDir "dir2"
88+
-- -- writeFile (tmpDir / "dir1" / "nested_file.txt") "content"
89+
-- -- assertEq "globDirsOnly *" #["dir1/", "dir2/"] (← globDirsOnly "*")),
90+
-- -- ("GlobSafe", fun (_tmpDir : FilePath) => do
91+
-- -- writeFile "present.txt" "content"
92+
-- -- assertEq "globSafe (match)" #["present.txt"] (← globSafe "*.txt")
93+
-- -- assertEq "globSafe (no match, nocheck)" #["nonexistent.*"] (← globSafe "nonexistent.*")
94+
-- -- assertEq "globSafe (literal no match, nocheck)" #["definitely_not_here.md"] (← globSafe "definitely_not_here.md")),
95+
-- -- ("FindByExtension", fun (_tmpDir : FilePath) => do
96+
-- -- writeFile "a.lean" "content"
97+
-- -- writeFile "b.md" "content"
98+
-- -- writeFile "c.lean" "content"
99+
-- -- assertEq "findByExtension lean" #["a.lean", "c.lean"] (← findByExtension "lean")
100+
-- -- assertIsEmpty "findByExtension xyz (empty)" (← findByExtension "xyz")),
101+
-- -- ("FindByExtensions", fun (_tmpDir : FilePath) => do
102+
-- -- writeFile "a.lean" "content"
103+
-- -- writeFile "b.md" "content"
104+
-- -- writeFile "c.txt" "content"
105+
-- -- writeFile "d.json" "content"
106+
-- -- assertEq "findByExtensions lean, txt" #["a.lean", "c.txt"] (← findByExtensions #["lean", "txt"])
107+
-- -- assertIsEmpty "findByExtensions xyz, abc (empty)" (← findByExtensions #["xyz", "abc"])),
108+
-- -- ("FindDirectories", fun (tmpDir : FilePath) => do
109+
-- -- writeFile "file.txt" "content"
110+
-- -- createDir "dir1"
111+
-- -- createDir "dir2"
112+
-- -- writeFile (tmpDir / "dir1" / "nested.txt") "content"
113+
-- -- assertEq "findDirectories" #["dir1/", "dir2/"] (← findDirectories)),
114+
-- -- ("NoMatchesWithoutNoCheck", fun (_tmpDir : FilePath) => do
115+
-- -- assertIsEmpty "No matches without nocheck" (← glob "*.nonexistent")),
116+
-- -- ("TestErrFlag", fun (tmpDir : FilePath) => do
117+
-- -- -- This test remains limited due to portability of permissions.
118+
-- -- -- It primarily ensures the flag passes and doesn't crash the FFI.
119+
-- -- let restrictedDir := tmpDir / "restricted"
120+
-- -- createDir restrictedDir
121+
-- -- -- One *could* attempt `IO.Process.runCommand` for `chmod` but it's not portable
122+
-- -- -- across OSes or always reliable for testing specific error conditions.
123+
-- -- let results ← glob (restrictedDir / "*").toString { GlobFlags.default with err := true }
124+
-- -- IO.println s!"TestErrFlag: Results: {results}"
125+
-- -- )
126+
-- /- ] -/

0 commit comments

Comments
 (0)