content: module Ditto.Parse where
  import Ditto.Syntax
  import Text.Parsec (parse, try)
  import Text.Parsec.String
  import Text.Parsec.Char
  import Text.Parsec.Combinator
  import Control.Applicative ((<*), many, (<$>), (<*>), (<|>))
  import Control.Monad
  import Data.ByteString.Char8 (ByteString, pack, unpack)
  
  ----------------------------------------------------------------------
  
  parseE = parse (whitespace >> parseExp <* eof) "" . stripComments
  parseP = parse (whitespace >> parseProg <* eof) "" . stripComments
  
  stripComments :: String -> String
  stripComments = unlines . map (takeWhile (/= '#')) . lines
  
  keyType = symbol "Type"
  keyData = symbol "data"
  keyMutual = symbol "mutual"
  keyDef = symbol "def"
  keyWhere = symbol "where"
  keyEnd = symbol "end"
  
  keywords = choice
    [keyType, keyData, keyDef, keyWhere, keyEnd]
  
  symAscribe = symbol ":"
  symKind = symbol "::"
  symChoice = symbol "|"
  symInfer = symbol "*"
  strHole = "?"
  symHole = symbol strHole
  symInacc = symbol "*"
  symEq = symbol "="
  symNeq = symbol "!="
  symAt = symbol "@"
  symArr = symbol "->"
  symComma = symbol ","
  
  symLParen = symbol "("
  symRParen = symbol ")"
  symLBrace = symbol "{"
  symRBrace = symbol "}"
  
  ----------------------------------------------------------------------
  
  parseProg :: Parser Prog
  parseProg = many1 $ (Right <$> parseMutual) <|> (Left <$> parseStmt)
  
  parseStmt :: Parser Stmt
  parseStmt = choice [
      parseDef
    , parseDefn
    , parseData
    ]
  
  parseMutual :: Parser [Stmt]
  parseMutual = try $ do
    keyMutual
    xs <- many1 parseStmt
    keyEnd
    return xs
  
  parseDef :: Parser Stmt
  parseDef = try $ do
    keyDef
    x <- parsePName
    optional $ symAscribe
    _A <- parseExp
    keyWhere
    a <- parseExp
    keyEnd
    return $ SDef x a _A
  
  ----------------------------------------------------------------------
  
  parseDefn :: Parser Stmt
  parseDefn = try $ do
    keyDef
    x <- parsePName
    optional $ symAscribe
    _A <- parseExp
    keyWhere
    cs <- many1 parseClause
    keyEnd
    return $ SDefn x _A cs
  
  parseClause :: Parser SClause
  parseClause = try $ do
    symChoice
    ps <- many parsePattern
    a <- parseRHS
    return (ps , a)
  
  parseRHS :: Parser RHS
  parseRHS = choice
    [ try $ MapsTo <$> (symEq >> parseExp)
    , try $ Caseless <$> (symNeq >> parseName)
    , try $ Split <$> (symAt >> parseName)
    ]
  
  ----------------------------------------------------------------------
  
  parsePattern :: Parser (Icit, Pat)
  parsePattern = choice
    [ parseImplPat parsePVar
    , parseExplPat parsePVar
    , parseImplPat parsePInacc
    , parseExplPat parsePInacc
    , parseImplPat parsePCon
    , parseExplPat (parens parsePCon)
    ]
  
  parseImplPat :: Parser Pat -> Parser (Icit, Pat)
  parseImplPat p = (Impl,) <$> try (braces p)
  
  parseExplPat :: Parser Pat -> Parser (Icit, Pat)
  parseExplPat p = (Expl,) <$> try p
  
  parsePCon :: Parser Pat
  parsePCon = try $ do
    x <- parsePName
    xs <- many parsePattern
    return $ PCon x xs
  
  parsePVar :: Parser Pat
  parsePVar = try $ PVar <$> parseAccName
  
  parsePInacc :: Parser Pat
  parsePInacc = try $ do
    symInacc
    return $ PInacc Nothing
  
  ----------------------------------------------------------------------
  
  parseData :: Parser Stmt
  parseData = try $ do
    keyData
    x <- parsePName
    _As <- parseParams <|> (optional symAscribe >> return [])
    _B <- pis _As <$> parseExp
    keyWhere
    cons <- paramCons _As . concat <$> many parseCon
    keyEnd
    return $ SData x _B cons
  
  parseParams :: Parser Tel
  parseParams = try $ do
    _As <- parseTel
    symKind
    return _As
  
  parseCon :: Parser SCons
  parseCon = try $ do
    symChoice
    xs <- commaSep parsePName
    optional symAscribe
    _A <- parseExp
    return (map (\x -> (x, _A)) xs)
  
  ----------------------------------------------------------------------
  
  parseExp :: Parser Exp
  parseExp = choice [
      parsePi
    , parseLam
    , parseApps
    ]
  
  parseApps :: Parser Exp
  parseApps = apps <$> parseAtom <*> many parseApp
  
  parseApp :: Parser (Icit, Exp)
  parseApp = parseImplApp <|> parseExplApp
  
  parseImplApp :: Parser (Icit, Exp)
  parseImplApp = (Impl,) <$> try (braces parseExp)
  
  parseExplApp :: Parser (Icit, Exp)
  parseExplApp = (Expl,) <$> parseAtom
  
  parseAtom :: Parser Exp
  parseAtom = choice [
      parens parseExp
    , parseType
    , parseInfer
    , parseHole
    , parseVar
    ]
  
  ----------------------------------------------------------------------
  
  parseType :: Parser Exp
  parseType = try $ keyType >> return EType
  
  parseInfer :: Parser Exp
  parseInfer = try $ symInfer >> return (EInfer MInfer)
  
  parseHole :: Parser Exp
  parseHole = parseNamedHole <|> parseAnonHole
  
  parseNamedHole :: Parser Exp
  parseNamedHole = try $ do
    string strHole
    nm <- parseIdent
    return . EInfer . MHole . Just $ nm
  
  parseAnonHole :: Parser Exp
  parseAnonHole = try $ do
    symHole
    return . EInfer . MHole $ Nothing
  
  parseVar :: Parser Exp
  parseVar = try $ EVar <$> parseName
  
  parsePName :: Parser PName
  parsePName = PName <$> parseIdent
  
  parseName :: Parser Name
  parseName = parseAccName <|> parseInaccName
  
  parseAccName :: Parser Name
  parseAccName = bs2n Acc <$> parseIdent
  
  parseInaccName :: Parser Name
  parseInaccName = try $ do
    symInacc
    return (s2n Inacc "x")
  
  parseIdent :: Parser ByteString
  parseIdent = try $ do
    notFollowedBy keywords
    prefix <- many (char '`')
    body <- (:) <$> letter <*> many alphaNum
    suffix <- many (char '\'')
    lexeme $ return $ pack $ prefix ++ body ++ suffix
  
  ----------------------------------------------------------------------
  
  parsePi :: Parser Exp
  parsePi = try $ do
    _As <- parseTel
    symAscribe
    _A <- parseExp
    return $ pis _As _A
  
  parseLam :: Parser Exp
  parseLam = try $ do
    _As <- parseTel
    symArr
    b <- parseExp
    return $ lams _As b
  
  ----------------------------------------------------------------------
  
  parseTel :: Parser Tel
  parseTel = concat <$> many1 (parseImplAnnot <|> parseExplAnnot)
  
  parseImplAnnot :: Parser Tel
  parseImplAnnot = try $ braces $ do
    xs <- commaSep parseName
    optional symAscribe
    a <- parseExp
    return $ map (\ x -> (Impl, x , a)) xs
  
  parseExplAnnot :: Parser Tel
  parseExplAnnot = try $ parens $ do
    xs <- commaSep parseName
    optional symAscribe
    a <- parseExp
    return $ map (\ x -> (Expl, x , a)) xs
  
  ----------------------------------------------------------------------
  
  commaSep :: Parser a -> Parser [a]
  commaSep p = p `sepBy1` symComma
  
  parens :: Parser a -> Parser a
  parens = between symLParen symRParen
  
  braces :: Parser a -> Parser a
  braces = between symLBrace symRBrace
  
  symbol :: String -> Parser String
  symbol s = lexeme $ string s
  
  lexeme :: Parser a -> Parser a
  lexeme p = p <* whitespace
  
  whitespace :: Parser ()
  whitespace = void $ many $ oneOf " \n\t"
  
  ----------------------------------------------------------------------
  