.. Copyright (C) 2001-2012 NLTK Project
.. For license information, see LICENSE.TXT

================================
 Discourse Representation Theory
================================

    >>> from nltk.sem import logic
    >>> from nltk.inference import TableauProver

Overview
========

A DRS can be created with the ``DRS()`` constructor. This takes two arguments: a list of
discourse referents and list of conditions. .

    >>> from nltk.sem.drt import *
    >>> dp = DrtParser()
    >>> man_x = dp.parse('man(x)')
    >>> walk_x = dp.parse('walk(x)')
    >>> x = dp.parse('x')
    >>> print DRS([x], [man_x, walk_x])
    ([x],[man(x), walk(x)])

The ``parse()`` method can also be applied directly to DRS
expressions, which allows them to be specified more
easily.

    >>> drs1 = dp.parse('([x],[man(x),walk(x)])')
    >>> print drs1
    ([x],[man(x), walk(x)])

DRSs can be *merged* using the ``+`` operator.

    >>> drs2 = dp.parse('([y],[woman(y),stop(y)])')
    >>> drs3 = drs1 + drs2
    >>> print drs3
    (([x],[man(x), walk(x)]) + ([y],[woman(y), stop(y)]))
    >>> print drs3.simplify()
    ([x,y],[man(x), walk(x), woman(y), stop(y)])

We can embed DRSs as components of an ``implies`` condition.

    >>> s = '([], [(%s -> %s)])' % (drs1, drs2)
    >>> print dp.parse(s)
    ([],[(([x],[man(x), walk(x)]) -> ([y],[woman(y), stop(y)]))])

The ``fol()`` method converts DRSs into FOL formulae.

    >>> print dp.parse(r'([x],[man(x), walks(x)])').fol()
    exists x.(man(x) & walks(x))
    >>> print dp.parse(r'([],[(([x],[man(x)]) -> ([],[walks(x)]))])').fol()
    all x.(man(x) -> walks(x))

In order to visualize a DRS, the ``pprint()`` method can be use.

    >>> drs3.pprint()
      _________     __________  
     | x       |   | y        | 
    (|---------| + |----------|)
     | man(x)  |   | woman(y) | 
     | walk(x) |   | stop(y)  | 
     |_________|   |__________| 
    

Parse to semantics
------------------

..
    >>> logic._counter._value = 0

DRSs can be used for building compositional semantics in a feature
based grammar. To specify that we want to use DRSs, the appropriate
logic parser needs be passed as a parameter to ``load_earley()``

    >>> from nltk.parse import load_parser
    >>> parser = load_parser('grammars/book_grammars/drt.fcfg', trace=0, logic_parser=DrtParser())
    >>> trees = parser.nbest_parse('a dog barks'.split())
    >>> print trees[0].node['SEM'].simplify()
    ([x],[dog(x), bark(x)])

Alternatively, a ``FeatStructParser`` can be passed with the ``logic_parser`` set on it

    >>> from nltk.featstruct import FeatStructParser
    >>> from nltk.grammar import FeatStructNonterminal
    >>> parser = load_parser('grammars/book_grammars/drt.fcfg', trace=0, fstruct_parser=FeatStructParser(fdict_class=FeatStructNonterminal, logic_parser=DrtParser()))
    >>> trees = parser.nbest_parse('every girl chases a dog'.split())
    >>> print trees[0].node['SEM'].simplify()
    ([],[(([x],[girl(x)]) -> ([z2],[dog(z2), chase(x,z2)]))])



Unit Tests
==========

