[removed dead code
martin.hofmann@uni-bamberg.de**20091126143324] hunk ./src/Data/HypoSpace.hs 49
--- DEPRECATED
----- | return one of the best valued Hypotheses
---bestHypo :: HSpace -> Hypo
---bestHypo = head . snd . H.getMin . heap
---
---bestHypoBy :: HSpace -> (Hypos -> Hypo) -> Hypo
----- | find the best valued Hypothesis
---bestHypos :: HSpace -> Hypos
---bestHypos =  snd . H.getMin . heap
---
---
----- Replace a rule by many rules
---replaceHypos :: Hypo -> Hypos -> HSpace -> HSpace
---replaceHypos h hs hsp =  uncurry  pushHypos . swap . (repl h hs) . popHypos $ hsp
---    where
---    swap (a,b) = (b,a)
---    repl h hs = first $ ((F.toList hs) ++) . (delete h)
-
hunk ./src/Data/Hypotheses.hs 58
---instance Eq Hypo where
---    (==) a@(HH o1 c1 d1) b@(HH o2 c2 d2) =  and [o1 == o2, c1 == c2]
--- 
-
-        
-        
---instance Ord Hypo where
---    compare(HH o1 c1 _) (HH o2 c2 _) = compare (compare o1 o2)(compare c1 c2)
-
hunk ./src/Data/Hypotheses.hs 174
+
hunk ./src/Data/Hypotheses.hs 180
---instance Show Hypos where
---    show  = show.pretty
---instance Pretty Hypos where
---    pretty (HHs s) = pretty s    
---    
---singletonHs :: Hypo -> Hypos
---singletonHs h = HHs $ S.singleton h
---
---hypos :: [Hypo] -> Hypos
---hypos = S.fromList
-
-
---
-----hyposToSet = unHHs
---
---emptyHs :: Hypos
---emptyHs = HHs $ S.empty
---
---nullHs :: Hypos -> Bool   
---nullHs = S.null.unHHs  
---
---countHs :: Hypos -> Int
---countHs = S.size.unHHs
---
---foldHs :: (Hypo -> a -> a) -> a -> Hypos -> a
---foldHs f i rs = foldl' (flip f) i (hyposToList rs) -- S.fold f i (unHHs rs)
---
---mapHs :: (Ord a) => (Hypo -> a) -> Hypos -> (Set a)
---mapHs f hs  = (S.map f) (unHHs hs)
---
---mapHs' :: (Hypo -> Maybe Hypo) -> Hypos -> Hypos
---mapHs' f hs = 
---    case mapM f (hyposToList hs) of
---        Just l  -> HHs $ S.fromList l
---        Nothing -> emptyHs 
---
---        
---mergeHs :: Hypos -> Hypos -> Hypos
---mergeHs hs1 hs2 = HHs $ S.union (unHHs hs1) (unHHs hs2)
---
---insertHs :: Hypo -> Hypos -> Hypos  
---insertHs h hs = HHs $ S.insert  h (unHHs hs)
---
---mbInsertHs :: Hypo -> Maybe Hypos -> Maybe Hypos
---mbInsertHs h hs = 
---    case hs of
---        Just hs' -> return $ insertHs h hs'
---        Nothing  -> return $ singletonHs h
---        
---deleteHs :: Hypo -> Hypos -> Hypos
---deleteHs h hs = HHs $ S.delete h (unHHs hs)
---
---mbDeleteHs :: Hypo -> Maybe Hypos -> Maybe Hypos
---mbDeleteHs _ Nothing   = Nothing 
---mbDeleteHs h (Just hs) = 
---    let hs' =  deleteHs h hs
---    in if nullHs hs' 
---         then Nothing
---         else Just hs'
---               
---replaceHs :: Hypo -> Hypo -> Hypos -> Hypos
---replaceHs h1 h2 hs = insertHs h1 (deleteHs h2 hs)
---
---hyposToList :: Hypos -> [Hypo]
---hyposToList = S.toList.unHHs
--- 
-
-
hunk ./src/Syntax/Class/Antiunifier.hs 10
-    lggL, -- aunify2,
+    lggL,
hunk ./src/Syntax/Class/Antiunifier.hs 13
---    Antiunifiable (
---        antiunify,        -- :: (Antiunifiable k v t) => [t] -> t
---        antiunifyWithMap, -- ::  (Antiunifiable k v t) => (VarMap k v) -> [t] -> LM t
---        antiunify2,        -- :: (Antiunifiable k v t') => [[t]] -> [t'] -> LM ([t],t')
---        aunify
---      ),
---    computeAntiInstance, checkforAntiInstance,updateVarTable
---      
+
hunk ./src/Syntax/Class/Antiunifier.hs 72
---    
---bindVar :: VImg -> AU Type
---bindVar img =  getMap >>= (maybe (mkVar img) (return)) . (lookup img)
---     
---mkVar :: VImg -> AU Type
---mkVar vimg = do 
---    vnm <- getCnt >>= return . ('a':) . show
---    cxt <- lift $ cmpCxt vnm vimg
---    var <- return . (flip quantify cxt)  . mkVarT $ vnm
---    putImg var vimg
---    return var
---      
---cmpCxt :: String -> VImg -> C TyCxt
---cmpCxt vnm vimg = do 
---    insts <- allInstances
---    nms   <- mapM (collectPreds vnm insts) vimg
---    reduce . (foldl1 intersect) $ nms
---    
---collectPreds :: String -> [(Name,[Type])] -> Type -> C [Pred] 
---collectPreds vnm is (ForallT _ c (VarT _)) = mapM (\(AppT (ConT n) _) -> bySuper $ mkPred n vnm) c >>= return . concat 
---collectPreds vnm is (VarT _) = return . map ((flip mkPred vnm) . fst) $ is 
---collectPreds vnm is t =    
---    filterM ( (anyM (`matches` t)) . snd ) is >>=
---    return . map ((flip mkPred vnm) . fst)
---
---lgg :: [Type] -> C (Maybe Type)
---lgg ts = ( evalStateT (aunify ts) emptyVIMap >>= return . Just ) 
---            `catchError` \_ -> return Nothing
---   
---hRoot :: (Term t) => [t] -> ([t] -> t)
---hRoot = root . head 
---
---sameRoot :: (Term t) => [Type] -> Bool
---sameRoot []  = error "sameRoot: empty List"
---sameRoot [x] = True
---sameRoot (x1:x2:xs) = (&&) (sameSymAtRoot x1 x2) $! sameRoot (x2:xs)
--- 
-
-
-
-
-
-
-
-
-
-
-
-
-
-
----------------------------------------------------------------------
----------------------------------------------------------------------
---------------------------------------------------------------------
-
----------------------------------------------------------------------
----------------------------------------------------------------------
---------------------------------------------------------------------
hunk ./src/Syntax/Class/Antiunifier.hs 73
---
---{- | 
---     This is a many-to-one mapping to model generalisation from many terms to a 
---     variable (here its name). 
----}
---type VarMap t = (M.Map [t] Name)
---
---{- | 
---     The 'AU t' monad which is required for antiunification. It is just a state 
---     monad 'StateT' to keep track of the replacements in a 'VarMap t'. The type 
---     parameter is 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 t = StateT (VarMap t) m t
---
----- Shotcut to evaluate the 'AU' monad, yielding the result value
---evalAU :: (Monad m) => StateT s m a -> s -> m a
---evalAU = evalStateT
---
----- Shortcut to evaluate the 'AU' monad, yielding the result value and the result 
----- state
---runAU :: (Monad m) => StateT s m a -> s -> m (a, s)
---runAU  = runStateT
---
-----------------------------------------------------------------------------------
----- The Antiunifiable class definition  
-----------------------------------------------------------------------------------
---{-|
---    The class 'Antiunifiable' 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 ].
---        
----}      
---class (Term t) => Antiunifiable t where
---    -- | Computes the anti-instance 't' of all terms in '[t]'
---    antiunify        :: (Monad m) => [t] -> m t
---    antiunify         = (\t -> evalAU (aunify t) M.empty)
---        
---    -- | The actual state transforming function, doing the anti-unification and 
---    --   keeping track of the variables in the state.
---    aunify           :: (Antiunifiable t, Monad m) => [t] -> AU m t
---
----- DEAD CODE       
---    -- | Same as 'antiunify' but uses a 'VarMap' as initial state
---    antiunifyWithMap ::  (Antiunifiable t, Monad m) => (VarMap t) -> [t] -> m t
---    antiunifyWithMap  = (\m t -> evalAU (aunify t) m)
---    
----- DEAD CODE    
-----    {- | Convenience function to antiunify different kind of terms, but keeping 
-----         track of the VarMap. @antiunify2 t1 t2@ corresponds approcimately to 
-----         @liftM2 (,) (mapM antiunify t1) (antiunify t2)@, where the latter 
-----         antiunify uses the VarMap of the further. 
-----         This is needed to antiunify all patterns on the lhs and the rhs of 
-----         multiple rules.
-----    -}
---    antiunify2        :: (Ord t', Antiunifiable t', Antiunifiable t, Monad m) 
---                      => [[t]] -> [t'] -> (t -> t') -> m ([t],t')
---    antiunify2 ts ts' trans = do
---            (ait,varmap) <- runAU ((mapM aunify) ts) M.empty
---            ait'         <- antiunifyWithMap (M.mapKeys (map trans) varmap) ts'
---            return (ait,ait')   
---
-----------------------------------------------------------------------------------
----- The Antiunifiable 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??? NO, Dec, body etc are not terms!!
---
----}    
-----instance Antiunifiable 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 'Antiunifiable Exp Exp Dec', all other functions yield a 
-----   'fail'.   
-----    
------}        
-----instance Antiunifiable 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 Antiunifiable 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 computeAntiInstance lof
-----            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 Antiunifiable Exp Exp Rule where 
-----    toKey = 
-----        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
-----                "number of patterns in Rule!"
-----    fromVal = 
-----        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
-----                "number of patterns in Rule!"
-----    mkVar = 
-----        fail $ "Antiunifier.aunify: Cannot generalise over an arbitrary " ++
-----                "number of patterns in Rule!"
-----       
-----    aunify rules  = do
-----        let tlhss   = transpose $ map lhs rules
-----        let rhss    = map rhs rules
-----        (ailhs,varmap) <- lift $ runAU ((mapM aunify) tlhss) M.empty
-----        airhs         <- lift $ antiunifyWithMap varmap rhss
-----        return $ rule ailhs airhs                
---   
--- 
---   
---{-------------------------------------------------------------------------------
---  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 t, Antiunifiable t, Monad m) => [t] -> AU m t
----- checkforAntiInstance [x] = return x -- is implied when condition below is True
---checkforAntiInstance l@(x:xs) =   
---    if (all (== x) l) && not (any isWild l || all isVar l)
---    -- all terms are equal, but they are not all variables or one is a wildcard
---       then return x 
---       else computeAntiInstance l
---       -- If all terms are wildcards or variables, they are anti-unified 
---       -- nevertheless. This is necessary to bind wildcards by a variable in the
---       -- pattern, so also images with the same variable must occur in the 
---       -- table. Thus variables are renamed. 
---       -- Even, iff all are wildcards, there should never be a new and unbound 
---       -- variable introduced for them, because there should always be some 
---       -- pattern which binds the wildcard. Hopefully! 
---
---{-|
---   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 t, Antiunifiable t, Monad m) => [t] -> AU m t
---computeAntiInstance l@(x:xs) =  do 
-----    lift (setCurrentLogger "Terms.Antiunifier.computeAntiInstance")
-----    llogEnterDE
-----    llogDE $ text "Term Image is:" <> pretty l
---    table <- get
-----    llogDE $ text "Current varTable is:" <> pretty table
-----    llogDE $ text "isIn?" <+> (pretty $ M.member l table)
-----    llogDE $ text "isIn?" <+> (pretty $ lookup l (M.toList table))
-----    llogDE $ text "map (==)?" <+> (pretty $ map (\ll -> l ==(fst ll)) (M.toList table))
---    (newTable, var) <- return $ updateVarTable table l
-----    llogDE $ text "update varTable with var:" <> pretty var
-----    llogDE $ text "Updated varTable is:" <> pretty 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 t, Antiunifiable t) => (VarMap t) -> [t] -> ((VarMap t) , t)
---updateVarTable table img = 
---    case lookup img (M.toList table) of
---    -- This is a hack!! Damn! Wildcards equal everything, this messes up the 
---    -- retrieval! So I look up in the list, which is searched linear.
---        (Just v)    -> (table, toVar (head img) v)
---        Nothing     -> let name   = mkName ("x" ++ (show $ toInteger(M.size table)))
---                           newval = toVar (head img) name
---                       in (M.insert img name table , newval)
---
---                                  
---   