{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

-- |
-- Module      : Data.Binding.Hobbits.NuMatching
-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
--
-- License     : BSD3
--
-- Maintainer  : westbrook@kestrel.edu
-- Stability   : experimental
-- Portability : GHC
--
-- This module defines the typeclass @'NuMatching' a@, which allows
-- pattern-matching on the bodies of multi-bindings when their bodies
-- have type a. To ensure adequacy, the actual machinery of how this
-- works is hidden from the user, but, for any given (G)ADT @a@, the
-- user can use the Template Haskell function 'mkNuMatching' to
-- create a 'NuMatching' instance for @a@.
--


module Data.Binding.Hobbits.NuMatching (
  NuMatching(..), mkNuMatching,
  MbTypeRepr(), isoMbTypeRepr, unsafeMbTypeRepr,
  NuMatchingAny1(..)
) where

import Data.Vector (Vector)
import qualified Data.Vector as Vector
--import Data.Typeable
import Language.Haskell.TH hiding (Name, Type(..))
import qualified Language.Haskell.TH as TH
import Control.Monad.State
import Numeric.Natural
import Data.Functor.Constant
import Data.Kind as DK
import Data.Word
import Data.Proxy
import Data.Type.Equality
--import Control.Monad.Identity

import Data.Type.RList hiding (map)
import Data.Binding.Hobbits.Internal.Name
import Data.Binding.Hobbits.Internal.Mb
import Data.Binding.Hobbits.Internal.Closed


{-| Just like 'mapNamesPf', except uses the NuMatching class. -}
mapNames :: NuMatching a => NameRefresher -> a -> a
mapNames :: NameRefresher -> a -> a
mapNames = MbTypeRepr a -> NameRefresher -> a -> a
forall a. MbTypeRepr a -> NameRefresher -> a -> a
mapNamesPf MbTypeRepr a
forall a. NuMatching a => MbTypeRepr a
nuMatchingProof

matchDataDecl :: Dec -> Maybe (Cxt, TH.Name, [TyVarBndr], [Con])
matchDataDecl :: Dec -> Maybe (Cxt, Name, [TyVarBndr], [Con])
matchDataDecl (DataD Cxt
cxt Name
name [TyVarBndr]
tyvars Maybe Kind
_ [Con]
constrs [DerivClause]
_) =
  (Cxt, Name, [TyVarBndr], [Con])
-> Maybe (Cxt, Name, [TyVarBndr], [Con])
forall a. a -> Maybe a
Just (Cxt
cxt, Name
name, [TyVarBndr]
tyvars, [Con]
constrs)
matchDataDecl (NewtypeD Cxt
cxt Name
name [TyVarBndr]
tyvars Maybe Kind
_ Con
constr [DerivClause]
_) =
  (Cxt, Name, [TyVarBndr], [Con])
-> Maybe (Cxt, Name, [TyVarBndr], [Con])
forall a. a -> Maybe a
Just (Cxt
cxt, Name
name, [TyVarBndr]
tyvars, [Con
constr])
matchDataDecl Dec
_ = Maybe (Cxt, Name, [TyVarBndr], [Con])
forall a. Maybe a
Nothing


mkInstanceD :: Cxt -> TH.Type -> [Dec] -> Dec
mkInstanceD :: Cxt -> Kind -> [Dec] -> Dec
mkInstanceD = Maybe Overlap -> Cxt -> Kind -> [Dec] -> Dec
InstanceD Maybe Overlap
forall a. Maybe a
Nothing

{-|
  Instances of the @'NuMatching' a@ class allow pattern-matching on
  multi-bindings whose bodies have type @a@, i.e., on multi-bindings
  of type @'Mb' ctx a@. The structure of this class is mostly hidden
  from the user; see 'mkNuMatching' to see how to create instances
  of the @NuMatching@ class.
-}
class NuMatching a where
    nuMatchingProof :: MbTypeRepr a

-- | Build an 'MbTypeRepr' for type @a@ by using an isomorphism with an
-- already-representable type @b@. This is useful for building 'NuMatching'
-- instances for, e.g., 'Integral' types, by mapping to and from 'Integer',
-- without having to define instances for each one in this module.
isoMbTypeRepr :: NuMatching b => (a -> b) -> (b -> a) -> MbTypeRepr a
isoMbTypeRepr :: (a -> b) -> (b -> a) -> MbTypeRepr a
isoMbTypeRepr a -> b
f_to b -> a
f_from =
  MbTypeReprData a -> MbTypeRepr a
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData (MbTypeReprData a -> MbTypeRepr a)
-> MbTypeReprData a -> MbTypeRepr a
forall a b. (a -> b) -> a -> b
$ (forall (ctx :: Any). NameRefresher -> a -> a) -> MbTypeReprData a
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> a -> a)
 -> MbTypeReprData a)
-> (forall (ctx :: Any). NameRefresher -> a -> a)
-> MbTypeReprData a
forall a b. (a -> b) -> a -> b
$ \NameRefresher
refresher a
a ->
  b -> a
f_from (b -> a) -> b -> a
forall a b. (a -> b) -> a -> b
$ NameRefresher -> b -> b
forall a. NuMatching a => NameRefresher -> a -> a
mapNames NameRefresher
refresher (a -> b
f_to a
a)

-- | Builds an 'MbTypeRepr' proof for use in a 'NuMatching' instance. This proof
-- is unsafe because it does no renaming of fresh names, so should only be used
-- for types that are guaranteed not to contain any 'Name' or 'Mb' values.
unsafeMbTypeRepr :: MbTypeRepr a
unsafeMbTypeRepr :: MbTypeRepr a
unsafeMbTypeRepr = MbTypeReprData a -> MbTypeRepr a
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> a -> a) -> MbTypeReprData a
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> a -> a)
 -> MbTypeReprData a)
-> (forall (ctx :: Any). NameRefresher -> a -> a)
-> MbTypeReprData a
forall a b. (a -> b) -> a -> b
$ (\NameRefresher
_ -> a -> a
forall a. a -> a
id))

instance NuMatching (Name a) where
    nuMatchingProof :: MbTypeRepr (Name a)
nuMatchingProof = MbTypeRepr (Name a)
forall k (a :: k). MbTypeRepr (Name a)
MbTypeReprName

instance NuMatching (Closed a) where
    -- no need to map free variables in a Closed object
    nuMatchingProof :: MbTypeRepr (Closed a)
nuMatchingProof = MbTypeReprData (Closed a) -> MbTypeRepr (Closed a)
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> Closed a -> Closed a)
-> MbTypeReprData (Closed a)
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> Closed a -> Closed a)
 -> MbTypeReprData (Closed a))
-> (forall (ctx :: Any). NameRefresher -> Closed a -> Closed a)
-> MbTypeReprData (Closed a)
forall a b. (a -> b) -> a -> b
$ (\NameRefresher
refresher -> Closed a -> Closed a
forall a. a -> a
id))

instance (NuMatching a, NuMatching b) => NuMatching (a -> b) where
    nuMatchingProof :: MbTypeRepr (a -> b)
nuMatchingProof = MbTypeRepr a -> MbTypeRepr b -> MbTypeRepr (a -> b)
forall a b. MbTypeRepr a -> MbTypeRepr b -> MbTypeRepr (a -> b)
MbTypeReprFun MbTypeRepr a
forall a. NuMatching a => MbTypeRepr a
nuMatchingProof MbTypeRepr b
forall a. NuMatching a => MbTypeRepr a
nuMatchingProof

instance NuMatching a => NuMatching (Mb ctx a) where
    nuMatchingProof :: MbTypeRepr (Mb ctx a)
nuMatchingProof = MbTypeRepr a -> MbTypeRepr (Mb ctx a)
forall k a (ctx :: RList k). MbTypeRepr a -> MbTypeRepr (Mb ctx a)
MbTypeReprMb MbTypeRepr a
forall a. NuMatching a => MbTypeRepr a
nuMatchingProof

instance NuMatching Bool where
    nuMatchingProof :: MbTypeRepr Bool
nuMatchingProof = MbTypeReprData Bool -> MbTypeRepr Bool
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> Bool -> Bool)
-> MbTypeReprData Bool
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> Bool -> Bool)
 -> MbTypeReprData Bool)
-> (forall (ctx :: Any). NameRefresher -> Bool -> Bool)
-> MbTypeReprData Bool
forall a b. (a -> b) -> a -> b
$ (\NameRefresher
_ -> Bool -> Bool
forall a. a -> a
id))

instance NuMatching Int where
    nuMatchingProof :: MbTypeRepr Int
nuMatchingProof = MbTypeReprData Int -> MbTypeRepr Int
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> Int -> Int)
-> MbTypeReprData Int
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> Int -> Int)
 -> MbTypeReprData Int)
-> (forall (ctx :: Any). NameRefresher -> Int -> Int)
-> MbTypeReprData Int
forall a b. (a -> b) -> a -> b
$ (\NameRefresher
_ -> Int -> Int
forall a. a -> a
id))

instance NuMatching Integer where
    nuMatchingProof :: MbTypeRepr Integer
