module UVMHS.Lang.ULC where

import UVMHS.Core

import UVMHS.Lib.Parser
import UVMHS.Lib.Pretty
import UVMHS.Lib.Annotated
import UVMHS.Lib.Substitution
import UVMHS.Lib.Rand
import UVMHS.Lib.Fuzzy
import UVMHS.Lib.Shrinky
import UVMHS.Lib.THLiftInstances ()

import qualified Language.Haskell.TH.Syntax as TH
import qualified Language.Haskell.TH.Quote  as TH

import GHC.Generics as HS
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,(forall x. ULCExp 𝒸 -> Rep (ULCExp 𝒸) x)
-> (forall x. Rep (ULCExp 𝒸) x -> ULCExp 𝒸) -> Generic (ULCExp 𝒸)
forall x. Rep (ULCExp 𝒸) x -> ULCExp 𝒸
forall x. ULCExp 𝒸 -> Rep (ULCExp 𝒸) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall 𝒸 x. Rep (ULCExp 𝒸) x -> ULCExp 𝒸
forall 𝒸 x. ULCExp 𝒸 -> Rep (ULCExp 𝒸) x
$cfrom :: forall 𝒸 x. ULCExp 𝒸 -> Rep (ULCExp 𝒸) x
from :: forall x. ULCExp 𝒸 -> Rep (ULCExp 𝒸) x
$cto :: forall 𝒸 x. Rep (ULCExp 𝒸) x -> ULCExp 𝒸
to :: forall x. Rep (ULCExp 𝒸) x -> ULCExp 𝒸
Generic,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)

onULCExp ∷ (𝐴 𝒸 (ULCExp_R 𝒸) → 𝐴 𝒸' (ULCExp_R 𝒸')) → ULCExp 𝒸 → ULCExp 𝒸'
onULCExp :: forall 𝒸 𝒸'.
(𝐴 𝒸 (ULCExp_R 𝒸) -> 𝐴 𝒸' (ULCExp_R 𝒸')) -> ULCExp 𝒸 -> ULCExp 𝒸'
onULCExp 𝐴 𝒸 (ULCExp_R 𝒸) -> 𝐴 𝒸' (ULCExp_R 𝒸')
f = 𝐴 𝒸' (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 𝒸')
f (𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp 𝒸')
-> (ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)) -> ULCExp 𝒸 -> ULCExp 𝒸'
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)
forall 𝒸. ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)
unULCExp

data ULCExp_R 𝒸 =
    Var_ULC (UVar () (ULCExp 𝒸))
  | Lam_ULC (𝑂 Name) (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,(forall x. ULCExp_R 𝒸 -> Rep (ULCExp_R 𝒸) x)
-> (forall x. Rep (ULCExp_R 𝒸) x -> ULCExp_R 𝒸)
-> Generic (ULCExp_R 𝒸)
forall x. Rep (ULCExp_R 𝒸) x -> ULCExp_R 𝒸
forall x. ULCExp_R 𝒸 -> Rep (ULCExp_R 𝒸) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall 𝒸 x. Rep (ULCExp_R 𝒸) x -> ULCExp_R 𝒸
forall 𝒸 x. ULCExp_R 𝒸 -> Rep (ULCExp_R 𝒸) x
$cfrom :: forall 𝒸 x. ULCExp_R 𝒸 -> Rep (ULCExp_R 𝒸) x
from :: forall x. ULCExp_R 𝒸 -> Rep (ULCExp_R 𝒸) x
$cto :: forall 𝒸 x. Rep (ULCExp_R 𝒸) x -> ULCExp_R 𝒸
to :: forall x. Rep (ULCExp_R 𝒸) x -> ULCExp_R 𝒸
HS.Generic,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)
makePrisms ''ULCExp_R

type ULCExpSrc = ULCExp (𝑃 SrcCxt)
type ULCExpRaw = ULCExp ()

wfULC ∷ ULCExp 𝒸 → 𝔹
wfULC :: forall 𝒸. ULCExp 𝒸 -> Bool
wfULC = (ULCExp 𝒸 -> ULCExp_R 𝒸)
-> (ULCExp_R 𝒸 -> Bool) -> ULCExp 𝒸 -> Bool
forall a b c. (a -> b) -> (b -> c) -> a -> c
pipe (𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp_R 𝒸
forall e a. 𝐴 e a -> a
aval (𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp_R 𝒸)
-> (ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)) -> ULCExp 𝒸 -> ULCExp_R 𝒸
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)
forall 𝒸. ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)
unULCExp) ((ULCExp_R 𝒸 -> Bool) -> ULCExp 𝒸 -> Bool)
-> (ULCExp_R 𝒸 -> Bool) -> ULCExp 𝒸 -> Bool
forall a b. (a -> b) -> a -> b
$ \case
  Var_ULC UVar () (ULCExp 𝒸)
