import copy

class ForwardChainingProver:
    def __init__(self):
        self.kb_facts = set()
        self.kb_rules = list()

    def add_fact(self, fact: str):        
        self.kb_facts.add(fact)

    def add_rule(self, premises: list, conclusion: str):
        entry = (
            premises,
            conclusion
        )

        self.kb_rules.append(entry)
        

    def forward_chain(self, query: str):

        # inferred table
        # table with all symbols and whether they are true or false
        # {"A1": True, "A2": False}
        inferred = list()

        for f in self.kb_facts:
            inferred.append(f)
        
        print("\ninferred table")
        print(inferred)
        
        q = copy.deepcopy(list(self.rules))
        print()
        print(q)

        while q != []:
            p = q.pop(0)
            print(f"popped {p}")
            
            if p == query:
                return True

        pass

    def print_kb(self):
        print("Facts")
        print(self.kb_facts)
        
        print("\nRules")
        for r in self.kb_rules:
            print(r)        


if __name__ == '__main__':
    print("Forward Chain prover\n")

    prover = ForwardChainingProver()
    #facts
    prover.add_fact("A1")
    prover.add_fact("A2")

    #rules
    prover.add_rule(["A2"], "D1")
    prover.add_rule(["D1"], "B1")
    prover.add_rule(["B1", "A2"], "C1")
    prover.add_rule(["A1", "B1"], "D2")
    prover.add_rule(["D2"], "E1")

    prover.print_kb()

    prover.forward_chain("E1")
