From 1d4cb6e62c9351ba6aee5e1422d84423d37873ce Mon Sep 17 00:00:00 2001 From: mmehdig Date: Wed, 8 Nov 2017 16:44:45 +0100 Subject: [PATCH] creating to_latex method for each type --- records.py | 17 +- ttr-overview.ipynb | 434 +++++++++++++++++++++++++++++++++++++++------ ttrtypes.py | 58 +++++- utils.py | 23 ++- 4 files changed, 466 insertions(+), 66 deletions(-) diff --git a/records.py b/records.py index 2ec9a98..16021f7 100644 --- a/records.py +++ b/records.py @@ -1,5 +1,5 @@ from collections import deque -from utils import show,ttracing,substitute +from utils import show,to_latex,ttracing,substitute class Rec(object): def __init__(self,d={}): @@ -23,6 +23,21 @@ def show(self): s = s + show(kvp[1]) return "{"+s+"}" + def to_latex(self): + s = "" + for kvp in self.__dict__.items(): + if s == "": + s = s + kvp[0] + " &=& " + else: + s = s + "\\\\\n"+kvp[0] + " &=& " + + if(isinstance(kvp[1], Rec)): + s = s + kvp[1].to_latex() + else: + s = s + to_latex(kvp[1]) + + return "\\left\\{\\begin{array}{rcl}\n"+s+"\n\\end{array}\\right\\}" + def addfield(self, label, value): if label in self.__dict__.keys(): print("\"" +label + "\"" + " is already a label in " +show(self)) diff --git a/ttr-overview.ipynb b/ttr-overview.ipynb index 4e8190d..b70e21a 100644 --- a/ttr-overview.ipynb +++ b/ttr-overview.ipynb @@ -2,7 +2,10 @@ "cells": [ { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "deletable": true, + "editable": true + }, "source": [ "# Examples from TTR overview lecture in `pyttr`" ] @@ -11,28 +14,52 @@ "cell_type": "code", "execution_count": 1, "metadata": { - "collapsed": false + "collapsed": false, + "deletable": true, + "editable": true }, "outputs": [], "source": [ "from ttrtypes import Type,BType,PType,Pred,Possibility,RecType,Fun,\\\n", " TTRStringType,KPlusStringType,LazyObj\n", "from records import Rec\n", - "from utils import show" + "from utils import show, to_ipython_latex" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "metadata": { + "collapsed": false + }, + "outputs": [], + "source": [ + "from IPython.display import Latex\n", + "\n", + "def print_latex(obj):\n", + " return print(to_ipython_latex(obj))\n", + "\n", + "def show_latex(obj):\n", + " return Latex(to_ipython_latex(obj))" ] }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "deletable": true, + "editable": true + }, "source": [ "## Judgement" ] }, { "cell_type": "code", - "execution_count": 2, + "execution_count": 3, "metadata": { - "collapsed": false + "collapsed": false, + "deletable": true, + "editable": true }, "outputs": [ { @@ -41,27 +68,65 @@ "text": [ "True\n" ] + }, + { + "data": { + "text/latex": [ + "\\begin{equation}T_{0}\\end{equation}" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 3, + "metadata": {}, + "output_type": "execute_result" } ], "source": [ "T = Type()\n", "T.judge('a')\n", "\n", - "print(T.query('a'))" + "print(T.query('a'))\n", + "show_latex(T)" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\\begin{equation}T_{0}\\end{equation}\n" + ] + } + ], + "source": [ + "print_latex(T)" ] }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "deletable": true, + "editable": true + }, "source": [ "## Basic types" ] }, { "cell_type": "code", - "execution_count": 3, + "execution_count": 5, "metadata": { - "collapsed": false + "collapsed": false, + "deletable": true, + "editable": true }, "outputs": [ { @@ -70,27 +135,46 @@ "text": [ "True\n" ] + }, + { + "data": { + "text/latex": [ + "\\begin{equation}Ind\\end{equation}" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 5, + "metadata": {}, + "output_type": "execute_result" } ], "source": [ "Ind = BType('Ind')\n", "Ind.judge('a')\n", "\n", - "print(Ind.query('a'))" + "print(Ind.query('a'))\n", + "show_latex(Ind)" ] }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "deletable": true, + "editable": true + }, "source": [ "## Intensionality" ] }, { "cell_type": "code", - "execution_count": 4, + "execution_count": 6, "metadata": { - "collapsed": false + "collapsed": false, + "deletable": true, + "editable": true }, "outputs": [ { @@ -116,18 +200,73 @@ "print(T1==T2)" ] }, + { + "cell_type": "code", + "execution_count": 7, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/latex": [ + "\\begin{equation}T_{1}\\end{equation}" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 7, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "show_latex(T1)" + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/latex": [ + "\\begin{equation}T_{2}\\end{equation}" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 8, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "show_latex(T2)" + ] + }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "deletable": true, + "editable": true + }, "source": [ "## Ptypes" ] }, { "cell_type": "code", - "execution_count": 5, + "execution_count": 9, "metadata": { - "collapsed": false + "collapsed": false, + "deletable": true, + "editable": true }, "outputs": [ { @@ -145,7 +284,7 @@ "Ind.judge('b')\n", "Ind.judge('d')\n", "run_d = PType(run,['d'])\n", - "hug_b_d = PType(run,['b','d'])\n", + "hug_b_d = PType(hug,['b','d'])\n", "run_d.judge('e1')\n", "hug_b_d.judge('e2')\n", "\n", @@ -153,18 +292,73 @@ "print(hug_b_d.query('e1'))" ] }, + { + "cell_type": "code", + "execution_count": 10, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/latex": [ + "\\begin{equation}hug(b, d)\\end{equation}" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 10, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "show_latex(hug_b_d)" + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "data": { + "text/latex": [ + "\\begin{equation}run(d)\\end{equation}" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 11, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "show_latex(run_d)" + ] + }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "deletable": true, + "editable": true + }, "source": [ "## Possibilities (models)" ] }, { "cell_type": "code", - "execution_count": 6, + "execution_count": 12, "metadata": { - "collapsed": false + "collapsed": false, + "deletable": true, + "editable": true }, "outputs": [ { @@ -175,8 +369,8 @@ "M1:\n", "_____________________________________________\n", "Ind: [a, b, d]\n", - "run(b, d): [e2]\n", "run(d): [e1]\n", + "hug(b, d): [e2]\n", "_____________________________________________\n", "\n" ] @@ -194,9 +388,11 @@ }, { "cell_type": "code", - "execution_count": 7, + "execution_count": 13, "metadata": { - "collapsed": false + "collapsed": false, + "deletable": true, + "editable": true }, "outputs": [ { @@ -224,43 +420,70 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "deletable": true, + "editable": true + }, "source": [ "## Record Types" ] }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 21, "metadata": { - "collapsed": false + "collapsed": false, + "deletable": true, + "editable": true }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "{x : Ind, e : (lambda v1:Ind . lambda v2:Ind . hug(v1, v2), [x, y]), c_boy : (lambda v:Ind . boy(v), [x]), c_dog : (lambda v:Ind . dog(v), [y]), y : Ind}\n" + "{x : Ind, c_{boy} : (lambda v:Ind . boy(v), [x]), y : Ind, c_{dog} : (lambda v:Ind . dog(v), [y]), e : (lambda v_1:Ind . lambda v_2:Ind . hug(v_1, v_2), [x, y])}\n" ] + }, + { + "data": { + "text/latex": [ + "\\begin{equation}\\left\\{\\begin{array}{rcl}\n", + "x &:& Ind\\\\\n", + "c_{boy} &:& \\langle \\lambda v:Ind . boy(v), [ x]\\rangle\\\\\n", + "y &:& Ind\\\\\n", + "c_{dog} &:& \\langle \\lambda v:Ind . dog(v), [ y]\\rangle\\\\\n", + "e &:& \\langle \\lambda v_1:Ind . \\lambda v_2:Ind . hug(v_1, v_2), [ x, y]\\rangle\n", + "\\end{array}\\right\\}\\end{equation}" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 21, + "metadata": {}, + "output_type": "execute_result" } ], "source": [ "boy = Pred('boy',[Ind])\n", "dog = Pred('dog',[Ind])\n", "a_boy_hugs_a_dog = RecType({'x':Ind,\n", - " 'c_boy':(Fun('v',Ind,PType(boy,['v'])), ['x']),\n", + " 'c_{boy}':(Fun('v',Ind,PType(boy,['v'])), ['x']),\n", " 'y':Ind,\n", - " 'c_dog':(Fun('v',Ind,PType(dog,['v'])), ['y']),\n", - " 'e':(Fun('v1',Ind,Fun('v2',Ind, PType(hug,['v1','v2']))), \n", + " 'c_{dog}':(Fun('v',Ind,PType(dog,['v'])), ['y']),\n", + " 'e':(Fun('v_1',Ind,Fun('v_2',Ind, PType(hug,['v_1','v_2']))), \n", " ['x','y'])})\n", - "print(show(a_boy_hugs_a_dog))" + "print(show(a_boy_hugs_a_dog))\n", + "show_latex(a_boy_hugs_a_dog)" ] }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 15, "metadata": { - "collapsed": false + "collapsed": false, + "deletable": true, + "editable": true }, "outputs": [ { @@ -271,9 +494,9 @@ "M3:\n", "_____________________________________________\n", "Ind: [a, b]\n", + "boy(a): [s1]\n", "dog(b): [s2]\n", "hug(a, b): [s3]\n", - "boy(a): [s1]\n", "_____________________________________________\n", "\n" ] @@ -285,8 +508,8 @@ "Ind3.in_poss(M3)\n", "Ind3.judge('a')\n", "Ind3.judge('b')\n", - "PType(boy,['a']).in_poss(M3).judge('s1')\n", - "PType(dog,['b']).in_poss(M3).judge('s2')\n", + "PType(boy,['a']).in_poss(M3).judge('s_1')\n", + "PType(dog,['b']).in_poss(M3).judge('s_2')\n", "PType(hug,['a','b']).in_poss(M3).judge('s3')\n", "\n", "print(show(M3))" @@ -294,16 +517,18 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 16, "metadata": { - "collapsed": false + "collapsed": false, + "deletable": true, + "editable": true }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "{x = a, e = s3, c_boy = s1, c_dog = s2, y = b}\n" + "{x = a, c_boy = s1, y = b, c_dog = s2, e = s3}\n" ] } ], @@ -315,16 +540,18 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 17, "metadata": { - "collapsed": false + "collapsed": false, + "deletable": true, + "editable": true }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "True\n" + "False\n" ] } ], @@ -334,7 +561,10 @@ }, { "cell_type": "markdown", - "metadata": {}, + "metadata": { + "deletable": true, + "editable": true + }, "source": [ "## String types\n", "\n", @@ -343,9 +573,11 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 18, "metadata": { - "collapsed": false + "collapsed": false, + "deletable": true, + "editable": true }, "outputs": [ { @@ -354,6 +586,19 @@ "text": [ "pick_up(a, c)^attract_attention(a, b)^throw(a, c)^run_after(b, c)^pick_up(b, c)^return_stick(b, c, a)+\n" ] + }, + { + "data": { + "text/latex": [ + "\\begin{equation}pick\\_up(a, c)⁀attract\\_attention(a, b)⁀throw(a, c)⁀run\\_after(b, c)⁀pick\\_up(b, c)⁀return\\_stick(b, c, a)+\\end{equation}" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 18, + "metadata": {}, + "output_type": "execute_result" } ], "source": [ @@ -378,12 +623,13 @@ " pick_up_b_c,return_stick_b_c_a])\n", "Fetch_a_b_c = KPlusStringType(FetchOnce_a_b_c)\n", "\n", - "print(show(Fetch_a_b_c))\n" + "print(show(Fetch_a_b_c))\n", + "show_latex(Fetch_a_b_c)" ] }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 19, "metadata": { "collapsed": false }, @@ -392,27 +638,101 @@ "name": "stdout", "output_type": "stream", "text": [ - "lambda r:{c_human : (lambda v:Ind . human(v), [x]), z : Ind, y : Ind, x : Ind, e : (lambda v1:Ind . lambda v2:Ind . lambda v3:Ind . pick_up(v1, v3)^attract_attention(v1, v2), [x, y, z]), c_dog : (lambda v:Ind . dog(v), [y]), c_stick : (lambda v:Ind . stick(v), [z])} . {e : play_fetch([r, ., x], [r, ., y])}\n" + "\\begin{equation}pick\\_up(a, c)⁀attract\\_attention(a, b)⁀throw(a, c)⁀run\\_after(b, c)⁀pick\\_up(b, c)⁀return\\_stick(b, c, a)+\\end{equation}\n" ] } ], + "source": [ + "print_latex(Fetch_a_b_c)" + ] + }, + { + "cell_type": "code", + "execution_count": 25, + "metadata": { + "collapsed": false, + "deletable": true, + "editable": true + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "lambda r:{x : Ind, c_{human} : (lambda v:Ind . human(v), [x]), y : Ind, c_{dog} : (lambda v:Ind . dog(v), [y]), z : Ind, c_{stick} : (lambda v:Ind . stick(v), [z]), e : (lambda v_1:Ind . lambda v_2:Ind . lambda v_3:Ind . pick_up(v_1, v_3)^attract_attention(v_1, v_2), [x, y, z])} . {e : play_fetch([r, ., x], [r, ., y])}\n" + ] + }, + { + "data": { + "text/latex": [ + "\\begin{equation}\\lambda r:\\left\\{\\begin{array}{rcl}\n", + "x &:& Ind\\\\\n", + "c_{human} &:& \\langle \\lambda v:Ind . human(v), [ x]\\rangle\\\\\n", + "y &:& Ind\\\\\n", + "c_{dog} &:& \\langle \\lambda v:Ind . dog(v), [ y]\\rangle\\\\\n", + "z &:& Ind\\\\\n", + "c_{stick} &:& \\langle \\lambda v:Ind . stick(v), [ z]\\rangle\\\\\n", + "e &:& \\langle \\lambda v_1:Ind . \\lambda v_2:Ind . \\lambda v_3:Ind . pick\\_up(v_1, v_3)⁀attract\\_attention(v_1, v_2), [ x, y, z]\\rangle\n", + "\\end{array}\\right\\} . \\left\\{\\begin{array}{rcl}\n", + "e &:& play\\_fetch([ r, ., x], [ r, ., y])\n", + "\\end{array}\\right\\}\\end{equation}" + ], + "text/plain": [ + "" + ] + }, + "execution_count": 25, + "metadata": {}, + "output_type": "execute_result" + } + ], "source": [ "human = Pred('human',[Ind])\n", "stick = Pred('stick',[Ind])\n", "play_fetch = Pred('play_fetch',[Ind,Ind])\n", "T = RecType({'x':Ind,\n", - " 'c_human':(Fun('v',Ind,PType(human,['v'])),['x']),\n", + " 'c_{human}':(Fun('v',Ind,PType(human,['v'])),['x']),\n", " 'y':Ind,\n", - " 'c_dog':(Fun('v',Ind,PType(dog,['v'])),['y']),\n", + " 'c_{dog}':(Fun('v',Ind,PType(dog,['v'])),['y']),\n", " 'z':Ind,\n", - " 'c_stick':(Fun('v',Ind,PType(stick,['v'])),['z']),\n", - " 'e':(Fun('v1',Ind,Fun('v2',Ind,Fun('v3',Ind, \n", - " TTRStringType([PType(pick_up,['v1','v3']),\n", - " PType(attract_attention,['v1','v2'])])))),\n", + " 'c_{stick}':(Fun('v',Ind,PType(stick,['v'])),['z']),\n", + " 'e':(Fun('v_1',Ind,Fun('v_2',Ind,Fun('v_3',Ind, \n", + " TTRStringType([PType(pick_up,['v_1','v_3']),\n", + " PType(attract_attention,['v_1','v_2'])])))),\n", " ['x','y','z'])})\n", "f = Fun('r',T,RecType({'e':PType(play_fetch,[LazyObj(['r','.','x']),LazyObj(['r','.','y'])])}))\n", "\n", - "print(show(f))" + "print(show(f))\n", + "show_latex(f)" + ] + }, + { + "cell_type": "code", + "execution_count": 22, + "metadata": { + "collapsed": false + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\\begin{equation}\\lambda r:\\left\\{\\begin{array}{rcl}\n", + "x &:& Ind\\\\\n", + "c_{human} &:& \\langle \\lambda v:Ind . human(v), [ x]\\rangle\\\\\n", + "y &:& Ind\\\\\n", + "c_{dog} &:& \\langle \\lambda v:Ind . dog(v), [ y]\\rangle\\\\\n", + "z &:& Ind\\\\\n", + "c_{stick} &:& \\langle \\lambda v:Ind . stick(v), [ z]\\rangle\\\\\n", + "e &:& \\langle \\lambda v1:Ind . \\lambda v2:Ind . \\lambda v3:Ind . pick\\_up(v1, v3)⁀attract\\_attention(v1, v2), [ x, y, z]\\rangle\n", + "\\end{array}\\right\\} . \\left\\{\\begin{array}{rcl}\n", + "e &:& play\\_fetch([ r, ., x], [ r, ., y])\n", + "\\end{array}\\right\\}\\end{equation}\n" + ] + } + ], + "source": [ + "print_latex(f)" ] }, { @@ -441,7 +761,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.4.3" + "version": "3.6.1" } }, "nbformat": 4, diff --git a/ttrtypes.py b/ttrtypes.py index 9ed13d5..4ef4297 100644 --- a/ttrtypes.py +++ b/ttrtypes.py @@ -1,6 +1,6 @@ from collections import deque #from types import MethodType -from utils import gensym, some_condition, forall, forsome, substitute, show, showall, ttracing +from utils import gensym, some_condition, forall, forsome, substitute, show, to_latex, showall, ttracing from records import Rec @@ -29,6 +29,8 @@ def in_poss(self,poss): return poss.model[self.show()] def show(self): return self.name + def to_latex(self): + return self.name def learn_witness_condition(self, c): self.witness_conditions.append(c) def validate_witness(self, a): @@ -114,7 +116,7 @@ def __init__(self,name=gensym('BT')): self.witness_cache = [] self.supertype_cache = [] self.witness_conditions = [] - + class PType(Type): def __init__(self,pred,args): self.comps = Rec({'pred':pred, 'args':args}) @@ -123,6 +125,8 @@ def __init__(self,pred,args): self.witness_conditions = [] def show(self): return self.comps.pred.name+'('+', '.join([show(x) for x in self.comps.args])+')' + def to_latex(self): + return self.comps.pred.name.replace('_','\\_')+'('+', '.join([to_latex(x) for x in self.comps.args])+')' def validate(self): if isinstance(self.comps.pred,Pred) \ and len(self.comps.args) == len(self.comps.pred.arity): @@ -165,6 +169,8 @@ def __init__(self,T1,T2): and self.comps.right.query(a)] def show(self): return '('+ self.comps.left.show()+'&'+self.comps.right.show()+')' + def to_latex(self): + return '\\left(\\begin{array}{rcl}\n'+ self.comps.left.to_latex()+'\land'+self.comps.right.to_latex()+'\n\\end{array}\\right)' def learn_witness_condition(self,c): if ttracing('learn_witness_condition'): print('Meet types are logical and cannot learn new conditions') @@ -207,6 +213,8 @@ def __init__(self,T1,T2): lambda a: self.comps.right.query(a)] def show(self): return '('+ self.comps.left.show()+'v'+self.comps.right.show()+')' + def to_latex(self): + return '\\left(\\begin{array}{rcl}\n'+ self.comps.left.to_latex()+'v'+self.comps.right.to_latex()+'\n\\end{array}\\right)' def learn_witness_condition(self,c): print('Join types are logical and cannot learn new conditions') def validate(self): @@ -245,6 +253,9 @@ def __init__(self,T1,T2): and self.comps.range.query(f.app(self.comps.domain.create_hypobj()))] def show(self): return '('+ self.comps.domain.show() + '->' + self.comps.range.show()+')' + def to_latex(self): + return '\\left(\\begin{array}{rcl}\n'+ self.comps.domain.to_latex() + '->' + self.comps.range.to_latex()+'\n\\end{array}\\right))' + def learn_witness_condition(self,c): print('Function types are logical and cannot learn new conditions') def validate(self): @@ -267,6 +278,8 @@ def __init__(self,T): self.witness_conditions = [lambda l: isinstance(l,list) and forall(l, lambda x: T.query(x))] def show(self): return '['+ show(self.comps.base_type)+']' + def to_latex(self): + return '\\left[\\begin{array}{rcl}\n'+ to_latex(self.comps.base_type)+'\n\\end{array}\\right]' def learn_witness_condition(self,c): print('Function types are logical and cannot learn new conditions') def validate(self): @@ -288,6 +301,8 @@ def __init__(self,T,a): and show(x) == show(a.eval()) and T.query(x)] def show(self): return show(self.comps.base_type)+'_'+ show(self.comps.obj) + def to_latex(self): + return to_latex(self.comps.base_type)+'_{'+ to_latex(self.comps.obj)+'}' def learn_witness_condition(self,c): print('Function types are logical and cannot learn new conditions') def validate(self): @@ -336,6 +351,21 @@ def show(self): else: s = s + show(kvp[1]) return "{"+s+"}" + + def to_latex(self): + s = "" + for kvp in self.comps.__dict__.items(): + if s == "": + s = s + kvp[0] + " &:& " + else: + s = s + "\\\\\n"+kvp[0] + " &:& " + + if(isinstance(kvp[1], RecType)): + s = s + kvp[1].to_latex() + else: + s = s + to_latex(kvp[1]) + return "\\left\\{\\begin{array}{rcl}\n"+s+"\n\\end{array}\\right\\}" + def validate(self): if forall(list(self.comps.__dict__.items()),lambda x: CheckField(x,self)) and not self.create_hypobj() == None: return True @@ -597,8 +627,8 @@ def ProcessDepFields(depfields,res,rtype,mode='real'): return None class TTRStringType(Type): - def __init__(self,list): - self.comps = Rec({'types' : list}) + def __init__(self,list_of_types): + self.comps = Rec({'types' : list_of_types}) self.witness_cache = [] self.supertype_cache = [] self.witness_conditions = \ @@ -612,6 +642,9 @@ def in_poss(self,poss): return self def show(self): return '^'.join([show(i) for i in self.comps.types]) + def to_latex(self): + # TODO + return '⁀'.join([to_latex(i) for i in self.comps.types]) def validate(self): return forall(self.comps.types, lambda T: isinstance(T,Type)) def learn_witness_condition(self,c): @@ -659,6 +692,9 @@ def __init__(self,T): self.poss = '' def show(self): return show(self.comps.base_type)+'+' + def to_latex(self): + # TODO + return to_latex(self.comps.base_type)+'+' def validate(self): return isinstance(self.comps.base_type, Type) def learn_witness_condition(self,c): @@ -737,6 +773,8 @@ def __init__(self,name,arity): self.arity = arity def show(self): return self.name + def to_latex(self): + return self.name.replace('_', '\\_') class Fun(object): def __init__(self,v,dom,body): @@ -745,6 +783,8 @@ def __init__(self,v,dom,body): self.__setattr__('body',body) def show(self): return 'lambda ' + self.var + ':' + self.domain_type.show() + ' . ' + show(self.body) + def to_latex(self): + return '\\lambda ' + self.var + ':' + self.domain_type.to_latex() + ' . ' + to_latex(self.body) def validate(self): if isinstance(self.var,str) and isinstance(self.domain_type,Type): return True @@ -801,7 +841,7 @@ def merge_dep_types(f1,f2): if ttracing('merge_dep_types'): print(show(f1)+' and '+show(f2)+' cannot be merged.') return None - + def combine_dep_types(f1,f2): if isinstance(f1,Type) and isinstance(f2,Type): @@ -846,6 +886,8 @@ def validate(self): return forall(self.types,lambda x: isinstance(x,Type)) def show(self): return self.name + def to_latex(self): + return self.name class LazyObj(object): def __init__(self,strlist): @@ -885,6 +927,8 @@ def type(self): return None def show(self): return show(self.oplist) + def to_latex(self): + return to_latex(self.oplist) class Possibility: def __init__(self,name='',d=None): @@ -903,6 +947,8 @@ def __init__(self,rec,path): self.path = path def show(self): return show(self.rec)+'.'+show(self.path) + def to_latex(self): + return to_latex(self.rec)+'.'+to_latex(self.path) def subst(self,v,a): return AbsPath(substitute(self.rec,v,a),substitute(self.path,v,a)) @@ -916,6 +962,8 @@ def concat(self,s): return TTRString(self.items+[s]) def show(self): return '^'.join([show(i) for i in self.items]) + def to_latex(self): + return '^'.join([to_latex(i) for i in self.items]) #============================ diff --git a/utils.py b/utils.py index 0a9aa3e..e231cb0 100644 --- a/utils.py +++ b/utils.py @@ -4,8 +4,8 @@ def gensym(x): if x not in gennum: - gennum[x] = count() - return x+str(gennum[x].__next__()) + gennum[x] = count() + return x+'_{'+str(gennum[x].__next__())+'}' def some_condition(conds,obj): @@ -40,6 +40,23 @@ def show(obj): return str(obj) +def to_latex(obj): + if isinstance(obj,str): + return obj + elif isinstance(obj,list): + return '[ '+ ', '.join([to_latex(x) for x in obj])+']' + elif isinstance(obj,tuple): + return '\\langle '+ ', '.join([to_latex(x) for x in obj])+'\\rangle' + elif isinstance(obj,dict): + return '\\left\\{\\begin{array}{rcl}\n'+'\\\\\n'.join([to_latex(i[0])+' &=& '+to_latex(i[1]) for i in obj.items()])+'\n\\end{array}\\right\\}' + elif 'to_latex' in dir(obj): + return obj.to_latex() + else: + return str(obj) + +def to_ipython_latex(obj): + return '\\begin{equation}' + to_latex(obj) + '\\end{equation}' + def showall(objs): return [show(obj) for obj in objs] @@ -57,7 +74,7 @@ def substitute(obj,v,a): def example(num): print('\n\nExample '+str(num)+':\n') - + ######################