cubical-0.2.0: Exp/Par.y

-- This Happy file was machine-generated by the BNF converter
{
{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}
module Exp.Par where
import Exp.Abs
import Exp.Lex
import Exp.ErrM

}

%name pModule Module
%name pExp Exp

-- no lexer declaration
%monad { Err } { thenM } { returnM }
%tokentype { Token }

%token 
 '(' { PT _ (TS _ 1) }
 ')' { PT _ (TS _ 2) }
 '*' { PT _ (TS _ 3) }
 ',' { PT _ (TS _ 4) }
 '->' { PT _ (TS _ 5) }
 '.1' { PT _ (TS _ 6) }
 '.2' { PT _ (TS _ 7) }
 ':' { PT _ (TS _ 8) }
 ';' { PT _ (TS _ 9) }
 '=' { PT _ (TS _ 10) }
 'U' { PT _ (TS _ 11) }
 '\\' { PT _ (TS _ 12) }
 'data' { PT _ (TS _ 13) }
 'import' { PT _ (TS _ 14) }
 'in' { PT _ (TS _ 15) }
 'let' { PT _ (TS _ 16) }
 'module' { PT _ (TS _ 17) }
 'mutual' { PT _ (TS _ 18) }
 'opaque' { PT _ (TS _ 19) }
 'primitive' { PT _ (TS _ 20) }
 'split' { PT _ (TS _ 21) }
 'transparent' { PT _ (TS _ 22) }
 'where' { PT _ (TS _ 23) }
 '{' { PT _ (TS _ 24) }
 '|' { PT _ (TS _ 25) }
 '}' { PT _ (TS _ 26) }

L_AIdent { PT _ (T_AIdent _) }
L_err    { _ }


%%

AIdent    :: { AIdent} : L_AIdent { AIdent (mkPosToken $1)}

Module :: { Module }
Module : 'module' AIdent 'where' '{' ListImp ListDecl '}' { Module $2 $5 $6 } 


Imp :: { Imp }
Imp : 'import' AIdent { Import $2 } 


ListImp :: { [Imp] }
ListImp : {- empty -} { [] } 
  | Imp { (:[]) $1 }
  | Imp ';' ListImp { (:) $1 $3 }


Decl :: { Decl }
Decl : AIdent ListAIdent '=' ExpWhere { DeclDef $1 (reverse $2) $4 } 
  | AIdent ':' Exp { DeclType $1 $3 }
  | 'primitive' AIdent ':' Exp { DeclPrim $2 $4 }
  | 'data' AIdent ListAIdent '=' ListLabel { DeclData $2 (reverse $3) $5 }
  | 'mutual' '{' ListDecl '}' { DeclMutual $3 }
  | 'opaque' AIdent { DeclOpaque $2 }
  | 'transparent' AIdent { DeclTransp $2 }


ListDecl :: { [Decl] }
ListDecl : {- empty -} { [] } 
  | Decl { (:[]) $1 }
  | Decl ';' ListDecl { (:) $1 $3 }


ExpWhere :: { ExpWhere }
ExpWhere : Exp 'where' '{' ListDecl '}' { Where $1 $4 } 
  | Exp { NoWhere $1 }


Exp :: { Exp }
Exp : 'let' '{' ListDecl '}' 'in' Exp { Let $3 $6 } 
  | '\\' AIdent ListAIdent '->' Exp { Lam $2 (reverse $3) $5 }
  | 'split' '{' ListBranch '}' { Split $3 }
  | Exp1 { $1 }


Exp1 :: { Exp }
Exp1 : Exp2 '->' Exp1 { Fun $1 $3 } 
  | ListPseudoTDecl '->' Exp1 { Pi $1 $3 }
  | ListPseudoTDecl '*' Exp1 { Sigma $1 $3 }
  | Exp2 { $1 }


Exp2 :: { Exp }
Exp2 : Exp2 Exp3 { App $1 $2 } 
  | Exp3 { $1 }


Exp3 :: { Exp }
Exp3 : Exp3 '.1' { Fst $1 } 
  | Exp3 '.2' { Snd $1 }
  | '(' Exp ',' Exp ')' { Pair $2 $4 }
  | AIdent { Var $1 }
  | 'U' { U }
  | '(' Exp ')' { $2 }


Branch :: { Branch }
Branch : AIdent ListAIdent '->' ExpWhere { Branch $1 (reverse $2) $4 } 


ListBranch :: { [Branch] }
ListBranch : {- empty -} { [] } 
  | Branch { (:[]) $1 }
  | Branch ';' ListBranch { (:) $1 $3 }


Label :: { Label }
Label : AIdent ListVTDecl { Label $1 (reverse $2) } 


ListLabel :: { [Label] }
ListLabel : {- empty -} { [] } 
  | Label { (:[]) $1 }
  | Label '|' ListLabel { (:) $1 $3 }


VTDecl :: { VTDecl }
VTDecl : '(' AIdent ListAIdent ':' Exp ')' { VTDecl $2 (reverse $3) $5 } 


ListVTDecl :: { [VTDecl] }
ListVTDecl : {- empty -} { [] } 
  | ListVTDecl VTDecl { flip (:) $1 $2 }


PseudoTDecl :: { PseudoTDecl }
PseudoTDecl : '(' Exp ':' Exp ')' { PseudoTDecl $2 $4 } 


ListPseudoTDecl :: { [PseudoTDecl] }
ListPseudoTDecl : PseudoTDecl { (:[]) $1 } 
  | PseudoTDecl ListPseudoTDecl { (:) $1 $2 }


ListAIdent :: { [AIdent] }
ListAIdent : {- empty -} { [] } 
  | ListAIdent AIdent { flip (:) $1 $2 }



{

returnM :: a -> Err a
returnM = return

thenM :: Err a -> (a -> Err b) -> Err b
thenM = (>>=)

happyError :: [Token] -> Err a
happyError ts =
  Bad $ "syntax error at " ++ tokenPos ts ++ 
  case ts of
    [] -> []
    [Err _] -> " due to lexer error"
    _ -> " before " ++ unwords (map (id . prToken) (take 4 ts))

myLexer = tokens
}