
module Igor2.Data.IOData (

    CovrRule, name, crul,
    isOpen, isClosed, modifycrul,

    CovrRules, covrRules,

    IOData, initIOData, getAll, breakup, fuse, fuseByName, insertRules

    )where

import Prelude hiding ((<$>))

import Igor2.Data.Rules hiding (mapRuleRhsM, mapRuleLhsM, mapRuleM, isOpen, isClosed)
import qualified Igor2.Data.Rules as Rules (isOpen, isClosed)

import Syntax (Name, mkName, C)

import Igor2.Logging
import Igor2.Ppr

import Data.List (intersect, sort, (\\))

import Data.Maybe (listToMaybe, maybe)

import Data.Map (Map)
import qualified Data.Map as M

import Data.MySet (Set)
import qualified Data.MySet as S 

import Data.List (nub, foldl', transpose)

import Data.Function
import Control.Monad
import Control.Monad.Error (Error, MonadError)
{-
 | IOData  defines the context in which a function is synthesised. 
   Theorem: The synthesis of a function is solely dependent on its context and 
            the search strategy. Same context --> same synthesised function 
            definition. 
-}
data IOData = IOD
    { evidence  :: !(Map Name Rules)
--    , rhsides   :: !(Map RHS [(Name,LHS)])
--    , lhsides   :: !(Map LHS [(Name,RHS)])
--    , functions :: !(Bimap Name Rules)
    }
    deriving (Show)

--------------------------------------------------------------------------------
-- Creating and Modifying IOData
--------------------------------------------------------------------------------

{-
 | /O(log n)/ Creates an IOData value with given Name-Rules-associations. It is neither 
 | checked, whether some Names or Rules do occur more than once. If so, 
 | overlapping associations are deleted. 
-}
-- PUBLIC
initIOData :: [(Name,Rules)] -> IOData
initIOData = foldr (\(n,r) -> insertUnsafe n r) emptyIOData
    
                        

-- | /O(1)/creates an empty IOdata value
-- PRIVATE
emptyIOData :: IOData
emptyIOData = IOD
    { evidence  = M.empty
--    , rhsides   = M.empty
--    , lhsides   = M.empty
--    , functions = B.empty -- unused yet, I think
    }

{-
 | /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. 
-}
--insertWithName :: Name -> Rules -> IOData -> IOData
--insertWithName n rs iod@(IOD{ evidence = bk }) =
--    iod{ evidence =  M.insert n rs bk}


{-
 | /O(log n)/ Insert the rules into the IOData value. The resulting IOdata value
 | paired with the key, the rules have been saved under, is returned. If the 
 | rules have previously been stored, the old key is returned, otherwise a new 
 | is generated. The 'key' is a TH Name, specifying the function name. 
-}
insertRules :: Rules -> IOData -> (Name,IOData)
insertRules rs iod@(IOD{ evidence = bk }) = (n', iod')
--    case moreGeneralSuperset rs iod of
--        Just n       -> (False,n,iod)
--        Nothing      -> (True,n',iod')
    where
        n' = mkName $ "fun" ++ show (M.size bk)
        iod' = insertUnsafe n' rs iod


-------------------------------------------------------------------------------
-- Retrieve Rules
-------------------------------------------------------------------------------

-- |Retrieve all 'Rules' of a function with the provided 'Name' from the 
--  background knowledge
-- PUBLIC
getRules :: Name -> IOData -> Rules
getRules n iod =
    case lookupByName n iod of
        Just rs -> rs
        Nothing -> error $ "no Rules for " ++ show n ++ " in IOData"

getAll :: Name -> IOData -> [CovrRule]
getAll n iod = [RF n r [i] | (r, i) <- zip (S.toList (getRules n iod)) [0..]]

-- |Retrieve the ith 'Rule' of a function with the provided 'Name' from the 
--  background knowledge (zero based). The position is determined by 
--  'Data.rules.ruleAtIndex'. Since 'Rules', once stored in IOData, is never 
--  changed, it is guaranteed, that the index does not change.      
-- UNSAFE
getSpecific :: Name -> IOData -> Int -> CovrRule
getSpecific n iod i =  (getAll n iod) !! i

-- |Retrieve the specified 'Rules' of a function with the provided 'Name' from the 
--  background knowledge (zero based)      . The position is determined by 
--  'Data.rules.ruleAtIndex'. Since 'Rules', once stored in IOData, is never 
--  changed, it is guaranteed, that the index does not change.
-- UNSAFE      
getSpecifics :: Name -> IOData -> [Int] -> [CovrRule]
getSpecifics n iod =  map (getSpecific n iod)

-- |Access 'Rules' in the background knowledge by the 'Name' of a function
-- PRIVATE        
--lookupByName :: (Monad m) => Name -> IOData -> m Rules
lookupByName :: Name -> IOData -> Maybe Rules
lookupByName n b = M.lookup n $ evidence b 

      
--------------------------------------------------------------------------------
-- Modify CovrRules       
--------------------------------------------------------------------------------
breakup :: CovrRule -> IOData -> [CovrRule]
breakup rf iod = getSpecifics (name rf) iod (covr rf)

fuseByName :: Name -> IOData -> LM CovrRule
fuseByName n iod = do
    let rs = getRules n iod
    rule <- lift $ lggRules $ S.toList rs
    let indices = [0 .. (S.size rs - 1)]
    return $ RF n rule indices

fuse :: (MonadError e m, Error e) => [CovrRule] -> C m CovrRule
fuse cruls = do
    rule <- lggRules rules
    if all (==n) names
      then return $  RF n rule indices
      else fail $ "Data.IOData.fuse : Cannot fuse CovrRules with different names!"
    where
    (n:names)    = map name cruls 
    rules        = map crul cruls
    indices      = sort $ nub $ concatMap covr cruls


---------------------
-- Unsafe functions
---------------------
{-|
 /O(log n)/ Insert the rules associated with the Name into the IOData. If either rules or
 Name exists already in IOData, previous bindings are deleted. 
-}
insertUnsafe :: Name -> Rules -> IOData -> IOData
insertUnsafe n rs iod =
    alterEvidence n rs iod

alterEvidence :: Name -> Rules -> IOData -> IOData
alterEvidence n rs iod =
    let evi = evidence iod in
    iod { evidence = M.insert n rs evi }

--alterRhss :: Name -> Rules -> IOData -> IOData
--alterRhss n rs iod =
--    iod{rhsides = foldl' ins  rhss (S.toList rs)}
--    where
--    ins = (\m r -> M.insertWith (++) (rhs r) [(n,lhs r)] m)
--    rhss = rhsides iod  
         
--alterLhss :: Name -> Rules -> IOData -> IOData
--alterLhss n rs iod =
--    iod{lhsides = foldl' ins  lhss (S.toList rs)}
--    where
--    ins = (\m r -> M.insertWith (++) (lhs r) [(n,rhs r)] m)
--    lhss = lhsides iod


--------------------------------------------------------------------------------
-- Datatype CovrRulement
--------------------------------------------------------------------------------

-- Encapsulating all information of an open/unfinished Rule
data CovrRule = RF
    { name  :: Name      -- ^ the name of the function/rule
    , crul  :: Rule      -- ^ the covering rule itself
    , covr  :: [Int]     -- ^ the indices of covered I/O examples (stored in a IOData)
    }
    deriving(Show, Eq, Ord)
    
   
type CovrRules = S.Set CovrRule

covrRules :: [CovrRule] -> CovrRules
covrRules = S.fromList    

isOpen :: CovrRule -> Bool
isOpen = Rules.isOpen . crul

isClosed :: CovrRule -> Bool
isClosed = Rules.isClosed . crul

-- | Applies the given function to the 'Rule'-part of a 'CovrRule', and updates 
--   the open positions, which might have been changed
modifycrul :: CovrRule -> (Rule -> Rule) -> CovrRule
modifycrul rf@(RF _ f _) g = 
    let f' = g f 
    in rf{crul= f'}
 
--------------------------------------------------------------------------------
-- Class Instances
--------------------------------------------------------------------------------
   
-- Pretty
--
            
instance Pretty IOData where
        pretty iod = text "IODATA" <$> 
                     parens ( indent 2 $ 
                        text "Evidence :" <$> pretty (evidence iod) )
                        
instance Pretty CovrRule where
    pretty  (RF n f c) = pretty n <+> pretty f <+> text "^" <>  (text $show c)
