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 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 :: (Hints -> f Hints) -> AutoOptions -> f 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 :: (TimeOut -> f TimeOut) -> AutoOptions -> f 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 :: (Int -> f Int) -> AutoOptions -> f 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 :: (Mode -> f Mode) -> AutoOptions -> f 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 :: (AutoHintMode -> f AutoHintMode) -> AutoOptions -> f 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 (String
"-t" : String
t : Hints
ws) = String -> AutoToken
T String
t        AutoToken -> [AutoToken] -> [AutoToken]
forall a. a -> [a] -> [a]
: Hints -> [AutoToken]
autoTokens Hints
ws
autoTokens (String
"-s" : String
s : 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 (String
"-l"     : Hints
ws) = AutoToken
L          AutoToken -> [AutoToken] -> [AutoToken]
forall a. a -> [a] -> [a]
: Hints -> [AutoToken]
autoTokens Hints
ws
autoTokens (String
"-d"     : Hints
ws) = AutoToken
D          AutoToken -> [AutoToken] -> [AutoToken]
forall a. a -> [a] -> [a]
: Hints -> [AutoToken]
autoTokens Hints
ws
autoTokens (String
"-m"     : Hints
ws) = AutoToken
M          AutoToken -> [AutoToken] -> [AutoToken]
forall a. a -> [a] -> [a]
: Hints -> [AutoToken]
autoTokens Hints
ws
autoTokens (String
"-c"     : Hints
ws) = AutoToken
C          AutoToken -> [AutoToken] -> [AutoToken]
forall a. a -> [a] -> [a]
: Hints -> [AutoToken]
autoTokens Hints
ws
autoTokens (String
"-r"     : Hints
ws) = AutoToken
R          AutoToken -> [AutoToken] -> [AutoToken]
forall a. a -> [a] -> [a]
: Hints -> [AutoToken]
autoTokens Hints
ws
autoTokens (String
h        : 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 [] = Int
0
parseTime 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
  (String
ds , String
modr) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isDigit String
xs
  (String
mod , 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
    String
"ms" -> Int
1
    String
"cs" -> Int
10
    String
"ds" -> Int
100
    String
"s"  -> Int
1000
    String
_    -> Int
1000

parseArgs :: String -> AutoOptions
parseArgs :: String -> AutoOptions
parseArgs 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 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 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 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 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 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 ()