>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
> module Ivor.TermParser(pTerm, pNoApp, pInductive,
> parseTermString, parseDataString) where
> import Ivor.ViewTerm
> import Ivor.TTCore(Name(..))
> import Text.ParserCombinators.Parsec
> import Text.ParserCombinators.Parsec.Expr
> import Text.ParserCombinators.Parsec.Language
> import qualified Text.ParserCombinators.Parsec.Token as PTok
> import Debug.Trace
> type TokenParser a = PTok.TokenParser a
> lexer :: TokenParser ()
> lexer = PTok.makeTokenParser haskellDef
> whiteSpace= PTok.whiteSpace lexer
> lexeme = PTok.lexeme lexer
> symbol = PTok.symbol lexer
> natural = PTok.natural lexer
> parens = PTok.parens lexer
> semi = PTok.semi lexer
> comma = PTok.comma lexer
> identifier= PTok.identifier lexer
> reserved = PTok.reserved lexer
> operator = PTok.operator lexer
> reservedOp= PTok.reservedOp lexer
> lchar = lexeme.char
> app :: Parser (ViewTerm -> ViewTerm -> ViewTerm)
> app = do whiteSpace ; return App
> arrow :: Parser (ViewTerm -> ViewTerm -> ViewTerm)
> arrow = do symbol "->" ; return $ Forall (name "X")
>
> pTerm :: Maybe (Parser ViewTerm)
>
> -> Parser ViewTerm
> pTerm Nothing = try (do chainl1 (pNoApp Nothing) app)
> <|> (pNoApp Nothing)
>
> pTerm (Just ext) = try (do chainl1 (pNoApp (Just ext)) app)
>
> <|> try (pNoApp (Just ext))
> <|> ext
>
>
> pNoApp :: Maybe (Parser ViewTerm) -> Parser ViewTerm
> pNoApp ext = try (do chainr1 (pExp ext) arrow)
> <|> pExp ext
> pNoInfix :: Maybe (Parser ViewTerm) -> Parser ViewTerm
> pNoInfix ext =
> do lchar '[' ; bs <- bindList ext ; lchar ']'
> sc <- pTerm ext ;
> return $ bindAll Lambda bs sc
> <|> try (do lchar '(' ; bs <- bindList ext ; lchar ')'
> option "" (symbol "->")
> sc <- pTerm ext ;
> return $ bindAll Forall bs sc)
> <|> do reserved "let" ; var <- identifier;
> lchar ':' ; ty <- pTerm ext ; lchar '=' ; val <- pTerm ext ;
> reserved "in" ; sc <- pTerm ext ;
> return $ Let (UN var) ty val sc
> <|> do lchar '(' ; t <- pTerm ext ; lchar ')' ; return t
> <|> do lchar '<'
> (nm,args) <- computation ext ; lchar ':' ; lty <- pTerm ext
> lchar '>';
> return $ Label nm args lty
> <|> do reserved "call" ; lchar '<'
> (nm,args) <- computation ext ;
> lchar '>' ; tm <- pNoApp ext;
> return $ Call nm args tm
> <|> do reserved "return"; tm <- pTerm ext;
> return $ Return tm
> <|> do nm <- identifier ; return (Name Unknown (UN nm))
> <|> do lchar '*' ; return Star
> <|> do lchar '_' ; return Placeholder
> <|> do lchar '?' ; var <- identifier ;
> return $ Metavar (UN var)
> <|> try (do symbol "{'" ; tm <- pTerm ext; lchar '}'
> return $ Quote tm)
> <|> try (do symbol "{{" ; tm <- pTerm ext; symbol "}}"
> return $ Code tm)
> <|> try (do symbol "!" ; tm <- pNoApp ext;
> return $ Eval tm)
> <|> try (do symbol "~" ; tm <- pNoApp ext;
> return $ Escape tm)
> <|> do case ext of
> Nothing -> fail "Parse error"
> Just ext -> ext
>
> pExp :: Maybe (Parser ViewTerm) -> Parser ViewTerm
> pExp ext = pNoInfix ext
> opTable = [[op "$" (\ l r -> apply (Name Unknown (name "Eq"))
> [Placeholder,Placeholder,l,r])
> AssocLeft]]
> where op s f assoc = Infix (do string s
> return f)
> assoc
>
> pInductive :: Maybe (Parser ViewTerm)
>
> -> Parser Inductive
> pInductive ext = do nm <- identifier
> parmsM <- many (do lchar '('
> xs <- bindList ext
> lchar ')' ; return xs)
> lchar ':'
> indicesM <- many (do lchar '('
> xs <- bindList ext
> lchar ')' ; return xs)
> ty <- pTerm ext ; whereIntro
> cons <- sepBy (constructor ext) (lchar '|')
> return $ Inductive (UN nm)
> (concat parmsM)
> (concat indicesM)
> ty cons
> where whereIntro = do lchar '='
> return ()
> <|> do reserved "where"
> return ()
> constructor ext = do nm <- identifier ; lchar ':'
> ty <- pTerm ext
> return $ (UN nm,ty)
> bindList :: Maybe (Parser ViewTerm) -> Parser [(Name, ViewTerm)]
> bindList ext
> = do namelist <- sepBy1 identifier comma
> lchar ':'
> ty <- pTerm ext
> rest <- option [] (do semi ; bindList ext)
> return $ (map (\x -> (UN x,ty)) namelist) ++ rest
> bindAll binder [] sc = sc
> bindAll binder ((n,ty):xs) sc = binder n ty (bindAll binder xs sc)
> computation :: Maybe (Parser ViewTerm) -> Parser (Name, [ViewTerm])
> computation ext = do nm <- identifier ; args <- many (pNoApp ext)
> return (UN nm, args)
>
>
> parseTermString :: Monad m => String -> m ViewTerm
> parseTermString str
> = case parse (do t <- pTerm Nothing ; eof ; return t) "(input)" str of
> Left err -> fail (show err)
> Right tm -> return tm
>
>
> parseDataString :: Monad m => String -> m Inductive
> parseDataString str
> = case parse (do t <- pInductive Nothing ; eof ; return t)
> "(input)" str of
> Left err -> fail (show err)
> Right d -> return d