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