Parser.hs

module PiSigma.Parser (module PiSigma.Parser, Parser) where

import Prelude hiding (pi)
import Data.Char
import Data.List

import Control.Monad
import Control.Applicative hiding ((<|>), many)

import Text.ParserCombinators.Parsec as P hiding (token, label)

import PiSigma.Syntax hiding (label)

type SParser = CharParser ()

-- * Comments and whitespace

blockComment :: SParser ()
blockComment = () <$ try (string "{-") <* inComment <* string "-}"

inComment :: SParser ()
inComment =
  () <$ many (choice [ () <$ noneOf "{-"
                     , try $ () <$ char '-' <* notFollowedBy (char '}')
                     , try $ () <$ char '{' <* notFollowedBy (char '-')
                     , blockComment ])

lineComment :: SParser ()
lineComment = () <$ try (string "--") <* many (noneOf "\n")

whiteSpace :: SParser ()
whiteSpace = () <$ spaces <* many ((lineComment <|> blockComment) <* spaces)
             <?> ""

-- * Identifiers

identChar :: SParser Char
identChar = alphaNum <|> oneOf "_'"

ident :: SParser String
ident = 
  (try $  do
            xs <- (:) <$> letter <*> many identChar <* whiteSpace
            guard (xs `notElem` keywords)
            return xs) <?> "identifier"

keywords :: [String]
keywords = [ "case", "of", "let", "in", "split", "Type", "with" ]

label :: SParser Name
label = char '\'' *> ident

-- * Tokens

token :: String -> SParser String
token xs = (try $ (string xs <* whiteSpace)) <?> show xs

-- * Brackets

parensed   = between (token "(") (token ")")
braced     = between (token "{") (token "}")
bracketed  = between (token "[") (token "]")

-- * Terms

sTerm5 :: SParser Term
sTerm5 =
       Type   <$  token "Type"
  <|>  (Enum  <$> braced (many ident) <?> "enumeration")
  <|>  Case   <$  token "case" <*> sTerm <* token "of"
              <*> braced (sBranch `sepBy` token "|")
  <|>  (Label <$> label <?> "label")
  <|>  (Box   <$> bracketed sTerm <?> "box")
  <|>  (Lift  <$  token "^" <*> sTerm5 <?> "'^'")
  <|>  Var    <$> ident
  <|>  parensed sTerm

sTerm4 :: SParser Term
sTerm4 =
       try (parensed (curry Pair <$> sTerm <* token "," <*> sTerm))
  <|>  sTerm5

sTerm3 :: SParser Term
sTerm3 =
       try (parensed (sigmas <$> many1 ident <* token ":" <*> sTerm) <* token "*")
          <*> sTerm3
  <|>  Force <$  token "!" <*> sTerm4
  <|>  foldl1 (:.) <$> many1 sTerm4

sTerm2 :: SParser Term
sTerm2 =
       foldl1 (-*-) <$> sTerm3 `sepBy1` token "*"

-- TODO: make more beautiful or renumber
sTerm1b :: SParser Term
sTerm1b =
       try (parensed (pis <$> many1 ident <* token ":" <*> sTerm) <* token "->")
          <*> sTerm
  <|>  sTerm2
       
sTerm1 :: SParser Term
sTerm1 =
       flip ($) <$> sTerm1b <*> option id (flip (->-) <$ token "->" <*> sTerm)

sTerm :: SParser Term
sTerm =
       lam   <$  token "\\" <*> many ident <* token "->" <*> sTerm
  <|>  split <$  token "split" <*> sTerm <* token "with"
             <*  token "(" <*> ident <* token "," <*> ident <* token ")"
             <*  token "->" <*> sTerm
  <|>  Let   <$  token "let" <*> sProg <* token "in" <*> sTerm
  <|>  sTerm1

sProg :: SParser Prog
sProg = concat <$> (sEntry `sepEndBy` token ";")

sEntry :: SParser [Entry]
sEntry = 
    do
      n <- ident
      b <- (True <$ token ":" <|> False <$ token "=")
      t <- sTerm
      if b
        then do
               d <- option Nothing (Just <$ token "=" <*> sTerm)
               case d of
                 Nothing -> return [Decl n t]
                 Just t' -> return [Decl n t, Defn n t']
        else return [Defn n t]

sBranch :: SParser (Label,Term)
sBranch = (,) <$> ident <* token "->" <*> sTerm

sPhrase :: SParser Phrase
sPhrase =
       (try $ Prog <$> sProg <* eof) <|> Term <$> sTerm <* eof

s2Terms :: SParser (Term, Term)
s2Terms = (,) <$> sTerm5 <*> sTerm5

parse p = P.parse (whiteSpace *> p <* eof)