"""This module implements a declarative Logic language using Scheme syntax.

Logic is a variant of the Prolog language, based on scmlog by Paul Hilfinger
and the logic programming example in SICP.

All valid logic expressions are Scheme lists.  Valid forms include:

(fact ...):  Assert a consequent, followed by zero or more hypotheses
(query ...): Query zero or more relations simultaneously
(load PATH): Load a .logic file by evaluating its expressions
"""

__version__ = '1.3'

from scheme import (Frame, Pair, nil, read_line, scheme_load,
                    scheme_atomp, scheme_symbolp, scheme_pairp, scheme_listp)
from ucb import main, trace

facts = []

#############
# Inference #
#############

glob = Frame(None)
glob.stack = []

DEPTH_LIMIT = None
def do_query(clauses):
    """Yield all bindings that simultaneously satisfy clauses."""
    for env in search(clauses, glob, 0):
        yield [(v, ground(v, env)) for v in get_vars(clauses)]

def search(clauses, env, depth):
    """Search for an application of rules to establish all the clauses,
    non-destructively extending the unifier env.  Limit the search to
    the nested application of depth rules."""
    if clauses is nil:
        yield env
    elif DEPTH_LIMIT is None or depth <= DEPTH_LIMIT:
        if clauses.first.first in ('not', '~'):
            clause = ground(clauses.first.rest, env)
            try:
                next(search(clause, glob, 0))
            except StopIteration:
                env_head = Frame(env)
                for result in search(clauses.rest, env_head, depth+1):
                    yield result
        else:
            for fact in facts:
                fact = rename_variables(fact, get_unique_id())
                env_head = Frame(env)
                if unify(fact.first, clauses.first, env_head):
                    for env_rule in search(fact.rest, env_head, depth+1):
                        for result in search(clauses.rest, env_rule, depth+1):
                            yield result

def unify(e, f, env):
    """Destructively extend env so as to unify (make equal) e and f, returning
    True if this succeeds and False otherwise.  env may be modified in either
    case (its existing bindings are never changed)."""
    e = lookup(e, env)
    f = lookup(f, env)
    if e == f:
        return True
    elif isvar(e):
        env.define(e, f)
        return True
    elif isvar(f):
        env.define(f, e)
        return True
    elif scheme_atomp(e) or scheme_atomp(f):
        return False
    else:
        return unify(e.first, f.first, env) and unify(e.rest, f.rest, env)

################
# Environments #
################

def lookup(sym, env):
    """Look up a symbol repeatedly until it is fully resolved."""
    try:
        return lookup(env.lookup(sym), env)
    except:
        return sym

def ground(expr, env):
    """Replace all variables with their values in expr."""
    if scheme_symbolp(expr):
        resolved = lookup(expr, env)
        if expr != resolved:
            return ground(resolved, env)
        else:
            return expr
    elif scheme_pairp(expr):
        return Pair(ground(expr.first, env), ground(expr.rest, env))
    else:
        return expr

def get_vars(expr):
    """Return all logical vars in expr as a list."""
    if isvar(expr):
        return [expr]
    elif scheme_pairp(expr):
        vs = get_vars(expr.first)
        for v in get_vars(expr.rest):
            if v not in vs:
                vs.append(v)
        return vs
    else:
        return []

IDENTIFIER = 0
def get_unique_id():
    """Return a unique identifier."""
    global IDENTIFIER
    IDENTIFIER += 1
    return IDENTIFIER

def rename_variables(expr, n):
    """Rename all variables in expr with an identifier N."""
    if isvar(expr):
        return expr + '_' + str(n)
    elif scheme_pairp(expr):
        return Pair(rename_variables(expr.first, n),
                    rename_variables(expr.rest, n))
    else:
        return expr

def isvar(symbol):
    """Return whether symbol is a logical variable."""
    return scheme_symbolp(symbol) and symbol.startswith("?")

##################
# User Interface #
##################

def process_input(expr, env):
    """Process an input expr, which may be a fact or query."""
    if expr == 'exit':
        print("Goodbye.")
        sys.exit(0)

    if not scheme_listp(expr):
        print('Improperly formed expression.')
    elif expr.first in ("fact", "!"):
        facts.append(expr.rest)
    elif expr.first in ("query", "?"):
        results = do_query(expr.rest)
        success = False
        for result in results:
            if not success:
                print('Success!')
            success = True
            output = "\t".join("{0}: {1}".format(k[1:], v) for k, v in result)
            if output:
                print(output)
        if not success:
            print('Failed.')
    elif expr.first == "load":
        scheme_load(expr.rest.first, env)
    else:
        print("Please provide a fact or query.")

import scheme

scheme.buffer_input.__defaults__ = ('logic> ',)
scheme.buffer_lines.__defaults__ = ('logic> ', False)
scheme.scheme_eval = process_input

@main
def run_logic(*argv):
    scheme.run(*argv)