add resistor-color exercise

config.json

@@ -426,6 +426,14 @@
         "prerequisites": [],
         "difficulty": 4
       },
+      {
+        "slug": "resistor-color",
+        "name": "Resistor Color",
+        "uuid": "189eb2e7-d2b2-4439-aa13-ade013566bdb",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 4
+      },
       {
         "slug": "roman-numerals",
         "name": "Roman Numerals",

exercises/practice/resistor-color/.docs/instructions.append.md

@@ -0,0 +1,19 @@
+# Instructions append
+
+## Defining syntax
+
+In this exercise, you must define syntax for colors using the `c!` prefix, e.g., `c!black`.
+This syntax should expand at compile time to each color's corresponding value as a `Fin 10`, according to the instructions.
+In the same way, you must define syntax for an array of all color values using `c!all`.
+
+This task will likely require you to use either notations or macros.
+You might want to check a [reference][macro-reference].
+
+Because new syntax is expanded at compile time, any test would fail to compile unless all the required syntax is defined.
+For this reason, instead of relying on traditional runtime tests, we check all values using theorems.
+If a theorem typechecks, you may consider it a passing test.
+
+If you work locally or in Lean's [online playground][playground], you will get instant feedback on whether any theorem succeeds or fails, and why it fails, through Lean InfoView.
+
+[macro-reference]: https://lean-lang.org/doc/reference/latest/Notations-and-Macros/#language-extension
+[playground]: https://live.lean-lang.org/

exercises/practice/resistor-color/.docs/instructions.md

@@ -0,0 +1,39 @@
+# Instructions
+
+If you want to build something using a Raspberry Pi, you'll probably use _resistors_.
+For this exercise, you need to know two things about them:
+
+- Each resistor has a resistance value.
+- Resistors are small - so small in fact that if you printed the resistance value on them, it would be hard to read.
+
+To get around this problem, manufacturers print color-coded bands onto the resistors to denote their resistance values.
+Each band has a position and a numeric value.
+
+The first 2 bands of a resistor have a simple encoding scheme: each color maps to a single number.
+
+In this exercise you are going to create a helpful program so that you don't have to remember the values of the bands.
+
+These colors are encoded as follows:
+
+- black: 0
+- brown: 1
+- red: 2
+- orange: 3
+- yellow: 4
+- green: 5
+- blue: 6
+- violet: 7
+- grey: 8
+- white: 9
+
+The goal of this exercise is to create a way:
+
+- to look up the numerical value associated with a particular color band
+- to list the different band colors
+
+Mnemonics map the colors to the numbers, that, when stored as an array, happen to map to their index in the array:
+Better Be Right Or Your Great Big Values Go Wrong.
+
+More information on the color encoding of resistors can be found in the [Electronic color code Wikipedia article][e-color-code].
+
+[e-color-code]: https://en.wikipedia.org/wiki/Electronic_color_code

exercises/practice/resistor-color/.meta/Example.lean

@@ -0,0 +1,28 @@
+/-
+notation "c!black"  => (0 : Fin 10)
+notation "c!brown"  => (1 : Fin 10)
+notation "c!red"    => (2 : Fin 10)
+notation "c!orange" => (3 : Fin 10)
+notation "c!yellow" => (4 : Fin 10)
+notation "c!green"  => (5 : Fin 10)
+notation "c!blue"   => (6 : Fin 10)
+notation "c!violet" => (7 : Fin 10)
+notation "c!grey"   => (8 : Fin 10)
+notation "c!white"  => (9 : Fin 10)
+notation "c!all"    => (Array.finRange 10)
+-/
+
+syntax "c!" ident:term
+
+macro_rules
+  | `(c!black)  => `((⟨0, by decide⟩ : Fin 10))
+  | `(c!brown)  => `((⟨1, by decide⟩ : Fin 10))
+  | `(c!red)    => `((⟨2, by decide⟩ : Fin 10))
+  | `(c!orange) => `((⟨3, by decide⟩ : Fin 10))
+  | `(c!yellow) => `((⟨4, by decide⟩ : Fin 10))
+  | `(c!green)  => `((⟨5, by decide⟩ : Fin 10))
+  | `(c!blue)   => `((⟨6, by decide⟩ : Fin 10))
+  | `(c!violet) => `((⟨7, by decide⟩ : Fin 10))
+  | `(c!grey)   => `((⟨8, by decide⟩ : Fin 10))
+  | `(c!white)  => `((⟨9, by decide⟩ : Fin 10))
+  | `(c!all)    => `((Array.finRange 10))

exercises/practice/resistor-color/.meta/config.json

@@ -0,0 +1,19 @@
+{
+  "authors": [
+    "oxe-i"
+  ],
+  "files": {
+    "solution": [
+      "ResistorColor.lean"
+    ],
+    "test": [
+      "ResistorColorTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Convert a resistor band's color to its numeric representation.",
+  "source": "Maud de Vries, Erik Schierboom",
+  "source_url": "https://github.com/exercism/problem-specifications/issues/1458"
+}

exercises/practice/resistor-color/.meta/tests.toml

@@ -0,0 +1,22 @@
+# 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.
+
+[49eb31c5-10a8-4180-9f7f-fea632ab87ef]
+description = "Color codes -> Black"
+
+[0a4df94b-92da-4579-a907-65040ce0b3fc]
+description = "Color codes -> White"
+
+[5f81608d-f36f-4190-8084-f45116b6f380]
+description = "Color codes -> Orange"
+
+[581d68fa-f968-4be2-9f9d-880f2fb73cf7]
+description = "Colors"

exercises/practice/resistor-color/ResistorColor.lean

@@ -0,0 +1,9 @@
+/-
+  You must define syntax for colors using the `c!` prefix, e.g., `c!black`.
+  This syntax should expand to its corresponding value as a `Fin 10`, according to the instructions.
+
+  You must also define syntax `c!all` that expands to an array containing all color values.
+
+  Macros and notations are not qualified by namespace.
+  For this reason, this exercise does not define a namespace.
+-/

exercises/practice/resistor-color/ResistorColorTest.lean

@@ -0,0 +1,19 @@
+import LeanTest
+import ResistorColor
+
+open LeanTest
+
+theorem h_black: c!black = (0 : Fin 10) := by rfl
+theorem h_brown: c!brown = (1 : Fin 10) := by rfl
+theorem h_red: c!red = (2 : Fin 10) := by rfl
+theorem h_orange: c!orange = (3 : Fin 10) := by rfl
+theorem h_yellow: c!yellow = (4 : Fin 10) := by rfl
+theorem h_green: c!green = (5 : Fin 10) := by rfl
+theorem h_blue: c!blue = (6 : Fin 10) := by rfl
+theorem h_violet: c!violet = (7 : Fin 10) := by rfl
+theorem h_grey: c!grey = (8 : Fin 10) := by rfl
+theorem h_white: c!white = (9 : Fin 10) := by rfl
+theorem h_all: c!all = #[c!black, c!brown, c!red, c!orange, c!yellow, c!green, c!blue, c!violet, c!grey, c!white] := by rfl
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode []

exercises/practice/resistor-color/lakefile.toml

@@ -0,0 +1,15 @@
+name = "resistor-color"
+version = "0.1.0"
+defaultTargets = ["ResistorColorTest"]
+testDriver = "ResistorColorTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "ResistorColor"
+
+[[lean_exe]]
+name = "ResistorColorTest"
+root = "ResistorColorTest"

exercises/practice/resistor-color/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.29.0

exercises/practice/resistor-color/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

exercises/practice/resistor-color/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