Not working yet

quineo.hs

{-# LANGUAGE PolymorphicComponents, GeneralizedNewtypeDeriving, DeriveDataTypeable #-}

import Data.Data
import Data.Maybe
import Data.Generics
import Data.Monoid
import Control.Applicative
import Control.Monad.State
import Control.Monad.Logic
import Control.Monad.Logic.Class

newtype Unknown t = Unknown { runUnknown :: Int } deriving (Show, Eq, Ord, Data, Typeable)

newtype Substitution = Substitution { runSubstitution :: forall t. (Unifiable t) => Unknown t -> t }

instance Monoid Substitution where
  mempty = Substitution unknown
  s1 `mappend` s2 = Substitution $ \u -> apply s1 (apply s2 (unknown u))
    

monoSubst :: (Typeable t) => (Unknown t -> t) -> Substitution
monoSubst f = Substitution $ \u -> fromMaybe (unknown u) $ do
  u1 <- cast u
  cast (f u1)

monoSubst1 :: (Unifiable t) => Unknown t -> t -> Substitution
monoSubst1 u t = monoSubst $ \u1 ->
  case u1 of 
    u2 | u2 == u -> t
       | otherwise -> unknown u2


replace :: (Unifiable t) => Unknown t -> t -> Kanren ()
replace u t' = do
  sub <- currentSubstitution <$> get
  let t = apply sub t'
  (Kanren . lift $ occursCheck u t) >>- \_ -> do
    let current = apply sub $ unknown u
    case isUnknown current of
      Just u1 | u1 == u -> return ()
      _ -> unify current t
    modify $ \s -> s { currentSubstitution = monoSubst1 u t <> currentSubstitution s }

class (Typeable t, Data t) => Unifiable t where
  unknown :: Unknown t -> t
  unify :: t -> t -> Kanren ()
  isUnknown :: t -> Maybe (Unknown t)
  apply :: Substitution -> t -> t
  unknowns :: t -> [Int]

occursCheck :: (Unifiable t) => Unknown t -> t -> Logic ()
occursCheck (Unknown u) t =
  case isUnknown t of
    Nothing -> guard (u `notElem` unknowns t)
    _ -> return ()

data KanrenState = KanrenState { currentSubstitution :: Substitution
                               , nextVariable :: Int }

newtype Kanren a = Kanren { unKanren :: StateT KanrenState Logic a } deriving (Functor, Monad, Applicative, MonadPlus, MonadState KanrenState, MonadLogic)

fresh :: (Unifiable t) => Kanren t
fresh = do
  n <- nextVariable <$> get
  modify $ \s -> s { nextVariable = succ (nextVariable s) }
  return $ unknown $ Unknown $ n

(~~) :: (Unifiable t) => t -> t -> Kanren ()
(~~) = unify

runKanren :: (Unifiable t, Data t) => Kanren t -> [t]
runKanren k = observeAll $ do
  runStateT (unKanren k) (KanrenState mempty 0) >>- \(a, KanrenState s _) -> 
    return (apply s a)



data Nat 
  = NatUnknown (Unknown Nat)
  | Zero
  | Succ Nat deriving (Show, Eq, Ord, Data, Typeable)


instance Unifiable Nat where
  unknown = NatUnknown
  unify (NatUnknown u1) (NatUnknown u2) | u1 == u2 = return ()
  unify (NatUnknown u) a = replace u a
  unify a (NatUnknown u) = replace u a
  unify (Succ n1) (Succ n2) = unify n1 n2
  unify Zero Zero = return ()
  unify _ _ = mzero
  isUnknown (NatUnknown u) = Just u
  isUnknown _ = Nothing
  apply s (NatUnknown u) = runSubstitution s u
  apply s Zero = Zero
  apply s (Succ n) = Succ (apply s n)
  unknowns (NatUnknown (Unknown u)) = [u]
  unknowns Zero = []
  unknowns (Succ n) = unknowns n

zeroo :: Nat -> Kanren ()
zeroo n = n ~~ Zero

succo :: Nat -> Nat -> Kanren ()
succo n pred = n ~~ Succ pred

addo :: Nat -> Nat -> Nat -> Kanren ()
addo n1 n2 n3 = foldl1 interleave
  [ zeroo n1 >>- \_ -> 
      n2 ~~ n3
  , do n1' <- fresh
       n3' <- fresh
       succo n1 n1' >>- \_ ->
         succo n3 n3' >>- \_ ->
           addo n1' n2 n3'
  ]

(===) :: Nat -> Nat -> Kanren ()
n1 === n2 = interleave
  (zeroo n1 >>- \_ -> zeroo n2)
  (do n1' <- fresh
      n2' <- fresh
      succo n1 n1' >>- \_ ->
        succo n2 n2' >>- \_ ->
          n1' === n2')

(=/=) :: Nat -> Nat -> Kanren ()
n1 =/= n2 = foldl1 interleave
  [ do n2' <- fresh
       zeroo n1 >>- \_ ->
         succo n2 n2'
  , do n1' <- fresh
       zeroo n2 >>- \_ ->
         succo n1 n1'
  , do n1' <- fresh
       n2' <- fresh
       succo n1 n1' >>- \_ ->
         succo n2 n2' >>- \_ ->
           n1' =/= n2'
  ]
  


data List a 
  = ListUnknown (Unknown (List a)) 
  | Nil 
  | Cons a (List a) deriving (Show, Eq, Ord, Data, Typeable)

instance (Unifiable a) => Unifiable (List a) where
  unknown = ListUnknown
  unify (ListUnknown u1) (ListUnknown u2) | u1 == u2 = return ()
  unify (ListUnknown u) a = replace u a
  unify a (ListUnknown u) = replace u a
  unify (Cons a1 l1) (Cons a2 l2) = unify a1 a2 >>- \_ -> unify l1 l2
  unify Nil Nil = return ()
  unify _ _ = mzero
  isUnknown (ListUnknown u) = Just u
  isUnknown _ = Nothing
  apply s (ListUnknown u) = runSubstitution s u
  apply s Nil = Nil
  apply s (Cons a l) = Cons (apply s a) (apply s l)
  unknowns (ListUnknown (Unknown u)) = [u]
  unknowns Nil = []
  unknowns (Cons a n) = unknowns a ++ unknowns n

nilo :: (Unifiable a) => List a -> Kanren ()
nilo a = a ~~ Nil

conso :: (Unifiable a) => List a -> a -> List a -> Kanren ()
conso a head tail = a ~~ Cons head tail


data Pair a b
  = PairUnknown (Unknown (Pair a b))
  | Pair a b deriving (Show, Eq, Ord, Data, Typeable)

instance (Unifiable a, Unifiable b) => Unifiable (Pair a b) where
  unknown = PairUnknown
  unify (PairUnknown u1) (PairUnknown u2) | u1 == u2 = return ()
  unify (PairUnknown u) a = replace u a
  unify a (PairUnknown u) = replace u a
  unify (Pair a1 b1) (Pair a2 b2) = unify a1 a2 >>- \_ -> unify b1 b2
  isUnknown (PairUnknown u) = Just u
  isUnknown _ = Nothing
  apply s (PairUnknown u) = runSubstitution s u
  apply s (Pair a b) = Pair (apply s a) (apply s b)
  unknowns (PairUnknown (Unknown u)) = [u]
  unknowns (Pair a b) = unknowns a ++ unknowns b

pairo :: (Unifiable a, Unifiable b) => Pair a b -> a -> b -> Kanren ()
pairo p a b = p ~~ Pair a b



data Expr
  = ExprUnknown (Unknown Expr)
  | Lam Nat Expr
  | Var Nat
  | Quote Expr
  | AntiQuote Expr
  | SyntaxQuote Expr
  | App Expr Expr
  | Closure Nat Expr Env deriving (Show, Eq, Ord, Data, Typeable)

instance Unifiable Expr where
  unknown = ExprUnknown
  unify (ExprUnknown u1) (ExprUnknown u2) | u1 == u2 = return ()
  unify (ExprUnknown u) a = replace u a
  unify a (ExprUnknown u) = replace u a
  unify (Lam n1 e1) (Lam n2 e2) = unify n1 n2 >>- \_ -> unify e1 e2
  unify (Var n1) (Var n2) = unify n1 n2
  unify (App e1 e2) (App e3 e4) = unify e1 e3 >>- \_ -> unify e2 e4
  unify (Quote e1) (Quote e2) = unify e1 e2
  unify (AntiQuote e1) (AntiQuote e2) = unify e1 e2
  unify (SyntaxQuote e1) (SyntaxQuote e2) = unify e1 e2
  unify (Closure x1 body1 env1) (Closure x2 body2 env2) = unify x1 x2 >>- \_ -> unify body1 body2 >>- \_ -> unify env1 env2
  unify _ _ = mzero
  isUnknown (ExprUnknown u) = Just u
  isUnknown _ = Nothing
  apply s (ExprUnknown u) = runSubstitution s u
  apply s (Lam n e) = Lam (apply s n) (apply s e)
  apply s (Var n) = Var (apply s n)
  apply s (Quote e) = Quote (apply s e)
  apply s (AntiQuote e) = AntiQuote (apply s e) 
  apply s (SyntaxQuote e) = SyntaxQuote (apply s e) 
  apply s (App e1 e2) = App (apply s e1) (apply s e2)
  apply s (Closure x body env) = Closure (apply s x) (apply s body) (apply s env)  
  unknowns (ExprUnknown (Unknown u)) = [u]
  unknowns (Lam n e) = unknowns n ++ unknowns e
  unknowns (Var n) = unknowns n
  unknowns (Quote e) = unknowns e
  unknowns (AntiQuote e) = unknowns e
  unknowns (SyntaxQuote e) = unknowns e
  unknowns (App e1 e2) = unknowns e1 ++ unknowns e2
  unknowns (Closure x body env) = unknowns x ++ unknowns body ++ unknowns env

lamo :: Expr -> Nat -> Expr -> Kanren ()
lamo e x body = e ~~ Lam x body

varo :: Expr -> Nat -> Kanren ()
varo e n = e ~~ Var n

appo :: Expr -> Expr -> Expr -> Kanren ()
appo e e1 e2 = e ~~ App e1 e2

quoteo :: Expr -> Expr -> Kanren ()
quoteo e e' = e ~~ Quote e'

syntaxQuoteo :: Expr -> Expr -> Kanren ()
syntaxQuoteo e e' = e ~~ SyntaxQuote e'

closureo :: Expr -> Nat -> Expr -> Env -> Kanren ()
closureo e x body env = e ~~ Closure x body env

type Env = List (Pair Nat Expr)

lookupo :: (Unifiable v) => List (Pair Nat v) -> Nat -> v -> Kanren ()
lookupo l k v = do
  p <- fresh
  tail <- fresh
  k1 <- fresh
  v1 <- fresh
  conso l p tail >>- \_ ->
    pairo p k1 v1 >>- \_ ->
      interleave 
        ((k === k1) >>- \_ -> (v ~~ v1)) 
        ((k =/= k1) >>- \_ -> lookupo tail k v)

notInEnvo :: Nat -> Env -> Kanren ()
notInEnvo n e = interleave
  (nilo e)
  (do p <- fresh
      tail <- fresh
      n1 <- fresh
      v1 <- fresh
      conso e p tail >>- \_ ->
        pairo p n1 v1 >>- \_ ->
          n1 =/= n >>- \_ ->
            notInEnvo n tail)

notClosure :: Expr -> Kanren ()
notClosure exp = foldl1 interleave
  [ foldl1 interleave 
    [ do x <- fresh
         body <- fresh
         lamo exp x body
    , do e <- fresh
         syntaxQuoteo exp e
    , do [e1, e2] <- replicateM 2 fresh 
         appo exp e1 e2
    ]
  , foldl1 interleave 
    [ do e <- fresh
         exp ~~ AntiQuote e
    , do n <- fresh
         varo exp n
    , do e' <- fresh
         quoteo exp e'
    ]
  ]

evalo :: Expr -> Env -> Expr -> Kanren ()
evalo exp env val = foldl1 interleave
  [ foldl1 interleave 
    [ do e <- fresh
         quoteo exp e
         notClosure e
         antiQuoteo e env val
    , do n <- fresh
         varo exp n
         lookupo env n val
    , do [rator, rand, body, a] <- replicateM 4 fresh
         x <- fresh
         env' <- fresh
         appo exp rator rand
         evalo rand env a >>- \_ ->
           evalo rator env (Closure x body env') >>- \_ ->
             evalo body (Cons (Pair x a) env') val 
    ]
  , foldl1 interleave 
    [ do x <- fresh
         body <- fresh
         lamo exp x body
         val ~~ Closure x body env
    , do syntaxQuoteo exp val
         notClosure val
    ]
  ]

antiQuoteo :: Expr -> Env -> Expr -> Kanren ()
antiQuoteo exp env val = foldl1 interleave
  [ foldl1 interleave
    [ do [e1, e2, v1, v2] <- replicateM 4 fresh
         appo exp e1 e2
         appo val v1 v2
         antiQuoteo e1 env v1 >>- \_ ->
           antiQuoteo e2 env v2
    , do x <- fresh
         [body, vbody] <- replicateM 2 fresh
         lamo exp x body
         lamo val x vbody
         antiQuoteo body env vbody
    , do [e, ve] <- replicateM 2 fresh
         quoteo exp e
         quoteo val ve
         antiQuoteo e env ve
    ]
  , foldl1 interleave
    [ foldl1 interleave
      [ do [e, ve] <- replicateM 2 fresh
           syntaxQuoteo exp e
           syntaxQuoteo val ve
           antiQuoteo e env ve
      , do x <- fresh
           env' <- fresh
           [body, vbody] <- replicateM 2 fresh
           closureo exp x body env'
           closureo val x vbody env'
           antiQuoteo body env vbody
      ]
    , foldl1 interleave 
      [ do e <- fresh
           exp ~~ AntiQuote e
           evalo e env val
      , do n <- fresh
           varo exp n
           varo val n
      ]
    ]
  ]

x .$ y = App x y

lamZ f = Lam Zero (f (Var Zero))

testQuine :: Expr
testQuine =
       (lamZ $ \x -> Quote (AntiQuote x .$ SyntaxQuote (AntiQuote x)))
    .$ SyntaxQuote (lamZ $ \x -> Quote (AntiQuote x .$ SyntaxQuote (AntiQuote x)))

quineo :: [Expr]
quineo = runKanren $ do
  q <- fresh
  evalo q Nil q
  return q

test1 :: [Expr]
test1 = runKanren $ do
  e <- fresh
  lookupo (Cons (Pair Zero (Lam Zero (Var Zero))) Nil) Zero e
  return e

test2 :: [Env]
test2 = runKanren $ do
  e <- fresh
  notInEnvo Zero e
  return e

test3 :: [Expr]
test3 = runKanren $ do
  e <- fresh
  notClosure e
  return e

test4 :: [Expr]
test4 = runKanren $ do
  e <- fresh
  evalo e Nil (Lam Zero (Var Zero))
  return e

test5 :: [List Nat]
test5 = runKanren $ do
  [n1, n2, n3] <- replicateM 3 fresh
  [l1, l2, l3, l4] <- replicateM 4 fresh
  conso l1 n1 l2
  conso l2 n2 l3
  conso l3 n3 l4
  nilo l4
  addo n1 n2 n3
  return l1

evens :: [Nat]
evens = runKanren $ do
  half <- fresh
  n <- fresh
  addo half half n
  return n



eval :: Env -> Expr -> Maybe Expr
eval env (App e1 e2) = 
  do e1e <- eval env e1
     e2e <- eval env e2
     case e1e of
       Closure x body env' -> eval (Cons (Pair x e2e) env') body
       e -> error $ show e
eval env (Lam x body) = Just $ Closure x body env
eval env (Quote e) = antiQuote env e
eval env (SyntaxQuote e) = Just e
eval env (Var n) = lookupE n env
eval _ _ = Nothing

antiQuote :: Env -> Expr -> Maybe Expr
antiQuote env (App e1 e2) = App <$> antiQuote env e1 <*> antiQuote env e2
antiQuote env (Lam x body) = Lam x <$> antiQuote env body
antiQuote env (Quote e) = Quote <$> antiQuote env e
antiQuote env (SyntaxQuote e) = SyntaxQuote <$> antiQuote env e
antiQuote env (Closure x body env') = Closure x <$> antiQuote env body <*> pure env'
antiQuote env (AntiQuote e) = eval env e
antiQuote _ e = pure e

lookupE n (Cons (Pair m v) e) | n == m = Just v
                              | otherwise = lookupE n e
lookupE _ _ = Nothing