-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Transform.TwoLevel
-- Copyright   :  (c) 2011 University of Minho
-- License     :  BSD3
--
-- Maintainer  :  hpacheco@di.uminho.pt
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Multifocal:
-- Bidirectional Two-level Transformation of XML Schemas
-- 
-- Combinators for Two-Level Data Transformation.
--
-----------------------------------------------------------------------------

module Data.Transform.TwoLevel where

import Data.Type
import Data.Pf
import Data.Equal
import Data.Eval
import Data.Spine
import Data.Lens
import Data.Default
import Generics.Pointless.Lenses
import Generics.Pointless.Combinators
import Generics.Pointless.Functors hiding (rep)
import Transform.Examples.Company
import Transform.Rewriting (reducePf,reduceIO)
import Transform.Rules.XPath
import Transform.Rules.PF
import Transform.Rules.Lenses

import Prelude hiding (all,Functor,until)
import Control.Monad.State as ST hiding (Functor,lift,when)
import Data.List hiding (all)
import Data.Char
import Data.Map as Map hiding (map)
import Data.Maybe

import Unsafe.Coerce

-- * Utils

maybeRead :: Read a => String -> Maybe a
maybeRead = maybe Nothing (Just . fst) . listToMaybe . reads

safeTail :: [a] -> [a]
safeTail [] = []
safeTail (x:xs) = xs

-- * Data rewriting monad: with a log of applied rules and an index of type names

type NewDatas = Map String DynFctr
type Log = [(String,String)]
type RuleTMonad m a =  StateT (Log,NewDatas) m a

type RuleT = forall a . Type a -> RuleTMonad Maybe (View a)
newtype RuleTRep = RuleTRep RuleT

nextName :: String -> String
nextName (span (/= '\'') -> (prefix,suffix)) = case (maybeRead (safeTail suffix) :: Maybe Int) of
    { Just i -> prefix ++ "'" ++ show (succ i)
    ; otherwise -> prefix ++ suffix ++ "'1" }

newData :: Functor f => String -> Fctr f -> RuleTMonad Maybe (Type (Fix f))
newData name fctr = do
    (log,datas) <- ST.get
    case (Map.lookup name datas) of
    {    Just (DynF g) -> case feq fctr g of
        {    Just Eq -> return (NewData name fctr)
        ;   otherwise -> newData (nextName name) fctr }
    ;   otherwise -> do
            ST.put (log,Map.insert name (DynF fctr) datas)
            return (NewData name fctr) }

data View a where
    View :: Pf (Lens a b) -> Type b -> View a
    
data ViewFunc a where
    ViewFunc :: Pf (a -> b) -> Type b -> ViewFunc a

instance Show (View a) where
    show (View _ b) = "(View Lens " ++ (show b) ++ ")"

transformtype :: Type a -> RuleT -> DynType
transformtype a r = maybe (DynT a) id $ do
	(View lns b,m) <- transform a r
	return $ DynT b

transformSafe :: Type a -> RuleT -> (View a,Map String DynFctr)
transformSafe a r = maybe (View ID_LNS a,Map.empty) (id >< snd) $ runStateT (r a) ([],collectNewDatas a)

transform :: Type a -> RuleT -> Maybe (View a,Map String DynFctr)
transform a r = maybe Nothing (Just . (id >< snd)) $ runStateT (r a) ([],collectNewDatas a)

-- Print the string representation of the target type encapsulated in a view.
showType :: View a -> String
showType (View _ b) = show b

showPf :: Type a -> View a -> String
showPf a (View f b) = gshow (Pf $ Lns a b) f

showOptimisedPf :: Type a -> View a -> String
showOptimisedPf a (View lns b) = gshow (Pf $ Lns a b) lns'
    where lns' = reducePf optimise_all_lns (Lns a b) lns
    
showOptimisedPfIO :: Type a -> View a -> IO ()
showOptimisedPfIO a (View lns b) = reduceIO optimise_all_lns (Lns a b) lns >> return ()

showLog :: Type a -> Log -> String 
showLog t l = show t ++ unlines (Prelude.map aux $ reverse l)
    where aux (n,s) = "\n<= {" ++  n ++ "}\n   " ++ s

-- Apply a traceable data transformation rule.
success :: String -> View a -> RuleTMonad Maybe (View a)
success n v = do
    (x,datas) <- ST.get
    ST.put $ ((n,showType v) : x,datas)
    return v
 
-- ** Two-level generic combinators

-- Sequential composition
(>>>) :: RuleT -> RuleT -> RuleT
(r >>> s) a = do (View f b) <- r a
                 (View g c) <- s b
                 return $ (View (COMP_LNS b g f) c)

