content: {-# LANGUAGE PackageImports, ConstraintKinds #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving,FlexibleInstances #-}
  {-# LANGUAGE StandaloneDeriving #-}
  {-# LANGUAGE ViewPatterns #-}
  -- A simple parser for the Frank language
  module Parser where
  
  import Control.Applicative
  import Control.Monad
  import Control.Monad.IO.Class
  
  import Data.Char
  import qualified Data.Map.Strict as M
  import qualified Data.HashSet as HashSet
  
  import Text.Trifecta
  import Text.Trifecta.Delta
  import "indentation-trifecta" Text.Trifecta.Indentation
  
  import Text.Parser.Token as Tok
  import Text.Parser.Token.Style
  import qualified Text.Parser.Token.Highlight as Hi
  
  import Test.Tasty (TestTree, testGroup)
  import Test.Tasty.HUnit (testCase, assertEqual, assertFailure, Assertion)
  
  import Syntax
  import ParserCommon
  import Debug
  
  import qualified Data.ByteString.Char8 as B
  
  -- the eof disallows gibberish at the end of the file!
  prog :: (Applicative m, MonadicParsing m) => m (Prog Raw)
  prog = MkProg <$ whiteSpace <*> do tts <- many tterm; eof; return tts
  
  tterm :: MonadicParsing m => m (TopTm Raw)
  tterm = do attachLoc $ (DataTm <$> parseDataT <|>
                          SigTm <$> try parseMHSig <|>
                          ClsTm <$> parseMHCls <|>
                          ItfTm <$> try parseItf <|>
                          ItfAliasTm <$> parseItfAlias)
  
  parseTyVar :: MonadicParsing m => m (Id, Kind)
  parseTyVar = (\x -> (x, ET)) <$> brackets parseEVar <|>
               (\x -> (x, VT)) <$> identifier
  
  parseDataT :: MonadicParsing m => m (DataT Raw)
  parseDataT = attachLoc $ do reserved "data"
                              name <- identifier
                              ps <- many parseTyVar
                              symbol "="
                              cs <- localIndentation Gt ctrlist
                              return $ DT name ps cs
  
  parseEVar :: MonadicParsing m => m Id
  parseEVar = do mx <- optional identifier
                 case mx of
                   Nothing -> return "£"
                   Just x -> return x
  
  ctrlist :: MonadicParsing m => m [Ctr Raw]
  ctrlist = sepBy parseCtr (symbol "|")
  
  parseCtr :: MonadicParsing m => m (Ctr Raw)
  parseCtr = attachLoc $ do name <- identifier
                            args <- many parseVType'
                            return $ Ctr name args
  
  parseMHSig :: MonadicParsing m => m (MHSig Raw)
  parseMHSig = attachLoc $ do name <- identifier
                              symbol ":"
                              ty <- parseSigType
                              return (Sig name ty)
  
  -- As the outer braces are optional in top-level signatures we require
  -- that plain pegs must have explicit ability brackets.
  --
  -- The following collections of signatures are equivalent:
  --
  --   f : {A -> B -> C}  and  f : A -> B -> C
  --   x : {Int}  and  x : {[]Int}  and x : []Int
  --
  -- A signature of the form
  --
  --   x : Int
  --
  -- is not currently valid. Once we add support for top level values it
  -- will become valid, but will not mean the same thing as:
  --
  --   x : []Int
  parseSigType :: MonadicParsing m => m (CType Raw)
  parseSigType = (do loc <- getLocation
                     symbol "{"
                     ct <- parseCType
                     symbol "}"
                     rest <- optional (symbol "->" *> parseCType)
                     return $
                       case rest of
                         Nothing -> ct
                         Just (CType ports peg a) ->
                           CType ((Port idAdjRaw (SCTy ct a) a) : ports) peg a) <|>
                 attachLoc (do ports <- some (try (parsePort <* symbol "->"))
                               peg <- parsePeg
                               return $ CType ports peg) <|>
                 attachLoc (do peg <- parsePegExplicit
                               return $ CType [] peg)
  
  parseMHCls :: MonadicParsing m => m (MHCls Raw)
  parseMHCls = attachProvideLoc $ \a -> do
                 name <- identifier
                 ps <- choice [some parsePattern, symbol "!" >> return []]
                 symbol "="
                 seq <- localIndentation Gt parseRawTmSeq
                 return $ MHCls name (Cls ps seq a) a
  
  parseItf :: MonadicParsing m => m (Itf Raw)
  parseItf = attachLoc $ do reserved "interface"
                            name <- identifier
                            ps <- many parseTyVar
                            symbol "="
                            xs <- localIndentation Gt $ sepBy1 parseCmd (symbol "|")
                            return (Itf name ps xs)
  
  parseCmd :: MonadicParsing m => m (Cmd Raw)
  parseCmd = attachLoc $ do cmd <- identifier
                            ps <- many parseTyVar  -- polymorphic commands
                            symbol ":"
                            (xs,y) <- parseCmdType
                            return (Cmd cmd ps xs y)
  
  -- type vars, input types, output type
  parseCmdType :: MonadicParsing m => m ([VType Raw], VType Raw)
  parseCmdType = do vs <- sepBy1 parseVType (symbol "->")
                    if length vs == 1 then return ([],head vs)
                    else return (init vs, last vs)
  
  parseItfAlias :: MonadicParsing m => m (ItfAlias Raw)
  parseItfAlias = attachLoc $ do reserved "interface"
                                 name <- identifier
                                 ps <- many parseTyVar
                                 symbol "="
                                 a <- getLocation
                                 symbol "["
                                 xs <- parseItfInstances
                                 symbol "]"
                                 return $ ItfAlias name ps (ItfMap (M.fromList xs) a)
  
  parseCType :: MonadicParsing m => m (CType Raw)
  parseCType = attachLoc $ do ports <- many (try (parsePort <* symbol "->"))
                              peg <- parsePeg
                              return $ CType ports peg
  
  parsePort :: MonadicParsing m => m (Port Raw)
  parsePort = attachLoc $ do adj <- parseAdj
                             ty <- parseVType
                             return $ Port adj ty
  
  parsePeg :: MonadicParsing m => m (Peg Raw)
  parsePeg = attachLoc $ do ab <- parseAb
                            ty <- parseVType
                            return $ Peg ab ty
  
  parsePegExplicit :: MonadicParsing m => m (Peg Raw)
  parsePegExplicit = attachLoc $ do ab <- brackets parseAbBody
                                    ty <- parseVType
                                    return $ Peg ab ty
  
  parseAdj :: MonadicParsing m => m (Adj Raw)
  parseAdj = attachProvideLoc $ \a -> do
                mxs <- optional $ angles (sepBy parseAdj' (symbol ","))
                case mxs of
                  Nothing -> return $ Adj (ItfMap M.empty a) a
                  Just xs -> return $ Adj (ItfMap (M.fromList xs) a) a
  
  parseAdj' :: MonadicParsing m => m (Id, [TyArg Raw])
  parseAdj' = do x <- identifier
                 ts <- many parseTyArg
                 return (x, ts)
  
  parseDTAb :: MonadicParsing m => m (Ab Raw)
  parseDTAb = brackets parseAbBody
  
  parseItfInstances :: MonadicParsing m => m [(Id, [TyArg Raw])]
  parseItfInstances = sepBy parseItfInstance (symbol ",")
  
  -- 0 | 0|Interfaces | E|Interfaces | Interfaces
  parseAbBody :: MonadicParsing m => m (Ab Raw)
  parseAbBody = attachProvideLoc $ \a ->
                  -- closed ability: [0] or [0 | i_1, ... i_n]
                  (do symbol "0"
                      xs <- option [] (symbol "|" *> parseItfInstances)
                      return $ Ab (EmpAb a) (ItfMap (M.fromList xs) a) a) <|>
                  -- open ability:   [i_1, ..., i_n] (implicitly e := £) or [e | i_1, ..., i_n]
                  (do e <- option (AbVar "£" a) (try $ AbVar <$> identifier <* symbol "|" <*> pure a)
                      xs <- parseItfInstances
                      return $ Ab e (ItfMap (M.fromList xs) a) a)
  
  parseAb :: MonadicParsing m => m (Ab Raw)
  parseAb = do mxs <- optional $ brackets parseAbBody
               case mxs of
                 Nothing -> attachProvideLoc $ \a ->
                   return $ Ab (AbVar "£" a) (ItfMap M.empty a) a
                 Just ab -> return ab
  
  parseItfInstance :: MonadicParsing m => m (Id, [TyArg Raw])
  parseItfInstance = do x <- identifier
                        ts <- many parseTyArg
                        return (x, ts)
  
  -- This parser gives higher precedence to MkDTTy when coming across "X"
  -- E.g., the type "X" becomes   MkDTTy "X" []   (instead of MkTVar "X")
  parseVType :: MonadicParsing m => m (VType Raw)
  parseVType = try parseDTType <|> -- could possibly also be a MKTvar (determined
                                   -- during refinement)
               parseVType'
  
  -- This parser gives higher precedence to MkTVar when coming across "X"
  -- E.g., the type "X" becomes   MkTVar "X"   (instead of MkDTTy "X" [])
  -- By writing "(X)" one can escape back to parseVType
  parseVType' :: MonadicParsing m => m (VType Raw)
  parseVType' = parens parseVType <|>
                (attachLoc $ SCTy <$> try (braces parseCType)) <|>
                (attachLoc $ StringTy <$ reserved "String") <|>
                (attachLoc $ IntTy <$ reserved "Int") <|>
                (attachLoc $ CharTy <$ reserved "Char") <|>
                (attachLoc $ TVar <$> identifier)  -- could possibly also be a MkDTTy
                                                   -- (determined during refinement)
  
  parseTyArg :: MonadicParsing m => m (TyArg Raw)
  parseTyArg = attachLoc $ VArg <$> parseVType' <|>
                           EArg <$> parseDTAb
  
  -- Parse a potential datatype. Note it may actually be a type variable.
  parseDTType :: MonadicParsing m => m (VType Raw)
  parseDTType = attachLoc $ do x <- identifier
                               args <- localIndentation Gt $ many parseTyArg
                               return $ DTTy x args
  
  parseRawTmSeq :: MonadicParsing m => m (Tm Raw)
  parseRawTmSeq = do loc <- getLocation
                     tm1 <- parseRawTm
                     m <- optional $ symbol ";"
                     case m of
                       Just _ -> do tm2 <- parseRawTmSeq
                                    return $ TmSeq tm1 tm2 loc
                       Nothing -> return tm1
  
  -- parse term of 1st syntactic category
  parseRawTm :: MonadicParsing m => m (Tm Raw)
  parseRawTm = parseLet <|>
               try parseRawOpTm <|>
               parseRawTm'
  
  -- parse term of 2nd syntactic category
  -- parse binary operation or term comb t_1 ... t_n
  parseRawOpTm :: (MonadicParsing m) => m (Tm Raw)
  parseRawOpTm = do loc <- getLocation
                    uminus <- optional $ symbol "-"
                    t1 <- parseRawOperandTm
                    let t1' = case uminus of
                                Just _ -> Use (RawComb (RawId "-" loc) [IntTm 0 loc, t1] loc) loc
                                Nothing -> t1
                    (do binOp <- parseBinOp
                        t2 <- parseRawOperandTm
                        return $ Use (RawComb binOp [t1',t2] loc) loc
                      <|> (return t1'))
  
  parseRawOperandTm :: MonadicParsing m => m (Tm Raw)
  parseRawOperandTm = (attachLoc $ Use <$> try parseComb) <|>
                      parens parseRawOpTm <|>
                      (attachLoc $ Use <$> parseId) <|>
                      (attachLoc $ IntTm <$> natural)
  
  parseBinOp :: MonadicParsing m => m (Use Raw)
  parseBinOp = attachLoc $ do op <- choice $ map symbol ["+","-","*","/","::"]
                              let op' = if op == "::" then "cons" else op
                              return $ RawId op'
  
  parseId :: MonadicParsing m => m (Use Raw)
  parseId = attachLoc $ do x <- identifier
                           return $ RawId x
  
  parseNullaryComb :: MonadicParsing m => m (Use Raw)
  parseNullaryComb = attachLoc $ do x <- choice [parseId, parens parseComb]
                                    symbol "!"
                                    return $ RawComb x []
  
  parseLet :: MonadicParsing m => m (Tm Raw)
  parseLet = attachLoc $ do reserved "let"
                            x <- identifier
                            symbol "="
                            tm1 <- parseRawTm
                            reserved "in"
                            tm2 <- parseRawTmSeq
                            return $ Let x tm1 tm2
  
  -- parse any term except let-expression or binary operation
  parseRawTm' :: MonadicParsing m => m (Tm Raw)
  parseRawTm' = (attachLoc $ Use <$> try parseNullaryComb) <|>  -- x!
                parens parseRawTmSeq <|>            -- t_1 ; ... ; t_n
                (attachLoc $ Use <$> parseId) <|>               -- x
                (attachLoc $ SC <$> parseRawSComp) <|>          -- { p_1 -> t_1 | ...
                (attachLoc $ StrTm <$> stringLiteral) <|>         -- "string"
                (attachLoc $ IntTm <$> natural) <|>               -- 42
                (attachLoc $ CharTm <$> charLiteral) <|>          -- 'c'
                (attachLoc $ ListTm <$> listTm)                   -- [t_1, ..., t_n]
  
  listTm :: MonadicParsing m => m [Tm Raw]          -- [t_1, ..., t_n]
  listTm = brackets (sepBy parseRawTm (symbol ","))
  
  parseComb :: MonadicParsing m => m (Use Raw)
  parseComb = attachLoc $ do x <- choice [parseId, parens parseComb]
                             args <- choice [some parseRawTm', symbol "!" >> pure []]
                             return $ RawComb x args
  
  parseRawClause :: MonadicParsing m => m (Clause Raw)
  parseRawClause = attachLoc $ do ps <- choice [try parsePatterns, pure []]
                                  seq <- parseRawTmSeq
                                  return $ Cls ps seq
    where parsePatterns =
            do ps <- choice [some parsePattern, symbol "!" >> return []]
               symbol "->"
               return $ ps
  
  parsePattern :: MonadicParsing m => m (Pattern Raw)
  parsePattern = try parseCPat <|> (attachLoc $ VPat <$> parseVPat)
  
  parseCPat :: MonadicParsing m => m (Pattern Raw)
  parseCPat = between (symbol "<") (symbol ">") $
              try parseCmdPat <|> parseThunkPat
  
  parseThunkPat :: MonadicParsing m => m (Pattern Raw)
  parseThunkPat = attachLoc $ do x <- identifier
                                 return (ThkPat x)
  
  parseCmdPat :: MonadicParsing m => m (Pattern Raw)
  parseCmdPat = attachLoc $ do cmd <- identifier
                               ps <- many parseVPat
                               symbol "->"
                               g <- identifier
                               return (CmdPat cmd ps g)
  
  parseVPat :: MonadicParsing m => m (ValuePat Raw)
  parseVPat = parseDataTPat <|>
              (attachLoc $ (do x <- identifier
                               return $ VarPat x)) <|>
              (attachLoc $ (IntPat <$> try integer)) <|> -- try block for unary minus
              (attachLoc $ (CharPat <$> charLiteral)) <|>
              (attachLoc $ (StrPat <$> stringLiteral)) <|>
              (attachLoc $ (ListPat <$> brackets (sepBy parseVPat (symbol ","))))
  
  parseDataTPat :: MonadicParsing m => m (ValuePat Raw)
  parseDataTPat = attachLoc $ parens $ ((try (do p <- parseVPat
                                                 symbol "::"
                                                 q <- parseVPat
                                                 return $ ConsPat p q)) <|>
                                       (do k <- identifier
                                           ps <- many parseVPat
                                           return $ DataPat k ps))
  
  parseRawSComp :: MonadicParsing m => m (SComp Raw)
  parseRawSComp = attachLoc $ localIndentation Gt $ absoluteIndentation $
                  do cs <- braces $ sepBy parseRawClause (symbol "|")
                     return $ SComp cs
  
  evalCharIndentationParserT :: Monad m => FrankParser Char m a ->
                                IndentationState -> m a
  evalCharIndentationParserT = evalIndentationParserT . runFrankParser
  
  evalTokenIndentationParserT :: Monad m => FrankParser Token m a ->
                                 IndentationState -> m a
  evalTokenIndentationParserT = evalIndentationParserT . runFrankParser
  
  runParse ev p input
   = let indA = ev p $ mkIndentationState 0 infIndentation True Ge
     in case parseString indA mempty input of
      Failure err -> Left (show err)
      Success t -> Right t
  
  runProgParse ev input = runParse ev prog input
  
  runParseFromFileEx ev p fname =
    let indA = ev p $ mkIndentationState 0 infIndentation True Ge in
    do res <- parseFromFileEx indA fname
       case res of
         Failure err -> return $ Left (show err)
         Success t -> return $ Right t
  
  runProgParseFromFileEx ev fname = runParseFromFileEx ev prog fname
  
  --runCharParseFromFile = runParseFromFileEx evalCharIndentationParserT
  runTokenParseFromFile :: (MonadIO m, Applicative m, MonadicParsing m) =>
                           String -> m (Either String (Prog Raw))
  runTokenParseFromFile = runProgParseFromFileEx evalTokenIndentationParserT
  
  --runCharParse = runParse evalCharIndentationParserT
  runTokenParse p = runParse evalTokenIndentationParserT p
  runTokenProgParse = runProgParse evalTokenIndentationParserT
  
  getLocation :: (MonadicParsing m) => m Raw
  getLocation = do r <- rend
                   line <- line
                   case delta r of
                     (Lines l c _ _) -> return $ Raw $ InCode (fromIntegral l + 1, fromIntegral c + 1)
                     _ -> return $ Raw $ InCode (-2, -2) -- TODO: LC: fix this after understanding
                                                         -- what the different Delta cases really mean
  
  attachLoc :: (MonadicParsing m) => (m (Raw -> AnnotFix f Raw)) -> m (AnnotFix f Raw)
  attachLoc parser = do a <- getLocation
                        parser <*> pure a
  
  attachProvideLoc :: (MonadicParsing m) => (Raw -> m (AnnotFix f Raw)) -> m (AnnotFix f Raw)
  attachProvideLoc parser = do a <- getLocation
                               parser a
  
  
  -- Tests
  input = [ "tests/evalState.fk"
          , "tests/listMap.fk"
          , "tests/suspended_computations.fk"
          , "tests/fib.fk"
          , "tests/paper.fk"]
  
  --outputc = map runCharParseFromFile input
  --outputt = map runTokenParseFromFile input
  
  assertParsedOk :: (Show err, Show a, Eq a) => IO (Either err a) -> IO a
                    -> Assertion
  assertParsedOk actual expected =
    do x <- actual
       case x of
         Right ok -> do y <- expected
                        assertEqual "parsing succeeded, but " y ok
         Left err -> do y <- expected
                        assertFailure ("parse failed with " ++ show err
                                       ++ ", expected " ++ show y)
  