module UVMHS.Core.LensDeriving where

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

import UVMHS.Core.Effects
import UVMHS.Core.IO
import UVMHS.Core.TH

import qualified Language.Haskell.TH as TH

-- makeLensLogic [C₁,…,Cₙ] ty [a₁,…,aₙ] field fieldty ≔ 
--   [| fieldL ∷ ∀ a₁ … aₙ. (C₁,…,Cₙ) ⇒ ty a₁ … aₙ ⟢ fieldty
--      fieldL ≔ lens field (\ x s → s { field = x })
--   |]
makeLensLogic ∷ TH.Cxt → TH.Name → 𝐿 (TH.TyVarBndr ()) → TH.Name → TH.Type → TH.Q (𝐿 TH.Dec)
makeLensLogic :: Cxt -> Name -> 𝐿 (TyVarBndr ()) -> Name -> Type -> Q (𝐿 Dec)
makeLensLogic Cxt
cx Name
ty 𝐿 (TyVarBndr ())
tyargs Name
field Type
fieldty = do
  let lensName :: Name
lensName = String -> Name
TH.mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ 𝕊 -> String
tohsChars (𝕊 -> String) -> 𝕊 -> String
forall a b. (a -> b) -> a -> b
$ String -> 𝕊
forall t. ToIter ℂ t => t -> 𝕊
string (Name -> String
TH.nameBase Name
field) 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
⧺ 𝕊
"L"
      tyargVars :: 𝐿 Type
tyargVars = (TyVarBndr () -> Type) -> 𝐿 (TyVarBndr ()) -> 𝐿 Type
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (Name -> Type
TH.VarT (Name -> Type) -> (TyVarBndr () -> Name) -> TyVarBndr () -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ TyVarBndr () -> Name
forall a. TyVarBndr a -> Name
thTyVarBndrName) 𝐿 (TyVarBndr ())
tyargs
      tyargs' :: 𝐿 (TyVarBndr Specificity)
tyargs' = 𝐿 (TyVarBndr ())
-> (TyVarBndr () -> TyVarBndr Specificity)
-> 𝐿 (TyVarBndr Specificity)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝐿 (TyVarBndr ())
tyargs ((TyVarBndr () -> TyVarBndr Specificity)
 -> 𝐿 (TyVarBndr Specificity))
-> (TyVarBndr () -> TyVarBndr Specificity)
-> 𝐿 (TyVarBndr Specificity)
forall a b. (a -> b) -> a -> b
$ \case
        TH.PlainTV Name
x () → Name -> Specificity -> TyVarBndr Specificity
forall flag. Name -> flag -> TyVarBndr flag
TH.PlainTV Name
x Specificity
TH.SpecifiedSpec
        TH.KindedTV Name
x () Type
κ → Name -> Specificity -> Type -> TyVarBndr Specificity
forall flag. Name -> flag -> Type -> TyVarBndr flag
TH.KindedTV Name
x Specificity
TH.SpecifiedSpec Type
κ
  Name
tmpˣ ← String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName (String -> Q Name) -> String -> Q Name
forall a b. (a -> b) -> a -> b
$ 𝕊 -> String
tohsChars 𝕊
"x"
  Name
tmpˢ ← String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName (String -> Q Name) -> String -> Q Name
forall a b. (a -> b) -> a -> b
$ 𝕊 -> String
tohsChars 𝕊
"s"
  𝐿 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