Parser
------
    
    >>> print dp.parse(r'([x,y],[sees(x,y)])')
    ([x,y],[sees(x,y)])
    >>> print dp.parse(r'([x],[man(x), walks(x)])')
    ([x],[man(x), walks(x)])
    >>> print dp.parse(r'\x.([],[man(x), walks(x)])')
    \x.([],[man(x), walks(x)])
    >>> print dp.parse(r'\x.\y.([],[sees(x,y)])')
    \x y.([],[sees(x,y)])

    >>> print dp.parse(r'([x,y],[(x = y)])')
    ([x,y],[(x = y)])
    >>> print dp.parse(r'([x,y],[(x != y)])')
    ([x,y],[-(x = y)])

    >>> print dp.parse(r'\x.([],[walks(x)])(john)')
    (\x.([],[walks(x)]))(john)
    >>> print dp.parse(r'\R.\x.([],[big(x,R)])(\y.([],[mouse(y)]))')
    (\R x.([],[big(x,R)]))(\y.([],[mouse(y)]))

    >>> print dp.parse(r'(([x],[walks(x)]) + ([y],[runs(y)]))')
    (([x],[walks(x)]) + ([y],[runs(y)]))
    >>> print dp.parse(r'(([x,y],[walks(x), jumps(y)]) + (([z],[twos(z)]) + ([w],[runs(w)])))')
    (([x,y],[walks(x), jumps(y)]) + ([z],[twos(z)]) + ([w],[runs(w)]))
    >>> print dp.parse(r'((([],[walks(x)]) + ([],[twos(x)])) + ([],[runs(x)]))')
    (([],[walks(x)]) + ([],[twos(x)]) + ([],[runs(x)]))
    >>> print dp.parse(r'((([],[walks(x)]) + ([],[runs(x)])) + (([],[threes(x)]) + ([],[fours(x)])))')
    (([],[walks(x)]) + ([],[runs(x)]) + ([],[threes(x)]) + ([],[fours(x)]))

    >>> print dp.parse(r'(([],[walks(x)]) -> ([],[runs(x)]))')
    (([],[walks(x)]) -> ([],[runs(x)]))

    >>> print dp.parse(r'([x],[PRO(x), sees(John,x)])')
    ([x],[PRO(x), sees(John,x)])
    >>> print dp.parse(r'([x],[man(x), -([],[walks(x)])])')
    ([x],[man(x), -([],[walks(x)])])
    >>> print dp.parse(r'([],[(([x],[man(x)]) -> ([],[walks(x)]))])')
    ([],[(([x],[man(x)]) -> ([],[walks(x)]))])
    
    >>> print dp.parse(r'DRS([x],[walk(x)])')
    ([x],[walk(x)])
    >>> print dp.parse(r'DRS([x][walk(x)])')
    ([x],[walk(x)])
    >>> print dp.parse(r'([x][walk(x)])')
    ([x],[walk(x)])
    
``simplify()``
--------------

    >>> print dp.parse(r'\x.([],[man(x), walks(x)])(john)').simplify()
    ([],[man(john), walks(john)])
    >>> print dp.parse(r'\x.\y.([z],[dog(z),sees(x,y)])(john)(mary)').simplify()
    ([z],[dog(z), sees(john,mary)])
    >>> print dp.parse(r'\R x.([],[big(x,R)])(\y.([],[mouse(y)]))').simplify()
    \x.([],[big(x,\y.([],[mouse(y)]))])
    
    >>> print dp.parse(r'(([x],[walks(x)]) + ([y],[runs(y)]))').simplify()
    ([x,y],[walks(x), runs(y)])
    >>> print dp.parse(r'(([x,y],[walks(x), jumps(y)]) + (([z],[twos(z)]) + ([w],[runs(w)])))').simplify()
    ([w,x,y,z],[walks(x), jumps(y), twos(z), runs(w)])
    >>> print dp.parse(r'((([],[walks(x)]) + ([],[runs(x)]) + ([],[threes(x)]) + ([],[fours(x)])))').simplify()
    ([],[walks(x), runs(x), threes(x), fours(x)])
    >>> dp.parse(r'([x],[man(x)])+([x],[walks(x)])').simplify() == \
    ... dp.parse(r'([x,z1],[man(x), walks(z1)])')
    True
    >>> dp.parse(r'([y],[boy(y), (([x],[dog(x)]) -> ([],[chase(x,y)]))])+([x],[run(x)])').simplify() == \
    ... dp.parse(r'([y,z1],[boy(y), (([x],[dog(x)]) -> ([],[chase(x,y)])), run(z1)])')
    True
        
    >>> dp.parse(r'\Q.(([x],[john(x),walks(x)]) + Q)(([x],[PRO(x),leaves(x)]))').simplify() == \
    ... dp.parse(r'([x,z1],[john(x), walks(x), PRO(z1), leaves(z1)])')
    True
    
    >>> logic._counter._value = 0
    >>> print dp.parse('([],[(([x],[dog(x)]) -> ([e,y],[boy(y), chase(e), subj(e,x), obj(e,y)]))])+([e,x],[PRO(x), run(e), subj(e,x)])').simplify()
    ([e02,z1],[(([x],[dog(x)]) -> ([e,y],[boy(y), chase(e), subj(e,x), obj(e,y)])), PRO(z1), run(e02), subj(e02,z1)])
    
