{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeOperators #-}

-- | Automatic generation of logic types.
module Kanren.TH (
  makeLogical,
  makeLogicals,

  -- * Logic representations
  makeLogicType,
  makeLogicTypes,
  LogicTypeRules,
  defaultLogicTypeRules,
  makeLogicTypeWith,
  makeLogicTypesWith,

  -- * 'Logical' instances
  makeLogicalInstance,
  makeLogicalInstances,

  -- * Exhaustive prisms
  makeExhaustivePrisms,
) where

import Control.Lens (from)
import Data.Char (isLower, isUpper, toLower, toUpper)
import Data.Foldable (foldl')
import GHC.Generics (Generic)
import Language.Haskell.TH hiding (bang)

import Kanren.Core
import Kanren.GenericLogical
import Kanren.Match (ExhaustivePrism, _Tagged)

-- | Generate a logic representation and a corresponding 'Logical' instance for
-- a given type.
--
-- Using this function requires you to enable the @DeriveGeneric@ and
-- @TypeFamilies@ extensions.
--
-- Consider the following type definition:
--
-- > data Tree a
-- >   = Empty
-- >   | Leaf a
-- >   | Tree a :* Tree a
--
-- @makeLogical ''Tree@ yields
--
-- > data LogicTree a
-- >   = LogicEmpty
-- >   | LogicLeaf (Term a)
-- >   | Term (Tree a) :?* Term (Tree a)
-- >   deriving (Generic)
-- >
-- > instance Logical a => Logical (Tree a) where
-- >   type Logic (Tree a) = LogicTree a
-- >   unify = genericUnify
-- >   walk = genericWalk
-- >   occursCheck = genericOccursCheck
-- >   inject = genericInject
-- >   extract = genericExtract
--
-- For details, see 'makeLogicType' and 'makeLogicalInstance'.
makeLogical :: Name -> Q [Dec]
makeLogical :: Name -> Q [Dec]
makeLogical Name
name = do
  TyConI Dec
declaration <- Name -> Q Info
reify Name
name
  Dec
logicType <- LogicTypeRules -> Name -> Dec -> Q Dec
makeLogicTypeWith' LogicTypeRules
logicTypeRules Name
name Dec
declaration
  [Dec]
logicalInstance <- Name -> Dec -> Name -> Dec -> Q [Dec]
makeLogicalInstance' Name
name Dec
declaration (Name -> Name
logicName Name
name) Dec
logicType
  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Dec
logicType Dec -> [Dec] -> [Dec]
forall a. a -> [a] -> [a]
: [Dec]
logicalInstance)
 where
  logicTypeRules :: LogicTypeRules
logicTypeRules = LogicTypeRules
defaultLogicTypeRules{derives = [ConT ''Generic]}

-- | Generate a logic representation and a corresponding 'Logical' instance for
-- each given type. This works like 'makeLogical', but better suits mutually
-- recursive types.
makeLogicals :: [Name] -> Q [Dec]
makeLogicals :: [Name] -> Q [Dec]
makeLogicals = (Name -> Q [Dec]) -> [Name] -> Q [Dec]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Name -> Q [Dec]
makeLogical

-- | Settings for generating a type's logic representation.
newtype LogicTypeRules = LogicTypeRules
  { LogicTypeRules -> [Type]
derives :: [Type]
  -- ^ Instances that should be derived for the logical representation.
  }

-- | Default 'LogicTypeRules'. Does not derive any instances for the logical
-- representation.
defaultLogicTypeRules :: LogicTypeRules
defaultLogicTypeRules :: LogicTypeRules
defaultLogicTypeRules = LogicTypeRules{derives :: [Type]
derives = []}

-- | Generate a logic representation for a given type.
--
-- Consider the following type definition:
--
-- > data Tree a
-- >   = Empty
-- >   | Leaf a
-- >   | Tree a :* Tree a
--
-- @makeLogicType ''Tree@ yields
--
-- > data LogicTree a
-- >   = LogicEmpty
-- >   | LogicLeaf (Term a)
-- >   | Term (Tree a) :?* Term (Tree a)
--
-- For @newtype@s, it doesn't make sense to introduce another layer of
-- variables. Hence, 'Logic' will be used instead of 'Term'.
--
-- > newtype BetterInt = BetterInt Int
-- > makeLogicType ''BetterInt
-- > -- ^ newtype LogicBetterInt = LogicBetterInt (Logic Int)
makeLogicType :: Name -> Q [Dec]
makeLogicType :: Name -> Q [Dec]
makeLogicType = LogicTypeRules -> Name -> Q [Dec]
makeLogicTypeWith LogicTypeRules
defaultLogicTypeRules

-- | 'makeLogicType', but allows configuring how the logical representation is
-- generated.
makeLogicTypeWith :: LogicTypeRules -> Name -> Q [Dec]
makeLogicTypeWith :: LogicTypeRules -> Name -> Q [Dec]
makeLogicTypeWith LogicTypeRules
rules Name
name = do
  TyConI Dec
declaration <- Name -> Q Info
reify Name
name
  Dec
logicType <- LogicTypeRules -> Name -> Dec -> Q Dec
makeLogicTypeWith' LogicTypeRules
rules Name
name Dec
declaration
  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return [Dec
logicType]

makeLogicTypeWith' :: LogicTypeRules -> Name -> Dec -> Q Dec
makeLogicTypeWith' :: LogicTypeRules -> Name -> Dec -> Q Dec
makeLogicTypeWith' (LogicTypeRules{[Type]
derives :: LogicTypeRules -> [Type]
derives :: [Type]
derives}) Name
name Dec
declaration = do
  let deriv :: [DerivClause]