nuMatchingProof = MbTypeReprData Integer -> MbTypeRepr Integer
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> Integer -> Integer)
-> MbTypeReprData Integer
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> Integer -> Integer)
 -> MbTypeReprData Integer)
-> (forall (ctx :: Any). NameRefresher -> Integer -> Integer)
-> MbTypeReprData Integer
forall a b. (a -> b) -> a -> b
$ (\NameRefresher
_ -> Integer -> Integer
forall a. a -> a
id))

instance NuMatching Char where
    nuMatchingProof :: MbTypeRepr Char
nuMatchingProof = MbTypeReprData Char -> MbTypeRepr Char
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> Char -> Char)
-> MbTypeReprData Char
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> Char -> Char)
 -> MbTypeReprData Char)
-> (forall (ctx :: Any). NameRefresher -> Char -> Char)
-> MbTypeReprData Char
forall a b. (a -> b) -> a -> b
$ (\NameRefresher
_ -> Char -> Char
forall a. a -> a
id))

instance NuMatching Natural where
    nuMatchingProof :: MbTypeRepr Natural
nuMatchingProof = MbTypeReprData Natural -> MbTypeRepr Natural
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> Natural -> Natural)
-> MbTypeReprData Natural
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> Natural -> Natural)
 -> MbTypeReprData Natural)
-> (forall (ctx :: Any). NameRefresher -> Natural -> Natural)
-> MbTypeReprData Natural
forall a b. (a -> b) -> a -> b
$ (\NameRefresher
_ -> Natural -> Natural
forall a. a -> a
id))

instance NuMatching Float where
    nuMatchingProof :: MbTypeRepr Float
nuMatchingProof = MbTypeReprData Float -> MbTypeRepr Float
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> Float -> Float)
-> MbTypeReprData Float
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> Float -> Float)
 -> MbTypeReprData Float)
-> (forall (ctx :: Any). NameRefresher -> Float -> Float)
-> MbTypeReprData Float
forall a b. (a -> b) -> a -> b
$ (\NameRefresher
_ -> Float -> Float
forall a. a -> a
id))

instance NuMatching Double where
    nuMatchingProof :: MbTypeRepr Double
nuMatchingProof = MbTypeReprData Double -> MbTypeRepr Double
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> Double -> Double)
-> MbTypeReprData Double
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> Double -> Double)
 -> MbTypeReprData Double)
-> (forall (ctx :: Any). NameRefresher -> Double -> Double)
-> MbTypeReprData Double
forall a b. (a -> b) -> a -> b
$ (\NameRefresher
_ -> Double -> Double
forall a. a -> a
id))

instance NuMatching Word where
    nuMatchingProof :: MbTypeRepr Word
nuMatchingProof = MbTypeReprData Word -> MbTypeRepr Word
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> Word -> Word)
-> MbTypeReprData Word
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> Word -> Word)
 -> MbTypeReprData Word)
-> (forall (ctx :: Any). NameRefresher -> Word -> Word)
-> MbTypeReprData Word
forall a b. (a -> b) -> a -> b
$ (\NameRefresher
_ -> Word -> Word
forall a. a -> a
id))

instance NuMatching Word8 where
    nuMatchingProof :: MbTypeRepr Word8
nuMatchingProof = MbTypeReprData Word8 -> MbTypeRepr Word8
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> Word8 -> Word8)
-> MbTypeReprData Word8
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> Word8 -> Word8)
 -> MbTypeReprData Word8)
-> (forall (ctx :: Any). NameRefresher -> Word8 -> Word8)
-> MbTypeReprData Word8
forall a b. (a -> b) -> a -> b
$ (\NameRefresher
_ -> Word8 -> Word8
forall a. a -> a
id))

instance NuMatching Word16 where
    nuMatchingProof :: MbTypeRepr Word16
nuMatchingProof = MbTypeReprData Word16 -> MbTypeRepr Word16
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> Word16 -> Word16)
-> MbTypeReprData Word16
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> Word16 -> Word16)
 -> MbTypeReprData Word16)
-> (forall (ctx :: Any). NameRefresher -> Word16 -> Word16)
-> MbTypeReprData Word16
forall a b. (a -> b) -> a -> b
$ (\NameRefresher
_ -> Word16 -> Word16
forall a. a -> a
id))

instance NuMatching Word32 where
    nuMatchingProof :: MbTypeRepr Word32
nuMatchingProof = MbTypeReprData Word32 -> MbTypeRepr Word32
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> Word32 -> Word32)
-> MbTypeReprData Word32
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> Word32 -> Word32)
 -> MbTypeReprData Word32)
-> (forall (ctx :: Any). NameRefresher -> Word32 -> Word32)
-> MbTypeReprData Word32
forall a b. (a -> b) -> a -> b
$ (\NameRefresher
_ -> Word32 -> Word32
forall a. a -> a
id))

instance NuMatching Word64 where
    nuMatchingProof :: MbTypeRepr Word64
nuMatchingProof = MbTypeReprData Word64 -> MbTypeRepr Word64
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> Word64 -> Word64)
-> MbTypeReprData Word64
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> Word64 -> Word64)
 -> MbTypeReprData Word64)
-> (forall (ctx :: Any). NameRefresher -> Word64 -> Word64)
-> MbTypeReprData Word64
forall a b. (a -> b) -> a -> b
$ (\NameRefresher
_ -> Word64 -> Word64
forall a. a -> a
id))

instance NuMatching () where
    nuMatchingProof :: MbTypeRepr ()
nuMatchingProof = MbTypeReprData () -> MbTypeRepr ()
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> () -> ())
-> MbTypeReprData ()
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> () -> ())
 -> MbTypeReprData ())
-> (forall (ctx :: Any). NameRefresher -> () -> ())
-> MbTypeReprData ()
forall a b. (a -> b) -> a -> b
$ (\NameRefresher
_ -> () -> ()
forall a. a -> a
id))

instance (NuMatching a, NuMatching b) => NuMatching (a,b) where
    nuMatchingProof :: MbTypeRepr (a, b)
nuMatchingProof = MbTypeReprData (a, b) -> MbTypeRepr (a, b)
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> (a, b) -> (a, b))
-> MbTypeReprData (a, b)
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> (a, b) -> (a, b))
 -> MbTypeReprData (a, b))
-> (forall (ctx :: Any). NameRefresher -> (a, b) -> (a, b))
-> MbTypeReprData (a, b)
forall a b. (a -> b) -> a -> b
$ \NameRefresher
r (a,b) ->
                                       (NameRefresher -> a -> a
forall a. NuMatching a => NameRefresher -> a -> a
mapNames NameRefresher
r a
a, NameRefresher -> b -> b
forall a. NuMatching a => NameRefresher -> a -> a
mapNames NameRefresher
r b
b))

instance (NuMatching a, NuMatching b, NuMatching c) => NuMatching (a,b,c) where
    nuMatchingProof :: MbTypeRepr (a, b, c)
nuMatchingProof = MbTypeReprData (a, b, c) -> MbTypeRepr (a, b, c)
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> (a, b, c) -> (a, b, c))
-> MbTypeReprData (a, b, c)
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> (a, b, c) -> (a, b, c))
 -> MbTypeReprData (a, b, c))
-> (forall (ctx :: Any). NameRefresher -> (a, b, c) -> (a, b, c))
-> MbTypeReprData (a, b, c)
forall a b. (a -> b) -> a -> b
$ \NameRefresher
r (a,b,c) ->
                                       (NameRefresher -> a -> a
forall a. NuMatching a => NameRefresher -> a -> a
mapNames NameRefresher
r a
a, NameRefresher -> b -> b
forall a. NuMatching a => NameRefresher -> a -> a
mapNames NameRefresher
r b
b, NameRefresher -> c -> c
forall a. NuMatching a => NameRefresher -> a -> a
mapNames NameRefresher
r c
c))

instance (NuMatching a, NuMatching b,
          NuMatching c, NuMatching d) => NuMatching (a,b,c,d) where
    nuMatchingProof :: MbTypeRepr (a, b, c, d)
nuMatchingProof = MbTypeReprData (a, b, c, d) -> MbTypeRepr (a, b, c, d)
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any).
 NameRefresher -> (a, b, c, d) -> (a, b, c, d))
-> MbTypeReprData (a, b, c, d)
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any).
  NameRefresher -> (a, b, c, d) -> (a, b, c, d))
 -> MbTypeReprData (a, b, c, d))
-> (forall (ctx :: Any).
    NameRefresher -> (a, b, c, d) -> (a, b, c, d))
-> MbTypeReprData (a, b, c, d)
forall a b. (a -> b) -> a -> b
$ \NameRefresher
r (a,b,c,d) ->
                                       (NameRefresher -> a -> a
forall a. NuMatching a => NameRefresher -> a -> a
mapNames NameRefresher
r a
a, NameRefresher -> b -> b
forall a. NuMatching a => NameRefresher -> a -> a
mapNames NameRefresher
r b
b,
                                        NameRefresher -> c -> c
forall a. NuMatching a => NameRefresher -> a -> a
mapNames NameRefresher
r c
c, NameRefresher -> d -> d
forall a. NuMatching a => NameRefresher -> a -> a
mapNames NameRefresher
r d
d))