``fol()``
-----------

    >>> print dp.parse(r'([x,y],[sees(x,y)])').fol()
    exists x y.sees(x,y)
    >>> print dp.parse(r'([x],[man(x), walks(x)])').fol()
    exists x.(man(x) & walks(x))
    >>> print dp.parse(r'\x.([],[man(x), walks(x)])').fol()
    \x.(man(x) & walks(x))
    >>> print dp.parse(r'\x y.([],[sees(x,y)])').fol()
    \x y.sees(x,y)

    >>> print dp.parse(r'\x.([],[walks(x)])(john)').fol()
    \x.walks(x)(john)
    >>> print dp.parse(r'\R x.([],[big(x,R)])(\y.([],[mouse(y)]))').fol()
    (\R x.big(x,R))(\y.mouse(y))

    >>> print dp.parse(r'(([x],[walks(x)]) + ([y],[runs(y)]))').fol()
    (exists x.walks(x) & exists y.runs(y))

    >>> print dp.parse(r'(([],[walks(x)]) -> ([],[runs(x)]))').fol()
    (walks(x) -> runs(x))

    >>> print dp.parse(r'([x],[PRO(x), sees(John,x)])').fol()
    exists x.(PRO(x) & sees(John,x))
    >>> print dp.parse(r'([x],[man(x), -([],[walks(x)])])').fol()
    exists x.(man(x) & -walks(x))
    >>> print dp.parse(r'([],[(([x],[man(x)]) -> ([],[walks(x)]))])').fol()
    all x.(man(x) -> walks(x))

    >>> print dp.parse(r'([x],[man(x) | walks(x)])').fol()
    exists x.(man(x) | walks(x))
    >>> print dp.parse(r'P(x) + ([x],[walks(x)])').fol()
    (P(x) & exists x.walks(x))

``resolve_anaphora()``
----------------------

    >>> from nltk.sem.drt import AnaphoraResolutionException

    >>> print resolve_anaphora(dp.parse(r'([x,y,z],[dog(x), cat(y), walks(z), PRO(z)])'))
    ([x,y,z],[dog(x), cat(y), walks(z), (z = [x,y])])
    >>> print resolve_anaphora(dp.parse(r'([],[(([x],[dog(x)]) -> ([y],[walks(y), PRO(y)]))])'))
    ([],[(([x],[dog(x)]) -> ([y],[walks(y), (y = x)]))])
    >>> print resolve_anaphora(dp.parse(r'(([x,y],[]) + ([],[PRO(x)]))')).simplify()
    ([x,y],[(x = y)])
    >>> try: print resolve_anaphora(dp.parse(r'([x],[walks(x), PRO(x)])'))
    ... except AnaphoraResolutionException, e: print e
    Variable 'x' does not resolve to anything.
    >>> print resolve_anaphora(dp.parse('([e01,z6,z7],[boy(z6), PRO(z7), run(e01), subj(e01,z7)])'))
    ([e01,z6,z7],[boy(z6), (z7 = z6), run(e01), subj(e01,z7)])

