Add Zipper practice exercise

config.json

@@ -642,6 +642,14 @@
         "prerequisites": [],
         "difficulty": 7
       },
+      {
+        "slug": "zipper",
+        "name": "Zipper",
+        "uuid": "f7bdcd13-7231-4895-a1f8-2f22838a6738",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 7
+      },
       {
         "slug": "all-your-base",
         "name": "All Your Base",

exercises/practice/difference-of-squares/.approaches/config.json

@@ -1,7 +1,8 @@
 {
   "introduction": {
-    "authors": ["oxe-i"],
-    "contributors": []
+    "authors": [
+      "oxe-i"
+    ]
   },
   "approaches": [
     {

exercises/practice/zipper/.docs/instructions.md

@@ -0,0 +1,27 @@
+# Instructions
+
+Creating a zipper for a binary tree.
+
+[Zippers][zipper] are a purely functional way of navigating within a data structure and manipulating it.
+They essentially contain a data structure and a pointer into that data structure (called the focus).
+
+For example given a rose tree (where each node contains a value and a list of child nodes) a zipper might support these operations:
+
+- `from_tree` (get a zipper out of a rose tree, the focus is on the root node)
+- `to_tree` (get the rose tree out of the zipper)
+- `value` (get the value of the focus node)
+- `prev` (move the focus to the previous child of the same parent,
+  returns a new zipper)
+- `next` (move the focus to the next child of the same parent, returns a
+  new zipper)
+- `up` (move the focus to the parent, returns a new zipper)
+- `set_value` (set the value of the focus node, returns a new zipper)
+- `insert_before` (insert a new subtree before the focus node, it
+  becomes the `prev` of the focus node, returns a new zipper)
+- `insert_after` (insert a new subtree after the focus node, it becomes
+  the `next` of the focus node, returns a new zipper)
+- `delete` (removes the focus node and all subtrees, focus moves to the
+  `next` node if possible otherwise to the `prev` node if possible,
+  otherwise to the parent node, returns a new zipper)
+
+[zipper]: https://en.wikipedia.org/wiki/Zipper_%28data_structure%29

exercises/practice/zipper/.meta/Example.lean

@@ -0,0 +1,65 @@
+namespace Zipper
+
+inductive BinTree (α : Type) where
+  | nil  : BinTree α
+  | node : α → BinTree α → BinTree α → BinTree α
+  deriving BEq, Repr, Inhabited
+
+inductive Crumb (α : Type) where
+  | leftOf  : α → BinTree α → Crumb α
+  | rightOf : α → BinTree α → Crumb α
+  deriving BEq, Repr
+
+structure Zipper (α : Type) where
+  focus  : BinTree α
+  crumbs : List (Crumb α)
+  deriving BEq, Repr
+
+def fromTree (tree : BinTree α) : Zipper α :=
+  { focus := tree, crumbs := [] }
+
+def Zipper.toTree : Zipper α → BinTree α
+  | { focus, crumbs := [] } => focus
+  | { focus, crumbs := .leftOf v r :: cs } =>
+    Zipper.toTree { focus := .node v focus r, crumbs := cs }
+  | { focus, crumbs := .rightOf v l :: cs } =>
+    Zipper.toTree { focus := .node v l focus, crumbs := cs }
+
+def Zipper.value : Zipper α → Option α
+  | { focus := .nil, .. } => none
+  | { focus := .node v _ _, .. } => some v
+
+def Zipper.left : Zipper α → Option (Zipper α)
+  | { focus := .nil, .. } => none
+  | { focus := .node v l r, crumbs } =>
+    match l with
+    | .nil => none
+    | _    => some { focus := l, crumbs := .leftOf v r :: crumbs }
+
+def Zipper.right : Zipper α → Option (Zipper α)
+  | { focus := .nil, .. } => none
+  | { focus := .node v l r, crumbs } =>
+    match r with
+    | .nil => none
+    | _    => some { focus := r, crumbs := .rightOf v l :: crumbs }
+
+def Zipper.up : Zipper α → Option (Zipper α)
+  | { crumbs := [], .. } => none
+  | { focus, crumbs := .leftOf v r :: cs } =>
+    some { focus := .node v focus r, crumbs := cs }
+  | { focus, crumbs := .rightOf v l :: cs } =>
+    some { focus := .node v l focus, crumbs := cs }
+
+def Zipper.setValue (val : α) : Zipper α → Zipper α
+  | { focus := .nil, crumbs } => { focus := .nil, crumbs }
+  | { focus := .node _ l r, crumbs } => { focus := .node val l r, crumbs }
+
+def Zipper.setLeft (tree : BinTree α) : Zipper α → Zipper α
+  | { focus := .nil, crumbs } => { focus := .nil, crumbs }
+  | { focus := .node v _ r, crumbs } => { focus := .node v tree r, crumbs }
+
+def Zipper.setRight (tree : BinTree α) : Zipper α → Zipper α
+  | { focus := .nil, crumbs } => { focus := .nil, crumbs }
+  | { focus := .node v l _, crumbs } => { focus := .node v l tree, crumbs }
+
+end Zipper

exercises/practice/zipper/.meta/config.json

@@ -0,0 +1,18 @@
+{
+  "authors": [
+    "jojo8356"
+  ],
+  "files": {
+    "solution": [
+      "Zipper.lean"
+    ],
+    "test": [
+      "ZipperTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "blurb": "Creating a zipper for a binary tree.",
+  "source": "https://en.wikipedia.org/wiki/Zipper_%28data_structure%29"
+}

exercises/practice/zipper/.meta/extra.json

@@ -0,0 +1,135 @@
+{
+  "exercise": "zipper",
+  "comments": [
+    "Extra test cases for the Lean track to test polymorphic tree support."
+  ],
+  "cases": [
+    {
+      "description": "string tree: data is retained",
+      "property": "expectedValue",
+      "input": {
+        "initialTree": {
+          "value": "a",
+          "left": {
+            "value": "b",
+            "left": null,
+            "right": {
+              "value": "c",
+              "left": null,
+              "right": null
+            }
+          },
+          "right": {
+            "value": "d",
+            "left": null,
+            "right": null
+          }
+        },
+        "operations": [
+          {
+            "operation": "to_tree"
+          }
+        ]
+      },
+      "expected": {
+        "type": "tree",
+        "value": {
+          "value": "a",
+          "left": {
+            "value": "b",
+            "left": null,
+            "right": {
+              "value": "c",
+              "left": null,
+              "right": null
+            }
+          },
+          "right": {
+            "value": "d",
+            "left": null,
+            "right": null
+          }
+        }
+      }
+    },
+    {
+      "description": "string tree: left, right and value",
+      "property": "expectedValue",
+      "input": {
+        "initialTree": {
+          "value": "a",
+          "left": {
+            "value": "b",
+            "left": null,
+            "right": {
+              "value": "c",
+              "left": null,
+              "right": null
+            }
+          },
+          "right": {
+            "value": "d",
+            "left": null,
+            "right": null
+          }
+        },
+        "operations": [
+          { "operation": "left" },
+          { "operation": "right" },
+          { "operation": "value" }
+        ]
+      },
+      "expected": {
+        "type": "string",
+        "value": "c"
+      }
+    },
+    {
+      "description": "string tree: set_value",
+      "property": "expectedValue",
+      "input": {
+        "initialTree": {
+          "value": "a",
+          "left": {
+            "value": "b",
+            "left": null,
+            "right": {
+              "value": "c",
+              "left": null,
+              "right": null
+            }
+          },
+          "right": {
+            "value": "d",
+            "left": null,
+            "right": null
+          }
+        },
+        "operations": [
+          { "operation": "left" },
+          { "operation": "set_value", "item": "x" }
+        ]
+      },
+      "expected": {
+        "type": "tree",
+        "value": {
+          "value": "a",
+          "left": {
+            "value": "x",
+            "left": null,
+            "right": {
+              "value": "c",
+              "left": null,
+              "right": null
+            }
+          },
+          "right": {
+            "value": "d",
+            "left": null,
+            "right": null
+          }
+        }
+      }
+    }
+  ]
+}

exercises/practice/zipper/.meta/tests.toml

@@ -0,0 +1,52 @@
+# 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.
+
+[771c652e-0754-4ef0-945c-0675d12ef1f5]
+description = "data is retained"
+
+[d7dcbb92-47fc-4d01-b81a-df3353bc09ff]
+description = "left, right and value"
+
+[613d8286-b05c-4453-b205-e6f9c5966339]
+description = "dead end"
+
+[dda31af7-1c68-4e29-933a-c9d198d94284]
+description = "tree from deep focus"
+
+[1e3072a6-f85b-430b-b014-cdb4087e3577]
+description = "traversing up from top"
+
+[b8505f6a-aed4-4c2e-824f-a0ed8570d74b]
+description = "left, right, and up"
+
+[b9aa8d54-07b7-4bfd-ab6b-7ff7f35930b6]
+description = "test ability to descend multiple levels and return"
+
+[47df1a27-b709-496e-b381-63a03b82ea5f]
+description = "set_value"
+
+[16a1f1a8-dbed-456d-95ac-1cbb6093e0ab]
+description = "set_value after traversing up"
+
+[535a91af-a02e-49cd-8d2c-ecb6e4647174]
+description = "set_left with leaf"
+
+[b3f60c4b-a788-4ffd-be5d-1e69aee61de3]
+description = "set_right with null"
+
+[e91c221d-7b90-4604-b4ec-46638a673a12]
+description = "set_right with subtree"
+
+[c246be85-6648-4e9c-866f-b08cd495149a]
+description = "set_value on deep focus"
+
+[47aa85a0-5240-48a4-9f42-e2ac636710ea]
+description = "different paths to same zipper"

exercises/practice/zipper/Zipper.lean

@@ -0,0 +1,23 @@
+namespace Zipper
+
+/-
+  You should define:
+
+  1. A `BinTree` type representing a binary tree where each node
+     has a value, a left subtree, and a right subtree.
+
+  2. A `Zipper` type that allows navigating within a binary tree.
+
+  3. The following functions:
+     - `fromTree`  : Create a zipper focused on the root of a tree.
+     - `toTree`    : Reconstruct the full tree from a zipper.
+     - `value`     : Get the value of the focused node.
+     - `left`      : Move focus to the left child (returns Option).
+     - `right`     : Move focus to the right child (returns Option).
+     - `up`        : Move focus to the parent (returns Option).
+     - `setValue`  : Set the value of the focused node.
+     - `setLeft`   : Set the left subtree of the focused node.
+     - `setRight`  : Set the right subtree of the focused node.
+-/
+
+end Zipper