module Agda.Auto.Options where

import Data.Char
import Control.Monad.State
import Agda.Utils.Lens

data Mode = MNormal Bool Bool -- true if list mode, true if disprove

          | MCaseSplit

          | MRefine Bool -- true if list mode


data AutoHintMode = AHMNone
                  | AHMModule

type Hints = [String]

newtype TimeOut = TimeOut { getTimeOut :: Int } -- in ms

instance Show TimeOut where
  show = show . getTimeOut

-- | Options for Auto, default value and lenses

data AutoOptions = AutoOptions
  { autoHints    :: Hints
  , autoTimeOut  :: TimeOut
  , autoPick     :: Int
  , autoMode     :: Mode
  , autoHintMode :: AutoHintMode
  }

initAutoOptions :: AutoOptions
initAutoOptions = AutoOptions
  { autoHints    = []
  , autoTimeOut  = TimeOut 1000
  , autoPick     = 0
  , autoMode     = MNormal False False
  , autoHintMode = AHMNone
  }

aoHints :: Lens' Hints AutoOptions
aoHints f s =
  f (autoHints s) <&>
  \x -> s {autoHints = x}

aoTimeOut :: Lens' TimeOut AutoOptions
aoTimeOut f s =
  f (autoTimeOut s) <&>
  \x -> s {autoTimeOut = x}

aoPick :: Lens' Int AutoOptions
aoPick f s =
  f (autoPick s) <&>
  \x -> s {autoPick = x}

aoMode :: Lens' Mode AutoOptions
aoMode f s =
  f (autoMode s) <&>
  \x -> s {autoMode = x}

aoHintMode :: Lens' AutoHintMode AutoOptions
aoHintMode f s =
  f (autoHintMode s) <&>
  \x -> s {autoHintMode = x}

-- | Tokenising the input (makes `parseArgs` cleaner)

data AutoToken =
    M | C | R | D | L
  | T String | S Int | H String

autoTokens :: [String] -> [AutoToken]
autoTokens []              = []
autoTokens ("-t" : t : ws) = T t        : autoTokens ws
autoTokens ("-s" : s : ws) = S (read s) : autoTokens ws
autoTokens ("-l"     : ws) = L          : autoTokens ws
autoTokens ("-d"     : ws) = D          : autoTokens ws
autoTokens ("-m"     : ws) = M          : autoTokens ws
autoTokens ("-c"     : ws) = C          : autoTokens ws
autoTokens ("-r"     : ws) = R          : autoTokens ws
autoTokens (h        : ws) = H h        : autoTokens ws

parseTime :: String -> Int
parseTime [] = 0
parseTime xs = read ds * modifier + parseTime r where
  (ds , modr) = span isDigit xs
  (mod , r)   = span (not . isDigit) modr

  modifier = case mod of
    "ms" -> 1
    "cs" -> 10
    "ds" -> 100
    "s"  -> 1000
    _    -> 1000

parseArgs :: String -> AutoOptions
parseArgs s = mapM_ step (autoTokens $ words s)
              `execState` initAutoOptions where

  step :: AutoToken -> State AutoOptions ()
  step M     = aoHintMode .= AHMModule
  step C     = aoMode     .= MCaseSplit
  step R     = aoPick     .= (-1)
            >> aoMode     .= MRefine False
  step (T t) = aoTimeOut  .= TimeOut (parseTime t)
  step (S p) = aoPick     .= p
  step (H h) = aoHints    %= (h :)
  step D     = do
    mode <- use aoMode
    case mode of
      MNormal lm _ -> aoMode .= MNormal lm True
      _            -> return ()
  step L     = do
    mode <- use aoMode
    case mode of
      MNormal _ dp -> aoMode .= MNormal True dp
      MRefine _    -> aoMode .= MRefine True
      _            -> return ()