def tableau_test(c, ps=None, verbose=False):
    pc = Expression.fromstring(c)
    pps = [Expression.fromstring(p) for p in ps] if ps else []
    if not ps:
        ps = []
    print(
        '%s |- %s: %s'
        % (', '.join(ps), pc, TableauProver().prove(pc, pps, verbose=verbose))
    )

def test_prove(arguments):
    """
    Try some proofs and exhibit the results.
    """
    for (goal, assumptions) in arguments:
        g = Expression.fromstring(goal)
        alist = [Expression.fromstring(a) for a in assumptions]
        p = Prover9Command(g, assumptions=alist).prove()
        for a in alist:
            print('   %s' % a)
        print('|- %s: %s\n' % (g, p))

def test_config():

    a = Expression.fromstring('(walk(j) & sing(j))')
    g = Expression.fromstring('walk(j)')
    p = Prover9Command(g, assumptions=[a])
    p._executable_path = None
    p.prover9_search=[]
    p.prove()
    #config_prover9('/usr/local/bin')
    print(p.prove())
    print(p.proof())

def testResolutionProver():
    resolution_test(r'man(x)')
    resolution_test(r'(man(x) -> man(x))')
    resolution_test(r'(man(x) -> --man(x))')
    resolution_test(r'-(man(x) and -man(x))')
    resolution_test(r'(man(x) or -man(x))')
    resolution_test(r'(man(x) -> man(x))')
    resolution_test(r'-(man(x) and -man(x))')
    resolution_test(r'(man(x) or -man(x))')
    resolution_test(r'(man(x) -> man(x))')
    resolution_test(r'(man(x) iff man(x))')
    resolution_test(r'-(man(x) iff -man(x))')
    resolution_test('all x.man(x)')
    resolution_test('-all x.some y.F(x,y) & some x.all y.(-F(x,y))')
    resolution_test('some x.all y.sees(x,y)')

    p1 = Expression.fromstring(r'all x.(man(x) -> mortal(x))')
    p2 = Expression.fromstring(r'man(Socrates)')
    c = Expression.fromstring(r'mortal(Socrates)')
    print('%s, %s |- %s: %s' % (p1, p2, c, ResolutionProver().prove(c, [p1,p2])))

    p1 = Expression.fromstring(r'all x.(man(x) -> walks(x))')
    p2 = Expression.fromstring(r'man(John)')
    c = Expression.fromstring(r'some y.walks(y)')
    print('%s, %s |- %s: %s' % (p1, p2, c, ResolutionProver().prove(c, [p1,p2])))

    p = Expression.fromstring(r'some e1.some e2.(believe(e1,john,e2) & walk(e2,mary))')
    c = Expression.fromstring(r'some e0.walk(e0,mary)')
    print('%s |- %s: %s' % (p, c, ResolutionProver().prove(c, [p])))

def test_convert_to_prover9(expr):
    """
    Test that parsing works OK.
    """
    for t in expr:
        e = Expression.fromstring(t)
        print(convert_to_prover9(e))

    def __init__(self, meaning, glue, indices=None):
        if not indices:
            indices = set()

        if isinstance(meaning, string_types):
            self.meaning = Expression.fromstring(meaning)
        elif isinstance(meaning, Expression):
            self.meaning = meaning
        else:
            raise RuntimeError(
                'Meaning term neither string or expression: %s, %s'
                % (meaning, meaning.__class__)
            )

        if isinstance(glue, string_types):
            self.glue = linearlogic.LinearLogicParser().parse(glue)
        elif isinstance(glue, linearlogic.Expression):
            self.glue = glue
        else:
            raise RuntimeError(
                'Glue term neither string or expression: %s, %s'
                % (glue, glue.__class__)
            )

        self.indices = indices

def demo():
    test_clausify()
    print()
    testResolutionProver()
    print()

    p = Expression.fromstring('man(x)')
    print(ResolutionProverCommand(p, [p]).prove())

