natural language toolkit discourse representation theory drt dan garrette dhgarrettegmail com c 20012023 nltk project url https www nltk org for license information see license txt import tkinterbased modules if they are available no need to print a warning here nltk draw has already printed one a lambda calculus expression parser def initself logicparser initself self operatorprecedence dict x 1 for x in drttokens lambdalist x 2 for x in drttokens notlist app 3 x 4 for x in drttokens eqlist tokens neqlist drttokens colon 5 drttokens drsconc 6 x 7 for x in drttokens orlist x 8 for x in drttokens implist none 9 def getallsymbolsself this method is intended to be overridden for logics that use different operators or expressions if tok in drttokens notlist return self handlenegationtok context elif tok in drttokens lambdalist return self handlelambdatok context elif tok drttokens open if self inrange0 and self token0 drttokens openbracket return self handledrstok context else return self handleopentok context elif tok upper drttokens drs self assertnexttokendrttokens open return self handledrstok context elif self isvariabletok if self inrange0 and self token0 drttokens colon return self handleproptok context else return self handlevariabletok context def makenegatedexpressionself expression return drtnegatedexpressionexpression def handledrsself tok context a drs refs self handlerefs if self inrange0 and self token0 drttokens comma if there is a comma it s optional self token swallow the comma conds self handlecondscontext self assertnexttokendrttokens close return drsrefs conds none def handlerefsself self assertnexttokendrttokens openbracket refs while self inrange0 and self token0 drttokens closebracket support expressions like drsx y c drsx y c if refs and self token0 drttokens comma self token swallow the comma refs appendself getnexttokenvariablequantified self assertnexttokendrttokens closebracket return refs def handlecondsself context self assertnexttokendrttokens openbracket conds while self inrange0 and self token0 drttokens closebracket support expressions like drsx y c drsx y c if conds and self token0 drttokens comma self token swallow the comma conds appendself processnextexpressioncontext self assertnexttokendrttokens closebracket return conds def handlepropself tok context variable self makevariableexpressiontok self assertnexttoken drs self processnextexpressiondrttokens colon return drtpropositionvariable drs def makeequalityexpressionself first second this method serves as a hook for other logic parsers that have different boolean operators if tok drttokens drsconc return lambda first second drtconcatenationfirst second none elif tok in drttokens orlist return drtorexpression elif tok in drttokens implist def makeimpexpressionfirst second if isinstancefirst drs return drsfirst refs first conds second if isinstancefirst drtconcatenation return drtconcatenationfirst first first second second raise exceptionantecedent of implication must be a drs return makeimpexpression else return none def makebooleanexpressionself factory first second return factoryfirst second def makeapplicationexpressionself function argument return drtapplicationexpressionfunction argument def makevariableexpressionself name return drtvariableexpressionvariablename def makelambdaexpressionself variables term return drtlambdaexpressionvariables term class drtexpression drtparser drtparser classmethod def fromstringcls s return cls drtparser parses def applytoself other return drtapplicationexpressionself other def negself return drtnegatedexpressionself def andself other return notimplemented def orself other assert isinstanceother drtexpression return drtorexpressionself other def gtself other assert isinstanceother drtexpression if isinstanceself drs return drsself refs self conds other if isinstanceself drtconcatenation return drtconcatenationself first self second other raise exceptionantecedent of implication must be a drs def equivself other provernone assert isinstanceother drtexpression f1 self simplify fol f2 other simplify fol return f1 equivf2 prover property def typeself raise attributeerror s object has no attribute type self class name def typecheckself signaturenone raise notimplementederror def addself other return drtconcatenationself other none def getrefsself recursivefalse raise notimplementederror def ispronounfunctionself draw the drs return the pretty print string a discourse representation structure def initself refs conds consequentnone self refs refs self conds conds self consequent consequent def replaceself variable expression replaceboundfalse alphaconverttrue if a bound variable is the thing being replaced any bound variable that appears in the expression must be alpha converted to avoid a conflict replace in the conditions see expression free condsfree reduceoperator or c free for c in self conds set if self consequent condsfree updateself consequent free return condsfree setself refs def getrefsself recursivefalse see expression visit parts listmapfunction self conds if self consequent parts appendfunctionself consequent return combinatorparts def visitstructuredself function combinator this is a factory method that instantiates and returns a subtype of drtabstractvariableexpression appropriate for the given variable see abstractexpression getrefs return def prettyself s s self blank lens return blank blank s blank def eliminateequalityself return self class drtindividualvariableexpression drtabstractvariableexpression individualvariableexpression pass class drtfunctionvariableexpression drtabstractvariableexpression functionvariableexpression pass class drteventvariableexpression drtindividualvariableexpression eventvariableexpression pass class drtconstantexpressiondrtabstractvariableexpression constantexpression pass class drtpropositiondrtexpression expression def initself variable drs self variable variable self drs drs def replaceself variable expression replaceboundfalse alphaconverttrue if self variable variable assert isinstance expression drtabstractvariableexpression can only replace a proposition label with a variable return drtproposition expression variable self drs replacevariable expression replacebound alphaconvert else return drtproposition self variable self drs replacevariable expression replacebound alphaconvert def eliminateequalityself return drtpropositionself variable self drs eliminateequality def getrefsself recursivefalse return self drs getrefstrue if recursive else def eqself other return self class other class and self variable other variable and self drs other drs def neself other return not self other hash expression hash def folself return self drs fol def prettyself drss self drs pretty blank lens self variable return blank line for line in drss 1 s self variable line for line in drss1 2 blank line for line in drss2 def visitself function combinator see expression visitstructured return combinatorself variable functionself drs def strself return fpropself variable self drs class drtnegatedexpressiondrtexpression negatedexpression def folself return negatedexpressionself term fol def getrefsself recursivefalse rename all occurrences of the variable introduced by this variable binder in the expression to newvar param newvar variable for the new variable see abstractexpression getrefs return self variable self term getrefstrue if recursive else self variable class drtbinaryexpressiondrtexpression binaryexpression def getrefsself recursivefalse drs of the form drs drs def initself first second consequentnone drtbooleanexpression initself first second self consequent consequent def replaceself variable expression replaceboundfalse alphaconverttrue if variable is bound alpha convert every ref that is free in expression todo at some point for now simplify for any ref that is in both first and second alpha convert the ref in second to prevent collision see abstractexpression getrefs refs self first getrefsrecursive self second getrefsrecursive if self consequent and recursive refs extendself consequent getrefstrue return refs def getopself return drttokens drsconc def eqself other rdefines equality modulo alphabetic variance if we are comparing x m and y n then check equality of m and nxy if isinstanceother drtconcatenation selfrefs self getrefs otherrefs other getrefs if lenselfrefs lenotherrefs convertedother other for r1 r2 in zipselfrefs otherrefs varex self makevariableexpressionr1 convertedother convertedother replacer2 varex true return self first convertedother first and self second convertedother second and self consequent convertedother consequent return false def neself other return not self other hash drtbooleanexpression hash def folself e andexpressionself first fol self second fol if self consequent e impexpressione self consequent fol return e def prettyself drs drtbinaryexpression assemblepretty self prettysubexself first self getop self prettysubexself second if self consequent drs drtbinaryexpression assemblepretty drs drttokens imp self consequent pretty return drs def prettysubexself subex if isinstancesubex drtconcatenation return line1 1 for line in subex pretty return drtbooleanexpression prettysubexself subex def visitself function combinator see abstractexpression getrefs return self function getrefstrue self argument getrefstrue if recursive else def prettyself function args self uncurry functionlines function pretty argslines arg pretty for arg in args maxlines maxmaplen functionlines argslines functionlines padverticallyfunctionlines maxlines argslines padverticallyarglines maxlines for arglines in argslines funcargslines listzipfunctionlines listzipargslines return funcline joinargsline for funcline argsline in funcargslines 2 funcline joinargsline for funcline argsline in funcargslines2 3 funcline joinargsline for funcline argsline in funcargslines3 def padverticallylines maxlines padline lenlines0 return lines padline maxlines lenlines class possibleantecedentslist drtexpression expression def freeself replace all instances of variable v with expression e in self where v is free in self result possibleantecedents for item in self if item variable self appendexpression else self appenditem return result def prettyself s s self blank lens return blank blank s def strself return joins it for it in self class anaphoraresolutionexceptionexception pass def resolveanaphoraexpression trail if isinstanceexpression applicationexpression if expression ispronounfunction possibleantecedents possibleantecedents for ancestor in trail for ref in ancestor getrefs refex expression makevariableexpressionref don t allow resolution to itself or other types if refex class expression argument class and not refex expression argument possibleantecedents appendrefex if lenpossibleantecedents 1 resolution possibleantecedents0 else resolution possibleantecedents return expression makeequalityexpressionexpression argument resolution else rfunction resolveanaphoraexpression function trail expression rargument resolveanaphoraexpression argument trail expression return expression classrfunction rargument elif isinstanceexpression drs rconds for cond in expression conds rcond resolveanaphoracond trail expression if the condition is of the form x then raise exception if isinstancercond equalityexpression if isinstancercond first possibleantecedents reverse the order so that the variable is on the left temp rcond first rcond first rcond second rcond second temp if isinstancercond second possibleantecedents if not rcond second raise anaphoraresolutionexception variable s does not resolve to anything rcond first rconds appendrcond if expression consequent consequent resolveanaphoraexpression consequent trail expression else consequent none return expression classexpression refs rconds consequent elif isinstanceexpression abstractvariableexpression return expression elif isinstanceexpression negatedexpression return expression class resolveanaphoraexpression term trail expression elif isinstanceexpression drtconcatenation if expression consequent consequent resolveanaphoraexpression consequent trail expression else consequent none return expression class resolveanaphoraexpression first trail expression resolveanaphoraexpression second trail expression consequent elif isinstanceexpression binaryexpression return expression class resolveanaphoraexpression first trail expression resolveanaphoraexpression second trail expression elif isinstanceexpression lambdaexpression return expression class expression variable resolveanaphoraexpression term trail expression class drsdrawer buffer 3 space between elements topspace 10 space above whole drs outerspace 6 space to the left right and bottom of the while drs def initself drs sizecanvastrue canvasnone master none if not canvas master tk master titledrt font fontfamilyhelvetica size12 if sizecanvas canvas canvasmaster width0 height0 canvas font font self canvas canvas right bottom self visitdrs self outerspace self topspace width maxright self outerspace 100 height bottom self outerspace canvas canvasmaster widthwidth heightheight bg white else canvas canvasmaster width300 height300 canvas pack canvas font font self canvas canvas self drs drs self master master def gettextheightself draw the drs self handleself drs self drawcommand x y if self master and not inidle self master mainloop else return self visitself drs x y def visitself expression x y return self handleexpression self visitcommand x y def drawcommandself item x y if isinstanceitem str self canvas createtextx y anchornw fontself canvas font textitem elif isinstanceitem tuple item is the lowerright of a box right bottom item self canvas createrectanglex y right bottom horizliney y self gettextheight self buffer 2 the line separating refs from conds self canvas createlinex horizliney right horizliney return self visitcommanditem x y def visitcommandself item x y if isinstanceitem str return x self canvas font measureitem y self gettextheight elif isinstanceitem tuple return item def handleself expression command x0 y0 if command self visitcommand if we don t need to draw the item then we can use the cached values try attempt to retrieve cached values right expression drawingwidth x bottom expression drawingheight y return right bottom except attributeerror the values have not been cached yet so compute them pass if isinstanceexpression drtabstractvariableexpression factory self handlevariableexpression elif isinstanceexpression drs factory self handledrs elif isinstanceexpression drtnegatedexpression factory self handlenegatedexpression elif isinstanceexpression drtlambdaexpression factory self handlelambdaexpression elif isinstanceexpression binaryexpression factory self handlebinaryexpression elif isinstanceexpression drtapplicationexpression factory self handleapplicationexpression elif isinstanceexpression possibleantecedents factory self handlevariableexpression elif isinstanceexpression drtproposition factory self handledrtproposition else raise exceptionexpression class name right bottom factoryexpression command x y cache the values expression drawingwidth right x expression drawingheight bottom y return right bottom def handlevariableexpressionself expression command x y return commands expression x y def handlenegatedexpressionself expression command x y find the width of the negation symbol right self visitcommanddrttokens not x y0 handle term right bottom self handleexpression term command right y handle variables now that we know the ycoordinate command drttokens not x self getcenteredtopy bottom y self gettextheight return right bottom def handledrsself expression command x y left x self buffer indent the left side bottom y self buffer indent the top handle discourse referents if expression refs refs joins r for r in expression refs else refs maxright bottom commandrefs left bottom bottom self buffer 2 handle conditions if expression conds for cond in expression conds right bottom self handlecond command left bottom maxright maxmaxright right bottom self buffer else bottom self gettextheight self buffer handle box maxright self buffer return commandmaxright bottom x y def handleapplicationexpressionself expression command x y function args expression uncurry if not isinstancefunction drtabstractvariableexpression it s not a predicate expression px y so leave arguments curried function expression function args expression argument get the max bottom of any element on the line functionbottom self visitfunction x y1 maxbottom max functionbottom self visitarg x y1 for arg in args lineheight maxbottom y handle function functiondrawingtop self getcenteredtop y lineheight function drawingheight right self handlefunction command x functiondrawingtop0 handle open paren centredstringtop self getcenteredtop y lineheight self gettextheight right commanddrttokens open right centredstringtop0 handle each arg for i arg in enumerateargs argdrawingtop self getcenteredtop y lineheight arg drawingheight right self handlearg command right argdrawingtop0 if i 1 lenargs since it s not the last arg add a comma right commanddrttokens comma right centredstringtop0 handle close paren right commanddrttokens close right centredstringtop0 return right maxbottom def handlelambdaexpressionself expression command x y find the width of the lambda symbol and abstracted variables variables drttokens lambda s expression variable drttokens dot right self visitcommandvariables x y0 handle term right bottom self handleexpression term command right y handle variables now that we know the ycoordinate command variables x self getcenteredtopy bottom y self gettextheight return right bottom def handlebinaryexpressionself expression command x y get the full height of the line based on the operands firstheight self visitexpression first 0 01 secondheight self visitexpression second 0 01 lineheight maxfirstheight secondheight handle open paren centredstringtop self getcenteredtop y lineheight self gettextheight right commanddrttokens open x centredstringtop0 handle the first operand firstheight expression first drawingheight right firstbottom self handle expression first command right self getcenteredtopy lineheight firstheight handle the operator right command s expression getop right centredstringtop0 handle the second operand secondheight expression second drawingheight right secondbottom self handle expression second command right self getcenteredtopy lineheight secondheight handle close paren right commanddrttokens close right centredstringtop0 return right maxfirstbottom secondbottom def handledrtpropositionself expression command x y find the width of the negation symbol right commandexpression variable x y0 handle term right bottom self handleexpression term command right y return right bottom def getcenteredtopself top fullheight itemheight natural language toolkit discourse representation theory drt dan garrette dhgarrette gmail com c 2001 2023 nltk project url https www nltk org for license information see license txt import tkinter based modules if they are available no need to print a warning here nltk draw has already printed one a lambda calculus expression parser this method exists to be overridden this method is intended to be overridden for logics that use different operators or expressions a drs if there is a comma it s optional swallow the comma support expressions like drs x y c drs x y c swallow the comma support expressions like drs x y c drs x y c swallow the comma this method serves as a hook for other logic parsers that have different equality expression classes this method serves as a hook for other logic parsers that have different boolean operators this is the base abstract drt expression from which every drt expression extends check for logical equivalence pass the expression self other to the theorem prover if the prover says it is valid then the self and other are equal param other an drtexpression to check equality against param prover a nltk inference api prover return the set of discourse referents in this drs param recursive bool also find discourse referents in subterms return list of variable objects is self of the form pro x draw the drs return the pretty print string a discourse representation structure param refs list of drtindividualvariableexpression for the discourse referents param conds list of expression for the conditions replace all instances of variable v with expression e in self where v is free in self if a bound variable is the thing being replaced any bound variable that appears in the expression must be alpha converted to avoid a conflict replace in the conditions see expression free see abstractexpression get_refs see expression visit see expression visit_structured defines equality modulo alphabetic variance if we are comparing x m and y n then check equality of m and n x y map str self conds this is a factory method that instantiates and returns a subtype of drtabstractvariableexpression appropriate for the given variable see abstractexpression get_refs see expression visit see expression visit_structured see abstractexpression get_refs rename all occurrences of the variable introduced by this variable binder in the expression to newvar param newvar variable for the new variable see abstractexpression get_refs see abstractexpression get_refs drs of the form drs drs replace all instances of variable v with expression e in self where v is free in self if variable is bound alpha convert every ref that is free in expression todo at some point for now simplify for any ref that is in both first and second alpha convert the ref in second to prevent collision see abstractexpression get_refs defines equality modulo alphabetic variance if we are comparing x m and y n then check equality of m and n x y see expression visit see abstractexpression get_refs set of free variables replace all instances of variable v with expression e in self where v is free in self don t allow resolution to itself or other types if the condition is of the form x then raise exception reverse the order so that the variable is on the left space between elements space above whole drs space to the left right and bottom of the while drs param drs drtexpression the drs to be drawn param size_canvas bool true if the canvas size should be the exact size of the drs param canvas canvas the canvas on which to draw the drs if none is given create a new canvas bg white get the height of a line of text draw the drs return the bottom rightmost point without actually drawing the item param expression the item to visit param x the top of the current drawing area param y the left side of the current drawing area return the bottom rightmost point draw the given item at the given location param item the item to draw param x the top of the current drawing area param y the left side of the current drawing area return the bottom rightmost point item is the lower right of a box the line separating refs from conds return the bottom rightmost point without actually drawing the item param item the item to visit param x the top of the current drawing area param y the left side of the current drawing area return the bottom rightmost point param expression the expression to handle param command the function to apply either _draw_command or _visit_command param x the top of the current drawing area param y the left side of the current drawing area return the bottom rightmost point if we don t need to draw the item then we can use the cached values attempt to retrieve cached values the values have not been cached yet so compute them cache the values find the width of the negation symbol handle term handle variables now that we know the y coordinate indent the left side indent the top handle discourse referents handle conditions handle box it s not a predicate expression p x y so leave arguments curried get the max bottom of any element on the line handle function handle open paren handle each arg since it s not the last arg add a comma handle close paren find the width of the lambda symbol and abstracted variables handle term handle variables now that we know the y coordinate get the full height of the line based on the operands handle open paren handle the first operand handle the operator handle the second operand handle close paren find the width of the negation symbol handle term get the y coordinate of the point that a figure should start at if its height is item_height and it needs to be centered in an area that starts at top and is full_height tall
import operator
from functools import reduce
from itertools import chain

