content: {-# LANGUAGE TupleSections #-}
  {-# LANGUAGE OverloadedStrings #-}
  --------------------------------------------------------------------
  -- |
  -- Copyright :  (c) Edward Kmett and Dan Doel 2013
  -- License   :  BSD2
  -- 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
  