module Form
( Form(..),  PropSymbol(..), NomSymbol(..), RelSymbol(..), Rel, parse )
where

import HyLo.Signature.Simple( PropSymbol(..),
                              NomSymbol(..),
                              RelSymbol(..) )

import qualified HyLo.InputFile as InputFile
import qualified HyLo.Formula as F

type Rel  = Int

data Form =  Top
           | Bot
           | Prop PropSymbol
           | Nom  NomSymbol
           | Neg  Form
           | Conj [Form]
           | Disj [Form]
           | Impl Form Form
           | A    Form
           | E    Form
           | Box  RelSymbol Form
           | Dia  RelSymbol Form
           | IBox  RelSymbol Form
           | IDia  RelSymbol Form
           | At   NomSymbol Form
           | Down NomSymbol Form
     deriving (Eq,Ord)

instance Show Form where 
   show Top                 = "T"
   show Bot                 = "F"
   show (Prop i)            = show i
   show (Nom i)             = show i
   show (Neg f)             = '-' : show f
   show (Conj [])           = "T" 
   show (Conj fs)           = "(" ++ separate " & " fs ++ ")"
   show (Disj [])           = "F" 
   show (Disj fs)           = "(" ++ separate " v " fs ++ ")"
   show (Impl f1 f2)        = "(" ++ show f1 ++ " -> " ++ show f2 ++ ")"
   show (A f)               = 'A' : show f
   show (E f)               = 'E' : show f
   show (Box name f)        = "[" ++ show name ++ "]" ++ show f
   show (Dia name f)        = "<" ++ show name ++ ">" ++ show f
   show (IBox name f)       = "[-" ++ show name ++ "]" ++ show f
   show (IDia name f)       = "<-" ++ show name ++ ">" ++ show f
   show (At nom f)          = show nom ++ ":" ++ show f
   show (Down i f)          = "down " ++ show i ++ "." ++ show f


parse :: String -> Form
parse = convert . InputFile.parseOldFormat

convert :: [F.Formula NomSymbol PropSymbol RelSymbol] -> Form
convert fs = conv_ $ foldr1 (F.:&:) fs

conv_ :: F.Formula NomSymbol PropSymbol RelSymbol -> Form
conv_ F.Top            = Top
conv_ F.Bot            = Bot
conv_ (F.Prop p)       = Prop p
conv_ (F.Nom n)        = Nom n
conv_ (F.Neg f)        = Neg $ conv_ f
conv_ (f1 F.:&: f2)    = Conj $ flattenConj [conv_ f1,conv_ f2]
conv_ (f1 F.:|: f2)    = Disj $ flattenDisj [conv_ f1,conv_ f2]
conv_ (f1 F.:-->: f2)  = conv_ f1 `Impl` conv_ f2
conv_ (f1 F.:<-->: f2) = Conj [Impl cf1 cf2, Impl cf2 cf1] where cf1 = conv_ f1 ; cf2 = conv_ f2
conv_ (F.Diam r f)     = Dia r (conv_ f)
conv_ (F.Box r f)      = Box r (conv_ f)
conv_ (F.IDiam r f)    = IDia r (conv_ f)
conv_ (F.IBox r f)     = IBox r (conv_ f)
conv_ (F.At n f)       = At n (conv_ f)
conv_ (F.A f)          = A (conv_ f)
conv_ (F.E f)          = E (conv_ f)
conv_ (F.Down v f)     = Down v (conv_ f)
conv_ _ = error "not implemented"

flattenConj :: [Form] -> [Form]
flattenConj []              = []
flattenConj (Conj conjs:fs) = flattenConj conjs ++ flattenConj fs
flattenConj ( f        :fs) = f : flattenConj fs

flattenDisj :: [Form] -> [Form]
flattenDisj []              = []
flattenDisj (Disj disjs:fs) = flattenDisj disjs ++ flattenDisj fs
flattenDisj ( f        :fs) = f : flattenDisj fs

separate :: Show a => String -> [a] -> String
separate _ [] = ""
separate s os = foldl1 (\a1 a2 -> (a1 ++ s ++ a2)) $ map show os