from nltk.sem.logic import (
    APP,
    AbstractVariableExpression,
    AllExpression,
    AndExpression,
    ApplicationExpression,
    BinaryExpression,
    BooleanExpression,
    ConstantExpression,
    EqualityExpression,
    EventVariableExpression,
    ExistsExpression,
    Expression,
    FunctionVariableExpression,
    ImpExpression,
    IndividualVariableExpression,
    LambdaExpression,
    LogicParser,
    NegatedExpression,
    OrExpression,
    Tokens,
    Variable,
    is_eventvar,
    is_funcvar,
    is_indvar,
    unique_variable,
)


try:
    from tkinter import Canvas, Tk
    from tkinter.font import Font

    from nltk.util import in_idle

except ImportError:
    
    pass


class DrtTokens(Tokens):
    DRS = "DRS"
    DRS_CONC = "+"
    PRONOUN = "PRO"
    OPEN_BRACKET = "["
    CLOSE_BRACKET = "]"
    COLON = ":"

    PUNCT = [DRS_CONC, OPEN_BRACKET, CLOSE_BRACKET, COLON]

    SYMBOLS = Tokens.SYMBOLS + PUNCT

    TOKENS = Tokens.TOKENS + [DRS] + PUNCT


class DrtParser(LogicParser):
    

    def __init__(self):
        LogicParser.__init__(self)

        self.operator_precedence = dict(
            [(x, 1) for x in DrtTokens.LAMBDA_LIST]
            + [(x, 2) for x in DrtTokens.NOT_LIST]
            + [(APP, 3)]
            + [(x, 4) for x in DrtTokens.EQ_LIST + Tokens.NEQ_LIST]
            + [(DrtTokens.COLON, 5)]
            + [(DrtTokens.DRS_CONC, 6)]
            + [(x, 7) for x in DrtTokens.OR_LIST]
            + [(x, 8) for x in DrtTokens.IMP_LIST]
            + [(None, 9)]
        )

    def get_all_symbols(self):
        
        return DrtTokens.SYMBOLS

    def isvariable(self, tok):
        return tok not in DrtTokens.TOKENS

    def handle(self, tok, context):
        
        if tok in DrtTokens.NOT_LIST:
            return self.handle_negation(tok, context)

        elif tok in DrtTokens.LAMBDA_LIST:
            return self.handle_lambda(tok, context)

        elif tok == DrtTokens.OPEN:
            if self.inRange(0) and self.token(0) == DrtTokens.OPEN_BRACKET:
                return self.handle_DRS(tok, context)
            else:
                return self.handle_open(tok, context)

        elif tok.upper() == DrtTokens.DRS:
            self.assertNextToken(DrtTokens.OPEN)
            return self.handle_DRS(tok, context)

        elif self.isvariable(tok):
            if self.inRange(0) and self.token(0) == DrtTokens.COLON:
                return self.handle_prop(tok, context)
            else:
                return self.handle_variable(tok, context)

    def make_NegatedExpression(self, expression):
        return DrtNegatedExpression(expression)

    def handle_DRS(self, tok, context):
        
        refs = self.handle_refs()
        if (
            self.inRange(0) and self.token(0) == DrtTokens.COMMA
        ):  
            self.token()  
        conds = self.handle_conds(context)
        self.assertNextToken(DrtTokens.CLOSE)
        return DRS(refs, conds, None)

    def handle_refs(self):
        self.assertNextToken(DrtTokens.OPEN_BRACKET)
        refs = []
        while self.inRange(0) and self.token(0) != DrtTokens.CLOSE_BRACKET:
            
            if refs and self.token(0) == DrtTokens.COMMA:
                self.token()  
            refs.append(self.get_next_token_variable("quantified"))
        self.assertNextToken(DrtTokens.CLOSE_BRACKET)
        return refs

    def handle_conds(self, context):
        self.assertNextToken(DrtTokens.OPEN_BRACKET)
        conds = []
        while self.inRange(0) and self.token(0) != DrtTokens.CLOSE_BRACKET:
            
            if conds and self.token(0) == DrtTokens.COMMA:
                self.token()  
            conds.append(self.process_next_expression(context))
        self.assertNextToken(DrtTokens.CLOSE_BRACKET)
        return conds

    def handle_prop(self, tok, context):
        variable = self.make_VariableExpression(tok)
        self.assertNextToken(":")
        drs = self.process_next_expression(DrtTokens.COLON)
        return DrtProposition(variable, drs)

    def make_EqualityExpression(self, first, second):
        
        return DrtEqualityExpression(first, second)

    def get_BooleanExpression_factory(self, tok):
        
        if tok == DrtTokens.DRS_CONC:
            return lambda first, second: DrtConcatenation(first, second, None)
        elif tok in DrtTokens.OR_LIST:
            return DrtOrExpression
        elif tok in DrtTokens.IMP_LIST:

            def make_imp_expression(first, second):
                if isinstance(first, DRS):
                    return DRS(first.refs, first.conds, second)
                if isinstance(first, DrtConcatenation):
                    return DrtConcatenation(first.first, first.second, second)
                raise Exception("Antecedent of implication must be a DRS")

            return make_imp_expression
        else:
            return None

    def make_BooleanExpression(self, factory, first, second):
        return factory(first, second)

    def make_ApplicationExpression(self, function, argument):
        return DrtApplicationExpression(function, argument)

    def make_VariableExpression(self, name):
        return DrtVariableExpression(Variable(name))

    def make_LambdaExpression(self, variables, term):
        return DrtLambdaExpression(variables, term)


