hoq-0.3: src/Syntax/Parser/Parser.y
--
{
module Syntax.Parser.Parser
( pDefs, pExpr
) where
import Control.Monad.Trans
import Control.Monad.State
import Control.Monad.Error
import Data.Bifunctor
import Data.Void
import Data.Maybe
import Syntax.Parser.Lexer
import Syntax
import TypeChecking.Monad.Warn
}
%name pDefs Defs
%name pExpr Expr
%tokentype { Token }
%error { parseError }
%monad { Parser } { bind } { return' }
%lexer { alexScanTokens } { TokEOF }
%token
PIdent { TokIdent $$ }
Import { TokImport $$ }
Operator { TokOperator $$ }
Infix { TokInfix $$ }
Integer { TokInteger $$ }
FieldAcc { TokField $$ }
'\\' { TokLam $$ }
'(' { TokLParen $$ }
'case' { TokCase $$ }
'of' { TokOf $$ }
'data' { TokData }
'record' { TokRecord }
'constructor' { TokConstructor }
'where' { TokWhere $$ }
':' { TokColon }
'=' { TokEquals }
'{' { TokLBrace $$ }
'}' { TokRBrace }
';' { TokSemicolon }
')' { TokRParen }
'|' { TokPipe }
'@' { TokAt }
'`' { TokApos }
'->' { TokArrow }
'with' { TokWith $$ }
%%
Name :: { PName }
: PIdent { (getPos $1, Ident (getName $1)) }
| '(' Operator ')' { (getPos $2, Operator (getName $2)) }
InfixOp :: { PName }
: Operator { (getPos $1, Operator (getName $1)) }
| '`' PIdent '`' { (getPos $2, Ident (getName $2)) }
InfixOps :: { [PName] }
: InfixOp { [$1] }
| InfixOps InfixOp { $2:$1 }
LBrace :: { Posn }
: '{' {% \_ -> lift (modify (NoLayout :)) >> return $1 }
with :: { () }
: 'with' '{' {% \_ -> lift $ modify (NoLayout :) }
| 'with' error {% \_ -> lift $ modify (Layout $1 :) }
where :: { () }
: 'where' '{' {% \_ -> lift $ modify (NoLayout :) }
| 'where' error {% \_ -> lift $ modify (Layout $1 :) }
of :: { () }
: 'of' '{' {% \_ -> lift $ modify (NoLayout :) }
| 'of' error {% \_ -> lift $ modify (Layout $1 :) }
Def :: { Def }
: Name ':' Expr { DefType $1 $3 }
| Name Patterns '=' Expr { DefFun $1 (reverse $2) (Just $4) }
| Name Patterns { DefFun $1 (reverse $2) Nothing }
| 'data' Name Teles { DefData $2 (reverse $3) [] [] }
| 'data' Name Teles '=' Cons MaybeFunClauses { DefData $2 (reverse $3) (reverse $5) $6 }
| 'record' Name Teles where
MaybeConstructor Fields '}' MaybeFunClauses { DefRecord $2 (reverse $3) $5 (reverse $6) $8 }
| Infix Integer InfixOps { DefFixity (fst $1) (snd $1) (snd $2) (map snd $3) }
| Import { DefImport $1 }
Defs :: { [Def] }
: {- empty -} { [] }
| Def { [$1] }
| Defs ';' { $1 }
| Defs ';' Def { $3:$1 }
MaybeConstructor :: { Maybe PName }
: {- empty -} { Nothing }
| 'constructor' Name { Just $2 }
Fields :: { [Field] }
: {- empty -} { [] }
| Field { [$1] }
| Fields ';' { $1 }
| Fields ';' Field { $3:$1 }
Field :: { Field }
: PIdent ':' Expr { Field $1 $3 }
MaybeFunClauses :: { [Clause] }
: {- empty -} { [] }
| with FunClauses '}' { reverse $2 }
FunClauses :: { [Clause] }
: Name Patterns '=' Expr { [Clause $1 (reverse $2) $4] }
| FunClauses ';' { $1 }
| FunClauses ';' Name Patterns '=' Expr { Clause $3 (reverse $4) $6 : $1 }
Pattern :: { Term PName Void }
: Name { Apply (fst $1, snd $1) [] }
| '(' ')' { Apply ($1, Operator "") [] }
| '(' Name Patterns ')' { Apply (fst $2, snd $2) (reverse $3) }
Patterns :: { [Term PName Void] }
: {- empty -} { [] }
| Patterns Pattern { $2:$1 }
Con :: { Con }
: Name Teles { ConDef $1 (reverse $2) }
Cons :: { [Con] }
: Con { [$1] }
| Cons '|' Con { $3:$1 }
Tele :: { Tele }
: Expr5 { TypeTele Explicit $1 }
| LBrace Expr5 '}' { TypeTele Implicit $2 }
| '(' Exprs ':' Expr ')' {% \_ -> mapM exprToVar $2 >>= \vars -> return (VarsTele Explicit (reverse vars) $4) }
| LBrace Exprs ':' Expr '}' {% \_ -> mapM exprToVar $2 >>= \vars -> return (VarsTele Implicit (reverse vars) $4) }
Teles :: { [Tele] }
: {- empty -} { [] }
| Teles Tele { $2:$1 }
PiTele :: { (Explicit,PiTele) }
: '(' Exprs ':' Expr ')' { (Explicit, PiTele $1 (reverse $2) $4) }
| LBrace Exprs ':' Expr '}' { (Implicit, PiTele $1 (reverse $2) $4) }
PiTeles :: { [(Explicit,PiTele)] }
: PiTele { [$1] }
| PiTeles PiTele { $2:$1 }
PIdents :: { [PIdent] }
: PIdent { [$1] }
| PIdents PIdent { $2:$1 }
Expr :: { RawExpr }
: Expr1 { $1 }
| '\\' PIdents '->' Expr { Apply ($1, Lam $ reverse $ map getName $2) [$4] }
Expr1 :: { RawExpr }
: Expr2 { $1 }
| Expr2 '->' Expr1 { Apply (termPos $1, Pi Explicit []) [$1, $3] }
| PiTeles '->' Expr1 {% \_ -> piExpr (reverse $1) $3 }
Expr2 :: { RawExpr }
: Expr3 { $1 }
| Expr3 '=' Expr3 { Apply (termPos $1, PathImp) [$1,$3] }
Expr3 :: { RawExpr }
: Expr4 { Apply (termPos $1, Null) [$1] }
| Expr3 '@' Expr4 { Apply (termPos $1, At) [$1, $3] }
| Expr3 InfixOp Expr4 { Apply (termPos $1, Name (Infix InfixL 90) $ snd $2) [$1, $3] }
Expr4 :: { RawExpr }
: Exprs { let e:es = reverse $1 in apps e es }
| Expr4 FieldAcc EExprs { Apply (termPos $1, FieldAcc 0 $2) ($1 : reverse $3) }
EExprs :: { [RawExpr] }
: {- empty -} { [] }
| EExprs Expr5 { $2:$1 }
Exprs :: { [RawExpr] }
: Expr5 { [$1] }
| Exprs Expr5 { $2:$1 }
Expr5 :: { RawExpr }
: Name { Apply (fst $1, Name Prefix $ snd $1) [] }
| '(' Expr ')' { $2 }
| 'case' Expr of CaseClauses '}' { Apply ($1, Case $ map vacuous $ reverse $ fst $4) ($2 : reverse (snd $4)) }
CaseClauses :: { ([Term PName Void], [RawExpr]) }
: Name Patterns '->' Expr { ([Apply $1 $ reverse $2], [$4]) }
| CaseClauses ';' { $1 }
| CaseClauses ';' Name Patterns '->' Expr { (Apply $3 (reverse $4) : fst $1, $6 : snd $1) }
{
return' :: a -> Parser a
return' a _ = return a
bind :: Parser a -> (a -> Parser b) -> Parser b
bind p k e = p e >>= \a -> k a e
data PiTele = PiTele Posn [RawExpr] RawExpr
piExpr :: [(Explicit,PiTele)] -> RawExpr -> ParserErr RawExpr
piExpr [] term = return term
piExpr ((e, PiTele pos t1 t2) : teles) term = do
vars <- mapM exprToVar t1
term' <- piExpr teles term
return $ Apply (pos, Pi e $ map getName vars) [t2,term']
termPos :: RawExpr -> Posn
termPos (Apply (pos, _) _) = pos
termPos _ = error "termPos"
exprToVar :: RawExpr -> ParserErr PIdent
exprToVar (Apply (pos, Name Prefix (Ident v)) []) = return (PIdent pos v)
exprToVar term = throwError [(termPos term, "Expected a list of identifiers")]
parseError :: Token -> Parser a
parseError tok (pos,_) = throwError [(maybe pos id (tokGetPos tok), "Syntax error")]
myLexer = alexScanTokens
}