-- Left-biased choice
(|||) :: RuleT -> RuleT -> RuleT
(r ||| s) x = r x `mplus` s x

-- Identity
nop :: RuleT
nop x = return $ (View ID_LNS x)

-- Apply a rule or do nothing.
try :: RuleT -> RuleT
try r = r ||| nop

-- Repeat until failure, zero or more times.
many :: RuleT -> RuleT
many r = try (r >>> many r)

-- ** Two-level locators

type TPredicate = forall a . Type a -> Bool

listP :: TPredicate -> TPredicate
listP p (List a) = p a
listP p _ = False

atP :: String -> TPredicate
atP name a@(dataName -> Just n) = sameName name n
atP name _ = False

andP :: TPredicate -> TPredicate -> TPredicate
andP f g a = f a && g a

orP :: TPredicate -> TPredicate -> TPredicate
orP f g a = f a || g a

prodP :: [TPredicate] -> TPredicate
prodP [p] a = p a
prodP (p:ps) (Prod a b) = p a && prodP ps b
prodP _ _ = False

sumP :: [TPredicate] -> TPredicate
sumP [p] a = p a
sumP (p:ps) (Either a b) = p a && sumP ps b
sumP _ _ = False

notP :: TPredicate -> TPredicate
notP p a = Prelude.not (p a)

-- Apply a rule whenever a type-level predicate is satisfied.
when :: TPredicate -> RuleT -> RuleT
when q r a = guard (q a) >> r a

-- Apply a rule to a data type with a given name.
at :: String -> RuleT -> RuleT
at name r = when (atP name) r

not :: RuleT -> RuleT -> RuleT
not r s a = case transform a r of
    {   Just v    -> mzero
    ;   otherwise -> s a
    }

hoist :: RuleT
hoist a@(Data _ fctr) = return $ View OUT_LNS (rep fctr a)
hoist a@(NewData _ fctr) = return $ View OUT_LNS (rep fctr a)
hoist _ = mzero

plunge :: String -> RuleT
plunge s a = do
    FRep f <- inferKFctr a
    new <- newData s f
    Eq <- teq (rep f Dynamic) (rep f new)
    return $ View INN_LNS new

rename :: String -> RuleT
rename s a@(Data _ fctr) = do
    new <- newData s fctr
    return $ View (CATA_LNS INN_LNS) new
rename s a@(NewData _ fctr) = do
    new <- newData s fctr
    return $ View (CATA_LNS INN_LNS) new
rename s a = mzero

-- ** Two-level abstractions

erase :: RuleT
erase a = success "erase" $ View (BANG_LNS (constPf $ defvalue a)) One

-- The argument types may involve patterns, i.e., type variables
liftPf :: Type a -> Type b -> Pf (a -> b) -> RuleT
liftPf patt app func a = do
    (Eq,vars) <- teqvars patt a
    b <- replacevar app vars
    lns <- lensify (Fun a b) func
    success "liftPf" $ View lns b    

lift :: Type a -> Type b -> Pf (Lens a b) -> RuleT
lift patt app lns a = do
        (Eq,vars) <- teqvars patt a
        b <- replacevar app vars
        success "lift" $ View lns b

liftQ :: Typeable r => Pf (Q r) -> RuleT
liftQ (q :: Pf (Q r)) a = do
    let r  = typeof :: Type r
        q' = reducePf optimise_xpath (Fun a r) (APPLYQ a q)
    liftQ' a r q'
    
liftQ' :: Type a -> Type r -> Pf (a -> r) -> RuleTMonad Maybe (View a)
liftQ' a r@(teq (List Dynamic) -> Just Eq) q = do
    ViewFunc l b <- eraseDyns a q
    liftPf a b l a
liftQ' a r@(teq Dynamic -> Just Eq) q = do
    ViewFunc l b <- eraseDyn a q
    liftPf a b l a
liftQ' a r q = liftPf a r q a

-- tries to eliminate dynamic values from an xpath query
eraseDyns :: MonadPlus m => Type a -> Pf (a -> [Dynamic]) -> m (ViewFunc a)
eraseDyns a pf = do
    DynT b <- collectDyn (Pf (Fun a (List Dynamic))) pf
    let pf' = reducePf optimise_pf (Fun a (List b)) (COMP (List Dynamic) (MAP $ UNDYN b) pf)
    -- unwrap singleton lists
    case pf' of
	(COMP b WRAP f) -> return $ ViewFunc f b
	otherwise       -> return $ ViewFunc pf' (List b)
-- tries to eliminate dynamic values from an xpath query returning a single value
eraseDyn :: MonadPlus m => Type a -> Pf (a -> Dynamic) -> m (ViewFunc a)
eraseDyn a pf = do
    DynT b <- collectDyn (Pf (Fun a Dynamic)) pf
    let pf' = reducePf optimise_pf (Fun a b) (COMP Dynamic (UNDYN b) pf)
    return $ ViewFunc pf' b