class DrtExpression:
    

    _drt_parser = DrtParser()

    @classmethod
    def fromstring(cls, s):
        return cls._drt_parser.parse(s)

    def applyto(self, other):
        return DrtApplicationExpression(self, other)

    def __neg__(self):
        return DrtNegatedExpression(self)

    def __and__(self, other):
        return NotImplemented

    def __or__(self, other):
        assert isinstance(other, DrtExpression)
        return DrtOrExpression(self, other)

    def __gt__(self, other):
        assert isinstance(other, DrtExpression)
        if isinstance(self, DRS):
            return DRS(self.refs, self.conds, other)
        if isinstance(self, DrtConcatenation):
            return DrtConcatenation(self.first, self.second, other)
        raise Exception("Antecedent of implication must be a DRS")

    def equiv(self, other, prover=None):
        
        assert isinstance(other, DrtExpression)

        f1 = self.simplify().fol()
        f2 = other.simplify().fol()
        return f1.equiv(f2, prover)

    @property
    def type(self):
        raise AttributeError(
            "'%s' object has no attribute 'type'" % self.__class__.__name__
        )

    def typecheck(self, signature=None):
        raise NotImplementedError()

    def __add__(self, other):
        return DrtConcatenation(self, other, None)

    def get_refs(self, recursive=False):
        
        raise NotImplementedError()

    def is_pronoun_function(self):
        
        return (
            isinstance(self, DrtApplicationExpression)
            and isinstance(self.function, DrtAbstractVariableExpression)
            and self.function.variable.name == DrtTokens.PRONOUN
            and isinstance(self.argument, DrtIndividualVariableExpression)
        )

    def make_EqualityExpression(self, first, second):
        return DrtEqualityExpression(first, second)

    def make_VariableExpression(self, variable):
        return DrtVariableExpression(variable)

    def resolve_anaphora(self):
        return resolve_anaphora(self)

    def eliminate_equality(self):
        return self.visit_structured(lambda e: e.eliminate_equality(), self.__class__)

    def pretty_format(self):
        
        return "\n".join(self._pretty())

    def pretty_print(self):
        print(self.pretty_format())

    def draw(self):
        DrsDrawer(self).draw()


