1 --
    2 -- Substitutions and Unification of Prolog Terms
    3 -- Mark P. Jones November 1990
    4 --
    5 -- uses Haskell B. version 0.99.3
    6 --
    7 module Subst(Subst, nullSubst, (->>), (@@), apply, unify) where
    8 
    9 import PrologData
   10 
   11 infixr 3 @@
   12 infix  4 ->>
   13 
   14 --- Substitutions:
   15 
   16 type Subst = Id -> Term
   17 
   18 -- substitutions are represented by functions mapping identifiers to terms.
   19 --
   20 -- apply s   extends the substitution s to a function mapping terms to terms
   21 -- nullSubst is the empty substitution which maps every identifier to the
   22 --           same identifier (as a term).
   23 -- i ->> t   is the substitution which maps the identifier i to the term t,
   24 --           but otherwise behaves like nullSubst.
   25 -- s1 @@ s2  is the composition of substitutions s1 and s2
   26 --           N.B.  apply is a monoid homomorphism from (Subst,nullSubst,(@@))
   27 --           to (Term -> Term, id, (.)) in the sense that:
   28 --                  apply (s1 @@ s2) = apply s1 . apply s2
   29 --                    s @@ nullSubst = s = nullSubst @@ s
   30 
   31 apply                   :: Subst -> Term -> Term
   32 apply s (Var i)          = s i
   33 apply s (Struct a ts)    = Struct a (map (apply s) ts)
   34 
   35 nullSubst               :: Subst
   36 nullSubst i              = Var i
   37 
   38 (->>)                   :: Id -> Term -> Subst
   39 (->>) i t j | j==i       = t
   40             | otherwise  = Var j
   41 
   42 (@@)                    :: Subst -> Subst -> Subst
   43 s1 @@ s2                 = apply s1 . s2 
   44 
   45 --- Unification:
   46 
   47 -- unify t1 t2 returns a list containing a single substitution s which is
   48 --             the most general unifier of terms t1 t2.  If no unifier
   49 --             exists, the list returned is empty.
   50 
   51 unify :: Term -> Term -> [Subst]
   52 unify (Var x)       (Var y)       = if x==y then [nullSubst] else [x->>Var y]
   53 unify (Var x)       t2            = [ x ->> t2 | not (x `elem` varsIn t2) ]
   54 unify t1            (Var y)       = [ y ->> t1 | not (y `elem` varsIn t1) ]
   55 unify (Struct a ts) (Struct b ss) = [ u | a==b, u<-listUnify ts ss ]
   56 
   57 listUnify :: [Term] -> [Term] -> [Subst]
   58 listUnify []     []     = [nullSubst]
   59 listUnify []     (r:rs) = []
   60 listUnify (t:ts) []     = []
   61 listUnify (t:ts) (r:rs) = [ u2 @@ u1 | u1<-unify t r,
   62                                        u2<-listUnify (map (apply u1) ts)
   63                                                      (map (apply u1) rs) ]
   64 
   65 --- End of Subst.hs