instance NuMatching a => NuMatching [a] where
    nuMatchingProof :: MbTypeRepr [a]
nuMatchingProof = MbTypeReprData [a] -> MbTypeRepr [a]
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> [a] -> [a])
-> MbTypeReprData [a]
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> [a] -> [a])
 -> MbTypeReprData [a])
-> (forall (ctx :: Any). NameRefresher -> [a] -> [a])
-> MbTypeReprData [a]
forall a b. (a -> b) -> a -> b
$ (\NameRefresher
r -> (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (NameRefresher -> a -> a
forall a. NuMatching a => NameRefresher -> a -> a
mapNames NameRefresher
r)))

instance NuMatching a => NuMatching (Vector a) where
    nuMatchingProof :: MbTypeRepr (Vector a)
nuMatchingProof =
      MbTypeReprData (Vector a) -> MbTypeRepr (Vector a)
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData ((forall (ctx :: Any). NameRefresher -> Vector a -> Vector a)
-> MbTypeReprData (Vector a)
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData ((forall (ctx :: Any). NameRefresher -> Vector a -> Vector a)
 -> MbTypeReprData (Vector a))
-> (forall (ctx :: Any). NameRefresher -> Vector a -> Vector a)
-> MbTypeReprData (Vector a)
forall a b. (a -> b) -> a -> b
$ (\NameRefresher
r -> (a -> a) -> Vector a -> Vector a
forall a b. (a -> b) -> Vector a -> Vector b
Vector.map (NameRefresher -> a -> a
forall a. NuMatching a => NameRefresher -> a -> a
mapNames NameRefresher
r)))


{-
type family NuMatchingListProof args
type instance NuMatchingListProof Nil = ()
type instance NuMatchingListProof (args :> arg) = (NuMatchingListProof args, MbTypeReprData arg)

-- the NuMatchingList class, for saying that NuMatching holds for a context of types
class NuMatchingList args where
    nuMatchingListProof :: NuMatchingListProof args

instance NuMatchingList Nil where
    nuMatchingListProof = ()

instance (NuMatchingList args, NuMatching a) => NuMatchingList (args :> a) where
    nuMatchingListProof = (nuMatchingListProof, nuMatchingProof)
-}

{-
-- | An object-level reification of the 'NuMatching' class
data NuMatchingObj a = NuMatching a => NuMatchingObj ()

class NuMatchingList args where
    nuMatchingListProof :: RAssign 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)
-}

-- README: deriving NuMatching from NuMatching1 leads to overlapping instances
-- for, e.g., Name a
{-
instance (NuMatching1 f, NuMatching a) => NuMatching (f a) where
    nuMatchingProof = nuMatchingProof1 nuMatchingProof
-}

