Instantly share code, notes, and snippets.

@paf31 /quineo.hs
Last active Dec 27, 2015

Embed
What would you like to do?
Not working yet
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment