module Sit.Abs where

-- Haskell module generated by the BNF converter




newtype Ident = Ident String deriving (Eq, Ord, Show, Read)
data Prg = Prg [Decl]
  deriving (Eq, Ord, Show, Read)

data Decl = Sig Ident Exp | Def Ident Exp | Open QualId | Blank
  deriving (Eq, Ord, Show, Read)

data QualId = Sg Ident | Cons QualId Ident
  deriving (Eq, Ord, Show, Read)

data IdU = Id Ident | Under
  deriving (Eq, Ord, Show, Read)

data Bind = BIrrel Ident | BRel Ident | BAnn [Ident] Exp
  deriving (Eq, Ord, Show, Read)

data Exp
    = Var IdU
    | Int Integer
    | Infty
    | Nat
    | Set
    | Set1
    | Set2
    | Zero
    | Suc
    | Fix
    | LZero
    | LSuc
    | Size
    | App Exp Exp
    | Lam [IdU] Exp
    | Forall [Bind] Exp
    | Pi Exp Exp Exp
    | Arrow Exp Exp
    | Case Exp Exp Exp
    | Plus Exp Integer
    | ELam Exp IdU Exp
  deriving (Eq, Ord, Show, Read)