{-
instance {-# OVERLAPPABLE #-} (NuMatching1 f, NuMatchingList ctx) =>
                              NuMatching (RAssign f ctx) where
    nuMatchingProof = MbTypeReprData $ MkMbTypeReprData $ helper nuMatchingListProof where
        helper :: NuMatching1 f =>
                  RAssign NuMatchingObj args -> NameRefresher ->
                  RAssign f args -> RAssign f args
        helper MNil r MNil = MNil
        helper (proofs :>: NuMatchingObj ()) r (elems :>: (elem :: f a)) =
            case nuMatchingProof1 :: NuMatchingObj (f a) of
              NuMatchingObj () ->
                  (helper proofs r elems) :>:
                  mapNames r elem
-}

-- | Typeclass for lifting the 'NuMatching' constraint to functors on arbitrary
-- kinds that do not require any constraints on their input types
class NuMatchingAny1 (f :: k -> Type) where
  nuMatchingAny1Proof :: MbTypeRepr (f a)

instance {-# INCOHERENT #-} NuMatchingAny1 f => NuMatching (f a) where
  nuMatchingProof :: MbTypeRepr (f a)
nuMatchingProof = MbTypeRepr (f a)
forall k (f :: k -> *) (a :: k).
NuMatchingAny1 f =>
MbTypeRepr (f a)
nuMatchingAny1Proof

instance NuMatchingAny1 Name where
  nuMatchingAny1Proof :: MbTypeRepr (Name a)
nuMatchingAny1Proof = MbTypeRepr (Name a)
forall a. NuMatching a => MbTypeRepr a
nuMatchingProof

instance NuMatchingAny1 ((:~:) a) where
  nuMatchingAny1Proof :: MbTypeRepr (a :~: a)
nuMatchingAny1Proof = MbTypeRepr (a :~: a)
forall a. NuMatching a => MbTypeRepr a
nuMatchingProof

instance NuMatching a => NuMatchingAny1 (Constant a) where
  nuMatchingAny1Proof :: MbTypeRepr (Constant a a)
nuMatchingAny1Proof = MbTypeRepr (Constant a a)
forall a. NuMatching a => MbTypeRepr a
nuMatchingProof

instance {-# OVERLAPPABLE #-} NuMatchingAny1 f => NuMatching (RAssign f ctx) where
    nuMatchingProof :: MbTypeRepr (RAssign f ctx)
nuMatchingProof = MbTypeReprData (RAssign f ctx) -> MbTypeRepr (RAssign f ctx)
forall a. MbTypeReprData a -> MbTypeRepr a
MbTypeReprData (MbTypeReprData (RAssign f ctx) -> MbTypeRepr (RAssign f ctx))
-> MbTypeReprData (RAssign f ctx) -> MbTypeRepr (RAssign f ctx)
forall a b. (a -> b) -> a -> b
$ (forall (ctx :: Any).
 NameRefresher -> RAssign f ctx -> RAssign f ctx)
-> MbTypeReprData (RAssign f ctx)
forall a k.
(forall (ctx :: k). NameRefresher -> a -> a) -> MbTypeReprData a
MkMbTypeReprData forall (ctx :: Any).
NameRefresher -> RAssign f ctx -> RAssign f ctx
forall (args :: RList k).
NuMatchingAny1 f =>
NameRefresher -> RAssign f args -> RAssign f args
helper where
        helper :: NuMatchingAny1 f => NameRefresher -> RAssign f args ->
                  RAssign f args
        helper :: NameRefresher -> RAssign f args -> RAssign f args
helper NameRefresher
r RAssign f args
MNil = RAssign f args
forall k (f :: k -> *). RAssign f 'RNil
MNil
        helper NameRefresher
r (RAssign f c
elems :>: f a
elem) = NameRefresher -> RAssign f c -> RAssign f c
forall (args :: RList k).
NuMatchingAny1 f =>
NameRefresher -> RAssign f args -> RAssign f args
helper NameRefresher
r RAssign f c
elems RAssign f c -> f a -> RAssign f (c ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: NameRefresher -> f a -> f a
forall a. NuMatching a => NameRefresher -> a -> a
mapNames NameRefresher
r f a
elem


-- now we define some TH to create NuMatchings

natsFrom :: t -> [t]
natsFrom t
i = t
i t -> [t] -> [t]
forall a. a -> [a] -> [a]
: t -> [t]
natsFrom (t
it -> t -> t
forall a. Num a => a -> a -> a
+t
1)

fst3 :: (a,b,c) -> a
fst3 :: (a, b, c) -> a
fst3 (a
x,b
_,c
_) = a
x

snd3 :: (a,b,c) -> b
snd3 :: (a, b, c) -> b
snd3 (a
_,b
y,c
_) = b
y

thd3 :: (a,b,c) -> c
thd3 :: (a, b, c) -> c
thd3 (a
_,b
_,c
z) = c
z


type Names = (TH.Name, TH.Name, TH.Name)

mapNamesType :: TypeQ -> TypeQ
mapNamesType TypeQ
a = [t| forall ctx. NameRefresher -> $a -> $a |]

{-|
  Template Haskell function for creating NuMatching instances for (G)ADTs.
  Typical usage is to include the following line in the source file for
  (G)ADT @T@ (here assumed to have two type arguments):

> $(mkNuMatching [t| forall a b . T a b |])

  The 'mkNuMatching' call here will create an instance declaration for
  @'NuMatching' (T a b)@. It is also possible to include a context in the
  forall type; for example, if we define the 'ID' data type as follows:

> data ID a = ID a

  then we can create a 'NuMatching' instance for it like this:

> $( mkNuMatching [t| NuMatching a => ID a |])

  Note that, when a context is included, the Haskell parser will add
  the @forall a@ for you.
-}
mkNuMatching :: Q TH.Type -> Q [Dec]
mkNuMatching :: TypeQ -> Q [Dec]
mkNuMatching TypeQ
tQ =
    do Kind
t <- TypeQ
tQ
       (Cxt
cxt, Kind
cType, Name
tName, [Con]
constrs, [Name]
tyvars) <- Kind -> Q (Cxt, Kind, Name, [Con], [Name])
getMbTypeReprInfoTop Kind
t
       Name
fName <- String -> Q Name
newName String
"f"
       Name
refrName <- String -> Q Name
newName String
"refresher"
       [Clause]
clauses <- Names -> [Con] -> Q [Clause]
getClauses (Name
tName, Name
fName, Name
refrName) [Con]
constrs
       Kind
mapNamesT <- TypeQ -> TypeQ
mapNamesType (Kind -> TypeQ
forall (m :: * -> *) a. Monad m => a -> m a
return Kind
cType)
       [Dec] -> Q [Dec]
forall (m :: * -> *) a. Monad m => a -> m a
return [Cxt -> Kind -> [Dec] -> Dec
mkInstanceD
               Cxt
cxt (Kind -> Kind -> Kind
TH.AppT (Name -> Kind
TH.ConT ''NuMatching) Kind
cType)
               [Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP 'nuMatchingProof)
                (Exp -> Body
NormalB
                 (Exp -> Body) -> Exp -> Body
forall a b. (a -> b) -> a -> b
$ Exp -> Exp -> Exp
AppE (Name -> Exp
ConE 'MbTypeReprData)
                   (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp -> Exp
AppE (Name -> Exp
ConE 'MkMbTypeReprData)
                         (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ [Dec] -> Exp -> Exp
LetE [Name -> Kind -> Dec
SigD Name
fName
                                 (Kind -> Dec) -> Kind -> Dec
forall a b. (a -> b) -> a -> b
$ [TyVarBndr] -> Cxt -> Kind -> Kind
TH.ForallT ((Name -> TyVarBndr) -> [Name] -> [TyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map Name -> TyVarBndr
PlainTV [Name]
tyvars) Cxt
cxt Kind
mapNamesT,
                                 Name -> [Clause] -> Dec
FunD Name
fName [Clause]
clauses]
                               (Name -> Exp
VarE Name
fName)) []]]

       {-
       return (LetE
               [SigD fName
                     (TH.ForallT tyvars reqCxt
                     $ foldl TH.AppT TH.ArrowT
                           [foldl TH.AppT (TH.ConT conName)
                                      (map tyVarToType tyvars)]),
                FunD fname clauses]
               (VarE fname))
        -}
    where
      -- extract the name from a TyVarBndr
      tyBndrToName :: TyVarBndr -> Name
tyBndrToName (PlainTV Name
n) = Name
n
      tyBndrToName (KindedTV Name
n Kind
_) = Name
n

      -- fail for getMbTypeReprInfo
      getMbTypeReprInfoFail :: a -> String -> m a
getMbTypeReprInfoFail a
t String
extraMsg =
          String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"mkMbTypeRepr: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
t
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not a type constructor for a (G)ADT applied to zero or more distinct type variables" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
extraMsg)

      -- get info for conName (top-level call)
      getMbTypeReprInfoTop :: Kind -> Q (Cxt, Kind, Name, [Con], [Name])
getMbTypeReprInfoTop Kind
t = Cxt -> [Name] -> Kind -> Kind -> Q (Cxt, Kind, Name, [Con], [Name])
forall a.
Show a =>
Cxt -> [Name] -> a -> Kind -> Q (Cxt, Kind, Name, [Con], [Name])
getMbTypeReprInfo [] [] Kind
t Kind
t

      -- get info for conName
      getMbTypeReprInfo :: Cxt -> [Name] -> a -> Kind -> Q (Cxt, Kind, Name, [Con], [Name])
getMbTypeReprInfo Cxt
ctx [Name]
tyvars a
topT (TH.ConT Name
tName) =
          do Info
info <- Name -> Q Info
reify Name
tName
             case Info
info of
               TyConI (Dec -> Maybe (Cxt, Name, [TyVarBndr], [Con])
matchDataDecl -> Just (Cxt
_, Name
_, [TyVarBndr]
tyvarsReq, [Con]
constrs)) ->
                 [TyVarBndr] -> [Con] -> Q (Cxt, Kind, Name, [Con], [Name])
success [TyVarBndr]
tyvarsReq [Con]
constrs
               Info
_ -> a -> String -> Q (Cxt, Kind, Name, [Con], [Name])
forall (m :: * -> *) a a.
(MonadFail m, Show a) =>
a -> String -> m a
getMbTypeReprInfoFail a
topT (String
": info for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Name -> String
forall a. Show a => a -> String
show Name
tName) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Info -> String
forall a. Show a => a -> String
show Info
info))
          where
            success :: [TyVarBndr] -> [Con] -> Q (Cxt, Kind, Name, [Con], [Name])
success [TyVarBndr]
tyvarsReq [Con]
constrs =
                let tyvarsRet :: [Name]
tyvarsRet = if [Name]
tyvars [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== [] Bool -> Bool -> Bool
&& Cxt
ctx Cxt -> Cxt -> Bool
forall a. Eq a => a -> a -> Bool
== []
                                then (TyVarBndr -> Name) -> [TyVarBndr] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndr -> Name
tyBndrToName [TyVarBndr]
tyvarsReq
                                else [Name]
tyvars in
                (Cxt, Kind, Name, [Con], [Name])
-> Q (Cxt, Kind, Name, [Con], [Name])
forall (m :: * -> *) a. Monad m => a -> m a
return (Cxt
ctx,
                        (Kind -> Kind -> Kind) -> Kind -> Cxt -> Kind
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Kind -> Kind -> Kind
TH.AppT (Name -> Kind
TH.ConT Name
tName) ((Name -> Kind) -> [Name] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> Kind
TH.VarT [Name]
tyvars),
                        Name
tName, [Con]
constrs, [Name]
tyvarsRet)

      getMbTypeReprInfo Cxt
ctx [Name]
tyvars a
topT (TH.AppT Kind
f (TH.VarT Name
argName)) =
          if Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Name
argName [Name]
tyvars then
              a -> String -> Q (Cxt, Kind, Name, [Con], [Name])
forall (m :: * -> *) a a.
(MonadFail m, Show a) =>
a -> String -> m a
getMbTypeReprInfoFail a
topT String
""
          else
              Cxt -> [Name] -> a -> Kind -> Q (Cxt, Kind, Name, [Con], [Name])
getMbTypeReprInfo Cxt
ctx (Name
argNameName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
tyvars) a
topT Kind
f

      getMbTypeReprInfo Cxt
ctx [Name]
tyvars a
topT (TH.ForallT [TyVarBndr]
_ Cxt
ctx' Kind
t) =
          Cxt -> [Name] -> a -> Kind -> Q (Cxt, Kind, Name, [Con], [Name])
getMbTypeReprInfo (Cxt
ctx Cxt -> Cxt -> Cxt
forall a. [a] -> [a] -> [a]
++ Cxt
ctx') [Name]
tyvars a
topT Kind
t

      getMbTypeReprInfo Cxt
ctx [Name]
tyvars a
topT Kind
t = a -> String -> Q (Cxt, Kind, Name, [Con], [Name])
forall (m :: * -> *) a a.
(MonadFail m, Show a) =>
a -> String -> m a
getMbTypeReprInfoFail a
topT String
""

      -- get the name from a data type
      getTCtor :: Kind -> Maybe (Kind, Name, [Name])
getTCtor Kind
t = Kind -> Kind -> [Name] -> Maybe (Kind, Name, [Name])
forall t. Kind -> t -> [Name] -> Maybe (t, Name, [Name])
getTCtorHelper Kind
t Kind
t []
      getTCtorHelper :: Kind -> t -> [Name] -> Maybe (t, Name, [Name])
getTCtorHelper (TH.ConT Name
tName) t
topT [Name]
tyvars = (t, Name, [Name]) -> Maybe (t, Name, [Name])
forall a. a -> Maybe a
Just (t
topT, Name
tName, [Name]
tyvars)
      getTCtorHelper (TH.AppT Kind
t1 (TH.VarT Name
var)) t
topT [Name]
tyvars =
          Kind -> t -> [Name] -> Maybe (t, Name, [Name])
getTCtorHelper Kind
t1 t
topT ([Name]
tyvars [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
var])
      getTCtorHelper (TH.SigT Kind
t1 Kind
_) t
topT [Name]
tyvars = Kind -> t -> [Name] -> Maybe (t, Name, [Name])
getTCtorHelper Kind
t1 t
topT [Name]
tyvars
      getTCtorHelper Kind
_ t
_ [Name]
_ = Maybe (t, Name, [Name])
forall a. Maybe a
Nothing

      -- get a list of Clauses, one for each constructor in constrs
      getClauses :: Names -> [Con] -> Q [Clause]
      getClauses :: Names -> [Con] -> Q [Clause]
getClauses Names
_ [] = [Clause] -> Q [Clause]
forall (m :: * -> *) a. Monad m => a -> m a
return []

      getClauses Names
names (NormalC Name
cName [BangType]
cTypes : [Con]
constrs) =
        do Clause
clause <-
             Names
-> Cxt
-> [Integer]
-> ([(Name, Kind, Integer)] -> Pat)
-> ([(Exp, Kind, Integer)] -> Exp)
-> Q Clause
forall a.
Names
-> Cxt
-> [a]
-> ([(Name, Kind, a)] -> Pat)
-> ([(Exp, Kind, a)] -> Exp)
-> Q Clause
getClauseHelper Names
names ((BangType -> Kind) -> [BangType] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Kind
forall a b. (a, b) -> b
snd [BangType]
cTypes) (Integer -> [Integer]
forall t. Num t => t -> [t]
natsFrom Integer
0)
             (\[(Name, Kind, Integer)]
l -> Name -> [Pat] -> Pat
ConP Name
cName (((Name, Kind, Integer) -> Pat) -> [(Name, Kind, Integer)] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Pat
VarP (Name -> Pat)
-> ((Name, Kind, Integer) -> Name) -> (Name, Kind, Integer) -> Pat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Kind, Integer) -> Name
forall a b c. (a, b, c) -> a
fst3) [(Name, Kind, Integer)]
l))
             (\[(Exp, Kind, Integer)]
l -> (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
AppE (Name -> Exp
ConE Name
cName) (((Exp, Kind, Integer) -> Exp) -> [(Exp, Kind, Integer)] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map (Exp, Kind, Integer) -> Exp
forall a b c. (a, b, c) -> a
fst3 [(Exp, Kind, Integer)]
l))
           [Clause]
clauses <- Names -> [Con] -> Q [Clause]
getClauses Names
names [Con]
constrs
           [Clause] -> Q [Clause]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause] -> Q [Clause]) -> [Clause] -> Q [Clause]
forall a b. (a -> b) -> a -> b
$ Clause
clause Clause -> [Clause] -> [Clause]
forall a. a -> [a] -> [a]
: [Clause]
clauses

      getClauses Names
names (RecC Name
cName [VarBangType]
cVarTypes : [Con]
constrs) =
        do Clause
clause <-
             Names
-> Cxt
-> [Name]
-> ([(Name, Kind, Name)] -> Pat)
-> ([(Exp, Kind, Name)] -> Exp)
-> Q Clause
forall a.
Names
-> Cxt
-> [a]
-> ([(Name, Kind, a)] -> Pat)
-> ([(Exp, Kind, a)] -> Exp)
-> Q Clause
getClauseHelper Names
names ((VarBangType -> Kind) -> [VarBangType] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> Kind
forall a b c. (a, b, c) -> c
thd3 [VarBangType]
cVarTypes) ((VarBangType -> Name) -> [VarBangType] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> Name
forall a b c. (a, b, c) -> a
fst3 [VarBangType]
cVarTypes)
             (\[(Name, Kind, Name)]
l -> Name -> [FieldPat] -> Pat
RecP Name
cName (((Name, Kind, Name) -> FieldPat)
-> [(Name, Kind, Name)] -> [FieldPat]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
var,Kind
_,Name
field) -> (Name
field, Name -> Pat
VarP Name
var)) [(Name, Kind, Name)]
l))
             (\[(Exp, Kind, Name)]
l -> Name -> [FieldExp] -> Exp
RecConE Name
cName (((Exp, Kind, Name) -> FieldExp)
-> [(Exp, Kind, Name)] -> [FieldExp]
forall a b. (a -> b) -> [a] -> [b]
map (\(Exp
exp,Kind
_,Name
field) -> (Name
field, Exp
exp)) [(Exp, Kind, Name)]
l))
           [Clause]
clauses <- Names -> [Con] -> Q [Clause]
getClauses Names
names [Con]
constrs
           [Clause] -> Q [Clause]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause] -> Q [Clause]) -> [Clause] -> Q [Clause]
forall a b. (a -> b) -> a -> b
$ Clause
clause Clause -> [Clause] -> [Clause]
forall a. a -> [a] -> [a]
: [Clause]
clauses

      getClauses Names
names (InfixC BangType
cType1 Name
cName BangType
cType2 : [Con]
constrs) =
        do Clause
clause <-
             Names
-> Cxt
-> [Integer]
-> ([(Name, Kind, Integer)] -> Pat)
-> ([(Exp, Kind, Integer)] -> Exp)
-> Q Clause
forall a.
Names
-> Cxt
-> [a]
-> ([(Name, Kind, a)] -> Pat)
-> ([(Exp, Kind, a)] -> Exp)
-> Q Clause
getClauseHelper Names
names ((BangType -> Kind) -> [BangType] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Kind
forall a b. (a, b) -> b
snd [BangType
cType1, BangType
cType2]) (Integer -> [Integer]
forall t. Num t => t -> [t]
natsFrom Integer
0)
             (\[(Name, Kind, Integer)]
l -> Name -> [Pat] -> Pat
ConP Name
cName (((Name, Kind, Integer) -> Pat) -> [(Name, Kind, Integer)] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Pat
VarP (Name -> Pat)
-> ((Name, Kind, Integer) -> Name) -> (Name, Kind, Integer) -> Pat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Kind, Integer) -> Name
forall a b c. (a, b, c) -> a
fst3) [(Name, Kind, Integer)]
l))
             (\[(Exp, Kind, Integer)]
l -> (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
AppE (Name -> Exp
ConE Name
cName) (((Exp, Kind, Integer) -> Exp) -> [(Exp, Kind, Integer)] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map (Exp, Kind, Integer) -> Exp
forall a b c. (a, b, c) -> a
fst3 [(Exp, Kind, Integer)]
l))
           [Clause]
clauses <- Names -> [Con] -> Q [Clause]
getClauses Names
names [Con]
constrs
           [Clause] -> Q [Clause]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause] -> Q [Clause]) -> [Clause] -> Q [Clause]
