First actually complete implementation
This commit is contained in:
parent
21d4fe3949
commit
288c999c0e
1
.gitignore
vendored
Normal file
1
.gitignore
vendored
Normal file
@ -0,0 +1 @@
|
|||||||
|
dist-newstyle
|
49
app/Binding.hs
Normal file
49
app/Binding.hs
Normal file
@ -0,0 +1,49 @@
|
|||||||
|
module Binding
|
||||||
|
( newVar, unify, instantiate
|
||||||
|
) where
|
||||||
|
import Terms
|
||||||
|
import Nondeterminism
|
||||||
|
import Primitives
|
||||||
|
import Control.Monad
|
||||||
|
import Control.Applicative
|
||||||
|
|
||||||
|
newVar :: Name -> PrologStream Var
|
||||||
|
newVar name = reversibly (newVarPrim name) unnewVarPrim
|
||||||
|
|
||||||
|
getVar :: Var -> PrologStream (Maybe Term)
|
||||||
|
getVar var = liftPrologIO (getVarPrim var)
|
||||||
|
|
||||||
|
setVar :: Var -> Term -> PrologStream ()
|
||||||
|
setVar var value = reversibly set unset
|
||||||
|
where
|
||||||
|
set = do
|
||||||
|
oldValue <- getVarPrim var
|
||||||
|
when (oldValue /= Nothing) (errorPrim "cannot set var that is currently set")
|
||||||
|
setVarPrim var (Just value)
|
||||||
|
unset = do
|
||||||
|
oldValue <- getVarPrim var
|
||||||
|
when (oldValue == Nothing) (errorPrim "cannot unset var that is already unset")
|
||||||
|
setVarPrim var Nothing
|
||||||
|
|
||||||
|
unify :: Term -> Term -> PrologStream ()
|
||||||
|
unify (Compound h0 args0) (Compound h1 args1) = do
|
||||||
|
when (h0 /= h1) empty
|
||||||
|
when (length args0 /= length args1) empty
|
||||||
|
forM_ (zip args0 args1) $ \(arg0, arg1) -> unify arg0 arg1
|
||||||
|
unify (Var v0) (Var v1) | v0 == v1 = return ()
|
||||||
|
unify (Var v0) t1 = do
|
||||||
|
binding <- getVar v0
|
||||||
|
case binding of
|
||||||
|
Just t0 -> unify t0 t1
|
||||||
|
Nothing -> setVar v0 t1
|
||||||
|
unify t0 t1@(Var _) = unify t1 t0
|
||||||
|
|
||||||
|
instantiate :: Term -> PrologStream Term
|
||||||
|
instantiate t@(Var v) = do
|
||||||
|
binding <- getVar v
|
||||||
|
case binding of
|
||||||
|
Just t0 -> instantiate t0
|
||||||
|
Nothing -> return t
|
||||||
|
instantiate (Compound h args) = do
|
||||||
|
instantiatedArgs <- mapM instantiate args
|
||||||
|
return (Compound h instantiatedArgs)
|
6
app/Classes.hs
Normal file
6
app/Classes.hs
Normal file
@ -0,0 +1,6 @@
|
|||||||
|
module Classes
|
||||||
|
( LiftIO (..)
|
||||||
|
) where
|
||||||
|
|
||||||
|
class Monad m => LiftIO m where
|
||||||
|
liftIO :: IO a -> m a
|
30
app/Database.hs
Normal file
30
app/Database.hs
Normal file
@ -0,0 +1,30 @@
|
|||||||
|
module Database
|
||||||
|
( Clause(..)
|
||||||
|
, Database(..)
|
||||||
|
, seekAndInstantiate, seek
|
||||||
|
) where
|
||||||
|
import Binding
|
||||||
|
import Nondeterminism
|
||||||
|
import Terms
|
||||||
|
import Control.Monad
|
||||||
|
import Control.Applicative
|
||||||
|
|
||||||
|
data Clause = Clause Term [Term]
|
||||||
|
|
||||||
|
data Database = Database
|
||||||
|
{ clauses :: [PrologStream Clause]
|
||||||
|
}
|
||||||
|
|
||||||
|
seekAndInstantiate :: Term -> Database -> PrologStream Term
|
||||||
|
seekAndInstantiate goal db = do
|
||||||
|
seek goal db
|
||||||
|
instantiate goal
|
||||||
|
|
||||||
|
seek :: Term -> Database -> PrologStream ()
|
||||||
|
seek goal db = do
|
||||||
|
foldr (<|>) mzero (map doClause (clauses db))
|
||||||
|
where
|
||||||
|
doClause clause = do
|
||||||
|
Clause chead body <- clause
|
||||||
|
unify goal chead
|
||||||
|
forM_ body $ \newGoal -> seek newGoal db
|
267
app/Main.hs
267
app/Main.hs
@ -1,237 +1,50 @@
|
|||||||
{-# LANGUAGE InstanceSigs #-}
|
{-# LANGUAGE InstanceSigs #-}
|
||||||
module Main where
|
module Main where
|
||||||
|
|
||||||
import Control.Monad
|
import Binding
|
||||||
import qualified Data.Map.Lazy as M
|
import Classes
|
||||||
import Data.IORef
|
import Database
|
||||||
import Control.Monad.RWS (MonadTrans(lift))
|
import Nondeterminism
|
||||||
import Control.Applicative
|
import Terms
|
||||||
|
|
||||||
data Atomic
|
demoProgram :: Database
|
||||||
= AString String
|
demoProgram = Database
|
||||||
deriving (Eq, Show)
|
{ clauses =
|
||||||
|
[ do
|
||||||
|
who <- newVar "who"
|
||||||
|
action <- newVar "action"
|
||||||
|
return $ Clause (Compound "act" [Var who, Var action])
|
||||||
|
[ Compound "is_vampire" [Var who]
|
||||||
|
, Compound "vampire_behavior" [Var action]
|
||||||
|
]
|
||||||
|
, do
|
||||||
|
progenitor <- newVar "progenitor"
|
||||||
|
progeny <- newVar "progeny"
|
||||||
|
return $ Clause (Compound "is_vampire" [Var progeny])
|
||||||
|
[ Compound "has_progenitor" [Var progenitor, Var progeny]
|
||||||
|
, Compound "is_vampire" [Var progenitor]
|
||||||
|
]
|
||||||
|
, return $ Clause (Compound "act" [Compound "Sam" [], Compound "goes to law school" []]) []
|
||||||
|
|
||||||
data Name
|
, return $ Clause (Compound "vampire_behavior" [Compound "drinks blood" []]) []
|
||||||
= NString String
|
, return $ Clause (Compound "vampire_behavior" [Compound "spits venom" []]) []
|
||||||
deriving (Ord, Eq, Show)
|
, return $ Clause (Compound "is_vampire" [Compound "Nyeogmi" []]) []
|
||||||
|
, return $ Clause (Compound "has_progenitor" [Compound "Nyeogmi" [], Compound "Pyrex" []]) []
|
||||||
data Term
|
, return $ Clause (Compound "has_progenitor" [Compound "Sam" [], Compound "Alex" []]) []
|
||||||
= TCompound Atomic [Term] -- functor, args
|
-- , return $ Clause (Compound "is_vampire" [Compound "Sam" []]) []
|
||||||
| TVariable Name -- name
|
]
|
||||||
deriving (Eq, Show)
|
|
||||||
|
|
||||||
type Vars = M.Map Name Term
|
|
||||||
|
|
||||||
emptyVars :: Vars
|
|
||||||
emptyVars = M.empty
|
|
||||||
|
|
||||||
|
|
||||||
data Globals = Globals {
|
|
||||||
psVars :: IORef Vars
|
|
||||||
}
|
|
||||||
|
|
||||||
newtype PrologIO a = PrologIO (Globals -> IO a)
|
|
||||||
|
|
||||||
instance Functor PrologIO where
|
|
||||||
fmap :: (a -> b) -> PrologIO a -> PrologIO b
|
|
||||||
fmap f (PrologIO a) = PrologIO (\globals -> fmap f (a globals))
|
|
||||||
|
|
||||||
instance Applicative PrologIO where
|
|
||||||
pure :: a -> PrologIO a
|
|
||||||
pure x = PrologIO (\_ -> pure x)
|
|
||||||
|
|
||||||
(PrologIO f) <*> (PrologIO x) = PrologIO (
|
|
||||||
\globals -> do
|
|
||||||
f' <- f globals
|
|
||||||
x' <- x globals
|
|
||||||
pure (f' x')
|
|
||||||
)
|
|
||||||
|
|
||||||
instance Monad PrologIO where
|
|
||||||
return :: a -> PrologIO a
|
|
||||||
return = pure
|
|
||||||
|
|
||||||
(PrologIO a) >>= f = PrologIO (
|
|
||||||
\globals -> do
|
|
||||||
a' <- a globals
|
|
||||||
let PrologIO b' = f a'
|
|
||||||
b' globals
|
|
||||||
)
|
|
||||||
|
|
||||||
runPrologIO :: Globals -> PrologIO a -> IO a
|
|
||||||
runPrologIO globals (PrologIO a) = a globals
|
|
||||||
|
|
||||||
data Suspend a = Yield a | Suspend
|
|
||||||
|
|
||||||
instance Functor Suspend where
|
|
||||||
fmap f (Yield a) = Yield (f a)
|
|
||||||
fmap _ Suspend = Suspend
|
|
||||||
|
|
||||||
data PrologStream a
|
|
||||||
= PYes (Suspend a) (PrologIO (PrologStream a))
|
|
||||||
| PNo
|
|
||||||
|
|
||||||
instance Functor PrologStream where
|
|
||||||
fmap :: (a -> b) -> PrologStream a -> PrologStream b
|
|
||||||
fmap f (PYes a next) = PYes (fmap f a) (fmap (fmap f) next)
|
|
||||||
fmap _ PNo = PNo
|
|
||||||
|
|
||||||
instance Applicative PrologStream where
|
|
||||||
pure :: a -> PrologStream a
|
|
||||||
pure x = PYes (Yield x) (pure PNo)
|
|
||||||
|
|
||||||
(<*>) :: PrologStream (a -> b) -> PrologStream a -> PrologStream b
|
|
||||||
f <*> x = f >>= (\f' -> x >>= (\x' -> return (f' x')))
|
|
||||||
|
|
||||||
instance Monad PrologStream where
|
|
||||||
return :: a -> PrologStream a
|
|
||||||
return = pure
|
|
||||||
|
|
||||||
(>>=) :: PrologStream a -> (a -> PrologStream b) -> PrologStream b
|
|
||||||
PNo >>= _ = PNo
|
|
||||||
PYes (Yield x) xs >>= f = f x <|> PYes Suspend (fmap (>>= f) xs)
|
|
||||||
PYes Suspend xs >>= f = PYes Suspend (fmap (>>= f) xs)
|
|
||||||
|
|
||||||
instance Alternative PrologStream where
|
|
||||||
empty :: PrologStream a
|
|
||||||
empty = PNo
|
|
||||||
|
|
||||||
(<|>) :: PrologStream a -> PrologStream a -> PrologStream a
|
|
||||||
(<|>) = append
|
|
||||||
|
|
||||||
|
|
||||||
instance MonadPlus PrologStream where
|
|
||||||
mzero :: PrologStream a
|
|
||||||
mzero = empty
|
|
||||||
|
|
||||||
mplus :: PrologStream a -> PrologStream a -> PrologStream a
|
|
||||||
mplus = (<|>)
|
|
||||||
|
|
||||||
|
|
||||||
append :: PrologStream a -> PrologStream a -> PrologStream a
|
|
||||||
append (PYes x xs) next = PYes x (liftM2 append xs (return next))
|
|
||||||
append PNo next = next
|
|
||||||
|
|
||||||
|
|
||||||
data Thread a = Thread
|
|
||||||
{ threadGlobals :: Globals
|
|
||||||
, threadStream :: IORef (PrologStream a)
|
|
||||||
}
|
}
|
||||||
|
|
||||||
startThread :: PrologStream a -> IO (Thread a)
|
|
||||||
startThread stream = do
|
|
||||||
vars <- newIORef emptyVars
|
|
||||||
streamRef <- newIORef stream
|
|
||||||
let globals = Globals { psVars = vars }
|
|
||||||
return (Thread { threadGlobals = globals, threadStream = streamRef })
|
|
||||||
|
|
||||||
advanceThread :: Thread a -> IO (Maybe a)
|
|
||||||
advanceThread (Thread { threadGlobals = globals, threadStream = streamRef }) = do
|
|
||||||
stream <- readIORef streamRef
|
|
||||||
(value, newStream) <- runPrologIO globals (squeeze stream)
|
|
||||||
writeIORef streamRef newStream
|
|
||||||
return value
|
|
||||||
|
|
||||||
completeThread :: Thread a -> IO [a]
|
|
||||||
completeThread thread = do
|
|
||||||
value <- advanceThread thread
|
|
||||||
case value of
|
|
||||||
Nothing -> return []
|
|
||||||
Just x -> fmap (x:) (completeThread thread)
|
|
||||||
|
|
||||||
squeeze :: PrologStream a -> PrologIO (Maybe a, PrologStream a)
|
|
||||||
squeeze PNo = return (Nothing, PNo)
|
|
||||||
squeeze (PYes Suspend rest) = rest >>= squeeze
|
|
||||||
squeeze (PYes (Yield x) rest) = fmap ((,) (Just x)) rest
|
|
||||||
|
|
||||||
exitUndo :: PrologIO a -> PrologIO () -> PrologStream a
|
|
||||||
exitUndo exit undo =
|
|
||||||
PYes Suspend $ exit >>= \v -> return $
|
|
||||||
PYes (Yield v) $ undo >>= \_ -> return $
|
|
||||||
PNo
|
|
||||||
|
|
||||||
liftPrologIO :: PrologIO a -> PrologStream a
|
|
||||||
liftPrologIO exit = exitUndo exit (return ())
|
|
||||||
|
|
||||||
liftIO :: IO a -> PrologStream a
|
|
||||||
liftIO x = liftPrologIO $ PrologIO (\_ -> x)
|
|
||||||
|
|
||||||
setVar :: Name -> Term -> PrologStream ()
|
|
||||||
setVar name value = exitUndo exit undo
|
|
||||||
where
|
|
||||||
exit = PrologIO (
|
|
||||||
\globals -> do
|
|
||||||
let varsRef = psVars globals
|
|
||||||
modifyIORef varsRef (M.insert name value)
|
|
||||||
)
|
|
||||||
undo = PrologIO (
|
|
||||||
\globals -> do
|
|
||||||
let varsRef = psVars globals
|
|
||||||
modifyIORef varsRef (M.delete name)
|
|
||||||
)
|
|
||||||
|
|
||||||
getVar :: Name -> PrologStream (Maybe Term)
|
|
||||||
getVar name = exitUndo exit undo
|
|
||||||
where
|
|
||||||
exit = PrologIO (
|
|
||||||
\globals -> do
|
|
||||||
let varsRef = psVars globals
|
|
||||||
vars <- readIORef varsRef
|
|
||||||
return (M.lookup name vars)
|
|
||||||
)
|
|
||||||
undo = PrologIO (\_ -> return ())
|
|
||||||
|
|
||||||
|
|
||||||
demoProgram :: PrologStream ()
|
|
||||||
demoProgram = do
|
|
||||||
setVar (NString "bat") (TCompound (AString "Nyeogmi") []) <|> setVar (NString "bat") (TCompound (AString "Pyrex") [])
|
|
||||||
setVar (NString "activity") (TCompound (AString "drinks blood") []) <|> setVar (NString "activity") (TCompound (AString "spits venom") [])
|
|
||||||
who <- getVar (NString "bat")
|
|
||||||
what <- getVar (NString "activity")
|
|
||||||
liftIO (print ("Value: ", who, "What: ", what))
|
|
||||||
|
|
||||||
|
|
||||||
main :: IO ()
|
main :: IO ()
|
||||||
main = do
|
main = do
|
||||||
thread <- startThread demoProgram
|
thread <- newThread runDemoProgram
|
||||||
results <- completeThread thread
|
_ <- takeAllRemainingSolutions thread
|
||||||
putStrLn ("Results: " ++ show results)
|
return ()
|
||||||
{-
|
|
||||||
no :: Prolog a
|
|
||||||
no = Prolog (\_ -> [])
|
|
||||||
|
|
||||||
readVars :: Prolog Vars
|
|
||||||
readVars = Prolog (\vars -> [(vars, vars)])
|
|
||||||
|
|
||||||
writeVars :: Vars -> Prolog ()
|
|
||||||
writeVars vars = Prolog (\_ -> [((), vars)])
|
|
||||||
|
|
||||||
unify :: Term -> Term -> Prolog ()
|
|
||||||
unify = unify_ []
|
|
||||||
where
|
where
|
||||||
unify_ :: [Name] -> Term -> Term -> Prolog ()
|
runDemoProgram = do
|
||||||
unify_ names (TCompound h0 args0) (TCompound h1 args1) = do
|
who <- newVar "who"
|
||||||
when (h0 /= h1) no
|
what <- newVar "what"
|
||||||
when (length args0 /= length args1) no
|
let goal = Compound "act" [Var who, Var what]
|
||||||
forM_ (zip args0 args1) $ \(arg0, arg1) -> unify_ names arg0 arg1
|
seek goal demoProgram
|
||||||
unify_ _ (TVariable name0) (TVariable name1) | name0 == name1 = return ()
|
instantiatedGoal <- instantiate goal
|
||||||
unify_ names (TVariable name) y = do
|
liftIO $ putStrLn ("Got " ++ show instantiatedGoal)
|
||||||
-- occurs check
|
|
||||||
when (name `elem` names) no
|
|
||||||
-- unify as usual
|
|
||||||
(Vars vs0) <- readVars
|
|
||||||
case M.lookup name vs0 of
|
|
||||||
Just existing -> unify_ (name:names) existing y
|
|
||||||
Nothing -> do
|
|
||||||
let vs1 = M.insert name y vs0
|
|
||||||
writeVars (Vars vs1)
|
|
||||||
unify_ names x@(TCompound _ _) y@(TVariable _) = unify_ names y x
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
main :: IO ()
|
|
||||||
main = putStrLn "Hello, Haskell!"
|
|
||||||
|
|
||||||
-}
|
|
@ -1,99 +0,0 @@
|
|||||||
{-# LANGUAGE InstanceSigs #-}
|
|
||||||
module Main where
|
|
||||||
|
|
||||||
import Control.Monad
|
|
||||||
import Control.Monad.State.Lazy
|
|
||||||
import qualified Data.Map.Lazy as M
|
|
||||||
import GHC.Conc (TVar(TVar))
|
|
||||||
|
|
||||||
data Atomic
|
|
||||||
= AString String
|
|
||||||
deriving (Eq, Show)
|
|
||||||
|
|
||||||
data Name
|
|
||||||
= NString String
|
|
||||||
deriving (Ord, Eq, Show)
|
|
||||||
|
|
||||||
data Term
|
|
||||||
= TCompound Atomic [Term] -- functor, args
|
|
||||||
| TVariable Name -- name
|
|
||||||
deriving (Eq, Show)
|
|
||||||
|
|
||||||
data Vars
|
|
||||||
= Vars { varsBindings :: M.Map Name Term }
|
|
||||||
|
|
||||||
emptyVars :: Vars
|
|
||||||
emptyVars = Vars { varsBindings = M.empty }
|
|
||||||
|
|
||||||
newtype Prolog a = Prolog (Vars -> [(a, Vars)])
|
|
||||||
|
|
||||||
instance Functor Prolog where
|
|
||||||
fmap :: (a -> b) -> Prolog a -> Prolog b
|
|
||||||
fmap f (Prolog x) = Prolog (\v0 -> [(f a, v1) | (a, v1) <- x v0])
|
|
||||||
|
|
||||||
instance Applicative Prolog where
|
|
||||||
pure :: a -> Prolog a
|
|
||||||
pure x = Prolog (\_ -> [(x, emptyVars)])
|
|
||||||
|
|
||||||
(<*>) :: Prolog (a -> b) -> Prolog a -> Prolog b
|
|
||||||
(Prolog f) <*> (Prolog x) = Prolog body
|
|
||||||
where
|
|
||||||
body vars0
|
|
||||||
= [
|
|
||||||
(function argument, vars2) |
|
|
||||||
(function, vars1) <- f vars0,
|
|
||||||
(argument, vars2) <- x vars1
|
|
||||||
]
|
|
||||||
|
|
||||||
instance Monad Prolog where
|
|
||||||
return :: a -> Prolog a
|
|
||||||
return = pure
|
|
||||||
|
|
||||||
(>>=) :: Prolog a -> (a -> Prolog b) -> Prolog b
|
|
||||||
(Prolog a0) >>= f = Prolog body
|
|
||||||
where
|
|
||||||
body vars0
|
|
||||||
= [
|
|
||||||
(b1, vars2) |
|
|
||||||
(a1, vars1) <- a0 vars0,
|
|
||||||
let Prolog b = f a1,
|
|
||||||
(b1, vars2) <- (b vars1)
|
|
||||||
]
|
|
||||||
|
|
||||||
|
|
||||||
no :: Prolog a
|
|
||||||
no = Prolog (\_ -> [])
|
|
||||||
|
|
||||||
readVars :: Prolog Vars
|
|
||||||
readVars = Prolog (\vars -> [(vars, vars)])
|
|
||||||
|
|
||||||
writeVars :: Vars -> Prolog ()
|
|
||||||
writeVars vars = Prolog (\_ -> [((), vars)])
|
|
||||||
|
|
||||||
unify :: Term -> Term -> Prolog ()
|
|
||||||
unify = unify_ []
|
|
||||||
where
|
|
||||||
unify_ :: [Name] -> Term -> Term -> Prolog ()
|
|
||||||
unify_ names (TCompound h0 args0) (TCompound h1 args1) = do
|
|
||||||
when (h0 /= h1) no
|
|
||||||
when (length args0 /= length args1) no
|
|
||||||
forM_ (zip args0 args1) $ \(arg0, arg1) -> unify_ names arg0 arg1
|
|
||||||
unify_ _ (TVariable name0) (TVariable name1) | name0 == name1 = return ()
|
|
||||||
unify_ names (TVariable name) y = do
|
|
||||||
-- occurs check
|
|
||||||
when (name `elem` names) no
|
|
||||||
-- unify as usual
|
|
||||||
(Vars vs0) <- readVars
|
|
||||||
case M.lookup name vs0 of
|
|
||||||
Just existing -> unify_ (name:names) existing y
|
|
||||||
Nothing -> do
|
|
||||||
let vs1 = M.insert name y vs0
|
|
||||||
writeVars (Vars vs1)
|
|
||||||
unify_ names x@(TCompound _ _) y@(TVariable _) = unify_ names y x
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
main :: IO ()
|
|
||||||
main = putStrLn "Hello, Haskell!"
|
|
167
app/Main.hs.old2
167
app/Main.hs.old2
@ -1,167 +0,0 @@
|
|||||||
{-# LANGUAGE InstanceSigs #-}
|
|
||||||
module Main where
|
|
||||||
|
|
||||||
import Control.Monad
|
|
||||||
import qualified Data.Map.Lazy as M
|
|
||||||
import Data.IORef
|
|
||||||
|
|
||||||
data Atomic
|
|
||||||
= AString String
|
|
||||||
deriving (Eq, Show)
|
|
||||||
|
|
||||||
data Name
|
|
||||||
= NString String
|
|
||||||
deriving (Ord, Eq, Show)
|
|
||||||
|
|
||||||
data Term
|
|
||||||
= TCompound Atomic [Term] -- functor, args
|
|
||||||
| TVariable Name -- name
|
|
||||||
deriving (Eq, Show)
|
|
||||||
|
|
||||||
data Vars
|
|
||||||
= Vars { varsBindings :: M.Map Name Term }
|
|
||||||
|
|
||||||
emptyVars :: Vars
|
|
||||||
emptyVars = Vars { varsBindings = M.empty }
|
|
||||||
|
|
||||||
|
|
||||||
data Globals = Globals {
|
|
||||||
psVars :: IORef Vars
|
|
||||||
}
|
|
||||||
|
|
||||||
newtype PrologIO a = PrologIO (Globals -> IO a)
|
|
||||||
|
|
||||||
instance Functor PrologIO where
|
|
||||||
fmap :: (a -> b) -> PrologIO a -> PrologIO b
|
|
||||||
fmap f (PrologIO a) = PrologIO (\globals -> fmap f (a globals))
|
|
||||||
|
|
||||||
instance Applicative PrologIO where
|
|
||||||
pure :: a -> PrologIO a
|
|
||||||
pure x = PrologIO (\_ -> pure x)
|
|
||||||
|
|
||||||
(PrologIO f) <*> (PrologIO x) = PrologIO (
|
|
||||||
\globals -> do
|
|
||||||
f' <- f globals
|
|
||||||
x' <- x globals
|
|
||||||
pure (f' x')
|
|
||||||
)
|
|
||||||
|
|
||||||
instance Monad PrologIO where
|
|
||||||
return :: a -> PrologIO a
|
|
||||||
return = pure
|
|
||||||
|
|
||||||
(PrologIO a) >>= f = PrologIO (
|
|
||||||
\globals -> do
|
|
||||||
a' <- a globals
|
|
||||||
let PrologIO b' = f a'
|
|
||||||
b' globals
|
|
||||||
)
|
|
||||||
|
|
||||||
runPrologIO :: Globals -> PrologIO a -> IO a
|
|
||||||
runPrologIO globals (PrologIO a) = a globals
|
|
||||||
|
|
||||||
data PrologStream a
|
|
||||||
= PYes (Maybe a) (PrologIO (PrologStream a))
|
|
||||||
| PNo
|
|
||||||
|
|
||||||
instance Functor PrologStream where
|
|
||||||
fmap :: (a -> b) -> PrologStream a -> PrologStream b
|
|
||||||
fmap f (PYes a next) = PYes (fmap f a) (fmap (fmap f) next)
|
|
||||||
fmap _ PNo = PNo
|
|
||||||
|
|
||||||
instance Monad PrologStream where
|
|
||||||
return :: a -> PrologStream a
|
|
||||||
return = pure
|
|
||||||
|
|
||||||
(>>=) :: PrologStream a -> (a -> PrologStream b) -> PrologStream b
|
|
||||||
x >>= f = join_ (fmap f x)
|
|
||||||
|
|
||||||
instance Applicative PrologStream where
|
|
||||||
pure :: a -> PrologStream a
|
|
||||||
pure x = PYes (Just x) (pure PNo)
|
|
||||||
|
|
||||||
(<*>) :: PrologStream (a -> b) -> PrologStream a -> PrologStream b
|
|
||||||
f <*> x = f >>= (\f' -> x >>= (\x' -> return (f' x')))
|
|
||||||
|
|
||||||
|
|
||||||
join_ :: PrologStream (PrologStream a) -> PrologStream a
|
|
||||||
join_ (PNo) = PNo
|
|
||||||
join_ (PYes Nothing rest) = PYes Nothing (fmap join_ rest)
|
|
||||||
join_ (PYes (Just PNo) rest) = PYes Nothing (fmap join_ rest)
|
|
||||||
join_ (PYes (Just (PYes a xs)) rest) =
|
|
||||||
let joinedRest = liftM2 append xs (fmap join_ rest) in
|
|
||||||
PYes a joinedRest
|
|
||||||
|
|
||||||
append :: PrologStream a -> PrologStream a -> PrologStream a
|
|
||||||
append (PYes x xs) next = PYes x (liftM2 append xs (return next))
|
|
||||||
append PNo next = next
|
|
||||||
|
|
||||||
|
|
||||||
data Thread a = Thread
|
|
||||||
{ threadGlobals :: Globals
|
|
||||||
, threadStream :: IORef (PrologStream a)
|
|
||||||
}
|
|
||||||
|
|
||||||
startThread :: PrologStream a -> IO (Thread a)
|
|
||||||
startThread stream = do
|
|
||||||
vars <- newIORef emptyVars
|
|
||||||
streamRef <- newIORef stream
|
|
||||||
let globals = Globals { psVars = vars }
|
|
||||||
return (Thread { threadGlobals = globals, threadStream = streamRef })
|
|
||||||
|
|
||||||
advanceThread :: Thread a -> IO (Maybe a)
|
|
||||||
advanceThread (Thread { threadGlobals = globals, threadStream = streamRef }) = do
|
|
||||||
stream <- readIORef streamRef
|
|
||||||
(value, newStream) <- runPrologIO globals (squeeze stream)
|
|
||||||
writeIORef streamRef newStream
|
|
||||||
return value
|
|
||||||
|
|
||||||
|
|
||||||
squeeze :: PrologStream a -> PrologIO (Maybe a, PrologStream a)
|
|
||||||
squeeze PNo = return (Nothing, PNo)
|
|
||||||
squeeze (PYes (Nothing) rest) = rest >>= squeeze
|
|
||||||
squeeze (PYes (Just x) rest) = fmap ((,) (Just x)) rest
|
|
||||||
|
|
||||||
|
|
||||||
main :: IO ()
|
|
||||||
main = do
|
|
||||||
putStrLn "Hello, world!"
|
|
||||||
{-
|
|
||||||
no :: Prolog a
|
|
||||||
no = Prolog (\_ -> [])
|
|
||||||
|
|
||||||
readVars :: Prolog Vars
|
|
||||||
readVars = Prolog (\vars -> [(vars, vars)])
|
|
||||||
|
|
||||||
writeVars :: Vars -> Prolog ()
|
|
||||||
writeVars vars = Prolog (\_ -> [((), vars)])
|
|
||||||
|
|
||||||
unify :: Term -> Term -> Prolog ()
|
|
||||||
unify = unify_ []
|
|
||||||
where
|
|
||||||
unify_ :: [Name] -> Term -> Term -> Prolog ()
|
|
||||||
unify_ names (TCompound h0 args0) (TCompound h1 args1) = do
|
|
||||||
when (h0 /= h1) no
|
|
||||||
when (length args0 /= length args1) no
|
|
||||||
forM_ (zip args0 args1) $ \(arg0, arg1) -> unify_ names arg0 arg1
|
|
||||||
unify_ _ (TVariable name0) (TVariable name1) | name0 == name1 = return ()
|
|
||||||
unify_ names (TVariable name) y = do
|
|
||||||
-- occurs check
|
|
||||||
when (name `elem` names) no
|
|
||||||
-- unify as usual
|
|
||||||
(Vars vs0) <- readVars
|
|
||||||
case M.lookup name vs0 of
|
|
||||||
Just existing -> unify_ (name:names) existing y
|
|
||||||
Nothing -> do
|
|
||||||
let vs1 = M.insert name y vs0
|
|
||||||
writeVars (Vars vs1)
|
|
||||||
unify_ names x@(TCompound _ _) y@(TVariable _) = unify_ names y x
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
main :: IO ()
|
|
||||||
main = putStrLn "Hello, Haskell!"
|
|
||||||
|
|
||||||
-}
|
|
104
app/Nondeterminism.hs
Normal file
104
app/Nondeterminism.hs
Normal file
@ -0,0 +1,104 @@
|
|||||||
|
{-# LANGUAGE InstanceSigs #-}
|
||||||
|
module Nondeterminism
|
||||||
|
( PrologStream
|
||||||
|
, newThread
|
||||||
|
, takeNextSolution, takeAllRemainingSolutions
|
||||||
|
, reversibly
|
||||||
|
, liftPrologIO
|
||||||
|
) where
|
||||||
|
import Primitives (Globals, PrologIO(..), newGlobals)
|
||||||
|
import Control.Applicative
|
||||||
|
import Control.Monad
|
||||||
|
import Classes (LiftIO (..))
|
||||||
|
import GHC.IORef
|
||||||
|
|
||||||
|
data Suspend a = Yield a | Suspend
|
||||||
|
|
||||||
|
instance Functor Suspend where
|
||||||
|
fmap f (Yield a) = Yield (f a)
|
||||||
|
fmap _ Suspend = Suspend
|
||||||
|
|
||||||
|
data PrologStream a
|
||||||
|
= PYes (Suspend a) (PrologIO (PrologStream a))
|
||||||
|
| PNo
|
||||||
|
|
||||||
|
instance Functor PrologStream where
|
||||||
|
fmap :: (a -> b) -> PrologStream a -> PrologStream b
|
||||||
|
fmap f (PYes a next) = PYes (fmap f a) (fmap (fmap f) next)
|
||||||
|
fmap _ PNo = PNo
|
||||||
|
|
||||||
|
instance Applicative PrologStream where
|
||||||
|
pure :: a -> PrologStream a
|
||||||
|
pure x = PYes (Yield x) (pure PNo)
|
||||||
|
|
||||||
|
(<*>) :: PrologStream (a -> b) -> PrologStream a -> PrologStream b
|
||||||
|
f <*> x = f >>= (\f' -> x >>= (\x' -> return (f' x')))
|
||||||
|
|
||||||
|
instance Monad PrologStream where
|
||||||
|
return :: a -> PrologStream a
|
||||||
|
return = pure
|
||||||
|
|
||||||
|
(>>=) :: PrologStream a -> (a -> PrologStream b) -> PrologStream b
|
||||||
|
PNo >>= _ = PNo
|
||||||
|
PYes (Yield x) xs >>= f = f x <|> PYes Suspend (fmap (>>= f) xs)
|
||||||
|
PYes Suspend xs >>= f = PYes Suspend (fmap (>>= f) xs)
|
||||||
|
|
||||||
|
instance Alternative PrologStream where
|
||||||
|
empty :: PrologStream a
|
||||||
|
empty = PNo
|
||||||
|
|
||||||
|
(<|>) :: PrologStream a -> PrologStream a -> PrologStream a
|
||||||
|
(PYes x xs) <|> next = PYes x (liftM2 (<|>) xs (return next))
|
||||||
|
PNo <|> next = next
|
||||||
|
|
||||||
|
instance MonadPlus PrologStream where
|
||||||
|
mzero :: PrologStream a
|
||||||
|
mzero = empty
|
||||||
|
|
||||||
|
mplus :: PrologStream a -> PrologStream a -> PrologStream a
|
||||||
|
mplus = (<|>)
|
||||||
|
|
||||||
|
data Thread a = Thread
|
||||||
|
{ threadGlobals :: Globals
|
||||||
|
, threadStream :: IORef (PrologStream a)
|
||||||
|
}
|
||||||
|
|
||||||
|
newThread :: PrologStream a -> IO (Thread a)
|
||||||
|
newThread stream = do
|
||||||
|
globals <- newGlobals
|
||||||
|
streamRef <- newIORef stream
|
||||||
|
return $ Thread
|
||||||
|
{ threadGlobals = globals
|
||||||
|
, threadStream = streamRef
|
||||||
|
}
|
||||||
|
|
||||||
|
takeNextSolution :: Thread a -> IO (Maybe a)
|
||||||
|
takeNextSolution (Thread { threadGlobals = globals, threadStream = streamRef }) = do
|
||||||
|
stream <- readIORef streamRef
|
||||||
|
(value, newStream) <- runPrologIO (squeeze stream) globals
|
||||||
|
writeIORef streamRef newStream
|
||||||
|
return value
|
||||||
|
|
||||||
|
takeAllRemainingSolutions :: Thread a -> IO [a]
|
||||||
|
takeAllRemainingSolutions thread = do
|
||||||
|
value <- takeNextSolution thread
|
||||||
|
case value of
|
||||||
|
Nothing -> return []
|
||||||
|
Just x -> fmap (x:) (takeAllRemainingSolutions thread)
|
||||||
|
|
||||||
|
squeeze :: PrologStream a -> PrologIO (Maybe a, PrologStream a)
|
||||||
|
squeeze PNo = return (Nothing, PNo)
|
||||||
|
squeeze (PYes Suspend rest) = rest >>= squeeze
|
||||||
|
squeeze (PYes (Yield x) rest) = fmap ((,) (Just x)) rest
|
||||||
|
|
||||||
|
reversibly :: PrologIO a -> PrologIO () -> PrologStream a
|
||||||
|
reversibly forward backward =
|
||||||
|
PYes Suspend $ forward >>= \v -> return $
|
||||||
|
PYes (Yield v) $ backward >>= \_ -> return $
|
||||||
|
PNo
|
||||||
|
|
||||||
|
liftPrologIO :: PrologIO a -> PrologStream a
|
||||||
|
liftPrologIO forward = reversibly forward (return ())
|
||||||
|
|
||||||
|
instance LiftIO PrologStream where
|
||||||
|
liftIO x = liftPrologIO (liftIO x)
|
85
app/Primitives.hs
Normal file
85
app/Primitives.hs
Normal file
@ -0,0 +1,85 @@
|
|||||||
|
{-# LANGUAGE InstanceSigs #-}
|
||||||
|
module Primitives
|
||||||
|
( PrologIO(..)
|
||||||
|
, Globals
|
||||||
|
, newGlobals
|
||||||
|
, newVarPrim, unnewVarPrim
|
||||||
|
, getVarPrim, setVarPrim
|
||||||
|
, errorPrim
|
||||||
|
)
|
||||||
|
where
|
||||||
|
|
||||||
|
import Data.IORef
|
||||||
|
import qualified Data.IntMap.Strict as M
|
||||||
|
import Terms
|
||||||
|
import Classes (LiftIO(..))
|
||||||
|
|
||||||
|
newtype PrologIO a = PrologIO { runPrologIO :: Globals -> IO a }
|
||||||
|
|
||||||
|
instance Functor PrologIO where
|
||||||
|
fmap :: (a -> b) -> PrologIO a -> PrologIO b
|
||||||
|
fmap f (PrologIO a) = PrologIO (\globals -> fmap f (a globals))
|
||||||
|
|
||||||
|
instance Applicative PrologIO where
|
||||||
|
pure :: a -> PrologIO a
|
||||||
|
pure x = PrologIO (\_ -> pure x)
|
||||||
|
|
||||||
|
(PrologIO f) <*> (PrologIO x) = PrologIO (
|
||||||
|
\globals -> do
|
||||||
|
f' <- f globals
|
||||||
|
x' <- x globals
|
||||||
|
pure (f' x')
|
||||||
|
)
|
||||||
|
|
||||||
|
instance Monad PrologIO where
|
||||||
|
return :: a -> PrologIO a
|
||||||
|
return = pure
|
||||||
|
|
||||||
|
(PrologIO a) >>= f = PrologIO (
|
||||||
|
\globals -> do
|
||||||
|
a' <- a globals
|
||||||
|
let PrologIO b' = f a'
|
||||||
|
b' globals
|
||||||
|
)
|
||||||
|
|
||||||
|
data Globals = Globals
|
||||||
|
{ values :: IORef (M.IntMap Term)
|
||||||
|
, names :: IORef (M.IntMap Name)
|
||||||
|
, nextVar :: IORef Int
|
||||||
|
}
|
||||||
|
|
||||||
|
newGlobals :: IO (Globals)
|
||||||
|
newGlobals = do
|
||||||
|
vs <- newIORef (M.empty)
|
||||||
|
ns <- newIORef (M.empty)
|
||||||
|
next <- newIORef 0
|
||||||
|
return $ Globals { values = vs, names = ns, nextVar = next }
|
||||||
|
|
||||||
|
newVarPrim :: Name -> PrologIO Var
|
||||||
|
newVarPrim name = PrologIO $ \globals -> do
|
||||||
|
var <- readIORef (nextVar globals)
|
||||||
|
modifyIORef (names globals) (M.insert var name)
|
||||||
|
modifyIORef (nextVar globals) succ
|
||||||
|
return (VInt var)
|
||||||
|
|
||||||
|
unnewVarPrim :: PrologIO ()
|
||||||
|
unnewVarPrim = PrologIO $ \globals -> do
|
||||||
|
modifyIORef (nextVar globals) pred
|
||||||
|
var <- readIORef (nextVar globals)
|
||||||
|
modifyIORef (names globals) (M.delete var)
|
||||||
|
return ()
|
||||||
|
|
||||||
|
getVarPrim :: Var -> PrologIO (Maybe Term)
|
||||||
|
getVarPrim (VInt var) = PrologIO $ \globals ->
|
||||||
|
fmap (M.lookup var) (readIORef (values globals))
|
||||||
|
|
||||||
|
setVarPrim :: Var -> Maybe Term -> PrologIO ()
|
||||||
|
setVarPrim (VInt var) term = PrologIO $ \globals -> do
|
||||||
|
modifyIORef (values globals) (M.alter (\_ -> term) var)
|
||||||
|
return ()
|
||||||
|
|
||||||
|
errorPrim :: String -> PrologIO a
|
||||||
|
errorPrim message = error message
|
||||||
|
|
||||||
|
instance LiftIO PrologIO where
|
||||||
|
liftIO x = PrologIO (\_ -> x)
|
17
app/Terms.hs
Normal file
17
app/Terms.hs
Normal file
@ -0,0 +1,17 @@
|
|||||||
|
module Terms(
|
||||||
|
Atom,
|
||||||
|
Name,
|
||||||
|
Term(..),
|
||||||
|
Var(..),
|
||||||
|
) where
|
||||||
|
|
||||||
|
type Atom = String
|
||||||
|
type Name = String
|
||||||
|
|
||||||
|
data Term
|
||||||
|
= Compound Atom [Term] -- functor, args
|
||||||
|
| Var Var
|
||||||
|
deriving (Eq, Show)
|
||||||
|
|
||||||
|
newtype Var = VInt Int
|
||||||
|
deriving (Ord, Eq, Show)
|
@ -61,13 +61,13 @@ executable prolog-in-haskell
|
|||||||
main-is: Main.hs
|
main-is: Main.hs
|
||||||
|
|
||||||
-- Modules included in this executable, other than Main.
|
-- Modules included in this executable, other than Main.
|
||||||
-- other-modules:
|
other-modules: Binding, Classes, Database, Nondeterminism, Primitives, Terms
|
||||||
|
|
||||||
-- LANGUAGE extensions used by modules in this package.
|
-- LANGUAGE extensions used by modules in this package.
|
||||||
-- other-extensions:
|
-- other-extensions:
|
||||||
|
|
||||||
-- Other library packages from which modules are imported.
|
-- Other library packages from which modules are imported.
|
||||||
build-depends: base ^>=4.20.0.0, containers^>=0.8, mtl^>=2.3
|
build-depends: base ^>=4.20.0.0, containers^>=0.8
|
||||||
|
|
||||||
-- Directories containing source files.
|
-- Directories containing source files.
|
||||||
hs-source-dirs: app
|
hs-source-dirs: app
|
||||||
|
Loading…
x
Reference in New Issue
Block a user