> -- | 
> -- 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