{
 "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": "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": "227271a9",
   "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": "code",
   "execution_count": 21,
   "id": "998512c6",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": []
    }
   ],
   "source": [
    "clear"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0a592c8e",
   "metadata": {},
   "source": [
    "## Addition of Like Signs `add-digits`\n",
    "\n",
    "Let's figure out how to add two lists of digits (we will assume that the signs are the same.)  We need to put an inital `false` value for a carry flag, and then there's a `genrec`.\n",
    "\n",
    "    initial-carry ≡ false rollup\n",
    "      add-digits' ≡ [P] [THEN] [R0] [R1] genrec\n",
    "      \n",
    "       add-digits ≡ initial-carry add-digits'"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7b0df08e",
   "metadata": {},
   "source": [
    "### The predicate\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",
    "There are two base cases: two empty lists or one empty list, the recursive branch is taken only if both lists are non-empty.\n",
    "\n",
    "    bool [a ...] [b ...] P\n",
    "\n",
    "The first thing to do is convert them to Booleans:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "id": "b2d4f3b2",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[[true true] [true false] [false true] [false false]]"
     ]
    }
   ],
   "source": [
    "clear\n",
    "[\n",
    "[[a] [b]]\n",
    "[[a] []]\n",
    "[[] [b]]\n",
    "[[] []]\n",
    "]\n",
    "[[[bool] ii] infra] \n",
    "map"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "id": "d87fa971",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[[false] [true] [true] [true]]"
     ]
    }
   ],
   "source": [
    "clear\n",
    "[\n",
    "[[a] [b]]\n",
    "[[a] []]\n",
    "[[] [b]]\n",
    "[[] []]\n",
    "]\n",
    "[[[bool] ii & not] infra] \n",
    "map"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6ce10b89",
   "metadata": {},
   "source": [
    "    P == [bool] ii & not"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3fc5095b",
   "metadata": {},
   "source": [
    "### The base cases\n",
    "We have to decide between three cases, but because addition we can lump together the first two cases:\n",
    "\n",
    "    bool [] [b ...] THEN\n",
    "    bool [a ...] [] THEN\n",
    "    bool [] [] THEN\n",
    "\n",
    "    THEN ≡ [P'] [THEN'] [ELSE] ifte"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "id": "491c0846",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[[true] [true] [false]]"
     ]
    }
   ],
   "source": [
    "clear\n",
    "[\n",
    "[[a] []]\n",
    "[[] [b]]\n",
    "[[] []]\n",
    "]\n",
    "[[[bool] ii |] infra] \n",
    "map"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9f2bdc8d",
   "metadata": {},
   "source": [
    "    P' ≡ [bool] ii |\n",
    "\n",
    "So `THEN'` deals with one number (list of digits) being longer than the other, while the `ELSE` branch deals with the case of both lists being empty."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fa51fd49",
   "metadata": {},
   "source": [
    "#### One list empty\n",
    "In the cases where one of the two lists (but not both) is empty:\n",
    "\n",
    "    carry [a ...] [] THEN'\n",
    "    carry [] [b ...] THEN'\n",
    "\n",
    "We first get rid of the empty list:\n",
    "\n",
    "    ditch-empty-list ≡ [bool] [popd] [pop] ifte"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "id": "bd51792f",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": []
    }
   ],
   "source": [
    "clear\n",
    "[ditch-empty-list [bool] [popd] [pop] ifte] inscribe"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "id": "fbf134e2",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[1]"
     ]
    }
   ],
   "source": [
    "[1][] ditch-empty-list"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "id": "90db3359",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[1]"
     ]
    }
   ],
   "source": [
    "clear\n",
    "[][1] ditch-empty-list"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3b624991",
   "metadata": {},
   "source": [
    "    THEN' ≡ ditch-empty-list THEN''\n",
    "\n",
    "Now we have:\n",
    "\n",
    "    carry [n ...] THEN''\n",
    "\n",
    "This is `add-carry-to-digits` that kicked my ass earlier today.  Like I mentioned above, I think it was because I put it in the recursive branch!  D'oh!"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c4d9e00f",
   "metadata": {},
   "source": [
    "#### But first  `add-with-carry`\n",
    "We will want some function `F` 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": 28,
   "id": "e86b7b90",
   "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": 29,
   "id": "cd70e18e",
   "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": 30,
   "id": "a27ff9f0",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "4"
     ]
    }
   ],
   "source": [
    "clear\n",
    "\n",
    "true 1 2 [bool_to_int] dipd + +"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "89b971c9",
   "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": 31,
   "id": "74a59ab5",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "4 false"
     ]
    }
   ],
   "source": [
    "clear\n",
    "\n",
    "4 base [mod] [>=] clop"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "id": "3a8f5078",
   "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": "2b7eb5d7",
   "metadata": {},
   "source": [
    "Put it all together and we have:\n",
    "\n",
    "    _add-with-carry0 ≡ [bool_to_int] dipd + +\n",
    "    _add-with-carry1 ≡ base [mod] [>=] clop\n",
    "\n",
    "    add-with-carry ≡ _add-with-carry0 _add-with-carry1\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "id": "c05bcd8e",
   "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": 34,
   "id": "03649114",
   "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": 35,
   "id": "9dca0fbc",
   "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": 36,
   "id": "c8f01d7d",
   "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": 37,
   "id": "a1e77990",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "103 false"
     ]
    }
   ],
   "source": [
    "clear\n",
    "\n",
    "true 2 100 add-with-carry"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "id": "b46a62ba",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": []
    }
   ],
   "source": [
    "clear"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "44429ac5",
   "metadata": {},
   "source": [
    "### Now back to `add-carry-to-digits`\n",
    "\n",
    "This should be a very simple recursive function.\n",
    "\n",
    "    add-carry-to-digits ≡ [_actd_P] [_actd_THEN] [_actd_R0] [_actd_R1] genrec\n",
    "\n",
    "    carry [n ...] add-carry-to-digits\n",
    "    carry [n ...] [_actd_P] [_actd_THEN] [_actd_R0] [_actd_R1] genrec\n",
    "\n",
    "The predicate is the carry flag itself inverted (but when we recur we will need to check if the list is non-empty because it may eventually be empty):\n",
    "\n",
    "    _actd_P ≡ pop not\n",
    "\n",
    "The base case simply discards the carry flag:\n",
    "\n",
    "    _actd_THEN ≡ popd"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6895e78b",
   "metadata": {},
   "source": [
    "That leaves the recursive branch:\n",
    "\n",
    "    true [n ...] R0 [add-carry-to-digits] R1\n",
    "\n",
    "-or-\n",
    "\n",
    "    true [] R0 [add-carry-to-digits] R1"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b2279fc8",
   "metadata": {},
   "source": [
    "We know that the Boolean value is `true`.  We also know that the list will be non-empty, but only on the first iteration of the `genrec`.  It may be that the list is empty on a later iteration.\n",
    "\n",
    "The `R0` function should check the list.\n",
    "\n",
    "    _actd_R0 ≡ [bool] [_actd_R0.then] [_actd_R0.else] ifte"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "d5898c6a",
   "metadata": {},
   "source": [
    "If it's empty...\n",
    "\n",
    "       true [] R0.else [add-carry-to-digits] R1\n",
    "    ----------------------------------------------\n",
    "        1 false [] [add-carry-to-digits] i cons\n",
    "\n",
    "and\n",
    "\n",
    "                true [a ...] R0.then [add-carry-to-digits] i cons\n",
    "    ----------------------------------------------------------------\n",
    "       true 0 a add-with-carry [...] [add-carry-to-digits] i cons\n",
    "    ----------------------------------------------------------------\n",
    "                   (a+1) carry [...] [add-carry-to-digits] i cons"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "13513fab",
   "metadata": {},
   "source": [
    "There we go.\n",
    "\n",
    "    _actd_R0.else ≡ popd 1 false rolldown\n",
    "\n",
    "    _actd_R0.then ≡ 0 swap uncons [add-with-carry] dip\n",
    "\n",
    "    _actd_R1 ≡ i cons"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "id": "c8f1aa44",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": []
    }
   ],
   "source": [
    "[add-carry-to-digits [_actd_P] [_actd_THEN] [_actd_R0] [_actd_R1] genrec] inscribe\n",
    "[_actd_P pop not] inscribe\n",
    "[_actd_THEN popd] inscribe\n",
    "[_actd_R0 [bool] [_actd_R0.then] [_actd_R0.else] ifte] inscribe\n",
    "[_actd_R0.else popd 1 false rolldown] inscribe\n",
    "[_actd_R0.then 0 swap uncons [add-with-carry] dip] inscribe\n",
    "[_actd_R1 i cons] inscribe"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "id": "1fa115d9",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[3 2 1]"
     ]
    }
   ],
   "source": [
    "clear\n",
    "\n",
    "false [3 2 1] add-carry-to-digits"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "id": "79d9c526",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[1]"
     ]
    }
   ],
   "source": [
    "clear\n",
    "\n",
    "true [] add-carry-to-digits"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "id": "bb030214",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[4 2 1]"
     ]
    }
   ],
   "source": [
    "clear\n",
    "\n",
    "true [3 2 1] add-carry-to-digits"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 43,
   "id": "5e0a05af",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "true [2147483647 2 1]"
     ]
    }
   ],
   "source": [
    "clear\n",
    "\n",
    "true base -- [2 1] cons "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 44,
   "id": "7c730d6d",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[0 3 1]"
     ]
    }
   ],
   "source": [
    "add-carry-to-digits"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cf558731",
   "metadata": {},
   "source": [
    "So that handles the cases where one of the two lists (but not both) is empty.\n",
    "\n",
    "#### Both lists empty\n",
    "If both lists are empty we discard one list and check the carry to determine our result as decribed above:\n",
    "\n",
    "    ELSE ≡ pop swap [] [1 swons] branch"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 45,
   "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": 46,
   "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": 47,
   "id": "59b1338c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": []
    }
   ],
   "source": [
    "clear"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "7687e503",
   "metadata": {},
   "source": [
    "The story so far...\n",
    "\n",
    "    add-digits ≡ initial-carry add-digits'\n",
    "    \n",
    "    add-digits' ≡ [P] [THEN] [R0] [R1] genrec\n",
    "\n",
    "    initial-carry ≡ false rollup\n",
    "\n",
    "    P ≡ [bool] ii & not\n",
    "\n",
    "    THEN ≡ [P'] [THEN'] [ELSE] ifte\n",
    "\n",
    "    P' ≡ [bool] ii |\n",
    "\n",
    "    THEN' ≡ ditch-empty-list add-carry-to-digits\n",
    "\n",
    "    ELSE ≡ pop swap [] [1 swons] branch\n",
    "\n",
    "We just need to knock out those recursive functions `R0` and `R1` and we're done."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "fa6dc5c6",
   "metadata": {},
   "source": [
    "### And recur...\n",
    "\n",
    "    bool [a ...] [b ...] R0 [add-digits'] R1"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "53b2a650",
   "metadata": {},
   "source": [
    "First we will want to `uncons` the digits"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 48,
   "id": "78dec757",
   "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": "435069f2",
   "metadata": {},
   "source": [
    "#### `uncons-two`\n",
    "We could call this `uncons-two`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 49,
   "id": "5b4bd2fe",
   "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": 50,
   "id": "f284ea19",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": []
    }
   ],
   "source": [
    "clear"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "2b49246f",
   "metadata": {},
   "source": [
    "    bool a b [...] [...] R0' [add-digits'] R1\n",
    "\n",
    "It's at this point that we'll want to employ the `add-with-carry` function:\n",
    "\n",
    "    bool a b [...] [...] [add-with-carry] dipd R0'' [add-digits'] R1\n",
    "\n",
    "    bool a b add-with-carry [...] [...] R0'' [add-digits'] R1\n",
    "\n",
    "    (a+b) bool [...] [...] R0'' [add-digits'] R1\n",
    "\n",
    "If we postulate a `cons` in our `R1` function...\n",
    "\n",
    "    (a+b) bool [...] [...] R0'' [add-digits'] i cons\n",
    "\n",
    "Then it seems like we're done?  `R0''` is nothing?\n",
    "\n",
    "    R0 ≡ uncons-two [add-with-carry] dipd\n",
    "    \n",
    "    R1 ≡ i cons\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 51,
   "id": "8adffacb",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": []
    }
   ],
   "source": [
    "[add-digits initial-carry add-digits'] inscribe\n",
    "[add-digits' [P] [THEN] [R0] [R1] genrec] inscribe\n",
    "[initial-carry false rollup] inscribe\n",
    "[P [bool] ii & not] inscribe\n",
    "[THEN [P'] [THEN'] [ELSE] ifte] inscribe\n",
    "[P' [bool] ii |] inscribe\n",
    "[THEN' ditch-empty-list add-carry-to-digits] inscribe\n",
    "[ELSE pop swap [] [1 swons] branch] inscribe\n",
    "[R0 uncons-two [add-with-carry] dipd] inscribe\n",
    "[R1 i cons] inscribe"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 52,
   "id": "5b2e5738",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[3 2 1] [1 1 1]"
     ]
    }
   ],
   "source": [
    "[3 2 1] [1 1 1]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 53,
   "id": "cd7ac0b9",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[4 3 2]"
     ]
    }
   ],
   "source": [
    "add-digits"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 54,
   "id": "50f2e62c",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[4 3 2] [2147483647]"
     ]
    }
   ],
   "source": [
    "base -- unit"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 55,
   "id": "54ca630f",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[3 4 2]"
     ]
    }
   ],
   "source": [
    "add-digits"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 56,
   "id": "27bb4638",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[3 4 2] [2147483647 2147483647 2147483647]"
     ]
    }
   ],
   "source": [
    "base -- dup dup unit ccons"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 57,
   "id": "4d2d446a",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[2 4 2 1]"
     ]
    }
   ],
   "source": [
    "add-digits"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0159b2e3",
   "metadata": {},
   "source": [
    "243 + 999 = "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 58,
   "id": "c187ffff",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "1242"
     ]
    }
   ],
   "source": [
    "clear 243 999 +"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c142268c",
   "metadata": {},
   "source": [
    "Bitchin'"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f2b707c1",
   "metadata": {},
   "source": [
    "## Appendix: Source Code\n",
    "\n",
    "    base 2147483648\n",
    "    ditch-empty-list [bool] [popd] [pop] ifte\n",
    "    bool_to_int [0] [1] branch\n",
    "    uncons-two [uncons] ii swapd\n",
    "\n",
    "    add-with-carry _a0 _a1\n",
    "    _a0 [bool_to_int] dipd + +\n",
    "    _a1 base [mod] [>=] clop\n",
    "\n",
    "    add-carry-to-digits [pop not] [popd] [_actd_R0] [i cons] genrec\n",
    "    _actd_R0 [bool] [_actd_R0.then] [_actd_R0.else] ifte\n",
    "    _actd_R0.else popd 1 false rolldown\n",
    "    _actd_R0.then 0 swap uncons [add-with-carry] dip\n",
    "\n",
    "    add-digits initial-carry add-digits'\n",
    "    initial-carry false rollup\n",
    "    add-digits' [P] [THEN] [R0] [i cons] genrec\n",
    "    P [bool] ii & not\n",
    "    THEN [P'] [THEN'] [ELSE] ifte\n",
    "    R0 uncons-two [add-with-carry] dipd\n",
    "    P' [bool] ii |\n",
    "    THEN' ditch-empty-list add-carry-to-digits\n",
    "    ELSE pop swap [] [1 swons] branch\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "84affe68",
   "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
}