{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Proof.Assistant.Helpers where

import Control.Concurrent (threadDelay)
import Control.Exception
import Data.Coerce (Coercible, coerce)
import Data.Char (isSpace)
import Data.ByteString (ByteString)
import Data.Text (Text)
import Dhall (Natural)

import Proof.Assistant.Settings (Time (..))

import qualified Data.ByteString.Char8 as BS8
import qualified Data.Text as Text
import qualified Data.Text.Encoding as Text

-- | Cast something to 'Int'.
toInt :: forall a b. (Num b, Integral b, Coercible a b) => a -> Int
toInt :: a -> Int
toInt = b -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (b -> Int) -> (a -> b) -> a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coercible a b => a -> b
coerce @_ @b

-- | Cast something to 'String'.
t2s :: Coercible a Text => a -> String
t2s :: a -> String
t2s = Text -> String
Text.unpack (Text -> String) -> (a -> Text) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Text
coerce

-- | Wait N seconds.
asyncWait :: Time -> IO ()
asyncWait :: Time -> IO ()
asyncWait Time
n = Int -> IO ()
threadDelay (Time -> Int
forall a b. (Num b, Integral b, Coercible a b) => a -> Int
toInt @_ @Natural Time
n Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
1000000)

-- | If input starts with @/@ drop the whole command with a space and return the remaining part.
dropCommand :: ByteString -> ByteString
dropCommand :: ByteString -> ByteString
dropCommand ByteString
xs = if Int -> ByteString -> ByteString
BS8.take Int
1 ByteString
xs ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
== ByteString
"/" then ByteString -> ByteString
drop' ByteString
xs else ByteString
xs
  where
    drop' :: ByteString -> ByteString
drop' = (Char -> Bool) -> ByteString -> ByteString
BS8.dropWhile Char -> Bool
isSpace (ByteString -> ByteString)
-> (ByteString -> ByteString) -> ByteString -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> ByteString -> ByteString
BS8.dropWhile (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isSpace)

-- | Drop not only command but sub-command too.
dropSubCommand :: ByteString -> ByteString
dropSubCommand :: ByteString -> ByteString
dropSubCommand = ByteString -> ByteString
dropCommand (ByteString -> ByteString)
-> (ByteString -> ByteString) -> ByteString -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
dropCommand

-- | Cast UTF-8 'String' to 'ByteString'.
toBS :: String -> ByteString
toBS :: String -> ByteString
toBS = Text -> ByteString
Text.encodeUtf8 (Text -> ByteString) -> (String -> Text) -> String -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
Text.pack

-- | Cast UTF-8 'ByteString' to 'String'.
fromBS :: ByteString -> String
fromBS :: ByteString -> String
fromBS = Text -> String
Text.unpack (Text -> String) -> (ByteString -> Text) -> ByteString -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Text
Text.decodeUtf8

-- | Cast UTF-8 'ByteString' to 'Text'.
bsToText :: ByteString -> Text
bsToText :: ByteString -> Text
bsToText = ByteString -> Text
Text.decodeUtf8

-- | Cast UTF-8 'ByteString' to 'Text'.
textToBS :: Text -> ByteString
textToBS :: Text -> ByteString
textToBS = Text -> ByteString
Text.encodeUtf8

-- | Cast some exception to 'ByteString'.
processError :: SomeException -> IO ByteString
processError :: SomeException -> IO ByteString
processError (SomeException e
ex) = ByteString -> IO ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> ByteString
toBS (String -> ByteString) -> String -> ByteString
forall a b. (a -> b) -> a -> b
$ e -> String
forall a. Show a => a -> String
show e
ex)

-- | Wrap IO action with 'processError' and return error message as 'ByteString'.
handleErrorMaybe :: IO ByteString -> IO ByteString
handleErrorMaybe :: IO ByteString -> IO ByteString
handleErrorMaybe = (IO ByteString -> (SomeException -> IO ByteString) -> IO ByteString
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` SomeException -> IO ByteString
processError)