module Parser (parseProgram) where

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

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
  whitespaceTo0
  name2 <- pName
  when (name /= name2) $
    fail $ "Definition of '" ++ name ++ "' followed by definition for '" ++ name2 ++ "'"
  whitespace
  token "="
  whitespace
  rhs <- pTerm
  return (Definition name (rhs :| typ))

pTerm :: Parser Term
pTerm = buildExpressionParser optable pTermEAtom
  where
    optable =
      [[Infix (token "->" >> return makePi) AssocRight
       ,Infix (token "→" >> return makePi) AssocRight]
      ,[Infix (token ":" >> return (\a b -> TAnnot (a :| b))) AssocNone]]

makePi :: Term -> Term -> Term
makePi (TAnnot (TVar x :| ty1)) ty2 = TPi x ty1 ty2
makePi ty1 ty2 = TPi ";_" ty1 ty2

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

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

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

pAtom :: Parser Term
pAtom = choice
  [do _ <- char '('
      whitespace
      e <- pTerm
      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)
  return name
  where
    keywords = ["=", "->", "→", ":", "?", "\\", "λ", "∀", "..", "..."
               ,"%"  -- for Sigma; hopefully temporary
               ,"forall", "data", "import", "in", "let"]

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

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

inlineComment :: Parser ()
inlineComment = token "--" >> manyTill anyChar 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 $
    many newline >> (void space <|> inlineComment) >> 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` ".;{}()@\""))))