deriv
        | [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
derives = []
        | Bool
otherwise = [Maybe DerivStrategy -> [Type] -> DerivClause
DerivClause Maybe DerivStrategy
forall a. Maybe a
Nothing [Type]
derives]

  case Dec
declaration of
    -- data T = A B ==> data LogicT = LogicA (Term B)
    DataD [Type]
constraints Name
_ [TyVarBndr ()]
variables Maybe Type
kind [Con]
constructors [DerivClause]
_ -> do
      let name' :: Name
name' = Name -> Name
logicName Name
name
      let constructors' :: [Con]
constructors' = Name -> [Con] -> [Con]
logicConstructors ''Term [Con]
constructors
      Dec -> Q Dec
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type]
-> Name
-> [TyVarBndr ()]
-> Maybe Type
-> [Con]
-> [DerivClause]
-> Dec
DataD [Type]
constraints Name
name' [TyVarBndr ()]
variables Maybe Type
kind [Con]
constructors' [DerivClause]
deriv)
    -- newtype T = A B = newtype LogicT = LogicA (Logic B)
    NewtypeD [Type]
constraints Name
_ [TyVarBndr ()]
variables Maybe Type
kind Con
constructor [DerivClause]
_ -> do
      let name' :: Name
name' = Name -> Name
logicName Name
name
      let constructor' :: Con
constructor' = Name -> Con -> Con
logicConstructor ''Logic Con
constructor
      Dec -> Q Dec
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type]
-> Name
-> [TyVarBndr ()]
-> Maybe Type
-> Con
-> [DerivClause]
-> Dec
NewtypeD [Type]
constraints Name
name' [TyVarBndr ()]
variables Maybe Type
kind Con
constructor' [DerivClause]
deriv)
    Dec
other -> String -> Q Dec
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Expected a `data` or `newtype` declaration, but got:\n" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Dec -> String
forall a. Show a => a -> String
show Dec
other)

-- | Generate a logic representation for several types. This works like
-- 'makeLogicType', but better suits mutually recursive types.
makeLogicTypes :: [Name] -> Q [Dec]
makeLogicTypes :: [Name] -> Q [Dec]
makeLogicTypes = (Name -> Q [Dec]) -> [Name] -> Q [Dec]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Name -> Q [Dec]
makeLogicType

-- | 'makeLogicTypes', but allows configuring how the logical representations
-- are generated.
makeLogicTypesWith :: LogicTypeRules -> [Name] -> Q [Dec]
makeLogicTypesWith :: LogicTypeRules -> [Name] -> Q [Dec]
makeLogicTypesWith = (Name -> Q [Dec]) -> [Name] -> Q [Dec]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((Name -> Q [Dec]) -> [Name] -> Q [Dec])
-> (LogicTypeRules -> Name -> Q [Dec])
-> LogicTypeRules
-> [Name]
-> Q [Dec]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LogicTypeRules -> Name -> Q [Dec]
makeLogicTypeWith

-- | Generate a logic name for any name. @Tree@ becomes @LogicTree@, @age@
-- becomes @logicAge@, @:^@ becomes @:?^@.
logicName :: Name -> Name
logicName :: Name -> Name
logicName Name
name = String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ case Name -> String
nameBase Name
name of
  String
"" -> String
""
  Char
':' : String
rest -> String
":?" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
rest
  Char
firstLetter : String
rest
    | Char -> Bool
isUpper Char
firstLetter -> String
"Logic" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
rest'
    | Char -> Bool
isLower Char
firstLetter -> String
"logic" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
rest'
    | Bool
otherwise -> Char
'?' Char -> String -> String
forall a. a -> [a] -> [a]
: String
rest'
   where
    rest' :: String
rest' = Char -> Char
toUpper Char
firstLetter Char -> String -> String
forall a. a -> [a] -> [a]
: String
rest

logicNames :: [Name] -> [Name]
logicNames :: [Name] -> [Name]
logicNames = (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
logicName

logicConstructor :: Name -> Con -> Con
-- C Int a ==> LogicC (Term Int) (Term a)
logicConstructor :: Name -> Con -> Con
logicConstructor Name
wrapper (NormalC Name
name [BangType]
fields) =
  Name -> [BangType] -> Con
NormalC (Name -> Name
logicName Name
name) (Name -> [BangType] -> [BangType]
wrapBangTypes Name
wrapper [BangType]
fields)
-- C { v :: Int, w :: a } ==>
-- LogicC { logicV :: Term Int, logicW :: Term a }
logicConstructor Name
wrapper (RecC Name
name [VarBangType]
fields) =
  Name -> [VarBangType] -> Con
RecC (Name -> Name
logicName Name
name) (Name -> [VarBangType] -> [VarBangType]
wrapVarBangTypes Name
wrapper [VarBangType]
fields)
-- Int :+ a ==> Term Int :?+ Term a
logicConstructor Name
wrapper (InfixC BangType
left Name
name BangType
right) =
  BangType -> Name -> BangType -> Con
InfixC BangType
left' (Name -> Name
logicName Name
name) BangType
right'
 where
  left' :: BangType
left' = Name -> BangType -> BangType
wrapBangType Name
wrapper BangType
left
  right' :: BangType
