
module Igor2.SynthesisEngine (

    startSynthesis,
    
    )where

import Prelude hiding ((<$>))

import Data.Function (on)
import Data.List (minimumBy, (\\))

import Control.Monad.State
import Control.Monad.Error
import qualified Data.Map as M (toList)
import Data.Maybe (isJust, fromJust)
import Data.List (partition, transpose)

import Syntax

import Igor2.Ppr 

import Data.Util
import qualified Data.MySet as S

import Igor2.Config
import Igor2.Data.HypoSpace
import Igor2.Data.IgorMonad
import Igor2.Data.IOData
import Igor2.Data.Rules (hypos2decs)
import Igor2.Logging
import Igor2.RuleDevelopment


type Funcrul = (Name,Rules)
type Funcruls = [(Name, Rules)]

{-
 | This is the top-level function, triggering all other stuff in the nested 
   Monads. It is responsible for IO, displaying the log and the result. 
-}
    
startSynthesis :: Context  -> SCR -> LogState -> [FunBind] -> [FunBind]
               -> IO (Either String ([(Name, Int)], [[[FunBind]]]))
startSynthesis ctx conf logstate tgt bgk =
    (withC (runLM (synthesise ctx conf (toRbs tgt)(toRbs bgk)) logstate) ctx)
         `catchError` \m -> return (Left (show m))
    where
    toRbs = map (\(FunB n es) -> (n, mkRules es))

synthesise :: Context -> SCR -> [(Name,Rules)] -> [(Name,Rules)]
           -> LM ([(Name,Int)],[[[FunBind]]])
synthesise ctx conf tgts bgks = do
    let allrs    = (++) tgts bgks
    let igordata = initIgor allrs conf ctx

    waypointL $ text "Initialising Igor"
    logIN ( pretty conf )
    logDE ( linebreak <> text "IGOR initialised to:" <$> 
            indent 2 (pretty igordata))
            
    (hs,l) <- (runIM (synthesiseTargets (scr_tgts conf) >>= \r -> 
                      loopsCount >>= \l -> 
                       return (r,l)) igordata)
                       
    bnds  <- mapM (simplify (scr_simplify conf)) hs
    when (scr_debug conf) (outputraw bnds)
    return . ((,) l) $ map hypos2decs bnds
    where
    simplify True hs  = lift $ 
                        mapM (\h -> mapM simplifiedBindings h >>= 
                                   return . (map snd) >>= return . concat) hs
    simplify False hs  = return  (map (concatMap allBindings) hs)

    outputraw hs =
      liftIO . putDoc $ linebreak <>
                text "### BEGIN RAW DATA ###" <$>
                text "I/O TGT" <$> (text . show $ tgts) <$>
                text "I/O BGK" <$> (text . show $ bgks) <$> 
                text "RESULTS" <$> (text . show $ map reverse hs) <$>
                text "### END RAW DATA ###" <> linebreak

synthesiseTargets :: [Name] -> IM [[Hypos]]
synthesiseTargets ns = 
  liftM ((map oneFromEach).transpose) $ mapM synthesiseTarget ns
    where 
    synthesiseTarget :: Name -> IM [Hypos]
    synthesiseTarget n =  do
    
        waypointL $ text "STARTING SYNTHESIS for TARGET" <+> 
                    squotes (pretty n)
        
        remBgk ns >> addBgk (ns \\ [n]) >> setTarget n >> coverAll n >>= 
         lift . lift . initHSpace >>= doLoop
    -- same as sequence !!(?)
    oneFromEach []    = [[]]
    oneFromEach (x:xs)= [e:es | e <- x, es <- (oneFromEach xs)]

doLoop :: HSpace -> IM [Hypos]
doLoop hsp 
    | isEmpty hsp = exhausted
    | otherwise   = do
      tick

      loopCount >>= \lc -> waypointM $
                          text "Entering Rule-Advancement-Loop for the" <+>
                               int lc <> text ". time"
      logNO . (text "#Hypos:" <+>) . pretty . countHypos $ hsp
      logDE . (text "HSpace:" <+>) . pretty $ hsp

      getEvidence >>= \io -> logDE ( linebreak <>
                                     text "IGOR initialised to:" <$>
                                     indent 2 (pretty io))
        
      debug <- isDebug
      atMxL <- atMaxLoops   
      atMxT <- atMaxTiers
      
      let (hypos,hsp') = popHypos hsp

      if atMxL then logNO (text "MaxLoops reached") >> stopWith hypos
       else if any isFinished hypos then finishTier hypos hsp'
             else continue hypos hsp'
      
-- Assumes at least one 'Hypo' to be finished! If we have reached maxTiers, 
-- then prune the HSpace, and try to finish Hypos which are as good as the 
-- finished ones. The best ones are pushed back unchanged, so they are on top 
-- in the next loop iteration again.
-- Otherwise if we are still under the maxTiers threshold and all best hypos 
-- are finised, eject those and enter loop again with remaining HSpace. If there
-- are still unfinished hypos, advance them and continue with best hypos pushed
-- back.
finishTier hypos hsp = do 
           
  atMxT  <- atMaxTiers
  logNO (linebreak <> text "FINISHED HYPOS, finish Tier:")
  case partition isFinished hypos of
    (f,[]) -> if atMxT
             then do logNO (text "Maximum tiers reached!")
                     stopWith hypos
             else do logNO (text "TIER FINISHED: Eject finished and continue!")
                     tickT >> doLoop hsp >>= eject hypos
    (f,uf) -> if atMxT
             then do logNO (text "Prune and finish tier.")
                     continue uf (pushHypos f emptyHSpace)
             else do logNO (text "Continue with unfinished.")
                     continue uf (pushHypos f hsp)
   -- if still unfinished hypos,

-- advance the given hypos, push them back into HSpace, and do loop again  
continue (h:hs) hsp = do 
    newhs   <- advance h
    doLoop  $ pushHypos (newhs ++ hs) hsp

exhausted = logNO( linebreak <>
                    text "SEARCHSPACE EXHAUSTED - - STOP" <>
                    linebreak ) >>
            return []     
            
eject :: Hypos -> [Hypos] -> IM [Hypos]
eject hs = return . (hs:)  
 
advance :: Hypo -> IM Hypos
advance h = advanceRule h (head . S.toList . open $ h) 
     
stopWith  :: Hypos -> IM [Hypos]
stopWith hs = do
       logDE $ text "STOP_WITH:" <^> pretty hs
       lc <- loopCount
       tc <- tierCount
       logNO $ text "Stopped after entering loop the" <+> int lc <>
                text ". time in tier" <+> int tc <> colon
       return [hs] -- $ map simplifiedBindings hs


