    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  -- ^ Skip the first this many solutions
      , Options -> Bool
    optList :: Bool -- ^ List solutions instead of filling the hole
      , 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
      -- TODO: Use 'parseName' instead?
      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]
        -- TODO: Do arg properly
        , 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

    -- instance Pretty Options where
    --   prettyht