3114 lines
61 KiB
Plaintext
3114 lines
61 KiB
Plaintext
{
|
|
"cells": [
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 1,
|
|
"id": "73967878",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"[all true swap [&] step] inscribe\n",
|
|
"[any false swap [|] step] inscribe"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 2,
|
|
"id": "b34d58ef",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"[base 2147483648] inscribe"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "9749000b",
|
|
"metadata": {},
|
|
"source": [
|
|
"Model bigints as a pair of Boolean for the sign and a list of integers for the digits, to keep things simple let the bool be the first item on a list followed by zero or more int digits. The digits shall be confined to the range zero to `pow(2, 31) - 1`\n",
|
|
"\n",
|
|
"Another way to say that is that our numbers are in base `2147483648` and our \"nine\" is `2147483647` (`0b1111111111111111111111111111111`, 31 ones.)\n",
|
|
"\n",
|
|
"This lets us use (Oberon RISC) 32-bit signed ints to store our digits."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "956c8ee2",
|
|
"metadata": {},
|
|
"source": [
|
|
"## Take Two\n",
|
|
"\n",
|
|
"This really got away from me the first time. I think the big mistake ai made was including the middle branch in the recursive branch.\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "afe33f94",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "03a44beb",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "9947b864",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "e91b6e37",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "8e7d4379",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "211669e7",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "d7ee0e4a",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "c9f34050",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "9d5972c4",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "cd6dc2e4",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "0beeac21",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "ccc32d74",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "7d2c5b56",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "83cbf474",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "be9be8d9",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "4c7df3f0",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "88f27acd",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "960edfef",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "2b3cad6c",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "7c613941",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "991f0d25",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "c3221039",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "ff5ab28c",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "58a46766",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "f488664c",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "5eefa527",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "d1f695de",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "22e5236c",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "5e069159",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "8e2fc444",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "025672cb",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "3359c82f",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "011563c0",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "f0e5eb9a",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "cb5a858d",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "936ef79c",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "e8a8bbe9",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "80672bab",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "aa635304",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "eba35315",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "14e8ca33",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 3,
|
|
"id": "35476eac",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"[valid_digit [0 >] [base <] &&] inscribe"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 4,
|
|
"id": "02a48806",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"32 true 1232147483648 false"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"32 valid_digit 1232147483648 valid_digit"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 5,
|
|
"id": "1d276daf",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"true"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"[true 3 2 1]\n",
|
|
"rest [valid_digit] map all"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 6,
|
|
"id": "2454e662",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[true 3 2 1]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"[true 3 2 1]"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "bfed1f25",
|
|
"metadata": {},
|
|
"source": [
|
|
"Because we are working with Python Joy right now we can convert ints to bigints.\n",
|
|
"\n",
|
|
"To get the sign bool we can just use `!-` (\"not negative\")"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 7,
|
|
"id": "8a60b54b",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"true false"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"23 !- -23 !-"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "73bfa634",
|
|
"metadata": {},
|
|
"source": [
|
|
"To get the list of digits...\n",
|
|
"\n",
|
|
"```\n",
|
|
" @staticmethod\n",
|
|
" def digitize(n):\n",
|
|
" if n < 0:\n",
|
|
" raise ValueError(f'Non-negative only: {n}')\n",
|
|
" while n:\n",
|
|
" n, digit = divmod(n, 2**31)\n",
|
|
" yield OberonInt(digit)\n",
|
|
"\n",
|
|
"```\n",
|
|
"\n",
|
|
" [0 >=] [base divmod swap] while"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 8,
|
|
"id": "3fc98ccd",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"1797196498 5748904729"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"12345678901234567890 base divmod swap"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 9,
|
|
"id": "b838c4cb",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"1797196498 1453937433 2"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"base divmod swap"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "4d9d926a",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 10,
|
|
"id": "faaac9d6",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"1312754386 1501085485 57659106 105448366 58"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"1234567890123456789012345678901234567890\n",
|
|
" [0 >] [base divmod swap] while pop"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 11,
|
|
"id": "2a613f36",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[58 105448366 57659106 1501085485 1312754386]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"[1234567890123456789012345678901234567890]\n",
|
|
" [ [0 >] [base divmod swap] while pop ]\n",
|
|
" infra"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 12,
|
|
"id": "e97b149d",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"1234567890123456789012345678901234567890 [0 <=] [pop []] [base divmod swap] [i cons]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"1234567890123456789012345678901234567890\n",
|
|
" [0 <=] [pop []] [base divmod swap] [i cons]"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 13,
|
|
"id": "de4fe588",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[1312754386 1501085485 57659106 105448366 58]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"genrec"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 14,
|
|
"id": "67bb934b",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"0 [0 <=] [pop []] [base divmod swap] [i cons] genrec"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 15,
|
|
"id": "e4c66f15",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"[digitalize [0 <=] [pop []] [base divmod swap] [i cons] genrec] inscribe"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 16,
|
|
"id": "b6f77ac6",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[1312754386 1501085485 57659106 105448366 58]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"1234567890123456789012345678901234567890 digitalize"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "1bf8ba9e",
|
|
"metadata": {},
|
|
"source": [
|
|
"So `!-` for the sign and `abs digitalize` for the digits, followed by `cons`:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 17,
|
|
"id": "246c2a58",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[true 1312754386 1501085485 57659106 105448366 58]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"1234567890123456789012345678901234567890 [!-] [abs digitalize] cleave cons"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 18,
|
|
"id": "5a72ce30",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[true 1312754386 1501085485 57659106 105448366 58]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"[to_bigint [!-] [abs digitalize] cleave cons] inscribe"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 19,
|
|
"id": "59514dcd",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[true 1312754386 1501085485 57659106 105448366 58]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"1234567890123456789012345678901234567890 to_bigint"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 20,
|
|
"id": "f3c19364",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[false 1312754386 1501085485 57659106 105448366 58]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"-1234567890123456789012345678901234567890 to_bigint"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "4dbd0f30",
|
|
"metadata": {},
|
|
"source": [
|
|
"## Addition of Like Signs\n",
|
|
"\n",
|
|
"I think we're going to want a recursive function (duh!?) but it's not quite a standard *hylomorphism* for (at least) two reasons:\n",
|
|
"\n",
|
|
"- We're tearing down two lists simultaneously.\n",
|
|
"- They might not be the same length.\n",
|
|
"\n",
|
|
"The base case would be two empty lists. In that case the result is determined by the `carry` bit, (Should zero be represented by the empty list `[]`, by `[0]`, or by both?) zero or one.\n",
|
|
"\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 21,
|
|
"id": "dd25bb96",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"false"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"[] bool"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 22,
|
|
"id": "c9bdd641",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"true"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"[] [] [bool not] ii &"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "50665e75",
|
|
"metadata": {},
|
|
"source": [
|
|
"### Predicate\n",
|
|
"so the predicate for the whole thing would be"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 121,
|
|
"id": "187aa6ec",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"[_add_p [bool not] ii &] inscribe"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 123,
|
|
"id": "ee3d2316",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"true"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"[][]_add_p"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 124,
|
|
"id": "7e8c4942",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"false"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"[1][]_add_p"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 125,
|
|
"id": "8b41766c",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"false"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"[][1]_add_p"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 126,
|
|
"id": "1bacc617",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"false"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"[1][1]_add_p"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "abe20e0b",
|
|
"metadata": {},
|
|
"source": [
|
|
"### Base Case\n",
|
|
"In the base case we discard one list and check the carry to determine our result as decribed above:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 127,
|
|
"id": "5e5ddf74",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[1]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"true [] [] pop swap [] [1 swons] branch"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 128,
|
|
"id": "c57d1fb2",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"false [] [] pop swap [] [1 swons] branch"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 129,
|
|
"id": "59b1338c",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"clear"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 31,
|
|
"id": "ed38fdb1",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"[_add_then pop swap [] [1 swons] branch] inscribe"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "978b5cac",
|
|
"metadata": {},
|
|
"source": [
|
|
"### Recursive Branch\n",
|
|
"So (ignoring the source of the initial carry bit for now) we have:\n",
|
|
"\n",
|
|
" _add_p == [bool not] ii &\n",
|
|
" _add_then == pop swap [] [1 swons] branch\n",
|
|
"\n",
|
|
" add_digits == [_add_p] [_add_then] [R0] [R1] genrec\n",
|
|
"\n",
|
|
"What should the recursive branch do?\n",
|
|
"\n",
|
|
"It will be some `ifte` expression:\n",
|
|
"\n",
|
|
" R0 [add_digits] R1 == [P] [THEN] [ELSE] ifte\n",
|
|
"\n",
|
|
"Ideally, we can arrange to neatly bracket the `[add_digits]` quote, but otherwise we can build up the `ifte` quotes in the usual way with `cons` and `concat`."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "7246fe3d",
|
|
"metadata": {},
|
|
"source": [
|
|
"#### Is One List Empty?\n",
|
|
"The context will be a Boolean carry bit and two lists, one of which (but not both!) may be empty.\n",
|
|
"\n",
|
|
" carry [a ...] [b ...] R0 [add_digits] R1\n",
|
|
"\n",
|
|
" carry [] [b ...] R0 [add_digits] R1\n",
|
|
"\n",
|
|
" carry [a ...] [] R0 [add_digits] R1\n",
|
|
"\n",
|
|
"So I think the first thing to do is detect and handle the (possibly) empty lists?"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "d54e0860",
|
|
"metadata": {},
|
|
"source": [
|
|
"#### predicate"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 92,
|
|
"id": "728f7b72",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"true"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"[1] [1] [bool] ii &"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 93,
|
|
"id": "3561502a",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"false"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"[1] [] [bool] ii &"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 94,
|
|
"id": "2c395fcc",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"false"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"[] [1] [bool] ii &"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "13993d1f",
|
|
"metadata": {},
|
|
"source": [
|
|
"So our `ifte` predicate is `[bool] ii &`, what's the rest look like?\n",
|
|
"\n",
|
|
" [[bool] ii &] ... [add_digits] ... ifte\n",
|
|
"\n",
|
|
"We will need `add_digits` on the `true` branch to deal with the rest of the lists, but not (I think) on the false branch?\n",
|
|
"\n",
|
|
" [[bool] ii &] [... [add_digits] ...] [ELSE] ifte"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 130,
|
|
"id": "9caf15b4",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"[_add_rec_pred [bool] ii &] inscribe"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "2adf3f59",
|
|
"metadata": {},
|
|
"source": [
|
|
"#### `true` branch\n",
|
|
"Let's square away the `true` branch first.\n",
|
|
"\n",
|
|
" carry [a ...] [b ...] ... [add_digits] ...\n",
|
|
"\n",
|
|
"First we will want to `uncons` the digits"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 95,
|
|
"id": "1e53236f",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"false 1 4 [2 3] [5 6]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"false [1 2 3] [4 5 6] [uncons] ii swapd"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "8d66b26b",
|
|
"metadata": {},
|
|
"source": [
|
|
"#### add-with-carry\n",
|
|
"So now we want some function `F` to `dipd` below the list tails that accepts a bool and two ints and leaves behind a new int and a new Boolean carry flag:\n",
|
|
"\n",
|
|
" carry0 a b F\n",
|
|
" --------------------------\n",
|
|
" (a+b+carry0) carry\n",
|
|
"\n",
|
|
"(I find it interesting that this function accepts the carry from below the int args but returns it above the result. Hmm...)"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 96,
|
|
"id": "2f70ca25",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"0 1"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"[bool_to_int [0] [1] branch] inscribe\n",
|
|
"\n",
|
|
"false bool_to_int\n",
|
|
"true bool_to_int"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 97,
|
|
"id": "c19916c5",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"3"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"false 1 2 [bool_to_int] dipd + +"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 98,
|
|
"id": "ead4cc5e",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"4"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"true 1 2 [bool_to_int] dipd + +"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "ddb201ca",
|
|
"metadata": {},
|
|
"source": [
|
|
"So the first part of `F` is `[bool_to_int] dipd + +` to get the total, then we need to"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 99,
|
|
"id": "129997e0",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"4"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"base mod"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 100,
|
|
"id": "22209a15",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"false"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"base >="
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 101,
|
|
"id": "57649cf3",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"4 false"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"4 base [mod] [>=] clop"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 102,
|
|
"id": "3c2e42be",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"100 true"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"base 100 +\n",
|
|
"\n",
|
|
"base [mod] [>=] clop"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "893a39c4",
|
|
"metadata": {},
|
|
"source": [
|
|
"\n",
|
|
" F == [bool_to_int] dipd + + base [mod] [>=] clop\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 103,
|
|
"id": "257d757c",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"[_add-with-carry0 [bool_to_int] dipd + +] inscribe\n",
|
|
"[_add-with-carry1 base [mod] [>=] clop] inscribe\n",
|
|
"[add-with-carry _add-with-carry0 _add-with-carry1] inscribe"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 104,
|
|
"id": "1d50a1c6",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"100 true"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"false base 100 add-with-carry"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 105,
|
|
"id": "b93ae376",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"101 true"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"true base 100 add-with-carry"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 106,
|
|
"id": "4f86c2c7",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"102 false"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"false 2 100 add-with-carry"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 107,
|
|
"id": "68a8a9c2",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"103 false"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"true 2 100 add-with-carry"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "e9a512f0",
|
|
"metadata": {},
|
|
"source": [
|
|
"Going back to our `true` branch we have:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 108,
|
|
"id": "74873f5b",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"false 1 4 [2 3] [5 6]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"false [1 2 3] [4 5 6] [uncons] ii swapd"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "5520db54",
|
|
"metadata": {},
|
|
"source": [
|
|
"#### `uncons-two`\n",
|
|
"We could call this `uncons-two`:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 116,
|
|
"id": "e7176ea9",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"1 4 [2 3] [5 6]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"[uncons-two [uncons] ii swapd] inscribe\n",
|
|
"\n",
|
|
"[1 2 3] [4 5 6] uncons-two"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 117,
|
|
"id": "64b575f7",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"clear"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "9445eb3c",
|
|
"metadata": {},
|
|
"source": [
|
|
"Plugging in `add-with-carry` we get:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 118,
|
|
"id": "7e745018",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"5 false [2 3] [5 6]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"false [1 2 3] [4 5 6] uncons-two [add-with-carry] dipd"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "121ff3c0",
|
|
"metadata": {},
|
|
"source": [
|
|
"### Recur\n",
|
|
"\n",
|
|
"It is at this point that we would recur:\n",
|
|
"\n",
|
|
" 5 false [2 3] [5 6] [add_digits] i ...\n",
|
|
" ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ \n",
|
|
"\n",
|
|
"This part runs and becomes some list (possibly empty) of result digits (the base case consumes the carry flag and one list):\n",
|
|
"\n",
|
|
" 5 [7 9]\n",
|
|
"\n",
|
|
"So our conclusion must be `cons`:\n",
|
|
"\n",
|
|
" 5 [7 9] cons\n",
|
|
" [5 7 9]\n",
|
|
"\n",
|
|
"And our whole branch function is:\n",
|
|
"\n",
|
|
" THEN == uncons-two [add-with-carry] dipd [add_digits] i cons\n",
|
|
"\n",
|
|
" [_add_rec_pred] [THEN] [ELSE] ifte\n",
|
|
"\n",
|
|
"It's a little tricky having that recursive call being nested like that:\n",
|
|
"\n",
|
|
" THEN0.1 == [add-with-carry] dipd\n",
|
|
" THEN0 == uncons-two THEN0.1\n",
|
|
" THEN1 == i cons\n",
|
|
"\n",
|
|
" [_add_rec_pred] [THEN0 [add_digits] THEN1] [ELSE] ifte\n",
|
|
"\n",
|
|
"But we can make it work."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "cd576704",
|
|
"metadata": {},
|
|
"source": [
|
|
"#### Interlude: Nested or Unnested?\n",
|
|
"\n",
|
|
" F == [P] [THEN] [R0] [R1] genrec\n",
|
|
" F == [P] [THEN] [R0 [F] R1] ifte\n",
|
|
"\n",
|
|
"Our recursive branch will take the form of an `ifte` expression that incorporates the function `[F]` into one of its branches:\n",
|
|
"\n",
|
|
" F == [P] [THEN] [[P0] [THEN0 [F] THEN1] [ELSE] ifte] ifte\n",
|
|
"\n",
|
|
" F == [P] [THEN] [[P0] [THEN0]] [F] [[THEN1] cons concat [ELSE] ifte] ifte\n",
|
|
"\n",
|
|
"\n",
|
|
"\n",
|
|
" [P0] [THEN0] [F] [THEN1] cons concat [ELSE] ifte\n",
|
|
" ------------------------------------------------------\n",
|
|
" [P0] [THEN0] [[F] THEN1] concat [ELSE] ifte\n",
|
|
" ------------------------------------------------------\n",
|
|
" [P0] [THEN0 [F] THEN1] [ELSE] ifte\n",
|
|
" ------------------------------------------------------\n",
|
|
" [P0] [THEN0 [F] THEN1] [ELSE] ifte\n",
|
|
"\n",
|
|
"It's awkward but it works."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 112,
|
|
"id": "4fcf1d97",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"clear"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "85a49679",
|
|
"metadata": {},
|
|
"source": [
|
|
"#### `false` branch\n",
|
|
"And now we deal with the cases where one of the two lists (but not both) is empty:\n",
|
|
"\n",
|
|
" carry [a ...] [] ELSE\n",
|
|
" carry [] [b ...] ELSE\n",
|
|
"\n",
|
|
"We get rid of the empty list:\n",
|
|
"\n",
|
|
"[bool] [popd] [pop] ifte"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 113,
|
|
"id": "affd02fb",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"[ditch-empty-list [bool] [popd] [pop] ifte] inscribe"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 114,
|
|
"id": "5cc19cea",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[1]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"[1][] ditch-empty-list"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 115,
|
|
"id": "12d72692",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[1]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"[][1] ditch-empty-list"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "aa76c2fc",
|
|
"metadata": {},
|
|
"source": [
|
|
"#### add-carry-to-digits\n",
|
|
"So now we have `carry` and one list of digits. (We also know that we have at least one digit in the list at this point but we likely won't need that information.)\n",
|
|
"\n",
|
|
" carry [a ...] add-carry-to-digits\n",
|
|
"\n",
|
|
"I think once we define `add-carry-to-digits` we are pretty much done? Let's find out."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "828699dc",
|
|
"metadata": {},
|
|
"source": [
|
|
"##### If `carry` is `false` we just return the digits list, eh?\n",
|
|
"\n",
|
|
" false [a ...] swap [] [THEN] branch\n",
|
|
" -----------------------------------------\n",
|
|
" [a ...]"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "2a386fe2",
|
|
"metadata": {},
|
|
"source": [
|
|
"##### If `true` we want to maybe reuse `add-with-carry`?\n",
|
|
"\n",
|
|
"\n",
|
|
" true [a ...] swap [THEN] [] branch\n",
|
|
" ----------------------------------------\n",
|
|
" [a ...] THEN\n",
|
|
" --------------------------------------\n",
|
|
" false 1 a add-with-carry [...] G\n",
|
|
" --------------------------------------\n",
|
|
" (1+a) carry [...] G\n",
|
|
" ------------------------------------------------\n",
|
|
" (1+a) carry [...] add-carry-to-digits cons\n",
|
|
" ------------------------------------------------\n",
|
|
" (1+a) [...] cons\n",
|
|
" ------------------------------------------------\n",
|
|
" [(1+a) ...]\n",
|
|
"\n",
|
|
"So `add-carry-to-digits` is a recursive function (not a `branch` after all.)"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "08a149fa",
|
|
"metadata": {},
|
|
"source": [
|
|
"Omitting `ditch-empty-list` for the moment:\n",
|
|
"\n",
|
|
" THEN == [false 1] dip uncons [add-with-carry] dip [add-carry-to-digits] i cons\n",
|
|
"\n",
|
|
" [a ...] THEN\n",
|
|
" [a ...] [false 1] dip uncons [add-with-carry] dip [add-carry-to-digits] i cons\n",
|
|
" false 1 [a ...] uncons [add-with-carry] dip [add-carry-to-digits] i cons\n",
|
|
" false 1 a [...] [add-with-carry] dip [add-carry-to-digits] i cons\n",
|
|
" false 1 a add-with-carry [...] [add-carry-to-digits] i cons\n",
|
|
" (1+a) false [...] [add-carry-to-digits] i cons\n",
|
|
" (1+a) false [...] add-carry-to-digits cons\n",
|
|
" (1+a) [...] cons\n",
|
|
" [(1+a) ...]\n",
|
|
"\n",
|
|
"QED"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 64,
|
|
"id": "9f4ebfd9",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"clear"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "afd8074b",
|
|
"metadata": {},
|
|
"source": [
|
|
"#### add-carry-to-digits, recursively\n",
|
|
"\n",
|
|
" carry [...] add-carry-to-digits\n",
|
|
"\n",
|
|
" carry [...] [P] [THEN] [R0] [R1] genrec\n",
|
|
"\n",
|
|
"So:\n",
|
|
"\n",
|
|
" P == swap not\n",
|
|
" \n",
|
|
"-or-\n",
|
|
"\n",
|
|
" P == pop not\n",
|
|
" \n",
|
|
"and\n",
|
|
"\n",
|
|
" THEN == popd\n",
|
|
"\n",
|
|
"That leaves:\n",
|
|
"\n",
|
|
" true [...] R0 [add-carry-to-digits] R1\n",
|
|
"\n",
|
|
"I am tempted to leave the transformation from the above form to\n",
|
|
"\n",
|
|
" true [...] popd [false 1] dip uncons [add-with-carry] dip [add-carry-to-digits] i cons\n",
|
|
"\n",
|
|
"as the proverbial \"exercise for the reader\" but it's kinda trivial:\n",
|
|
"\n",
|
|
" R0 == popd [false 1] dip uncons [add-with-carry] dip\n",
|
|
" R1 == i cons\n",
|
|
"\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 65,
|
|
"id": "0c095d53",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"2 false [2 3]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"true [1 2 3] popd [false 1] dip uncons [add-with-carry] dip"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 66,
|
|
"id": "e793bd13",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"2 [2 3]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"popd"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 67,
|
|
"id": "e5d3966a",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[2 2 3]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"cons"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 73,
|
|
"id": "c8aec12d",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"[add-carry-to-digits [pop not] [popd] [popd [false 1] dip uncons [add-with-carry] dip] [i cons] genrec] inscribe"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 74,
|
|
"id": "d290d896",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[2 2 3]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"true [1 2 3] add-carry-to-digits"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 75,
|
|
"id": "10cb7a1f",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[1 2 3]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"false [1 2 3] add-carry-to-digits"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 84,
|
|
"id": "89298766",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"true [2147483647 2147483647 2 3]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"true base -- dup [2 3] ccons"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 85,
|
|
"id": "af73db1b",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[0 0 3 3]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"add-carry-to-digits"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "69f59f45",
|
|
"metadata": {},
|
|
"source": [
|
|
"E.g. 3299 + 1 = 3300"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 90,
|
|
"id": "00fa293e",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"false [2147483647 2147483647 2 3]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"false base -- dup [2 3] ccons"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 91,
|
|
"id": "227a28f1",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[2147483647 2147483647 2 3]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"add-carry-to-digits"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "50d06f33",
|
|
"metadata": {},
|
|
"source": [
|
|
"So that seems like it works."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 119,
|
|
"id": "7e735e04",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"clear"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "b55599cb",
|
|
"metadata": {},
|
|
"source": [
|
|
"## Our Story So Far...\n",
|
|
" _add_p == [bool not] ii &\n",
|
|
" _add_then == pop swap [] [1 swons] branch\n",
|
|
" _add_rec_pred == [bool] ii &\n",
|
|
"\n",
|
|
" add_digits == [_add_p] [_add_then] [R0] [R1] genrec"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "f515f498",
|
|
"metadata": {},
|
|
"source": [
|
|
"Where:\n",
|
|
"\n",
|
|
" R0 [add_digits] R1\n",
|
|
" -----------------------------------------------------\n",
|
|
" [_add_rec_pred] [ THEN ] [ELSE] ifte\n",
|
|
" -----------------------------------------------------\n",
|
|
" [_add_rec_pred] [THEN0 [add_digits] THEN1] [ELSE] ifte\n",
|
|
"\n",
|
|
" THEN0 == uncons-two [add-with-carry] dipd\n",
|
|
"\n",
|
|
" THEN1 == i cons\n",
|
|
"\n",
|
|
" ELSE == ditch-empty-list add-carry-to-digits"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 131,
|
|
"id": "348e377d",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"[THEN0 uncons-two [add-with-carry] dipd] inscribe\n",
|
|
"[THEN1 i cons] inscribe\n",
|
|
"[ELSE ditch-empty-list add-carry-to-digits] inscribe"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "c3b2768f",
|
|
"metadata": {},
|
|
"source": [
|
|
"Recalling:\n",
|
|
"\n",
|
|
" [P0] [THEN0] [F] [THEN1] cons concat [ELSE] ifte\n",
|
|
" ------------------------------------------------------\n",
|
|
" [P0] [THEN0] [[F] THEN1] concat [ELSE] ifte\n",
|
|
" ------------------------------------------------------\n",
|
|
" [P0] [THEN0 [F] THEN1] [ELSE] ifte\n",
|
|
" ------------------------------------------------------\n",
|
|
" [P0] [THEN0 [F] THEN1] [ELSE] ifte"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "2d58b809",
|
|
"metadata": {},
|
|
"source": [
|
|
"Ergo:\n",
|
|
"\n",
|
|
" R0 == [_add_rec_pred] [THEN0]\n",
|
|
" R1 == [THEN1] cons concat [ELSE] ifte\n",
|
|
"\n",
|
|
" add_digits == [_add_p] [_add_then] [R0] [R1] genrec\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 132,
|
|
"id": "2219756c",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"[_add_R0 [_add_rec_pred] [THEN0]] inscribe\n",
|
|
"[_add_R1 [THEN1] cons concat [ELSE] ifte] inscribe"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 133,
|
|
"id": "80866347",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"[add_digits [_add_p] [_add_then] [_add_R0] [_add_R1] genrec] inscribe"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 134,
|
|
"id": "51314100",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"false [3 2 1] [8]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"false [3 2 1] [8] "
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 135,
|
|
"id": "63a589cb",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[11 2 1]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"add_digits"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 136,
|
|
"id": "b5c5b50b",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[2147483647 11 2 1]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"base -- swons"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 137,
|
|
"id": "1c81b4bc",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"false [2147483647 11 2 1] [23]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"false swap [23]"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 138,
|
|
"id": "cdd845ef",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[22 12 2 1]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"add_digits"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 142,
|
|
"id": "583a2390",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[2147483647] [1]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear base -- unit [1]"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "defedd4b",
|
|
"metadata": {},
|
|
"source": [
|
|
"When i tried it it failed and inspection revealed that I had forgotten to set the initial carry value."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 144,
|
|
"id": "532967be",
|
|
"metadata": {
|
|
"scrolled": true
|
|
},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"false [2147483647] [1]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear false base -- unit [1]"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 145,
|
|
"id": "e15c8b33",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[0 1]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"add_digits"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "84c6c958",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 148,
|
|
"id": "ca5c95af",
|
|
"metadata": {
|
|
"scrolled": true
|
|
},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"false [2147483647 2147483647 2147483647 2147483647] [1]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear false base -- unit dup concat dup concat [1]"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "3a6960ea",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "8c32715b",
|
|
"metadata": {},
|
|
"source": [
|
|
"#### I made a mistake in add-carry-to-digits\n",
|
|
"\n",
|
|
"The recursive branch:\n",
|
|
"\n",
|
|
" true [...] R0 [add-carry-to-digits] R1\n",
|
|
"\n",
|
|
"Must also deal with the case where the list is empty!\n",
|
|
"\n",
|
|
" true [] R0 [add-carry-to-digits] R1\n",
|
|
"\n",
|
|
"The `popd` is okay, but then we need a branch:\n",
|
|
"\n",
|
|
" R0 == popd ? [1 swons] [R0.t] branch\n",
|
|
" R0.t == [false 1] dip uncons [add-with-carry] dip\n",
|
|
"\n",
|
|
" R1 == i cons\n",
|
|
"\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "1b4b1302",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "cab5271f",
|
|
"metadata": {},
|
|
"source": [
|
|
"#### add-carry-to-digits, recursively, TAKE TWO\n",
|
|
"\n",
|
|
" carry [...] add-carry-to-digits\n",
|
|
"\n",
|
|
" carry [...] [P] [THEN] [R0] [R1] genrec\n",
|
|
"\n",
|
|
" P == pop not\n",
|
|
" THEN == popd\n",
|
|
"\n",
|
|
"That leaves one of:\n",
|
|
"\n",
|
|
" true [...] R0 [add-carry-to-digits] R1\n",
|
|
"\n",
|
|
"-or-\n",
|
|
"\n",
|
|
" true [] R0 [add-carry-to-digits] R1\n",
|
|
"\n",
|
|
"It would be fun to just set `R1` to `ifte`\n",
|
|
"\n",
|
|
" true [] R0 [add-carry-to-digits] ifte\n",
|
|
"\n",
|
|
"Which means that `R0` must be a predicate and the \"then\" branch.\n",
|
|
"\n",
|
|
" true [] [bool not] [THEN] [add-carry-to-digits] ifte\n",
|
|
"\n",
|
|
"And I think `THEN` would just be:\n",
|
|
"\n",
|
|
" THEN == popd 1 swons\n",
|
|
"\n",
|
|
"\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 162,
|
|
"id": "955aed77",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"[R0.t [false 1] dip uncons [add-with-carry] dip] inscribe\n",
|
|
"[add-carry-to-digits\n",
|
|
" [pop not]\n",
|
|
" [popd]\n",
|
|
" [[bool not] [popd 1 swons]]\n",
|
|
" [ifte]\n",
|
|
" genrec\n",
|
|
"] inscribe"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "1ee5b941",
|
|
"metadata": {},
|
|
"source": [
|
|
"This is still broken because the "
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 160,
|
|
"id": "8ca1f509",
|
|
"metadata": {
|
|
"scrolled": true
|
|
},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"true [2147483647 2147483647 2147483647 2147483647]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear true base -- unit dup concat dup concat"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "77e2e26f",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"add-carry-to-digits"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "07a528bd",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "97ed01aa",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "dee054a6",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "f92eebb0",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "36e683fd",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "91ffeec1",
|
|
"metadata": {},
|
|
"source": [
|
|
"#### add-carry-to-digits\n",
|
|
"\n",
|
|
"So `add-carry-to-digits` is a recursive function:\n",
|
|
"\n",
|
|
" carry [a ...] add-carry-to-digits\n",
|
|
"\n",
|
|
" carry [a ...] [P] [THEN] [R0] [R1] genrec\n",
|
|
"\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "dc5f3cba",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"[pop not] [popd] [[bool not] [1 cons swap]] [ifte] genrec"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "6201b301",
|
|
"metadata": {},
|
|
"source": [
|
|
"##### If `carry` is `false` we just return the digits list, eh?\n",
|
|
"\n",
|
|
" false [a ...] [pop not] [popd] [R0] [R1] genrec\n",
|
|
" -----------------------------------------------------\n",
|
|
" [a ...]"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "2ffbb77c",
|
|
"metadata": {},
|
|
"source": [
|
|
"##### If `true` we want to maybe reuse `add-with-carry`?\n",
|
|
"\n",
|
|
" true [a ...] R0 [add-carry-to-digits] R1\n",
|
|
"\n",
|
|
"-or-\n",
|
|
"\n",
|
|
" true [] R0 [add-carry-to-digits] R1\n",
|
|
"\n",
|
|
"Um...\n",
|
|
"\n",
|
|
" true [] [bool not] [1 cons popd] [add-carry-to-digits] ifte\n",
|
|
"\n",
|
|
"\n",
|
|
" true [] [bool not] [1 cons popd] [add-carry-to-digits] ifte\n",
|
|
" true [] 1 cons popd\n",
|
|
" true [1] popd\n",
|
|
" [1]\n",
|
|
"\n",
|
|
"-or-\n",
|
|
"\n",
|
|
" true [a ...] [bool not] [1 cons swap] [F add-carry-to-digits] itfe\n",
|
|
" true [a ...] F add-carry-to-digits\n",
|
|
"\n",
|
|
"\n",
|
|
" true [a ...] F add-carry-to-digits\n",
|
|
" ---------------------------------------------------------\n",
|
|
" true 0 a add-with-carry [...] add-carry-to-digits\n",
|
|
"\n",
|
|
" \n",
|
|
" F == 0 swap uncons [add-with-carry] dip\n",
|
|
"\n",
|
|
"\n",
|
|
" true [a ...] [bool not] [1 cons swap] [add-carry-to-digits] [F] swoncat itfe\n",
|
|
"\n",
|
|
"\n",
|
|
"\n",
|
|
" true [a ...] [bool not] [1 cons swap] [add-carry-to-digits] [0 swap uncons [add-with-carry] dip] swoncat itfe\n",
|
|
"\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 162,
|
|
"id": "0ee18517",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"[R0.t [false 1] dip uncons [add-with-carry] dip] inscribe\n",
|
|
"[add-carry-to-digits\n",
|
|
" [pop not]\n",
|
|
" [popd]\n",
|
|
" [[bool not] [popd 1 swons]]\n",
|
|
" [ifte]\n",
|
|
" genrec\n",
|
|
"] inscribe"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "965cf4df",
|
|
"metadata": {},
|
|
"source": [
|
|
"Omitting `ditch-empty-list` for the moment:\n",
|
|
"\n",
|
|
" THEN == [false 1] dip uncons [add-with-carry] dip [add-carry-to-digits] i cons\n",
|
|
"\n",
|
|
" [a ...] THEN\n",
|
|
" [a ...] [false 1] dip uncons [add-with-carry] dip [add-carry-to-digits] i cons\n",
|
|
" false 1 [a ...] uncons [add-with-carry] dip [add-carry-to-digits] i cons\n",
|
|
" false 1 a [...] [add-with-carry] dip [add-carry-to-digits] i cons\n",
|
|
" false 1 a add-with-carry [...] [add-carry-to-digits] i cons\n",
|
|
" (1+a) false [...] [add-carry-to-digits] i cons\n",
|
|
" (1+a) false [...] add-carry-to-digits cons\n",
|
|
" (1+a) [...] cons\n",
|
|
" [(1+a) ...]\n",
|
|
"\n",
|
|
"QED"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 64,
|
|
"id": "1787863d",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"clear"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "77eeace6",
|
|
"metadata": {},
|
|
"source": [
|
|
"#### add-carry-to-digits, recursively\n",
|
|
"\n",
|
|
" carry [...] add-carry-to-digits\n",
|
|
"\n",
|
|
" carry [...] [P] [THEN] [R0] [R1] genrec\n",
|
|
"\n",
|
|
"So:\n",
|
|
"\n",
|
|
" P == swap not\n",
|
|
" \n",
|
|
"-or-\n",
|
|
"\n",
|
|
" P == pop not\n",
|
|
" \n",
|
|
"and\n",
|
|
"\n",
|
|
" THEN == popd\n",
|
|
"\n",
|
|
"That leaves:\n",
|
|
"\n",
|
|
" true [...] R0 [add-carry-to-digits] R1\n",
|
|
"\n",
|
|
"I am tempted to leave the transformation from the above form to\n",
|
|
"\n",
|
|
" true [...] popd [false 1] dip uncons [add-with-carry] dip [add-carry-to-digits] i cons\n",
|
|
"\n",
|
|
"as the proverbial \"exercise for the reader\" but it's kinda trivial:\n",
|
|
"\n",
|
|
" R0 == popd [false 1] dip uncons [add-with-carry] dip\n",
|
|
" R1 == i cons\n",
|
|
"\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "2a37982c",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "0c1ad90d",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "a184d47c",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "0343594a",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "e13c8b2e",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "e921d72a",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "2727bab9",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "3373be97",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "342e9982",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "7f655e89",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "611f40ff",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "bada9caa",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "fb66962d",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "6764903e",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "b4b10bfe",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"[base 2147483648] inscribe\n",
|
|
"[valid_digit [0 >] [base <] &&] inscribe\n",
|
|
"[_add_p [bool not] ii &] inscribe\n",
|
|
"[_add_then pop swap [] [1 swons] branch] inscribe\n",
|
|
"[_add_rec_pred [bool] ii &] inscribe\n",
|
|
"[bool_to_int [0] [1] branch] inscribe\n",
|
|
"[_add-with-carry0 [bool_to_int] dipd + +] inscribe\n",
|
|
"[_add-with-carry1 base [mod] [>=] clop] inscribe\n",
|
|
"[add-with-carry _add-with-carry0 _add-with-carry1] inscribe\n",
|
|
"[uncons-two [uncons] ii swapd] inscribe\n",
|
|
"[ditch-empty-list [bool] [popd] [pop] ifte] inscribe\n",
|
|
"[add-carry-to-digits [pop not] [popd] [popd [false 1] dip uncons [add-with-carry] dip] [i cons] genrec] inscribe\n",
|
|
"[THEN0 uncons-two [add-with-carry] dipd] inscribe\n",
|
|
"[THEN1 i cons] inscribe\n",
|
|
"[ELSE ditch-empty-list add-carry-to-digits] inscribe\n",
|
|
"[_add_R0 [_add_rec_pred] [THEN0]] inscribe\n",
|
|
"[_add_R1 [THEN1] cons concat [ELSE] ifte] inscribe\n",
|
|
"[add_digits [_add_p] [_add_then] [_add_R0] [_add_R1] genrec] inscribe\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "11c66f4e",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "60cda31e",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "0852a374",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "c2c3f8f5",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "eb4d2dac",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "6c7f705e",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "8e69a883",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "551b52de",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 55,
|
|
"id": "3fb6905c",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[1] 2 false [2 3]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"[isnt_bigint\n",
|
|
"[first isnt_bool]\n",
|
|
"[rest [isnt_int] map]\n",
|
|
"cleave cons\n",
|
|
"] inscribe"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 56,
|
|
"id": "39b3d4bc",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"[1] 2 false [2 3] [[!] [!-] [!=] [%] [&] [&&] [*] [+] [++] [-] [--] [/] [<] [<<] [<<{}] [<=] [<>] [<{}] [=] [>] [>=] [>>] [?] [abs] [add] [add-with-carry] [all] [anamorphism] [and] [any] [app1] [app2] [app3] [appN] [at] [b] [base] [binary] [bool] [bool_to_int] [branch] [ccccons] [ccons] [choice] [clear] [cleave] [clop] [cmp] [codi] [codireco] [concat] [cond] [cons] [digitalize] [dinfrirst] [dip] [dipd] [dipdd] [disenstacken] [ditch-empty-list] [div] [divmod] [down_to_zero] [drop] [dup] [dupd] [dupdd] [dupdip] [dupdipd] [enstacken] [eq] [first] [first_two] [flatten] [floordiv] [fork] [fourth] [gcd] [gcd2] [ge] [genrec] [getitem] [grabN] [grba] [gt] [help] [i] [ifte] [ii] [infra] [infrst] [inscribe] [isnt_bigint] [isnt_bool] [isnt_int] [isnt_stack] [le] [loop] [lshift] [lt] [make_generator] [manual] [map] [max] [min] [mod] [mul] [ne] [neg] [not] [nulco] [nullary] [of] [or] [over] [pam] [pm] [pop] [popd] [popdd] [popop] [popopd] [popopdd] [popopop] [pow] [pred] [primrec] [product] [quit] [quoted] [range] [range_to_zero] [reco] [remove] [rest] [reverse] [roll<] [roll>] [rolldown] [rollup] [rrest] [rshift] [run] [second] [select] [sharing] [shift] [shunt] [size] [sort] [spiral_next] [split_at] [split_list] [sqr] [stack] [stackd] [step] [step_zero] [stuncons] [stununcons] [sub] [succ] [sum] [swaack] [swap] [swapd] [swoncat] [swons] [tailrec] [take] [ternary] [third] [times] [to_bigint] [trace] [tuck] [unary] [uncons] [unique] [unit] [unquoted] [unswons] [valid_digit] [warranty] [while] [words] [x] [xor] [zip] [|] [||] [•]]"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"words"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 57,
|
|
"id": "4c5edbfa",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": []
|
|
}
|
|
],
|
|
"source": [
|
|
"clear"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 58,
|
|
"id": "1e201000",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"2147483648"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"1 31 <<"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "b310e739",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 59,
|
|
"id": "fc53f72d",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"12 3"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"clear\n",
|
|
"\n",
|
|
"123 10 divmod"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 60,
|
|
"id": "2cb7c88f",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"12 0 3"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"base divmod"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "e7c36361",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": []
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 61,
|
|
"id": "005ac08e",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"\n",
|
|
"==== Help on divmod ====\n",
|
|
"\n",
|
|
"Similarly to pm (\"Plus or minus\") this function computes\n",
|
|
"both the\n",
|
|
"::\n",
|
|
"\n",
|
|
" a b divmod\n",
|
|
" ---------------------\n",
|
|
" a b div a b mod\n",
|
|
" ---------------------\n",
|
|
" q r\n",
|
|
"\n",
|
|
"Where: q * b + r == a\n",
|
|
"\n",
|
|
"---- end ( divmod )\n",
|
|
"\n",
|
|
"\n",
|
|
"12 0 3"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"[divmod] help"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"id": "6ebcf6d8",
|
|
"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
|
|
}
|