[Modified synthesis to output tiers of alternative hypotheses
martin.hofmann@uni-bamberg.de**20091020100643
 I am not sure if whether this is good or not. I am afraid that logging will force execution until SearchSpace is exhausted, so laziness does not help here.
] hunk ./src/Data/HypoSpace.hs 5
-    bestHypos, replaceHypos, countHypos,
+    countHypos, isEmpty,
+    pushHypo, pushHypos, popHypos,
hunk ./src/Data/HypoSpace.hs 29
-
+isEmpty :: HSpace -> Bool
+isEmpty = H.isEmpty . heap
+ 
hunk ./src/Data/HypoSpace.hs 46
--- | find the best valued Hypotheses
-bestHypo :: HSpace -> Hypo
-bestHypo = head . snd . H.getMin . heap
-
--- | 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)
-               
---------------------------------------------------------------------------------
--- Hidden helpers
---------------------------------------------------------------------------------
-
+-- 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/HypoSpace.hs 67
-pushHypos :: HSpace -> [Hypo] -> HSpace
-pushHypos h = foldl pushHypo h
+pushHypos :: [Hypo] -> HSpace ->  HSpace
+pushHypos h hsp  = foldl pushHypo hsp h
hunk ./src/Data/HypoSpace.hs 71
-popHypos = (second decCntr) . popUnsafe
+popHypos = (\(hl,hs) -> (hl, decCntrBy (length hl) hs)) . popUnsafe
hunk ./src/Data/HypoSpace.hs 78
-incCntr :: HSpace -> HSpace
-incCntr (HS c hp) = HS (c+1) hp
+incCntrBy:: Int -> HSpace -> HSpace
+incCntrBy i (HS c hp) = HS (c+i) hp
+
+incCntr = incCntrBy 1
+
+decCntrBy :: Int -> HSpace  -> HSpace
+decCntrBy i (HS c hp) = HS (c-i) hp
hunk ./src/Data/HypoSpace.hs 86
-decCntr :: HSpace -> HSpace
-decCntr (HS c hp) = HS (c-1) hp
+decCntr = decCntrBy 1
hunk ./src/Data/IgorMonad.hs 4
-    initIgor, setupTarget, propagate,
+    initIgor, setupTarget,
hunk ./src/Data/IgorMonad.hs 13
-    setTarget, getTarget, addBgk, remBgk, currentBestHypos, getEvidence, 
-    getSearchSpace, tick, loopCount, loopsCount, hypoCount, isDebug, 
+    setTarget, getTarget, addBgk, remBgk, getEvidence, 
+    tick, loopCount, loopsCount, isDebug, 
hunk ./src/Data/IgorMonad.hs 47
-    , igor_sp  :: !HSpace
+--    , igor_sp  :: !HSpace
hunk ./src/Data/IgorMonad.hs 66
-setTarget n = get >>= lift . (setupTarget n) >>= put
+setTarget n = get >>= lift . (setupTarget n) >>= put 
hunk ./src/Data/IgorMonad.hs 75
--- | Set the target for the given 'Igor' to a function with name 'Name'. If no 
+-- | Set the target for the given 'Igor' to a function with name 'Name'. If no
hunk ./src/Data/IgorMonad.hs 78
-setupTarget n ( Igor iod _ lc cf ct) = do
-    initH <- fuse . (getAll n) $ iod
-    return $ Igor iod (initHSpace initH) ((n,0):lc) cf ct  
+setupTarget n ( Igor iod lc cf ct) = do
+    return $ Igor iod ((n,0):lc) cf ct  
hunk ./src/Data/IgorMonad.hs 86
-initIgor nr = Igor (initIOData nr) emptyHSpace []
+initIgor nr = Igor (initIOData nr) []
hunk ./src/Data/IgorMonad.hs 138
-    modify (\i@(Igor _ _ _ c _) -> i{igor_cnf=c{scr_bgks=bgk'}})
+    modify (\i@(Igor _ _ c _) -> i{igor_cnf=c{scr_bgks=bgk'}})
hunk ./src/Data/IgorMonad.hs 144
-    modify (\i@(Igor _ _ _ c _) -> i{igor_cnf=c{scr_bgks=bgk'}})
+    modify (\i@(Igor _ _ c _) -> i{igor_cnf=c{scr_bgks=bgk'}})
hunk ./src/Data/IgorMonad.hs 151
+-- DEPRECATED
hunk ./src/Data/IgorMonad.hs 153
-currentBestHypos :: IM Hypos
-currentBestHypos = liftM bestHypos $! gets igor_sp
-
-getSearchSpace :: IM HSpace
-getSearchSpace = gets igor_sp
-
-modifyHS :: (HSpace -> HSpace) -> IM()
-modifyHS f = 
-    modify $ \igor@(Igor _ sp _ _ _) ->
-      igor{igor_sp = f sp}
+--currentBestHypos :: IM Hypos
+--currentBestHypos = liftM bestHypos $! gets igor_sp
+--
+--getSearchSpace :: IM HSpace
+--getSearchSpace = gets igor_sp
+--
+--modifyHS :: (HSpace -> HSpace) -> IM()
+--modifyHS f = 
+--    modify $ \igor@(Igor _ sp _ _ _) ->
+--      igor{igor_sp = f sp}
+--    
+--propagate :: Hypo -> Hypos -> IM ()  
+--propagate  = (modifyHS .) . replaceHypos
hunk ./src/Data/IgorMonad.hs 175
-    modify $ \igor@(Igor io _ _ _ _) ->
+    modify $ \igor@(Igor io _ _ _) ->
hunk ./src/Data/IgorMonad.hs 179
-tick = get >>= \i@(Igor _ _ ((n,lc):lcs) _ _) ->
+tick = get >>= \i@(Igor _ ((n,lc):lcs) _ _) ->
hunk ./src/Data/IgorMonad.hs 182
-propagate :: Hypo -> Hypos -> IM ()  
-propagate  = (modifyHS .) . replaceHypos
-    
hunk ./src/Data/IgorMonad.hs 188
-hypoCount :: IM Int
-hypoCount = gets $ countHypos.igor_sp
+--hypoCount :: IM Int
+--hypoCount = gets $ countHypos.igor_sp
hunk ./src/Data/IgorMonad.hs 193
-    i@(Igor iod _ _ _ _) <- get
+    i@(Igor iod _ _ _) <- get
hunk ./src/Data/IgorMonad.hs 220
-                        pretty (igor_sp i) <$>
+                        --pretty (igor_sp i) <$>
hunk ./src/Logging/Logger.hs 4
-    tp,ts,lift3,lputStrLn,lputDoc,
+    tp,ts,lift3, lputStrLn,lputDoc,
hunk ./src/Logging/Logger.hs 50
-
hunk ./src/SynthesisEngine.hs 15
+import Data.HypoSpace
hunk ./src/SynthesisEngine.hs 24
+import Data.List (partition, transpose)
hunk ./src/SynthesisEngine.hs 38
-               -> IO (Either String ([(Name,Int)],[[Dec]]),Log)
+               -> IO (Either String ([(Name,Int)],[[[Dec]]]),Log)
hunk ./src/SynthesisEngine.hs 45
-synthesise :: SynCtx -> SCR -> [(Name,Rules)] -> [(Name,Rules)] -> LM ([(Name,Int)],[[Dec]])
+synthesise :: SynCtx -> SCR -> [(Name,Rules)] -> [(Name,Rules)] -> LM ([(Name,Int)],[[[Dec]]])
hunk ./src/SynthesisEngine.hs 57
-    let hs' = simplify (scr_simplify conf) $ hs
+    let hs' = take 2 $ map (simplify (scr_simplify conf)) $ hs
hunk ./src/SynthesisEngine.hs 59
-    return . ((,) l) . hypos2decs $ hs'
+    return . ((,) l) $ map hypos2decs hs'
hunk ./src/SynthesisEngine.hs 70
-synthesiseTargets :: [Name] -> IM [[Hypo]]
-synthesiseTargets ns = liftM oneFromEach $ mapM synthesiseTarget ns
+synthesiseTargets :: [Name] -> IM [[Hypos]]
+synthesiseTargets ns = liftM ((map oneFromEach).transpose) $ mapM synthesiseTarget ns
hunk ./src/SynthesisEngine.hs 73
-    synthesiseTarget :: Name -> IM [Hypo]
+    synthesiseTarget :: Name -> IM [Hypos]
hunk ./src/SynthesisEngine.hs 78
-        remBgk ns >> addBgk (ns \\ [n]) >> setTarget n >> enterLoop
+        remBgk ns >> addBgk (ns \\ [n]) >> setTarget n >> coverAll n >>= 
+         doLoop . initHSpace
hunk ./src/SynthesisEngine.hs 83
-enterLoop :: IM [Hypo]
-enterLoop =  do
+doLoop :: HSpace -> IM [Hypos]
+doLoop hsp =  do
hunk ./src/SynthesisEngine.hs 90
-    hypoCount >>= llogNO . (text "#Hypos:" <+>) . pretty
+    llogNO . (text "#Hypos:" <+>) . pretty . countHypos $ hsp
+    llogNO . (text "HSpace:" <+>) . pretty $ hsp
hunk ./src/SynthesisEngine.hs 93
-    
-    besthypos  <- currentBestHypos
-    candidates <- chooseCandidateHypo besthypos >>= return . chooseCandidateRule
-
-    let nocandidates = not. isJust $ candidates
-    maxloopcount <- stopAtMaxLoopCount
+    if (isEmpty hsp) 
+       then llogNO(linebreak <> text "SEARCHSPACE EXHAUSTED - - STOP") >>
+             return []
+       else do 
+            let (hypos,hsp') = popHypos hsp
+            let (ejcts,cnds) = partition isFinished hypos
+            
+            maxloopcount <- stopAtMaxLoopCount
+         
+            if maxloopcount then stopWith hypos
+              else if (null cnds) 
+                     then llogNO(linebreak <> text "ALL CANDIDATES CLOSED, go to next tier") >> 
+                           doLoop hsp' >>= eject ejcts
+                     else do ahs   <- advance . head $ cnds
+                             hsp'' <- doLoop $ pushHypos ahs $ pushHypos (tail cnds) $ hsp'
+                             eject ejcts hsp'' 
hunk ./src/SynthesisEngine.hs 110
-    llogDE $ text "Stopping Criteria?" <^>
-             text "Empty Candidates :" <+> bool nocandidates <^>
-             text "Max Loopcount    :" <+> bool maxloopcount   
+     
+eject :: Hypos -> [Hypos] -> IM [Hypos]
+eject hs 
+    | null hs   = return . id
+    | otherwise = return . (hs:)  
hunk ./src/SynthesisEngine.hs 116
-    if nocandidates  || maxloopcount
-      then stopWith besthypos
-      else uncurry applyAdvacements  (fromJust candidates) >> enterLoop
-      
+advance :: Hypo -> IM Hypos
+advance h = advanceRule h (head . S.toList . open $ h) 
hunk ./src/SynthesisEngine.hs 119
-stopWith  :: Hypos -> IM [Hypo]
+stopWith  :: Hypos -> IM [Hypos]
hunk ./src/SynthesisEngine.hs 124
-       return hs -- $ map simplifiedBindings hs
+       return [hs] -- $ map simplifiedBindings hs
hunk ./src/SynthesisEngine.hs 132
-
-chooseCandidateHypo :: (Monad m)=> Hypos -> (m Hypo)
-chooseCandidateHypo = headM 
-    
-chooseCandidateRule :: (Monad m) => Hypo -> (m (Hypo,CovrRule))
-chooseCandidateRule hs =  liftM ((,) hs) (headM . S.toList . open $ hs) 
-  
-applyAdvacements :: Hypo -> CovrRule -> IM ()
-applyAdvacements h r = advanceRule h r >>= propagate h 
hunk ./src/UI/UIStarter.hs 70
-modifyHistory :: EnvState -> ([Name],[Name]) -> [[Dec]] -> EnvState
+modifyHistory :: EnvState -> ([Name],[Name]) -> [[[Dec]]] -> EnvState
hunk ./src/UI/UIStarter.hs 72
-    let v' = map (unlines.(map (show.pretty))) v
+    let v' = map (unlines.(map (show.pretty))) (head v)
+    -- TODO : Now only the first tier of results ist stored in history
hunk ./src/UI/UIStarter.hs 228
+    
hunk ./src/UI/UIStarter.hs 235
-                 then mapM_ (test d) [1..(length d)]
-                 else test d i 
+                 then mapM_ (test e d) [1..(length d)]
+                 else test e d i 
hunk ./src/UI/UIStarter.hs 239
-    test d i = do r <- (interprete (ctxtFile s) $ prepare (d !! (i-1)) e) 
-                  hPutDoc stdout $ text "Testing" <+> int i <> 
-                                   text ". hypothesis" <+> text "of:" <+> 
-                                   setDoc <^> text e <+> text " == " <+> 
-                                   text r <$> linebreak
+    test e d i = do r <- (interprete (ctxtFile s) $ prepare (d !! (i-1)) e) 
+                    hPutDoc stdout $ text "Testing" <+> int i <> 
+                                     text ". hypothesis" <+> text "of:" <+> 
+                                     setDoc <^> text e <+> text " == " <+> 
+                                     text r <$> linebreak
hunk ./src/UI/UIStarter.hs 300
-            -> (Either String ([(Name,Int)],[[Dec]]),Log) -> IO()
-printResult s c t (r,l) = do 
+            -> (Either String ([(Name,Int)],[[[Dec]]]),Log) -> IO()
+printResult s c t (rs,l) = do 
hunk ./src/UI/UIStarter.hs 303
-    let res = resToDoc w t r
+    let res = resToDoc w t rs
hunk ./src/UI/UIStarter.hs 332
-resToDoc :: Int -> Doc -> Either String ([(Name,Int)],[[Dec]]) -> Doc
+resToDoc :: Int -> Doc -> Either String ([(Name,Int)],[[[Dec]]]) -> Doc
hunk ./src/UI/UIStarter.hs 336
-resToDoc w t (Right (ls,ds)) = 
+resToDoc w t (Right (ls,ts)) = 
hunk ./src/UI/UIStarter.hs 340
-    vcat (map (printHypo (length ds)) (zip ds [1..]))
+    vcat (map (printTier (length ts)) (zip ts [1..]))
hunk ./src/UI/UIStarter.hs 345
-
+printTier :: Int -> ([[Dec]],Int) ->  Doc
+printTier j (hs,i) = linebreak <> 
+                     (bold (text "TIER" <+> int i <+> text "of" <+> int j)) <$$>
+                     vcat (map (printHypo (length hs)) (zip hs [1..]))  <$$>
+                     linebreak  