{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Kanren.Example.Tree (example) where

import Control.Lens.TH (makePrisms)
import Data.Function ((&))
import GHC.Generics (Generic)

import Kanren.Core
import Kanren.Goal
import Kanren.LogicalBase ()
import Kanren.Match
import Kanren.TH

data Tree a = Empty | Node a (Tree a) (Tree a)
  deriving (Int -> Tree a -> ShowS
[Tree a] -> ShowS
Tree a -> String
(Int -> Tree a -> ShowS)
-> (Tree a -> String) -> ([Tree a] -> ShowS) -> Show (Tree a)
forall a. Show a => Int -> Tree a -> ShowS
forall a. Show a => [Tree a] -> ShowS
forall a. Show a => Tree a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Tree a -> ShowS
showsPrec :: Int -> Tree a -> ShowS
$cshow :: forall a. Show a => Tree a -> String
show :: Tree a -> String
$cshowList :: forall a. Show a => [Tree a] -> ShowS
showList :: [Tree a] -> ShowS
Show, (forall x. Tree a -> Rep (Tree a) x)
-> (forall x. Rep (Tree a) x -> Tree a) -> Generic (Tree a)
forall x. Rep (Tree a) x -> Tree a
forall x. Tree a -> Rep (Tree a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Tree a) x -> Tree a
forall a x. Tree a -> Rep (Tree a) x
$cfrom :: forall a x. Tree a -> Rep (Tree a) x
from :: forall x. Tree a -> Rep (Tree a) x
$cto :: forall a x. Rep (Tree a) x -> Tree a
to :: forall x. Rep (Tree a) x -> Tree a
Generic)
makeLogical ''Tree
makePrisms ''LogicTree

treeo :: Term (Tree Int) -> Goal ()
treeo :: Term (Tree Int) -> Goal ()
treeo =
  Term (Tree Int) -> Goal ()
forall a x. Term a -> Goal x
matche
    (Term (Tree Int) -> Goal ())
-> ((Term (Tree Int) -> Goal ()) -> Term (Tree Int) -> Goal ())
-> Term (Tree Int)
-> Goal ()
forall a b. a -> (a -> b) -> b
& Prism' (Logic (Tree Int)) ()
-> (() -> Goal ())
-> (Term (Tree Int) -> Goal ())
-> Term (Tree Int)
-> Goal ()
forall a v x.
(Logical a, Fresh v) =>
Prism' (Logic a) v
-> (v -> Goal x) -> (Term a -> Goal x) -> Term a -> Goal x
on p () (f ()) -> p (Logic (Tree Int)) (f (Logic (Tree Int)))
p () (f ()) -> p (LogicTree Int) (f (LogicTree Int))
forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p () (f ()) -> p (LogicTree a) (f (LogicTree a))
Prism' (Logic (Tree Int)) ()
_LogicEmpty () -> Goal ()
forall a. a -> Goal a
forall (m :: * -> *) a. Monad m => a -> m a
return
    (Term (Tree Int) -> Goal ())
-> ((Term (Tree Int) -> Goal ()) -> Term (Tree Int) -> Goal ())
-> Term (Tree Int)
-> Goal ()
forall a b. a -> (a -> b) -> b
& Prism'
  (Logic (Tree Int)) (Term Int, Term (Tree Int), Term (Tree Int))
-> ((Term Int, Term (Tree Int), Term (Tree Int)) -> Goal ())
-> (Term (Tree Int) -> Goal ())
-> Term (Tree Int)
-> Goal ()
forall a v x.
(Logical a, Fresh v) =>
Prism' (Logic a) v
-> (v -> Goal x) -> (Term a -> Goal x) -> Term a -> Goal x
on
      p (Term Int, Term (Tree Int), Term (Tree Int))
  (f (Term Int, Term (Tree Int), Term (Tree Int)))
-> p (Logic (Tree Int)) (f (Logic (Tree Int)))
p (Term Int, Term (Tree Int), Term (Tree Int))
  (f (Term Int, Term (Tree Int), Term (Tree Int)))
-> p (LogicTree Int) (f (LogicTree Int))
forall a a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Term a, Term (Tree a), Term (Tree a))
  (f (Term a, Term (Tree a), Term (Tree a)))
