-- File generated by the BNF Converter. -- Parser definition for use with Happy. { {-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-} {-# LANGUAGE PatternSynonyms #-} module ParCubicaltt ( happyError , myLexer , pModule , pImp , pListImp , pDecl , pListDecl , pExpWhere , pExp , pExp1 , pExp2 , pExp3 , pExp4 , pExp5 , pListExp , pDir , pSystem , pFace , pListFace , pSide , pListSide , pFormula , pFormula1 , pFormula2 , pBranch , pListBranch , pLabel , pListLabel , pTele , pListTele , pPTele , pListPTele , pListAIdent ) where import Prelude import qualified AbsCubicaltt import LexCubicaltt } %name pModule Module %name pImp Imp %name pListImp ListImp %name pDecl Decl %name pListDecl ListDecl %name pExpWhere ExpWhere %name pExp Exp %name pExp1 Exp1 %name pExp2 Exp2 %name pExp3 Exp3 %name pExp4 Exp4 %name pExp5 Exp5 %name pListExp ListExp %name pDir Dir %name pSystem System %name pFace Face %name pListFace ListFace %name pSide Side %name pListSide ListSide %name pFormula Formula %name pFormula1 Formula1 %name pFormula2 Formula2 %name pBranch Branch %name pListBranch ListBranch %name pLabel Label %name pListLabel ListLabel %name pTele Tele %name pListTele ListTele %name pPTele PTele %name pListPTele ListPTele %name pListAIdent ListAIdent %monad { Err } { (>>=) } { return } %tokentype {Token} %token '(' { PT _ (TS _ 1) } ')' { PT _ (TS _ 2) } '*' { PT _ (TS _ 3) } ',' { PT _ (TS _ 4) } '-' { PT _ (TS _ 5) } '->' { PT _ (TS _ 6) } '.1' { PT _ (TS _ 7) } '.2' { PT _ (TS _ 8) } '0' { PT _ (TS _ 9) } '1' { PT _ (TS _ 10) } ':' { PT _ (TS _ 11) } ';' { PT _ (TS _ 12) } '<' { PT _ (TS _ 13) } '=' { PT _ (TS _ 14) } '>' { PT _ (TS _ 15) } '@' { PT _ (TS _ 16) } 'Glue' { PT _ (TS _ 17) } 'Id' { PT _ (TS _ 18) } 'PathP' { PT _ (TS _ 19) } 'U' { PT _ (TS _ 20) } '[' { PT _ (TS _ 21) } '\\' { PT _ (TS _ 22) } '\\/' { PT _ (TS _ 23) } ']' { PT _ (TS _ 24) } 'comp' { PT _ (TS _ 25) } 'data' { PT _ (TS _ 26) } 'fill' { PT _ (TS _ 27) } 'glue' { PT _ (TS _ 28) } 'hComp' { PT _ (TS _ 29) } 'hdata' { PT _ (TS _ 30) } 'idC' { PT _ (TS _ 31) } 'idJ' { PT _ (TS _ 32) } 'import' { PT _ (TS _ 33) } 'in' { PT _ (TS _ 34) } 'let' { PT _ (TS _ 35) } 'module' { PT _ (TS _ 36) } 'mutual' { PT _ (TS _ 37) } 'opaque' { PT _ (TS _ 38) } 'split' { PT _ (TS _ 39) } 'split@' { PT _ (TS _ 40) } 'transparent' { PT _ (TS _ 41) } 'transparent_all' { PT _ (TS _ 42) } 'transport' { PT _ (TS _ 43) } 'undefined' { PT _ (TS _ 44) } 'unglue' { PT _ (TS _ 45) } 'where' { PT _ (TS _ 46) } 'with' { PT _ (TS _ 47) } '{' { PT _ (TS _ 48) } '|' { PT _ (TS _ 49) } '}' { PT _ (TS _ 50) } L_AIdent { PT _ (T_AIdent _) } L_CIdent { PT _ (T_CIdent $$) } L_HoleIdent { PT _ (T_HoleIdent _) } %% AIdent :: { AbsCubicaltt.AIdent } AIdent : L_AIdent { AbsCubicaltt.AIdent (mkPosToken $1) } CIdent :: { AbsCubicaltt.CIdent } CIdent : L_CIdent { AbsCubicaltt.CIdent $1 } HoleIdent :: { AbsCubicaltt.HoleIdent } HoleIdent : L_HoleIdent { AbsCubicaltt.HoleIdent (mkPosToken $1) } Module :: { AbsCubicaltt.Module } Module : 'module' AIdent 'where' '{' ListImp ListDecl '}' { AbsCubicaltt.Module $2 $5 $6 } Imp :: { AbsCubicaltt.Imp } Imp : 'import' AIdent { AbsCubicaltt.Import $2 } ListImp :: { [AbsCubicaltt.Imp] } ListImp : {- empty -} { [] } | Imp { (:[]) $1 } | Imp ';' ListImp { (:) $1 $3 } Decl :: { AbsCubicaltt.Decl } Decl : 'data' AIdent ListTele '=' ListLabel { AbsCubicaltt.DeclData $2 $3 $5 } | 'hdata' AIdent ListTele '=' ListLabel { AbsCubicaltt.DeclHData $2 $3 $5 } | 'mutual' '{' ListDecl '}' { AbsCubicaltt.DeclMutual $3 } | 'opaque' AIdent { AbsCubicaltt.DeclOpaque $2 } | 'transparent' AIdent { AbsCubicaltt.DeclTransparent $2 } | 'transparent_all' { AbsCubicaltt.DeclTransparentAll } | AIdent ListTele ':' Exp '=' 'split' '{' ListBranch '}' { AbsCubicaltt.DeclSplit $1 $2 $4 $8 } | AIdent ListTele ':' Exp '=' 'undefined' { AbsCubicaltt.DeclUndef $1 $2 $4 } | AIdent ListTele ':' Exp '=' ExpWhere { AbsCubicaltt.DeclDef $1 $2 $4 $6 } ListDecl :: { [AbsCubicaltt.Decl] } ListDecl : {- empty -} { [] } | Decl { (:[]) $1 } | Decl ';' ListDecl { (:) $1 $3 } ExpWhere :: { AbsCubicaltt.ExpWhere } ExpWhere : Exp { AbsCubicaltt.NoWhere $1 } | Exp 'where' '{' ListDecl '}' { AbsCubicaltt.Where $1 $4 } Exp :: { AbsCubicaltt.Exp } Exp : '<' ListAIdent '>' Exp { AbsCubicaltt.PLam $2 $4 } | '\\' ListPTele '->' Exp { AbsCubicaltt.Lam $2 $4 } | 'let' '{' ListDecl '}' 'in' Exp { AbsCubicaltt.Let $3 $6 } | 'split@' Exp 'with' '{' ListBranch '}' { AbsCubicaltt.Split $2 $5 } | Exp1 { $1 } Exp1 :: { AbsCubicaltt.Exp } Exp1 : ListPTele '*' Exp1 { AbsCubicaltt.Sigma $1 $3 } | ListPTele '->' Exp1 { AbsCubicaltt.Pi $1 $3 } | Exp2 { $1 } | Exp2 '->' Exp1 { AbsCubicaltt.Fun $1 $3 } Exp2 :: { AbsCubicaltt.Exp } Exp2 : Exp2 '@' Formula { AbsCubicaltt.AppFormula $1 $3 } | Exp2 Exp3 { AbsCubicaltt.App $1 $2 } | Exp3 { $1 } Exp3 :: { AbsCubicaltt.Exp } Exp3 : 'Glue' Exp4 System { AbsCubicaltt.Glue $2 $3 } | 'Id' Exp4 Exp4 Exp3 { AbsCubicaltt.Id $2 $3 $4 } | 'PathP' Exp4 Exp4 Exp4 { AbsCubicaltt.PathP $2 $3 $4 } | 'comp' Exp4 Exp4 System { AbsCubicaltt.Comp $2 $3 $4 } | 'fill' Exp4 Exp4 System { AbsCubicaltt.Fill $2 $3 $4 } | 'glue' Exp4 System { AbsCubicaltt.GlueElem $2 $3 } | 'hComp' Exp4 Exp4 System { AbsCubicaltt.HComp $2 $3 $4 } | 'idC' Exp4 System { AbsCubicaltt.IdPair $2 $3 } | 'idJ' Exp4 Exp4 Exp4 Exp4 Exp4 Exp4 { AbsCubicaltt.IdJ $2 $3 $4 $5 $6 $7 } | 'transport' Exp4 Exp4 { AbsCubicaltt.Trans $2 $3 } | 'unglue' Exp4 System { AbsCubicaltt.UnGlueElem $2 $3 } | Exp4 { $1 } Exp4 :: { AbsCubicaltt.Exp } Exp4 : Exp4 '.1' { AbsCubicaltt.Fst $1 } | Exp4 '.2' { AbsCubicaltt.Snd $1 } | Exp5 { $1 } Exp5 :: { AbsCubicaltt.Exp } Exp5 : '(' Exp ')' { $2 } | '(' Exp ',' ListExp ')' { AbsCubicaltt.Pair $2 $4 } | 'U' { AbsCubicaltt.U } | AIdent { AbsCubicaltt.Var $1 } | AIdent '{' Exp '}' { AbsCubicaltt.PCon $1 $3 } | HoleIdent { AbsCubicaltt.Hole $1 } ListExp :: { [AbsCubicaltt.Exp] } ListExp : Exp { (:[]) $1 } | Exp ',' ListExp { (:) $1 $3 } Dir :: { AbsCubicaltt.Dir } Dir : '0' { AbsCubicaltt.Dir0 } | '1' { AbsCubicaltt.Dir1 } System :: { AbsCubicaltt.System } System : '[' ListSide ']' { AbsCubicaltt.System $2 } Face :: { AbsCubicaltt.Face } Face : '(' AIdent '=' Dir ')' { AbsCubicaltt.Face $2 $4 } ListFace :: { [AbsCubicaltt.Face] } ListFace : {- empty -} { [] } | Face ListFace { (:) $1 $2 } Side :: { AbsCubicaltt.Side } Side : ListFace '->' Exp { AbsCubicaltt.Side $1 $3 } ListSide :: { [AbsCubicaltt.Side] } ListSide : {- empty -} { [] } | Side { (:[]) $1 } | Side ',' ListSide { (:) $1 $3 } Formula :: { AbsCubicaltt.Formula } Formula : Formula '\\/' Formula1 { AbsCubicaltt.Disj $1 $3 } | Formula1 { $1 } Formula1 :: { AbsCubicaltt.Formula } Formula1 : Formula1 CIdent Formula2 { AbsCubicaltt.Conj $1 $2 $3 } | Formula2 { $1 } Formula2 :: { AbsCubicaltt.Formula } Formula2 : '(' Formula ')' { $2 } | '-' Formula2 { AbsCubicaltt.Neg $2 } | AIdent { AbsCubicaltt.Atom $1 } | Dir { AbsCubicaltt.Dir $1 } Branch :: { AbsCubicaltt.Branch } Branch : AIdent ListAIdent '->' ExpWhere { AbsCubicaltt.OBranch $1 $2 $4 } | AIdent ListAIdent '@' ListAIdent '->' ExpWhere { AbsCubicaltt.PBranch $1 $2 $4 $6 } ListBranch :: { [AbsCubicaltt.Branch] } ListBranch : {- empty -} { [] } | Branch { (:[]) $1 } | Branch ';' ListBranch { (:) $1 $3 } Label :: { AbsCubicaltt.Label } Label : AIdent ListTele { AbsCubicaltt.OLabel $1 $2 } | AIdent ListTele '<' ListAIdent '>' System { AbsCubicaltt.PLabel $1 $2 $4 $6 } ListLabel :: { [AbsCubicaltt.Label] } ListLabel : {- empty -} { [] } | Label { (:[]) $1 } | Label '|' ListLabel { (:) $1 $3 } Tele :: { AbsCubicaltt.Tele } Tele : '(' AIdent ListAIdent ':' Exp ')' { AbsCubicaltt.Tele $2 $3 $5 } ListTele :: { [AbsCubicaltt.Tele] } ListTele : {- empty -} { [] } | Tele ListTele { (:) $1 $2 } PTele :: { AbsCubicaltt.PTele } PTele : '(' Exp ':' Exp ')' { AbsCubicaltt.PTele $2 $4 } ListPTele :: { [AbsCubicaltt.PTele] } ListPTele : PTele { (:[]) $1 } | PTele ListPTele { (:) $1 $2 } ListAIdent :: { [AbsCubicaltt.AIdent] } ListAIdent : {- empty -} { [] } | AIdent ListAIdent { (:) $1 $2 } { type Err = Either String happyError :: [Token] -> Err a happyError ts = Left $ "syntax error at " ++ tokenPos ts ++ case ts of [] -> [] [Err _] -> " due to lexer error" t:_ -> " before `" ++ (prToken t) ++ "'" myLexer :: String -> [Token] myLexer = tokens }