Play idris on haskell

idris.hs

{-# LANGUAGE TypeInType #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ExistentialQuantification #-}
module Main where

import System.IO
import Data.IORef
import Data.Char
import Data.Singletons.TH
import Control.Concurrent
import Control.Monad


$(singletons [d|
  data EditorState = Adding | Subtracting

  data Key = Kq | Kt | Kd | K0 | K1 | K2 | K3 | K4 | K5 | K6 | K7 | K8 | K9

  toggle :: EditorState -> EditorState
  toggle Adding = Subtracting
  toggle Subtracting = Adding

  |])

toKey :: Char -> Maybe Key
toKey 'q' = Just Kq
toKey 't' = Just Kt
toKey '0' = Just K0
toKey '1' = Just K1
toKey '2' = Just K2
toKey '3' = Just K3
toKey '4' = Just K4
toKey '5' = Just K5
toKey '6' = Just K6
toKey '7' = Just K7
toKey '8' = Just K8
toKey '9' = Just K9
toKey _   = Nothing



type family Interpret e p :: Maybe EditorState where
  Interpret _ Kq = Nothing
  Interpret t Kt = Just (Toggle t)
  Interpret t _  = Just t

newtype Model = M {unM::Int} deriving ( Show, Num)

data State = S EditorState Model

data NextState (x :: Maybe EditorState) where
  Next :: Sing k -> Model -> NextState (Just k)
  Stop :: NextState Nothing

constr :: NextState x -> Maybe State
constr (Next s m) = Just (S (fromSing s) m) -- FIXME: looks like it unsafe
constr Stop       = Nothing

withSomeKey :: Key -> (forall (k::Key) . Sing k -> r) -> r
withSomeKey = withSomeSing

withSomeState :: State -> (forall (k::EditorState) . Model -> Sing k -> r) -> r
withSomeState (S s m) f = withSomeSing s (f m)

runProcessKeyboard
  :: State
  -> Key
  -> (forall (k::Key) (s::EditorState) . Sing k -> Model -> Sing s -> NextState (Interpret s k))
  -> Maybe State
runProcessKeyboard st k f = withSomeKey k (\sk -> withSomeState st ((constr .). f sk))


internalProcessKeyboard :: Sing k -> Model -> Sing s -> NextState (Interpret s k)
internalProcessKeyboard sk m@(M t) ss = case sk of
                                         SKq -> Stop
                                         SKt -> Next (sToggle ss) m
                                         SK0 -> Next ss (action 0)
                                         SK1 -> Next ss (action 1)
                                         SK2 -> Next ss (action 2)
                                         SK3 -> Next ss (action 3)
                                         SK4 -> Next ss (action 4)
                                         SK5 -> Next ss (action 5)
                                         SK6 -> Next ss (action 6)
                                         SK7 -> Next ss (action 7)
                                         SK8 -> Next ss (action 8)
                                         SK9 -> Next ss (action 9)
    where
      action :: Int -> Model
      action i = case ss of
                   SAdding -> M $ t + i
                   SSubtracting -> M $ t - i


processKeyboard :: State -> Char -> Maybe State
processKeyboard s c = case toKey c of
   Nothing -> Just s
   Just k  -> runProcessKeyboard s k internalProcessKeyboard


render :: State -> String
render (S Adding (M n)) =  show n ++ " (adding)"
render (S Subtracting (M n)) =  show n ++ " (subtracting)"

data Event = Keyboard Char | Show deriving ( Eq)

processEvent :: IORef State -> Event -> IO Bool
processEvent stateRef event = do
    s <- readIORef stateRef
    case event of
     Show -> putStrLn (render s) >> return True
     Keyboard c -> case processKeyboard s c of
                     Nothing -> pure False
                     Just s  -> writeIORef stateRef s >> pure True

eventLoop :: IORef State -> Chan Event -> IO ()
eventLoop stateRef queueRef = do
    event <- readChan queueRef
    cont <- processEvent stateRef event
    when cont $ eventLoop stateRef queueRef

main :: IO ()
main = do
    hSetBuffering stdin NoBuffering
    stateRef <- newIORef (S Adding 4)
    queue <- newChan
    showTimerId <- forkIO $ showTimer queue
    keyboardId <- forkIO $ keyboard queue
    eventLoop stateRef queue
    killThread showTimerId
    killThread keyboardId

keyboard :: Chan Event -> IO ()
keyboard y = do
      d <- getChar
      putStr "\n"
      writeChan y (Keyboard d)
      keyboard y

showTimer :: Chan Event -> IO ()
showTimer y = do
  writeChan y Show
  threadDelay 1000000
  showTimer y