-- This Happy file was machine-generated by the BNF converter
{
{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}
module Sit.Par
  ( happyError
  , myLexer
  , pPrg
  , pDecl
  , pQualId
  , pListDecl
  , pIdU
  , pBind
  , pListBind
  , pListIdent
  , pListIdU
  , pExp2
  , pExp1
  , pExp
  ) where
import qualified Sit.Abs
import Sit.Lex
}

%name pPrg Prg
%name pDecl Decl
%name pQualId QualId
%name pListDecl ListDecl
%name pIdU IdU
%name pBind Bind
%name pListBind ListBind
%name pListIdent ListIdent
%name pListIdU ListIdU
%name pExp2 Exp2
%name pExp1 Exp1
%name pExp Exp
-- no lexer declaration
%monad { Either String } { (>>=) } { return }
%tokentype {Token}
%token
  '(' { PT _ (TS _ 1) }
  ')' { PT _ (TS _ 2) }
  '+' { PT _ (TS _ 3) }
  '--;' { PT _ (TS _ 4) }
  '->' { PT _ (TS _ 5) }
  '.' { PT _ (TS _ 6) }
  '..' { PT _ (TS _ 7) }
  ':' { PT _ (TS _ 8) }
  ';' { PT _ (TS _ 9) }
  '=' { PT _ (TS _ 10) }
  'Nat' { PT _ (TS _ 11) }
  'Set' { PT _ (TS _ 12) }
  'Set1' { PT _ (TS _ 13) }
  'Set2' { PT _ (TS _ 14) }
  '\\' { PT _ (TS _ 15) }
  '_' { PT _ (TS _ 16) }
  'case' { PT _ (TS _ 17) }
  'fix' { PT _ (TS _ 18) }
  'forall' { PT _ (TS _ 19) }
  'import' { PT _ (TS _ 20) }
  'lsuc' { PT _ (TS _ 21) }
  'lzero' { PT _ (TS _ 22) }
  'of' { PT _ (TS _ 23) }
  'oo' { PT _ (TS _ 24) }
  'open' { PT _ (TS _ 25) }
  'return' { PT _ (TS _ 26) }
  'suc' { PT _ (TS _ 27) }
  'zero' { PT _ (TS _ 28) }
  '{' { PT _ (TS _ 29) }
  '}' { PT _ (TS _ 30) }
  L_Ident  { PT _ (TV $$) }
  L_integ  { PT _ (TI $$) }

%%

Ident :: { Sit.Abs.Ident }
Ident  : L_Ident { Sit.Abs.Ident $1 }

Integer :: { Integer }
Integer  : L_integ  { (read ($1)) :: Integer }

Prg :: { Sit.Abs.Prg }
Prg : ListDecl { Sit.Abs.Prg $1 }

Decl :: { Sit.Abs.Decl }
Decl : Ident ':' Exp { Sit.Abs.Sig $1 $3 }
     | Ident '=' Exp { Sit.Abs.Def $1 $3 }
     | 'open' 'import' QualId { Sit.Abs.Open $3 }
     | {- empty -} { Sit.Abs.Blank }

QualId :: { Sit.Abs.QualId }
QualId : Ident { Sit.Abs.Sg $1 }
       | QualId '.' Ident { Sit.Abs.Cons $1 $3 }

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

IdU :: { Sit.Abs.IdU }
IdU : Ident { Sit.Abs.Id $1 } | '_' { Sit.Abs.Under }

Bind :: { Sit.Abs.Bind }
Bind : '.' Ident { Sit.Abs.BIrrel $2 }
     | '..' Ident { Sit.Abs.BRel $2 }
     | '(' ListIdent ':' Exp ')' { Sit.Abs.BAnn $2 $4 }

ListBind :: { [Sit.Abs.Bind] }
ListBind : Bind { (:[]) $1 } | Bind ListBind { (:) $1 $2 }

ListIdent :: { [Sit.Abs.Ident] }
ListIdent : Ident { (:[]) $1 } | Ident ListIdent { (:) $1 $2 }

ListIdU :: { [Sit.Abs.IdU] }
ListIdU : IdU { (:[]) $1 } | IdU ListIdU { (:) $1 $2 }

Exp2 :: { Sit.Abs.Exp }
Exp2 : IdU { Sit.Abs.Var $1 }
     | Integer { Sit.Abs.Int $1 }
     | 'oo' { Sit.Abs.Infty }
     | 'Nat' { Sit.Abs.Nat }
     | 'Set' { Sit.Abs.Set }
     | 'Set1' { Sit.Abs.Set1 }
     | 'Set2' { Sit.Abs.Set2 }
     | 'zero' { Sit.Abs.Zero }
     | 'suc' { Sit.Abs.Suc }
     | 'fix' { Sit.Abs.Fix }
     | 'lzero' { Sit.Abs.LZero }
     | 'lsuc' { Sit.Abs.LSuc }
     | '(' Exp ')' { $2 }

Exp1 :: { Sit.Abs.Exp }
Exp1 : Exp1 Exp2 { Sit.Abs.App $1 $2 } | Exp2 { $1 }

Exp :: { Sit.Abs.Exp }
Exp : '\\' ListIdU '->' Exp { Sit.Abs.Lam $2 $4 }
    | 'forall' ListBind '->' Exp { Sit.Abs.Forall $2 $4 }
    | '(' Exp ':' Exp ')' '->' Exp { Sit.Abs.Pi $2 $4 $7 }
    | Exp1 '->' Exp { Sit.Abs.Arrow $1 $3 }
    | 'case' Exp 'return' Exp 'of' Exp { Sit.Abs.Case $2 $4 $6 }
    | Exp1 '+' Integer { Sit.Abs.Plus $1 $3 }
    | '\\' '{' '(' 'zero' '_' ')' '->' Exp ';' '(' 'suc' '_' IdU ')' '->' Exp '}' { Sit.Abs.ELam $8 $13 $16 }
    | Exp1 { $1 }
{

happyError :: [Token] -> Either String a
happyError ts = Left $
  "syntax error at " ++ tokenPos ts ++
  case ts of
    []      -> []
    [Err _] -> " due to lexer error"
    t:_     -> " before `" ++ (prToken t) ++ "'"

myLexer = tokens

}