+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "id": "0edff064",
+ "metadata": {},
+ "source": [
+ "# `remove`\n",
+ "\n",
+ " [1 2 3 4] 5 remove\n",
+ " ------------------------\n",
+ " [1 2 3 4]\n",
+ "\n",
+ " [1 2 3 4] 2 remove\n",
+ " ------------------------\n",
+ " [1 3 4]\n",
+ "\n",
+ " [] a remove\n",
+ " ------------------------\n",
+ " []\n",
+ "\n",
+ "## First attempt\n",
+ "\n",
+ "First let's handle the case of an empty list:\n",
+ "\n",
+ " remove == [pop not] [pop] [remove'] ifte\n",
+ "\n",
+ "For non-empty lists, the predicate and base case are easy:\n",
+ "\n",
+ " remove' == [swap first =] [pop rest] [R0] [R1] genrec\n",
+ "\n",
+ "The recursive branch:\n",
+ "\n",
+ " [1 2 3 4] 3 R0 [remove'] R1\n",
+ "\n",
+ "For `R0` use `[uncons] dip`:\n",
+ "\n",
+ " [1 2 3 4] 3 [uncons] dip [remove'] R1\n",
+ " [1 2 3 4] uncons 3 [remove'] R1\n",
+ " 1 [2 3 4] 3 [remove'] R1\n",
+ "\n",
+ "For `R1` let's try `i cons`:\n",
+ "\n",
+ " 1 [2 3 4] 3 [remove'] i cons\n",
+ " 1 [2 3 4] 3 remove' cons\n",
+ " ...\n",
+ " 1 2 [3 4] 3 remove' cons cons\n",
+ " ...\n",
+ " 1 2 [4] cons cons\n",
+ " ...\n",
+ " [1 2 4]\n",
+ "\n",
+ "Ergo:\n",
+ "\n",
+ " remove' == [swap first =] [pop rest] [[uncons] dip] [i cons] genrec\n",
+ " remove == [pop not] [pop] [remove'] ifte\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "id": "80f0926d",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": []
+ }
+ ],
+ "source": [
+ "[remove' [swap first =] [pop rest] [[uncons] dip] [i cons] genrec] inscribe\n",
+ "[remo [pop not] [pop] [remove'] ifte] inscribe"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "id": "6ef0d06a",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[1 2 3 4] 3"
+ ]
+ }
+ ],
+ "source": [
+ "[1 2 3 4] 3 "
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "id": "e0c12f34",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[1 2 4]"
+ ]
+ }
+ ],
+ "source": [
+ "remo"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "e34f9996",
+ "metadata": {},
+ "source": [
+ "So far so good but I made a mistake. The recursive part doesn't handle empty lists, so it's broken for the case of the item not being in the list:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "id": "ecb11a12",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[1 2 4] 45"
+ ]
+ }
+ ],
+ "source": [
+ "45"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "fb6472f5",
+ "metadata": {},
+ "outputs": [],
+ "source": [
+ " remo"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "fd33d021",
+ "metadata": {},
+ "source": [
+ "## Second attempt\n",
+ "\n",
+ " remove == [pop not] [pop] [R0] [R1] genrec\n",
+ " remove == [pop not] [pop] [R0 [remove] R1] ifte\n",
+ "\n",
+ "Non-empty:\n",
+ "\n",
+ " [a b c] item R0 [remove] R1\n",
+ "\n",
+ "\n",
+ " R0 [remove] R1\n",
+ " -----------------------------------------------------\n",
+ " [swap first =] [pop rest] [E1 [remove] E2] ifte\n",
+ "\n",
+ "Recursive branch:\n",
+ "\n",
+ " [a b c] d E1 [remove] E2\n",
+ "\n",
+ "With:\n",
+ "\n",
+ " E1 == [uncons] dip\n",
+ " E2 == i cons\n",
+ "\n",
+ " [a b c] d [uncons] dip [remove] i cons\n",
+ " a [b c] d [remove] i cons\n",
+ " a [b c] d remove cons\n",
+ "\n",
+ "How to make it?\n",
+ "\n",
+ " R0 == [swap first =] [pop rest]\n",
+ "\n",
+ "Then we want:\n",
+ "\n",
+ " R1 == [[uncons] dip [remove] i cons] ifte\n",
+ "\n",
+ "But of course `[remove]` can't appear in there like that, we have to package it up:\n",
+ "\n",
+ " R1 == [i cons] cons [[uncons] dip] swoncat ifte\n",
+ "\n",
+ "Or better yet:\n",
+ "\n",
+ " [[uncons] dip remove cons] ifte\n",
+ "\n",
+ " R1 == [cons] concat [[uncons] dip] swoncat ifte\n",
+ "\n",
+ "Clunky, but it works:\n",
+ "\n",
+ " remove == [pop not] [pop] [[swap first =] [pop rest]] [[cons] concat [[uncons] dip] swoncat ifte] genrec\n",
+ " "
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 6,
+ "id": "891135c8",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[1 2 4] 45"
+ ]
+ }
+ ],
+ "source": [
+ "[remo2 [pop not] [pop] [[swap first =] [pop rest]] [[cons] concat [[uncons] dip] swoncat ifte] genrec] inscribe"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 7,
+ "id": "c32ea032",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[1 2 4]"
+ ]
+ }
+ ],
+ "source": [
+ "remo2"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 8,
+ "id": "6bd05f5b",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[1 2 4] 2"
+ ]
+ }
+ ],
+ "source": [
+ "2"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 9,
+ "id": "20bdec4c",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[1 4]"
+ ]
+ }
+ ],
+ "source": [
+ "remo2"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "7605e056",
+ "metadata": {},
+ "source": [
+ "## Third attempt\n",
+ "\n",
+ "What if we let `[remove]` be on the stack instead of building the else-part each iteration?:\n",
+ "\n",
+ " remove == [pop not] [pop] [] [[P] [THEN] [ELSE] ifte] genrec\n",
+ " remove == [pop not] [pop] [ [remove] [P] [THEN] [ELSE] ifte] ifte\n",
+ "\n",
+ "So:\n",
+ "\n",
+ " [a b c] item [remove] [P] [THEN] [ELSE] ifte\n",
+ " \n",
+ " P == pop swap first =\n",
+ " \n",
+ " THEN == popop rest\n",
+ " \n",
+ " ELSE == ...\n",
+ "\n",
+ "Hmm...\n",
+ "\n",
+ " [a b c] item [remove] ELSE\n",
+ " [a b c] item [remove] [uncons] dipd i cons\n",
+ " a [b c] item [remove] i cons\n",
+ " a [b c] item remove cons\n",
+ " ...\n",
+ " a [b c] cons\n",
+ " [a b c]\n",
+ "\n",
+ "So:\n",
+ "\n",
+ " ELSE == [uncons] dipd i cons\n",
+ "\n",
+ "And:\n",
+ "\n",
+ " remove == [pop not] [pop] [] [[pop swap first =] [popop rest] [[uncons] dipd i cons] ifte] genrec"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 10,
+ "id": "acd3f326",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[1 4]"
+ ]
+ }
+ ],
+ "source": [
+ "[remo3 [pop not] [pop] [] [[pop swap first =] [popop rest] [[uncons] dipd i cons] ifte] genrec] inscribe"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 11,
+ "id": "70178b16",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[1 4 5 6]"
+ ]
+ }
+ ],
+ "source": [
+ "[5 6] concat"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 12,
+ "id": "f6cb0b12",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[1 4 5 6] 5"
+ ]
+ }
+ ],
+ "source": [
+ "5"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 13,
+ "id": "d2e6aeb8",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[1 4 6]"
+ ]
+ }
+ ],
+ "source": [
+ "remo3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 14,
+ "id": "f2c8c0be",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[1 4 6] 5"
+ ]
+ }
+ ],
+ "source": [
+ "5"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 15,
+ "id": "deb5e389",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[1 4 6]"
+ ]
+ }
+ ],
+ "source": [
+ "remo3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 16,
+ "id": "84fc4e3f",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[] 5"
+ ]
+ }
+ ],
+ "source": [
+ "pop [] 5"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 17,
+ "id": "ee99b894",
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[]"
+ ]
+ }
+ ],
+ "source": [
+ "remo3"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "id": "0518f168",
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "Joypy",
+ "language": "",
+ "name": "thun"
+ },
+ "language_info": {
+ "file_extension": ".joy",
+ "mimetype": "text/plain",
+ "name": "Joy"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}