right' = Name -> BangType -> BangType
wrapBangType Name
wrapper BangType
right
-- forall a. Eq a => C ... ==> forall a. Eq a => LogicC ...
logicConstructor Name
wrapper (ForallC [TyVarBndr Specificity]
vars [Type]
constraints Con
constructor) =
  [TyVarBndr Specificity] -> [Type] -> Con -> Con
ForallC [TyVarBndr Specificity]
vars [Type]
constraints (Name -> Con -> Con
logicConstructor Name
wrapper Con
constructor)
-- C1, C2 :: a -> T b ==> LogicC1, LogicC2 :: Term a -> LogicT b
logicConstructor Name
wrapper (GadtC [Name]
names [BangType]
fields Type
returnType) =
  [Name] -> [BangType] -> Type -> Con
GadtC ([Name] -> [Name]
logicNames [Name]
names) (Name -> [BangType] -> [BangType]
wrapBangTypes Name
wrapper [BangType]
fields) (Type -> Type
logicGadt Type
returnType)
-- C1, C2 :: { v :: Int } -> T b ==>
-- LogicC1, LogicC2 :: { logicV :: Term Int } -> LogicT b
logicConstructor Name
wrapper (RecGadtC [Name]
names [VarBangType]
fields Type
returnType) =
  [Name] -> [VarBangType] -> Type -> Con
RecGadtC ([Name] -> [Name]
logicNames [Name]
names) (Name -> [VarBangType] -> [VarBangType]
wrapVarBangTypes Name
wrapper [VarBangType]
fields) (Type -> Type
logicGadt Type
returnType)

logicConstructors :: Name -> [Con] -> [Con]
logicConstructors :: Name -> [Con] -> [Con]
logicConstructors = (Con -> Con) -> [Con] -> [Con]
forall a b. (a -> b) -> [a] -> [b]
map ((Con -> Con) -> [Con] -> [Con])
-> (Name -> Con -> Con) -> Name -> [Con] -> [Con]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Con -> Con
logicConstructor

wrapType :: Name -> Type -> Type
wrapType :: Name -> Type -> Type
wrapType = Type -> Type -> Type
AppT (Type -> Type -> Type) -> (Name -> Type) -> Name -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Type
ConT

wrapBangType :: Name -> BangType -> BangType
wrapBangType :: Name -> BangType -> BangType
wrapBangType = (Type -> Type) -> BangType -> BangType
forall a b. (a -> b) -> (Bang, a) -> (Bang, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Type -> Type) -> BangType -> BangType)
-> (Name -> Type -> Type) -> Name -> BangType -> BangType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Type -> Type
wrapType

