diff --git a/exercises/practice/etl/EtlTest.lean b/exercises/practice/etl/EtlTest.lean index b38fd07..a2d04b5 100644 --- a/exercises/practice/etl/EtlTest.lean +++ b/exercises/practice/etl/EtlTest.lean @@ -3,31 +3,78 @@ import Etl import Std open LeanTest -open Std -instance : BEq (HashMap Char Nat) where - beq h1 h2 := - h1.size == h2.size && - h1.fold (fun acc k v => - acc && match h2.get? k with - | some v' => v == v' - | none => false - ) true +def Std.HashMap.toSortedList (map : Std.HashMap Char Nat) := + map.toArray.qsort (λ (k1, _) (k2, _) => k1 ≤ k2) + +instance : BEq (Std.HashMap Char Nat) where + beq a b := a.toSortedList == b.toSortedList def etlTests : TestSuite := (TestSuite.empty "Etl") |>.addTest "single letter" (do - return assertEqual (.ofList [('a', 1)]) - (Etl.transform (.ofList [(1, ['A'])]))) + return assertEqual (.ofList [ + ('a', 1) + ]) $ Etl.transform (.ofList [ + (1, ['A']) + ])) |>.addTest "single score with multiple letters" (do - return assertEqual (.ofList [('a', 1), ('e', 1), ('i', 1), ('o', 1), ('u', 1)]) - (Etl.transform (.ofList [(1, ['A','E','I','O','U'])]))) + return assertEqual (.ofList [ + ('a', 1), + ('e', 1), + ('i', 1), + ('o', 1), + ('u', 1) + ]) $ Etl.transform (.ofList [ + (1, ['A', 'E', 'I', 'O', 'U']) + ])) |>.addTest "multiple scores with multiple letters" (do - return assertEqual (.ofList [('a', 1), ('d', 2), ('e', 1), ('g', 2)]) - (Etl.transform (.ofList [(1, ['A','E']), (2, ['D','G'])]))) + return assertEqual (.ofList [ + ('a', 1), + ('d', 2), + ('e', 1), + ('g', 2) + ]) $ Etl.transform (.ofList [ + (1, ['A', 'E']), + (2, ['D', 'G']) + ])) |>.addTest "multiple scores with differing numbers of letters" (do - return assertEqual (.ofList [('a', 1), ('b', 3), ('c', 3), ('d', 2), ('e', 1), ('f', 4), ('g', 2), ('h', 4), ('i', 1), ('j', 8), ('k', 5), ('l', 1), ('m', 3), ('n', 1), ('o', 1), ('p', 3), ('q', 10), ('r', 1), ('s', 1), ('t', 1), ('u', 1), ('v', 4), ('w', 4), ('x', 8), ('y', 4), ('z', 10)]) - (Etl.transform (.ofList [(1, ['A','E','I','O','U','L','N','R','S','T']), (10, ['Q','Z']), (2, ['D','G']), (3, ['B','C','M','P']), (4, ['F','H','V','W','Y']), (5, ['K']), (8, ['J','X'])]))) + return assertEqual (.ofList [ + ('a', 1), + ('b', 3), + ('c', 3), + ('d', 2), + ('e', 1), + ('f', 4), + ('g', 2), + ('h', 4), + ('i', 1), + ('j', 8), + ('k', 5), + ('l', 1), + ('m', 3), + ('n', 1), + ('o', 1), + ('p', 3), + ('q', 10), + ('r', 1), + ('s', 1), + ('t', 1), + ('u', 1), + ('v', 4), + ('w', 4), + ('x', 8), + ('y', 4), + ('z', 10) + ]) $ Etl.transform (.ofList [ + (1, ['A', 'E', 'I', 'O', 'U', 'L', 'N', 'R', 'S', 'T']), + (10, ['Q', 'Z']), + (2, ['D', 'G']), + (3, ['B', 'C', 'M', 'P']), + (4, ['F', 'H', 'V', 'W', 'Y']), + (5, ['K']), + (8, ['J', 'X']) + ])) def main : IO UInt32 := do runTestSuitesWithExitCode [etlTests] diff --git a/generators/Generator/Generator/EtlGenerator.lean b/generators/Generator/Generator/EtlGenerator.lean index dcd21cc..d0ab15c 100644 --- a/generators/Generator/Generator/EtlGenerator.lean +++ b/generators/Generator/Generator/EtlGenerator.lean @@ -13,32 +13,39 @@ import {exercise} import Std open LeanTest -open Std -instance : BEq (HashMap Char Nat) where - beq h1 h2 := - h1.size == h2.size && - h1.fold (fun acc k v => - acc && match h2.get? k with - | some v' => v == v' - | none => false - ) true +def Std.HashMap.toSortedList (map : Std.HashMap Char Nat) := + map.toArray.qsort (λ (k1, _) (k2, _) => k1 ≤ k2) + +instance : BEq (Std.HashMap Char Nat) where + beq a b := a.toSortedList == b.toSortedList def {exercise.decapitalize}Tests : TestSuite := (TestSuite.empty \"{exercise}\")" +def mapJsonArray (array : Json) : String := + array.getArr? + |> getOk + |>.map (λ v => s!"'{toLiteral v.compress}'") + |>.toList + |> (s!"{·}") + +def serializeLegacy (key : String) (val : Json) : String := + s!"({key}, {mapJsonArray val})" + +def serializeOutput (key : String) (val : Json) : String := + s!"('{key}', {val})" + def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String := - let input := case.get! "input" |> (·.getObjValD "legacy") - let legacyKeys := (getKeyValues input).map (λ (k, v) => (toLiteral k, v.replace "\"" "'")) + let input := case.get! "input" |>.getObjValD "legacy" let expected := case.get! "expected" - let expectedKeys := (getKeyValues expected).map (λ (k, v) => (s!"'{k}'", toLiteral v)) let description := case.get! "description" |> (·.compress) let funName := getFunName (case.get! "property") - let call := s!"({exercise}.{funName} (.ofList {legacyKeys}))" + let call := s!"$ {exercise}.{funName} (.ofList {serializeObjectAsList input serializeLegacy})" s!" |>.addTest {description} (do - return assertEqual (.ofList {expectedKeys})\n {call})" + return assertEqual (.ofList {serializeObjectAsList expected serializeOutput}) {call})" def genEnd (exercise : String) : String := s!"