ivor-0.1.5: Ivor/TermParser.lhs
> -- |
> -- Module : Ivor.TermParser
> -- Copyright : Edwin Brady
> -- Licence : BSD-style (see LICENSE in the distribution)
> --
> -- Maintainer : eb@dcs.st-and.ac.uk
> -- Stability : experimental
> -- Portability : non-portable
> --
> -- Extensible Parsec based parsing library for 'ViewTerm's.
> --
> -- Briefly, the syntax is as follows:
> --
> -- * @[x:A]y@ -- Lambda binding with scope @y@.
> --
> -- * @(x:A) -> B@ -- Forall binding with scope @B@ (@->@ optional).
> --
> -- * @A -> B@ -- Forall binding where name bound is not used in @B@..
> --
> -- * @let x:A=v in y@ -- Let binding, @x=v@ in scope @y@.
> --
> -- * @f a@ -- Function application (left associative, by juxtaposition).
> --
> -- * @[identifier]@ -- names are legal Haskell identifiers.
> --
> -- * @\*@ -- Asterisk is type of types.
> --
> -- * @_@ -- Underscore is a placeholder.
> --
> -- * @?identifier@ -- metavariable, add a name to be defined later
> --
> -- Lambda\/forall bindings of multiple variables are also accepted,
> -- in the form @[x,y:A;z:B]@
> --
> -- Staging annotations have the following syntax:
> --
> -- * @{'x}@ -- quoted term @x@
> --
> -- * @{{A}}@ -- code type @A@ (if @x:A@, @{'x}:{{A}}@
> --
> -- * @!x@ -- evaluate a quoted term
> --
> -- * @~x@ -- escape a quoted term (i.e. splice into a quoted term)
> --
> -- Extensions for labelled types (see McBride\/McKinna \"The View
> -- From The Left\" for details):
> --
> -- * @\<[identifier] args : t\>@ -- Labelled type.
> --
> -- * @call \<label\> term@ -- Call a computation.
> --
> -- * @return t@ -- Return a value from a computation.
> --
> 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")
> -- | Basic parsec combinator for parsing terms.
> pTerm :: Maybe (Parser ViewTerm) -- ^ Extra parse rules (for example
> -- for any primitive types or operators you might have added).
> -> Parser ViewTerm
> pTerm Nothing = try (do chainl1 (pNoApp Nothing) app)
> <|> (pNoApp Nothing)
> -- <|> pInfix Nothing
> pTerm (Just ext) = try (do chainl1 (pNoApp (Just ext)) app)
> -- <|> try (pInfix (Just ext))
> <|> try (pNoApp (Just ext))
> <|> ext
> -- | Parse a term which is not an application;
> -- use for parsing lists of terms.
> 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
> -- | Parse an expression with infix expressions (doesn't work!)
> pExp :: Maybe (Parser ViewTerm) -> Parser ViewTerm
> pExp ext = pNoInfix ext -- buildExpressionParser opTable (pNoInfix ext)
-- > pInfix ext = do
-- > lexp <- trace ("Trying = ") $ pNoApp ext
-- > lchar '='
-- > rexp <- trace (show lexp) $ pTerm ext
-- > return $ apply (Name Unknown (name "Eq"))
-- > [Placeholder,Placeholder,lexp,rexp]
> 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
> -- | Basic parsec combinator for parsing inductive data types
> pInductive :: Maybe (Parser ViewTerm) -- ^ Extra parse rules (for example
> -- for any primitive types or operators you might have added).
> -> 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)
> -- | Parse a string into a ViewTerm, without mucking about with parsec
> -- or any extra parse rules.
> 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
> -- | Parse a string into an Inductive, without mucking about with parsec
> -- or any extra parse rules.
> 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