module LambdaCube.STLC.Ast where

import           Data.Data                  (Data)
import           Data.Text                  (Text)
import           Language.Haskell.TH.Syntax (Lift)

data ExtLCTerm
  = ExtLCVar Text
  | ExtLCLam Text ExtLCType ExtLCTerm
  | ExtLCApp ExtLCTerm ExtLCTerm
  | ExtLCMVar String
  deriving stock (ExtLCTerm -> ExtLCTerm -> Bool
(ExtLCTerm -> ExtLCTerm -> Bool)
-> (ExtLCTerm -> ExtLCTerm -> Bool) -> Eq ExtLCTerm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ExtLCTerm -> ExtLCTerm -> Bool
$c/= :: ExtLCTerm -> ExtLCTerm -> Bool
== :: ExtLCTerm -> ExtLCTerm -> Bool
$c== :: ExtLCTerm -> ExtLCTerm -> Bool
Eq, Int -> ExtLCTerm -> ShowS
[ExtLCTerm] -> ShowS
ExtLCTerm -> String
(Int -> ExtLCTerm -> ShowS)
-> (ExtLCTerm -> String)
-> ([ExtLCTerm] -> ShowS)
-> Show ExtLCTerm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExtLCTerm] -> ShowS
$cshowList :: [ExtLCTerm] -> ShowS
show :: ExtLCTerm -> String
$cshow :: ExtLCTerm -> String
showsPrec :: Int -> ExtLCTerm -> ShowS
$cshowsPrec :: Int -> ExtLCTerm -> ShowS
Show, Typeable ExtLCTerm
DataType
Constr
Typeable ExtLCTerm
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> ExtLCTerm -> c ExtLCTerm)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ExtLCTerm)
-> (ExtLCTerm -> Constr)
-> (ExtLCTerm -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ExtLCTerm))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExtLCTerm))
-> ((forall b. Data b => b -> b) -> ExtLCTerm -> ExtLCTerm)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ExtLCTerm -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ExtLCTerm -> r)
-> (forall u. (forall d. Data d => d -> u) -> ExtLCTerm -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ExtLCTerm -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ExtLCTerm -> m ExtLCTerm)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ExtLCTerm -> m ExtLCTerm)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ExtLCTerm -> m ExtLCTerm)
-> Data ExtLCTerm
ExtLCTerm -> DataType
ExtLCTerm -> Constr
(forall b. Data b => b -> b) -> ExtLCTerm -> ExtLCTerm
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExtLCTerm -> c ExtLCTerm
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ExtLCTerm
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> ExtLCTerm -> u
forall u. (forall d. Data d => d -> u) -> ExtLCTerm -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExtLCTerm -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExtLCTerm -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ExtLCTerm -> m ExtLCTerm
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ExtLCTerm -> m ExtLCTerm
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ExtLCTerm
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExtLCTerm -> c ExtLCTerm
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ExtLCTerm)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExtLCTerm)
$cExtLCMVar :: Constr
$cExtLCApp :: Constr
$cExtLCLam :: Constr
$cExtLCVar :: Constr
$tExtLCTerm :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ExtLCTerm -> m ExtLCTerm
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ExtLCTerm -> m ExtLCTerm
gmapMp :: (forall d. Data d => d -> m d) -> ExtLCTerm -> m ExtLCTerm
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ExtLCTerm -> m ExtLCTerm
gmapM :: (forall d. Data d => d -> m d) -> ExtLCTerm -> m ExtLCTerm
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ExtLCTerm -> m ExtLCTerm
gmapQi :: Int -> (forall d. Data d => d -> u) -> ExtLCTerm -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ExtLCTerm -> u
gmapQ :: (forall d. Data d => d -> u) -> ExtLCTerm -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ExtLCTerm -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExtLCTerm -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExtLCTerm -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExtLCTerm -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExtLCTerm -> r
gmapT :: (forall b. Data b => b -> b) -> ExtLCTerm -> ExtLCTerm
$cgmapT :: (forall b. Data b => b -> b) -> ExtLCTerm -> ExtLCTerm
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExtLCTerm)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExtLCTerm)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ExtLCTerm)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ExtLCTerm)
dataTypeOf :: ExtLCTerm -> DataType
$cdataTypeOf :: ExtLCTerm -> DataType
toConstr :: ExtLCTerm -> Constr
$ctoConstr :: ExtLCTerm -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ExtLCTerm
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ExtLCTerm
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExtLCTerm -> c ExtLCTerm
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExtLCTerm -> c ExtLCTerm
$cp1Data :: Typeable ExtLCTerm
Data, ExtLCTerm -> Q Exp
ExtLCTerm -> Q (TExp ExtLCTerm)
(ExtLCTerm -> Q Exp)
-> (ExtLCTerm -> Q (TExp ExtLCTerm)) -> Lift ExtLCTerm
forall t. (t -> Q Exp) -> (t -> Q (TExp t)) -> Lift t
liftTyped :: ExtLCTerm -> Q (TExp ExtLCTerm)
$cliftTyped :: ExtLCTerm -> Q (TExp ExtLCTerm)
lift :: ExtLCTerm -> Q Exp
$clift :: ExtLCTerm -> Q Exp
Lift)
infixl 6 `ExtLCApp`

