JSON-Lang/resolution.py

from emis_funky_funktions import *

from itertools import product

from ir import Clause, IRNeg, IRProp, IRTerm, IRVar, Substitutions, sub_all, unify, unify_clauses

def terms_cancel(t1: IRTerm, t2: IRTerm) -> Option[Substitutions]:
	"""
	Determine if two terms could cancel each other out, given the right substitutions

	That is, is there some set of substitutions such that t1 = ¬t2 or ¬t1 = t2?

	If negation is possible and a substitution exists, that substitution is returned.
	Otherwise, `None` is returned.

	>>> terms_cancel(IRNeg(IRVar('x1')), IRProp('Terezi'))
	Some((Terezi()/x1,))

	>>> terms_cancel(IRProp('Nepeta'), IRVar('x1'))
	Some((¬Nepeta()/x1,))

	>>> terms_cancel(IRProp('ancestor', [IRVar('x1')]), IRVar('x1')) is None
	True
	"""
	match (t1, t2):
		case (IRNeg(a), b) | (b, IRNeg(a)): #type: ignore
			return hush(unify(a, b))
		case (IRVar(_) as x, a) | (a, IRVar(_) as x): #type: ignore
			return hush(unify(x, IRNeg(a)))
	return None

def merge_clauses(c1: Clause, c2: Clause) -> Sequence[Clause]:
    """
    Produce a list of all possible clauses which resolution could derive from c1 and c2

    For each term in c1 that could cancel with a term in c2 using a substitution, a
    possible clause is produced equal to the concatenation of c1 and c2 with the canceled
    terms removed and the substitution applied.

    >>> merge_clauses(
    ...     [ IRProp('day'), IRNeg(IRProp('night')) ],
    ...     [ IRProp('night') ]
    ... )
    [[day()]]

    >>> merge_clauses(
    ...     [ IRNeg(IRProp('transgender', [IRVar('x1')])), IRProp('powerful', [IRVar('x1')]) ],
    ...     [ IRNeg(IRProp('powerful', [IRVar('x2')])), IRProp('god', [IRVar('x2')]) ]
    ... )
    [[¬transgender(*x1), god(*x1)]]

    >>> merge_clauses(
    ...     [ IRNeg(IRProp('day')), IRProp('night') ],
    ...     [ IRVar('x2') ]
    ... )
    [[night()], [¬day()]]

    If two clauses cannot merge, an empty list is returned

    >>> merge_clauses(
    ...     [ IRProp('day') ],
    ...     [ IRProp('wet') ]
    ... )
    []
    """
    valid_substitutions = drop_none(
        map_opt(lambda subs: (subs, i1, i2), terms_cancel(t1, t2))
        for ((i1, t1), (i2, t2)) in product(enumerate(c1), enumerate(c2))
    )
    return [
        [
            sub_all(subs, term)
            for term in (*c1[:i1], *c1[i1 + 1:], *c2[:i2], *c2[i2 + 1:])
        ]
        for (subs, i1, i2) in valid_substitutions
    ]

if __name__ == '__main__':
	import doctest
	doctest.testmod()