y → UVar () (ULCExp 𝒸) -> Bool
forall s e. Ord s => UVar s e -> Bool
wfUVar UVar () (ULCExp 𝒸)
y
  Lam_ULC 𝑂 Name
_wO ULCExp 𝒸
e → ULCExp 𝒸 -> Bool
forall 𝒸. ULCExp 𝒸 -> Bool
wfULC ULCExp 𝒸
e
  App_ULC ULCExp 𝒸
e₁ ULCExp 𝒸
e₂ → [Bool] -> Bool
forall t. ToIter Bool t => t -> Bool
and [ULCExp 𝒸 -> Bool
forall 𝒸. ULCExp 𝒸 -> Bool
wfULC ULCExp 𝒸
e₁,ULCExp 𝒸 -> Bool
forall 𝒸. ULCExp 𝒸 -> Bool
wfULC ULCExp 𝒸
e₂]

canonULC ∷ (Null 𝒸,Show 𝒸) ⇒ ULCExp 𝒸 → ULCExp 𝒸
canonULC :: forall 𝒸. (Null 𝒸, Show 𝒸) => ULCExp 𝒸 -> ULCExp 𝒸
canonULC = (𝐴 𝒸 (ULCExp_R 𝒸) -> 𝐴 𝒸 (ULCExp_R 𝒸)) -> ULCExp 𝒸 -> ULCExp 𝒸
forall 𝒸 𝒸'.
(𝐴 𝒸 (ULCExp_R 𝒸) -> 𝐴 𝒸' (ULCExp_R 𝒸')) -> ULCExp 𝒸 -> ULCExp 𝒸'
onULCExp ((𝐴 𝒸 (ULCExp_R 𝒸) -> 𝐴 𝒸 (ULCExp_R 𝒸)) -> ULCExp 𝒸 -> ULCExp 𝒸)
-> (𝐴 𝒸 (ULCExp_R 𝒸) -> 𝐴 𝒸 (ULCExp_R 𝒸)) -> ULCExp 𝒸 -> ULCExp 𝒸
forall a b. (a -> b) -> a -> b
$ (ULCExp_R 𝒸 -> ULCExp_R 𝒸) -> 𝐴 𝒸 (ULCExp_R 𝒸) -> 𝐴 𝒸 (ULCExp_R 𝒸)
forall a b e. (a -> b) -> 𝐴 e a -> 𝐴 e b
mapAVal ((ULCExp_R 𝒸 -> ULCExp_R 𝒸)
 -> 𝐴 𝒸 (ULCExp_R 𝒸) -> 𝐴 𝒸 (ULCExp_R 𝒸))
-> (ULCExp_R 𝒸 -> ULCExp_R 𝒸)
-> 𝐴 𝒸 (ULCExp_R 𝒸)
-> 𝐴 𝒸 (ULCExp_R 𝒸)
forall a b. (a -> b) -> a -> b
$ \case
  Var_ULC UVar () (ULCExp 𝒸)
x → UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸
forall 𝒸. UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸
Var_ULC (UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸)
-> UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸
forall a b. (a -> b) -> a -> b
$ (ULCExp 𝒸 -> ULCExp 𝒸) -> UVar () (ULCExp 𝒸) -> UVar () (ULCExp 𝒸)
forall s e.
(Ord s, Eq e, Substy s e e) =>
(e -> e) -> UVar s e -> UVar s e
canonUVar ULCExp 𝒸 -> ULCExp 𝒸
forall 𝒸. (Null 𝒸, Show 𝒸) => ULCExp 𝒸 -> ULCExp 𝒸
canonULC UVar () (ULCExp 𝒸)
x
  Lam_ULC 𝑂 Name