wrapBangTypes :: Name -> [BangType] -> [BangType]
wrapBangTypes :: Name -> [BangType] -> [BangType]
wrapBangTypes = (BangType -> BangType) -> [BangType] -> [BangType]
forall a b. (a -> b) -> [a] -> [b]
map ((BangType -> BangType) -> [BangType] -> [BangType])
-> (Name -> BangType -> BangType)
-> Name
-> [BangType]
-> [BangType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> BangType -> BangType
wrapBangType

wrapVarBangType :: Name -> VarBangType -> VarBangType
wrapVarBangType :: Name -> VarBangType -> VarBangType
wrapVarBangType Name
wrapper (Name
name, Bang
bang, Type
typ) =
  (Name -> Name
logicName Name
name, Bang
bang, Name -> Type -> Type
wrapType Name
wrapper Type
typ)

wrapVarBangTypes :: Name -> [VarBangType] -> [VarBangType]
wrapVarBangTypes :: Name -> [VarBangType] -> [VarBangType]
wrapVarBangTypes = (VarBangType -> VarBangType) -> [VarBangType] -> [VarBangType]
forall a b. (a -> b) -> [a] -> [b]
map ((VarBangType -> VarBangType) -> [VarBangType] -> [VarBangType])
-> (Name -> VarBangType -> VarBangType)
-> Name
-> [VarBangType]
-> [VarBangType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> VarBangType -> VarBangType
wrapVarBangType

logicGadt :: Type -> Type
-- forall a. Eq a => T ==> forall a. Eq a => LogicT
logicGadt :: Type -> Type
logicGadt (ForallT [TyVarBndr Specificity]
vars [Type]
constraints Type
typ) =
  [TyVarBndr Specificity] -> [Type] -> Type -> Type
ForallT [TyVarBndr Specificity]
vars [Type]
constraints (Type -> Type
logicGadt Type
typ)
-- forall a -> T ==> forall a -> LogicT
logicGadt (ForallVisT [TyVarBndr ()]
vars Type
typ) = [TyVarBndr ()] -> Type -> Type
ForallVisT [TyVarBndr ()]
vars Type
typ
-- T a ==> LogicT a
logicGadt (AppT Type
typ Type
arg) = Type -> Type -> Type
AppT (Type -> Type
logicGadt Type
typ) Type
arg
-- T @k ==> LogicT @k
logicGadt (AppKindT Type
typ Type
kind) = Type -> Type -> Type
AppT (Type -> Type
logicGadt Type
typ) Type
kind
logicGadt (VarT Name
var) = Name -> Type
VarT Name
var
-- T ==> LogicT
logicGadt (ConT Name
name) = Name -> Type
ConT (Name -> Name
logicName Name
name)
-- 'T ==> 'LogicT
logicGadt (PromotedT Name
name) = Name -> Type
PromotedT (Name -> Name
logicName Name
name)
-- A :+ B ==> A :?+ B
logicGadt (InfixT Type
left Name
name Type
right) = Type -> Name -> Type -> Type
InfixT Type
left (Name -> Name
logicName Name
name) Type
right
logicGadt (UInfixT Type
left Name
name Type
right) = Type -> Name -> Type -> Type
UInfixT Type
left (Name -> Name
logicName Name
name) Type
right
-- A :+: B ==> A :?+: B
logicGadt (PromotedInfixT Type
left Name
name Type
right) =
  Type -> Name -> Type -> Type
PromotedInfixT Type
left (Name -> Name
logicName Name
name) Type
right
logicGadt (PromotedUInfixT Type
left Name
name Type
right) =
  Type -> Name -> Type -> Type
PromotedUInfixT Type
left (Name -> Name
logicName Name
name) Type
right
-- (T) ==> (LogicT)
logicGadt (ParensT Type
typ) = Type -> Type
ParensT (Type -> Type
logicGadt Type
typ)
-- ?x :: T ===> ?x :: LogicT
logicGadt (ImplicitParamT String
param Type
typ) = String -> Type -> Type
ImplicitParamT String
param (Type -> Type
logicGadt Type
typ)
logicGadt Type
other = Type
other -- give up. shouldn't appear in a GADT anyway

data LogicalInstanceTypeInfo
  = Data
  | Newtype Name Name

-- | Generate a 'Logical' instance, given a type and its logical representation.
--
-- Currently, the instance relies on @"GenericLogical"@, so both types need to
-- have a 'Generic' instance. When using 'makeLogical', the logical
-- representation will have a derived 'Generic' instance.
--
-- For each type variable, there will be a 'Logical' constraint.
--
-- Since 'Logical' includes a type family definition, using this function
-- requires enabling the @TypeFamilies@ extension.
--
-- Consider the following declarations:
--
-- > data Tree a
-- >   = Empty
-- >   | Leaf a
-- >   | Tree a :* Tree a
-- >   deriving (Generic)
-- > makeLogicType ''Tree
-- > deriving instance Generic (LogicTree a)
--
-- @makeLogicalInstance ''Tree ''LogicTree@ yields
--
-- > instance Logical a => Logical (Tree a) where
-- >   type Logic (Tree a) = LogicTree a
-- >   unify = genericUnify
-- >   walk = genericWalk
-- >   occursCheck = genericOccursCheck
-- >   inject = genericInject
-- >   extract = genericExtract
makeLogicalInstance :: Name -> Name -> Q [Dec]
makeLogicalInstance :: Name -> Name -> Q [Dec]
makeLogicalInstance Name
name Name
logicTypeName = do
  TyConI Dec
declaration <- Name -> Q Info
reify Name
name
  TyConI Dec
logicDeclaration <- Name -> Q Info
reify Name
logicTypeName
  Name -> Dec -> Name -> Dec -> Q [Dec]
makeLogicalInstance' Name
name Dec
declaration Name
logicTypeName Dec
logicDeclaration

makeLogicalInstance' :: Name -> Dec -> Name -> Dec -> Q [Dec]
makeLogicalInstance' :: Name -> Dec -> Name -> Dec -> Q [Dec]
makeLogicalInstance' Name
name Dec
declaration Name
logicTypeName Dec
logicDeclaration = do
  ([TyVarBndr ()]
variables, LogicalInstanceTypeInfo
typeInfo) <- case Dec
declaration of
    DataD [Type]
_ Name
_ [TyVarBndr ()]
variables Maybe Type
_ [Con]
_ [DerivClause]
_ -> ([TyVarBndr ()], LogicalInstanceTypeInfo)
-> Q ([TyVarBndr ()], LogicalInstanceTypeInfo)
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyVarBndr ()]
variables, LogicalInstanceTypeInfo
Data)
    NewtypeD [Type]
_ Name
_ [TyVarBndr ()]
variables Maybe Type
_ Con
constructor [DerivClause]
_ -> do
      Name
con <- Con -> Q Name
extractConstructorName Con
constructor
      NewtypeD [Type]
_ Name
_ [TyVarBndr ()]
_ Maybe Type
_ Con
logicC [DerivClause]
_ <- Dec -> Q Dec
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Dec
logicDeclaration
      Name
logicCon <- Con -> Q Name
extractConstructorName Con
logicC
      ([TyVarBndr ()], LogicalInstanceTypeInfo)
-> Q ([TyVarBndr ()], LogicalInstanceTypeInfo)
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyVarBndr ()]
variables, Name -> Name -> LogicalInstanceTypeInfo
Newtype Name
con Name
logicCon)
    Dec
other -> String -> Q ([TyVarBndr ()], LogicalInstanceTypeInfo)
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Expected a `data` or `newtype` declaration, but got:\n" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Dec -> String
forall a. Show a => a -> String
show Dec
other)

  let constraints :: [Type]
constraints = [TyVarBndr ()] -> [Type]
forall flag. [TyVarBndr flag] -> [Type]
logicalConstraints [TyVarBndr ()]
variables
  let typ :: Type
typ = Name -> [TyVarBndr ()] -> Type
forall flag. Name -> [TyVarBndr flag] -> Type
applyVariables Name
name [TyVarBndr ()]
variables
  let logicTyp :: Type
logicTyp = Name -> [TyVarBndr ()] -> Type
forall flag. Name -> [TyVarBndr flag] -> Type
applyVariables Name
logicTypeName [TyVarBndr ()]
variables

  [Dec]
logicTypeFamily <- [d|type instance Logic $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
typ) = $(Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
logicTyp)|]
  [Dec]
methods <- LogicalInstanceTypeInfo -> Q [Dec]
makeMethods LogicalInstanceTypeInfo
typeInfo
  let body :: [Dec]
