gistfile1.hs

import Data.List
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as M


data Literal = AtomL String | IntL Int | DoubleL Double deriving (Eq)

data Term = Functor String [Term] 
          | Atomic Literal
          | Variable String deriving (Eq)

instance Show Term where
  show (Functor f ts) | null ts   = f
                      | otherwise = f ++ "(" ++ intercalate "," (map show ts) ++ ")"
  show (Atomic lit) = show lit
  show (Variable v)   = v

instance Show Literal where
  show (AtomL atom) = "'" ++ atom ++ "'"
  show (IntL i)     = show i
  show (DoubleL d)   = show d

newtype Unificator = Unificator (HashMap String Term) deriving (Show)

sample1 = Functor "add" [ Functor "s" [Variable "X"]
                        , Variable "Y"
                        , Functor "s" [Variable "Z"]]

sample2 = Functor "add" [ Functor "s" [Functor "s" [Atomic (IntL 0)]]
                        , Functor "s" [Atomic (IntL 0)]
                        , Variable "N"]

occurs :: String -> Term -> Bool
occurs v (Functor f ts) = any (occurs v) ts
occurs v (Atomic _)     = False
occurs v (Variable u)   = v == u

-- | Sucht den allgemeinsten Unifikator von zwei Termen
--   Eingabe: zwei Terme T1 und T2
--   Ausgabe: Ein allgemeinster Unifikator U für T1 und T2, ansonsten Fehlschlag
-- 1. Wenn T1 und T2 gleiche Konstanten oder Variablen sind, ...
-- 2. Wenn T1 eine Variable ist, die nicht in T2 vorkommt, ...
-- 3. Wenn T2 eine Variable ist, die nicht in T1 vorkommt, ...
-- 4. Falls T1 und T2 Strukturen mit dem gleichen FUnktor un der gleichen Anzahl von Komponenten sind, ...
-- 5. Sonst nicht unifizierbar
unify :: Term -> Term -> Maybe Unificator
unify (Atomic l1) (Atomic l2) | l1 == l2 = Just uniEmpty
unify (Variable v) t   | not $ occurs v t = Just $ Unificator $ M.fromList [(v,t)]
unify t x@(Variable v)                    = unify x t
unify (Functor f1 ts1) (Functor f2 ts2) 
  | f1 == f2 && length ts1 == length ts2 = unifyList ts1 ts2
unify _ _  = Nothing

unifyList :: [Term] -> [Term] -> Maybe Unificator
unifyList [] [] = Just uniEmpty
unifyList (x:xs) (y:ys) = do 
  first <- unify x y
  rest <- unifyList xs ys
  return $ first `uniCat` rest
unifyList _ _ = Nothing

uniEmpty :: Unificator
uniEmpty = Unificator M.empty

applyUnificator :: Unificator -> Term -> Term
applyUnificator (Unificator v) = app where
  app (Functor x xs) = Functor x (map app xs)
  app (Variable x)   = case M.lookup x v of
    Nothing -> Variable x
    Just t  -> t
  app x              = x

uniCat :: Unificator -> Unificator -> Unificator
u@(Unificator a) `uniCat` (Unificator b) = Unificator tmp where
  tmp = a `M.union` fmap (applyUnificator u) b