module CC.Term.Parse

import CC.Name
import CC.Term
import CC.Term.Raw

import Data.List

import Text.Lexer
import Text.Parser

-- Tokens ----------------------------------------------------------------------

data CCTokenKind
  = TIgnore
  | TIdent
  -- Keywords
  | TLet
  -- Symbols
  | TLambda
  | TPOpen
  | TPClose
  | TComma
  | TFatArrow
  | TDef
  | TSemi

%name CCTokenKind k

Eq CCTokenKind where
  TIgnore == TIgnore = True
  TIdent == TIdent = True
  TLet == TLet = True
  TLambda == TLambda = True
  TPOpen == TPOpen = True
  TPClose == TPClose = True
  TComma == TComma = True
  TFatArrow == TFatArrow = True
  TDef == TDef = True
  TSemi == TSemi = True
  _ == _ = False

TokenKind CCTokenKind where
  TokType TIdent = String
  TokType _ = ()

  tokValue TIgnore s = ()
  tokValue TIdent s = s
  tokValue TLet s = ()
  tokValue TLambda s = ()
  tokValue TPOpen s = ()
  tokValue TPClose s = ()
  tokValue TComma s = ()
  tokValue TFatArrow s = ()
  tokValue TDef s = ()
  tokValue TSemi s = ()

export
CCToken : Type
CCToken = Token CCTokenKind

-- Lexer -----------------------------------------------------------------------

ignored : List Lexer
ignored = [spaces, lineComment (exact "--"), blockComment (exact "{-") (exact "-}")]

identifier : Lexer
identifier = alpha <+> many alphaNum

keywords : List (String, CCTokenKind)
keywords = [("let", TLet)]

tokenMap : TokenMap CCToken
tokenMap =
  toTokenMap (map (, TIgnore) ignored) ++
  [(identifier, \s =>
    case lookup s keywords of
      Just kind => Tok kind s
      Nothing => Tok TIdent s)
  ] ++ toTokenMap [
    (exact "\\", TLambda),
    (exact "\x03BB", TLambda),
    (exact "(", TPOpen),
    (exact ")", TPClose),
    (exact ",", TComma),
    (exact "=>", TFatArrow),
    (exact "=", TDef),
    (exact ";", TSemi)
  ]

-- Parser ----------------------------------------------------------------------

%tcinline
parens : {b : Bool} -> Grammar state CCToken b ty -> Grammar state CCToken True ty
parens p = match TPOpen >> commit >> p >>= (\t => match TPClose *> commit *> pure t)

parseTerm : Grammar state CCToken True RawTerm
parseLambda : Grammar state CCToken True RawTerm
parseLet : Grammar state CCToken True RawTerm
parseSpine : Grammar state CCToken True RawTerm
parseAtom : Grammar state CCToken True RawTerm

parseTerm = parseLambda <|> parseLet <|> parseSpine

parseLambda = do
  match TLambda
  commit
  names <- sepBy1 (match TComma >> commit) (MkName <$> (bounds $ match TIdent))
  commit
  match TFatArrow
  commit
  t <- parseTerm
  pure $ foldr1By RAbs (flip RAbs t) names

parseLet = do
  match TLet
  commit
  n <- bounds $ match TIdent
  commit
  match TDef
  commit
  t <- parseTerm
  match TSemi
  commit
  u <- parseTerm
  pure $ RLet (MkName n) t u

parseSpine = foldl1 RApp <$> some parseAtom

parseAtom =
  (RVar <$> MkName <$> (bounds $ match TIdent <* commit)) <|>
  (parens parseTerm)

parseSrc : Grammar state CCToken True RawTerm
parseSrc = parseTerm <* eof

export
parseString : String -> Either (List1 (ParsingError CCToken)) RawTerm
parseString str = do
  let (tokens, _, _, "") = lex tokenMap str
    | (_, line, col, rest) =>
      let bounds = MkBounds { startCol = col, startLine = line, endCol = col, endLine = line } in
      Left (Error "failed to lex input" (Just bounds) ::: [])
  (val, []) <- parse parseSrc $ filter (\tok => tok.val.kind /= TIgnore) tokens
    | (_, fst :: rest) => Left (Error "unexpected token" (Just fst.bounds) ::: [])
  pure val