module Robinson where

type TCon  = (String,Int) -- Name, Stelligkeit
data Types = TVar String 
           | SType TCon [Types]
           | FType Types Types
           deriving Eq
type Subst = [(String,Types)]

-- zentrale Unifikationsfunktion
-- Ausgabe Nothing bedeutet fail
unify :: Types -> Types -> Maybe Subst
unify (TVar cs) t 
    | occursNot cs t = Just [(cs,t)]
    | otherwise      = Nothing
unify t (TVar cs) 
    | occursNot cs t = Just [(cs,t)]
    | otherwise      = Nothing
unify (SType tcon1 ts1) (SType tcon2 ts2)
    | tcon1 == tcon2 = unifylist ts1 ts2 []
    | otherwise      = Nothing
unify (FType t11 t12) (FType t21 t22) 
                     = unifylist [t11,t12] [t21,t22] []
unify _ _            = Nothing


-- Unifikation von mehreren Gleichungen
unifylist :: [Types] -> [Types] -> Subst
             -> Maybe Subst
unifylist [] [] sigma  = Just sigma
unifylist (t1:ts1) (t2:ts2) sigma 
    =  case unify (applySubst sigma t1)
                  (applySubst sigma t2) of
         Nothing       -> Nothing
         (Just sigma1) -> unifylist ts1 ts2 sigma1
                    

applySubst :: Subst -> Types -> Types
applySubst sigma (TVar cs)  
   = head ([ t | (tv,t) <- sigma, 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 = printResult $ 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"))
           ]
           []

-- Ausgabefunktionen           
printSubst  :: Subst -> String
printSubst  =  unlines . map (\ (cs,typ) -> cs ++ " |-> " ++ show typ)

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 ++ ")"
    
printResult              :: Maybe Subst -> IO ()
printResult Nothing      =  putStr "Nothing" 
printResult (Just sigma) =  putStr $ printSubst sigma