xO ULCExp 𝒸
e → 𝑂 Name -> ULCExp 𝒸 -> ULCExp_R 𝒸
forall 𝒸. 𝑂 Name -> ULCExp 𝒸 -> ULCExp_R 𝒸
Lam_ULC 𝑂 Name
xO (ULCExp 𝒸 -> ULCExp_R 𝒸) -> ULCExp 𝒸 -> ULCExp_R 𝒸
forall a b. (a -> b) -> a -> b
$ ULCExp 𝒸 -> ULCExp 𝒸
forall 𝒸. (Null 𝒸, Show 𝒸) => ULCExp 𝒸 -> ULCExp 𝒸
canonULC ULCExp 𝒸
e
  App_ULC ULCExp 𝒸
e₁ ULCExp 𝒸
e₂ → ULCExp 𝒸 -> ULCExp 𝒸 -> ULCExp_R 𝒸
forall 𝒸. ULCExp 𝒸 -> ULCExp 𝒸 -> ULCExp_R 𝒸
App_ULC (ULCExp 𝒸 -> ULCExp 𝒸
forall 𝒸. (Null 𝒸, Show 𝒸) => ULCExp 𝒸 -> ULCExp 𝒸
canonULC ULCExp 𝒸
e₁) (ULCExp 𝒸 -> ULCExp_R 𝒸) -> ULCExp 𝒸 -> ULCExp_R 𝒸
forall a b. (a -> b) -> a -> b
$ ULCExp 𝒸 -> ULCExp 𝒸
forall 𝒸. (Null 𝒸, Show 𝒸) => ULCExp 𝒸 -> ULCExp 𝒸
canonULC ULCExp 𝒸
e₂

syntaxULC ∷ LexerBasicSyntax
syntaxULC :: LexerBasicSyntax
syntaxULC = [LexerBasicSyntax] -> LexerBasicSyntax
forall a t. (Monoid a, ToIter a t) => t -> a
concat
  [ LexerBasicSyntax
syntaxUVar
  , LexerBasicSyntax
forall a. Null a => a
null { lexerBasicSyntaxPuns = pow ["(",")","->","→"] 
         , lexerBasicSyntaxKeys = pow ["lam","λ"]
         }
  ]

lexULCExp ∷ Lexer CharClass ℂ TokenClassBasic ℕ64 TokenBasic
lexULCExp :: Lexer CharClass ℂ TokenClassBasic ℕ64 TokenBasic
lexULCExp = LexerBasicSyntax
-> Lexer CharClass ℂ TokenClassBasic ℕ64 TokenBasic
lexerBasic LexerBasicSyntax
syntaxULC

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)
fmixfixWithContextSet 𝕊
"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
      UVar () ULCExpSrc
x ← (() -> CParser TokenBasic ULCExpSrc)
-> CParser TokenBasic (UVar () ULCExpSrc)
forall e.
(Eq e, Substy () e e) =>
(() -> CParser TokenBasic e) -> CParser TokenBasic (UVar () e)
pUVar ((() -> CParser TokenBasic ULCExpSrc)
 -> CParser TokenBasic (UVar () ULCExpSrc))
-> (() -> CParser TokenBasic ULCExpSrc)
-> CParser TokenBasic (UVar () ULCExpSrc)
forall a b. (a -> b) -> a -> b
$ \ () → CParser TokenBasic ULCExpSrc
pULCExp
      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
$ UVar () ULCExpSrc -> ULCExp_R (𝑃 SrcCxt)
forall 𝒸. UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸
Var_ULC UVar () ULCExpSrc
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",𝕊
"λ"]
      𝑂 Name
xO ← CParser TokenBasic Name -> CParser TokenBasic (𝑂 Name)
forall t a. Ord t => CParser t a -> CParser t (𝑂 a)
cpOptional (CParser TokenBasic Name -> CParser TokenBasic (𝑂 Name))
-> CParser TokenBasic Name -> CParser TokenBasic (𝑂 Name)
forall a b. (a -> b) -> a -> b
$ CParser TokenBasic Name
pName
      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 → 𝑂 Name -> ULCExpSrc -> ULCExp_R (𝑃 SrcCxt)
forall 𝒸. 𝑂 Name -> ULCExp 𝒸 -> ULCExp_R 𝒸
Lam_ULC 𝑂 Name
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 (Show 𝒸) ⇒ 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 (Show 𝒸) ⇒ Pretty (ULCExp_R 𝒸) where
  pretty :: ULCExp_R 𝒸 -> Doc
pretty = \case
    Var_ULC UVar () (ULCExp 𝒸)