-> p (LogicTree a) (f (LogicTree a))
Prism'
  (Logic (Tree Int)) (Term Int, Term (Tree Int), Term (Tree Int))
_LogicNode
      ( \(Term Int
value, Term (Tree Int)
left, Term (Tree Int)
right) -> do
          Term Int
value Term Int -> Term Int -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term Int
0
          Term (Tree Int) -> Goal ()
treeo Term (Tree Int)
left
          Term (Tree Int) -> Goal ()
treeo Term (Tree Int)
right
      )

inverto :: (Logical a) => Term (Tree a) -> Term (Tree a) -> Goal ()
inverto :: forall a. Logical a => Term (Tree a) -> Term (Tree a) -> Goal ()
inverto Term (Tree a)
tree Term (Tree a)
inverted =
  Term (Tree a)
tree
    Term (Tree a) -> (Term (Tree a) -> Goal ()) -> Goal ()
forall a b. a -> (a -> b) -> b
& ( Term (Tree a) -> Goal ()
forall a x. Term a -> Goal x
matche
          (Term (Tree a) -> Goal ())
-> ((Term (Tree a) -> Goal ()) -> Term (Tree a) -> Goal ())
-> Term (Tree a)
-> Goal ()
forall a b. a -> (a -> b) -> b
& Prism' (Logic (Tree a)) ()
-> (() -> Goal ())
-> (Term (Tree a) -> Goal ())
-> Term (Tree a)
-> Goal ()
forall a v x.
(Logical a, Fresh v) =>
Prism' (Logic a) v
-> (v -> Goal x) -> (Term a -> Goal x) -> Term a -> Goal x
on p () (f ()) -> p (Logic (Tree a)) (f (Logic (Tree a)))
p () (f ()) -> p (LogicTree a) (f (LogicTree a))
forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p () (f ()) -> p (LogicTree a) (f (LogicTree a))
Prism' (Logic (Tree a)) ()
_LogicEmpty (\() -> Term (Tree a)
inverted Term (Tree a) -> Term (Tree a) -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic (Tree a) -> Term (Tree a)
forall a. Logic a -> Term a
Value Logic (Tree a)
LogicTree a
forall a. LogicTree a
LogicEmpty)
          (Term (Tree a) -> Goal ())
-> ((Term (Tree a) -> Goal ()) -> Term (Tree a) -> Goal ())
-> Term (Tree a)
-> Goal ()
forall a b. a -> (a -> b) -> b
& Prism' (Logic (Tree a)) (Term a, Term (Tree a), Term (Tree a))
-> ((Term a, Term (Tree a), Term (Tree a)) -> Goal ())
-> (Term (Tree a) -> Goal ())
-> Term (Tree a)
-> Goal ()
forall a v x.
(Logical a, Fresh v) =>
Prism' (Logic a) v
-> (v -> Goal x) -> (Term a -> Goal x) -> Term a -> Goal x
on
            p (Term a, Term (Tree a), Term (Tree a))
  (f (Term a, Term (Tree a), Term (Tree a)))
-> p (Logic (Tree a)) (f (Logic (Tree a)))
p (Term a, Term (Tree a), Term (Tree a))
  (f (Term a, Term (Tree a), Term (Tree a)))
-> p (LogicTree a) (f (LogicTree a))
forall a a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Term a, Term (Tree a), Term (Tree a))
  (f (Term a, Term (Tree a), Term (Tree a)))
