module Agda.Auto.Options where
import Control.Monad.State
import Agda.Utils.Lens
data Mode = MNormal Bool Bool
| MCaseSplit
| MRefine Bool
data AutoHintMode = AHMNone
| AHMModule
type Hints = [String]
newtype TimeOut = TimeOut { getTimeOut :: Int }
instance Show TimeOut where
show = show . getTimeOut
data AutoOptions = AutoOptions
{ autoHints :: Hints
, autoTimeOut :: TimeOut
, autoPick :: Int
, autoMode :: Mode
, autoHintMode :: AutoHintMode
}
initAutoOptions :: AutoOptions
initAutoOptions = AutoOptions
{ autoHints = []
, autoTimeOut = TimeOut 1
, autoPick = 0
, autoMode = MNormal False False
, autoHintMode = AHMNone
}
aoHints :: Lens' Hints AutoOptions
aoHints f s =
f (autoHints s) <&>
\x -> s {autoHints = x}
aoTimeOut :: Lens' TimeOut AutoOptions
aoTimeOut f s =
f (autoTimeOut s) <&>
\x -> s {autoTimeOut = x}
aoPick :: Lens' Int AutoOptions
aoPick f s =
f (autoPick s) <&>
\x -> s {autoPick = x}
aoMode :: Lens' Mode AutoOptions
aoMode f s =
f (autoMode s) <&>
\x -> s {autoMode = x}
aoHintMode :: Lens' AutoHintMode AutoOptions
aoHintMode f s =
f (autoHintMode s) <&>
\x -> s {autoHintMode = x}
data AutoToken =
M | C | R | D | L
| T Int | S Int | H String
autoTokens :: [String] -> [AutoToken]
autoTokens [] = []
autoTokens ("-t" : t : ws) = T (read t) : autoTokens ws
autoTokens ("-s" : s : ws) = S (read s) : autoTokens ws
autoTokens ("-l" : ws) = L : autoTokens ws
autoTokens ("-d" : ws) = D : autoTokens ws
autoTokens ("-m" : ws) = M : autoTokens ws
autoTokens ("-c" : ws) = C : autoTokens ws
autoTokens ("-r" : ws) = R : autoTokens ws
autoTokens (h : ws) = H h : autoTokens ws
parseArgs :: String -> AutoOptions
parseArgs s = mapM_ step (autoTokens $ words s)
`execState` initAutoOptions where
step :: AutoToken -> State AutoOptions ()
step M = aoHintMode .= AHMModule
step C = aoMode .= MCaseSplit
step R = aoPick .= (-1)
>> aoMode .= MRefine False
step (T t) = aoTimeOut .= TimeOut t
step (S p) = aoPick .= p
step (H h) = aoHints %= (h :)
step D = do
mode <- use aoMode
case mode of
MNormal lm _ -> aoMode .= MNormal lm True
_ -> return ()
step L = do
mode <- use aoMode
case mode of
MNormal _ dp -> aoMode .= MNormal True dp
MRefine _ -> aoMode .= MRefine True
_ -> return ()