{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Type Checking"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "import logging, sys\n",
    "\n",
    "logging.basicConfig(\n",
    "  format='%(message)s',\n",
    "  stream=sys.stdout,\n",
    "  level=logging.INFO,\n",
    "  )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "from joy.utils.types import (\n",
    "    doc_from_stack_effect, \n",
    "    infer,\n",
    "    reify,\n",
    "    unify,\n",
    "    FUNCTIONS,\n",
    "    JoyTypeError,\n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "D = FUNCTIONS.copy()\n",
    "del D['product']\n",
    "globals().update(D)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## An Example"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      " 25 (--) ∘ pop swap rolldown rrest ccons\n",
      " 28 (a1 --) ∘ swap rolldown rrest ccons\n",
      " 31 (a3 a2 a1 -- a2 a3) ∘ rolldown rrest ccons\n",
      " 34 (a4 a3 a2 a1 -- a2 a3 a4) ∘ rrest ccons\n",
      " 37 ([a4 a5 ...1] a3 a2 a1 -- a2 a3 [...1]) ∘ ccons\n",
      " 40 ([a4 a5 ...1] a3 a2 a1 -- [a2 a3 ...1]) ∘ \n"
     ]
    }
   ],
   "source": [
    "fi, fo = infer(pop, swap, rolldown, rrest, ccons)[0]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "([a4 a5 ...1] a3 a2 a1 -- [a2 a3 ...1])\n"
     ]
    }
   ],
   "source": [
    "print doc_from_stack_effect(fi, fo)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [],
   "source": [
    "from joy.parser import text_to_expression\n",
    "from joy.utils.stack import stack_to_string\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[3 4] 2 1 0\n"
     ]
    }
   ],
   "source": [
    "e = text_to_expression('0 1 2 [3 4]')  # reverse order\n",
    "print stack_to_string(e)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{a1: 0, a2: 1, a3: 2, a4: 3, a5: 4, s2: (), s1: ()}"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "u = unify(e, fi)[0]\n",
    "u"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(... [3 4 ] 2 1 0 -- ... [1 2 ])\n"
     ]
    }
   ],
   "source": [
    "g = reify(u, (fi, fo))\n",
    "print doc_from_stack_effect(*g)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "##  Unification Works \"in Reverse\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [],
   "source": [
    "e = text_to_expression('[2 3]')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{a2: 2, a3: 3, s2: (), s1: ()}"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "u = unify(e, fo)[0]  # output side, not input side\n",
    "u"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "(... [a4 a5 ] 3 2 a1 -- ... [2 3 ])\n"
     ]
    }
   ],
   "source": [
    "g = reify(u, (fi, fo))\n",
    "print doc_from_stack_effect(*g)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Failing a Check"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      " 25 (--) ∘ dup mul\n",
      " 28 (a1 -- a1 a1) ∘ mul\n",
      " 31 (f1 -- f2) ∘ \n",
      " 31 (i1 -- i2) ∘ \n"
     ]
    }
   ],
   "source": [
    "fi, fo = infer(dup, mul)[0]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "'two'\n"
     ]
    }
   ],
   "source": [
    "e = text_to_expression('\"two\"')\n",
    "print stack_to_string(e)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Cannot unify 'two' and f1.\n"
     ]
    }
   ],
   "source": [
    "try:\n",
    "    unify(e, fi)\n",
    "except JoyTypeError, err:\n",
    "    print err"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 2",
   "language": "python",
   "name": "python2"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 2
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython2",
   "version": "2.7.12"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}