path: root/Logic.icl

/**
 * 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 e)        = show opt op +++ show opt e
    show opt (App2 e1 op e2)    = show opt e1 +++ " " +++ show opt op +++ " " +++ show opt 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 = [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}

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 = 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 = removeDup (flatten (map all_atom_options es))}

compute :: TruthTable -> FilledTruthTable   // Fill in a truthtable
compute table=:{exprs,options} = {table=table, values=values}
where
    values = [[toMaybeBool val \\ val <- map (eval o substitute_all options`) exprs] \\ options` <- options]
    toMaybeBool [] = Nothing
    toMaybeBool [b:bs] = 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