-- 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

}