[Initial revision the second.
martin.hofmann@uni-bamberg.de**20081113091923] addfile ./src/Advancement.hs
adddir ./src/Data
addfile ./src/Data.hs
addfile ./src/Data/HypoSpace.hs
addfile ./src/Data/Hypotheses.hs
addfile ./src/Data/IOData.hs
addfile ./src/Data/IgorData.hs
addfile ./src/Data/PSQueue.hs
addfile ./src/Data/Rules.hs
addfile ./src/Data/Test.hs
addfile ./src/Data/Util.hs
addfile ./src/IgorMonad.hs
adddir ./src/Logging
addfile ./src/Logging.hs
addfile ./src/Logging/Logger.hs
addfile ./src/Logging/PrettyPrinter.hs
adddir ./src/Terms
addfile ./src/Terms.hs
addfile ./src/Terms/Antiunifier.hs
addfile ./src/Terms/Class.hs
addfile ./src/Terms/Unifier.hs
addfile ./src/Test.hs
addfile ./src/Test.lhs
hunk ./src/Advancement.hs 1
-
+
+module Advancement where
+
+import Data.Rules
+import Terms
+import IgorMonad
+
+--advanceRule :: Rule -> IM Rules
+--advanceRule  = rulesFromList.(:[])
+
+partition :: Rule -> IM [(Rule,FunFragment)]
+
+type FunFragment = (Name,Rules)
+
+functionCall :: 
+    Rule ->                 -- ^the rule to partition 
+                            --  FIXME: need covered target rules here) 
+    IM (Rule,[FunFragment]) -- ^the modified rule(now closed), and the 
+                            -- synthesised subfunctions
+functionCall r = return (r,[])          -- FIXME
+-- TODO:
+-- * uses abduce :: Rules -> Rules -> IM FunFragment
+-- * find a Funfragment 'frag' in background knowledge which contains a rule f
+--   for each rule in the rules covered by r (covering(r)) which matches its rhs
+-- * create a ne rules from 'r' by replacing its rhs by a function call to 'frag'
+-- * for each argument of 'frag' abduce the I/O pairs for a subfunction which
+--   returns the argument value from the input of r
+   
+subfunction :: 
+    Rule ->                 -- ^the rule to partition 
+                            --  FIXME: need covered target rules here) 
+    IM (Rule,[FunFragment]) -- ^the modified rule (now closed), and the 
+                            -- synthesised subfunctions
+subfunction r = return (r,[])          -- FIXME
+-- TODO:
+-- * uses abduce :: Rules -> Rules -> IM FunFragment
+-- * replace every open variable by a call to a subfunction 
+-- * abduce I/O pairs for every subfunction
+-- * the abduced I/O pairs of each subfunction are added to the background 
+--   knowledge (check if it is feasible to modify the IM at this point or 
+--   better at top-level 
+-- * synthesize every subfunction recursively. 
+--   !!! 
+--       If inserting the synthesized function into a hypothese,
+--       a hypothese should never be strict  
+--   !!!
+ 
hunk ./src/Data/HypoSpace.hs 1
-
+{-# OPTIONS_GHC -fglasgow-exts #-}
+module Data.HypoSpace (
+    HSpace, initHSpace, insert, delete, update,
+    bestHypos
+    
+    
+    
+
+) where
+
+import qualified Data.Rules as R (fold)
+import Data.Rules (Rule, rule, Rules, rules, RatingData, Rateable(..))
+import qualified Data.Hypotheses as H 
+import Data.Hypotheses (Hypo, hypo, updateRule, fold, Hypos, openRs, closedRs, allRs)
+import qualified Data.Hypotheses as Hs
+
+import qualified Data.Set as S
+import qualified Data.Map as M
+import Control.Monad (liftM)
+import Data.Maybe (maybeToList)
+
+import Text.Show
+import Data.Util (showAsSet)
+  
+import Debug.Trace                        
+
+{- 
+ |-----------------------------------------------------------------------------
+ | Datatype Definitions
+ |----------------------------------------------------------------------------- 
+-}
+
+
+
+
+
+
+-- | Hypotheses Space
+{- Hypospace is a Priority Queue, where each element is a Set of Hypotheses with
+ | equal RatingData. Thus a each element isan  equivalence classes over 
+ | hypotheses which are prioritized over the RatingData in ascending order.
+-} 
+data  HSpace = HSpace
+    { rateHyposMap :: !(M.Map RatingData Hypos) -- 
+    , ruleHyposMap :: !(M.Map Rule Hypos)
+    , hypoRateMap  :: !(M.Map Hypo RatingData)
+    }
+
+
+-- | /O(1)/, create an empty Search Space
+initHSpace :: HSpace
+initHSpace = HSpace 
+    { rateHyposMap  = M.empty
+    , ruleHyposMap = M.empty
+    , hypoRateMap = M.empty
+    }
+
+-- | /O(log n)/, insert a new hypothese into the search space
+insert :: Hypo -> HSpace -> HSpace
+insert h (HSpace pri rhm hrm) = HSpace
+    { rateHyposMap  = M.alter (Hs.insert h) (rate h) pri
+    , ruleHyposMap  = R.fold (M.alter (Hs.insert h)) rhm (allRs h)
+    , hypoRateMap   = M.insert h (rate h) hrm
+    }
+    
+   
+
+ -- | /O(log n)/, delete a hypothese from the search space   
+delete :: Hypo -> HSpace -> HSpace
+delete h hsp@(HSpace pri rhm hrm) = HSpace
+    { rateHyposMap   = case (M.lookup h hrm) of 
+                      Just r  -> M.alter  (Hs.delete h) r pri
+                      Nothing -> pri
+    , ruleHyposMap = R.fold (M.alter (Hs.delete h)) rhm (allRs h)
+    , hypoRateMap  = M.delete h hrm
+    }
+    
+replace :: Hypo -> Hypo -> HSpace -> HSpace       
+replace ho hn = (insert hn).(delete ho)
+
+-- | /O(m log n)/ where m is the number of affected hypotheses and n the number 
+--   of total rules
+update :: Rule -> Rule -> HSpace -> HSpace
+update ro rn hsp   = ins $ del hsp
+    
+    where
+    del = \sp -> Hs.fold delete sp affectedHs
+    ins = \sp -> Hs.fold insert sp modifiedHs
+    affectedHs = case M.lookup  ro (ruleHyposMap hsp) of 
+                    Just hs -> hs
+                    Nothing -> Hs.empty
+    -- get all affected Hypos 
+    modifiedHs = Hs.map (updateRule ro rn) affectedHs
+    -- update the rules in each hypo     
+
+
+-- | /O(log n)/ find the best valued Hypotheses
+bestHypos :: HSpace -> Hypos
+bestHypos         = snd . M.findMin . rateHyposMap 
+
+
+
+ 
+ 
+
+-- DEPRECATED
+---- | /alterPrios f k h/ alters the 'priorities' of 'h' at key position 'k' with
+----   function 'f' and leaves the other record lsots of 'h' unchanged
+--alterPrios :: (Maybe Hypos -> Maybe Hypos) -> RatingData -> HSpace -> HSpace
+--alterPrios f k (HSpace p r h) = let
+--    p' = Q.alter f k p
+--    in (HSpace p' r h)
+--
+---- | /alterRHM f r h/ alters the 'ruleHyposMap' of 'h' at key position 'k' with
+----   function 'f' and leaves the other record lsots of 'h' unchanged
+--alterRHM :: (Maybe Hypos -> Maybe Hypos) -> Rule -> HSpace -> HSpace
+--alterRHM f k (HSpace p r h) = let
+--    r' = M.alter f k r
+--    in (HSpace p r' h)
+--
+---- | folds all hypotheses in Hypos over the 'ruleHyposMap' of
+----   the HSpace using 'f'
+--foldRHM :: (Rule -> M.Map Rule Hypos -> M.Map Rule Hypos)
+--           -> Rules -> HSpace -> HSpace    
+--foldRHM f hs (HSpace p r h) = let 
+--    r' = R.fold f r hs
+--    in (HSpace p r' h)
+--
+--
+---- | /alterHRM f r h/ alters the 'hypoRateMap' of 'h' at key position 'k' with
+----   function 'f' and leaves the other record lsots of 'h' unchanged
+--alterHRM :: (Maybe RatingData -> Maybe RatingData) -> Hypo -> HSpace -> HSpace
+--alterHRM f k (HSpace p r h) = let
+--    h' = M.alter f k h
+--    in (HSpace p r h')   
+--
+--
+---- | folds the elemens in the Set (usually hypos) over the 'hypoRateMap' of
+----   the HSpace using 'f'    
+--foldHRM :: (a -> M.Map Hypo RatingData -> M.Map Hypo RatingData)
+--           -> [a] -> HSpace -> HSpace    
+--foldHRM f hs (HSpace p r h) = let
+--    h' = foldr f h hs
+--    in (HSpace p r h')   
+
+    
+    
+--{- -----------------------------------------------------------------------------
+-- | Show instances and pretty printing stuff
+------------------------------------------------------------------------------- -}
+
+
+    
+
+             
+        
+    
+instance Show HSpace where
+    show hsp = showString "HSpace {\nrateHyposMap =\n" .
+               shows (rateHyposMap hsp) .
+               showString "\nruleHyposMap =\n" .
+               showAsSet (M.toList (ruleHyposMap hsp)) .
+               showString "\nhypoRateMap =\n" .
+               showAsSet (M.toList (hypoRateMap hsp)) $
+               "\n}"
+
+               
+rule1 = rule 1 "a"
+rule2 = rule 2 "b"
+rule3 = rule 3 "c"
+rule4 = rule 4 "d"
+rule5 = rule 5 "e"
+rule6 = rule 6 "f"
+rule7 = rule 7 "g"
+rule8 = rule 8 "h"
+rule9 = rule 9 "i"
+rule10 = rule 10 "j"
+
+rule1' = rule 1 "aaaaaaaaa"
+rule2' = rule 2 "bbbbbbbbbbbbbbbbbbbb"
+rule3' = rule 3 "ccc"
+rule4' = rule 4 "ddd"
+rule5' = rule 5 "eeeeeeeeeeeeeeee"
+rule6' = rule 6 "fff"
+rule7' = rule 7 "ggg"
+rule8' = rule 8 "hhh"
+rule9' = rule 9 "iii"
+rule10' = rule 10 "jjj"
+
+rules1o = rules [rule1,rule2,rule3]
+rules1c = rules [rule4,rule5]
+rules1ao = rules [rule1]
+rules1ac = rules [rule4,rule5]
+rules1bo = rules [rule1,rule2,rule3]
+rules1bc = rules [rule4,rule5]
+rules1co = rules [rule6]
+rules1cc = rules [rule4,rule5]
+rules2o = rules [rule6,rule7,rule8]
+rules2c = rules [rule9,rule10]
+rules3o = rules [rule1,rule6,rule8]
+rules3c = rules [rule4,rule10]
+rules4o = rules [rule9,rule2,rule3]
+rules4c = rules [rule9,rule5]
+
+
+hypo1 = hypo rules1o rules1c
+hypo1a = hypo rules1ao rules1ac
+hypo1b = hypo rules1bo rules1bc
+hypo1c = hypo rules1co rules1cc
+hypo2 = hypo rules2o rules2c
+hypo3 = hypo rules3o rules3c
+hypo4 = hypo rules4o rules4c
+
+hsp = initHSpace
+hsp1 = insert hypo1 hsp
+hsp1a = insert hypo1c hsp1
+hsp2 = insert hypo2 hsp1
+
+hsp3 = insert hypo3 hsp2
+hsp4 = insert hypo4 hsp3
+hsp5 = insert hypo1b hsp4
+hsp6 = insert hypo1c hsp5
+               
hunk ./src/Data/Hypotheses.hs 1
+{-# OPTIONS_GHC -fglasgow-exts #-}
+module Data.Hypotheses (
+
+    Hypo, openRs, closedRs, allRs, 
+    hypo, updateRule,
+    
+    Hypos, empty, singleton, null,
+    merge, insert, delete, replace,
+    
+    map, fold
+
+
+    )where
+
+import Prelude hiding (null, map)
+import Data.Rules (Rule, Rules, rule, rules, isOpen, Rateable(..), RatingData, )
+import qualified Data.Rules as R (insert,delete, replace, map, fold, union)
+import Data.Util (showAsSet)
+import Data.Set (Set)
+import qualified Data.Set as S
+
+--------------------------------------------------------------------------------
+-- | Hypothese
+--------------------------------------------------------------------------------
+
+data Hypo  = HH { open   :: Rules
+                , closed :: Rules
+                }
+    deriving(Eq, Ord)
+
+-- should be more like this
+--data Hypo  = HH { open   :: [(Rule,[Int])]
+--                , closed :: Rules
+--                }
+-- where the Ints are the indices of the covered rule, stored in IOData
+
+
+{- ----------
+ | Instance declarations of data type 'Hypo'
+-} ----------
+instance Show Hypo where
+    show (HH o c) = showString "Hypo(o" .
+                    shows o .
+                    showString ",c" .
+                    shows c $
+                    ")"
+       
+instance Rateable Hypo where
+    rate h       = R.fold (\r d -> (rate r)+d) 0 (open h)
+
+      
+--instance Ord Hypo where
+--    compare = ( \l r -> compare (rate l) (rate r) )
+--    (<)     = ( \l r -> (<) (rate l) (rate r) )
+--    (<=)    = ( \l r -> (<=) (rate l) (rate r) )
+--    (>=)    = ( \l r -> (>=) (rate l) (rate r) )
+--    (>)     = ( \l r -> (>) (rate l) (rate r) )  
+
+    
+-- | Constructor for data type 'Hypothese'
+hypo 
+     :: Rules   -- ^open rules 
+     -> Rules   -- ^closed rules
+     -> Hypo    
+hypo ro rc  = HH ro rc
+
+-- | Accessors for Hypothese
+openRs, closedRs, allRs :: Hypo -> Rules
+openRs   = open
+closedRs = closed
+allRs h  = R.union (open h) (closed h)
+
+     
+-- | Modifiers for data type 'Hypo'
+updateRule 
+     :: Rule    -- ^replace/update old rule
+     -> Rule    -- ^with new rule
+     -> Hypo    -- ^in hypothese
+     -> Hypo
+updateRule rold rnew h = 
+    let
+        openrs = if isOpen rnew
+                    then R.replace rold rnew $ open $ h
+                    -- we assume a new rule to be 'brand' new
+                    else R.delete rold $ open $ h
+        clsdrs = if (isOpen rnew)
+                    then closed  h
+                    else R.insert rnew $ closed h
+        in hypo openrs clsdrs
+    
+--------------------------------------------------------------------------------
+-- | Hypotheses
+--------------------------------------------------------------------------------
+newtype Hypos = HHs {unHHs :: S.Set Hypo }
+    deriving(Eq, Ord)
+
+instance Show Hypos where
+    show hs = (showAsSet $ S.toList.unHHs $ hs) ""    
+    
+singleton :: Hypo -> Hypos
+singleton h = HHs $ S.singleton h
+
+hyposToSet = unHHs
+
+empty :: Hypos
+empty = HHs $ S.empty
+
+null :: Hypos -> Bool   
+null = S.null.unHHs  
+
+
+size :: Hypos -> Int
+size = S.size.unHHs
+
+
+fold :: (Hypo -> a -> a) -> a -> Hypos -> a
+fold f i rs = S.fold f i (unHHs rs)
+
+map :: (Hypo -> Hypo) -> Hypos -> Hypos
+map f hs  = HHs $ (S.map f) (unHHs hs)
+
+
+merge :: Hypos -> Hypos -> Hypos
+merge hs1 hs2 = HHs $ S.union (unHHs hs1) (unHHs hs2)
+
+insert :: Hypo -> Maybe Hypos -> Maybe Hypos  
+insert h Nothing   = Just $ singleton h
+insert h (Just hs) = Just $ HHs $ S.insert h (unHHs hs)
+
+delete :: Hypo -> Maybe Hypos -> Maybe Hypos
+delete _ Nothing = Nothing -- should, however, never be the case
+delete h (Just hs) = 
+    let postDel = HHs $ S.delete h (unHHs hs)
+    in if null postDel 
+         then Nothing
+         else Just postDel
+    
+replace :: Hypo -> Hypo -> Maybe Hypos -> Maybe Hypos
+replace h1 h2 hs = insert h1 (delete h2 hs)
hunk ./src/Data/IOData.hs 1
-
+
+module Data.IOData where
+
+import Data.Rules
+import Data.Hypotheses
+import Data.Bimap (Bimap)
+import qualified Data.Bimap as B
+import Terms
+
+{-
+ | IOData  
+-}
+data IOData = IOD 
+    { targetName :: Name
+    , targetIO :: Rules
+    , backgroundKnowledge :: Bimap Name Rules 
+    }
+
+-- | /O(1)/creates an empty IOdata value
+emptyIOData :: IOData
+emptyIOData = IOD
+    { targetName = mkName "" 
+    , targetIO = rules []
+    , backgroundKnowledge = B.empty
+    }
+
+{-
+ | /O(log n)/ Creates an IOData value with given Name-Rules-associations. It is neither 
+ | checked, whether some Names or Rules do occur more than once. If so, 
+ | overlapping associations are deleted. 
+-}
+initIOData :: [(Name,Rules)] -> IOData
+initIOData nrs =
+    foldr (\(n,r) -> insertUnsafe n r) emptyIOData nrs
+
+{-
+ | /O(log n)/ Insert the rules associated with the Name into the IOData, but only if 
+ |neither is already in IOData. 
+-}
+insertWithName :: Name -> Rules -> IOData -> IOData
+insertWithName n rs iod@(IOD{ backgroundKnowledge = bk }) =
+    iod{ backgroundKnowledge =  B.tryInsert n rs bk}
+
+
+{-
+ | /O(log n)/ Insert the rules into the IOData value. The resulting IOdata value
+ | paired with the key, the rules have been saved under, is returned. If the 
+ | rules have previously been stored, the old key is returned, otherwise a new 
+ | is generated. The 'key' is a TH Name, specifying the function name. 
+-}
+insert :: Rules -> IOData -> (Name,IOData)
+insert rs iod@(IOD{ backgroundKnowledge = bk }) =
+    case B.lookupR rs bk of
+        Just n  -> (n,iod)
+        Nothing -> (n',iod')
+    where
+    n' = mkName $ (++) "fun" $ show $ B.size bk
+    iod' = insertUnsafe n' rs iod
+
+
+lookupByName :: (Monad m) => Name -> IOData -> m Rules
+lookupByName n b = B.lookup n $ backgroundKnowledge b 
+
+
+lookupByRules :: (Monad m) => Rules -> IOData -> m Name
+lookupByRules rs b = B.lookupR rs $ backgroundKnowledge b 
+ 
+-- | Create a IOData value from a new I/O pairs of a new target function and an
+-- existing IOData value.
+--asNew :: (Name,Rules) -> IOData -> IOData
+-- TODO:
+--asNew (n,rs) iod =
+-- * insert old target function into background knowledge
+-- * check if new target function is in BK, if so, remove
+-- * set new target function as current target function 
+
+
+---------------------
+-- Unsafe functions
+---------------------
+{-
+ | /O(log n)/ Insert the rules associated with the Name into the IOData. If either rules or
+ | Name exists already in IOData, previous bindings are deleted. 
+-}
+insertUnsafe :: Name -> Rules -> IOData -> IOData
+insertUnsafe n rs iod@(IOD{ backgroundKnowledge = bk }) =
+    iod{ backgroundKnowledge =  B.insert n rs bk}
+    
+    
hunk ./src/Data/IgorData.hs 1
-
+
+module Data.IgorData where
+
+import Data.IOData
+import Data.HypoSpace
+import Data.Rules
+import Data.Hypotheses
+
+data Igor = Igor 
+    { iodata :: IOData, searchSpace :: HSpace}
hunk ./src/Data/PSQueue.hs 1
+{- |
+
+A /priority search queue/ (henceforth /queue/) efficiently supports the
+opperations of both a search tree and a priority queue. A 'Binding' is a
+product of a key and a priority. Bindings can be inserted, deleted, modified
+and queried in logarithmic time, and the binding with the least priority can be
+retrieved in constant time. A queue can be built from a list of bindings,
+sorted by keys, in linear time.
+
+This implementation is due to Ralf Hinze.
+
+* Hinze, R., /A Simple Implementation Technique for Priority Search Queues/, ICFP 2001, pp. 110-121
+
+<http://citeseer.ist.psu.edu/hinze01simple.html>
+
+-}
+
+-- Some modifications by Scott Dillard
+
+
+module Data.PSQueue
+    ( 
+    -- * Binding Type
+    Binding((:->))
+    , key
+    , prio
+    -- * Priority Search Queue Type
+    , PSQ
+    -- * Query
+    , size
+    , null
+    , lookup
+    -- * Construction
+    , empty
+    , singleton
+    -- * Insertion
+    , insert
+    , insertWith
+    -- * Delete/Update 
+    , delete
+    , adjust
+    , adjustWithKey
+    , update
+    , updateWithKey
+    , alter
+    -- * Conversion
+    , keys
+    , toList
+    , toAscList
+    , toDescList
+    , fromList
+    , fromAscList
+    , fromDistinctAscList
+    -- * Priority Queue
+    , findMin
+    , deleteMin
+    , minView
+    , atMost
+    , atMostRange
+    -- * Fold
+    , foldr
+    , foldl
+) where
+
+import Prelude hiding (lookup,null,foldl,foldr)
+import qualified Prelude as P
+
+{-
+-- testing
+import Test.QuickCheck
+import Data.List (sort)
+-}
+
+
+
+
+-- | @k :-> p@ binds the key @k@ with the priority @p@.
+data Binding k p = k :-> p deriving (Eq,Ord,Show,Read)
+
+infix 0 :->
+
+-- | The key of a binding
+key  :: Binding k p -> k
+key  (k :-> _) =  k
+
+-- | The priority of a binding
+prio :: Binding k p -> p
+prio (_ :-> p) =  p
+
+
+
+-- | A mapping from keys @k@ to priorites @p@. 
+
+data PSQ k p = Void | Winner k p (LTree k p) k
+
+instance (Show k, Show p, Ord k, Ord p) => Show (PSQ k p) where
+  --show = show . toAscList
+  show Void = "[]"
+  show (Winner k1 p lt k2) = "Winner "++show k1++" "++show p++" ("++show lt++") "++show k2
+
+
+
+
+-- | /O(1)/ The number of bindings in a queue.
+size :: PSQ k p -> Int
+size Void = 0
+size (Winner _ _ lt _) = 1 + size' lt
+
+-- | /O(1)/ True if the queue is empty.
+null :: PSQ k p -> Bool
+null Void = True
+null (Winner _ _ _ _) = False
+
+-- | /O(log n)/ The priority of a given key, or Nothing if the key is not
+-- bound.
+lookup :: (Ord k, Ord p) => k -> PSQ k p -> Maybe p
+lookup k q = 
+  case tourView q of
+    Null -> fail "PSQueue.lookup: Empty queue"
+    Single k' p
+      | k == k'   -> return p
+      | otherwise -> fail "PSQueue.lookup: Key not found"
+    tl `Play` tr
+      | k <= maxKey tl -> lookup k tl
+      | otherwise      -> lookup k tr
+
+
+
+empty :: (Ord k, Ord p) => PSQ k p
+empty = Void
+
+-- | O(1) Build a queue with one binding.
+singleton :: (Ord k, Ord p) => k -> p -> PSQ k p
+singleton k p =  Winner k p Start k
+
+
+-- | /O(log n)/ Insert a binding into the queue.
+insert :: (Ord k, Ord p) => k -> p -> PSQ k p -> PSQ k p
+insert k p q = 
+  case tourView q of
+    Null -> singleton k p
+    Single k' p' ->
+      case compare k k' of
+        LT -> singleton k  p  `play` singleton k' p'
+        EQ -> singleton k  p
+        GT -> singleton k' p' `play` singleton k  p
+    tl `Play` tr
+      | k <= maxKey tl -> insert k p tl `play` tr
+      | otherwise      -> tl `play` insert k p tr
+
+
+-- | /O(log n)/ Insert a binding with a combining function. 
+insertWith :: (Ord k, Ord p) => (p->p->p) -> k -> p -> PSQ k p -> PSQ k p
+insertWith f = insertWithKey (\_ p p'-> f p p')
+
+-- | /O(log n)/ Insert a binding with a combining function. 
+insertWithKey :: (Ord k, Ord p) => (k->p->p->p) -> k -> p -> PSQ k p -> PSQ k p
+insertWithKey f k p q =  
+  case tourView q of
+    Null -> singleton k p
+    Single k' p' ->
+      case compare k k' of 
+        LT -> singleton k  p  `play` singleton k' p'
+        EQ -> singleton k  (f k p p')
+        GT -> singleton k' p' `play` singleton k  p
+    tl `Play` tr
+      | k <= maxKey tl -> insertWithKey f k p tl `unsafePlay` tr
+      | otherwise      -> tl `unsafePlay` insertWithKey f k p tr
+
+
+
+-- | /O(log n)/ Remove a binding from the queue.
+delete :: (Ord k, Ord p) => k -> PSQ k p -> PSQ k p
+delete k q = 
+  case tourView q of
+    Null -> empty
+    Single k' p
+      | k == k'   -> empty
+      | otherwise -> singleton k' p
+    tl `Play` tr
+      | k <= maxKey tl -> delete k tl `play` tr
+      | otherwise      -> tl `play` delete k tr
+
+-- | /O(log n)/ Adjust the priority of a key.
+adjust ::  (Ord p, Ord k) => (p -> p) -> k -> PSQ k p -> PSQ k p
+adjust f = adjustWithKey (\_ p -> f p)
+
+-- | /O(log n)/ Adjust the priority of a key.
+adjustWithKey :: (Ord k, Ord p) => (k -> p -> p) -> k -> PSQ k p -> PSQ k p
+adjustWithKey f k q =  
+  case tourView q of
+    Null -> empty
+    Single k' p
+      | k == k'   -> singleton k' (f k p)
+      | otherwise -> singleton k' p
+    tl `Play` tr
+      | k <= maxKey tl -> adjustWithKey f k tl `unsafePlay` tr
+      | otherwise      -> tl `unsafePlay` adjustWithKey f k tr
+
+
+-- | /O(log n)/ The expression (@update f k q@) updates the
+-- priority @p@ bound @k@ (if it is in the queue). If (@f p@) is 'Nothing',
+-- the binding is deleted. If it is (@'Just' z@), the key @k@ is bound
+-- to the new priority @z@.
+
+update :: (Ord k, Ord p) => (p -> Maybe p) -> k -> PSQ k p -> PSQ k p
+update f = updateWithKey (\_ p -> f p)
+
+-- | /O(log n)/. The expression (@updateWithKey f k q@) updates the
+-- priority @p@ bound @k@ (if it is in the queue). If (@f k p@) is 'Nothing',
+-- the binding is deleted. If it is (@'Just' z@), the key @k@ is bound
+-- to the new priority @z@.
+
+updateWithKey :: (Ord k, Ord p) => (k -> p -> Maybe p) -> k -> PSQ k p -> PSQ k p
+updateWithKey f k q =  
+  case tourView q of
+    Null -> empty
+    Single k' p 
+      | k==k' -> case f k p of
+                  Nothing -> empty
+                  Just p' -> singleton k p'
+      | otherwise -> singleton k' p
+    tl `Play` tr
+      | k <= maxKey tl -> updateWithKey f k tl `unsafePlay` tr
+      | otherwise      -> tl `unsafePlay` updateWithKey f k tr
+
+
+-- | /O(log n)/. The expression (@'alter' f k q@) alters the priority @p@ bound to @k@, or absence thereof.
+-- alter can be used to insert, delete, or update a priority in a queue.
+alter :: (Ord k, Ord p) => (Maybe p -> Maybe p) -> k -> PSQ k p -> PSQ k p
+alter f k q =
+  case tourView q of
+    Null -> 
+      case f Nothing of
+        Nothing -> empty
+        Just p  -> singleton k p
+    Single k' p 
+      | k == k'   ->  case f (Just p) of
+                        Nothing -> empty
+                        Just p' -> singleton k' p'
+      | otherwise ->  case f Nothing of
+                        Nothing -> singleton k' p
+                        Just p' -> insert k p' $ singleton k' p
+    tl `Play` tr
+      | k <= maxKey tl -> alter f k tl `unsafePlay` tr
+      | otherwise      -> tl `unsafePlay` alter f k tr
+
+
+
+-- | /O(n)/ The keys of a priority queue
+keys :: (Ord k, Ord p) => PSQ k p -> [k]
+keys = map key . toList
+
+-- | /O(n log n)/ Build a queue from a list of bindings.
+fromList :: (Ord k, Ord p) => [Binding k p] -> PSQ k p
+fromList = P.foldr (\(k:->p) q -> insert k p q) empty
+
+-- | /O(n)/ Build a queue from a list of bindings in order of
+-- ascending keys. The precondition that the keys are ascending is not checked.
+fromAscList :: (Ord k, Ord p) => [Binding k p] -> PSQ k p
+fromAscList = fromDistinctAscList . stripEq 
+  where stripEq []         = []
+        stripEq (x:xs)     = stripEq' x xs
+        stripEq' x' []     = [x']
+        stripEq' x' (x:xs) 
+          | x' == x   = stripEq' x' xs
+          | otherwise = x' : stripEq' x xs
+
+-- | /O(n)/ Build a queue from a list of distinct bindings in order of
+-- ascending keys. The precondition that keys are distinct and ascending is not checked.
+fromDistinctAscList :: (Ord k, Ord p) => [Binding k p] -> PSQ k p
+fromDistinctAscList = foldm unsafePlay empty . map (\(k:->p) -> singleton k p)
+
+-- Folding a list in a binary-subdivision scheme.
+foldm :: (a -> a -> a) -> a -> [a] -> a
+foldm (*) e x
+  | P.null  x             = e
+  | otherwise             = fst (rec (length x) x)
+  where rec 1 (a : as)    = (a, as)
+        rec n as          = (a1 * a2, as2)
+          where m         = n `div` 2
+                (a1, as1) = rec (n - m) as 
+                (a2, as2) = rec m       as1
+
+-- | /O(n)/ Convert a queue to a list.
+toList :: (Ord k, Ord p) => PSQ k p -> [Binding k p]
+toList = toAscList
+
+-- | /O(n)/ Convert a queue to a list in ascending order of keys.
+toAscList :: (Ord k, Ord p) => PSQ k p -> [Binding k p]
+toAscList q  = seqToList (toAscLists q)
+
+toAscLists :: (Ord k, Ord p) => PSQ k p -> Sequ (Binding k p)
+toAscLists q = case tourView q of
+  Null -> emptySequ
+  Single k p -> singleSequ (k :-> p)
+  tl `Play` tr -> toAscLists tl <> toAscLists tr
+
+-- | /O(n)/ Convert a queue to a list in descending order of keys.
+toDescList :: (Ord k, Ord p) => PSQ k p -> [ Binding k p ]
+toDescList q = seqToList (toDescLists q)
+
+toDescLists :: (Ord k, Ord p) => PSQ k p -> Sequ (Binding k p)
+toDescLists q = case tourView q of 
+  Null -> emptySequ
+  Single k p -> singleSequ (k :-> p)
+  tl `Play` tr -> toDescLists tr <> toDescLists tl
+
+
+-- | /O(1)/ The binding with the lowest priority.
+findMin :: (Ord k, Ord p) => PSQ k p -> Maybe (Binding k p)
+findMin Void             = Nothing
+findMin (Winner k p t m) = Just (k :-> p) 
+
+-- | /O(log n)/ Remove the binding with the lowest priority.
+deleteMin :: (Ord k, Ord p) => PSQ k p -> PSQ k p
+deleteMin Void             = Void
+deleteMin (Winner k p t m) = secondBest t m
+
+-- | /O(log n)/ Retrieve the binding with the least priority, and the rest of
+-- the queue stripped of that binding. 
+minView :: (Ord k, Ord p) => PSQ k p -> Maybe (Binding k p, PSQ k p)
+minView Void             = Nothing
+minView (Winner k p t m) = Just ( k :-> p , secondBest t m )
+
+secondBest :: (Ord k, Ord p) => LTree k p -> k -> PSQ k p
+secondBest Start _m = Void
+secondBest (LLoser _ k p tl m tr) m' = Winner k p tl m `play` secondBest tr m'
+secondBest (RLoser _ k p tl m tr) m' = secondBest tl m `play` Winner k p tr m'
+
+
+
+-- | /O(r(log n - log r)/ @atMost p q@ is a list of all the bindings in @q@ with
+-- priority less than @p@, in order of ascending keys.
+-- Effectively, 
+--
+-- @
+--   atMost p' q = filter (\\(k:->p) -> p<=p') . toList
+-- @
+atMost :: (Ord k, Ord p) => p -> PSQ k p -> [Binding k p]
+atMost pt q = seqToList (atMosts pt q)
+
+atMosts :: (Ord k, Ord p) => p -> PSQ k p -> Sequ (Binding k p)
+atMosts _pt Void  = emptySequ
+atMosts pt (Winner k p t _) =  prune k p t
+  where
+  prune k p t
+    | p > pt         = emptySequ
+    | otherwise      = traverse k p t
+  traverse k p Start = singleSequ (k :-> p)
+  traverse k p (LLoser _ k' p' tl _m tr) = prune k' p' tl <> traverse k p tr
+  traverse k p (RLoser _ k' p' tl _m tr) = traverse k p tl <> prune k' p' tr
+
+-- | /O(r(log n - log r))/ @atMostRange p (l,u) q@ is a list of all the bindings in
+-- @q@ with a priority less than @p@ and a key in the range @(l,u)@ inclusive.
+-- Effectively,
+-- 
+-- @
+--    atMostRange p' (l,u) q = filter (\\(k:->p) -> l<=k && k<=u ) . 'atMost' p'
+-- @
+atMostRange :: (Ord k, Ord p) => p -> (k, k) -> PSQ k p -> [Binding k p]
+atMostRange pt (kl, kr) q = seqToList (atMostRanges pt (kl, kr) q)
+
+atMostRanges :: (Ord k, Ord p) => p -> (k, k) -> PSQ k p -> Sequ (Binding k p)
+
+atMostRanges _pt _range Void = emptySequ
+atMostRanges pt range@(kl, kr) (Winner k p t _) = prune k p t
+  where
+  prune k p t
+    | p > pt    = emptySequ
+    | otherwise = traverse k p t
+  traverse k p Start
+    | k `inrange` range = singleSequ (k :-> p)
+    | otherwise         = emptySequ
+  traverse k p (LLoser _ k' p' tl m tr) =  
+    guard (kl <= m) (prune k' p' tl) <> guard (m <= kr) (traverse k p tr)
+  traverse k p (RLoser _ k' p' tl m tr) =  
+    guard (kl <= m) (traverse k p tl) <> guard (m <= kr) (prune k' p' tr)
+
+inrange :: (Ord a) => a -> (a, a) -> Bool
+a `inrange` (l, r)  =  l <= a && a <= r
+
+
+
+
+-- | Right fold over the bindings in the queue, in key order.
+foldr :: (Ord k,Ord p) => (Binding k p -> b -> b) -> b -> PSQ k p -> b
+foldr f z q = 
+  case tourView q of
+    Null -> z
+    Single k p -> f (k:->p) z
+    l`Play`r -> foldr f (foldr f z r) l
+    
+
+-- | Left fold over the bindings in the queue, in key order.
+foldl :: (Ord k,Ord p) => (b -> Binding k p -> b) -> b -> PSQ k p -> b
+foldl f z q = 
+  case tourView q of
+    Null -> z
+    Single k p -> f z (k:->p)
+    l`Play`r -> foldl f (foldl f z l) r
+
+
+
+
+-----------------------
+------- Internals -----
+----------------------
+
+type Size = Int
+
+data LTree k p = Start
+               | LLoser {-# UNPACK #-}!Size !k !p (LTree k p) !k (LTree k p)
+               | RLoser {-# UNPACK #-}!Size !k !p (LTree k p) !k (LTree k p)
+    deriving(Show)
+
+size' :: LTree k p -> Size
+size' Start                = 0
+size' (LLoser s _ _ _ _ _) = s
+size' (RLoser s _ _ _ _ _) = s
+
+left, right :: LTree a b -> LTree a b
+
+left  Start                   =  error "left: empty loser tree"
+left  (LLoser _ _ _ tl _ _ ) =  tl
+left  (RLoser _ _ _ tl _ _ ) =  tl
+
+right Start                   =  error "right: empty loser tree"
+right (LLoser _ _ _ _  _ tr) =  tr
+right (RLoser _ _ _ _  _ tr) =  tr
+
+maxKey :: PSQ k p -> k
+maxKey Void                =  error "maxKey: empty queue"
+maxKey (Winner _k _p _t m) =  m
+
+lloser, rloser :: k -> p -> LTree k p -> k -> LTree k p -> LTree k p
+lloser k p tl m tr =  LLoser (1 + size' tl + size' tr) k p tl m tr
+rloser k p tl m tr =  RLoser (1 + size' tl + size' tr) k p tl m tr
+
+--balance factor
+omega :: Int
+omega = 4
+
+lbalance, rbalance :: 
+  (Ord k, Ord p) => k-> p -> LTree k p -> k -> LTree k p -> LTree k p
+
+lbalance k p l m r
+  | size' l + size' r < 2     = lloser        k p l m r
+  | size' r > omega * size' l = lbalanceLeft  k p l m r
+  | size' l > omega * size' r = lbalanceRight k p l m r
+  | otherwise               = lloser        k p l m r
+
+rbalance k p l m r
+  | size' l + size' r < 2     = rloser        k p l m r
+  | size' r > omega * size' l = rbalanceLeft  k p l m r
+  | size' l > omega * size' r = rbalanceRight k p l m r
+  | otherwise               = rloser        k p l m r
+
+lbalanceLeft  k p l m r
+  | size' (left r) < size' (right r) = lsingleLeft  k p l m r
+  | otherwise                      = ldoubleLeft  k p l m r
+
+lbalanceRight k p l m r
+  | size' (left l) > size' (right l) = lsingleRight k p l m r
+  | otherwise                      = ldoubleRight k p l m r
+
+
+rbalanceLeft  k p l m r
+  | size' (left r) < size' (right r) = rsingleLeft  k p l m r
+  | otherwise                      = rdoubleLeft  k p l m r
+
+rbalanceRight k p l m r
+  | size' (left l) > size' (right l) = rsingleRight k p l m r
+  | otherwise                      = rdoubleRight k p l m r
+
+
+
+
+lsingleLeft k1 p1 t1 m1 (LLoser _ k2 p2 t2 m2 t3)
+  | p1 <= p2  = lloser k1 p1 (rloser k2 p2 t1 m1 t2) m2 t3
+  | otherwise = lloser k2 p2 (lloser k1 p1 t1 m1 t2) m2 t3
+
+lsingleLeft k1 p1 t1 m1 (RLoser _ k2 p2 t2 m2 t3) =  
+  rloser k2 p2 (lloser k1 p1 t1 m1 t2) m2 t3
+
+rsingleLeft k1 p1 t1 m1 (LLoser _ k2 p2 t2 m2 t3) =  
+  rloser k1 p1 (rloser k2 p2 t1 m1 t2) m2 t3
+
+rsingleLeft k1 p1 t1 m1 (RLoser _ k2 p2 t2 m2 t3) =  
+  rloser k2 p2 (rloser k1 p1 t1 m1 t2) m2 t3
+
+lsingleRight k1 p1 (LLoser _ k2 p2 t1 m1 t2) m2 t3 =  
+  lloser k2 p2 t1 m1 (lloser k1 p1 t2 m2 t3)
+
+lsingleRight k1 p1 (RLoser _ k2 p2 t1 m1 t2) m2 t3 =  
+  lloser k1 p1 t1 m1 (lloser k2 p2 t2 m2 t3)
+
+rsingleRight k1 p1 (LLoser _ k2 p2 t1 m1 t2) m2 t3 =  
+  lloser k2 p2 t1 m1 (rloser k1 p1 t2 m2 t3)
+
+rsingleRight k1 p1 (RLoser _ k2 p2 t1 m1 t2) m2 t3
+  | p1 <= p2  = rloser k1 p1 t1 m1 (lloser k2 p2 t2 m2 t3)
+  | otherwise = rloser k2 p2 t1 m1 (rloser k1 p1 t2 m2 t3)
+
+
+
+ldoubleLeft k1 p1 t1 m1 (LLoser _ k2 p2 t2 m2 t3) = 
+  lsingleLeft k1 p1 t1 m1 (lsingleRight k2 p2 t2 m2 t3)
+
+ldoubleLeft k1 p1 t1 m1 (RLoser _ k2 p2 t2 m2 t3) =  
+  lsingleLeft k1 p1 t1 m1 (rsingleRight k2 p2 t2 m2 t3)
+
+ldoubleRight k1 p1 (LLoser _ k2 p2 t1 m1 t2) m2 t3 =  
+  lsingleRight k1 p1 (lsingleLeft k2 p2 t1 m1 t2) m2 t3
+
+ldoubleRight k1 p1 (RLoser _ k2 p2 t1 m1 t2) m2 t3 =  
+  lsingleRight k1 p1 (rsingleLeft k2 p2 t1 m1 t2) m2 t3
+
+rdoubleLeft k1 p1 t1 m1 (LLoser _ k2 p2 t2 m2 t3) = 
+  rsingleLeft k1 p1 t1 m1 (lsingleRight k2 p2 t2 m2 t3)
+
+rdoubleLeft k1 p1 t1 m1 (RLoser _ k2 p2 t2 m2 t3) =  
+  rsingleLeft k1 p1 t1 m1 (rsingleRight k2 p2 t2 m2 t3)
+
+rdoubleRight k1 p1 (LLoser _ k2 p2 t1 m1 t2) m2 t3 =  
+  rsingleRight k1 p1 (lsingleLeft k2 p2 t1 m1 t2) m2 t3
+
+rdoubleRight k1 p1 (RLoser _ k2 p2 t1 m1 t2) m2 t3 =  
+  rsingleRight k1 p1 (rsingleLeft k2 p2 t1 m1 t2) m2 t3
+
+
+play :: (Ord k, Ord p) => PSQ k p -> PSQ k p -> PSQ k p
+
+Void `play` t' = t'
+t `play` Void  = t
+
+Winner k p t m  `play`  Winner k' p' t' m'
+  | p <= p'   = Winner k  p  (rbalance k' p' t m t') m'
+  | otherwise = Winner k' p' (lbalance k  p  t m t') m'
+
+unsafePlay :: (Ord k, Ord p) => PSQ k p -> PSQ k p -> PSQ k p
+
+Void `unsafePlay` t' =  t'
+t `unsafePlay` Void  =  t
+
+Winner k p t m  `unsafePlay`  Winner k' p' t' m'
+  | p <= p'   = Winner k  p  (rbalance k' p' t m t') m'
+  | otherwise = Winner k' p' (lbalance k  p  t m t') m'
+
+
+
+data TourView k p = Null | Single k p | PSQ k p `Play` PSQ k p
+
+tourView :: (Ord k) => PSQ k p -> TourView k p
+
+tourView Void                  =  Null
+tourView (Winner k p Start _m) =  Single k p
+
+tourView (Winner k p (RLoser _ k' p' tl m tr) m') =  
+  Winner k  p  tl m `Play` Winner k' p' tr m'
+
+tourView (Winner k p (LLoser _ k' p' tl m tr) m') =  
+  Winner k' p' tl m `Play` Winner k  p  tr m'
+
+
+
+
+
+
+--------------------------------------
+-- Hughes's efficient sequence type --
+--------------------------------------
+
+emptySequ  :: Sequ a
+singleSequ :: a -> Sequ a
+(<>)       :: Sequ a -> Sequ a -> Sequ a
+seqFromList   :: [a] -> Sequ a
+seqFromListT  :: ([a] -> [a]) -> Sequ a
+seqToList     :: Sequ a -> [a] 
+
+infixr 5 <>
+
+newtype Sequ a  =  Sequ ([a] -> [a])
+
+emptySequ          = Sequ (\as -> as)
+singleSequ a       = Sequ (\as -> a : as)
+Sequ x1 <> Sequ x2 = Sequ (\as -> x1 (x2 as))
+seqFromList as     = Sequ (\as' -> as ++ as')
+seqFromListT as    = Sequ as
+seqToList (Sequ x) = x []
+
+instance Show a => Show (Sequ a) where
+    showsPrec d a = showsPrec d (seqToList a)
+
+guard :: Bool -> Sequ a -> Sequ a
+guard False _as = emptySequ
+guard True  as  = as
+
+
+
+
+---------------------------------
+------------ Tests --------------
+---------------------------------
+
+{-
+
+isBalanced Start = True
+isBalanced (LLoser s k p l m r) =
+  (size' l + size' r <= 2 ||(size' l<=omega*size' r && size' r<=omega*size' l))
+  && isBalanced l && isBalanced r
+isBalanced (RLoser s k p l m r) =
+  (size' l + size' r <= 2 ||(size' l<=omega*size' r && size' r<=omega*size' l))
+  && isBalanced l && isBalanced r
+
+instance (Ord k, Ord p, Arbitrary k, Arbitrary p) => Arbitrary (PSQ k p)
+  where 
+    coarbitrary = undefined
+    arbitrary = 
+      do ks <- arbitrary
+         ps <- arbitrary
+         return . fromList $ zipWith (:->) ks ps
+
+prop_Balanced :: PSQ Int Int -> Bool
+prop_Balanced Void = True
+prop_Balanced (Winner _ _ t _) = isBalanced t
+
+prop_OrderedKeys :: PSQ Int Int -> Bool
+prop_OrderedKeys t = let ks = map key . toAscList $ t in sort ks == ks
+
+prop_AtMost :: (PSQ Int Int,Int) -> Bool
+prop_AtMost (t,p) = 
+  let ps = map prio . atMost p $ t 
+  in all (<=p) ps
+
+prop_AtMostRange :: (PSQ Int Int,Int,Int,Int) -> Bool
+prop_AtMostRange (t,p,l_,r_) = 
+  let l = min (abs l_) (abs r_)
+      r = max (abs l_) (abs r_)
+      (ks,ps) = unzip . map (\b -> (key b,prio b)) . atMostRange p (l,r) $ t 
+  in  all (flip inrange (l,r)) ks && all (<=p) ps
+
+prop_MinView :: PSQ Int Int -> Bool
+prop_MinView t = 
+  case minView t of 
+    Nothing -> True
+    Just (b1,t') ->
+      case minView t' of
+        Nothing -> True
+        Just (b2,_) -> prio b1 <= prio b2 && prop_MinView t'
+
+tests =
+  do
+  putStrLn "Balanced"
+  quickCheck prop_Balanced
+  putStrLn "OrderedKeys"
+  quickCheck prop_OrderedKeys
+  putStrLn "MinView"
+  quickCheck prop_MinView
+  putStrLn "AtMost"
+  quickCheck prop_AtMost
+  putStrLn "AtMostRange"
+  quickCheck prop_AtMostRange
+-}
+
+
+
+
+
+
hunk ./src/Data/Rules.hs 1
-
+{-# OPTIONS_GHC -fglasgow-exts #-}
+module Data.Rules (
+    
+    Rule, rule, 
+    isOpen,
+    Rateable(..), RatingData,   
+    
+    Rules, rules,
+    insert, delete, replace, union,
+    map , fold 
+    --rulesFromList, rulesFromSet,
+    --rulesToList, rulesToSet,
+    
+    
+    )where
+
+import Prelude hiding (map)
+import Data.Set (Set)
+import Data.Util 
+import qualified Data.Set as S (fromList, toList, fold, map, insert, delete, union)
+import Terms (Exp, Pat, size, Size)
+
+--------------------------------------------------------------------------------
+-- Datatype Rule
+--------------------------------------------------------------------------------
+
+--type LHS = Pat
+type LHS = Int
+--type RHS = Exp
+type RHS = String
+
+-- | Rule with hidden data constructor
+data Rule = HR {lhs :: LHS, rhs :: RHS} deriving( Eq, Ord)
+
+-- | Rule constructor
+rule :: LHS -> RHS -> Rule
+rule = HR
+
+-- | Rule accessors
+isOpen :: Rule -> Bool
+isOpen _ = True    
+
+type RatingData = Int
+
+class Rateable r where
+    rate :: r -> RatingData
+    
+instance Rateable Rule where
+    rate (HR ls rs) = size ls * size rs
+    
+instance Show Rule where
+    show (HR ls rs) = show ls ++ "=" ++ show rs
+    
+--------------------------------------------------------------------------------
+-- Datatype Rules
+--------------------------------------------------------------------------------    
+
+newtype Rules = HRs { unHRs :: Set Rule }
+    deriving(Eq, Ord)
+
+instance Show Rules where
+    show rs = showAsSet ((S.toList.rulesToSet) rs) $ ""
+    
+    
+rules = rulesFromList
+
+
+fold :: (Rule -> a -> a) -> a -> Rules -> a
+fold f i rs = S.fold f i (unHRs rs)
+
+map :: (Rule -> Rule) -> Rules -> Rules
+map f rs  = HRs $ (S.map f) (unHRs rs)
+
+
+union :: Rules -> Rules -> Rules
+union (HRs rs1) (HRs rs2) = HRs $ S.union rs1 rs2
+
+insert :: Rule -> Rules -> Rules
+insert r rs = HRs $ (S.insert r) $ unHRs rs
+
+delete :: Rule -> Rules -> Rules
+delete r rs = HRs $ (S.delete r) $ unHRs rs
+
+
+replace :: Rule ->  -- ^replace old rule 
+           Rule ->  -- ^by new rule
+           Rules -> -- ^in some rules
+           Rules
+replace r1 r2 = (insert r2).(delete r1) 
+
+
+rulesFromList :: [Rule] -> Rules
+rulesFromList rs  = HRs $ S.fromList rs
+
+rulesFromSet :: Set Rule -> Rules
+rulesFromSet rs = HRs rs
+
+rulesToList = S.toList.unHRs
+rulesToSet = unHRs
hunk ./src/Data/Test.hs 1
+
+module Data.Test where
+
+import Data.HypoSpace 
+import Data.Rules (rules, rule)
+import Data.Hypotheses (Hypo, hypo)
+
+
+--{- -----------------------------------------------------------------------------
+-- | test Data
+------------------------------------------------------------------------------- -}
+--
+
+rule1 = rule 1 "a"
+rule2 = rule 2 "b"
+rule3 = rule 3 "c"
+rule4 = rule 4 "d"
+rule5 = rule 5 "e"
+rule6 = rule 6 "f"
+rule7 = rule 7 "g"
+rule8 = rule 8 "h"
+rule9 = rule 9 "i"
+rule10 = rule 10 "j"
+
+rule1' = rule 1 "aaaaaaaaa"
+rule2' = rule 2 "bbbbbbbbbbbbbbbbbbbb"
+rule3' = rule 3 "ccc"
+rule4' = rule 4 "ddd"
+rule5' = rule 5 "eeeeeeeeeeeeeeee"
+rule6' = rule 6 "fff"
+rule7' = rule 7 "ggg"
+rule8' = rule 8 "hhh"
+rule9' = rule 9 "iii"
+rule10' = rule 10 "jjj"
+
+rules1o = rules [rule1,rule2,rule3]
+rules1c = rules [rule4,rule5]
+rules1ao = rules [rule6]
+rules1ac = rules [rule4,rule5]
+rules2o = rules [rule6,rule7,rule8]
+rules2c = rules [rule9,rule10]
+rules3o = rules [rule1,rule6,rule8]
+rules3c = rules [rule4,rule10]
+rules4o = rules [rule9,rule2,rule3]
+rules4c = rules [rule9,rule5]
+
+
+hypo1 = hypo rules1o rules1c
+hypo1a = hypo rules1ao rules1ac
+hypo2 = hypo rules2o rules2c
+hypo3 = hypo rules3o rules3c
+hypo4 = hypo rules4o rules4c
+
+hsp = initHSpace
+hsp1 = insert hypo1 hsp
+hsp2 = insert hypo2 hsp1
+
+hsp3 = insert hypo3 hsp2
+hsp4 = insert hypo4 hsp3
hunk ./src/Data/Util.hs 1
-
+
+module Data.Util where
+
+--showAsSet :: (Show a) => [a] -> String
+
+showAsSet l = showString 
+            $ showString "{"
+            $ if length l > 0 
+                 then shows (head l) $ foldr (\s -> showString ", " . shows s) " }" (tail l) 
+                 else "}"
hunk ./src/Data.hs 1
-
+
+module Data --(
+--
+--
+--
+--    toFunDef, FunDef,
+--    Equation, lhs, rhs,
+--     )
+where
+
+
+import Language.Haskell.TH
+import Terms.Class
+import Data.List (sortBy, intersperse, (\\))
+import Data.Ord (comparing)
+import Data.HypoSpace
+
+data FunDef   = FD {fun :: Name, eqs :: [Equation], eq :: Int -> Equation}
+
+instance Show FunDef where
+    show FD {fun = nm, eqs = es} = 
+        let s = "FD " ++ show nm ++ ":"
+            space = replicate (length s) ' '
+        in s ++ concat(intersperse ("\n" ++ space) (map show es))
+
+toFunDef :: Dec -> FunDef
+toFunDef (FunD nm  cls) = 
+    let es = sortBy (comparing size) $ map toEquation cls  
+    in FD { fun  = nm
+          , eqs  = es
+          , eq   = (\i -> es!!i)
+          }
+          
+fromFunDef :: FunDef -> Dec
+fromFunDef fd = FunD (fun fd) (map fromEquation (eqs fd))
+
+data Example  = EXM {fnm :: Name, equ :: Equation}
+    deriving (Show)
+    
+data Equation = EQU {lhs :: LHS, rhs :: RHS}
+instance Show Equation where
+    show EQU {lhs = ls, rhs = rs} = (concatMap pprint ls) ++ " = " ++ (pprint rs)
+
+instance Size Equation where
+    size_ done  equation        = sum $ done : (size (rhs equation)) : (map size (lhs equation))
+    
+toEquation :: Clause -> Equation
+toEquation (Clause ls (NormalB rs) _) = EQU {lhs = ls, rhs = rs}
+toEquation c = error $ "Cannot transform clause " ++ (show c) ++ " to an equation!"
+
+fromEquation :: Equation -> Clause
+fromEquation EQU {lhs = ls, rhs = rs} = (Clause ls (NormalB rs) []) 
+    
+freeVars    :: Equation -> [Exp]
+freeVars  e = 
+    let lhsvars = getVarNames.rhs $ e
+        rhsvars = concatMap getVarNames $ lhs e
+        diff    = (\\) rhsvars lhsvars
+    in map (\n -> (VarE n)) diff
+
+hasFreeVars :: Equation -> Bool
+hasFreeVars = not.null.freeVars
+
+type LHS = [Pat]
+type RHS = Exp
hunk ./src/IgorMonad.hs 1
-
+
+module IgorMonad where
+
+
+import Logging
+import Control.Monad.Identity
+import Control.Monad.State
+import Data.IgorData
+
+type IM a = ELT (State Igor) a 
+
+runIM = runState.runELT
hunk ./src/Logging/Logger.hs 1
+{-# OPTIONS_GHC -fglasgow-exts -fth  -XTypeSynonymInstances #-}
+module Logging.Logger 
+(
+    
+    runELT, -- runLT,
+    Log, Logger, Message, Priority,
+    ELog(..),
+    ELT,
+    
+    pnd, skip,
+    
+    module Control.Monad , 
+    module Control.Monad.Writer , 
+    module Control.Monad.State,
+    module Control.Monad.Error, 
+    module Control.Monad.Trans,
+    module Language.Haskell.TH
+    ) 
+    where
+
+import Logging.PrettyPrinter
+import Data.Monoid (Monoid(..))
+import Data.List (isPrefixOf, intersperse)
+import Language.Haskell.TH (Ppr(..), pprint)
+import Control.Monad (liftM, liftM2, liftM3)
+import Control.Monad.Writer (MonadWriter(..), WriterT, Writer(..), runWriter, runWriterT)
+import Control.Monad.State (MonadState, StateT, evalStateT, gets, modify)
+import Control.Monad.Reader (MonadReader(..), ReaderT(..), runReader, runReaderT, asks)
+import Control.Monad.Error (ErrorT(..), MonadError(..), when)
+import Control.Monad.Trans (MonadTrans (..))
+import Control.Monad.Identity (runIdentity, Identity (..))
+import Data.Maybe (maybeToList)
+
+data Priority = DEBUG       -- ^Debug messages
+              | INFO        -- ^Information
+              | NOTICE      -- ^Normal runtime conditions
+              | WARNING     -- ^General Warnings
+              | ERROR       -- ^General Errors
+              | CRITICAL    -- ^Severe situations
+              | ALERT       -- ^Take immediate action
+              | EMERGENCY   -- ^System is unusable
+    deriving (Ord, Show, Eq)
+
+type Error = String
+
+--instance Pretty Error where
+--    view s = "ERROR: " ++ (show s)
+    
+type Logger   = String
+type Message  = [String]
+type LogEntry = (Priority,Logger,Message)
+
+mergeEntries :: LogEntry -> LogEntry -> [LogEntry]
+mergeEntries (p1,l1,m1) (p2,l2,m2)
+    | p1 == p2 && l1 == l2 = [(p1,l1,(m1++m2))]
+    | otherwise            = [(p1,l1,m1),(p2,l2,m2)]
+    
+type LogState = (Priority,Logger,Logger)
+
+showLogEntry :: LogEntry -> String
+showLogEntry (p,l,m) = shows p 
+                     . showString (replicate (9 - length (show p)) ' ') 
+                     . showString " -> " 
+                     . showString l 
+                     . showString ":\n\n\t" 
+                     . showString (concat (intersperse "\n\t" m)) 
+                     $ "\n\n"
+
+    
+data Log = Log  {logs :: [LogEntry], lst :: Maybe LogEntry}
+
+instance Show Log where
+    show l = showString "\n" 
+           . showString (concatMap showLogEntry (logs l)) 
+           . showString (concatMap showLogEntry (maybeToList(lst l)))
+           $ "\n"
+    
+instance Pretty Log where
+    pretty l = map showLogEntry (logs l) ++
+               map showLogEntry (maybeToList(lst l))
+
+instance Monoid Log where
+    mempty  = Log [] Nothing
+    mappend (Log _ Nothing) l2  = l2
+    mappend l1 (Log _ Nothing)  = l1
+    mappend (Log logs1 (Just l)) (Log logs2 (Just l2)) =
+        let (x:xs)  = logs2 ++ [l2]
+            mes     = mergeEntries l x
+            logs    = mes ++ xs
+            newlst  = last logs
+            newlogs = logs1 ++ (init logs)
+        in Log newlogs (Just newlst)
+
+class ( MonadError Error m
+      , MonadState LogState m
+      , MonadWriter Log m) => ELog m where   
+           
+    logDE,logIN,logNO,logWA,logER,logCR,logAL,logEM   :: 
+        (MonadWriter Log m, MonadState LogState m) =>
+               Message -> m ()           
+    logDE = logging DEBUG
+    logIN = logging INFO
+    logNO = logging NOTICE
+    logWA = logging WARNING
+    logER = logging ERROR
+    logCR = logging CRITICAL
+    logAL = logging ALERT
+    logEM = logging EMERGENCY
+    
+    llogDE,llogIN,llogNO,llogWA,llogER,llogCR,llogAL,llogEM   :: 
+         (MonadState LogState m, MonadWriter Log m, MonadTrans t) =>
+               Message -> t m ()        
+    llogDE = \m -> lift (logDE m)
+    llogIN = \m -> lift (logIN m)
+    llogNO = \m -> lift (logNO m)
+    llogWA = \m -> lift (logWA m)
+    llogER = \m -> lift (logER m)
+    llogCR = \m -> lift (logCR m)
+    llogAL = \m -> lift (logAL m)
+    llogEM = \m -> lift (logEM m) 
+        
+    llogEnterDE, llogEnterIN :: ( MonadWriter Log m, MonadState LogState m
+                                , MonadTrans t) => t m ()           
+    llogEnterDE = lift logEnterDE
+    llogEnterIN = lift logEnterIN
+    
+    logEnterDE, logEnterIN :: (MonadWriter Log m, MonadState LogState m) => m ()           
+    logEnterDE = logDE [" - - - - - - Function entered - - - - - - "]
+    logEnterIN = logIN [" - - - - - - Function entered - - - - - - "]
+     
+    logEntered :: (MonadWriter Log m, MonadState LogState m) => Priority -> m ()           
+    logEntered p = logging p [" - - - - - - Function entered - - - - - - "]
+    
+    llogEntered :: (MonadWriter Log m, MonadState LogState m, MonadTrans t) 
+                    => Priority -> t m ()           
+    llogEntered p = lift $ logEntered p
+    
+    getPriority ::  (MonadState LogState m, MonadWriter Log m) => m Priority
+    getPriority = gets (\(p,_,_) -> p)
+
+    setPriority ::  (MonadState LogState m, MonadWriter Log m) =>Priority -> m ()
+    setPriority p = modify (\(_,gll,cl) -> (p,gll,cl))
+    
+    getGlobalLogLevel ::  (MonadState LogState m, MonadWriter Log m) =>m Logger
+    getGlobalLogLevel = gets (\(_,gll,_) -> gll)
+    
+    setGlobalLogLevel ::  (MonadState LogState m, MonadWriter Log m) =>Logger -> m ()
+    setGlobalLogLevel gll = modify (\(p,_,cl) -> (p,gll,cl))
+    
+    getCurrentLogger ::  (MonadState LogState m, MonadWriter Log m) =>m Logger
+    getCurrentLogger = gets (\(_,_,cl) -> cl)
+    
+    setCurrentLogger ::  (MonadState LogState m, MonadWriter Log m) =>Logger -> m ()
+    setCurrentLogger cl = modify (\(p,gll,_) -> (p,gll,cl))
+    
+    logging :: (ELog m) => Priority -> Message -> m ()
+    logging p msg   = getCurrentLogger >>= \l ->
+                      handle (p,l,msg)
+
+--instance (Monad m) => ELog (EL m) 
+--     
+--type EL m = (ErrorT String (StateT (Priority,Logger) (WriterT Log m )))
+--      
+--runEL :: (Monad m, Monoid w) =>
+--    ErrorT e (StateT (Priority, [Char]) (WriterT w m)) a  -> m (Either e a, w)
+--runEL = \m -> runWriterT (evalStateT (runErrorT m) (DEBUG,""))
+     
+type EL = (ErrorT Error (StateT LogState (WriterT Log Identity)))
+
+--runEL :: EL a -> (Either Error a, Log)
+--runEL = \m -> runIdentity (runWriterT (evalStateT (runErrorT m) (DEBUG,"","")))
+--instance ELog EL
+ 
+type ELT m = (ErrorT Error (StateT LogState (WriterT Log m)))
+instance (Monad m) => ELog (ELT m)     
+runELT :: (Monad m) => (ELT m a) -> m (Either Error a, Log)
+runELT =  \m -> (runWriterT (evalStateT (runErrorT m) (DEBUG,"","")))             
+
+
+
+handle :: (ELog m) =>  LogEntry -> m ()
+handle (p,l,msg) =
+    do lvl <- getPriority
+       gll <- getGlobalLogLevel
+       when ((isPrefixOf gll l) && (lvl <= p)) $ tell (Log [] (Just (p,l,msg)))
+                 
+
+pnd :: [String] -> [String]
+pnd as = "Pattern not defined !!!":
+         [ "arg" ++ show (i+1) ++ " " ++ (as !! i) | i <- [0 .. (length as)-1]]
+
+skip :: String -> String
+skip = ("  " ++)
+
+
hunk ./src/Logging/PrettyPrinter.hs 1
+{-# OPTIONS_GHC -fglasgow-exts -fth  -XTypeSynonymInstances #-}
+module Logging.PrettyPrinter (
+    Pretty(..),
+    viewlist
+    ) where
+
+
+import Language.Haskell.TH --(Exp, Pat, Ppr(..), pprint)
+import Data.List (intersperse)
+class (Show p) => Pretty p where
+
+    view :: p -> String
+    view = concat.pretty
+    
+    pretty :: p -> [String]
+
+instance Pretty Exp where
+    pretty = (:[]).pprint
+    
+instance Pretty Pat where
+    pretty = (:[]).pprint
+      
+instance Pretty Dec where
+    pretty = (:[]).pprint
+    
+instance Pretty Char where
+    pretty = (:[]).show
+    
+instance Pretty String where
+    pretty = (:[]).show
+    
+--instance (Pretty p) => Pretty [p] where
+--    pretty u =  ["[" ++ ((concat.(intersperse ",")) (map view u)) ++ "]"]
+
+viewlist :: (Pretty e) => [e] -> String
+viewlist = concatMap view
hunk ./src/Logging.hs 1
-
+
+module Logging (
+    
+       module Logging.Logger,
+       module Logging.PrettyPrinter
+       
+    )where
+
+import Logging.Logger
+import Logging.PrettyPrinter
hunk ./src/Terms/Antiunifier.hs 1
-
+{-# OPTIONS_GHC -fglasgow-exts -fth  -XTypeSynonymInstances #-}
+{-| 
+  The module "Antiunifier" defines antiunification for terms in a general way.  
+-}
+module Terms.Antiunifier
+    ( 
+    -- * The class Antiunifieable
+      Antiunifieable (
+        antiunify      -- :: (Antiunifieable k v t) => [t] -> t
+      )
+      
+    
+    ) where
+
+import Language.Haskell.TH
+import qualified Data.Map as M
+import Logging
+import Control.Monad.State
+import Data.List
+import Terms.Class
+
+
+    
+
+{- | 
+     A map from keys 'k' to values 'v' which is used in the 'AU' monad. In fact,
+     it is a many-to-one mapping to model generalisation from many terms to a 
+     variable. So, a list of keys is always mapped to the same value.
+-}
+type VarMap k v = (M.Map [k] v)
+
+{- | 
+     The 'AU' monad which is rewuired for antiunification. It is just a state 
+     monad 'StateT' to keep track of the replacements in a 'VarMap'. The type 
+     parameters are:
+        * the type of the keys 'k' in 'VarMap'
+        * the type of the variables 'v' in 'VarMap'
+        * the type of term 't' to antiunify
+     The value is wrapped into the 'Identity' monad to be felxible enought to
+     allow for extensions for probable logging, error handling, etc. later
+-}
+type AU m k v t = StateT (VarMap k v) m t
+
+-- Shotcut to evaluate the 'AU' monad, yielding the result value
+evalAU :: (ELog m) => StateT s m a -> s -> m a
+evalAU = evalStateT
+
+-- Shotcut to evaluate the 'AU' monad, yielding the result value and the result 
+-- state
+runAU :: (ELog m) => StateT s m a -> s -> m (a, s)
+runAU  = runStateT
+
+--------------------------------------------------------------------------------
+-- The Antiunifieable class definition  
+--------------------------------------------------------------------------------
+{-|
+    The class 'Antiunifieable' defines the antiunifcation in a quite general 
+    way. It generalises a list of types 't' into a single term of the same type,
+    probably intorducing variables. Different subterms are hereby always 
+    replaced with the same variable if antiunified twice. This mapping is called
+    the /image of a variable/.For example:
+    
+    >   tail (1:xs)   = xs
+    >   tail (1:2:xs) = (2:xs)
+    
+    would yield
+    
+    >   tail (1:x1) = x1
+    
+    with image [[xs, 2:xs] ~> x1], whereas the anti-instance of
+    
+    >   last (1:[]) = 1
+    >   last (1:xs) = last xs
+    
+    is
+    
+    >   last (1:x1) = x2
+    
+    with image [ [[], xs] ~> x1, [1,last xs] ~> x2 ].
+    
+    The parameters 'k' and 'v' specify 
+    
+        * the types of the keys 'k' 
+        
+        * and variables 'v' 
+        
+    used in the internal representation to keep track which terms were
+    antiunified into which variable. This might be counter-intuitive, but allows
+    the variable images be of different type as the terms to antiunify. This is 
+    especially necessary when the variable image of one antiunifcation is needed
+    in another, but the terms are of different types. Consider for example the
+    terms of the previous @tail@. The terms @xs@ and @2:xs@ on the left-hand 
+    side as well as on the right-hand side should be replaced with the same 
+    variable. If the terms are of type 'Language.Haskell.TH.Clause' the left-hand
+    side is of type 'Language.Haskell.TH.Pat' whereas the right-hand side is of 
+    type 'Language.Haskell.TH.Exp' 
+    (see <http://www.haskell.org/ghc/docs/latest/html/libraries/template-haskell/Language-Haskell-TH.html> for 
+    details of the Template Haskell syntax.    
+-}      
+class (Show v, Show k, Show t) => Antiunifieable k v t |t -> k v where
+    -- | Computes the anti-instance 't' of all terms in '[t]'
+    antiunify        :: (ELog m) => [t] -> m t
+    antiunify         = (\t -> evalAU (aunify t) M.empty)
+   
+    -- | Same as 'antiunify' but uses a 'VarMp' as initial state
+    antiunifyWithMap ::  (Antiunifieable k v t, ELog m) => (VarMap k v) -> [t] -> m t
+    antiunifyWithMap  = (\m t -> evalAU (aunify t) m)
+    
+    -- | Translator function to transform a term 't' into its representation as
+    --   a key of type 'k'
+    toKey            :: t -> k    
+    
+    -- | Translator function to transform a variable 'v' into its representation
+    --   as term of type 't'
+    fromVal          :: v -> t
+    
+    -- | Given a term 't' and an Integer, returns a variable of type 'v'
+    --   The first argument is moe or less to dissolve the functional 
+    --   dependencies.
+    mkVar            :: t -> Integer -> v   
+    
+    -- | The actual state transforming function, doing the anti-unification and 
+    --   keeping track of the variables in the state.
+    aunify           :: (Antiunifieable k v t, ELog m) => [t] -> AU m k v t
+
+
+--------------------------------------------------------------------------------
+-- The Antiunifieable instance declarations
+--------------------------------------------------------------------------------
+{- |
+  This is more or less for convenience and aunify simply calls 'antiunify' with 
+  the clauses list as argument. All other functions are undefined and yield in 
+  a 'fail'. 
+  
+  TODO: good coding style??? 
+
+-}    
+instance Antiunifieable Exp Exp Dec where    
+    toKey                      = 
+        fail $ "Antiunifier.aunify: Cannot generalise over arbitrary " ++
+                   "function definitions!"
+    fromVal  = 
+        fail $ "Antiunifier.aunify: Cannot generalise over arbitrary " ++
+               "function definitions!"
+    mkVar                      = 
+        fail $ "Antiunifier.aunify: Cannot generalise over arbitrary " ++
+               "function definitions!"
+    aunify [FunD name clauses] = 
+        do ai_clauses <- lift $ antiunify clauses
+           return $ FunD name [ai_clauses]
+    aunify [] = 
+        fail $ "Antiunifier.aunify: empty list of Dec, no terms to antiunify"
+    aunify (_:_)               =
+        fail $ "Antiunifier.aunify: Cannot generalise over arbitrary " ++
+                "function definitions!"
+
+{-
+   The result state of anitunifying the patterns is passed to the 
+   antiunification of the expression on the right-hand side. This is necessary 
+   because the same terms may occur both on the lhs and on the rhs, here as 
+   patterns 'Pat' there as expressions 'Exp'.
+   
+   Same as with 'Antiunifieable Exp Exp Dec', all other functions yield a 
+   'fail'.   
+    
+-}        
+instance Antiunifieable Exp Exp Clause where 
+    toKey = 
+        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
+                "number of patterns in Clause!"
+    fromVal = 
+        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
+                "number of patterns in Clause!"
+    mkVar = 
+        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
+                "number of patterns in Clause!"
+                
+    {- If all elements in the provided list are 'Clauses's the result is just 
+       a tuple with their patterns 'pat' i.e. a list of patern lists, their 
+       'bodies' and their declarations 'dec', 'Nothing' otherwise.
+       To antiunify the patterns we transpose the pattern list, to antiunify
+       all nth pattern of the clauses. 
+       We don't care about the 'dec' so we just put them all together. 
+       After antiunifying all patterns we pss the result state to the 
+       antiunification of the expressions.
+    -}
+    aunify l@((Clause _ _ _):xs)  =
+        case collectSubtermsC  l of
+            Just (pats,bodies,decs) -> 
+                do let tpats   = transpose pats
+                   let alldecs = concat decs
+                   (ai_pats,varmap) <- lift $ runAU ((mapM aunify) tpats) M.empty
+                   ai_bodies <- lift $ antiunifyWithMap varmap bodies
+                   return $ Clause ai_pats ai_bodies alldecs
+            Nothing   ->  
+                fail "Antiunifier.aunify: Cannot generalise over arbitrary clauses!"
+                
+{-|
+  Same as in the previous instance declarations. Here the state of antiunifying 
+  'Body's is simply passed to antiunifying 'Exp's.
+-}                
+instance Antiunifieable Exp Exp Body where  
+    toKey (NormalB e)         = e
+    fromVal e                 = (NormalB e)
+    mkVar                     = (\_d i -> VarE $ mkName $ "x" ++ (show i))
+    
+    {-|
+       Same as above. Collect subterms, and antiunify them with the current 
+       state.
+    -}
+    aunify l@((NormalB _):xs) =
+        case collectSubtermsB l of
+            Just subterms -> 
+                do varmap <- get 
+                   ai_exps <- lift $ antiunifyWithMap varmap  subterms
+                   return $ NormalB ai_exps
+            Nothing       -> 
+                computeAntiInstance l
+    aunify [] = fail "Antiunifier.aunify: empty list, no terms to antiunify"
+    aunify (x:_) = 
+        fail $ "Antiunifier.aunify: Antiunification for " ++ show x ++
+                "of Type Body is not implemented!"
+    
+instance Antiunifieable Exp Exp Pat where
+
+    toKey (LitP lit)              = LitE lit
+    toKey (VarP name)             = VarE name
+    toKey (TupP pats)             = TupE $ map toKey pats
+    toKey (ConP name pats)        = let keys = map toKey pats
+                                    in foldr AppE (ConE name) keys
+    toKey (InfixP p1 name p2)     = let e1 = toKey p1
+                                        e2 = toKey p2
+                                    in InfixE (Just e1)(ConE name)(Just e2)
+    toKey (ListP pats)            = ListE $ map toKey pats
+    
+    fromVal = \(VarE n) -> VarP n
+    mkVar = (\_d i -> VarE $ mkName $ "x" ++ (show i))
+
+    -- antiunifying (TupP [Pat])
+    aunify l@((TupP _):xs) = 
+        case collectSubtermsP l of
+            Just subterms -> do                
+                ai_subterms <- mapM aunify subterms
+                return $ TupP ai_subterms
+            Nothing       -> 
+                computeAntiInstance l
+    
+    -- antiunifying (ConP Name [Pat])
+    aunify l@((ConP nm _ ):xs) = 
+        case collectSubtermsP l of
+            Just subterms -> do           
+                ai_subterms <- mapM aunify subterms
+                return $ ConP nm ai_subterms
+            Nothing       -> 
+                computeAntiInstance l
+                
+    -- antiunifying (InfixP Pat Name Pat)
+    aunify l@((InfixP _ nm _):xs) =
+        case collectSubtermsP l of
+            Just subterms -> do 
+                fstai <- aunify (subterms !! 0)
+                sndai <- aunify (subterms !! 1)
+                return $ InfixP fstai nm sndai
+            Nothing       -> 
+                  computeAntiInstance l 
+    
+    -- antiunifying (ListP [Pat])
+    -- Here some hack is necessary, because of Haskell's inconsistent way of
+    -- representing lists. If the pattern lists have different lengths, we
+    -- antiunify argument-wise starting with the first arguments until some 
+    -- pattern has no nth argument. If so, the whole rest is antiunified
+    -- and the ouput is constructed as a (:)-List with a variable as tail.
+    -- (see also @aunify (ListE _)@ )
+    aunify l@((ListP _):xs) = 
+        case collectSubtermsP l of
+            Just subterms  -> do
+                let len = length l
+                    straight = takeWhile (\l -> length l == len) subterms 
+                    ragged   = dropWhile (\l -> length l == len) subterms 
+                straightai <- mapM aunify straight
+                if null ragged 
+                  then return $ ListP straightai 
+                  else do raggedai <- computeAntiInstance $ map ListP ragged
+                          return $ (foldr1 (\p1 p2 -> ConP '(:) [p1,p2]) (straightai ++ [raggedai]))                                     
+            Nothing     ->
+                computeAntiInstance l 
+    
+    -- antiunifying (VarP Name)              
+    aunify l@((VarP _):xs) =  
+        checkforAntiInstance l     
+    -- antiunifying (LitP Lit)
+    aunify l@((LitP _):xs) =
+        checkforAntiInstance l
+    aunify [] = 
+        fail $ "Antiunifier.aunify: empty list, no terms to antiunify"
+    
+    -- NOT IMPLEMENTED !!!
+    --    TildeP Pat  
+    --    AsP Name Pat    
+    --    WildP   
+    --    RecP Name [FieldPat] 
+    --    SigP Pat Type 
+    aunify (x:_) = 
+        fail $ "Antiunifier.aunify: Antiunification for " ++ show x ++
+                "of Type Pat is not implemented!"
+                
+instance Antiunifieable Exp Exp Exp where
+    fromVal = id
+    toKey = id
+    mkVar = (\_d i -> VarE $ mkName $ "x" ++ (show i))
+    -- antiunifying (AppE Exp Exp)
+    aunify l@((AppE _ _):xs) =
+        case collectSubtermsE l of
+            Just subterms -> do
+                args1ai <- aunify (subterms !! 0)
+                args2ai <- aunify (subterms !! 1)
+                table <- get
+                if args1ai `elem` (M.elems table) -- no AppE (VarE _) _
+                  then return args1ai
+                  else return $ AppE args1ai args2ai
+            Nothing             ->
+                computeAntiInstance l
+                
+    -- antiunifying (ListE [Exp])
+    aunify l@((ListE _):xs) =
+        lift (setCurrentLogger "Terms.Antiunifier.aunify") >>
+        llogEnterDE >>
+        llogDE ["Input arguments are :", viewlist l] >>
+        case collectSubtermsE l of            
+            Just subterms  -> do
+                llogDE ["Subterms are :", concatMap viewlist subterms] 
+                let len = length l
+                    -- This is necessary for lists as eg. [[1,3],[1,2,3]] 
+                    -- after collecting subterms we get [[1,1],[3,2],[3]] which 
+                    -- must yield  (1:x:xs)
+                    -- So compute anti-instance up to minimum list length and 
+                    -- then add the anti-instance of thge rest lists
+                    straight = takeWhile (\l -> length l == len) subterms 
+                    ragged   = dropWhile (\l -> length l == len) subterms 
+                straightai <- mapM aunify straight
+                llogDE ["Antinunified subterms (straight) are :", viewlist straightai] 
+                if null ragged -- check if we have ragged liss at all
+                  then return $ ListE straightai -- we can keep the f*** ListE
+                          -- convert back to lists, to get correct variable image
+                  else do raggedai <- computeAntiInstance $ map ListE ragged
+                          llogDE ["List have different length"]
+                          llogDE ["Antinunified subterms (ragged) are :", viewlist straightai]
+                          -- here we need the the prefix style
+                          let apps = map (AppE (ConE '(:))) straightai
+                          return $ (foldr1 AppE (apps ++ [raggedai]))                                     
+            Nothing     ->
+                computeAntiInstance l 
+                
+    -- antiunifying (TupE [Exp])        
+    aunify l@((TupE _):xs) =  
+        case collectSubtermsE l of
+            Just subterms -> do                
+                ai_subterms <- mapM aunify subterms
+                return $ TupE ai_subterms
+            Nothing       -> 
+                computeAntiInstance l         
+
+    -- antiunifying (InfixE (Maybe Exp) Exp (Maybe Exp))
+    aunify l@((InfixE _ _ _):xs) =
+        case collectSubtermsE l of
+            Just subterms -> do 
+                fstai <- aunify (subterms !! 0)
+                sndai <- aunify (subterms !! 1)
+                thrai <- aunify (subterms !! 2)
+                -- here we have to check if we there is a DummyExp in there
+                -- If so, all expressions we antiunified were sections, so put
+                -- Nothing back at place
+                let fstai' = if fstai == dexp then Nothing else Just fstai
+                let thrai' = if thrai == dexp then Nothing else Just thrai
+                return $ InfixE fstai' sndai thrai'
+            Nothing       -> 
+                  computeAntiInstance l           
+
+   -- antiunifying (CondE Exp Exp Exp)
+    aunify l@((CondE _ _ _):xs) =
+        case collectSubtermsE l of
+            Just subterms -> do 
+                fstai <- aunify (subterms !! 0)
+                sndai <- aunify (subterms !! 1)
+                thrai <- aunify (subterms !! 2)
+                return $ CondE fstai sndai thrai
+            Nothing       -> 
+                  computeAntiInstance l       
+    
+    -- antiunifying (VarE Name)              
+    aunify l@((VarE _):xs) =  
+        checkforAntiInstance l         
+    -- antiunifying (ConE Name)
+    aunify l@((ConE _):xs) =
+        checkforAntiInstance l     
+    -- antiunifying (LitE Lit)
+    aunify l@((LitE _):xs) =
+        checkforAntiInstance l
+    aunify [] = 
+        fail $ "Antiunifier.aunify: empty list, no terms to antiunify"
+        
+    -- NOT IMPLEMENTED !!!
+    --LamE [Pat] Exp  
+    --LetE [Dec] Exp  
+    --CaseE Exp [Match]   
+    --DoE [Stmt]  
+    --CompE [Stmt]    
+    --ArithSeqE Range 
+    --SigE Exp Type   
+    --RecConE Name [FieldExp] 
+    --RecUpdE Exp [FieldExp]
+    aunify (x:_) = 
+        fail $ "Antiunifier.aunify: Antiunification for " ++ show x ++
+                "of Type Exp is not implemented!"
+
+    
+
+
+{-------------------------------------------------------------------------------
+  Auxiliary Functions for antiunifying expressions of type Exp
+-------------------------------------------------------------------------------}
+
+{-|
+   A dummy data type to model antiunification of InfixE (see below). This is not 
+   very nice, but I have no clue how to do it in a more elegant way.
+-}
+data DummyExp = DummyExp  
+dexp = ConE 'DummyExp
+
+{-|
+   Determine the collector function by means of the first element. The 
+   collector, which is fixed to a certain data constructor and collects the 
+   subterms or returns 'Nothing' if one element does not match with the fixed 
+   data constructor.
+-}
+collectSubtermsE :: [Exp] -> Maybe [[Exp]]
+collectSubtermsE l = liftM transpose $ sequence $ map collector l 
+    where
+    collector = case head l of 
+        (TupE _)         -> collectSubtermsTupE
+        (AppE _ _)       -> collectSubtermsAppE
+        (ListE _)        -> collectSubtermsListE
+        (InfixE _ _ _)   -> collectSubtermsInfixE
+        (CondE _ _ _)    -> collectSubtermsCondE
+        
+    collectSubtermsTupE :: Exp -> Maybe [Exp]        
+    collectSubtermsTupE (TupE vals)         = Just vals 
+    collectSubTermsTupE _                   = Nothing
+    
+    collectSubtermsAppE :: Exp -> Maybe [Exp]
+    collectSubtermsAppE (AppE e1 e2)        = Just [e1,e2]
+    collectSubtermsAppE _                   = Nothing
+    
+    collectSubtermsListE :: Exp -> Maybe [Exp]
+    collectSubtermsListE (ListE l)          = Just l
+    collectSubtermsListE _                  = Nothing
+    
+    collectSubtermsCondE :: Exp -> Maybe [Exp]
+    collectSubtermsCondE (CondE e1 e2 e3)   = Just [e1, e2, e3]
+    collectSubtermsCondE _                  = Nothing
+    
+    -- If the expression is a section e.g. (+1) we have to substitute the value
+    -- 'Nothing' with the dummy expression 'dex', which has to be replaced later.
+    collectSubtermsInfixE :: Exp -> Maybe [Exp]
+    collectSubtermsInfixE (InfixE (Just e1) e2 (Just e3)) = Just [e1, e2, e3]
+    collectSubtermsInfixE (InfixE Nothing e2 (Just e3))   = Just [dexp, e2, e3]
+    collectSubtermsInfixE (InfixE (Just e1) e2 Nothing)   = Just [e1, e2, dexp]
+    collectSubtermsInfixE (InfixE Nothing e2 Nothing)     = Just [dexp, e2, dexp]
+    collectSubtermsInfixE _                               = Nothing
+
+
+{-------------------------------------------------------------------------------
+  Auxiliary Functions for antiunifying expressions of type Pat 
+-------------------------------------------------------------------------------}
+
+{-|
+  See 'collectSubtermsE'
+-}
+collectSubtermsP :: [Pat] -> Maybe [[Pat]]
+collectSubtermsP l = liftM transpose $ sequence $ map collector l 
+    where
+    collector = case head l of 
+        (ConP nm _)     -> collectSubtermsConP nm
+        (InfixP _ nm _) -> collectSubtermsInfixP nm
+        (ListP _ )      -> collectSubtermsListP
+        (TupP _ )       -> collectSubtermsTupP
+        _owise          -> fail $ "No match for " ++ ( show l)
+
+    collectSubtermsConP nm (ConP nm' pats) 
+        | nm == nm'          = Just pats  --  always [p1,p2]
+        | otherwise          = Nothing
+    collectSubtermsConP _ _  = Nothing
+    
+    collectSubtermsInfixP nm (InfixP p1 nm' p2) 
+        | nm == nm'              = Just [p1,p2]
+        | otherwise              = Nothing
+    collectSubtermsInfixP _ _    = Nothing    
+
+    collectSubtermsListP (ListP l)          = Just l
+    collectSubtermsListP _                  = Nothing    
+     
+    collectSubtermsTupP (TupP pats)         = Just pats -- [fst,snd]
+    collectSubTermsTupP _                   = Nothing    
+ 
+    
+{-------------------------------------------------------------------------------
+  Auxiliary Functions for antiunifying expressions of type Body 
+-------------------------------------------------------------------------------}  
+
+{-|
+  See 'collectSubtermsE'
+-}
+collectSubtermsB l = sequence $ map collector l 
+    where
+    collector = case head l of 
+        (NormalB _)      -> collectSubtermsNormalB
+    collectSubtermsNormalB (NormalB expr)      = Just expr
+    collectSubtermsNormalB _                   = Nothing
+
+{-------------------------------------------------------------------------------
+  Auxiliary Functions for antiunifying expressions of type Clause 
+-------------------------------------------------------------------------------}  
+
+{-|
+  See 'collectSubtermsE'
+-}
+collectSubtermsC l = liftM unzip3 $ sequence $ map collector $ l 
+    where
+    collector = case head l of 
+        (Clause pats _ _ ) -> collectSubtermsClause (length pats)
+    collectSubtermsClause l (Clause ps b ds) = 
+        if (length ps) == l
+           then Just (ps,b,ds)
+           else  Nothing
+
+{-------------------------------------------------------------------------------
+  General Auxiliary Functions for Antiunification 
+-------------------------------------------------------------------------------} 
+
+{-|
+  Checks if in the provided list all terms are equal. If so, the first element 
+  is returned, otherwise a variable.
+-}            
+checkforAntiInstance :: (Ord k, Eq t, Antiunifieable k v t, ELog m) => [t] -> AU m k v t
+checkforAntiInstance l@(x:xs) =    
+    if and $ map (== x) xs
+       then return x
+       else computeAntiInstance l
+
+{-|
+   Computes the anti-instance for a list of expressions. It is assumed that the 
+   expressions do not anti-unify, so the result is simply a variable. This is 
+   either a fresh variable if the image of the provided terms does not yet 
+   exists in the the Monad 'AU' or it just returns the previously generated 
+   variable.
+-}       
+computeAntiInstance :: (Ord k, Antiunifieable k v t, ELog m) => [t] -> AU m k v t
+computeAntiInstance l@(x:xs) =  do 
+    lift (setCurrentLogger "Terms.Antiunifier.computeAntiInstance")
+    llogEnterDE
+    llogDE ["Term Image is:", show l]
+    table <- get
+    llogDE ["Current varTable is:", show table]
+    (newTable, var) <- return $ updateVarTable table l
+    llogDE ["update varTable with var:", show var]
+    llogDE ["Updated varTable is:", show newTable]
+    put newTable
+    return var
+
+{-|
+  If the provided list of terms does not yet exists in the variable table of the
+  'AU' Monad a fresh variable is generated and the variable table is updated.  
+  Otherwise, the previously generated variable is returned.
+-}              
+updateVarTable :: (Ord k, Antiunifieable k v t) => 
+                    (VarMap k v) -> [t] -> ((VarMap k v) , t)
+updateVarTable table img = 
+    let img' = map toKey img
+    in case M.lookup img' table of
+        (Just v)    -> (table, fromVal v)
+        Nothing     -> let newval = mkVar (head img) $ toInteger(M.size table)
+                       in (M.insert img' newval table , fromVal newval)
+
+ 
hunk ./src/Terms/Class.hs 1
-
+{-# OPTIONS_GHC -fglasgow-exts -fth  -XTypeSynonymInstances #-}
+module Terms.Class (
+    -- * Class Definition
+    Term(..), 
+    -- * Data Types
+    Position(Root, P),
+    -- * Constructors
+    (°),
+    
+    Size(..),
+    
+    -- Auxiliary functions
+    unfoldAppE, foldAppE,
+    
+    )where
+
+import Language.Haskell.TH ( Dec (FunD)
+                           , Clause (Clause)
+                           , Body (NormalB)
+                           , Exp (VarE, ConE, LitE, ListE, TupE, InfixE, AppE, CondE)
+                           , Pat (VarP, ConP, LitP, ListP, TupP, InfixP) 
+                           , Q(..)
+                           , Name)
+import Language.Haskell.TH.Ppr
+import qualified Data.List as L
+import qualified Data.Set as S
+import Data.Maybe
+import Control.Monad
+import Control.Monad.Error
+import Debug.Trace
+
+
+-- | Composed 'Position' defining positions in terms
+data Position = Root
+              | P Int
+              | Int `Dot` Position
+    deriving( Eq )
+
+instance Show Position where
+    show Root       = "R"
+    show (P i)      = show i
+    show (Dot i p)  = (show i) ++ "." ++ (show p)
+
+
+-- | Data type for holes in terms
+data Hole = Hole
+
+-- | Infix constructor for 'Position's
+infixr 5 °
+(°) :: Int              -- ^ the nth subterm 
+    -> Position         -- ^ sub-position, i.e. position in the nth subterm
+    -> Position         -- ^ the resulting position
+i ° Root = (P i)
+i ° p | i > 0      = i `Dot` p
+      | otherwise   = error $ "Terms.(°): Illegal position, no subternms " ++
+                              "with index =< 0 !"
+
+
+class Size t where
+    size :: t -> Int
+    size = size_ 0 
+    
+    size_ :: Int -> t -> Int
+    
+instance Size Exp where
+    size_ done (VarE _)             = done + 1
+    size_ done (ConE _)             = done + 1
+    size_ done (LitE _)             = done + 1
+    size_ done (TupE vals)          = sum $ (done + 1):(map size vals)
+    size_ done t@(AppE e1 e2 )      = sum $ (done + 1):(map size (unfoldAppEargs t))
+    size_ done (ListE l)            = sum $ (done + 1):(map size l)
+    size_ done (CondE e1 e2 e3)     = sum $ (done + 1):(map size [e1, e2, e3])    
+    size_ done (InfixE e1 _ e2)     = sum $ (done + 1):(map size (concatMap maybeToList[e1,e2]))
+    size_ _  e                      = 
+        error $ "Terms.Class.size: Not implemented for Expression " ++ (show e)
+
+instance Size Pat where
+    size_ done (VarP _)         = done + 1
+    size_ done (LitP _)         = done + 1
+    size_ done (ConP _ pats)    = sum $ (done + 1):(map size pats)
+    size_ done (InfixP p1 _ p2) = sum $ (done + 1):(map size [p1,p2] )
+    size_ done (ListP pats)     = sum $ (done + 1):(map size pats)
+    size_ done (TupP pats)      = sum $ (done + 1):(map size pats)
+    size_ _    p                = 
+        error $ "Terms.Class.size: Not implemented for Pattern " ++ (show p)
+
+
+-- testing
+
+instance Size Int where
+    size_ a b= a+b
+instance Size String where
+    size_ a b = a + length b
+
+
+-- Think about a better ordering relation than lexocographic which does not 
+-- return wrong result with maps (e.g. when using Size)
+-- 
+instance Ord Exp where
+    compare = ( \l r -> compare (show l) (show r) )
+    (<)     = ( \l r -> (<) (show l) (show r) )
+    (<=)    = ( \l r -> (<=) (show l) (show r) )
+    (>=)    = ( \l r -> (>=) (show l) (show r) )
+    (>)     = ( \l r -> (>) (show l) (show r) )
+             
+instance Ord Pat where
+    compare = ( \l r -> compare (show l) (show r) )
+    (<)     = ( \l r -> (<) (show l) (show r) )
+    (<=)    = ( \l r -> (<=) (show l) (show r) )
+    (>=)    = ( \l r -> (>=) (show l) (show r) )
+    (>)     = ( \l r -> (>) (show l) (show r) )
+
+
+
+    
+{- |
+    The class definition of 'Term's. Defining operations common to all terms
+-}
+class (Eq t, Show t, Ppr t) => Term t where
+    -- |Returns the positions of a subterm @s@ in a term @t@. I
+    getPos          :: t                 -- ^ the term
+                    -> t                 -- ^ the subterm
+                    -> [Position]        -- ^ the positions
+    subtermOf       :: t
+                    -> t
+                    -> Bool
+    subtermOf t s = not $ null $ (getPos t s)
+    -- | returns subterm @s@ at position @p@ in term @t@    
+    subtermAt         :: t                 -- ^ the term @t@
+                    -> Position          -- ^ a position @p@
+                    -> Maybe t               -- ^ subterm @s@ in @t@ at position @p@
+    subtermAt t Root = return t
+    subtermAt t pos = 
+        case pos of
+            (P i)     -> do { let subs = subterms t
+                            ; r <-  subs !?! i 
+                            ; noHole "Terms.subterm: No subterm at position" r}
+            (Dot i p) -> do { let subs = subterms t
+                            ; sub <- subs !?! i
+                            ; r <- subtermAt sub p
+                            ; noHole "Terms.subterm: No subterm at position" r}
+    
+    subtermsNoHole :: t -> [t]
+    subtermsNoHole t = filter (== hole) (subterms t)
+             
+    -- |Returns the immediate subterms of a term (which may be holes)
+    --  E.g.: subterms f(a,b) ~~> [a,b]               
+    subterms        :: t -> [t]
+                    
+    -- |Subsitute subterm at position @p@ in term @t@ with term @s@
+    --  If there is no such position @p@, @t@ is returned.
+    substitute      :: t                 -- ^ the substitute @s@
+                    -> Position          -- ^ the postion @p@
+                    -> t                 -- ^ the initial term @t@
+                    -> t                 -- ^ the result
+    
+    -- |Returns a (unique) list of all variables in t
+    getVars         :: t -> [t]
+    getVars         = S.elems.getVars_ S.empty
+    
+    -- |Returns a list of all variable position in t
+    getVarPos       :: t -> [(t,[Position])]
+    getVarPos t     =  [(st,getPos t st) | st <- (getVars t)]
+    
+    getVars_        :: (S.Set t) -> t -> (S.Set t)
+    
+    -- |Returns a (unique) list of all variable names in t
+    getVarNames     :: t -> [Name]
+    
+    
+    -- |The empty term. Especially to avoid the nasty 'Nothing' in 
+    --  'Language.Haskell.TH.InfixE' Not really sure if I need it. Should at 
+    --  least not be visible outside.
+    hole            :: t
+    noHole          :: String
+                    -> t
+                    -> Maybe t
+    noHole s t = if t == hole then fail s else return t
+
+
+instance Term Exp where
+    getPos t s | s == t     = [Root]
+               | otherwise  = 
+                    case t of
+                      (AppE e1 e2)                    -> let args = unfoldAppEargs t 
+                                                         in mapGetPos args s
+                      -- | _e is the operator (see <http://haskell.org/ghc/docs/latest/html/libraries/template-haskell/src/Language-Haskell-TH-Syntax.html#Exp>)
+                      (InfixE Nothing _e Nothing)     -> []
+                      (InfixE (Just e1) _e Nothing)   -> map (1°) (getPos e1 s)
+                      (InfixE Nothing _e (Just e2))   -> map (2°) (getPos e2 s)
+                      (InfixE (Just e1) _e (Just e2)) -> 
+                            let pos1 = map (1°) (getPos e1 s)
+                                pos2 = map (2°) (getPos e2 s)
+                            in pos1 ++ pos2
+                      (ListE (e1:es))                 -> mapGetPos [e1, ListE es] s  -- I HATE SYNTACTIC SUGAR!!!
+                      (TupE es)                       -> mapGetPos es s                                    
+                      _owise                          -> [] --  VarE Name, ConE Name, LitE Lit          
+                      -- These parts of the TH syntax are ignored:                      
+                      --LamE [Pat] Exp  
+                      --CondE Exp Exp Exp   
+                      --LetE [Dec] Exp  
+                      --CaseE Exp [Match]   
+                      --DoE [Stmt]  
+                      --CompE [Stmt]    
+                      --ArithSeqE Range 
+                      --SigE Exp Type   
+                      --RecConE Name [FieldExp] 
+                      --RecUpdE Exp [FieldExp]  
+            
+    substitute s Root _ = s
+    substitute s pos t =
+        case pos of
+            (P i)     -> maybe t id $  moveToSubtermE i t (Just.(substitute s Root))
+            (Dot i p) -> maybe t id $  moveToSubtermE i t (Just.(substitute s p))
+            
+    subterms (VarE _)                        = []
+    subterms (ConE _)                        = []
+    subterms (LitE _)                        = []
+    subterms (TupE vals)                     = vals
+    subterms t@(AppE _ _ )                   = unfoldAppE t
+    subterms (ListE l)                       = l
+    subterms (CondE e1 e2 e3)                = [e1, e2, e3]    
+    subterms (InfixE (Just e1) e2 (Just e3)) = [e1, e2, e3]
+    subterms (InfixE Nothing e2 (Just e3))   = [hole, e2, e3]
+    subterms (InfixE (Just e1) e2 Nothing)   = [e1, e2, hole]
+    subterms (InfixE Nothing e2 Nothing)     = [hole, e2, hole]
+    subterms    e                            = 
+        error $ "Terms.subterms: Not implemented for Expression " ++ (show e)
+    
+    getVars_ done t@(VarE _)                      = S.insert t done
+    getVars_ done (ConE _)                        = done
+    getVars_ done (LitE _)                        = done
+    getVars_ done (TupE vals)                     = 
+        S.unions (done:(map (getVars_ S.empty) vals))
+    getVars_ done (AppE a1 a2)                    = 
+        S.unions (done:(map (getVars_ S.empty) [a1,a2]))                                                        
+    getVars_ done (ListE l)                       = 
+        S.unions (done:(map (getVars_ S.empty) l))
+    getVars_ done (CondE e1 e2 e3)                = 
+        S.unions (done:(map (getVars_ S.empty) [e1, e2, e3]))
+    getVars_ done (InfixE e1 e2 e3)               = 
+        S.unions $ done: 
+                   (map (getVars_ S.empty) $
+                        (maybeToList e1) ++ [e2] ++ (maybeToList e3))
+                        
+    getVarNames t = map (\(VarE n) -> n)  $ getVars t
+        
+    hole = ConE 'Hole
+        
+instance Term Pat where
+    getPos t s | s == t     = [Root]
+               | otherwise  = 
+                    case t of
+                      (ConP _ ps)                    -> mapGetPos ps s
+                      (InfixP p1 _ p2) -> 
+                            let pos1 = map (1°) (getPos p1 s)
+                                pos2 = map (2°) (getPos p2 s)
+                            in pos1 ++ pos2
+                      (ListP (p1:ps))                 -> mapGetPos [p1, ListP ps] s  -- I HATE SYNTACTIC SUGAR!!!
+                      (TupP ps)                       -> mapGetPos ps s                                    
+                      _owise                          -> [] --  VarP Name, LitP Lit 
+    
+            
+    substitute s Root _ = s
+    substitute s pos t =
+        case pos of
+            (P i)     -> maybe t id $  moveToSubtermP i t (Just.(substitute s Root))
+            (Dot i p) -> maybe t id $  moveToSubtermP i t (Just.(substitute s p))
+            
+    
+    subterms (VarP _)         = []
+    subterms (LitP _)         = []
+    subterms (ConP _ pats)    = pats
+    subterms (InfixP p1 _ p2) = [p1,p2] 
+    subterms (ListP (p:ps))   = [p, ListP ps]
+    subterms (TupP pats)      = pats
+    subterms    p                            = 
+        error $ "Terms.subterms: Not implemented for Pattern " ++ (show p)
+        
+    getVars_ done t@(VarP _)                     = S.insert t done
+    getVars_ done (LitP _)                       = done
+    getVars_ done (TupP ps)                      = 
+        S.unions (done:(map (getVars_ S.empty) ps))
+    getVars_ done (ConP _ ps)                    = 
+        S.unions (done:(map (getVars_ S.empty) ps))
+    getVars_ done (ListP l)                      = 
+        S.unions (done:(map (getVars_ S.empty) l))
+    getVars_ done (InfixP e1 _ e2)              = 
+        S.unions (done:(map (getVars_ S.empty) [e1, e2]))
+                        
+    getVarNames t = map (\(VarP n) -> n)  $ getVars t
+        
+    hole = ConP 'Hole []
+ 
+--------------------------------------------------------------------------------
+-- General auxiliary functions for 'Term's
+--------------------------------------------------------------------------------  
+-- |This monster applies 'getPos' to a list of terms and keeps track of the 
+--  argument position.
+mapGetPos :: (Term x) => [x] -> x -> [Position]                              
+mapGetPos ts s = concat $ snd $ L.mapAccumL (\i t -> (i+1, map (i°) (getPos t s))) 1 ts
+       
+-- | Applys a function @f@ at the nth element i of a list (zero-based)
+applyAtIndex  :: (Monad m) => [a] -> Int -> (a -> m a) -> (m [a])
+applyAtIndex xs n _ | n < 0 = fail "Terms.applyAtIndex: negative index"
+applyAtIndex [] _ _        =  fail "Terms.applyAtIndex: index too large"
+applyAtIndex (x:xs) 0 f    =  do {fx <- (f x); return (fx:xs) }
+applyAtIndex (x:xs) n f    =  do {fxs <- (applyAtIndex xs (n-1) f); return (x:fxs)}
+
+
+-- | /Secure/ 'Prelude.!!'
+infix 5 !?!
+(!?!) ::(Monad m) => [a] -> Int -> m a
+[] !?! i        = fail "Terms.applyAtIndex: index too large"
+(x:xs) !?! i  
+    | i < 0     = fail "Terms.applyAtIndex: negative index"
+    | i == 0    = return x
+    | otherwise = xs  !?! (i-1)
+
+--------------------------------------------------------------------------------
+-- Auxiliary functions for 'Exp' as 'Term's
+--------------------------------------------------------------------------------
+
+unfoldAppEargs = tail . unfoldAppE
+
+-- | Peals the @Exp@s out of a @AppE@
+unfoldAppE :: Exp -> [Exp]
+unfoldAppE e = f [] e
+    where 
+    f done e =
+        case e of
+            (AppE e1@(VarE _) e2) -> e1:e2:done
+            (AppE e1@(ConE _) e2) -> e1:e2:done
+            (AppE e1 e2)       -> f (e2:done) e1
+            _owise             -> e:done
+ 
+foldAppE :: [Exp] -> Exp
+foldAppE es = foldl1 AppE es
+
+
+-- |Moves to the specified subterm in the term @t@ and applies function @f@.
+--  The result is term @t@ with modified @i@th subterm
+--  It assures, that everything is put back at place when returning the result.
+moveToSubtermE :: (Monad m) => Int -> Exp -> (Exp -> m Exp) -> m Exp
+moveToSubtermE _ (VarE _) _ = fail "Terms.moveToSubtermE. No subterm at position"        
+moveToSubtermE _ (LitE _) _ = fail "Terms.moveToSubtermE. No subterm at position"    
+moveToSubtermE _ (ConE _) _ = fail "Terms.moveToSubtermE. No subterm at position"
+    
+moveToSubtermE i t@(AppE _ _ ) f  = 
+   liftM foldAppE (applyAtIndex (unfoldAppE t) i f)
+    
+moveToSubtermE i (TupE es) f      = 
+   liftM TupE (applyAtIndex es i f)
+    
+moveToSubtermE i (ListE (e:es)) f = do
+    let elist = [e, ListE es]
+    [e', ListE es'] <- (applyAtIndex elist i f)
+    return $ ListE (e:es)
+    
+moveToSubtermE 1 (InfixE (Just e1) op e2) f = 
+    do { e <- f e1; return $ (InfixE (Just e) op e2)}
+moveToSubtermE 2 (InfixE e1 op (Just e2)) f = 
+    do { e <- f e2; return $ (InfixE e1 op (Just e))}
+moveToSubtermE _ (InfixE _ _ _ ) _          = 
+    fail "Terms.moveToSubtermE: No subterm at position"
+                                    
+
+--------------------------------------------------------------------------------
+-- Auxiliary functions for 'Pat' as 'Term's
+--------------------------------------------------------------------------------
+
+-- |Moves to the specified subterm in the term @t@ and applies function @f@.
+--  The result is term @t@ with modified @i@th subterm
+--  It is assured, that everything is put back in place when returning the result.
+moveToSubtermP :: (Monad m) => Int -> Pat -> (Pat -> m Pat) -> m Pat
+moveToSubtermP _ (VarP _) _ = fail "Terms.moveToSubtermE. No subterm at position"        
+moveToSubtermP _ (LitP _) _ = fail "Terms.moveToSubtermE. No subterm at position"    
+moveToSubtermP i (ConP n ps) f = liftM (ConP n) (applyAtIndex ps i f)
+   
+moveToSubtermP i (TupP ps) f      = 
+    liftM TupP (applyAtIndex ps i f)
+    
+moveToSubtermP i (ListP (p:ps)) f = do
+    let plist = [p,  ListP ps]
+    [p', ListP ps'] <- (applyAtIndex plist i f)
+    return $  ListP (p:ps)
+    
+moveToSubtermP i (InfixP p1 op p2) f = do
+    [p1',p2'] <- applyAtIndex [p1,p2] i f
+    return $ (InfixP p1' op p2')
hunk ./src/Terms/Unifier.hs 1
-
+{-# OPTIONS_GHC -fglasgow-exts -fth  -XTypeSynonymInstances #-}
+module Terms.Unifier (
+
+    Replacement,
+    Substitution,
+    Unifieable(mgu, applyMgu,matches)
+    
+    )where
+
+import Language.Haskell.TH (Pat(..), Exp(..))
+import Control.Monad.State (MonadState, StateT, execStateT, put, get)
+import Terms.Class
+import Data.List (insert, intersperse)
+import Logging
+import qualified Data.Traversable as T (sequence)
+
+
+infixr 0 <~
+(<~) :: a -> b -> (a, b)
+(<~) = (,)  
+
+type Replacement a = (a,a)
+instance (Pretty a) => Pretty (Replacement a) where
+    pretty (e1,e2) = ["(" ++ (view e1) ++ " <~ " ++ (view e2) ++ ")"]
+   
+type Substitution t = [Replacement t]
+instance (Pretty a) => Pretty (Substitution a) where
+    pretty s = map view s
+
+insertApply :: (Eq a) =>  (Replacement a) -> (Substitution a) -> (Substitution a)
+insertApply s [] = [s]
+insertApply s@(x,v) (u@(y,w):us) 
+    | (w == x) && (y == v) = (insertApply s us)
+    | w == x               = (y <~ v):(insertApply s us)
+    | otherwise            =  u:(insertApply s us)
+
+--instance (Show a, Pretty a) => Pretty (Substitution a) where
+--    view u =  "[" ++ ((concat.(intersperse ",")) (map view u)) ++ "]"
+    
+    
+type U m a = StateT (Substitution a) m ()
+
+
+class (Term t, Ord t, Show t, Pretty t) => Unifieable t where
+    
+    mgu :: ( ELog m) => t -> t -> m (Substitution t)
+    mgu x y = 
+              -- Logging stuff
+              setCurrentLogger "Terms.Unifier.mgu" >>
+              logDE ["Unifying terms:",skip (view x),skip (view y)] >> 
+              -- 
+              execStateT (unify x y) []
+    
+    applyMgu :: ( ELog m) => (Substitution t) -> t -> m t
+        
+    matchesWithSubs :: ( ELog m) =>  t -> t -> m (Substitution t)  
+    matchesWithSubs x y = execStateT (match x y) []
+                          -- `catchError` (\_ -> return [])
+                          -- distinguish between equality and nomatch
+                          -- , so propagate error
+    
+    matches :: ( ELog m) =>  t -> t -> m Bool
+    matches t1 t2 = liftM (not.null) (matchesWithSubs t1 t2)
+    
+    subsumes :: ( ELog m) =>  t -> t -> m Bool
+    subsumes t1 t2 = matches t2 t1
+    
+    match :: ( ELog m) =>  t -> t -> U m t
+    
+    matchVar :: ( ELog m) => t -> t -> U m t
+    matchVar var t = 
+        do unifier <- get  
+           case (lookup var unifier) of
+            Just val -> 
+                llogDE ["Found (Var <~ Val) in current unifier:"
+                        ,skip (view var) ++ " <~ " ++ (view val)
+                        ,skip "but need to match:"
+                        ,skip (view var) ++ " <~ " ++ (view t)] >>
+                flush >> fail "No Match!"
+            Nothing  -> put (insert (var <~ t) unifier)
+    
+    unify :: ( ELog m) =>  t -> t -> U m t
+             
+    unifyVar :: ( ELog m) => t -> t -> U m t
+    unifyVar var x = 
+        do unifier <- get  
+           lift $ setCurrentLogger "Terms.Unifier.unifyVar"
+           llogEnterDE
+           llogDE ["Var is:"
+                  ,skip $ view var
+                  ,"X is:"
+                  ,skip $ view x
+                  ,"Current unifier is:"
+                  ,skip $ view unifier]     
+           case (lookup var unifier) of
+            Just val -> 
+                llogDE ["Found (Var <~ Val) in current unifier:"
+                                            ,skip (view var) ++ " <~ " ++ (view val)
+                                            ,skip "continue unify val x"] >>
+                unify val x
+            Nothing  -> do case (lookup x unifier) of
+                             Just val -> 
+                                llogDE ["Found (X <~ Val) in current unifier:"
+                                                            ,skip (view x) ++ " <~ " ++ (view val)
+                                                            ,skip "continue unify var val"] >>
+                                unify var val
+                             Nothing  -> if var `subtermOf` x
+                                            then flush >> fail "Not unifieable"
+                                            else do llogDE ["Apply (Var <~ X) to current Unifier and Insert:"
+                                                                                ,skip (view var) ++ " <~ " ++ (view x)] 
+                                                    put (insertApply (var <~ x) unifier)
+    
+    
+instance Unifieable Exp where
+    -- | Straight forward walking down Exp-terms, pass the function call to
+    --   subterms and replace variables as specified by the Unifier.
+    --   Well, and of course some necessary lifting. 
+    applyMgu u v@(VarE _)        = case lookup v u of 
+                                     Just val -> return val
+                                     Nothing  -> return v
+    applyMgu u t@(ConE _ )       = return t
+    applyMgu u t@(LitE _)        = return t
+    applyMgu u (ListE ts)        = liftM ListE (mapM (applyMgu u) ts)
+    applyMgu u (TupE ts)         = liftM TupE (mapM (applyMgu u) ts)
+    applyMgu u (AppE a1 a2)      = liftM2 AppE (applyMgu u a1) (applyMgu u a2)
+    applyMgu u (InfixE e1 op e2) = 
+        do subs1 <- T.sequence $ liftM (applyMgu []) e1 -- Monad juggling because of Maybe
+           subs2 <- T.sequence $ liftM (applyMgu []) e2 -- Maybe (m a) ~~> m (Maybe a)
+           return $ InfixE subs1 op subs2
+    applyMgu u (CondE e1 e2 e3)  = 
+        liftM3 CondE (applyMgu u e1) (applyMgu u e1) (applyMgu u e1)
+    applyMgu u t                               =   
+        let msg =  pnd [view u, view t]
+        in setCurrentLogger "Terms.Unifier.applyMgu" >>
+           logWA msg >> fail (concat msg)
+         
+    
+    match s@(VarE _) t@(VarE _)             = if (s == t) 
+                                                then return () 
+                                                else matchVar s t
+    match s@(VarE _) t                      = matchVar s t
+    match s          t@(VarE _)             = flush >> fail "No Match" 
+    
+    match s@(ConE _) t@(ConE _) 
+        | (s == t)                          = return () 
+        | otherwise                         = flush >> fail "No Match!"  
+        
+    match s@(LitE _) t@(LitE _) 
+        | (s == t)                          = return () 
+        | otherwise                         = flush >> fail "No Match!"  
+         
+    match (TupE s) (TupE t) 
+        | (length s) == (length t)          = mapM_ (uncurry unify) (zip s t)
+        | otherwise                         = flush >> fail "No Match!"  
+        
+    match (ListE [])(ListE [])              = return ()
+    match (ListE (s:ss))(ListE (t:ts))      = match s t >> match (ListE ss) (ListE ts)
+    -- as usual, something special for lists, so check whether the AppE is of 
+    -- the form (AppE (AppE (ConE GHC.Base.:) elem) restlist)
+    match (ListE (s:ss)) t@(AppE _ _)       = do
+        case unfoldAppE t of
+            (op:a1:[a2]) ->
+                if op == (ConE '(:))
+                  then match s a1 >> match (ListE ss) a2
+                  else flush >> fail "No Match!"  
+            _owise       -> flush >> fail "No Match!"  
+    match t@(AppE _ _) s@(ListE _)          = match s t 
+    
+    match (AppE s1 s2)(AppE t1 t2)          = match s1 t1 >> match s2 t2
+    
+    match (InfixE s1 s2 s3)(InfixE t1 t2 t3)
+        | s2 == t2                          = liftMatch s1 t1 >> liftMatch s3 t3
+        | otherwise                         = flush >> fail "No Match!"  
+        
+    match (CondE s1 s2 s3) (CondE t1 t2 t3) = 
+        match s1 t1 >> match s2 t2 >> match s3 t3
+    
+    match s t                               =   
+        let msg =  pnd [view s, view t]
+        in lift (setCurrentLogger "Terms.Unifier.match") >>
+           llogWA msg >> llogDE (map show (unfoldAppE t)) >>
+           fail (concat msg)
+         
+    
+    unify s@(VarE _) t@(VarE _)             = if (s == t) 
+                                                then return () 
+                                                else unifyVar s t
+    unify s@(VarE _) t                      = unifyVar s t
+    unify s          t@(VarE _)             = unifyVar t s    
+    
+    unify s@(ConE _) t@(ConE _) 
+        | (s == t)                          = return () 
+        | otherwise                         = flush >> fail "Not unifieable" 
+        
+    unify s@(LitE _) t@(LitE _) 
+        | (s == t)                          = return () 
+        | otherwise                         = flush >> fail "Not unifieable"
+         
+    unify (TupE s) (TupE t) 
+        | (length s) == (length t)          = mapM_ (uncurry unify) (zip s t)
+        | otherwise                         = flush >> fail "Not unifieable" 
+        
+    unify (ListE [])(ListE [])              = return ()
+    unify (ListE (s:ss))(ListE (t:ts))      = unify s t >> unify (ListE ss) (ListE ts)
+    -- as usual, something special for lists, so check whether the AppE is of 
+    -- the form (AppE (AppE (ConE GHC.Base.:) elem) restlist)
+    unify (ListE (s:ss)) t@(AppE _ _)       = do
+        case unfoldAppE t of
+            (op:a1:[a2]) ->
+                if op == (ConE '(:))
+                  then unify s a1 >> unify (ListE ss) a2
+                  else flush >> fail "Not unifieable" 
+            _owise       -> flush >> fail "Not unifieable" 
+    unify t@(AppE _ _) s@(ListE _)          = unify s t 
+    
+    unify (AppE s1 s2)(AppE t1 t2)          = unify s1 t1 >> unify s2 t2
+    
+    unify (InfixE s1 s2 s3)(InfixE t1 t2 t3)
+        | s2 == t2                          = liftUnify s1 t1 >> liftUnify s3 t3
+        | otherwise                         = flush >> fail "Not unifieable" 
+        
+    unify (CondE s1 s2 s3) (CondE t1 t2 t3) = 
+        unify s1 t1 >> unify s2 t2 >> unify s3 t3
+    
+    unify s t                               =   
+        let msg =  pnd [view s, view t]
+        in lift (setCurrentLogger "Terms.Unifier.unify") >>
+           llogWA msg >> llogDE (map show (unfoldAppE t)) >>
+           fail (concat msg)
+
+-- | Helper for unifying (InfixE Maybe Exp) Exp (Maybe Exp))
+liftUnify :: ( ELog m) => Maybe Exp -> Maybe Exp -> U m Exp
+liftUnify = (\u v -> maybe (return ()) (\(s,t) -> unify s t) (liftM2 (,) u v))
+
+-- | Helper for matching (InfixE Maybe Exp) Exp (Maybe Exp))
+liftMatch :: ( ELog m) => Maybe Exp -> Maybe Exp -> U m Exp
+liftMatch = (\u v -> maybe (return ()) (\(s,t) -> match s t) (liftM2 (,) u v))     
+   
+instance Unifieable Pat where
+
+    applyMgu u v@(VarP _)        = case lookup v u of 
+                                     Just val -> return val
+                                     Nothing  -> return v
+    applyMgu u (ConP n ps)       = liftM (ConP n) (mapM (applyMgu u) ps )
+    applyMgu u t@(LitP _)        = return t
+    applyMgu u (ListP ts)        = liftM ListP (mapM (applyMgu u) ts)
+    applyMgu u (TupP ts)         = liftM TupP (mapM (applyMgu u) ts)
+    applyMgu u (InfixP e1 op e2) =
+        liftM3 InfixP (applyMgu u e1) (return op) (applyMgu u e2)
+    applyMgu u t                 =   
+        let msg =  pnd [view u, view t]
+        in  setCurrentLogger "Terms.Unifier.applyMgu" >>
+            logWA msg >> fail (concat msg) 
+    
+    match s@(VarP _) t@(VarP _ )       = if (s == t) then return () else matchVar s t
+    match s@(VarP _) t                 = matchVar s t
+    match s          t@(VarP _)        = matchVar t s 
+         
+    match s@(LitP _) t@(LitP _) 
+        | (s == t)                     = return () 
+        | otherwise                    = flush >> fail  "No Match!"  
+         
+    match (ListP [])(ListP [])         = return ()
+    match (ListP (s:ss))(ListP (t:ts)) = match s t >> match (ListP ss) (ListP ts) 
+    -- as usual, something special for lists, so check whether the ConP is of 
+    -- the form (ConP GHC.Base.: [elem, restlist])
+    match (ListP (s:ss))(ConP n ([p,ps]))= 
+        if n == '(:)
+          then match s p >> match (ListP ss) ps
+          else flush >> fail  "Not unifieable"  
+    match s@(ListP _) t@(ConP _ _)     = match t s
+    
+    match s@(ConP n1 p1) t@(ConP n2 p2) 
+        | n1 == n2                     = mapM_ (uncurry match) (zip p1 p2)
+        | otherwise                    = flush >> fail  "No Match!"  
+        
+    match (TupP s) (TupP t) 
+        | (length s) == (length t)     = mapM_ (uncurry match) (zip s t)
+        | otherwise                    = flush >> fail  "No Match!"  
+        
+    match (InfixP s1 s2 s3)(InfixP t1 t2 t3)
+        | s2 == t2                     = match s1 t1 >> match s3 t3
+        | otherwise = flush >> fail  "No Match!"  
+        
+    match s t                          =    
+        flush >> fail  ("Term " ++ (show s) ++ "does not match with term " ++ (show t))
+        
+    
+    unify s@(VarP _) t@(VarP _ )       = if (s == t) then return () else unifyVar s t
+    unify s@(VarP _) t                 = unifyVar s t
+    unify s          t@(VarP _)        = unifyVar t s 
+         
+    unify s@(LitP _) t@(LitP _) 
+        | (s == t)                     = return () 
+        | otherwise                    = flush >> fail  "Not unifieable"
+         
+    unify (ListP [])(ListP [])         = return ()
+    unify (ListP (s:ss))(ListP (t:ts)) = unify s t >> unify (ListP ss) (ListP ts) 
+    -- as usual, something special for lists, so check whether the ConP is of 
+    -- the form (ConP GHC.Base.: [elem, restlist])
+    unify (ListP (s:ss))(ConP n ([p,ps]))= 
+        if n == '(:)
+          then unify s p >> unify (ListP ss) ps
+          else flush >> fail  "Not unifieable"
+    unify s@(ListP _) t@(ConP _ _)     = unify t s
+    
+    unify s@(ConP n1 p1) t@(ConP n2 p2) 
+        | n1 == n2                     = mapM_ (uncurry unify) (zip p1 p2)
+        | otherwise                    = flush >> fail  "Not unifieable"
+        
+    unify (TupP s) (TupP t) 
+        | (length s) == (length t)     = mapM_ (uncurry unify) (zip s t)
+        | otherwise                    = flush >> fail  "Not unifieable"
+        
+    unify (InfixP s1 s2 s3)(InfixP t1 t2 t3)
+        | s2 == t2                     = unify s1 t1 >> unify s3 t3
+        | otherwise = flush >> fail  "Not unifieable"
+        
+    unify s t                          = 
+        flush >> fail  ("Term " ++ (show s) ++ "not unifieable with " ++ (show t))
+        
+flush :: (MonadState (Substitution t) m) => m () 
+flush = put []
hunk ./src/Terms.hs 1
-
+module Terms (
+    
+    module Language.Haskell.TH,
+    module Terms.Class,
+    module Terms.Unifier,
+    module Terms.Antiunifier
+    
+    ) where
+
+import Language.Haskell.TH ( Dec (FunD)
+                           , Clause (Clause)
+                           , Body (NormalB)
+                           , Name, mkName
+                           , Exp (VarE, ConE, LitE, ListE, TupE, InfixE, AppE, CondE)
+                           , Pat (VarP, ConP, LitP, ListP, TupP, InfixP) 
+                           , Q(..))
+import Terms.Class
+import Terms.Unifier (Replacement, Substitution, Unifieable(..))
+import Terms.Antiunifier
hunk ./src/Test.hs 1
-
+{-# OPTIONS_GHC -fglasgow-exts -fth   #-}
+module Test where
+
+import Terms
+import Data
+import Logging
+import Control.Monad.Trans (liftIO)
+import Language.Haskell.TH
+import IgorMonad
+
+{-------------------------------------------------------------------------------
+   Test Cases
+-------------------------------------------------------------------------------}
+
+data Tree a = E | N a (Tree a) (Tree a)
+
+
+printQ q = (runQ q) >>= putStrLn . pprint 
+showQ q = (runQ q) >>= putStrLn . show
+
+
+tuples1,tuples2,tuples3,tuples4 :: Q [Exp]        
+tuples1 = sequence [[|(1,1)|]
+          ,[|(2,2)|]
+          ,[|(3,3)|]] 
+tuples2 = sequence [[|(1,2)|]
+          ,[|(2,2)|]
+          ,[|(3,3)|]]
+tuples3 = sequence [[|(3,1)|]
+          ,[|(2,2)|]
+          ,[|(3,3)|]]
+tuples4 = sequence [[|(3,1)|]
+          ,[|(3,2)|]
+          ,[|(3,3)|]]
+
+apps1, apps2, apps3, apps4, apps5  :: Q [Exp]                  
+apps1 = sequence [[|(:) 1 ((:) 2 [])|]
+        ,[|(:) 1 ((:) 2 [])|]]
+apps2 = sequence [[|(:) 2 ((:) 2 [])|]
+        ,[|(:) 1 ((:) 2 [])|]]
+apps3 = sequence [[|(:) 1 ((:) 2 [])|]
+        ,[|(:) 1 ((:) 2 ((:) 3 []))|]
+        ,[|(:) 1 ((:) 2 [])|]]
+apps4 = sequence [[|reverse ((:) 1 ((:) 2 []))|]
+        ,[|reverse ((:) 1 ((:) 2 ((:) 3 [])))|]
+        ,[|reverse ((:) 1 ((:) 2 []))|]]
+apps5 = sequence [[|reverse ((:) 1 ((:) 2 []))|]
+        ,[|(:) 1 ((:) 2 ((:) 3 []))|]
+        ,[|(:) 1 ((:) 2 [])|]]
+
+list1,list2,list3,list4,list5,list6 :: Q [Exp]       
+list1 = sequence [[|[1,2,3]|]
+        ,[|[1,2,3]|]]
+list2 = sequence [[|[1,2,3]|]
+        ,[|[1,2,4]|]]
+list3 = sequence [[|[1,2,3]|]
+        ,[|[1,2,4,5]|]]
+list4 = sequence [[|[1,2,3]|]
+        ,[|[4,5,6]|]]
+list5 = sequence [[|[1,2,3]|]
+        ,[|[4,5,6,7]|]]
+list6 = sequence [[|[]|]
+        ,[|[]|]]
+
+infix1,infix2,infix3,infix4,infix5,infix6,infix7,infix8 :: Q [Exp]
+infix1 = sequence [[|1+2|]
+         ,[|1+2|]]
+infix2 = sequence [[|2+2|]
+         ,[|1+2|]] 
+infix3 = sequence [[|1+2|]
+         ,[|2+1|]]
+infix4 = sequence [[|(+2)|]
+         ,[|(+2)|]]
+infix5 = sequence [[|(1+)|]
+         ,[|(1+)|]]
+infix6 = sequence [[|(+2)|]
+         ,[|(1+)|]
+         ,[|1+2|]]
+infix7 = sequence [[|(2+)|]
+         ,[|(1+)|]]
+infix8 = sequence [[|(+2)|]
+         ,[|(+1)|]]
+
+fundef0,fundef1,fundef2,fundef3,fundef4,fundef5 :: Q [Dec]
+fundef0 = return []
+fundef1 = sequence [liftM head [d| reverse (1:xs)   = xs ; 
+                                   reverse (1:2:xs) = (2:xs) |]]
+fundef2 = sequence [liftM head [d| reverse (1:xs)   = xs ; 
+                                   reverse (1:2:xs) = 2 |]]
+fundef3 = sequence [liftM head [d| reverse [1,2,3] = [3,2,1] ;
+                                   reverse [3,2,1] = [1,2,3] |]]
+fundef4 = sequence [liftM head [d| fst (1,2) = 1 ;
+                                   fst (1,4) = 1 |]]
+fundef5 = sequence [liftM head [d| fst (1,x) = 1 ;
+                                   fst (1,x) = 1 |]]
+
+
+
+
+u = 1
+v = 2
+w = 3
+x = 4
+y = 5
+z = 6
+
+
+varU = varE $ mkName "u"
+varV = varE $ mkName "v"
+varW = varE $ mkName "w"
+varX = varE $ mkName "x"
+varY = varE $ mkName "y"
+varZ = varE $ mkName "z"
+var0 = varE $ mkName "0"
+var1 = varE $ mkName "1"
+var2 = varE $ mkName "2"
+var3 = varE $ mkName "3"
+var4 = varE $ mkName "4"
+
+
+varpU = varP $ mkName "u"
+varpV = varP $ mkName "v"
+varpW = varP $ mkName "w"
+varpX = varP $ mkName "x"
+varpY = varP $ mkName "y"
+varpZ = varP $ mkName "z"
+varp0 = varP $ mkName "0"
+varp1 = varP $ mkName "1"
+varp2 = varP $ mkName "2"
+varp3 = varP $ mkName "3"
+varp4 = varP $ mkName "4"
+
+term00 =  [| (w,2,y)|]
+term00v = [| (1,x,3)|]
+
+term01 =  [| (x,y)|]
+term01v = [| (y,x)|]
+
+term02 =  [| (x,x)|]
+term02v = [| (w,y)|]
+
+term03 =  [| (x,w)|]
+term03v = [| (w,y)|]
+
+term04 =  [| (x,w,w)|]
+term04v = [| (x,w,x)|]
+
+term04' =  [| (x,w,w)|]
+term04v' = [| (x,w,x)|]
+
+term1 = [| (x,y)|]
+term1v = [| (fst (x,y),y)|]
+
+term2 =   [|reverse ((:) 1 ((:) 2 ((:) 3 ((:) 4 [] ))))|]
+term2v =  [|reverse ((:) u ((:) v ((:) w ((:) x [] ))))|]    
+
+term3 = appE (varE 'reverse) (appE (appE (conE '(:)) (litE (IntegerL 1))) (appE (appE (conE '(:)) (litE (IntegerL 2))) (appE (appE (conE '(:)) (litE (IntegerL 3))) (appE (appE (conE '(:)) (litE (IntegerL 4))) (conE '[])))))
+term3v = appE (varE 'reverse) (appE (appE (conE '(:)) (varU )) (appE (appE (conE '(:)) ( varV)) (appE (appE (conE '(:)) (varW)) (appE (appE (conE '(:)) (varX)) (conE '[])))))
+
+term4 = appE (appE (varE 'drop) (litE (IntegerL 3))) (listE [tupE [litE (IntegerL 1),litE (IntegerL 2),litE (IntegerL 3),litE (IntegerL 4)],tupE [litE (IntegerL 1),litE (IntegerL 2),litE (IntegerL 3),litE (IntegerL 4)],tupE [litE (IntegerL 1),litE (IntegerL 2),litE (IntegerL 3),litE (IntegerL 4)]])
+term4v = appE (appE (varE 'drop) (litE (IntegerL 3))) (listE [tupE [litE (IntegerL 1),litE (IntegerL 2),litE (IntegerL 3),litE (IntegerL 4)],tupE [litE (IntegerL 1),litE (IntegerL 2),litE (IntegerL 3),litE (IntegerL 4)],tupE [litE (IntegerL 1),litE (IntegerL 2),litE (IntegerL 3),litE (IntegerL 4)]])
+
+term5' = appE (appE (varE 'drop) (litE (IntegerL 3))) (appE (appE (conE '(:)) (appE (appE (appE (appE (conE '(,,,)) (litE (IntegerL 1))) (litE (IntegerL 2))) (litE (IntegerL 3))) (litE (IntegerL 4)))) (appE (appE (conE '(:)) (appE (appE (appE (appE (conE '(,,,)) (litE (IntegerL 1))) (litE (IntegerL 2))) (litE (IntegerL 3))) (litE (IntegerL 4)))) (appE (appE (conE '(:)) (appE (appE (appE (appE (conE '(,,,)) (litE (IntegerL 1))) (litE (IntegerL 2))) (litE (IntegerL 3))) (litE (IntegerL 4)))) (conE '[]))))
+term5v' = appE (appE (varE 'drop) (varX)) (appE (appE (conE '(:)) (appE (appE (appE (appE (conE '(,,,)) (varW)) (varY)) (varX)) (varZ))) (appE (appE (conE '(:)) (appE (appE (appE (appE (conE '(,,,)) (varW)) (varY)) (varX)) (varZ))) (appE (appE (conE '(:)) (appE (appE (appE (appE (conE '(,,,)) (varW)) (varY)) (varX)) (varZ))) (conE '[]))))
+term5    = [|drop 3 [(1,2,3,4,5),(1,2,3,4,5),(1,2,3,4,5),(1,2,3,4,5)]|]
+term5v   = [|drop 3 [(5,4,3,2,1),(5,4,3,2,1),(5,4,3,2,1),(5,4,3,2,1)]|]
+term5''  = [|drop 3 [(1,2,3,4,5),(1,2,3,4,5),(1,2,3,4,5),(1,2,3,4,5)]|]
+term5v'' = [|drop 3 [(5,4,3,2,1),(5,4,3,2,1),(5,4,3,2,1)]|]
+
+term6' = (appE (appE (appE (appE (conE '(,,,)) (litE (IntegerL 1))) (litE (IntegerL 2))) (litE (IntegerL 3))) (litE (IntegerL 4)))
+term6v' = (appE (appE (appE (appE (conE '(,,,)) (varZ)) (varY)) (varX)) (varU))
+term6 = [|(1,2,3,4)|]
+term6v = [|(w,x,y,z)|]
+
+term7' = (appE (appE (appE (appE (conE '(,,,)) (litE (IntegerL 1))) (litE (IntegerL 1))) (litE (IntegerL 1))) (litE (IntegerL 1)))
+term7v' = (appE (appE (appE (appE (conE '(,,,)) (varZ)) (varY)) (varX)) (varU))
+term7 = [|(1,1,1,1)|]
+term7v = [|(w,x,y,z)|]
+
+term8 =  [| N 1 (N 3 (N 4 E E) ( N 5 E E)) (N 2 (E) (E)) |] 
+term8' = [| N 2 (N 2 (E) (E)) (N 3 (N 4 E E) ( N 5 E E)) |]
+
+
+a = (N 4 E E)
+term9b  =  [| N 1 (N 3 (N 4 E E) ( N 5 E E)) (N 2 (E) (E)) |] 
+term9b' =  [| N 1 (N 3     a     ( N 5 E E)) (N 2 (E) (E)) |] 
+
+terms9 = sequence [ [d|rev [] = []|]
+                  , [d|rev [a] = [a]|]
+                  , [d|rev [a,b] = [b,a]|]
+                  , [d|rev [a,b,c] = [c,b,a]|]
+                  ]
+term10 = [| [x,y,z]|]        
+term10' = [| [u,v]|]        
+pat1 = conP '(:) [litP (IntegerL 1),conP '(:) [litP (IntegerL 2),conP '(:) [litP (IntegerL 3),conP '(:) [litP (IntegerL 4),conP '[] []]]]]
+pat1v = conP '(:) [varpZ,conP '(:) [varpY,conP '(:) [varpX,conP '(:) [varpW,conP '[] []]]]]
+
+
+revexmpls1 = liftM head [d| rev [] = []
+                            rev [x] = [x]
+                            rev [x,y] = [y,x]
+                            rev [x,y,z] = [z,x,y]
+                         |]
+revexmpls2 = liftM head [d| rev [x,y,z] = [z,x,y]
+                            rev [x,y] = [y,x]
+                            rev [x] = [x] 
+                            rev [] = []
+                         |]
+
+testunify :: (Term t, ELog m,Antiunifieable k v t,Unifieable t) => t -> t -> m t
+testunify t s = do setCurrentLogger "testunify"
+                   logIN $ ["Term 1 is ", skip (view t),"Term 2 is ", skip (view s) ]
+                                      
+                   logIN $ ["Unifying Term1 and Term1"]
+                   u1 <- mgu t s
+                   logIN $ ["Resulting unifier is " ++ (view u1)]      
+                   return t
+                   
+testantiunify :: (Term t, ELog m,Antiunifieable k v t,Unifieable t) => t -> t -> m t
+testantiunify t s = do logIN $ ["Term 1 is ", skip (view t),"Term 2 is ", skip (view s) ]
+                   
+                       logIN $ ["Antiunifying Term1 and Term2"]
+                       ai <- antiunify [t,s]
+                       logIN $ ["Resulting antiinstance is " ++ (view ai)]    
+                       return t                                   
+testcase1 :: (Term t, ELog m,Antiunifieable k v t,Unifieable t) => t -> t -> m t
+testcase1 t s = do --setGlobalLogLevel "Test"
+                   setCurrentLogger "Test.testcase1" 
+                   logIN $ ["Term 1 is ", skip (view t),"Term 2 is ", skip (view s) ]
+                   
+                   logIN $ ["Antiunifying Term1 and Term2"]
+                   ai <- antiunify [t,s]
+                   logIN $ ["Resulting antiinstance is " ++ (view ai)]                   
+                   
+                   logIN $ ["Unifying Term1 and antiinstance"]
+                   u1 <- mgu t ai
+                   logIN $ ["Resulting unifier is " ++ (view u1)]      
+                   
+                   logIN $ ["Unifying Term1 and Term2"]
+                   u2 <- mgu t s
+                   logIN $ ["Resulting unifier is " ++ (view u2)]
+                   
+                   logIN ["Applying unifier to Term1: " ++ (view t)]
+                   au1 <- applyMgu u2 t
+                   logIN $ ["Result is " ++ (view au1)]    
+                   
+                   logIN ["Applying unifier to Term2: " ++ (view s)]
+                   au2 <- applyMgu u2 s
+                   logIN $ ["Result is " ++ (view au2)]            
+                   return au2
+                   
+testcase2 :: (Term t, ELog m,Antiunifieable k v t,Unifieable t) => t -> t -> m t
+testcase2 t s = do --setGlobalLogLevel "Test"
+                   setCurrentLogger "Test.testcase2" 
+                   logIN $ ["Term 1 is ", skip (view t),"Term 2 is ", skip (view s) ]
+                   
+                   logIN $ ["Antiunifying Term1 and Term2"]
+                   ai <- antiunify [t,s]
+                   logIN $ ["Resulting antiinstance is " ++ (view ai)]                   
+                   
+                   logIN $ ["Unifying Term1 and antiinstance"]
+                   u1 <- mgu t ai
+                   logIN $ ["Resulting unifier is " ++ (view u1)]
+                   
+                   logIN $ ["Matching Term1 and antiinstance"]
+                   m <- matches t ai
+                   logIN $ ["Result is " ++ (show m)]
+                   return t
+                   
+testcase3 :: (Term t, ELog m,Antiunifieable k v t,Unifieable t) => t -> t -> m t
+testcase3 t s = do --setGlobalLogLevel "Test"
+                   setCurrentLogger "Test.testcase3" 
+                   logIN $ ["Term 1 is ", skip (view t),"Term 2 is ", skip (view s) ]
+                   
+                   logIN $ ["Antiunifying Term1 and Term2"]
+                   ai <- antiunify [t,s]
+                   logIN $ ["Resulting antiinstance is ",(view ai)]  
+                   
+                   logIN $ ["Positions of Variable in Anitinstance"]
+                   let varpos = getVarPos ai
+                   logIN $ ["Variables at positions:",(show varpos)]
+                   
+                   return t
+                   
+testinit :: (ELog m) => Dec -> Dec -> m Dec
+testinit d1 d2 = do logIN $ ["Dec1 is ", skip (view d1),"Dec2 is ", skip (view d2) ]
+
+                    logIN $ ["Transforming Dec1 to FunDef"] 
+                    let fdef1 = toFunDef d1
+                    logIN $ ["Resulting FunDef is:", skip (show fdef1)]
+                    
+                    logIN $ ["Transforming Dec2 to FunDef"]
+                    let fdef2 = toFunDef d2
+                    logIN $ ["Resulting FunDef is:", skip (show fdef2)]
+                    return d1
+
+                   
+dotest  :: (Ppr t) => (t -> t -> IM t) -> (Q t) -> (Q t) -> IO ()
+dotest f t s = runQ $
+    do t1 <- t
+       t2 <- s 
+       let (r,l) = runIM $ f t1 t2
+       runIO $ putStrLn "*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*"
+       runIO $ putStrLn "|                                 Logging Result                                |"
+       runIO $ putStrLn "*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*"
+       runIO $ putStrLn (view l)
+       runIO $ putStrLn "*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*"
+       runIO $ putStrLn "|                              Computational Result                             |"
+       runIO $ putStrLn "*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*"
+       runIO $ either (putStrLn.view) (printQ.return) r
+              
+
+main = dotest testunify term7 term7v
+     
+   
hunk ./src/Test.lhs 1
-
+Hi Scott,
+
+I am using the PSQueue module, and I was puzzled by the behaviour of 'alter'.  Shouldn't it be the same behaviour than Data.Map.alter?
+
+Following some test code:
+
+> module Test where
+
+> import qualified Data.PSQueue as Q
+> import qualified Data.Map as M
+> import qualified Data.List as L
+
+> ins :: (Eq a) =>[a] -> Maybe [[a]] -> Maybe [[a]]
+> ins l Nothing   = Just $ [l]
+> ins l (Just ls) = Just $ l:ls
+
+> del :: (Eq a) => [a] -> Maybe [[a]] -> Maybe [[a]]
+> del l Nothing   = Nothing
+> del l (Just ls) = let postDel = L.delete l ls
+>                   in if length postDel > 0
+>                         then Just postDel
+>                         else Nothing
+
+> rep :: (Eq a) =>[a] -> [a] -> Maybe [[a]] -> Maybe [[a]]
+> rep l1 l2 v = ins l2 (del l1 v)
+
+> qins :: (Ord a, Show a) => [a] -> Q.PSQ Int [[a]] -> Q.PSQ Int [[a]]
+> qins = \l ls -> Q.alter (ins l) (length l) ls
+
+> mins :: (Ord a, Show a) => [a] -> M.Map Int [[a]] -> M.Map Int [[a]]
+> mins = \l ls -> M.alter (ins l) (length l) ls
+
+> qdel :: (Ord a, Show a) => [a] -> Q.PSQ Int [[a]] -> Q.PSQ Int [[a]]
+> qdel = \l ls -> Q.alter (del l) (length l) ls
+
+> mdel :: (Ord a, Show a) => [a] -> M.Map Int [[a]] -> M.Map Int [[a]]
+> mdel = \l ls -> M.alter (del l) (length l) ls
+
+> qrep :: (Ord a, Show a) => [a] -> [a] -> Q.PSQ Int [[a]] -> Q.PSQ Int [[a]]
+> qrep l1 l2 =  \ls -> qins l2 $qdel l1 ls
+
+> mrep :: (Ord a, Show a) => [a] -> [a] -> M.Map Int [[a]] -> M.Map Int [[a]]
+> mrep l1 l2 =  \ls -> mins l2 $mdel l1 ls
+
+> testm = mins "askfg" $ mins "a" $ mins "b" $ mins "asd" $ mins "ab" $ mins "agsdf" $ mins "as" M.empty
+> testq = qins "askfg" $ qins "a" $ qins "b" $ qins "asd" $ qins "ab" $ qins "agsdf" $ qins "as" Q.empty
+
+> testqrep = qrep "a" "bbbbbb" testq
+> testmrep = mrep "a" "bbbbbb" testm 
+ 
+IMHO, it needs to be checked, whether the keys were the same _and_ whether the result of 'f' was 'Nothing'. Otherwise, it cannot be used for insert, delete and update at the same time.
+
+I took the liberty to slightly change the code, but maybe I am wrong. 
+
+
+alter :: (Show p, Show k, Ord k, Ord p) => (Maybe p -> Maybe p) -> k -> PSQ k p -> PSQ k p
+alter f k q = 
+  case tourView q of
+    Null -> 
+      case f Nothing of
+        Nothing -> empty
+        Just p  -> singleton k p
+    Single k' p -> 
+      case f (if k==k' then Just p else Nothing) of
+        -- WAS: Nothing -> empty
+        Nothing -> if k==k'     
+                      then empty                        
+                      -- binding has been deleted
+                      else singleton k' p               
+                      -- key k not found, current binding left unchanged
+        -- WAS : Just p' -> singleton k p'              
+        Just p' -> if k==k'                             
+                      then singleton k p'               
+                      -- p has been altered to p'
+                      else insert k p' $ singleton k' p 
+                      -- new binding (k :-> p') inserted, current left unchanged
+    tl `Play` tr
+      | k <= maxKey tl -> alter f k tl `unsafePlay` tr
+      | otherwise      -> tl `unsafePlay` alter f k tr
+ 
+Nevertheless, thanks a lot for the implementation.
+
+Greetings, 
+
+
+Martin