data ExtLCType
  = ExtLCBase
  | ExtLCArr ExtLCType ExtLCType
  | ExtLCMTVar String
  deriving stock (ExtLCType -> ExtLCType -> Bool
(ExtLCType -> ExtLCType -> Bool)
-> (ExtLCType -> ExtLCType -> Bool) -> Eq ExtLCType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ExtLCType -> ExtLCType -> Bool
$c/= :: ExtLCType -> ExtLCType -> Bool
== :: ExtLCType -> ExtLCType -> Bool
$c== :: ExtLCType -> ExtLCType -> Bool
Eq, Int -> ExtLCType -> ShowS
[ExtLCType] -> ShowS
ExtLCType -> String
(Int -> ExtLCType -> ShowS)
-> (ExtLCType -> String)
-> ([ExtLCType] -> ShowS)
-> Show ExtLCType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExtLCType] -> ShowS
$cshowList :: [ExtLCType] -> ShowS
show :: ExtLCType -> String
$cshow :: ExtLCType -> String
showsPrec :: Int -> ExtLCType -> ShowS
$cshowsPrec :: Int -> ExtLCType -> ShowS
Show, Typeable ExtLCType
DataType
Constr
Typeable ExtLCType
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> ExtLCType -> c ExtLCType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ExtLCType)
-> (ExtLCType -> Constr)
-> (ExtLCType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ExtLCType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExtLCType))
-> ((forall b. Data b => b -> b) -> ExtLCType -> ExtLCType)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ExtLCType -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ExtLCType -> r)
-> (forall u. (forall d. Data d => d -> u) -> ExtLCType -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ExtLCType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ExtLCType -> m ExtLCType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ExtLCType -> m ExtLCType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ExtLCType -> m ExtLCType)
-> Data ExtLCType
ExtLCType -> DataType
ExtLCType -> Constr
(forall b. Data b => b -> b) -> ExtLCType -> ExtLCType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExtLCType -> c ExtLCType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ExtLCType
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> ExtLCType -> u
forall u. (forall d. Data d => d -> u) -> ExtLCType -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExtLCType -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExtLCType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ExtLCType -> m ExtLCType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ExtLCType -> m ExtLCType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ExtLCType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExtLCType -> c ExtLCType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ExtLCType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExtLCType)
$cExtLCMTVar :: Constr
$cExtLCArr :: Constr
$cExtLCBase :: Constr
$tExtLCType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ExtLCType -> m ExtLCType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ExtLCType -> m ExtLCType
gmapMp :: (forall d. Data d => d -> m d) -> ExtLCType -> m ExtLCType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ExtLCType -> m ExtLCType
gmapM :: (forall d. Data d => d -> m d) -> ExtLCType -> m ExtLCType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ExtLCType -> m ExtLCType
gmapQi :: Int -> (forall d. Data d => d -> u) -> ExtLCType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ExtLCType -> u
gmapQ :: (forall d. Data d => d -> u) -> ExtLCType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ExtLCType -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExtLCType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExtLCType -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExtLCType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExtLCType -> r
gmapT :: (forall b. Data b => b -> b) -> ExtLCType -> ExtLCType
$cgmapT :: (forall b. Data b => b -> b) -> ExtLCType -> ExtLCType
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExtLCType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExtLCType)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ExtLCType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ExtLCType)
dataTypeOf :: ExtLCType -> DataType
$cdataTypeOf :: ExtLCType -> DataType
toConstr :: ExtLCType -> Constr
$ctoConstr :: ExtLCType -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ExtLCType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ExtLCType
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExtLCType -> c ExtLCType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ExtLCType -> c ExtLCType
$cp1Data :: Typeable ExtLCType
Data, ExtLCType -> Q Exp
ExtLCType -> Q (TExp ExtLCType)
(ExtLCType -> Q Exp)
-> (ExtLCType -> Q (TExp ExtLCType)) -> Lift ExtLCType
forall t. (t -> Q Exp) -> (t -> Q (TExp t)) -> Lift t
liftTyped :: ExtLCType -> Q (TExp ExtLCType)
$cliftTyped :: ExtLCType -> Q (TExp ExtLCType)
lift :: ExtLCType -> Q Exp
$clift :: ExtLCType -> Q Exp
Lift)
infixr 5 `ExtLCArr`

