Skip to content

Commit c916ce2

Browse files
author
oxe-i
committed
add generator
1 parent fe574a3 commit c916ce2

File tree

3 files changed

+123
-20
lines changed

3 files changed

+123
-20
lines changed
Lines changed: 83 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,44 +1,107 @@
11
import LeanTest
2+
import Std
23
import WordCount
34

45
open LeanTest
56

6-
def sort (list : List (String × Nat)) : List (String × Nat) :=
7-
list.mergeSort (fun x y => x.fst <= y.fst)
8-
9-
def sortedResult (sentence : String) : List (String × Nat) :=
10-
WordCount.countWords sentence |> Std.HashMap.toList |> sort
11-
127
def wordCountTests : TestSuite :=
138
(TestSuite.empty "WordCount")
149
|>.addTest "count one word" (do
15-
return assertEqual (sort [("word", 1)]) (sortedResult "word"))
10+
return assertEqual [
11+
("word", 1)
12+
] ((·.mergeSort (λ (k1, _) (k2, _) => k1 ≤ k2)) <| Std.HashMap.toList <| WordCount.countWords "word"))
1613
|>.addTest "count one of each word" (do
17-
return assertEqual (sort [("one", 1), ("of", 1), ("each", 1)]) (sortedResult "one of each"))
14+
return assertEqual [
15+
("each", 1),
16+
("of", 1),
17+
("one", 1)
18+
] ((·.mergeSort (λ (k1, _) (k2, _) => k1 ≤ k2)) <| Std.HashMap.toList <| WordCount.countWords "one of each"))
1819
|>.addTest "multiple occurrences of a word" (do
19-
return assertEqual (sort [("one", 1), ("fish", 4), ("two", 1), ("red", 1), ("blue", 1)]) (sortedResult "one fish two fish red fish blue fish"))
20+
return assertEqual [
21+
("blue", 1),
22+
("fish", 4),
23+
("one", 1),
24+
("red", 1),
25+
("two", 1)
26+
] ((·.mergeSort (λ (k1, _) (k2, _) => k1 ≤ k2)) <| Std.HashMap.toList <| WordCount.countWords "one fish two fish red fish blue fish"))
2027
|>.addTest "handles cramped lists" (do
21-
return assertEqual (sort [("one", 1), ("two", 1), ("three", 1)]) (sortedResult "one,two,three"))
28+
return assertEqual [
29+
("one", 1),
30+
("three", 1),
31+
("two", 1)
32+
] ((·.mergeSort (λ (k1, _) (k2, _) => k1 ≤ k2)) <| Std.HashMap.toList <| WordCount.countWords "one,two,three"))
2233
|>.addTest "handles expanded lists" (do
23-
return assertEqual (sort [("one", 1), ("two", 1), ("three", 1)]) (sortedResult "one,\ntwo,\nthree"))
34+
return assertEqual [
35+
("one", 1),
36+
("three", 1),
37+
("two", 1)
38+
] ((·.mergeSort (λ (k1, _) (k2, _) => k1 ≤ k2)) <| Std.HashMap.toList <| WordCount.countWords "one,\ntwo,\nthree"))
2439
|>.addTest "ignore punctuation" (do
25-
return assertEqual (sort [("car", 1), ("carpet", 1), ("as", 1), ("java", 1), ("javascript", 1)]) (sortedResult "car: carpet as java: javascript!!&@$%^&"))
40+
return assertEqual [
41+
("as", 1),
42+
("car", 1),
43+
("carpet", 1),
44+
("java", 1),
45+
("javascript", 1)
46+
] ((·.mergeSort (λ (k1, _) (k2, _) => k1 ≤ k2)) <| Std.HashMap.toList <| WordCount.countWords "car: carpet as java: javascript!!&@$%^&"))
2647
|>.addTest "include numbers" (do
27-
return assertEqual (sort [("testing", 2), ("1", 1), ("2", 1)]) (sortedResult "testing, 1, 2 testing"))
48+
return assertEqual [
49+
("1", 1),
50+
("2", 1),
51+
("testing", 2)
52+
] ((·.mergeSort (λ (k1, _) (k2, _) => k1 ≤ k2)) <| Std.HashMap.toList <| WordCount.countWords "testing, 1, 2 testing"))
2853
|>.addTest "normalize case" (do
29-
return assertEqual (sort [("go", 3), ("stop", 2)]) (sortedResult "go Go GO Stop stop"))
54+
return assertEqual [
55+
("go", 3),
56+
("stop", 2)
57+
] ((·.mergeSort (λ (k1, _) (k2, _) => k1 ≤ k2)) <| Std.HashMap.toList <| WordCount.countWords "go Go GO Stop stop"))
3058
|>.addTest "with apostrophes" (do
31-
return assertEqual (sort [("first", 1), ("don't", 2), ("laugh", 1), ("then", 1), ("cry", 1), ("you're", 1), ("getting", 1), ("it", 1)] ) (sortedResult "'First: don't laugh. Then: don't cry. You're getting it.'"))
59+
return assertEqual [
60+
("cry", 1),
61+
("don't", 2),
62+
("first", 1),
63+
("getting", 1),
64+
("it", 1),
65+
("laugh", 1),
66+
("then", 1),
67+
("you're", 1)
68+
] ((·.mergeSort (λ (k1, _) (k2, _) => k1 ≤ k2)) <| Std.HashMap.toList <| WordCount.countWords "'First: don't laugh. Then: don't cry. You're getting it.'"))
3269
|>.addTest "with quotations" (do
33-
return assertEqual (sort [("joe", 1), ("can't", 1), ("tell", 1), ("between", 1), ("large", 2), ("and", 1)]) (sortedResult "Joe can't tell between 'large' and large."))
70+
return assertEqual [
71+
("and", 1),
72+
("between", 1),
73+
("can't", 1),
74+
("joe", 1),
75+
("large", 2),
76+
("tell", 1)
77+
] ((·.mergeSort (λ (k1, _) (k2, _) => k1 ≤ k2)) <| Std.HashMap.toList <| WordCount.countWords "Joe can't tell between 'large' and large."))
3478
|>.addTest "substrings from the beginning" (do
35-
return assertEqual (sort [("joe", 1), ("can't", 1), ("tell", 1), ("between", 1), ("app", 1), ("apple", 1), ("and", 1), ("a", 1)]) (sortedResult "Joe can't tell between app, apple and a."))
79+
return assertEqual [
80+
("a", 1),
81+
("and", 1),
82+
("app", 1),
83+
("apple", 1),
84+
("between", 1),
85+
("can't", 1),
86+
("joe", 1),
87+
("tell", 1)
88+
] ((·.mergeSort (λ (k1, _) (k2, _) => k1 ≤ k2)) <| Std.HashMap.toList <| WordCount.countWords "Joe can't tell between app, apple and a."))
3689
|>.addTest "multiple spaces not detected as a word" (do
37-
return assertEqual (sort [("multiple", 1), ("whitespaces", 1)]) (sortedResult " multiple whitespaces"))
90+
return assertEqual [
91+
("multiple", 1),
92+
("whitespaces", 1)
93+
] ((·.mergeSort (λ (k1, _) (k2, _) => k1 ≤ k2)) <| Std.HashMap.toList <| WordCount.countWords " multiple whitespaces"))
3894
|>.addTest "alternating word separators not detected as a word" (do
39-
return assertEqual (sort [("one", 1), ("two", 1), ("three", 1)]) (sortedResult ",\n,one,\n ,two \n 'three'"))
95+
return assertEqual [
96+
("one", 1),
97+
("three", 1),
98+
("two", 1)
99+
] ((·.mergeSort (λ (k1, _) (k2, _) => k1 ≤ k2)) <| Std.HashMap.toList <| WordCount.countWords ",\n,one,\n ,two \n 'three'"))
40100
|>.addTest "quotation for word with apostrophe" (do
41-
return assertEqual (sort [("can", 1), ("can't", 2)]) (sortedResult "can, can't, 'can't'"))
101+
return assertEqual [
102+
("can", 1),
103+
("can't", 2)
104+
] ((·.mergeSort (λ (k1, _) (k2, _) => k1 ≤ k2)) <| Std.HashMap.toList <| WordCount.countWords "can, can't, 'can't'"))
42105