class DRS(DrtExpression, Expression):
    

    def __init__(self, refs, conds, consequent=None):
        
        self.refs = refs
        self.conds = conds
        self.consequent = consequent

    def replace(self, variable, expression, replace_bound=False, alpha_convert=True):
        
        if variable in self.refs:
            
            if not replace_bound:
                return self
            else:
                i = self.refs.index(variable)
                if self.consequent:
                    consequent = self.consequent.replace(
                        variable, expression, True, alpha_convert
                    )
                else:
                    consequent = None
                return DRS(
                    self.refs[:i] + [expression.variable] + self.refs[i + 1 :],
                    [
                        cond.replace(variable, expression, True, alpha_convert)
                        for cond in self.conds
                    ],
                    consequent,
                )
        else:
            if alpha_convert:
                
                
                for ref in set(self.refs) & expression.free():
                    newvar = unique_variable(ref)
                    newvarex = DrtVariableExpression(newvar)
                    i = self.refs.index(ref)
                    if self.consequent:
                        consequent = self.consequent.replace(
                            ref, newvarex, True, alpha_convert
                        )
                    else:
                        consequent = None
                    self = DRS(
                        self.refs[:i] + [newvar] + self.refs[i + 1 :],
                        [
                            cond.replace(ref, newvarex, True, alpha_convert)
                            for cond in self.conds
                        ],
                        consequent,
                    )

            
            if self.consequent:
                consequent = self.consequent.replace(
                    variable, expression, replace_bound, alpha_convert
                )
            else:
                consequent = None
            return DRS(
                self.refs,
                [
                    cond.replace(variable, expression, replace_bound, alpha_convert)
                    for cond in self.conds
                ],
                consequent,
            )

    def free(self):
        
        conds_free = reduce(operator.or_, [c.free() for c in self.conds], set())
        if self.consequent:
            conds_free.update(self.consequent.free())
        return conds_free - set(self.refs)

    def get_refs(self, recursive=False):
        
        if recursive:
            conds_refs = self.refs + list(
                chain.from_iterable(c.get_refs(True) for c in self.conds)
            )
            if self.consequent:
                conds_refs.extend(self.consequent.get_refs(True))
            return conds_refs
        else:
            return self.refs

    def visit(self, function, combinator):
        
        parts = list(map(function, self.conds))
        if self.consequent:
            parts.append(function(self.consequent))
        return combinator(parts)

    def visit_structured(self, function, combinator):
        
        consequent = function(self.consequent) if self.consequent else None
        return combinator(self.refs, list(map(function, self.conds)), consequent)

    def eliminate_equality(self):
        drs = self
        i = 0
        while i < len(drs.conds):
            cond = drs.conds[i]
            if (
                isinstance(cond, EqualityExpression)
                and isinstance(cond.first, AbstractVariableExpression)
                and isinstance(cond.second, AbstractVariableExpression)
            ):
                drs = DRS(
                    list(set(drs.refs) - {cond.second.variable}),
                    drs.conds[:i] + drs.conds[i + 1 :],
                    drs.consequent,
                )
                if cond.second.variable != cond.first.variable:
                    drs = drs.replace(cond.second.variable, cond.first, False, False)
                    i = 0
                i -= 1
            i += 1

        conds = []
        for cond in drs.conds:
            new_cond = cond.eliminate_equality()
            new_cond_simp = new_cond.simplify()
            if (
                not isinstance(new_cond_simp, DRS)
                or new_cond_simp.refs
                or new_cond_simp.conds
                or new_cond_simp.consequent
            ):
                conds.append(new_cond)

        consequent = drs.consequent.eliminate_equality() if drs.consequent else None
        return DRS(drs.refs, conds, consequent)

    def fol(self):
        if self.consequent:
            accum = None
            if self.conds:
                accum = reduce(AndExpression, [c.fol() for c in self.conds])

            if accum:
                accum = ImpExpression(accum, self.consequent.fol())
            else:
                accum = self.consequent.fol()

            for ref in self.refs[::-1]:
                accum = AllExpression(ref, accum)

            return accum

        else:
            if not self.conds:
                raise Exception("Cannot convert DRS with no conditions to FOL.")
            accum = reduce(AndExpression, [c.fol() for c in self.conds])
            for ref in map(Variable, self._order_ref_strings(self.refs)[::-1]):
                accum = ExistsExpression(ref, accum)
            return accum

    def _pretty(self):
        refs_line = " ".join(self._order_ref_strings(self.refs))

        cond_lines = [
            cond
            for cond_line in [
                filter(lambda s: s.strip(), cond._pretty()) for cond in self.conds
            ]
            for cond in cond_line
        ]
        length = max([len(refs_line)] + list(map(len, cond_lines)))
        drs = (
            [
                " _" + "_" * length + "_ ",
                "| " + refs_line.ljust(length) + " |",
                "|-" + "-" * length + "-|",
            ]
            + ["| " + line.ljust(length) + " |" for line in cond_lines]
            + ["|_" + "_" * length + "_|"]
        )
        if self.consequent:
            return DrtBinaryExpression._assemble_pretty(
                drs, DrtTokens.IMP, self.consequent._pretty()
            )
        return drs

    def _order_ref_strings(self, refs):
        strings = ["%s" % ref for ref in refs]
        ind_vars = []
        func_vars = []
        event_vars = []
        other_vars = []
        for s in strings:
            if is_indvar(s):
                ind_vars.append(s)
            elif is_funcvar(s):
                func_vars.append(s)
            elif is_eventvar(s):
                event_vars.append(s)
            else:
                other_vars.append(s)
        return (
            sorted(other_vars)
            + sorted(event_vars, key=lambda v: int([v[2:], -1][len(v[2:]) == 0]))
            + sorted(func_vars, key=lambda v: (v[0], int([v[1:], -1][len(v[1:]) == 0])))
            + sorted(ind_vars, key=lambda v: (v[0], int([v[1:], -1][len(v[1:]) == 0])))
        )

    def __eq__(self, other):
        r
        if isinstance(other, DRS):
            if len(self.refs) == len(other.refs):
                converted_other = other
                for (r1, r2) in zip(self.refs, converted_other.refs):
                    varex = self.make_VariableExpression(r1)
                    converted_other = converted_other.replace(r2, varex, True)
                if self.consequent == converted_other.consequent and len(
                    self.conds
                ) == len(converted_other.conds):
                    for c1, c2 in zip(self.conds, converted_other.conds):
                        if not (c1 == c2):
                            return False
                    return True
        return False

    def __ne__(self, other):
        return not self == other

    __hash__ = Expression.__hash__

    def __str__(self):
        drs = "([{}],[{}])".format(
            ",".join(self._order_ref_strings(self.refs)),
            ", ".join("%s" % cond for cond in self.conds),
        )  
        if self.consequent:
            return (
                DrtTokens.OPEN
                + drs
                + " "
                + DrtTokens.IMP
                + " "
                + "%s" % self.consequent
                + DrtTokens.CLOSE
            )
        return drs


