Combinators for logic programming (Haskell98)

combinators_for_logic.hs

-- Authors: Mike Spivey and Silvija Seres
-- Taken from: https://www.cs.ox.ac.uk/publications/books/fop/dist/fop/chapters/9/Logic.hs,
-- "The fun of programming book", https://www.cs.ox.ac.uk/publications/books/fop/,
-- Chapter 9, Combinators for logic programming
-- Haskell 98 compliant.

module Logic where
import List

-- Section 9.2

-- factor :: Int -> [(Int,Int)]
-- factor n = [(r,s) | r <- [1..], s <- [1..], r*s == n]
-- factor n = [(r,s) | (r,s) <- diagprod [1..] [1..], r*s==n]

diagprod :: [a] -> [b] -> [(a,b)]
diagprod xs ys = [(xs!!i,ys!!(n-i)) | n <- [0..], i <- [0..n]]

-- Section 9.3

type Stream a = [a]

newtype Diag a = MkDiag (Stream a)
   deriving Show

unDiag (MkDiag xs) = xs

instance Monad Diag where
   return x = MkDiag [x]
   MkDiag xs >>= f = MkDiag (concat (diag (map (unDiag . f) xs)))

diag :: Stream (Stream a) -> Stream [a]
diag [] = []
diag (xs:xss) = lzw (++) [[x] | x <- xs] ([] : diag xss)

lzw :: (a -> a -> a) -> [a] -> [a] -> [a]
lzw f [] ys = ys
lzw f xs [] = xs
lzw f (x:xs) (y:ys) = f x y : lzw f xs ys

-- Section 9.4

class Monad m => Bunch m where
   zero :: m a
   alt :: m a -> m a -> m a
   wrap :: m a -> m a

instance Bunch [] where
   zero = []
   alt xs ys = xs ++ ys
   wrap xs = xs

instance Bunch Diag where
   zero = MkDiag []
   alt (MkDiag xs) (MkDiag ys) = MkDiag (shuffle xs ys)
   wrap xm = xm

shuffle [] ys = ys
shuffle (x:xs) ys = x : shuffle xs ys

test :: Bunch m => Bool -> m ()
test b = if b then return () else zero

-- Section 9.5

newtype Matrix a = MkMatrix (Stream [a])
    deriving Show

unMatrix (MkMatrix xm) = xm

instance Monad Matrix where
   return x = MkMatrix [[x]]
   MkMatrix xm >>= f = MkMatrix (bindm xm (unMatrix.f))

instance Bunch Matrix where
   zero = MkMatrix []
   alt (MkMatrix xm) (MkMatrix ym) = MkMatrix (lzw (++) xm ym)
   wrap (MkMatrix xm) = MkMatrix ([]:xm)

-- bindm :: Stream [a] -> (a -> Stream [b]) -> Stream [b]
-- bindm xm f = [ row n | n <- [0..]]
--   where row n = [y | k <- [0..n], x <- xm!!k , y <- (f x)!!(n-k)]

concatAll :: [Stream [b]] -> Stream [b]
concatAll = foldr (lzw (++)) []

bindm xm f = map concat (diag (map (concatAll.map f) xm))

intMat = MkMatrix [[n] | n <- [1..]]

-- Section 9.6

choose :: Bunch m => Stream a -> m a
choose (x:xs) = wrap (return x `alt` choose xs)

factor :: Bunch m => Int -> m (Int,Int)
factor n = do r <- choose [1..] 
              s <- choose [1..]
              test (r*s==n)
              return (r,s)

-- Section 9.7

data Term = Int Int | Nil | Cons Term Term | Var Variable
    deriving Eq

data Variable = Named String | Generated Int
    deriving (Show,Eq)

var :: String -> Term
var s = Var (Named s)

list :: [Int] -> Term
list xs = foldr Cons Nil (map Int xs)

-- Subst, apply, idSubst and unify defined below

type Pred m = Answer -> m Answer
newtype Answer = MkAnswer (Subst,Int)

initial :: Answer
initial = MkAnswer (idsubst,0)

run :: Bunch m => Pred m -> m Answer
run p = p initial