x → UVar () (ULCExp 𝒸) -> Doc
forall a. Pretty a => a -> Doc
pretty UVar () (ULCExp 𝒸)
x
    Lam_ULC 𝑂 Name
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) -> (Name -> 𝐼 Doc) -> 𝑂 Name -> 𝐼 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) -> (Name -> Doc) -> Name -> 𝐼 Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Name -> Doc
forall a. Pretty a => a -> Doc
pretty) 𝑂 Name
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₂

instance Shrinky (ULCExp 𝒸) where
  shrink :: ULCExp 𝒸 -> 𝐼 (ULCExp 𝒸)
shrink (ULCExp (𝐴 𝒸
𝒸 ULCExp_R 𝒸
e)) = 𝐴 𝒸 (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 (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ ULCExp_R 𝒸 -> 𝐼 (ULCExp_R 𝒸)
forall a. Shrinky a => a -> 𝐼 a
shrink ULCExp_R 𝒸
e
instance Shrinky (ULCExp_R 𝒸) where
  shrink :: ULCExp_R 𝒸 -> 𝐼 (ULCExp_R 𝒸)
shrink = \case
    Var_ULC UVar () (ULCExp 𝒸)
x → UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸
forall 𝒸. UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸
Var_ULC (UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸)
-> 𝐼 (UVar () (ULCExp 𝒸)) -> 𝐼 (ULCExp_R 𝒸)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ UVar () (ULCExp 𝒸) -> 𝐼 (UVar () (ULCExp 𝒸))
forall a. Shrinky a => a -> 𝐼 a
shrink UVar () (ULCExp 𝒸)
x
    Lam_ULC 𝑂 Name
xO ULCExp 𝒸
e → [𝐼 (ULCExp_R 𝒸)] -> 𝐼 (ULCExp_R 𝒸)
forall a t. (Monoid a, ToIter a t) => t -> a
concat
      [ ULCExp_R 𝒸 -> 𝐼 (ULCExp_R 𝒸)
forall a t. Single a t => a -> t
single (ULCExp_R 𝒸 -> 𝐼 (ULCExp_R 𝒸)) -> ULCExp_R 𝒸 -> 𝐼 (ULCExp_R 𝒸)
forall a b. (a -> b) -> a -> b
$ 𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp_R 𝒸
forall e a. 𝐴 e a -> a
aval (𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp_R 𝒸) -> 𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp_R 𝒸
forall a b. (a -> b) -> a -> b
$ ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)
forall 𝒸. ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)
unULCExp ULCExp 𝒸
e
      , do (𝑂 Name
xO',ULCExp 𝒸
e') ← (𝑂 Name, ULCExp 𝒸) -> 𝐼 (𝑂 Name, ULCExp 𝒸)
forall a. Shrinky a => a -> 𝐼 a
shrink (𝑂 Name
xO,ULCExp 𝒸
e) ; ULCExp_R 𝒸 -> 𝐼 (ULCExp_R 𝒸)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (ULCExp_R 𝒸 -> 𝐼 (ULCExp_R 𝒸)) -> ULCExp_R 𝒸 -> 𝐼 (ULCExp_R 𝒸)
forall a b. (a -> b) -> a -> b
$ 𝑂 Name -> ULCExp 𝒸 -> ULCExp_R 𝒸
forall 𝒸. 𝑂 Name -> ULCExp 𝒸 -> ULCExp_R 𝒸
Lam_ULC 𝑂 Name
xO' ULCExp 𝒸
e'
      ]
    App_ULC ULCExp 𝒸
e₁ ULCExp 𝒸
e₂ → [𝐼 (ULCExp_R 𝒸)] -> 𝐼 (ULCExp_R 𝒸)
forall a t. (Monoid a, ToIter a t) => t -> a
concat
      [ ULCExp_R 𝒸 -> 𝐼 (ULCExp_R 𝒸)
forall a t. Single a t => a -> t
single (ULCExp_R 𝒸 -> 𝐼 (ULCExp_R 𝒸)) -> ULCExp_R 𝒸 -> 𝐼 (ULCExp_R 𝒸)
forall a b. (a -> b) -> a -> b
$ 𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp_R 𝒸
forall e a. 𝐴 e a -> a
aval (𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp_R 𝒸) -> 𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp_R 𝒸
forall a b. (a -> b) -> a -> b
$ ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)
forall 𝒸. ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)
unULCExp ULCExp 𝒸
e₁
      , ULCExp_R 𝒸 -> 𝐼 (ULCExp_R 𝒸)
