{-# 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 fname :: Name
fname = do
    TyConI (DataD _cxt :: Cxt
_cxt tname :: Name
tname targs :: [TyVarBndr]
targs _ constrs :: [Con]
constrs _deriving :: [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 -> Name
tyVarBndrName (TyVarBndr -> Name) -> TyVarBndr -> Name
forall a b. (a -> b) -> a -> b
$ [TyVarBndr] -> TyVarBndr
forall a. [a] -> a
last [TyVarBndr]
targs
    let cons :: [((Name, Int), Maybe (Cxt, Type))]
cons = (Con -> ((Name, Int), Maybe (Cxt, Type)))
-> [Con] -> [((Name, Int), Maybe (Cxt, Type))]
forall a b. (a -> b) -> [a] -> [b]
map (Con -> (Name, Int)
abstractConType (Con -> (Name, Int))
-> (Con -> Maybe (Cxt, Type))
-> Con
-> ((Name, Int), Maybe (Cxt, Type))
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Name -> Con -> Maybe (Cxt, Type)
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, Type)) -> Q [Dec])
-> [((Name, Int), Maybe (Cxt, Type))] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Name] -> Name -> ((Name, Int), Maybe (Cxt, Type)) -> Q [Dec]
genSmartConstr ((TyVarBndr -> Name) -> [TyVarBndr] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndr -> Name
tyVarBndrName [TyVarBndr]
targs) Name
tname) [((Name, Int), Maybe (Cxt, Type))]
cons
        where iTp :: Name -> Con -> Maybe (Cxt, Type)
iTp iVar :: Name
iVar (ForallC _ cxt :: Cxt
cxt t :: Con
t) =
                  -- Check if the GADT phantom type is constrained
                  case [Type
y | AppT (AppT (ConT eqN :: Name
eqN) x :: Type
x) y :: Type
y <- Cxt
cxt, Type
x Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Type
VarT Name
iVar, Name
eqN Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''(~)] of
                    [] -> Name -> Con -> Maybe (Cxt, Type)
iTp Name
iVar Con
t
                    tp :: Type
tp:_ ->
                      let args :: Cxt
args = case Con
t of
                            NormalC _ vs :: [BangType]
vs -> (BangType -> Type) -> [BangType] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Type
forall a b. (a, b) -> b
snd [BangType]
vs
                            RecC _ vs :: [VarBangType]
vs -> (VarBangType -> Type) -> [VarBangType] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (\(_, _, v :: Type
v) -> Type
v) [VarBangType]
vs
                            _ -> []
                      in (Cxt, Type) -> Maybe (Cxt, Type)
forall a. a -> Maybe a
Just (Cxt
args, Type
tp)
              iTp _iVar :: Name
_iVar (GadtC _ vs :: [BangType]
vs (AppT _ tp :: Type
tp)) =
                  case Type
tp of
                    VarT _ -> Maybe (Cxt, Type)
forall a. Maybe a
Nothing
                    _      -> (Cxt, Type) -> Maybe (Cxt, Type)
forall a. a -> Maybe a
Just ((BangType -> Type) -> [BangType] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Type
forall a b. (a, b) -> b
snd [BangType]
vs, Type
tp)
              iTp _iVar :: Name
_iVar (RecGadtC _ vs :: [VarBangType]
vs (AppT _ tp :: Type
tp)) =
                  case Type
tp of
                    VarT _ -> Maybe (Cxt, Type)
forall a. Maybe a
Nothing
                    _      -> (Cxt, Type) -> Maybe (Cxt, Type)
forall a. a -> Maybe a
Just ((VarBangType -> Type) -> [VarBangType] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (\(_, _, v :: Type
v) -> Type
v) [VarBangType]
vs, Type
tp)
              iTp _ _ = Maybe (Cxt, Type)
forall a. Maybe a
Nothing
              genSmartConstr :: [Name] -> Name -> ((Name, Int), Maybe (Cxt, Type)) -> Q [Dec]
genSmartConstr targs :: [Name]
targs tname :: Name
tname ((name :: Name
name, args :: Int
args), miTp :: Maybe (Cxt, Type)
miTp) = do
                let bname :: String
bname = Name -> String
nameBase Name
name
                [Name]
-> Name -> Name -> Name -> Int -> Maybe (Cxt, Type) -> Q [Dec]
genSmartConstr' [Name]
targs Name
tname (String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ 'i' Char -> String -> String
forall a. a -> [a] -> [a]
: String
bname) Name
name Int
args Maybe (Cxt, Type)
miTp
              genSmartConstr' :: [Name]