data LCTerm
  = LCVar Int
  | LCLam LCType LCTerm
  | LCApp LCTerm LCTerm
  deriving stock (LCTerm -> LCTerm -> Bool
(LCTerm -> LCTerm -> Bool)
-> (LCTerm -> LCTerm -> Bool) -> Eq LCTerm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LCTerm -> LCTerm -> Bool
$c/= :: LCTerm -> LCTerm -> Bool
== :: LCTerm -> LCTerm -> Bool
$c== :: LCTerm -> LCTerm -> Bool
Eq, Int -> LCTerm -> ShowS
[LCTerm] -> ShowS
LCTerm -> String
(Int -> LCTerm -> ShowS)
-> (LCTerm -> String) -> ([LCTerm] -> ShowS) -> Show LCTerm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LCTerm] -> ShowS
$cshowList :: [LCTerm] -> ShowS
show :: LCTerm -> String
$cshow :: LCTerm -> String
showsPrec :: Int -> LCTerm -> ShowS
$cshowsPrec :: Int -> LCTerm -> ShowS
Show, Typeable LCTerm
DataType
Constr
Typeable LCTerm
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LCTerm -> c LCTerm)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LCTerm)
-> (LCTerm -> Constr)
-> (LCTerm -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LCTerm))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LCTerm))
-> ((forall b. Data b => b -> b) -> LCTerm -> LCTerm)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LCTerm -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LCTerm -> r)
-> (forall u. (forall d. Data d => d -> u) -> LCTerm -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> LCTerm -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LCTerm -> m LCTerm)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LCTerm -> m LCTerm)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LCTerm -> m LCTerm)
-> Data LCTerm
LCTerm -> DataType
LCTerm -> Constr
(forall b. Data b => b -> b) -> LCTerm -> LCTerm
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCTerm -> c LCTerm
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCTerm
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> LCTerm -> u
forall u. (forall d. Data d => d -> u) -> LCTerm -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LCTerm -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LCTerm -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LCTerm -> m LCTerm
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LCTerm -> m LCTerm
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCTerm
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCTerm -> c LCTerm
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LCTerm)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LCTerm)
$cLCApp :: Constr
$cLCLam :: Constr
$cLCVar :: Constr
$tLCTerm :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> LCTerm -> m LCTerm
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LCTerm -> m LCTerm
gmapMp :: (forall d. Data d => d -> m d) -> LCTerm -> m LCTerm
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LCTerm -> m LCTerm
gmapM :: (forall d. Data d => d -> m d) -> LCTerm -> m LCTerm
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LCTerm -> m LCTerm
gmapQi :: Int -> (forall d. Data d => d -> u) -> LCTerm -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LCTerm -> u
gmapQ :: (forall d. Data d => d -> u) -> LCTerm -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LCTerm -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LCTerm -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LCTerm -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LCTerm -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LCTerm -> r
gmapT :: (forall b. Data b => b -> b) -> LCTerm -> LCTerm
$cgmapT :: (forall b. Data b => b -> b) -> LCTerm -> LCTerm
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LCTerm)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LCTerm)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c LCTerm)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LCTerm)
dataTypeOf :: LCTerm -> DataType
$cdataTypeOf :: LCTerm -> DataType
toConstr :: LCTerm -> Constr
$ctoConstr :: LCTerm -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCTerm
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCTerm
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCTerm -> c LCTerm
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCTerm -> c LCTerm
$cp1Data :: Typeable LCTerm
Data, LCTerm -> Q Exp
LCTerm -> Q (TExp LCTerm)
(LCTerm -> Q Exp) -> (LCTerm -> Q (TExp LCTerm)) -> Lift LCTerm
forall t. (t -> Q Exp) -> (t -> Q (TExp t)) -> Lift t
liftTyped :: LCTerm -> Q (TExp LCTerm)
$cliftTyped :: LCTerm -> Q (TExp LCTerm)
lift :: LCTerm -> Q Exp
$clift :: LCTerm -> Q Exp
Lift)
infixl 6 `LCApp`