-> p (LogicTree a) (f (LogicTree a))
Prism' (Logic (Tree a)) (Term a, Term (Tree a), Term (Tree a))
_LogicNode
            ( \(Term a
value, Term (Tree a)
left, Term (Tree a)
right) -> do
                (Term (Tree a)
invertedLeft, Term (Tree a)
invertedRight) <- Goal (Term (Tree a), Term (Tree a))
forall v. Fresh v => Goal v
fresh
                Term (Tree a)
inverted Term (Tree a) -> Term (Tree a) -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic (Tree a) -> Term (Tree a)
forall a. Logic a -> Term a
Value (Term a -> Term (Tree a) -> Term (Tree a) -> LogicTree a
forall a. Term a -> Term (Tree a) -> Term (Tree a) -> LogicTree a
LogicNode Term a
value Term (Tree a)
invertedLeft Term (Tree a)
invertedRight)
                Term (Tree a) -> Term (Tree a) -> Goal ()
forall a. Logical a => Term (Tree a) -> Term (Tree a) -> Goal ()
inverto Term (Tree a)
left Term (Tree a)
invertedRight
                Term (Tree a) -> Term (Tree a) -> Goal ()
forall a. Logical a => Term (Tree a) -> Term (Tree a) -> Goal ()
inverto Term (Tree a)
right Term (Tree a)
invertedLeft
            )
      )

--    4
--  2   6
-- 1 3 5 7
exampleTree :: Tree Int
exampleTree :: Tree Int
exampleTree =
  Int -> Tree Int -> Tree Int -> Tree Int
forall a. a -> Tree a -> Tree a -> Tree a
Node
    Int
4
    (Int -> Tree Int -> Tree Int -> Tree Int
forall a. a -> Tree a -> Tree a -> Tree a
Node Int
2 (Int -> Tree Int
forall {a}. a -> Tree a
leaf Int
1) (Int -> Tree Int
forall {a}. a -> Tree a
leaf Int
3))
    (Int -> Tree Int -> Tree Int -> Tree Int
forall a. a -> Tree a -> Tree a -> Tree a
Node Int
6 (Int -> Tree Int
forall {a}. a -> Tree a
leaf Int
5) (Int -> Tree Int
forall {a}. a -> Tree a
leaf Int
7))
 where
  leaf :: a -> Tree a
leaf a
x = a -> Tree a -> Tree a -> Tree a
forall a. a -> Tree a -> Tree a -> Tree a
Node a
x Tree a
forall a. Tree a
Empty Tree a
forall a. Tree a
Empty

example :: IO ()
example :: IO ()
example = do
  String -> IO ()
putStrLn String
"trees:"
  (Maybe (Tree Int) -> IO ()) -> [Maybe (Tree Int)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Maybe (Tree Int) -> IO ()
forall a. Show a => a -> IO ()
print ([Maybe (Tree Int)] -> IO ()) -> [Maybe (Tree Int)] -> IO ()
forall a b. (a -> b) -> a -> b
$ Term (Tree Int) -> Maybe (Tree Int)
forall a. Logical a => Term a -> Maybe a
extract' (Term (Tree Int) -> Maybe (Tree Int))
-> [Term (Tree Int)] -> [Maybe (Tree Int)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [Term (Tree Int)] -> [Term (Tree Int)]
forall a. Int -> [a] -> [a]
take Int
10 ((Term (Tree Int) -> Goal ()) -> [Term (Tree Int)]
forall v. Fresh v => (v -> Goal ()) -> [v]
run Term (Tree Int) -> Goal ()
treeo)

  String -> IO ()
putStrLn String
"\ninverto example:"
  (Maybe (Tree Int) -> IO ()) -> [Maybe (Tree Int)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Maybe (Tree Int) -> IO ()
forall a. Show a => a -> IO ()
print ([Maybe (Tree Int)] -> IO ()) -> [Maybe (Tree Int)] -> IO ()
forall a b. (a -> b) -> a -> b
$ Term (Tree Int) -> Maybe (Tree Int)
forall a. Logical a => Term a -> Maybe a
extract' (Term (Tree Int) -> Maybe (Tree Int))
-> [Term (Tree Int)] -> [Maybe (Tree Int)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term (Tree Int) -> Goal ()) -> [Term (Tree Int)]
forall v. Fresh v => (v -> Goal ()) -> [v]
run (Term (Tree Int) -> Term (Tree Int) -> Goal ()
forall a. Logical a => Term (Tree a) -> Term (Tree a) -> Goal ()
inverto (Tree Int -> Term (Tree Int)
forall a. Logical a => a -> Term a
inject' Tree Int
exampleTree))