From 3c79c8e5f64080d599bc2e033f336ff2bd14b59a Mon Sep 17 00:00:00 2001 From: polsinelli johan Date: Tue, 24 Mar 2026 12:08:21 +0100 Subject: [PATCH 1/4] Add List-Ops practice exercise Implements all 8 list operations: append, concat, filter, length, map, foldl, foldr, reverse. Includes test generator, reference solution, and 22 test cases from canonical data. Closes #158 --- config.json | 8 + .../practice/list-ops/.docs/instructions.md | 19 ++ .../practice/list-ops/.meta/Example.lean | 44 +++++ exercises/practice/list-ops/.meta/config.json | 18 ++ exercises/practice/list-ops/.meta/tests.toml | 106 +++++++++++ exercises/practice/list-ops/ListOps.lean | 27 +++ exercises/practice/list-ops/ListOpsTest.lean | 54 ++++++ exercises/practice/list-ops/lakefile.toml | 15 ++ exercises/practice/list-ops/lean-toolchain | 1 + .../list-ops/vendor/LeanTest/LeanTest.lean | 4 + .../vendor/LeanTest/LeanTest/Assertions.lean | 166 ++++++++++++++++++ .../vendor/LeanTest/LeanTest/Test.lean | 130 ++++++++++++++ generators/Generator/Generator.lean | 4 +- .../Generator/Generator/ListOpsGenerator.lean | 151 ++++++++++++++++ 14 files changed, 746 insertions(+), 1 deletion(-) create mode 100644 exercises/practice/list-ops/.docs/instructions.md create mode 100644 exercises/practice/list-ops/.meta/Example.lean create mode 100644 exercises/practice/list-ops/.meta/config.json create mode 100644 exercises/practice/list-ops/.meta/tests.toml create mode 100644 exercises/practice/list-ops/ListOps.lean create mode 100644 exercises/practice/list-ops/ListOpsTest.lean create mode 100644 exercises/practice/list-ops/lakefile.toml create mode 100644 exercises/practice/list-ops/lean-toolchain create mode 100644 exercises/practice/list-ops/vendor/LeanTest/LeanTest.lean create mode 100644 exercises/practice/list-ops/vendor/LeanTest/LeanTest/Assertions.lean create mode 100644 exercises/practice/list-ops/vendor/LeanTest/LeanTest/Test.lean create mode 100644 generators/Generator/Generator/ListOpsGenerator.lean diff --git a/config.json b/config.json index 07f848e..6f05403 100644 --- a/config.json +++ b/config.json @@ -234,6 +234,14 @@ "prerequisites": [], "difficulty": 3 }, + { + "slug": "list-ops", + "name": "List Ops", + "uuid": "e6e4e258-e669-4875-afce-c6a65405b3d0", + "practices": [], + "prerequisites": [], + "difficulty": 3 + }, { "slug": "gigasecond", "name": "Gigasecond", diff --git a/exercises/practice/list-ops/.docs/instructions.md b/exercises/practice/list-ops/.docs/instructions.md new file mode 100644 index 0000000..ebc5dff --- /dev/null +++ b/exercises/practice/list-ops/.docs/instructions.md @@ -0,0 +1,19 @@ +# Instructions + +Implement basic list operations. + +In functional languages list operations like `length`, `map`, and `reduce` are very common. +Implement a series of basic list operations, without using existing functions. + +The precise number and names of the operations to be implemented will be track dependent to avoid conflicts with existing names, but the general operations you will implement include: + +- `append` (_given two lists, add all items in the second list to the end of the first list_); +- `concatenate` (_given a series of lists, combine all items in all lists into one flattened list_); +- `filter` (_given a predicate and a list, return the list of all items for which `predicate(item)` is True_); +- `length` (_given a list, return the total number of items within it_); +- `map` (_given a function and a list, return the list of the results of applying `function(item)` on all items_); +- `foldl` (_given a function, a list, and initial accumulator, fold (reduce) each item into the accumulator from the left_); +- `foldr` (_given a function, a list, and an initial accumulator, fold (reduce) each item into the accumulator from the right_); +- `reverse` (_given a list, return a list with all the original items, but in reversed order_). + +Note, the ordering in which arguments are passed to the fold functions (`foldl`, `foldr`) is significant. diff --git a/exercises/practice/list-ops/.meta/Example.lean b/exercises/practice/list-ops/.meta/Example.lean new file mode 100644 index 0000000..c3b2707 --- /dev/null +++ b/exercises/practice/list-ops/.meta/Example.lean @@ -0,0 +1,44 @@ +namespace ListOps + +def append (list1 : List α) (list2 : List α) : List α := + match list1 with + | [] => list2 + | x :: xs => x :: append xs list2 + +def concat (lists : List (List α)) : List α := + match lists with + | [] => [] + | xs :: rest => append xs (concat rest) + +def filter (f : α → Bool) (list : List α) : List α := + match list with + | [] => [] + | x :: xs => if f x then x :: filter f xs else filter f xs + +def length (list : List α) : Nat := + match list with + | [] => 0 + | _ :: xs => 1 + length xs + +def map (f : α → β) (list : List α) : List β := + match list with + | [] => [] + | x :: xs => f x :: map f xs + +def foldl (f : β → α → β) (initial : β) (list : List α) : β := + match list with + | [] => initial + | x :: xs => foldl f (f initial x) xs + +def foldr (f : α → β → β) (initial : β) (list : List α) : β := + match list with + | [] => initial + | x :: xs => f x (foldr f initial xs) + +def reverse (list : List α) : List α := + let rec go (acc : List α) : List α → List α + | [] => acc + | x :: xs => go (x :: acc) xs + go [] list + +end ListOps diff --git a/exercises/practice/list-ops/.meta/config.json b/exercises/practice/list-ops/.meta/config.json new file mode 100644 index 0000000..c806a49 --- /dev/null +++ b/exercises/practice/list-ops/.meta/config.json @@ -0,0 +1,18 @@ +{ + "authors": [ + "oxe-i" + ], + "files": { + "solution": [ + "ListOps.lean" + ], + "test": [ + "ListOpsTest.lean" + ], + "example": [ + ".meta/Example.lean" + ] + }, + "blurb": "Implement basic list operations.", + "source": "https://github.com/exercism/problem-specifications/tree/main/exercises/list-ops" +} diff --git a/exercises/practice/list-ops/.meta/tests.toml b/exercises/practice/list-ops/.meta/tests.toml new file mode 100644 index 0000000..11d4527 --- /dev/null +++ b/exercises/practice/list-ops/.meta/tests.toml @@ -0,0 +1,106 @@ +# This is an auto-generated file. +# +# Regenerating this file via `configlet sync` will: +# - Recreate every `description` key/value pair +# - Recreate every `reimplements` key/value pair, where they exist in problem-specifications +# - Remove any `include = true` key/value pair (an omitted `include` key implies inclusion) +# - Preserve any other key/value pair +# +# As user-added comments (using the # character) will be removed when this file +# is regenerated, comments can be added via a `comment` key. + +[485b9452-bf94-40f7-a3db-c3cf4850066a] +description = "append entries to a list and return the new list -> empty lists" + +[2c894696-b609-4569-b149-8672134d340a] +description = "append entries to a list and return the new list -> list to empty list" + +[e842efed-3bf6-4295-b371-4d67a4fdf19c] +description = "append entries to a list and return the new list -> empty list to list" + +[71dcf5eb-73ae-4a0e-b744-a52ee387922f] +description = "append entries to a list and return the new list -> non-empty lists" + +[28444355-201b-4af2-a2f6-5550227bde21] +description = "concatenate a list of lists -> empty list" + +[331451c1-9573-42a1-9869-2d06e3b389a9] +description = "concatenate a list of lists -> list of lists" + +[d6ecd72c-197f-40c3-89a4-aa1f45827e09] +description = "concatenate a list of lists -> list of nested lists" + +[0524fba8-3e0f-4531-ad2b-f7a43da86a16] +description = "filter list returning only values that satisfy the filter function -> empty list" + +[88494bd5-f520-4edb-8631-88e415b62d24] +description = "filter list returning only values that satisfy the filter function -> non-empty list" + +[1cf0b92d-8d96-41d5-9c21-7b3c37cb6aad] +description = "returns the length of a list -> empty list" + +[d7b8d2d9-2d16-44c4-9a19-6e5f237cb71e] +description = "returns the length of a list -> non-empty list" + +[c0bc8962-30e2-4bec-9ae4-668b8ecd75aa] +description = "return a list of elements whose values equal the list value transformed by the mapping function -> empty list" + +[11e71a95-e78b-4909-b8e4-60cdcaec0e91] +description = "return a list of elements whose values equal the list value transformed by the mapping function -> non-empty list" + +[613b20b7-1873-4070-a3a6-70ae5f50d7cc] +description = "folds (reduces) the given list from the left with a function -> empty list" +include = false + +[e56df3eb-9405-416a-b13a-aabb4c3b5194] +description = "folds (reduces) the given list from the left with a function -> direction independent function applied to non-empty list" +include = false + +[d2cf5644-aee1-4dfc-9b88-06896676fe27] +description = "folds (reduces) the given list from the left with a function -> direction dependent function applied to non-empty list" + +[36549237-f765-4a4c-bfd9-5d3a8f7b07d2] +description = "folds (reduces) the given list from the left with a function -> empty list" +reimplements = "613b20b7-1873-4070-a3a6-70ae5f50d7cc" + +[7a626a3c-03ec-42bc-9840-53f280e13067] +description = "folds (reduces) the given list from the left with a function -> direction independent function applied to non-empty list" +reimplements = "e56df3eb-9405-416a-b13a-aabb4c3b5194" + +[d7fcad99-e88e-40e1-a539-4c519681f390] +description = "folds (reduces) the given list from the left with a function -> direction dependent function applied to non-empty list" +reimplements = "d2cf5644-aee1-4dfc-9b88-06896676fe27" +include = false + +[aeb576b9-118e-4a57-a451-db49fac20fdc] +description = "folds (reduces) the given list from the right with a function -> empty list" +include = false + +[c4b64e58-313e-4c47-9c68-7764964efb8e] +description = "folds (reduces) the given list from the right with a function -> direction independent function applied to non-empty list" +include = false + +[be396a53-c074-4db3-8dd6-f7ed003cce7c] +description = "folds (reduces) the given list from the right with a function -> direction dependent function applied to non-empty list" + +[17214edb-20ba-42fc-bda8-000a5ab525b0] +description = "folds (reduces) the given list from the right with a function -> empty list" +reimplements = "aeb576b9-118e-4a57-a451-db49fac20fdc" + +[e1c64db7-9253-4a3d-a7c4-5273b9e2a1bd] +description = "folds (reduces) the given list from the right with a function -> direction independent function applied to non-empty list" +reimplements = "c4b64e58-313e-4c47-9c68-7764964efb8e" + +[8066003b-f2ff-437e-9103-66e6df474844] +description = "folds (reduces) the given list from the right with a function -> direction dependent function applied to non-empty list" +reimplements = "be396a53-c074-4db3-8dd6-f7ed003cce7c" +include = false + +[94231515-050e-4841-943d-d4488ab4ee30] +description = "reverse the elements of the list -> empty list" + +[fcc03d1e-42e0-4712-b689-d54ad761f360] +description = "reverse the elements of the list -> non-empty list" + +[40872990-b5b8-4cb8-9085-d91fc0d05d26] +description = "reverse the elements of the list -> list of lists is not flattened" diff --git a/exercises/practice/list-ops/ListOps.lean b/exercises/practice/list-ops/ListOps.lean new file mode 100644 index 0000000..b5154aa --- /dev/null +++ b/exercises/practice/list-ops/ListOps.lean @@ -0,0 +1,27 @@ +namespace ListOps + +def append (list1 : List α) (list2 : List α) : List α := + sorry --remove this line and implement the function + +def concat (lists : List (List α)) : List α := + sorry --remove this line and implement the function + +def filter (f : α → Bool) (list : List α) : List α := + sorry --remove this line and implement the function + +def length (list : List α) : Nat := + sorry --remove this line and implement the function + +def map (f : α → β) (list : List α) : List β := + sorry --remove this line and implement the function + +def foldl (f : β → α → β) (initial : β) (list : List α) : β := + sorry --remove this line and implement the function + +def foldr (f : α → β → β) (initial : β) (list : List α) : β := + sorry --remove this line and implement the function + +def reverse (list : List α) : List α := + sorry --remove this line and implement the function + +end ListOps diff --git a/exercises/practice/list-ops/ListOpsTest.lean b/exercises/practice/list-ops/ListOpsTest.lean new file mode 100644 index 0000000..e871886 --- /dev/null +++ b/exercises/practice/list-ops/ListOpsTest.lean @@ -0,0 +1,54 @@ +import LeanTest +import ListOps + +open LeanTest + +def listOpsTests : TestSuite := + (TestSuite.empty "ListOps") + |>.addTest "append entries to a list and return the new list -> empty lists" (do + return assertEqual ([] : List Int) (ListOps.append [] [])) + |>.addTest "append entries to a list and return the new list -> list to empty list" (do + return assertEqual [1, 2, 3, 4] (ListOps.append ([] : List Int) [1, 2, 3, 4])) + |>.addTest "append entries to a list and return the new list -> empty list to list" (do + return assertEqual [1, 2, 3, 4] (ListOps.append [1, 2, 3, 4] ([] : List Int))) + |>.addTest "append entries to a list and return the new list -> non-empty lists" (do + return assertEqual [1, 2, 2, 3, 4, 5] (ListOps.append [1, 2] [2, 3, 4, 5])) + |>.addTest "concatenate a list of lists -> empty list" (do + return assertEqual ([] : List Int) (ListOps.concat ([] : List (List Int)))) + |>.addTest "concatenate a list of lists -> list of lists" (do + return assertEqual [1, 2, 3, 4, 5, 6] (ListOps.concat [[1, 2], [3], [], [4, 5, 6]])) + |>.addTest "concatenate a list of lists -> list of nested lists" (do + return assertEqual [[1], [2], [3], [], [4, 5, 6]] (ListOps.concat [[[1], [2]], [[3]], [[]], [[4, 5, 6]]])) + |>.addTest "filter list returning only values that satisfy the filter function -> empty list" (do + return assertEqual ([] : List Int) (ListOps.filter (fun x => x % 2 == 1) [])) + |>.addTest "filter list returning only values that satisfy the filter function -> non-empty list" (do + return assertEqual [1, 3, 5] (ListOps.filter (fun x => x % 2 == 1) [1, 2, 3, 5])) + |>.addTest "returns the length of a list -> empty list" (do + return assertEqual 0 (ListOps.length ([] : List Int))) + |>.addTest "returns the length of a list -> non-empty list" (do + return assertEqual 4 (ListOps.length [1, 2, 3, 4])) + |>.addTest "return a list of elements whose values equal the list value transformed by the mapping function -> empty list" (do + return assertEqual ([] : List Int) (ListOps.map (· + 1) ([] : List Int))) + |>.addTest "return a list of elements whose values equal the list value transformed by the mapping function -> non-empty list" (do + return assertEqual [2, 4, 6, 8] (ListOps.map (· + 1) [1, 3, 5, 7])) + |>.addTest "folds (reduces) the given list from the left with a function -> empty list" (do + return assertEqual 2 (ListOps.foldl (fun acc el => el * acc) 2 ([] : List Int))) + |>.addTest "folds (reduces) the given list from the left with a function -> direction independent function applied to non-empty list" (do + return assertEqual 15 (ListOps.foldl (fun acc el => el + acc) 5 [1, 2, 3, 4])) + |>.addTest "folds (reduces) the given list from the left with a function -> direction dependent function applied to non-empty list" (do + return assertEqual 0 (ListOps.foldl (· / ·) 5 [2, 5])) + |>.addTest "folds (reduces) the given list from the right with a function -> empty list" (do + return assertEqual 2 (ListOps.foldr (fun el acc => el * acc) 2 ([] : List Int))) + |>.addTest "folds (reduces) the given list from the right with a function -> direction independent function applied to non-empty list" (do + return assertEqual 15 (ListOps.foldr (fun el acc => el + acc) 5 [1, 2, 3, 4])) + |>.addTest "folds (reduces) the given list from the right with a function -> direction dependent function applied to non-empty list" (do + return assertEqual 2 (ListOps.foldr (· / ·) 5 [2, 5])) + |>.addTest "reverse the elements of the list -> empty list" (do + return assertEqual ([] : List Int) (ListOps.reverse ([] : List Int))) + |>.addTest "reverse the elements of the list -> non-empty list" (do + return assertEqual [7, 5, 3, 1] (ListOps.reverse [1, 3, 5, 7])) + |>.addTest "reverse the elements of the list -> list of lists is not flattened" (do + return assertEqual [[4, 5, 6], [], [3], [1, 2]] (ListOps.reverse [[1, 2], [3], [], [4, 5, 6]])) + +def main : IO UInt32 := do + runTestSuitesWithExitCode [listOpsTests] diff --git a/exercises/practice/list-ops/lakefile.toml b/exercises/practice/list-ops/lakefile.toml new file mode 100644 index 0000000..3acf9d1 --- /dev/null +++ b/exercises/practice/list-ops/lakefile.toml @@ -0,0 +1,15 @@ +name = "list-ops" +version = "0.1.0" +defaultTargets = ["ListOpsTest"] +testDriver = "ListOpsTest" + +[[lean_lib]] +name = "LeanTest" +srcDir = "vendor/LeanTest" + +[[lean_lib]] +name = "ListOps" + +[[lean_exe]] +name = "ListOpsTest" +root = "ListOpsTest" diff --git a/exercises/practice/list-ops/lean-toolchain b/exercises/practice/list-ops/lean-toolchain new file mode 100644 index 0000000..370b26d --- /dev/null +++ b/exercises/practice/list-ops/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.25.2 diff --git a/exercises/practice/list-ops/vendor/LeanTest/LeanTest.lean b/exercises/practice/list-ops/vendor/LeanTest/LeanTest.lean new file mode 100644 index 0000000..012ba20 --- /dev/null +++ b/exercises/practice/list-ops/vendor/LeanTest/LeanTest.lean @@ -0,0 +1,4 @@ +-- This module serves as the root of the `LeanTest` library. +-- Import modules here that should be built as part of the library. +import LeanTest.Assertions +import LeanTest.Test diff --git a/exercises/practice/list-ops/vendor/LeanTest/LeanTest/Assertions.lean b/exercises/practice/list-ops/vendor/LeanTest/LeanTest/Assertions.lean new file mode 100644 index 0000000..60e4ad8 --- /dev/null +++ b/exercises/practice/list-ops/vendor/LeanTest/LeanTest/Assertions.lean @@ -0,0 +1,166 @@ +/- +Assertion functions for unit testing. +-/ + +namespace LeanTest + +/-- Result of a test assertion -/ +inductive AssertionResult where + | success : AssertionResult + | failure (message : String) : AssertionResult + deriving Repr, BEq + +namespace AssertionResult + +def isSuccess : AssertionResult → Bool + | success => true + | failure _ => false + +def getMessage : AssertionResult → String + | success => "Assertion passed" + | failure msg => msg + +end AssertionResult + +/-- Assert that a boolean condition is true -/ +def assert (condition : Bool) (message : String := "Assertion failed") : AssertionResult := + if condition then + .success + else + .failure message + +/-- Assert that two values are equal -/ +def assertEqual [BEq α] [Repr α] (expected : α) (actual : α) (message : String := "") : AssertionResult := + if expected == actual then + .success + else + let msg := if message.isEmpty then + s!"Expected: {repr expected}\nActual: {repr actual}" + else + s!"{message}\nExpected: {repr expected}\nActual: {repr actual}" + .failure msg + +/-- Assert that two values are not equal -/ +def assertNotEqual [BEq α] [Repr α] (expected : α) (actual : α) (message : String := "") : AssertionResult := + if expected != actual then + .success + else + let msg := if message.isEmpty then + s!"Expected values to be different, but both were: {repr expected}" + else + s!"{message}\nExpected values to be different, but both were: {repr expected}" + .failure msg + +/-- Refute that a boolean condition is true (assert it's false) -/ +def refute (condition : Bool) (message : String := "Refute failed - condition was true") : AssertionResult := + if !condition then + .success + else + .failure message + +/-- Assert that a value is true -/ +def assertTrue (value : Bool) (message : String := "Expected true but got false") : AssertionResult := + assert value message + +/-- Assert that a value is false -/ +def assertFalse (value : Bool) (message : String := "Expected false but got true") : AssertionResult := + refute value message + +/-- Assert that an Option is some -/ +def assertSome [Repr α] (opt : Option α) (message : String := "Expected Some but got None") : AssertionResult := + match opt with + | some _ => .success + | none => .failure message + +/-- Assert that an Option is none -/ +def assertNone [Repr α] (opt : Option α) (message : String := "") : AssertionResult := + match opt with + | none => .success + | some val => + let msg := if message.isEmpty then + s!"Expected None but got Some: {repr val}" + else + s!"{message}\nExpected None but got Some: {repr val}" + .failure msg + +/-- Assert that a list is empty -/ +def assertEmpty [Repr α] (list : List α) (message : String := "") : AssertionResult := + match list with + | [] => .success + | _ => + let msg := if message.isEmpty then + s!"Expected empty list but got: {repr list}" + else + s!"{message}\nExpected empty list but got: {repr list}" + .failure msg + +/-- Assert that a list contains an element -/ +def assertContains [BEq α] [Repr α] (list : List α) (element : α) (message : String := "") : AssertionResult := + if list.contains element then + .success + else + let msg := if message.isEmpty then + s!"Expected list to contain {repr element}\nList: {repr list}" + else + s!"{message}\nExpected list to contain {repr element}\nList: {repr list}" + .failure msg + +/-- Assert that a value is within a range (inclusive) -/ +def assertInRange [LE α] [DecidableRel (· ≤ · : α → α → Prop)] [Repr α] + (value : α) (min : α) (max : α) (message : String := "") : AssertionResult := + if min ≤ value ∧ value ≤ max then + .success + else + let msg := if message.isEmpty then + s!"Expected {repr value} to be in range [{repr min}, {repr max}]" + else + s!"{message}\nExpected {repr value} to be in range [{repr min}, {repr max}]" + .failure msg + +/-- Assert that an Except value is an error -/ +def assertError [Repr ε] [Repr α] (result : Except ε α) (message : String := "") : AssertionResult := + match result with + | .error _ => .success + | .ok val => + let msg := if message.isEmpty then + s!"Expected error but got Ok: {repr val}" + else + s!"{message}\nExpected error but got Ok: {repr val}" + .failure msg + +/-- Assert that an Except value is ok -/ +def assertOk [Repr ε] [Repr α] (result : Except ε α) (message : String := "") : AssertionResult := + match result with + | .ok _ => .success + | .error err => + let msg := if message.isEmpty then + s!"Expected Ok but got error: {repr err}" + else + s!"{message}\nExpected Ok but got error: {repr err}" + .failure msg + +/-- Assert that an IO action throws an error -/ +def assertThrows (action : IO α) (message : String := "") : IO AssertionResult := do + try + let _ ← action + let msg := if message.isEmpty then + "Expected IO action to throw an error, but it succeeded" + else + s!"{message}\nExpected IO action to throw an error, but it succeeded" + return .failure msg + catch _ => + return .success + +/-- Assert that an IO action succeeds (doesn't throw) -/ +def assertSucceeds (action : IO α) (message : String := "") : IO AssertionResult := do + try + let _ ← action + return .success + catch e => + let msg := if message.isEmpty then + s!"Expected IO action to succeed, but it threw: {e}" + else + s!"{message}\nExpected IO action to succeed, but it threw: {e}" + return .failure msg + +end LeanTest diff --git a/exercises/practice/list-ops/vendor/LeanTest/LeanTest/Test.lean b/exercises/practice/list-ops/vendor/LeanTest/LeanTest/Test.lean new file mode 100644 index 0000000..5ddbae5 --- /dev/null +++ b/exercises/practice/list-ops/vendor/LeanTest/LeanTest/Test.lean @@ -0,0 +1,130 @@ +/- +Test case and test suite management. +-/ + +import LeanTest.Assertions + +namespace LeanTest + +/-- A single test case -/ +structure TestCase where + description : String + test : IO AssertionResult + deriving Inhabited + +/-- Result of running a test -/ +structure TestResult where + description : String + result : AssertionResult + deriving Repr + +/-- A collection of tests (test suite) -/ +structure TestSuite where + name : String + tests : List TestCase + deriving Inhabited + +namespace TestSuite + +/-- Create an empty test suite -/ +def empty (name : String) : TestSuite := + { name := name, tests := [] } + +/-- Add a test to the suite -/ +def addTest (suite : TestSuite) (description : String) (test : IO AssertionResult) : TestSuite := + { suite with tests := suite.tests ++ [{ description := description, test := test }] } + +end TestSuite + +/-- Test statistics -/ +structure TestStats where + total : Nat + passed : Nat + failed : Nat + deriving Repr + +namespace TestStats + +def empty : TestStats := + { total := 0, passed := 0, failed := 0 } + +def addResult (stats : TestStats) (result : AssertionResult) : TestStats := + { total := stats.total + 1 + , passed := if result.isSuccess then stats.passed + 1 else stats.passed + , failed := if result.isSuccess then stats.failed else stats.failed + 1 + } + +end TestStats + +/-- ANSI color codes for terminal output -/ +def greenColor : String := "\x1b[32m" +def redColor : String := "\x1b[31m" +def yellowColor : String := "\x1b[33m" +def resetColor : String := "\x1b[0m" +def boldColor : String := "\x1b[1m" + +/-- Run a single test and print the result -/ +def runTest (testCase : TestCase) : IO TestResult := do + let result ← testCase.test + match result with + | .success => + IO.println s!" {greenColor}✓{resetColor} {testCase.description}" + | .failure msg => + IO.println s!" {redColor}✗{resetColor} {testCase.description}" + IO.println s!" {redColor}{msg}{resetColor}" + return { description := testCase.description, result := result } + +/-- Run all tests in a test suite -/ +def runTestSuite (suite : TestSuite) : IO TestStats := do + IO.println s!"\n{boldColor}{suite.name}{resetColor}" + let mut stats := TestStats.empty + + for testCase in suite.tests do + let result ← runTest testCase + stats := stats.addResult result.result + + return stats + +/-- Print test summary -/ +def printSummary (stats : TestStats) : IO Unit := do + IO.println "" + IO.println s!"{boldColor}Test Summary:{resetColor}" + IO.println s!" Total: {stats.total}" + IO.println s!" {greenColor}Passed: {stats.passed}{resetColor}" + + if stats.failed > 0 then + IO.println s!" {redColor}Failed: {stats.failed}{resetColor}" + IO.println s!"\n{redColor}FAILED{resetColor}" + else + IO.println s!"\n{greenColor}ALL TESTS PASSED{resetColor}" + +/-- Run multiple test suites -/ +def runTestSuites (suites : List TestSuite) : IO Unit := do + let mut totalStats := TestStats.empty + + for suite in suites do + let stats ← runTestSuite suite + totalStats := { + total := totalStats.total + stats.total, + passed := totalStats.passed + stats.passed, + failed := totalStats.failed + stats.failed + } + + printSummary totalStats + +/-- Run multiple test suites and return exit code (0 = all passed, 1 = some failed) -/ +def runTestSuitesWithExitCode (suites : List TestSuite) : IO UInt32 := do + let mut totalStats := TestStats.empty + + for suite in suites do + let stats ← runTestSuite suite + totalStats := { + total := totalStats.total + stats.total, + passed := totalStats.passed + stats.passed, + failed := totalStats.failed + stats.failed + } + + printSummary totalStats + return if totalStats.failed > 0 then 1 else 0 + +end LeanTest diff --git a/generators/Generator/Generator.lean b/generators/Generator/Generator.lean index 44e01eb..8cf7e4c 100644 --- a/generators/Generator/Generator.lean +++ b/generators/Generator/Generator.lean @@ -85,6 +85,7 @@ import Generator.AnagramGenerator import Generator.BobGenerator import Generator.MatchingBracketsGenerator import Generator.ReverseStringGenerator +import Generator.ListOpsGenerator import Std import Lean.Data.Json @@ -183,7 +184,8 @@ def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBod ("Anagram", (AnagramGenerator.genIntro, AnagramGenerator.genTestCase, AnagramGenerator.genEnd)), ("Bob", (BobGenerator.genIntro, BobGenerator.genTestCase, BobGenerator.genEnd)), ("MatchingBrackets", (MatchingBracketsGenerator.genIntro, MatchingBracketsGenerator.genTestCase, MatchingBracketsGenerator.genEnd)), - ("ReverseString", (ReverseStringGenerator.genIntro, ReverseStringGenerator.genTestCase, ReverseStringGenerator.genEnd)) + ("ReverseString", (ReverseStringGenerator.genIntro, ReverseStringGenerator.genTestCase, ReverseStringGenerator.genEnd)), + ("ListOps", (ListOpsGenerator.genIntro, ListOpsGenerator.genTestCase, ListOpsGenerator.genEnd)) ] end Generator diff --git a/generators/Generator/Generator/ListOpsGenerator.lean b/generators/Generator/Generator/ListOpsGenerator.lean new file mode 100644 index 0000000..ebb65a4 --- /dev/null +++ b/generators/Generator/Generator/ListOpsGenerator.lean @@ -0,0 +1,151 @@ +import Lean.Data.Json +import Std +import Helper + +open Lean +open Std +open Helper + +namespace ListOpsGenerator + +def genIntro (exercise : String) : String := s!"import LeanTest +import {exercise} + +open LeanTest + +def {exercise.decapitalize}Tests : TestSuite := + (TestSuite.empty \"{exercise}\")" + +def functionToLean (property : String) (funStr : String) : String := + match property, funStr with + | "filter", "\"(x) -> x modulo 2 == 1\"" => "(fun x => x % 2 == 1)" + | "map", "\"(x) -> x + 1\"" => "(· + 1)" + | "foldl", "\"(acc, el) -> el * acc\"" => "(fun acc el => el * acc)" + | "foldl", "\"(acc, el) -> el + acc\"" => "(fun acc el => el + acc)" + | "foldl", "\"(x, y) -> x / y\"" => "(· / ·)" + | "foldr", "\"(acc, el) -> el * acc\"" => "(fun el acc => el * acc)" + | "foldr", "\"(acc, el) -> el + acc\"" => "(fun el acc => el + acc)" + | "foldr", "\"(x, y) -> x / y\"" => "(· / ·)" + | _, _ => funStr + +def serializeIntList (json : Json) : String := + match json.getArr? with + | .error _ => s!"{json}" + | .ok arr => + if arr.isEmpty then "([] : List Int)" + else + let items := arr.map (fun j => s!"{j}") |>.toList + "[" ++ String.intercalate ", " items ++ "]" + +def serializeNestedList (json : Json) : String := + match json.getArr? with + | .error _ => s!"{json}" + | .ok arr => + if arr.isEmpty then "([] : List (List Int))" + else + let items := arr.map (fun j => serializeIntList j) |>.toList + "[" ++ String.intercalate ", " items ++ "]" + +def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String := + let description := case.get! "description" |> (·.compress) + let property := getFunName (case.get! "property") + let input := case.get! "input" + match property with + | "append" => + let list1 := input.getObjValD "list1" + let list2 := input.getObjValD "list2" + let expected := case.get! "expected" + let call := s!"(ListOps.append {serializeIntList list1} {serializeIntList list2})" + s!" + |>.addTest {description} (do + return assertEqual {serializeIntList expected} {call})" + | "concat" => + let lists := input.getObjValD "lists" + let expected := case.get! "expected" + let call := s!"(ListOps.concat {serializeNestedList lists})" + s!" + |>.addTest {description} (do + return assertEqual {serializeIntList expected} {call})" + | "filter" => + let list := input.getObjValD "list" + let funJson := input.getObjValD "function" + let expected := case.get! "expected" + let leanFun := functionToLean property funJson.compress + let call := s!"(ListOps.filter {leanFun} {serializeIntList list})" + s!" + |>.addTest {description} (do + return assertEqual {serializeIntList expected} {call})" + | "length" => + let list := input.getObjValD "list" + let expected := case.get! "expected" + let call := s!"(ListOps.length {serializeIntList list})" + s!" + |>.addTest {description} (do + return assertEqual {expected} {call})" + | "map" => + let list := input.getObjValD "list" + let funJson := input.getObjValD "function" + let expected := case.get! "expected" + let leanFun := functionToLean property funJson.compress + let call := s!"(ListOps.map {leanFun} {serializeIntList list})" + s!" + |>.addTest {description} (do + return assertEqual {serializeIntList expected} {call})" + | "foldl" => + let list := input.getObjValD "list" + let initial := case.get! "input" |> (·.getObjValD "initial") + let funJson := input.getObjValD "function" + let expected := case.get! "expected" + let leanFun := functionToLean property funJson.compress + let call := s!"(ListOps.foldl {leanFun} {initial} {serializeIntList list})" + s!" + |>.addTest {description} (do + return assertEqual {expected} {call})" + | "foldr" => + let list := input.getObjValD "list" + let initial := case.get! "input" |> (·.getObjValD "initial") + let funJson := input.getObjValD "function" + let expected := case.get! "expected" + let leanFun := functionToLean property funJson.compress + let call := s!"(ListOps.foldr {leanFun} {initial} {serializeIntList list})" + s!" + |>.addTest {description} (do + return assertEqual {expected} {call})" + | "reverse" => + let list := input.getObjValD "list" + let expected := case.get! "expected" + -- Check if it's a list of lists + match list.getArr? with + | .error _ => + let call := s!"(ListOps.reverse {serializeIntList list})" + s!" + |>.addTest {description} (do + return assertEqual {serializeIntList expected} {call})" + | .ok arr => + if arr.isEmpty then + let call := s!"(ListOps.reverse {serializeIntList list})" + s!" + |>.addTest {description} (do + return assertEqual {serializeIntList expected} {call})" + else + match arr[0]!.getArr? with + | .ok _ => + let call := s!"(ListOps.reverse {serializeNestedList list})" + s!" + |>.addTest {description} (do + return assertEqual {serializeNestedList expected} {call})" + | .error _ => + let call := s!"(ListOps.reverse {serializeIntList list})" + s!" + |>.addTest {description} (do + return assertEqual {serializeIntList expected} {call})" + | _ => "" + +def genEnd (exercise : String) : String := + s!" + +def main : IO UInt32 := do + runTestSuitesWithExitCode [{exercise.decapitalize}Tests] +" + +end ListOpsGenerator From f3f63f46d6f135485dc56b527be146478abfe365 Mon Sep 17 00:00:00 2001 From: jojo8356 Date: Tue, 24 Mar 2026 21:56:39 +0100 Subject: [PATCH 2/4] Fix author username in config.json Co-Authored-By: Claude Opus 4.6 (1M context) --- exercises/practice/list-ops/.meta/config.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/exercises/practice/list-ops/.meta/config.json b/exercises/practice/list-ops/.meta/config.json index c806a49..e074c83 100644 --- a/exercises/practice/list-ops/.meta/config.json +++ b/exercises/practice/list-ops/.meta/config.json @@ -1,6 +1,6 @@ { "authors": [ - "oxe-i" + "jojo8356" ], "files": { "solution": [ From 66eca585e24341b0a61746844771c163bac31764 Mon Sep 17 00:00:00 2001 From: jojo8356 Date: Wed, 25 Mar 2026 08:32:15 +0100 Subject: [PATCH 3/4] Reorder list-ops exercise alphabetically in config.json --- config.json | 16 ++++++++-------- .../.approaches/config.json | 5 +++-- 2 files changed, 11 insertions(+), 10 deletions(-) diff --git a/config.json b/config.json index 6f05403..a7b2801 100644 --- a/config.json +++ b/config.json @@ -234,14 +234,6 @@ "prerequisites": [], "difficulty": 3 }, - { - "slug": "list-ops", - "name": "List Ops", - "uuid": "e6e4e258-e669-4875-afce-c6a65405b3d0", - "practices": [], - "prerequisites": [], - "difficulty": 3 - }, { "slug": "gigasecond", "name": "Gigasecond", @@ -266,6 +258,14 @@ "prerequisites": [], "difficulty": 3 }, + { + "slug": "list-ops", + "name": "List Ops", + "uuid": "e6e4e258-e669-4875-afce-c6a65405b3d0", + "practices": [], + "prerequisites": [], + "difficulty": 3 + }, { "slug": "matrix", "name": "Matrix", diff --git a/exercises/practice/difference-of-squares/.approaches/config.json b/exercises/practice/difference-of-squares/.approaches/config.json index 650d318..9a043ac 100644 --- a/exercises/practice/difference-of-squares/.approaches/config.json +++ b/exercises/practice/difference-of-squares/.approaches/config.json @@ -1,7 +1,8 @@ { "introduction": { - "authors": ["oxe-i"], - "contributors": [] + "authors": [ + "oxe-i" + ] }, "approaches": [ { From ada1065cbf2263848e310426a4c85dcb63112f99 Mon Sep 17 00:00:00 2001 From: pj509414 Date: Wed, 25 Mar 2026 13:38:07 +0100 Subject: [PATCH 4/4] Add foldl/foldr power (^) extra test cases --- exercises/practice/list-ops/.meta/extra.json | 28 +++++++++++++++++++ exercises/practice/list-ops/ListOpsTest.lean | 4 +++ .../Generator/Generator/ListOpsGenerator.lean | 2 ++ 3 files changed, 34 insertions(+) create mode 100644 exercises/practice/list-ops/.meta/extra.json diff --git a/exercises/practice/list-ops/.meta/extra.json b/exercises/practice/list-ops/.meta/extra.json new file mode 100644 index 0000000..67248d7 --- /dev/null +++ b/exercises/practice/list-ops/.meta/extra.json @@ -0,0 +1,28 @@ +{ + "exercise": "list-ops", + "comments": [ + "Extra test cases for the Lean track to test power function with foldl/foldr." + ], + "cases": [ + { + "description": "folds (reduces) the given list from the left with a function -> direction dependent function applied to non-empty list (power)", + "property": "foldl", + "input": { + "list": [3, 2], + "initial": 2, + "function": "(acc, el) -> el ^ acc" + }, + "expected": 512 + }, + { + "description": "folds (reduces) the given list from the right with a function -> direction dependent function applied to non-empty list (power)", + "property": "foldr", + "input": { + "list": [3, 2], + "initial": 2, + "function": "(acc, el) -> el ^ acc" + }, + "expected": 81 + } + ] +} diff --git a/exercises/practice/list-ops/ListOpsTest.lean b/exercises/practice/list-ops/ListOpsTest.lean index e871886..a2b86bd 100644 --- a/exercises/practice/list-ops/ListOpsTest.lean +++ b/exercises/practice/list-ops/ListOpsTest.lean @@ -43,6 +43,10 @@ def listOpsTests : TestSuite := return assertEqual 15 (ListOps.foldr (fun el acc => el + acc) 5 [1, 2, 3, 4])) |>.addTest "folds (reduces) the given list from the right with a function -> direction dependent function applied to non-empty list" (do return assertEqual 2 (ListOps.foldr (· / ·) 5 [2, 5])) + |>.addTest "folds (reduces) the given list from the left with a function -> direction dependent function applied to non-empty list (power)" (do + return assertEqual (512 : Int) (ListOps.foldl (fun acc el => el ^ acc.toNat) (2 : Int) [(3 : Int), 2])) + |>.addTest "folds (reduces) the given list from the right with a function -> direction dependent function applied to non-empty list (power)" (do + return assertEqual (81 : Int) (ListOps.foldr (fun el acc => el ^ acc.toNat) (2 : Int) [(3 : Int), 2])) |>.addTest "reverse the elements of the list -> empty list" (do return assertEqual ([] : List Int) (ListOps.reverse ([] : List Int))) |>.addTest "reverse the elements of the list -> non-empty list" (do diff --git a/generators/Generator/Generator/ListOpsGenerator.lean b/generators/Generator/Generator/ListOpsGenerator.lean index ebb65a4..30d15df 100644 --- a/generators/Generator/Generator/ListOpsGenerator.lean +++ b/generators/Generator/Generator/ListOpsGenerator.lean @@ -26,6 +26,8 @@ def functionToLean (property : String) (funStr : String) : String := | "foldr", "\"(acc, el) -> el * acc\"" => "(fun el acc => el * acc)" | "foldr", "\"(acc, el) -> el + acc\"" => "(fun el acc => el + acc)" | "foldr", "\"(x, y) -> x / y\"" => "(· / ·)" + | "foldl", "\"(acc, el) -> el ^ acc\"" => "(fun acc el => el ^ acc.toNat)" + | "foldr", "\"(acc, el) -> el ^ acc\"" => "(fun el acc => el ^ acc.toNat)" | _, _ => funStr def serializeIntList (json : Json) : String :=