diff --git a/config.json b/config.json index e0870f0..01866f5 100644 --- a/config.json +++ b/config.json @@ -586,6 +586,14 @@ "prerequisites": [], "difficulty": 7 }, + { + "slug": "custom-set", + "name": "Custom Set", + "uuid": "d643def0-b87f-44b9-ab31-787d94d4f6a0", + "practices": [], + "prerequisites": [], + "difficulty": 7 + }, { "slug": "pythagorean-triplet", "name": "Pythagorean Triplet", diff --git a/exercises/practice/custom-set/.docs/instructions.md b/exercises/practice/custom-set/.docs/instructions.md new file mode 100644 index 0000000..33b90e2 --- /dev/null +++ b/exercises/practice/custom-set/.docs/instructions.md @@ -0,0 +1,7 @@ +# Instructions + +Create a custom set type. + +Sometimes it is necessary to define a custom data structure of some type, like a set. +In this exercise you will define your own set. +How it works internally doesn't matter, as long as it behaves like a set of unique elements. diff --git a/exercises/practice/custom-set/.meta/Example.lean b/exercises/practice/custom-set/.meta/Example.lean new file mode 100644 index 0000000..fc227d7 --- /dev/null +++ b/exercises/practice/custom-set/.meta/Example.lean @@ -0,0 +1,78 @@ +namespace CustomSet + +abbrev Size := Nat + +inductive Set where + | nil : Set + | node : Size → Nat → Set → Set → Set + deriving Repr, Inhabited + +instance : EmptyCollection Set := + ⟨ .nil ⟩ -- takes care of ∅ + +private def Set.size : Set → Size + | .nil => 0 + | .node s _ _ _ => s + +private def Set.contains : Set → Nat → Bool + | .nil, _ => false + | .node _ x l r, e => e == x || if e < x then l.contains e else r.contains e + +private def Set.foldl {α} (fn : α → Nat → α) (init : α) (set : Set) : α := + match set with + | .nil => init + | .node _ x l r => + let leftAcc := l.foldl fn init + let acc := fn leftAcc x + r.foldl fn acc + +instance : BEq Set where -- takes care of == and != + beq s1 s2 := s1.size == s2.size && s1.foldl (fun acc x => acc && s2.contains x) true + +instance : Membership Nat Set where -- takes care of ∈ and ∉ + mem s n := s.contains n + +instance (a : Nat) (s : Set) : Decidable (a ∈ s) := by + simp [Membership.mem] + exact inferInstance + +private def Set.subset (set1 set2 : Set) : Bool := + set1.foldl (fun acc x => acc && set2.contains x) true + +instance : HasSubset Set where + Subset s1 s2 := s1.subset s2 + +instance (s1 s2 : Set) : Decidable (s1 ⊆ s2) := by + simp [HasSubset.Subset] + exact inferInstance + +notation a " ⊈ " b => ¬(a ⊆ b) + +private def Set.addHelper (e : Nat) (s : Set) : Set := + match s with + | .nil => .node 1 e .nil .nil + | .node s x l r => + if e < x + then Set.node (s + 1) x (l.addHelper e) r + else Set.node (s + 1) x l (r.addHelper e) + +def Set.add (elem : Nat) (set : Set) : Set := + if elem ∈ set then set + else set.addHelper elem + +def Set.ofList (xs : List Nat) : Set := + xs.foldl (fun acc x => acc.add x) ∅ + +instance : Inter Set where -- takes care of ∩ + inter s1 s2 := s1.foldl (fun acc x => if s2.contains x then acc.add x else acc) ∅ + +instance : Union Set where -- takes care of ∪ + union s1 s2 := s1.foldl (fun acc x => acc.add x) s2 + +instance : SDiff Set where -- takes care of \ + sdiff s1 s2 := s1.foldl (fun acc x => if s2.contains x then acc else acc.add x) ∅ + +def Set.disjoint (set1 set2 : Set) : Bool := + set1.foldl (fun acc x => acc && !set2.contains x) true + +end CustomSet diff --git a/exercises/practice/custom-set/.meta/config.json b/exercises/practice/custom-set/.meta/config.json new file mode 100644 index 0000000..d234818 --- /dev/null +++ b/exercises/practice/custom-set/.meta/config.json @@ -0,0 +1,17 @@ +{ + "authors": [ + "oxe-i" + ], + "files": { + "solution": [ + "CustomSet.lean" + ], + "test": [ + "CustomSetTest.lean" + ], + "example": [ + ".meta/Example.lean" + ] + }, + "blurb": "Create a custom set type." +} diff --git a/exercises/practice/custom-set/.meta/tests.toml b/exercises/practice/custom-set/.meta/tests.toml new file mode 100644 index 0000000..430c139 --- /dev/null +++ b/exercises/practice/custom-set/.meta/tests.toml @@ -0,0 +1,130 @@ +# 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. + +[20c5f855-f83a-44a7-abdd-fe75c6cf022b] +description = "Returns true if the set contains no elements -> sets with no elements are empty" + +[d506485d-5706-40db-b7d8-5ceb5acf88d2] +description = "Returns true if the set contains no elements -> sets with elements are not empty" + +[759b9740-3417-44c3-8ca3-262b3c281043] +description = "Sets can report if they contain an element -> nothing is contained in an empty set" + +[f83cd2d1-2a85-41bc-b6be-80adbff4be49] +description = "Sets can report if they contain an element -> when the element is in the set" + +[93423fc0-44d0-4bc0-a2ac-376de8d7af34] +description = "Sets can report if they contain an element -> when the element is not in the set" + +[c392923a-637b-4495-b28e-34742cd6157a] +description = "A set is a subset if all of its elements are contained in the other set -> empty set is a subset of another empty set" + +[5635b113-be8c-4c6f-b9a9-23c485193917] +description = "A set is a subset if all of its elements are contained in the other set -> empty set is a subset of non-empty set" + +[832eda58-6d6e-44e2-92c2-be8cf0173cee] +description = "A set is a subset if all of its elements are contained in the other set -> non-empty set is not a subset of empty set" + +[c830c578-8f97-4036-b082-89feda876131] +description = "A set is a subset if all of its elements are contained in the other set -> set is a subset of set with exact same elements" + +[476a4a1c-0fd1-430f-aa65-5b70cbc810c5] +description = "A set is a subset if all of its elements are contained in the other set -> set is a subset of larger set with same elements" + +[d2498999-3e46-48e4-9660-1e20c3329d3d] +description = "A set is a subset if all of its elements are contained in the other set -> set is not a subset of set that does not contain its elements" + +[7d38155e-f472-4a7e-9ad8-5c1f8f95e4cc] +description = "Sets are disjoint if they share no elements -> the empty set is disjoint with itself" + +[7a2b3938-64b6-4b32-901a-fe16891998a6] +description = "Sets are disjoint if they share no elements -> empty set is disjoint with non-empty set" + +[589574a0-8b48-48ea-88b0-b652c5fe476f] +description = "Sets are disjoint if they share no elements -> non-empty set is disjoint with empty set" + +[febeaf4f-f180-4499-91fa-59165955a523] +description = "Sets are disjoint if they share no elements -> sets are not disjoint if they share an element" + +[0de20d2f-c952-468a-88c8-5e056740f020] +description = "Sets are disjoint if they share no elements -> sets are disjoint if they share no elements" + +[4bd24adb-45da-4320-9ff6-38c044e9dff8] +description = "Sets with the same elements are equal -> empty sets are equal" + +[f65c0a0e-6632-4b2d-b82c-b7c6da2ec224] +description = "Sets with the same elements are equal -> empty set is not equal to non-empty set" + +[81e53307-7683-4b1e-a30c-7e49155fe3ca] +description = "Sets with the same elements are equal -> non-empty set is not equal to empty set" + +[d57c5d7c-a7f3-48cc-a162-6b488c0fbbd0] +description = "Sets with the same elements are equal -> sets with the same elements are equal" + +[dd61bafc-6653-42cc-961a-ab071ee0ee85] +description = "Sets with the same elements are equal -> sets with different elements are not equal" + +[06059caf-9bf4-425e-aaff-88966cb3ea14] +description = "Sets with the same elements are equal -> set is not equal to larger set with same elements" + +[d4a1142f-09aa-4df9-8b83-4437dcf7ec24] +description = "Sets with the same elements are equal -> set is equal to a set constructed from an array with duplicates" + +[8a677c3c-a658-4d39-bb88-5b5b1a9659f4] +description = "Unique elements can be added to a set -> add to empty set" + +[0903dd45-904d-4cf2-bddd-0905e1a8d125] +description = "Unique elements can be added to a set -> add to non-empty set" + +[b0eb7bb7-5e5d-4733-b582-af771476cb99] +description = "Unique elements can be added to a set -> adding an existing element does not change the set" + +[893d5333-33b8-4151-a3d4-8f273358208a] +description = "Intersection returns a set of all shared elements -> intersection of two empty sets is an empty set" + +[d739940e-def2-41ab-a7bb-aaf60f7d782c] +description = "Intersection returns a set of all shared elements -> intersection of an empty set and non-empty set is an empty set" + +[3607d9d8-c895-4d6f-ac16-a14956e0a4b7] +description = "Intersection returns a set of all shared elements -> intersection of a non-empty set and an empty set is an empty set" + +[b5120abf-5b5e-41ab-aede-4de2ad85c34e] +description = "Intersection returns a set of all shared elements -> intersection of two sets with no shared elements is an empty set" + +[af21ca1b-fac9-499c-81c0-92a591653d49] +description = "Intersection returns a set of all shared elements -> intersection of two sets with shared elements is a set of the shared elements" + +[c5e6e2e4-50e9-4bc2-b89f-c518f015b57e] +description = "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference of two empty sets is an empty set" + +[2024cc92-5c26-44ed-aafd-e6ca27d6fcd2] +description = "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference of empty set and non-empty set is an empty set" + +[e79edee7-08aa-4c19-9382-f6820974b43e] +description = "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference of a non-empty set and an empty set is the non-empty set" + +[c5ac673e-d707-4db5-8d69-7082c3a5437e] +description = "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference of two non-empty sets is a set of elements that are only in the first set" + +[20d0a38f-7bb7-4c4a-ac15-90c7392ecf2b] +description = "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference removes all duplicates in the first set" + +[c45aed16-5494-455a-9033-5d4c93589dc6] +description = "Union returns a set of all elements in either set -> union of empty sets is an empty set" + +[9d258545-33c2-4fcb-a340-9f8aa69e7a41] +description = "Union returns a set of all elements in either set -> union of an empty set and non-empty set is the non-empty set" + +[3aade50c-80c7-4db8-853d-75bac5818b83] +description = "Union returns a set of all elements in either set -> union of a non-empty set and empty set is the non-empty set" + +[a00bb91f-c4b4-4844-8f77-c73e2e9df77c] +description = "Union returns a set of all elements in either set -> union of non-empty sets contains all unique elements" diff --git a/exercises/practice/custom-set/CustomSet.lean b/exercises/practice/custom-set/CustomSet.lean new file mode 100644 index 0000000..f8941ba --- /dev/null +++ b/exercises/practice/custom-set/CustomSet.lean @@ -0,0 +1,21 @@ +namespace CustomSet + +/- + Define here a Set type + + It must have operators defined with the following semantics: + * ∈, ∉ : an element is, or is not, in a Set + * ⊆, ⊈ : a Set is, or is not, a subset of another + * ==, != : two Sets have, or don't have, the same elements + * ∩ : gets the intersection of two Sets + * ∪ : gets the union of two Sets + * \ : gets the difference of two Sets + * ∅ : references an empty Set + + In addition, at least three other functions must be defined: + * Set.ofList, that takes a List Nat and returns a Set + * Set.add, that adds a Nat to a Set, returning the new Set + * Set.disjoint, that checks if two Sets are, or are not, disjoint +-/ + +end CustomSet diff --git a/exercises/practice/custom-set/CustomSetTest.lean b/exercises/practice/custom-set/CustomSetTest.lean new file mode 100644 index 0000000..1f5e838 --- /dev/null +++ b/exercises/practice/custom-set/CustomSetTest.lean @@ -0,0 +1,90 @@ +import LeanTest +import CustomSet + +open LeanTest + +def customSetTests : TestSuite := + (TestSuite.empty "CustomSet") + |>.addTest "Returns true if the set contains no elements -> sets with no elements are empty" (do + return assertEqual ∅ <| CustomSet.Set.ofList []) + |>.addTest "Returns true if the set contains no elements -> sets with elements are not empty" (do + return assertNotEqual ∅ <| CustomSet.Set.ofList [1]) + |>.addTest "Sets can report if they contain an element -> nothing is contained in an empty set" (do + return assert <| decide <| 1 ∉ CustomSet.Set.ofList []) + |>.addTest "Sets can report if they contain an element -> when the element is in the set" (do + return assert <| decide <| 1 ∈ CustomSet.Set.ofList [1, 2, 3]) + |>.addTest "Sets can report if they contain an element -> when the element is not in the set" (do + return assert <| decide <| 4 ∉ CustomSet.Set.ofList [1, 2, 3]) + |>.addTest "A set is a subset if all of its elements are contained in the other set -> empty set is a subset of another empty set" (do + return assert <| decide <| CustomSet.Set.ofList [] ⊆ CustomSet.Set.ofList []) + |>.addTest "A set is a subset if all of its elements are contained in the other set -> empty set is a subset of non-empty set" (do + return assert <| decide <| CustomSet.Set.ofList [] ⊆ CustomSet.Set.ofList [1]) + |>.addTest "A set is a subset if all of its elements are contained in the other set -> non-empty set is not a subset of empty set" (do + return assert <| decide <| CustomSet.Set.ofList [1] ⊈ CustomSet.Set.ofList []) + |>.addTest "A set is a subset if all of its elements are contained in the other set -> set is a subset of set with exact same elements" (do + return assert <| decide <| CustomSet.Set.ofList [1, 2, 3] ⊆ CustomSet.Set.ofList [1, 2, 3]) + |>.addTest "A set is a subset if all of its elements are contained in the other set -> set is a subset of larger set with same elements" (do + return assert <| decide <| CustomSet.Set.ofList [1, 2, 3] ⊆ CustomSet.Set.ofList [4, 1, 2, 3]) + |>.addTest "A set is a subset if all of its elements are contained in the other set -> set is not a subset of set that does not contain its elements" (do + return assert <| decide <| CustomSet.Set.ofList [1, 2, 3] ⊈ CustomSet.Set.ofList [4, 1, 3]) + |>.addTest "Sets are disjoint if they share no elements -> the empty set is disjoint with itself" (do + return assertTrue <| (CustomSet.Set.ofList []).disjoint <| CustomSet.Set.ofList []) + |>.addTest "Sets are disjoint if they share no elements -> empty set is disjoint with non-empty set" (do + return assertTrue <| (CustomSet.Set.ofList []).disjoint <| CustomSet.Set.ofList [1]) + |>.addTest "Sets are disjoint if they share no elements -> non-empty set is disjoint with empty set" (do + return assertTrue <| (CustomSet.Set.ofList [1]).disjoint <| CustomSet.Set.ofList []) + |>.addTest "Sets are disjoint if they share no elements -> sets are not disjoint if they share an element" (do + return assertFalse <| (CustomSet.Set.ofList [1, 2]).disjoint <| CustomSet.Set.ofList [2, 3]) + |>.addTest "Sets are disjoint if they share no elements -> sets are disjoint if they share no elements" (do + return assertTrue <| (CustomSet.Set.ofList [1, 2]).disjoint <| CustomSet.Set.ofList [3, 4]) + |>.addTest "Sets with the same elements are equal -> empty sets are equal" (do + return assert <| CustomSet.Set.ofList [] == CustomSet.Set.ofList []) + |>.addTest "Sets with the same elements are equal -> empty set is not equal to non-empty set" (do + return assert <| CustomSet.Set.ofList [] != CustomSet.Set.ofList [1, 2, 3]) + |>.addTest "Sets with the same elements are equal -> non-empty set is not equal to empty set" (do + return assert <| CustomSet.Set.ofList [1, 2, 3] != CustomSet.Set.ofList []) + |>.addTest "Sets with the same elements are equal -> sets with the same elements are equal" (do + return assert <| CustomSet.Set.ofList [1, 2] == CustomSet.Set.ofList [2, 1]) + |>.addTest "Sets with the same elements are equal -> sets with different elements are not equal" (do + return assert <| CustomSet.Set.ofList [1, 2, 3] != CustomSet.Set.ofList [1, 2, 4]) + |>.addTest "Sets with the same elements are equal -> set is not equal to larger set with same elements" (do + return assert <| CustomSet.Set.ofList [1, 2, 3] != CustomSet.Set.ofList [1, 2, 3, 4]) + |>.addTest "Sets with the same elements are equal -> set is equal to a set constructed from an array with duplicates" (do + return assert <| CustomSet.Set.ofList [1] == CustomSet.Set.ofList [1, 1]) + |>.addTest "Unique elements can be added to a set -> add to empty set" (do + return assertEqual (CustomSet.Set.ofList [3]) <| (CustomSet.Set.ofList []).add 3) + |>.addTest "Unique elements can be added to a set -> add to non-empty set" (do + return assertEqual (CustomSet.Set.ofList [1, 2, 3, 4]) <| (CustomSet.Set.ofList [1, 2, 4]).add 3) + |>.addTest "Unique elements can be added to a set -> adding an existing element does not change the set" (do + return assertEqual (CustomSet.Set.ofList [1, 2, 3]) <| (CustomSet.Set.ofList [1, 2, 3]).add 3) + |>.addTest "Intersection returns a set of all shared elements -> intersection of two empty sets is an empty set" (do + return assertEqual (CustomSet.Set.ofList []) <| CustomSet.Set.ofList [] ∩ CustomSet.Set.ofList []) + |>.addTest "Intersection returns a set of all shared elements -> intersection of an empty set and non-empty set is an empty set" (do + return assertEqual (CustomSet.Set.ofList []) <| CustomSet.Set.ofList [] ∩ CustomSet.Set.ofList [3, 2, 5]) + |>.addTest "Intersection returns a set of all shared elements -> intersection of a non-empty set and an empty set is an empty set" (do + return assertEqual (CustomSet.Set.ofList []) <| CustomSet.Set.ofList [1, 2, 3, 4] ∩ CustomSet.Set.ofList []) + |>.addTest "Intersection returns a set of all shared elements -> intersection of two sets with no shared elements is an empty set" (do + return assertEqual (CustomSet.Set.ofList []) <| CustomSet.Set.ofList [1, 2, 3] ∩ CustomSet.Set.ofList [4, 5, 6]) + |>.addTest "Intersection returns a set of all shared elements -> intersection of two sets with shared elements is a set of the shared elements" (do + return assertEqual (CustomSet.Set.ofList [2, 3]) <| CustomSet.Set.ofList [1, 2, 3, 4] ∩ CustomSet.Set.ofList [3, 2, 5]) + |>.addTest "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference of two empty sets is an empty set" (do + return assertEqual (CustomSet.Set.ofList []) <| CustomSet.Set.ofList [] \ CustomSet.Set.ofList []) + |>.addTest "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference of empty set and non-empty set is an empty set" (do + return assertEqual (CustomSet.Set.ofList []) <| CustomSet.Set.ofList [] \ CustomSet.Set.ofList [3, 2, 5]) + |>.addTest "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference of a non-empty set and an empty set is the non-empty set" (do + return assertEqual (CustomSet.Set.ofList [1, 2, 3, 4]) <| CustomSet.Set.ofList [1, 2, 3, 4] \ CustomSet.Set.ofList []) + |>.addTest "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference of two non-empty sets is a set of elements that are only in the first set" (do + return assertEqual (CustomSet.Set.ofList [1, 3]) <| CustomSet.Set.ofList [3, 2, 1] \ CustomSet.Set.ofList [2, 4]) + |>.addTest "Difference (or Complement) of a set is a set of all elements that are only in the first set -> difference removes all duplicates in the first set" (do + return assertEqual (CustomSet.Set.ofList []) <| CustomSet.Set.ofList [1, 1] \ CustomSet.Set.ofList [1]) + |>.addTest "Union returns a set of all elements in either set -> union of empty sets is an empty set" (do + return assertEqual (CustomSet.Set.ofList []) <| CustomSet.Set.ofList [] ∪ CustomSet.Set.ofList []) + |>.addTest "Union returns a set of all elements in either set -> union of an empty set and non-empty set is the non-empty set" (do + return assertEqual (CustomSet.Set.ofList [2]) <| CustomSet.Set.ofList [] ∪ CustomSet.Set.ofList [2]) + |>.addTest "Union returns a set of all elements in either set -> union of a non-empty set and empty set is the non-empty set" (do + return assertEqual (CustomSet.Set.ofList [1, 3]) <| CustomSet.Set.ofList [1, 3] ∪ CustomSet.Set.ofList []) + |>.addTest "Union returns a set of all elements in either set -> union of non-empty sets contains all unique elements" (do + return assertEqual (CustomSet.Set.ofList [3, 2, 1]) <| CustomSet.Set.ofList [1, 3] ∪ CustomSet.Set.ofList [2, 3]) + +def main : IO UInt32 := do + runTestSuitesWithExitCode [customSetTests] diff --git a/exercises/practice/custom-set/lakefile.toml b/exercises/practice/custom-set/lakefile.toml new file mode 100644 index 0000000..542aa99 --- /dev/null +++ b/exercises/practice/custom-set/lakefile.toml @@ -0,0 +1,15 @@ +name = "custom-set" +version = "0.1.0" +defaultTargets = ["CustomSetTest"] +testDriver = "CustomSetTest" + +[[lean_lib]] +name = "LeanTest" +srcDir = "vendor/LeanTest" + +[[lean_lib]] +name = "CustomSet" + +[[lean_exe]] +name = "CustomSetTest" +root = "CustomSetTest" diff --git a/exercises/practice/custom-set/lean-toolchain b/exercises/practice/custom-set/lean-toolchain new file mode 100644 index 0000000..370b26d --- /dev/null +++ b/exercises/practice/custom-set/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.25.2 diff --git a/exercises/practice/custom-set/vendor/LeanTest/LeanTest.lean b/exercises/practice/custom-set/vendor/LeanTest/LeanTest.lean new file mode 100644 index 0000000..012ba20 --- /dev/null +++ b/exercises/practice/custom-set/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/custom-set/vendor/LeanTest/LeanTest/Assertions.lean b/exercises/practice/custom-set/vendor/LeanTest/LeanTest/Assertions.lean new file mode 100644 index 0000000..60e4ad8 --- /dev/null +++ b/exercises/practice/custom-set/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/custom-set/vendor/LeanTest/LeanTest/Test.lean b/exercises/practice/custom-set/vendor/LeanTest/LeanTest/Test.lean new file mode 100644 index 0000000..5ddbae5 --- /dev/null +++ b/exercises/practice/custom-set/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 5a7ae15..63fb676 100644 --- a/generators/Generator/Generator.lean +++ b/generators/Generator/Generator.lean @@ -1,3 +1,4 @@ +import Generator.CustomSetGenerator import Generator.WordCountGenerator import Generator.SgfParsingGenerator import Generator.DndCharacterGenerator @@ -95,6 +96,7 @@ abbrev endBodyGenerator := String -> String def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBodyGenerator) := Std.HashMap.ofList [ + ("CustomSet", (CustomSetGenerator.genIntro, CustomSetGenerator.genTestCase, CustomSetGenerator.genEnd)), ("WordCount", (WordCountGenerator.genIntro, WordCountGenerator.genTestCase, WordCountGenerator.genEnd)), ("SgfParsing", (SgfParsingGenerator.genIntro, SgfParsingGenerator.genTestCase, SgfParsingGenerator.genEnd)), ("DndCharacter", (DndCharacterGenerator.genIntro, DndCharacterGenerator.genTestCase, DndCharacterGenerator.genEnd)), diff --git a/generators/Generator/Generator/CustomSetGenerator.lean b/generators/Generator/Generator/CustomSetGenerator.lean new file mode 100644 index 0000000..086f397 --- /dev/null +++ b/generators/Generator/Generator/CustomSetGenerator.lean @@ -0,0 +1,103 @@ +import Lean.Data.Json +import Std +import Helper + +open Lean +open Std +open Helper + +namespace CustomSetGenerator + +def genIntro (exercise : String) : String := s!"import LeanTest +import {exercise} + +open LeanTest + +def {exercise.decapitalize}Tests : TestSuite := + (TestSuite.empty \"{exercise}\")" + +def operatorsBool : Std.HashMap String (Std.HashMap Bool String) := .ofList [ + ("contains", .ofList [(true, "∈"), (false, "∉")]), + ("subset", .ofList [(true, "⊆"), (false, "⊈")]), +] + +def operatorsSet : Std.HashMap String String := .ofList [ + ("intersection", "∩"), + ("union", "∪"), + ("difference", "\\") +] + +def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String := + let input := case.get! "input" + let expected := case.get! "expected" + let description := case.get! "description" + |> (·.compress) + let funName := getFunName (case.get! "property") + match funName with + | "empty" => + let equal := match getOk expected.getBool? with + | true => "Equal" + | false => "NotEqual" + s!" + |>.addTest {description} (do + return assert{equal} ∅ <| {exercise}.Set.ofList {insertAllInputs input})" + | "contains" => + let set := input.getObjValD "set" + let elem := input.getObjValD "element" + let operator := operatorsBool[funName]![getOk expected.getBool?]! + s!" + |>.addTest {description} (do + return assert <| decide <| {elem} {operator} {exercise}.Set.ofList {set})" + | "disjoint" => + let set1 := input.getObjValD "set1" + let set2 := input.getObjValD "set2" + let result := s!"{getOk expected.getBool?}".capitalize + s!" + |>.addTest {description} (do + return assert{result} <| ({exercise}.Set.ofList {set1}).disjoint <| {exercise}.Set.ofList {set2})" + | "equal" => + let set1 := input.getObjValD "set1" + let set2 := input.getObjValD "set2" + match getOk expected.getBool? with + | true => + s!" + |>.addTest {description} (do + return assert <| {exercise}.Set.ofList {set1} == {exercise}.Set.ofList {set2})" + | false => + s!" + |>.addTest {description} (do + return assert <| {exercise}.Set.ofList {set1} != {exercise}.Set.ofList {set2})" + | "add" => + let set := input.getObjValD "set" + let elem := input.getObjValD "element" + let result := s!"({exercise}.Set.ofList {expected})" + s!" + |>.addTest {description} (do + return assertEqual {result} <| ({exercise}.Set.ofList {set}).add {elem})" + | "subset" => + let set1 := input.getObjValD "set1" + let set2 := input.getObjValD "set2" + let operator := operatorsBool[funName]![getOk expected.getBool?]! + s!" + |>.addTest {description} (do + return assert <| decide <| {exercise}.Set.ofList {set1} {operator} {exercise}.Set.ofList {set2})" + | "intersection" + | "difference" + | "union" => + let set1 := input.getObjValD "set1" + let set2 := input.getObjValD "set2" + let operator := operatorsSet[funName]! + let result := s!"({exercise}.Set.ofList {expected})" + s!" + |>.addTest {description} (do + return assertEqual {result} <| {exercise}.Set.ofList {set1} {operator} {exercise}.Set.ofList {set2})" + | _ => "" + +def genEnd (exercise : String) : String := + s!" + +def main : IO UInt32 := do + runTestSuitesWithExitCode [{exercise.decapitalize}Tests] +" + +end CustomSetGenerator