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

parseTime :: String -> Int
parseTime :: [Char] -> Int
parseTime [] = Int
0
parseTime [Char]
xs = forall a. Read a => [Char] -> a
read [Char]
ds forall a. Num a => a -> a -> a
* Int
modifier forall a. Num a => a -> a -> a
+ [Char] -> Int
parseTime [Char]
r where
  ([Char]
ds , [Char]
modr) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isDigit [Char]
xs
  ([Char]
mod , [Char]
r)   = 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 = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ AutoToken -> State AutoOptions ()
step (Hints -> [AutoToken]
autoTokens forall a b. (a -> b) -> a -> b
$ [Char] -> Hints
words [Char]
s)
              forall s a. State s a -> s -> s
`execState` AutoOptions
initAutoOptions where

  step :: AutoToken -> State AutoOptions ()
  step :: AutoToken -> State AutoOptions ()
step AutoToken
M     = Lens' AutoHintMode AutoOptions
aoHintMode forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= AutoHintMode
AHMModule
  step AutoToken
C     = Lens' Mode AutoOptions
aoMode     forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= Mode
MCaseSplit
  step AutoToken
R     = Lens' Int AutoOptions
aoPick     forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= (-Int
1)
            forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Lens' Mode AutoOptions
aoMode     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  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     forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= Int
p
  step (H [Char]
h) = Lens' Hints AutoOptions
aoHints    forall o (m :: * -> *) i.
MonadState o m =>
Lens' i o -> (i -> i) -> m ()
%= ([Char]
h forall a. a -> [a] -> [a]
:)
  step AutoToken
D     = do
    Mode
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 forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= Bool -> Bool -> Mode
MNormal Bool
lm Bool
True
      Mode
_            -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
  step AutoToken
L     = do
    Mode
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 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 forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= Bool -> Mode
MRefine Bool
True
      Mode
_            -> forall (m :: * -> *) a. Monad m => a -> m a
return ()