    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 -> [Char]
    show = Int -> [Char]
    forall a. Show a => a -> [Char]
    show (Int -> [Char]) -> (TimeOut -> Int) -> TimeOut -> [Char]
    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 Int
    1000
      , autoPick :: Int
    autoPick     = Int
    0
      , autoMode :: Mode
    autoMode     = Bool -> Bool -> Mode
    MNormal Bool
    False Bool
    False
      , autoHintMode :: AutoHintMode
    autoHintMode = AutoHintMode
    AHMNone
      }

    aoHints :: Lens' Hints AutoOptions
    aoHints :: Lens' Hints AutoOptions
    aoHints Hints -> f Hints
    f 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
    <&>
      \Hints
    x -> AutoOptions
    s {autoHints :: Hints
    autoHints = Hints
    x}

    aoTimeOut :: Lens' TimeOut AutoOptions
    aoTimeOut :: Lens' TimeOut AutoOptions
    aoTimeOut TimeOut -> f TimeOut
    f 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
    <&>
      \TimeOut
    x -> AutoOptions
    s {autoTimeOut :: TimeOut
    autoTimeOut = TimeOut
    x}

    aoPick :: Lens' Int AutoOptions
    aoPick :: Lens' Int AutoOptions
    aoPick Int -> f Int
    f 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
    <&>
      \Int
    x -> AutoOptions
    s {autoPick :: Int
    autoPick = Int
    x}

    aoMode :: Lens' Mode AutoOptions
    aoMode :: Lens' Mode AutoOptions
    aoMode Mode -> f Mode
    f 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
    <&>
      \Mode
    x -> AutoOptions
    s {autoMode :: Mode
    autoMode = Mode
    x}

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

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

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

    parseArgs :: String -> AutoOptions
    parseArgs :: [Char] -> AutoOptions
    parseArgs [Char]
    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
    $ [Char] -> Hints
    words [Char]
    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 AutoToken
    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 AutoToken
    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 AutoToken
    R     = Lens' Int AutoOptions
    aoPick     Lens' Int AutoOptions -> Int -> StateT AutoOptions Identity ()
    forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
    .= (-Int
    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 [Char]
    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 ([Char] -> Int
    parseTime [Char]
    t)
      step (S 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 [Char]
    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 ()
    %= ([Char]
    h [Char] -> Hints -> Hints
    forall a. a -> [a] -> [a]
    :)
      step AutoToken
    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 Bool
    lm Bool
    _ -> 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
          Mode
    _            -> () -> StateT AutoOptions Identity ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      step AutoToken
    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 Bool
    _ 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 Bool
    _    -> 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
          Mode
    _            -> () -> StateT AutoOptions Identity ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()