module Data.Cursor.CLASE.Language where
import Data.Cursor.CLASE.Util
import Data.Maybe
import Control.Monad
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
class Reify l a where
reify :: a -> TypeRep l a
data ExistsR l (r :: * -> *) where
ExistsR :: (Reify l a) => r a -> ExistsR l r
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
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
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))
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))