eval_idea.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "# Counting Usage of Lemmas \n",
    "\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "This script attempts to evaluate the project \n",
    "\n",
    "The first stage is finding the usage of lemmas towards the declaration\n",
    "\n",
    "A further step is to score the difficulty of lemmas given their counts of the basic lemmas\n",
    "    refl\n",
    "    sym\n",
    "    trans\n",
    "    cong \n",
    "    ε-right\n",
    "    ε-left \n",
    "    ∙-assoc\n",
    "    "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "collapsed": true,
    "deletable": true,
    "editable": true
   },
   "outputs": [],
   "source": [
    "from __future__ import unicode_literals\n",
    "import re\n",
    "\n",
    "import pandas as pd\n",
    "import numpy as np"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "collapsed": true,
    "deletable": true,
    "editable": true
   },
   "outputs": [],
   "source": [
    "agda_file_location = 'agda-playground/fingertree/FingerTree-measure-size-c.agda'\n",
    "#agda_file_location = 'agda-playground/fingertree/list-reverse-proof.agda'\n",
    "\n",
    "#requirements are that all declarations are separated by at least a newline\n",
    "\n",
    "#as a styling techinique to make this easier:\n",
    "# all lemmas contain the word lemma\n",
    "# lemmas that are derived through the monoid solver have a dash (') at the end\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "collapsed": true,
    "deletable": true,
    "editable": true
   },
   "outputs": [],
   "source": [
    "# regular expressions\n",
    "\n",
    "#comment in the begining\n",
    "comment_begining = r'^\\s*--'\n",
    "\n",
    "#imports \n",
    "imports_begining = r'^(\\s*open)|(\\s*open\\s*import)|(\\s*import)'\n",
    "\n",
    "#infixation\n",
    "infix_begining = r'^\\s*infix[lr]*'\n",
    "\n",
    "#instance\n",
    "instance_begining = r'^\\s*instance'\n",
    "\n",
    "#data\n",
    "data_begining = r'^\\s*data'\n",
    "\n",
    "#mutual\n",
    "mutual_begining = r'^\\s*mutual'\n",
    "\n",
    "#module \n",
    "module = r'^\\s*module'\n",
    "\n",
    "#declarations\n",
    "decl = r'^\\s*(postulate){0,1}\\s*([^\\s:]+)\\s*:'\n",
    "\n",
    "#lemmas \n",
    "lemmas = [r'refl',\n",
    "          r'sym',\n",
    "          r'cong',\n",
    "          r'≡⟨',          \n",
    "          r'ε-left',\n",
    "          r'ε-right',\n",
    "          r'∙-assoc',\n",
    "          r'[^\\s:\\(]+lemma[^\\s:\\)]*',    #two ways through which\n",
    "          r'[^\\s:\\(]+correct[^\\s:\\)]*']  #I identify lemmas in the src.\n",
    "\n",
    "#lemma building blocks.\n",
    "basic_lemmas = [r'refl',\n",
    "          r'sym',\n",
    "          r'cong',\n",
    "          r'≡⟨',     #this is equivalent to a trans application\n",
    "          r'ε-left',\n",
    "          r'ε-right',\n",
    "          r'∙-assoc']\n",
    "\n",
    "\n",
    "#for pretty printing\n",
    "basic_lemmas_names = [r'refl',\n",
    "          r'sym',\n",
    "          r'cong',\n",
    "          r'trans',    \n",
    "          r'ε-left',\n",
    "          r'ε-right',\n",
    "          r'∙-assoc']                "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [],
   "source": [
    "import codecs\n",
    "\n",
    "agda_file = codecs.open(agda_file_location, 'r', encoding='utf-8')\n",
    "lines = agda_file.readlines()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [],
   "source": [
    "def remove_all_lines(reg, lines):\n",
    "    filter_fun = lambda x : (re.match(reg, x) == None)\n",
    "    return [x for x in lines if filter_fun(x)]\n",
    "\n",
    "def remove_ending_comment(line):\n",
    "    return line.split('--')[0]\n",
    "\n",
    "def strip_ending_comments(lines):\n",
    "    return [remove_ending_comment(x) for x in lines]\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [],
   "source": [
    "#preprocessing the lines -- decluttering the document \n",
    "\n",
    "\n",
    "lines = remove_all_lines(comment_begining, lines)\n",
    "lines = remove_all_lines(imports_begining, lines)\n",
    "lines = remove_all_lines(infix_begining, lines)\n",
    "lines = remove_all_lines(mutual_begining, lines)\n",
    "lines = remove_all_lines(module, lines)\n",
    "lines = strip_ending_comments(lines)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [],
   "source": [
    "# at least * all top level declarations \n",
    "#these are toplogically sorted\n",
    "\n",
    "declarations = [re.search(decl, x).group(1) for x in lines if re.search(decl,x) is not None]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [],
   "source": [
    "#splitting in sections \n",
    "\n",
    "new_lines = [i for (i, x) in enumerate(lines) if x == u'\\n']\n",
    "\n",
    "#partition to sections\n",
    "#that is, each section corresponds to a declaration\n",
    "def partition(new_lines, lines):\n",
    "    parts = []\n",
    "    N = len (new_lines)\n",
    "    for i in range(1, N):\n",
    "        parts.append(lines[new_lines[i-1] + 1 : new_lines[i]])\n",
    "    return parts\n",
    "\n",
    "parts = partition(new_lines, lines)\n",
    "\n",
    "#remove empty lists \n",
    "parts = [x for x in parts if len(x) > 0]\n",
    "\n",
    "#select only sections that are not data declarations\n",
    "#we are only interested in function declarations\n",
    "def select_parts_begining(regex, parts):\n",
    "    filter_fun = lambda x : (re.match(regex, x[0]) == None) \n",
    "    return [x for x in parts if filter_fun(x)]\n",
    "\n",
    "decl_parts = select_parts_begining(data_begining, parts)\n",
    "\n",
    "#select all sections that are not instance declarations -- makes things easier\n",
    "decl_parts = select_parts_begining(instance_begining, decl_parts)\n",
    "\n",
    "#identify declarations in each part\n",
    "def parts_dict(parts):\n",
    "    p_dict = {}\n",
    "    for part in parts:\n",
    "        line = part[0]\n",
    "        decl_match = re.search(decl, line)\n",
    "        if (decl_match is None):\n",
    "            print part\n",
    "        declr = decl_match.group(2)\n",
    "        assert declr not in p_dict\n",
    "        p_dict[declr] = part\n",
    "    return p_dict\n",
    "\n",
    "# find all the lemmas used in a declaration(part)\n",
    "def find_lemmas(decl, part):\n",
    "    #outputs {n_lines, rec, lemmas}\n",
    "    results = []    \n",
    "    n_lines = len(part)\n",
    "    rec = False \n",
    "    \n",
    "    for regex in lemmas:\n",
    "        for line in part:\n",
    "            results += re.findall(regex, line)\n",
    "        #    print results\n",
    "    results = [x for x in results if not (x == decl)]\n",
    "    \n",
    "    #find whether it is recursive -- TODO    \n",
    "    rec_regex = r'\\s+[^\\s]+\\s+' + decl\n",
    "    # don't want the declaration to appear at new line, \n",
    "    # because that's just caused by initialisation    \n",
    "    rec_list = []\n",
    "    for line in part: \n",
    "        rec_list += re.findall(rec_regex, line)        \n",
    "    if rec_list is not []:\n",
    "        rec = True;\n",
    "        \n",
    "    return {'n_lines' : n_lines, 'rec' : rec, 'lemmas' : results}\n",
    "    "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [],
   "source": [
    "decl_dict = parts_dict(decl_parts)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [],
   "source": [
    "def lemma_dict(decl_dict):\n",
    "    result = {}\n",
    "    for key in decl_dict:\n",
    "        result[key] = find_lemmas(key, decl_dict[key])['lemmas']\n",
    "    return result\n",
    "\n",
    "\n",
    "# other lemmas stats\n",
    "\n",
    "def declaration_stats(decl_dict):\n",
    "    result = {}\n",
    "    for key in decl_dict:\n",
    "        lemma_stat = find_lemmas(key, decl_dict[key])\n",
    "        result[key] = lemma_stat['n_lines'], lemma_stat['rec']\n",
    "    result = pd.DataFrame.from_dict(result, 'index')\n",
    "    result.columns = ['n_lines', 'rec']\n",
    "    return result"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[u'refl',\n",
       " u'refl',\n",
       " u'refl',\n",
       " u'sym',\n",
       " u'sym',\n",
       " u'cong',\n",
       " u'cong',\n",
       " u'cong',\n",
       " u'\\u2261\\u27e8',\n",
       " u'\\u2261\\u27e8',\n",
       " u'\\u2261\\u27e8',\n",
       " u'\\u2261\\u27e8',\n",
       " u'\\u2261\\u27e8',\n",
       " u'\\u2261\\u27e8',\n",
       " u'flatten-fold-lemma',\n",
       " u'foldl-append-lemma2',\n",
       " u'foldl-dig-correct',\n",
       " u'foldl-dig-correct']"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "lemma_usage = lemma_dict(decl_dict)\n",
    "lemma_usage['foldl-correct']"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [],
   "source": [
    "#this fills up automatically because of memoisation\n",
    "flattened_lemmas = {}\n",
    "\n",
    "def flatten_list(l):\n",
    "    result = []\n",
    "    if type(element) is str:\n",
    "        result.append(element)\n",
    "    else:\n",
    "        result += element\n",
    "    return result\n",
    "\n",
    "def flatten_lemma(decl, lemma_dict):\n",
    "    if decl in flattened_lemmas:\n",
    "        return flattened_lemmas[decl]\n",
    "    \n",
    "    if decl in lemma_dict:\n",
    "        used_lemmas = lemma_dict[decl]\n",
    "    else:\n",
    "        used_lemmas = []\n",
    "        \n",
    "    for (i, lemma) in enumerate(used_lemmas):\n",
    "        if lemma not in basic_lemmas:\n",
    "            flat = flatten_lemma(lemma, lemma_dict)\n",
    "            used_lemmas[i:i+1] = flat\n",
    "             \n",
    "    flattened_lemmas[decl] = used_lemmas\n",
    "    return used_lemmas    "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [],
   "source": [
    "def flatten_dict(lemma_usage):\n",
    "    for key in lemma_usage:\n",
    "        flatten_lemma(key, lemma_usage)\n",
    "\n",
    "flatten_dict(lemma_usage)\n",
    "\n",
    "lemma_dict = flattened_lemmas\n",
    "\n",
    "\n",
    "# normalizes a lemma list as a frequency vector of basic lemmas usage\n",
    "def normalize_lemma_vec(lemmas):\n",
    "    result = np.zeros(len(basic_lemmas))\n",
    "    for lemma in lemmas:\n",
    "        if lemma in basic_lemmas:\n",
    "            i = basic_lemmas.index(lemma)\n",
    "            result[i] += 1\n",
    "    return result\n",
    "\n",
    "# normalize the whole dictionary\n",
    "def normalize_lemma_dict(lemma_dict):\n",
    "    result = {}\n",
    "    for key in lemma_dict:\n",
    "        result[key] = normalize_lemma_vec(lemma_dict[key])\n",
    "    return result\n",
    "\n",
    "# alternative lemma dictionary with unique lemmas\n",
    "def all_lemma_dict(lemma_dict):\n",
    "    result = {}\n",
    "    for key in lemma_dict:\n",
    "        result[key] = set(lemma_dict[key])\n",
    "    return result\n",
    "\n",
    "norm_lemma_dict = normalize_lemma_dict(lemma_dict)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true,
    "scrolled": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "refl       3\n",
       "sym        5\n",
       "cong       1\n",
       "trans      6\n",
       "ε-left     4\n",
       "ε-right    2\n",
       "∙-assoc    3\n",
       "dtype: int64"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "#need to find a way to analyze this data\n",
    "df_lemmas = pd.DataFrame.from_dict(norm_lemma_dict, orient='index', dtype=int)\n",
    "df_lemmas.columns = basic_lemmas_names\n",
    "df_lemmas.loc['deepL'] + df_lemmas.loc['viewL']"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true,
    "scrolled": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "refl       48\n",
       "sym        23\n",
       "cong       15\n",
       "trans      46\n",
       "ε-left     22\n",
       "ε-right    13\n",
       "∙-assoc    21\n",
       "dtype: int64"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "df_lemmas.loc['split-Tree'] +  \\\n",
    "df_lemmas.loc['split-Tree-if'] +  \\\n",
    "df_lemmas.loc['split-Tree1'] +  \\\n",
    "df_lemmas.loc['split-Tree2'] +  \\\n",
    "df_lemmas.loc['split-Tree3'] +  \\\n",
    "df_lemmas.loc['split-Tree-single'] "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "refl        0\n",
       "sym        16\n",
       "cong       11\n",
       "trans      23\n",
       "ε-left      2\n",
       "ε-right     0\n",
       "∙-assoc    18\n",
       "Name: _▷_, dtype: int64"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "df_lemmas.loc['_▷_']"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "refl       1\n",
       "sym        2\n",
       "cong       3\n",
       "trans      3\n",
       "ε-left     1\n",
       "ε-right    1\n",
       "∙-assoc    6\n",
       "Name: _◁_, dtype: int64"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "df_lemmas.loc['_◁_']"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "refl        3\n",
       "sym         8\n",
       "cong        5\n",
       "trans      10\n",
       "ε-left      2\n",
       "ε-right     4\n",
       "∙-assoc     8\n",
       "dtype: int64"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "df_lemmas.loc['viewR'] + df_lemmas.loc['deepR']"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "refl       6\n",
       "sym        2\n",
       "cong       4\n",
       "trans      4\n",
       "ε-left     1\n",
       "ε-right    1\n",
       "∙-assoc    6\n",
       "Name: cons-correct, dtype: int64"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "df_lemmas.loc['cons-correct']"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {
    "collapsed": true,
    "deletable": true,
    "editable": true
   },
   "outputs": [],
   "source": [
    "myline = \"\"\" trans\n",
    "  (sym\n",
    "   (trans\n",
    "    (trans\n",
    "     (cong (M Monoid.∙ x)\n",
    "      (trans\n",
    "       (cong (M Monoid.∙ x₁)\n",
    "        (trans\n",
    "         (cong (M Monoid.∙ x₂)\n",
    "          (sym (Monoid.ε-left M ((M Monoid.∙ x₃) (Monoid.ε M)))))\n",
    "         (trans\n",
    "          (Monoid.∙-assoc M x₂ (Monoid.ε M) ((M Monoid.∙ x₃) (Monoid.ε M)))\n",
    "          refl)))\n",
    "       (trans\n",
    "        (Monoid.∙-assoc M x₁ ((M Monoid.∙ x₂) (Monoid.ε M))\n",
    "         ((M Monoid.∙ x₃) (Monoid.ε M)))\n",
    "        refl)))\n",
    "     (trans\n",
    "      (Monoid.∙-assoc M x\n",
    "       ((M Monoid.∙ x₁) ((M Monoid.∙ x₂) (Monoid.ε M)))\n",
    "       ((M Monoid.∙ x₃) (Monoid.ε M)))\n",
    "      refl))\n",
    "    (trans\n",
    "     (cong₂ (Monoid._∙_ M)\n",
    "      (trans\n",
    "       (trans\n",
    "        (cong (M Monoid.∙ x)\n",
    "         (trans\n",
    "          (cong (M Monoid.∙ x₁)\n",
    "           (sym (Monoid.ε-left M ((M Monoid.∙ x₂) (Monoid.ε M)))))\n",
    "          (trans\n",
    "           (Monoid.∙-assoc M x₁ (Monoid.ε M) ((M Monoid.∙ x₂) (Monoid.ε M)))\n",
    "           refl)))\n",
    "        (trans\n",
    "         (Monoid.∙-assoc M x ((M Monoid.∙ x₁) (Monoid.ε M))\n",
    "          ((M Monoid.∙ x₂) (Monoid.ε M)))\n",
    "         refl))\n",
    "       (trans\n",
    "        (cong₂ (Monoid._∙_ M)\n",
    "         (trans\n",
    "          (trans\n",
    "           (cong (M Monoid.∙ x)\n",
    "            (sym (Monoid.ε-left M ((M Monoid.∙ x₁) (Monoid.ε M)))))\n",
    "           (trans\n",
    "            (Monoid.∙-assoc M x (Monoid.ε M) ((M Monoid.∙ x₁) (Monoid.ε M)))\n",
    "            refl))\n",
    "          (trans\n",
    "           (cong₂ (Monoid._∙_ M) (Monoid.ε-right M x) (Monoid.ε-right M x₁))\n",
    "           refl))\n",
    "         (Monoid.ε-right M x₂))\n",
    "        refl))\n",
    "      (Monoid.ε-right M x₃))\n",
    "     refl)))\n",
    "  (trans\n",
    "   (trans\n",
    "    (trans\n",
    "     (cong (M Monoid.∙ x)\n",
    "      (sym\n",
    "       (Monoid.ε-left M\n",
    "        ((M Monoid.∙ x₁)\n",
    "         ((M Monoid.∙ x₂) ((M Monoid.∙ x₃) (Monoid.ε M)))))))\n",
    "     (trans\n",
    "      (Monoid.∙-assoc M x (Monoid.ε M)\n",
    "       ((M Monoid.∙ x₁) ((M Monoid.∙ x₂) ((M Monoid.∙ x₃) (Monoid.ε M)))))\n",
    "      refl))\n",
    "    (trans\n",
    "     (cong₂ (Monoid._∙_ M) (Monoid.ε-right M x)\n",
    "      (trans\n",
    "       (trans\n",
    "        (cong (M Monoid.∙ x₁)\n",
    "         (sym\n",
    "          (Monoid.ε-left M\n",
    "           ((M Monoid.∙ x₂) ((M Monoid.∙ x₃) (Monoid.ε M))))))\n",
    "        (trans\n",
    "         (Monoid.∙-assoc M x₁ (Monoid.ε M)\n",
    "          ((M Monoid.∙ x₂) ((M Monoid.∙ x₃) (Monoid.ε M))))\n",
    "         refl))\n",
    "       (trans\n",
    "        (cong₂ (Monoid._∙_ M) (Monoid.ε-right M x₁)\n",
    "         (trans\n",
    "          (trans\n",
    "           (cong (M Monoid.∙ x₂)\n",
    "            (sym (Monoid.ε-left M ((M Monoid.∙ x₃) (Monoid.ε M)))))\n",
    "           (trans\n",
    "            (Monoid.∙-assoc M x₂ (Monoid.ε M) ((M Monoid.∙ x₃) (Monoid.ε M)))\n",
    "            refl))\n",
    "          (trans\n",
    "           (cong₂ (Monoid._∙_ M) (Monoid.ε-right M x₂) (Monoid.ε-right M x₃))\n",
    "           refl)))\n",
    "        refl)))\n",
    "     refl))\n",
    "   refl)\"\"\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{u'lemmas': [], u'n_lines': 2685, u'rec': True}"
      ]
     },
     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "find_lemmas(\"asdaf\", myline)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "32"
      ]
     },
     "execution_count": 23,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "myline.count(\"trans\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "7"
      ]
     },
     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "myline.count(\"sym\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "16"
      ]
     },
     "execution_count": 25,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "myline.count(\"refl\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "15"
      ]
     },
     "execution_count": 26,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "myline.count(\"cong\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "9"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "myline.count(\"∙-assoc\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "6"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "myline.count(\"ε-left\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "metadata": {
    "collapsed": false
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "8"
      ]
     },
     "execution_count": 29,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "myline.count(\"ε-right\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": []
  }
 ],
 "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
}