``equiv()``:
----------------

    >>> a = dp.parse(r'([x],[man(x), walks(x)])')
    >>> b = dp.parse(r'([x],[walks(x), man(x)])')
    >>> print a.equiv(b, TableauProver())
    True


``replace()``:
--------------

    >>> a = dp.parse(r'a')
    >>> w = dp.parse(r'w')
    >>> x = dp.parse(r'x')
    >>> y = dp.parse(r'y')
    >>> z = dp.parse(r'z')


replace bound
-------------

    >>> print dp.parse(r'([x],[give(x,y,z)])').replace(x.variable, a, False)
    ([x],[give(x,y,z)])
    >>> print dp.parse(r'([x],[give(x,y,z)])').replace(x.variable, a, True)
    ([a],[give(a,y,z)])

replace unbound
---------------

    >>> print dp.parse(r'([x],[give(x,y,z)])').replace(y.variable, a, False)
    ([x],[give(x,a,z)])
    >>> print dp.parse(r'([x],[give(x,y,z)])').replace(y.variable, a, True)
    ([x],[give(x,a,z)])

replace unbound with bound
--------------------------

    >>> dp.parse(r'([x],[give(x,y,z)])').replace(y.variable, x, False) == \
    ... dp.parse('([z1],[give(z1,x,z)])')
    True
    >>> dp.parse(r'([x],[give(x,y,z)])').replace(y.variable, x, True) == \
    ... dp.parse('([z1],[give(z1,x,z)])')
    True

replace unbound with unbound
----------------------------

    >>> print dp.parse(r'([x],[give(x,y,z)])').replace(y.variable, z, False)
    ([x],[give(x,z,z)])
    >>> print dp.parse(r'([x],[give(x,y,z)])').replace(y.variable, z, True)
    ([x],[give(x,z,z)])
    

replace unbound
---------------

    >>> print dp.parse(r'([x],[P(x,y,z)])+([y],[Q(x,y,z)])').replace(z.variable, a, False)
    (([x],[P(x,y,a)]) + ([y],[Q(x,y,a)]))
    >>> print dp.parse(r'([x],[P(x,y,z)])+([y],[Q(x,y,z)])').replace(z.variable, a, True)
    (([x],[P(x,y,a)]) + ([y],[Q(x,y,a)]))

replace bound
-------------

    >>> print dp.parse(r'([x],[P(x,y,z)])+([y],[Q(x,y,z)])').replace(x.variable, a, False)
    (([x],[P(x,y,z)]) + ([y],[Q(x,y,z)]))
    >>> print dp.parse(r'([x],[P(x,y,z)])+([y],[Q(x,y,z)])').replace(x.variable, a, True)
    (([a],[P(a,y,z)]) + ([y],[Q(a,y,z)]))

replace unbound with unbound
----------------------------

    >>> print dp.parse(r'([x],[P(x,y,z)])+([y],[Q(x,y,z)])').replace(z.variable, a, False)
    (([x],[P(x,y,a)]) + ([y],[Q(x,y,a)]))
    >>> print dp.parse(r'([x],[P(x,y,z)])+([y],[Q(x,y,z)])').replace(z.variable, a, True)
    (([x],[P(x,y,a)]) + ([y],[Q(x,y,a)]))

replace unbound with bound on same side
---------------------------------------

    >>> dp.parse(r'([x],[P(x,y,z)])+([y],[Q(x,y,w)])').replace(z.variable, x, False) == \
    ... dp.parse(r'(([z1],[P(z1,y,x)]) + ([y],[Q(z1,y,w)]))')
    True
    >>> dp.parse(r'([x],[P(x,y,z)])+([y],[Q(x,y,w)])').replace(z.variable, x, True) == \
    ... dp.parse(r'(([z1],[P(z1,y,x)]) + ([y],[Q(z1,y,w)]))')
    True

