module Quox.Parser

import Quox.Syntax
import Quox.Token
import Quox.Lexer

import Data.Maybe
import Data.SnocVect
import Data.SnocList
import Text.Parser

%default total


public export
Vars : Nat -> Type
Vars n = SnocVect n String

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

public export
data Error
= Lex (Lexer.Error)
| Parse (List1 (ParsingError Token))
| Leftover (List BToken)
%hide Lexer.Error


public export
parseAll : {c : Bool} -> Grammar c a -> List BToken -> Either Error a
parseAll grm input =
  case parse grm input of
       Right (x, [])   => Right x
       Right (x, rest) => Left $ Leftover rest
       Left  errs      => Left $ Parse errs

public export
lexParseAll : {c : Bool} -> Grammar c a -> String -> Either Error a
lexParseAll grm = lex' >=> parseAll grm
  where lex' : String -> Either Error (List BToken)
        lex' = bimap Lex id . lex



export
punc : Punc -> Grammar True ()
punc p = terminal (show p) $ \case
  P p' => if p == p' then Just () else Nothing
  _    => Nothing

export
keyword : Keyword -> Grammar True ()
keyword k = terminal (show k) $ \case
  K k' => if k == k' then Just () else Nothing
  _    => Nothing

export
between : Punc -> Punc -> Grammar True a -> Grammar True a
between opener closer inner = punc opener *> inner <* punc closer

export
parens, squares, braces : Grammar True a -> Grammar True a
parens  = between LParen  RParen
squares = between LSquare RSquare
braces  = between LBrace  RBrace


export
number : Grammar True Nat
number = terminal "number" $ \case
  N Zero      => Just 0
  N One       => Just 1
  N (Other k) => Just k
  _           => Nothing

export
universe : Grammar True Nat
universe = terminal "universe" $ \case TYPE k => Just k; _ => Nothing

export
zero, one, omega : Grammar True ()
zero  = terminal "0" $ \case N Zero  => Just (); _ => Nothing
one   = terminal "1" $ \case N One   => Just (); _ => Nothing
omega = terminal "ω" $ \case K Omega => Just (); _ => Nothing

export
quantity : Grammar True Qty
quantity = Zero <$ zero <|> One <$ one <|> Any <$ omega


find1 : Eq a => SnocVect k a -> a -> Maybe (Var k)
find1 [<]       y = Nothing
find1 (sx :< x) y = if x == y then Just VZ else VS <$> find1 sx y

find : Vars k -> Name -> Maybe (Var k)
find vs (MakeName [<] (UN y)) = find1 vs y
find _  _                     = Nothing


export
checkAvoid1 : Vars n -> String -> Grammar False ()
checkAvoid1 avoid y =
  when (isJust $ find1 avoid y) $
    fail "wrong type of bound variable: \{show y}"

export
checkAvoid : Vars n -> Name -> Grammar False ()
checkAvoid avoid (MakeName [<] (UN y)) = checkAvoid1 avoid y
checkAvoid _     _                     = pure ()

export
bound : (what : String) -> (bound : Vars k) -> (avoid : Vars n) ->
        Grammar True (Var k)
bound what vs avoid = do
  x <- terminal "bound \{what} variable" $ \case Name x => Just x; _ => Nothing
  checkAvoid1 avoid x
  maybe (fail "not in scope: \{x}") pure $ find1 vs x

export
sname : Grammar True String
sname = terminal "simple name" $ \case Name x => pure x; _ => Nothing

export
qname : Grammar True Name
qname = do
  parts <- sepBy1 (punc Dot) sname
  pure $ MakeName {mods = cast $ init parts, base = UN $ last parts}

export
nameWith : (bound : Vars k) -> (avoid : Vars n) ->
           Grammar True (Either (Var k) Name)
nameWith bound avoid = do
  y <- qname
  checkAvoid avoid y
  pure $ maybe (Right y) Left $ find bound y


export
dimension : (dvars : Vars d) -> (tvars : Vars n) -> Grammar True (Dim d)
dimension dvars tvars =
      K Zero <$  zero
  <|> K One  <$  one
  <|> B      <$> bound "dimension" {bound = dvars, avoid = tvars}


mutual
  export
  term : (dvars : Vars d) -> (tvars : Vars n) -> Grammar True (Term d n)
  term dvars tvars =
        E <$> squares (elim {dvars, tvars})
    <|> TYPE . U <$> universe

  export
  elim : (dvars : Vars d) -> (tvars : Vars n) -> Grammar True (Elim d n)
  elim dvars tvars =
        either B F <$> nameWith {bound = tvars, avoid = dvars}