list
    [ Pragma -> Dec
TH.PragmaD (Pragma -> Dec) -> Pragma -> Dec
forall a b. (a -> b) -> a -> b
$ Name -> Inline -> RuleMatch -> Phases -> Pragma
TH.InlineP Name
lensName Inline
TH.Inline RuleMatch
TH.FunLike Phases
TH.AllPhases
    , Name -> Type -> Dec
TH.SigD Name
lensName (Type -> Dec) -> Type -> Dec
forall a b. (a -> b) -> a -> b
$ 
        [TyVarBndr Specificity] -> Cxt -> Type -> Type
TH.ForallT (𝐿 (TyVarBndr Specificity) -> [TyVarBndr Specificity]
forall a b. CHS a b => a -> b
tohs 𝐿 (TyVarBndr Specificity)
tyargs') Cxt
cx (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
          Name -> Type
TH.ConT ''(⟢) Type -> Type -> Type
forall a. Apply a => a -> a -> a
⊙ (Name -> Type
TH.ConT Name
ty Type -> 𝐿 Type -> Type
forall e t. (Apply e, ToIter e t) => e -> t -> e
⊙⋆ 𝐿 Type
tyargVars) Type -> Type -> Type
forall a. Apply a => a -> a -> a
⊙ Type
fieldty
    , Name -> [Clause] -> Dec
TH.FunD Name
lensName ([Clause] -> Dec) -> [Clause] -> Dec
forall a b. (a -> b) -> a -> b
$ Clause -> [Clause]
forall a t. Single a t => a -> t
single (Clause -> [Clause]) -> Clause -> [Clause]
forall a b. (a -> b) -> a -> b
$ 𝐿 Pat -> Exp -> Clause
thSingleClause 𝐿 Pat
forall a. Null a => a
null (Exp -> Clause) -> Exp -> Clause
forall a b. (a -> b) -> a -> b
$ 
        Name -> Exp
TH.VarE 'lens Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ Name -> Exp
TH.VarE Name
field Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙$ [Pat] -> Exp -> Exp
TH.LamE [Name -> Pat
TH.VarP Name
tmpˢ,Name -> Pat
TH.VarP Name
tmpˣ] (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> [FieldExp] -> Exp
TH.RecUpdE (Name -> Exp
TH.VarE Name
tmpˢ) [(Name
field,Name -> Exp
TH.VarE Name
tmpˣ)]
    ]

makeLenses ∷ TH.Name → TH.Q [TH.Dec]
makeLenses :: Name -> Q [Dec]
makeLenses Name
name = do
  (Cxt
cx :* Name
ty :* 𝐿 (TyVarBndr ())
tyargs :* 𝑂 Type
_ :* Con
c :* 𝐿 DerivClause
_) ← Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ Con)
   ∧ 𝐿 DerivClause)
-> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ Con)
      ∧ 𝐿 DerivClause)
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ Con)
      ∧ 𝐿 DerivClause)
forall (m :: * -> *) a. Return m => m a -> 𝑂 a -> m a
ifNoneM (IO
  (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ Con)
   ∧ 𝐿 DerivClause)
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ Con)
      ∧ 𝐿 DerivClause)
forall a. IO a -> Q a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io IO
  (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ Con)
   ∧ 𝐿 DerivClause)
forall a. IO a
abortIO) (𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ Con)
    ∧ 𝐿 DerivClause)
 -> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ Con)
       ∧ 𝐿 DerivClause))
-> (Info
    -> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ Con)
          ∧ 𝐿 DerivClause))
-> Info
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ Con)
      ∧ 𝐿 DerivClause)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (Dec
-> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ Con)
      ∧ 𝐿 DerivClause)
thViewSingleConADT (Dec
 -> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ Con)
       ∧ 𝐿 DerivClause))
-> (Info -> 𝑂 Dec)
-> Info
-> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ Con)
      ∧ 𝐿 DerivClause)
forall (m :: * -> *) b c a.
Bind m =>
(b -> m c) -> (a -> m b) -> a -> m c
*∘ (Info ⌲ Dec) -> Info -> 𝑂 Dec
forall a b. (a ⌲ b) -> a -> 𝑂 b
view Info ⌲ Dec
thTyConIL) (Info
 -> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ Con)
       ∧ 𝐿 DerivClause))
-> Q Info
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ Con)
      ∧ 𝐿 DerivClause)
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ Name -> Q Info
TH.reify Name
name
  (Name
_ :* 𝐿 VarStrictType
fields) ← Q (Name ∧ 𝐿 VarStrictType)
-> 𝑂 (Name ∧ 𝐿 VarStrictType) -> Q (Name ∧ 𝐿 VarStrictType)
forall (m :: * -> *) a. Return m => m a -> 𝑂 a -> m a
ifNoneM (IO (Name ∧ 𝐿 VarStrictType) -> Q (Name ∧ 𝐿 VarStrictType)
forall a. IO a -> Q a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io IO (Name ∧ 𝐿 VarStrictType)
forall a. IO a
abortIO) (𝑂 (Name ∧ 𝐿 VarStrictType) -> Q (Name ∧ 𝐿 VarStrictType))
-> 𝑂 (Name ∧ 𝐿 VarStrictType) -> Q (Name ∧ 𝐿 VarStrictType)
forall a b. (a -> b) -> a -> b
$ (Con ⌲ (Name ∧ 𝐿 VarStrictType))
-> Con -> 𝑂 (Name ∧ 𝐿 VarStrictType)
forall a b. (a ⌲ b) -> a -> 𝑂 b
view Con ⌲ (Name ∧ 𝐿 VarStrictType)
thRecCL Con
c
  (𝐿 (𝐿 Dec) -> [Dec]) -> Q (𝐿 (𝐿 Dec)) -> Q [Dec]
