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β‚‚'