module UVMHS.Lib.Pretty.Deriving where

import UVMHS.Core

import UVMHS.Lib.Pretty.Doc

import qualified Language.Haskell.TH as TH

import qualified Data.Text as Text

-- makePrettySumLogic [C₁,…,Cₙ] ty [a₁,…,aₙ] [(con₁,[conty₁₁,…,conty₁⸤n₁⸥]),…,(conₘ,[contyₘ₁,…,contyₘ⸤nₘ⸥])] ≔ 
--   [| instance 
--        (C₁,…,Cₙ
--        ,Pretty conty₁₁,…,Pretty conty₁⸤n₁⸥,…,Pretty contyₘ₁,…,Pretty contyₘ⸤nₘ⸥
--        ) ⇒ Pretty (ty a₁ … aₙ) where
--          pretty (con₁ (x₁₁ ∷ conty₁₁) … x₁⸤n₁⸥) = app [con "con₁",pretty x₁₁,…,pretty x₁⸤n₁⸥]
--          …
--          pretty (conₘ (xₘ₁ ∷ contyₘ₁) … xₘ⸤nₘ⸥) = app [con "conₘ",pretty xₘ₁,…,pretty xₘ⸤nₘ⸥]
--   |]
makePrettySumLogic ∷ TH.Cxt → TH.Name → 𝐿 (TH.TyVarBndr ()) → 𝐿 (TH.Name ∧ 𝐿 TH.Type) → TH.Q (𝐿 TH.Dec)
makePrettySumLogic :: Cxt -> Name -> 𝐿 (TyVarBndr ()) -> 𝐿 (Name ∧ 𝐿 Pred) -> Q (𝐿 Dec)
makePrettySumLogic Cxt
cx Name
ty 𝐿 (TyVarBndr ())
tyargs 𝐿 (Name ∧ 𝐿 Pred)
concontys = do
  𝐿 (Name ∧ 𝐿 Name)
conxs ∷ 𝐿 (TH.Name ∧ 𝐿 TH.Name) ← 𝐿 (Name ∧ 𝐿 Pred)
-> ((Name ∧ 𝐿 Pred) -> Q (Name ∧ 𝐿 Name)) -> Q (𝐿 (Name ∧ 𝐿 Name))
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
t a -> (a -> m b) -> m (t b)
mapMOn 𝐿 (Name ∧ 𝐿 Pred)
concontys (((Name ∧ 𝐿 Pred) -> Q (Name ∧ 𝐿 Name)) -> Q (𝐿 (Name ∧ 𝐿 Name)))
-> ((Name ∧ 𝐿 Pred) -> Q (Name ∧ 𝐿 Name)) -> Q (𝐿 (Name ∧ 𝐿 Name))
forall a b. (a -> b) -> a -> b
$ \ (Name
con :* 𝐿 Pred
contys) → do
    𝐿 Name
tmpˣˢ ← 𝐿 Pred -> (Pred -> Q Name) -> Q (𝐿 Name)
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
t a -> (a -> m b) -> m (t b)
mapMOn 𝐿 Pred
contys ((Pred -> Q Name) -> Q (𝐿 Name)) -> (Pred -> Q Name) -> Q (𝐿 Name)
forall a b. (a -> b) -> a -> b
$ Q Name -> Pred -> Q Name
forall a b. a -> b -> a
const (Q Name -> Pred -> Q Name) -> Q Name -> Pred -> 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"
    (Name ∧ 𝐿 Name) -> Q (Name ∧ 𝐿 Name)
forall a. a -> Q a
forall (m :: * -> *) a. Return m => a -> m a
return (Name
con Name -> 𝐿 Name -> Name ∧ 𝐿 Name
forall a b. a -> b -> a ∧ b
:* 𝐿 Name
tmpˣˢ)
  let tyargVars ∷ 𝐿 TH.Type
      tyargVars :: 𝐿 Pred
tyargVars = (TyVarBndr () -> Pred) -> 𝐿 (TyVarBndr ()) -> 𝐿 Pred
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (Name -> Pred
TH.VarT (Name -> Pred) -> (TyVarBndr () -> Name) -> TyVarBndr () -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ TyVarBndr () -> Name
forall a. TyVarBndr a -> Name
thTyVarBndrName) 𝐿 (TyVarBndr ())
tyargs
      instanceCx ∷ 𝐿 TH.Pred
      instanceCx :: 𝐿 Pred
instanceCx = 𝐼 Pred -> 𝐿 Pred
forall a t. ToIter a t => t -> 𝐿 a
list (𝐼 Pred -> 𝐿 Pred) -> 𝐼 Pred -> 𝐿 Pred
forall a b. (a -> b) -> a -> b
$ 𝐿 Pred -> 𝐼 Pred
forall a t. (Ord a, ToIter a t) => t -> 𝐼 a
uniques𝑃 (𝐿 Pred -> 𝐼 Pred) -> 𝐿 Pred -> 𝐼 Pred
forall a b. (a -> b) -> a -> b
$ [𝐿 Pred] -> 𝐿 Pred
forall a t. (Monoid a, ToIter a t) => t -> a
concat 
        [ Cxt -> 𝐿 Pred
forall a b. CHS a b => b -> a
frhs Cxt
cx
        , (Pred -> Pred) -> 𝐿 Pred -> 𝐿 Pred
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (\ Pred
x → Name -> Pred
TH.ConT ''Pretty Pred -> Pred -> Pred
forall a. Apply a => a -> a -> a
⊙ Pred
x) (𝐿 Pred -> 𝐿 Pred) -> 𝐿 Pred -> 𝐿 Pred
forall a b. (a -> b) -> a -> b
$ 𝐿 (𝐿 Pred) -> 𝐿 Pred
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐿 (𝐿 Pred) -> 𝐿 Pred) -> 𝐿 (𝐿 Pred) -> 𝐿 Pred
forall a b. (a -> b) -> a -> b
$ ((Name ∧ 𝐿 Pred) -> 𝐿 Pred) -> 𝐿 (Name ∧ 𝐿 Pred) -> 𝐿 (𝐿 Pred)
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (Name ∧ 𝐿 Pred) -> 𝐿 Pred
forall a b. (a ∧ b) -> b
snd (𝐿 (Name ∧ 𝐿 Pred) -> 𝐿 (𝐿 Pred))
-> 𝐿 (Name ∧ 𝐿 Pred) -> 𝐿 (𝐿 Pred)
forall a b. (a -> b) -> a -> b
$ 𝐿 (Name ∧ 𝐿 Pred)
concontys
        ]
      instanceTy ∷ TH.Type
      instanceTy :: Pred
