{-# LANGUAGE TupleSections #-}
{-# LANGUAGE OverloadedStrings #-}
--------------------------------------------------------------------
-- |
-- Copyright :  (c) Edward Kmett and Dan Doel 2013
-- License   :  BSD3
-- Maintainer:  Edward Kmett <ekmett@gmail.com>
-- Stability :  experimental
-- Portability: non-portable
--
-- This module provides the parser for terms
--------------------------------------------------------------------
module Ermine.Parser.Pattern
  ( validate
  , pattern
  , pattern0
  , pattern1
  , PP
  ) where

import Control.Applicative
import Control.Lens hiding (op)
import Data.Foldable as Foldable
import Data.Text (Text)
import Data.Void
import qualified Data.Set as Set
import Ermine.Builtin.Global
import Ermine.Builtin.Pattern
import Ermine.Builtin.Type (anyType)
import Ermine.Parser.Literal
import Ermine.Parser.Style
import Ermine.Parser.Type
import Ermine.Syntax
import Text.Parser.Combinators
import Text.Parser.Token

-- | Check a 'Binder' for linearity.
--
-- Each variable name must be used at most once in the pattern.
validate :: (Functor m, Monad m, Ord v) => Binder v a -> (v -> m Void) -> m ()
validate b e =
  () <$ foldlM (\s n -> if n `Set.member` s then vacuous $ e n else return $ Set.insert n s)
               Set.empty
               (vars b)

-- | The simple pattern type generated by pattern parsing.
type PP = P Ann Text

varP :: (Monad m, TokenParsing m) => m PP
varP = termIdentifier <&> sigp ?? anyType

-- | Parse a single pattern part (e.g. an argument to a lambda)
pattern0 :: (Monad m, TokenParsing m) => m PP
pattern0
   = conp nothingg [] <$ symbol "Nothing"
 <|> varP
 <|> strictp <$ symbol "!" <*> pattern0
 <|> _p <$ symbol "_"
 <|> litp <$> literal
 <|> parens (tup' <$> patterns)

sigP :: (Monad m, TokenParsing m) => m PP
sigP = sigp <$> try (termIdentifier <* colon) <*> annotation

-- TODO: remove this when constructor patterns really work.
eP, longhP, justP, nothingP :: (Monad m, TokenParsing m) => m PP
eP       = conp eg       <$ symbol "E"       <*> many pattern1
justP    = conp justg    <$ symbol "Just"    <*> many pattern1
nothingP = conp nothingg <$ symbol "Nothing" <*> many pattern1
longhP   = conp longhg   <$ symbol "Long#"   <*> many pattern1

-- as patterns
pattern1 :: (Monad m, TokenParsing m) => m PP
pattern1
    = asp <$> try (termIdentifier <* symbol "@") <*> pattern1
  <|> pattern0

-- | Parse a single pattern (e.g. a case statement alt pattern)
pattern2 :: (Monad m, TokenParsing m) => m PP
pattern2
    = eP
  <|> justP
  <|> nothingP
  <|> longhP
  <|> pattern1

-- existentials sigP
pattern3 :: (Monad m, TokenParsing m) => m PP
pattern3
   = sigP
 <|> pattern2

patterns :: (Monad m, TokenParsing m) => m [PP]
patterns = commaSep pattern3

-- | Parse a single pattern (e.g. a case statement alt pattern)
pattern :: (Monad m, TokenParsing m) => m PP
pattern = pattern2