content: {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE TypeSynonymInstances #-}
  
  
  
  
  
  -- | This module defines how to parser a program in the simply typed lambda
  -- calculus w/ non-parametric user defined types (eg Bool, Nat).
  
  module Simple.Core.Parser where
  
  import Utils.ABT
  import Utils.Vars
  import Simple.Core.ConSig
  import Simple.Core.Term
  import Simple.Core.Type
  import Simple.Core.Program
  
  import Control.Applicative ((<$>),(<*>),(*>),(<*))
  import Control.Monad (guard)
  import Data.List (foldl')
  import Text.Parsec
  import qualified Text.Parsec.Token as Token
  
  
  
  
  
  languageDef :: Token.LanguageDef st
  languageDef = Token.LanguageDef
                  { Token.commentStart = "{-"
                  , Token.commentEnd = "-}"
                  , Token.commentLine = "--"
                  , Token.nestedComments = True
                  , Token.identStart = letter <|> char '_'
                  , Token.identLetter = alphaNum <|> char '_' <|> char '\''
                  , Token.opStart = oneOf ""
                  , Token.opLetter = oneOf ""
                  , Token.reservedNames = ["data","case","of","end","where","let"]
                  , Token.reservedOpNames = ["|","->","\\",":","=","||"]
                  , Token.caseSensitive = True
                  }
  
  tokenParser = Token.makeTokenParser languageDef
  
  identifier = Token.identifier tokenParser
  reserved = Token.reserved tokenParser
  reservedOp = Token.reservedOp tokenParser
  parens = Token.parens tokenParser
  symbol = Token.symbol tokenParser
  whiteSpace = Token.whiteSpace tokenParser
  
  
  
  
  
  -- Parsers for identifiers
  
  varName = do lookAhead (lower <|> char '_')
               identifier
  
  decName = do lookAhead upper
               identifier
  
  
  
  
  
  -- Type parsers
  
  typeCon = tyConH <$> decName
  
  funType = do arg <- try $ do
                 arg <- funLeft
                 _ <- reservedOp "->"
                 return arg
               ret <- funRight
               return $ funH arg ret
  
  parenType = parens datatype
  
  datatype = funType <|> typeCon <|> parenType
  
  
  
  funLeft = typeCon <|> parenType
  
  funRight = funType <|> typeCon <|> parenType
  
  
  
  
  
  -- Term parsers
  
  variable = do x <- varName
                guard (x /= "_")
                return $ Var (Free (FreeVar x))
  
  annotation = do m <- try $ do
                    m <- annLeft
                    _ <- reservedOp ":"
                    return m
                  t <- datatype
                  return $ annH m t
  
  lambda = do _ <- reservedOp "\\"
              xs <- many1 varName
              _ <- reservedOp "->"
              b <- lamBody
              let xsFreshDummies =
                    map unBNSString
                        (dummiesToFreshNames
                          (freeVarNames b)
                          (map BNSString xs))
              return $ helperFold lamH xsFreshDummies b
  
  application = do (f,a) <- try $ do
                     f <- appFun
                     a <- appArg
                     return (f,a)
                   as <- many appArg
                   return $ foldl' appH f (a:as)
  
  noArgConData = do c <- decName
                    return $ conH c []
  
  conData = do c <- decName
               as <- many conArg
               return $ conH c as
  
  varPattern = do x <- varName
                  return $ Var (Free (FreeVar x))
  
  noArgConPattern = do c <- decName
                       return $ conPatH c []
  
  conPattern = do c <- decName
                  ps <- many conPatternArg
                  return $ conPatH c ps
  
  parenPattern = parens pattern
  
  pattern = parenPattern <|> conPattern <|> varPattern
  
  clause = do ps <- try $ do
                ps <- pattern `sepBy` reservedOp "||"
                _ <- reservedOp "->"
                return ps
              b <- term
              let freshenedPs = dummiesToFreshNames (freeVarNames b) ps
                  xs = freeVarNames =<< freshenedPs
              return $ clauseH xs freshenedPs b
  
  caseExp = do _ <- reserved "case"
               m <- caseArg `sepBy` reservedOp "||"
               _ <- reserved "of"
               _ <- optional (reservedOp "|")
               cs <- clause `sepBy` reservedOp "|"
               _ <- reserved "end"
               return $ caseH m cs
  
  parenTerm = parens term
  
  term = annotation <|> application <|> parenTerm <|> lambda <|> conData <|> caseExp <|> variable
  
  
  
  
  
  annLeft = application <|> parenTerm <|> conData <|> variable
  
  lamBody = annotation <|> application <|> parenTerm <|> lambda <|> conData <|> caseExp <|> variable
  
  appFun = parenTerm <|> variable
  
  appArg = parenTerm <|> noArgConData <|> variable
  
  conArg = parenTerm <|> noArgConData <|> variable
  
  caseArg = annotation <|> application <|> parenTerm <|> lambda <|> conData <|> variable
  
  conPatternArg = parenPattern <|> noArgConPattern <|> varPattern
  
  
  
  
  
  parseTerm str = case parse (whiteSpace *> term <* eof) "(unknown)" str of
                    Left e -> Left (show e)
                    Right p -> Right p
  
  
  
  
  
  -- Program parsers
  
  eqTermDecl = do (x,t) <- try $ do
                    _ <- reserved "let"
                    x <- varName
                    _ <- reservedOp ":"
                    t <- datatype
                    _ <- reservedOp "="
                    return (x,t)
                  m <- term
                  _ <- reserved "end"
                  return $ TermDeclaration x t m
  
  whereTermDecl = do (x,t) <- try $ do
                       _ <- reserved "let"
                       x <- varName
                       _ <- reservedOp ":"
                       t <- datatype
                       _ <- reserved "where"
                       return (x,t)
                     _ <- optional (reservedOp "|")
                     preclauses <- patternMatchClause x `sepBy1` reservedOp "|"
                     _ <- reserved "end"
                     return $ WhereDeclaration x t preclauses
  
  patternMatchClause x = do _ <- symbol x
                            ps <- many patternMatchPattern
                            _ <- reservedOp "="
                            b <- term
                            let freshenedPs =
                                  dummiesToFreshNames (freeVarNames b) ps
                                xs = freeVarNames =<< freshenedPs
                            return (freshenedPs,xs,b)
  
  patternMatchPattern = parenPattern <|> noArgConPattern <|> varPattern
  
  termDecl = eqTermDecl <|> whereTermDecl
  
  alternative = do c <- decName
                   as <- many alternativeArg
                   return (c,as)
  
  alternativeArg = parenType <|> typeCon
  
  typeDecl = do _ <- reserved "data"
                tycon <- decName
                alts <- option [] $ do
                  _ <- reservedOp "="
                  alternative `sepBy` reservedOp "|"
                _ <- reserved "end"
                return $ TypeDeclaration
                           tycon
                           [ (c, ConSig as (tyConH tycon)) | (c,as) <- alts ]
  
  statement = TmDecl <$> termDecl
          <|> TyDecl <$> typeDecl
  
  program = Program <$> many statement
  
  
  
  
  
  -- | A convenience function that will parse or return the parse error string.
  
  parseProgram :: String -> Either String Program
  parseProgram str =
    case parse (whiteSpace *> program <* eof) "(unknown)" str of
      Left e -> Left (show e)
      Right p -> Right p