why3-0.8: src/Language/Why3/Parser.y
-- vim: ft=haskell
{
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE OverloadedStrings #-}
module Language.Why3.Parser
( parse
, ParseM
, theories
, expr
, pType
) where
import Language.Why3.AST
import Language.Why3.Lexer
import qualified Data.ByteString.Lazy as BS
import qualified Data.Text.Lazy as Lazy
import Data.Text ( Text )
import qualified Data.Text as Text
import Control.Monad(liftM,ap)
import qualified Control.Applicative as A
}
%token
INTEGER { Token { tokenType = Num $$ _ } }
REAL { Token { tokenType = RealTok, tokenText = Lazy.toStrict -> $$ } }
STR { Token { tokenType = StrLit (Lazy.toStrict -> $$) } }
LIDENT { Token { tokenType = Ident Unqual Lower, tokenText = Lazy.toStrict -> $$ } }
UIDENT { Token { tokenType = Ident Unqual Upper, tokenText = Lazy.toStrict -> $$ } }
QLIDENT { Token { tokenType = Ident Qual Lower, tokenText = Lazy.toStrict -> $$ } }
QUIDENT { Token { tokenType = Ident Qual Upper, tokenText = Lazy.toStrict -> $$ } }
TQUALID { Token { tokenType = TIdent, tokenText = Lazy.toStrict -> $$ } }
BANG_OP { Token { tokenType = Op BangOp, tokenText = Lazy.toStrict -> $$ } }
OP4 { Token { tokenType = Op (OtherOp 4), tokenText = Lazy.toStrict -> $$ } }
OP3 { Token { tokenType = Op (OtherOp 3), tokenText = Lazy.toStrict -> $$ } }
OP2 { Token { tokenType = Op (OtherOp 2), tokenText = Lazy.toStrict -> $$ } }
OP1 { Token { tokenType = Op (OtherOp 1), tokenText = Lazy.toStrict -> $$ } }
'[' { Token { tokenType = Sym BracketL, tokenPos = $$ }}
']' { Token { tokenType = Sym BracketR, tokenPos = $$ }}
'(' { Token { tokenType = Sym ParenL , tokenPos = $$ }}
')' { Token { tokenType = Sym ParenR , tokenPos = $$ }}
'{' { Token { tokenType = Sym CurlyL , tokenPos = $$ }}
'}' { Token { tokenType = Sym CurlyR , tokenPos = $$ }}
'_' { Token { tokenType = Sym Underscore, tokenPos = $$ }}
'=' { Token { tokenType = Sym Eq, tokenPos = $$ }}
'\'' { Token { tokenType = Sym Quote, tokenPos = $$ }}
',' { Token { tokenType = Sym Comma, tokenPos = $$ }}
'.' { Token { tokenType = Sym Dot, tokenPos = $$ }}
':' { Token { tokenType = Sym Colon, tokenPos = $$ }}
';' { Token { tokenType = Sym Semi, tokenPos = $$ }}
'|' { Token { tokenType = Sym Bar, tokenPos = $$ }}
'<-' { Token { tokenType = Op ArrowL, tokenPos = $$ }}
'->' { Token { tokenType = Op ArrowR, tokenPos = $$ }}
'<->' { Token { tokenType = Op ArrowLR, tokenPos = $$ }}
'theory' { Token { tokenType = KW KW_theory, tokenPos = $$ }}
'end' { Token { tokenType = KW KW_end, tokenPos = $$ }}
'goal' { Token { tokenType = KW KW_goal, tokenPos = $$ }}
'use' { Token { tokenType = KW KW_use, tokenPos = $$ }}
'import' { Token { tokenType = KW KW_import, tokenPos = $$ }}
'export' { Token { tokenType = KW KW_export, tokenPos = $$ }}
'predicate' { Token { tokenType = KW KW_predicate, tokenPos = $$ }}
'function' { Token { tokenType = KW KW_function, tokenPos = $$ }}
'constant' { Token { tokenType = KW KW_constant, tokenPos = $$ }}
'axiom' { Token { tokenType = KW KW_axiom, tokenPos = $$ }}
'lemma' { Token { tokenType = KW KW_lemma, tokenPos = $$ }}
'type' { Token { tokenType = KW KW_type, tokenPos = $$ }}
'with' { Token { tokenType = KW KW_with, tokenPos = $$ }}
'as' { Token { tokenType = KW KW_as, tokenPos = $$ }}
'true' { Token { tokenType = KW KW_true, tokenPos = $$ }}
'false' { Token { tokenType = KW KW_false, tokenPos = $$ }}
'forall' { Token { tokenType = KW KW_forall,tokenPos = $$ }}
'exists' { Token { tokenType = KW KW_exists,tokenPos = $$ }}
'not' { Token { tokenType = KW KW_not, tokenPos = $$ }}
'\\/' { Token { tokenType = Op Disj, tokenPos = $$ }}
'||' { Token { tokenType = Op AsymDisj, tokenPos = $$ }}
'/\\' { Token { tokenType = Op Conj, tokenPos = $$ }}
'&&' { Token { tokenType = Op AsymConj, tokenPos = $$ }}
'if' { Token { tokenType = KW KW_if, tokenPos = $$ }}
'match' { Token { tokenType = KW KW_match, tokenPos = $$ }}
'then' { Token { tokenType = KW KW_then, tokenPos = $$ }}
'else' { Token { tokenType = KW KW_else, tokenPos = $$ }}
'let' { Token { tokenType = KW KW_let, tokenPos = $$ }}
'in' { Token { tokenType = KW KW_in, tokenPos = $$ }}
%name theories theories
%name theory theory
%name pType type
%name expr expr
%tokentype { Token }
%monad { ParseM }
%lexer { lexerP } { Token { tokenType = EOF } }
%nonassoc QUALID
%nonassoc QUANT
%nonassoc LET IF
%nonassoc LABEL
%right '->' '<->'
%right '\\/' '||'
%right '/\\' '&&'
%nonassoc 'not'
%left OP1 '='
%left OP2
%left OP3
%left OP4 '.' ':'
%nonassoc PREFIX_OP
%left APP
%nonassoc '['
%nonassoc BANG_OP
%%
--------------------------------------------------------------------------------
theories :: { [Theory] }
: theories_rev { reverse $1 }
theories_rev :: { [Theory] }
: { [] }
| theories_rev theory { $2 : $1 }
theory :: { Theory }
: 'theory' uident decls 'end' { Theory $2 (reverse $3) }
decls :: { [Decl] }
: { [] }
| decls decl { $2 : $1 }
-- XXX: A lot of these are missing the 'with' part
decl :: { Decl }
: 'use' imp_exp tqualid opt_as { Use $2 $3 $4 }
| 'predicate' lident labels type_params
{ Predicate $2 $3 (map snd $4) }
| 'predicate' lident labels type_params '=' expr
{ PredicateDef $2 $3 $4 $6 }
| 'function' lident labels type_params ':' type
{ Function $2 $3 (map snd $4) $6 }
| 'function' lident labels type_params ':' type '=' expr
{ FunctionDef $2 $3 $4 $6 $8 }
| 'constant' lident labels ':' type
{ Function $2 $3 [] $5 }
| 'constant' lident labels ':' type '=' expr
{ FunctionDef $2 $3 [] $5 $7 }
| 'axiom' ident ':' expr { Axiom $2 $4 }
| 'lemma' ident ':' expr { Lemma $2 $4 }
| 'goal' ident ':' expr { Goal $2 $4 }
| 'type' lident labels tyvars { Type $2 $3 $4 }
| 'type' lident labels tyvars '=' type_defn{ TypeDef $2 $3 $4 $6 }
imp_exp :: { Maybe ImpExp }
: 'import' { Just Import }
| 'export' { Just Export }
| {- empty -} { Nothing }
opt_as :: { Maybe Name }
: {- empty -} { Nothing }
| 'as' uident { Just $2 }
--------------------------------------------------------------------------------
-- Types
type_defn :: { TypeDef }
: type { Ty $1 }
| '{' rec_fields '}' { TyRecord $ reverse $2 }
| opt_bar type_cases { TyCase (reverse $2) }
opt_bar :: { () }
opt_bar
: '|' { () }
| {- empty -} { () }
-- reversed
type_cases :: { [TyCaseAlt] }
: type_case { [$1] }
| type_cases '|' type_case { $3 : $1 }
type_case :: { TyCaseAlt }
: uident labels type_params { TyCaseAlt $1 $2 $3 }
-- reversed
rec_fields :: { [(Name,Type)] }
: rec_field { [$1] }
| rec_fields ';' rec_field { $3 : $1 }
rec_field :: { (Name,Type) }
: lident ':' type { ($1, $3) }
type :: { Type }
: lqualid typeAs { TyCon $1 (reverse $2) }
| typeA { $1 }
typeA :: { Type }
: '\'' lident { TyVar $2 }
| lqualid { TyCon $1 [] }
| '(' type ')' { $2 }
| '(' ')' { Tuple [] }
| '(' types2 ')' { Tuple (reverse $2) }
typeAs :: { [Type] }
: typeA { [$1] }
| typeAs typeA { $2 : $1 }
-- reversed
types2 :: { [Type] }
: type ',' type { [$3, $1] }
| types2 ',' type { $3 : $1 }
-- reversed
tyvars :: { [(Name, [Text])] }
: {- empty -} { [] }
| tyvars '\'' lident labels { ($3,$4) : $1 }
-- NOT reversed
type_params :: { [(Maybe Name, Type)] }
: {- empty -} { [] }
| type_params type_param { $1 ++ $2 }
-- NOT reversed!
type_param :: { [ (Maybe Name, Type) ] }
: typeA { [ (Nothing, $1) ] }
{- HACKERY:
Next is the case for: `x y z : Int`
It is parsed like this so tha we can decide what to do with 1 look ahead.
Technically, this is not fully correct because we'll also accept things like:
`x (y) : Int` but it seems close enough. -}
| '(' type ':' type ')' {% mkTypeParam $2 >>= \xs -> return
[ (Just x, $4) | x <- xs ] }
--------------------------------------------------------------------------------
-- Names
opt_label :: { Maybe Text }
: STR { Just $1 }
| {- empty -} { Nothing }
labels :: { [ Text ] }
: labelsRev { reverse $1 }
-- reverse
labelsRev :: { [ Text ] }
: {- empty -} { [] }
| labelsRev STR { $2 : $1 }
ident :: { Name }
: LIDENT opt_label { $1 }
| UIDENT opt_label { $1 }
lident :: { Name }
: LIDENT { $1 }
lidents1 :: { [Name] }
: lident { [$1] }
| lidents1 lident { $2 : $1 }
uident :: { Name }
: UIDENT { $1 }
lqualid :: { Name }
: LIDENT { $1 }
| QLIDENT { $1 }
uqualid :: { Name }
: UIDENT { $1 }
| QUIDENT { $1 }
prefix_op :: { Name }
: OP1 { $1 }
| OP2 { $1 }
| OP3 { $1 }
| OP4 { $1 }
qualid :: { Name }
: uqualid { $1 }
| lqualid %prec QUALID { $1 }
tqualid
: uqualid { $1 }
| TQUALID { $1 }
--------------------------------------------------------------------------------
expr :: { Expr }
: exprA { $1 }
| qualid exprAs1 { App $1 (reverse $2) }
| prefix_op expr %prec PREFIX_OP { App $1 [$2] }
| expr '=' expr { App "=" [$1, $3] }
| expr OP1 expr { App $2 [$1, $3] }
| expr OP2 expr { App $2 [$1, $3] }
| expr OP3 expr { App $2 [$1, $3] }
| expr OP4 expr { App $2 [$1, $3] }
| expr '.' lqualid { Field $3 $1 }
| 'if' expr 'then' expr
'else' expr %prec IF { If $2 $4 $6 }
| 'match' revExprs1 'with' opt_bar
revExprCases 'end' { Match (reverse $2) (reverse $5) }
| 'let' pattern '=' expr
'in' expr %prec LET { Let $2 $4 $6 }
| expr '->' expr { Conn Implies $1 $3 }
| expr '<->' expr { Conn Iff $1 $3 }
| expr '/\\' expr { Conn And $1 $3 }
| expr '&&' expr { Conn AsymAnd $1 $3 }
| expr '\\/' expr { Conn Or $1 $3 }
| expr '||' expr { Conn AsymOr $1 $3 }
| expr ':' type { Cast $1 $3 }
| STR expr %prec LABEL { Labeled $1 $2 }
| 'not' expr { Not $2 }
| quant binders1 opt_trig '.' expr %prec QUANT
{ Quant $1 (concat (reverse $2)) $3 $5 }
quant :: { Quant }
: 'forall' { Forall }
| 'exists' { Exists }
binder :: { [(Name,Type)] }
: lidents1 ':' type { [ (x,$3) | x <- reverse $1 ] }
binders1 :: { [[(Name,Type)]] }
: binder { [$1] }
| binders1 ',' binder { $3 : $1 }
opt_trig :: { [[Expr]] }
: {- empty -} { [] }
| '[' triggers ']' { reverse $2 }
triggers :: { [[Expr]] }
: trigger { [reverse $1] }
| triggers '|' trigger { reverse $3 : $1 }
trigger :: { [Expr] }
: expr { [$1] }
| trigger ',' expr { $3 : $1 }
exprA :: { Expr }
: INTEGER { Lit $ Integer $1 }
| REAL { Lit $ Real $1 }
| 'true' { Lit $ Bool True }
| 'false' { Lit $ Bool False }
| qualid { App $1 [] }
| BANG_OP exprA { App $1 [$2] }
| exprA '[' expr ']' { App "[]" [$1, $3] }
| exprA '[' expr '<-' expr ']' { App "[<-]" [$1, $3, $5] }
| '(' expr ')' { $2 }
| '{' term_fields1 '}' { Record (reverse $2) }
-- TODO: not properly implemented
| '{' expr 'with' term_fields1 '}' { RecordUpdate $2 (reverse $4) }
-- reversed
term_fields1 :: { [(Name,Expr)] }
: term_field { [$1] }
| term_fields1 ';' term_field { $3 : $1 }
term_field :: { (Name, Expr) }
term_field
: lqualid '=' expr { ($1,$3) }
-- reversed
exprAs1 :: { [Expr] }
: exprA { [$1] }
| exprAs1 exprA { $2 : $1 }
pattern :: { Pattern }
: patternA { $1 }
| uident revPatternAs1 { PCon $1 (reverse $2) }
patternA :: { Pattern }
: '_' { PWild }
| lident { PVar $1 }
| uident { PCon $1 [] }
| '(' pattern ')' { $2 }
revPatternAs1 :: { [Pattern] }
: patternA { [$1] }
| revPatternAs1 patternA { $2 : $1 }
revExprs1 :: { [Expr] }
: expr { [$1] }
| revExprs1 ',' expr { $3 : $1 }
revExprCases :: { [(Pattern, Expr)] }
: exprCase { [$1] }
| revExprCases '|' exprCase { $3 : $1 }
exprCase :: { (Pattern,Expr) }
: pattern '->' expr { ($1, $3) }
{
mkTypeParam :: Type -> ParseM [Name]
mkTypeParam ty =
case ty of
TyCon x ts | notQual x && all simpleTyCon ts ->
return (x : [ y | TyCon y [] <- ts ])
_ -> fail "Malformed type-parameters"
where
simpleTyCon (TyCon x []) = notQual x
simpleTyCon _ = False
notQual nm = not (Text.any (== '.') nm)
textPos :: Position -> String
textPos p = show (line p) ++ ":" ++ show (col p)
happyError :: ParseM a
happyError = P $ \ts ->
Left $ "Parser error around " ++
case ts of
t : _ -> textPos (tokenPos t)
[] -> "the end of the file"
data ParseM a = P { unP :: [Token] -> Either String (a,[Token]) }
instance Functor ParseM where
fmap = liftM
instance A.Applicative ParseM where
pure = return
(<*>) = ap
instance Monad ParseM where
return a = P (\x -> Right (a,x))
fail x = P (\_ -> Left x)
P m >>= f = P (\x -> case m x of
Left err -> Left err
Right (a,y) -> unP (f a) y)
lexerP :: (Token -> ParseM a) -> ParseM a
lexerP k = P $ \ts ->
case ts of
Token { tokenType = Err e, tokenText = txt } : _ ->
Left $
case e of
UnterminatedComment -> "unterminated comment"
UnterminatedString -> "unterminated string"
UnterminatedChar -> "unterminated character"
InvalidString -> "invalid string literal: " ++ Lazy.unpack txt
LexicalError -> "unexpected symbol"
t : more -> unP (k t) more
[] -> Left "unexpected end of file"
parse :: ParseM a -> BS.ByteString -> Either String a
parse p txt = case unP p (lexer txt) of
Left err -> Left err
Right (a,_) -> Right a
}