instanceTy = Name -> Pred
TH.ConT ''Pretty Pred -> Pred -> Pred
forall a. Apply a => a -> a -> a
⊙ (Name -> Pred
TH.ConT Name
ty Pred -> 𝐿 Pred -> Pred
forall e t. (Apply e, ToIter e t) => e -> t -> e
⊙⋆ 𝐿 Pred
tyargVars)
      instanceDec ∷ TH.Dec
      instanceDec :: Dec
instanceDec = Name -> [Clause] -> Dec
TH.FunD 'pretty ([Clause] -> Dec) -> [Clause] -> Dec
forall a b. (a -> b) -> a -> b
$ 𝐿 Clause -> [Clause]
forall a b. CHS a b => a -> b
tohs (𝐿 Clause -> [Clause]) -> 𝐿 Clause -> [Clause]
forall a b. (a -> b) -> a -> b
$ 𝐿 (Name ∧ 𝐿 Name) -> ((Name ∧ 𝐿 Name) -> Clause) -> 𝐿 Clause
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝐿 (Name ∧ 𝐿 Name)
conxs (((Name ∧ 𝐿 Name) -> Clause) -> 𝐿 Clause)
-> ((Name ∧ 𝐿 Name) -> Clause) -> 𝐿 Clause
forall a b. (a -> b) -> a -> b
$ \ (Name
con :* 𝐿 Name
tmpˣˢ) →
        let conString :: Exp
conString = 𝕊 -> Exp
thString (𝕊 -> Exp) -> 𝕊 -> Exp
forall a b. (a -> b) -> a -> b
$ String -> 𝕊
forall t. ToIter ℂ t => t -> 𝕊
string (String -> 𝕊) -> String -> 𝕊
forall a b. (a -> b) -> a -> b
$ Name -> String
TH.nameBase Name
con
            prettyCon :: Exp
prettyCon = Name -> Exp
TH.VarE 'ppCon Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ Exp
conString
            prettyXs :: 𝐿 Exp
prettyXs = 𝐿 Name -> (Name -> Exp) -> 𝐿 Exp
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝐿 Name
tmpˣˢ ((Name -> Exp) -> 𝐿 Exp) -> (Name -> Exp) -> 𝐿 Exp
forall a b. (a -> b) -> a -> b
$ \ Name
x → Name -> Exp
TH.VarE 'pretty Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ Name -> Exp
TH.VarE Name
x
        in 𝐿 Pat -> Exp -> Clause
thSingleClause (Pat -> 𝐿 Pat
forall a t. Single a t => a -> t
single (Pat -> 𝐿 Pat) -> Pat -> 𝐿 Pat
forall a b. (a -> b) -> a -> b
$ 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 (𝐿 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 -> Clause) -> Exp -> Clause
forall a b. (a -> b) -> a -> b
$ Name -> Exp
TH.VarE 'ppApp Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ Exp
prettyCon Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙$ Name -> Exp
TH.VarE 'list Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙$ [Exp] -> Exp
TH.ListE (𝐿 Exp -> [Exp]
forall a b. CHS a b => a -> b
tohs 𝐿 Exp
prettyXs)
  𝐿 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. Single a t => a -> t
single (Dec -> 𝐿 Dec) -> Dec -> 𝐿 Dec
forall a b. (a -> b) -> a -> b
$ Maybe Overlap -> Cxt -> Pred -> [Dec] -> Dec
TH.InstanceD (𝑂 Overlap -> Maybe Overlap
forall a b. CHS a b => a -> b
tohs 𝑂 Overlap
forall a. 𝑂 a
None) (𝐿 Pred -> Cxt
forall a b. CHS a b => a -> b
tohs 𝐿 Pred
instanceCx) Pred
instanceTy ([Dec] -> Dec) -> [Dec] -> Dec
forall a b. (a -> b) -> a -> b
$ Dec -> [Dec]
forall a t. Single a t => a -> t
single Dec
instanceDec

makePrettySum ∷ TH.Name → TH.Q [TH.Dec]
makePrettySum :: Name -> Q [Dec]
makePrettySum Name
name = do
  (Cxt
cx :* Name
ty :* 𝐿 (TyVarBndr ())
tyargs :* 𝑂 Pred
_ :* 𝐿 Con
cs :* 𝐿 DerivClause
_) ← Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
   ∧ 𝐿 DerivClause)
-> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
forall (m :: * -> *) a. Return m => m a -> 𝑂 a -> m a
ifNoneM (IO
  (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
   ∧ 𝐿 DerivClause)
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
forall a. IO a -> Q a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io IO
  (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
   ∧ 𝐿 DerivClause)
forall a. IO a
abortIO) (𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
    ∧ 𝐿 DerivClause)
 -> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
       ∧ 𝐿 DerivClause))
