cubical-0.1.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) }
 '=' { PT _ (TS _ 6) }
 'PN' { PT _ (TS _ 7) }
 'U' { PT _ (TS _ 8) }
 '\\' { PT _ (TS _ 9) }
 '_' { PT _ (TS _ 10) }
 'data' { PT _ (TS _ 11) }
 'import' { PT _ (TS _ 12) }
 'in' { PT _ (TS _ 13) }
 'let' { PT _ (TS _ 14) }
 'module' { PT _ (TS _ 15) }
 'split' { PT _ (TS _ 16) }
 'undefined' { PT _ (TS _ 17) }
 'where' { PT _ (TS _ 18) }
 '{' { PT _ (TS _ 19) }
 '|' { PT _ (TS _ 20) }
 '}' { PT _ (TS _ 21) }

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


%%

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

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


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


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


Def :: { Def }
Def : AIdent ListArg '=' ExpWhere { Def $1 (reverse $2) $4 } 
  | AIdent ':' Exp { DefTDecl $1 $3 }
  | 'data' AIdent ListArg '=' ListSum { DefData $2 (reverse $3) $5 }


ListDef :: { [Def] }
ListDef : {- empty -} { [] } 
  | Def { (:[]) $1 }
  | Def ';' ListDef { (:) $1 $3 }


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


Exp :: { Exp }
Exp : 'let' '{' ListDef '}' 'in' Exp { Let $3 $6 } 
  | '\\' ListBinder '->' Exp { Lam $2 $4 }
  | 'split' '{' ListBranch '}' { Split $3 }
  | Exp1 { $1 }


Exp1 :: { Exp }
Exp1 : Exp2 '->' Exp1 { Fun $1 $3 } 
  | ListPiDecl '->' Exp1 { Pi $1 $3 }
  | Exp2 { $1 }


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


Exp3 :: { Exp }
Exp3 : Arg { Var $1 } 
  | 'U' { U }
  | 'undefined' { Undef }
  | 'PN' { PN }
  | '(' Exp ')' { $2 }


Binder :: { Binder }
Binder : Arg { Binder $1 } 


ListBinder :: { [Binder] }
ListBinder : Binder { (:[]) $1 } 
  | Binder ListBinder { (:) $1 $2 }


Arg :: { Arg }
Arg : AIdent { Arg $1 } 
  | '_' { NoArg }


ListArg :: { [Arg] }
ListArg : {- empty -} { [] } 
  | ListArg Arg { flip (:) $1 $2 }


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


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


Sum :: { Sum }
Sum : AIdent ListVDecl { Sum $1 (reverse $2) } 


ListSum :: { [Sum] }
ListSum : {- empty -} { [] } 
  | Sum { (:[]) $1 }
  | Sum '|' ListSum { (:) $1 $3 }


VDecl :: { VDecl }
VDecl : '(' ListBinder ':' Exp ')' { VDecl $2 $4 } 


ListVDecl :: { [VDecl] }
ListVDecl : {- empty -} { [] } 
  | ListVDecl VDecl { flip (:) $1 $2 }


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


ListPiDecl :: { [PiDecl] }
ListPiDecl : PiDecl { (:[]) $1 } 
  | PiDecl ListPiDecl { (:) $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
}