{-# LANGUAGE TemplateHaskell #-}

{-|
   This is part of an experiment in using sort-inclusions (i.e. injf) in parametric syntax.
   This file is sinful because it is a code-clone of the smartConstructors generator in the compdata library,
   and also copies Data.Comp.Derive.Utils verbatim
  
   After being validated and reaching maturity, this should be pull-requested in to the real compdata
   library (or the alternative, perhaps better solution, of redefining inject to what is currently called injectF)
 -}

module Cubix.Sin.Compdata.Derive (
    smartFConstructors
  ) where

import Control.Arrow ( (&&&) )
import Control.Monad

import Data.Comp.Multi.Sum
import Data.Comp.Multi.Term

import Language.Haskell.TH hiding ( Cxt )

import Cubix.Language.Parametric.InjF ( InjF, injectF )

smartFConstructors :: Name -> Q [Dec]
smartFConstructors :: Name -> Q [Dec]
smartFConstructors Name
fname = do
    TyConI (DataD Cxt
_cxt Name
tname [TyVarBndr BndrVis]
targs Maybe Kind
_ [Con]
constrs [DerivClause]
_deriving) <- Q Info -> Q Info
abstractNewtypeQ (Q Info -> Q Info) -> Q Info -> Q Info
forall a b. (a -> b) -> a -> b
$ Name -> Q Info
reify Name
fname
    let iVar :: Name
iVar = TyVarBndr BndrVis -> Name
forall {flag}. TyVarBndr flag -> Name
tyVarBndrName (TyVarBndr BndrVis -> Name) -> TyVarBndr BndrVis -> Name
forall a b. (a -> b) -> a -> b
$ [TyVarBndr BndrVis] -> TyVarBndr BndrVis
forall a. HasCallStack => [a] -> a
last [TyVarBndr BndrVis]
targs
    let cons :: [((Name, Int), Maybe (Cxt, Kind))]
cons = (Con -> ((Name, Int), Maybe (Cxt, Kind)))
-> [Con] -> [((Name, Int), Maybe (Cxt, Kind))]
forall a b. (a -> b) -> [a] -> [b]
map (Con -> (Name, Int)
abstractConType (Con -> (Name, Int))
-> (Con -> Maybe (Cxt, Kind))
-> Con
-> ((Name, Int), Maybe (Cxt, Kind))
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Name -> Con -> Maybe (Cxt, Kind)
iTp Name
iVar) [Con]
constrs
    ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Q [[Dec]] -> Q [Dec]) -> Q [[Dec]] -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ (((Name, Int), Maybe (Cxt, Kind)) -> Q [Dec])
-> [((Name, Int), Maybe (Cxt, Kind))] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([Name] -> Name -> ((Name, Int), Maybe (Cxt, Kind)) -> Q [Dec]
genSmartConstr ((TyVarBndr BndrVis -> Name) -> [TyVarBndr BndrVis] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndr BndrVis -> Name
forall {flag}. TyVarBndr flag -> Name
tyVarBndrName [TyVarBndr BndrVis]
targs) Name
tname) [((Name, Int), Maybe (Cxt, Kind))]
cons
        where iTp :: Name -> Con -> Maybe (Cxt, Kind)
iTp Name
iVar (ForallC [TyVarBndr Specificity]
_ Cxt
cxt Con
t) =
                  -- Check if the GADT phantom type is constrained
                  case [Kind
y | AppT (AppT (ConT Name
eqN) Kind
x) Kind
y <- Cxt
cxt, Kind
x Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Kind
VarT Name
iVar, Name
eqN Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''(~)] of
                    [] -> Name -> Con -> Maybe (Cxt, Kind)
iTp Name
iVar Con
t
                    Kind
tp:Cxt
_ ->
                      let args :: Cxt
args = case Con
t of
                            NormalC Name
_ [BangType]
vs -> (BangType -> Kind) -> [BangType] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Kind
forall a b. (a, b) -> b
snd [BangType]
vs
                            RecC Name
_ [VarBangType]
vs -> (VarBangType -> Kind) -> [VarBangType] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
_, Bang
_, Kind
v) -> Kind
v) [VarBangType]
vs
                            Con
_ -> []
                      in (Cxt, Kind) -> Maybe (Cxt, Kind)
forall a. a -> Maybe a
Just (Cxt
args, Kind
tp)
              iTp Name
_iVar (GadtC [Name]
_ [BangType]
vs (AppT Kind
_ Kind
tp)) =
                  case Kind
tp of
                    VarT Name
_ -> Maybe (Cxt, Kind)
forall a. Maybe a
Nothing
                    Kind
_      -> (Cxt, Kind) -> Maybe (Cxt, Kind)
forall a. a -> Maybe a
Just ((BangType -> Kind) -> [BangType] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Kind
forall a b. (a, b) -> b
snd [BangType]
vs, Kind
tp)
              iTp Name
_iVar (RecGadtC [Name]
_ [VarBangType]
vs (AppT Kind
_ Kind
tp)) =
                  case Kind
tp of
                    VarT Name
_ -> Maybe (Cxt, Kind)
forall a. Maybe a
Nothing
                    Kind
_      -> (Cxt, Kind) -> Maybe (Cxt, Kind)
forall a. a -> Maybe a
Just ((VarBangType -> Kind) -> [VarBangType] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
_, Bang
_, Kind
v) -> Kind
v) [VarBangType]
vs, Kind
tp)
              iTp Name
_ Con
_ = Maybe (Cxt, Kind)
forall a. Maybe a
Nothing
              genSmartConstr :: [Name] -> Name -> ((Name, Int), Maybe (Cxt, Kind)) -> Q [Dec]
genSmartConstr [Name]
targs Name
tname ((Name
name, Int
args), Maybe (Cxt, Kind)
miTp) = do
                let bname :: String
bname = Name -> String
nameBase Name
name
                [Name]
-> Name -> Name -> Name -> Int -> Maybe (Cxt, Kind) -> Q [Dec]
genSmartConstr' [Name]
targs Name
tname (String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ Char
'i' Char -> String -> String
forall a. a -> [a] -> [a]
: String
bname) Name
name Int
args Maybe (Cxt, Kind)
miTp
              genSmartConstr' :: [Name]
-> Name -> Name -> Name -> Int -> Maybe (Cxt, Kind) -> Q [Dec]
genSmartConstr' [Name]
targs Name
tname Name
sname Name
name Int
args Maybe (Cxt, Kind)
miTp = do
                [Name]
varNs <- Int -> String -> Q [Name]
newNames Int
args String
"x"
                let pats :: [Q Pat]