def satdemo(trace=None):
    """Satisfiers of an open formula in a first order model."""

    print()
    print('*' * mult)
    print("Satisfiers Demo")
    print('*' * mult)

    folmodel(quiet=True)

    formulas = [
               'boy(x)',
               '(x = x)',
               '(boy(x) | girl(x))',
               '(boy(x) & girl(x))',
               'love(adam, x)',
               'love(x, adam)',
               '-(x = adam)',
               'exists z22. love(x, z22)',
               'exists y. love(y, x)',
               'all y. (girl(y) -> love(x, y))',
               'all y. (girl(y) -> love(y, x))',
               'all y. (girl(y) -> (boy(x) & love(y, x)))',
               '(boy(x) & all y. (girl(y) -> love(x, y)))',
               '(boy(x) & all y. (girl(y) -> love(y, x)))',
               '(boy(x) & exists y. (girl(y) & love(y, x)))',
               '(girl(x) -> dog(x))',
               'all y. (dog(y) -> (x = y))',
               'exists y. love(y, x)',
               'exists y. (love(adam, y) & love(y, x))'
                ]

    if trace:
        print(m2)

    for fmla in formulas:
        print(fmla)
        Expression.fromstring(fmla)

    parsed = [Expression.fromstring(fmla) for fmla in formulas]

    for p in parsed:
        g2.purge()
        print("The satisfiers of '%s' are: %s" % (p, m2.satisfiers(p, 'x', g2, trace)))

def folmodel(quiet=False, trace=None):
    """Example of a first-order model."""

    global val2, v2, dom2, m2, g2

    v2 = [('adam', 'b1'), ('betty', 'g1'), ('fido', 'd1'),\
         ('girl', set(['g1', 'g2'])), ('boy', set(['b1', 'b2'])), ('dog', set(['d1'])),
         ('love', set([('b1', 'g1'), ('b2', 'g2'), ('g1', 'b1'), ('g2', 'b1')]))]
    val2 = Valuation(v2)
    dom2 = val2.domain
    m2 = Model(dom2, val2)
    g2 = Assignment(dom2, [('x', 'b1'), ('y', 'g2')])

    if not quiet:
        print()
        print('*' * mult)
        print("Models Demo")
        print("*" * mult)
        print("Model m2:\n", "-" * 14,"\n", m2)
        print("Variable assignment = ", g2)

        exprs = ['adam', 'boy', 'love', 'walks', 'x', 'y', 'z']
        parsed_exprs = [Expression.fromstring(e) for e in exprs]

        print()
        for parsed in parsed_exprs:
            try:
                print("The interpretation of '%s' in m2 is %s" % (parsed, m2.i(parsed, g2)))
            except Undefined:
                print("The interpretation of '%s' in m2 is Undefined" % parsed)


        applications = [('boy', ('adam')), ('walks', ('adam',)), ('love', ('adam', 'y')), ('love', ('y', 'adam'))]

        for (fun, args) in applications:
            try:
                funval = m2.i(Expression.fromstring(fun), g2)
                argsval = tuple(m2.i(Expression.fromstring(arg), g2) for arg in args)
                print("%s(%s) evaluates to %s" % (fun, args, argsval in funval))
            except Undefined:
                print("%s(%s) evaluates to Undefined" % (fun, args))

def fromstring(lex_str, include_semantics=False):
    """
    Convert string representation into a lexicon for CCGs.
    """
    CCGVar.reset_id()
    primitives = []
    families = {}
    entries = defaultdict(list)
    for line in lex_str.splitlines():
        # Strip comments and leading/trailing whitespace.
        line = COMMENTS_RE.match(line).groups()[0].strip()
        if line == "":
            continue

        if line.startswith(':-'):
            # A line of primitive categories.
            # The first one is the target category
            # ie, :- S, N, NP, VP
            primitives = primitives + [
                prim.strip() for prim in line[2:].strip().split(',')
            ]
        else:
            # Either a family definition, or a word definition
            (ident, sep, rhs) = LEX_RE.match(line).groups()
            (catstr, semantics_str) = RHS_RE.match(rhs).groups()
            (cat, var) = augParseCategory(catstr, primitives, families)

            if sep == '::':
                # Family definition
                # ie, Det :: NP/N
                families[ident] = (cat, var)
            else:
                semantics = None
                if include_semantics is True:
                    if semantics_str is None:
                        raise AssertionError(
                            line
                            + " must contain semantics because include_semantics is set to True"
                        )
                    else:
                        semantics = Expression.fromstring(
                            SEMANTICS_RE.match(semantics_str).groups()[0]
                        )
                # Word definition
                # ie, which => (N\N)/(S/NP)
                entries[ident].append(Token(ident, cat, semantics))
    return CCGLexicon(primitives[0], primitives, families, entries)