forall a t. Single a t => a -> t
single (ULCExp_R 𝒸 -> 𝐼 (ULCExp_R 𝒸)) -> ULCExp_R 𝒸 -> 𝐼 (ULCExp_R 𝒸)
forall a b. (a -> b) -> a -> b
$ 𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp_R 𝒸
forall e a. 𝐴 e a -> a
aval (𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp_R 𝒸) -> 𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp_R 𝒸
forall a b. (a -> b) -> a -> b
$ ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)
forall 𝒸. ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)
unULCExp ULCExp 𝒸
e₂
      , do (ULCExp 𝒸
e₁',ULCExp 𝒸
e₂') ← (ULCExp 𝒸, ULCExp 𝒸) -> 𝐼 (ULCExp 𝒸, ULCExp 𝒸)
forall a. Shrinky a => a -> 𝐼 a
shrink (ULCExp 𝒸
e₁,ULCExp 𝒸
e₂) ; ULCExp_R 𝒸 -> 𝐼 (ULCExp_R 𝒸)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (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₂'
      ]

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
      Loc
l ← Q Loc
TH.location
      let lS :: 𝕊
lS = [𝕊] -> 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat [String -> 𝕊
frhsChars (String -> 𝕊) -> String -> 𝕊
forall a b. (a -> b) -> a -> b
$ Loc -> String
TH.loc_module Loc
l,𝕊
":",ℤ64 -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 (ℤ64 -> 𝕊) -> ℤ64 -> 𝕊
forall a b. (a -> b) -> a -> b
$ (ℤ64 ∧ ℤ64) -> ℤ64
forall a b. (a ∧ b) -> a
fst ((ℤ64 ∧ ℤ64) -> ℤ64) -> (ℤ64 ∧ ℤ64) -> ℤ64
forall a b. (a -> b) -> a -> b
$ CharPos -> ℤ64 ∧ ℤ64
forall a b. CHS a b => b -> a
frhs (CharPos -> ℤ64 ∧ ℤ64) -> CharPos -> ℤ64 ∧ ℤ64
forall a b. (a -> b) -> a -> b
$ Loc -> CharPos
TH.loc_start Loc
l]
      𝕍 (ParserToken TokenBasic)
ts ← case Lexer CharClass ℂ TokenClassBasic ℕ64 TokenBasic
-> 𝕊 -> 𝕍 (ParserToken ℂ) -> Doc ∨ 𝕍 (PreParserToken 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) -> Doc ∨ 𝕍 (PreParserToken w)
tokenize Lexer CharClass ℂ TokenClassBasic ℕ64 TokenBasic
lexULCExp 𝕊
lS (𝕍 (ParserToken ℂ) -> Doc ∨ 𝕍 (PreParserToken TokenBasic))
-> 𝕍 (ParserToken ℂ) -> Doc ∨ 𝕍 (PreParserToken TokenBasic)
forall a b. (a -> b) -> a -> b
$ 𝕊 -> 𝕍 (ParserToken ℂ)
tokens (𝕊 -> 𝕍 (ParserToken ℂ)) -> 𝕊 -> 𝕍 (ParserToken ℂ)
forall a b. (a -> b) -> a -> b
$ String -> 𝕊
frhsChars String
s of
        Inl Doc
r → do
          -- [hack] call to `replaced𝕊` required to make the whole error show
          -- up when using ghcid
          String -> Q (𝕍 (ParserToken TokenBasic))
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
HS.fail (String -> Q (𝕍 (ParserToken TokenBasic)))
-> String -> Q (𝕍 (ParserToken TokenBasic))
forall a b. (a -> b) -> a -> b
$ 𝕊 -> String
tohsChars (𝕊 -> String) -> 𝕊 -> String
forall a b. (a -> b) -> a -> b
$ 𝕊 -> 𝕊 -> 𝕊 -> 𝕊
replace𝕊 𝕊
"\n" 𝕊
"\n        " (𝕊 -> 𝕊) -> 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ Doc -> 𝕊
ppRender (Doc -> 𝕊) -> Doc -> 𝕊
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall t. ToIter Doc t => t -> Doc
ppVertical
            [ 𝕊 -> Doc
ppHeader 𝕊
"[Lexing Failure]"
            , Doc
r
            ]
        Inr 𝕍 (PreParserToken TokenBasic)
xs → 𝕍 (ParserToken TokenBasic) -> Q (𝕍 (ParserToken TokenBasic))
forall a. a -> Q a
forall (m :: * -> *) a. Return m => a -> m a
return (𝕍 (ParserToken TokenBasic) -> Q (𝕍 (ParserToken TokenBasic)))
-> 𝕍 (ParserToken TokenBasic) -> Q (𝕍 (ParserToken TokenBasic))
forall a b. (a -> b) -> a -> b
$ 𝕍 (PreParserToken TokenBasic) -> 𝕍 (ParserToken TokenBasic)
forall t. 𝕍 (PreParserToken t) -> 𝕍 (ParserToken t)
finalizeTokens 𝕍 (PreParserToken TokenBasic)
xs
      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 𝕊
lS 𝕍 (ParserToken TokenBasic)
ts
      case Doc ∨ ULCExpSrc
eC of
        Inl Doc
r → do
          -- [hack] call to `replace𝕊` is required to make the whole error show
          -- up when using ghcid
          String -> Q Exp
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
HS.fail (String -> Q Exp) -> String -> Q Exp
forall a b. (a -> b) -> a -> b
$ 𝕊 -> String
tohsChars (𝕊 -> String) -> 𝕊 -> String
forall a b. (a -> b) -> a -> b
$ 𝕊 -> 𝕊 -> 𝕊 -> 𝕊
replace𝕊 𝕊
"\n" 𝕊
"\n        " (𝕊 -> 𝕊) -> 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ Doc -> 𝕊
ppRender (Doc -> 𝕊) -> Doc -> 𝕊
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall t. ToIter Doc t => t -> Doc
ppVertical
            [ 𝕊 -> Doc
ppHeader 𝕊
"[Parsing Failure]"
            , Doc
r
            ]
        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
$ \ () → UVar () ULCExpRaw -> ULCExp_R ()
forall 𝒸. UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸
Var_ULC (UVar () ULCExpRaw -> ULCExp_R ())
-> FuzzyM (UVar () ULCExpRaw) -> FuzzyM (ULCExp_R ())
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM (UVar () ULCExpRaw)
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
                𝑂 Name
xO ← FuzzyM (𝑂 Name)
forall a. Fuzzy a => FuzzyM a
fuzzy
                ULCExpRaw
e ← FuzzyM ULCExpRaw
forall a. Fuzzy a => FuzzyM a
fuzzyRec
                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
$ 𝑂 Name -> ULCExpRaw -> ULCExp_R ()
forall 𝒸. 𝑂 Name -> ULCExp 𝒸 -> ULCExp_R 𝒸
Lam_ULC 𝑂 Name
xO ULCExpRaw
e

          , \ () → do
              ULCExpRaw
e₁ ← FuzzyM ULCExpRaw
forall a. Fuzzy a => FuzzyM a
fuzzyRec
              ULCExpRaw
e₂ ← FuzzyM ULCExpRaw
forall a. Fuzzy a => FuzzyM a
fuzzyRec
              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 (Null 𝒸) ⇒ SVarView () (ULCExp 𝒸) where
  svarL :: () -> ULCExp 𝒸 ⌲ SVar
svarL () = 
    let ctor ∷ SVar → ULCExp 𝒸
        ctor :: SVar -> ULCExp 𝒸
ctor = 𝐴 𝒸 (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
𝐴 𝒸
forall a. Null a => a
null (ULCExp_R 𝒸 -> ULCExp 𝒸)
-> (UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸)
-> UVar () (ULCExp 𝒸)
-> ULCExp 𝒸
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸
forall 𝒸. UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸
Var_ULC (UVar () (ULCExp 𝒸) -> ULCExp 𝒸)
-> (SVar -> UVar () (ULCExp 𝒸)) -> SVar -> ULCExp 𝒸
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (UVar () (ULCExp 𝒸) ⌲ SVar) -> SVar -> UVar () (ULCExp 𝒸)
forall a b. (a ⌲ b) -> b -> a
construct UVar () (ULCExp 𝒸) ⌲ SVar
forall s e. UVar s e ⌲ SVar
svar_UVarL
        dtor ∷ ULCExp 𝒸 → 𝑂 SVar
        dtor :: ULCExp 𝒸 -> 𝑂 SVar
dtor ULCExp 𝒸
e = (ULCExp_R 𝒸 ⌲ SVar) -> ULCExp_R 𝒸 -> 𝑂 SVar
forall a b. (a ⌲ b) -> a -> 𝑂 b
view (UVar () (ULCExp 𝒸) ⌲ SVar
forall s e. UVar s e ⌲ SVar
svar_UVarL (UVar () (ULCExp 𝒸) ⌲ SVar)
-> (ULCExp_R 𝒸 ⌲ UVar () (ULCExp 𝒸)) -> ULCExp_R 𝒸 ⌲ SVar
forall b c a. (b ⌲ c) -> (a ⌲ b) -> a ⌲ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ ULCExp_R 𝒸 ⌲ UVar () (ULCExp 𝒸)
forall 𝒸. ULCExp_R 𝒸 ⌲ UVar () (ULCExp 𝒸)
var_ULCL) (ULCExp_R 𝒸 -> 𝑂 SVar) -> ULCExp_R 𝒸 -> 𝑂 SVar
forall a b. (a -> b) -> a -> b
$ 𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp_R 𝒸
forall e a. 𝐴 e a -> a
aval (𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp_R 𝒸) -> 𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp_R 𝒸
forall a b. (a -> b) -> a -> b
$ ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)
forall 𝒸. ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)
unULCExp ULCExp 𝒸
e
    in (SVar -> ULCExp 𝒸) -> (ULCExp 𝒸 -> 𝑂 SVar) -> ULCExp 𝒸 ⌲ SVar
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism SVar -> ULCExp 𝒸
ctor ULCExp 𝒸 -> 𝑂 SVar
dtor

