import Data.Char  -- in order to use the function "toLower"


data PrologVar = PrologVar Int

instance Eq PrologVar where
  (PrologVar n) == (PrologVar m) = n==m

instance Show PrologVar where
  show (PrologVar n) = "X"++(show n)

data InitialAtomChar = InitalAtomChar Char

instance Eq InitialAtomChar where
    (InitalAtomChar c1)==(InitalAtomChar c2) = (toLower c1)==(toLower c2)


data PrologAtom =  PrologAtom String

instance Show PrologAtom where
     show (PrologAtom [])    = error "no empty string atom allowed!"
     show (PrologAtom [c])   = show c
     show (PrologAtom (c:cs)) = show ((toLower c):cs)

instance Eq PrologAtom where
  (PrologAtom s1) == (PrologAtom s2) = (s1==s2)


type PrologFunSymb = PrologAtom


data PrologTerm =  Var PrologVar | Atom PrologAtom | Apply PrologFunSymb [PrologTerm]

instance Eq PrologTerm where
    (Var pv1) == (Var pv2)                 = (pv1==pv2)
    (Atom pa1)== (Atom pa2)                = (pa1==pa2)
    (Apply pfs1 pts1) == (Apply pfs2 pts2) = (pfs1==pfs2) && 
                                             ((lenght pts1)==(lenght pts2)) &&
                                             (eqList pts1 pts2)  
                                                       where eqList [] [] = True
                                                             eqList (p1:ps1) (p2:ps2) = (p1==p2) &&
                                                                                        (eqList ps1 ps2)
    _          == _         = False                        



instance Show PrologTerm where
    show (Var pv)    = show pv
    show (Atom pa)   = show pa
    show (Apply pfs args) = (show pfs)++"("++(showargs args)++")"
             where showargs []   = ""
                   showargs [arg]  = show arg
                   showargs (arg:args) = (show arg)++","++(showargs args)



-- examples of Prolog terms 

myPrologTerm1 = Apply (PrologAtom "g") [(Apply (PrologAtom "f") [Var (PrologVar 3),Var (PrologVar 3)]), (Var (PrologVar 2))]

myPrologTerm2 = Apply (PrologAtom "g") [(Apply (PrologAtom "f") [Var (PrologVar 5),Var (PrologVar 3)]), (Apply (PrologAtom "h") [Var (PrologVar 6)] )]



type PrologSubst = (PrologTerm -> PrologTerm)


occur :: PrologVar -> PrologTerm -> Bool

occur pv1 (Var pv2)              = (pv1 == pv2)
occur pv  (Atom pa)              = False
occur pv  (Apply pfs [])         = False
occur pv  (Apply pfs (arg:args)) = (occur pv arg) || (occur pv (Apply pfs args) ) 
occur _   _                      = error "First arg of occur must be a variable"


lenght [] = 0

lenght (x:xs) = 1 + (lenght xs)


identity x = x


compose f g x = (f (g x))


mksubst :: PrologVar -> PrologTerm -> PrologSubst


mksubst pv1 pt (Var pv2)             = if (pv1 == pv2) then pt
                                                       else (Var pv2)
mksubst pv pt (Atom pa)              = (Atom pa)

mksubst pv pt (Apply pfs [])         = Apply pfs []

mksubst pv pt (Apply pfs (arg:args)) = Apply pfs ((mksubst pv pt arg):(args >>= \t1 -> [((mksubst pv pt) t1)]))
    





unify :: PrologTerm -> PrologTerm -> (Bool,PrologSubst)  -- subst is identity when non unifiable

unify (Var pv) pt
      | ((Var pv) == pt)      = (True,identity)
      | (not (occur pv pt))   = (True,(mksubst pv pt))

unify (Atom pa1) (Atom pa2)   = if (pa1 == pa2) then (True,identity)
                                                else (False,identity)
unify (Atom pa)  (Var pv)     = unify (Var pv) (Atom pa)

unify (Atom pa)  _            = (False,identity)

unify (Apply pfs args) (Atom pa) = (False,identity)

unify (Apply pfs args) (Var pv)  = unify (Var pv) (Apply pfs args)

unify (Apply pfs1 args1) (Apply pfs2 args2) 
                 | ((pfs1==pfs2) && ((lenght args1)==(lenght args2))) = unifyList args1 args2
                 | otherwise                                          = (False, identity)
                                                              where unifyList []           []            = (True,identity) 
                                                                    unifyList (a1:as1) (a2:as2)  = (b1 && b2, (compose subst1 subst2)) 
                                                                                      where (b1,subst1) = (unify a1 a2)
                                                                                            (b2,subst2) = (unifyList as1 as2)