{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TupleSections #-}
module Kanren.Goal (
Goal,
run,
successo,
failo,
(===),
conj,
conjMany,
disj,
disjMany,
conde,
delay,
(=/=),
Fresh (..),
fresh,
) where
import Control.Applicative (Alternative (..))
import Control.Monad (ap)
import qualified Data.Foldable as Foldable
import Kanren.Core
import qualified Kanren.Core as Core
import Kanren.Stream
infix 4 ===, =/=
infixr 3 `conj`
infixr 2 `disj`
newtype Goal x = Goal {forall x. Goal x -> State -> Stream (State, x)
runGoal :: State -> Stream (State, x)}
instance Functor Goal where
fmap :: forall a b. (a -> b) -> Goal a -> Goal b
fmap a -> b
f (Goal State -> Stream (State, a)
g) = (State -> Stream (State, b)) -> Goal b
forall x. (State -> Stream (State, x)) -> Goal x
Goal ((Stream (State, a) -> Stream (State, b))
-> (State -> Stream (State, a)) -> State -> Stream (State, b)
forall a b. (a -> b) -> (State -> a) -> State -> b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((State, a) -> (State, b))
-> Stream (State, a) -> Stream (State, b)
forall a b. (a -> b) -> Stream a -> Stream b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> b) -> (State, a) -> (State, b)
forall a b. (a -> b) -> (State, a) -> (State, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f)) State -> Stream (State, a)
g)
instance Applicative Goal where
pure :: forall a. a -> Goal a
pure a
x = (State -> Stream (State, a)) -> Goal a
forall x. (State -> Stream (State, x)) -> Goal x
Goal (\State
s -> (State, a) -> Stream (State, a)
forall a. a -> Stream a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (State
s, a
x))
<*> :: forall a b. Goal (a -> b) -> Goal a -> Goal b
(<*>) = Goal (a -> b) -> Goal a -> Goal b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Monad Goal where
return :: forall a. a -> Goal a
return = a -> Goal a
forall a. a -> Goal a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
>> :: forall a b. Goal a -> Goal b -> Goal b
(>>) = Goal a -> Goal b -> Goal b
forall a b. Goal a -> Goal b -> Goal b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
(*>)
Goal State -> Stream (State, a)
g1 >>= :: forall a b. Goal a -> (a -> Goal b) -> Goal b
>>= a -> Goal b
f = (State -> Stream (State, b)) -> Goal b
forall x. (State -> Stream (State, x)) -> Goal x
Goal ((State -> Stream (State, b)) -> Goal b)
-> (State -> Stream (State, b)) -> Goal b
forall a b. (a -> b) -> a -> b
$ \State
s -> do
(State
s', a
x) <- State -> Stream (State, a)
g1 State
s
Goal b -> State -> Stream (State, b)
forall x. Goal x -> State -> Stream (State, x)
runGoal (a -> Goal b
f a
x) State
s'
instance Alternative Goal where
empty :: forall a. Goal a
empty = Goal a
forall a. Goal a
failo
<|> :: forall a. Goal a -> Goal a -> Goal a
(<|>) = Goal a -> Goal a -> Goal a
forall a. Goal a -> Goal a -> Goal a
disj
run :: (Fresh v) => (v -> Goal ()) -> [v]
run :: forall v. Fresh v => (v -> Goal ()) -> [v]
run v -> Goal ()
f = Stream v -> [v]
forall a. Stream a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList Stream v
solutions
where
states :: Stream (State, v)
states = (Goal v -> State -> Stream (State, v))
-> State -> Goal v -> Stream (State, v)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Goal v -> State -> Stream (State, v)
forall x. Goal x -> State -> Stream (State, x)
runGoal State
Core.empty (Goal v -> Stream (State, v)) -> Goal v -> Stream (State, v)
forall a b. (a -> b) -> a -> b
$ do
v
vars <- Goal v
forall v. Fresh v => Goal v
fresh
v -> Goal ()
f v
vars
v -> Goal v
forall a. a -> Goal a
forall (f :: * -> *) a. Applicative f => a -> f a
pure v
vars
solutions :: Stream v
solutions = ((State, v) -> v) -> Stream (State, v) -> Stream v
forall a b. (a -> b) -> Stream a -> Stream b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((State -> v -> v) -> (State, v) -> v
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry State -> v -> v
forall v. Fresh v => State -> v -> v
resolve) Stream (State, v)
states
successo :: x -> Goal x
successo :: forall a. a -> Goal a
successo = x -> Goal x
forall a. a -> Goal a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
failo :: Goal x
failo :: forall a. Goal a
failo = (State -> Stream (State, x)) -> Goal x
forall x. (State -> Stream (State, x)) -> Goal x
Goal (Stream (State, x) -> State -> Stream (State, x)
forall a b. a -> b -> a
const Stream (State, x)
forall a. Stream a
Done)
(===) :: (Logical a) => Term a -> Term a -> Goal ()
Term a
a === :: forall a. Logical a => Term a -> Term a -> Goal ()
=== Term a
b = (State -> Stream (State, ())) -> Goal ()
forall x. (State -> Stream (State, x)) -> Goal x
Goal (Maybe (State, ()) -> Stream (State, ())
forall a. Maybe a -> Stream a
maybeToStream (Maybe (State, ()) -> Stream (State, ()))
-> (State -> Maybe (State, ())) -> State -> Stream (State, ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State -> (State, ())) -> Maybe State -> Maybe (State, ())
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,()) (Maybe State -> Maybe (State, ()))
-> (State -> Maybe State) -> State -> Maybe (State, ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term a -> Term a -> State -> Maybe State
forall a. Logical a => Term a -> Term a -> State -> Maybe State
unify' Term a
a Term a
b)
(=/=) :: (Logical a) => Term a -> Term a -> Goal ()
Term a
a =/= :: forall a. Logical a => Term a -> Term a -> Goal ()
=/= Term a
b = (State -> Stream (State, ())) -> Goal ()
forall x. (State -> Stream (State, x)) -> Goal x
Goal (Maybe (State, ()) -> Stream (State, ())
forall a. Maybe a -> Stream a
maybeToStream (Maybe (State, ()) -> Stream (State, ()))
-> (State -> Maybe (State, ())) -> State -> Stream (State, ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State -> (State, ())) -> Maybe State -> Maybe (State, ())
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,()) (Maybe State -> Maybe (State, ()))
-> (State -> Maybe State) -> State -> Maybe (State, ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term a -> Term a -> State -> Maybe State
forall a. Logical a => Term a -> Term a -> State -> Maybe State
disequality Term a
a Term a
b)
conj :: Goal x -> Goal y -> Goal y
conj :: forall a b. Goal a -> Goal b -> Goal b
conj = Goal x -> Goal y -> Goal y
forall a b. Goal a -> Goal b -> Goal b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
(>>)
conjMany :: [Goal ()] -> Goal ()
conjMany :: [Goal ()] -> Goal ()
conjMany = (Goal () -> Goal () -> Goal ()) -> Goal () -> [Goal ()] -> Goal ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Goal () -> Goal () -> Goal ()
forall a b. Goal a -> Goal b -> Goal b
conj (() -> Goal ()
forall a. a -> Goal a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
disj :: Goal x -> Goal x -> Goal x
disj :: forall a. Goal a -> Goal a -> Goal a
disj Goal x
left Goal x
right = Goal x -> Goal x
forall a. Goal a -> Goal a
delay (Goal x -> Goal x -> Goal x
forall a. Goal a -> Goal a -> Goal a
unsafeDisjunction Goal x
left Goal x
right)
disjMany :: [Goal x] -> Goal x
disjMany :: forall x. [Goal x] -> Goal x
disjMany = Goal x -> Goal x
forall a. Goal a -> Goal a
delay (Goal x -> Goal x) -> ([Goal x] -> Goal x) -> [Goal x] -> Goal x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Goal x] -> Goal x
forall x. [Goal x] -> Goal x
go
where
go :: [Goal x] -> Goal x
go [] = Goal x
forall a. Goal a
failo
go [Goal x
x] = Goal x
x
go (Goal x
x : xs :: [Goal x]
xs@(Goal x
_ : [Goal x]
_)) = Goal x -> Goal x -> Goal x
forall a. Goal a -> Goal a -> Goal a
unsafeDisjunction Goal x
x ([Goal x] -> Goal x
go [Goal x]
xs)
conde :: [[Goal ()]] -> Goal ()
conde :: [[Goal ()]] -> Goal ()
conde = [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany ([Goal ()] -> Goal ())
-> ([[Goal ()]] -> [Goal ()]) -> [[Goal ()]] -> Goal ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Goal ()] -> Goal ()) -> [[Goal ()]] -> [Goal ()]
forall a b. (a -> b) -> [a] -> [b]
map [Goal ()] -> Goal ()
conjMany
class Fresh v where
fresh' :: Goal v
resolve :: State -> v -> v
fresh :: (Fresh v) => Goal v
fresh :: forall v. Fresh v => Goal v
fresh = Goal v -> Goal v
forall a. Goal a -> Goal a
delay Goal v
forall v. Fresh v => Goal v
fresh'
instance Fresh () where
fresh' :: Goal ()
fresh' = () -> Goal ()
forall a. a -> Goal a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
resolve :: State -> () -> ()
resolve State
_ () = ()
instance (Logical a) => Fresh (Term a) where
fresh' :: Goal (Term a)
fresh' = (State -> Stream (State, Term a)) -> Goal (Term a)
forall x. (State -> Stream (State, x)) -> Goal x
Goal ((State, Term a) -> Stream (State, Term a)
forall a. a -> Stream a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((State, Term a) -> Stream (State, Term a))
-> (State -> (State, Term a)) -> State -> Stream (State, Term a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State -> (State, Term a)
forall a. State -> (State, Term a)
makeVariable)
resolve :: State -> Term a -> Term a
resolve = State -> Term a -> Term a
forall a. Logical a => State -> Term a -> Term a
walk'
instance (Fresh a, Fresh b) => Fresh (a, b) where
fresh' :: Goal (a, b)
fresh' = do
a
a <- Goal a
forall v. Fresh v => Goal v
fresh'
b
b <- Goal b
forall v. Fresh v => Goal v
fresh'
(a, b) -> Goal (a, b)
forall a. a -> Goal a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a, b
b)
resolve :: State -> (a, b) -> (a, b)
resolve State
state (a
a, b
b) = (a
a', b
b')
where
a' :: a
a' = State -> a -> a
forall v. Fresh v => State -> v -> v
resolve State
state a
a
b' :: b
b' = State -> b -> b
forall v. Fresh v => State -> v -> v
resolve State
state b
b
instance (Fresh a, Fresh b, Fresh c) => Fresh (a, b, c) where
fresh' :: Goal (a, b, c)
fresh' = do
a
a <- Goal a
forall v. Fresh v => Goal v
fresh'
(b
b, c
c) <- Goal (b, c)
forall v. Fresh v => Goal v
fresh'
(a, b, c) -> Goal (a, b, c)
forall a. a -> Goal a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a, b
b, c
c)
resolve :: State -> (a, b, c) -> (a, b, c)
resolve State
state (a
a, b
b, c
c) = (a
a', b
b', c
c')
where
a' :: a
a' = State -> a -> a
forall v. Fresh v => State -> v -> v
resolve State
state a
a
(b
b', c
c') = State -> (b, c) -> (b, c)
forall v. Fresh v => State -> v -> v
resolve State
state (b
b, c
c)
instance
(Fresh a, Fresh b, Fresh c, Fresh d)
=> Fresh (a, b, c, d)
where
fresh' :: Goal (a, b, c, d)
fresh' = do
a
a <- Goal a
forall v. Fresh v => Goal v
fresh'
(b
b, c
c, d
d) <- Goal (b, c, d)
forall v. Fresh v => Goal v
fresh'
(a, b, c, d) -> Goal (a, b, c, d)
forall a. a -> Goal a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a, b
b, c
c, d
d)
resolve :: State -> (a, b, c, d) -> (a, b, c, d)
resolve State
state (a
a, b
b, c
c, d
d) = (a
a', b
b', c
c', d
d')
where
a' :: a
a' = State -> a -> a
forall v. Fresh v => State -> v -> v
resolve State
state a
a
(b
b', c
c', d
d') = State -> (b, c, d) -> (b, c, d)
forall v. Fresh v => State -> v -> v
resolve State
state (b
b, c
c, d
d)
instance
(Fresh a, Fresh b, Fresh c, Fresh d, Fresh e)
=> Fresh (a, b, c, d, e)
where
fresh' :: Goal (a, b, c, d, e)
fresh' = do
a
a <- Goal a
forall v. Fresh v => Goal v
fresh'
(b
b, c
c, d
d, e
e) <- Goal (b, c, d, e)
forall v. Fresh v => Goal v
fresh'
(a, b, c, d, e) -> Goal (a, b, c, d, e)
forall a. a -> Goal a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a, b
b, c
c, d
d, e
e)
resolve :: State -> (a, b, c, d, e) -> (a, b, c, d, e)
resolve State
state (a
a, b
b, c
c, d
d, e
e) = (a
a', b
b', c
c', d
d', e
e')
where
a' :: a
a' = State -> a -> a
forall v. Fresh v => State -> v -> v
resolve State
state a
a
(b
b', c
c', d
d', e
e') = State -> (b, c, d, e) -> (b, c, d, e)
forall v. Fresh v => State -> v -> v
resolve State
state (b
b, c
c, d
d, e
e)
instance
(Fresh a, Fresh b, Fresh c, Fresh d, Fresh e, Fresh f)
=> Fresh (a, b, c, d, e, f)
where
fresh' :: Goal (a, b, c, d, e, f)
fresh' = do
a
a <- Goal a
forall v. Fresh v => Goal v
fresh'
(b
b, c
c, d
d, e
e, f
f) <- Goal (b, c, d, e, f)
forall v. Fresh v => Goal v
fresh'
(a, b, c, d, e, f) -> Goal (a, b, c, d, e, f)
forall a. a -> Goal a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a, b
b, c
c, d
d, e
e, f
f)
resolve :: State -> (a, b, c, d, e, f) -> (a, b, c, d, e, f)
resolve State
state (a
a, b
b, c
c, d
d, e
e, f
f) = (a
a', b
b', c
c', d
d', e
e', f
f')
where
a' :: a
a' = State -> a -> a
forall v. Fresh v => State -> v -> v
resolve State
state a
a
(b
b', c
c', d
d', e
e', f
f') = State -> (b, c, d, e, f) -> (b, c, d, e, f)
forall v. Fresh v => State -> v -> v
resolve State
state (b
b, c
c, d
d, e
e, f
f)
delay :: Goal a -> Goal a
delay :: forall a. Goal a -> Goal a
delay (Goal State -> Stream (State, a)
g) = (State -> Stream (State, a)) -> Goal a
forall x. (State -> Stream (State, x)) -> Goal x
Goal (Stream (State, a) -> Stream (State, a)
forall a. Stream a -> Stream a
Await (Stream (State, a) -> Stream (State, a))
-> (State -> Stream (State, a)) -> State -> Stream (State, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State -> Stream (State, a)
g)
unsafeDisjunction :: Goal x -> Goal x -> Goal x
unsafeDisjunction :: forall a. Goal a -> Goal a -> Goal a
unsafeDisjunction (Goal State -> Stream (State, x)
g1) (Goal State -> Stream (State, x)
g2) = (State -> Stream (State, x)) -> Goal x
forall x. (State -> Stream (State, x)) -> Goal x
Goal (\State
state -> State -> Stream (State, x)
g1 State
state Stream (State, x) -> Stream (State, x) -> Stream (State, x)
forall a. Stream a -> Stream a -> Stream a
`interleave` State -> Stream (State, x)
g2 State
state)