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`