data LCType
  = LCBase
  | LCArr LCType LCType
  deriving stock (LCType -> LCType -> Bool
(LCType -> LCType -> Bool)
-> (LCType -> LCType -> Bool) -> Eq LCType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LCType -> LCType -> Bool
$c/= :: LCType -> LCType -> Bool
== :: LCType -> LCType -> Bool
$c== :: LCType -> LCType -> Bool
Eq, Int -> LCType -> ShowS
[LCType] -> ShowS
LCType -> String
(Int -> LCType -> ShowS)
-> (LCType -> String) -> ([LCType] -> ShowS) -> Show LCType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LCType] -> ShowS
$cshowList :: [LCType] -> ShowS
show :: LCType -> String
$cshow :: LCType -> String
showsPrec :: Int -> LCType -> ShowS
$cshowsPrec :: Int -> LCType -> ShowS
Show, Typeable LCType
DataType
Constr
Typeable LCType
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LCType -> c LCType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LCType)
-> (LCType -> Constr)
-> (LCType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LCType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LCType))
-> ((forall b. Data b => b -> b) -> LCType -> LCType)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LCType -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LCType -> r)
-> (forall u. (forall d. Data d => d -> u) -> LCType -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> LCType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LCType -> m LCType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LCType -> m LCType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LCType -> m LCType)
-> Data LCType
LCType -> DataType
LCType -> Constr
(forall b. Data b => b -> b) -> LCType -> LCType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCType -> c LCType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCType
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> LCType -> u
forall u. (forall d. Data d => d -> u) -> LCType -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LCType -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LCType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LCType -> m LCType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LCType -> m LCType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCType -> c LCType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LCType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LCType)
$cLCArr :: Constr
$cLCBase :: Constr
$tLCType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> LCType -> m LCType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LCType -> m LCType
gmapMp :: (forall d. Data d => d -> m d) -> LCType -> m LCType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LCType -> m LCType
gmapM :: (forall d. Data d => d -> m d) -> LCType -> m LCType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LCType -> m LCType
gmapQi :: Int -> (forall d. Data d => d -> u) -> LCType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LCType -> u
gmapQ :: (forall d. Data d => d -> u) -> LCType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LCType -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LCType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LCType -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LCType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LCType -> r
gmapT :: (forall b. Data b => b -> b) -> LCType -> LCType
$cgmapT :: (forall b. Data b => b -> b) -> LCType -> LCType
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LCType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LCType)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c LCType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LCType)
dataTypeOf :: LCType -> DataType
$cdataTypeOf :: LCType -> DataType
toConstr :: LCType -> Constr
$ctoConstr :: LCType -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCType
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCType -> c LCType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCType -> c LCType
$cp1Data :: Typeable LCType
Data, LCType -> Q Exp
LCType -> Q (TExp LCType)
(LCType -> Q Exp) -> (LCType -> Q (TExp LCType)) -> Lift LCType
forall t. (t -> Q Exp) -> (t -> Q (TExp t)) -> Lift t
liftTyped :: LCType -> Q (TExp LCType)
$cliftTyped :: LCType -> Q (TExp LCType)
lift :: LCType -> Q Exp
$clift :: LCType -> Q Exp
Lift)
infixr 5 `LCArr`