body = [Dec]
logicTypeFamily [Dec] -> [Dec] -> [Dec]
forall a. Semigroup a => a -> a -> a
<> [Dec]
methods
  let instanc :: Dec
instanc = Maybe Overlap -> [Type] -> Type -> [Dec] -> Dec
InstanceD Maybe Overlap
forall a. Maybe a
Nothing [Type]
constraints (Type -> Type -> Type
AppT (Name -> Type
ConT ''Logical) Type
typ) [Dec]
body
  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return [Dec
instanc]

makeMethods :: LogicalInstanceTypeInfo -> Q [Dec]
makeMethods :: LogicalInstanceTypeInfo -> Q [Dec]
makeMethods LogicalInstanceTypeInfo
Data =
  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
    [ Name -> Name -> Dec
method 'unify 'genericUnify
    , Name -> Name -> Dec
method 'walk 'genericWalk
    , Name -> Name -> Dec
method 'occursCheck 'genericOccursCheck
    , Name -> Name -> Dec
method 'inject 'genericInject
    , Name -> Name -> Dec
method 'extract 'genericExtract
    ]
makeMethods (Newtype Name
con Name
logicCon) =
  [Q Dec] -> Q [Dec]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a. Applicative f => [f a] -> f [a]
sequenceA
    [ Name -> Q Dec
delegateUnify Name
logicCon
    , Name -> Q Dec
delegateWalk Name
logicCon
    , Name -> Q Dec
delegateOccursCheck Name
logicCon
    , Name -> Name -> Q Dec
delegateInject Name
con Name
logicCon
    , Name -> Name -> Q Dec
delegateExtract Name
con Name
logicCon
    ]

extractConstructorName :: Con -> Q Name
extractConstructorName :: Con -> Q Name
extractConstructorName (NormalC Name
con [BangType]
_) = Name -> Q Name
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
con
extractConstructorName (RecC Name
con [VarBangType]
_) = Name -> Q Name
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
con
extractConstructorName Con
other = String -> Q Name
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Strange constructor for a `newtype`:\n" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Con -> String
forall a. Show a => a -> String
show Con
other)

-- | Generate 'Logical' instances, given pairs of a type and its logical
-- representation. This works like 'makeLogicalInstance', but better suits
-- mutually recursive types.
makeLogicalInstances :: [(Name, Name)] -> Q [Dec]
makeLogicalInstances :: [(Name, Name)] -> Q [Dec]
makeLogicalInstances = ((Name, Name) -> Q [Dec]) -> [(Name, Name)] -> Q [Dec]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((Name -> Name -> Q [Dec]) -> (Name, Name) -> Q [Dec]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Name -> Q [Dec]
makeLogicalInstance)

method :: Name -> Name -> Dec
method :: Name -> Name -> Dec
method Name
name Name
generic = Name -> [Clause] -> Dec
FunD Name
name [[Pat] -> Body -> [Dec] -> Clause
Clause [] (Exp -> Body
NormalB (Name -> Exp
VarE Name
generic)) []]

delegateUnify :: Name -> Q Dec
delegateUnify :: Name -> Q Dec
delegateUnify Name
logicCon = do
  Name
left <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"left"
  Name
right <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"right"
  let leftSide :: [Pat]
leftSide = [Name -> [Type] -> [Pat] -> Pat
ConP Name
logicCon [] [Name -> Pat
VarP Name
left], Name -> [Type] -> [Pat] -> Pat
ConP Name
logicCon [] [Name -> Pat
VarP Name
right]]
  let rightSide :: Exp
rightSide = Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'unify) (Name -> Exp
VarE Name
left)) (Name -> Exp
VarE Name
right)
  Dec -> Q Dec
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> [Clause] -> Dec
FunD 'unify [[Pat] -> Body -> [Dec] -> Clause
Clause [Pat]
leftSide (Exp -> Body
NormalB Exp
rightSide) []])

delegateWalk :: Name -> Q Dec
delegateWalk :: Name -> Q Dec
delegateWalk Name
logicCon = do
  Name
state <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"state"
  Name
inner <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"inner"
  let leftSide :: [Pat]
leftSide = [Name -> Pat
VarP Name
state, Name -> [Type] -> [Pat] -> Pat
ConP Name
logicCon [] [Name -> Pat
VarP Name
inner]]
  let delegated :: Exp
delegated = Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'walk) (Name -> Exp
VarE Name
state)) (Name -> Exp
VarE Name
inner)
  let rightSide :: Exp
rightSide = Exp -> Exp -> Exp
AppE (Name -> Exp
ConE Name
logicCon) Exp
delegated
  Dec -> Q Dec
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> [Clause] -> Dec
FunD 'walk [[Pat] -> Body -> [Dec] -> Clause
Clause [Pat]
leftSide (Exp -> Body
NormalB Exp
rightSide) []])

delegateOccursCheck :: Name -> Q Dec
delegateOccursCheck :: Name -> Q Dec
delegateOccursCheck Name
logicCon = do
  Name
variable <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"variable"
  Name
inner <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"inner"
  let leftSide :: [Pat]
leftSide = [Name -> Pat
VarP Name
variable, Name -> [Type] -> [Pat] -> Pat
ConP Name
logicCon [] [Name -> Pat
VarP Name
inner]]
  let rightSide :: Exp