replace unbound with bound on other side
----------------------------------------

    >>> dp.parse(r'([x],[P(x,y,z)])+([y],[Q(x,y,w)])').replace(w.variable, x, False) == \
    ... dp.parse(r'(([z1],[P(z1,y,z)]) + ([y],[Q(z1,y,x)]))')
    True
    >>> dp.parse(r'([x],[P(x,y,z)])+([y],[Q(x,y,w)])').replace(w.variable, x, True) == \
    ... dp.parse(r'(([z1],[P(z1,y,z)]) + ([y],[Q(z1,y,x)]))')
    True

replace unbound with double bound
---------------------------------

    >>> dp.parse(r'([x],[P(x,y,z)])+([x],[Q(x,y,w)])').replace(z.variable, x, False) == \
    ... dp.parse(r'(([z1],[P(z1,y,x)]) + ([z1],[Q(z1,y,w)]))')
    True
    >>> dp.parse(r'([x],[P(x,y,z)])+([x],[Q(x,y,w)])').replace(z.variable, x, True) == \
    ... dp.parse(r'(([z1],[P(z1,y,x)]) + ([z1],[Q(z1,y,w)]))')
    True


regression tests
----------------

    >>> d = dp.parse('([x],[A(c), ([y],[B(x,y,z,a)])->([z],[C(x,y,z,a)])])')
    >>> print d
    ([x],[A(c), (([y],[B(x,y,z,a)]) -> ([z],[C(x,y,z,a)]))])
    >>> d.pprint()
     ____________________________________ 
    | x                                  |
    |------------------------------------|
    | A(c)                               |
    |   ____________      ____________   |
    |  | y          |    | z          |  |
    | (|------------| -> |------------|) |
    |  | B(x,y,z,a) |    | C(x,y,z,a) |  |
    |  |____________|    |____________|  |
    |____________________________________|
    >>> print str(d)
    ([x],[A(c), (([y],[B(x,y,z,a)]) -> ([z],[C(x,y,z,a)]))])
    >>> print d.fol()
    exists x.(A(c) & all y.(B(x,y,z,a) -> exists z.C(x,y,z,a)))
    >>> print d.replace(Variable('a'), DrtVariableExpression(Variable('r')))
    ([x],[A(c), (([y],[B(x,y,z,r)]) -> ([z],[C(x,y,z,r)]))])
    >>> print d.replace(Variable('x'), DrtVariableExpression(Variable('r')))
    ([x],[A(c), (([y],[B(x,y,z,a)]) -> ([z],[C(x,y,z,a)]))])
    >>> print d.replace(Variable('y'), DrtVariableExpression(Variable('r')))
    ([x],[A(c), (([y],[B(x,y,z,a)]) -> ([z],[C(x,y,z,a)]))])
    >>> print d.replace(Variable('z'), DrtVariableExpression(Variable('r')))    
    ([x],[A(c), (([y],[B(x,y,r,a)]) -> ([z],[C(x,y,z,a)]))])
    >>> print d.replace(Variable('x'), DrtVariableExpression(Variable('r')), True)
    ([r],[A(c), (([y],[B(r,y,z,a)]) -> ([z],[C(r,y,z,a)]))])
    >>> print d.replace(Variable('y'), DrtVariableExpression(Variable('r')), True)
    ([x],[A(c), (([r],[B(x,r,z,a)]) -> ([z],[C(x,r,z,a)]))])
    >>> print d.replace(Variable('z'), DrtVariableExpression(Variable('r')), True)
    ([x],[A(c), (([y],[B(x,y,r,a)]) -> ([r],[C(x,y,r,a)]))])
    >>> print d == dp.parse('([l],[A(c), ([m],[B(l,m,z,a)])->([n],[C(l,m,n,a)])])')
    True
    >>> d = dp.parse('([],[([x,y],[B(x,y,h), ([a,b],[dee(x,a,g)])])->([z,w],[cee(x,y,f), ([c,d],[E(x,c,d,e)])])])')
    >>> print d.free()
    set([Variable('B'), Variable('E'), Variable('g'), Variable('f'), Variable('h'), Variable('e')])
    >>> print d.variables()
    set([Variable('B'), Variable('E'), Variable('g'), Variable('f'), Variable('h'), Variable('e')])
    >>> print d.get_refs(True)
    [Variable('x'), Variable('y'), Variable('a'), Variable('b'), Variable('z'), Variable('w'), Variable('c'), Variable('d')]
    >>> print d.conds[0].get_refs(False)
    [Variable('x'), Variable('y')]
    >>> print dp.parse('([x,y],[A(x,y), (x=y), ([],[B(x,y)])->([],[C(x,y)]), ([x,y],[D(x,y)])->([],[E(x,y)]), ([],[F(x,y)])->([x,y],[G(x,y)])])').eliminate_equality()
    ([x],[A(x,x), (([],[B(x,x)]) -> ([],[C(x,x)])), (([x,y],[D(x,y)]) -> ([],[E(x,y)])), (([],[F(x,x)]) -> ([x,y],[G(x,y)]))])
    >>> print dp.parse('([x,y],[A(x,y), (x=y)]) -> ([],[B(x,y)])').eliminate_equality()
    (([x],[A(x,x)]) -> ([],[B(x,x)]))
    >>> print dp.parse('([x,y],[A(x,y)]) -> ([],[B(x,y), (x=y)])').eliminate_equality()
    (([x,y],[A(x,y)]) -> ([],[B(x,x)]))
    >>> print dp.parse('([x,y],[A(x,y), (x=y), ([],[B(x,y)])])').eliminate_equality()
    ([x],[A(x,x), ([],[B(x,x)])])
    >>> print dp.parse('([x,y],[A(x,y), ([],[B(x,y), (x=y)])])').eliminate_equality()
    ([x,y],[A(x,y), ([],[B(x,x)])])
    >>> print dp.parse('([z8 z9 z10],[A(z8), z8=z10, z9=z10, B(z9), C(z10), D(z10)])').eliminate_equality()
    ([z9],[A(z9), B(z9), C(z9), D(z9)])

    >>> print dp.parse('([x,y],[A(x,y), (x=y), ([],[B(x,y)]), ([x,y],[C(x,y)])])').eliminate_equality()
    ([x],[A(x,x), ([],[B(x,x)]), ([x,y],[C(x,y)])])
    >>> print dp.parse('([x,y],[A(x,y)]) + ([],[B(x,y), (x=y)]) + ([],[C(x,y)])').eliminate_equality()
    ([x],[A(x,x), B(x,x), C(x,x)])
    >>> print dp.parse('([x,y],[B(x,y)])+([x,y],[C(x,y)])').replace(Variable('y'), DrtVariableExpression(Variable('x')))
    (([x,y],[B(x,y)]) + ([x,y],[C(x,y)]))
    >>> print dp.parse('(([x,y],[B(x,y)])+([],[C(x,y)]))+([],[D(x,y)])').replace(Variable('y'), DrtVariableExpression(Variable('x')))
    (([x,y],[B(x,y)]) + ([],[C(x,y)]) + ([],[D(x,y)]))
    >>> print dp.parse('(([],[B(x,y)])+([],[C(x,y)]))+([],[D(x,y)])').replace(Variable('y'), DrtVariableExpression(Variable('x')))
    (([],[B(x,x)]) + ([],[C(x,x)]) + ([],[D(x,x)]))
    >>> print dp.parse('(([],[B(x,y), ([x,y],[A(x,y)])])+([],[C(x,y)]))+([],[D(x,y)])').replace(Variable('y'), DrtVariableExpression(Variable('x')))
    (([],[B(z15,x), ([y,z15],[A(z15,y)])]) + ([],[C(z15,x)]) + ([],[D(z15,x)]))


