module Data.Binding.Hobbits.NuMatching (
NuMatching(..), mkNuMatching, NuMatchingList(..), NuMatching1(..),
MbTypeRepr()
) where
import Language.Haskell.TH hiding (Name)
import qualified Language.Haskell.TH as TH
import Control.Monad.State
import Data.Type.RList
import Data.Binding.Hobbits.Internal.Name
import Data.Binding.Hobbits.Internal.Mb
import Data.Binding.Hobbits.Internal.Closed
mapNames :: NuMatching a => MapRList Name ctx -> MapRList Name ctx -> a -> a
mapNames = mapNamesPf nuMatchingProof
class NuMatching a where
nuMatchingProof :: MbTypeRepr a
instance NuMatching (Name a) where
nuMatchingProof = MbTypeReprName
instance NuMatching (Cl a) where
nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
instance (NuMatching a, NuMatching b) => NuMatching (a -> b) where
nuMatchingProof = MbTypeReprFun nuMatchingProof nuMatchingProof
instance NuMatching a => NuMatching (Mb ctx a) where
nuMatchingProof = MbTypeReprMb nuMatchingProof
instance NuMatching Int where
nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
instance NuMatching Integer where
nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
instance NuMatching Char where
nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
instance NuMatching () where
nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
instance (NuMatching a, NuMatching b) => NuMatching (a,b) where
nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 (a,b) -> (mapNames c1 c2 a, mapNames c1 c2 b)))
instance (NuMatching a, NuMatching b, NuMatching c) => NuMatching (a,b,c) where
nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 (a,b,c) -> (mapNames c1 c2 a, mapNames c1 c2 b, mapNames c1 c2 c)))
instance (NuMatching a, NuMatching b, NuMatching c, NuMatching d) => NuMatching (a,b,c,d) where
nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 (a,b,c,d) -> (mapNames c1 c2 a, mapNames c1 c2 b, mapNames c1 c2 c, mapNames c1 c2 d)))
instance (NuMatching a, NuMatching b) => NuMatching (Either a b) where
nuMatchingProof = MbTypeReprData
(MkMbTypeReprData
$ (\c1 c2 x -> case x of
Left l -> Left (mapNames c1 c2 l)
Right r -> Right (mapNames c1 c2 r)))
instance NuMatching a => NuMatching [a] where
nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> map (mapNames c1 c2)))
instance NuMatching (Member c a) where
nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
data NuMatchingObj a = NuMatching a => NuMatchingObj ()
class NuMatchingList args where
nuMatchingListProof :: MapRList NuMatchingObj args
instance NuMatchingList RNil where
nuMatchingListProof = MNil
instance (NuMatchingList args, NuMatching a) => NuMatchingList (args :> a) where
nuMatchingListProof = nuMatchingListProof :>: NuMatchingObj ()
class NuMatching1 f where
nuMatchingProof1 :: NuMatching a => NuMatchingObj (f a)
instance (NuMatching1 f, NuMatchingList ctx) => NuMatching (MapRList f ctx) where
nuMatchingProof = MbTypeReprData $ MkMbTypeReprData $ helper nuMatchingListProof where
helper :: NuMatching1 f =>
MapRList NuMatchingObj args -> MapRList Name ctx1 ->
MapRList Name ctx1 -> MapRList f args -> MapRList f args
helper MNil c1 c2 MNil = MNil
helper (proofs :>: NuMatchingObj ()) c1 c2 (elems :>: (elem :: f a)) =
case nuMatchingProof1 :: NuMatchingObj (f a) of
NuMatchingObj () ->
(helper proofs c1 c2 elems) :>:
mapNames c1 c2 elem
natsFrom i = i : natsFrom (i+1)
fst3 :: (a,b,c) -> a
fst3 (x,_,_) = x
snd3 :: (a,b,c) -> b
snd3 (_,y,_) = y
thd3 :: (a,b,c) -> c
thd3 (_,_,z) = z
type Names = (TH.Name, TH.Name, TH.Name, TH.Name)
mapNamesType a = [t| forall ctx. MapRList Name ctx -> MapRList Name ctx -> $a -> $a |]
mkNuMatching :: Q Type -> Q [Dec]
mkNuMatching tQ =
do t <- tQ
(cxt, cType, tName, constrs, tyvars) <- getMbTypeReprInfoTop t
fName <- newName "f"
x1Name <- newName "x1"
x2Name <- newName "x2"
clauses <- mapM (getClause (tName, fName, x1Name, x2Name)) constrs
mapNamesT <- mapNamesType (return cType)
return [InstanceD
cxt (AppT (ConT ''NuMatching) cType)
[ValD (VarP 'nuMatchingProof)
(NormalB
$ AppE (ConE 'MbTypeReprData)
$ AppE (ConE 'MkMbTypeReprData)
$ LetE [SigD fName
$ ForallT (map PlainTV tyvars) cxt mapNamesT,
FunD fName clauses]
(VarE fName)) []]]
where
tyBndrToName (PlainTV n) = n
tyBndrToName (KindedTV n _) = n
getMbTypeReprInfoFail t extraMsg =
fail ("mkMbTypeRepr: " ++ show t
++ " is not a type constructor for a (G)ADT applied to zero or more distinct type variables" ++ extraMsg)
getMbTypeReprInfoTop t = getMbTypeReprInfo [] [] t t
getMbTypeReprInfo ctx tyvars topT (ConT tName) =
do info <- reify tName
case info of
TyConI (DataD _ _ tyvarsReq constrs _) ->
success tyvarsReq constrs
TyConI (NewtypeD _ _ tyvarsReq constr _) ->
success tyvarsReq [constr]
_ -> getMbTypeReprInfoFail topT (": info for " ++ (show tName) ++ " = " ++ (show info))
where
success tyvarsReq constrs =
let tyvarsRet = if tyvars == [] && ctx == []
then map tyBndrToName tyvarsReq
else tyvars in
return (ctx,
foldl AppT (ConT tName) (map VarT tyvars),
tName, constrs, tyvarsRet)
getMbTypeReprInfo ctx tyvars topT (AppT f (VarT argName)) =
if elem argName tyvars then
getMbTypeReprInfoFail topT ""
else
getMbTypeReprInfo ctx (argName:tyvars) topT f
getMbTypeReprInfo ctx tyvars topT (ForallT _ ctx' t) =
getMbTypeReprInfo (ctx ++ ctx') tyvars topT t
getMbTypeReprInfo ctx tyvars topT t = getMbTypeReprInfoFail topT ""
getTCtor t = getTCtorHelper t t []
getTCtorHelper (ConT tName) topT tyvars = Just (topT, tName, tyvars)
getTCtorHelper (AppT t1 (VarT var)) topT tyvars =
getTCtorHelper t1 topT (tyvars ++ [var])
getTCtorHelper (SigT t1 _) topT tyvars = getTCtorHelper t1 topT tyvars
getTCtorHelper _ _ _ = Nothing
getClauses :: Names -> [Con] -> Q [Clause]
getClauses names constrs = mapM (getClause names) constrs
getClause :: Names -> Con -> Q Clause
getClause names (NormalC cName cTypes) =
getClauseHelper names (map snd cTypes)
(natsFrom 0)
(\l -> ConP cName (map (VarP . fst3) l))
(\l -> foldl AppE (ConE cName) (map fst3 l))
getClause names (RecC cName cVarTypes) =
getClauseHelper names (map thd3 cVarTypes)
(map fst3 cVarTypes)
(\l -> RecP cName
(map (\(var,_,field) -> (field, VarP var)) l))
(\l -> RecConE cName
(map (\(exp,_,field) -> (field, exp)) l))
getClause names (InfixC cType1 cName cType2) =
undefined
getClause names (ForallC _ _ con) = getClause names con
getClauseHelper :: Names -> [Type] -> [a] ->
([(TH.Name,Type,a)] -> Pat) ->
([(Exp,Type,a)] -> Exp) ->
Q Clause
getClauseHelper names@(tName, fName, x1Name, x2Name) cTypes cData pFun eFun =
do varNames <- mapM (newName . ("x" ++) . show . fst)
$ zip (natsFrom 0) cTypes
let varsTypesData = zip3 varNames cTypes cData
let expsTypesData = map (mkExpTypeData names) varsTypesData
return $ Clause [(VarP x1Name), (VarP x2Name), (pFun varsTypesData)]
(NormalB $ eFun expsTypesData) []
mkExpTypeData :: Names -> (TH.Name,Type,a) -> (Exp,Type,a)
mkExpTypeData (tName, fName, x1Name, x2Name)
(varName, getTCtor -> Just (t, tName', _), cData)
| tName == tName' =
(foldl AppE (VarE fName)
[(VarE x1Name), (VarE x2Name), (VarE varName)],
t, cData)
mkExpTypeData (tName, fName, x1Name, x2Name) (varName, t, cData) =
(foldl AppE (VarE 'mapNames)
[(VarE x1Name), (VarE x2Name), (VarE varName)],
t, cData)
type CxtStateQ a = StateT Cxt Q a
mkMkMbTypeReprDataOld :: Q TH.Name -> Q Exp
mkMkMbTypeReprDataOld conNameQ =
do conName <- conNameQ
(cxt, name, tyvars, constrs) <- getMbTypeReprInfo conName
(clauses, reqCxt) <- runStateT (getClauses cxt name tyvars constrs) []
fname <- newName "f"
return (LetE
[SigD fname
(ForallT tyvars reqCxt
$ foldl AppT ArrowT
[foldl AppT (ConT conName)
(map tyVarToType tyvars)]),
FunD fname clauses]
(VarE fname))
where
tyVarToType (PlainTV n) = VarT n
tyVarToType (KindedTV n _) = VarT n
getMbTypeReprInfo conName =
reify conName >>= \info ->
case info of
TyConI (DataD cxt name tyvars constrs _) ->
return (cxt, name, tyvars, constrs)
_ -> fail ("mkMkMbTypeReprData: " ++ show conName
++ " is not a (G)ADT")
getClauses :: Cxt -> TH.Name -> [TyVarBndr] -> [Con] -> CxtStateQ [Clause]
getClauses cxt name tyvars constrs =
mapM (getClause cxt name tyvars []) constrs
getClause :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] -> Con ->
CxtStateQ Clause
getClause cxt name tyvars locTyvars (NormalC cName cTypes) =
getClauseHelper cxt name tyvars locTyvars (map snd cTypes)
(natsFrom 0)
(\l -> ConP cName (map (VarP . fst3) l))
(\l -> foldl AppE (ConE cName) (map (VarE . fst3) l))
getClause cxt name tyvars locTyvars (RecC cName cVarTypes) =
getClauseHelper cxt name tyvars locTyvars (map thd3 cVarTypes)
(map fst3 cVarTypes)
(\l -> RecP cName
(map (\(var,_,field) -> (field, VarP var)) l))
(\l -> RecConE cName
(map (\(var,_,field) -> (field, VarE var)) l))
getClause cxt name tyvars locTyvars (InfixC cType1 cName cType2) =
undefined
getClause cxt name tyvars locTyvars (ForallC tyvars2 cxt2 con) =
getClause (cxt ++ cxt2) name tyvars (locTyvars ++ tyvars2) con
getClauseHelper :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] ->
[Type] -> [a] ->
([(TH.Name,Type,a)] -> Pat) ->
([(TH.Name,Type,a)] -> Exp) ->
CxtStateQ Clause
getClauseHelper cxt name tyvars locTyvars cTypes cData pFun eFun =
do varNames <- mapM (lift . newName . ("x" ++) . show . fst)
$ zip (natsFrom 0) cTypes
() <- ensureCxt cxt locTyvars cTypes
let varsTypesData = zip3 varNames cTypes cData
return $ Clause [(pFun varsTypesData)]
(NormalB $ eFun varsTypesData) []
ensureCxt :: Cxt -> [TyVarBndr] -> [Type] -> CxtStateQ ()
ensureCxt cxt locTyvars cTypes =
foldM (const (ensureCxt1 cxt locTyvars)) () cTypes
ensureCxt1 :: Cxt -> [TyVarBndr] -> Type -> CxtStateQ ()
ensureCxt1 cxt locTyvars t = undefined