-> Name -> Name -> Name -> Int -> Maybe (Cxt, Type) -> Q [Dec]
genSmartConstr' targs :: [Name]
targs tname :: Name
tname sname :: Name
sname name :: Name
name args :: Int
args miTp :: Maybe (Cxt, Type)
miTp = do
                [Name]
varNs <- Int -> String -> Q [Name]
newNames Int
args "x"
                let pats :: [PatQ]
pats = (Name -> PatQ) -> [Name] -> [PatQ]
forall a b. (a -> b) -> [a] -> [b]
map Name -> PatQ
varP [Name]
varNs
                    vars :: [ExpQ]
vars = (Name -> ExpQ) -> [Name] -> [ExpQ]
forall a b. (a -> b) -> [a] -> [b]
map Name -> ExpQ
varE [Name]
varNs
                    val :: ExpQ
val = (ExpQ -> ExpQ -> ExpQ) -> ExpQ -> [ExpQ] -> ExpQ
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ExpQ -> ExpQ -> ExpQ
appE (Name -> ExpQ
conE Name
name) [ExpQ]
vars
                    sig :: [Q Dec]
sig = [Name] -> Name -> Name -> Int -> Maybe (Cxt, Type) -> [Q Dec]
forall p.
[Name] -> Name -> Name -> p -> Maybe (Cxt, Type) -> [Q Dec]
genSig [Name]
targs Name
tname Name
sname Int
args Maybe (Cxt, Type)
miTp
                    body :: ExpQ
body = ExpQ -> ((Cxt, Type) -> ExpQ) -> Maybe (Cxt, Type) -> ExpQ
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [|inject $val|] (ExpQ -> (Cxt, Type) -> ExpQ
forall a b. a -> b -> a
const [|injectF $val|]) Maybe (Cxt, Type)
miTp
                    function :: [Q Dec]
function = [Name -> [ClauseQ] -> Q Dec
funD Name
sname [[PatQ] -> BodyQ -> [Q Dec] -> ClauseQ
clause [PatQ]
pats (ExpQ -> BodyQ
normalB ExpQ
body) []]]
                [Q Dec] -> Q [Dec]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t 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 -> p -> Maybe (Cxt, Type) -> [Q Dec]
genSig targs :: [Name]
targs tname :: Name
tname sname :: Name
sname tys :: p
tys miTp :: Maybe (Cxt, Type)
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
newName "fs"
                Name
hvar <- String -> Q Name
newName "h"
                Name
avar <- String -> Q Name
newName "a"
                Name
jvar <- String -> Q Name
newName "j"
                let targs' :: [Name]
targs' = [Name] -> [Name]
forall a. [a] -> [a]
init ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ [Name] -> [Name]
forall a. [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 :: TypeQ
fs = Name -> TypeQ
varT Name
fsvar
                    h :: TypeQ
h = Name -> TypeQ
varT Name
hvar
                    a :: TypeQ
a = Name -> TypeQ
varT Name
avar
                    j :: TypeQ
j = Name -> TypeQ
varT Name
jvar
                    ftype :: TypeQ
ftype = (TypeQ -> TypeQ -> TypeQ) -> TypeQ -> [TypeQ] -> TypeQ
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl TypeQ -> TypeQ -> TypeQ
appT (Name -> TypeQ
conT Name
tname) ((Name -> TypeQ) -> [Name] -> [TypeQ]
forall a b. (a -> b) -> [a] -> [b]
map Name -> TypeQ
varT [Name]
targs')
                    typGen :: TypeQ
typGen = (TypeQ -> TypeQ -> TypeQ) -> TypeQ -> [TypeQ] -> TypeQ
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl TypeQ -> TypeQ -> TypeQ
appT (Name -> TypeQ
conT ''CxtS) [TypeQ
h, TypeQ
fs, TypeQ
a]
                    args :: [TypeQ]
args = case (Cxt, Type) -> Cxt
forall a b. (a, b) -> a
fst ((Cxt, Type) -> Cxt) -> Maybe (Cxt, Type) -> Maybe Cxt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Cxt, Type)
miTp of
                      Nothing -> []
                      Just as :: Cxt
as -> (Type -> TypeQ) -> Cxt -> [TypeQ]
forall a b. (a -> b) -> [a] -> [b]
map (TypeQ -> TypeQ -> TypeQ -> Type -> TypeQ
mkArgType TypeQ
h TypeQ
fs TypeQ
a) Cxt
as
                    typ :: TypeQ
typ = [TypeQ] -> TypeQ
arrow ([TypeQ]
args [TypeQ] -> [TypeQ] -> [TypeQ]
forall a. [a] -> [a] -> [a]
++ [TypeQ -> TypeQ -> TypeQ
appT TypeQ
typGen TypeQ
j])
                    constr :: TypeQ
constr = Name -> [TypeQ] -> TypeQ
classP ''(:-<:) [TypeQ
ftype, TypeQ
fs]
                    constr' :: TypeQ
constr' = Name -> [TypeQ] -> TypeQ
classP ''InjF [TypeQ
fs, TypeQ -> ((Cxt, Type) -> TypeQ) -> Maybe (Cxt, Type) -> TypeQ
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TypeQ
j (Type -> TypeQ
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> TypeQ) -> ((Cxt, Type) -> Type) -> (Cxt, Type) -> TypeQ
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cxt, Type) -> Type
forall a b. (a, b) -> b
snd) Maybe (Cxt, Type)
miTp, TypeQ
j]
                    typeSig :: TypeQ
