Skip to content

Commit ace4138

Browse files
oxe-ioxe-i
authored
add resistor-color-duo exercise (#180)
1 parent 9a7636b commit ace4138

16 files changed

Lines changed: 626 additions & 0 deletions

File tree

‎config.json‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -538,6 +538,14 @@
538538
"prerequisites": [],
539539
"difficulty": 5
540540
},
541+
{
542+
"slug": "resistor-color-duo",
543+
"name": "Resistor Color Duo",
544+
"uuid": "de08a88e-1fd2-49fa-b501-11649b2e42af",
545+
"practices": [],
546+
"prerequisites": [],
547+
"difficulty": 5
548+
},
541549
{
542550
"slug": "transpose",
543551
"name": "Transpose",

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

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
# Instructions append
2+
3+
## Defining syntax
4+
5+
~~~~exercism/caution
6+
This exercise is intended as a continuation of [`Resistor Color`][resistor-color] and builds upon it.
7+
Although you may solve practice exercises in any order, we encourage you to follow the suggested sequence.
8+
9+
[resistor-color]: https://exercism.org/tracks/lean/exercises/resistor-color
10+
~~~~
11+
12+
In this exercise, you are given syntax for colors already predefined using the `c*` prefix, e.g., `c*black`.
13+
You must then define syntax that associates a sequence of colors to a number, according to the instructions.
14+
The colors are within `*[[` and `]]` and separated by `, `, e.g., `*[[c*black, c*yellow, c*violet]]`.
15+
16+
This task will likely require you to use either notations or macros.
17+
You might want to check a [reference][macro-reference].
18+
19+
Because new syntax is expanded at compile time, any test would fail to compile unless all the required syntax is defined.
20+
For this reason, instead of relying on traditional runtime tests, we use [`#guard_msgs`][guard-msgs].
21+
This command compares a given docstring with a message generated by another command, in this case [`#eval`][eval], and reports an error if they are different.
22+
You may consider the absence of an error as a passing test.
23+
24+
If you work locally or in Lean's [online playground][playground], you will get instant feedback on any error reported by `#guard_msgs` through Lean InfoView.
25+
26+
~~~~exercism/caution
27+
For practical reasons, the online test runner does not currently have support to the built-in `Lean` library.
28+
This means that, although you are free to import this library, or any module within it, when working locally or in Lean's online playground, this will cause a solution to fail when submitted to exercism.
29+
30+
Note that this library is not necessary to solve the exercise.
31+
~~~~
32+
33+
[macro-reference]: https://lean-lang.org/doc/reference/latest/Notations-and-Macros/#language-extension
34+
[guard-msgs]: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean/#hash-guard_msgs
35+
[eval]: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean/#hash-eval
36+
[playground]: https://live.lean-lang.org/

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

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
# Instructions
2+
3+
If you want to build something using a Raspberry Pi, you'll probably use _resistors_.
4+
For this exercise, you need to know two things about them:
5+
6+
- Each resistor has a resistance value.
7+
- Resistors are small - so small in fact that if you printed the resistance value on them, it would be hard to read.
8+
9+
To get around this problem, manufacturers print color-coded bands onto the resistors to denote their resistance values.
10+
Each band has a position and a numeric value.
11+
12+
The first 2 bands of a resistor have a simple encoding scheme: each color maps to a single number.
13+
For example, if they printed a brown band (value 1) followed by a green band (value 5), it would translate to the number 15.
14+
15+
In this exercise you are going to create a helpful program so that you don't have to remember the values of the bands.
16+
The program will take color names as input and output a two digit number, even if the input is more than two colors!
17+
18+
The band colors are encoded as follows:
19+
20+
- black: 0
21+
- brown: 1
22+
- red: 2
23+
- orange: 3
24+
- yellow: 4
25+
- green: 5
26+
- blue: 6
27+
- violet: 7
28+
- grey: 8
29+
- white: 9
30+
31+
From the example above:
32+
brown-green should return 15, and
33+
brown-green-violet should return 15 too, ignoring the third color.

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

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
/-
2+
The solution in this comment reuses the macro already defined in `Extra.lean`.
3+
In order to make use of the values expanded by this macro, the expression must be evaluated in an elaborator.
4+
However, the tools to do that are inside `Lean.Elab`, a module not supported by the online test runner.
5+
6+
For this reason, this solution is only presented here as a reference.
7+
8+
import Lean.Elab
9+
import Extra
10+
11+
open Lean Elab Term
12+
13+
syntax "*[[" term,* "]]" : term
14+
15+
elab_rules : term
16+
| `(*[[ $vals,* ]]) => do
17+
let elems := vals.getElems
18+
19+
guard (elems.size >= 2)
20+
21+
let a₁ ← elabTerm elems[0]! none
22+
let a₂ ← elabTerm elems[1]! none
23+
24+
match a₁.nat? >>= fun v₁ => a₂.nat? >>= fun v₂ => pure (v₁ * 10 + v₂) with
25+
| none => throwUnsupportedSyntax
26+
| some sum => return Lean.mkNatLit sum
27+
-/
28+
29+
import Extra
30+
31+
syntax "*[[" term,* "]]" : term
32+
33+
def getValue : Lean.TSyntax `term → Option Nat
34+
| `(c*black) => some 0
35+
| `(c*brown) => some 1
36+
| `(c*red) => some 2
37+
| `(c*orange) => some 3
38+
| `(c*yellow) => some 4
39+
| `(c*green) => some 5
40+
| `(c*blue) => some 6
41+
| `(c*violet) => some 7
42+
| `(c*grey) => some 8
43+
| `(c*white) => some 9
44+
| _ => none
45+
46+
macro_rules
47+
| `(*[[ $vals,* ]]) => do
48+
let elems := vals.getElems.toList
49+
match elems with
50+
| a₁ :: a₂ :: _ =>
51+
match getValue a₁, getValue a₂ with
52+
| some v₁, some v₂ => return Lean.Syntax.mkNatLit (10 * v₁ + v₂)
53+
| _, _ => Lean.Macro.throwUnsupported
54+
| _ => Lean.Macro.throwUnsupported

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

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
{
2+
"authors": [
3+
"oxe-i"
4+
],
5+
"files": {
6+
"solution": [
7+
"ResistorColorDuo.lean"
8+
],
9+
"test": [
10+
"ResistorColorDuoTest.lean"
11+
],
12+
"example": [
13+
".meta/Example.lean"
14+
],
15+
"editor": [
16+
"Extra.lean"
17+
]
18+
},
19+
"blurb": "Convert color codes, as used on resistors, to a numeric value.",
20+
"source": "Maud de Vries, Erik Schierboom",
21+
"source_url": "https://github.com/exercism/problem-specifications/issues/1464"
22+
}

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

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
# This is an auto-generated file.
2+
#
3+
# Regenerating this file via `configlet sync` will:
4+
# - Recreate every `description` key/value pair
5+
# - Recreate every `reimplements` key/value pair, where they exist in problem-specifications
6+
# - Remove any `include = true` key/value pair (an omitted `include` key implies inclusion)
7+
# - Preserve any other key/value pair
8+
#
9+
# As user-added comments (using the # character) will be removed when this file
10+
# is regenerated, comments can be added via a `comment` key.
11+
12+
[ce11995a-5b93-4950-a5e9-93423693b2fc]
13+
description = "Brown and black"
14+
15+
[7bf82f7a-af23-48ba-a97d-38d59406a920]
16+
description = "Blue and grey"
17+
18+
[f1886361-fdfd-4693-acf8-46726fe24e0c]
19+
description = "Yellow and violet"
20+
21+
[b7a6cbd2-ae3c-470a-93eb-56670b305640]
22+
description = "White and red"
23+
24+
[77a8293d-2a83-4016-b1af-991acc12b9fe]
25+
description = "Orange and orange"
26+
27+
[0c4fb44f-db7c-4d03-afa8-054350f156a8]
28+
description = "Ignore additional colors"
29+
30+
[4a8ceec5-0ab4-4904-88a4-daf953a5e818]
31+
description = "Black and brown, one-digit"

‎exercises/practice/resistor-color-duo/Extra.lean‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
syntax "c*" ident:term
2+
3+
macro_rules
4+
| `(c*black) => `((0 : Fin 10))
5+
| `(c*brown) => `((1 : Fin 10))
6+
| `(c*red) => `((2 : Fin 10))
7+
| `(c*orange) => `((3 : Fin 10))
8+
| `(c*yellow) => `((4 : Fin 10))
9+
| `(c*green) => `((5 : Fin 10))
10+
| `(c*blue) => `((6 : Fin 10))
11+
| `(c*violet) => `((7 : Fin 10))
12+
| `(c*grey) => `((8 : Fin 10))
13+
| `(c*white) => `((9 : Fin 10))

‎exercises/practice/resistor-color-duo/ResistorColorDuo.lean‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
import Extra
2+
3+
/-
4+
You are given syntax for colors already predefined using the `c*` prefix, e.g., `c*black`.
5+
You must then define syntax that associates a sequence of colors to a number, according to the instructions.
6+
The colors are within `*[[` and `]]` and separated by `, `, e.g., `*[[c*black, c*yellow, c*violet]]`.
7+
8+
Note that the online test runner does not have support to the `Lean` library.
9+
Any solution that uses it will fail when submitted to exercism, even if correct.
10+
This library is not necessary to solve the exercise.
11+
12+
Macros and notations are not qualified by namespace.
13+
For this reason, this exercise does not define a namespace.
14+
-/

‎exercises/practice/resistor-color-duo/ResistorColorDuoTest.lean‎

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
import LeanTest
2+
import ResistorColorDuo
3+
4+
open LeanTest
5+
6+
/--
7+
info: 10
8+
-/
9+
#guard_msgs(info, drop all) in
10+
#eval *[[c*brown, c*black]]
11+
12+
/--
13+
info: 68
14+
-/
15+
#guard_msgs(info, drop all) in
16+
#eval *[[c*blue, c*grey]]
17+
18+
/--
19+
info: 47
20+
-/
21+
#guard_msgs(info, drop all) in
22+
#eval *[[c*yellow, c*violet]]
23+
24+
/--
25+
info: 92
26+
-/
27+
#guard_msgs(info, drop all) in
28+
#eval *[[c*white, c*red]]
29+
30+
/--
31+
info: 33
32+
-/
33+
#guard_msgs(info, drop all) in
34+
#eval *[[c*orange, c*orange]]
35+
36+
/--
37+
info: 51
38+
-/
39+
#guard_msgs(info, drop all) in
40+
#eval *[[c*green, c*brown, c*orange]]
41+
42+
/--
43+
info: 1
44+
-/
45+
#guard_msgs(info, drop all) in
46+
#eval *[[c*black, c*brown]]
47+
48+
def main : IO UInt32 := do
49+
runTestSuitesWithExitCode []

‎exercises/practice/resistor-color-duo/lakefile.toml‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
name = "resistor-color-duo"
2+
version = "0.1.0"
3+
defaultTargets = ["ResistorColorDuoTest"]
4+
testDriver = "ResistorColorDuoTest"
5+
moreLeanArgs = [ "-DwarningAsError=true" ]
6+
7+
[[lean_lib]]
8+
name = "LeanTest"
9+
srcDir = "vendor/LeanTest"
10+
11+
[[lean_lib]]
12+
name = "ResistorColorDuo"
13+
14+
[[lean_lib]]
15+
name = "Extra"
16+
17+
[[lean_exe]]
18+
name = "ResistorColorDuoTest"
19+
root = "ResistorColorDuoTest"

0 commit comments

Comments
 (0)
⚡