system_L.py

'''
Name: Formal Deduction System   
Author: mbinary  
Time: 2018-3-6
Description:

denots:
deduce: >
negation: ~

read from left to right
e.g. p>~(q>~r)
'''

import re
import sympy
from random import randint
from collections import namedtuple


NON = sympy.Symbol('~')
CONTAIN = sympy.Symbol('>')
AND = sympy .Symbol('&')
OR = sympy.Symbol('|')
EQUAL = sympy.Symbol('-')
LEFT = sympy.Symbol('(')
RIGHT = sympy.Symbol(')')
CONN = [NON, CONTAIN, LEFT, RIGHT]
PAIR = namedtuple('pair', ['pre', 'suf'])


def non(p):
    li = p.getPreOrderLst()
    if li[0] == NON:
        return formula(li[1:])
    return formula([NON]+li)


def contain(p, q):
    '''p->q'''
    return formula([CONTAIN]+p.getPreOrderLst()+q.getPreOrderLst())


def isConn(p):
    return p in CONN


def in2pre(s):
    ''' 
        inorder symbols of list ->  prorder symbols of list
    '''
    def matchParentheses(i=0, reverse=False):
        '''match parentheses from one end  of s and ret pointer i'''
        delta = -1 if reverse is True else 1
        ct = 0
        while 1:
            if s[i] == LEFT:
                ct -= 1
            elif s[i] == RIGHT:
                ct += 1
            i += delta
            if ct == 0:
                break
        try:
            while s[i] == NON:
                i += delta
        except:
            pass
        return i

    n = len(s)
    if n <= 2:
        return s
    i = matchParentheses()
    if i == n and s[0] == LEFT and s[-1] == RIGHT:
        return in2pre(s[1:-1])
    if s[0] == NON and s[1] == LEFT and matchParentheses(1) == n and s[-1] == RIGHT:
        return [NON]+in2pre(s[2:-1])
    i = -1
    if s[-1] == RIGHT:
        i = matchParentheses(-1, True)
    else:
        while s[i] != CONTAIN:
            i -= 1
    return [CONTAIN]+in2pre(s[:i])+in2pre(s[i+1:])


class formula:
    def __init__(self, preOrderLst):
        self.preOrderLst = preOrderLst
        if not self.isValid():
            raise Exception('invalid formula')
        self.inOrderLst = self.pre2in(self.preOrderLst)
        self.sz = len(self.preOrderLst)

    def __bool__(self): return bool(self.preOrderLst)

    def __len__(self): return self.sz

    def __getitem(self, i): return self.preOrderLst[i]

    def __iter__(self): return iter(self.preOrderLst)

    def __repr__(self): return 'formula({})'.format(str(self))

    def __str__(self): return ''.join([str(i) for i in self.inOrderLst])

    def __hash__(self): return hash(
        ''.join([str(i) for i in self.preOrderLst]))

    def __eq__(self, x):
        return isinstance(x, formula) and self.preOrderLst == x.preOrderLst

    def getPreOrderLst(self): return self.preOrderLst

    def getInOrderLst(self): return self.inOrderLst

    def isValid(self):
        return self.validSub(self.preOrderLst)[0]

    def isNonType(self):
        '''return  True if it's ~p form'''
        return self.preOrderLst[0] == NON

    def validSub(self, s=None, begin=0, end=None):
        '''
            check a *preOrder-list* s from left of its preOrderLst
            until forming a valid proposition
            return ('if s[begin:end] froms a  valid prop' , the index)
            return:  (bool,int)
        '''

        weight = {NON: 0, CONTAIN: -1}  # proposition varible :1
        if s is None:
            s = self.preOrderLst

        def w(sym):
            return weight[sym] if sym in weight else 1

        ct, i = 0, begin
        n = len(s) if end is None else end
        while ct != 1 and i != n:
            ct += w(s[i])
            i += 1
        return (ct == 1 and i == n, i)

    def getPairs(self):
        '''return Pairs of formulas likr[(p,q)...] after applying enough p2p func,
            eg q>(~r>(~t>s)): return [(q,~r>(~t>s)),(~r,~t>s),(~t,s)]
        '''
        s = []
        cur = self
        while 1:
            p, q = cur.p2q()
            if q is None:
                return s
            s.append(PAIR(p, q))
            cur = q

    def p2q(self, fm=None):
        '''
            if f can be formed in the form of  p->q:  return (p,q),  
            else return f,None
            p,q,f are all formula s
        '''
        if fm is None:
            fm = self
        f = fm.preOrderLst
        n = len(f)
        ct, i = self.getContNonNum(f, 0)
        if n >= 3 and ct % 2 == 0 and f[i] == CONTAIN:
            _, i = self.validSub(f, begin=i+1)
            if i != n:
                return formula(f[1:i]), formula(f[i:])
        return fm, None

    def getContNonNum(self, s=None, i=0):
        '''
            visit s from i until s[i] isn't NON,
            then return the num of continuous NON  and the pointer i
        '''
        if s is None:
            s = self.preOrderLst
        ct = 0
        while s and s[i] == NON:
            i += 1
            ct += 1
        return ct, i

    def pre2in(self, li, begin=0):
        ''' li is a list of preorder symbols repring a proposition
            this func converts it to preorder form(probably  contains parentheses)
        '''
        def addParentheses(li):
            return [LEFT]+li + [RIGHT] if len(li) >= 3 else li

        self.pt = begin

        if not li:
            return []
        if li[self.pt] == NON:
            ct, self.pt = self.getContNonNum(li, self.pt)
            nn = [NON] if ct % 2 == 1 else []
            if li[self.pt] == CONTAIN:
                return nn + addParentheses(self.pre2in(li, self.pt))
            else:
                nn.append(li[self.pt])
                self.pt += 1
                return nn
        elif li[self.pt] == CONTAIN:
            self.pt += 1
            ct, lst = 0, []
            last = self.pt
            while ct != 1:
                tmp = li[self.pt]
                self.pt += 1
                if not isConn(tmp):
                    ct += 1
                elif tmp == CONTAIN:
                    ct -= 1
            return addParentheses(self.pre2in(li, last)) \
                + [CONTAIN] + addParentheses(self.pre2in(li, self.pt))
        else:
            self.pt += 1
            return [li[self.pt-1]]


