{-# LANGUAGE TupleSections #-}
{-# LANGUAGE LambdaCase #-}
--------------------------------------------------------------------
-- |
-- Copyright :  (c) Edward Kmett and Dan Doel 2012
-- License   :  BSD3
-- Maintainer:  Edward Kmett <ekmett@gmail.com>
-- Stability :  experimental
-- Portability: non-portable
--
-- This module provides the parser for types
--------------------------------------------------------------------
module Ermine.Parser.Type
  ( Ann
  , Typ
  , typ
  , typ0
  , annotation
  , typVarBinding
  , typVarBindings
  , someTypVarBindings
  , quantifier
  , quantBindings
  ) where

import Bound
import Bound.Var
import Control.Applicative
import Control.Lens (folded, filtered, to, (^..))
import Data.Text (Text)
import Data.Traversable (for)
import Ermine.Builtin.Type
import Ermine.Parser.Kind
import Ermine.Parser.Style
import Ermine.Syntax
import Ermine.Syntax.Kind as Kind hiding (Var, constraint)
import Ermine.Syntax.Type
import Text.Parser.Combinators
import Text.Parser.Token

type Ann = Annot Text
type Typ = Type (Maybe Text) (Var Text Text)

banana :: (Monad m, TokenParsing m) => m a -> m a
banana p = reserve op "(|" *> p <* reserve op "|)"

typic :: (Monad m, TokenParsing m) => m Typ
typic
   = Var . B <$> typeIdentifier
 <|> Var . F <$> ident typeCon

-- | Parse an atomic type
typ0 :: (Monad m, TokenParsing m) => m Typ
typ0 = typic
   <|> banana ( Var . B <$ reserve op ".." <*> typeIdentifier
            <|> concreteRho <$> commaSep (ident typeCon)
              )
   <|> parens ( arrow <$ reserve op "->"
            <|> tuple . (+1) . length <$> some comma
            <|> tup' <$> commaSep anyTyp
              )

typ1 :: (Monad m, TokenParsing m) => m Typ
typ1 = apps <$> typ0 <*> many typ0

-- TODO: typ2 shunting yard
typ2 :: (Monad m, TokenParsing m) => m Typ
typ2 = chainr1 typ1 ((~~>) <$ symbol "->")

-- | Parses an optionally annotated type variable.
--
--   typVarBinding ::= ( ident : kind )
--                   | ident
typVarBinding :: (Monad m, TokenParsing m) => m ([Text], Kind (Maybe Text))
typVarBinding = flip (,) unk <$> simpleTypVarBinding
            <|> parens ((,) <$> some typeIdentifier <* colon <*> (fmap Just <$> kind))
 where
 unk = pure Nothing

simpleTypVarBinding :: (Monad m, TokenParsing m) => m [Text]
simpleTypVarBinding = some typeIdentifier

-- | Parses a series of type var bindings, processing the result to a more
-- usable format.
--
--   typVarBindings ::= empty | someTypVarBindings
typVarBindings :: (Monad m, TokenParsing m) => m [(Var Text a, Kind (Maybe Text))]
typVarBindings = concatMap (\(vs, k) -> flip (,) k . B <$> vs) <$> many typVarBinding

-- | Parses a series of type var bindings, processing the result to a more
-- usable format.
--
--   someTypVarBindings ::= typVarBinding typVarBindings
someTypVarBindings :: (Monad m, TokenParsing m) => m [(Var Text a, Kind (Maybe Text))]
someTypVarBindings = concatMap (\(vs, k) -> flip (,) k . B <$> vs) <$> some typVarBinding

-- | Parses the bound variables for a quantifier.
--
--   quantBindings ::= {kindVars}
--                   | someTypVarBindings
--                   | {kindVars} typVarBindings
quantBindings :: (Monad m, TokenParsing m) => m ([Text], [(Var Text a, Kind (Maybe Text))])
quantBindings = optional (braces $ some typeIdentifier) >>= \mks -> case mks of
  Just ks -> (,) ks <$> typVarBindings
  Nothing -> (,) [] <$> someTypVarBindings

-- | Parses a quantifier.
--
--   quantifier ::= Q quantBindings .
quantifier :: (Monad m, TokenParsing m)
           => String -> m ([Text], [(Var Text a, Kind (Maybe Text))])
quantifier q = symbol q *> quantBindings <* dot

-- | Parser for a context that expects 0 or more constraints, together
--
--   constraints ::= constraints1
--                 | empty
--   constraints1 ::= constraint , constraints1
--                  | constraint
constraints :: (Monad m, TokenParsing m) => m Typ
constraints = allConstraints <$> commaSep constraint

-- | Parser for a context that expects a single constraint.
--   constraint ::= exists <vs>. constraint
--                | ( constraints )
--                | ident
constraint :: (Monad m, TokenParsing m) => m Typ
constraint =
      buildE <$ symbol "exists" <*> quantBindings <* dot <*> constraint
  <|> parens constraints
  <|> apps lame <$ symbol "Lame" <*> many typ0
  <|> apps fromInteg <$ symbol "FromInteger" <*> many typ0
  -- Single constraints
  <|> typic
 where buildE (kvs, tvks) =
         exists id (unvar Just Just) (Just <$> kvs) tvks

typ3 :: (Applicative m, Monad m, TokenParsing m) => m Typ
typ3 = forall id (unvar Just Just) [] [] <$> try (constraint <* reserve op "=>") <*> typ4
    <|> typ2

typ4 :: (Applicative m, Monad m, TokenParsing m) => m Typ
typ4 =  build <$ symbol "forall" <*> quantBindings <* dot <*> typ4
    <|> typ3
 where
 build (kvs, tvks) = forall id (unvar Just Just) (Just <$> kvs) tvks (And [])

-- | Parse a 'Type'.
typ :: (Monad m, TokenParsing m) => m Typ
typ = typ4

-- anyTyp = exists | typ
anyTyp :: (Monad m, TokenParsing m) => m Typ
anyTyp = typ

annotation :: (Monad m, TokenParsing m) => m Ann
annotation = do
  xs <- build <$> optional (symbol "some" *> some typeIdentifier <* dot) <*> typ
  for xs $ unvar (\x -> fail $ "bound variable in annotation: " ++ show x) pure
 where
   build mvs t = annot Just (unvar Just Just) [] vs (quant vs t)
     where vs = maybe [] (fmap B) mvs
   quant ss t = forall id (unvar Just Just) [] ts (And []) t
     where ts = t^..folded.filtered (`notElem` ss).to (, pure Nothing)