Add phone-number exercise (#50)

Author: keiravillekode

config.json

@@ -209,6 +209,14 @@
         "prerequisites": [],
         "difficulty": 3
       },
+      {
+        "slug": "phone-number",
+        "name": "Phone Number",
+        "uuid": "692e89e0-b392-4a82-98e5-7bf7a948ffbf",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 3
+      },
       {
         "slug": "rotational-cipher",
         "name": "Rotational Cipher",

exercises/practice/phone-number/.docs/instructions.md

@@ -0,0 +1,34 @@
+# Instructions
+
+Clean up phone numbers so that they can be sent SMS messages.
+
+The **North American Numbering Plan (NANP)** is a telephone numbering system used by many countries in North America like the United States, Canada or Bermuda.
+All NANP-countries share the same international country code: `1`.
+
+NANP numbers are ten-digit numbers consisting of a three-digit Numbering Plan Area code, commonly known as _area code_, followed by a seven-digit local number.
+The first three digits of the local number represent the _exchange code_, followed by the unique four-digit number which is the _subscriber number_.
+
+The format is usually represented as
+
+```text
+NXX NXX-XXXX
+```
+
+where `N` is any digit from 2 through 9 and `X` is any digit from 0 through 9.
+
+Sometimes they also have the country code (represented as `1` or `+1`) prefixed.
+
+Your task is to clean up differently formatted telephone numbers by removing punctuation and the country code if present.
+
+For example, the inputs
+
+- `+1 (613)-995-0253`
+- `613-995-0253`
+- `1 613 995 0253`
+- `613.995.0253`
+
+should all produce the output
+
+`6139950253`
+
+**Note:** As this exercise only deals with telephone numbers used in NANP-countries, only 1 is considered a valid country code.

exercises/practice/phone-number/.docs/introduction.md

@@ -0,0 +1,12 @@
+# Introduction
+
+You've joined LinkLine, a leading communications company working to ensure reliable connections for everyone.
+The team faces a big challenge: users submit phone numbers in all sorts of formats — dashes, spaces, dots, parentheses, and even prefixes.
+Some numbers are valid, while others are impossible to use.
+
+Your mission is to turn this chaos into order.
+You'll clean up valid numbers, formatting them appropriately for use in the system.
+At the same time, you'll identify and filter out any invalid entries.
+
+The success of LinkLine's operations depends on your ability to separate the useful from the unusable.
+Are you ready to take on the challenge and keep the connections running smoothly?

exercises/practice/phone-number/.meta/Example.lean

@@ -0,0 +1,12 @@
+namespace PhoneNumber
+
+def clean (phrase : String) : Option String := Id.run do
+  if phrase.any (fun (c : Char) => c > '9') then none
+  else
+    let mut digits := phrase.toList.filter Char.isDigit
+    if digits.length == 11 && digits[0]! == '1' then
+      digits := List.tail? digits |> Option.get!
+    if digits.length != 10 || digits[0]! <= '1' || digits[3]! <= '1' then none
+    else some digits.asString
+
+end PhoneNumber

exercises/practice/phone-number/.meta/config.json

@@ -0,0 +1,19 @@
+{
+  "authors": [
+    "keiravillekode"
+  ],
+  "files": {
+    "solution": [
+      "PhoneNumber.lean"
+    ],
+    "test": [
+      "PhoneNumberTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Clean up user-entered phone numbers so that they can be sent SMS messages.",
+  "source": "Exercise by the JumpstartLab team for students at The Turing School of Software and Design.",
+  "source_url": "https://turing.edu"
+}

exercises/practice/phone-number/.meta/tests.toml

@@ -0,0 +1,84 @@
+# 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.
+
+[79666dce-e0f1-46de-95a1-563802913c35]
+description = "cleans the number"
+
+[c360451f-549f-43e4-8aba-fdf6cb0bf83f]
+description = "cleans numbers with dots"
+
+[08f94c34-9a37-46a2-a123-2a8e9727395d]
+description = "cleans numbers with multiple spaces"
+
+[598d8432-0659-4019-a78b-1c6a73691d21]
+description = "invalid when 9 digits"
+include = false
+
+[2de74156-f646-42b5-8638-0ef1d8b58bc2]
+description = "invalid when 9 digits"
+reimplements = "598d8432-0659-4019-a78b-1c6a73691d21"
+
+[57061c72-07b5-431f-9766-d97da7c4399d]
+description = "invalid when 11 digits does not start with a 1"
+
+[9962cbf3-97bb-4118-ba9b-38ff49c64430]
+description = "valid when 11 digits and starting with 1"
+
+[fa724fbf-054c-4d91-95da-f65ab5b6dbca]
+description = "valid when 11 digits and starting with 1 even with punctuation"
+
+[c6a5f007-895a-4fc5-90bc-a7e70f9b5cad]
+description = "invalid when more than 11 digits"
+include = false
+
+[4a1509b7-8953-4eec-981b-c483358ff531]
+description = "invalid when more than 11 digits"
+reimplements = "c6a5f007-895a-4fc5-90bc-a7e70f9b5cad"
+
+[63f38f37-53f6-4a5f-bd86-e9b404f10a60]
+description = "invalid with letters"
+include = false
+
+[eb8a1fc0-64e5-46d3-b0c6-33184208e28a]
+description = "invalid with letters"
+reimplements = "63f38f37-53f6-4a5f-bd86-e9b404f10a60"
+
+[4bd97d90-52fd-45d3-b0db-06ab95b1244e]
+description = "invalid with punctuations"
+include = false
+
+[065f6363-8394-4759-b080-e6c8c351dd1f]
+description = "invalid with punctuations"
+reimplements = "4bd97d90-52fd-45d3-b0db-06ab95b1244e"
+
+[d77d07f8-873c-4b17-8978-5f66139bf7d7]
+description = "invalid if area code starts with 0"
+
+[c7485cfb-1e7b-4081-8e96-8cdb3b77f15e]
+description = "invalid if area code starts with 1"
+
+[4d622293-6976-413d-b8bf-dd8a94d4e2ac]
+description = "invalid if exchange code starts with 0"
+
+[4cef57b4-7d8e-43aa-8328-1e1b89001262]
+description = "invalid if exchange code starts with 1"
+
+[9925b09c-1a0d-4960-a197-5d163cbe308c]
+description = "invalid if area code starts with 0 on valid 11-digit number"
+
+[3f809d37-40f3-44b5-ad90-535838b1a816]
+description = "invalid if area code starts with 1 on valid 11-digit number"
+
+[e08e5532-d621-40d4-b0cc-96c159276b65]
+description = "invalid if exchange code starts with 0 on valid 11-digit number"
+
+[57b32f3d-696a-455c-8bf1-137b6d171cdf]
+description = "invalid if exchange code starts with 1 on valid 11-digit number"

exercises/practice/phone-number/PhoneNumber.lean

@@ -0,0 +1,6 @@
+namespace PhoneNumber
+
+def clean (phrase : String) : Option String :=
+  sorry
+
+end PhoneNumber

exercises/practice/phone-number/PhoneNumberTest.lean

@@ -0,0 +1,46 @@
+import LeanTest
+import PhoneNumber
+
+open LeanTest
+
+def phoneNumberTests : TestSuite :=
+  (TestSuite.empty "PhoneNumber")
+  |>.addTest "cleans the number" (do
+      return assertEqual (some "2234567890") (PhoneNumber.clean "(223) 456-7890"))
+  |>.addTest "cleans numbers with dots" (do
+      return assertEqual (some "2234567890") (PhoneNumber.clean "223.456.7890"))
+  |>.addTest "cleans numbers with multiple spaces" (do
+      return assertEqual (some "2234567890") (PhoneNumber.clean "223 456   7890   "))
+  |>.addTest "invalid when 9 digits" (do
+      return assertEqual none (PhoneNumber.clean "123456789"))
+  |>.addTest "invalid when 11 digits does not start with a 1" (do
+      return assertEqual none (PhoneNumber.clean "22234567890"))
+  |>.addTest "valid when 11 digits and starting with 1" (do
+      return assertEqual (some "2234567890") (PhoneNumber.clean "12234567890"))
+  |>.addTest "valid when 11 digits and starting with 1 even with punctuation" (do
+      return assertEqual (some "2234567890") (PhoneNumber.clean "+1 (223) 456-7890"))
+  |>.addTest "invalid when more than 11 digits" (do
+      return assertEqual none (PhoneNumber.clean "321234567890"))
+  |>.addTest "invalid with letters" (do
+      return assertEqual none (PhoneNumber.clean "523-abc-7890"))
+  |>.addTest "invalid with punctuations" (do
+      return assertEqual none (PhoneNumber.clean "523-@:!-7890"))
+  |>.addTest "invalid if area code starts with 0" (do
+      return assertEqual none (PhoneNumber.clean "(023) 456-7890"))
+  |>.addTest "invalid if area code starts with 1" (do
+      return assertEqual none (PhoneNumber.clean "(123) 456-7890"))
+  |>.addTest "invalid if exchange code starts with 0" (do
+      return assertEqual none (PhoneNumber.clean "(223) 056-7890"))
+  |>.addTest "invalid if exchange code starts with 1" (do
+      return assertEqual none (PhoneNumber.clean "(223) 156-7890"))
+  |>.addTest "invalid if area code starts with 0 on valid 11-digit number" (do
+      return assertEqual none (PhoneNumber.clean "1 (023) 456-7890"))
+  |>.addTest "invalid if area code starts with 1 on valid 11-digit number" (do
+      return assertEqual none (PhoneNumber.clean "1 (123) 456-7890"))
+  |>.addTest "invalid if exchange code starts with 0 on valid 11-digit number" (do
+      return assertEqual none (PhoneNumber.clean "1 (223) 056-7890"))
+  |>.addTest "invalid if exchange code starts with 1 on valid 11-digit number" (do
+      return assertEqual none (PhoneNumber.clean "1 (223) 156-7890"))
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [phoneNumberTests]

exercises/practice/phone-number/lakefile.toml

@@ -0,0 +1,15 @@
+name = "phone-number"
+version = "0.1.0"
+defaultTargets = ["PhoneNumberTest"]
+testDriver = "PhoneNumberTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "PhoneNumber"
+
+[[lean_exe]]
+name = "PhoneNumberTest"
+root = "PhoneNumberTest"

exercises/practice/phone-number/lean-toolchain

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