{-# LANGUAGE TypeFamilies, EmptyDataDecls, GADTs, 
             ScopedTypeVariables,
             PatternSignatures,
             RankNTypes,
             MultiParamTypeClasses, NoMonomorphismRestriction #-}
{-# OPTIONS_GHC -Wall -fno-warn-name-shadowing #-}
module Data.Cursor.CLASE.Language where

import Data.Cursor.CLASE.Util
import Data.Maybe
import Control.Monad

{- Directions -}
data Up
data Down

type family Invert d :: *

type instance Invert Up = Down
type instance Invert Down = Up

data DirectionT a where
  UpT   :: DirectionT Up
  DownT :: DirectionT Down


{- Reify -} 
class Reify l a where
  reify :: a -> TypeRep l a

data ExistsR l (r :: * -> *) where
  ExistsR :: (Reify l a) => r a -> ExistsR l r

{- Language -}
class Language l where
  data Context l :: * -> * -> *
  data Movement l :: * -> * -> * -> *
  data TypeRep l :: * -> *

  buildOne :: Context l a b -> a -> b

  unbuildOne :: Movement l Down a b -> a -> Maybe (Context l b a, b)

  invertMovement :: Movement l d a b -> Movement l (Invert d) b a
  
  movementEq :: Movement l d a b -> Movement l d a c -> Maybe (TyEq b c)

  reifyDirection :: Movement l d a b -> DirectionT d

  contextToMovement :: Context l a b -> Movement l Up a b

  
  downMoves :: TypeRep l a -> [ExistsR l (Movement l Down a)]
  moveLeft  :: Movement l Down a x -> Maybe (ExistsR l (Movement l Down a))
  moveRight :: Movement l Down a x -> Maybe (ExistsR l (Movement l Down a))


contextMovementEq :: (Language l) => Context l a b -> Movement l Up a c -> Maybe (TyEq b c)
contextMovementEq context mov = (contextToMovement context) `movementEq` mov

{- Paths -}
infixr 5 `Step`

data Path l r a b where
  Stop :: Path l r a a
  Step :: (Reify l b) => r a b -> Path l r b c -> Path l r a c

foldPath :: (forall from to . (Reify l to) => r from to -> from -> to) -> start -> Path l r start finish -> finish
foldPath _ val Stop = val
foldPath step val (Step ng np) = foldPath step (step ng val) np 


{- Cursor -}
data Cursor l x a = (Reify l a) => Cursor { 
    it :: a,
    ctx :: Path l (Context l) a l,
    log :: Route l a x
  }

data CursorWithMovement l d x from where
  CWM :: (Reify l to) => Cursor l x to -> Movement l d from to -> CursorWithMovement l d x from

rebuild :: (Language l) => Cursor l x a -> l
rebuild cursor = foldPath buildOne (it cursor) (ctx cursor) 

applyMovement :: (Language l, Reify l a, Reify l b) => 
                 Movement l d a b -> Cursor l x a -> Maybe (Cursor l x b)
applyMovement mov (Cursor it ctx log) = case (reifyDirection mov) of
  UpT   -> case ctx of
    (Step up ups) -> case (up `contextMovementEq` mov) of
      Just Eq -> Just $ Cursor (buildOne up it) ups (updateRoute mov log)
      Nothing -> Nothing
    Stop -> Nothing
  DownT -> fmap (\(ctx', it') -> Cursor it' (Step ctx' ctx) (updateRoute mov log)) 
                (unbuildOne mov it)

genericMoveUp :: (Language l) => Cursor l x a -> Maybe (CursorWithMovement l Up x a) 
genericMoveUp (Cursor it (Step up ups) log) = Just $ CWM (Cursor (buildOne up it) ups (updateRoute upMov log)) upMov
  where
    upMov = contextToMovement up
genericMoveUp (Cursor _ Stop _) = Nothing

genericMoveDown :: (Language l) => Cursor l x a -> Maybe (CursorWithMovement l Down x a)
genericMoveDown cursor@Cursor {} = msum . map (\(ExistsR c) -> fmap (flip CWM c) . flip applyMovement cursor $ c) . downMoves . reify . it $ cursor

genericMoveLeft  :: (Language l) => Cursor l x a -> Maybe (ExistsR l (Cursor l x)) 
genericMoveLeft = genericMoveSideways moveLeft 

genericMoveRight :: (Language l) => Cursor l x a -> Maybe (ExistsR l (Cursor l x)) 
genericMoveRight = genericMoveSideways moveRight

genericMoveSideways :: forall l x a . (Language l) => 
                       (forall a z . Movement l Down a z -> Maybe (ExistsR l (Movement l Down a))) -> Cursor l x a -> Maybe (ExistsR l (Cursor l x)) 
genericMoveSideways fn cursor = do
  (CWM cursor' upmov ) <- genericMoveUp cursor
  let downmov = invertMovement upmov
  (ExistsR newDownMov) <- fn downmov
  cursor'' <- applyMovement newDownMov cursor'
  return $ ExistsR cursor''

moveToRoot :: (Language l) => Cursor l x a -> Cursor l x l
moveToRoot cursor@(Cursor _ Stop _)      = cursor
moveToRoot (Cursor it (Step up ups) log) = moveToRoot (Cursor (buildOne up it) ups (updateRoute (contextToMovement up) log))

{- Routes -}
data Route l from to where
  Route :: (Reify l mid) => Path l (Movement l Up) from mid ->
                            Path l (Movement l Down) mid to -> Route l from to 


route_invariant :: forall l from to . (Language l) => Route l from to -> Bool
route_invariant (Route (Step mup   Stop) 
                       (Step mdown _)) = not . isJust $ res
  where
    mup' = invertMovement mup
    res = (mup' `movementEq` mdown)
route_invariant (Route (Step _ ups) downs) = route_invariant (Route ups downs)
route_invariant (Route Stop _) = True

updateRoute :: (Language l, 
                Reify l a, 
                Reify l b) => Movement l d a b -> Route l a c -> Route l b c
updateRoute mov route = case (reifyDirection mov) of
  UpT   -> case route of
    Route (Step up ups) downs -> case (mov `movementEq` up) of
      Just Eq -> Route ups downs
      Nothing -> error $ "Precondition violation: route up =/= movement up!"
    Route Stop steps -> Route Stop (Step (invertMovement mov) steps)
  DownT -> case route of
    Route Stop sdowns@(Step down downs) -> case (mov `movementEq` down) of
      Just Eq -> Route Stop downs
      Nothing -> Route (Step (invertMovement mov) Stop) sdowns
    Route ups downs -> Route (Step (invertMovement mov) ups) downs

resetLog :: Cursor l x a -> Cursor l a a
resetLog (Cursor it ctx _) = (Cursor it ctx (Route Stop Stop))

appendRoute :: (Language l, Reify l a, Reify l b, Reify l c) => 
                Route l a b -> Route l b c -> Route l a c
appendRoute (Route Stop Stop) x = x
appendRoute (Route (Step up rst) y) r2 = updateRoute (invertMovement up)
                                                     (appendRoute (Route rst y) r2)
appendRoute (Route Stop (Step dwn rst)) r2 = updateRoute (invertMovement dwn) 
                                                         (appendRoute (Route Stop rst) r2)

followRoute :: (Language l) => Cursor l x a -> Route l a c -> Maybe (Cursor l x c)
followRoute cursor (Route Stop Stop) = Just $ cursor
followRoute cursor@Cursor{} route@(Route (Step mup _) _)      = (applyMovement mup cursor)   >>= (\cursor'   -> followRoute cursor' (updateRoute mup route))
followRoute cursor@Cursor{} route@(Route Stop (Step mdown _)) = (applyMovement mdown cursor) >>= (\cursor' -> followRoute cursor' (updateRoute mdown route))