{-# LANGUAGE ConstraintKinds            #-}
{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FunctionalDependencies     #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE OverloadedLabels           #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE RebindableSyntax           #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE TypeOperators              #-}

module Main where

import           Prelude

import           Control.Concurrent     (threadDelay)
import           Control.Monad.Indexed
import           Control.Monad.IO.Class
import           Data.Row.Records
import           GHC.OverloadedLabels

import           Motor.FSM

-- * Protocol (Abstract state types)

-- We only use marker types for states in the Door protocol.
data Open
data Closed

class MonadFSM m => Door m where
  -- The associated type lets the instance choose the concrete state
  -- data type.
  type State m :: * -> *

  -- Events:
  initial :: Name n -> Actions m '[ n !+ State m Closed ] r ()
  open :: Name n -> Actions m '[ n := State m Closed !--> State m Open ] r ()
  close :: Name n -> Actions m '[ n := State m Open !--> State m Closed ] r ()
  end :: Name n -> Actions m '[ n !- State m Closed ] r ()

-- * Implemention (Concrete types)
--
-- This could be in another module, hiding the constructors.

newtype ConsoleDoor m (i :: Row *) (o :: Row *) a =
  ConsoleDoor { runConsoleDoor :: FSM m i o a }
  deriving (IxFunctor, IxPointed, IxApplicative, IxMonad, MonadFSM)

run :: Monad m => ConsoleDoor m Empty Empty () -> m ()
run = runFSM . runConsoleDoor

deriving instance Monad m => Functor (ConsoleDoor m i i)
deriving instance Monad m => Applicative (ConsoleDoor m i i)
deriving instance Monad m => Monad (ConsoleDoor m i i)

instance (MonadIO m) => MonadIO (ConsoleDoor m i i) where
  liftIO = ConsoleDoor . liftIO

data DoorState s where
  Open :: DoorState Open
  Closed :: DoorState Closed

instance Show (DoorState s) where
  show Open   = "Open"
  show Closed = "Closed"

logLn :: (MonadIO m) => String -> m ()
logLn = liftIO . putStrLn

logDoor :: (MonadIO m, HasType n (DoorState s) i) => Name n -> ConsoleDoor m i i ()
logDoor n =
    get n
    >>>= \s -> logLn ("Door is now " ++ show s)

-- Extremely boring implementation:
instance (MonadIO m) => Door (ConsoleDoor m) where
  type State (ConsoleDoor m) = DoorState
  initial n = new n Closed
  open n = enter n Open >>> logDoor n
  close n = enter n Closed >>> logDoor n
  end = delete

-- * Runner Program

-- This uses the protocol to define a program using the Door protocol.

sleep :: (MonadIO (m i i)) => Int -> m (i :: Row *) (i :: Row *) ()
sleep seconds = liftIO (threadDelay (seconds * 1000000))

confirm :: (MonadIO (m i i)) => String -> m (i :: Row *) (i :: Row *) Bool
confirm s = liftIO (putStrLn s >> ("y" ==) <$> getLine)

type OpenAndClose m n o c =
    ( Door m
    -- TODO: Can these constraints be added to the Sugar module
    -- automatically?
    , ((n .== State m Open) .// c) ~ o
    , ((n .== State m Closed) .// o) ~ c
    , (o .! n) ~ State m Open
    , (c .! n) ~ State m Closed
    , (o .- n) ~ (c .- n)
    )

type OpenAndCloseIO m n o c =
    ( OpenAndClose m n o c
    , MonadIO (m o o)
    , MonadIO (m c c)
    )

inClosed :: OpenAndCloseIO m n o c => Name n -> m c (c .- n) ()
inClosed door = confirm "Open door?" >>>= \case
  True  -> open door >>>= const (inOpen door)
  False -> end door

inOpen :: OpenAndCloseIO m n o c => Name n -> m o (o .- n) ()
inOpen door = confirm "The door must be closed. OK?" >>>= \case
  True  -> close door >>>= const (inClosed door)
  False -> inOpen door

-- The program initializes a door, and starts the looping between
-- open/closed.
main :: IO ()
main = run $ initial #door >>>= const (inClosed #door)

{- $example-run

Running this program can look like this:

>>> main
Open door?
y
Door is now Open
The door must be closed. OK?
y
Door is now Closed
Open door?
y
Door is now Open
The door must be closed. OK?
n
The door must be closed. OK?
n
The door must be closed. OK?
n
The door must be closed. OK?
y
Door is now Closed
Open door?
n
-}