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.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 -> [Char]
(Int -> HintMode -> ShowS)
-> (HintMode -> [Char]) -> ([HintMode] -> ShowS) -> Show HintMode
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HintMode -> ShowS
showsPrec :: Int -> HintMode -> ShowS
$cshow :: HintMode -> [Char]
show :: HintMode -> [Char]
$cshowList :: [HintMode] -> ShowS
showList :: [HintMode] -> ShowS
Show)

data Options = Options
  { Options -> Integer
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 -> [Char]
(Int -> Options -> ShowS)
-> (Options -> [Char]) -> ([Options] -> ShowS) -> Show Options
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Options -> ShowS
showsPrec :: Int -> Options -> ShowS
$cshow :: Options -> [Char]
show :: Options -> [Char]
$cshowList :: [Options] -> ShowS
showList :: [Options] -> ShowS
Show

parseOptions :: InteractionId -> Range -> String -> TCM Options
parseOptions :: InteractionId -> Range -> [Char] -> TCM Options
parseOptions InteractionId
ii Range
range [Char]
argStr = do
  let tokens :: [Token]
tokens = [[Char]] -> [Token]
readTokens ([[Char]] -> [Token]) -> [[Char]] -> [Token]
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]]
words [Char]
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 -> [Char] -> TCMT IO Expr
parseExprIn InteractionId
ii Range
range [Char]
h | H [Char]
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 :: [Char] -> Int
parseTime [] = Int
0
parseTime [Char]
xs = [Char] -> Int
forall a. Read a => [Char] -> a
read [Char]
ds Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
modifier Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Char] -> Int
parseTime [Char]
r where
  ([Char]
ds , [Char]
modr) = (Char -> Bool) -> [Char] -> ([Char], [Char])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Char -> Bool
isDigit [Char]
xs
  ([Char]
mod , [Char]
r)   = (Char -> Bool) -> [Char] -> ([Char], [Char])
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

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 -> [Char]
(Int -> Token -> ShowS)
-> (Token -> [Char]) -> ([Token] -> ShowS) -> Show Token
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Token -> ShowS
showsPrec :: Int -> Token -> ShowS
$cshow :: Token -> [Char]
show :: Token -> [Char]
$cshowList :: [Token] -> ShowS
showList :: [Token] -> ShowS
Show)

readTokens :: [String] -> [Token]
readTokens :: [[Char]] -> [Token]
readTokens []              = []
readTokens ([Char]
"-t" : [Char]
t : [[Char]]
ws) = [Char] -> Token
T [Char]
t Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [[Char]] -> [Token]
readTokens [[Char]]
ws
readTokens ([Char]
"-s" : [Char]
n : [[Char]]
ws) = [Char] -> Token
S [Char]
n Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [[Char]] -> [Token]
readTokens [[Char]]
ws
readTokens ([Char]
"-l"     : [[Char]]
ws) = Token
L   Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [[Char]] -> [Token]
readTokens [[Char]]
ws
readTokens ([Char]
"-m"     : [[Char]]
ws) = Token
M   Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [[Char]] -> [Token]
readTokens [[Char]]
ws
readTokens ([Char]
"-c"     : [[Char]]
ws) = Token
C   Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [[Char]] -> [Token]
readTokens [[Char]]
ws
readTokens ([Char]
"-u"     : [[Char]]
ws) = Token
U   Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [[Char]] -> [Token]
readTokens [[Char]]
ws
readTokens ([Char]
h        : [[Char]]
ws) = [Char] -> Token
H [Char]
h Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [[Char]] -> [Token]
readTokens [[Char]]
ws

instance Pretty HintMode where
  pretty :: HintMode -> Doc
pretty = [Char] -> Doc
forall a. [Char] -> Doc a
text ([Char] -> Doc) -> (HintMode -> [Char]) -> HintMode -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HintMode -> [Char]
forall a. Show a => a -> [Char]
show

-- instance Pretty Options where
--   prettyht