
module Igor2.RuleDevelopment.Partition (

    partition, trivialPartition

    )where

import qualified Data.Set as S
import Data.List (foldl', nub, intersperse)
import qualified Data.List as L (partition)
import Data.Maybe (isJust, mapMaybe)
import Control.Monad (ap)
import Data.Function

import Igor2.Logging
import IOInterpreter
import Igor2.Data.IgorMonad
import qualified Igor2.Data.Rules as R (sameSymAt)
import Syntax
import Igor2.Ppr

-- FOR TESTING ONLY
-- No real partition, but an implementaion of overfitting :-), simply always
-- splitting the first rule from the rest.
trivialPartition :: CovrRule -> IM (CovrRules,[Call])
trivialPartition rf = do
    (first:rest) <- breakupM rf
    fusedrest    <- lift . lift $ fuse rest
    return (covrRules [first, fusedrest], [])

-- creates new partitions (i.e. CovrRules) from one CovrRule
-- the resulting rules may be closed by antiunification
-- and it should be assured, that each CovrRule has only one open position
-- --> closing pairwise with functionCall and subfunction (not yet implemented
-- but maybe a good improvement?)
partition :: CovrRule -> IM [(CovrRules,[Call])]
partition cr = do
    waypointS $ text "Partitioning"
    gsplt <- doGreedySplt
    cruls <- breakupM cr
    let pivotpos  = concat.init.ruleVarPos $ crul cr
    parts <- fuseParts . noTrivial $ doPart gsplt cruls pivotpos
    let nubbedparts = nub parts
--               (if gsplt then (((:[]) .) . fullPartitioning)
--                  else singlePartitioning) cruls pivotpos
    logIN ( text "Rule:" <+> pretty cr )
    logDE ( text "At  :" <+> pretty pivotpos <^>
             text "Into:" <+> pretty nubbedparts
            )
--    ps <- predicates
--    parts' <- partitionWith cr
--    logIN (text "Partition with" <+> pretty ps <^>
--            text "Into:" <+> pretty parts'
--            )
    return $ map (\p -> (p, [])) nubbedparts
    where
      noTrivial = filter (\l -> case l of [_] -> False; _owise -> True)
      doPart _ [a] _ = [] 
      -- partitioning a single rule results in no partitions
      doPart gsplt cruls pivotpos
          | gsplt = [fullPartitioning  cruls pivotpos]
          | otherwise = singlePartitioning cruls pivotpos


fuseParts :: [[[CovrRule]]] -> IM [CovrRules]
fuseParts = lift . lift . mapM (liftM covrRules . mapM fuse)

-- complexity should be O(n*m) where n is the number of rules and m the number
-- of partitions. To reduce it, an ordering of partitions is necessary
singlePartitioning :: [CovrRule] -> [RulePos] -> [[[CovrRule]]]
singlePartitioning = (filter (not . null) .) . map . flip mkPartitionAt
   
-- described as 'Rapid RuleSplitting' in Emanuel's diss. Given 'n' pivot 
-- positions, instead of making $n$ new hypothesis with partitions 
-- corresponding to the construcotrs, make one new hypothisis, with partitions 
-- corresponding to all pivot positions  Instead of making one partition for 
-- each pivot position.
fullPartitioning :: [CovrRule] -> [RulePos] -> [[CovrRule]]
-- fullPartitioning =  foldr ((=<<) . mkPartitionAt) . return
fullPartitioning crs pos = foldl partAll [crs] pos
    where 
      partAll cs p = concatMap (mkPartitionAt p) cs
-- partitioning helper, partitioning given CovrRule list w.r.t. the given RulePos

mkPartitionAt :: RulePos -> [CovrRule] -> [[CovrRule]]
mkPartitionAt p crs =  foldl' bin [] crs
    where
      cmpAtPos = (R.sameSymAt p) `on` crul
      bin [] e            = [[e]]
      bin ((x:xs):done) e
           | cmpAtPos e x  =  (e:x:xs):done
           | otherwise     =  (x:xs):(bin done e)  
     
