{-# OPTIONS_GHC -Wunused-imports #-}

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
  { 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' AutoOptions Hints
aoHints :: Lens' AutoOptions Hints
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 = x}

aoTimeOut :: Lens' AutoOptions TimeOut
aoTimeOut :: Lens' AutoOptions TimeOut
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 = x}

aoPick :: Lens' AutoOptions Int
aoPick :: Lens' AutoOptions Int
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 = x}

aoMode :: Lens' AutoOptions Mode
aoMode :: Lens' AutoOptions Mode
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 = x}

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