{-# LANGUAGE RecordWildCards #-} module Language.DSKanren.Core ( Term(..) , Var , Neq , (===) , (=/=) , fresh , conj , disconj , Predicate , failure , success , currentGoal , run ) where import Control.Monad.Logic import Data.String import qualified Data.Map as M -- | The abstract type of variables. As a consumer you should never -- feel the urge to manipulate these directly. newtype Var = V Integer deriving (Eq, Ord) instance Show Var where show (V i) = '_' : show i suc :: Var -> Var suc (V i) = V (i + 1) -- | The terms of our logical language. data Term = Var Var -- ^ Logical variables that can unify with other terms | Atom String -- ^ The equivalent of Scheme's symbols or keywords | Pair Term Term -- ^ Pairs of terms deriving Eq instance Show Term where show t = case t of Var v -> show v Atom a -> '\'' : a Pair l r -> "(" ++ show l ++ ", " ++ show r ++ ")" instance IsString Term where fromString = Atom type Sol = M.Map Var Term -- | Substitute all bound variables in a term giving the canonical -- term in an environment. Sometimes the solution isn't canonical, -- so some ugly recursion happens. Happily we don't have to prove -- normalization. canonize :: Sol -> Term -> Term canonize sol t = case t of Atom a -> Atom a Pair l r -> canonize sol l `Pair` canonize sol r Var i -> maybe (Var i) (canonize $ M.delete i sol) $ M.lookup i sol -- | Ensures that a variable doesn't occur in some other term. This -- prevents us from getting some crazy infinite term. None of that -- nonsense. notIn :: Var -> Term -> Bool notIn v t = case t of Var v' -> v /= v' Atom _ -> True Pair l r -> notIn v l && notIn v r -- | Extend an environment with a given term. Note that -- that we don't even bother to canonize things here, that -- can wait until we extact a solution. extend :: Var -> Term -> Sol -> Sol extend = M.insert -- | Unification cannot need not backtrack so this will either -- universally succeed or failure. Tricksy bit, we don't want to allow -- infinite terms since that can be narly. To preserve reflexivity, we -- have a special check for when we compare a var to itself. This -- doesn't extend the enviroment. With this special case we can add a -- check to make sure we never unify a var with a term containing it. unify :: Term -> Term -> Sol -> Maybe Sol unify l r sol= case (l, r) of (Atom a, Atom a') | a == a' -> Just sol (Pair h t, Pair h' t') -> unify h h' sol >>= unify t t' (Var i, Var j) | i == j -> Just sol (Var i, t) | i `notIn` t -> Just (extend i t sol) (t, Var i) | i `notIn` t -> Just (extend i t sol) _ -> Nothing type Neq = (Term, Term) data State = State { sol :: Sol , var :: Var , neq :: [Neq] } newtype Predicate = Predicate {unPred :: State -> Logic State} -- | Validate the inqualities still hold. -- To do this we try to unify each pair under the current -- solution, if this fails we're okay. If they *don't* then -- make sure that the solution under which they unify is an -- extension of the solution set, ie we must add more facts -- to get a contradiction. checkNeqs :: State -> Logic State checkNeqs s@State{..} = foldr go (return s) neq where go (l, r) m = case unify (canonize sol l) (canonize sol r) sol of Nothing -> m Just badSol -> if domain badSol == domain sol then mzero else m domain = M.keys -- | Equating two terms will attempt to unify them and backtrack if -- this is impossible. (===) :: Term -> Term -> Predicate (===) l r = Predicate $ \s@State {..} -> case unify (canonize sol l) (canonize sol r) sol of Just sol' -> checkNeqs s{sol = sol'} Nothing -> mzero -- | The opposite of unification. If any future unification would -- cause these two terms to become equal we'll backtrack. (=/=) :: Term -> Term -> Predicate (=/=) l r = Predicate $ \s@State{..} -> checkNeqs s{neq = (l, r) : neq} -- | Generate a fresh (not rigid) term to use for our program. fresh :: (Term -> Predicate) -> Predicate fresh withTerm = Predicate $ \State{..} -> unPred (withTerm $ Var var) $ State sol (suc var) neq -- | Conjunction. This will return solutions that satsify both the -- first and second predicate. conj :: Predicate -> Predicate -> Predicate conj p1 p2 = Predicate $ \s -> unPred p1 s >>- unPred p2 -- | Disjunction. This will return solutions that satisfy either the -- first predicate or the second. disconj :: Predicate -> Predicate -> Predicate disconj p1 p2 = Predicate $ \s -> unPred p1 s `interleave` unPred p2 s -- | The Eeyore of predicates, always fails. This is mostly useful as -- a way of pruning out various conditions, as in -- @'conj' (a '===' b) 'failure'@. This is also an identity for -- 'disconj'. failure :: Predicate failure = Predicate $ const mzero -- | The Tigger of predicates! always passes. This isn't very useful -- on it's own, but is helpful when building up new combinators. This -- is also an identity for 'conj'. success :: Predicate success = Predicate return -- | The goal that this logic program is trying to create. This is -- occasionally useful when we're doing generating programs. currentGoal :: Term currentGoal = Var (V 0) -- | Run a program and find all solutions for the parametrized term. run :: (Term -> Predicate) -> [(Term, [Neq])] run mkProg = map answer . observeAll $ prog where prog = unPred (fresh mkProg) (State M.empty (V 0) []) answer State{..} = (canonize sol . Var $ V 0, neq)