/**
 * 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, StdMaybe, 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 == OutputOption
where
	(==) Plain Plain = True
	(==) Html Html = True
	(==) LaTeX LaTeX = True
	(==) _ _ = False

instance show Bool
where
	show LaTeX True	 = "\\top"
	show LaTeX False	= "\\bot"
	show _ b			= toString b

instance show Char
where
	show LaTeX c		= " " +++ toString c
	show _ c			= toString c

instance show Op1
where
	show Plain Not	  = "~"
	show Html Not	   = "¬"
	show LaTeX Not	  = "\\neg"

instance show Op2
where
	show Plain And	  = "&"
	show Plain Or	   = "|"
	show Plain Impl	 = "->"
	show Plain Equiv	= "<->"
	show Html And	   = "&and;"
	show Html Or		= "&or;"
	show Html Impl	  = "&rarr;"
	show Html Equiv	 = "&harr;"
	show LaTeX And	  = "\\land"
	show LaTeX Or	   = "\\lor"
	show LaTeX Impl	 = "\\rightarrow"
	show LaTeX Equiv	= "\\leftrightarrow"

instance show Expr
where
	show opt (B b)			  = show opt b
	show opt (Atom a)		   = show opt a
	show opt (App1 op (App2 x y z)) = show opt op +++ "(" +++ show opt (App2 x y z) +++ ")"
	show opt (App1 op e)		= show opt op +++ show opt e
	show opt (App2 e1 op e2)	= if needs_l "(" "" +++
									show opt e1 +++
									if needs_l ")" "" +++
									" " +++ show opt op +++ " " +++
									if needs_r "(" "" +++
									show opt e2 +++
									if needs_r ")" ""
	where
		needs_l = needs_parentheses_left (App2 e1 op e2)
		needs_r = needs_parentheses_right (App2 e1 op e2)

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 (show Plain e1) < strlen (show Plain 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 = removeDup [opt \\ opt <- all_opts (sort (all_atoms e)) []]
where
	all_opts :: [AtomName] [AtomOption] -> [[AtomOption]]
	all_opts [] opts = [opts]
	all_opts [a:as] opts
		= all_opts as (opts ++ [(a,False)]) ++ all_opts 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}

simple_truthtable_n :: [Expr] -> TruthTable // Simple truthtable with multiple expressions
simple_truthtable_n es = {exprs = removeDup ([Atom a \\ a <- flatten (map all_atoms es)] ++ es), options = removeDup (flatten (map all_atom_options es))}

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

truthtable_n :: [Expr] -> TruthTable
truthtable_n es = {exprs = sort (removeDup (flatten ([[e:subexprs e] \\ e <- es]))), options = removeSubOptions (flatten (map all_atom_options es))}
where
    removeSubOptions :: [[AtomOption]] -> [[AtomOption]]
    removeSubOptions opts = filter (\this -> not (any (\that -> all (flip isMember that) this) (removeMember this opts))) opts

compute :: TruthTable -> FilledTruthTable   // Fill in a truthtable
compute table=:{exprs,options} = {table=table, values=values}
where
	values = [map (toMaybeBool o eval o substitute_all options`) exprs \\ options` <- options]
	toMaybeBool [] = Nothing
	toMaybeBool [b:_] = Just b

instance show FilledTruthTable
where
	show :: OutputOption FilledTruthTable -> String
	show opt t=:{table=table=:{exprs,options},values}
		= begin +++
		  head_b +++
			join head_s [pad_right (showOrNot head_i) header len \\ header <- map (show opt) exprs & len <- padlens] +++
			head_e +++
		  line_b +++
			join line_s [foldr (+++) "" (repeatn len (showOrNot line_i)) \\ len <- padlens] +++
			line_e +++
		  foldr (+++) "" [row_b +++ join row_s [pad_right (showOrNot row_i) (showOrNot v) len \\ v <- r & len <- padlens] +++ row_e \\ r <- values] +++
		  end
	where
		padlens = map ((\l . maxList (map strlen [l,show opt True,show opt False])) o (show opt)) exprs
		// Ideally, we would some kind of DOM writer for Html, but for this project this is sufficient (although not very readable)
		(begin,end) = gen
		gen
		| opt == Plain = ("","")
		| opt == Html  = ("<table>", "</tbody></table>")
		| opt == LaTeX = ("\\begin{tabular}{" +++ join "|" (repeatn (length exprs) "c") +++ "}", "\\end{tabular}")
		(head_b,head_e,head_s,head_i) = head
		head
		| opt == Html = ("<thead><tr><th>", "</th></tr></thead><tbody>", "</th><th>", Nothing)
		| otherwise = row
		(row_b,row_e,row_s,row_i) = row
		row
		| opt == Plain = (" ", " \n", " | ", Just ' ')
		| opt == Html  = ("<tr><td>", "</td></tr>", "</td><td>", Nothing)
		| opt == LaTeX = ("$", "$\\\\", "$&$", Nothing)
		(line_b,line_e,line_s,line_i) = line
		line
		| opt == Plain = ("-", "-\n", "-+-", Just '-')
		| opt == Html  = ("", "", "", Nothing)
		| opt == LaTeX = ("\\hline", "", "", Nothing)
		showOrNot :: (Maybe a) -> String | show a
		showOrNot Nothing = ""
		showOrNot (Just a) = show opt a

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 (show Plain) 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 (" +++ show Plain c +++ ") with too few expressions on the stack:\n" +++ join "," (map (show Plain) 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