-- 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 (Ident -> Ident -> Bool
(Ident -> Ident -> Bool) -> (Ident -> Ident -> Bool) -> Eq Ident
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ident -> Ident -> Bool
$c/= :: Ident -> Ident -> Bool
== :: Ident -> Ident -> Bool
$c== :: Ident -> Ident -> Bool
C.Eq, Eq Ident
Eq Ident
-> (Ident -> Ident -> Ordering)
-> (Ident -> Ident -> Bool)
-> (Ident -> Ident -> Bool)
-> (Ident -> Ident -> Bool)
-> (Ident -> Ident -> Bool)
-> (Ident -> Ident -> Ident)
-> (Ident -> Ident -> Ident)
-> Ord Ident
Ident -> Ident -> Bool
Ident -> Ident -> Ordering
Ident -> Ident -> Ident
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Ident -> Ident -> Ident
$cmin :: Ident -> Ident -> Ident
max :: Ident -> Ident -> Ident
$cmax :: Ident -> Ident -> Ident
>= :: Ident -> Ident -> Bool
$c>= :: Ident -> Ident -> Bool
> :: Ident -> Ident -> Bool
$c> :: Ident -> Ident -> Bool
<= :: Ident -> Ident -> Bool
$c<= :: Ident -> Ident -> Bool
< :: Ident -> Ident -> Bool
$c< :: Ident -> Ident -> Bool
compare :: Ident -> Ident -> Ordering
$ccompare :: Ident -> Ident -> Ordering
C.Ord, Int -> Ident -> String -> String
[Ident] -> String -> String
Ident -> String
(Int -> Ident -> String -> String)
-> (Ident -> String) -> ([Ident] -> String -> String) -> Show Ident
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Ident] -> String -> String
$cshowList :: [Ident] -> String -> String
show :: Ident -> String
$cshow :: Ident -> String
showsPrec :: Int -> Ident -> String -> String
$cshowsPrec :: Int -> Ident -> String -> String
C.Show, ReadPrec [Ident]
ReadPrec Ident
Int -> ReadS Ident
ReadS [Ident]
(Int -> ReadS Ident)
-> ReadS [Ident]
-> ReadPrec Ident
-> ReadPrec [Ident]
-> Read Ident
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Ident]
$creadListPrec :: ReadPrec [Ident]
readPrec :: ReadPrec Ident
$creadPrec :: ReadPrec Ident
readList :: ReadS [Ident]
$creadList :: ReadS [Ident]
readsPrec :: Int -> ReadS Ident
$creadsPrec :: Int -> ReadS Ident
C.Read, String -> Ident
(String -> Ident) -> IsString Ident
forall a. (String -> a) -> IsString a
fromString :: String -> Ident
$cfromString :: String -> Ident
Data.String.IsString)

data Prg = Prg [Decl]
  deriving (Prg -> Prg -> Bool
(Prg -> Prg -> Bool) -> (Prg -> Prg -> Bool) -> Eq Prg
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Prg -> Prg -> Bool
$c/= :: Prg -> Prg -> Bool
== :: Prg -> Prg -> Bool
$c== :: Prg -> Prg -> Bool
C.Eq, Eq Prg
Eq Prg
-> (Prg -> Prg -> Ordering)
-> (Prg -> Prg -> Bool)
-> (Prg -> Prg -> Bool)
-> (Prg -> Prg -> Bool)
-> (Prg -> Prg -> Bool)
-> (Prg -> Prg -> Prg)
-> (Prg -> Prg -> Prg)
-> Ord Prg
Prg -> Prg -> Bool
Prg -> Prg -> Ordering
Prg -> Prg -> Prg
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Prg -> Prg -> Prg
$cmin :: Prg -> Prg -> Prg
max :: Prg -> Prg -> Prg
$cmax :: Prg -> Prg -> Prg
>= :: Prg -> Prg -> Bool
$c>= :: Prg -> Prg -> Bool
> :: Prg -> Prg -> Bool
$c> :: Prg -> Prg -> Bool
<= :: Prg -> Prg -> Bool
$c<= :: Prg -> Prg -> Bool
< :: Prg -> Prg -> Bool
$c< :: Prg -> Prg -> Bool
compare :: Prg -> Prg -> Ordering
$ccompare :: Prg -> Prg -> Ordering
C.Ord, Int -> Prg -> String -> String
[Prg] -> String -> String
Prg -> String
(Int -> Prg -> String -> String)
-> (Prg -> String) -> ([Prg] -> String -> String) -> Show Prg
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Prg] -> String -> String
$cshowList :: [Prg] -> String -> String
show :: Prg -> String
$cshow :: Prg -> String
showsPrec :: Int -> Prg -> String -> String
$cshowsPrec :: Int -> Prg -> String -> String
C.Show, ReadPrec [Prg]
ReadPrec Prg
Int -> ReadS Prg
ReadS [Prg]
(Int -> ReadS Prg)
-> ReadS [Prg] -> ReadPrec Prg -> ReadPrec [Prg] -> Read Prg
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Prg]
$creadListPrec :: ReadPrec [Prg]
readPrec :: ReadPrec Prg
$creadPrec :: ReadPrec Prg
readList :: ReadS [Prg]
$creadList :: ReadS [Prg]
readsPrec :: Int -> ReadS Prg
$creadsPrec :: Int -> ReadS Prg
C.Read)