43106
def main : IO UInt32 := do
44107
runTestSuitesWithExitCode [wordCountTests]

generators/Generator/Generator.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
import Generator.WordCountGenerator
12
import Generator.SgfParsingGenerator
23
import Generator.DndCharacterGenerator
34
import Generator.BankAccountGenerator
@@ -92,6 +93,7 @@ abbrev endBodyGenerator := String -> String
9293

9394
def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBodyGenerator) :=
9495
Std.HashMap.ofList [
96+
("WordCount", (WordCountGenerator.genIntro, WordCountGenerator.genTestCase, WordCountGenerator.genEnd)),
9597
("SgfParsing", (SgfParsingGenerator.genIntro, SgfParsingGenerator.genTestCase, SgfParsingGenerator.genEnd)),
9698
("DndCharacter", (DndCharacterGenerator.genIntro, DndCharacterGenerator.genTestCase, DndCharacterGenerator.genEnd)),
9799
("BankAccount", (BankAccountGenerator.genIntro, BankAccountGenerator.genTestCase, BankAccountGenerator.genEnd)),
Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
import Lean.Data.Json
2+
import Std
3+
import Helper
4+
5+
open Lean
6+
open Std
7+
open Helper
8+
9+
namespace WordCountGenerator
10+
11+
def genIntro (exercise : String) : String := s!"import LeanTest
12+
import Std
13+
import {exercise}
14+
15+
open LeanTest
16+
17+
def {exercise.decapitalize}Tests : TestSuite :=
18+
(TestSuite.empty \"{exercise}\")"
19+
20+
def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String :=
21+
let input := case.get! "input"
22+
let expected := case.get! "expected" |> (serializeObjectAsList · λ k v => s!"(\"{k}\", {v})")
23+
let description := case.get! "description"
24+
|> (·.compress)
25+
let funName := getFunName (case.get! "property")
26+
let call := s!"((·.mergeSort (λ (k1, _) (k2, _) => k1 ≤ k2)) <| Std.HashMap.toList <| {exercise}.{funName} {insertAllInputs input})"
27+
s!"
28+
|>.addTest {description} (do
29+
return assertEqual {expected} {call})"
30+
31+
def genEnd (exercise : String) : String :=
32+
s!"
33+
34+
def main : IO UInt32 := do
35+
runTestSuitesWithExitCode [{exercise.decapitalize}Tests]
36+
"
37+
38+
end WordCountGenerator

0 commit comments

Comments
 (0)