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.

Generate a logic representation and a corresponding Logical instance for each given type. This works like makeLogical, but better suits mutually recursive types.

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 newtypes, 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)

Generate a logic representation for several types. This works like makeLogicType, but better suits mutually recursive types.

Settings for generating a type's logic representation.

Default LogicTypeRules. Does not derive any instances for the logical representation.

makeLogicType, but allows configuring how the logical representation is generated.

makeLogicTypes, but allows configuring how the logical representations are generated.

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

Generate Logical instances, given pairs of a type and its logical representation. This works like makeLogicalInstance, but better suits mutually recursive types.

Generate ExhaustivePrisms 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 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