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