forall a b. (a -> b) -> Q a -> Q b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (𝐿 Dec -> [Dec]
forall a b. CHS a b => a -> b
tohs (𝐿 Dec -> [Dec]) -> (𝐿 (𝐿 Dec) -> 𝐿 Dec) -> 𝐿 (𝐿 Dec) -> [Dec]
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐿 (𝐿 Dec) -> 𝐿 Dec
forall a t. (Monoid a, ToIter a t) => t -> a
concat) (Q (𝐿 (𝐿 Dec)) -> Q [Dec]) -> Q (𝐿 (𝐿 Dec)) -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ 𝐿 VarStrictType -> (VarStrictType -> Q (𝐿 Dec)) -> Q (𝐿 (𝐿 Dec))
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
t a -> (a -> m b) -> m (t b)
mapMOn 𝐿 VarStrictType
fields ((VarStrictType -> Q (𝐿 Dec)) -> Q (𝐿 (𝐿 Dec)))
-> (VarStrictType -> Q (𝐿 Dec)) -> Q (𝐿 (𝐿 Dec))
forall a b. (a -> b) -> a -> b
$ \ (VarStrictType -> (Name ∧ Bang) ∧ Type
forall a b. CHS a b => b -> a
frhs → (Name
field :* Bang
_ :* Type
fieldty)) → Cxt -> Name -> 𝐿 (TyVarBndr ()) -> Name -> Type -> Q (𝐿 Dec)
makeLensLogic Cxt
cx Name
ty 𝐿 (TyVarBndr ())
tyargs Name
field Type
fieldty

-- makePrismLogic [C₁,…,Cₙ] ty [a₁,…,aₙ] con (fieldty₁,…,fieldtyₙ) ≔ 
--   [| fieldL ∷ ∀ a₁ … aₙ. (C₁,…,Cₙ) ⇒ ty a₁ … aₙ ⌲ (fieldty₁,…,fieldtyₙ)
--      fieldL ≔ Prism 
--        { inject = con
--        , view = \ v → case v of
--            con x₁ … xₙ → Some (x₁,…,xₙ)
--            _ → None
--        }
--   |]
makePrismLogic ∷ TH.Cxt → TH.Name → 𝐿 (TH.TyVarBndr ()) → TH.Name → 𝐿 TH.Type → ℕ → TH.Q (𝐿 TH.Dec)
makePrismLogic :: Cxt -> Name -> 𝐿 (TyVarBndr ()) -> Name -> 𝐿 Type -> ℕ -> Q (𝐿 Dec)
makePrismLogic Cxt
cx Name
ty 𝐿 (TyVarBndr ())
tyargs Name
con 𝐿 Type
fieldtys ℕ
numcons = do
  let prismName :: Name
prismName = String -> Name
TH.mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ 𝕊 -> String
tohsChars (𝕊 -> String) -> 𝕊 -> String
forall a b. (a -> b) -> a -> b
$ (𝐼 ℂ -> 𝕊
forall t. ToIter ℂ t => t -> 𝕊
string (𝐼 ℂ -> 𝕊) -> 𝐼 ℂ -> 𝕊
forall a b. (a -> b) -> a -> b
$ (ℂ -> ℂ) -> String -> 𝐼 ℂ
forall a t. ToIter a t => (a -> a) -> t -> 𝐼 a
mapFirst ℂ -> ℂ
toLower (String -> 𝐼 ℂ) -> String -> 𝐼 ℂ
forall a b. (a -> b) -> a -> b
$ Name -> String
TH.nameBase Name
con) 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
⧺ 𝕊
"L"
      tyargVars :: 𝐿 Type
