From e7d7c16811f7a776e0cc2e8080db3eda0d68fdae Mon Sep 17 00:00:00 2001 From: oxe-i Date: Fri, 16 Jan 2026 15:07:26 -0300 Subject: [PATCH 1/2] add all-your-base exercise --- config.json | 8 + .../all-your-base/.docs/instructions.md | 28 +++ .../all-your-base/.docs/introduction.md | 8 + .../practice/all-your-base/.meta/Example.lean | 36 ++++ .../practice/all-your-base/.meta/config.json | 17 ++ .../practice/all-your-base/.meta/tests.toml | 82 +++++++++ .../practice/all-your-base/AllYourBase.lean | 8 + .../all-your-base/AllYourBaseTest.lean | 34 ++++ .../practice/all-your-base/lakefile.toml | 15 ++ .../practice/all-your-base/lean-toolchain | 1 + .../vendor/LeanTest/LeanTest.lean | 4 + .../vendor/LeanTest/LeanTest/Assertions.lean | 166 ++++++++++++++++++ .../vendor/LeanTest/LeanTest/Test.lean | 130 ++++++++++++++ generators/Generator/Generator.lean | 2 + .../Generator/AllYourBaseGenerator.lean | 56 ++++++ 15 files changed, 595 insertions(+) create mode 100644 exercises/practice/all-your-base/.docs/instructions.md create mode 100644 exercises/practice/all-your-base/.docs/introduction.md create mode 100644 exercises/practice/all-your-base/.meta/Example.lean create mode 100644 exercises/practice/all-your-base/.meta/config.json create mode 100644 exercises/practice/all-your-base/.meta/tests.toml create mode 100644 exercises/practice/all-your-base/AllYourBase.lean create mode 100644 exercises/practice/all-your-base/AllYourBaseTest.lean create mode 100644 exercises/practice/all-your-base/lakefile.toml create mode 100644 exercises/practice/all-your-base/lean-toolchain create mode 100644 exercises/practice/all-your-base/vendor/LeanTest/LeanTest.lean create mode 100644 exercises/practice/all-your-base/vendor/LeanTest/LeanTest/Assertions.lean create mode 100644 exercises/practice/all-your-base/vendor/LeanTest/LeanTest/Test.lean create mode 100644 generators/Generator/Generator/AllYourBaseGenerator.lean diff --git a/config.json b/config.json index 9f7af31..16b6236 100644 --- a/config.json +++ b/config.json @@ -336,6 +336,14 @@ "practices": [], "prerequisites": [], "difficulty": 7 + }, + { + "slug": "all-your-base", + "name": "All Your Base", + "uuid": "da51714a-5399-40ed-9fd7-787cb1bcb925", + "practices": [], + "prerequisites": [], + "difficulty": 8 } ] }, diff --git a/exercises/practice/all-your-base/.docs/instructions.md b/exercises/practice/all-your-base/.docs/instructions.md new file mode 100644 index 0000000..1b688b6 --- /dev/null +++ b/exercises/practice/all-your-base/.docs/instructions.md @@ -0,0 +1,28 @@ +# Instructions + +Convert a sequence of digits in one base, representing a number, into a sequence of digits in another base, representing the same number. + +~~~~exercism/note +Try to implement the conversion yourself. +Do not use something else to perform the conversion for you. +~~~~ + +## About [Positional Notation][positional-notation] + +In positional notation, a number in base **b** can be understood as a linear combination of powers of **b**. + +The number 42, _in base 10_, means: + +`(4 × 10¹) + (2 × 10⁰)` + +The number 101010, _in base 2_, means: + +`(1 × 2⁵) + (0 × 2⁴) + (1 × 2³) + (0 × 2²) + (1 × 2¹) + (0 × 2⁰)` + +The number 1120, _in base 3_, means: + +`(1 × 3³) + (1 × 3²) + (2 × 3¹) + (0 × 3⁰)` + +_Yes. Those three numbers above are exactly the same. Congratulations!_ + +[positional-notation]: https://en.wikipedia.org/wiki/Positional_notation diff --git a/exercises/practice/all-your-base/.docs/introduction.md b/exercises/practice/all-your-base/.docs/introduction.md new file mode 100644 index 0000000..68aaffb --- /dev/null +++ b/exercises/practice/all-your-base/.docs/introduction.md @@ -0,0 +1,8 @@ +# Introduction + +You've just been hired as professor of mathematics. +Your first week went well, but something is off in your second week. +The problem is that every answer given by your students is wrong! +Luckily, your math skills have allowed you to identify the problem: the student answers _are_ correct, but they're all in base 2 (binary)! +Amazingly, it turns out that each week, the students use a different base. +To help you quickly verify the student answers, you'll be building a tool to translate between bases. diff --git a/exercises/practice/all-your-base/.meta/Example.lean b/exercises/practice/all-your-base/.meta/Example.lean new file mode 100644 index 0000000..01bcc79 --- /dev/null +++ b/exercises/practice/all-your-base/.meta/Example.lean @@ -0,0 +1,36 @@ +namespace AllYourBase + +def ValidBase := { x : Nat // x >= 2 } + +def rebase (inputBase : ValidBase) (digits : List (Fin inputBase.val)) (outputBase : ValidBase) : List (Fin outputBase.val) := Id.run do + /- + Nat.lt_of_lt_of_le = n < m -> m <= k -> n < k + decide proves that 0 < 2 (0 is n and 2 is m in the theorem) + outputBase.property = outputBase.val >= 2 (outputBase.val is k in the theorem) + so: 0 < 2 -> 2 <= outputBase.val -> 0 < outputBase.val + -/ + have hpos : 0 < outputBase.val := + Nat.lt_of_lt_of_le (by decide : 0 < 2) outputBase.property + let mut base10 := + digits.reverse.mapIdx (inputBase.val ^ · * ·.val) + |> (List.foldl (· + ·) 0 .) + match base10 with + | 0 => return [⟨0, hpos⟩] /- have already proved that 0 < outputBase.val, so 0 "fits" in Fin outputBase.val -/ + | _ => + let mut result : List (Fin outputBase.val) := [] + while base10 > 0 do + let digit := base10 % outputBase.val + /- + Nat.mod_lt = x, y ∈ Nat -> 0 < y -> x % y < y + digit = base10 % outputBase.val + base10, outputBase.val ∈ Nat + so, to prove that digit < outputBase.val, we can prove that 0 < outputBase.val + which was already proved by hpos + -/ + have hmod : digit < outputBase.val := + Nat.mod_lt base10 hpos + result := ⟨digit, hmod⟩ :: result /- hmod proves that digit < outputBase.val, so digit "fits" in Fin outputBase.val -/ + base10 := base10 / outputBase.val + return result + +end AllYourBase diff --git a/exercises/practice/all-your-base/.meta/config.json b/exercises/practice/all-your-base/.meta/config.json new file mode 100644 index 0000000..244af85 --- /dev/null +++ b/exercises/practice/all-your-base/.meta/config.json @@ -0,0 +1,17 @@ +{ + "authors": [ + "oxe-i" + ], + "files": { + "solution": [ + "AllYourBase.lean" + ], + "test": [ + "AllYourBaseTest.lean" + ], + "example": [ + ".meta/Example.lean" + ] + }, + "blurb": "Convert a number, represented as a sequence of digits in one base, to any other base." +} diff --git a/exercises/practice/all-your-base/.meta/tests.toml b/exercises/practice/all-your-base/.meta/tests.toml new file mode 100644 index 0000000..d519402 --- /dev/null +++ b/exercises/practice/all-your-base/.meta/tests.toml @@ -0,0 +1,82 @@ +# 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. + +[5ce422f9-7a4b-4f44-ad29-49c67cb32d2c] +description = "single bit one to decimal" + +[0cc3fea8-bb79-46ac-a2ab-5a2c93051033] +description = "binary to single decimal" + +[f12db0f9-0d3d-42c2-b3ba-e38cb375a2b8] +description = "single decimal to binary" + +[2c45cf54-6da3-4748-9733-5a3c765d925b] +description = "binary to multiple decimal" + +[65ddb8b4-8899-4fcc-8618-181b2cf0002d] +description = "decimal to binary" + +[8d418419-02a7-4824-8b7a-352d33c6987e] +description = "trinary to hexadecimal" + +[d3901c80-8190-41b9-bd86-38d988efa956] +description = "hexadecimal to trinary" + +[5d42f85e-21ad-41bd-b9be-a3e8e4258bbf] +description = "15-bit integer" + +[d68788f7-66dd-43f8-a543-f15b6d233f83] +description = "empty list" + +[5e27e8da-5862-4c5f-b2a9-26c0382b6be7] +description = "single zero" + +[2e1c2573-77e4-4b9c-8517-6c56c5bcfdf2] +description = "multiple zeros" + +[3530cd9f-8d6d-43f5-bc6e-b30b1db9629b] +description = "leading zeros" + +[a6b476a1-1901-4f2a-92c4-4d91917ae023] +description = "input base is one" +include = false + +[e21a693a-7a69-450b-b393-27415c26a016] +description = "input base is zero" +include = false + +[54a23be5-d99e-41cc-88e0-a650ffe5fcc2] +description = "input base is negative" +include = false + +[9eccf60c-dcc9-407b-95d8-c37b8be56bb6] +description = "negative digit" +include = false + +[232fa4a5-e761-4939-ba0c-ed046cd0676a] +description = "invalid positive digit" +include = false + +[14238f95-45da-41dc-95ce-18f860b30ad3] +description = "output base is one" +include = false + +[73dac367-da5c-4a37-95fe-c87fad0a4047] +description = "output base is zero" +include = false + +[13f81f42-ff53-4e24-89d9-37603a48ebd9] +description = "output base is negative" +include = false + +[0e6c895d-8a5d-4868-a345-309d094cfe8d] +description = "both bases are negative" +include = false diff --git a/exercises/practice/all-your-base/AllYourBase.lean b/exercises/practice/all-your-base/AllYourBase.lean new file mode 100644 index 0000000..0ea4580 --- /dev/null +++ b/exercises/practice/all-your-base/AllYourBase.lean @@ -0,0 +1,8 @@ +namespace AllYourBase + +def ValidBase := { x : Nat // x >= 2 } + +def rebase (inputBase : ValidBase) (digits : List (Fin inputBase.val)) (outputBase : ValidBase) : List (Fin outputBase.val) := + sorry + +end AllYourBase diff --git a/exercises/practice/all-your-base/AllYourBaseTest.lean b/exercises/practice/all-your-base/AllYourBaseTest.lean new file mode 100644 index 0000000..a94033b --- /dev/null +++ b/exercises/practice/all-your-base/AllYourBaseTest.lean @@ -0,0 +1,34 @@ +import LeanTest +import AllYourBase + +open LeanTest + +def allYourBaseTests : TestSuite := + (TestSuite.empty "AllYourBase") + |>.addTest "single bit one to decimal" (do + return assertEqual [1] (AllYourBase.rebase ⟨2, (by decide)⟩ [1] ⟨10, (by decide)⟩)) + |>.addTest "binary to single decimal" (do + return assertEqual [5] (AllYourBase.rebase ⟨2, (by decide)⟩ [1, 0, 1] ⟨10, (by decide)⟩)) + |>.addTest "single decimal to binary" (do + return assertEqual [1, 0, 1] (AllYourBase.rebase ⟨10, (by decide)⟩ [5] ⟨2, (by decide)⟩)) + |>.addTest "binary to multiple decimal" (do + return assertEqual [4, 2] (AllYourBase.rebase ⟨2, (by decide)⟩ [1, 0, 1, 0, 1, 0] ⟨10, (by decide)⟩)) + |>.addTest "decimal to binary" (do + return assertEqual [1, 0, 1, 0, 1, 0] (AllYourBase.rebase ⟨10, (by decide)⟩ [4, 2] ⟨2, (by decide)⟩)) + |>.addTest "trinary to hexadecimal" (do + return assertEqual [2, 10] (AllYourBase.rebase ⟨3, (by decide)⟩ [1, 1, 2, 0] ⟨16, (by decide)⟩)) + |>.addTest "hexadecimal to trinary" (do + return assertEqual [1, 1, 2, 0] (AllYourBase.rebase ⟨16, (by decide)⟩ [2, 10] ⟨3, (by decide)⟩)) + |>.addTest "15-bit integer" (do + return assertEqual [6, 10, 45] (AllYourBase.rebase ⟨97, (by decide)⟩ [3, 46, 60] ⟨73, (by decide)⟩)) + |>.addTest "empty list" (do + return assertEqual [0] (AllYourBase.rebase ⟨2, (by decide)⟩ [] ⟨10, (by decide)⟩)) + |>.addTest "single zero" (do + return assertEqual [0] (AllYourBase.rebase ⟨10, (by decide)⟩ [0] ⟨2, (by decide)⟩)) + |>.addTest "multiple zeros" (do + return assertEqual [0] (AllYourBase.rebase ⟨10, (by decide)⟩ [0, 0, 0] ⟨2, (by decide)⟩)) + |>.addTest "leading zeros" (do + return assertEqual [4, 2] (AllYourBase.rebase ⟨7, (by decide)⟩ [0, 6, 0] ⟨10, (by decide)⟩)) + +def main : IO UInt32 := do + runTestSuitesWithExitCode [allYourBaseTests] diff --git a/exercises/practice/all-your-base/lakefile.toml b/exercises/practice/all-your-base/lakefile.toml new file mode 100644 index 0000000..7747ff2 --- /dev/null +++ b/exercises/practice/all-your-base/lakefile.toml @@ -0,0 +1,15 @@ +name = "all-your-base" +version = "0.1.0" +defaultTargets = ["AllYourBaseTest"] +testDriver = "AllYourBaseTest" + +[[lean_lib]] +name = "LeanTest" +srcDir = "vendor/LeanTest" + +[[lean_lib]] +name = "AllYourBase" + +[[lean_exe]] +name = "AllYourBaseTest" +root = "AllYourBaseTest" diff --git a/exercises/practice/all-your-base/lean-toolchain b/exercises/practice/all-your-base/lean-toolchain new file mode 100644 index 0000000..370b26d --- /dev/null +++ b/exercises/practice/all-your-base/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.25.2 diff --git a/exercises/practice/all-your-base/vendor/LeanTest/LeanTest.lean b/exercises/practice/all-your-base/vendor/LeanTest/LeanTest.lean new file mode 100644 index 0000000..012ba20 --- /dev/null +++ b/exercises/practice/all-your-base/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/all-your-base/vendor/LeanTest/LeanTest/Assertions.lean b/exercises/practice/all-your-base/vendor/LeanTest/LeanTest/Assertions.lean new file mode 100644 index 0000000..60e4ad8 --- /dev/null +++ b/exercises/practice/all-your-base/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/all-your-base/vendor/LeanTest/LeanTest/Test.lean b/exercises/practice/all-your-base/vendor/LeanTest/LeanTest/Test.lean new file mode 100644 index 0000000..5ddbae5 --- /dev/null +++ b/exercises/practice/all-your-base/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 706f367..c95f96a 100644 --- a/generators/Generator/Generator.lean +++ b/generators/Generator/Generator.lean @@ -1,5 +1,6 @@ import Generator.PrimeFactorsGenerator import Generator.PrimeFactorsGenerator +import Generator.AllYourBaseGenerator import Generator.SayGenerator import Generator.BinarySearchGenerator import Generator.PythagoreanTripletGenerator @@ -24,6 +25,7 @@ def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBod Std.HashMap.ofList [ ("PrimeFactors", (PrimeFactorsGenerator.genIntro, PrimeFactorsGenerator.genTestCase, PrimeFactorsGenerator.genEnd)), ("PrimeFactors", (PrimeFactorsGenerator.genIntro, PrimeFactorsGenerator.genTestCase, PrimeFactorsGenerator.genEnd)), + ("AllYourBase", (AllYourBaseGenerator.genIntro, AllYourBaseGenerator.genTestCase, AllYourBaseGenerator.genEnd)), ("Say", (SayGenerator.genIntro, SayGenerator.genTestCase, SayGenerator.genEnd)), ("BinarySearch", (BinarySearchGenerator.genIntro, BinarySearchGenerator.genTestCase, BinarySearchGenerator.genEnd)), ("PythagoreanTriplet", (PythagoreanTripletGenerator.genIntro, PythagoreanTripletGenerator.genTestCase, PythagoreanTripletGenerator.genEnd)), diff --git a/generators/Generator/Generator/AllYourBaseGenerator.lean b/generators/Generator/Generator/AllYourBaseGenerator.lean new file mode 100644 index 0000000..68ef498 --- /dev/null +++ b/generators/Generator/Generator/AllYourBaseGenerator.lean @@ -0,0 +1,56 @@ +import Lean +import Std + +open Lean +open Std + +namespace AllYourBaseGenerator + +def genIntro (exercise : String) : String := s!"import LeanTest +import {exercise} + +open LeanTest + +def {exercise.decapitalize}Tests : TestSuite := + (TestSuite.empty \"{exercise}\")" + +def getOk {α β} (except : Except α β) [Inhabited β] : β := except.toOption |> (·.get!) + +def errorToOption (expected : Json) : Option String := + match expected.getObjVal? "error" with + | .error _ => some s!"{expected}" + | .ok _ => none + +def insertAllInputs (input : Json) : String := + let map := getOk input.getObj? + map.values.map (fun val => s!"{val}") |> (String.intercalate " " .) + +def intLiteral (n : Int) : String := + if n < 0 then s!"({n})" + else s!"{n}" + +def getFunName (property : Json) : String := + property.compress.dropWhile (·=='"') |> (·.dropRightWhile (·=='"')) + +def genTestCase (exercise : String) (case : TreeMap.Raw String Json) : String := + let input := case.get! "input" + let inputBase := input.getObjValD "inputBase" + let digits := input.getObjValD "digits" + let outputBase := input.getObjValD "outputBase" + let expected := case.get! "expected" + let description := case.get! "description" + |> (·.compress) + let funName := getFunName (case.get! "property") + let call := s!"({exercise}.{funName} ⟨{inputBase}, (by decide)⟩ {digits} ⟨{outputBase}, (by decide)⟩)" + s!" + |>.addTest {description} (do + return assertEqual {expected} {call})" + +def genEnd (exercise : String) : String := + s!" + +def main : IO UInt32 := do + runTestSuitesWithExitCode [{exercise.decapitalize}Tests] +" + +end AllYourBaseGenerator From 416a89f12bb63b4cefb9561a0b9bb033ad19cb8a Mon Sep 17 00:00:00 2001 From: oxe-i Date: Fri, 16 Jan 2026 15:36:08 -0300 Subject: [PATCH 2/2] correct upper bound in Say --- exercises/practice/say/.meta/Example.lean | 2 +- exercises/practice/say/Say.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/exercises/practice/say/.meta/Example.lean b/exercises/practice/say/.meta/Example.lean index 623f7c4..944fb55 100644 --- a/exercises/practice/say/.meta/Example.lean +++ b/exercises/practice/say/.meta/Example.lean @@ -9,7 +9,7 @@ def tens : Array String := #[ "twenty", "thirty", "forty", "fifty", "sixty", "seventy", "eighty", "ninety" ] -def say (number : Fin 999999999999) : String := +def say (number : Fin 1000000000000) : String := let rec helper := fun n => if n >= 1000000000 then let billion := n / 1000000000 diff --git a/exercises/practice/say/Say.lean b/exercises/practice/say/Say.lean index 0f2ce4a..2ee60b5 100644 --- a/exercises/practice/say/Say.lean +++ b/exercises/practice/say/Say.lean @@ -1,6 +1,6 @@ namespace Say -def say (number : Fin 999999999999) : String := +def say (number : Fin 1000000000000) : String := sorry end Say