-- ** Two-level strategies

onceNorm :: RuleT -> RuleT
onceNorm r = once r >>> normalize

-- Apply a rule exhaustively many times starting from the top.
outermost :: RuleT -> RuleT
outermost r = many (onceNorm r)

allNorm :: RuleT -> RuleT
allNorm r = all r >>> normalize

-- Apply argument rule everywhere, in a bottom-up approach
everywhere :: RuleT -> RuleT
everywhere r = allNorm (everywhere r) >>> r

-- Apply argument rule where possible, in a bottom-up approach
anywhere :: RuleT -> RuleT
anywhere r = everywhere (try r)

-- Apply argument rule everywhere, in a top-down approach
everywhere' :: RuleT -> RuleT
everywhere' r = r >>> allNorm (everywhere' r)

type RuleF = forall f. Functor f => Fctr f -> RuleTMonad Maybe (ViewF f)

type NatPfLens f g = forall a. Type a -> Pf (Lens (Rep f a) (Rep g a))

data ViewF f where
    ViewF :: (Functor f,Functor g) => NatPfLens f g -> Fctr g -> ViewF f

-- Apply a rule to all childs.
all :: RuleT -> RuleT
all r (List a) = do
    View f b <- r a
    return $ View (MAP_LNS f) (List b)
all r (Prod a b) = do
    View f c <- r a
    View g d <- r b
    return $ View (PROD_LNS f g) (Prod c d)
all r (Either a b) = do
    View f c <- r a
    View g d <- r b
    return $ View (SUM_LNS f g) (Either c d)
all r t@(Data s f) = (do
    ViewF l g <- allF r f
    Eq <- feq f g
    let cata = CATA_LNS $ COMP_LNS (rep g t) INN_LNS (l t)
    return $ View cata t)
        `mplus` (do
    (ViewF l g) <- allF r f
    new <- newData s g
    let cata = CATA_LNS $ COMP_LNS (rep g new) INN_LNS (l new)
    return $ View cata new)
all r t@(NewData s f) = do
    (ViewF l g) <- allF r f
    new <- newData s g
    let cata = CATA_LNS $ COMP_LNS (rep g new) INN_LNS (l new)
    return $ View cata new
all r a = return $ View ID_LNS a