def DrtVariableExpression(variable):
    
    if is_indvar(variable.name):
        return DrtIndividualVariableExpression(variable)
    elif is_funcvar(variable.name):
        return DrtFunctionVariableExpression(variable)
    elif is_eventvar(variable.name):
        return DrtEventVariableExpression(variable)
    else:
        return DrtConstantExpression(variable)


class DrtAbstractVariableExpression(DrtExpression, AbstractVariableExpression):
    def fol(self):
        return self

    def get_refs(self, recursive=False):
        
        return []

    def _pretty(self):
        s = "%s" % self
        blank = " " * len(s)
        return [blank, blank, s, blank]

    def eliminate_equality(self):
        return self


class DrtIndividualVariableExpression(
    DrtAbstractVariableExpression, IndividualVariableExpression
):
    pass


class DrtFunctionVariableExpression(
    DrtAbstractVariableExpression, FunctionVariableExpression
):
    pass


class DrtEventVariableExpression(
    DrtIndividualVariableExpression, EventVariableExpression
):
    pass


class DrtConstantExpression(DrtAbstractVariableExpression, ConstantExpression):
    pass


class DrtProposition(DrtExpression, Expression):
    def __init__(self, variable, drs):
        self.variable = variable
        self.drs = drs

    def replace(self, variable, expression, replace_bound=False, alpha_convert=True):
        if self.variable == variable:
            assert isinstance(
                expression, DrtAbstractVariableExpression
            ), "Can only replace a proposition label with a variable"
            return DrtProposition(
                expression.variable,
                self.drs.replace(variable, expression, replace_bound, alpha_convert),
            )
        else:
            return DrtProposition(
                self.variable,
                self.drs.replace(variable, expression, replace_bound, alpha_convert),
            )

    def eliminate_equality(self):
        return DrtProposition(self.variable, self.drs.eliminate_equality())

    def get_refs(self, recursive=False):
        return self.drs.get_refs(True) if recursive else []

    def __eq__(self, other):
        return (
            self.__class__ == other.__class__
            and self.variable == other.variable
            and self.drs == other.drs
        )

    def __ne__(self, other):
        return not self == other

    __hash__ = Expression.__hash__

    def fol(self):
        return self.drs.fol()

    def _pretty(self):
        drs_s = self.drs._pretty()
        blank = " " * len("%s" % self.variable)
        return (
            [blank + " " + line for line in drs_s[:1]]
            + ["%s" % self.variable + ":" + line for line in drs_s[1:2]]
            + [blank + " " + line for line in drs_s[2:]]
        )

    def visit(self, function, combinator):
        
        return combinator([function(self.drs)])

    def visit_structured(self, function, combinator):
        
        return combinator(self.variable, function(self.drs))

    def __str__(self):
        return f"prop({self.variable}, {self.drs})"


class DrtNegatedExpression(DrtExpression, NegatedExpression):
    def fol(self):
        return NegatedExpression(self.term.fol())

    def get_refs(self, recursive=False):
        
        return self.term.get_refs(recursive)

    def _pretty(self):
        term_lines = self.term._pretty()
        return (
            ["    " + line for line in term_lines[:2]]
            + ["__  " + line for line in term_lines[2:3]]
            + ["  | " + line for line in term_lines[3:4]]
            + ["    " + line for line in term_lines[4:]]
        )


