#!/usr/bin/python3
"""Sentential database.

This is just a very first initial inefficient prototype.  See
sentential-database.md in Derctuo for more details, but this version
just handles very simple inference without negation, stratification,
formulas, abbreviation, goal seek, units, libraries, existentials,
tabular output, nesting, regexps, denesting, inequalities, frames and
modal reasoning, arrays and dynamical systems, etc.

Example input:

    Socrates is a man
    Every man is a mortal
    Every mortal is dead eventually

    Every {X} is {Y}
    {Z} is a {X}
    => {Z} is {Y}

Resulting output:

    ∴ Every man is dead eventually
    ∴ Socrates is a mortal
    ∴ Socrates is dead eventually

"""
import re
import sys


class DB:
    def __init__(self):
        self.rules = []
        self.premises = []
        self.premises_done = False
        self.facts = set()

    def dump(self, print):
        for rule in self.rules:
            for premise in rule.premises:
                print(premise.pat)
            print('=>', rule.conclusion.printf)

        print()

    def add_conclusion(self, conclusion):
        self.premises_done = True
        self.rules.append(Rule(self.premises[:], conclusion))

    def add_premise(self, premise):
        if self.premises_done:
            self.premises, self.premises_done = [], False
        self.premises.append(premise)

    def add_fact(self, fact):
        self.premises_done = True
        self.facts.add(fact)

    def match(self, premises, instantiated):
        if not premises:
            yield instantiated
            return

        premise, remaining = premises[0], premises[1:]
        for fact in self.facts:
            mo = premise.match(fact, instantiated)
            if mo:
                for assignment in self.match(remaining, mo):
                    yield assignment

    def apply(self, rule, callback=lambda _: ...):
        new_facts = set()
        for assignment in self.match(rule.premises, {}):
            fact = rule.conclusion.render(assignment)
            if fact not in self.facts and fact not in new_facts:
                callback(fact)
                new_facts.add(fact)

        self.facts.update(new_facts)


class Rule:
    def __init__(self, premises, conclusion):
        self.premises = [Pattern(p) for p in premises]
        self.conclusion = Pattern(conclusion)


class Pattern:
    def __init__(self, text):
        seen = set()
        regexps = [r'\A']
        printf = []
        for token in re.split(r'(\{.*?\})', text):
            if not token.startswith('{'):
                regexps.append(re.escape(token))
                printf.append(token.replace('%', '%%'))
                continue

            name = token[1:-1].lower()
            printf.append('%%(%s)s' % name)
            if name in seen:
                regexps.append('(?P=%s)' % name)
            else:
                seen.add(name)
                regexps.append('(?P<%s>.*?)' % name)

        regexps.append(r'\Z')

        self.pat = ''.join(regexps)
        self.printf = ''.join(printf)

    def render(self, instantiated):
        return self.printf % instantiated

    def match(self, text, instantiated):
        mo = re.match(self.pat, text)
        if not mo:
            return None

        d = mo.groupdict()
        for k, v in instantiated.items():
            if k in d and v.lower() != d[k].lower():
                return None
            d[k] = v

        return d


def read_database(infile):
    db = DB()
    for line in infile:
        line = line.strip()
        if line.startswith('=>'):
            db.add_conclusion(line[2:].strip())
        elif '{' in line:
            db.add_premise(line)
        elif line.strip():
            db.add_fact(line)

    return db


def main(argv):
    db = read_database(open(argv[1]))

    inferred = []
    def notify(new_fact):
        print('∴', new_fact)
        inferred.append(new_fact)

    while True:
        inferred.clear()
        for rule in db.rules:
            db.apply(rule, notify)
        if not inferred:
            break


if __name__ == '__main__':
    main(sys.argv)