data LCValue
  = LCValLam LCType LCTerm
  deriving stock (LCValue -> LCValue -> Bool
(LCValue -> LCValue -> Bool)
-> (LCValue -> LCValue -> Bool) -> Eq LCValue
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LCValue -> LCValue -> Bool
$c/= :: LCValue -> LCValue -> Bool
== :: LCValue -> LCValue -> Bool
$c== :: LCValue -> LCValue -> Bool
Eq, Int -> LCValue -> ShowS
[LCValue] -> ShowS
LCValue -> String
(Int -> LCValue -> ShowS)
-> (LCValue -> String) -> ([LCValue] -> ShowS) -> Show LCValue
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LCValue] -> ShowS
$cshowList :: [LCValue] -> ShowS
show :: LCValue -> String
$cshow :: LCValue -> String
showsPrec :: Int -> LCValue -> ShowS
$cshowsPrec :: Int -> LCValue -> ShowS
Show, Typeable LCValue
DataType
Constr
Typeable LCValue
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LCValue -> c LCValue)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LCValue)
-> (LCValue -> Constr)
-> (LCValue -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LCValue))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LCValue))
-> ((forall b. Data b => b -> b) -> LCValue -> LCValue)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LCValue -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LCValue -> r)
-> (forall u. (forall d. Data d => d -> u) -> LCValue -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> LCValue -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LCValue -> m LCValue)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LCValue -> m LCValue)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LCValue -> m LCValue)
-> Data LCValue
LCValue -> DataType
LCValue -> Constr
(forall b. Data b => b -> b) -> LCValue -> LCValue
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCValue -> c LCValue
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCValue
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> LCValue -> u
forall u. (forall d. Data d => d -> u) -> LCValue -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LCValue -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LCValue -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LCValue -> m LCValue
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LCValue -> m LCValue
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCValue
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCValue -> c LCValue
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LCValue)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LCValue)
$cLCValLam :: Constr
$tLCValue :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> LCValue -> m LCValue
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LCValue -> m LCValue
gmapMp :: (forall d. Data d => d -> m d) -> LCValue -> m LCValue
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LCValue -> m LCValue
gmapM :: (forall d. Data d => d -> m d) -> LCValue -> m LCValue
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LCValue -> m LCValue
gmapQi :: Int -> (forall d. Data d => d -> u) -> LCValue -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LCValue -> u
gmapQ :: (forall d. Data d => d -> u) -> LCValue -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LCValue -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LCValue -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LCValue -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LCValue -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LCValue -> r
gmapT :: (forall b. Data b => b -> b) -> LCValue -> LCValue
$cgmapT :: (forall b. Data b => b -> b) -> LCValue -> LCValue
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LCValue)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LCValue)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c LCValue)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LCValue)
dataTypeOf :: LCValue -> DataType
$cdataTypeOf :: LCValue -> DataType
toConstr :: LCValue -> Constr
$ctoConstr :: LCValue -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCValue
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCValue
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCValue -> c LCValue
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCValue -> c LCValue
$cp1Data :: Typeable LCValue
Data, LCValue -> Q Exp
LCValue -> Q (TExp LCValue)
(LCValue -> Q Exp) -> (LCValue -> Q (TExp LCValue)) -> Lift LCValue
forall t. (t -> Q Exp) -> (t -> Q (TExp t)) -> Lift t
liftTyped :: LCValue -> Q (TExp LCValue)
$cliftTyped :: LCValue -> Q (TExp LCValue)
lift :: LCValue -> Q Exp
$clift :: LCValue -> Q Exp
Lift)