-> (Info
    -> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
          ∧ 𝐿 DerivClause))
-> Info
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (Dec
-> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
thViewADT (Dec
 -> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
       ∧ 𝐿 DerivClause))
-> (Info -> 𝑂 Dec)
-> Info
-> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 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 ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
       ∧ 𝐿 DerivClause))
-> Q Info
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ Name -> Q Info
TH.reify Name
name
  𝐿 (Name ∧ 𝐿 Pred)
scs ← (Con -> Q (Name ∧ 𝐿 Pred)) -> 𝐿 Con -> Q (𝐿 (Name ∧ 𝐿 Pred))
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 ∧ 𝐿 Pred) -> 𝑂 (Name ∧ 𝐿 Pred) -> Q (Name ∧ 𝐿 Pred)
forall (m :: * -> *) a. Return m => m a -> 𝑂 a -> m a
ifNoneM (IO (Name ∧ 𝐿 Pred) -> Q (Name ∧ 𝐿 Pred)
forall a. IO a -> Q a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io IO (Name ∧ 𝐿 Pred)
forall a. IO a
abortIO) (𝑂 (Name ∧ 𝐿 Pred) -> Q (Name ∧ 𝐿 Pred))
-> (Con -> 𝑂 (Name ∧ 𝐿 Pred)) -> Con -> Q (Name ∧ 𝐿 Pred)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Con -> 𝑂 (Name ∧ 𝐿 Pred)
thViewSimpleCon) 𝐿 Con
cs
  (𝐿 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 (Q (𝐿 Dec) -> Q [Dec]) -> Q (𝐿 Dec) -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ Cxt -> Name -> 𝐿 (TyVarBndr ()) -> 𝐿 (Name ∧ 𝐿 Pred) -> Q (𝐿 Dec)
makePrettySumLogic Cxt
cx Name
ty 𝐿 (TyVarBndr ())
tyargs 𝐿 (Name ∧ 𝐿 Pred)
scs

-- makePrettyUnionLogic [C₁,…,Cₙ] ty [a₁,…,aₙ] [(con₁,[conty₁₁,…,conty₁⸤n₁⸥]),…,(conₘ,[contyₘ₁,…,contyₘ⸤nₘ⸥])] ≔ 
--   [| instance 
--        (C₁,…,Cₙ
--        ,Pretty conty₁₁,…,Pretty conty₁⸤n₁⸥,…,Pretty contyₘ₁,…,Pretty contyₘ⸤nₘ⸥
--        ) ⇒ Pretty (ty a₁ … aₙ) where
--          pretty (con₁ (x₁₁ ∷ conty₁₁) … x₁⸤n₁⸥) = tup [pretty x₁₁,…,pretty x₁⸤n₁⸥]
--          …
--          pretty (conₘ (xₘ₁ ∷ contyₘ₁) … xₘ⸤nₘ⸥) = tup [pretty xₘ₁,…,pretty xₘ⸤nₘ⸥]
--   |]
makePrettyUnionLogic ∷ TH.Cxt → TH.Name → 𝐿 (TH.TyVarBndr ()) → 𝐿 (TH.Name ∧ 𝐿 TH.Type) → TH.Q (𝐿 TH.Dec)
makePrettyUnionLogic :: Cxt -> Name -> 𝐿 (TyVarBndr ()) -> 𝐿 (Name ∧ 𝐿 Pred) -> Q (𝐿 Dec)
makePrettyUnionLogic Cxt
cx Name
ty 𝐿 (TyVarBndr ())
tyargs 𝐿 (Name ∧ 𝐿 Pred)
concontys = do
  𝐿 (Name ∧ 𝐿 Name)
conxs ∷ 𝐿 (TH.Name ∧ 𝐿 TH.Name) ← 𝐿 (Name ∧ 𝐿 Pred)
-> ((Name ∧ 𝐿 Pred) -> Q (Name ∧ 𝐿 Name)) -> Q (𝐿 (Name ∧ 𝐿 Name))
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
t a -> (a -> m b) -> m (t b)
mapMOn 𝐿 (Name ∧ 𝐿 Pred)
concontys (((Name ∧ 𝐿 Pred) -> Q (Name ∧ 𝐿 Name)) -> Q (𝐿 (Name ∧ 𝐿 Name)))
-> ((Name ∧ 𝐿 Pred) -> Q (Name ∧ 𝐿 Name)) -> Q (𝐿 (Name ∧ 𝐿 Name))
forall a b. (a -> b) -> a -> b
$ \ (Name
con :* 𝐿 Pred
fieldtys) → do
    𝐿 Name
tmpˣˢ ← 𝐿 Pred -> (Pred -> Q Name) -> Q (𝐿 Name)
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
t a -> (a -> m b) -> m (t b)
mapMOn 𝐿 Pred
fieldtys ((Pred -> Q Name) -> Q (𝐿 Name)) -> (Pred -> Q Name) -> Q (𝐿 Name)
forall a b. (a -> b) -> a -> b
$ Q Name -> Pred -> Q Name
forall a b. a -> b -> a
const (Q Name -> Pred -> Q Name) -> Q Name -> Pred -> 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"
    (Name ∧ 𝐿 Name) -> Q (Name ∧ 𝐿 Name)
forall a. a -> Q a
forall (m :: * -> *) a. Return m => a -> m a
return (Name
con Name -> 𝐿 Name -> Name ∧ 𝐿 Name
forall a b. a -> b -> a ∧ b
:* 𝐿 Name
tmpˣˢ)
  let tyargVars :: 𝐿 Pred
tyargVars = (TyVarBndr () -> Pred) -> 𝐿 (TyVarBndr ()) -> 𝐿 Pred
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (Name -> Pred
TH.VarT (Name -> Pred) -> (TyVarBndr () -> Name) -> TyVarBndr () -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ TyVarBndr () -> Name
forall a. TyVarBndr a -> Name
thTyVarBndrName) 𝐿 (TyVarBndr ())
tyargs
      instanceCx ∷ 𝐿 TH.Pred
      instanceCx :: 𝐿 Pred
instanceCx = 𝐼 Pred -> 𝐿 Pred
forall a t. ToIter a t => t -> 𝐿 a
list (𝐼 Pred -> 𝐿 Pred) -> 𝐼 Pred -> 𝐿 Pred
forall a b. (a -> b) -> a -> b
$ 𝐿 Pred -> 𝐼 Pred
forall a t. (Ord a, ToIter a t) => t -> 𝐼 a
uniques𝑃 (𝐿 Pred -> 𝐼 Pred) -> 𝐿 Pred -> 𝐼 Pred
forall a b. (a -> b) -> a -> b
$ [𝐿 Pred] -> 𝐿 Pred
forall a t. (Monoid a, ToIter a t) => t -> a
concat [Cxt -> 𝐿 Pred
forall a b. CHS a b => b -> a
frhs Cxt
cx,(Pred -> Pred) -> 𝐿 Pred -> 𝐿 Pred
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (\ Pred
x → Name -> Pred
TH.ConT ''Pretty Pred -> Pred -> Pred
forall a. Apply a => a -> a -> a
⊙ Pred
x) (𝐿 Pred -> 𝐿 Pred) -> 𝐿 Pred -> 𝐿 Pred
forall a b. (a -> b) -> a -> b
$ 𝐿 (𝐿 Pred) -> 𝐿 Pred
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐿 (𝐿 Pred) -> 𝐿 Pred) -> 𝐿 (𝐿 Pred) -> 𝐿 Pred
forall a b. (a -> b) -> a -> b
$ ((Name ∧ 𝐿 Pred) -> 𝐿 Pred) -> 𝐿 (Name ∧ 𝐿 Pred) -> 𝐿 (𝐿 Pred)
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (Name ∧ 𝐿 Pred) -> 𝐿 Pred
forall a b. (a ∧ b) -> b
snd 𝐿 (Name ∧ 𝐿 Pred)
concontys]
      instanceTy ∷ TH.Type
      instanceTy :: Pred
