module UVMHS.Lang.ULC where import UVMHS.Core import UVMHS.Lib.Parser import UVMHS.Lib.Pretty import UVMHS.Lib.Annotated import UVMHS.Lib.Variables import UVMHS.Lib.Substitution import UVMHS.Lib.Rand import UVMHS.Lib.THLiftInstances () import qualified Language.Haskell.TH.Syntax as TH import qualified Language.Haskell.TH.Quote as TH import Control.Monad.Fail as HS newtype ULCExp πΈ = ULCExp { forall πΈ. ULCExp πΈ -> π΄ πΈ (ULCExp_R πΈ) unULCExp β· π΄ πΈ (ULCExp_R πΈ) } deriving (ULCExp πΈ -> ULCExp πΈ -> Bool (ULCExp πΈ -> ULCExp πΈ -> Bool) -> (ULCExp πΈ -> ULCExp πΈ -> Bool) -> Eq (ULCExp πΈ) forall πΈ. ULCExp πΈ -> ULCExp πΈ -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a $c== :: forall πΈ. ULCExp πΈ -> ULCExp πΈ -> Bool == :: ULCExp πΈ -> ULCExp πΈ -> Bool $c/= :: forall πΈ. ULCExp πΈ -> ULCExp πΈ -> Bool /= :: ULCExp πΈ -> ULCExp πΈ -> Bool Eq,Eq (ULCExp πΈ) Eq (ULCExp πΈ) => (ULCExp πΈ -> ULCExp πΈ -> Ordering) -> (ULCExp πΈ -> ULCExp πΈ -> Bool) -> (ULCExp πΈ -> ULCExp πΈ -> Bool) -> (ULCExp πΈ -> ULCExp πΈ -> Bool) -> (ULCExp πΈ -> ULCExp πΈ -> Bool) -> (ULCExp πΈ -> ULCExp πΈ -> ULCExp πΈ) -> (ULCExp πΈ -> ULCExp πΈ -> ULCExp πΈ) -> Ord (ULCExp πΈ) ULCExp πΈ -> ULCExp πΈ -> Bool ULCExp πΈ -> ULCExp πΈ -> Ordering ULCExp πΈ -> ULCExp πΈ -> ULCExp πΈ forall πΈ. Eq (ULCExp πΈ) forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a forall πΈ. ULCExp πΈ -> ULCExp πΈ -> Bool forall πΈ. ULCExp πΈ -> ULCExp πΈ -> Ordering forall πΈ. ULCExp πΈ -> ULCExp πΈ -> ULCExp πΈ $ccompare :: forall πΈ. ULCExp πΈ -> ULCExp πΈ -> Ordering compare :: ULCExp πΈ -> ULCExp πΈ -> Ordering $c< :: forall πΈ. ULCExp πΈ -> ULCExp πΈ -> Bool < :: ULCExp πΈ -> ULCExp πΈ -> Bool $c<= :: forall πΈ. ULCExp πΈ -> ULCExp πΈ -> Bool <= :: ULCExp πΈ -> ULCExp πΈ -> Bool $c> :: forall πΈ. ULCExp πΈ -> ULCExp πΈ -> Bool > :: ULCExp πΈ -> ULCExp πΈ -> Bool $c>= :: forall πΈ. ULCExp πΈ -> ULCExp πΈ -> Bool >= :: ULCExp πΈ -> ULCExp πΈ -> Bool $cmax :: forall πΈ. ULCExp πΈ -> ULCExp πΈ -> ULCExp πΈ max :: ULCExp πΈ -> ULCExp πΈ -> ULCExp πΈ $cmin :: forall πΈ. ULCExp πΈ -> ULCExp πΈ -> ULCExp πΈ min :: ULCExp πΈ -> ULCExp πΈ -> ULCExp πΈ Ord,Int -> ULCExp πΈ -> ShowS [ULCExp πΈ] -> ShowS ULCExp πΈ -> String (Int -> ULCExp πΈ -> ShowS) -> (ULCExp πΈ -> String) -> ([ULCExp πΈ] -> ShowS) -> Show (ULCExp πΈ) forall πΈ. Show πΈ => Int -> ULCExp πΈ -> ShowS forall πΈ. Show πΈ => [ULCExp πΈ] -> ShowS forall πΈ. Show πΈ => ULCExp πΈ -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a $cshowsPrec :: forall πΈ. Show πΈ => Int -> ULCExp πΈ -> ShowS showsPrec :: Int -> ULCExp πΈ -> ShowS $cshow :: forall πΈ. Show πΈ => ULCExp πΈ -> String show :: ULCExp πΈ -> String $cshowList :: forall πΈ. Show πΈ => [ULCExp πΈ] -> ShowS showList :: [ULCExp πΈ] -> ShowS Show) data ULCExp_R πΈ = Var_ULC π | Lam_ULC (π π) (ULCExp πΈ) | App_ULC (ULCExp πΈ) (ULCExp πΈ) deriving (ULCExp_R πΈ -> ULCExp_R πΈ -> Bool (ULCExp_R πΈ -> ULCExp_R πΈ -> Bool) -> (ULCExp_R πΈ -> ULCExp_R πΈ -> Bool) -> Eq (ULCExp_R πΈ) forall πΈ. ULCExp_R πΈ -> ULCExp_R πΈ -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a $c== :: forall πΈ. ULCExp_R πΈ -> ULCExp_R πΈ -> Bool == :: ULCExp_R πΈ -> ULCExp_R πΈ -> Bool $c/= :: forall πΈ. ULCExp_R πΈ -> ULCExp_R πΈ -> Bool /= :: ULCExp_R πΈ -> ULCExp_R πΈ -> Bool Eq,Eq (ULCExp_R πΈ) Eq (ULCExp_R πΈ) => (ULCExp_R πΈ -> ULCExp_R πΈ -> Ordering) -> (ULCExp_R πΈ -> ULCExp_R πΈ -> Bool) -> (ULCExp_R πΈ -> ULCExp_R πΈ -> Bool) -> (ULCExp_R πΈ -> ULCExp_R πΈ -> Bool) -> (ULCExp_R πΈ -> ULCExp_R πΈ -> Bool) -> (ULCExp_R πΈ -> ULCExp_R πΈ -> ULCExp_R πΈ) -> (ULCExp_R πΈ -> ULCExp_R πΈ -> ULCExp_R πΈ) -> Ord (ULCExp_R πΈ) ULCExp_R πΈ -> ULCExp_R πΈ -> Bool ULCExp_R πΈ -> ULCExp_R πΈ -> Ordering ULCExp_R πΈ -> ULCExp_R πΈ -> ULCExp_R πΈ forall πΈ. Eq (ULCExp_R πΈ) forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a forall πΈ. ULCExp_R πΈ -> ULCExp_R πΈ -> Bool forall πΈ. ULCExp_R πΈ -> ULCExp_R πΈ -> Ordering forall πΈ. ULCExp_R πΈ -> ULCExp_R πΈ -> ULCExp_R πΈ $ccompare :: forall πΈ. ULCExp_R πΈ -> ULCExp_R πΈ -> Ordering compare :: ULCExp_R πΈ -> ULCExp_R πΈ -> Ordering $c< :: forall πΈ. ULCExp_R πΈ -> ULCExp_R πΈ -> Bool < :: ULCExp_R πΈ -> ULCExp_R πΈ -> Bool $c<= :: forall πΈ. ULCExp_R πΈ -> ULCExp_R πΈ -> Bool <= :: ULCExp_R πΈ -> ULCExp_R πΈ -> Bool $c> :: forall πΈ. ULCExp_R πΈ -> ULCExp_R πΈ -> Bool > :: ULCExp_R πΈ -> ULCExp_R πΈ -> Bool $c>= :: forall πΈ. ULCExp_R πΈ -> ULCExp_R πΈ -> Bool >= :: ULCExp_R πΈ -> ULCExp_R πΈ -> Bool $cmax :: forall πΈ. ULCExp_R πΈ -> ULCExp_R πΈ -> ULCExp_R πΈ max :: ULCExp_R πΈ -> ULCExp_R πΈ -> ULCExp_R πΈ $cmin :: forall πΈ. ULCExp_R πΈ -> ULCExp_R πΈ -> ULCExp_R πΈ min :: ULCExp_R πΈ -> ULCExp_R πΈ -> ULCExp_R πΈ Ord,Int -> ULCExp_R πΈ -> ShowS [ULCExp_R πΈ] -> ShowS ULCExp_R πΈ -> String (Int -> ULCExp_R πΈ -> ShowS) -> (ULCExp_R πΈ -> String) -> ([ULCExp_R πΈ] -> ShowS) -> Show (ULCExp_R πΈ) forall πΈ. Show πΈ => Int -> ULCExp_R πΈ -> ShowS forall πΈ. Show πΈ => [ULCExp_R πΈ] -> ShowS forall πΈ. Show πΈ => ULCExp_R πΈ -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a $cshowsPrec :: forall πΈ. Show πΈ => Int -> ULCExp_R πΈ -> ShowS showsPrec :: Int -> ULCExp_R πΈ -> ShowS $cshow :: forall πΈ. Show πΈ => ULCExp_R πΈ -> String show :: ULCExp_R πΈ -> String $cshowList :: forall πΈ. Show πΈ => [ULCExp_R πΈ] -> ShowS showList :: [ULCExp_R πΈ] -> ShowS Show) type ULCExpSrc = ULCExp SrcCxt type ULCExpRaw = ULCExp () lexULCExp β· Lexer CharClass β TokenClassBasic β64 TokenBasic lexULCExp :: Lexer CharClass β TokenClassBasic β64 TokenBasic lexULCExp = πΏ π -> πΏ π -> πΏ π -> πΏ π -> Lexer CharClass β TokenClassBasic β64 TokenBasic lexerBasic ([π] -> πΏ π forall a t. ToIter a t => t -> πΏ a list [π "(",π ")",π "->",π "β",π "^",π "β",π ":"]) ([π] -> πΏ π forall a t. ToIter a t => t -> πΏ a list [π "lam",π "Ξ»"]) ([π] -> πΏ π forall a t. ToIter a t => t -> πΏ a list [π "glbl",π "π€",π "meta",π "πͺ"]) πΏ π forall a. Null a => a null pULCExp β· CParser TokenBasic ULCExpSrc pULCExp :: CParser TokenBasic ULCExpSrc pULCExp = π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExpSrc forall πΈ. π΄ πΈ (ULCExp_R πΈ) -> ULCExp πΈ ULCExp (π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExpSrc) -> CParser TokenBasic (π΄ SrcCxt (ULCExp_R SrcCxt)) -> CParser TokenBasic ULCExpSrc forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b ^$ π -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt) -> CParser TokenBasic (π΄ SrcCxt (ULCExp_R SrcCxt)) forall t a. Ord t => π -> MixfixF t (π΄ SrcCxt) a -> CParser t (π΄ SrcCxt a) fmixfixWithContext π "exp" (MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt) -> CParser TokenBasic (π΄ SrcCxt (ULCExp_R SrcCxt))) -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt) -> CParser TokenBasic (π΄ SrcCxt (ULCExp_R SrcCxt)) forall a b. (a -> b) -> a -> b $ [MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt)] -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt) forall a t. (Monoid a, ToIter a t) => t -> a concat [ CParser TokenBasic (ULCExp_R SrcCxt) -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt) forall t a (f :: * -> *). CParser t a -> MixfixF t f a fmixTerminal (CParser TokenBasic (ULCExp_R SrcCxt) -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt)) -> CParser TokenBasic (ULCExp_R SrcCxt) -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt) forall a b. (a -> b) -> a -> b $ do CParser TokenBasic TokenBasic -> CParser TokenBasic () forall (m :: * -> *) a. Functor m => m a -> m () void (CParser TokenBasic TokenBasic -> CParser TokenBasic ()) -> CParser TokenBasic TokenBasic -> CParser TokenBasic () forall a b. (a -> b) -> a -> b $ π -> CParser TokenBasic TokenBasic cpSyntax π "(" ULCExpSrc e β CParser TokenBasic ULCExpSrc pULCExp CParser TokenBasic TokenBasic -> CParser TokenBasic () forall (m :: * -> *) a. Functor m => m a -> m () void (CParser TokenBasic TokenBasic -> CParser TokenBasic ()) -> CParser TokenBasic TokenBasic -> CParser TokenBasic () forall a b. (a -> b) -> a -> b $ π -> CParser TokenBasic TokenBasic cpSyntax π ")" ULCExp_R SrcCxt -> CParser TokenBasic (ULCExp_R SrcCxt) forall a. a -> CParser TokenBasic a forall (m :: * -> *) a. Return m => a -> m a return (ULCExp_R SrcCxt -> CParser TokenBasic (ULCExp_R SrcCxt)) -> ULCExp_R SrcCxt -> CParser TokenBasic (ULCExp_R SrcCxt) forall a b. (a -> b) -> a -> b $ π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt forall e a. π΄ e a -> a aval (π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt) -> π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt forall a b. (a -> b) -> a -> b $ ULCExpSrc -> π΄ SrcCxt (ULCExp_R SrcCxt) forall πΈ. ULCExp πΈ -> π΄ πΈ (ULCExp_R πΈ) unULCExp ULCExpSrc e , CParser TokenBasic (ULCExp_R SrcCxt) -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt) forall t a (f :: * -> *). CParser t a -> MixfixF t f a fmixTerminal (CParser TokenBasic (ULCExp_R SrcCxt) -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt)) -> CParser TokenBasic (ULCExp_R SrcCxt) -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt) forall a b. (a -> b) -> a -> b $ do β64 n β π β64 -> CParser TokenBasic β64 forall (m :: * -> *) a. (Monad m, MonadFail m) => π a -> m a failEff (π β64 -> CParser TokenBasic β64) -> (β€ -> π β64) -> β€ -> CParser TokenBasic β64 forall b c a. (b -> c) -> (a -> b) -> a -> c β β€ -> π β64 forall a. ToNatO64 a => a -> π β64 natO64 (β€ -> CParser TokenBasic β64) -> CParser TokenBasic β€ -> CParser TokenBasic β64 forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b *$ CParser TokenBasic β€ cpInteger ULCExp_R SrcCxt -> CParser TokenBasic (ULCExp_R SrcCxt) forall a. a -> CParser TokenBasic a forall (m :: * -> *) a. Return m => a -> m a return (ULCExp_R SrcCxt -> CParser TokenBasic (ULCExp_R SrcCxt)) -> ULCExp_R SrcCxt -> CParser TokenBasic (ULCExp_R SrcCxt) forall a b. (a -> b) -> a -> b $ π -> ULCExp_R SrcCxt forall πΈ. π -> ULCExp_R πΈ Var_ULC (π -> ULCExp_R SrcCxt) -> π -> ULCExp_R SrcCxt forall a b. (a -> b) -> a -> b $ β64 -> π DVar β64 n , CParser TokenBasic (ULCExp_R SrcCxt) -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt) forall t a (f :: * -> *). CParser t a -> MixfixF t f a fmixTerminal (CParser TokenBasic (ULCExp_R SrcCxt) -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt)) -> CParser TokenBasic (ULCExp_R SrcCxt) -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt) forall a b. (a -> b) -> a -> b $ do π (π -> π) fO β CParser TokenBasic (π -> π) -> CParser TokenBasic (π (π -> π)) forall t a. Ord t => CParser t a -> CParser t (π a) cpOptional (CParser TokenBasic (π -> π) -> CParser TokenBasic (π (π -> π))) -> CParser TokenBasic (π -> π) -> CParser TokenBasic (π (π -> π)) forall a b. (a -> b) -> a -> b $ [CParser TokenBasic (π -> π)] -> CParser TokenBasic (π -> π) forall a t. (Monoid a, ToIter a t) => t -> a concat [ do CParser TokenBasic TokenBasic -> CParser TokenBasic () forall (m :: * -> *) a. Functor m => m a -> m () void (CParser TokenBasic TokenBasic -> CParser TokenBasic ()) -> CParser TokenBasic TokenBasic -> CParser TokenBasic () forall a b. (a -> b) -> a -> b $ [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic forall a t. (Monoid a, ToIter a t) => t -> a concat ([CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic) -> [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic forall a b. (a -> b) -> a -> b $ (π -> CParser TokenBasic TokenBasic) -> [π] -> [CParser TokenBasic TokenBasic] forall a b. (a -> b) -> [a] -> [b] forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b map π -> CParser TokenBasic TokenBasic cpSyntax [π "glbl",π "π€"] CParser TokenBasic TokenBasic -> CParser TokenBasic () forall (m :: * -> *) a. Functor m => m a -> m () void (CParser TokenBasic TokenBasic -> CParser TokenBasic ()) -> CParser TokenBasic TokenBasic -> CParser TokenBasic () forall a b. (a -> b) -> a -> b $ π -> CParser TokenBasic TokenBasic cpSyntax π ":" (π -> π) -> CParser TokenBasic (π -> π) forall a. a -> CParser TokenBasic a forall (m :: * -> *) a. Return m => a -> m a return π -> π GVar , do CParser TokenBasic TokenBasic -> CParser TokenBasic () forall (m :: * -> *) a. Functor m => m a -> m () void (CParser TokenBasic TokenBasic -> CParser TokenBasic ()) -> CParser TokenBasic TokenBasic -> CParser TokenBasic () forall a b. (a -> b) -> a -> b $ [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic forall a t. (Monoid a, ToIter a t) => t -> a concat ([CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic) -> [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic forall a b. (a -> b) -> a -> b $ (π -> CParser TokenBasic TokenBasic) -> [π] -> [CParser TokenBasic TokenBasic] forall a b. (a -> b) -> [a] -> [b] forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b map π -> CParser TokenBasic TokenBasic cpSyntax [π "meta",π "πͺ"] CParser TokenBasic TokenBasic -> CParser TokenBasic () forall (m :: * -> *) a. Functor m => m a -> m () void (CParser TokenBasic TokenBasic -> CParser TokenBasic ()) -> CParser TokenBasic TokenBasic -> CParser TokenBasic () forall a b. (a -> b) -> a -> b $ π -> CParser TokenBasic TokenBasic cpSyntax π ":" (π -> π) -> CParser TokenBasic (π -> π) forall a. a -> CParser TokenBasic a forall (m :: * -> *) a. Return m => a -> m a return π -> π MVar ] π x β CParser TokenBasic π cpVar case π (π -> π) fO of Some π -> π f β ULCExp_R SrcCxt -> CParser TokenBasic (ULCExp_R SrcCxt) forall a. a -> CParser TokenBasic a forall (m :: * -> *) a. Return m => a -> m a return (ULCExp_R SrcCxt -> CParser TokenBasic (ULCExp_R SrcCxt)) -> ULCExp_R SrcCxt -> CParser TokenBasic (ULCExp_R SrcCxt) forall a b. (a -> b) -> a -> b $ π -> ULCExp_R SrcCxt forall πΈ. π -> ULCExp_R πΈ Var_ULC (π -> ULCExp_R SrcCxt) -> π -> ULCExp_R SrcCxt forall a b. (a -> b) -> a -> b $ π -> π f π x π (π -> π) None β do β64 n β β64 -> π β64 -> β64 forall a. a -> π a -> a ifNone β64 0 (π β64 -> β64) -> CParser TokenBasic (π β64) -> CParser TokenBasic β64 forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b ^$ CParser TokenBasic β64 -> CParser TokenBasic (π β64) forall t a. Ord t => CParser t a -> CParser t (π a) cpOptional (CParser TokenBasic β64 -> CParser TokenBasic (π β64)) -> CParser TokenBasic β64 -> CParser TokenBasic (π β64) forall a b. (a -> b) -> a -> b $ do CParser TokenBasic TokenBasic -> CParser TokenBasic () forall (m :: * -> *) a. Functor m => m a -> m () void (CParser TokenBasic TokenBasic -> CParser TokenBasic ()) -> CParser TokenBasic TokenBasic -> CParser TokenBasic () forall a b. (a -> b) -> a -> b $ [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic forall a t. (Monoid a, ToIter a t) => t -> a concat ([CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic) -> [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic forall a b. (a -> b) -> a -> b $ (π -> CParser TokenBasic TokenBasic) -> [π] -> [CParser TokenBasic TokenBasic] forall a b. (a -> b) -> [a] -> [b] forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b map π -> CParser TokenBasic TokenBasic cpSyntax [π "^",π "β"] π β64 -> CParser TokenBasic β64 forall (m :: * -> *) a. (Monad m, MonadFail m) => π a -> m a failEff (π β64 -> CParser TokenBasic β64) -> (β€ -> π β64) -> β€ -> CParser TokenBasic β64 forall b c a. (b -> c) -> (a -> b) -> a -> c β β€ -> π β64 forall a. ToNatO64 a => a -> π β64 natO64 (β€ -> CParser TokenBasic β64) -> CParser TokenBasic β€ -> CParser TokenBasic β64 forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b *$ CParser TokenBasic β€ cpInteger ULCExp_R SrcCxt -> CParser TokenBasic (ULCExp_R SrcCxt) forall a. a -> CParser TokenBasic a forall (m :: * -> *) a. Return m => a -> m a return (ULCExp_R SrcCxt -> CParser TokenBasic (ULCExp_R SrcCxt)) -> ULCExp_R SrcCxt -> CParser TokenBasic (ULCExp_R SrcCxt) forall a b. (a -> b) -> a -> b $ π -> ULCExp_R SrcCxt forall πΈ. π -> ULCExp_R πΈ Var_ULC (π -> ULCExp_R SrcCxt) -> π -> ULCExp_R SrcCxt forall a b. (a -> b) -> a -> b $ β64 -> π -> π NVar β64 n π x , β64 -> CParser TokenBasic (π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt) -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt) forall t (f :: * -> *) a. β64 -> CParser t (f a -> a) -> MixfixF t f a fmixPrefix β64 pLET (CParser TokenBasic (π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt) -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt)) -> CParser TokenBasic (π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt) -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt) forall a b. (a -> b) -> a -> b $ do CParser TokenBasic TokenBasic -> CParser TokenBasic () forall (m :: * -> *) a. Functor m => m a -> m () void (CParser TokenBasic TokenBasic -> CParser TokenBasic ()) -> CParser TokenBasic TokenBasic -> CParser TokenBasic () forall a b. (a -> b) -> a -> b $ [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic forall a t. (Monoid a, ToIter a t) => t -> a concat ([CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic) -> [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic forall a b. (a -> b) -> a -> b $ (π -> CParser TokenBasic TokenBasic) -> [π] -> [CParser TokenBasic TokenBasic] forall a b. (a -> b) -> [a] -> [b] forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b map π -> CParser TokenBasic TokenBasic cpSyntax [π "lam",π "Ξ»"] π π xO β CParser TokenBasic π -> CParser TokenBasic (π π) forall t a. Ord t => CParser t a -> CParser t (π a) cpOptional (CParser TokenBasic π -> CParser TokenBasic (π π)) -> CParser TokenBasic π -> CParser TokenBasic (π π) forall a b. (a -> b) -> a -> b $ CParser TokenBasic π cpVar CParser TokenBasic TokenBasic -> CParser TokenBasic () forall (m :: * -> *) a. Functor m => m a -> m () void (CParser TokenBasic TokenBasic -> CParser TokenBasic ()) -> CParser TokenBasic TokenBasic -> CParser TokenBasic () forall a b. (a -> b) -> a -> b $ [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic forall a t. (Monoid a, ToIter a t) => t -> a concat ([CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic) -> [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic forall a b. (a -> b) -> a -> b $ (π -> CParser TokenBasic TokenBasic) -> [π] -> [CParser TokenBasic TokenBasic] forall a b. (a -> b) -> [a] -> [b] forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b map π -> CParser TokenBasic TokenBasic cpSyntax [π "->",π "β"] (π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt) -> CParser TokenBasic (π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt) forall a. a -> CParser TokenBasic a forall (m :: * -> *) a. Return m => a -> m a return ((π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt) -> CParser TokenBasic (π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt)) -> (π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt) -> CParser TokenBasic (π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt) forall a b. (a -> b) -> a -> b $ \ π΄ SrcCxt (ULCExp_R SrcCxt) e β π π -> ULCExpSrc -> ULCExp_R SrcCxt forall πΈ. π π -> ULCExp πΈ -> ULCExp_R πΈ Lam_ULC π π xO (ULCExpSrc -> ULCExp_R SrcCxt) -> ULCExpSrc -> ULCExp_R SrcCxt forall a b. (a -> b) -> a -> b $ π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExpSrc forall πΈ. π΄ πΈ (ULCExp_R πΈ) -> ULCExp πΈ ULCExp π΄ SrcCxt (ULCExp_R SrcCxt) e , β64 -> CParser TokenBasic (π΄ SrcCxt (ULCExp_R SrcCxt) -> π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt) -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt) forall t (f :: * -> *) a. β64 -> CParser t (f a -> f a -> a) -> MixfixF t f a fmixInfixL β64 pAPP (CParser TokenBasic (π΄ SrcCxt (ULCExp_R SrcCxt) -> π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt) -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt)) -> CParser TokenBasic (π΄ SrcCxt (ULCExp_R SrcCxt) -> π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt) -> MixfixF TokenBasic (π΄ SrcCxt) (ULCExp_R SrcCxt) forall a b. (a -> b) -> a -> b $ (π΄ SrcCxt (ULCExp_R SrcCxt) -> π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt) -> CParser TokenBasic (π΄ SrcCxt (ULCExp_R SrcCxt) -> π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt) forall a. a -> CParser TokenBasic a forall (m :: * -> *) a. Return m => a -> m a return ((π΄ SrcCxt (ULCExp_R SrcCxt) -> π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt) -> CParser TokenBasic (π΄ SrcCxt (ULCExp_R SrcCxt) -> π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt)) -> (π΄ SrcCxt (ULCExp_R SrcCxt) -> π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt) -> CParser TokenBasic (π΄ SrcCxt (ULCExp_R SrcCxt) -> π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExp_R SrcCxt) forall a b. (a -> b) -> a -> b $ \ π΄ SrcCxt (ULCExp_R SrcCxt) eβ π΄ SrcCxt (ULCExp_R SrcCxt) eβ β ULCExpSrc -> ULCExpSrc -> ULCExp_R SrcCxt forall πΈ. ULCExp πΈ -> ULCExp πΈ -> ULCExp_R πΈ App_ULC (π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExpSrc forall πΈ. π΄ πΈ (ULCExp_R πΈ) -> ULCExp πΈ ULCExp π΄ SrcCxt (ULCExp_R SrcCxt) eβ) (ULCExpSrc -> ULCExp_R SrcCxt) -> ULCExpSrc -> ULCExp_R SrcCxt forall a b. (a -> b) -> a -> b $ π΄ SrcCxt (ULCExp_R SrcCxt) -> ULCExpSrc forall πΈ. π΄ πΈ (ULCExp_R πΈ) -> ULCExp πΈ ULCExp π΄ SrcCxt (ULCExp_R SrcCxt) eβ ] instance Pretty (ULCExp πΈ) where pretty :: ULCExp πΈ -> Doc pretty = ULCExp_R πΈ -> Doc forall a. Pretty a => a -> Doc pretty (ULCExp_R πΈ -> Doc) -> (π΄ πΈ (ULCExp_R πΈ) -> ULCExp_R πΈ) -> π΄ πΈ (ULCExp_R πΈ) -> Doc forall b c a. (b -> c) -> (a -> b) -> a -> c β π΄ πΈ (ULCExp_R πΈ) -> ULCExp_R πΈ forall e a. π΄ e a -> a aval (π΄ πΈ (ULCExp_R πΈ) -> Doc) -> (ULCExp πΈ -> π΄ πΈ (ULCExp_R πΈ)) -> ULCExp πΈ -> Doc forall b c a. (b -> c) -> (a -> b) -> a -> c β ULCExp πΈ -> π΄ πΈ (ULCExp_R πΈ) forall πΈ. ULCExp πΈ -> π΄ πΈ (ULCExp_R πΈ) unULCExp instance Pretty (ULCExp_R πΈ) where pretty :: ULCExp_R πΈ -> Doc pretty = \case Var_ULC π x β π -> Doc forall a. Pretty a => a -> Doc pretty π x Lam_ULC π π xO ULCExp πΈ e β (Doc -> Doc -> Doc) -> Doc -> Doc -> Doc forall a b c. (a -> b -> c) -> b -> a -> c flip (β64 -> Doc -> Doc -> Doc ppPreSep β64 pLET) (ULCExp πΈ -> Doc forall a. Pretty a => a -> Doc pretty ULCExp πΈ e) (Doc -> Doc) -> Doc -> Doc forall a b. (a -> b) -> a -> b $ πΌ Doc -> Doc forall t. ToIter Doc t => t -> Doc ppHorizontal (πΌ Doc -> Doc) -> πΌ Doc -> Doc forall a b. (a -> b) -> a -> b $ [πΌ Doc] -> πΌ Doc forall a t. (Monoid a, ToIter a t) => t -> a concat [ Doc -> πΌ Doc forall a. a -> πΌ a singleπΌ (Doc -> πΌ Doc) -> Doc -> πΌ Doc forall a b. (a -> b) -> a -> b $ π -> Doc ppKey π "Ξ»" , (() -> πΌ Doc) -> (π -> πΌ Doc) -> π π -> πΌ Doc forall b a. (() -> b) -> (a -> b) -> π a -> b elimπ () -> πΌ Doc forall a. Null a => a null (Doc -> πΌ Doc forall a t. Single a t => a -> t single (Doc -> πΌ Doc) -> (Doc -> Doc) -> Doc -> πΌ Doc forall b c a. (b -> c) -> (a -> b) -> a -> c β Doc -> Doc ppBdrFmt (Doc -> πΌ Doc) -> (π -> Doc) -> π -> πΌ Doc forall b c a. (b -> c) -> (a -> b) -> a -> c β π -> Doc forall a. Pretty a => a -> Doc pretty) π π xO , Doc -> πΌ Doc forall a. a -> πΌ a singleπΌ (Doc -> πΌ Doc) -> Doc -> πΌ Doc forall a b. (a -> b) -> a -> b $ π -> Doc ppKey π "β" ] App_ULC ULCExp πΈ eβ ULCExp πΈ eβ β β64 -> Doc -> Doc -> Doc -> Doc ppInfl β64 pAPP (β64 -> Doc ppSpace β64 forall a. One a => a one) (ULCExp πΈ -> Doc forall a. Pretty a => a -> Doc pretty ULCExp πΈ eβ) (Doc -> Doc) -> Doc -> Doc forall a b. (a -> b) -> a -> b $ ULCExp πΈ -> Doc forall a. Pretty a => a -> Doc pretty ULCExp πΈ eβ deriving instance (TH.Lift πΈ) β TH.Lift (ULCExp πΈ) deriving instance (TH.Lift πΈ) β TH.Lift (ULCExp_R πΈ) ulc β· TH.QuasiQuoter ulc :: QuasiQuoter ulc = (String -> Q Exp) -> (String -> Q Pat) -> (String -> Q Type) -> (String -> Q [Dec]) -> QuasiQuoter TH.QuasiQuoter String -> Q Exp qe String -> Q Pat forall {b} {a}. b -> Q a qp String -> Q Type forall {b} {a}. b -> Q a qt String -> Q [Dec] forall {b} {a}. b -> Q a qd where qe :: String -> Q Exp qe String s = do let sourceName :: π sourceName = π "" π (ParserToken TokenBasic) ts β IO (π (ParserToken TokenBasic)) -> Q (π (ParserToken TokenBasic)) forall a. IO a -> Q a forall (m :: * -> *) a. MonadIO m => IO a -> m a io (IO (π (ParserToken TokenBasic)) -> Q (π (ParserToken TokenBasic))) -> IO (π (ParserToken TokenBasic)) -> Q (π (ParserToken TokenBasic)) forall a b. (a -> b) -> a -> b $ Lexer CharClass β TokenClassBasic β64 TokenBasic -> π -> π (ParserToken β) -> IO (π (ParserToken TokenBasic)) forall c t o u w. (Show u, Ord c, Ord t, Pretty t, Classified c t, Eq o, Eq u, Plus u) => Lexer c t o u w -> π -> π (ParserToken t) -> IO (π (ParserToken w)) tokenizeIO Lexer CharClass β TokenClassBasic β64 TokenBasic lexULCExp π sourceName (π (ParserToken β) -> IO (π (ParserToken TokenBasic))) -> π (ParserToken β) -> IO (π (ParserToken TokenBasic)) forall a b. (a -> b) -> a -> b $ π -> π (ParserToken β) tokens (π -> π (ParserToken β)) -> π -> π (ParserToken β) forall a b. (a -> b) -> a -> b $ String -> π frhsChars String s let eC :: Doc β¨ ULCExpSrc eC = CParser TokenBasic ULCExpSrc -> π -> π (ParserToken TokenBasic) -> Doc β¨ ULCExpSrc forall a t ts. (Pretty a, ToIter (ParserToken t) ts, Ord t) => CParser t a -> π -> ts -> Doc β¨ a parse CParser TokenBasic ULCExpSrc pULCExp π sourceName π (ParserToken TokenBasic) ts case Doc β¨ ULCExpSrc eC of Inl Doc r β do String -> Q () TH.reportError (String -> Q ()) -> String -> Q () forall a b. (a -> b) -> a -> b $ π -> String tohsChars (π -> String) -> π -> String forall a b. (a -> b) -> a -> b $ Doc -> π ppRenderNoFmt Doc r String -> Q Exp forall a. String -> Q a forall (m :: * -> *) a. MonadFail m => String -> m a HS.fail String "Parse Failure" Inr ULCExpSrc e β [| e |] qp :: b -> Q a qp = Q a -> b -> Q a forall a b. a -> b -> a const (Q a -> b -> Q a) -> Q a -> b -> Q a forall a b. (a -> b) -> a -> b $ String -> Q a forall a. String -> Q a forall (m :: * -> *) a. MonadFail m => String -> m a HS.fail String "quoting patterns not supported" qt :: b -> Q a qt = Q a -> b -> Q a forall a b. a -> b -> a const (Q a -> b -> Q a) -> Q a -> b -> Q a forall a b. (a -> b) -> a -> b $ String -> Q a forall a. String -> Q a forall (m :: * -> *) a. MonadFail m => String -> m a HS.fail String "quoting types not supported" qd :: b -> Q a qd = Q a -> b -> Q a forall a b. a -> b -> a const (Q a -> b -> Q a) -> Q a -> b -> Q a forall a b. (a -> b) -> a -> b $ String -> Q a forall a. String -> Q a forall (m :: * -> *) a. MonadFail m => String -> m a HS.fail String "quoting declarations not supported" instance Fuzzy ULCExpRaw where fuzzy :: FuzzyM ULCExpRaw fuzzy = do β64 d β (FuzzyEnv β’ β64) -> FuzzyM β64 forall r'. (FuzzyEnv β’ r') -> FuzzyM r' forall r (m :: * -> *) r'. MonadReader r m => (r β’ r') -> m r' askL FuzzyEnv β’ β64 fuzzyEnvDepthL π΄ () (ULCExp_R ()) -> ULCExpRaw forall πΈ. π΄ πΈ (ULCExp_R πΈ) -> ULCExp πΈ ULCExp (π΄ () (ULCExp_R ()) -> ULCExpRaw) -> (ULCExp_R () -> π΄ () (ULCExp_R ())) -> ULCExp_R () -> ULCExpRaw forall b c a. (b -> c) -> (a -> b) -> a -> c β () -> ULCExp_R () -> π΄ () (ULCExp_R ()) forall e a. e -> a -> π΄ e a π΄ () (ULCExp_R () -> ULCExpRaw) -> FuzzyM (ULCExp_R ()) -> FuzzyM ULCExpRaw forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b ^$ [β64 β§ (() -> FuzzyM (ULCExp_R ()))] -> FuzzyM (ULCExp_R ()) forall t (m :: * -> *) a. (Monad m, MonadRand m, ToIter (β64 β§ (() -> m a)) t) => t -> m a wrchoose [ β64 -> (() -> FuzzyM (ULCExp_R ())) -> β64 β§ (() -> FuzzyM (ULCExp_R ())) forall a b. a -> b -> a β§ b (:*) β64 forall a. One a => a one ((() -> FuzzyM (ULCExp_R ())) -> β64 β§ (() -> FuzzyM (ULCExp_R ()))) -> (() -> FuzzyM (ULCExp_R ())) -> β64 β§ (() -> FuzzyM (ULCExp_R ())) forall a b. (a -> b) -> a -> b $ \ () β π -> ULCExp_R () forall πΈ. π -> ULCExp_R πΈ Var_ULC (π -> ULCExp_R ()) -> FuzzyM π -> FuzzyM (ULCExp_R ()) forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b ^$ FuzzyM π forall a. Fuzzy a => FuzzyM a fuzzy , β64 -> (() -> FuzzyM (ULCExp_R ())) -> β64 β§ (() -> FuzzyM (ULCExp_R ())) forall a b. a -> b -> a β§ b (:*) β64 d ((() -> FuzzyM (ULCExp_R ())) -> β64 β§ (() -> FuzzyM (ULCExp_R ()))) -> (() -> FuzzyM (ULCExp_R ())) -> β64 β§ (() -> FuzzyM (ULCExp_R ())) forall a b. (a -> b) -> a -> b $ \ () β [() -> FuzzyM (ULCExp_R ())] -> FuzzyM (ULCExp_R ()) forall (m :: * -> *) a t. (Monad m, MonadRand m, ToIter (() -> m a) t) => t -> m a rchoose [ \ () β do π π xO β FuzzyM (π π) forall a. Fuzzy a => FuzzyM a fuzzy ULCExpRaw e β FuzzyM ULCExpRaw -> FuzzyM ULCExpRaw forall a. FuzzyM a -> FuzzyM a fuzzyRec FuzzyM ULCExpRaw forall a. Fuzzy a => FuzzyM a fuzzy ULCExp_R () -> FuzzyM (ULCExp_R ()) forall a. a -> FuzzyM a forall (m :: * -> *) a. Return m => a -> m a return (ULCExp_R () -> FuzzyM (ULCExp_R ())) -> ULCExp_R () -> FuzzyM (ULCExp_R ()) forall a b. (a -> b) -> a -> b $ π π -> ULCExpRaw -> ULCExp_R () forall πΈ. π π -> ULCExp πΈ -> ULCExp_R πΈ Lam_ULC π π xO ULCExpRaw e , \ () β do ULCExpRaw eβ β FuzzyM ULCExpRaw -> FuzzyM ULCExpRaw forall a. FuzzyM a -> FuzzyM a fuzzyRec FuzzyM ULCExpRaw forall a. Fuzzy a => FuzzyM a fuzzy ULCExpRaw eβ β FuzzyM ULCExpRaw -> FuzzyM ULCExpRaw forall a. FuzzyM a -> FuzzyM a fuzzyRec FuzzyM ULCExpRaw forall a. Fuzzy a => FuzzyM a fuzzy ULCExp_R () -> FuzzyM (ULCExp_R ()) forall a. a -> FuzzyM a forall (m :: * -> *) a. Return m => a -> m a return (ULCExp_R () -> FuzzyM (ULCExp_R ())) -> ULCExp_R () -> FuzzyM (ULCExp_R ()) forall a b. (a -> b) -> a -> b $ ULCExpRaw -> ULCExpRaw -> ULCExp_R () forall πΈ. ULCExp πΈ -> ULCExp πΈ -> ULCExp_R πΈ App_ULC ULCExpRaw eβ ULCExpRaw eβ ] ] instance Substy () (ULCExp πΈ) (ULCExp πΈ) where substy :: ULCExp πΈ -> SubstM () (ULCExp πΈ) (ULCExp πΈ) substy = (ULCExp πΈ -> π΄ πΈ (ULCExp_R πΈ)) -> (π΄ πΈ (ULCExp_R πΈ) -> SubstM () (ULCExp πΈ) (ULCExp πΈ)) -> ULCExp πΈ -> SubstM () (ULCExp πΈ) (ULCExp πΈ) forall a b c. (a -> b) -> (b -> c) -> a -> c pipe ULCExp πΈ -> π΄ πΈ (ULCExp_R πΈ) forall πΈ. ULCExp πΈ -> π΄ πΈ (ULCExp_R πΈ) unULCExp ((π΄ πΈ (ULCExp_R πΈ) -> SubstM () (ULCExp πΈ) (ULCExp πΈ)) -> ULCExp πΈ -> SubstM () (ULCExp πΈ) (ULCExp πΈ)) -> (π΄ πΈ (ULCExp_R πΈ) -> SubstM () (ULCExp πΈ) (ULCExp πΈ)) -> ULCExp πΈ -> SubstM () (ULCExp πΈ) (ULCExp πΈ) forall a b. (a -> b) -> a -> b $ \ (π΄ πΈ πΈ ULCExp_R πΈ eβ) β π΄ πΈ (ULCExp_R πΈ) -> ULCExp πΈ forall πΈ. π΄ πΈ (ULCExp_R πΈ) -> ULCExp πΈ ULCExp (π΄ πΈ (ULCExp_R πΈ) -> ULCExp πΈ) -> SubstM () (ULCExp πΈ) (π΄ πΈ (ULCExp_R πΈ)) -> SubstM () (ULCExp πΈ) (ULCExp πΈ) forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b ^$ case ULCExp_R πΈ eβ of Var_ULC π x β ULCExp πΈ -> π΄ πΈ (ULCExp_R πΈ) forall πΈ. ULCExp πΈ -> π΄ πΈ (ULCExp_R πΈ) unULCExp (ULCExp πΈ -> π΄ πΈ (ULCExp_R πΈ)) -> SubstM () (ULCExp πΈ) (ULCExp πΈ) -> SubstM () (ULCExp πΈ) (π΄ πΈ (ULCExp_R πΈ)) forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b ^$ () -> (π -> ULCExp πΈ) -> π -> SubstM () (ULCExp πΈ) (ULCExp πΈ) forall s e. (Ord s, Substy s e e) => s -> (π -> e) -> π -> SubstM s e e substyπ () (π΄ πΈ (ULCExp_R πΈ) -> ULCExp πΈ forall πΈ. π΄ πΈ (ULCExp_R πΈ) -> ULCExp πΈ ULCExp (π΄ πΈ (ULCExp_R πΈ) -> ULCExp πΈ) -> (ULCExp_R πΈ -> π΄ πΈ (ULCExp_R πΈ)) -> ULCExp_R πΈ -> ULCExp πΈ forall b c a. (b -> c) -> (a -> b) -> a -> c β πΈ -> ULCExp_R πΈ -> π΄ πΈ (ULCExp_R πΈ) forall e a. e -> a -> π΄ e a π΄ πΈ πΈ (ULCExp_R πΈ -> ULCExp πΈ) -> (π -> ULCExp_R πΈ) -> π -> ULCExp πΈ forall b c a. (b -> c) -> (a -> b) -> a -> c β π -> ULCExp_R πΈ forall πΈ. π -> ULCExp_R πΈ Var_ULC) π x Lam_ULC π π xO ULCExp πΈ e β SubstM () (ULCExp πΈ) (π΄ πΈ (ULCExp_R πΈ)) -> SubstM () (ULCExp πΈ) (π΄ πΈ (ULCExp_R πΈ)) forall (m :: * -> *) a. (Monad m, MonadUCont m) => m a -> m a ureset (SubstM () (ULCExp πΈ) (π΄ πΈ (ULCExp_R πΈ)) -> SubstM () (ULCExp πΈ) (π΄ πΈ (ULCExp_R πΈ))) -> SubstM () (ULCExp πΈ) (π΄ πΈ (ULCExp_R πΈ)) -> SubstM () (ULCExp πΈ) (π΄ πΈ (ULCExp_R πΈ)) forall a b. (a -> b) -> a -> b $ do case π π xO of π π None β () -> SubstM () (ULCExp πΈ) () forall s e. Ord s => s -> SubstM s e () substyDBdr () Some π x β () -> (π -> ULCExp πΈ) -> π -> SubstM () (ULCExp πΈ) () forall s e. (Ord s, Substy s e e) => s -> (π -> e) -> π -> SubstM s e () substyBdr () (π΄ πΈ (ULCExp_R πΈ) -> ULCExp πΈ forall πΈ. π΄ πΈ (ULCExp_R πΈ) -> ULCExp πΈ ULCExp (π΄ πΈ (ULCExp_R πΈ) -> ULCExp πΈ) -> (ULCExp_R πΈ -> π΄ πΈ (ULCExp_R πΈ)) -> ULCExp_R πΈ -> ULCExp πΈ forall b c a. (b -> c) -> (a -> b) -> a -> c β πΈ -> ULCExp_R πΈ -> π΄ πΈ (ULCExp_R πΈ) forall e a. e -> a -> π΄ e a π΄ πΈ πΈ (ULCExp_R πΈ -> ULCExp πΈ) -> (π -> ULCExp_R πΈ) -> π -> ULCExp πΈ forall b c a. (b -> c) -> (a -> b) -> a -> c β π -> ULCExp_R πΈ forall πΈ. π -> ULCExp_R πΈ Var_ULC) π x ULCExp πΈ e' β ULCExp πΈ -> SubstM () (ULCExp πΈ) (ULCExp πΈ) forall s e a. Substy s e a => a -> SubstM s e a substy ULCExp πΈ e π΄ πΈ (ULCExp_R πΈ) -> SubstM () (ULCExp πΈ) (π΄ πΈ (ULCExp_R πΈ)) forall a. a -> SubstM () (ULCExp πΈ) a forall (m :: * -> *) a. Return m => a -> m a return (π΄ πΈ (ULCExp_R πΈ) -> SubstM () (ULCExp πΈ) (π΄ πΈ (ULCExp_R πΈ))) -> π΄ πΈ (ULCExp_R πΈ) -> SubstM () (ULCExp πΈ) (π΄ πΈ (ULCExp_R πΈ)) forall a b. (a -> b) -> a -> b $ πΈ -> ULCExp_R πΈ -> π΄ πΈ (ULCExp_R πΈ) forall e a. e -> a -> π΄ e a π΄ πΈ πΈ (ULCExp_R πΈ -> π΄ πΈ (ULCExp_R πΈ)) -> ULCExp_R πΈ -> π΄ πΈ (ULCExp_R πΈ) forall a b. (a -> b) -> a -> b $ π π -> ULCExp πΈ -> ULCExp_R πΈ forall πΈ. π π -> ULCExp πΈ -> ULCExp_R πΈ Lam_ULC π π xO ULCExp πΈ e' App_ULC ULCExp πΈ eβ ULCExp πΈ eβ β do ULCExp πΈ eβ' β ULCExp πΈ -> SubstM () (ULCExp πΈ) (ULCExp πΈ) forall s e a. Substy s e a => a -> SubstM s e a substy ULCExp πΈ eβ ULCExp πΈ eβ' β ULCExp πΈ -> SubstM () (ULCExp πΈ) (ULCExp πΈ) forall s e a. Substy s e a => a -> SubstM s e a substy ULCExp πΈ eβ π΄ πΈ (ULCExp_R πΈ) -> SubstM () (ULCExp πΈ) (π΄ πΈ (ULCExp_R πΈ)) forall a. a -> SubstM () (ULCExp πΈ) a forall (m :: * -> *) a. Return m => a -> m a return (π΄ πΈ (ULCExp_R πΈ) -> SubstM () (ULCExp πΈ) (π΄ πΈ (ULCExp_R πΈ))) -> π΄ πΈ (ULCExp_R πΈ) -> SubstM () (ULCExp πΈ) (π΄ πΈ (ULCExp_R πΈ)) forall a b. (a -> b) -> a -> b $ πΈ -> ULCExp_R πΈ -> π΄ πΈ (ULCExp_R πΈ) forall e a. e -> a -> π΄ e a π΄ πΈ πΈ (ULCExp_R πΈ -> π΄ πΈ (ULCExp_R πΈ)) -> ULCExp_R πΈ -> π΄ πΈ (ULCExp_R πΈ) forall a b. (a -> b) -> a -> b $ ULCExp πΈ -> ULCExp πΈ -> ULCExp_R πΈ forall πΈ. ULCExp πΈ -> ULCExp πΈ -> ULCExp_R πΈ App_ULC ULCExp πΈ eβ' ULCExp πΈ eβ'