[ Introducing subfunction
martin.hofmann@uni-bamberg.de**20090218122713] hunk ./src/Data/IOData.hs 5
-    isOpen,
+    isOpen, isClosed, modifyFrag,
hunk ./src/Data/IOData.hs 9
-    IOData, initIOData, getAll, breakup, fuse --, getSpecifics--, coverAll, coverRules 
+    IOData, initIOData, getAll, breakup, fuse, insertRules 
hunk ./src/Data/IOData.hs 11
-    
hunk ./src/Data/IOData.hs 13
-
---import Data.Rules (Rules, Rule, rulesToList, RHS, LHS, rhs, lhs)
---import qualified Data.Hypotheses as H
hunk ./src/Data/IOData.hs 16
---import Terms
---import Terms.Antiunifier
hunk ./src/Data/IOData.hs 19
+import Data.List (intersect)
+
+import Data.Maybe (listToMaybe)
+
hunk ./src/Data/IOData.hs 34
---------------------------------------------------------------------------------
--- Datatype RuleFragment
---------------------------------------------------------------------------------
-
--- | An open position is defined by an expression (which should be a variable)
---   and a list of 'Position's in a term, which are open. 
---   This only makes sense in combination with a 'Rule'
-
-
--- 
--- Encapsulating all information of an open/unfinished Rule
-data RuleFrag = RF
-    { name  :: !Name      -- ^ the name of the function/rule
-    , frag  :: !Rule      -- ^ the rule itself
-    , covr  :: ![Int]     -- ^ the indices of covered I/O examples (stored in a IOData)
-    , opos  :: ![OpenPos] -- ^ the open positions of this fragment    
-    }
-    deriving(Eq, Ord)
-  
-instance Show RuleFrag where
-	show (RF n f c _) =
-		(shows n) . (shows f) . (showString " ") $ show c
-instance Pretty RuleFrag where
-	pretty = text.show
-    
-type RuleFrags = Set RuleFrag
-    
- -- | A rule is open if it is not closed
-isOpen :: RuleFrag -> Bool
-isOpen = not.isClosed
-
--- | A rule is closed if it does not have any open positions
-isClosed = null.opos
-
-
-    
---------------------------------------------------------------------------------
--- Datatype RuleFragment
---------------------------------------------------------------------------------
-
+import Data.Function
hunk ./src/Data/IOData.hs 42
-    { evidence  :: !(Bimap Name Rules)
+    { evidence  :: !(Map Name Rules)
hunk ./src/Data/IOData.hs 49
--- | /O(1)/creates an empty IOdata value
-emptyIOData :: IOData
-emptyIOData = IOD
-    { evidence  = B.empty
-    , rhsides   = M.empty
-    , lhsides   = M.empty
-    , functions = B.empty
-    }
+--------------------------------------------------------------------------------
+-- Creating and Modifying IOData
+--------------------------------------------------------------------------------
hunk ./src/Data/IOData.hs 58
+-- PUBLIC
hunk ./src/Data/IOData.hs 62
+-- | /O(1)/creates an empty IOdata value
+-- PRIVATE
+emptyIOData :: IOData
+emptyIOData = IOD
+    { evidence  = M.empty
+    , rhsides   = M.empty
+    , lhsides   = M.empty
+    , functions = B.empty
+    }
+
hunk ./src/Data/IOData.hs 73
- | /O(log n)/ Insert the rules associated with the Name into the IOData, but 
-   only if neither is already in IOData. 
+ | /O(log n)/ Insert the rules associated with the Name into the IOData. If Name 
+   is already present in the map, the associated Rules is replaced with the 
+   supplied ones. 
hunk ./src/Data/IOData.hs 79
-    iod{ evidence =  B.tryInsert n rs bk}
+    iod{ evidence =  M.insert n rs bk}
hunk ./src/Data/IOData.hs 88
-insert :: Rules -> IOData -> (Name,IOData)
-insert rs iod@(IOD{ evidence = bk }) =
-    case B.lookupR rs bk of
-        Just n  -> (n,iod)
-        Nothing -> (n',iod')
+insertRules :: Rules -> IOData -> (Bool,Name,IOData)
+insertRules rs iod@(IOD{ evidence = bk }) = (True,n',iod')
+--    case moreGeneralSuperset rs iod of
+--        Just n       -> (False,n,iod)
+--        Nothing      -> (True,n',iod')
hunk ./src/Data/IOData.hs 94
-    n' = mkName $ (++) "fun" $ show $ B.size bk
+    n' = mkName $ (++) "fun" $ show $ M.size bk
hunk ./src/Data/IOData.hs 100
+
hunk ./src/Data/IOData.hs 103
+-- PUBLIC
hunk ./src/Data/IOData.hs 126
- 
-breakup :: IOData -> RuleFrag -> [RuleFrag]
-breakup iod rf = getSpecifics (name rf) iod (covr rf)
+
+-- |Access 'Rules' in the background knowledge by the 'Name' of a function
+-- PRIVATE        
+lookupByName :: (Monad m) => Name -> IOData -> m Rules
+lookupByName n b = M.lookup n $ evidence b 
+
+
+moreGeneralSuperset :: Rules -> IOData -> Maybe Name
+moreGeneralSuperset rs iod = 
+        listToMaybe $ map fst $ filter (( flip subsumesAll rs).snd)  (M.toList.evidence $ iod ) 
+       
+--------------------------------------------------------------------------------
+-- Modify RuleFrags       
+--------------------------------------------------------------------------------
+breakup :: RuleFrag -> IOData -> [RuleFrag]
+breakup rf iod = getSpecifics (name rf) iod (covr rf)
hunk ./src/Data/IOData.hs 154
-        
-
--- |Access 'Rules' in the background knowledge by the 'Name' of a function        
-lookupByName :: (Monad m) => Name -> IOData -> m Rules
-lookupByName n b = B.lookup n $ evidence b 
-
--- |Access the 'Name' of a function in the background knowledge by its 'Rules'
-lookupByRules :: (Monad m) => Rules -> IOData -> m Name
-lookupByRules rs b = B.lookupR rs $ evidence b 
-
-       
-
hunk ./src/Data/IOData.hs 173
-    iod{evidence = B.insert n rs evi} 
+    iod{evidence = M.insert n rs evi} 
hunk ./src/Data/IOData.hs 190
- 
+--------------------------------------------------------------------------------
+-- Datatype RuleFragment
+--------------------------------------------------------------------------------
+
+-- Encapsulating all information of an open/unfinished Rule
+data RuleFrag = RF
+    { name  :: !Name      -- ^ the name of the function/rule
+    , frag  :: !Rule      -- ^ the rule itself
+    , covr  :: ![Int]     -- ^ the indices of covered I/O examples (stored in a IOData)
+    , opos  :: ![OpenPos] -- ^ the open positions of this fragment    
+    }
+    deriving(Show, Eq, Ord)
+    
+type RuleFrags = Set RuleFrag
hunk ./src/Data/IOData.hs 205
+ -- | A rule is open if it is not closed
+isOpen :: RuleFrag -> Bool
+isOpen = not.isClosed
+
+-- | A rule is closed if it does not have any open positions
+isClosed = null.opos
+
+-- | Applies the given function to the 'Rule'-part of a 'RuleFrag', and updates 
+--   the open positions, which might have been changed
+modifyFrag :: RuleFrag -> (Rule -> Rule) -> RuleFrag
+modifyFrag rf@(RF _ f _ o ) g = rf{frag= g f, opos= openPositions (g f)}
+ 
+--------------------------------------------------------------------------------
+-- Class Instances
+--------------------------------------------------------------------------------
+   
+-- Pretty
+--
+            
+instance Pretty IOData where
+        pretty iod = text "IODATA" <$> 
+                     parens ( indent 2 $ 
+                        text "Evidence :" <$> pretty (evidence iod) <$>
+                        text "Functions:" <$> pretty (functions  iod))
+                        
+instance Pretty RuleFrag where
+    pretty  (RF n f c _) = pretty n <+> pretty f <+> text "^" <>  (text $show c)
hunk ./src/Data/IgorMonad.hs 9
-    tick, loopCount, hypoCount,
+    tick, loopCount, hypoCount, addIO, breakupM, fuseM, coverAll,
hunk ./src/Data/IgorMonad.hs 12
-    module Data.HypoSpace
+  --  module Data.HypoSpace
+    module Data.Hypotheses
+    
hunk ./src/Data/IgorMonad.hs 23
-import Data.HypoSpace 
+import Data.HypoSpace
+ 
+import Data.Hypotheses
hunk ./src/Data/IgorMonad.hs 29
+ 
+data Igor = Igor 
+    { iodata :: !IOData, searchSpace :: !HSpace, loopcount :: [(Name,Int)]}
+    deriving (Show)
hunk ./src/Data/IgorMonad.hs 40
+--------------------------------------------------------------------------------
+-- Monadic operations on 'Igor'
+--------------------------------------------------------------------------------
hunk ./src/Data/IgorMonad.hs 46
-    let igor' = setupTarget igor n
+    let igor' = setupTarget n igor
hunk ./src/Data/IgorMonad.hs 51
+--------------------------------------------------------------------------------
+-- Monadic operations on the SearchSpace
+--------------------------------------------------------------------------------
hunk ./src/Data/IgorMonad.hs 57
-getEvidence :: IM IOData
-getEvidence = gets iodata
-
hunk ./src/Data/IgorMonad.hs 60
+--------------------------------------------------------------------------------
+-- Monadic operations on IOData
+--------------------------------------------------------------------------------
+getEvidence :: IM IOData
+getEvidence = gets iodata
hunk ./src/Data/IgorMonad.hs 67
-tick = modify incrLCount
-
+tick = get >>= \i@(Igor _ _ ((n,lc):lcs)) ->
+          put i{loopcount = (n,lc+1):lcs}
+    
+propagate :: RuleFrag -> [(RuleFrags,[Call])] -> IM ()  
+propagate rf adv = get >>= \igor@(Igor _ sp _) ->
+                    put $ igor{searchSpace = (propagateHSp rf adv sp)}
+    
hunk ./src/Data/IgorMonad.hs 79
- 
-data Igor = Igor 
-    { iodata :: !IOData, searchSpace :: !HSpace, loopcount :: [(Name,Int)]}
-    deriving (Show)
-    
-instance Pretty Igor where
-	pretty = text.show
+
+addIO :: Rules -> IM (Bool,Name)
+addIO rs = do
+    i@(Igor iod _ _) <- get
+    let (b,n,iod') = insertRules rs iod
+    put i{iodata = iod'}
+    return (b,n)
hunk ./src/Data/IgorMonad.hs 87
+breakupM :: RuleFrag -> IM [RuleFrag]
+breakupM rf = gets iodata >>= return . (breakup rf)
+
+fuseM :: [RuleFrag] -> IM RuleFrag  
+fuseM = return . fuse
+
+coverAll :: Name -> IM RuleFrag
+coverAll n = gets iodata >>= return.getAll n >>= fuseM
+
+
+--------------------------------------------------------------------------------
+-- Non-Monadic operations on 'Igor'
+--------------------------------------------------------------------------------
+
hunk ./src/Data/IgorMonad.hs 103
-setupTarget :: Igor -> Name -> Igor
-setupTarget ( Igor iod _ lc) n  = Igor iod (initHSpace (fuse (getAll n iod))) ((n,0):lc) 
+setupTarget :: Name -> Igor -> Igor
+setupTarget n ( Igor iod _ lc) = 
+    Igor iod (initHSpace (fuse . (getAll n) $ iod)) ((n,0):lc)  
+    
+
+
+
hunk ./src/Data/IgorMonad.hs 116
- 
-    
-propagate :: RuleFrag -> [(RuleFrags,[Call])] -> Igor -> Igor   
-propagate rf adv (Igor iod sp lc) = Igor iod (propagateHSp rf adv sp) lc
hunk ./src/Data/IgorMonad.hs 118
--- Bookkeeping: Increment the loop counter
-incrLCount :: Igor -> Igor
-incrLCount i@(Igor _ _ ((n,lc):lcs)) =
-    i{loopcount = (n,lc+1):lcs}
-      
+
+--------------------------------------------------------------------------------
+-- Instamnce declarations
+--------------------------------------------------------------------------------          
+instance Pretty Igor where
+    pretty i = text "IGOR" <$> 
+               parens ( indent 2 $ 
+                        pretty (iodata i) <$>
+                        pretty (searchSpace  i)<$>
+                        text "LOOPCOUNT: " <$> pretty (loopcount i))
+    
hunk ./src/Data/Rules.hs 9
-    Rules, rules,
+    Rules, rules, subrule, insertCall, subsumesAll,
hunk ./src/Data/Rules.hs 14
-    --module Terms.Class    
+    module Terms.Class,    
+    module Terms.Unifier    
hunk ./src/Data/Rules.hs 36
+
hunk ./src/Data/Rules.hs 46
-
hunk ./src/Data/Rules.hs 47
-data Rule = R {lhs :: LHS, rhs :: RHS} deriving(Ord)
+data Rule = R {lhs :: LHS, rhs :: RHS} deriving(Ord, Show)
hunk ./src/Data/Rules.hs 51
-
+    
hunk ./src/Data/Rules.hs 63
+-- | An open position is defined by an expression (which should be a variable)
+--   and a list of 'Position's in a term, which are open. 
+--   This only makes sense in combination with a 'Rule'
hunk ./src/Data/Rules.hs 96
+subrule :: RulePos -> Rule -> Maybe Rule
+subrule (Body p)  (R l r) = liftM2 R (Just l) (subtermAt r p)
+subrule (Arg i p) (R l r) = liftM2 newrule (subtermAt (l!!i) p) (Just r)
+    where 
+    newrule l r = R [l] r 
hunk ./src/Data/Rules.hs 102
+replaceInLhs :: Rule -> RulePos -> Pat -> Rule
+replaceInLhs r (Arg i pos) t = 
+    let (pb,(p:pa)) = splitAt i (lhs r)
+    in r{lhs= concat [pb, [(substitute t pos p)],pa]}
+
+replaceInRhs :: Rule -> RulePos -> Exp -> Rule
+replaceInRhs r (Body pos) t = 
+    let rs = rhs r
+    in r{rhs= (substitute t pos rs)}
+
+insertCall :: RulePos -> Name -> Rule -> Rule
+insertCall p n r = replaceInRhs r p (pat2Call n (lhs r)) 
+    
hunk ./src/Data/Rules.hs 148
+isMoreSpecific :: Rule -> Rule -> Bool
+isMoreSpecific a b = (&&) (matchLhss a b) (matchRhs a b)
+
+isMoreGeneral :: Rule -> Rule -> Bool
+isMoreGeneral = flip isMoreSpecific
+
hunk ./src/Data/Rules.hs 159
-             
--- *FIXME* necessary?    
-instance Show Rule where
-    show (R ls rs) = show ls ++ "=" ++ show rs
hunk ./src/Data/Rules.hs 160
-instance Pretty Rule where
-	pretty = text.show    
- 
+subsumeLhss :: Rule -> Rule -> Bool
+subsumeLhss = flip matchLhss
hunk ./src/Data/Rules.hs 163
+subsumeRhs :: Rule -> Rule -> Bool
+subsumeRhs = flip matchRhs
+
+instance Pretty Rule where
+	pretty r = text.pprint $ Clause (lhs r) (NormalB $ rhs r) []
+    -- Need the TH.PprLib to get the correct variable names on lhs and rhs
+  
hunk ./src/Data/Rules.hs 197
-     
hunk ./src/Data/Rules.hs 198
+subsumesAll :: Rules -> Rules -> Bool
+subsumesAll r1 r2 = 
+       trace ("DEBUG :" ++ (show.pretty $ r1) ++ " subsumes all " ++ (show.pretty $ r2) ++ "?" ++ (show (all (anySubsumes r1) (S.toAscList r2))))$
+       all (anySubsumes r1) (S.toAscList r2) 
+    
+anySubsumes :: Rules -> Rule -> Bool
+anySubsumes rs r = 
+        any (isMoreSpecific r) (S.toAscList rs)