types.ipynb

{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "from ttrtypes import Type, BType, PType, Pred, MeetType, JoinType, ListType, \\\n",
    "SingletonType, HypObj, LazyObj, FunType, RecType, Fun, Ty, Re, RecTy, Possibility, \\\n",
    "AbsPath, TTRString, TTRStringType, KPlusStringType\n",
    "from records import Rec\n",
    "from utils import show, example, ttrace, nottrace, ttracing, show_latex"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Basic Types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "True\n",
      "['j', 'k', 'l', 'm', 'n']\n"
     ]
    }
   ],
   "source": [
    "Ind = BType('Ind')\n",
    "\n",
    "Ind.judge('j')\n",
    "Ind.judge('k')\n",
    "Ind.judge('l')\n",
    "Ind.judge('m')\n",
    "\n",
    "print(Ind.judge('j'))\n",
    "print(Ind.judge('n'))\n",
    "print(Ind.witness_cache)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n"
     ]
    }
   ],
   "source": [
    "print(Ind.query('h'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "_a0\n"
     ]
    }
   ],
   "source": [
    "print(Ind.create())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# PTypes"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "run(j)\n",
      "True\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "\\begin{equation}\\text{run}(\\text{j})\\end{equation}"
      ],
      "text/plain": [
       "<IPython.core.display.Latex object>"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "run = Pred('run',[Ind])\n",
    "p = PType(run,['j'])\n",
    "\n",
    "print(show(p))\n",
    "print(p.validate())\n",
    "show_latex(p)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "['_e0']\n",
      "True\n",
      "True\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "p.create()\n",
    "\n",
    "print(p.witness_cache)\n",
    "print(Ind.judge_nonspec())\n",
    "print(p.query_nonspec())\n",
    "print(p.judge_nonspec())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "['_e1']\n"
     ]
    }
   ],
   "source": [
    "man = Pred('man',[Ind])\n",
    "manj = PType(man,['j'])\n",
    "manj.create()\n",
    "\n",
    "print(manj.witness_cache)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Meet types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "False\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "T1 = Type()\n",
    "T2 = Type()\n",
    "T1.judge('a')\n",
    "T2.judge('a')\n",
    "T1.judge('b')\n",
    "T = MeetType(T1,T2)\n",
    "\n",
    "print(T.query('a'))\n",
    "print(T.query('b'))\n",
    "print(T.judge_nonspec())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "[]\n",
      "['_a1']\n",
      "['_a1']\n",
      "_a2\n"
     ]
    }
   ],
   "source": [
    "T11 = Type()\n",
    "T21 = Type()\n",
    "T31 = MeetType(T11,T21)\n",
    "\n",
    "print(T31.judge_nonspec())\n",
    "print(T31.witness_cache)\n",
    "print(T11.witness_cache)\n",
    "print(T21.witness_cache)\n",
    "print(T31.create())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Join types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[]\n",
      "True\n",
      "True\n",
      "_a3\n",
      "['a', 'b', '_a3']\n",
      "['a', 'b']\n",
      "['a']\n"
     ]
    }
   ],
   "source": [
    "T3 = JoinType(T1,T2)\n",
    "\n",
    "print(T3.witness_cache)\n",
    "print(T3.query('a'))\n",
    "print(T3.query('b'))\n",
    "print(T3.create())\n",
    "print(T3.witness_cache)\n",
    "print(T1.witness_cache)\n",
    "print(T2.witness_cache)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# The subtype relation"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[Ind]\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "x = HypObj([Ind])\n",
    "\n",
    "print(show(x.types))\n",
    "print(x.validate())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[T4]\n"
     ]
    }
   ],
   "source": [
    "T4 = Type()\n",
    "x1 = T4.create_hypobj()\n",
    "\n",
    "print(show(x1.types))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[T0, T1, (T0&T1)]\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "x2 = T.create_hypobj()\n",
    "\n",
    "print(show(x2.types))\n",
    "print(T1.query(x2))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "True\n",
      "True\n",
      "True\n",
      "False\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "print(T1.subtype_of(T1))\n",
    "print(T.subtype_of(T1))\n",
    "print(T.subtype_of(T2))\n",
    "print(T1.subtype_of(T3))\n",
    "print(T3.subtype_of(T1))\n",
    "print(T.subtype_of(T3))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Learning witness conditions"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Meet types are logical and cannot learn new conditions\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "[]"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "ttrace()\n",
    "T.learn_witness_condition(lambda x: x)\n",
    "nottrace()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Functions and function types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "j\n"
     ]
    },
    {
     "data": {
      "text/latex": [
       "\\begin{equation}\\lambda x:\\textit{Ind}\\ .\\ x\\end{equation}"
      ],
      "text/plain": [
       "<IPython.core.display.Latex object>"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "f = Fun('x',Ind,'x')\n",
    "print(f.app('j'))\n",
    "show_latex(f)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "True\n"
     ]
    }
   ],
   "source": [
    "IndToInd = FunType(Ind,Ind)\n",
    "\n",
    "print(IndToInd.query(f))\n",
    "print(IndToInd.query_nonspec()) # Perhaps function types should be non-empty if their domain and range types are non-empty or if it's not the case that: the domain type is empty and the range type is non-empty (material conditional)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "h17\n"
     ]
    }
   ],
   "source": [
    "a = IndToInd.create_hypobj()\n",
    "print(show(a))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "print(f.validate_arg('j'))\n",
    "print(f.validate_arg('x'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "lambda x:Ind . run(x)\n"
     ]
    }
   ],
   "source": [
    "f1 = Fun('x',Ind,PType(run,['x']))\n",
    "print(f1.show())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [
    {
     "ename": "AttributeError",
     "evalue": "'str' object has no attribute 'model'",
     "output_type": "error",
     "traceback": [
      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[0;31mAttributeError\u001b[0m                            Traceback (most recent call last)",
      "\u001b[0;32m<ipython-input-21-84727a6ed4ae>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mp1\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mf1\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mapp\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m'j'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m      2\u001b[0m \u001b[0mprint\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mshow\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mp1\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;32m~/python/pyttr/ttrtypes.py\u001b[0m in \u001b[0;36mapp\u001b[0;34m(self, arg)\u001b[0m\n\u001b[1;32m    988\u001b[0m             \u001b[0;32mreturn\u001b[0m \u001b[0marg\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    989\u001b[0m         \u001b[0;32melse\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 990\u001b[0;31m             \u001b[0mres\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0msubstitute\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mbody\u001b[0m\u001b[0;34m,\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mvar\u001b[0m\u001b[0;34m,\u001b[0m\u001b[0marg\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m    991\u001b[0m             \u001b[0;32mif\u001b[0m \u001b[0;34m'cache'\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mdir\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mres\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;32mand\u001b[0m \u001b[0;32mnot\u001b[0m \u001b[0misinstance\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0marg\u001b[0m\u001b[0;34m,\u001b[0m\u001b[0mHypObj\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    992\u001b[0m                 \u001b[0;32mreturn\u001b[0m \u001b[0mres\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mcache\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;31m#This conditional not used?\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;32m~/python/pyttr/utils.py\u001b[0m in \u001b[0;36msubstitute\u001b[0;34m(obj, v, a)\u001b[0m\n\u001b[1;32m    175\u001b[0m         \u001b[0mres\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mtuple\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0msubstitute\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mx\u001b[0m\u001b[0;34m,\u001b[0m\u001b[0mv\u001b[0m\u001b[0;34m,\u001b[0m\u001b[0ma\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;32mfor\u001b[0m \u001b[0mx\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mobj\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    176\u001b[0m     \u001b[0;32melif\u001b[0m \u001b[0;34m'subst'\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mdir\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mobj\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 177\u001b[0;31m         \u001b[0mres\u001b[0m \u001b[0;34m=\u001b[0m  \u001b[0mobj\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0msubst\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mv\u001b[0m\u001b[0;34m,\u001b[0m\u001b[0ma\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m    178\u001b[0m     \u001b[0;32melse\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    179\u001b[0m         \u001b[0mres\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mobj\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;32m~/python/pyttr/ttrtypes.py\u001b[0m in \u001b[0;36msubst\u001b[0;34m(self, v, a)\u001b[0m\n\u001b[1;32m    228\u001b[0m                 \u001b[0;32melif\u001b[0m \u001b[0misinstance\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0marg\u001b[0m\u001b[0;34m,\u001b[0m\u001b[0mstr\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m \u001b[0mnewargs\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mappend\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0marg\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    229\u001b[0m                 \u001b[0;32melse\u001b[0m\u001b[0;34m:\u001b[0m \u001b[0mnewargs\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mappend\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0msubstitute\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0marg\u001b[0m\u001b[0;34m,\u001b[0m\u001b[0mv\u001b[0m\u001b[0;34m,\u001b[0m\u001b[0ma\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m      \u001b[0;31m#arg.subst(v,a))\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 230\u001b[0;31m             \u001b[0;32mreturn\u001b[0m \u001b[0mPType\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mcomps\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mpred\u001b[0m\u001b[0;34m,\u001b[0m\u001b[0mnewargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0min_poss\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mposs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m    231\u001b[0m     \u001b[0;32mdef\u001b[0m \u001b[0meval\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    232\u001b[0m         \u001b[0mnewargs\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0;34m[\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;32m~/python/pyttr/ttrtypes.py\u001b[0m in \u001b[0;36min_poss\u001b[0;34m(self, poss)\u001b[0m\n\u001b[1;32m     66\u001b[0m         \u001b[0;32mif\u001b[0m \u001b[0mposs\u001b[0m \u001b[0;34m==\u001b[0m \u001b[0m_M\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m     67\u001b[0m             \u001b[0;32mreturn\u001b[0m \u001b[0mself\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m---> 68\u001b[0;31m         \u001b[0;32melif\u001b[0m \u001b[0mkey\u001b[0m \u001b[0;32mnot\u001b[0m \u001b[0;32min\u001b[0m \u001b[0mposs\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mmodel\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m     69\u001b[0m             \u001b[0mposs\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mmodel\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0mkey\u001b[0m\u001b[0;34m]\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mdeepcopy\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mself\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m     70\u001b[0m             \u001b[0mposs\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mmodel\u001b[0m\u001b[0;34m[\u001b[0m\u001b[0mkey\u001b[0m\u001b[0;34m]\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mposs\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mposs\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;31mAttributeError\u001b[0m: 'str' object has no attribute 'model'"
     ]
    }
   ],
   "source": [
    "p1 = f1.app('j')\n",
    "print(show(p1))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "p1c = f1.appc('j')\n",
    "print(show(p1c))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "ttrace()\n",
    "print(show(f1.appc('x')))\n",
    "nottrace()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# The type $\\textit{Type}$ (called `Ty` in `pyttr`)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(Ty.query(T))\n",
    "print(Ty.query(Ty))\n",
    "print(Ty.query(p1))\n",
    "print(Ty.query_nonspec()) # Presumably this should be True since at least Ty.query(Ty) returns True"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "ttrace()\n",
    "Ty.learn_witness_condition(lambda x: x)\n",
    "nottrace()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "IndToTy = FunType(Ind,Ty)\n",
    "\n",
    "print(IndToTy.query(f1))\n",
    "print(IndToTy.query(f))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Dependent types -- functions which return types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "f2 = Fun('x',Ind,PType(man,['x']))\n",
    "print(show(f2))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "love = Pred('love',[Ind,Ind])\n",
    "f3 = Fun('x',Ind,Fun('y',Ind,PType(love,['x','y'])))\n",
    "p2 = f3.app('j').app('m')\n",
    "print(show(p2))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "p3 = Fun('x',Ind,Fun('y',Ind,PType(love,['x','y'])).app('j')).app('m')\n",
    "print(show(p3))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# List types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "ListInd = ListType(Ind)\n",
    "\n",
    "print(ListInd.query(['j','k']))\n",
    "print(show(ListInd))\n",
    "print(ListInd.query([]))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Singleton types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Ind_j = SingletonType(Ind,'j')\n",
    "\n",
    "print(Ind_j.query('j'))\n",
    "print(Ind_j.query('k'))\n",
    "print(Ind_j.query('x'))\n",
    "print(show(Ind_j))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Ind_jk = SingletonType(ListType(Ind),['j']+['k'])\n",
    "\n",
    "print(show(Ind_jk))\n",
    "print(Ind_jk.query(['j','k']))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Ind_appk = SingletonType(Ind,Fun('x',Ind,'j').app('k'))\n",
    "\n",
    "print(show(Ind_appk))\n",
    "print(Ind_appk.query('j'))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Possibilities"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(Fun('x',Ind,Ind).app('j').query('k'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(Fun('x',Ind,PType(man,['x'])).app('j').query_nonspec())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(show(Fun('x',Ind,PType(man,['x'])).app('j')))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(show(manj))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(manj.query_nonspec())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "M = Possibility('M')\n",
    "manj.in_poss(M)\n",
    "\n",
    "print(Fun('x',Ind,PType(man,['x'])).app('j').in_poss(M).query_nonspec())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(show(M))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Record types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(Ty.query(RecType({'x':Ind})))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(RecType({'x':Ind}).query(Rec({'x':'j'})))\n",
    "print(RecType({'x':Ind}).query(Rec({'x':'j', 'y':'k','z':'e1'})))\n",
    "print(RecType({'x':Ind, 'y':Ind}).query(Rec({'x':'j'}))) #False"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(RecTy.query(RecType({'x':Ind,\n",
    "                           'c':(Fun('v',Ind,PType(man,['v'])), ['x'])})))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T_man = RecType({'x':Ind, 'c':(Fun('v',Ind,PType(man,['v'])), ['x'])})\n",
    "\n",
    "print(T_man.query(Rec({'x':'j', 'c':'_e1'})))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "Ind.in_poss(M)\n",
    "T_man.in_poss(M)\n",
    "\n",
    "print(show(M))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(T_man.in_poss(M).query(Rec({'x':'j', 'c':'_e1'})))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "##### Using singleton types in manifest fields to ensure identity"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(RecType({'x':Ind, \\\n",
    "               'y':(Fun('v',Ind,SingletonType(Ind,'v')),['x'])})\n",
    "      .in_poss(M)\n",
    "      .query(Rec({'x':'j',\n",
    "                  'y':'j',\n",
    "                  'c':'e1'})))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(show(T_man))\n",
    "print(show(T_man.create())) \n",
    "print(show(M))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(T_man.query(T_man.create()))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(RecTy.query(RecType({'x':Ind,\n",
    "                           'c': RecType({'c': (Fun('v',Ind,PType(man,['v'])), ['x'])})}))) "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "True, even though the path in the dependent field is not defined (too deeply embedded)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Subtyping for record types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(T_man.subtype_of(T_man))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(RecType({'x':Ind,\n",
    "               'c': (Fun('v',Ind,PType(man,['v'])), ['x'])}).subtype_of(Re))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(RecType({'x':Ind,\n",
    "               'c': RecType({'c': (Fun('v',Ind,PType(man,['v'])), ['x'])})})\n",
    "      .subtype_of(Re))  "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Paths in dependent fields"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(show(RecType({'x':Ind,\n",
    "                    'c': RecType({'c': (Fun('v',Ind,PType(man,['v'])), ['x'])})})))\n",
    "\n",
    "print(RecType({'x':Ind,\n",
    "               'c': RecType({'c': (Fun('v',Ind,PType(man,['v'])), ['x'])})})\n",
    "      .validate()) \n",
    " "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "False.  This would have been True in the Oz implementation since\n",
    " paths always started from the top of the record type.  Now paths\n",
    " start in the record type in which they occur."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(T_man.validate())\n",
    "\n",
    "print(RecType({'x':Ind,\n",
    "               'e':(Fun('v',Ind,RecType({'e':PType(man,['v'])})), ['x'])})\n",
    "      .validate())\n",
    "# True. Here the function is at the right level. \n",
    "\n",
    "print(RecType({'x':Ind,\n",
    "               'e':(Fun('v',Ind,RecType({'e':PType(man,['v'])})), ['x'])})\n",
    "      .in_poss(M)\n",
    "      .query(Rec({'x':'j',\n",
    "                  'y':'j',\n",
    "                  'e':Rec({'e':'_e1'})}))) \n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(RecType({'x':Ind,\n",
    "               'y':(Fun('v',Ind,SingletonType(Ind,'v')),['x'])})\n",
    "      .in_poss(M)\n",
    "      .query(Rec({'x':'j',\n",
    "                  'y':'j',\n",
    "                  'e':Rec({'e':'_e1'})})))\n",
    "\n",
    "print(RecType({'x':Ind,\n",
    "               'y':(Fun('v',Ind,SingletonType(Ind,'v')),['x']),\n",
    "               'e':(Fun('v',Ind,RecType({'e':PType(man,['v'])})), ['y'])})\n",
    "      .in_poss(M).query(Rec({'x':'j',\n",
    "                             'y':'j',\n",
    "                             'e':Rec({'e':'_e1'})})))\n",
    "\n",
    "print(show(RecType({'x':Ind,\n",
    "                    'y':(Fun('v',Ind,SingletonType(Ind,'v')),['x']),\n",
    "                    'e':(Fun('v',Ind,RecType({'e':PType(man,['v'])})), ['y'])})\n",
    "           .in_poss(M)\n",
    "           .create()))\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(RecType({'x':Ind,\n",
    "               'y':(Fun('v',Ind,SingletonType(Ind,'v')),['x']),\n",
    "               'e':(Fun('v',Ind,RecType({'e':PType(man,['v'])})), ['y'])})\n",
    "      .in_poss(M)\n",
    "      .judge(Rec({'x':'j',\n",
    "                  'y':'j',\n",
    "                  'e':Rec({'e':'_e1'})})))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T_a_man =  RecType({'x':Ind,\n",
    "                    'y':(Fun('v',Ind,SingletonType(Ind,'v')),['x']),\n",
    "                    'e':(Fun('v',Ind,RecType({'e':PType(man,['v'])})), ['y'])})\n",
    "\n",
    "T_a_man.in_poss(M).judge(Rec({'x':'j',\n",
    "                              'y':'j',\n",
    "                              'e':Rec({'e':'_e1'})}))\n",
    "\n",
    "print(show(T_a_man.witness_cache))\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Tricky cases of subtyping"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "print(RecType({'x':Ind,\n",
    "               'y':Ind})\n",
    "      .subtype_of(RecType({'x':Ind})))\n",
    "\n",
    "print(RecType({'x':Ind,\n",
    "               'y':Ind,\n",
    "               'e': (Fun('v',Ind,PType(man,['v'])),['y'])})\n",
    "      .subtype_of(RecType({'x':Ind,\n",
    "                           'y':(Fun('v',Ind,SingletonType(Ind,'v')),['x']),\n",
    "                           'e': (Fun('v',Ind,PType(man,['v'])),['y'])}))) #False\n",
    "\n",
    "print(RecType({'x':Ind,\n",
    "               'y':(Fun('v',Ind,SingletonType(Ind,'v')),['x']),\n",
    "               'e': (Fun('v',Ind,PType(man,['v'])),['y'])})\n",
    "      .subtype_of(RecType({'x':Ind,\n",
    "                           'y':Ind,\n",
    "                           'e': (Fun('v',Ind,PType(man,['v'])),['y'])})))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "R1 = RecType({'x':Ind,\n",
    "              'y':(Fun('v',Ind,SingletonType(Ind,'v')),['x']),\n",
    "              'e': (Fun('v',Ind,PType(man,['v'])),['y'])})\n",
    "\n",
    "R2 = RecType({'x':Ind,\n",
    "              'y':Ind,\n",
    "              'e': (Fun('v',Ind,PType(man,['v'])),['y'])})\n",
    "\n",
    "print(R1.subtype_of(R2))\n",
    "\n",
    "print(RecType({'x' : R1})\n",
    "      .subtype_of(RecType({'x' : R2})))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Validation of record types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "print(RecTy.query(RecType({'x' : Ind,\n",
    "                           'e' : (Fun('v',Ind,PType(man,['v'])),['x'])})))\n",
    "\n",
    "print(RecType({'x' : Ind,\n",
    "               'e' : (Fun('v',Ind,PType(man,['v'])),['x'])}).validate())\n",
    "\n",
    "print(RecTy.query(RecType({'x' : Ty,\n",
    "                           'e' : (Fun('v',Ind,PType(man,['v'])),['x'])})))\n",
    "#In the earlier implementation this was false.  If we want to replicate this we can first validate as below.\n",
    "\n",
    "print(RecType({'x' : Ty,\n",
    "               'e' : (Fun('v',Ind,PType(man,['v'])),['x'])}).validate())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "ttrace()\n",
    "h1 = RecType({'x' : Ty,\n",
    "              'e' : (Fun('v',Ind,PType(man,['v'])),['x'])}).create_hypobj()\n",
    "print(show(h1))\n",
    "nottrace()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(RecType({'x' : RecType({'x' : Ind,\n",
    "                              'e' : (Fun('v',Ind,PType(man,['v'])),['x'])})}).\n",
    "            validate())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(RecType({'x' : (Fun('v',Ind,RecType({'x' : Ind,\n",
    "                                           'e' : PType(man,['v'])})),['x'])}).\n",
    "            validate())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(show(RecType({'x' : RecType({'x' : Ind,\n",
    "                                   'e' : (Fun('v',Ind,PType(man,['v'])),['x'])})})\n",
    "           .create()))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(show(RecTy.create()))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(RecType({'x' : RecType({'x' : Ind,\\\n",
    "                              'e' : (Fun('v',Ind,PType(man,['v'])),['y'])}),\n",
    "                'y' : Ind}).\n",
    "            validate()) #False"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(RecType({'x' : (Fun('v',Ind,RecType({'x' : Ind,\n",
    "                                           'e' : PType(man,['v'])})),['y']),\n",
    "               'y' : Ind}).\n",
    "            validate())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(show(RecType({'x' : (Fun('v',Ind,RecType({'x' : Ind,\n",
    "                                           'e' : PType(man,['v'])})),['y']),\n",
    "               'y' : Ind}).\n",
    "            create()))\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(show(RecType({'x' : (Fun('v',Ind,RecType({'x' : Ind,\n",
    "                                                'e' : PType(man,['v'])})),['y']),\n",
    "                    'y' : Ind}).\n",
    "            create_hypobj()))\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(RecType({'x' : RecType({'x' : Ind,\n",
    "                              'e' : (Fun('v',Ind,PType(man,['v'])),['x'])}),\n",
    "               'y' : (Fun('v',Ind,SingletonType(Ind,'v')),['x.x'])}).\n",
    "            validate()) "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(RecType({'x' : (Fun('v',Ind,RecType({'x' : Ind,\n",
    "                                           'e' : PType(man,['v'])})),['y']),\n",
    "               'y' : (Fun('v',Ind,SingletonType(Ind,'v')),['x.x'])}).\n",
    "            validate())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    " The corresponding type in the previous implementation would have\n",
    " been ok since it would have been written (mutatis mutandis)\n",
    " \n",
    " `RecType({'x' : RecType({'x' : Ind,\\\n",
    "                         'e' : (Fun('v',Ind, PType(man,['v'])),['y'])}),\\\n",
    "          'y' : (Fun('v',Ind,SingletonType(Ind,'v')),['x.x'])})`\n",
    " \n",
    " and path names in the dependent fields would always have been\n",
    " interpreted from the top of the record.  So this type from the old\n",
    " system is not expressible if path names are interpreted locally.\n",
    " However, there is a type very like it in the two following cells:\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(RecType({'x' : (Fun('v',Ind,RecType({'x' : SingletonType(Ind,'v'),\n",
    "                                           'e' : (Fun('v',Ind,PType(man,['v'])),['x'])})), ['y']),\n",
    "               'y' : Ind}).\n",
    "            validate())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(show(RecType({'x' : (Fun('v',Ind,RecType({'x' : SingletonType(Ind,'v'),\n",
    "                                                'e' : (Fun('v',Ind,PType(man,['v'])),['x'])})), ['y']),\n",
    "               'y' : Ind}).\n",
    "            create()))\n",
    "\n",
    "print(show(RecType({'x' : (Fun('v',Ind,RecType({'x' : SingletonType(Ind,'v'),\n",
    "                                                'e' : (Fun('v',Ind,PType(man,['v'])),['x'])})), ['y']),\n",
    "               'y' : Ind}).\n",
    "            create_hypobj()))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(RecType({'x' : (Fun('v',Ind,RecType({'x' : SingletonType(Ind,'v'),\\\n",
    "                                     'e' : (Fun('v',Ind,PType(man,['v'])),['x'])})), ['y']),\n",
    "               'y' : Ind}).subtype_of(\n",
    "RecType({'x' : RecType({'x' : Ind,\n",
    "                        'e' : (Fun('v',Ind,PType(man,['v'])),['x'])}),\n",
    "               'y' : Ind})\n",
    "))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The reverse of the above is false:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "RecType({'x' : RecType({'x' : Ind,\n",
    "                        'e' : (Fun('v',Ind,PType(man,['v'])),['x'])}),\n",
    "         'y' : Ind}).subtype_of(\n",
    "RecType({'x' : (Fun('v',Ind,RecType({'x' : SingletonType(Ind,'v'),\n",
    "                                     'e' : (Fun('v',Ind,PType(man,['v'])),['x'])})), ['y']),\n",
    "         'y' : Ind})\n",
    "))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "RecType({'x' : (Fun('v',Ind,SingletonType(Ind,'v')),['y']),\\\n",
    "         'y' : (Fun('v',Ind,SingletonType(Ind,'v')),['x'])}).\\\n",
    "validate()\n",
    ") #False"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "ttrace()\n",
    "print(\n",
    "RecType({'x' : (Fun('v',Ind,SingletonType(Ind,'v')),['y']),\n",
    "         'y' : (Fun('v',Ind,SingletonType(Ind,'v')),['x'])}).\n",
    "create()\n",
    ") #None\n",
    "nottrace()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "ttrace()\n",
    "print(\n",
    "RecType({'x' : (Fun('v',Ind,SingletonType(Ind,'v')),['y']),\n",
    "         'y' : (Fun('v',Ind,SingletonType(Ind,'v')),['x'])}).\n",
    "create_hypobj()\\\n",
    ") #None\n",
    "nottrace()\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\\\n",
    "RecType({'x' : (Fun('v',Ind,SingletonType(Ind,'v')),['y']),\n",
    "         'y' : (Fun('v',Ind,SingletonType(Ind,'v')),['x'])}).\n",
    "query(\\\n",
    "Rec({'x' : 'j',\\\n",
    "     'y' : 'j'})\\\n",
    ")\\\n",
    ") # True!"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\\\n",
    "RecType({'x' : (Fun('v',Ind,SingletonType(Ind,'v')),['y']),\n",
    "         'y' : (Fun('v',Ind,SingletonType(Ind,'v')),['x'])}).\n",
    "query(\n",
    "Rec({'x' : 'j',\n",
    "     'y' : 'k'})\n",
    ")\n",
    ") # False"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    " The five previous examples show that circularity in dependencies can be used\n",
    " in a limited fashion if desired.  Given a record that you are\n",
    " checking it is possible for the dependencies to be resolved using\n",
    " the record.  However, the type will not be validated and it is not\n",
    " possible to create objects of the type, which in turn means that it\n",
    " will not be possible to show that it is a subtype of another type."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Lazy objects in record types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "RecType({'x' : ListType(Ind),\n",
    "         'y' : ListType(Ind),\n",
    "         'z' : (Fun('v1',ListType(Ind),\n",
    "                Fun('v2',ListType(Ind),SingletonType(ListType(Ind),LazyObj(['v1','+','v2'])))),['x','y'])}).\n",
    "validate()\n",
    ") "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "RecType({'x' : Ind,\n",
    "         'y' : Ind,\n",
    "         'e' : (Fun('v1',Ind,\n",
    "                 Fun('v2',Ind,PType(love,['v1','v2']))), ['x','y'])}).\n",
    "validate()\n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "PType(love,['j','m']).in_poss(M).judge('e8')\n",
    "print(\n",
    "RecType({'x' : Ind,\n",
    "         'y' : Ind,\n",
    "         'e' : (Fun('v1',Ind,\n",
    "                 Fun('v2',Ind,PType(love,['v1','v2']))), ['x','y'])}).\n",
    "in_poss(M).\n",
    "query(Rec({'x' : 'j',\n",
    "       'y' : 'm',\n",
    "       'e' : 'e8'}))\n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "RecType({'x' : ListType(Ind),\n",
    "         'y' : ListType(Ind),\n",
    "         'z' : (Fun('v1',ListType(Ind),\n",
    "                Fun('v2',ListType(Ind),SingletonType(ListType(Ind),LazyObj(['v1','+','v2'])))),['x','y'])}).\n",
    "query(\n",
    "Rec({'x' : ['j'],\n",
    "     'y' : ['m'],\n",
    "     'z' : ['j', 'm']})\n",
    ")\n",
    ") "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "show(\n",
    "RecType({'x' : ListType(Ind),\n",
    "         'y' : ListType(Ind),\n",
    "         'z' : (Fun('v1',ListType(Ind),\n",
    "                Fun('v2',ListType(Ind),SingletonType(ListType(Ind),LazyObj(['v1','+','v2'])))),['x','y'])}).\n",
    "create_hypobj()\n",
    ")\n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "show(\n",
    "RecType({'x' : SingletonType(ListType(Ind),['j']),\n",
    "         'y' : ListType(Ind),\n",
    "         'z' : (Fun('v1',ListType(Ind),\n",
    "                Fun('v2',ListType(Ind),SingletonType(ListType(Ind),LazyObj(['v1','+','v2'])))),['x','y'])}).\n",
    "create_hypobj()\n",
    ")\n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "show(\n",
    "RecType({'x' : SingletonType(ListType(Ind),['j']),\n",
    "         'y' : SingletonType(ListType(Ind),['m']),\n",
    "         'z' : (Fun('v1',ListType(Ind),\n",
    "                Fun('v2',ListType(Ind),SingletonType(ListType(Ind),LazyObj(['v1','+','v2'])))),['x','y'])}).\n",
    "create_hypobj()\n",
    ")\n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "show(\n",
    "RecType({'x' : FunType(Ind,RecTy),\n",
    "         'y' : Ind,\n",
    "         'z' : (Fun('f',FunType(Ind,RecTy), Fun('v',Ind,SingletonType(RecTy,LazyObj(['f','@','v'])))),\n",
    "                 ['x','y'])}).\n",
    "query(\n",
    "Rec({'x' : Fun('v',Ind,RecType({'e' : PType(man, ['v'])})),\n",
    "     'y' : 'j',\n",
    "     'z' : RecType({'e' : PType(man, ['j'])})})\n",
    ")\n",
    ")\n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "show(\n",
    "RecType({'x' : FunType(Ind,RecTy),\n",
    "         'y' : Ind,\n",
    "         'w' : Ind,\n",
    "         'z' : (Fun('f',FunType(Ind,RecTy), Fun('v',Ind,SingletonType(RecTy,LazyObj(['f','@','v'])))),\n",
    "                 ['x','y'])}).\n",
    "subtype_of(\n",
    "RecType({'x' : FunType(Ind,RecTy),\n",
    "         'y' : Ind,\n",
    "         'w' : Ind,\n",
    "         'z' : (Fun('f',FunType(Ind,RecTy), Fun('v',Ind,SingletonType(RecTy,LazyObj(['f','@','v'])))),\n",
    "                 ['x','w'])})\n",
    ")\n",
    ")\n",
    ") # False"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "show(\n",
    "RecType({'x' : FunType(Ind,RecTy),\n",
    "         'y' : Ind,\n",
    "         'w' : Ind,\n",
    "         'z' : (Fun('f',FunType(Ind,RecTy), Fun('v',Ind,SingletonType(RecTy,LazyObj(['f','@','v'])))),\n",
    "                 ['x','y'])}).\n",
    "create_hypobj(\n",
    ")\n",
    ")\n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "show(\n",
    "RecType({'x' : FunType(Ind,RecTy),\n",
    "         'y' : Ind,\n",
    "         'w' : Ind,\n",
    "         'z' : (Fun('f',FunType(Ind,RecTy), Fun('v',Ind,SingletonType(RecTy,LazyObj(['f','@','v'])))),\n",
    "                 ['x','y'])\n",
    "         })\n",
    ")\n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "    show(\n",
    "RecType({'x' : FunType(Ind,RecTy),\n",
    "         'y' : Ind,\n",
    "         'w' : Ind,\n",
    "         'z' : (Fun('f',FunType(Ind,RecTy), Fun('v',Ind,SingletonType(RecTy,LazyObj(['f','@','v'])))),\n",
    "                 ['x','y'])\n",
    "         }).\n",
    "subtype_of(RecType({'z' : RecTy}))\n",
    ")\n",
    ")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "    show(\n",
    "RecType({'x' : FunType(Ind,RecTy),\n",
    "         'y' : Ind,\n",
    "         'w' : Ind,\n",
    "         'z' : (Fun('f',FunType(Ind,RecTy), Fun('v',Ind,SingletonType(RecTy,LazyObj(['f','@','v'])))),\n",
    "                 ['x','y'])\n",
    "         }).\n",
    "         create_hypobj()\n",
    "         )\n",
    "         )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "    show(\n",
    "        RecType({'x' : FunType(Ind,RecTy),\n",
    "         'y' : Ind,\n",
    "         'w' : Ind,\n",
    "         'z' : (Fun('f',FunType(Ind,RecTy), Fun('v',Ind,SingletonType(RecTy,LazyObj(['f','@','v'])))),\n",
    "                 ['x','y'])\n",
    "         }).\n",
    "         subtype_of(RecType({'z' : RecTy}))\n",
    "         )\n",
    "         )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "TT1 = FunType(Ind, RecTy)\n",
    "TT2 = FunType(Ind, Ty)\n",
    "TT3 = FunType(TT1, TT2)\n",
    "ff = Fun('f', TT1, Fun('x', Ind, LazyObj(['f','@','x'])))\n",
    "print(TT3.query(ff))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Absolute paths"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "Ty.query(RecType({'c' : (Fun('v', Ind, PType(man,['v'])),\n",
    "                       [AbsPath(Rec({'x' : 'j'}), 'x')])}))\n",
    "                       )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "TxInd = RecType({'x' : Ind})\n",
    "print(\n",
    "    FunType(TxInd, RecTy).\n",
    "    query(Fun('r', TxInd, RecType({'c' : (Fun('v', Ind, PType(man,['v'])),\n",
    "                        [AbsPath('r', 'x')])})))\n",
    "                       )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "    show(\n",
    "        Fun('r', TxInd, RecType({'c' : (Fun('v', Ind, PType(man,['v'])),\n",
    "                            [AbsPath('r', 'x')])})).app(Rec({'x' : 'j'}))\n",
    "                        ))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Merging record types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "    show(\n",
    "        RecType({'x' : Ind,\n",
    "                 'y' : Ind})\n",
    "        .merge(RecType({'x':Ind}))\n",
    "        )\n",
    "        )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "    show(\n",
    "     RecType({'x':Ind}).\n",
    "     merge(RecType({'x' : Ind,\n",
    "                    'y' : Ind}))\n",
    "                    )\n",
    "                    )\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "##### Merging not only for record types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "    show(\n",
    "        JoinType(Ind,Ty).merge(RecTy)))\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "    show(\n",
    "        JoinType(Ind,Ty).merge(Ind)\n",
    "    )\n",
    "    )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "    show(\n",
    "        JoinType(Ind,Ty).merge(JoinType(Ind,RecTy))\n",
    "        )\n",
    "        )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "    show(\n",
    "        Ind.merge(JoinType(Ind,Ty))\n",
    "        ))\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Tricky cases of merging"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "    show(\n",
    "        RecType({'a' : Ind}).merge(RecType({'b' : Ind}))\n",
    "        )\n",
    "        )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "print(\n",
    "    show(\n",
    "        RecType({'a' : Ind,\n",
    "                 'c' : JoinType(Ind,Ty)}).merge(RecType({'b' : Ind,\n",
    "                                                         'c' : Ind}))\n",
    "                                                         )\n",
    "                                                         )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = RecType({'x' : Ind,\n",
    "              'y' : (Fun('v', Ind, RecType({'a' : Ind,\n",
    "                                            'c' : PType(man, ['v'])})), ['x']),\n",
    "              'z' : Ind})\n",
    "T2 = RecType({'x' : Ind,\n",
    "              'y' : (Fun('v', Ind, RecType({'a' : Ind,\n",
    "                                            'c' : PType(man, ['v'])})), ['x']),\n",
    "              'w' : Ind})\n",
    "print(\n",
    "    show(\n",
    "        T1.merge(T2)\n",
    "        )\n",
    "        )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = RecType({'x' : Ind,\n",
    "              'y' : (Fun('v', Ind, RecType({'a' : Ind,\n",
    "                                            'c' : PType(man, ['v'])})), ['x']),\n",
    "              'z' : Ind})\n",
    "T2 = RecType({'x' : Ind,\n",
    "              'y' : (Fun('v', Ind, RecType({'a' : Ind,\n",
    "                                            'c' : PType(man, ['v'])})), ['z']),\n",
    "              'z' : Ind})\n",
    "print(\n",
    "    show(\n",
    "        T1.merge(T2)\n",
    "        )\n",
    "        )\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = RecType({'x' : SingletonType(Ind, 'j'),\n",
    "              'y' : (Fun('v', Ind, RecType({'a' : Ind,\n",
    "                                            'c' : PType(man, ['v'])})), ['x']),\n",
    "              'z' : Ind})\n",
    "T2 = RecType({'x' : Ind,\n",
    "              'y' : (Fun('v', Ind, RecType({'a' : Ind,\n",
    "                                            'c' : PType(man, ['v'])})), ['z']),\n",
    "              'z' : SingletonType(Ind, 'j')})\n",
    "print(\n",
    "    show(\n",
    "        T1.merge(T2)\n",
    "        )\n",
    "        )    "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    " In the previous Oz implementation there was an operation that would simplify\n",
    " dependent types when the path associated with them pointed to a singleton\n",
    " type.  Not (yet) implemented here."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = RecType({'a' : Ind,\n",
    "              'b' : Ind})\n",
    "T2 = RecType({'a' : SingletonType(Ind, 'j')})\n",
    "print(\n",
    "    show(\n",
    "        T1.merge(T2)\n",
    "        )\n",
    "        )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = Re\n",
    "T2 = RecType({'a' : Ind})\n",
    "print(\n",
    "    show(\n",
    "        T1.merge(T2)\n",
    "        )\n",
    "        )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = RecType({'a' : PType(man, ['j'])})\n",
    "T2 = RecType({'a' : PType(man, ['m'])})\n",
    "print(\n",
    "    show(\n",
    "        T1.merge(T2)\n",
    "        )\n",
    "        )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = RecType({'x' : Ind,\n",
    "              'e' : (Fun('v',Ind,PType(man,['v'])),['x'])})\n",
    "T2 = RecType({'e' : PType(man,['j'])})\n",
    "print(\n",
    "    show(\n",
    "        T1.merge(T2)\n",
    "        )\n",
    "        )\n",
    "print(\n",
    "    show(\n",
    "        T2.merge(T1)\n",
    "        )\n",
    "        )"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Asymmetric merge"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = Ind\n",
    "T2 = RecTy\n",
    "print(\n",
    "    show(\n",
    "        T1.amerge(T2)\n",
    "        )\n",
    "        )\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = RecType({'agenda' : SingletonType(ListType(Ty), [RecType({'e' : PType(run,['j'])})]),\n",
    "              'latest_move' : SingletonType(ListType(Re),[])})\n",
    "T2 = RecType({'agenda' : SingletonType(ListType(Ty),[]),\n",
    "              'latest_move' : RecType({'e' : PType(run,['j'])})})\n",
    "print(\n",
    "    show(\n",
    "        T1.amerge(T2)\n",
    "        )\n",
    "        )      "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = RecType({'x' : Ind,\n",
    "              'agenda' : (Fun('v',Ind,SingletonType(ListType(Ty), [RecType({'e' : PType(run,['v'])})])),['x']),\n",
    "              'latest_move' : SingletonType(ListType(Re),[])})\n",
    "T2 = RecType({'x' : Ind,\n",
    "              'agenda' : SingletonType(ListType(Ty),[]),\n",
    "              'latest_move' : (Fun('v',Ind,RecType({'e' : PType(run,['v'])})),['x'])})\n",
    "print(\n",
    "    show(\n",
    "        T1.amerge(T2)\n",
    "        )\n",
    "        )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = RecType({'x' : Ind,\n",
    "              'e' : (Fun('v',Ind,PType(run,['v'])),['x'])})\n",
    "T2 = RecType({'x' : Ind,\n",
    "              'e' : (Fun('v',Ind,PType(man,['v'])),['x'])})\n",
    "print(\n",
    "    show(\n",
    "        T1.merge(T2)\n",
    "        )\n",
    "        )\n",
    "print(\n",
    "    show(\n",
    "        T1.amerge(T2)\n",
    "        )\n",
    "        )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = RecType({'x' : Ind,\n",
    "              'e' : (Fun('v',Ind,PType(run,['v'])),['x'])})\n",
    "T2 = RecType({'y' : Ind,\n",
    "              'e' : (Fun('v',Ind,PType(man,['v'])),['y'])})\n",
    "print(\n",
    "    show(\n",
    "        T1.merge(T2)\n",
    "        )\n",
    "        )\n",
    "print(\n",
    "    show(\n",
    "        T1.amerge(T2)\n",
    "        )\n",
    "        )"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = RecType({'x' : Ind,\n",
    "              'e' : (Fun('v',Ind,RecType({'y' : Ind,\n",
    "                                          'e' : PType(run,['v'])})),['x'])})\n",
    "T2 = RecType({'y' : Ind,\n",
    "              'e' : (Fun('v',Ind,PType(man,['v'])),['y'])})\n",
    "print(\n",
    "    show(\n",
    "        T1.merge(T2)\n",
    "        )\n",
    "        )\n",
    "print(\n",
    "    show(\n",
    "        T1.amerge(T2)\n",
    "        )\n",
    "        )\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = RecType({'x' : Ind,\n",
    "              'e' : (Fun('v',Ind,RecType({'y' : Ind,\n",
    "                                          'e' : PType(run,['v'])})),['x'])})\n",
    "T2 = RecType({'y' : Ind,\n",
    "              'e' : (Fun('v',Ind,RecType({'x' : Ind,\n",
    "                                          'e' : PType(man,['v'])})),['y'])})\n",
    "print(\n",
    "    show(\n",
    "        T1.merge(T2)\n",
    "        )\n",
    "        )\n",
    "print(\n",
    "    show(\n",
    "        T1.amerge(T2)\n",
    "        )\n",
    "        )"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# String types"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "s = TTRString(['e1','e2'])\n",
    "print(show(s))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T = TTRStringType([PType(run,['j']),PType(run,['m'])])\n",
    "print(show(T))\n",
    "print(T.validate())\n",
    "ttrace()\n",
    "print(show(T.learn_witness_condition(lambda x: x)))\n",
    "nottrace()\n",
    "print(show(T.create()))\n",
    "print(show(T.create_hypobj()))\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "KPlusStringType(TTRStringType([RecTy])).query(TTRString([RecType({'e' : PType(run,['j'])}),\n",
    "                           RecType({'e' : PType(run,['m'])})]))\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T = KPlusStringType(TTRStringType([RecTy]))\n",
    "print(show(T))\n",
    "print(\n",
    "    show(\n",
    "        T.query(TTRString([RecType({'e' : PType(run,['j'])}),\n",
    "                           RecType({'e' : PType(run,['m'])})]))\n",
    "        )\n",
    "    )\n",
    "print(T.validate())\n",
    "ttrace()\n",
    "print(show(T.learn_witness_condition(lambda x: x)))\n",
    "nottrace()\n",
    "print(show(T.create()))\n",
    "print(show(T.create_hypobj()))\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = TTRStringType([Re,Re])\n",
    "T2 = KPlusStringType(TTRStringType([Re]))\n",
    "print(show(T1.subtype_of(T2)))\n",
    "print(show(T2.subtype_of(T1)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = TTRStringType([Re,Re])\n",
    "T2 = TTRStringType([RecType({'x' : Ind}), RecType({'y' : Ind})])\n",
    "print(show(T1.subtype_of(T2)))\n",
    "print(show(T2.subtype_of(T1)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = KPlusStringType(TTRStringType([Re]))\n",
    "T2 = TTRStringType([RecType({'x' : Ind}), RecType({'y' : Ind})])\n",
    "print(show(T1.subtype_of(T2)))\n",
    "print(show(T2.subtype_of(T1)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "f = Fun('v',Ty,TTRStringType([RecType({'x' : 'v'}), RecType({'y' : 'v'})]))\n",
    "print(show(f.app(Ind)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "f = Fun('v',Ty,KPlusStringType(TTRStringType([RecType({'x' : 'v'})])))\n",
    "print(show(f.app(Ind)))\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = TTRStringType([RecType({'x' : Ind}), Re])\n",
    "T2 = TTRStringType([Re, RecType({'y' : Ind})])\n",
    "print(show(T1.merge(T2)))\n",
    "print(show(T1.amerge(T2)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = TTRStringType([RecType({'x' : Ind}), RecType({'x' : Ind})])\n",
    "T2 = TTRStringType([Re, RecType({'x' : Ty})])\n",
    "print(show(T1.merge(T2)))\n",
    "print(show(T1.amerge(T2)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = KPlusStringType(TTRStringType([RecType({'x':Ind})]))\n",
    "T2 = KPlusStringType(TTRStringType([Re]))\n",
    "print(show(T1.merge(T2)))\n",
    "print(show(T1.amerge(T2)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = KPlusStringType(TTRStringType([RecTy]))\n",
    "T2 = KPlusStringType(TTRStringType([Ty]))\n",
    "print(show(T1.merge(T2)))\n",
    "print(show(T1.amerge(T2)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = TTRStringType([RecType({'x' : Ind}), RecType({'x' : Ind})])\n",
    "T2 = KPlusStringType(TTRStringType([RecType({'x':Ind})]))\n",
    "print(show(T1.merge(T2)))\n",
    "print(show(T1.amerge(T2)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "T1 = TTRStringType([RecType({'x' : Ind}), RecType({'x' : Ind})])\n",
    "T2 = KPlusStringType(TTRStringType([Ty]))\n",
    "print(show(T1.merge(T2)))\n",
    "print(show(T1.amerge(T2)))\n"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.7.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}