instance (Null 𝒸,Show 𝒸) ⇒ Substy () (ULCExp 𝒸) (ULCExp 𝒸) where
  substy :: ULCExp 𝒸 -> SubstyM () (ULCExp 𝒸) (ULCExp 𝒸)
substy = (ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸))
-> (𝐴 𝒸 (ULCExp_R 𝒸) -> SubstyM () (ULCExp 𝒸) (ULCExp 𝒸))
-> ULCExp 𝒸
-> SubstyM () (ULCExp 𝒸) (ULCExp 𝒸)
forall a b c. (a -> b) -> (b -> c) -> a -> c
pipe ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)
forall 𝒸. ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)
unULCExp ((𝐴 𝒸 (ULCExp_R 𝒸) -> SubstyM () (ULCExp 𝒸) (ULCExp 𝒸))
 -> ULCExp 𝒸 -> SubstyM () (ULCExp 𝒸) (ULCExp 𝒸))
-> (𝐴 𝒸 (ULCExp_R 𝒸) -> SubstyM () (ULCExp 𝒸) (ULCExp 𝒸))
-> ULCExp 𝒸
-> SubstyM () (ULCExp 𝒸) (ULCExp 𝒸)
forall a b. (a -> b) -> a -> b
$ \ (𝐴 𝒸
𝒸 ULCExp_R 𝒸
e₀) → 𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp 𝒸
forall 𝒸. 𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp 𝒸
ULCExp (𝐴 𝒸 (ULCExp_R 𝒸) -> ULCExp 𝒸)
-> SubstyM () (ULCExp 𝒸) (𝐴 𝒸 (ULCExp_R 𝒸))
-> SubstyM () (ULCExp 𝒸) (ULCExp 𝒸)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ case ULCExp_R 𝒸
e₀ of
    Var_ULC UVar () (ULCExp 𝒸)
x → ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)
forall 𝒸. ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸)
unULCExp (ULCExp 𝒸 -> 𝐴 𝒸 (ULCExp_R 𝒸))
-> SubstyM () (ULCExp 𝒸) (ULCExp 𝒸)
-> SubstyM () (ULCExp 𝒸) (𝐴 𝒸 (ULCExp_R 𝒸))
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (UVar () (ULCExp 𝒸) -> ULCExp 𝒸)
-> () -> UVar () (ULCExp 𝒸) -> SubstyM () (ULCExp 𝒸) (ULCExp 𝒸)
forall s e.
(Ord s, Ord e, Pretty e, Pretty s, Substy s e e) =>
(UVar s e -> e) -> s -> UVar s e -> SubstyM s e e
substyUVar (𝐴 𝒸 (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 𝒸)
-> (UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸)
-> UVar () (ULCExp 𝒸)
-> ULCExp 𝒸
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸
forall 𝒸. UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸
Var_ULC) () UVar () (ULCExp 𝒸)
x
    Lam_ULC 𝑂 Name
xO ULCExp 𝒸
e → SubstyM () (ULCExp 𝒸) (𝐴 𝒸 (ULCExp_R 𝒸))
-> SubstyM () (ULCExp 𝒸) (𝐴 𝒸 (ULCExp_R 𝒸))
forall (m :: * -> *) a. (Monad m, MonadUCont m) => m a -> m a
ureset (SubstyM () (ULCExp 𝒸) (𝐴 𝒸 (ULCExp_R 𝒸))
 -> SubstyM () (ULCExp 𝒸) (𝐴 𝒸 (ULCExp_R 𝒸)))