tyargVars = (TyVarBndr () -> Type) -> 𝐿 (TyVarBndr ()) -> 𝐿 Type
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (Name -> Type
TH.VarT (Name -> Type) -> (TyVarBndr () -> Name) -> TyVarBndr () -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ TyVarBndr () -> Name
forall a. TyVarBndr a -> Name
thTyVarBndrName) 𝐿 (TyVarBndr ())
tyargs
      tyargs' :: 𝐿 (TyVarBndr Specificity)
tyargs' = 𝐿 (TyVarBndr ())
-> (TyVarBndr () -> TyVarBndr Specificity)
-> 𝐿 (TyVarBndr Specificity)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝐿 (TyVarBndr ())
tyargs ((TyVarBndr () -> TyVarBndr Specificity)
 -> 𝐿 (TyVarBndr Specificity))
-> (TyVarBndr () -> TyVarBndr Specificity)
-> 𝐿 (TyVarBndr Specificity)
forall a b. (a -> b) -> a -> b
$ \case
        TH.PlainTV Name
x () → Name -> Specificity -> TyVarBndr Specificity
forall flag. Name -> flag -> TyVarBndr flag
TH.PlainTV Name
x Specificity
TH.SpecifiedSpec
        TH.KindedTV Name
x () Type
κ → Name -> Specificity -> Type -> TyVarBndr Specificity
forall flag. Name -> flag -> Type -> TyVarBndr flag
TH.KindedTV Name
x Specificity
TH.SpecifiedSpec Type
κ
  Name
tmpˣ ← String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName (String -> Q Name) -> String -> Q Name
forall a b. (a -> b) -> a -> b
$ 𝕊 -> String
tohsChars 𝕊
"x"
  𝐿 Name
tmpˣˢ ← 𝐿 Type -> (Type -> Q Name) -> Q (𝐿 Name)
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
t a -> (a -> m b) -> m (t b)
mapMOn 𝐿 Type
fieldtys ((Type -> Q Name) -> Q (𝐿 Name)) -> (Type -> Q Name) -> Q (𝐿 Name)
forall a b. (a -> b) -> a -> b
$ Q Name -> Type -> Q Name
forall a b. a -> b -> a
const (Q Name -> Type -> Q Name) -> Q Name -> Type -> Q Name
forall a b. (a -> b) -> a -> b
$ String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName (String -> Q Name) -> String -> Q Name
forall a b. (a -> b) -> a -> b
$ 𝕊 -> String
tohsChars 𝕊
"x"
  𝐿 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
