{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-|
Module      : ToString 
Description : To print logical formulas
-}
module ToString (toString) where

import Logics

instance Show (Formula a) where
   show f = toString f

instance Show Var where
  show (BVar a) = a
  show (NVar a) = a

instance Show (Expr a) where
  show (BValue v) = show v
  show (Eq m n) = show m ++ "=" ++ show n
  show (LEq m n) = show m ++ "≤" ++ show n
  show (Mul m n) = show m ++ "×" ++ show n
  show (Add m n) = show m ++ "+" ++ show n
  show (BEq p q) = show p ++ "=" ++ show q
  show (B True) = "T"
  show (B False) = "F"
  show (I a) = show a
  show (IValue a) = show a
  show (Xor [b]) = show b
  show (Xor (b:bs)) = show b ++ "⊕" ++ show (Xor bs) 
  show (Or [b]) = show b
  show (Or (b:bs)) = show b ++ "∨" ++ show (Or bs) 
  show (And [b]) = show b
  show (And (b:bs)) = show b ++ "∧" ++ show (And bs) 


instance Show Prog where
  show (Test f) = (toString f) ++ "?"
  show (Sequence []) = ""
  show (Sequence [p]) = show p
  show (Sequence (p:ps)) = show p ++ ";" ++ show (Sequence ps) 
  show (Nondet [] ) = ""
  show (Nondet [p] ) = show p
  show (Nondet (p:ps)) = show p ++ "⊓" ++ show (Sequence ps) 
-- precedence rules to decide parentheses
precedence :: Formula t -> Int
precedence Box{} = 15
precedence ForAllI{} = 13
precedence ForAllB{} = 12
precedence ExistsB{} = 11
precedence ExistsI{} = 11
precedence Atom{} = 10
precedence Neg {} = 9
precedence K{} = 3
precedence Disj{} = 7
precedence Conj{} = 6
precedence Imp{} = 5
precedence Equiv{} = 4

-- precedence rules for numberical expressions
precedenceNE :: NExpr -> Int
precedenceNE I{} = 4
precedenceNE IValue{} = 3
precedenceNE Mul{} = 2
precedenceNE Add{} = 1
--
-- | The main function takes any formula ('FOLFormula' or 'ModalFormula') 
-- and returns a string. The output string is formatted to be parsable by Python.
-- The plan is to use SymPy to remove redundant tautologies.
-- The elimination of the annouce logical operator exploded the size of the formula.
toString :: Formula a -> String
toString = toStringPrec 0
--
toStringNExprPrec :: Int -> NExpr -> String
toStringNExprPrec dCntxt f = bracket unbracketed where
    dHere       = precedenceNE f
    recurse     = toStringNExprPrec dHere
    unbracketed = case f of
        IValue (NVar v)  -> v
        I n -> show n 
        Add e1 e2 -> recurse e1 ++ " + " ++ recurse e2
        Mul e1 e2 -> recurse e1 ++ " * " ++ recurse e2
    bracket
        | dCntxt > dHere = \s -> "(" ++ s ++ ")"
        | otherwise      = id
toStringNExpr :: NExpr -> String
toStringNExpr = toStringNExprPrec 0

toStringPrec :: Int -> Formula a -> String
toStringPrec dCntxt f = bracket unbracketed where
    dHere       = precedence f
    recurse     = toStringPrec dHere
    unbracketed = case f of
        Atom (B t)    -> show t
        Atom (BValue (BVar b))    -> b 
        Atom (BValue (NVar x))   -> x 
        Atom (Xor (bs))  -> "Xor(" ++ separateWithCommas [recurse (Atom b) | b <- bs]  ++ ")"
        Atom (Eq e1 e2)    -> toStringNExpr e1 ++ " = " ++ toStringNExpr e2
        Atom (LEq e1 e2)    -> toStringNExpr e1 ++ " ≤ " ++ toStringNExpr e2
        Atom e -> show e
        K ag p   -> "K_" ++ show (identity ag) ++ " " ++ recurse p
        Neg p   -> "¬" ++ recurse p
        Conj [] -> "True"
        Disj [] -> "False" 
        Conj [p] -> recurse p
        Disj [p] -> recurse p 
        Conj (p:ps) -> recurse p ++ " ∧ " ++ recurse (Conj ps) 
        Disj (p:ps) -> recurse p ++ " ∨ " ++ recurse (Disj ps) 
        Imp p q -> recurse p ++ " ⇒ " ++ recurse q
        Equiv p q -> recurse p ++ " ⇔ " ++ recurse q
        Box prog q -> "[" ++ (show prog) ++ "]" ++ recurse q
        ExistsB b f -> "∃y" ++ show b ++ "⋅"++ recurse f
        ForAllB b f -> "∀u" ++ show b ++ "⋅"++ recurse f
        ExistsI n f -> "∃y" ++ show n ++ "⋅"++ recurse f
        ForAllI n f -> "∀u" ++ show n ++ "⋅"++ recurse f
    bracket
        | dCntxt > dHere = \s -> "(" ++ s ++ ")"
        | otherwise      = id


separateWithCommas :: [String] -> String
separateWithCommas [b] = b
separateWithCommas (b:bs) = b ++ ", " ++ separateWithCommas bs