485 lines
9.2 KiB
Plaintext
485 lines
9.2 KiB
Plaintext
{
|
|
"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
|
|
}
|