class system_L:
    def __init__(self):
        pass

    def l1(self, p, q):
        '''p->(q->p)'''
        return contain(p, contain(q, p))

    def l2(self, p, q, r):
        '''p->(q->r)'''
        origin = contain(p, contain(q, r))
        new = contain(contain(p, q), contain(p, r))
        return contain(origin, new)

    def l3(self, p, q):
        '''~p->~q -> (p->q)'''
        left = contain(non(p), non(q))
        right = contain(p, q)
        return contain(left, right)

    def genFormula(self, s: str)->formula:
        s = s.replace('~~', '')  # simplify the deduction,  to do
        s = s.replace('<->', '-')
        # to do
        s = s.replace('->', '>')
        li = re.findall(r'[\(\)\>\~]|\w+', s)
        li = [sympy.Symbol(i) for i in li]
        s = in2pre(li)
        return formula(s)

    def addL1(self, i, p, q, tmp_mp):
        '''i = p>q,加入由 否定前件律 或 L1 得来的公式'''
        if not p.isNonType():
            #  p>q or p>~q: get  ~p>(p>q)
            tmp_mp[contain(non(p), i)] = ([], '否定前件律')
        if not q.isNonType():
            # p>q  :  get theorem  q>(p>q)
            tmp_mp[contain(q, i)] = ([], 'L1')

    def addMP(self, i, p, q, tmp_mp):
        '''i=p>q 加入由 换位律 或 MP 得来的公式'''
        if p.isNonType() and q.isNonType():
            # p=~a,q=~b:   ~a->~b ->(b->a)
            nonpq = contain(non(q), non(p))
            comb = contain(i, nonpq)
            tmp_mp[comb] = ([], 'L3')
            tmp_mp[nonpq] = ([i, comb], 'MP')
        elif not p.isNonType() and not q.isNonType():
            # p->q ->(~q->~p)
            pq = contain(non(q), non(p))
            comb = contain(i, pq)
            tmp_mp[comb] = ([], '换位律')

            tmp_mp[pq] = ([i, comb], 'MP')

    def addTheo(self, li, mp):
        def _iterLst(li, f):
            tmp_mp = {}
            for i in li:
                p, q = i.p2q()
                if q is None:
                    i = non(i)
                    p, q = i.p2q()
                if q is None:
                    continue
                f(i, p, q, tmp_mp)
            return tmp_mp

        tmp_mp = _iterLst(li, self.addMP)
        tmp_mp.update(_iterLst(li, self.addMP))
        for i in tmp_mp:
            if i not in mp:
                mp[i] = tmp_mp[i]

        lst = [i.pre for p in mp for i in p.getPairs() if i not in mp]
        tmp_mp = _iterLst(lst, self.addL1)
        for i in tmp_mp:
            if i not in mp:
                mp[i] = tmp_mp[i]

    def mpDeduce(self, formulas, x, mp=None):

        def getIdx(x):
            '''insert x in deduction and get idx of it, var ct, mp is in the outer func'''
            if x in appeared:
                return appeared[x]
            li, wds = mp[x]
            for p in li:
                wds += ' [{}]'.format(getIdx(p))
            deduction.append((x, wds))
            nonlocal ct
            ct += 1
            appeared[x] = ct
            return ct

        def _mpDeduce(x):
            if x in proved:
                return mp[x] if x in mp else None
            proved[x] = True
            if x in mp:
                return mp[x]

            li = []
            # x在fomrulas 中的 可能的证明: [p1,p2,p3...,x]  的列表

            for p in mp:
                pairs = p.getPairs()
                for idx, pair in enumerate(pairs):
                    if pair.suf == x:
                        li.append(pairs[:idx+1])
                        break

            for pairs in li:
                for pre, suf in pairs:
                    if suf in mp:
                        continue
                    tmp = _mpDeduce(pre)
                    if tmp is not None:
                        mp[pre] = tmp
                        mp[suf] = ([pre, contain(pre, suf)], 'MP')
                    else:
                        break
                else:
                    return mp[x]
            return None

        if mp is None:
            mp = {i: ([], '假定') for i in formulas}
        proved = {}
        tmp = _mpDeduce(x)
        if tmp is None:
            return None
        mp[x] = tmp
        ct, deduction, appeared = 0, [], {}
        tmp = getIdx(x)
        return deduction

    def nonDeduce(self, formulas, x, mp=None):
        '''反证法,归谬法'''
        if mp is None:
            mp = {i: ([], '假定') for i in formulas}
        mp[non(x)] = ([], '假定')
        formulas.append(non(x))
        self.addTheo([non(x)], mp)
        nonSet = []
        for i in mp:
            if i.isNonType():
                nonSet.append(i)
            pairs = i.getPairs()
            if pairs and pairs[-1].suf.isNonType():
                nonSet.append(pairs[-1].suf)

        meth = '归谬法' if x.isNonType() else '反证法'

        for i in nonSet:
            p1 = self.mpDeduce(formulas, i, mp)
            p2 = self.mpDeduce(formulas, non(i), mp)
            if p1 is None or p2 is None:
                continue
            else:
                s = '由{meth},即证: \n(1) {{{formulas}}} |- {p}\n(2) {{{formulas}}} |- {nonp}'\
                    .format(meth=meth, formulas=','.join([str(i) for i in formulas]), p=i, nonp=non(i))
                return s, p1, p2
        return None, None, None

    def prove(self, formulas, x):
        print('*'*65)
        x = self.genFormula(x)
        formulas = [self.genFormula(i) for i in formulas]
        print(
            '证明: {{{}}} |- {}'.format(', '.join([str(i) for i in formulas]), x))

        # 演绎定理　　syllogism
        origin = x
        pairs = x.getPairs()
        if pairs:
            formulas += [i[0] for i in pairs]
            x = pairs[-1].suf
            print(
                '由演绎定理,即证  {{{}}} |- {} '.format(', '.join([str(i) for i in formulas]), x))

        mp = {i: ([], '假定') for i in formulas}
        self.addTheo(mp.keys(), mp)  # get some theorem

        # MP  modus ponous
        p = self.mpDeduce(formulas, x, mp)

        if p is None:
            # 反证,归谬
            s, prv1, prv2 = self.nonDeduce(formulas, x, mp)
            if s is None:
                print("Sorry! I can't prove this proposition. Maybe it's unprovale ")
            else:
                print(s)
                print('证明(1)')
                self.display(prv1)
                print('证明(2)')
                self.display(prv2)
        else:
            self.display(p)
        print('*'*65)
        print('\n')

    def display(self, props):
        for i, (f, wds) in enumerate(props):
            print('[{}]: {}{explan}'.format(
                i+1, str(f).ljust(50, '-'), explan=wds))


def random_prop(prop=formula([sympy.Symbol('p')]),
                symbols=sympy.symbols('p q r s t'), n=15):
    def addLevel(p, sig):
        if sig == 0:
            return non(p)
        else:
            cur = fs[randint(0, len(fs)-1)]
            if randint(0, 1) == 0:
                return contain(cur, p)
            else:
                return contain(p, cur)
    fs = [formula([i]) for i in symbols]
    for i in range(n):
        prop = addLevel(prop, randint(0, 1))
    return prop