module UVMHS.Core.TH where

import UVMHS.Core.Init
import UVMHS.Core.Classes
import UVMHS.Core.Data

import UVMHS.Core.Effects
import UVMHS.Core.Monads

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

import qualified Prelude as HS

type THLift = TH.Lift

class MonadQ (m ∷ ★ → ★) where qio ∷ TH.Q a → m a

instance Functor TH.Q where map :: forall a b. (a -> b) -> Q a -> Q b
map = (a -> b) -> Q a -> Q b
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
mmap
instance Return TH.Q where return :: forall a. a -> Q a
return = a -> Q a
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
HS.return
instance Bind TH.Q where ≫= :: forall a b. Q a -> (a -> Q b) -> Q b
(≫=) = Q a -> (a -> Q b) -> Q b
forall a b. Q a -> (a -> Q b) -> Q b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
(HS.>>=)
instance Monad TH.Q
instance MonadIO TH.Q where io :: forall a. IO a -> Q a
io = IO a -> Q a
forall a. IO a -> Q a
TH.runIO
instance MonadQ TH.Q where qio :: forall a. Q a -> Q a
qio = Q a -> Q a
forall a. a -> a
id

instance Apply TH.Exp where ⊙ :: Exp -> Exp -> Exp
(⊙) = Exp -> Exp -> Exp
TH.AppE

-- instance Tup TH.Exp where tup = TH.TupE ∘ lazyList
-- instance Tup TH.Pat where tup = TH.TupP ∘ lazyList
-- instance Tup TH.Type where tup ts = TH.TupleT (tohs $ intΩ64 $ count ts) ⊙⋆ ts

instance Tup TH.Exp where 
  tup :: forall t. ToIter Exp t => t -> Exp
tup t
es = case t -> 𝐿 Exp
forall a t. ToIter a t => t -> 𝐿 a
list t
es of
    𝐿 Exp
Nil → Name -> Exp
TH.ConE '()
    Exp
e :& 𝐿 Exp
es' → 𝐿 Exp -> Exp -> (Exp -> Exp -> Exp) -> Exp
forall a t b. ToIter a t => t -> b -> (a -> b -> b) -> b
foldOnFrom 𝐿 Exp
es' Exp
e ((Exp -> Exp -> Exp) -> Exp) -> (Exp -> Exp -> Exp) -> Exp
forall a b. (a -> b) -> a -> b
$ \ Exp
e' Exp
eᵢ → Name -> Exp
TH.ConE '(:*) Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ Exp
eᵢ Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ Exp
e'

instance Tup TH.Pat where 
  tup :: forall t. ToIter Pat t => t -> Pat
tup t
ps = case t -> 𝐿 Pat
forall a t. ToIter a t => t -> 𝐿 a
list t
ps of
    𝐿 Pat
Nil → Name -> [Kind] -> [Pat] -> Pat
TH.ConP '() [] []
    Pat
p :& 𝐿 Pat
ps' → 𝐿 Pat -> Pat -> (Pat -> Pat -> Pat) -> Pat
forall a t b. ToIter a t => t -> b -> (a -> b -> b) -> b
foldOnFrom 𝐿 Pat
ps' Pat
p ((Pat -> Pat -> Pat) -> Pat) -> (Pat -> Pat -> Pat) -> Pat
forall a b. (a -> b) -> a -> b
$ \ Pat
p' Pat
pᵢ → Name -> [Kind] -> [Pat] -> Pat
TH.ConP '(:*) [] [Pat
pᵢ,Pat
p']

instance Tup TH.Type where 
  tup :: forall t. ToIter Kind t => t -> Kind
tup t
ts = case t -> 𝐿 Kind
forall a t. ToIter a t => t -> 𝐿 a
list t
ts of
    𝐿 Kind
Nil → Name -> Kind
TH.ConT ''()
    Kind
t :& 𝐿 Kind
ts' → 𝐿 Kind -> Kind -> (Kind -> Kind -> Kind) -> Kind
forall a t b. ToIter a t => t -> b -> (a -> b -> b) -> b
foldOnFrom 𝐿 Kind
ts' Kind
t ((Kind -> Kind -> Kind) -> Kind) -> (Kind -> Kind -> Kind) -> Kind
forall a b. (a -> b) -> a -> b
$ \ Kind
t' Kind
tᵢ → Name -> Kind
TH.ConT ''(∧) Kind -> Kind -> Kind
forall a. Apply a => a -> a -> a
⊙ Kind
tᵢ Kind -> Kind -> Kind
forall a. Apply a => a -> a -> a
⊙ Kind
t'