data Decl = Sig Ident Exp | Def Ident Exp | Open QualId | Blank
  deriving (Decl -> Decl -> Bool
(Decl -> Decl -> Bool) -> (Decl -> Decl -> Bool) -> Eq Decl
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Decl -> Decl -> Bool
$c/= :: Decl -> Decl -> Bool
== :: Decl -> Decl -> Bool
$c== :: Decl -> Decl -> Bool
C.Eq, Eq Decl
Eq Decl
-> (Decl -> Decl -> Ordering)
-> (Decl -> Decl -> Bool)
-> (Decl -> Decl -> Bool)
-> (Decl -> Decl -> Bool)
-> (Decl -> Decl -> Bool)
-> (Decl -> Decl -> Decl)
-> (Decl -> Decl -> Decl)
-> Ord Decl
Decl -> Decl -> Bool
Decl -> Decl -> Ordering
Decl -> Decl -> Decl
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Decl -> Decl -> Decl
$cmin :: Decl -> Decl -> Decl
max :: Decl -> Decl -> Decl
$cmax :: Decl -> Decl -> Decl
>= :: Decl -> Decl -> Bool
$c>= :: Decl -> Decl -> Bool
> :: Decl -> Decl -> Bool
$c> :: Decl -> Decl -> Bool
<= :: Decl -> Decl -> Bool
$c<= :: Decl -> Decl -> Bool
< :: Decl -> Decl -> Bool
$c< :: Decl -> Decl -> Bool
compare :: Decl -> Decl -> Ordering
$ccompare :: Decl -> Decl -> Ordering
C.Ord, Int -> Decl -> String -> String
[Decl] -> String -> String
Decl -> String
(Int -> Decl -> String -> String)
-> (Decl -> String) -> ([Decl] -> String -> String) -> Show Decl
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Decl] -> String -> String
$cshowList :: [Decl] -> String -> String
show :: Decl -> String
$cshow :: Decl -> String
showsPrec :: Int -> Decl -> String -> String
$cshowsPrec :: Int -> Decl -> String -> String
C.Show, ReadPrec [Decl]
ReadPrec Decl
Int -> ReadS Decl
ReadS [Decl]
(Int -> ReadS Decl)
-> ReadS [Decl] -> ReadPrec Decl -> ReadPrec [Decl] -> Read Decl
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Decl]
$creadListPrec :: ReadPrec [Decl]
readPrec :: ReadPrec Decl
$creadPrec :: ReadPrec Decl
readList :: ReadS [Decl]
$creadList :: ReadS [Decl]
readsPrec :: Int -> ReadS Decl
$creadsPrec :: Int -> ReadS Decl
C.Read)

