{-# OPTIONS -fglasgow-exts #-}
module Rewriting where

import Prelude hiding (all)

import Data.Set (Set)
import Data.Map (Map)
import Control.Monad.State

import PType

import Data.Transform.Type
import Data.Transform.RulesPF (simplifypf)
import Dynamics
import PFIsomorphisms
    
-----------------------------------------------------------------------------
-- * Encapsulation of type-changing transformations

-- | Pairs of bi-directional value-level data transformation functions.
data Rep a b = Rep {to :: PF (a -> b), from :: PF (b -> a)}

data View a where
    View :: Rep a b -> Type b -> PFctr -> View (Type a)

instance Show (View a) where
    show (View r b fc) = "(View (Rep <to>:"++show (to r)++" <from>: "++show (from r)++") "++(show b)++") with "++show fc

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

-- | Type-changing rewrite rules.
type Rule = MonadPlus m => (forall a . Type a -> PFctr -> m (View (Type a)))


----------------------------------------
-- ** Value-level combinators used to define two-level combinators.

idrep :: Rep a a
idrep = Rep {to = ID, from = ID}

comprep :: Type b -> Rep a b -> Rep b c -> Rep a c
comprep b f g = Rep {from = COMP b (from f) (from g), to = COMP b (to g) (to f)}

prodmaprep :: Rep a b -> Rep c d -> Rep (a,c) (b,d)
prodmaprep f g = Rep {to = PROD (to f) (to g), from = PROD (from f) (from g)}

summaprep :: Rep a b -> Rep c d -> Rep (Either a c) (Either b d)
summaprep f g = Rep {to = SUM (to f) (to g), from = SUM (from f) (from g)}

listmaprep :: Rep a b -> Rep [a] [b]
listmaprep f = Rep {to = LIST (to f), from = LIST (from f)}

setmaprep :: Rep a b -> Rep (Set a) (Set b)
setmaprep f = Rep {to = SET (to f), from = SET (from f)}

mapmaprep :: Rep b c -> Rep (Map a b) (Map a c)
mapmaprep f = Rep {to = MAP (to f), from = MAP (from f)}

mapkeysrep :: Rep a b -> Rep (Map a c) (Map b c)
mapkeysrep f = Rep {to = MAPKEYS (to f), from = MAPKEYS (from f)}

-----------------------------------------------------------------------------
-- * Strategy combinators for two-level transformations

-- | Sequential composition.
(>>>) :: Rule -> Rule -> Rule
(f >>> g) a fc1 = do 
  View r b fc2 <- f a fc1
  View s c fc3 <- g b fc2
  return (View (comprep b r s) c fc3)

-- | Left-biased choice.
(|||) :: Rule -> Rule -> Rule
(f ||| g) x fc = f x fc `mplus` g x fc

-- | Do-nothing operation. 
--   Unit for sequential composition. 
--   Left-zero and right-unit for left-biased choice.
nop :: Rule
nop x fc = return (View idrep x fc)

-- | Repeat until failure.
--   Zero or more repetitions.
many :: Rule -> Rule
many r = (r >>> many r) ||| nop

-- | Apply argument rule exactly once, at arbitrary depth.
once :: Rule -> Rule
once r (Either a b) fc@(fc1 ::+:: fc2) = r (Either a b) fc `mplus`
                      (do View s c tfc1 <- once r a fc1
                          return (View (summaprep s idrep) (Either c b) (tfc1 ::+:: fc2))) `mplus`
                      (do View s c tfc2 <- once r b fc2
                          return (View (summaprep idrep s) (Either a c) (fc1 ::+:: tfc2)))
once r (Prod a b) fc@(fc1 ::*:: fc2) = r (Prod a b) fc `mplus`
                    (do View s c tfc1 <- once r a fc1
                        return (View (prodmaprep s idrep) (Prod c b) (tfc1 ::*:: fc2))) `mplus`
                    (do View s c tfc2 <- once r b fc2
                        return (View (prodmaprep idrep s) (Prod a c) (fc1 ::*:: tfc2)))
once r x fc = r x fc

try :: Rule -> Rule
try r = r ||| nop

everywhere :: Rule -> Rule
everywhere r = all (everywhere r) >>> r

all :: Rule -> Rule
all r (Either a b) (fc1 ::+:: fc2) = do
  View rep1 ta tfc1 <- r a fc1
  View rep2 tb tfc2 <- r b fc2
  return $ View (summaprep rep1 rep2) (Either ta tb) (tfc1 ::+:: tfc2)
all r (Prod a b) (fc1 ::*:: fc2) = do
  View rep1 ta tfc1 <- r a fc1
  View rep2 tb tfc2 <- r b fc2
  return $ View (prodmaprep rep1 rep2) (Prod ta tb) (tfc1 ::*:: tfc2)
all r t fc = return $ View idrep t fc
  
-----------------------------------------------------------------------------
-- * Unleashing composed data migration functions
{-
-- | Apply the forward value-level function masked by a view.
forth :: View (Type a) -> Type b -> a -> Maybe b
forth (View rep tb') tb a = do {Eq <- teq tb tb'; return (eval (to rep) a)}

-- | Apply the backward value-level function masked by a view.
back :: View (Type a) -> Type b -> b -> Maybe a
back (View rep tb') tb b = do {Eq <- teq tb tb'; return (eval (from rep) b)}

-- | Take the representations of forward and backward value-level 
--   functions out of a view.
unView :: View (Type a) -> Type b -> Maybe (PF (a->b), PF (b->a))
unView (View (Rep to fro) tb') tb = do
  Eq <- teq tb tb'
  return (to,fro)
-}

-- Rules
swap :: Rule
swap (a `Prod` b) (f ::*:: g) =
	return $ View (Rep swapiso swapiso) (b `Prod` a) (g ::*:: f)
swap _ _ = mzero

coswap :: Rule
coswap (a `Either` b) (f ::+:: g) =
	return $ View (Rep coswapiso coswapiso) (b `Either` a) (g ::+:: f)
coswap _ _ = mzero

assocr :: Rule
assocr ((a `Prod` b) `Prod` c) ((f ::*:: g) ::*:: h) =
	return $ View (Rep (assocriso a b c) (assocliso a b c)) (a `Prod` (b `Prod` c)) (f ::*:: (g ::*:: h))
assocr _ _ = mzero

assocl :: Rule
assocl (a `Prod` (b `Prod` c)) (f ::*:: (g ::*:: h)) =
	return $ View (Rep (assocliso a b c) (assocriso a b c)) ((a `Prod` b) `Prod` c) ((f ::*:: g) ::*:: h)
assocl _ _ = mzero

coassocr :: Rule
coassocr ((a `Either` b) `Either` c) ((f ::+:: g) ::+:: h) =
	return $ View (Rep (coassocriso a b c) (coassocliso a b c)) (a `Either` (b `Either` c)) (f ::+:: (g ::+:: h))
coassocr _ _ = mzero

coassocl :: Rule
coassocl (a `Either` (b `Either` c)) (f ::+:: (g ::+:: h)) =
	return $ View (Rep (coassocliso a b c) (coassocriso a b c)) ((a `Either` b) `Either` c) ((f ::+:: g) ::+:: h)
coassocl _ _ = mzero

distr :: Rule
distr (a `Prod` (b `Either` c)) (f ::*:: (g ::+:: h)) =
	return $ View (Rep (distriso a b c) undistriso) ((a `Prod` b) `Either` (a `Prod` c)) ((f ::*:: g) ::+:: (f ::*:: h))
distr _ _ = mzero

distl :: Rule
distl ((a `Either` b) `Prod` c) ((f ::+:: g) ::*:: h) =
	return $ View (Rep (distliso a b c) undistliso) ((a `Prod` c) `Either` (b `Prod` c)) ((f ::*:: h) ::+:: (g ::*:: h))
distl _ _ = mzero

prodone :: Rule
prodone (One `Prod` a) (f ::*:: g) = return $ View (Rep SND (BANG `SPLIT` ID)) a g
prodone (a `Prod` One) (f ::*:: g) = return $ View (Rep FST (ID `SPLIT` BANG)) a f
prodone _ _ = mzero

sortstep :: Rule
sortstep (a `Either` (b `Either` c)) (f ::+:: (g ::+:: h))
	| ids f > ids g || ids f == ids g && mus f > mus g =
        let to = (COMP (b `Either` a) (ID `SUM` INL) INR) `EITHER` (ID `SUM` INR)
            from = (COMP (a `Either` b) (ID `SUM` INL) INR) `EITHER` (ID `SUM` INR) in
        return $ View (Rep to from) (b `Either` (a `Either` c)) (g ::+:: (f ::+:: h))
sortstep t@(a `Either` b) fc@(f ::+:: g) | ids f > ids g || ids f == ids g && mus f > mus g = coswap t fc
sortstep (a `Prod` (b `Prod` c)) (f ::*:: (g ::*:: h))
	| ids f > ids g || ids f == ids g && mus f > mus g =
        let to = (COMP (b `Prod` c) FST SND) `SPLIT` (ID `PROD` SND)
            from = (COMP (a `Prod` c) FST SND) `SPLIT` (ID `PROD` SND) in
        return $ View (Rep to from) (b `Prod` (a `Prod` c)) (g ::*:: (f ::*:: h))
sortstep t@(a `Prod` b) fc@(f ::*:: g) | ids f > ids g || ids f == ids g && mus f > mus g = swap t fc
sortstep _ _ = mzero

groupstep :: Rule
groupstep t@(a `Either` (b `Either` c)) fc@(f ::+:: (g ::+:: h)) | ids f + ids g == 0 = coassocl t fc
groupstep t@(a `Prod` (b `Prod` c)) fc@(f ::*:: (g ::*:: h)) | ids f + ids g == 0 = assocl t fc
groupstep _ _ = mzero


flatten :: Rule
flatten = many (once (distr ||| distl)) >>> many (once prodone)

sort :: Rule
sort = many (once sortstep)

assocs :: Rule
assocs = many (once (coassocr ||| assocr))

group :: Rule
group = many (once groupstep)

-- Usage
use :: MonadPlus m => Rule -> Type a -> PFctr -> m (DynTransf, PFctr)
use r t1 fc1 = do
  View rep t2 fc2 <- r t1 fc1
  return $ (DynTransf (t1 `Func` t2) (simplifypf (t1 `Func` t2) (to rep)) (simplifypf (t2 `Func` t1) (from rep)), fc2)

normalize :: MonadPlus m => Type a -> PFctr -> m (DynTransf, PFctr)
normalize = use (flatten >>> assocs >>> sort >>> group)

-- auxiliars
ids :: PFctr -> Int
ids PId = 1
ids (f ::+:: g) = ids f + ids g
ids (f ::*:: g) = ids f + ids g
ids _ = 0

mus :: PFctr -> Int
mus (PK (PMu _)) = 1
mus (f ::+:: g) = mus f + mus g
mus (f ::*:: g) = mus f + mus g
mus _ = 0

data DynTransf where
        DynTransf :: Type (a -> b) -> PF (a -> b) -> PF (b -> a) -> DynTransf

instance Show DynTransf where
        show (DynTransf t pfto pffrom) = "to:"++show pfto++" from:"++show pffrom++ " of type "++show t

-- examples
tex1 a = Int `Prod` (((a `Either` One) `Prod` a) `Either` Char)
ex1 = PK PInt ::*::
	   (((PId ::+:: PK POne) ::*:: PId) ::+:: PK PChar)

tex2 a = a `Either` (Int `Either` (tex1 a))
ex2 = PId ::+:: (PK PInt ::+:: ex1)