instance Apply TH.Type where ⊙ :: Kind -> Kind -> Kind
(⊙) = Kind -> Kind -> Kind
TH.AppT
instance Arrow TH.Type where Kind
f ⇨ :: Kind -> Kind -> Kind
⇨ Kind
x = Kind
TH.ArrowT Kind -> Kind -> Kind
forall a. Apply a => a -> a -> a
⊙ Kind
f Kind -> Kind -> Kind
forall a. Apply a => a -> a -> a
⊙ Kind
x

thString ∷ 𝕊 → TH.Exp
thString :: 𝕊 -> Exp
thString = Lit -> Exp
TH.LitE (Lit -> Exp) -> (String -> Lit) -> String -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ String -> Lit
TH.StringL (String -> Exp) -> (𝕊 -> String) -> 𝕊 -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕊 -> String
forall a t. ToIter a t => t -> [a]
lazyList
      
thConNames ∷ TH.Con → 𝐿 TH.Name
thConNames :: Con -> 𝐿 Name
thConNames (TH.NormalC Name
n [BangType]
_) = Name -> 𝐿 Name
forall a t. Single a t => a -> t
single Name
n
thConNames (TH.RecC Name
n [VarStrictType]
_) = Name -> 𝐿 Name
forall a t. Single a t => a -> t
single Name
n
thConNames (TH.InfixC BangType
_ Name
n BangType
_) = Name -> 𝐿 Name
forall a t. Single a t => a -> t
single Name
n
thConNames (TH.ForallC [TyVarBndr Specificity]
_ [Kind]
_ Con
c) = Con -> 𝐿 Name
thConNames Con
c
thConNames (TH.GadtC ([Name] -> 𝐿 Name
forall a b. CHS a b => b -> a
frhs → 𝐿 Name
ns) [BangType]
_ Kind
_) = 𝐿 Name
ns
thConNames (TH.RecGadtC ([Name] -> 𝐿 Name
forall a b. CHS a b => b -> a
frhs → 𝐿 Name
ns) [VarStrictType]
_ Kind
_) = 𝐿 Name
ns

thTyVarBndrName ∷ TH.TyVarBndr a → TH.Name
thTyVarBndrName :: forall a. TyVarBndr a -> Name
thTyVarBndrName (TH.PlainTV Name
name a
_) = Name
name
thTyVarBndrName (TH.KindedTV Name
name a
_ Kind
_) = Name
name

thSingleClause ∷ 𝐿 TH.Pat → TH.Exp → TH.Clause
thSingleClause :: 𝐿 Pat -> Exp -> Clause
thSingleClause 𝐿 Pat
p Exp
b = [Pat] -> Body -> [Dec] -> Clause
TH.Clause (𝐿 Pat -> [Pat]
forall a b. CHS a b => a -> b
tohs 𝐿 Pat
p) (Exp -> Body
TH.NormalB Exp
b) []

thSingleMatch ∷ TH.Pat → TH.Exp → TH.Match
thSingleMatch :: Pat -> Exp -> Match
thSingleMatch Pat
p Exp
b = Pat -> Body -> [Dec] -> Match
TH.Match Pat
p (Exp -> Body
TH.NormalB Exp
b) []