forall a b. (a -> b) -> a -> b
$ Clause
clause Clause -> [Clause] -> [Clause]
forall a. a -> [a] -> [a]
: [Clause]
clauses

      getClauses Names
names (GadtC [Name]
cNames [BangType]
cTypes Kind
_ : [Con]
constrs) =
        do [Clause]
clauses1 <-
             [Name] -> (Name -> Q Clause) -> Q [Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Name]
cNames ((Name -> Q Clause) -> Q [Clause])
-> (Name -> Q Clause) -> Q [Clause]
forall a b. (a -> b) -> a -> b
$ \Name
cName ->
             Names
-> Cxt
-> [Integer]
-> ([(Name, Kind, Integer)] -> Pat)
-> ([(Exp, Kind, Integer)] -> Exp)
-> Q Clause
forall a.
Names
-> Cxt
-> [a]
-> ([(Name, Kind, a)] -> Pat)
-> ([(Exp, Kind, a)] -> Exp)
-> Q Clause
getClauseHelper Names
names ((BangType -> Kind) -> [BangType] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Kind
forall a b. (a, b) -> b
snd [BangType]
cTypes) (Integer -> [Integer]
forall t. Num t => t -> [t]
natsFrom Integer
0)
             (\[(Name, Kind, Integer)]
l -> Name -> [Pat] -> Pat
ConP Name
cName (((Name, Kind, Integer) -> Pat) -> [(Name, Kind, Integer)] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Pat
VarP (Name -> Pat)
-> ((Name, Kind, Integer) -> Name) -> (Name, Kind, Integer) -> Pat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Kind, Integer) -> Name
forall a b c. (a, b, c) -> a
fst3) [(Name, Kind, Integer)]
l))
             (\[(Exp, Kind, Integer)]
l -> (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
AppE (Name -> Exp
ConE Name
cName) (((Exp, Kind, Integer) -> Exp) -> [(Exp, Kind, Integer)] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map (Exp, Kind, Integer) -> Exp
forall a b c. (a, b, c) -> a
fst3 [(Exp, Kind, Integer)]
l))
           [Clause]
clauses2 <- Names -> [Con] -> Q [Clause]
getClauses Names
names [Con]
constrs
           [Clause] -> Q [Clause]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause]
clauses1 [Clause] -> [Clause] -> [Clause]
forall a. [a] -> [a] -> [a]
++ [Clause]
clauses2)

      getClauses Names
names (RecGadtC [Name]
cNames [VarBangType]
cVarTypes Kind
_ : [Con]
constrs) =
        do [Clause]
clauses1 <-
             [Name] -> (Name -> Q Clause) -> Q [Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Name]
cNames ((Name -> Q Clause) -> Q [Clause])
-> (Name -> Q Clause) -> Q [Clause]
forall a b. (a -> b) -> a -> b
$ \Name
cName ->
             Names
-> Cxt
-> [Name]
-> ([(Name, Kind, Name)] -> Pat)
-> ([(Exp, Kind, Name)] -> Exp)
-> Q Clause
forall a.
Names
-> Cxt
-> [a]
-> ([(Name, Kind, a)] -> Pat)
-> ([(Exp, Kind, a)] -> Exp)
-> Q Clause
getClauseHelper Names
names ((VarBangType -> Kind) -> [VarBangType] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> Kind
forall a b c. (a, b, c) -> c
thd3 [VarBangType]
cVarTypes) ((VarBangType -> Name) -> [VarBangType] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> Name
forall a b c. (a, b, c) -> a
fst3 [VarBangType]
cVarTypes)
             (\[(Name, Kind, Name)]
l -> Name -> [FieldPat] -> Pat
RecP Name
cName (((Name, Kind, Name) -> FieldPat)
-> [(Name, Kind, Name)] -> [FieldPat]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
var,Kind
_,Name
field) -> (Name
field, Name -> Pat
VarP Name
var)) [(Name, Kind, Name)]
l))
             (\[(Exp, Kind, Name)]
l -> Name -> [FieldExp] -> Exp
RecConE Name
cName (((Exp, Kind, Name) -> FieldExp)
-> [(Exp, Kind, Name)] -> [FieldExp]
forall a b. (a -> b) -> [a] -> [b]
map (\(Exp
exp,Kind
_,Name
field) -> (Name
field, Exp
exp)) [(Exp, Kind, Name)]
l))
           [Clause]
