module Agda.Mimer.Options where
import Data.Char
import Data.Maybe
import Text.Read
import Agda.Interaction.BasicOps (parseExprIn)
import Agda.Syntax.Common (Nat)
import Agda.Syntax.Common.Pretty (Pretty, pretty, text)
import Agda.Syntax.Abstract.Name (QName)
import Agda.TypeChecking.Monad.Base (TCM)
import Agda.Interaction.Highlighting.Range (empty)
import Agda.Syntax.Common (InteractionId)
import Agda.Syntax.Position (Range)
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Abstract.Name as AN
import Agda.Utils.Maybe (catMaybes)
type MilliSeconds = Integer
data HintMode = Unqualified | AllModules | Module | NoHints
deriving (HintMode -> HintMode -> Bool
(HintMode -> HintMode -> Bool)
-> (HintMode -> HintMode -> Bool) -> Eq HintMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HintMode -> HintMode -> Bool
== :: HintMode -> HintMode -> Bool
$c/= :: HintMode -> HintMode -> Bool
/= :: HintMode -> HintMode -> Bool
Eq, Int -> HintMode -> ShowS
[HintMode] -> ShowS
HintMode -> String
(Int -> HintMode -> ShowS)
-> (HintMode -> String) -> ([HintMode] -> ShowS) -> Show HintMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HintMode -> ShowS
showsPrec :: Int -> HintMode -> ShowS
$cshow :: HintMode -> String
show :: HintMode -> String
$cshowList :: [HintMode] -> ShowS
showList :: [HintMode] -> ShowS
Show)
data Options = Options
{ Options -> MilliSeconds
optTimeout :: MilliSeconds
, Options -> HintMode
optHintMode :: HintMode
, Options -> Int
optSkip :: Int
, Options -> Bool
optList :: Bool
, Options -> [QName]
optExplicitHints :: [QName]
} deriving Int -> Options -> ShowS
[Options] -> ShowS
Options -> String
(Int -> Options -> ShowS)
-> (Options -> String) -> ([Options] -> ShowS) -> Show Options
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Options -> ShowS
showsPrec :: Int -> Options -> ShowS
$cshow :: Options -> String
show :: Options -> String
$cshowList :: [Options] -> ShowS
showList :: [Options] -> ShowS
Show
parseOptions :: InteractionId -> Range -> String -> TCM Options
parseOptions :: InteractionId -> Range -> String -> TCM Options
parseOptions InteractionId
ii Range
range String
argStr = do
let tokens :: [Token]
tokens = [String] -> [Token]
readTokens ([String] -> [Token]) -> [String] -> [Token]
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
argStr
hintExprs <- [TCMT IO Expr] -> TCMT IO [Expr]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [InteractionId -> Range -> String -> TCMT IO Expr
parseExprIn InteractionId
ii Range
range String
h | H String
h <- [Token]
tokens]
let hints = [Maybe QName] -> [QName]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe QName] -> [QName]) -> [Maybe QName] -> [QName]
forall a b. (a -> b) -> a -> b
$ (Expr -> Maybe QName) -> [Expr] -> [Maybe QName]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Maybe QName
hintExprToQName [Expr]
hintExprs
return Options
{ optTimeout = firstOr 1000 [fromIntegral $ parseTime t | T t <- tokens]
, optHintMode = firstOr NoHints ([Module | M <- tokens] ++ [Unqualified | U <- tokens])
, optExplicitHints = hints
, optList = L `elem` tokens
, optSkip = firstOr 0 [ n | S s <- tokens, n <- maybeToList $ readMaybe s ]
}
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])
break 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
hintExprToQName :: A.Expr -> Maybe QName
hintExprToQName :: Expr -> Maybe QName
hintExprToQName (A.ScopedExpr ScopeInfo
_ Expr
e) = Expr -> Maybe QName
hintExprToQName Expr
e
hintExprToQName (A.Def QName
qname) = QName -> Maybe QName
forall a. a -> Maybe a
Just (QName -> Maybe QName) -> QName -> Maybe QName
forall a b. (a -> b) -> a -> b
$ QName
qname
hintExprToQName (A.Proj ProjOrigin
_ AmbiguousQName
qname) = QName -> Maybe QName
forall a. a -> Maybe a
Just (QName -> Maybe QName) -> QName -> Maybe QName
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
AN.headAmbQ AmbiguousQName
qname
hintExprToQName (A.Con AmbiguousQName
qname) = QName -> Maybe QName
forall a. a -> Maybe a
Just (QName -> Maybe QName) -> QName -> Maybe QName
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
AN.headAmbQ AmbiguousQName
qname
hintExprToQName Expr
_ = Maybe QName
forall a. Maybe a
Nothing
firstOr :: a -> [a] -> a
firstOr :: forall a. a -> [a] -> a
firstOr a
x [] = a
x
firstOr a
_ (a
x:[a]
_) = a
x
data Token = T String | M | U | C | L | S String | H String
deriving (Token -> Token -> Bool
(Token -> Token -> Bool) -> (Token -> Token -> Bool) -> Eq Token
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Token -> Token -> Bool
== :: Token -> Token -> Bool
$c/= :: Token -> Token -> Bool
/= :: Token -> Token -> Bool
Eq, Int -> Token -> ShowS
[Token] -> ShowS
Token -> String
(Int -> Token -> ShowS)
-> (Token -> String) -> ([Token] -> ShowS) -> Show Token
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Token -> ShowS
showsPrec :: Int -> Token -> ShowS
$cshow :: Token -> String
show :: Token -> String
$cshowList :: [Token] -> ShowS
showList :: [Token] -> ShowS
Show)
readTokens :: [String] -> [Token]
readTokens :: [String] -> [Token]
readTokens [] = []
readTokens (String
"-t" : String
t : [String]
ws) = String -> Token
T String
t Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [String] -> [Token]
readTokens [String]
ws
readTokens (String
"-s" : String
n : [String]
ws) = String -> Token
S String
n Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [String] -> [Token]
readTokens [String]
ws
readTokens (String
"-l" : [String]
ws) = Token
L Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [String] -> [Token]
readTokens [String]
ws
readTokens (String
"-m" : [String]
ws) = Token
M Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [String] -> [Token]
readTokens [String]
ws
readTokens (String
"-c" : [String]
ws) = Token
C Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [String] -> [Token]
readTokens [String]
ws
readTokens (String
"-u" : [String]
ws) = Token
U Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [String] -> [Token]
readTokens [String]
ws
readTokens (String
h : [String]
ws) = String -> Token
H String
h Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [String] -> [Token]
readTokens [String]
ws
instance Pretty HintMode where
pretty :: HintMode -> Doc
pretty = String -> Doc
forall a. String -> Doc a
text (String -> Doc) -> (HintMode -> String) -> HintMode -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HintMode -> String
forall a. Show a => a -> String
show