data QualId = Sg Ident | Cons QualId Ident
  deriving (QualId -> QualId -> Bool
(QualId -> QualId -> Bool)
-> (QualId -> QualId -> Bool) -> Eq QualId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: QualId -> QualId -> Bool
$c/= :: QualId -> QualId -> Bool
== :: QualId -> QualId -> Bool
$c== :: QualId -> QualId -> Bool
C.Eq, Eq QualId
Eq QualId
-> (QualId -> QualId -> Ordering)
-> (QualId -> QualId -> Bool)
-> (QualId -> QualId -> Bool)
-> (QualId -> QualId -> Bool)
-> (QualId -> QualId -> Bool)
-> (QualId -> QualId -> QualId)
-> (QualId -> QualId -> QualId)
-> Ord QualId
QualId -> QualId -> Bool
QualId -> QualId -> Ordering
QualId -> QualId -> QualId
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: QualId -> QualId -> QualId
$cmin :: QualId -> QualId -> QualId
max :: QualId -> QualId -> QualId
$cmax :: QualId -> QualId -> QualId
>= :: QualId -> QualId -> Bool
$c>= :: QualId -> QualId -> Bool
> :: QualId -> QualId -> Bool
$c> :: QualId -> QualId -> Bool
<= :: QualId -> QualId -> Bool
$c<= :: QualId -> QualId -> Bool
< :: QualId -> QualId -> Bool
$c< :: QualId -> QualId -> Bool
compare :: QualId -> QualId -> Ordering
$ccompare :: QualId -> QualId -> Ordering
C.Ord, Int -> QualId -> String -> String
[QualId] -> String -> String
QualId -> String
(Int -> QualId -> String -> String)
-> (QualId -> String)
-> ([QualId] -> String -> String)
-> Show QualId
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [QualId] -> String -> String
$cshowList :: [QualId] -> String -> String
show :: QualId -> String
$cshow :: QualId -> String
showsPrec :: Int -> QualId -> String -> String
$cshowsPrec :: Int -> QualId -> String -> String
C.Show, ReadPrec [QualId]
ReadPrec QualId
Int -> ReadS QualId
ReadS [QualId]
(Int -> ReadS QualId)
-> ReadS [QualId]
-> ReadPrec QualId
-> ReadPrec [QualId]
-> Read QualId
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [QualId]
$creadListPrec :: ReadPrec [QualId]
readPrec :: ReadPrec QualId
$creadPrec :: ReadPrec QualId
readList :: ReadS [QualId]
$creadList :: ReadS [QualId]
readsPrec :: Int -> ReadS QualId
$creadsPrec :: Int -> ReadS QualId
C.Read)

data IdU = Id Ident | Under
  deriving (IdU -> IdU -> Bool
(IdU -> IdU -> Bool) -> (IdU -> IdU -> Bool) -> Eq IdU
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IdU -> IdU -> Bool
$c/= :: IdU -> IdU -> Bool
== :: IdU -> IdU -> Bool
$c== :: IdU -> IdU -> Bool
C.Eq, Eq IdU
Eq IdU
-> (IdU -> IdU -> Ordering)
-> (IdU -> IdU -> Bool)
-> (IdU -> IdU -> Bool)
-> (IdU -> IdU -> Bool)
-> (IdU -> IdU -> Bool)
-> (IdU -> IdU -> IdU)
-> (IdU -> IdU -> IdU)
-> Ord IdU
IdU -> IdU -> Bool
IdU -> IdU -> Ordering
IdU -> IdU -> IdU
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: IdU -> IdU -> IdU
$cmin :: IdU -> IdU -> IdU
max :: IdU -> IdU -> IdU
$cmax :: IdU -> IdU -> IdU
>= :: IdU -> IdU -> Bool
$c>= :: IdU -> IdU -> Bool
> :: IdU -> IdU -> Bool
$c> :: IdU -> IdU -> Bool
<= :: IdU -> IdU -> Bool
$c<= :: IdU -> IdU -> Bool
< :: IdU -> IdU -> Bool
$c< :: IdU -> IdU -> Bool
compare :: IdU -> IdU -> Ordering
$ccompare :: IdU -> IdU -> Ordering
C.Ord, Int -> IdU -> String -> String
[IdU] -> String -> String
IdU -> String
(Int -> IdU -> String -> String)
-> (IdU -> String) -> ([IdU] -> String -> String) -> Show IdU
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [IdU] -> String -> String
$cshowList :: [IdU] -> String -> String
show :: IdU -> String
$cshow :: IdU -> String
showsPrec :: Int -> IdU -> String -> String
$cshowsPrec :: Int -> IdU -> String -> String
C.Show, ReadPrec [IdU]
ReadPrec IdU
Int -> ReadS IdU
ReadS [IdU]
(Int -> ReadS IdU)
-> ReadS [IdU] -> ReadPrec IdU -> ReadPrec [IdU] -> Read IdU
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [IdU]
$creadListPrec :: ReadPrec [IdU]
readPrec :: ReadPrec IdU
$creadPrec :: ReadPrec IdU
readList :: ReadS [IdU]
$creadList :: ReadS [IdU]
readsPrec :: Int -> ReadS IdU
$creadsPrec :: Int -> ReadS IdU
C.Read)