list
    [ Pragma -> Dec
TH.PragmaD (Pragma -> Dec) -> Pragma -> Dec
forall a b. (a -> b) -> a -> b
$ Name -> Inline -> RuleMatch -> Phases -> Pragma
TH.InlineP Name
prismName Inline
TH.Inline RuleMatch
TH.FunLike Phases
TH.AllPhases
    , Name -> Type -> Dec
TH.SigD Name
prismName (Type -> Dec) -> Type -> Dec
forall a b. (a -> b) -> a -> b
$ 
        [TyVarBndr Specificity] -> Cxt -> Type -> Type
TH.ForallT (𝐿 (TyVarBndr Specificity) -> [TyVarBndr Specificity]
forall a b. CHS a b => a -> b
tohs 𝐿 (TyVarBndr Specificity)
tyargs') Cxt
cx (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ 
          Name -> Type
TH.ConT ''(⌲) Type -> Type -> Type
forall a. Apply a => a -> a -> a
⊙ (Name -> Type
TH.ConT Name
ty Type -> 𝐿 Type -> Type
forall e t. (Apply e, ToIter e t) => e -> t -> e
⊙⋆ 𝐿 Type
tyargVars) Type -> Type -> Type
forall a. Apply a => a -> a -> a
⊙ 𝐿 Type -> Type
forall t. ToIter Type t => t -> Type
forall a t. (Tup a, ToIter a t) => t -> a
tup 𝐿 Type
fieldtys
    , Name -> [Clause] -> Dec
TH.FunD Name
prismName ([Clause] -> Dec) -> [Clause] -> Dec
forall a b. (a -> b) -> a -> b
$ Clause -> [Clause]
forall a t. Single a t => a -> t
single (Clause -> [Clause]) -> Clause -> [Clause]
forall a b. (a -> b) -> a -> b
$ 𝐿 Pat -> Exp -> Clause
thSingleClause 𝐿 Pat
forall a. Null a => a
null (Exp -> Clause) -> Exp -> Clause
forall a b. (a -> b) -> a -> b
$ 
        Name -> Exp
TH.ConE 'Prism 
        Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ ([Pat] -> Exp -> Exp
TH.LamE [𝐿 Pat -> Pat
forall t. ToIter Pat t => t -> Pat
forall a t. (Tup a, ToIter a t) => t -> a
tup (𝐿 Pat -> Pat) -> 𝐿 Pat -> Pat
forall a b. (a -> b) -> a -> b
$ (Name -> Pat) -> 𝐿 Name -> 𝐿 Pat
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map Name -> Pat
TH.VarP 𝐿 Name
tmpˣˢ] (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Name -> Exp
TH.ConE Name
con Exp -> 𝐿 Exp -> Exp
forall e t. (Apply e, ToIter e t) => e -> t -> e
⊙⋆ (Name -> Exp) -> 𝐿 Name -> 𝐿 Exp
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map Name -> Exp
TH.VarE 𝐿 Name
tmpˣˢ)
        Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ ([Pat] -> Exp -> Exp
TH.LamE [Name -> Pat
TH.VarP Name
tmpˣ] (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ 
            Exp -> [Match] -> Exp
TH.CaseE (Name -> Exp
TH.VarE Name
tmpˣ) ([Match] -> Exp) -> [Match] -> Exp
forall a b. (a -> b) -> a -> b
$ [[Match]] -> [Match]
forall a t. (Monoid a, ToIter a t) => t -> a
concat
              [ Match -> [Match]
forall a t. Single a t => a -> t
single (Match -> [Match]) -> Match -> [Match]
forall a b. (a -> b) -> a -> b
$ Pat -> Exp -> Match
thSingleMatch (Name -> Cxt -> [Pat] -> Pat
TH.ConP Name
con [] ([Pat] -> Pat) -> [Pat] -> Pat
forall a b. (a -> b) -> a -> b
$ 𝐿 Pat -> [Pat]
forall a b. CHS a b => a -> b
tohs ((Name -> Pat) -> 𝐿 Name -> 𝐿 Pat
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map Name -> Pat
TH.VarP 𝐿 Name
tmpˣˢ)) (Exp -> Match) -> Exp -> Match
forall a b. (a -> b) -> a -> b
$ 
                  Name -> Exp
TH.ConE 'Some Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ 𝐿 Exp -> Exp
forall t. ToIter Exp t => t -> Exp
forall a t. (Tup a, ToIter a t) => t -> a
tup ((Name -> Exp) -> 𝐿 Name -> 𝐿 Exp
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map Name -> Exp
TH.VarE 𝐿 Name
tmpˣˢ)
              , case ℕ
numcons ℕ -> ℕ -> 𝔹
forall a. Ord a => a -> a -> 𝔹
≤ ℕ
1 of
                  -- avoids generating code that has a dead branch
                  𝔹
True → []
                  𝔹
False → Match -> [Match]
forall a t. Single a t => a -> t
single (Match -> [Match]) -> Match -> [Match]
forall a b. (a -> b) -> a -> b
$ Pat -> Exp -> Match
thSingleMatch Pat
TH.WildP (Exp -> Match) -> Exp -> Match
forall a b. (a -> b) -> a -> b
$ Name -> Exp
TH.ConE 'None
              ])
    ]

makePrisms ∷ TH.Name → TH.Q [TH.Dec]
makePrisms :: Name -> Q [Dec]
makePrisms Name
name = do
  (Cxt
cx :* Name
ty :* 𝐿 (TyVarBndr ())
tyargs :* 𝑂 Type
_ :* 𝐿 Con
cs :* 𝐿 DerivClause
_) ← Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ 𝐿 Con)
   ∧ 𝐿 DerivClause)
-> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
forall (m :: * -> *) a. Return m => m a -> 𝑂 a -> m a
ifNoneM (IO
  (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ 𝐿 Con)
   ∧ 𝐿 DerivClause)
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
forall a. IO a -> Q a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io IO
  (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ 𝐿 Con)
   ∧ 𝐿 DerivClause)
forall a. IO a
abortIO) (𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ 𝐿 Con)
    ∧ 𝐿 DerivClause)
 -> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ 𝐿 Con)
       ∧ 𝐿 DerivClause))
