module Quox.Parser

import public Quox.Lexer
import public Quox.Parser.Syntax

import Data.Fin
import Data.Vect
import public Text.Parser


-- [fixme] without this import idris fails to solve the
-- IsReserved arguments, which, ??????????????????????
import Derive.Prelude
%hide TT.Name

%default total


public export
0 Grammar : Bool -> Type -> Type
Grammar = Core.Grammar () Token
%hide Core.Grammar

private
data PArg = T PTerm | D PDim


private
apply : PTerm -> List PArg -> PTerm
apply = foldl $ \f, x => case x of T x => f :@ x; D p => f :% p

private
annotate : PTerm -> Maybe PTerm -> PTerm
annotate s a = maybe s (s :#) a


export
res : (str : String) -> (0 _ : IsReserved str) => Grammar True ()
res str = terminal "expecting \"\{str}\"" $
  \x => guard $ x == R str

export
resC : (str : String) -> (0 _ : IsReserved str) => Grammar True ()
resC str = do res str; commit


parameters {default True commit : Bool}
  private
  maybeCommit : Grammar False ()
  maybeCommit = when commit Core.commit

  export
  betweenR : {c : Bool} -> (op, cl : String) ->
             (0 _ : IsReserved op) => (0 _ : IsReserved cl) =>
             Grammar c a -> Grammar True a
  betweenR o c p = res o *> maybeCommit *> p <* res c <* maybeCommit

  export
  parens, bracks, braces : {c : Bool} -> Grammar c a -> Grammar True a
  parens = betweenR "(" ")"
  bracks = betweenR "[" "]"
  braces = betweenR "{" "}"


export
commaSep : {c : Bool} -> Grammar c a -> Grammar False (List a)
commaSep = sepEndBy (res ",")
  -- don't commit because of the possible terminating ","

export
semiSep : {c : Bool} -> Grammar c a -> Grammar False (List a)
semiSep = sepEndBy (res ";")

export
commaSep1 : {c : Bool} -> Grammar c a -> Grammar c (List1 a)
commaSep1 = sepEndBy1 (res ",")

export
darr : Grammar True ()
darr = resC "⇒"


export
name : Grammar True Name
name = terminal "expecting name" $
  \case I i => Just i; _ => Nothing

export
baseName : Grammar True BaseName
baseName = terminal "expecting unqualified name" $
  \case I i => guard (null i.mods) $> i.base
        _   => Nothing

export
nat : Grammar True Nat
nat = terminal "expecting natural number" $
  \case N n => pure n; _ => Nothing

export
string : Grammar True String
string = terminal "expecting string literal" $
  \case S s => pure s; _ => Nothing

export
tag : Grammar True String
tag = terminal "expecting tag constructor" $
  \case T t => pure t; _ => Nothing

export
bareTag : Grammar True String
bareTag = string <|> [|toDots name|]

export
universe : Grammar True PUniverse
universe = terminal "expecting type universe" $
  \case TYPE u => Just u; _ => Nothing

export
bname : Grammar True BName
bname = Nothing <$ res "_"
    <|> [|Just baseName|]

export
zeroOne : (zero, one : a) -> Grammar True a
zeroOne zero one = terminal "expecting zero or one" $
  \case N 0 => Just zero; N 1 => Just one; _ => Nothing


export covering
qty : Grammar True PQty
qty = zeroOne Zero One
  <|> Any <$ res "ω"
  <|> parens qty

private covering
qtys : Grammar False (List PQty)
qtys = option [] [|toList $ some qty <* res "·"|]

export
dimConst : Grammar True DimConst
dimConst = zeroOne Zero One

export covering
dim : Grammar True PDim
dim = [|V baseName|]
  <|> [|K dimConst|]
  <|> parens dim

private
0 PBinderHead : Nat -> Type
PBinderHead n = (Vect n PQty, BName, PTerm)

private
toVect : List a -> (n ** Vect n a)
toVect []        = (_ ** [])
toVect (x :: xs) = (_ ** x :: snd (toVect xs))

private
0 MakeBinder : Nat -> Type
MakeBinder n = (String, PBinderHead n -> PTerm -> PTerm)

private
makePi : MakeBinder 1
makePi = ("→", \([pi], x, s) => Pi pi x s)

private
makeSig : MakeBinder 0
makeSig = ("×", \([], x, s) => Sig x s)

private
plural : Nat -> a -> a -> a
plural 1 s p = s
plural _ s p = p

private
makeBinder : {m, n : Nat} -> MakeBinder m -> PBinderHead n -> PTerm ->
             Grammar False PTerm
makeBinder (str, f) h t =
  case decEq m n of
    Yes Refl => pure $ f h t
    No  _    => fatalError
      "'\{str}' expects \{show m} quantit\{plural m "y" "ies"}, got \{show n}"

private
binderInfix : Grammar True (n ** MakeBinder n)
binderInfix = res "→" $> (1 ** makePi)
          <|> res "×" $> (0 ** makeSig)

private
lamIntro : Grammar True (BName -> PTerm -> PTerm)
lamIntro = Lam  <$ resC "λ"
       <|> DLam <$ resC "δ"

private covering
caseIntro : Grammar True PQty
caseIntro = resC "case1" $> One
        <|> resC "caseω" $> Any
        <|> resC "case" *> qty <* resC "·"

private
optNameBinder : Grammar False BName
optNameBinder = [|join $ optional $ bname <* darr|]

mutual
  export covering
  term : Grammar True PTerm
  term = lamTerm
     <|> caseTerm
     <|> bindTerm
     <|> [|annotate infixEqTerm (optional $ resC "∷" *> term)|]

  private covering
  lamTerm : Grammar True PTerm
  lamTerm = flip . foldr <$> lamIntro <*> some bname <* darr <*> term

  private covering
  caseTerm : Grammar True PTerm
  caseTerm =
    [|Case caseIntro term
           (resC "return" *> optBinderTerm)
           (resC "of"     *> braces caseBody)|]

  private covering
  caseBody : Grammar False PCaseBody
  caseBody = [|CasePair (pairPat <* darr) (term <* optSemi)|]
         <|> [|CaseEnum $ semiSep [|MkPair tag (darr *> term)|]|]
  where
    optSemi = ignore $ optional $ res ";"
    pairPat = parens [|MkPair bname (resC "," *> bname)|]

  private covering
  bindTerm : Grammar True PTerm
  bindTerm = do
    bnd <- binderHead
    inf <- binderInfix
    body <- term
    makeBinder (snd inf) (snd bnd) body

  private covering
  infixEqTerm : Grammar True PTerm
  infixEqTerm = do
    l <- appTerm
    rty <- optional [|MkPair (resC "≡" *> term) (resC ":" *> appTerm)|]
    pure $ maybe l (\rty => Eq (Nothing, snd rty) l (fst rty)) rty

  private covering
  appTerm : Grammar True PTerm
  appTerm = resC "★"  *> [|TYPE nat|]
        <|> resC "Eq" *> [|Eq (bracks optBinderTerm) aTerm aTerm|]
        <|> [|apply aTerm (many appArg)|]

  private covering
  appArg : Grammar True PArg
  appArg = [|D $ resC "@" *> dim|]
       <|> [|T aTerm|]

  private covering
  aTerm : Grammar True PTerm
  aTerm = [|Enum $ braces $ commaSep bareTag|]
      <|> [|TYPE universe|]
      <|> [|V name|]
      <|> [|Tag tag|]
      <|> foldr1 Pair <$> parens (commaSep1 term)

  private covering
  binderHead : Grammar True (n ** PBinderHead n)
  binderHead = parens {commit = False} $ do
    qs <- [|toVect qtys|]
    name <- bname
    resC ":"
    ty <- term
    pure (_ ** (qs.snd, name, ty))

  private covering
  optBinderTerm : Grammar True (BName, PTerm)
  optBinderTerm = [|MkPair optNameBinder term|]