instanceTy = Name -> Pred
TH.ConT ''Pretty Pred -> Pred -> Pred
forall a. Apply a => a -> a -> a
⊙ (Name -> Pred
TH.ConT Name
ty Pred -> 𝐿 Pred -> Pred
forall e t. (Apply e, ToIter e t) => e -> t -> e
⊙⋆ 𝐿 Pred
tyargVars)
      instanceDec ∷ TH.Dec
      instanceDec :: Dec
instanceDec = Name -> [Clause] -> Dec
TH.FunD 'pretty ([Clause] -> Dec) -> [Clause] -> Dec
forall a b. (a -> b) -> a -> b
$ 𝐿 Clause -> [Clause]
forall a b. CHS a b => a -> b
tohs (𝐿 Clause -> [Clause]) -> 𝐿 Clause -> [Clause]
forall a b. (a -> b) -> a -> b
$ 𝐿 (Name ∧ 𝐿 Name) -> ((Name ∧ 𝐿 Name) -> Clause) -> 𝐿 Clause
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝐿 (Name ∧ 𝐿 Name)
conxs (((Name ∧ 𝐿 Name) -> Clause) -> 𝐿 Clause)
-> ((Name ∧ 𝐿 Name) -> Clause) -> 𝐿 Clause
forall a b. (a -> b) -> a -> b
$ \ (Name
con :* 𝐿 Name
tmpˣˢ) → 
        𝐿 Pat -> Exp -> Clause
thSingleClause (Pat -> 𝐿 Pat
forall a t. Single a t => a -> t
single (Pat -> 𝐿 Pat) -> Pat -> 𝐿 Pat
forall a b. (a -> b) -> a -> b
$ 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 (𝐿 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 -> Clause) -> Exp -> Clause
forall a b. (a -> b) -> a -> b
$  case 𝐿 Name
tmpˣˢ of
          𝐿 Name
Nil → Name -> Exp
TH.VarE 'pretty Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ Name -> Exp
TH.ConE '()
          Name
x :& 𝐿 Name
Nil → Name -> Exp
TH.VarE 'pretty Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ Name -> Exp
TH.VarE Name
x
          𝐿 Name
_ → 
            let prettyXs :: 𝐿 Exp
prettyXs = 𝐿 Name -> (Name -> Exp) -> 𝐿 Exp
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝐿 Name
tmpˣˢ ((Name -> Exp) -> 𝐿 Exp) -> (Name -> Exp) -> 𝐿 Exp
forall a b. (a -> b) -> a -> b
$ \ Name
x → Name -> Exp
TH.VarE 'pretty Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ Name -> Exp
TH.VarE Name
x
            in 
            Name -> Exp
TH.VarE 'ppCollection 
            Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ (Name -> Exp
TH.VarE 'ppPun Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ 𝕊 -> Exp
thString 𝕊
"⟨") 
            Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ (Name -> Exp
TH.VarE 'ppPun Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ 𝕊 -> Exp
thString 𝕊
"⟩") 
            Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ (Name -> Exp
TH.VarE 'ppPun Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ 𝕊 -> Exp
thString 𝕊
",") 
            Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙$ Name -> Exp
TH.VarE 'list 
            Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙$ [Exp] -> Exp
TH.ListE (𝐿 Exp -> [Exp]
forall a b. CHS a b => a -> b
tohs 𝐿 Exp
prettyXs)
  𝐿 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. Single a t => a -> t
single (Dec -> 𝐿 Dec) -> Dec -> 𝐿 Dec
forall a b. (a -> b) -> a -> b
$ Maybe Overlap -> Cxt -> Pred -> [Dec] -> Dec
TH.InstanceD (𝑂 Overlap -> Maybe Overlap
forall a b. CHS a b => a -> b
tohs 𝑂 Overlap
forall a. 𝑂 a
None) (𝐿 Pred -> Cxt
forall a b. CHS a b => a -> b
tohs 𝐿 Pred
instanceCx) Pred
instanceTy ([Dec] -> Dec) -> [Dec] -> Dec
forall a b. (a -> b) -> a -> b
$ Dec -> [Dec]
forall a t. Single a t => a -> t
single (Dec -> [Dec]) -> Dec -> [Dec]
forall a b. (a -> b) -> a -> b
$ Dec
instanceDec

makePrettyUnion ∷ TH.Name → TH.Q [TH.Dec]
makePrettyUnion :: Name -> Q [Dec]
makePrettyUnion Name
name = do
  (Cxt
cx :* Name
ty :* 𝐿 (TyVarBndr ())
tyargs :* 𝑂 Pred
_ :* 𝐿 Con
cs :* 𝐿 DerivClause
_) ← Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
   ∧ 𝐿 DerivClause)
-> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
forall (m :: * -> *) a. Return m => m a -> 𝑂 a -> m a
ifNoneM (IO
  (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
   ∧ 𝐿 DerivClause)
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
forall a. IO a -> Q a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io IO
  (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
   ∧ 𝐿 DerivClause)
forall a. IO a
abortIO) (𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
    ∧ 𝐿 DerivClause)
 -> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
       ∧ 𝐿 DerivClause))
-> (Info
    -> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
          ∧ 𝐿 DerivClause))
-> Info
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (Dec
-> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
thViewADT (Dec
 -> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
       ∧ 𝐿 DerivClause))
-> (Info -> 𝑂 Dec)
-> Info
-> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 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 ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
       ∧ 𝐿 DerivClause))
-> Q Info
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 𝐿 Con)
      ∧ 𝐿 DerivClause)
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ Name -> Q Info
TH.reify Name
name
  𝐿 (Name ∧ 𝐿 Pred)
scs ← (Con -> Q (Name ∧ 𝐿 Pred)) -> 𝐿 Con -> Q (𝐿 (Name ∧ 𝐿 Pred))
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 ∧ 𝐿 Pred) -> 𝑂 (Name ∧ 𝐿 Pred) -> Q (Name ∧ 𝐿 Pred)
forall (m :: * -> *) a. Return m => m a -> 𝑂 a -> m a
ifNoneM (IO (Name ∧ 𝐿 Pred) -> Q (Name ∧ 𝐿 Pred)
forall a. IO a -> Q a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io IO (Name ∧ 𝐿 Pred)
forall a. IO a
abortIO) (𝑂 (Name ∧ 𝐿 Pred) -> Q (Name ∧ 𝐿 Pred))
-> (Con -> 𝑂 (Name ∧ 𝐿 Pred)) -> Con -> Q (Name ∧ 𝐿 Pred)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Con -> 𝑂 (Name ∧ 𝐿 Pred)
thViewSimpleCon) 𝐿 Con
cs
  (𝐿 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 (Q (𝐿 Dec) -> Q [Dec]) -> Q (𝐿 Dec) -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ Cxt -> Name -> 𝐿 (TyVarBndr ()) -> 𝐿 (Name ∧ 𝐿 Pred) -> Q (𝐿 Dec)
makePrettyUnionLogic Cxt
cx Name
ty 𝐿 (TyVarBndr ())
tyargs 𝐿 (Name ∧ 𝐿 Pred)
scs

-- makePrettyRecordLogic [C₁,…,Cₙ] ty [a₁,…,aₙ] con [(field₁,fieldty₁),…,(fieldₙ,fieldtyₙ)] ≔
--   [| instance 
--        (C₁,…,Cₙ
--        ,Pretty fieldty₁,…,Pretty fieldtyₙ
--        ) ⇒ Pretty (ty a₁ … aₙ) where
--          pretty (con {field₁ = tmp₁;fieldₙ = tmpₙ}) = app [con "con",record [("field₁",tmp₁),…,("fieldₙ",tmpₙ)
--   |]
makePrettyRecordLogic ∷ TH.Cxt → TH.Name → 𝐿 (TH.TyVarBndr ()) → TH.Name → 𝐿 (TH.Name ∧ TH.Type) → TH.Q (𝐿 TH.Dec)
makePrettyRecordLogic :: Cxt
-> Name -> 𝐿 (TyVarBndr ()) -> Name -> 𝐿 (Name ∧ Pred) -> Q (𝐿 Dec)
makePrettyRecordLogic Cxt
cx Name
ty 𝐿 (TyVarBndr ())
tyargs Name
con 𝐿 (Name ∧ Pred)
fieldfieldtys = do
  let conName :: 𝕊
conName = String -> 𝕊
forall t. ToIter ℂ t => t -> 𝕊
string (String -> 𝕊) -> String -> 𝕊
forall a b. (a -> b) -> a -> b
$ Name -> String
TH.nameBase Name
con
      conNameFirstLower :: 𝕊
conNameFirstLower = 𝐼 ℂ -> 𝕊
forall t. ToIter ℂ t => t -> 𝕊
string (𝐼 ℂ -> 𝕊) -> 𝐼 ℂ -> 𝕊
forall a b. (a -> b) -> a -> b
$ (ℂ -> ℂ) -> 𝐼 ℂ -> 𝐼 ℂ
forall a t. ToIter a t => (a -> a) -> t -> 𝐼 a
mapFirst ℂ -> ℂ
toLower (𝐼 ℂ -> 𝐼 ℂ) -> 𝐼 ℂ -> 𝐼 ℂ
forall a b. (a -> b) -> a -> b
$ 𝕊 -> 𝐼 ℂ
forall a t. ToIter a t => t -> 𝐼 a
iter 𝕊
conName
      conNameAllLower :: 𝕊
conNameAllLower = 𝐼 ℂ -> 𝕊
forall t. ToIter ℂ t => t -> 𝕊
string (𝐼 ℂ -> 𝕊) -> 𝐼 ℂ -> 𝕊
forall a b. (a -> b) -> a -> b
$ (ℂ -> ℂ) -> 𝐼 ℂ -> 𝐼 ℂ
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ℂ -> ℂ
toLower (𝐼 ℂ -> 𝐼 ℂ) -> 𝐼 ℂ -> 𝐼 ℂ
forall a b. (a -> b) -> a -> b
$ 𝕊 -> 𝐼 ℂ
forall a t. ToIter a t => t -> 𝐼 a
iter 𝕊
conName
  𝐿 ((Name ∧ 𝕊) ∧ Name)
fieldNameTmps ← 𝐿 (Name ∧ Pred)
-> ((Name ∧ Pred) -> Q ((Name ∧ 𝕊) ∧ Name))
-> Q (𝐿 ((Name ∧ 𝕊) ∧ Name))
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
t a -> (a -> m b) -> m (t b)
mapMOn 𝐿 (Name ∧ Pred)
fieldfieldtys (((Name ∧ Pred) -> Q ((Name ∧ 𝕊) ∧ Name))
 -> Q (𝐿 ((Name ∧ 𝕊) ∧ Name)))
-> ((Name ∧ Pred) -> Q ((Name ∧ 𝕊) ∧ Name))
-> Q (𝐿 ((Name ∧ 𝕊) ∧ Name))
forall a b. (a -> b) -> a -> b
$ \ (Name
field :* Pred
_) → do
    let fieldName :: 𝕊
fieldName = String -> 𝕊
forall t. ToIter ℂ t => t -> 𝕊
string (String -> 𝕊) -> String -> 𝕊
forall a b. (a -> b) -> a -> b
$ Name -> String
TH.nameBase Name
field
    let afterPrefix :: 𝕊
afterPrefix = 𝕊 -> 𝑂 𝕊 -> 𝕊
forall a. a -> 𝑂 a -> a
ifNone 𝕊
fieldName (𝑂 𝕊 -> 𝕊) -> 𝑂 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ 𝐿 (𝑂 𝕊) -> 𝑂 𝕊
forall a. 𝐿 (𝑂 a) -> 𝑂 a
firstSome (𝐿 (𝑂 𝕊) -> 𝑂 𝕊) -> 𝐿 (𝑂 𝕊) -> 𝑂 𝕊
forall a b. (a -> b) -> a -> b
$ [𝑂 𝕊] -> 𝐿 (𝑂 𝕊)
forall a t. ToIter a t => t -> 𝐿 a
list
          [ Maybe 𝕊 -> 𝑂 𝕊
forall a b. CHS a b => b -> a
frhs (Maybe 𝕊 -> 𝑂 𝕊) -> Maybe 𝕊 -> 𝑂 𝕊
forall a b. (a -> b) -> a -> b
$ 𝕊 -> 𝕊 -> Maybe 𝕊
Text.stripPrefix 𝕊
conNameFirstLower 𝕊
fieldName
          , Maybe 𝕊 -> 𝑂 𝕊
forall a b. CHS a b => b -> a
frhs (Maybe 𝕊 -> 𝑂 𝕊) -> Maybe 𝕊 -> 𝑂 𝕊
forall a b. (a -> b) -> a -> b
$ 𝕊 -> 𝕊 -> Maybe 𝕊
Text.stripPrefix 𝕊
conNameAllLower 𝕊
fieldName
          , Maybe 𝕊 -> 𝑂 𝕊
forall a b. CHS a b => b -> a
frhs (Maybe 𝕊 -> 𝑂 𝕊) -> Maybe 𝕊 -> 𝑂 𝕊
forall a b. (a -> b) -> a -> b
$ 𝕊 -> 𝕊 -> Maybe 𝕊
Text.stripSuffix 𝕊
conName 𝕊
fieldName
          ]
        afterPrefix' :: 𝕊
afterPrefix' = if 𝕊
afterPrefix 𝕊 -> 𝕊 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ 𝕊
forall a. Null a => a
null then 𝕊
fieldName else 𝕊
afterPrefix
        loweredAfterPrefix :: 𝕊
loweredAfterPrefix = 𝐼 ℂ -> 𝕊
forall t. ToIter ℂ t => t -> 𝕊
string (𝐼 ℂ -> 𝕊) -> 𝐼 ℂ -> 𝕊
forall a b. (a -> b) -> a -> b
$ (ℂ -> ℂ) -> 𝕊 -> 𝐼 ℂ
forall a t. ToIter a t => (a -> a) -> t -> 𝐼 a
mapFirst ℂ -> ℂ
toLower 𝕊
afterPrefix'
    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 ∧ 𝕊) ∧ Name) -> Q ((Name ∧ 𝕊) ∧ Name)
forall a. a -> Q a
forall (m :: * -> *) a. Return m => a -> m a
return (Name
field Name -> 𝕊 -> Name ∧ 𝕊
forall a b. a -> b -> a ∧ b
:* 𝕊
loweredAfterPrefix (Name ∧ 𝕊) -> Name -> (Name ∧ 𝕊) ∧ Name
forall a b. a -> b -> a ∧ b
:* Name
tmpˣ)
  let tyargVars :: 𝐿 Pred
tyargVars = (TyVarBndr () -> Pred) -> 𝐿 (TyVarBndr ()) -> 𝐿 Pred
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (Name -> Pred
TH.VarT (Name -> Pred) -> (TyVarBndr () -> Name) -> TyVarBndr () -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ TyVarBndr () -> Name
forall a. TyVarBndr a -> Name
thTyVarBndrName) 𝐿 (TyVarBndr ())
tyargs
      instanceCx ∷ 𝐿 TH.Pred
      instanceCx :: 𝐿 Pred
instanceCx = 𝐼 Pred -> 𝐿 Pred
forall a t. ToIter a t => t -> 𝐿 a
list (𝐼 Pred -> 𝐿 Pred) -> 𝐼 Pred -> 𝐿 Pred
forall a b. (a -> b) -> a -> b
$ 𝐿 Pred -> 𝐼 Pred
forall a t. (Ord a, ToIter a t) => t -> 𝐼 a
uniques𝑃 (𝐿 Pred -> 𝐼 Pred) -> 𝐿 Pred -> 𝐼 Pred
forall a b. (a -> b) -> a -> b
$ [𝐿 Pred] -> 𝐿 Pred
forall a t. (Monoid a, ToIter a t) => t -> a
concat 
        [ Cxt -> 𝐿 Pred
forall a b. CHS a b => b -> a
frhs Cxt
cx
        , (Pred -> Pred) -> 𝐿 Pred -> 𝐿 Pred
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (\ Pred
x → Name -> Pred
TH.ConT ''Pretty Pred -> Pred -> Pred
forall a. Apply a => a -> a -> a
⊙ Pred
x) (𝐿 Pred -> 𝐿 Pred) -> 𝐿 Pred -> 𝐿 Pred
forall a b. (a -> b) -> a -> b
$ ((Name ∧ Pred) -> Pred) -> 𝐿 (Name ∧ Pred) -> 𝐿 Pred
forall a b. (a -> b) -> 𝐿 a -> 𝐿 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (Name ∧ Pred) -> Pred
forall a b. (a ∧ b) -> b
snd 𝐿 (Name ∧ Pred)
fieldfieldtys
        ]
      instanceTy ∷ TH.Type
      instanceTy :: Pred
instanceTy = Name -> Pred
TH.ConT ''Pretty Pred -> Pred -> Pred
forall a. Apply a => a -> a -> a
⊙ (Name -> Pred
TH.ConT Name
ty Pred -> 𝐿 Pred -> Pred
forall e t. (Apply e, ToIter e t) => e -> t -> e
⊙⋆ 𝐿 Pred
tyargVars)
      instanceDec ∷ TH.Dec
      instanceDec :: Dec
instanceDec = 
        Name -> [Clause] -> Dec
TH.FunD 'pretty 
        ([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 -> 𝐿 Pat
forall a t. Single a t => a -> t
single (Pat -> 𝐿 Pat) -> Pat -> 𝐿 Pat
forall a b. (a -> b) -> a -> b
$ Name -> [FieldPat] -> Pat
TH.RecP Name
con ([FieldPat] -> Pat) -> [FieldPat] -> Pat
forall a b. (a -> b) -> a -> b
$ 𝐿 (Name ∧ Pat) -> [FieldPat]
forall a b. CHS a b => a -> b
tohs (𝐿 (Name ∧ Pat) -> [FieldPat]) -> 𝐿 (Name ∧ Pat) -> [FieldPat]
forall a b. (a -> b) -> a -> b
$ 𝐿 ((Name ∧ 𝕊) ∧ Name)
-> (((Name ∧ 𝕊) ∧ Name) -> Name ∧ Pat) -> 𝐿 (Name ∧ Pat)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝐿 ((Name ∧ 𝕊) ∧ Name)
fieldNameTmps ((((Name ∧ 𝕊) ∧ Name) -> Name ∧ Pat) -> 𝐿 (Name ∧ Pat))
-> (((Name ∧ 𝕊) ∧ Name) -> Name ∧ Pat) -> 𝐿 (Name ∧ Pat)
forall a b. (a -> b) -> a -> b
$ \ (Name
field :* 𝕊
_name :* Name
tmpˣ) → (Name
field Name -> Pat -> Name ∧ Pat
forall a b. a -> b -> a ∧ b
:* Name -> Pat
TH.VarP Name
tmpˣ)) 
        (Exp -> Clause) -> Exp -> Clause
forall a b. (a -> b) -> a -> b
$ Name -> Exp
TH.VarE 'ppApp 
          Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ (Name -> Exp
TH.VarE 'ppCon Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ (𝕊 -> Exp
thString (𝕊 -> Exp) -> 𝕊 -> Exp
forall a b. (a -> b) -> a -> b
$ String -> 𝕊
forall t. ToIter ℂ t => t -> 𝕊
string (String -> 𝕊) -> String -> 𝕊
forall a b. (a -> b) -> a -> b
$ Name -> String
TH.nameBase Name
con)) 
          Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙$ Name -> Exp
TH.VarE 'list 
          Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙$ [Exp] -> Exp
TH.ListE 
             ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> [Exp]
forall a t. Single a t => a -> t
single 
             (Exp -> [Exp]) -> Exp -> [Exp]
forall a b. (a -> b) -> a -> b
$ Name -> Exp
TH.VarE 'ppRecord 
               Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ (Name -> Exp
TH.VarE 'ppPun Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ 𝕊 -> Exp
thString 𝕊
"⇒") 
               Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙$ Name -> Exp
TH.VarE 'list 
               Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙$ [Exp] -> Exp
TH.ListE 
                  ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ 𝐿 Exp -> [Exp]
forall a b. CHS a b => a -> b
tohs 
                  (𝐿 Exp -> [Exp]) -> 𝐿 Exp -> [Exp]
forall a b. (a -> b) -> a -> b
$ 𝐿 ((Name ∧ 𝕊) ∧ Name) -> (((Name ∧ 𝕊) ∧ Name) -> Exp) -> 𝐿 Exp
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝐿 ((Name ∧ 𝕊) ∧ Name)
fieldNameTmps ((((Name ∧ 𝕊) ∧ Name) -> Exp) -> 𝐿 Exp)
-> (((Name ∧ 𝕊) ∧ Name) -> Exp) -> 𝐿 Exp
forall a b. (a -> b) -> a -> b
$ \ (((Name ∧ 𝕊) ∧ Name) -> (Name ∧ 𝕊) ∧ Name
forall a b. CHS a b => b -> a
frhs → Name
_field :* 𝕊
name :* Name
tmpˣ) → 
                      Name -> Exp
TH.ConE '(:*)
                      Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ (Name -> Exp
TH.VarE 'ppString Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ (𝕊 -> Exp
thString 𝕊
name))
                      Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ (Name -> Exp
TH.VarE 'pretty Exp -> Exp -> Exp
forall a. Apply a => a -> a -> a
⊙ Name -> Exp
TH.VarE Name
tmpˣ)
  𝐿 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. Single a t => a -> t