-- TODO: Patition using predicates
--   
--partitionWith :: CovrRule -> IM [(CovrRules,[Call])]
--partitionWith cr = do
--    let vars = (tp $ "VARPOS" ++ (showp cr)) . concatMap (uncurry (map . (,))) $ (concatMap getVarPos) . lhs . crul $ cr
--    -- all variables on the lhs of 'cr' paired with their position
--    -- TODO What about constant term, e.g. partitioning whether the first arg
--    -- of a list is '1' ?
--    rs <- liftM (breakup cr) getEvidence
--    ps <- predicates
--    liftM concat $  mapM (tryWith vars rs) ps
--     
---- TODO: It is sufficient to use Type instead of TExp in first arg, and it is 
----       necessary t ouse RulePos instead of Position, or at least keep track 
----       of the argumet position
--tryWith :: [(TExp,Position)] -> [CovrRule] -> (Name,Type) -> IM [(CovrRules,[Call])]
--tryWith varPos rules (fn,ft) = do
--    i <- instances
--    p <- ctxFile
--    let argpos = (mapMaybe =<< flip lookup . tyPosList i) (argTyList ft)
--    -- argpos :: [[Position]], for each argument of the function 'f', get those
--    -- positions which variables are of a compatible type
--    let crulExprs =  mapMaybe pos2strExpr $ sequence argpos
--    -- crulExprs :: [[(CovrRule,String)]]
--    rawparts <- lift4 $  mapM ((liftM (L.partition snd)) .(mapM (evaluate p))) crulExprs
--    -- parts :: [([(CovrRule,Bool)],[(CovrRule,Bool)])]
--    lift $ mapM mkParts $ filter (\(a,b) -> not (null a || null b)) rawparts
--    
--    where
--    nothingIf f a = if f a then Nothing else Just a
--    argTyList = init . unArrowT
--    -- atys :: [Type], get the argument types as a list
--    tyPosList i = (maybe [] id) . sequence . (map (mbTyPos i)) . nub
--    -- tyPos :: [(Type,[Positions])]
--    -- for each different argument type get the positions of a matching type
--    -- if any argument type has no matching type, [] is returned
--    
--    mbTyPos i = (nothingIf (null . snd)) . (ap (,) (posWithMatchTy i))
--    -- maybe returns the input type paired with the position of compatible variables    
--    posWithMatchTy i t = map snd $ filter (isJust . (matchT i t) . typeOf . fst) varPos
--    -- get all positions from 'varPos' which match the given type 't'
--    
--    pos2strExpr ps = mapM (\r -> liftM (((,) r) . mkStrExpr) (getSubterms ps r)) rules
--    -- pos2Terms :: Maybe [(CovrRule,String)]
--    -- maybe make pairs of rule and the test epression as a string, made from the
--    -- function name and the the terms at the provided positions 'ps'
--    getSubterms ps = (maybe Nothing (nothingIf null)) . flip mapM ps .  (nothingIfHasVars .) . subtermAt . rhs . crul
--    -- get the subterms at positions in 'ps', return Nothing if either one
--    -- is undefined, or a subterms ontains a variable
--    mkStrExpr = foldl'  (flip ((. (' ' :)) . (++) . showp)) (show . parens . pretty $ fn)
--              -- equal to @(intersperse " ") . ((show fn):) . (map show)@
--              -- but more efficient (?)
--    nothingIfHasVars = maybe Nothing (nothingIf hasVars)
--    mergeCovRs = fuse . fst . unzip
--    mkParts (a,b) = do a' <- mergeCovRs a
--                       b' <- mergeCovRs b
--                       return (covrRules [a',b'],[])
--    lift4 = lift . lift . lift . lift
--    
--    
--evaluate :: FilePath -> (a,String) -> IO (a,Bool)
--evaluate p (a,s) = interprete p s >>= return . ((,) a) . read . (tp $ "XXX\n" ++ (show p) ++ "\n" ++ (show s) ++ "\n")
--
--    