clauses2 <- Names -> [Con] -> Q [Clause]
getClauses Names
names [Con]
constrs
           [Clause] -> Q [Clause]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause]
clauses1 [Clause] -> [Clause] -> [Clause]
forall a. [a] -> [a] -> [a]
++ [Clause]
clauses2)

      getClauses Names
names (ForallC [TyVarBndr]
_ Cxt
_ Con
constr : [Con]
constrs) =
        Names -> [Con] -> Q [Clause]
getClauses Names
names (Con
constr Con -> [Con] -> [Con]
forall a. a -> [a] -> [a]
: [Con]
constrs)

      getClauseHelper :: Names -> [TH.Type] -> [a] ->
                         ([(TH.Name,TH.Type,a)] -> Pat) ->
                         ([(Exp,TH.Type,a)] -> Exp) ->
                         Q Clause
      getClauseHelper :: Names
-> Cxt
-> [a]
-> ([(Name, Kind, a)] -> Pat)
-> ([(Exp, Kind, a)] -> Exp)
-> Q Clause
getClauseHelper names :: Names
names@(Name
tName, Name
fName, Name
refrName) Cxt
cTypes [a]
cData [(Name, Kind, a)] -> Pat
pFun [(Exp, Kind, a)] -> Exp
eFun =
          do [Name]
varNames <- ((Integer, Kind) -> Q Name) -> [(Integer, Kind)] -> Q [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String -> Q Name
newName (String -> Q Name)
-> ((Integer, Kind) -> String) -> (Integer, Kind) -> Q Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String)
-> ((Integer, Kind) -> String) -> (Integer, Kind) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String
forall a. Show a => a -> String
show (Integer -> String)
-> ((Integer, Kind) -> Integer) -> (Integer, Kind) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer, Kind) -> Integer
forall a b. (a, b) -> a
fst)
                         ([(Integer, Kind)] -> Q [Name]) -> [(Integer, Kind)] -> Q [Name]
forall a b. (a -> b) -> a -> b
$ [Integer] -> Cxt -> [(Integer, Kind)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Integer -> [Integer]
forall t. Num t => t -> [t]
natsFrom Integer
0) Cxt
cTypes
             let varsTypesData :: [(Name, Kind, a)]
varsTypesData = [Name] -> Cxt -> [a] -> [(Name, Kind, a)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Name]
varNames Cxt
cTypes [a]
cData
             let expsTypesData :: [(Exp, Kind, a)]
expsTypesData = ((Name, Kind, a) -> (Exp, Kind, a))
-> [(Name, Kind, a)] -> [(Exp, Kind, a)]
forall a b. (a -> b) -> [a] -> [b]
map (Names -> (Name, Kind, a) -> (Exp, Kind, a)
forall a. Names -> (Name, Kind, a) -> (Exp, Kind, a)
mkExpTypeData Names
names) [(Name, Kind, a)]
varsTypesData
             Clause -> Q Clause
forall (m :: * -> *) a. Monad m => a -> m a
return (Clause -> Q Clause) -> Clause -> Q Clause
forall a b. (a -> b) -> a -> b
$ [Pat] -> Body -> [Dec] -> Clause
Clause [(Name -> Pat
VarP Name
refrName), ([(Name, Kind, a)] -> Pat
pFun [(Name, Kind, a)]
varsTypesData)]
                        (Exp -> Body
NormalB (Exp -> Body) -> Exp -> Body
forall a b. (a -> b) -> a -> b
$ [(Exp, Kind, a)] -> Exp
eFun [(Exp, Kind, a)]
expsTypesData) []

      mkExpTypeData :: Names -> (TH.Name,TH.Type,a) -> (Exp,TH.Type,a)
      mkExpTypeData :: Names -> (Name, Kind, a) -> (Exp, Kind, a)
mkExpTypeData (Name
tName, Name
fName, Name
refrName)
                    (Name
varName, Kind -> Maybe (Kind, Name, [Name])
getTCtor -> Just (Kind
t, Name
tName', [Name]
_), a
cData)
          | Name
tName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
tName' =
              -- the type of the arg is the same as the (G)ADT we are
              -- recursing over; apply the recursive function
              ((Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
fName)
                         [(Name -> Exp
VarE Name
refrName), (Name -> Exp
VarE Name
varName)],
               Kind
t, a
cData)
      mkExpTypeData (Name
tName, Name
fName, Name
refrName) (Name
varName, Kind
t, a
cData) =
          -- the type of the arg is not the same as the (G)ADT; call mapNames
          ((Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'mapNames)
                     [(Name -> Exp
VarE Name
refrName), (Name -> Exp
VarE Name
varName)],
           Kind
t, a
cData)

-- FIXME: old stuff below

type CxtStateQ a = StateT Cxt Q a

-- create a MkMbTypeReprData for a (G)ADT
mkMkMbTypeReprDataOld :: Q TH.Name -> Q Exp
mkMkMbTypeReprDataOld :: Q Name -> Q Exp
mkMkMbTypeReprDataOld Q Name
conNameQ =
    do Name
conName <- Q Name
conNameQ
       (Cxt
cxt, Name
name, [TyVarBndr]
tyvars, [Con]
constrs) <- Name -> Q (Cxt, Name, [TyVarBndr], [Con])
getMbTypeReprInfo Name
conName
       ([Clause]
clauses, Cxt
reqCxt) <- StateT Cxt Q [Clause] -> Cxt -> Q ([Clause], Cxt)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Cxt
-> Name
-> [TyVarBndr]
-> [TyVarBndr]
-> [Con]
-> StateT Cxt Q [Clause]
getClauses Cxt
cxt Name
name [TyVarBndr]
tyvars [] [Con]
constrs) []
       Name
fname <- String -> Q Name
newName String
"f"
       Exp -> Q Exp
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dec] -> Exp -> Exp
LetE
               [Name -> Kind -> Dec
SigD Name
fname
                     ([TyVarBndr] -> Cxt -> Kind -> Kind
TH.ForallT [TyVarBndr]
tyvars Cxt
reqCxt
                     (Kind -> Kind) -> Kind -> Kind
forall a b. (a -> b) -> a -> b
$ (Kind -> Kind -> Kind) -> Kind -> Cxt -> Kind
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Kind -> Kind -> Kind
TH.AppT Kind
TH.ArrowT
                           [(Kind -> Kind -> Kind) -> Kind -> Cxt -> Kind
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Kind -> Kind -> Kind
TH.AppT (Name -> Kind
TH.ConT Name
conName)
                                      ((TyVarBndr -> Kind) -> [TyVarBndr] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndr -> Kind
tyVarToType [TyVarBndr]
tyvars)]),
                Name -> [Clause] -> Dec
FunD Name
fname [Clause]
clauses]
               (Name -> Exp
VarE Name
fname))
    where
      -- convert a TyVar to a Name
      tyVarToType :: TyVarBndr -> Kind
tyVarToType (PlainTV Name
n) = Name -> Kind
TH.VarT Name
n
      tyVarToType (KindedTV Name
n Kind
_) = Name -> Kind
TH.VarT Name
n

      -- get info for conName
      getMbTypeReprInfo :: Name -> Q (Cxt, Name, [TyVarBndr], [Con])
getMbTypeReprInfo Name
conName =
          Name -> Q Info
reify Name
conName Q Info
-> (Info -> Q (Cxt, Name, [TyVarBndr], [Con]))
-> Q (Cxt, Name, [TyVarBndr], [Con])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Info
info ->
              case Info
info of
                TyConI (Dec -> Maybe (Cxt, Name, [TyVarBndr], [Con])
matchDataDecl -> Just (Cxt
cxt, Name
name, [TyVarBndr]
tyvars, [Con]
constrs)) ->
                    (Cxt, Name, [TyVarBndr], [Con])
-> Q (Cxt, Name, [TyVarBndr], [Con])
forall (m :: * -> *) a. Monad m => a -> m a
return (Cxt
cxt, Name
name, [TyVarBndr]
tyvars, [Con]
constrs)
                Info