rightSide = Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'occursCheck) (Name -> Exp
VarE Name
variable)) (Name -> Exp
VarE Name
inner)
  Dec -> Q Dec
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> [Clause] -> Dec
FunD 'occursCheck [[Pat] -> Body -> [Dec] -> Clause
Clause [Pat]
leftSide (Exp -> Body
NormalB Exp
rightSide) []])

delegateInject :: Name -> Name -> Q Dec
delegateInject :: Name -> Name -> Q Dec
delegateInject Name
con Name
logicCon = do
  Name
inner <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"inner"
  let leftSide :: [Pat]
leftSide = [Name -> [Type] -> [Pat] -> Pat
ConP Name
con [] [Name -> Pat
VarP Name
inner]]
  let rightSide :: Exp
rightSide = Exp -> Exp -> Exp
AppE (Name -> Exp
ConE Name
logicCon) (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'inject) (Name -> Exp
VarE Name
inner))
  Dec -> Q Dec
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> [Clause] -> Dec
FunD 'inject [[Pat] -> Body -> [Dec] -> Clause
Clause [Pat]
leftSide (Exp -> Body
NormalB Exp
rightSide) []])

delegateExtract :: Name -> Name -> Q Dec
delegateExtract :: Name -> Name -> Q Dec
delegateExtract Name
con Name
logicCon = do
  Name
inner <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"inner"
  let leftSide :: [Pat]
leftSide = [Name -> [Type] -> [Pat] -> Pat
ConP Name
logicCon [] [Name -> Pat
VarP Name
inner]]
  let rightSide :: Exp
rightSide = Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'fmap) (Name -> Exp
ConE Name
con)) (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'extract) (Name -> Exp
VarE Name
inner))
  Dec -> Q Dec
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> [Clause] -> Dec
FunD 'extract [[Pat] -> Body -> [Dec] -> Clause
Clause [Pat]
leftSide (Exp -> Body
NormalB Exp
rightSide) []])

logicalConstraints :: [TyVarBndr flag] -> Cxt
logicalConstraints :: forall flag. [TyVarBndr flag] -> [Type]
logicalConstraints = (TyVarBndr flag -> Type) -> [TyVarBndr flag] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndr flag -> Type
forall flag. TyVarBndr flag -> Type
logicalConstraint

logicalConstraint :: TyVarBndr flag -> Pred
logicalConstraint :: forall flag. TyVarBndr flag -> Type
logicalConstraint TyVarBndr flag
variable = Type -> Type -> Type
AppT (Name -> Type
ConT ''Logical) (TyVarBndr flag -> Type
forall flag. TyVarBndr flag -> Type
variableName TyVarBndr flag
variable)

variableName :: TyVarBndr flag -> Type
variableName :: forall flag. TyVarBndr flag -> Type
variableName (PlainTV Name
name flag
_) = Name -> Type
VarT Name
name
variableName (KindedTV Name
name flag
_ Type
_) = Name -> Type
VarT Name
name

applyVariables :: Name -> [TyVarBndr flag] -> Type
applyVariables :: forall flag. Name -> [TyVarBndr flag] -> Type
applyVariables = (Type -> TyVarBndr flag -> Type)
-> Type -> [TyVarBndr flag] -> Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Type
typ -> Type -> Type -> Type
AppT Type
typ (Type -> Type)
-> (TyVarBndr flag -> Type) -> TyVarBndr flag -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarBndr flag -> Type
forall flag. TyVarBndr flag -> Type
variableName) (Type -> [TyVarBndr flag] -> Type)
-> (Name -> Type) -> Name -> [TyVarBndr flag] -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Type
ConT

-- | Generate 'ExhaustivePrism's for a given (supposedly logic) type.
--
-- This function expects that you already have regular prisms in the scope whose
-- names are constructor names prefixed with @_@ (i.e. you used
-- 'Control.Lens.TH.makePrisms'). Then, exhaustive prisms will have a prime in
-- the end (or an exclamation mark for infix constructors).
--
-- Consider the following declarations:
--
-- > data Tree a
-- >   = Empty
-- >   | Leaf a
-- >   | Tree a :* Tree a
-- >   deriving (Generic)
-- > makeLogicType ''Tree
-- > makePrisms ''LogicTree
--
-- @makeExhaustivePrisms ''LogicTree@ yields (sans short tags)
--
-- > _LogicEmpty' :: ExhaustivePrism (LogicTree a) (e, l, n) (e', l, n) () e e'
-- > _LogicEmpty' = from _Tagged . _LogicEmpty . _Tagged
-- >
-- > _LogicLeaf' :: ExhaustivePrism (LogicTree a) (e, l, n) (e, l', n) (Term a) l l'
-- > _LogicLeaf' = from _Tagged . _LogicLeaf . _Tagged
-- >
-- > (.:?*!) :: ExhaustivePrism (LogicTree a) (e, l, n) (e, l, n') (Term (Tree a), Term (Tree a)) n n'
-- > (.:?*!) = from _Tagged . (.:?*) . _Tagged
makeExhaustivePrisms :: Name -> Q [Dec]
makeExhaustivePrisms :: Name -> Q [Dec]
makeExhaustivePrisms Name
name = do
  TyConI Dec
declaration <- Name -> Q Info
reify Name
name
  ([TyVarBndr ()]
variables, [Constructor]
constructors) <- case Dec
declaration of
    DataD [Type]
_ Name
_ [TyVarBndr ()]
variables Maybe Type
_ [Con]
constructors [DerivClause]
_ ->
      ([TyVarBndr ()]
variables,) ([Constructor] -> ([TyVarBndr ()], [Constructor]))
-> Q [Constructor] -> Q ([TyVarBndr ()], [Constructor])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Con] -> Q [Constructor]
normalizeConstructors [Con]
constructors
    NewtypeD [Type]