data LCNormalTerm
  = LCNormLam LCType LCNormalTerm
  | LCNormNeut LCNeutralTerm
  deriving stock (LCNormalTerm -> LCNormalTerm -> Bool
(LCNormalTerm -> LCNormalTerm -> Bool)
-> (LCNormalTerm -> LCNormalTerm -> Bool) -> Eq LCNormalTerm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LCNormalTerm -> LCNormalTerm -> Bool
$c/= :: LCNormalTerm -> LCNormalTerm -> Bool
== :: LCNormalTerm -> LCNormalTerm -> Bool
$c== :: LCNormalTerm -> LCNormalTerm -> Bool
Eq, Int -> LCNormalTerm -> ShowS
[LCNormalTerm] -> ShowS
LCNormalTerm -> String
(Int -> LCNormalTerm -> ShowS)
-> (LCNormalTerm -> String)
-> ([LCNormalTerm] -> ShowS)
-> Show LCNormalTerm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LCNormalTerm] -> ShowS
$cshowList :: [LCNormalTerm] -> ShowS
show :: LCNormalTerm -> String
$cshow :: LCNormalTerm -> String
showsPrec :: Int -> LCNormalTerm -> ShowS
$cshowsPrec :: Int -> LCNormalTerm -> ShowS
Show, Typeable LCNormalTerm
DataType
Constr
Typeable LCNormalTerm
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LCNormalTerm -> c LCNormalTerm)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LCNormalTerm)
-> (LCNormalTerm -> Constr)
-> (LCNormalTerm -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LCNormalTerm))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c LCNormalTerm))
-> ((forall b. Data b => b -> b) -> LCNormalTerm -> LCNormalTerm)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LCNormalTerm -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LCNormalTerm -> r)
-> (forall u. (forall d. Data d => d -> u) -> LCNormalTerm -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> LCNormalTerm -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LCNormalTerm -> m LCNormalTerm)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LCNormalTerm -> m LCNormalTerm)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LCNormalTerm -> m LCNormalTerm)
-> Data LCNormalTerm
LCNormalTerm -> DataType
LCNormalTerm -> Constr
(forall b. Data b => b -> b) -> LCNormalTerm -> LCNormalTerm
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCNormalTerm -> c LCNormalTerm
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCNormalTerm
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> LCNormalTerm -> u
forall u. (forall d. Data d => d -> u) -> LCNormalTerm -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LCNormalTerm -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LCNormalTerm -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LCNormalTerm -> m LCNormalTerm
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LCNormalTerm -> m LCNormalTerm
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCNormalTerm
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCNormalTerm -> c LCNormalTerm
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LCNormalTerm)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LCNormalTerm)
$cLCNormNeut :: Constr
$cLCNormLam :: Constr
$tLCNormalTerm :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> LCNormalTerm -> m LCNormalTerm
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LCNormalTerm -> m LCNormalTerm
gmapMp :: (forall d. Data d => d -> m d) -> LCNormalTerm -> m LCNormalTerm
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LCNormalTerm -> m LCNormalTerm
gmapM :: (forall d. Data d => d -> m d) -> LCNormalTerm -> m LCNormalTerm
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LCNormalTerm -> m LCNormalTerm
gmapQi :: Int -> (forall d. Data d => d -> u) -> LCNormalTerm -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LCNormalTerm -> u
gmapQ :: (forall d. Data d => d -> u) -> LCNormalTerm -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LCNormalTerm -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LCNormalTerm -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LCNormalTerm -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LCNormalTerm -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LCNormalTerm -> r
gmapT :: (forall b. Data b => b -> b) -> LCNormalTerm -> LCNormalTerm
$cgmapT :: (forall b. Data b => b -> b) -> LCNormalTerm -> LCNormalTerm
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LCNormalTerm)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LCNormalTerm)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c LCNormalTerm)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LCNormalTerm)
dataTypeOf :: LCNormalTerm -> DataType
$cdataTypeOf :: LCNormalTerm -> DataType
toConstr :: LCNormalTerm -> Constr
$ctoConstr :: LCNormalTerm -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCNormalTerm
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCNormalTerm
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCNormalTerm -> c LCNormalTerm
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCNormalTerm -> c LCNormalTerm
$cp1Data :: Typeable LCNormalTerm
Data, LCNormalTerm -> Q Exp
LCNormalTerm -> Q (TExp LCNormalTerm)
(LCNormalTerm -> Q Exp)
-> (LCNormalTerm -> Q (TExp LCNormalTerm)) -> Lift LCNormalTerm
forall t. (t -> Q Exp) -> (t -> Q (TExp t)) -> Lift t
liftTyped :: LCNormalTerm -> Q (TExp LCNormalTerm)
$cliftTyped :: LCNormalTerm -> Q (TExp LCNormalTerm)
lift :: LCNormalTerm -> Q Exp
$clift :: LCNormalTerm -> Q Exp
Lift)