single (Dec -> 𝐿 Dec) -> Dec -> 𝐿 Dec
forall a b. (a -> b) -> a -> b
$ Maybe Overlap -> Cxt -> Pred -> [Dec] -> Dec
TH.InstanceD (𝑂 Overlap -> Maybe Overlap
forall a b. CHS a b => a -> b
tohs 𝑂 Overlap
forall a. 𝑂 a
None) (𝐿 Pred -> Cxt
forall a b. CHS a b => a -> b
tohs 𝐿 Pred
instanceCx) Pred
instanceTy ([Dec] -> Dec) -> [Dec] -> Dec
forall a b. (a -> b) -> a -> b
$ Dec -> [Dec]
forall a t. Single a t => a -> t
single (Dec -> [Dec]) -> Dec -> [Dec]
forall a b. (a -> b) -> a -> b
$ Dec
instanceDec

makePrettyRecord ∷ TH.Name → TH.Q [TH.Dec]
makePrettyRecord :: Name -> Q [Dec]
makePrettyRecord Name
name = do
  (Cxt
cx :* Name
ty :* 𝐿 (TyVarBndr ())
tyargs :* 𝑂 Pred
_ :* Con
c :* 𝐿 DerivClause
_) ← Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ Con)
   ∧ 𝐿 DerivClause)
-> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ Con)
      ∧ 𝐿 DerivClause)
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ Con)
      ∧ 𝐿 DerivClause)
forall (m :: * -> *) a. Return m => m a -> 𝑂 a -> m a
ifNoneM (IO
  (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ Con)
   ∧ 𝐿 DerivClause)
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ Con)
      ∧ 𝐿 DerivClause)
forall a. IO a -> Q a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io IO
  (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ Con)
   ∧ 𝐿 DerivClause)
forall a. IO a
abortIO) (𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ Con)
    ∧ 𝐿 DerivClause)
 -> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ Con)
       ∧ 𝐿 DerivClause))
-> (Info
    -> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ Con)
          ∧ 𝐿 DerivClause))
-> Info
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ Con)
      ∧ 𝐿 DerivClause)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (Dec
-> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ Con)
      ∧ 𝐿 DerivClause)
thViewSingleConADT (Dec
 -> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ Con)
       ∧ 𝐿 DerivClause))
-> (Info -> 𝑂 Dec)
-> Info
-> 𝑂 (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ 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 ())) ∧ 𝑂 Pred) ∧ Con)
       ∧ 𝐿 DerivClause))
-> Q Info
-> Q (((((Cxt ∧ Name) ∧ 𝐿 (TyVarBndr ())) ∧ 𝑂 Pred) ∧ Con)
      ∧ 𝐿 DerivClause)
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ Name -> Q Info
TH.reify Name
name
  (Name
con :* 𝐿 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
  let fieldfieldtys :: 𝐿 (Name ∧ Pred)
fieldfieldtys = 𝐿 VarStrictType
-> (VarStrictType -> Name ∧ Pred) -> 𝐿 (Name ∧ Pred)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝐿 VarStrictType
fields ((VarStrictType -> Name ∧ Pred) -> 𝐿 (Name ∧ Pred))
-> (VarStrictType -> Name ∧ Pred) -> 𝐿 (Name ∧ Pred)
forall a b. (a -> b) -> a -> b
$ \ (VarStrictType -> (Name ∧ Bang) ∧ Pred
forall a b. CHS a b => b -> a
frhs → Name
field :* Bang
_ :* Pred
fieldty) → (Name
field Name -> Pred -> Name ∧ Pred
forall a b. a -> b -> a ∧ b
:* Pred
fieldty)
  (𝐿 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 (Q (𝐿 Dec) -> Q [Dec]) -> Q (𝐿 Dec) -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ Cxt
-> Name -> 𝐿 (TyVarBndr ()) -> Name -> 𝐿 (Name ∧ Pred) -> Q (𝐿 Dec)
makePrettyRecordLogic Cxt
cx Name
ty 𝐿 (TyVarBndr ())
tyargs Name
con 𝐿 (Name ∧ Pred)
fieldfieldtys