class DrtLambdaExpression(DrtExpression, LambdaExpression):
    def alpha_convert(self, newvar):
        
        return self.__class__(
            newvar,
            self.term.replace(self.variable, DrtVariableExpression(newvar), True),
        )

    def fol(self):
        return LambdaExpression(self.variable, self.term.fol())

    def _pretty(self):
        variables = [self.variable]
        term = self.term
        while term.__class__ == self.__class__:
            variables.append(term.variable)
            term = term.term
        var_string = " ".join("%s" % v for v in variables) + DrtTokens.DOT
        term_lines = term._pretty()
        blank = " " * len(var_string)
        return (
            ["    " + blank + line for line in term_lines[:1]]
            + [r" \  " + blank + line for line in term_lines[1:2]]
            + [r" /\ " + var_string + line for line in term_lines[2:3]]
            + ["    " + blank + line for line in term_lines[3:]]
        )

    def get_refs(self, recursive=False):
        
        return (
            [self.variable] + self.term.get_refs(True) if recursive else [self.variable]
        )


class DrtBinaryExpression(DrtExpression, BinaryExpression):
    def get_refs(self, recursive=False):
        
        return (
            self.first.get_refs(True) + self.second.get_refs(True) if recursive else []
        )

    def _pretty(self):
        return DrtBinaryExpression._assemble_pretty(
            self._pretty_subex(self.first),
            self.getOp(),
            self._pretty_subex(self.second),
        )

    @staticmethod
    def _assemble_pretty(first_lines, op, second_lines):
        max_lines = max(len(first_lines), len(second_lines))
        first_lines = _pad_vertically(first_lines, max_lines)
        second_lines = _pad_vertically(second_lines, max_lines)
        blank = " " * len(op)
        first_second_lines = list(zip(first_lines, second_lines))
        return (
            [
                " " + first_line + " " + blank + " " + second_line + " "
                for first_line, second_line in first_second_lines[:2]
            ]
            + [
                "(" + first_line + " " + op + " " + second_line + ")"
                for first_line, second_line in first_second_lines[2:3]
            ]
            + [
                " " + first_line + " " + blank + " " + second_line + " "
                for first_line, second_line in first_second_lines[3:]
            ]
        )

    def _pretty_subex(self, subex):
        return subex._pretty()


class DrtBooleanExpression(DrtBinaryExpression, BooleanExpression):
    pass


class DrtOrExpression(DrtBooleanExpression, OrExpression):
    def fol(self):
        return OrExpression(self.first.fol(), self.second.fol())

    def _pretty_subex(self, subex):
        if isinstance(subex, DrtOrExpression):
            return [line[1:-1] for line in subex._pretty()]
        return DrtBooleanExpression._pretty_subex(self, subex)


class DrtEqualityExpression(DrtBinaryExpression, EqualityExpression):
    def fol(self):
        return EqualityExpression(self.first.fol(), self.second.fol())


class DrtConcatenation(DrtBooleanExpression):
    

    def __init__(self, first, second, consequent=None):
        DrtBooleanExpression.__init__(self, first, second)
        self.consequent = consequent

    def replace(self, variable, expression, replace_bound=False, alpha_convert=True):
        
        first = self.first
        second = self.second
        consequent = self.consequent

        
        if variable in self.get_refs():
            if replace_bound:
                first = first.replace(
                    variable, expression, replace_bound, alpha_convert
                )
                second = second.replace(
                    variable, expression, replace_bound, alpha_convert
                )
                if consequent:
                    consequent = consequent.replace(
                        variable, expression, replace_bound, alpha_convert
                    )
        else:
            if alpha_convert:
                
                for ref in set(self.get_refs(True)) & expression.free():
                    v = DrtVariableExpression(unique_variable(ref))
                    first = first.replace(ref, v, True, alpha_convert)
                    second = second.replace(ref, v, True, alpha_convert)
                    if consequent:
                        consequent = consequent.replace(ref, v, True, alpha_convert)

            first = first.replace(variable, expression, replace_bound, alpha_convert)
            second = second.replace(variable, expression, replace_bound, alpha_convert)
            if consequent:
                consequent = consequent.replace(
                    variable, expression, replace_bound, alpha_convert
                )

        return self.__class__(first, second, consequent)

    def eliminate_equality(self):
        
        drs = self.simplify()
        assert not isinstance(drs, DrtConcatenation)
        return drs.eliminate_equality()

    def simplify(self):
        first = self.first.simplify()
        second = self.second.simplify()
        consequent = self.consequent.simplify() if self.consequent else None

        if isinstance(first, DRS) and isinstance(second, DRS):
            
            for ref in set(first.get_refs(True)) & set(second.get_refs(True)):
                
                newvar = DrtVariableExpression(unique_variable(ref))
                second = second.replace(ref, newvar, True)

            return DRS(first.refs + second.refs, first.conds + second.conds, consequent)
        else:
            return self.__class__(first, second, consequent)

    def get_refs(self, recursive=False):
        
        refs = self.first.get_refs(recursive) + self.second.get_refs(recursive)
        if self.consequent and recursive:
            refs.extend(self.consequent.get_refs(True))
        return refs

    def getOp(self):
        return DrtTokens.DRS_CONC

    def __eq__(self, other):
        r
        if isinstance(other, DrtConcatenation):
            self_refs = self.get_refs()
            other_refs = other.get_refs()
            if len(self_refs) == len(other_refs):
                converted_other = other
                for (r1, r2) in zip(self_refs, other_refs):
                    varex = self.make_VariableExpression(r1)
                    converted_other = converted_other.replace(r2, varex, True)
                return (
                    self.first == converted_other.first
                    and self.second == converted_other.second
                    and self.consequent == converted_other.consequent
                )
        return False

    def __ne__(self, other):
        return not self == other

    __hash__ = DrtBooleanExpression.__hash__

    def fol(self):
        e = AndExpression(self.first.fol(), self.second.fol())
        if self.consequent:
            e = ImpExpression(e, self.consequent.fol())
        return e

    def _pretty(self):
        drs = DrtBinaryExpression._assemble_pretty(
            self._pretty_subex(self.first),
            self.getOp(),
            self._pretty_subex(self.second),
        )
        if self.consequent:
            drs = DrtBinaryExpression._assemble_pretty(
                drs, DrtTokens.IMP, self.consequent._pretty()
            )
        return drs

    def _pretty_subex(self, subex):
        if isinstance(subex, DrtConcatenation):
            return [line[1:-1] for line in subex._pretty()]
        return DrtBooleanExpression._pretty_subex(self, subex)

    def visit(self, function, combinator):
        
        if self.consequent:
            return combinator(
                [function(self.first), function(self.second), function(self.consequent)]
            )
        else:
            return combinator([function(self.first), function(self.second)])

    def __str__(self):
        first = self._str_subex(self.first)
        second = self._str_subex(self.second)
        drs = Tokens.OPEN + first + " " + self.getOp() + " " + second + Tokens.CLOSE
        if self.consequent:
            return (
                DrtTokens.OPEN
                + drs
                + " "
                + DrtTokens.IMP
                + " "
                + "%s" % self.consequent
                + DrtTokens.CLOSE
            )
        return drs

    def _str_subex(self, subex):
        s = "%s" % subex
        if isinstance(subex, DrtConcatenation) and subex.consequent is None:
            return s[1:-1]
        return s