_ Name
_ [TyVarBndr ()]
variables Maybe Type
_ Con
constructor [DerivClause]
_ ->
      ([TyVarBndr ()]
variables,) ([Constructor] -> ([TyVarBndr ()], [Constructor]))
-> Q [Constructor] -> Q ([TyVarBndr ()], [Constructor])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Con -> Q [Constructor]
normalizeConstructor Con
constructor
    Dec
other -> String -> Q ([TyVarBndr ()], [Constructor])
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Expected a `data` or `newtype` declaration, but got:\n" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Dec -> String
forall a. Show a => a -> String
show Dec
other)
  let tags :: [Name]
tags = [Constructor] -> [Name]
makeTags [Constructor]
constructors
  let typ :: Type
typ = Name -> [TyVarBndr ()] -> Type
forall flag. Name -> [TyVarBndr flag] -> Type
applyVariables Name
name [TyVarBndr ()]
variables
  let prismsInfo :: [PrismInfo]
prismsInfo = ([(Name, Constructor)]
 -> (Name, Constructor) -> [(Name, Constructor)] -> PrismInfo)
-> [(Name, Constructor)] -> [PrismInfo]
forall a b. ([a] -> a -> [a] -> b) -> [a] -> [b]
focusEach [(Name, Constructor)]
-> (Name, Constructor) -> [(Name, Constructor)] -> PrismInfo
makePrismInfo ([Name] -> [Constructor] -> [(Name, Constructor)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
tags [Constructor]
constructors)
  (PrismInfo -> Q [Dec]) -> [PrismInfo] -> Q [Dec]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Type -> Type -> PrismInfo -> Q [Dec]
makePrism Type
typ ([Name] -> Type
tagsToType [Name]
tags)) [PrismInfo]
prismsInfo

data Constructor = Constructor Name [Type]

normalizeConstructor :: Con -> Q [Constructor]
normalizeConstructor :: Con -> Q [Constructor]
normalizeConstructor (NormalC Name
name [BangType]
fields) =
  [Constructor] -> Q [Constructor]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return [Name -> [Type] -> Constructor
Constructor Name
name ([BangType] -> [Type]
extractBangTypes [BangType]
fields)]
normalizeConstructor (RecC Name
name [VarBangType]
fields) =
  [Constructor] -> Q [Constructor]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return [Name -> [Type] -> Constructor
Constructor Name
name ([VarBangType] -> [Type]
extractVarBangTypes [VarBangType]
fields)]
normalizeConstructor (InfixC (Bang
_, Type
left) Name
name (Bang
_, Type
right)) =
  [Constructor] -> Q [Constructor]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return [Name -> [Type] -> Constructor
Constructor Name
name [Type
left, Type
right]]
normalizeConstructor ForallC{} =
  String -> Q [Constructor]
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Generation of exhaustive prisms for existential types is not supported (yet)"
normalizeConstructor (GadtC [Name]
names [BangType]
fields Type
_) =
  [Constructor] -> Q [Constructor]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return [Name -> [Type] -> Constructor
Constructor Name
name ([BangType] -> [Type]
extractBangTypes [BangType]
fields) | Name
name <- [Name]
names]
normalizeConstructor (RecGadtC [Name]
names [VarBangType]
fields Type
_) =
  [Constructor] -> Q [Constructor]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return [Name -> [Type] -> Constructor
Constructor Name
name ([VarBangType] -> [Type]
extractVarBangTypes [VarBangType]
fields) | Name
name <- [Name]
names]

normalizeConstructors :: [Con] -> Q [Constructor]
normalizeConstructors :: [Con] -> Q [Constructor]
normalizeConstructors = (Con -> Q [Constructor]) -> [Con] -> Q [Constructor]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Con -> Q [Constructor]
normalizeConstructor

extractBangTypes :: [BangType] -> [Type]
extractBangTypes :: [BangType] -> [Type]
extractBangTypes = (BangType -> Type) -> [BangType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map BangType -> Type
forall a b. (a, b) -> b
snd

extractVarBangTypes :: [VarBangType] -> [Type]
extractVarBangTypes :: [VarBangType] -> [Type]
extractVarBangTypes = (VarBangType -> Type) -> [VarBangType] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
_, Bang
_, Type
typ) -> Type
typ)

type Tag = Name
type Tags = [Tag]

makeTags :: [Constructor] -> Tags
makeTags :: [Constructor] -> [Name]
makeTags = (Int -> Constructor -> Name) -> [Int] -> [Constructor] -> [Name]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Constructor -> Name
makeTag [Int
1 ..]

makeTag :: Int -> Constructor -> Tag
makeTag :: Int -> Constructor -> Name
makeTag Int
n (Constructor Name
name [Type]
_) = String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ case Name -> String
nameBase Name
name of
  String
"" -> String
""
  Char
firstLetter : String
rest
    | Char -> Bool
isUpper Char
firstLetter -> Char -> Char
toLower Char
firstLetter Char -> String -> String
forall a. a -> [a] -> [a]
: String
rest
    | Bool
otherwise -> String
"op" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
n

focusEach :: ([a] -> a -> [a] -> b) -> [a] -> [b]
focusEach :: forall a b. ([a] -> a -> [a] -> b) -> [a] -> [b]
focusEach = [a] -> ([a] -> a -> [a] -> b) -> [a] -> [b]
forall {a} {a}. [a] -> ([a] -> a -> [a] -> a) -> [a] -> [a]
go []
 where
  go :: [a] -> ([a] -> a -> [a] -> a) -> [a] -> [a]
