/**
 * The MIT License (MIT)
 * 
 * Copyright (c) 2015 Camil Staps
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * The above copyright notice and this permission notice shall be included in all
 * copies or substantial portions of the Software.
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 * SOFTWARE.
 */
implementation module Logic

import StdEnv, StringUtils

isBool  :: Expr -> Bool
isBool (B _) = True
isBool _ = False

isAtom  :: Expr -> Bool
isAtom (Atom _) = True
isAtom _ = False

isApp1  :: Expr -> Bool
isApp1 (App1 _ _) = True
isApp1 _ = False

isApp2  :: Expr -> Bool
isApp2 (App2 _ _ _) = True
isApp2 _ = False

isApp   :: Expr -> Bool
isApp e = isApp1 e || isApp2 e

isNot   :: Expr -> Bool
isNot (App1 Not _) = True
isNot _ = False

isAnd   :: Expr -> Bool
isAnd (App2 _ And _) = True
isAnd _ = False

isOr    :: Expr -> Bool
isOr (App2 _ Or _) = True
isOr _ = False

isImpl  :: Expr -> Bool
isImpl (App2 _ Impl _) = True
isImpl _ = False

isEquiv :: Expr -> Bool
isEquiv (App2 _ Equiv _) = True
isEquiv _ = False

apply1 :: Op1 Bool -> Bool
apply1 Not b = not b

apply2 :: Bool Op2 Bool -> Bool
apply2 x And y = x && y
apply2 x Or y = x || y
apply2 x Impl y = y || not x
apply2 x Equiv y = x == y

instance toString Op1
where
    toString Not = "~"

instance toString Op2
where
    toString And = "&"
    toString Or = "|"
    toString Impl = "->"
    toString Equiv = "<->"

instance toString Expr
where
    toString (B b) = toString b
    toString (Atom a) = toString a
    toString (App1 op e)
    | needs_parentheses (App1 op e) = toString op +++ "(" +++ toString e +++ ")"
    | otherwise = toString op +++ toString e
    toString (App2 e1 op e2) = e1` +++ " " +++ toString op +++ " " +++ e2`
    where
        e1`
        | needs_parentheses_left (App2 e1 op e2) = "(" +++ toString e1 +++ ")"
        | otherwise = toString e1
        e2`
        | needs_parentheses_right (App2 e1 op e2) = "(" +++ toString e2 +++ ")"
        | otherwise = toString e2

