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 { TimeOut -> Int
getTimeOut :: Int } -- in ms

instance Show TimeOut where
  show :: TimeOut -> String
show = Int -> String
forall a. Show a => a -> String
show (Int -> String) -> (TimeOut -> Int) -> TimeOut -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TimeOut -> Int
getTimeOut

-- | Options for Auto, default value and lenses

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

initAutoOptions :: AutoOptions
initAutoOptions :: AutoOptions
initAutoOptions = AutoOptions :: Hints -> TimeOut -> Int -> Mode -> AutoHintMode -> AutoOptions
AutoOptions
  { autoHints :: Hints
autoHints    = []
  , autoTimeOut :: TimeOut
autoTimeOut  = Int -> TimeOut
TimeOut 1000
  , autoPick :: Int
autoPick     = 0
  , autoMode :: Mode
autoMode     = Bool -> Bool -> Mode
MNormal Bool
False Bool
False
  , autoHintMode :: AutoHintMode
autoHintMode = AutoHintMode
AHMNone
  }

aoHints :: Lens' Hints AutoOptions
aoHints :: (Hints -> f Hints) -> AutoOptions -> f AutoOptions
aoHints f :: Hints -> f Hints
f s :: AutoOptions
s =
  Hints -> f Hints
f (AutoOptions -> Hints
autoHints AutoOptions
s) f Hints -> (Hints -> AutoOptions) -> f AutoOptions
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&>
  \x :: Hints
x -> AutoOptions
s {autoHints :: Hints
autoHints = Hints
x}

aoTimeOut :: Lens' TimeOut AutoOptions
aoTimeOut :: (TimeOut -> f TimeOut) -> AutoOptions -> f AutoOptions
aoTimeOut f :: TimeOut -> f TimeOut
f s :: AutoOptions
s =
  TimeOut -> f TimeOut
f (AutoOptions -> TimeOut
autoTimeOut AutoOptions
s) f TimeOut -> (TimeOut -> AutoOptions) -> f AutoOptions
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&>
  \x :: TimeOut
x -> AutoOptions
s {autoTimeOut :: TimeOut
autoTimeOut = TimeOut
x}

aoPick :: Lens' Int AutoOptions
aoPick :: (Int -> f Int) -> AutoOptions -> f AutoOptions
aoPick f :: Int -> f Int
f s :: AutoOptions
s =
  Int -> f Int
f (AutoOptions -> Int
autoPick AutoOptions
s) f Int -> (Int -> AutoOptions) -> f AutoOptions
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&>
  \x :: Int
x -> AutoOptions
s {autoPick :: Int
autoPick = Int
x}

aoMode :: Lens' Mode AutoOptions
aoMode :: (Mode -> f Mode) -> AutoOptions -> f AutoOptions
aoMode f :: Mode -> f Mode
f s :: AutoOptions
s =
  Mode -> f Mode
f (AutoOptions -> Mode
autoMode AutoOptions
s) f Mode -> (Mode -> AutoOptions) -> f AutoOptions
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&>
  \x :: Mode
x -> AutoOptions
s {autoMode :: Mode
autoMode = Mode
x}

aoHintMode :: Lens' AutoHintMode AutoOptions
aoHintMode :: (AutoHintMode -> f AutoHintMode) -> AutoOptions -> f AutoOptions
aoHintMode f :: AutoHintMode -> f AutoHintMode
f s :: AutoOptions
s =
  AutoHintMode -> f AutoHintMode
f (AutoOptions -> AutoHintMode
autoHintMode AutoOptions
s) f AutoHintMode -> (AutoHintMode -> AutoOptions) -> f AutoOptions
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&>
  \x :: AutoHintMode
