[many bugfixes, Igor returns at least the correct hypo (amongst others)
martin.hofmann@uni-bamberg.de**20090513065143] hunk ./src/Data/IOData.hs 15
+import Syntax.Terms (subterms)
+
hunk ./src/Data/IgorMonad.hs 8
-    setTarget, currentBestHypos, getEvidence, getSearchSpace, 
+    setTarget, getTarget, currentBestHypos, getEvidence, getSearchSpace, 
hunk ./src/Data/IgorMonad.hs 47
-    llogIN $ text "Target set, IGOR initialised to:"
-    llogIN $ indent 2 (pretty igor')
hunk ./src/Data/IgorMonad.hs 49
+getTarget :: IM Name
+getTarget = gets $ fst.head.loopcount
hunk ./src/Data/Rules.hs 24
-import Data.List (foldl', transpose, (\\), nub)
+import Data.List (foldl', transpose, (\\), nub, sort)
hunk ./src/Data/Rules.hs 231
-hypos2decs hs =  map rules2decs hs
+hypos2decs hs =  map (sort.rules2decs) hs
hunk ./src/Data/Rules.hs 240
-rules2clauses rs = map rule2clause (S.toList rs)
+rules2clauses rs = map rule2clause (reverse.S.toAscList $ rs)
hunk ./src/Logging/Logger.hs 6
-    Log, Logger, Message, Priority(..),
+    Log, Logger, Message, Priority(..), emptyLog,
hunk ./src/Logging/Logger.hs 44
--- if set, all ogging is directly dumped to stdout via 'trace'
+-- if set, all olgging is directly dumped to stdout via 'trace'
hunk ./src/Logging/Logger.hs 77
+emptyLog = Log [] Nothing
hunk ./src/Logging/PrettyPrinter.hs 100
+instance (Pretty a, Pretty b) => Pretty (Either a b) where
+    pretty (Left a) = pretty a
+    pretty (Right a) = pretty a
hunk ./src/Logging/PrettyPrinter.hs 145
-        | otherwise = text "Cannot print a TimeDuff with Month or Year field set"
+        | otherwise = text "Cannot print a TimeDiff with Month or Year field set"
hunk ./src/Rating/Rateable.hs 19
-type RatingData = Int   
+type RatingData = (Int,Int, Int)   
hunk ./src/Rating/Rateable.hs 39
-    rate h       =  numberOfPartitions h
+    rate h       = ( numberOfPartitions h
+                   , numberOfOpenRules h
+                   , numberOfTotalRules h)
hunk ./src/Rating/Rateable.hs 44
-numberOfOpenRules :: Hypo -> RatingData                 
+numberOfOpenRules :: Hypo -> Int                 
hunk ./src/Rating/Rateable.hs 48
-numberOfTotalRules :: Hypo -> RatingData 
+numberOfTotalRules :: Hypo -> Int 
hunk ./src/Rating/Rateable.hs 51
-numberOfPartitions :: Hypo -> RatingData
+numberOfPartitions :: Hypo -> Int
hunk ./src/RuleDevelopment/Matching.hs 7
-import Data.Maybe (catMaybes)
+import Data.Maybe (catMaybes, isJust)
hunk ./src/RuleDevelopment/Matching.hs 24
+    
+    let subcalls    = allowedMaxCall (name cr) cd
+    let bckgcalls i = map (flip (,) (Just GT)) (background i)
+    let selfcall    = (name cr, Just LT)
+    let allowdCs i  =  M.toList $ foldl (flip $ uncurry M.insert) subcalls ((bckgcalls i)++[selfcall])
+    
hunk ./src/RuleDevelopment/Matching.hs 35
-    where
-    subcalls    = allowedMaxCall (name cr) cd
-    bckgcalls i =  map (flip (,) (Just GT)) (background i)
-    allowdCs i  =  M.toList $ foldl (flip $ uncurry M.insert) subcalls (bckgcalls i)
hunk ./src/RuleDevelopment/Matching.hs 38
-    llogIN ( text "* Not allowed to call" <+> (text.show $ n)) >> 
+    llogIN (indent 2 $ text "- Not allowed to call" <+> (text.show $ n)) >> 
hunk ./src/RuleDevelopment/Matching.hs 41
-     tgtrs  <- breakupM $ cr
-     cllrs  <- liftM (getAll n) getEvidence
-     cllios <- (do { r <- (liftM oneFromEachCol $ makeIOMatrix tgtrs o cllrs) 
-                  ; (llogIN ( text "* Make call to" <+> (text.show $ n))) 
-                  ;  return r}) 
-                `catchError` 
-                (\msg -> llogIN ( text "* Not able to call" <+> 
-                                      (text.show $ n) <+>
-                                      text "because of" <+> text msg) >> 
-                             return [])     
-     mapM (makeCall cr n) $ cllios
+     cllrs  <- breakupM $ cr
+     tgtrs  <- liftM (getAll n) getEvidence
+     llogIN (text "Matching (target,caller)" <$> pretty (tgtrs,cllrs))
+     ios <-  makeIOMatrix tgtrs o cllrs  
+     llogIN (text "Matchings" <$> (pretty ios))
+     if any null ios then llogIN (text "Insufficient matching! At least one argument didn't match at all!") >> return []
+       else mapM (makeCall cr n) $ (oneFromEachCol ios)
hunk ./src/RuleDevelopment/Matching.hs 76
-    sequence [ liftM catMaybes $ sequence $ [abduceIO t o c | t <- tgtrs] | c <- cllrs ]
+    sequence [ liftM catMaybes $ sequence $ [abduceIO t o c | t <- tgtrs ] | c <- cllrs] 
hunk ./src/RuleDevelopment/Matching.hs 86
-abduceIO tgt o cll = do
-    let callrel = on compare (lhs.crul) tgt cll 
-    if o < callrel then return Nothing
-    -- check whether matching is allowed
-      else do s <- lift $ on matchesWithSubs (rhs.crul) tgt cll
+abduceIO tgt maxcallrel cll = do
+    let callrel = on compare (lhs.crul) tgt cll
+    if maxcallrel < callrel then 
+              llogIN (text "Discarded Match" <+> pretty tgt <+> text (show callrel) <+>
+                      pretty cll <+> text "not allowed" <+> text (show callrel)) >> 
+              return Nothing
+    -- check whether matching is allowed, not allowed if maxcallrel < callrel
+      else do s <- lift $ (liftM Just $ on (matchesWithSubs) (rhs.crul) tgt cll) `catchError`
+                          (\_ -> return Nothing)
hunk ./src/RuleDevelopment/Matching.hs 96
-              let cllvars = (concatMap getVars (lhs.crul $ cll))
-              let unaffectedvars = cllvars \\ (map fst s)
-              let s' = s ++ [ v <~ (TWildE n t) | v@(TVarE n t) <- unaffectedvars]
-              -- replace all vars not in the substitution by wildcards 
-              let lhss' = lhs.crul $ cll
-              rhss' <- lift $ mapM (apply s') (lhs.crul $ tgt)  
-              -- new rhss are the substituted lhss of tgt
-              return.Just $ (callrel, map (rule lhss') rhss')
+              llogIN (text "Try Match      " <+> pretty tgt <+> text (show callrel) <+>
+                      pretty cll <+> text "allowed" <+> text (show maxcallrel) <+> text "Match?" <+> (bool $ isJust s)) 
+              case s of
+               Nothing  -> return Nothing
+               (Just s) -> do let cllvars = (concatMap getVars (lhs.crul $ cll))
+                              let unaffectedvars = cllvars \\ (map fst s)
+                              let s' = s ++ [ v <~ (TWildE n t) | v@(TVarE n t) <- unaffectedvars]
+                              -- replace all vars not in the substitution by wildcards 
+                              let lhss' = lhs.crul $ cll
+                              rhss' <- lift $ mapM (apply s') (lhs.crul $ tgt)  
+                              -- new rhss are the substituted lhss of tgt
+                              return.Just $  (callrel, map (rule lhss') rhss')
hunk ./src/RuleDevelopment/Subfunction.hs 27
-    let novarpos = posOfNoVarSubts cr
+    let novarpos = posOfVarSubts cr
hunk ./src/RuleDevelopment/Subfunction.hs 48
-    posOfNoVarSubts = fst.unzip.filterNoVars.label.subterms.rhs.crul 
+    posOfVarSubts = fst.unzip.filterNoVars.label.subterms.rhs.crul 
hunk ./src/Syntax/Antiunifier.hs 22
+import Data.Function (on)
hunk ./src/Syntax/Antiunifier.hs 200
---        case collectSubtermsB l of
+--        case collectSubtermsB l computeAntiInstance lof
hunk ./src/Syntax/Antiunifier.hs 290
+--    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))
hunk ./src/Syntax/Antiunifier.hs 305
-updateVarTable table img = 
-    case M.lookup img table of
+updateVarTable table img =
+    case lookup img (M.toList table) of
hunk ./src/Syntax/Expressions.hs 186
-    root (TListE (l:ls) t)                  = \(l:ls) -> trace ("ROOT at LIST" ++ (show.pretty $ (l:ls)))$ TListE (l:ls) t 
+    root (TListE (l:ls) t)                  = \(l:ls) -> TListE (l:ls) t 
hunk ./src/Syntax/Expressions.hs 228
-        if  i1 == i2 then return () else matchVar s t
+       -- if  i1 == i2 then return () else matchVar s t
+        matchVar s t
hunk ./src/Syntax/Expressions.hs 410
---                llogDE (text "Subterms are :" <> pretty 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 the rest lists
-                    straight = takeWhile (\l -> length l == len) subterms 
-                    ragged   = dropWhile (\l -> length l == len) subterms 
-                straightai <- mapM aunify straight
---                llogDE (text "Antinunified subterms (straight) are :" <> pretty straightai) 
-                if (null ragged) then return $ TListE straightai ty
-                 -- check if we have ragged list at allm and if so we can keep the f***ing ListE
-                  else do raggedai <- computeAntiInstance $ map (flip TListE ty) ragged
-                          -- convert back to lists, to get correct variable image
-                          if (null straight) then return raggedai
-                            else do
-                              -- iff there are straight, we add them in 'cons' style 
-    --                          llogDE $ text "List have different length"
-    --                          llogDE $ text "Antinunified subterms (ragged) are :" <> pretty straightai
-                                let tcone = TConE '(:) (mkArrowT [ety, ty, ty]) 
-                                let sections = map (mkTInfixE tcone) straightai
-                                return $ foldTInfixE sections raggedai
+                ai <- mapM aunify subterms
+                if(all null subterms) 
+                  then return $ TListE [] ty
+                  else case ai of
+                        [e,TListE l ty] -> return $ TListE (e:l) ty
+                        _owise          -> do 
+                            let tcone = TConE (mkName ":") (mkArrowT [ety, ty, ty]) 
+                            return $ mkTInfixE tcone (head ai) (last ai)
+----                llogDE (text "Subterms are :" <> pretty 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 the rest lists
+--                    straight = takeWhile (\l -> length l == len) subterms 
+--                    ragged   = dropWhile (\l -> length l == len) subterms 
+--                straightai <- mapM aunify straight
+----                llogDE (text "Antinunified subterms (straight) are :" <> pretty straightai) 
+--                if (null ragged) then return $ TListE straightai ty
+--                 -- check if we have ragged list at allm and if so we can keep the f***ing ListE
+--                  else do raggedai <- computeAntiInstance $ map (flip TListE ty) ragged
+--                          -- convert back to lists, to get correct variable image
+--                          if (null straight) then return raggedai
+--                            else do
+--                              -- iff there are straight, we add them in 'cons' style 
+--    --                          llogDE $ text "List have different length"
+--    --                          llogDE $ text "Antinunified subterms (ragged) are :" <> pretty straightai
+--                                let tcone = TConE '(:) (mkArrowT [ety, ty, ty]) 
+--                                let sections = map (mkTInfixE tcone) straightai
+--                                return $ foldTInfixE sections raggedai
hunk ./src/Syntax/Expressions.hs 454
-    aunify l@((TInfixE _ _ _ ty):xs) =
+    aunify l@((TInfixE _ c _ ty):xs) =
hunk ./src/Syntax/Expressions.hs 457
-                fstai <- aunify (subterms !! 0)
-                sndai <- aunify (subterms !! 1)
-                thrai <- aunify (subterms !! 2)
+                lai <- aunify (subterms !! 0)
+                rai <- aunify (subterms !! 1)
hunk ./src/Syntax/Expressions.hs 464
-                return $ TInfixE fstai sndai thrai ty
+                return $ TInfixE lai c rai ty
hunk ./src/Syntax/Expressions.hs 532
-        
+--    collectSubterms pivot t = 
+--        if sameSymAtRoot pivot t then checkSame pivot t >> return $ subterms t
+--           else fail ""
+--        
hunk ./src/Syntax/Expressions.hs 540
-        checkSame s t >> return [e1,e2]      
-    collectSubterms s@(TListE _ _) t@(TListE l _) = 
-        checkSame s t >> return l      
+        checkSame s t >> return [e1,e2] 
+    collectSubterms s@(TListE [] _) t@(TListE [] _) = 
+        checkSame s t >> return []     
+    collectSubterms s@(TListE (x:xs) _) t@(TListE (l:ls) ty) = 
+        checkSame s t >> return [l, TListE ls ty]      
+--    collectSubterms s@(TListE _ _) t@(TListE l _) = 
+--        checkSame s t >> return l      
hunk ./src/Syntax/Unifier.hs 71
-              setCurrentLogger "Terms.Unifier.mgu" >>
-              logDE (text "Unifying terms:" <+> pretty x <+> pretty y) >> 
+--              setCurrentLogger "Terms.Unifier.mgu" >>
+--              logDE (text "Unifying terms:" <+> pretty x <+> pretty y) >> 
hunk ./src/Syntax/Unifier.hs 106
-            llogDE ( text "Found (Var <~ Val) in current unifier:" <^>
-                     pretty var <+> text " <~ " <+> pretty val <$>
-                     text "but need to match:" <^>
-                     pretty var <+> text " <~ " <+> pretty t
-                   )
-            >> flush "No Match!"
+--            llogDE ( text "Found (Var <~ Val) in current unifier:" <^>
+--                     pretty var <+> text " <~ " <+> pretty val <$>
+--                     text "but need to match:" <^>
+--                     pretty var <+> text " <~ " <+> pretty t
+--                   ) >>
+            flush "No Match!"
hunk ./src/Syntax/Unifier.hs 118
-       lift $ setCurrentLogger "Terms.Unifier.unifyVar"
-       llogEnterDE
-       llogDE ( text "Var is:" <^> (pretty var) <$>
-                text "X is:" <^> (pretty x) <$>
-                text "Current unifier is:" <^> pretty unifier
-              ) 
+--       lift $ setCurrentLogger "Terms.Unifier.unifyVar"
+--       llogEnterDE
+--       llogDE ( text "Var is:" <^> (pretty var) <$>
+--                text "X is:" <^> (pretty x) <$>
+--                text "Current unifier is:" <^> pretty unifier
+--              ) 
hunk ./src/SynthesisEngine.hs 4
-
+import Data.Function (on)
+import Data.List (minimumBy)
hunk ./src/SynthesisEngine.hs 12
+import Control.Monad.Error
hunk ./src/SynthesisEngine.hs 21
-
-_MaxLoopCount = 50
+-- stop after @_MaxLoopCount@ iterations, if < 0 loop count has no effect.
+_MaxLoopCount = 20
hunk ./src/SynthesisEngine.hs 38
-    let allrs    =  (++) tgts bgks 
+    let allrs    =  (++) tgts bgks
hunk ./src/SynthesisEngine.hs 40
-    result <- runIM ( synthesiseTargets tnms) igordata 
+    
+    logIN (text "SYNTHESISING" <+> hsep (map (squotes.pretty) tnms) <$>
+           text "USING       " <+> hsep (map (squotes.pretty.fst) bgks) <$> 
+           linebreak <>
+           text "IGOR initialised to:" <$>
+           indent 2 (pretty igordata))
+           
+    result <- (runIM ( synthesiseTargets tnms) igordata)
hunk ./src/SynthesisEngine.hs 73
+
hunk ./src/SynthesisEngine.hs 90
-    (dependencies,candidaterules) <- chooseCandidateRules candidatehypos
-    
-    llogIN $ text "Candidate Hypos:" <^> pretty candidatehypos
-    llogIN $ text "Candidate Rules:" <^> pretty candidaterules
-    
+    candidaterules <- chooseCandidateRules candidatehypos 
+       
hunk ./src/SynthesisEngine.hs 94
-    
-    llogIN $ text "Stopping Criteria?" <^>
+
+    --llogIN $ text "Candidate Hypos:" <^> pretty candidatehypos
+    llogIN $ text "Candidate Rules:" <^> pretty candidaterules <$>  
+             text "Candidate Hyposs:" <^> pretty candidatehypos <$>  
+             text "Stopping Criteria?" <^>
hunk ./src/SynthesisEngine.hs 100
-             text "Max Loopcount    :" <+> bool maxloopcount 
-                                
-    
-    candidaterule  <- chooseOneRule candidaterules
-    if nocandidates || maxloopcount
+             text "Max Loopcount    :" <+> bool maxloopcount   
+ 
+    if nocandidates  || maxloopcount
hunk ./src/SynthesisEngine.hs 104
-      else applyAdvacements dependencies candidaterule >>  enterLoop
+      else chooseOneRule candidaterules >>=
+           uncurry applyAdvacements >> 
+           enterLoop
+      
hunk ./src/SynthesisEngine.hs 112
+       lc <- loopCount
+       llogIN $ text "Stopping after" <+> int lc <+> text "loops."
hunk ./src/SynthesisEngine.hs 116
-stopWhenNoCandidateRules :: CovrRules -> IM Bool
-stopWhenNoCandidateRules = return . S.null
+stopWhenNoCandidateRules :: [(CallDep,CovrRule)] -> IM Bool
+stopWhenNoCandidateRules = return . null
hunk ./src/SynthesisEngine.hs 120
-stopAtMaxLoopCount = liftM2 (==) loopCount (return _MaxLoopCount)
+stopAtMaxLoopCount = 
+    if _MaxLoopCount < 0 then return False
+      else liftM2 (==) loopCount (return _MaxLoopCount)
hunk ./src/SynthesisEngine.hs 125
-chooseCandidateRules :: Hypos -> IM (CallDep,CovrRules)
-chooseCandidateRules = 
-    return . (\h -> (callings h, open h)) . S.findMin
---    return . S.fold collect S.empty  
---    where    
---    collect = S.union . open
+chooseCandidateRules :: Hypos -> IM [(CallDep,CovrRule)]
+chooseCandidateRules hs =
+    return $  concatMap collect (S.toList hs)
+    where
+    collect h = map ((,) (callings h)) (S.toList $ open h)   
+--
+--    return . (\h -> (callings h, open h)) . S.findMin
+----    return . S.fold collect S.empty  
+----    where    
+----    collect = S.union . open
hunk ./src/SynthesisEngine.hs 136
-chooseOneRule :: CovrRules -> IM CovrRule
-chooseOneRule = return . S.findMin
+chooseOneRule :: [(CallDep,CovrRule)] -> IM (CallDep,CovrRule)
+chooseOneRule = return .  minimumBy (compare `on` snd)
hunk ./src/SynthesisEngine.hs 142
+    
hunk ./src/SynthesisEngine.hs 144
-    llogIN $ text "Resulted in" <+> int (length advancements) <+> text "different sucessor hypotheses."
+    llogIN $ text "Resulted in" <+> int (length advancements) <+> 
+             text "different sucessor hypotheses."
+    
hunk ./src/UI/UIStarter.hs 14
-import System.Mem
-import System.Time
+
+import Text.Printf
+
hunk ./src/UI/UIStarter.hs 19
+import Data.Time.LocalTime
hunk ./src/UI/UIStarter.hs 27
-import Time 
+
hunk ./src/UI/UIStarter.hs 124
-runCmd s (Load path)            =  loadFile s path
+runCmd s (Load path)            = loadFile s path
hunk ./src/UI/UIStarter.hs 198
-                         return $ ctx `seq` (False,s{context=ctx})
+                         return $ (False,s{context=ctx})
hunk ./src/UI/UIStarter.hs 212
-            start  <- getClockTime
-            res <- return $  startSynthesis ts bs
-            end    <- getClockTime
-            printResult s (diffClockTimes end start) res
+            (t,res) <- time (return $ startSynthesis ts bs)
+            printResult s t res
hunk ./src/UI/UIStarter.hs 217
-date :: IO (Integer,Int,Int,Integer) -- :: (year,month,day,CPUTime)
+time :: IO a -> IO (String, a)
+time ioa = do
+    t1 <- getCPUTime
+    a <- ioa
+    t2 <- getCPUTime
+    let t :: Double
+        t = fromIntegral (t2-t1) * 1e-12
+    return (printf "CPU time: %6.5fs\n" t, a)
+
+date :: IO (Integer,Int,Int,TimeOfDay) -- :: (year,month,day,CPUTime)
hunk ./src/UI/UIStarter.hs 229
-       s       <- getCPUTime
-       return (y,m,d,s)
+       t       <- getZonedTime >>= return . localTimeOfDay . zonedTimeToLocalTime 
+       return (y,m,d,t)
hunk ./src/UI/UIStarter.hs 233
-             return $ (shows y).(addzero m).(shows m).(addzero d).(shows d) $ show s
+             return $ (shows y).(addzero m).(shows m).(addzero d).(shows d).(showChar '_') $ show s
hunk ./src/UI/UIStarter.hs 237
-printResult :: EnvState -> TimeDiff -> (Either String [[Dec]],Log) -> IO()
+printResult :: EnvState -> String -> (Either String [[Dec]],Log) -> IO()
hunk ./src/UI/UIStarter.hs 241
-    let elt = text "elapsed time: " <> pretty t <$$> linebreak
+    let elt = text t <$$> linebreak
hunk ./src/UI/UIStarter.hs 261
-resToDoc w (Left msg) = return . text $ "UNCAUGHT ERROR: " ++ msg
+resToDoc w (Left msg) = return . red . text $ "UNCAUGHT ERROR: " ++ msg
hunk ./src/UI/UIStarter.hs 270
-                         indent 6 (text "- - - - - HYPOTHESE" <+> int i <+> 
-                                   text "of" <+> int j <+> text "- - - - -") <$$>
+                         indent 6 (bold (text "- - - - - HYPOTHESE" <+> int i <+> 
+                                   text "of" <+> int j <+> text "- - - - -")) <$$>