reasoned-schemer/Main.hs

121 lines
2.2 KiB
Haskell

import Test.Hspec
import Control.Monad.Identity
import Control.Monad.Logic
import Control.Monad.State
test = it
data Never = Never Never
deriving (Show, Eq)
--
-- Search state
--
newtype Bindings t = Bindings (Binding t)
getBinding :: () -> Bindings t -> Binding t
getBinding () (Bindings b) = b
emptyBindings :: Bindings t
emptyBindings = Bindings Fresh
data Binding t
= Fresh
| Associated t
deriving (Eq, Show)
isFresh :: Binding t -> Bool
isFresh Fresh = True
isFresh (Associated _) = False
--
-- Public API
--
type Goal t = Schemer t ()
run :: (Term t -> Goal t) -> [Binding t]
run query =
let
goal = query $ Ref ()
m = execStateT goal emptyBindings
results = observeAll m
in
fmap (getBinding ()) results
satisfied :: Goal t
satisfied = return ()
eq :: Eq t => Term t -> Term t -> Goal t
eq a1 a2 = do
v1 <- resolve a1
v2 <- resolve a2
case (v1, v2) of
(Associated t1, Associated t2) ->
if t1 == t2
then return ()
else fail "not equal"
(Fresh, Associated t) ->
do
put (Bindings $ Associated t)
(Associated t, Fresh) ->
do
put (Bindings $ Associated t)
_ ->
error "TODO: unify two free terms"
--
-- Private
--
type Schemer t a = StateT (Bindings t) (LogicT Identity) a
binding :: () -> Schemer t (Binding t)
binding var =
fmap (getBinding var) get
resolve :: Term t -> Schemer t (Binding t)
resolve (Ref var) = binding var
resolve (Value t) = return (Associated t)
data Term t
= Ref ()
| Value t
--
-- Tests
--
main :: IO ()
main =
hspec $ do
describe "Chapter 1." $ do
test "7. fail" $ do
(run (\_ -> fail "") :: [Binding Never]) `shouldBe` []
test "10. eq" $ do
run (\_ -> Value "pea" `eq` Value "pod") `shouldBe` []
test "11. unify with query" $ do
run (\q -> eq q (Value "pea")) `shouldBe` [Associated "pea"]
test "12. eq commutes" $ do
run (\q -> eq (Value "pea") q) `shouldBe` [Associated "pea"]
test "15. isFresh" $ do
fmap isFresh (run (\q -> eq (Value "pea") q)) `shouldBe` [False]
test "16. satisfied" $ do
fmap isFresh (run (\_q -> satisfied)) `shouldBe` [True]