_ -> String -> Q (Cxt, Name, [TyVarBndr], [Con])
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"mkMkMbTypeReprData: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
conName
                           String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not a (G)ADT")
      {-
      -- report failure
      getMbTypeReprInfoFail t =
          fail ("mkMkMbTypeReprData: " ++ show t
                ++ " is not a fully applied (G)ADT")

      getMbTypeReprInfo (TH.ConT conName) topT =
          reify conName >>= \info ->
              case info of
                TyConI (DataD cxt name tyvars constrs _) ->
                    return (cxt, name, tyvars, constrs)
                _ -> getMbTypeReprInfoFail topT
      getMbTypeReprInfo (TH.AppT t _) topT = getMbTypeReprInfo t topT
      getMbTypeReprInfo (TH.SigT t _) topT = getMbTypeReprInfo t topT
      getMbTypeReprInfo _ topT = getMbTypeReprInfoFail topT
       -}

      -- get a list of Clauses, one for each constructor in constrs
      getClauses :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] -> [Con] ->
                    CxtStateQ [Clause]
      getClauses :: Cxt
-> Name
-> [TyVarBndr]
-> [TyVarBndr]
-> [Con]
-> StateT Cxt Q [Clause]
getClauses Cxt
cxt Name
name [TyVarBndr]
tyvars [TyVarBndr]
locTyvars [] = [Clause] -> StateT Cxt Q [Clause]
forall (m :: * -> *) a. Monad m => a -> m a
return []

      getClauses Cxt
cxt Name
name [TyVarBndr]
tyvars [TyVarBndr]
locTyvars (NormalC Name
cName [BangType]
cTypes : [Con]
constrs) =
        do Clause
clause <-
             Cxt
-> Name
-> [TyVarBndr]
-> [TyVarBndr]
-> Cxt
-> [Integer]
-> ([(Name, Kind, Integer)] -> Pat)
-> ([(Name, Kind, Integer)] -> Exp)
-> CxtStateQ Clause
forall a.
Cxt
-> Name
-> [TyVarBndr]
-> [TyVarBndr]
-> Cxt
-> [a]
-> ([(Name, Kind, a)] -> Pat)
-> ([(Name, Kind, a)] -> Exp)
-> CxtStateQ Clause
getClauseHelper Cxt
cxt Name
name [TyVarBndr]
tyvars [TyVarBndr]
locTyvars ((BangType -> Kind) -> [BangType] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Kind
forall a b. (a, b) -> b
snd [BangType]
cTypes)
             (Integer -> [Integer]
forall t. Num t => t -> [t]
natsFrom Integer
0)
             (\[(Name, Kind, Integer)]
l -> Name -> [Pat] -> Pat
ConP Name
cName (((Name, Kind, Integer) -> Pat) -> [(Name, Kind, Integer)] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Pat
VarP (Name -> Pat)
-> ((Name, Kind, Integer) -> Name) -> (Name, Kind, Integer) -> Pat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Kind, Integer) -> Name
forall a b c. (a, b, c) -> a
fst3) [(Name, Kind, Integer)]
l))
             (\[(Name, Kind, Integer)]
l -> (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
AppE (Name -> Exp
ConE Name
cName) (((Name, Kind, Integer) -> Exp) -> [(Name, Kind, Integer)] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Exp
VarE (Name -> Exp)
-> ((Name, Kind, Integer) -> Name) -> (Name, Kind, Integer) -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Kind, Integer) -> Name
forall a b c. (a, b, c) -> a
fst3) [(Name, Kind, Integer)]
l))
           [Clause]
clauses <- Cxt
-> Name
-> [TyVarBndr]
-> [TyVarBndr]
-> [Con]
-> StateT Cxt Q [Clause]
getClauses Cxt
cxt Name
name [TyVarBndr]
tyvars [TyVarBndr]
locTyvars [Con]
constrs
           [Clause] -> StateT Cxt Q [Clause]
forall (m :: * -> *) a. Monad m => a -> m a
return (Clause
clause Clause -> [Clause] -> [Clause]
forall a. a -> [a] -> [a]
: [Clause]
clauses)

      getClauses Cxt
cxt Name
name [TyVarBndr]
tyvars [TyVarBndr]
locTyvars (RecC Name
cName [VarBangType]
cVarTypes : [Con]
constrs) =
        do Clause
clause <-
             Cxt
-> Name
-> [TyVarBndr]
-> [TyVarBndr]
-> Cxt
-> [Name]
-> ([(Name, Kind, Name)] -> Pat)
-> ([(Name, Kind, Name)] -> Exp)
-> CxtStateQ Clause
forall a.
Cxt
-> Name
-> [TyVarBndr]
-> [TyVarBndr]
-> Cxt
-> [a]
-> ([(Name, Kind, a)] -> Pat)
-> ([(Name, Kind, a)] -> Exp)
-> CxtStateQ Clause
getClauseHelper Cxt
cxt Name
name [TyVarBndr]
tyvars [TyVarBndr]
locTyvars ((VarBangType -> Kind) -> [VarBangType] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> Kind
forall a b c. (a, b, c) -> c
thd3 [VarBangType]
cVarTypes)
             ((VarBangType -> Name) -> [VarBangType] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> Name
forall a b c. (a, b, c) -> a
fst3 [VarBangType]
cVarTypes)
             (\[(Name, Kind, Name)]
l -> Name -> [FieldPat] -> Pat
RecP Name
cName (((Name, Kind, Name) -> FieldPat)
-> [(Name, Kind, Name)] -> [FieldPat]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
var,Kind
_,Name
field) -> (Name
field, Name -> Pat
VarP Name
var)) [(Name, Kind, Name)]
l))
             (\[(Name, Kind, Name)]
l -> Name -> [FieldExp] -> Exp
RecConE Name
cName (((Name, Kind, Name) -> FieldExp)
-> [(Name, Kind, Name)] -> [FieldExp]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
var,Kind
_,Name
field) -> (Name
field, Name -> Exp
VarE Name
var)) [(Name, Kind, Name)]
l))
           [Clause]
clauses <- Cxt
-> Name
-> [TyVarBndr]
-> [TyVarBndr]
-> [Con]
-> StateT Cxt Q [Clause]
getClauses Cxt
cxt Name
name [TyVarBndr]
tyvars [TyVarBndr]
locTyvars [Con]
constrs
           [Clause] -> StateT Cxt Q [Clause]
forall (m :: * -> *) a. Monad m => a -> m a
return (Clause
clause Clause -> [Clause] -> [Clause]
forall a. a -> [a] -> [a]
: [Clause]
clauses)

      getClauses Cxt
cxt Name
name [TyVarBndr]
tyvars [TyVarBndr]
locTyvars (InfixC BangType
cType1 Name
cName BangType
cType2 : [Con]
_) =
        StateT Cxt Q [Clause]
forall a. HasCallStack => a
undefined -- FIXME

      getClauses Cxt
cxt Name
name [TyVarBndr]
tyvars [TyVarBndr]
locTyvars (ForallC [TyVarBndr]
tyvars2 Cxt
cxt2 Con
constr
                                            : [Con]
constrs) =
        do [Clause]
clauses1 <-
             Cxt
-> Name
-> [TyVarBndr]
-> [TyVarBndr]
-> [Con]
-> StateT Cxt Q [Clause]
getClauses (Cxt
cxt Cxt -> Cxt -> Cxt
forall a. [a] -> [a] -> [a]
++ Cxt
cxt2) Name
name [TyVarBndr]
tyvars ([TyVarBndr]
locTyvars [TyVarBndr] -> [TyVarBndr] -> [TyVarBndr]
forall a. [a] -> [a] -> [a]
++ [TyVarBndr]
tyvars2) [Con
constr]
           [Clause]
clauses2 <- Cxt
-> Name
-> [TyVarBndr]
-> [TyVarBndr]
-> [Con]
-> StateT Cxt Q [Clause]
getClauses Cxt
cxt Name
name [TyVarBndr]
tyvars [TyVarBndr]
locTyvars [Con]
constrs
           [Clause] -> StateT Cxt Q [Clause]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause]
clauses1 [Clause] -> [Clause] -> [Clause]
forall a. [a] -> [a] -> [a]
++ [Clause]
clauses2)

      getClauses Cxt
cxt Name
name [TyVarBndr]
tyvars [TyVarBndr]
locTyvars (GadtC [Name]
cNames [BangType]
cTypes Kind
_ : [Con]
constrs) =
        do [Clause]
clauses1 <-
             [Name] -> (Name -> CxtStateQ Clause) -> StateT Cxt Q [Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Name]
cNames ((Name -> CxtStateQ Clause) -> StateT Cxt Q [Clause])
-> (Name -> CxtStateQ Clause) -> StateT Cxt Q [Clause]
forall a b. (a -> b) -> a -> b
$ \Name
cName ->
             Cxt
