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)
------------------------------------------------------------------------------------------

HOAS based self interpreter for lambda calculus

Just copied this out of Self-applicable Partial Evaluation for Pure Lambda Calculus

(define-syntax Q ; quote a lambda term
  (syntax-rules (lambda)
    ((Q (lambda (x) M)) (lambda (a)
                          (lambda (b)
                            (lambda (c)
                              (a (lambda (x) (Q M)))))))
    ((Q (M N)) (lambda (a)
                 (lambda (b)
                   (lambda (c)
                     ((b (Q M)) (Q N))))))
    ((Q x) (lambda (a)
             (lambda (b)
               (lambda (c)
                 (c x)))))))

(define E ; evaluate a quoted lambda term
  ((lambda (m)
    ((lambda (f) (m (lambda (a) ((f f) a))))
     (lambda (f) (m (lambda (a) ((f f) a))))))
   (lambda (E)
     (lambda (t)
       (((t (lambda (M) (lambda (x) (E (M x)))))
         (lambda (M) (lambda (N) ((E M) (E N)))))
        (lambda (x) x))))))

(define test-1
  (E (Q (lambda (i) i))))

(define test-2
  (E (Q (((lambda (m)
            ((lambda (f) (m (lambda (a) ((f f) a))))
             (lambda (f) (m (lambda (a) ((f f) a))))))
          (lambda (E)
            (lambda (t)
              (((t (lambda (M) (lambda (x) (E (M x)))))
                (lambda (M) (lambda (N) ((E M) (E N)))))
               (lambda (x) x)))))
         (lambda (a) (lambda (b) (lambda (c) (a (lambda (i) (lambda (a) (lambda (b) (lambda (c) (c i)))))))))))))

; ((lambda (i) i) 'ok)
; ok 
; > (test-1 'ok)
; ok
; > (test-2 'ok)
; ok

Rascal - Mini-haskell like language

http://rascal-haskell.googlecode.com/files/Rascal.zip
http://code.google.com/p/rascal-haskell/source/checkout

Thank you to google for hosting this.

more code: http://code.google.com/p/janus-haskell/

more still: http://prolog-thoughts.googlecode.com/files/Prolog.zip