typeSig = [TyVarBndr] -> CxtQ -> TypeQ -> TypeQ
forallT ((Name -> TyVarBndr) -> [Name] -> [TyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map Name -> TyVarBndr
PlainTV [Name]
vars) ([TypeQ] -> CxtQ
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [TypeQ
constr, TypeQ
constr']) TypeQ
typ
                Name -> TypeQ -> Q Dec
sigD Name
sname TypeQ
typeSig

              mkArgType :: TypeQ -> TypeQ -> TypeQ -> Type -> TypeQ
mkArgType h :: TypeQ
h fs :: TypeQ
fs a :: TypeQ
a (AppT (VarT _) t :: Type
t) =
                -- NOTE: e ( .. ) case
                (TypeQ -> TypeQ -> TypeQ) -> TypeQ -> [TypeQ] -> TypeQ
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl TypeQ -> TypeQ -> TypeQ
appT (Name -> TypeQ
conT ''CxtS) [TypeQ
h, TypeQ
fs, TypeQ
a, Type -> TypeQ
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t]
              mkArgType _ _ _ t :: Type
t =
                Type -> TypeQ
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
              arrow :: [TypeQ] -> TypeQ
arrow =
                (TypeQ -> TypeQ -> TypeQ) -> [TypeQ] -> TypeQ
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\a :: TypeQ
a acc :: TypeQ
acc -> TypeQ
arrowT TypeQ -> TypeQ -> TypeQ
`appT` TypeQ
a TypeQ -> TypeQ -> TypeQ
`appT` TypeQ
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
cxt name :: Name
name args :: [TyVarBndr]
args mk :: Maybe Type
mk constr :: Con
constr derive :: [DerivClause]
derive))
    = Dec -> Info
TyConI (Cxt
-> Name
-> [TyVarBndr]
-> Maybe Type
-> [Con]
-> [DerivClause]
-> Dec
DataD Cxt
cxt Name
name [TyVarBndr]
args Maybe Type
mk [Con
constr] [DerivClause]
derive)
abstractNewtype owise :: 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 constr :: Name
constr args :: [BangType]
args) = (Name
constr, [BangType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [BangType]
args)
abstractConType (RecC constr :: Name
constr args :: [VarBangType]
args) = (Name
constr, [VarBangType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [VarBangType]
args)
abstractConType (InfixC _ constr :: Name
constr _) = (Name
constr, 2)
abstractConType (ForallC _ _ constr :: Con
constr) = Con -> (Name, Int)
abstractConType Con
constr
abstractConType (GadtC [constr :: Name
constr] args :: [BangType]
args _) = (Name
constr, [BangType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [BangType]
args)
abstractConType (RecGadtC [constr :: Name
constr] args :: [VarBangType]
args _) = (Name
constr, [VarBangType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [VarBangType]
args)

{-|
  This function returns the name of a bound type variable
-}
tyVarBndrName :: TyVarBndr -> Name
tyVarBndrName (PlainTV n :: Name
n) = Name
n
tyVarBndrName (KindedTV n :: Name
n _) = 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 n :: Int
n name :: String
name = Int -> Q Name -> Q [Name]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (String -> Q Name
newName String
name)