go [a]
_ [a] -> a -> [a] -> a
_ [] = []
  go [a]
previous [a] -> a -> [a] -> a
f (a
current : [a]
next) =
    [a] -> a -> [a] -> a
f [a]
previous a
current [a]
next a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> ([a] -> a -> [a] -> a) -> [a] -> [a]
go ([a]
previous [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a
current]) [a] -> a -> [a] -> a
f [a]
next

data PrismInfo = PrismInfo
  { PrismInfo -> Name
regularPrism :: Name
  , PrismInfo -> Name
exhaustivePrism :: Name
  , PrismInfo -> [Name]
m' :: Tags
  , PrismInfo -> Type
a :: Type
  , PrismInfo -> Name
t :: Tag
  , PrismInfo -> Name
t' :: Tag
  }

makePrismInfo
  :: [(Tag, Constructor)]
  -> (Tag, Constructor)
  -> [(Tag, Constructor)]
  -> PrismInfo
makePrismInfo :: [(Name, Constructor)]
-> (Name, Constructor) -> [(Name, Constructor)] -> PrismInfo
makePrismInfo [(Name, Constructor)]
previous (Name
t, Constructor Name
name [Type]
fields) [(Name, Constructor)]
next =
  PrismInfo{Name
regularPrism :: Name
regularPrism :: Name
regularPrism, Name
exhaustivePrism :: Name
exhaustivePrism :: Name
exhaustivePrism, [Name]
m' :: [Name]
m' :: [Name]
m', Type
a :: Type
a :: Type
a, Name
t :: Name
t :: Name
t, Name
t' :: Name
t' :: Name
t'}
 where
  regularPrism :: Name
regularPrism = String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ case Name -> String
nameBase Name
name of
    String
"" -> String
""
    name' :: String
name'@(Char
firstLetter : String
_)
      | Char -> Bool
isUpper Char
firstLetter -> Char
'_' Char -> String -> String
forall a. a -> [a] -> [a]
: String
name'
      | Bool
otherwise -> Char
'.' Char -> String -> String
forall a. a -> [a] -> [a]
: String
name'

  exhaustivePrism :: Name
exhaustivePrism = Name -> Name
addPrime Name
regularPrism
  previousTags :: [Name]
previousTags = ((Name, Constructor) -> Name) -> [(Name, Constructor)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Constructor) -> Name
forall a b. (a, b) -> a
fst [(Name, Constructor)]
previous
  nextTags :: [Name]
nextTags = ((Name, Constructor) -> Name) -> [(Name, Constructor)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Constructor) -> Name
forall a b. (a, b) -> a
fst [(Name, Constructor)]
next
  t' :: Name
t' = Name -> Name
addPrime Name
t
  m' :: [Name]
m' = [Name]
previousTags [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ (Name
t' Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
nextTags)
  a :: Type
a = [Type] -> Type
fieldsToType [Type]
fields

addPrime :: Name -> Name
addPrime :: Name -> Name
addPrime Name
name = String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ case Name -> String
nameBase Name
name of
  String
"" -> String
""
  name' :: String
name'@(Char
'.' : String
_) -> String
name' String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"!"
  String
name' -> String
name' String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"'"

fieldsToType :: [Type] -> Type
fieldsToType :: [Type] -> Type
fieldsToType [Type
x] = Type
x
fieldsToType [Type]
fields = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Type -> Type -> Type
AppT (Int -> Type
TupleT ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
fields)) [Type]
fields

tagsToType :: Tags -> Type
tagsToType :: [Name] -> Type
tagsToType = [Type] -> Type
fieldsToType ([Type] -> Type) -> ([Name] -> [Type]) -> [Name] -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Type) -> [Name] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Type
VarT

makePrism :: Type -> Type -> PrismInfo -> Q [Dec]
makePrism :: Type -> Type -> PrismInfo -> Q [Dec]
makePrism Type
ss Type
mm (PrismInfo Name
regularPrism Name
exhaustivePrism [Name]
mm' Type
aa Name
tt Name
tt') = do
  let s :: Q Type
s = Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ss
  let m :: Q Type
m = Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
mm
  let m' :: Q Type
m' = Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> Type
tagsToType [Name]
mm')
  let a :: Q Type
a = Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
aa
  let t :: Q Type
t = Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
VarT Name
tt)
  let t' :: Q Type
t' = Type -> Q Type
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
VarT Name
tt')

  Type
prismType <- [t|ExhaustivePrism $Q Type
s $Q Type
m $Q Type
m' $Q Type
a $Q Type
t $Q Type
t'|]
  Body
prismBody <- Name -> Q Body
makePrismBody Name
regularPrism
  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return
    [ Name -> Type -> Dec
SigD Name
exhaustivePrism Type
prismType
    , Name -> [Clause] -> Dec
FunD Name
exhaustivePrism [[Pat] -> Body -> [Dec] -> Clause
Clause [] Body
prismBody []]
    ]

makePrismBody :: Name -> Q Body
makePrismBody :: Name -> Q Body
makePrismBody Name
regularPrismName = do
  let regularPrism :: Q Exp
regularPrism = Exp -> Q Exp
forall a. a -> Q a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Exp
VarE Name
regularPrismName)
  Exp -> Body
NormalB (Exp -> Body) -> Q Exp -> Q Body
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [e|from _Tagged . $Q Exp
regularPrism . _Tagged|]