def load_fol(s):
    """
    Temporarily duplicated from ``nltk.sem.util``.
    Convert a  file of first order formulas into a list of ``Expression`` objects.

    :param s: the contents of the file
    :type s: str
    :return: a list of parsed formulas.
    :rtype: list(Expression)
    """
    statements = []
    for linenum, line in enumerate(s.splitlines()):
        line = line.strip()
        if line.startswith('#') or line=='': continue
        try:
            statements.append(Expression.fromstring(line))
        except Exception:
            raise ValueError('Unable to parse line %s: %s' % (linenum, line))
    return statements

 def evaluate(self, expr, g, trace=None):
     """
     Read input expressions, and provide a handler for ``satisfy``
     that blocks further propagation of the ``Undefined`` error.
     :param expr: An ``Expression`` of ``logic``.
     :type g: Assignment
     :param g: an assignment to individual variables.
     :rtype: bool or 'Undefined'
     """
     try:
         parsed = Expression.fromstring(expr)
         value = self.satisfy(parsed, g, trace=trace)
         if trace:
             print()
             print("'%s' evaluates to %s under M, %s" %  (expr, value, g))
         return value
     except Undefined:
         if trace:
             print()
             print("'%s' is undefined under M, %s" %  (expr, g))
         return 'Undefined'

def resolution_test(e):
    f = Expression.fromstring(e)
    t = ResolutionProver().prove(f)
    print('|- %s: %s' % (f, t))

    def _get_transitions(self,
                         expression: Expression,
                         current_transitions: List[str]) -> List[str]:
        # The way we handle curried functions in here is a bit of a mess, but it works.  For any
        # function that takes more than one argument, the NLTK Expression object will be curried,
        # and so the standard "visitor" pattern used by NLTK will result in action sequences that
        # are also curried.  We need to detect these curried functions and uncurry them in the
        # action sequence.  We do that by keeping around a dictionary mapping multi-argument
        # functions to the number of arguments they take.  When we see a multi-argument function,
        # we check to see if we're at the top-level, first instance of that function by checking
        # its number of arguments with NLTK's `uncurry()` function.  If it is, we output an action
        # using those arguments.  Otherwise, we're at an intermediate node of a curried function,
        # and we squelch the action that would normally be generated.
        # TODO(mattg): There might be some way of removing the need for `curried_functions` here,
        # using instead the `argument_types()` function I added to `ComplexType`, but my guess is
        # that it would involve needing to modify nltk, and I don't want to bother with figuring
        # that out right now.
        curried_functions = self._get_curried_functions()
        expression_type = expression.type
        try:
            # ``Expression.visit()`` takes two arguments: the first one is a function applied on
            # each sub-expression and the second is a combinator that is applied to the list of
            # values returned from the function applications. We just want the list of all
            # sub-expressions here.
            sub_expressions = expression.visit(lambda x: x, lambda x: x)
            transformed_types = [sub_exp.type for sub_exp in sub_expressions]

            if isinstance(expression, LambdaExpression):
                # If the expression is a lambda expression, the list of sub expressions does not
                # include the "lambda x" term. We're adding it here so that we will see transitions
                # like
                #   <e,d> -> [\x, d] instead of
                #   <e,d> -> [d]
                transformed_types = ["lambda x"] + transformed_types
            elif isinstance(expression, ApplicationExpression):
                function, arguments = expression.uncurry()
                function_type = function.type
                if function_type in curried_functions:
                    expected_num_arguments = curried_functions[function_type]
                    if len(arguments) == expected_num_arguments:
                        # This is the initial application of a curried function.  We'll use this
                        # node in the expression to generate the action for this function, using
                        # all of its arguments.
                        transformed_types = [function.type] + [argument.type for argument in arguments]
                    else:
                        # We're at an intermediate node.  We'll set `transformed_types` to `None`
                        # to indicate that we need to squelch this action.
                        transformed_types = None

            if transformed_types:
                transition = f"{expression_type} -> {transformed_types}"
                current_transitions.append(transition)
            for sub_expression in sub_expressions:
                self._get_transitions(sub_expression, current_transitions)
        except NotImplementedError:
            # This means that the expression is a leaf. We simply make a transition from its type to itself.
            original_name = str(expression)
            if original_name in self.reverse_name_mapping:
                original_name = self.reverse_name_mapping[original_name]
            transition = f"{expression_type} -> {original_name}"
            current_transitions.append(transition)
        return current_transitions