-> SubstyM () (ULCExp 𝒸) (𝐴 𝒸 (ULCExp_R 𝒸))
-> SubstyM () (ULCExp 𝒸) (𝐴 𝒸 (ULCExp_R 𝒸))
forall a b. (a -> b) -> a -> b
$ do
      case 𝑂 Name
xO of
        𝑂 Name
None → () -> SubstyM () (ULCExp 𝒸) ()
forall s e. (Ord s, Ord e) => s -> SubstyM s e ()
substyDBdr ()
        Some Name
x → () -> (SVar -> ULCExp 𝒸) -> Name -> SubstyM () (ULCExp 𝒸) ()
forall s e.
(Ord s, Ord e, Substy s e e) =>
s -> (SVar -> e) -> Name -> SubstyM 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 𝒸)
-> (UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸)
-> UVar () (ULCExp 𝒸)
-> ULCExp 𝒸
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸
forall 𝒸. UVar () (ULCExp 𝒸) -> ULCExp_R 𝒸
Var_ULC (UVar () (ULCExp 𝒸) -> ULCExp 𝒸)
-> (SVar -> UVar () (ULCExp 𝒸)) -> SVar -> ULCExp 𝒸
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SVar -> UVar () (ULCExp 𝒸)
forall s e. SVar -> UVar s e
uvar_SVar) Name
x
      ULCExp 𝒸
e' ← ULCExp 𝒸 -> SubstyM () (ULCExp 𝒸) (ULCExp 𝒸)
forall s e a. Substy s e a => a -> SubstyM s e a
substy ULCExp 𝒸
e
      𝐴 𝒸 (ULCExp_R 𝒸) -> SubstyM () (ULCExp 𝒸) (𝐴 𝒸 (ULCExp_R 𝒸))
forall a. a -> SubstyM () (ULCExp 𝒸) a
forall (m :: * -> *) a. Return m => a -> m a
return (𝐴 𝒸 (ULCExp_R 𝒸) -> SubstyM () (ULCExp 𝒸) (𝐴 𝒸 (ULCExp_R 𝒸)))
-> 𝐴 𝒸 (ULCExp_R 𝒸) -> SubstyM () (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
$ 𝑂 Name -> ULCExp 𝒸 -> ULCExp_R 𝒸
forall 𝒸. 𝑂 Name -> ULCExp 𝒸 -> ULCExp_R 𝒸
Lam_ULC 𝑂 Name
xO ULCExp 𝒸
e'
    App_ULC ULCExp 𝒸
e₁ ULCExp 𝒸
e₂ → do
      ULCExp 𝒸
e₁' ← ULCExp 𝒸 -> SubstyM () (ULCExp 𝒸) (ULCExp 𝒸)
forall s e a. Substy s e a => a -> SubstyM s e a
substy ULCExp 𝒸
e₁
      ULCExp 𝒸
e₂' ← ULCExp 𝒸 -> SubstyM () (ULCExp 𝒸) (ULCExp 𝒸)
forall s e a. Substy s e a => a -> SubstyM s e a
substy ULCExp 𝒸
e₂
      𝐴 𝒸 (ULCExp_R 𝒸) -> SubstyM () (ULCExp 𝒸) (𝐴 𝒸 (ULCExp_R 𝒸))
forall a. a -> SubstyM () (ULCExp 𝒸) a
forall (m :: * -> *) a. Return m => a -> m a
return (𝐴 𝒸 (ULCExp_R 𝒸) -> SubstyM () (ULCExp 𝒸) (𝐴 𝒸 (ULCExp_R 𝒸)))
-> 𝐴 𝒸 (ULCExp_R 𝒸) -> SubstyM () (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₂'