module Robinson where

type TCon  = (String,Int) -- Name, Stelligkeit
data Types = TVar String 
           | SType TCon [Types]
           | FType Types Types
           deriving Eq
newtype Subst = S [(String, Types)]
data Result a = Fail | Success a

-- zentrale Unifikationsfunktion
unify :: Types -> Types -> Result Subst
unify (TVar cs1) (TVar cs2) 
    | cs1 == cs2     = Success $ S []
    | otherwise      = Success $ S [(cs1,(TVar cs2))]
unify (TVar cs) t 
    | occursNot cs t = Success $ S [(cs,t)]
    | otherwise      = Fail
unify t (TVar cs) 
    | occursNot cs t = Success $ S [(cs,t)]
    | otherwise      = Fail
unify (SType tcon1 ts1) (SType tcon2 ts2)
    | tcon1 == tcon2 = unifylist ts1 ts2 (S [])
    | otherwise      = Fail
unify (FType t11 t12) (FType t21 t22) 
                     = unifylist [t11,t12] [t21,t22] (S [])
unify _ _            = Fail


-- Unifikation von mehreren Gleichungen
unifylist :: [Types] -> [Types] -> Subst
             -> Result Subst
unifylist [] [] sigma  = Success sigma
unifylist (t1:ts1) (t2:ts2) sigma 
    =  case unify (applySubst sigma t1)
                  (applySubst sigma t2) of
         Fail       -> Fail
         (Success sigma1) -> unifylist ts1 ts2 (join sigma sigma1)


-- Hintereinanderausfuehrung von Substitutionen 
join :: Subst -> Subst -> Subst
join (S sts1) delta@(S sts2) 
  = S ([(tv, applySubst delta t) | (tv,t) <- sts1]
                     ++ sts2)


applySubst :: Subst -> Types -> Types
applySubst (S sts) (TVar cs)  
   = head ([ t | (tv,t) <- sts, tv == cs] ++ [TVar cs])
applySubst sigma (SType tcon ts) 
   = SType tcon (map (applySubst sigma) ts)
applySubst sigma (FType t1 t2)
   = FType (applySubst sigma t1) (applySubst sigma t2)


occursNot :: String -> Types -> Bool
occursNot cs (TVar cs1)      = cs /= cs1
occursNot cs (SType tcon ts) = and (map (occursNot cs) ts)
occursNot cs (FType t1 t2)   = occursNot cs t1 && occursNot cs t2



-- Beispielaufruf
mapBsp = unifylist 
           [ TVar "a3"
           , TVar "a1"
           , FType (TVar "a1") (FType (SType ("List",1) [TVar "a2"]) 
                                      (TVar "a3"))
           , FType (TVar "a7") (FType (SType ("List",1) [TVar "a7"]) 
                                      (SType ("List",1) [TVar "a7"]))
           ]
           [ SType ("List",1) [TVar "a4"]
           , FType (TVar "a2") (TVar "a5")
           , FType (TVar "a1") (FType (SType ("List",1) [TVar "a2"]) 
                                      (TVar "a6"))
           , FType (TVar "a5") (FType (TVar "a6") (TVar "a3"))
           ]
           (S [])          
   
failBsp = unify (SType ("Bool",0) []) (SType ("Int",0) [])
                 
-- Ausgabefunktionen           
instance Show Subst where
   show (S sts) 
     = unlines $ map (\ (cs,typ) -> cs ++ " |-> " ++ show typ) sts

instance Show Types where
   show (TVar cs)         = cs
   show (SType (cs,n) ts) = '(':cs ++ ' ' : concatMap show ts ++ ")"
   show (FType t1 t2)     = '(': show t1 ++ "->" ++ show t2 ++ ")"
    
instance Show a => Show (Result a) where
   show Fail        = "Fehlschlag"
   show (Success s) = show s