allF :: RuleT -> RuleF
allF r I = return $ ViewF (\a -> ID_LNS) I
allF r L = return $ ViewF (\a -> ID_LNS) L
allF r (K t) = do
    View l t' <- r t
    return $ ViewF (\a -> l) (K t')
allF r (f :*!: g) = do
    ViewF lf f' <- allF r f
    ViewF lg g' <- allF r g
    return $ ViewF (\a -> PROD_LNS (lf a) (lg a)) (f' :*!: g')
allF r (f :+!: g) = do
    ViewF lf f' <- allF r f
    ViewF lg g' <- allF r g
    return $ ViewF (\a -> SUM_LNS (lf a) (lg a)) (f' :+!: g')
allF r (f :@!: g) = do
    ViewF lf f' <- allF r f
    ViewF lg g' <- allF r g
    return $ ViewF (\a -> COMP_LNS (rep (f :@!: g') a) (lf (rep g' a)) (FMAP_LNS f (Fun (rep g a) (rep g' a)) (lg a))) (f' :@!: g')

once :: RuleT -> RuleT
once r (Id a) = mzero
once r (List a) = r (List a) `mplus` (do
	(View f b) <- once r a
	return $ View (MAP_LNS f) (List b))
once r (Prod a b) = r (Prod a b) `mplus` (do
    View f c <- once r a
    return $ View (PROD_LNS f ID_LNS) (Prod c b))
        `mplus` (do
    View g d <- once r b
    return $ View (PROD_LNS ID_LNS g) (Prod a d))
once r (Either a b) = r (Either a b) `mplus` (do
    View f c <- once r a
    return $ View (SUM_LNS f ID_LNS) (Either c b))
    `mplus` (do
    View g d <- once r b
    return $ View (SUM_LNS ID_LNS g) (Either a d))
once r a@(Data s f) = r a `mplus` (do
    ViewF l g <- onceF r f
    Eq <- feq f g
    let anal = (ANA_LNS $ COMP_LNS (rep f a) (l a) OUT_LNS)
    return $ View anal a)
        `mplus` (do
    ViewF l g <- onceF r f
    new <- newData s g
    let anal = ANA_LNS $ COMP_LNS (rep f a) (l a) OUT_LNS
    return $ View anal new)
once r a@(NewData s f) = r a `mplus` (do
    ViewF l g <- onceF r f
    new <- newData s g
    let anal = ANA_LNS $ COMP_LNS (rep f a) (l a) OUT_LNS
    return $ View anal new)
once r a = r a

onceF :: RuleT -> RuleF 
onceF r f = do
	View l ga <- onceF' r f (Id Any)
	FRep g <- inferFctr (Id Any) ga
	return $ ViewF (\b -> unsafeCoerce l) g

onceF' :: RuleT -> Fctr f -> Type a -> RuleTMonad Maybe (View (Rep f a))
onceF' r I a = mzero
onceF' r L a = r (List a)
onceF' r (K t) a = r t `mplus` (do
    View l t' <- once r t
    return $ View l t')
onceF' r (f :*!: g) a = r (rep (f:*!:g) a) `mplus` (do
    View lf b <- onceF' r f a
    return $ View (PROD_LNS lf ID_LNS) $ Prod b (rep g a))
        `mplus` (do
    View lg b <- onceF' r g a
    return $ View (PROD_LNS ID_LNS lg) $ Prod (rep f a) b)
onceF' r (f :+!: g) a = r (rep (f:+!:g) a) `mplus` (do
    View lf b <- onceF' r f a
    return $ View (SUM_LNS lf ID_LNS) $ Either b (rep g a))
        `mplus` (do
    View lg b <- onceF' r g a
    return $ View (SUM_LNS ID_LNS lg) $ Either (rep f a) b)
onceF' r (f :@!: g) a = r (rep (f:@!:g) a) `mplus` (do
    View lf b <- onceF' r f (rep g a)
    return $ View lf b)
        `mplus` (do
    View lg b <- onceF' r g a
    return $ View (FMAP_LNS f (Fun (rep g a) b) lg) $ rep f b)

-- ** Normalized type equality

normalizetype :: RuleT
normalizetype = many (once normalizetyperules)

normalizetyperules :: RuleT
normalizetyperules = prodAssoc ||| sumAssoc

normalizedteq :: Type a -> Type b -> Bool
normalizedteq a b = let dyna = transformtype a normalizetype
                        dynb = transformtype b normalizetype
                    in applyDynT2 (\a b -> teqBool (replacedyn a) b) dyna dynb
	
-- ** Normalization

normalize :: RuleT
normalize = many (once normalizerules)

normalizerules :: RuleT
normalizerules = prodAssoc ||| prodOne ||| listOne ||| filterOne
             ||| sumAssoc ||| eitherSame ||| listList

prodOne :: RuleT
prodOne (Prod a One) = return $ View (FST_LNS BANG) a
prodOne (Prod One a) = return $ View (SND_LNS BANG) a
prodOne _ = mzero

listOne :: RuleT
listOne (Either (List a) One) = do
    l <- lensify (Fun (Either (List a) One) (List a)) (ID `EITHER` ZERO)
    return $ View l (List a)
listOne (Either One (List a)) = do
    l <- lensify (Fun (Either One (List a)) (List a)) (ZERO `EITHER` ID)
    return $ View l (List a)
listOne _ = mzero

filterOne :: RuleT
filterOne (List (Either a One)) = return $ View FILTER_LEFT_LNS (List a)
filterOne (List (Either One a)) = return $ View FILTER_RIGHT_LNS (List a)
filterOne (List a@(Data _ _)) = filterOne' (List a)
filterOne (List a@(NewData _ _)) = filterOne' (List a)
filterOne _ = mzero

filterOne' :: (Mu a,Functor (PF a)) => Type [a] -> RuleTMonad Maybe (View [a])
filterOne' (List a@(dataNameFctr -> Just (n,f :+!: K One))) = do
    guard $ Prelude.not $ isRec f
    new <- newData n f
    Eq <- teq (rep f a) (rep f new)
    let l = COMP_LNS (List $ rep f a) (MAP_LNS INN_LNS) $ COMP_LNS (List $ rep (f :+!: K One) a) FILTER_LEFT_LNS (MAP_LNS OUT_LNS)
    return $ View l $ List new
filterOne' _ = mzero

eitherSame :: RuleT
eitherSame (Either a a') = do
    Eq <- teq a a'
    return $ View (ID_LNS .\/<< ID_LNS) a
eitherSame _ = mzero

listList :: RuleT
listList (List (List a)) = return $ View CONCAT_LNS (List a)
listList _ = mzero

prodAssoc :: RuleT
prodAssoc (Prod (Prod a b) c) = return $ View ASSOCR_LNS (Prod a (Prod b c))
prodAssoc _ = mzero

sumAssoc :: RuleT
sumAssoc (Either (Either a b) c) = return $ View COASSOCR_LNS (Either a (Either b c))
sumAssoc _ = mzero