x -> AutoOptions
s {autoHintMode :: AutoHintMode
autoHintMode = 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 :: Hints -> [AutoToken]
autoTokens []              = []
autoTokens ("-t" : t :: String
t : ws :: Hints
ws) = String -> AutoToken
T String
t        AutoToken -> [AutoToken] -> [AutoToken]
forall a. a -> [a] -> [a]
: Hints -> [AutoToken]
autoTokens Hints
ws
autoTokens ("-s" : s :: String
s : ws :: Hints
ws) = Int -> AutoToken
S (String -> Int
forall a. Read a => String -> a
read String
s) AutoToken -> [AutoToken] -> [AutoToken]
forall a. a -> [a] -> [a]
: Hints -> [AutoToken]
autoTokens Hints
ws
autoTokens ("-l"     : ws :: Hints
ws) = AutoToken
L          AutoToken -> [AutoToken] -> [AutoToken]
forall a. a -> [a] -> [a]
: Hints -> [AutoToken]
autoTokens Hints
ws
autoTokens ("-d"     : ws :: Hints
ws) = AutoToken
D          AutoToken -> [AutoToken] -> [AutoToken]
forall a. a -> [a] -> [a]
: Hints -> [AutoToken]
autoTokens Hints
ws
autoTokens ("-m"     : ws :: Hints
ws) = AutoToken
M          AutoToken -> [AutoToken] -> [AutoToken]
forall a. a -> [a] -> [a]
: Hints -> [AutoToken]
autoTokens Hints
ws
autoTokens ("-c"     : ws :: Hints
ws) = AutoToken
C          AutoToken -> [AutoToken] -> [AutoToken]
forall a. a -> [a] -> [a]
: Hints -> [AutoToken]
autoTokens Hints
ws
autoTokens ("-r"     : ws :: Hints
ws) = AutoToken
R          AutoToken -> [AutoToken] -> [AutoToken]
forall a. a -> [a] -> [a]
: Hints -> [AutoToken]
autoTokens Hints
ws
autoTokens (h :: String
h        : ws :: Hints
ws) = String -> AutoToken
H String
h        AutoToken -> [AutoToken] -> [AutoToken]
forall a. a -> [a] -> [a]
: Hints -> [AutoToken]
autoTokens Hints
ws

parseTime :: String -> Int
parseTime :: String -> Int
parseTime [] = 0
parseTime xs :: String
xs = String -> Int
forall a. Read a => String -> a
read String
ds Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
modifier Int -> Int -> Int
forall a. Num a => a -> a -> a
+ String -> Int
parseTime String
r where
  (ds :: String
ds , modr :: String
modr) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isDigit String
xs
  (mod :: String
mod , r :: String
r)   = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isDigit) String
modr

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

parseArgs :: String -> AutoOptions
parseArgs :: String -> AutoOptions
parseArgs s :: String
s = (AutoToken -> StateT AutoOptions Identity ())
-> [AutoToken] -> StateT AutoOptions Identity ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ AutoToken -> StateT AutoOptions Identity ()
step (Hints -> [AutoToken]
autoTokens (Hints -> [AutoToken]) -> Hints -> [AutoToken]
forall a b. (a -> b) -> a -> b
$ String -> Hints
words String
s)
              StateT AutoOptions Identity () -> AutoOptions -> AutoOptions
forall s a. State s a -> s -> s
`execState` AutoOptions
initAutoOptions where

  step :: AutoToken -> State AutoOptions ()
  step :: AutoToken -> StateT AutoOptions Identity ()
step M     = Lens' AutoHintMode AutoOptions
aoHintMode Lens' AutoHintMode AutoOptions
-> AutoHintMode -> StateT AutoOptions Identity ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= AutoHintMode
AHMModule
  step C     = Lens' Mode AutoOptions
aoMode     Lens' Mode AutoOptions -> Mode -> StateT AutoOptions Identity ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= Mode
MCaseSplit
  step R     = Lens' Int AutoOptions
aoPick     Lens' Int AutoOptions -> Int -> StateT AutoOptions Identity ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= (-1)
            StateT AutoOptions Identity ()
-> StateT AutoOptions Identity () -> StateT AutoOptions Identity ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Lens' Mode AutoOptions
aoMode     Lens' Mode AutoOptions -> Mode -> StateT AutoOptions Identity ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= Bool -> Mode
MRefine Bool
False
  step (T t :: String
t) = Lens' TimeOut AutoOptions
aoTimeOut  Lens' TimeOut AutoOptions
-> TimeOut -> StateT AutoOptions Identity ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= Int -> TimeOut
TimeOut (String -> Int
parseTime String
t)
  step (S p :: Int
p) = Lens' Int AutoOptions
aoPick     Lens' Int AutoOptions -> Int -> StateT AutoOptions Identity ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= Int
p
  step (H h :: String
h) = Lens' Hints AutoOptions
aoHints    Lens' Hints AutoOptions
-> (Hints -> Hints) -> StateT AutoOptions Identity ()
forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (i -> i) -> m ()
%= (String
h String -> Hints -> Hints
forall a. a -> [a] -> [a]
:)
  step D     = do
    Mode
mode <- Lens' Mode AutoOptions -> StateT AutoOptions Identity Mode
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' Mode AutoOptions
aoMode
    case Mode
mode of
      MNormal lm :: Bool
lm _ -> Lens' Mode AutoOptions
aoMode Lens' Mode AutoOptions -> Mode -> StateT AutoOptions Identity ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= Bool -> Bool -> Mode
MNormal Bool
lm Bool
True
      _            -> () -> StateT AutoOptions Identity ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  step L     = do
    Mode
mode <- Lens' Mode AutoOptions -> StateT AutoOptions Identity Mode
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' Mode AutoOptions
aoMode
    case Mode
mode of
      MNormal _ dp :: Bool
dp -> Lens' Mode AutoOptions
aoMode Lens' Mode AutoOptions -> Mode -> StateT AutoOptions Identity ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= Bool -> Bool -> Mode
MNormal Bool
True Bool
dp
      MRefine _    -> Lens' Mode AutoOptions
aoMode Lens' Mode AutoOptions -> Mode -> StateT AutoOptions Identity ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= Bool -> Mode
MRefine Bool
True
      _            -> () -> StateT AutoOptions Identity ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()