hoq-0.1.0.0: src/Syntax/BNFC/ParGrammar.y

-- This Happy file was machine-generated by the BNF converter
{
{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}
module Syntax.BNFC.ParGrammar where
import Syntax.BNFC.AbsGrammar
import Syntax.BNFC.LexGrammar
import Syntax.BNFC.ErrM

}

%name pDefs Defs
%name pExpr Expr

-- 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) }
 'data' { PT _ (TS _ 7) }
 'with' { PT _ (TS _ 8) }
 '{' { PT _ (TS _ 9) }
 '|' { PT _ (TS _ 10) }
 '}' { PT _ (TS _ 11) }

L_U { PT _ (T_U _) }
L_I { PT _ (T_I _) }
L_PLeft { PT _ (T_PLeft _) }
L_PRight { PT _ (T_PRight _) }
L_PPath { PT _ (T_PPath _) }
L_Ppath { PT _ (T_Ppath _) }
L_PCoe { PT _ (T_PCoe _) }
L_PIso { PT _ (T_PIso _) }
L_PSqueeze { PT _ (T_PSqueeze _) }
L_PLam { PT _ (T_PLam _) }
L_PPar { PT _ (T_PPar _) }
L_Pus { PT _ (T_Pus _) }
L_PIdent { PT _ (T_PIdent _) }
L_err    { _ }


%%

U    :: { U} : L_U { U (mkPosToken $1)}
I    :: { I} : L_I { I (mkPosToken $1)}
PLeft    :: { PLeft} : L_PLeft { PLeft (mkPosToken $1)}
PRight    :: { PRight} : L_PRight { PRight (mkPosToken $1)}
PPath    :: { PPath} : L_PPath { PPath (mkPosToken $1)}
Ppath    :: { Ppath} : L_Ppath { Ppath (mkPosToken $1)}
PCoe    :: { PCoe} : L_PCoe { PCoe (mkPosToken $1)}
PIso    :: { PIso} : L_PIso { PIso (mkPosToken $1)}
PSqueeze    :: { PSqueeze} : L_PSqueeze { PSqueeze (mkPosToken $1)}
PLam    :: { PLam} : L_PLam { PLam (mkPosToken $1)}
PPar    :: { PPar} : L_PPar { PPar (mkPosToken $1)}
Pus    :: { Pus} : L_Pus { Pus (mkPosToken $1)}
PIdent    :: { PIdent} : L_PIdent { PIdent (mkPosToken $1)}

Defs :: { Defs }
Defs : ListDef { Defs $1 } 


Def :: { Def }
Def : PIdent ':' Expr { DefType $1 $3 } 
  | FunCase { DefFun $1 }
  | Pattern { DefFunEmpty $1 }
  | 'data' PIdent ListDataTele '=' ListCon { DefData $2 (reverse $3) $5 }
  | 'data' PIdent ListDataTele '=' ListCon 'with' '{' ListFunCase '}' { DefDataWith $2 (reverse $3) $5 $8 }
  | 'data' PIdent ListDataTele { DefDataEmpty $2 (reverse $3) }


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


FunCase :: { FunCase }
FunCase : Pattern '=' Expr { FunCase $1 $3 } 


ListFunCase :: { [FunCase] }
ListFunCase : {- empty -} { [] } 
  | FunCase { (:[]) $1 }
  | FunCase ';' ListFunCase { (:) $1 $3 }


Pattern :: { Pattern }
Pattern : PIdent ListParPat { Pattern $1 (reverse $2) } 


ParPat :: { ParPat }
ParPat : Arg { ParVar $1 } 
  | PLeft { ParLeft $1 }
  | PRight { ParRight $1 }
  | PPar ')' { ParEmpty $1 }
  | PPar Pattern ')' { ParPat $1 $2 }


ListParPat :: { [ParPat] }
ListParPat : {- empty -} { [] } 
  | ListParPat ParPat { flip (:) $1 $2 }


Con :: { Con }
Con : PIdent ListConTele { Con $1 (reverse $2) } 


ListCon :: { [Con] }
ListCon : Con { (:[]) $1 } 
  | Con '|' ListCon { (:) $1 $3 }


ConTele :: { ConTele }
ConTele : PPar Expr ':' Expr ')' { VarTele $1 $2 $4 } 
  | Expr5 { TypeTele $1 }


ListConTele :: { [ConTele] }
ListConTele : {- empty -} { [] } 
  | ListConTele ConTele { flip (:) $1 $2 }


DataTele :: { DataTele }
DataTele : PPar Expr ':' Expr ')' { DataTele $1 $2 $4 } 


ListDataTele :: { [DataTele] }
ListDataTele : {- empty -} { [] } 
  | ListDataTele DataTele { flip (:) $1 $2 }


PiTele :: { PiTele }
PiTele : PPar Expr ':' Expr ')' { PiTele $1 $2 $4 } 


ListPiTele :: { [PiTele] }
ListPiTele : PiTele { (:[]) $1 } 
  | PiTele ListPiTele { (:) $1 $2 }


Expr :: { Expr }
Expr : PLam ListArg '->' Expr { Lam $1 $2 $4 } 
  | Expr1 { $1 }


Expr1 :: { Expr }
Expr1 : Expr2 '->' Expr1 { Arr $1 $3 } 
  | ListPiTele '->' Expr1 { Pi $1 $3 }
  | Expr2 { $1 }


Expr2 :: { Expr }
Expr2 : Expr3 '=' Expr3 { PathImp $1 $3 } 
  | Expr3 { $1 }


Expr3 :: { Expr }
Expr3 : Expr3 '@' Expr4 { At $1 $3 } 
  | Expr4 { $1 }


Expr4 :: { Expr }
Expr4 : Expr4 Expr5 { App $1 $2 } 
  | Expr5 { $1 }


Expr5 :: { Expr }
Expr5 : Arg { Var $1 } 
  | U { Universe $1 }
  | I { Interval $1 }
  | PLeft { ELeft $1 }
  | PRight { ERight $1 }
  | PPath { Path $1 }
  | Ppath { PathCon $1 }
  | PCoe { Coe $1 }
  | PIso { Iso $1 }
  | PSqueeze { Squeeze $1 }
  | PPar Expr ')' { Paren $1 $2 }


Arg :: { Arg }
Arg : PIdent { Arg $1 } 
  | Pus { NoArg $1 }


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