instance toString TruthTable
where
    toString t=:{exprs,options}
        = row_b +++ join row_s [pad_right ' ' head len \\ head <- map toString exprs & len <- padlens] +++ row_e +++
          line_b +++ join line_s [toString (repeatn len '-') \\ len <- padlens] +++ line_e +++
          foldr (+++) "" [row_b +++ join row_s [pad_right ' ' (toStringOrEmpty val) len \\ val <- map (eval o substitute_all options`) exprs & len <- padlens] +++ row_e \\ options` <- options]
    where
        row_b = " "     // Row / Line begin, end, separator
        row_e = " \n"
        row_s = " | "
        line_b = "-"
        line_e = "-\n"
        line_s = "-+-"
        padlens = map ((max 5) o strlen o toString) exprs // 5 is the length of False
        toStringOrEmpty :: [Bool] -> String
        toStringOrEmpty [] = ""
        toStringOrEmpty [b:bs] = toString b

instance == Op1
where
    (==) Not Not = True

instance < Op1
where
    (<) Not Not = False

instance == Op2
where
    (==) And And = True
    (==) Or Or = True
    (==) Impl Impl = True
    (==) Equiv Equiv = True
    (==) _ _ = False

instance < Op2
where
    (<) op1 op2
    | op1 == op2 = False
    | otherwise = comp op1 op2
    where
        comp And And = False
        comp And _ = True
        comp _ And = False
        comp Or Or = False
        comp Or _ = True
        comp _ Or = False
        comp Impl Impl = False
        comp Impl _ = True
        comp Equiv Equiv = False

instance == Expr
where
    (==) (B b1) (B b2) = b1 == b2
    (==) (Atom a1) (Atom a2) = a1 == a2
    (==) (App1 op e) (App1 op` e`) = op == op` && e == e`
    (==) (App2 e1 op e2) (App2 e1` op` e2`) = e1 == e1` && op == op` && e2 == e2`
    (==) _ _ = False

instance < Expr
where
    (<) e1 e2
    | e1 == e2 = False
    | otherwise = comp e1 e2
    where
        comp (B False) _ = True
        comp _ (B False) = False
        comp (B _) _ = True
        comp _ (B _) = False
        comp (Atom a) (Atom b) = a < b
        comp (Atom _) _ = True
        comp _ (Atom _) = False
        comp (App1 Not e) (App1 Not e`) = e < e`
        comp e1 e2 
        | isMember e1 (subexprs e2) = True
        | isMember e2 (subexprs e1) = False
        | otherwise = strlen (toString e1) < strlen (toString e2)

// Does a the argument of a unary operator need parentheses?
needs_parentheses :: Expr -> Bool
needs_parentheses (App1 Not (B _)) = False
needs_parentheses (App1 Not (Atom _)) = False
needs_parentheses (App1 Not (App1 Not _)) = False
needs_parentheses _ = True

// Does the first argument of a binary operator need parentheses?
needs_parentheses_left :: Expr -> Bool
needs_parentheses_left (App2 (B _) _ _) = False
needs_parentheses_left (App2 (Atom _) _ _) = False
needs_parentheses_left (App2 (App1 Not _) _ _) = False
needs_parentheses_left (App2 (App2 _ op1 _) op2 _) = binds_stronger op2 op1

// Does the second argument of a binary operator need parentheses?
needs_parentheses_right :: Expr -> Bool
needs_parentheses_right (App2 _ _ (B _)) = False
needs_parentheses_right (App2 _ _ (Atom _)) = False
needs_parentheses_right (App2 _ _ (App1 Not _)) = False
needs_parentheses_right (App2 _ op1 (App2 _ op2 _)) = not (binds_stronger op2 op1)

// Associativity rules
binds_stronger :: Op2 Op2 -> Bool
binds_stronger _ And = False        // And is left-associative
binds_stronger And _ = True
binds_stronger Or _ = True          // The rest is right-associative
binds_stronger _ Or = False
binds_stronger Impl _ = True
binds_stronger _ Impl = False
binds_stronger Equiv Equiv = True

all_atoms :: Expr -> [AtomName]
all_atoms (Atom a) = [a]
all_atoms (B _) = []
all_atoms (App1 _ e) = all_atoms e
all_atoms (App2 e1 _ e2) = removeDup (all_atoms e1 ++ all_atoms e2)

all_atom_options :: Expr -> [[AtomOption]]
all_atom_options e = [opt \\ opt <- all_options (all_atoms e) []]
where
    all_options :: [AtomName] [AtomOption] -> [[AtomOption]]
    all_options [] opts = [opts]
    all_options [a:as] opts = all_options as (opts ++ [(a,False)]) ++ all_options as (opts ++ [(a,True)])

substitute :: AtomOption Expr -> Expr
substitute (a,b) (Atom a`)
| a == a` = B b
| otherwise = Atom a`
substitute (a,b) (App1 op e) = App1 op (substitute (a,b) e)
substitute (a,b) (App2 e1 op e2) = App2 (substitute (a,b) e1) op (substitute (a,b) e2)
substitute _ e = e

substitute_all :: [AtomOption] Expr -> Expr
substitute_all opts e = foldr substitute e opts

eval :: Expr -> [Bool]
eval (B b) = [b]
eval (App1 op e) = [apply1 op e` \\ e` <- eval e]
eval (App2 e1 op e2) = [apply2 e1` op e2` \\ e1` <- eval e1 & e2` <- eval e2]
eval _ = []

subexprs :: Expr -> [Expr]
subexprs (B _) = []
subexprs (Atom _) = []
subexprs (App1 op e) = removeDup (subexprs e ++ [e])
subexprs (App2 e1 op e2) = removeDup (subexprs e1 ++ subexprs e2 ++ [e1,e2])

sorted_subexprs :: (Expr -> [Expr])
sorted_subexprs = sort o subexprs

simple_truthtable :: Expr -> TruthTable
simple_truthtable e = {exprs = [Atom a \\ a <- all_atoms e] ++ [e], options = all_atom_options e}

truthtable :: Expr -> TruthTable
truthtable e = {exprs = sorted_subexprs e ++ [e], options = all_atom_options e}

NOT     :== '~'
AND     :== '&'
OR      :== '|'
IMPL    :== '>'
EQUIV   :== '='

parse :: String -> Expr
parse s = parse_stack (shunting_yard (prep s) [] [])
where
    // Make sure every token is ONE character by replacing <-> and ->
    // Remove whitespace
    prep :: String -> [Char]
    prep s
    # s = repl "<->" EQUIV s
    # s = repl "->" IMPL s
    # cs = fromString s
    # cs = removeAll ' ' cs
    = cs
    where 
        removeAll c cs
        | isMember c cs = removeAll c (removeMember c cs)
        | otherwise = cs
    
    // The shunting yard algorithm for propositional logic; see https://en.wikipedia.org/wiki/Shunting-yard_algorithm
    shunting_yard :: [Char] [Char] [Char] -> [Char]
    shunting_yard [] output [] = output
    shunting_yard [] output ['(':_] = abort "Mismatched parentheses"
    shunting_yard [] output [')':_] = abort "Mismatched parentheses"
    shunting_yard [] output [op:operators] = shunting_yard [] (output ++ [op]) operators
    shunting_yard ['(':input] output operators = shunting_yard input output ['(':operators]
    shunting_yard [')':input] output ['(':operators] = shunting_yard input output operators
    shunting_yard [')':input] output [op:operators] = shunting_yard [')':input] (output ++ [op]) operators
    shunting_yard [NOT:input] output operators = shunting_yard input output [NOT:operators]
    shunting_yard [AND:input] output operators 
    | not (isEmpty operators) && (hd operators == NOT || hd operators == AND) = shunting_yard [AND:input] (output ++ [hd operators]) (tl operators)
    | otherwise = shunting_yard input output [AND:operators]
    shunting_yard [OR:input] output operators
    | not (isEmpty operators) && (hd operators == NOT || hd operators == AND) = shunting_yard [OR:input] (output ++ [hd operators]) (tl operators)
    | otherwise = shunting_yard input output [OR:operators]
    shunting_yard [IMPL:input] output operators
    | not (isEmpty operators) && (hd operators == NOT || hd operators == AND || hd operators == OR) = shunting_yard [IMPL:input] (output ++ [hd operators]) (tl operators)
    | otherwise = shunting_yard input output [IMPL:operators]
    shunting_yard [EQUIV:input] output operators
    | not (isEmpty operators) && (hd operators == NOT || hd operators == AND || hd operators == OR || hd operators == IMPL) = shunting_yard [EQUIV:input] (output ++ [hd operators]) (tl operators)
    | otherwise = shunting_yard input output [EQUIV:operators]
    shunting_yard [ip:input] output operators
    | cIsAtom [ip] || cIsBool [ip] = shunting_yard input (output ++ [ip]) operators
    | otherwise = abort ("Unknown character " +++ toString ip)
    
    // Parse the outcome of the shunting yard algorithm into one expression
    parse_stack :: [Char] -> Expr
    parse_stack [] = abort "Cannot parse: empty input"
    parse_stack cs = parse_stack` cs []
    where
        parse_stack` :: [Char] [Expr] -> Expr
        parse_stack` [] [e] = e
        parse_stack` [] [] = abort "Cannot parse: not enough expressoins on the stack"
        parse_stack` [] es = abort ("Cannot parse: too many expressions on the stack:\n" +++ join "\n" (map toString es) +++ "\n")
        parse_stack` [AND:st] [e1:[e2:es]]   = parse_stack` st [App2 e2 And e1:es]
        parse_stack` [OR:st] [e1:[e2:es]]    = parse_stack` st [App2 e2 Or e1:es]
        parse_stack` [IMPL:st] [e1:[e2:es]]  = parse_stack` st [App2 e2 Impl e1:es]
        parse_stack` [EQUIV:st] [e1:[e2:es]] = parse_stack` st [App2 e2 Equiv e1:es]
        parse_stack` [NOT:st] [e:es]           = parse_stack` st [App1 Not e:es]
        parse_stack` [c:st] es
        | cIsAtom [c] = parse_stack` st [Atom (cToAtom [c]) : es]
        | cIsBool [c] = parse_stack` st [B (cToBool [c]) : es]
        parse_stack` [c:st] es = abort ("Cannot parse: tried to perform an operation (" +++ toString c +++ ") with too few expressions on the stack:\n" +++ join "," (map toString es) +++ "\n")

    cIsOp :: [Char] -> Bool
    cIsOp ['~'] = True
    cIsOp ['&'] = True
    cIsOp ['|'] = True
    cIsOp ['->'] = True
    cIsOp ['<->'] = True
    cIsOp _ = False
    
    cIsAtom :: [Char] -> Bool
    cIsAtom [c] = 'a' <= c && c <= 'z' || 'A' <= c && c <= 'Z'
    cIsAtom _ = False
    
    cToAtom :: [Char] -> AtomName
    cToAtom [c:cs] = c
    
    cIsBool :: [Char] -> Bool
    cIsBool ['1'] = True
    cIsBool ['0'] = True
    cIsBool _ = False
    
    cToBool :: [Char] -> Bool
    cToBool ['1'] = True
    cToBool _ = False