{-# LANGUAGE DeriveGeneric #-}

module Dhall.Syntax.Const
    ( Const(..)
    ) where

import GHC.Generics (Generic)

{-| Constants for a pure type system

    The axioms are:

> ⊦ Type : Kind
> ⊦ Kind : Sort

    ... and the valid rule pairs are:

> ⊦ Type ↝ Type : Type  -- Functions from terms to terms (ordinary functions)
> ⊦ Kind ↝ Type : Type  -- Functions from types to terms (type-polymorphic functions)
> ⊦ Sort ↝ Type : Type  -- Functions from kinds to terms
> ⊦ Kind ↝ Kind : Kind  -- Functions from types to types (type-level functions)
> ⊦ Sort ↝ Kind : Sort  -- Functions from kinds to types (kind-polymorphic functions)
> ⊦ Sort ↝ Sort : Sort  -- Functions from kinds to kinds (kind-level functions)

    Note that Dhall does not support functions from terms to types and therefore
    Dhall is not a dependently typed language
-}
data Const = Type | Kind | Sort
    deriving (Const
Const -> Const -> Bounded Const
forall a. a -> a -> Bounded a
$cminBound :: Const
minBound :: Const
$cmaxBound :: Const
maxBound :: Const
Bounded, Int -> Const
Const -> Int
Const -> [Const]
Const -> Const
Const -> Const -> [Const]
Const -> Const -> Const -> [Const]
(Const -> Const)
-> (Const -> Const)
-> (Int -> Const)
-> (Const -> Int)
-> (Const -> [Const])
-> (Const -> Const -> [Const])
-> (Const -> Const -> [Const])
-> (Const -> Const -> Const -> [Const])
-> Enum Const
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Const -> Const
succ :: Const -> Const
$cpred :: Const -> Const
pred :: Const -> Const
$ctoEnum :: Int -> Const
toEnum :: Int -> Const
$cfromEnum :: Const -> Int
fromEnum :: Const -> Int
$cenumFrom :: Const -> [Const]
enumFrom :: Const -> [Const]
$cenumFromThen :: Const -> Const -> [Const]
enumFromThen :: Const -> Const -> [Const]
$cenumFromTo :: Const -> Const -> [Const]
enumFromTo :: Const -> Const -> [Const]
$cenumFromThenTo :: Const -> Const -> Const -> [Const]
enumFromThenTo :: Const -> Const -> Const -> [Const]
Enum, (forall x. Const -> Rep Const x)
-> (forall x. Rep Const x -> Const) -> Generic Const
forall x. Rep Const x -> Const
forall x. Const -> Rep Const x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Const -> Rep Const x
from :: forall x. Const -> Rep Const x
$cto :: forall x. Rep Const x -> Const
to :: forall x. Rep Const x -> Const
Generic)