class DrtApplicationExpression(DrtExpression, ApplicationExpression):
    def fol(self):
        return ApplicationExpression(self.function.fol(), self.argument.fol())

    def get_refs(self, recursive=False):
        
        return (
            self.function.get_refs(True) + self.argument.get_refs(True)
            if recursive
            else []
        )

    def _pretty(self):
        function, args = self.uncurry()
        function_lines = function._pretty()
        args_lines = [arg._pretty() for arg in args]
        max_lines = max(map(len, [function_lines] + args_lines))
        function_lines = _pad_vertically(function_lines, max_lines)
        args_lines = [_pad_vertically(arg_lines, max_lines) for arg_lines in args_lines]
        func_args_lines = list(zip(function_lines, list(zip(*args_lines))))
        return (
            [
                func_line + " " + " ".join(args_line) + " "
                for func_line, args_line in func_args_lines[:2]
            ]
            + [
                func_line + "(" + ",".join(args_line) + ")"
                for func_line, args_line in func_args_lines[2:3]
            ]
            + [
                func_line + " " + " ".join(args_line) + " "
                for func_line, args_line in func_args_lines[3:]
            ]
        )


def _pad_vertically(lines, max_lines):
    pad_line = [" " * len(lines[0])]
    return lines + pad_line * (max_lines - len(lines))


class PossibleAntecedents(list, DrtExpression, Expression):
    def free(self):
        
        return set(self)

    def replace(self, variable, expression, replace_bound=False, alpha_convert=True):
        
        result = PossibleAntecedents()
        for item in self:
            if item == variable:
                self.append(expression)
            else:
                self.append(item)
        return result

    def _pretty(self):
        s = "%s" % self
        blank = " " * len(s)
        return [blank, blank, s]

    def __str__(self):
        return "[" + ",".join("%s" % it for it in self) + "]"


class AnaphoraResolutionException(Exception):
    pass


def resolve_anaphora(expression, trail=[]):
    if isinstance(expression, ApplicationExpression):
        if expression.is_pronoun_function():
            possible_antecedents = PossibleAntecedents()
            for ancestor in trail:
                for ref in ancestor.get_refs():
                    refex = expression.make_VariableExpression(ref)

                    
                    
                    
                    if refex.__class__ == expression.argument.__class__ and not (
                        refex == expression.argument
                    ):
                        possible_antecedents.append(refex)

            if len(possible_antecedents) == 1:
                resolution = possible_antecedents[0]
            else:
                resolution = possible_antecedents
            return expression.make_EqualityExpression(expression.argument, resolution)
        else:
            r_function = resolve_anaphora(expression.function, trail + [expression])
            r_argument = resolve_anaphora(expression.argument, trail + [expression])
            return expression.__class__(r_function, r_argument)

    elif isinstance(expression, DRS):
        r_conds = []
        for cond in expression.conds:
            r_cond = resolve_anaphora(cond, trail + [expression])

            
            if isinstance(r_cond, EqualityExpression):
                if isinstance(r_cond.first, PossibleAntecedents):
                    
                    temp = r_cond.first
                    r_cond.first = r_cond.second
                    r_cond.second = temp
                if isinstance(r_cond.second, PossibleAntecedents):
                    if not r_cond.second:
                        raise AnaphoraResolutionException(
                            "Variable '%s' does not "
                            "resolve to anything." % r_cond.first
                        )

            r_conds.append(r_cond)
        if expression.consequent:
            consequent = resolve_anaphora(expression.consequent, trail + [expression])
        else:
            consequent = None
        return expression.__class__(expression.refs, r_conds, consequent)

    elif isinstance(expression, AbstractVariableExpression):
        return expression

    elif isinstance(expression, NegatedExpression):
        return expression.__class__(
            resolve_anaphora(expression.term, trail + [expression])
        )

    elif isinstance(expression, DrtConcatenation):
        if expression.consequent:
            consequent = resolve_anaphora(expression.consequent, trail + [expression])
        else:
            consequent = None
        return expression.__class__(
            resolve_anaphora(expression.first, trail + [expression]),
            resolve_anaphora(expression.second, trail + [expression]),
            consequent,
        )

    elif isinstance(expression, BinaryExpression):
        return expression.__class__(
            resolve_anaphora(expression.first, trail + [expression]),
            resolve_anaphora(expression.second, trail + [expression]),
        )

    elif isinstance(expression, LambdaExpression):
        return expression.__class__(
            expression.variable, resolve_anaphora(expression.term, trail + [expression])
        )