pats = (Name -> Q Pat) -> [Name] -> [Q Pat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Q Pat
forall (m :: * -> *). Quote m => Name -> m Pat
varP [Name]
varNs
                    vars :: [Q Exp]
vars = (Name -> Q Exp) -> [Name] -> [Q Exp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
varE [Name]
varNs
                    val :: Q Exp
val = (Q Exp -> Q Exp -> Q Exp) -> Q Exp -> [Q Exp] -> Q Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Q Exp -> Q Exp -> Q Exp
forall (m :: * -> *). Quote m => m Exp -> m Exp -> m Exp
appE (Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
conE Name
name) [Q Exp]
vars
                    sig :: [Q Dec]
sig = [Name] -> Name -> Name -> Int -> Maybe (Cxt, Kind) -> [Q Dec]
genSig [Name]
targs Name
tname Name
sname Int
args Maybe (Cxt, Kind)
miTp
                    body :: Q Exp
body = Q Exp -> ((Cxt, Kind) -> Q Exp) -> Maybe (Cxt, Kind) -> Q Exp
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [|inject $Q Exp
val|] (Q Exp -> (Cxt, Kind) -> Q Exp
forall a b. a -> b -> a
const [|injectF $Q Exp
val|]) Maybe (Cxt, Kind)
miTp
                    function :: [Q Dec]
function = [Name -> [Q Clause] -> Q Dec
forall (m :: * -> *). Quote m => Name -> [m Clause] -> m Dec
funD Name
sname [[Q Pat] -> Q Body -> [Q Dec] -> Q Clause
forall (m :: * -> *).
Quote m =>
[m Pat] -> m Body -> [m Dec] -> m Clause
clause [Q Pat]
pats (Q Exp -> Q Body
forall (m :: * -> *). Quote m => m Exp -> m Body
normalB Q Exp
body) []]]
                [Q Dec] -> Q [Dec]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([Q Dec] -> Q [Dec]) -> [Q Dec] -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ [Q Dec]
sig [Q Dec] -> [Q Dec] -> [Q Dec]
forall a. [a] -> [a] -> [a]
++ [Q Dec]
function
              genSig :: [Name] -> Name -> Name -> Int -> Maybe (Cxt, Kind) -> [Q Dec]
genSig [Name]
targs Name
tname Name
sname Int
tys Maybe (Cxt, Kind)
miTp = (Q Dec -> [Q Dec] -> [Q Dec]
forall a. a -> [a] -> [a]
:[]) (Q Dec -> [Q Dec]) -> Q Dec -> [Q Dec]
forall a b. (a -> b) -> a -> b
$ do
                Name
fsvar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"fs"
                Name
hvar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"h"
                Name
avar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"a"
                Name
jvar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"j"
                let targs' :: [Name]
targs' = [Name] -> [Name]
forall a. HasCallStack => [a] -> [a]
init ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ [Name] -> [Name]
forall a. HasCallStack => [a] -> [a]
init [Name]
targs
                    vars :: [Name]
vars = Name
hvarName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:Name
fsvarName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:Name
avarName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name
jvar][Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++[Name]
targs'
                    fs :: Q Kind
fs = Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
varT Name
fsvar
                    h :: Q Kind
h = Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
varT Name
hvar
                    a :: Q Kind
a = Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
varT Name
avar
                    j :: Q Kind
j = Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
varT Name
jvar
                    ftype :: Q Kind
ftype = (Q Kind -> Q Kind -> Q Kind) -> Q Kind -> [Q Kind] -> Q Kind
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
appT (Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
conT Name
tname) ((Name -> Q Kind) -> [Name] -> [Q Kind]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
varT [Name]
targs')
                    typGen :: Q Kind
typGen = (Q Kind -> Q Kind -> Q Kind) -> Q Kind -> [Q Kind] -> Q Kind
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
appT (Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
conT ''CxtS) [Q Kind
h, Q Kind
fs, Q Kind
a]
                    args :: [Q Kind]
args = case (Cxt, Kind) -> Cxt
forall a b. (a, b) -> a
fst ((Cxt, Kind) -> Cxt) -> Maybe (Cxt, Kind) -> Maybe Cxt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Cxt, Kind)
miTp of
                      Maybe Cxt
Nothing -> []
                      Just Cxt
as -> (Kind -> Q Kind) -> Cxt -> [Q Kind]
forall a b. (a -> b) -> [a] -> [b]
map (Q Kind -> Q Kind -> Q Kind -> Kind -> Q Kind
forall {m :: * -> *}.
Quote m =>
m Kind -> m Kind -> m Kind -> Kind -> m Kind
mkArgType Q Kind
h Q Kind
fs Q Kind
a) Cxt
as
                    typ :: Q Kind
typ = [Q Kind] -> Q Kind
arrow ([Q Kind]
args [Q Kind] -> [Q Kind] -> [Q Kind]
forall a. [a] -> [a] -> [a]
++ [Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
appT Q Kind
typGen Q Kind
j])
                    constr :: Q Kind
constr = Name -> [Q Kind] -> Q Kind
forall (m :: * -> *). Quote m => Name -> [m Kind] -> m Kind
classP ''(:-<:) [Q Kind
ftype, Q Kind
fs]
                    constr' :: Q Kind
constr' = Name -> [Q Kind] -> Q Kind
forall (m :: * -> *). Quote m => Name -> [m Kind] -> m Kind
classP ''InjF [Q Kind
fs, Q Kind -> ((Cxt, Kind) -> Q Kind) -> Maybe (Cxt, Kind) -> Q Kind
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Q Kind
j (Kind -> Q Kind
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind -> Q Kind) -> ((Cxt, Kind) -> Kind) -> (Cxt, Kind) -> Q Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cxt, Kind) -> Kind
forall a b. (a, b) -> b
snd) Maybe (Cxt, Kind)
miTp, Q Kind
j]

                    -- NOTE 2023.06.29: Unsure if SpecifiedSpec is what we want here to get working type applications
                    typeSig :: Q Kind