thViewSimpleCon ∷ TH.Con → 𝑂 (TH.Name ∧ 𝐿 TH.Type)
thViewSimpleCon :: Con -> 𝑂 (Name ∧ 𝐿 Kind)
thViewSimpleCon (TH.NormalC Name
name ([BangType] -> 𝐿 (Bang ∧ Kind)
forall a b. CHS a b => b -> a
frhs → 𝐿 (Bang ∧ Kind)
strictTypes)) = (Name ∧ 𝐿 Kind) -> 𝑂 (Name ∧ 𝐿 Kind)
forall a. a -> 𝑂 a
Some (Name
name Name -> 𝐿 Kind -> Name ∧ 𝐿 Kind
forall a b. a -> b -> a ∧ b
:* ((Bang ∧ Kind) -> Kind) -> 𝐿 (Bang ∧ Kind) -> 𝐿 Kind
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (Bang ∧ Kind) -> Kind
forall a b. (a ∧ b) -> b
snd 𝐿 (Bang ∧ Kind)
strictTypes)
thViewSimpleCon (TH.RecC Name
name ([VarStrictType] -> 𝐿 ((Name ∧ Bang) ∧ Kind)
forall a b. CHS a b => b -> a
frhs → 𝐿 ((Name ∧ Bang) ∧ Kind)
varStrictTypes)) = (Name ∧ 𝐿 Kind) -> 𝑂 (Name ∧ 𝐿 Kind)
forall a. a -> 𝑂 a
Some (Name
name Name -> 𝐿 Kind -> Name ∧ 𝐿 Kind
forall a b. a -> b -> a ∧ b
:* (((Name ∧ Bang) ∧ Kind) -> Kind)
-> 𝐿 ((Name ∧ Bang) ∧ Kind) -> 𝐿 Kind
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((Name ∧ Bang) ∧ Kind) -> Kind
forall a b. (a ∧ b) -> b
snd 𝐿 ((Name ∧ Bang) ∧ Kind)
varStrictTypes)
thViewSimpleCon (TH.InfixC (Bang
_,Kind
typeL) Name
name (Bang
_,Kind
typeR)) = (Name ∧ 𝐿 Kind) -> 𝑂 (Name ∧ 𝐿 Kind)
forall a. a -> 𝑂 a
Some (Name
name Name -> 𝐿 Kind -> Name ∧ 𝐿 Kind
forall a b. a -> b -> a ∧ b
:* [Kind] -> 𝐿 Kind
forall a t. ToIter a t => t -> 𝐿 a
list [Kind
typeL,Kind
typeR])
thViewSimpleCon (TH.ForallC [TyVarBndr Specificity]
_ [Kind]
_ Con
_) = 𝑂 (Name ∧ 𝐿 Kind)
forall a. 𝑂 a
None
thViewSimpleCon (TH.GadtC [Name]
_ [BangType]
_ Kind
_) = 𝑂 (Name ∧ 𝐿 Kind)
forall a. 𝑂 a
None
thViewSimpleCon (TH.RecGadtC [Name]
_ [VarStrictType]
_ Kind
_) = 𝑂 (Name ∧ 𝐿 Kind)
forall a. 𝑂 a
None

thTyConIL ∷ TH.Info ⌲ TH.Dec
thTyConIL :: Info ⌲ Dec
thTyConIL = Prism
  { view :: Info -> 𝑂 Dec
view = \case
      TH.TyConI Dec
d → Dec -> 𝑂 Dec
forall a. a -> 𝑂 a
Some Dec
d
      Info
_ → 𝑂 Dec
forall a. 𝑂 a
None
  , construct :: Dec -> Info
construct = Dec -> Info
TH.TyConI
  }

thDataDL ∷ TH.Dec ⌲ TH.Cxt ∧ TH.Name ∧ 𝐿 (TH.TyVarBndr ()) ∧ 𝑂 TH.Kind ∧ 𝐿 TH.Con ∧ 𝐿 TH.DerivClause
thDataDL :: Dec
⌲ ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
   ∧ 𝐿 DerivClause)
thDataDL = Prism
  { view :: Dec
-> 𝑂 ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
view = \case
      TH.DataD [Kind]
cx Name
t ([TyVarBndr ()] -> 𝐿 (TyVarBndr ())
forall a b. CHS a b => b -> a
frhs → 𝐿 (TyVarBndr ())
args) (Maybe Kind -> 𝑂 Kind
forall a b. CHS a b => b -> a
frhs → 𝑂 Kind
kM) ([Con] -> 𝐿 Con
forall a b. CHS a b => b -> a
frhs → 𝐿 Con
cs) ([DerivClause] -> 𝐿 DerivClause
forall a b. CHS a b => b -> a
frhs → 𝐿 DerivClause
ders) → ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
 ∧ 𝐿 DerivClause)
