Interpreter for Prolog without cut

I thought this was a good way to write a Prolog interpreter but it is very hard to add cut to. How could it be done?

{-# OPTIONS_GHC -XTypeOperators #-}
{-# OPTIONS_GHC -fno-monomorphism-restriction #-}

import Prelude hiding ((.),(+))
import Data.List hiding (groupBy)
import Control.Applicative
import Control.Monad
import Control.Monad.State
import Control.Monad.List
import Control.Monad.Identity
import Control.Arrow

infix 8 ≡
infix 8 ⤴
infix 8 ↗

(.) = fmap
(<||>) = liftA2 (||)
(&) = liftM2 (,)
p << q = do x <- q ; p ; return x
message `should` assertion = if assertion then mzero else return ()

groupBy p [] = []
groupBy p (x:xs) = let (yes,no) = sift p (p x) (x:xs)
                    in yes : groupBy p no

sift p e = foldr sort ([],[])
 where sort x (ys,ns) | e == p x  = (x:ys,ns)
                      | otherwise = (ys,x:ns)

type Identifier = String
type Name = String
type Arity = Integer
------------------------------------------------------------------------------------------

------------------------------------------------------------------------------------------
type key :--> val = [(key,val)]
(k ~~> v) σ = (k,v):σ

-- type key -> val
(i --> t) σ = \e -> if e == Var i then t else σ e
------------------------------------------------------------------------------------------

------------------------------------------------------------------------------------------
data Term = Var Identifier | (Name,Arity):>[Term]  deriving Eq

instance Show Term where
 show (Var v) = v
 show ((name,0):>[]) = name
 show ((name,_):>args) = name ++ "(" ++ intercalate "," (show . args) ++ ")"

functor (f:>_) = f
variables (Var v) = [v] ; variables (_:>vs) = variables=<<vs

σ⤴ t = case σ t of p:>ps -> p:>(σ↗ps) ; v -> if t == v then t else σ⤴ v
σ↗ ts = (σ⤴).ts

i `occur` Var _ = False
i `occur` (_:>ts) = any ((== Var i) <||> (i `occur`)) ts

(p:>ps ≡ q:>qs) σ = do "Cyclic" `should` (p /= q) ; foldM unify σ (zip (σ↗ ps) (σ↗ qs))
(Var x ≡ t) σ = do "Occurs check" `should` (x `occur` (σ⤴ t)) ; return $ (x --> t) σ
(t ≡ Var x) σ = (Var x ≡ t) σ
unify σ (p,q) = (p ≡ q) σ
------------------------------------------------------------------------------------------

------------------------------------------------------------------------------------------
type Gensym k v m a = StateT (k :--> v,[v]) m a

withGensyms freshVariables = flip evalStateT ([],freshVariables)
names = flip replicateM ['A'..'Z'] =<< [1..]

gensym k = get >>= \(sto,g:gs) -> case lookup k sto of
  Nothing -> do put ((k ~~> g) sto,gs) ; return g
  Just v  -> do                          return v

putSupply = modify . second . const
symScope p = get >>= runStateT p >>= \(v,s) -> putSupply (snd s) >> return v

copyTerm (Var v) = Var . gensym v
copyTerm (a:>as) = (a:>) . mapM copyTerm as
copyRule (p,q) = symScope (copyTerm p & mapM copyTerm q)
------------------------------------------------------------------------------------------

------------------------------------------------------------------------------------------
type Prolog m a = ListT (StateT (Identifier :--> Identifier,[Identifier]) m) a
--type Prolog m a = ListT (StateT (Identifier :--> Identifier,[Identifier]) (StateT Bool m)) a

type Database = [((Name, Arity), [(Term, [Term])])]

--cut = lift $ lift $ put True
--uncut = lift $ lift $ put False
--branch p q = do b <- lift $ lift $ get ; if b then p else q

clause :: Database -> (Name,Arity) -> Prolog Identity (Term, [Term])
clause db functor = ListT . mapM copyRule $ lookup' db functor
lookup' q db = maybe [] id (lookup db q)

(?-) :: (Database,Term -> Term) -> Term -> Prolog Identity (Term -> Term)
--(db,σ) ?- (("!",0):>[]) = do cut ; return σ
(db,σ) ?- query = do (head,body) <- clause db (functor query)
                     σ <- (head ≡ query) σ
                     foldM (prove db) σ body

prove db σ query = (db,σ) ?- (σ⤴ query)

runQuery db query = map (⤴ query).
  runIdentity.
--    flip evalStateT False.
      withGensyms (names \\ variables query).
        runListT$
          (db,id) ?- query
------------------------------------------------------------------------------------------

------------------------------------------------------------------------------------------
data Syntax = Term :- [Term]
makeRule (head :- body) = (functor head,[(head,body)])
mergeGroups ((functor,body):rest) = (functor,concat (body:map snd rest))
exampleDb :: Database
exampleDb = map mergeGroups $ groupBy fst $ map makeRule
 [true :- [],
 
  Var "X" == Var "X" :- [],
  
  call(Var "P") :- [Var "P"],
  
  and(Var "This",Var "That") :- [Var "This", Var "That"],
  
  or(Var "This",Var "That") :- [Var "This"],
  or(Var "This",Var "That") :- [Var "That"],
  
--  not(Var "P") :- [call(Var "P"), (!), fail],
--  not(Var "P") :- [],
  
  flip(heads) :- [],
  flip(tails) :- [],
  
  n(z) :- [],
  n(s(Var "N")) :- [n(Var "N")],
  
  member(Var"E", Var "E" . Var "Xs") :- [],
  member(Var"E", Var "X" . Var "Xs") :- [member(Var "E",Var "Xs")],
  
  append(nil,               Var "Ys",Var "Ys") :- [],
  append(Var "X" . Var "XS",Var "YS",Var "X" . Var "Zs") :- [append(Var "XS",Var "YS",Var "Zs")] 
  
  ] where true = ("true",0):>[];fail = ("fail",0):>[]
          x==y = ("=",2):>[x,y]
          call(p) = ("call",1):>[p];flip(p) = ("flip",1):>[p];not(p) = ("not",1):>[p]
          (!) = ("!",0):>[];heads = ("heads",0):>[];tails = ("tails",0):>[]
          and(p,q) = (",",2):>[p,q];or(p,q) = (";",2):>[p,q]
          member(x,y) = ("member",2):>[x,y];append(x,y,z) = ("append",3):>[x,y,z]
          nil = ("[]",0):>[];t . ts = (".",2):>[t,ts]
          z = ("z",0):>[];s(x) = ("s",1):>[x];n(x) = ("n",1):>[x]

instance Show Syntax where
  show (head :- []) = show head ++ "."
  show (head :- body) = show head ++ " :- " ++ intercalate ", " (map show body) ++ "."

showDb = unlines (map show exampleDb)
------------------------------------------------------------------------------------------