less prototype, less bad code implementation of CCHM type theory
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 

107 lines
2.5 KiB

{
module Presyntax.Parser where
import qualified Data.Text as T
import Data.Text (Text)
import Presyntax.Presyntax
import Presyntax.Tokens
import Presyntax.Lexer
}
%name parseExp Exp
%name parseStmt Statement
%name parseProg Program
%tokentype { Token }
%monad { Alex }
%lexer { lexer } { Token TokEof _ _ }
%errorhandlertype explist
%error { parseError }
%token
var { Token (TokVar $$) _ _ }
'(' { Token TokOParen _ _ }
')' { Token TokCParen _ _ }
'{' { Token TokOBrace _ _ }
'}' { Token TokCBrace _ _ }
'\\' { Token TokLambda _ _ }
'->' { Token TokArrow _ _ }
':' { Token TokColon _ _ }
';' { Token TokSemi _ _ }
'=' { Token TokEqual _ _ }
',' { Token TokComma _ _ }
'*' { Token TokStar _ _ }
'.1' { Token TokPi1 _ _ }
'.2' { Token TokPi2 _ _ }
%%
Exp :: { Expr }
Exp
: Exp ExpProj { App Ex $1 $2 }
| Exp '{' Exp '}' { App Im $1 $3 }
| '\\' LambdaList '->' Exp { makeLams $2 $4 }
| '(' VarList ':' Exp ')' ProdTail { makePis Ex $2 $4 $6 }
| '{' VarList ':' Exp '}' ProdTail { makePis Im $2 $4 $6 }
| ExpProj '->' Exp { Pi Ex (T.singleton '_') $1 $3 }
| '(' VarList ':' Exp ')' '*' Exp { makeSigmas $2 $4 $7 }
| ExpProj '*' Exp { Sigma (T.singleton '_') $1 $3 }
| ExpProj { $1 }
ProdTail :: { Expr }
: '(' VarList ':' Exp ')' ProdTail { makePis Ex $2 $4 $6 }
| '{' VarList ':' Exp '}' ProdTail { makePis Im $2 $4 $6 }
| '->' Exp { $2 }
LambdaList :: { [(Plicity, Text)] }
: var { [(Ex, $1)] }
| var LambdaList { (Ex, $1):$2 }
| '{'var'}' { [(Im, $2)] }
| '{'var'}' LambdaList { (Im, $2):$4 }
VarList :: { [Text] }
: var { [$1] }
| var VarList { $1:$2 }
ExpProj :: { Expr }
: ExpProj '.1' { Proj1 $1 }
| ExpProj '.2' { Proj2 $1 }
| Atom { $1 }
Atom :: { Expr }
: var { Var $1 }
| '(' Tuple ')' { $2 }
Tuple :: { Expr }
: Exp { $1 }
| Exp ',' Tuple { Pair $1 $3 }
Statement :: { Statement }
: var ':' Exp { Decl $1 $3 }
| var '=' Exp { Defn $1 $3 }
Program :: { [Statement] }
: Statement { [$1] }
| Statement ';' Program { $1:$3 }
{
lexer cont = alexMonadScan >>= cont
parseError x = alexError (show x)
makeLams xs b = foldr (uncurry Lam) b xs
makePis p xs t b = foldr (flip (Pi p) t) b xs
makeSigmas xs t b = foldr (flip Sigma t) b xs
}