module Parser (parseProgram) where

import Control.Monad
import Data.Char
import Data.List (foldl')
import Text.Parsec hiding (token)

import AST


type Parser = Parsec String ()

parseProgram :: String -> String -> Either ParseError [Definition]
parseProgram fname source = parse pProgram fname source

pProgram :: Parser [Definition]
pProgram = do
  whitespaceTo0
  choice
    [eof >> return []
    ,(:) <$> pDef <*> pProgram]

-- | Assumes column 0
pDef :: Parser Definition
pDef = do
  name <- pName
  whitespace
  token ":"
  whitespace
  typ <- pTerm 0
  whitespaceTo0
  name2 <- pName
  when (name /= name2) $
    fail $ "Definition of '" ++ name ++ "' followed by definition for '" ++ name2 ++ "'"
  whitespace
  token "="
  whitespace
  rhs <- pTerm 0
  return (Definition name (rhs :| typ))

-- operator precedences:
--   0 _:_
--   1 (_ : _) -> _
--   2 _,_

pTerm :: Int -> Parser Term
pTerm p | p <= 0 = do
  e1 <- pTerm 1
  whitespace
  choice
    [do token ":"
        whitespace
        e2 <- pTerm 1
        return (TAnnot (e1 :| e2))
    ,return e1]

pTerm 1 = do
  e1 <- pTerm 2
  whitespace
  choice
    [do (token "->" <|> token "→")
        (x :| ty) <- case e1 of
          TAnnot (TVar x :| ty) -> return (x :| ty)
          _ -> fail $ "Expected (x : type) as left-hand side of (->)"
        whitespace
        e2 <- pTerm 1
        return (TPi x ty e2)
    ,return e1]

pTerm 2 = do
  e1 <- pTerm 3
  whitespace
  choice
    [do token ","
        whitespace
        e2 <- pTerm 2
        return (TPair e1 e2)
    ,return e1]

pTerm _ = pTermEAtom

pTermEAtom :: Parser Term
pTermEAtom = pLambda <|> pSpecialApp <|> pApp

pLambda :: Parser Term
pLambda = do
  void (char '\\') <|> token "λ"
  whitespace
  _ <- char '('
  whitespace
  x <- pName
  whitespace
  token ":"
  whitespace
  ty <- pTerm 0
  whitespace
  _ <- char ')'
  whitespace
  token "->"
  whitespace
  rhs <- pTerm 0
  return (TLam x ty rhs)

pSpecialApp :: Parser Term
pSpecialApp = pSet <|> pSetw <|> pSigma
  where
    pSet :: Parser Term
    pSet = do
      token "Set"
      whitespace
      e <- pTermEAtom
      return (TSet e)

    pSetw :: Parser Term
    pSetw = do
      token "Setw"
      whitespace
      n <- read <$> many1 digit
      return (TSetw n)

    pSigma :: Parser Term
    pSigma = do
      token "Sigma"
      whitespace
      _ <- char '('
      whitespace
      x <- pName
      whitespace
      token ":"
      whitespace
      ty <- pTerm 0
      whitespace
      _ <- char ')'
      whitespace
      rhs <- pTermEAtom
      return (TSigma x ty rhs)

pApp :: Parser Term
pApp = do
  e1 <- pAtom
  args <- many (try (whitespace >> pAtom))
  return (foldl' TApp e1 args)

pAtom :: Parser Term
pAtom = choice
  [do _ <- char '('
      whitespace
      e <- pTerm 0
      whitespace
      _ <- char ')'
      return e
  ,TVar <$> pName]

-- TODO TPair, TSigma ("%"). The rest are environment entries.

pName :: Parser Name
pName = do
  name <- many1 pNameChar
  guard (name `notElem` keywords)
  guard (head name /= '\\')  -- lambda syntax
  return name
  where
    keywords = ["=", "->", "→", ":", "?", "\\", "λ", "∀", "..", "..."
               ,"forall", "data", "import", "in", "let"
               ,"Sigma", ","  -- temporary
               ]

pNameChar :: Parser Char
pNameChar = satisfy (\c -> not (isSpace c) && c `notElem` ".;{}()@\"")

inlineWhite :: Parser ()
inlineWhite = do
  skipMany inlineSpace
  choice
    [inlineComment
    -- TODO: nested {- -} comments
    ,return ()]

inlineComment :: Parser ()
inlineComment = token "--" >> manyTill anyChar (lookAhead newline) >> return ()

-- | Skips to the furthest point from here that can be reached without
-- consuming any tokens, and without ending on column 0.
whitespace :: Parser ()
whitespace = do
  inlineWhite
  optional $ try $
    many newline >> (inlineSpace <|> inlineComment) >> whitespace

inlineSpace :: Parser ()
inlineSpace = void (satisfy (\c -> isSpace c && c /= '\n')) <?> "inline whitespace"

-- | Skips as much whitespace as possible, and throws an error if that doesn't
-- leave us on column 0.
whitespaceTo0 :: Parser ()
whitespaceTo0 = do
  inlineWhite
  choice
    [eof
    ,newline >> whitespaceTo0
    ,do pos <- getPosition
        when (sourceColumn pos /= 1) $
          unexpected "indented code"]

token :: String -> Parser ()
token s = try $ string s >> (eof <|> void (lookAhead (satisfy (\c -> isSpace c || c `elem` ".;{}()@\""))))