-> Name
-> [TyVarBndr]
-> [TyVarBndr]
-> Cxt
-> [Integer]
-> ([(Name, Kind, Integer)] -> Pat)
-> ([(Name, Kind, Integer)] -> Exp)
-> CxtStateQ Clause
forall a.
Cxt
-> Name
-> [TyVarBndr]
-> [TyVarBndr]
-> Cxt
-> [a]
-> ([(Name, Kind, a)] -> Pat)
-> ([(Name, Kind, a)] -> Exp)
-> CxtStateQ Clause
getClauseHelper Cxt
cxt Name
name [TyVarBndr]
tyvars [TyVarBndr]
locTyvars ((BangType -> Kind) -> [BangType] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Kind
forall a b. (a, b) -> b
snd [BangType]
cTypes)
             (Integer -> [Integer]
forall t. Num t => t -> [t]
natsFrom Integer
0) (\[(Name, Kind, Integer)]
l -> Name -> [Pat] -> Pat
ConP Name
cName (((Name, Kind, Integer) -> Pat) -> [(Name, Kind, Integer)] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Pat
VarP (Name -> Pat)
-> ((Name, Kind, Integer) -> Name) -> (Name, Kind, Integer) -> Pat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Kind, Integer) -> Name
forall a b c. (a, b, c) -> a
fst3) [(Name, Kind, Integer)]
l))
             (\[(Name, Kind, Integer)]
l -> (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
AppE (Name -> Exp
ConE Name
cName) (((Name, Kind, Integer) -> Exp) -> [(Name, Kind, Integer)] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Exp
VarE (Name -> Exp)
-> ((Name, Kind, Integer) -> Name) -> (Name, Kind, Integer) -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Kind, Integer) -> Name
forall a b c. (a, b, c) -> a
fst3) [(Name, Kind, Integer)]
l))
           [Clause]
clauses2 <- Cxt
-> Name
-> [TyVarBndr]
-> [TyVarBndr]
-> [Con]
-> StateT Cxt Q [Clause]
getClauses Cxt
cxt Name
name [TyVarBndr]
tyvars [TyVarBndr]
locTyvars [Con]
constrs
           [Clause] -> StateT Cxt Q [Clause]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause]
clauses1 [Clause] -> [Clause] -> [Clause]
forall a. [a] -> [a] -> [a]
++ [Clause]
clauses2)

      getClauses Cxt
cxt Name
name [TyVarBndr]
tyvars [TyVarBndr]
locTyvars (RecGadtC [Name]
cNames [VarBangType]
cVarTypes Kind
_
                                            : [Con]
constrs) =
        do [Clause]
clauses1 <-
             [Name] -> (Name -> CxtStateQ Clause) -> StateT Cxt Q [Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Name]
cNames ((Name -> CxtStateQ Clause) -> StateT Cxt Q [Clause])
-> (Name -> CxtStateQ Clause) -> StateT Cxt Q [Clause]
forall a b. (a -> b) -> a -> b
$ \Name
cName ->
             Cxt
-> Name
-> [TyVarBndr]
-> [TyVarBndr]
-> Cxt
-> [Name]
-> ([(Name, Kind, Name)] -> Pat)
-> ([(Name, Kind, Name)] -> Exp)
-> CxtStateQ Clause
forall a.
Cxt
-> Name
-> [TyVarBndr]
-> [TyVarBndr]
-> Cxt
-> [a]
-> ([(Name, Kind, a)] -> Pat)
-> ([(Name, Kind, a)] -> Exp)
-> CxtStateQ Clause
getClauseHelper Cxt
cxt Name
name [TyVarBndr]
tyvars [TyVarBndr]
locTyvars
             ((VarBangType -> Kind) -> [VarBangType] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> Kind
forall a b c. (a, b, c) -> c
thd3 [VarBangType]
cVarTypes) ((VarBangType -> Name) -> [VarBangType] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map VarBangType -> Name
forall a b c. (a, b, c) -> a
fst3 [VarBangType]
cVarTypes)
             (\[(Name, Kind, Name)]
l -> Name -> [FieldPat] -> Pat
RecP Name
cName (((Name, Kind, Name) -> FieldPat)
-> [(Name, Kind, Name)] -> [FieldPat]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
var,Kind
_,Name
field) -> (Name
field, Name -> Pat
VarP Name
var)) [(Name, Kind, Name)]
l))
             (\[(Name, Kind, Name)]
l -> Name -> [FieldExp] -> Exp
RecConE Name
cName (((Name, Kind, Name) -> FieldExp)
-> [(Name, Kind, Name)] -> [FieldExp]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
var,Kind
_,Name
field) -> (Name
field, Name -> Exp
VarE Name
var)) [(Name, Kind, Name)]
l))
           [Clause]
clauses2 <- Cxt
-> Name
-> [TyVarBndr]
-> [TyVarBndr]
-> [Con]
-> StateT Cxt Q [Clause]
getClauses Cxt
cxt Name
name [TyVarBndr]
tyvars [TyVarBndr]
locTyvars [Con]
constrs
           [Clause] -> StateT Cxt Q [Clause]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause]
clauses1 [Clause] -> [Clause] -> [Clause]
forall a. [a] -> [a] -> [a]
++ [Clause]
clauses2)

      getClauseHelper :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] ->
                         [TH.Type] -> [a] ->
                         ([(TH.Name,TH.Type,a)] -> Pat) ->
                         ([(TH.Name,TH.Type,a)] -> Exp) ->
                         CxtStateQ Clause
      getClauseHelper :: Cxt
-> Name
-> [TyVarBndr]
-> [TyVarBndr]
-> Cxt
-> [a]
-> ([(Name, Kind, a)] -> Pat)
-> ([(Name, Kind, a)] -> Exp)
-> CxtStateQ Clause
getClauseHelper Cxt
cxt Name
name [TyVarBndr]
tyvars [TyVarBndr]
locTyvars Cxt
cTypes [a]
cData [(Name, Kind, a)] -> Pat
pFun [(Name, Kind, a)] -> Exp
eFun =
          do [Name]
varNames <- ((Integer, Kind) -> StateT Cxt Q Name)
-> [(Integer, Kind)] -> StateT Cxt Q [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Q Name -> StateT Cxt Q Name
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Q Name -> StateT Cxt Q Name)
-> ((Integer, Kind) -> Q Name)
-> (Integer, Kind)
-> StateT Cxt Q Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Q Name
newName (String -> Q Name)
-> ((Integer, Kind) -> String) -> (Integer, Kind) -> Q Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String)
-> ((Integer, Kind) -> String) -> (Integer, Kind) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String
forall a. Show a => a -> String
show (Integer -> String)
-> ((Integer, Kind) -> Integer) -> (Integer, Kind) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integer, Kind) -> Integer
forall a b. (a, b) -> a
fst)
                         ([(Integer, Kind)] -> StateT Cxt Q [Name])
-> [(Integer, Kind)] -> StateT Cxt Q [Name]
forall a b. (a -> b) -> a -> b
$ [Integer] -> Cxt -> [(Integer, Kind)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Integer -> [Integer]
forall t. Num t => t -> [t]
natsFrom Integer
0) Cxt
cTypes
             () <- Cxt -> [TyVarBndr] -> Cxt -> CxtStateQ ()
ensureCxt Cxt
cxt [TyVarBndr]
locTyvars Cxt
cTypes
             let varsTypesData :: [(Name, Kind, a)]
varsTypesData = [Name] -> Cxt -> [a] -> [(Name, Kind, a)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Name]
varNames Cxt
cTypes [a]
cData
             Clause -> CxtStateQ Clause
forall (m :: * -> *) a. Monad m => a -> m a
return (Clause -> CxtStateQ Clause) -> Clause -> CxtStateQ Clause
forall a b. (a -> b) -> a -> b
$ [Pat] -> Body -> [Dec] -> Clause
Clause [([(Name, Kind, a)] -> Pat
pFun [(Name, Kind, a)]
varsTypesData)]
                        (Exp -> Body
NormalB (Exp -> Body) -> Exp -> Body
forall a b. (a -> b) -> a -> b
$ [(Name, Kind, a)] -> Exp
eFun [(Name, Kind, a)]
varsTypesData) []

      -- ensure that MbTypeRepr a holds for each type a in cTypes
      ensureCxt :: Cxt -> [TyVarBndr] -> [TH.Type] -> CxtStateQ ()
      ensureCxt :: Cxt -> [TyVarBndr] -> Cxt -> CxtStateQ ()
ensureCxt Cxt
cxt [TyVarBndr]
locTyvars Cxt
cTypes =
          (() -> Kind -> CxtStateQ ()) -> () -> Cxt -> CxtStateQ ()
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((Kind -> CxtStateQ ()) -> () -> Kind -> CxtStateQ ()
forall a b. a -> b -> a
const (Cxt -> [TyVarBndr] -> Kind -> CxtStateQ ()
ensureCxt1 Cxt
cxt [TyVarBndr]
locTyvars)) () Cxt
cTypes

      -- FIXME: it is not possible (or, at least, not easy) to determine
      -- if MbTypeRepr a is implied from a current Cxt... so we just add
      -- everything we need to the returned Cxt, except for 
      ensureCxt1 :: Cxt -> [TyVarBndr] -> TH.Type -> CxtStateQ ()
      ensureCxt1 :: Cxt -> [TyVarBndr] -> Kind -> CxtStateQ ()
ensureCxt1 Cxt
cxt [TyVarBndr]
locTyvars Kind
t = CxtStateQ ()
forall a. HasCallStack => a
undefined
      {-
      ensureCxt1 cxt locTyvars t = do
        curCxt = get
        let fullCxt = cxt ++ curCxt
        isOk <- isMbTypeRepr fullCxt 

      isMbTypeRepr 
       -}