Parse errors
============

    >>> try: dp.parse(r'')
    ... except logic.ParseException, e: print e
    End of input found.  Expression expected.
    <BLANKLINE>
    ^
    >>> try: dp.parse(r'(')
    ... except logic.ParseException, e: print e
    End of input found.  Expression expected.
    (
     ^
    >>> try: dp.parse(r'()')
    ... except logic.ParseException, e: print e
    Unexpected token: ')'.  Expression expected.
    ()
     ^
    >>> try: dp.parse(r'([')
    ... except logic.ParseException, e: print e
    End of input found.  Expected token ']'.
    ([
      ^
    >>> try: dp.parse(r'([,')
    ... except logic.ParseException, e: print e
    ',' is an illegal variable name.  Constants may not be quantified.
    ([,
      ^
    >>> try: dp.parse(r'([x,')
    ... except logic.ParseException, e: print e
    End of input found.  Variable expected.
    ([x,
        ^
    >>> try: dp.parse(r'([]')
    ... except logic.ParseException, e: print e
    End of input found.  Expected token '['.
    ([]
       ^
    >>> try: dp.parse(r'([][')
    ... except logic.ParseException, e: print e
    End of input found.  Expected token ']'.
    ([][
        ^
    >>> try: dp.parse(r'([][,')
    ... except logic.ParseException, e: print e
    Unexpected token: ','.  Expression expected.
    ([][,
        ^
    >>> try: dp.parse(r'([][]')
    ... except logic.ParseException, e: print e
    End of input found.  Expected token ')'.
    ([][]
         ^
    >>> try: dp.parse(r'([x][man(x)]) |')
    ... except logic.ParseException, e: print e
    End of input found.  Expression expected.
    ([x][man(x)]) |
                   ^

Pretty Printing
===============

    >>> dp.parse(r"([],[])").pprint()
     __ 
    |  |
    |--|
    |__|
    >>> dp.parse(r"([],[([x],[big(x), dog(x)]) -> ([],[bark(x)]) -([x],[walk(x)])])").pprint()
     _____________________________ 
    |                             |
    |-----------------------------|
    |   ________      _________   |
    |  | x      |    |         |  |
    | (|--------| -> |---------|) |
    |  | big(x) |    | bark(x) |  |
    |  | dog(x) |    |_________|  |
    |  |________|                 |
    |      _________              |
    |     | x       |             |
    | __  |---------|             |
    |   | | walk(x) |             |
    |     |_________|             |
    |_____________________________|
    >>> dp.parse(r"([x,y],[x=y]) + ([z],[dog(z), walk(z)])").pprint()
      _________     _________  
     | x y     |   | z       | 
    (|---------| + |---------|)
     | (x = y) |   | dog(z)  | 
     |_________|   | walk(z) | 
                   |_________| 
    >>> dp.parse(r"([],[([x],[]) | ([y],[]) | ([z],[dog(z), walk(z)])])").pprint()
     _______________________________ 
    |                               |
    |-------------------------------|
    |   ___     ___     _________   |
    |  | x |   | y |   | z       |  |
    | (|---| | |---| | |---------|) |
    |  |___|   |___|   | dog(z)  |  |
    |                  | walk(z) |  |
    |                  |_________|  |
    |_______________________________|
    >>> dp.parse(r"\P.\Q.(([x],[]) + P(x) + Q(x))(\x.([],[dog(x)]))").pprint()
              ___                        ________  
     \       | x |                 \    |        | 
     /\ P Q.(|---| + P(x) + Q(x))( /\ x.|--------|)
             |___|                      | dog(x) | 
                                        |________|