#!/usr/bin/env python3
# ----------------------------------
#
# Module knf.py

"""
This program implements the conversion to clause normal form.

Copyright 2018 Stephan Schulz, schulz@eprover.org

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program ; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston,
MA  02111-1307 USA

The original copyright holder can be contacted as

Stephan Schulz
Auf der Altenburg 7
70376 Stuttgart
Germany
Email: schulz@eprover.org
"""

import unittest
import sys
import getopt
from lexer import Lexer, Token
from prop_formula import PropFormula, parseForm,PropFormulaSetPrintStyle


tex = False

def processOptions(opts):
    """
    Process the options given. The only one so far is to run unit
    tests. By default, read and print back a set of arithmetic
    expressions.
    """
    global tex

    for opt, optarg in opts:
        if opt == "-t" or opt == "--tex":
            PropFormulaSetPrintStyle("tex")
            tex = True


def elimEquiv(formula):
    res = []
    while formula.hasOp("<=>"):
        formula = formula.elimFirstEquiv()
        res.append(formula)
    return formula, res


def elimImpl(formula):
    res = []
    while formula.hasOp("->"):
        formula = formula.elimFirstImpl()
        res.append(formula)
    return formula, res



def printStepTex(formula, reason):
    print("   \\equiv  & ", formula, " & \\text{", reason, "\\\\")


def printStepTxt(formula, reason):
    if type(formula) != type("a"):
        formula = repr(formula)
    print("%-60s  %s"%(formula, reason))


printStep = printStepTxt

def printSteps(form, reason):
    for f in form:
        printStep(f, reason)



if __name__ == '__main__':

    opts, args = getopt.gnu_getopt(sys.argv[1:],
                                   "t",
                                   ["tex"])

    PropFormulaSetPrintStyle("txt")
    processOptions(opts)

    for file in args:
        fp = open(file, "r")
        input = fp.read()
        fp.close()

        lex = Lexer(input)
        while(not lex.TestTok(Token.EOFToken)):
            expr = parseForm(lex)
            if tex:
                print("\\begin{array}{rll}")
                print("           & ", expr, "& \\\\")
                print("           & ", expr.__str3__(), "& (full parentheses) \\\\")
                expr = expr.elimEquiv()
                print("   \\equiv  & ", expr, " & \\text{ Aufl{\"osen} $\lequiv$}\\\\")
                expr = expr.elimImpl()
                print("   \\equiv  & ", expr, " & \\text{ Aufl{\"osen} $\limpl$}\\\\")
                expr = expr.shiftNeg()
                print("   \\equiv  & ", expr, " & \\text{ NNF}\\\\")
                expr = expr.distributeOr()
                print("   \\equiv  & ", expr, " & \\text{ KNF}\\\\")
                print("\\end{array}")
            else:
                printStep(expr, "Original")
                printStep(expr.__str3__(), "Original (full parentheses)")
                expr, steps = elimEquiv(expr)
                printSteps(steps, "<=> eliminated")
                expr, steps = elimImpl(expr)
                printSteps(steps, "-> eliminated")
                expr = expr.shiftNeg()
                printStep(expr, "NNF")
                expr = expr.distributeOr()
                printStep(expr, "KNF")