-> (Info
    -> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ 𝐿 Con)
          ∧ 𝐿 DerivClause))
-> Info
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (Dec
-> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
thViewADT (Dec
 -> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ 𝐿 Con)
       ∧ 𝐿 DerivClause))
-> (Info -> 𝑂 Dec)
-> Info
-> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
forall (m :: * -> *) b c a.
Bind m =>
(b -> m c) -> (a -> m b) -> a -> m c
*∘ (Info ⌲ Dec) -> Info -> 𝑂 Dec
forall a b. (a ⌲ b) -> a -> 𝑂 b
view Info ⌲ Dec
thTyConIL) (Info
 -> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ 𝐿 Con)
       ∧ 𝐿 DerivClause))
-> Q Info
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Type) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ Name -> Q Info
TH.reify Name
name
  𝐿 (Name ∧ 𝐿 Type)
scs ← (Con -> Q (Name ∧ 𝐿 Type)) -> 𝐿 Con -> Q (𝐿 (Name ∧ 𝐿 Type))
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> 𝐿 a -> m (𝐿 b)
mapM (Q (Name ∧ 𝐿 Type) -> 𝑂 (Name ∧ 𝐿 Type) -> Q (Name ∧ 𝐿 Type)
forall (m :: * -> *) a. Return m => m a -> 𝑂 a -> m a
ifNoneM (IO (Name ∧ 𝐿 Type) -> Q (Name ∧ 𝐿 Type)
forall a. IO a -> Q a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io IO (Name ∧ 𝐿 Type)
forall a. IO a
abortIO) (𝑂 (Name ∧ 𝐿 Type) -> Q (Name ∧ 𝐿 Type))
-> (Con -> 𝑂 (Name ∧ 𝐿 Type)) -> Con -> Q (Name ∧ 𝐿 Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Con -> 𝑂 (Name ∧ 𝐿 Type)
thViewSimpleCon) 𝐿 Con
cs
  let numcons :: ℕ
numcons = 𝐿 (Name ∧ 𝐿 Type) -> ℕ
forall n t a. (Zero n, One n, Plus n, ToIter a t) => t -> n
count 𝐿 (Name ∧ 𝐿 Type)
scs
  (𝐿 (𝐿 Dec) -> [Dec]) -> Q (𝐿 (𝐿 Dec)) -> Q [Dec]
forall a b. (a -> b) -> Q a -> Q b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (𝐿 Dec -> [Dec]
forall a b. CHS a b => a -> b
tohs (𝐿 Dec -> [Dec]) -> (𝐿 (𝐿 Dec) -> 𝐿 Dec) -> 𝐿 (𝐿 Dec) -> [Dec]
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐿 (𝐿 Dec) -> 𝐿 Dec
forall a t. (Monoid a, ToIter a t) => t -> a
concat) (Q (𝐿 (𝐿 Dec)) -> Q [Dec]) -> Q (𝐿 (𝐿 Dec)) -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ 𝐿 (Name ∧ 𝐿 Type)
-> ((Name ∧ 𝐿 Type) -> Q (𝐿 Dec)) -> Q (𝐿 (𝐿 Dec))
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
t a -> (a -> m b) -> m (t b)
mapMOn 𝐿 (Name ∧ 𝐿 Type)
scs (((Name ∧ 𝐿 Type) -> Q (𝐿 Dec)) -> Q (𝐿 (𝐿 Dec)))
-> ((Name ∧ 𝐿 Type) -> Q (𝐿 Dec)) -> Q (𝐿 (𝐿 Dec))
forall a b. (a -> b) -> a -> b
$ \ (Name
con :* 𝐿 Type
fieldtys) → Cxt -> Name -> 𝐿 (TyVarBndr ()) -> Name -> 𝐿 Type -> ℕ -> Q (𝐿 Dec)
makePrismLogic Cxt
cx Name
ty 𝐿 (TyVarBndr ())
tyargs Name
con 𝐿 Type
fieldtys ℕ
numcons