module Formula

where

type Name     = String
type Index    = [Int]
type Id       = (Name,Index)
data Term     = Var Id | Struct Id [Term] deriving Eq

instance Ord Term where 
  compare (Var x) (Var y) = compare x y 
  compare (Var x) _       = LT
  compare _       (Var y) = GT 
  compare (Struct a ts) (Struct b rs) | a == b = compare ts rs
                                      | a < b  = LT
                                      | a > b  = GT


data Form =  Atom Id [Term]
           | Eq Term Term
           | Neg Form
           | Conj [Form]
           | Disj [Form]
           | Forall Id Form
           | Exists Id Form
     deriving (Eq,Ord)


showId :: Id -> String
showId (name,[])     = name 
showId (name,ints)   = name ++ ('_': showInts (reverse ints))
  where showInts [] = ""  
        showInts (i:is) = show i ++ showInts is
instance Show Term where 
  show (Var id) = showId id 
  show (Struct ("z",[]) [])                                        = "0"
  show (Struct ("s",[]) [Struct ("z",[]) []])                      = "1"
  show (Struct ("s",[]) [Struct ("s",[]) [Struct ("z",[]) []]])    = "2"
  show (Struct ("s",[]) [Struct ("s",[]) [Struct ("s",[]) 
       [Struct ("z",[]) []]]])                                     = "3"
  show (Struct ("s",[]) [Struct ("s",[]) [Struct ("s",[]) 
       [Struct ("s",[]) [Struct ("z",[]) []]]]])                   = "4"
  show (Struct ("s",[]) [Struct ("s",[]) [Struct ("s",[])  
       [Struct ("s",[]) [Struct ("s",[]) [Struct ("z",[]) []]]]]]) = "5"
  show (Struct id [])   = showId id 
  show (Struct id ts)   = showId id ++ concat [ show ts ]
instance Show Form where 
  show (Atom id []) = showId id 
  show (Atom id ts) = showId id ++ concat [ show ts ]
  show (Eq t1 t2)   = show t1 ++ "==" ++ show t2
  show (Neg form)   = '~': (show form)
  show (Conj []) =  "true" 
  show (Conj fs) =  "conj" ++ concat [ show fs ]
  show (Disj []) =  "false" 
  show (Disj fs) =  "disj" ++ concat [ show fs ]
  show (Forall id f) = "A" ++  showId id ++ (' ' : show f)
  show (Exists id f) = "E" ++  showId id ++ (' ' : show f)