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?
  [Expr]
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 :: [QName]
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
  Options -> TCM Options
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Options
    { optTimeout :: MilliSeconds
optTimeout = MilliSeconds -> [MilliSeconds] -> MilliSeconds
forall a. a -> [a] -> a
firstOr MilliSeconds
1000 [Int -> MilliSeconds
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> MilliSeconds) -> Int -> MilliSeconds
forall a b. (a -> b) -> a -> b
$ String -> Int
parseTime String
t | T String
t <- [Token]
tokens]
    -- TODO: Do arg properly
    , optHintMode :: HintMode
optHintMode = HintMode -> [HintMode] -> HintMode
forall a. a -> [a] -> a
firstOr HintMode
NoHints ([HintMode
Module | Token
M <- [Token]
tokens] [HintMode] -> [HintMode] -> [HintMode]
forall a. [a] -> [a] -> [a]
++ [HintMode
Unqualified | Token
U <- [Token]
tokens])
    , optExplicitHints :: [QName]
optExplicitHints = [QName]
hints
    , optList :: Bool
optList = Token
L Token -> [Token] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Token]
tokens
    , optSkip :: Int
optSkip = Int -> [Int] -> Int
forall a. a -> [a] -> a
firstOr Int
0 [ Int
n | S String
s <- [Token]
tokens, Int
n <- Maybe Int -> [Int]
forall a. Maybe a -> [a]
maybeToList (Maybe Int -> [Int]) -> Maybe Int -> [Int]
forall a b. (a -> b) -> a -> b
$ String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe String
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