-- Haskell data types for the abstract syntax.
-- Generated by the BNF converter.

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module Sit.Abs where

import Prelude (Char, Double, Integer, String)
import qualified Prelude as C (Eq, Ord, Show, Read)
import qualified Data.String

newtype Ident = Ident String
  deriving (C.Eq, C.Ord, C.Show, C.Read, Data.String.IsString)

data Prg = Prg [Decl]
  deriving (C.Eq, C.Ord, C.Show, C.Read)

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

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

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

data Bind = BIrrel Ident | BRel Ident | BAnn [Ident] Exp
  deriving (C.Eq, C.Ord, C.Show, C.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 (C.Eq, C.Ord, C.Show, C.Read)