Add linked-list exercise (exercism#113)

Author: oxe-i

config.json

@@ -642,6 +642,14 @@
         "prerequisites": [],
         "difficulty": 8
       },
+      {
+        "slug": "linked-list",
+        "name": "Linked List",
+        "uuid": "55d105a8-0f79-47b3-8599-53136584aa60",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 8
+      },
       {
         "slug": "rational-numbers",
         "name": "Rational Numbers",

exercises/practice/linked-list/.docs/instructions.append.md

@@ -0,0 +1,30 @@
+# Instructions append
+
+## Stateful data structures
+
+In functional languages, such as Lean, most values are immutable by design.
+This means updates are usually made by producing a new value.
+Both the old and the new value coexist and may be referenced and used.
+
+However, there are many situations where a _stateful_ value is desired, or even necessary.
+A stateful value is updated by mutation, _replacing_ the old value rather than creating a new one.
+After a mutation, only the updated value remains accessible.
+
+Note that mutations can break some guarantees of the language.
+A pure function must always return the same result for the same set of inputs, but if an input may change over time, then the function may return different results even when called with the same arguments.
+Similarly, if a function can produce external changes other than returning a result, or can read from sources other than its parameters, then two calls to the same function may have different and sometimes unpredictable outcomes.
+
+To handle such stateful behavior, Lean, like other functional languages, requires that effectful functions be wrapped in a special kind of structure that distinguishes them from pure functions.
+These structures are called _monads_.
+
+It is important to note that, although every stateful value lives inside some effectful monad, not every monad represents mutable state.
+Notable examples of "pure" monads are `Option`, `Except` and `Id`.
+
+In this exercise, you are going to define a stateful data structure called `LinkedList`.
+Instances of this data structure are updated by mutation.
+
+To support this, all functions are wrapped inside the `ST` monad.
+In this monad, mutable state is the only side effect, and mutable references cannot escape.
+For more information, you can check the [reference][reference].
+
+[reference]: https://lean-lang.org/doc/reference/latest/IO/Mutable-References/#mutable-st-references

exercises/practice/linked-list/.docs/instructions.md

@@ -0,0 +1,26 @@
+# Instructions
+
+Your team has decided to use a doubly linked list to represent each train route in the schedule.
+Each station along the train's route will be represented by a node in the linked list.
+
+You don't need to worry about arrival and departure times at the stations.
+Each station will simply be represented by a number.
+
+Routes can be extended, adding stations to the beginning or end of a route.
+They can also be shortened by removing stations from the beginning or the end of a route.
+
+Sometimes a station gets closed down, and in that case the station needs to be removed from the route, even if it is not at the beginning or end of the route.
+
+The size of a route is measured not by how far the train travels, but by how many stations it stops at.
+
+~~~~exercism/note
+The linked list is a fundamental data structure in computer science, often used in the implementation of other data structures.
+As the name suggests, it is a list of nodes that are linked together.
+It is a list of "nodes", where each node links to its neighbor or neighbors.
+In a **singly linked list** each node links only to the node that follows it.
+In a **doubly linked list** each node links to both the node that comes before, as well as the node that comes after.
+
+If you want to dig deeper into linked lists, check out [this article][intro-linked-list] that explains it using nice drawings.
+
+[intro-linked-list]: https://medium.com/basecs/whats-a-linked-list-anyway-part-1-d8b7e6508b9d
+~~~~

exercises/practice/linked-list/.docs/introduction.md

@@ -0,0 +1,6 @@
+# Introduction
+
+You are working on a project to develop a train scheduling system for a busy railway network.
+
+You've been asked to develop a prototype for the train routes in the scheduling system.
+Each route consists of a sequence of train stations that a given train stops at.

exercises/practice/linked-list/.meta/Example.lean

@@ -0,0 +1,127 @@
+import Std
+open Std
+
+namespace LinkedList
+
+variable {α σ : Type} [BEq α] [Inhabited α]
+
+structure Node (α : Type) where
+  prev  : Option Nat
+  value : α
+  next  : Option Nat
+  deriving Inhabited
+
+structure LinkedList σ α where
+  nodes  : ST.Ref σ (Array (Node α))
+  free   : ST.Ref σ (Array Nat)
+  head   : ST.Ref σ (Option Nat)
+  tail   : ST.Ref σ (Option Nat)
+  length : ST.Ref σ Nat
+
+def LinkedList.empty : ST σ (LinkedList σ α) := do
+  return {
+    nodes  := ← ST.mkRef #[],
+    free   := ← ST.mkRef #[],
+    head   := ← ST.mkRef none,
+    tail   := ← ST.mkRef none,
+    length := ← ST.mkRef 0
+  }
+
+private def buildNode (value : α) (list : LinkedList σ α) : ST σ Nat := do
+  let node : Node α := { prev := none, value := value, next := none}
+  match (← list.free.get).back? with
+  | none =>
+    let id := (← list.nodes.get).size
+    list.nodes.modify (·.push node)
+    return id
+  | some id =>
+    list.nodes.modify (·.set! id node)
+    list.free.modify (·.pop)
+    return id
+
+private def LinkedList.unlinkPrev (node : Node α) (list : LinkedList σ α) : ST σ Unit := do
+  match node.prev with
+  | some p =>
+    list.nodes.modify (·.modify p (λ pn => { pn with next := node.next }))
+  | none =>
+    list.head.set node.next
+
+private def LinkedList.unlinkNext (node : Node α) (list : LinkedList σ α) : ST σ Unit := do
+  match node.next with
+  | some n =>
+    list.nodes.modify (·.modify n (λ np => { np with prev := node.prev }))
+  | none =>
+    list.tail.set node.prev
+
+private def LinkedList.unlink (node : Node α) (list : LinkedList σ α) : ST σ Unit := do
+  list.unlinkPrev node
+  list.unlinkNext node
+
+def LinkedList.count (list : LinkedList σ α) : ST σ Nat :=
+  list.length.get
+
+def LinkedList.push (value : α) (list : LinkedList σ α) : ST σ Unit := do
+  let id ← buildNode value list
+  match ← list.tail.get with
+  | none =>
+    list.head.set (some id)
+    list.tail.set (some id)
+    list.length.modify (· + 1)
+  | some t =>
+    list.nodes.modify (λ ns =>
+      ns.modify t (λ n => { n with next := some id })
+      |>.modify id (λ n => { n with prev := some t })
+    )
+    list.tail.set (some id)
+    list.length.modify (· + 1)
+
+def LinkedList.unshift (value : α) (list : LinkedList σ α) : ST σ Unit := do
+  let id ← buildNode value list
+  match ← list.head.get with
+  | none =>
+    list.head.set (some id)
+    list.tail.set (some id)
+    list.length.modify (· + 1)
+  | some h =>
+    list.nodes.modify (λ ns =>
+      ns.modify h (λ n => { n with prev := some id })
+      |>.modify id (λ n => { n with next := some h })
+    )
+    list.head.set (some id)
+    list.length.modify (· + 1)
+
+def LinkedList.pop (list : LinkedList σ α) : ST σ (Option α) := do
+  match (← list.length.get) with
+  | 0 => return none
+  | n + 1 =>
+    let id := (← list.tail.get).get!
+    let node := (← list.nodes.get)[id]!
+    list.unlink node
+    list.length.set n
+    list.free.modify (·.push id)
+    return node.value
+
+def LinkedList.shift (list : LinkedList σ α) : ST σ (Option α) := do
+  match (← list.length.get) with
+  | 0 => return none
+  | n + 1 =>
+    let id := (← list.head.get).get!
+    let node := (← list.nodes.get)[id]!
+    list.unlink node
+    list.length.set n
+    list.free.modify (·.push id)
+    return node.value
+
+def LinkedList.delete (value : α) (list : LinkedList σ α) : ST σ Unit := do
+  let mut crtId ← list.head.get
+  while crtId.isSome do
+    let id := crtId.get!
+    let node := (← list.nodes.get)[id]!
+    if node.value == value then
+      list.unlink node
+      list.length.modify (· - 1)
+      list.free.modify (·.push id)
+      break
+    crtId := node.next
+
+end LinkedList

exercises/practice/linked-list/.meta/config.json

@@ -0,0 +1,18 @@
+{
+  "authors": [
+    "oxe-i"
+  ],
+  "files": {
+    "solution": [
+      "LinkedList.lean"
+    ],
+    "test": [
+      "LinkedListTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Implement a doubly linked list.",
+  "source": "Classic computer science topic"
+}

exercises/practice/linked-list/.meta/tests.toml

@@ -0,0 +1,67 @@
+# 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.
+
+[7f7e3987-b954-41b8-8084-99beca08752c]
+description = "pop gets element from the list"
+
+[c3f67e5d-cfa2-4c3e-a18f-7ce999c3c885]
+description = "push/pop respectively add/remove at the end of the list"
+
+[00ea24ce-4f5c-4432-abb4-cc6e85462657]
+description = "shift gets an element from the list"
+
+[37962ee0-3324-4a29-b588-5a4c861e6564]
+description = "shift gets first element from the list"
+
+[30a3586b-e9dc-43fb-9a73-2770cec2c718]
+description = "unshift adds element at start of the list"
+
+[042f71e4-a8a7-4cf0-8953-7e4f3a21c42d]
+description = "pop, push, shift, and unshift can be used in any order"
+
+[88f65c0c-4532-4093-8295-2384fb2f37df]
+description = "count an empty list"
+
+[fc055689-5cbe-4cd9-b994-02e2abbb40a5]
+description = "count a list with items"
+
+[8272cef5-130d-40ea-b7f6-5ffd0790d650]
+description = "count is correct after mutation"
+
+[229b8f7a-bd8a-4798-b64f-0dc0bb356d95]
+description = "popping to empty doesn't break the list"
+
+[4e1948b4-514e-424b-a3cf-a1ebbfa2d1ad]
+description = "shifting to empty doesn't break the list"
+
+[e8f7c600-d597-4f79-949d-8ad8bae895a6]
+description = "deletes the only element"
+
+[fd65e422-51f3-45c0-9fd0-c33da638f89b]
+description = "deletes the element with the specified value from the list"
+
+[59db191a-b17f-4ab7-9c5c-60711ec1d013]
+description = "deletes the element with the specified value from the list, re-assigns tail"
+
+[58242222-5d39-415b-951d-8128247f8993]
+description = "deletes the element with the specified value from the list, re-assigns head"
+
+[ee3729ee-3405-4bd2-9bad-de0d4aa5d647]
+description = "deletes the first of two elements"
+
+[47e3b3b4-b82c-4c23-8c1a-ceb9b17cb9fb]
+description = "deletes the second of two elements"
+
+[7b420958-f285-4922-b8f9-10d9dcab5179]
+description = "delete does not modify the list if the element is not found"
+
+[7e04828f-6082-44e3-a059-201c63252a76]
+description = "deletes only the first occurrence"

exercises/practice/linked-list/LinkedList.lean

@@ -0,0 +1,29 @@
+namespace LinkedList
+
+variable {α σ : Type} [BEq α]
+
+structure LinkedList (σ α : Type) where
+  -- You should define a data structure LinkedList to represent your doubly-linked list here.
+
+def LinkedList.empty : ST σ (LinkedList σ α) :=
+  sorry
+
+def LinkedList.count (list : LinkedList σ α) : ST σ Nat :=
+  sorry
+
+def LinkedList.push (value : α) (list : LinkedList σ α) : ST σ Unit :=
+  sorry
+
+def LinkedList.unshift (value : α) (list : LinkedList σ α) : ST σ Unit :=
+  sorry
+
+def LinkedList.pop (list : LinkedList σ α) : ST σ (Option α) :=
+  sorry
+
+def LinkedList.shift (list : LinkedList σ α) : ST σ (Option α) :=
+  sorry
+
+def LinkedList.delete (value : α) (list : LinkedList σ α) : ST σ Unit :=
+  sorry
+
+end LinkedList