data LCNeutralTerm
  = LCNeutVar Int
  | LCNeutApp LCNeutralTerm LCNormalTerm
  deriving stock (LCNeutralTerm -> LCNeutralTerm -> Bool
(LCNeutralTerm -> LCNeutralTerm -> Bool)
-> (LCNeutralTerm -> LCNeutralTerm -> Bool) -> Eq LCNeutralTerm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LCNeutralTerm -> LCNeutralTerm -> Bool
$c/= :: LCNeutralTerm -> LCNeutralTerm -> Bool
== :: LCNeutralTerm -> LCNeutralTerm -> Bool
$c== :: LCNeutralTerm -> LCNeutralTerm -> Bool
Eq, Int -> LCNeutralTerm -> ShowS
[LCNeutralTerm] -> ShowS
LCNeutralTerm -> String
(Int -> LCNeutralTerm -> ShowS)
-> (LCNeutralTerm -> String)
-> ([LCNeutralTerm] -> ShowS)
-> Show LCNeutralTerm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LCNeutralTerm] -> ShowS
$cshowList :: [LCNeutralTerm] -> ShowS
show :: LCNeutralTerm -> String
$cshow :: LCNeutralTerm -> String
showsPrec :: Int -> LCNeutralTerm -> ShowS
$cshowsPrec :: Int -> LCNeutralTerm -> ShowS
Show, Typeable LCNeutralTerm
DataType
Constr
Typeable LCNeutralTerm
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LCNeutralTerm -> c LCNeutralTerm)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LCNeutralTerm)
-> (LCNeutralTerm -> Constr)
-> (LCNeutralTerm -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LCNeutralTerm))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c LCNeutralTerm))
-> ((forall b. Data b => b -> b) -> LCNeutralTerm -> LCNeutralTerm)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LCNeutralTerm -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LCNeutralTerm -> r)
-> (forall u. (forall d. Data d => d -> u) -> LCNeutralTerm -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> LCNeutralTerm -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LCNeutralTerm -> m LCNeutralTerm)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LCNeutralTerm -> m LCNeutralTerm)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LCNeutralTerm -> m LCNeutralTerm)
-> Data LCNeutralTerm
LCNeutralTerm -> DataType
LCNeutralTerm -> Constr
(forall b. Data b => b -> b) -> LCNeutralTerm -> LCNeutralTerm
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCNeutralTerm -> c LCNeutralTerm
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCNeutralTerm
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> LCNeutralTerm -> u
forall u. (forall d. Data d => d -> u) -> LCNeutralTerm -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LCNeutralTerm -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LCNeutralTerm -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LCNeutralTerm -> m LCNeutralTerm
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LCNeutralTerm -> m LCNeutralTerm
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCNeutralTerm
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCNeutralTerm -> c LCNeutralTerm
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LCNeutralTerm)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LCNeutralTerm)
$cLCNeutApp :: Constr
$cLCNeutVar :: Constr
$tLCNeutralTerm :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> LCNeutralTerm -> m LCNeutralTerm
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LCNeutralTerm -> m LCNeutralTerm
gmapMp :: (forall d. Data d => d -> m d) -> LCNeutralTerm -> m LCNeutralTerm
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LCNeutralTerm -> m LCNeutralTerm
gmapM :: (forall d. Data d => d -> m d) -> LCNeutralTerm -> m LCNeutralTerm
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LCNeutralTerm -> m LCNeutralTerm
gmapQi :: Int -> (forall d. Data d => d -> u) -> LCNeutralTerm -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LCNeutralTerm -> u
gmapQ :: (forall d. Data d => d -> u) -> LCNeutralTerm -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LCNeutralTerm -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LCNeutralTerm -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LCNeutralTerm -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LCNeutralTerm -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LCNeutralTerm -> r
gmapT :: (forall b. Data b => b -> b) -> LCNeutralTerm -> LCNeutralTerm
$cgmapT :: (forall b. Data b => b -> b) -> LCNeutralTerm -> LCNeutralTerm
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LCNeutralTerm)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LCNeutralTerm)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c LCNeutralTerm)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LCNeutralTerm)
dataTypeOf :: LCNeutralTerm -> DataType
$cdataTypeOf :: LCNeutralTerm -> DataType
toConstr :: LCNeutralTerm -> Constr
$ctoConstr :: LCNeutralTerm -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCNeutralTerm
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LCNeutralTerm
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCNeutralTerm -> c LCNeutralTerm
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LCNeutralTerm -> c LCNeutralTerm
$cp1Data :: Typeable LCNeutralTerm
Data, LCNeutralTerm -> Q Exp
LCNeutralTerm -> Q (TExp LCNeutralTerm)
(LCNeutralTerm -> Q Exp)
-> (LCNeutralTerm -> Q (TExp LCNeutralTerm)) -> Lift LCNeutralTerm
forall t. (t -> Q Exp) -> (t -> Q (TExp t)) -> Lift t
liftTyped :: LCNeutralTerm -> Q (TExp LCNeutralTerm)
$cliftTyped :: LCNeutralTerm -> Q (TExp LCNeutralTerm)
lift :: LCNeutralTerm -> Q Exp
$clift :: LCNeutralTerm -> Q Exp
Lift)
infixl 6 `LCNeutApp`