-- Section 9.8

(=:=) :: Bunch m => Term -> Term -> Pred m
(t =:= u) (MkAnswer (s,n)) = 
   case unify s (t,u) of
     Just s' -> return (MkAnswer (s',n))
     Nothing -> zero


(&&&) :: Bunch m => Pred m -> Pred m -> Pred m
(p &&& q) s = p s >>= q

(|||) :: Bunch m => Pred m -> Pred m -> Pred m
(p ||| q) s = alt (p s) (q s)

exists :: Bunch m => (Term -> Pred m) -> Pred m
exists p (MkAnswer (s,n)) =
  p (Var (Generated n)) (MkAnswer (s,n+1))

step :: Bunch m => Pred m -> Pred m
step p s = wrap (p s)

-- Section 9.9

append(p,q,r) =
    step (p =:= Nil &&& q =:= r
            ||| exists (\x -> exists (\a -> exists (\b ->
                  p =:= Cons x a &&& r =:= Cons x b
                    &&& append(a,q,b)))))

good(s) = 
    step (s =:= Cons (Int 0) Nil
           ||| (exists (\t -> exists (\q -> exists (\r ->
                s =:= Cons (Int 1) t &&& append(q,r,t)
                    &&& good(q) &&& good(r))))))

cross :: (a->b) -> (c->d) -> (a,c) -> (b,d)
cross f g (a,c) = (f a, g c)

-- Appendix

infix 5 =:=
infixr 4 &&&
infixl 3 |||


newtype Subst = MkSubst [(Variable,Term)]
idsubst = MkSubst []
extend x t (MkSubst b) = MkSubst ((x,t):b)

apply :: Subst -> Term -> Term
apply s t = case deref s t of
              Cons x xs -> Cons (apply s x) (apply s xs)
              t' -> t'

deref :: Subst -> Term -> Term
deref s@(MkSubst b) (Var v) 
  = head ([deref s t | (u,t) <- b, u==v] ++ [Var v])
deref s t = t

unify :: Subst -> (Term, Term) -> Maybe Subst
unify s (t,u) =
    unify' (deref s t,deref s u)
  where unify' (Nil,Nil) = Just s
        unify' (Cons x xs,Cons y ys) = 
            unify s (x,y) >>= (\s' -> unify s' (xs,ys))
        unify' (Int n,Int m) = if n==m then Just s else Nothing
        unify' (Var x,t) = univar (x,t)
        unify' (t,Var x) = univar (x,t)
        unify' (_,_) = Nothing

        univar (x,t) = if t==Var x then Just s
                       else if occurs s x t then Nothing
                       else Just (extend x t s)

occurs s x t = occurs' s x (deref s t)
    where occurs' s x Nil = False
          occurs' s x (Cons y ys) = occurs s x y || occurs s x ys
          occurs' s x (Int n) = False
          occurs' s x (Var y) = (x==y)


-- Footnote 7 - you could try to improve this output using the pretty printer 
--              in Chapter 11

instance Show Term where 
    show t = pp t

pp Nil = "Nil"
pp (Cons t1 t2) = "[" ++ pp t1 ++ pp_tail t2 ++ "]"
pp (Int n) = show n
pp (Var (Named s)) = s
pp (Var (Generated n)) = "_g" ++ show n

pp_tail Nil = ""
pp_tail (Cons t1 t2) = "," ++ pp t1 ++ pp_tail t2
pp_tail t = "|" ++ pp t

instance Show Subst where
   show (s @ (MkSubst b)) =
     "{" ++ joinwith "," (map showb (sort vars)) ++ "}"

        where showb x = x ++ "=" ++ show (apply s (Var (Named x)))
              vars = [x | (Named x,_) <- b]

              showg n = "_g" ++ show n ++ "=" 
                             ++ show (apply s (Var (Generated n)))
              gvars = [n | (Generated n,_) <- b]

joinwith sep [] = ""
joinwith sep [s] = s
joinwith sep (s:ss) = s ++ sep ++ joinwith sep ss

instance Show Answer where show (MkAnswer (s,n)) = show s