-> 𝑂 ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
forall a. a -> 𝑂 a
Some ([Kind]
cx [Kind] -> Name -> [Kind] ∧ Name
forall a b. a -> b -> a ∧ b
:* Name
t ([Kind] ∧ Name)
-> 𝐿 (TyVarBndr ()) -> ([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())
forall a b. a -> b -> a ∧ b
:* 𝐿 (TyVarBndr ())
args (([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ()))
-> 𝑂 Kind -> (([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind
forall a b. a -> b -> a ∧ b
:* 𝑂 Kind
kM ((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind)
-> 𝐿 Con -> ((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con
forall a b. a -> b -> a ∧ b
:* 𝐿 Con
cs (((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
-> 𝐿 DerivClause
-> (((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
   ∧ 𝐿 DerivClause
forall a b. a -> b -> a ∧ b
:* 𝐿 DerivClause
ders)
      Dec
_ → 𝑂 ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
   ∧ 𝐿 DerivClause)
forall a. 𝑂 a
None
  , construct :: ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
 ∧ 𝐿 DerivClause)
-> Dec
construct = \ ([Kind]
cx :* Name
t :* 𝐿 (TyVarBndr ())
args :* 𝑂 Kind
kM :* 𝐿 Con
cs :* 𝐿 DerivClause
ders) → [Kind]
-> Name
-> [TyVarBndr ()]
-> Maybe Kind
-> [Con]
-> [DerivClause]
-> Dec
TH.DataD [Kind]
cx Name
t (𝐿 (TyVarBndr ()) -> [TyVarBndr ()]
forall a b. CHS a b => a -> b
tohs 𝐿 (TyVarBndr ())
args) (𝑂 Kind -> Maybe Kind
forall a b. CHS a b => a -> b
tohs 𝑂 Kind
kM) (𝐿 Con -> [Con]
forall a b. CHS a b => a -> b
tohs 𝐿 Con
cs) (𝐿 DerivClause -> [DerivClause]
forall a b. CHS a b => a -> b
tohs 𝐿 DerivClause
ders)
  }

thNewtypeDL ∷ TH.Dec ⌲ TH.Cxt ∧ TH.Name ∧ 𝐿 (TH.TyVarBndr ()) ∧ 𝑂 TH.Kind ∧ TH.Con ∧ 𝐿 TH.DerivClause
thNewtypeDL :: Dec
⌲ ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
   ∧ 𝐿 DerivClause)
thNewtypeDL = Prism
  { view :: Dec
-> 𝑂 ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
      ∧ 𝐿 DerivClause)
view = \case
      TH.NewtypeD [Kind]
cx Name
t ([TyVarBndr ()] -> 𝐿 (TyVarBndr ())
forall a b. CHS a b => b -> a
frhs → 𝐿 (TyVarBndr ())
args) (Maybe Kind -> 𝑂 Kind
forall a b. CHS a b => b -> a
frhs → 𝑂 Kind
kM) (Con -> Con
forall a b. CHS a b => b -> a
frhs → Con
c) ([DerivClause] -> 𝐿 DerivClause
forall a b. CHS a b => b -> a
frhs → 𝐿 DerivClause
ders) → ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
 ∧ 𝐿 DerivClause)
-> 𝑂 ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
      ∧ 𝐿 DerivClause)
forall a. a -> 𝑂 a
Some ([Kind]
cx [Kind] -> Name -> [Kind] ∧ Name
forall a b. a -> b -> a ∧ b
:* Name
t ([Kind] ∧ Name)
-> 𝐿 (TyVarBndr ()) -> ([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())
forall a b. a -> b -> a ∧ b
:* 𝐿 (TyVarBndr ())
args (([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ()))
-> 𝑂 Kind -> (([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind
forall a b. a -> b -> a ∧ b
:* 𝑂 Kind
kM ((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind)
-> Con -> ((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con
forall a b. a -> b -> a ∧ b
:* Con
c (((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
-> 𝐿 DerivClause
-> (((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
   ∧ 𝐿 DerivClause
forall a b. a -> b -> a ∧ b
:* 𝐿 DerivClause
ders)
      Dec
_ → 𝑂 ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
   ∧ 𝐿 DerivClause)
forall a. 𝑂 a
None
  , construct :: ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
 ∧ 𝐿 DerivClause)
-> Dec
construct = \ ([Kind]
cx :* Name
t :* 𝐿 (TyVarBndr ())
args :* 𝑂 Kind
kM :* Con
c :* 𝐿 DerivClause
ders) → [Kind]
-> Name
-> [TyVarBndr ()]
-> Maybe Kind
-> Con
-> [DerivClause]
-> Dec
TH.NewtypeD [Kind]
cx Name
t (𝐿 (TyVarBndr ()) -> [TyVarBndr ()]
forall a b. CHS a b => a -> b
tohs 𝐿 (TyVarBndr ())
args) (𝑂 Kind -> Maybe Kind
forall a b. CHS a b => a -> b
tohs 𝑂 Kind
kM) (Con -> Con
forall a b. CHS a b => a -> b
tohs Con
c) (𝐿 DerivClause -> [DerivClause]
forall a b. CHS a b => a -> b
tohs 𝐿 DerivClause
ders)
  }

thViewADT ∷ TH.Dec → 𝑂 (TH.Cxt ∧ TH.Name ∧ 𝐿 (TH.TyVarBndr ()) ∧ 𝑂 TH.Kind ∧ 𝐿 TH.Con ∧ 𝐿 TH.DerivClause)
thViewADT :: Dec
-> 𝑂 ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
thViewADT Dec
d =
  (Dec
 ⌲ ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
    ∧ 𝐿 DerivClause))
-> Dec
-> 𝑂 ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
forall a b. (a ⌲ b) -> a -> 𝑂 b
view Dec
⌲ ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
   ∧ 𝐿 DerivClause)
thDataDL Dec
d
  𝑂 ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
   ∧ 𝐿 DerivClause)
-> 𝑂 ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
-> 𝑂 ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
forall a. 𝑂 a -> 𝑂 a -> 𝑂 a
forall {k} (m :: k -> *) (a :: k). MonadFail m => m a -> m a -> m a
⎅
  (((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
 ∧ 𝐿 DerivClause)
-> (((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
   ∧ 𝐿 DerivClause
forall {b} {b} {a} {b} {b} {b} {b}.
Single b b =>
(((((a ∧ b) ∧ b) ∧ b) ∧ b) ∧ b) -> ((((a ∧ b) ∧ b) ∧ b) ∧ b) ∧ b
ff (((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
  ∧ 𝐿 DerivClause)
 -> (((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
    ∧ 𝐿 DerivClause)
-> (Dec
    -> 𝑂 ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
          ∧ 𝐿 DerivClause))
-> Dec
-> 𝑂 ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
forall (t :: * -> *) b c a.
Functor t =>
(b -> c) -> (a -> t b) -> a -> t c
^∘ (Dec
 ⌲ ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
    ∧ 𝐿 DerivClause))
-> Dec
-> 𝑂 ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
      ∧ 𝐿 DerivClause)
forall a b. (a ⌲ b) -> a -> 𝑂 b
view Dec
⌲ ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
   ∧ 𝐿 DerivClause)
thNewtypeDL) Dec
d
  where
    ff :: (((((a ∧ b) ∧ b) ∧ b) ∧ b) ∧ b) -> ((((a ∧ b) ∧ b) ∧ b) ∧ b) ∧ b
ff (a
cx :* b
t :* b
args :* b
kM :* b
c :* b
ders) = (a
cx a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* b
t (a ∧ b) -> b -> (a ∧ b) ∧ b
forall a b. a -> b -> a ∧ b
:* b
args ((a ∧ b) ∧ b) -> b -> ((a ∧ b) ∧ b) ∧ b
forall a b. a -> b -> a ∧ b
:* b
kM (((a ∧ b) ∧ b) ∧ b) -> b -> (((a ∧ b) ∧ b) ∧ b) ∧ b
forall a b. a -> b -> a ∧ b
:* b -> b
forall a t. Single a t => a -> t
single b
c ((((a ∧ b) ∧ b) ∧ b) ∧ b) -> b -> ((((a ∧ b) ∧ b) ∧ b) ∧ b) ∧ b
forall a b. a -> b -> a ∧ b
:* b
ders)

thViewSingleConADT ∷ TH.Dec → 𝑂 (TH.Cxt ∧ TH.Name ∧ 𝐿 (TH.TyVarBndr ()) ∧ 𝑂 TH.Kind ∧ TH.Con ∧ 𝐿 TH.DerivClause)
thViewSingleConADT :: Dec
-> 𝑂 ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
      ∧ 𝐿 DerivClause)
thViewSingleConADT Dec
dec = do
  ([Kind]
cx :* Name
t :* 𝐿 (TyVarBndr ())
args :* 𝑂 Kind
kM :* 𝐿 Con
cs :* 𝐿 DerivClause
ders) ← Dec
-> 𝑂 ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
thViewADT Dec
dec
  Con
c ← (𝐿 Con ⌲ Con) -> 𝐿 Con -> 𝑂 Con
forall a b. (a ⌲ b) -> a -> 𝑂 b
view 𝐿 Con ⌲ Con
forall a. 𝐿 a ⌲ a
singleL 𝐿 Con
cs
  ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
 ∧ 𝐿 DerivClause)
-> 𝑂 ((((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
      ∧ 𝐿 DerivClause)
forall a. a -> 𝑂 a
forall (m :: * -> *) a. Return m => a -> m a
return ([Kind]
cx [Kind] -> Name -> [Kind] ∧ Name
forall a b. a -> b -> a ∧ b
:* Name
t ([Kind] ∧ Name)
-> 𝐿 (TyVarBndr ()) -> ([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())
forall a b. a -> b -> a ∧ b
:* 𝐿 (TyVarBndr ())
args (([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ()))
-> 𝑂 Kind -> (([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind
forall a b. a -> b -> a ∧ b
:* 𝑂 Kind
kM ((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind)
-> Con -> ((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con
forall a b. a -> b -> a ∧ b
:* Con
c (((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
-> 𝐿 DerivClause
-> (((([Kind] ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Kind) ∧ Con)
   ∧ 𝐿 DerivClause
forall a b. a -> b -> a ∧ b
:* 𝐿 DerivClause
ders)

thRecCL ∷ TH.Con ⌲ TH.Name ∧ 𝐿 TH.VarStrictType
thRecCL :: Con ⌲ (Name ∧ 𝐿 VarStrictType)
thRecCL = Prism
  { view :: Con -> 𝑂 (Name ∧ 𝐿 VarStrictType)
view = \case
      TH.RecC Name
n ([VarStrictType] -> 𝐿 VarStrictType
forall a b. CHS a b => b -> a
frhs → 𝐿 VarStrictType
fs) → (Name ∧ 𝐿 VarStrictType) -> 𝑂 (Name ∧ 𝐿 VarStrictType)
forall a. a -> 𝑂 a
Some (Name
n Name -> 𝐿 VarStrictType -> Name ∧ 𝐿 VarStrictType
forall a b. a -> b -> a ∧ b
:* 𝐿 VarStrictType
fs)
      Con
_ → 𝑂 (Name ∧ 𝐿 VarStrictType)
forall a. 𝑂 a
None
  , construct :: (Name ∧ 𝐿 VarStrictType) -> Con
construct = \ (Name
n :* 𝐿 VarStrictType
fs) → Name -> [VarStrictType] -> Con
TH.RecC Name
n (𝐿 VarStrictType -> [VarStrictType]
forall a b. CHS a b => a -> b
tohs 𝐿 VarStrictType
fs)
  }

thLoc𝕊 ∷ TH.Q 𝕊
thLoc𝕊 :: Q 𝕊
thLoc𝕊 = do
  Loc
l ← Q Loc
TH.location
  𝕊 -> Q 𝕊
forall a. a -> Q a
forall (m :: * -> *) a. Return m => a -> m a
return (𝕊 -> Q 𝕊) -> 𝕊 -> Q 𝕊
forall a b. (a -> b) -> a -> b
$ [𝕊] -> 𝕊
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 
    , 𝕊
"@" 
    , CharPos -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 (CharPos -> 𝕊) -> CharPos -> 𝕊
forall a b. (a -> b) -> a -> b
$ Loc -> CharPos
TH.loc_start Loc
l 
    , 𝕊
":" 
    , CharPos -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 (CharPos -> 𝕊) -> CharPos -> 𝕊
forall a b. (a -> b) -> a -> b
$ Loc -> CharPos
TH.loc_end Loc
l
    ]

thLoc ∷ TH.Q (TH.TExp ((𝕊 → c) → c))
thLoc :: forall c. Q (TExp ((𝕊 -> c) -> c))
thLoc = do
  𝕊
lS ← Q 𝕊
thLoc𝕊
  Code Q ((𝕊 -> c) -> c) -> Q (TExp ((𝕊 -> c) -> c))
forall (m :: * -> *) a. Code m a -> m (TExp a)
TH.examineCode [|| \ p
f → p
f a
lS ||]

thExp ∷ TH.Q (TH.TExp a) → TH.Q (TH.TExp ((𝕊 → a → c) → c))
thExp :: forall a c. Q (TExp a) -> Q (TExp ((𝕊 -> a -> c) -> c))
thExp Q (TExp a)
xQ = do
  𝕊
xS ← Exp -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 (Exp -> 𝕊) -> (TExp a -> Exp) -> TExp a -> 𝕊
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ TExp a -> Exp
forall a. TExp a -> Exp
TH.unType (TExp a -> 𝕊) -> Q (TExp a) -> Q 𝕊
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ Q (TExp a)
xQ
  Code Q ((𝕊 -> a -> c) -> c) -> Q (TExp ((𝕊 -> a -> c) -> c))
forall (m :: * -> *) a. Code m a -> m (TExp a)
TH.examineCode [|| \ p
f → p
f a
xS $$(Q (TExp a) -> Code Q a
forall (m :: * -> *) a. m (TExp a) -> Code m a
TH.Code Q (TExp a)
xQ) ||]

thmut ∷ (HS.Monad (WriterT (𝐼 TH.Dec) TH.Q) ⇒ WriterT (𝐼 TH.Dec) TH.Q ()) → TH.Q [TH.Dec]
thmut :: (Monad (WriterT (𝐼 Dec) Q) => WriterT (𝐼 Dec) Q ()) -> Q [Dec]
thmut Monad (WriterT (𝐼 Dec) Q) => WriterT (𝐼 Dec) Q ()
xM = do
  𝐼 Dec
ds :* () ← WriterT (𝐼 Dec) Q () -> Q (𝐼 Dec ∧ ())
forall o (m :: * -> *) a. WriterT o m a -> m (o ∧ a)
unWriterT (WriterT (𝐼 Dec) Q () -> Q (𝐼 Dec ∧ ()))
-> WriterT (𝐼 Dec) Q () -> Q (𝐼 Dec ∧ ())
forall a b. (a -> b) -> a -> b
$ W (Monad (WriterT (𝐼 Dec) Q))
-> (Monad (WriterT (𝐼 Dec) Q) => WriterT (𝐼 Dec) Q ())
-> WriterT (𝐼 Dec) Q ()
forall (c :: Constraint) a. W c -> (c => a) -> a
with (forall (m :: * -> *). Monad m => W (Monad m)
tohsMonad @(WriterT (𝐼 TH.Dec) TH.Q)) WriterT (𝐼 Dec) Q ()
Monad (WriterT (𝐼 Dec) Q) => WriterT (𝐼 Dec) Q ()
xM
  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Return m => a -> m a
return ([Dec] -> Q [Dec]) -> [Dec] -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ 𝐼 Dec -> [Dec]
forall a t. ToIter a t => t -> [a]
lazyList 𝐼 Dec
ds

thdec ∷ TH.Q [TH.Dec] → WriterT (𝐼 TH.Dec) TH.Q ()
thdec :: Q [Dec] -> WriterT (𝐼 Dec) Q ()
thdec Q [Dec]
dsM = 𝐼 Dec -> WriterT (𝐼 Dec) Q ()
forall o (m :: * -> *). MonadWriter o m => o -> m ()
tell (𝐼 Dec -> WriterT (𝐼 Dec) Q ())
-> WriterT (𝐼 Dec) Q (𝐼 Dec) -> WriterT (𝐼 Dec) Q ()
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ [Dec] -> 𝐼 Dec
forall a t. ToIter a t => t -> 𝐼 a
iter ([Dec] -> 𝐼 Dec)
-> WriterT (𝐼 Dec) Q [Dec] -> WriterT (𝐼 Dec) Q (𝐼 Dec)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ Q [Dec] -> WriterT (𝐼 Dec) Q [Dec]
forall (m :: * -> *) a. Monad m => m a -> WriterT (𝐼 Dec) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(Transformer t, Monad m) =>
m a -> t m a
lift Q [Dec]
dsM