data Bind = BIrrel Ident | BRel Ident | BAnn [Ident] Exp
  deriving (Bind -> Bind -> Bool
(Bind -> Bind -> Bool) -> (Bind -> Bind -> Bool) -> Eq Bind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Bind -> Bind -> Bool
$c/= :: Bind -> Bind -> Bool
== :: Bind -> Bind -> Bool
$c== :: Bind -> Bind -> Bool
C.Eq, Eq Bind
Eq Bind
-> (Bind -> Bind -> Ordering)
-> (Bind -> Bind -> Bool)
-> (Bind -> Bind -> Bool)
-> (Bind -> Bind -> Bool)
-> (Bind -> Bind -> Bool)
-> (Bind -> Bind -> Bind)
-> (Bind -> Bind -> Bind)
-> Ord Bind
Bind -> Bind -> Bool
Bind -> Bind -> Ordering
Bind -> Bind -> Bind
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Bind -> Bind -> Bind
$cmin :: Bind -> Bind -> Bind
max :: Bind -> Bind -> Bind
$cmax :: Bind -> Bind -> Bind
>= :: Bind -> Bind -> Bool
$c>= :: Bind -> Bind -> Bool
> :: Bind -> Bind -> Bool
$c> :: Bind -> Bind -> Bool
<= :: Bind -> Bind -> Bool
$c<= :: Bind -> Bind -> Bool
< :: Bind -> Bind -> Bool
$c< :: Bind -> Bind -> Bool
compare :: Bind -> Bind -> Ordering
$ccompare :: Bind -> Bind -> Ordering
C.Ord, Int -> Bind -> String -> String
[Bind] -> String -> String
Bind -> String
(Int -> Bind -> String -> String)
-> (Bind -> String) -> ([Bind] -> String -> String) -> Show Bind
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Bind] -> String -> String
$cshowList :: [Bind] -> String -> String
show :: Bind -> String
$cshow :: Bind -> String
showsPrec :: Int -> Bind -> String -> String
$cshowsPrec :: Int -> Bind -> String -> String
C.Show, ReadPrec [Bind]
ReadPrec Bind
Int -> ReadS Bind
ReadS [Bind]
(Int -> ReadS Bind)
-> ReadS [Bind] -> ReadPrec Bind -> ReadPrec [Bind] -> Read Bind
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Bind]
$creadListPrec :: ReadPrec [Bind]
readPrec :: ReadPrec Bind
$creadPrec :: ReadPrec Bind
readList :: ReadS [Bind]
$creadList :: ReadS [Bind]
readsPrec :: Int -> ReadS Bind
$creadsPrec :: Int -> ReadS Bind
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 (Exp -> Exp -> Bool
(Exp -> Exp -> Bool) -> (Exp -> Exp -> Bool) -> Eq Exp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Exp -> Exp -> Bool
$c/= :: Exp -> Exp -> Bool
== :: Exp -> Exp -> Bool
$c== :: Exp -> Exp -> Bool
C.Eq, Eq Exp
Eq Exp
-> (Exp -> Exp -> Ordering)
-> (Exp -> Exp -> Bool)
-> (Exp -> Exp -> Bool)
-> (Exp -> Exp -> Bool)
-> (Exp -> Exp -> Bool)
-> (Exp -> Exp -> Exp)
-> (Exp -> Exp -> Exp)
-> Ord Exp
Exp -> Exp -> Bool
Exp -> Exp -> Ordering
Exp -> Exp -> Exp
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Exp -> Exp -> Exp
$cmin :: Exp -> Exp -> Exp
max :: Exp -> Exp -> Exp
$cmax :: Exp -> Exp -> Exp
>= :: Exp -> Exp -> Bool
$c>= :: Exp -> Exp -> Bool
> :: Exp -> Exp -> Bool
$c> :: Exp -> Exp -> Bool
<= :: Exp -> Exp -> Bool
$c<= :: Exp -> Exp -> Bool
< :: Exp -> Exp -> Bool
$c< :: Exp -> Exp -> Bool
compare :: Exp -> Exp -> Ordering
$ccompare :: Exp -> Exp -> Ordering
C.Ord, Int -> Exp -> String -> String
[Exp] -> String -> String
Exp -> String
(Int -> Exp -> String -> String)
-> (Exp -> String) -> ([Exp] -> String -> String) -> Show Exp
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Exp] -> String -> String
$cshowList :: [Exp] -> String -> String
show :: Exp -> String
$cshow :: Exp -> String
showsPrec :: Int -> Exp -> String -> String
$cshowsPrec :: Int -> Exp -> String -> String
C.Show, ReadPrec [Exp]
ReadPrec Exp
Int -> ReadS Exp
ReadS [Exp]
(Int -> ReadS Exp)
-> ReadS [Exp] -> ReadPrec Exp -> ReadPrec [Exp] -> Read Exp
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Exp]
$creadListPrec :: ReadPrec [Exp]
readPrec :: ReadPrec Exp
$creadPrec :: ReadPrec Exp
readList :: ReadS [Exp]
$creadList :: ReadS [Exp]
readsPrec :: Int -> ReadS Exp
$creadsPrec :: Int -> ReadS Exp
C.Read)