query :: [Clause] -> [Atom] -> [Substitution] query cs [] = return M.empty query cs (a : as) = do u1 <- single cs a u2 <- query cs $ map ( apply u1 ) as return $ u1 `times` u2
single :: [Clause] -> Atom -> [Substitution] single cs a = do c <- cs let c' = rename c u1 <- maybeToList $ unify a $ head c' u2 <- query cs $ map ( apply u1 ) $ body c' return $ u1 `times` u2