typeSig = [TyVarBndr Specificity] -> Q Cxt -> Q Kind -> Q Kind
forall (m :: * -> *).
Quote m =>
[TyVarBndr Specificity] -> m Cxt -> m Kind -> m Kind
forallT ((Name -> TyVarBndr Specificity)
-> [Name] -> [TyVarBndr Specificity]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
v -> Name -> Specificity -> TyVarBndr Specificity
forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
v Specificity
SpecifiedSpec) [Name]
vars) ([Q Kind] -> Q Cxt
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [Q Kind
constr, Q Kind
constr']) Q Kind
typ
                Name -> Q Kind -> Q Dec
forall (m :: * -> *). Quote m => Name -> m Kind -> m Dec
sigD Name
sname Q Kind
typeSig

              mkArgType :: m Kind -> m Kind -> m Kind -> Kind -> m Kind
mkArgType m Kind
h m Kind
fs m Kind
a (AppT (VarT Name
_) Kind
t) =
                -- NOTE: e ( .. ) case
                (m Kind -> m Kind -> m Kind) -> m Kind -> [m Kind] -> m Kind
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl m Kind -> m Kind -> m Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
appT (Name -> m Kind
forall (m :: * -> *). Quote m => Name -> m Kind
conT ''CxtS) [m Kind
h, m Kind
fs, m Kind
a, Kind -> m Kind
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind
t]
              mkArgType m Kind
_ m Kind
_ m Kind
_ Kind
t =
                Kind -> m Kind
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind
t
              arrow :: [Q Kind] -> Q Kind
arrow =
                (Q Kind -> Q Kind -> Q Kind) -> [Q Kind] -> Q Kind
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\Q Kind
a Q Kind
acc -> Q Kind
forall (m :: * -> *). Quote m => m Kind
arrowT Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`appT` Q Kind
a Q Kind -> Q Kind -> Q Kind
forall (m :: * -> *). Quote m => m Kind -> m Kind -> m Kind
`appT` Q Kind
acc)



{-|
  This is the @Q@-lifted version of 'abstractNewtypeQ.
-}
abstractNewtypeQ :: Q Info -> Q Info
abstractNewtypeQ :: Q Info -> Q Info
abstractNewtypeQ = (Info -> Info) -> Q Info -> Q Info
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Info -> Info
abstractNewtype

{-|
  This function abstracts away @newtype@ declaration, it turns them into
  @data@ declarations.
-}
abstractNewtype :: Info -> Info
abstractNewtype :: Info -> Info
abstractNewtype (TyConI (NewtypeD Cxt
cxt Name
name [TyVarBndr BndrVis]
args Maybe Kind
mk Con
constr [DerivClause]
derive))
    = Dec -> Info
TyConI (Cxt
-> Name
-> [TyVarBndr BndrVis]
-> Maybe Kind
-> [Con]
-> [DerivClause]
-> Dec
DataD Cxt
cxt Name
name [TyVarBndr BndrVis]
args Maybe Kind
mk [Con
constr] [DerivClause]
derive)
abstractNewtype Info
owise = Info
owise


{-|
  This function provides the name and the arity of the given data constructor.
-}
abstractConType :: Con -> (Name,Int)
abstractConType :: Con -> (Name, Int)
abstractConType (NormalC Name
constr [BangType]
args) = (Name
constr, [BangType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [BangType]
args)
abstractConType (RecC Name
constr [VarBangType]
args) = (Name
constr, [VarBangType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [VarBangType]
args)
abstractConType (InfixC BangType
_ Name
constr BangType
_) = (Name
constr, Int
2)
abstractConType (ForallC [TyVarBndr Specificity]
_ Cxt
_ Con
constr) = Con -> (Name, Int)
abstractConType Con
constr
abstractConType (GadtC [Name
constr] [BangType]
args Kind
_) = (Name
constr, [BangType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [BangType]
args)
abstractConType (RecGadtC [Name
constr] [VarBangType]
args Kind
_) = (Name
constr, [VarBangType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [VarBangType]
args)

{-|
  This function returns the name of a bound type variable
-}
tyVarBndrName :: TyVarBndr flag -> Name
tyVarBndrName (PlainTV Name
n flag
_) = Name
n
tyVarBndrName (KindedTV Name
n flag
_ Kind
_) = Name
n



{-|
  This function provides a list (of the given length) of new names based
  on the given string.
-}
newNames :: Int -> String -> Q [Name]
newNames :: Int -> String -> Q [Name]
newNames Int
n String
name = Int -> Q Name -> Q [Name]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
name)