class DrsDrawer:
    BUFFER = 3  
    TOPSPACE = 10  
    OUTERSPACE = 6  

    def __init__(self, drs, size_canvas=True, canvas=None):
        
        master = None
        if not canvas:
            master = Tk()
            master.title("DRT")

            font = Font(family="helvetica", size=12)

            if size_canvas:
                canvas = Canvas(master, width=0, height=0)
                canvas.font = font
                self.canvas = canvas
                (right, bottom) = self._visit(drs, self.OUTERSPACE, self.TOPSPACE)

                width = max(right + self.OUTERSPACE, 100)
                height = bottom + self.OUTERSPACE
                canvas = Canvas(master, width=width, height=height)  
            else:
                canvas = Canvas(master, width=300, height=300)

            canvas.pack()
            canvas.font = font

        self.canvas = canvas
        self.drs = drs
        self.master = master

    def _get_text_height(self):
        
        return self.canvas.font.metrics("linespace")

    def draw(self, x=OUTERSPACE, y=TOPSPACE):
        
        self._handle(self.drs, self._draw_command, x, y)

        if self.master and not in_idle():
            self.master.mainloop()
        else:
            return self._visit(self.drs, x, y)

    def _visit(self, expression, x, y):
        
        return self._handle(expression, self._visit_command, x, y)

    def _draw_command(self, item, x, y):
        
        if isinstance(item, str):
            self.canvas.create_text(x, y, anchor="nw", font=self.canvas.font, text=item)
        elif isinstance(item, tuple):
            
            (right, bottom) = item
            self.canvas.create_rectangle(x, y, right, bottom)
            horiz_line_y = (
                y + self._get_text_height() + (self.BUFFER * 2)
            )  
            self.canvas.create_line(x, horiz_line_y, right, horiz_line_y)

        return self._visit_command(item, x, y)

    def _visit_command(self, item, x, y):
        
        if isinstance(item, str):
            return (x + self.canvas.font.measure(item), y + self._get_text_height())
        elif isinstance(item, tuple):
            return item

    def _handle(self, expression, command, x=0, y=0):
        
        if command == self._visit_command:
            
            try:
                
                right = expression._drawing_width + x
                bottom = expression._drawing_height + y
                return (right, bottom)
            except AttributeError:
                
                pass

        if isinstance(expression, DrtAbstractVariableExpression):
            factory = self._handle_VariableExpression
        elif isinstance(expression, DRS):
            factory = self._handle_DRS
        elif isinstance(expression, DrtNegatedExpression):
            factory = self._handle_NegatedExpression
        elif isinstance(expression, DrtLambdaExpression):
            factory = self._handle_LambdaExpression
        elif isinstance(expression, BinaryExpression):
            factory = self._handle_BinaryExpression
        elif isinstance(expression, DrtApplicationExpression):
            factory = self._handle_ApplicationExpression
        elif isinstance(expression, PossibleAntecedents):
            factory = self._handle_VariableExpression
        elif isinstance(expression, DrtProposition):
            factory = self._handle_DrtProposition
        else:
            raise Exception(expression.__class__.__name__)

        (right, bottom) = factory(expression, command, x, y)

        
        expression._drawing_width = right - x
        expression._drawing_height = bottom - y

        return (right, bottom)

    def _handle_VariableExpression(self, expression, command, x, y):
        return command("%s" % expression, x, y)

    def _handle_NegatedExpression(self, expression, command, x, y):
        
        right = self._visit_command(DrtTokens.NOT, x, y)[0]

        
        (right, bottom) = self._handle(expression.term, command, right, y)

        
        command(
            DrtTokens.NOT,
            x,
            self._get_centered_top(y, bottom - y, self._get_text_height()),
        )

        return (right, bottom)

    def _handle_DRS(self, expression, command, x, y):
        left = x + self.BUFFER  
        bottom = y + self.BUFFER  

        
        if expression.refs:
            refs = " ".join("%s" % r for r in expression.refs)
        else:
            refs = "     "
        (max_right, bottom) = command(refs, left, bottom)
        bottom += self.BUFFER * 2

        
        if expression.conds:
            for cond in expression.conds:
                (right, bottom) = self._handle(cond, command, left, bottom)
                max_right = max(max_right, right)
                bottom += self.BUFFER
        else:
            bottom += self._get_text_height() + self.BUFFER

        
        max_right += self.BUFFER
        return command((max_right, bottom), x, y)

    def _handle_ApplicationExpression(self, expression, command, x, y):
        function, args = expression.uncurry()
        if not isinstance(function, DrtAbstractVariableExpression):
            
            function = expression.function
            args = [expression.argument]

        
        function_bottom = self._visit(function, x, y)[1]
        max_bottom = max(
            [function_bottom] + [self._visit(arg, x, y)[1] for arg in args]
        )

        line_height = max_bottom - y

        
        function_drawing_top = self._get_centered_top(
            y, line_height, function._drawing_height
        )
        right = self._handle(function, command, x, function_drawing_top)[0]

        
        centred_string_top = self._get_centered_top(
            y, line_height, self._get_text_height()
        )
        right = command(DrtTokens.OPEN, right, centred_string_top)[0]

        
        for (i, arg) in enumerate(args):
            arg_drawing_top = self._get_centered_top(
                y, line_height, arg._drawing_height
            )
            right = self._handle(arg, command, right, arg_drawing_top)[0]

            if i + 1 < len(args):
                
                right = command(DrtTokens.COMMA + " ", right, centred_string_top)[0]

        
        right = command(DrtTokens.CLOSE, right, centred_string_top)[0]

        return (right, max_bottom)

    def _handle_LambdaExpression(self, expression, command, x, y):
        
        variables = DrtTokens.LAMBDA + "%s" % expression.variable + DrtTokens.DOT
        right = self._visit_command(variables, x, y)[0]

        
        (right, bottom) = self._handle(expression.term, command, right, y)

        
        command(
            variables, x, self._get_centered_top(y, bottom - y, self._get_text_height())
        )

        return (right, bottom)

    def _handle_BinaryExpression(self, expression, command, x, y):
        
        first_height = self._visit(expression.first, 0, 0)[1]
        second_height = self._visit(expression.second, 0, 0)[1]
        line_height = max(first_height, second_height)

        
        centred_string_top = self._get_centered_top(
            y, line_height, self._get_text_height()
        )
        right = command(DrtTokens.OPEN, x, centred_string_top)[0]

        
        first_height = expression.first._drawing_height
        (right, first_bottom) = self._handle(
            expression.first,
            command,
            right,
            self._get_centered_top(y, line_height, first_height),
        )

        
        right = command(" %s " % expression.getOp(), right, centred_string_top)[0]

        
        second_height = expression.second._drawing_height
        (right, second_bottom) = self._handle(
            expression.second,
            command,
            right,
            self._get_centered_top(y, line_height, second_height),
        )

        
        right = command(DrtTokens.CLOSE, right, centred_string_top)[0]

        return (right, max(first_bottom, second_bottom))

    def _handle_DrtProposition(self, expression, command, x, y):
        
        right = command(expression.variable, x, y)[0]

        
        (right, bottom) = self._handle(expression.term, command, right, y)

        return (right, bottom)

    def _get_centered_top(self, top, full_height, item_height):
        
        return top + (full_height - item_height) / 2


def demo():
    print("=" * 20 + "TEST PARSE" + "=" * 20)
    dexpr = DrtExpression.fromstring
    print(dexpr(r"([x,y],[sees(x,y)])"))
    print(dexpr(r"([x],[man(x), walks(x)])"))
    print(dexpr(r"\x.\y.([],[sees(x,y)])"))
    print(dexpr(r"\x.([],[walks(x)])(john)"))
    print(dexpr(r"(([x],[walks(x)]) + ([y],[runs(y)]))"))
    print(dexpr(r"(([],[walks(x)]) -> ([],[runs(x)]))"))
    print(dexpr(r"([x],[PRO(x), sees(John,x)])"))
    print(dexpr(r"([x],[man(x), -([],[walks(x)])])"))
    print(dexpr(r"([],[(([x],[man(x)]) -> ([],[walks(x)]))])"))

    print("=" * 20 + "Test fol()" + "=" * 20)
    print(dexpr(r"([x,y],[sees(x,y)])").fol())

    print("=" * 20 + "Test alpha conversion and lambda expression equality" + "=" * 20)
    e1 = dexpr(r"\x.([],[P(x)])")
    print(e1)
    e2 = e1.alpha_convert(Variable("z"))
    print(e2)
    print(e1 == e2)

    print("=" * 20 + "Test resolve_anaphora()" + "=" * 20)
    print(resolve_anaphora(dexpr(r"([x,y,z],[dog(x), cat(y), walks(z), PRO(z)])")))
    print(
        resolve_anaphora(dexpr(r"([],[(([x],[dog(x)]) -> ([y],[walks(y), PRO(y)]))])"))
    )
    print(resolve_anaphora(dexpr(r"(([x,y],[]) + ([],[PRO(x)]))")))

    print("=" * 20 + "Test pretty_print()" + "=" * 20)
    dexpr(r"([],[])").pretty_print()
    dexpr(
        r"([],[([x],[big(x), dog(x)]) -> ([],[bark(x)]) -([x],[walk(x)])])"
    ).pretty_print()
    dexpr(r"([x,y],[x=y]) + ([z],[dog(z), walk(z)])").pretty_print()
    dexpr(r"([],[([x],[]) | ([y],[]) | ([z],[dog(z), walk(z)])])").pretty_print()
    dexpr(r"\P.\Q.(([x],[]) + P(x) + Q(x))(\x.([],[dog(x)]))").pretty_print()


def test_draw():
    try:
        from tkinter import Tk
    except ImportError as e:
        raise ValueError("tkinter is required, but it's not available.")

    expressions = [
        r"x",
        r"([],[])",
        r"([x],[])",
        r"([x],[man(x)])",
        r"([x,y],[sees(x,y)])",
        r"([x],[man(x), walks(x)])",
        r"\x.([],[man(x), walks(x)])",
        r"\x y.([],[sees(x,y)])",
        r"([],[(([],[walks(x)]) + ([],[runs(x)]))])",
        r"([x],[man(x), -([],[walks(x)])])",
        r"([],[(([x],[man(x)]) -> ([],[walks(x)]))])",
    ]

    for e in expressions:
        d = DrtExpression.fromstring(e)
        d.draw()


if __name__ == "__main__":
    demo()