Improve the TH module

src/Kanren/Data/Binary.hs

@@ -1,4 +1,3 @@
-{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -34,37 +33,21 @@ module Kanren.Data.Binary (
 ) where
 
 import Control.DeepSeq (NFData)
-import Control.Lens (Prism, from)
 import Control.Lens.TH (makePrisms)
 import Data.Bifunctor (bimap)
 import Data.Function ((&))
-import Data.Tagged (Tagged)
 import GHC.Generics (Generic)
 
 import Kanren.Core
 import Kanren.Goal
 import Kanren.LogicalBase
 import Kanren.Match
+import Kanren.TH
 
 data Bit = O | I deriving (Eq, Show, Generic, NFData)
 instance Logical Bit
 makePrisms ''Bit
-
-_O'
-  :: Prism
-      (Tagged (o, i) Bit)
-      (Tagged (o', i) Bit)
-      (Tagged o ())
-      (Tagged o' ())
-_O' = from _Tagged . _O . _Tagged
-
-_I'
-  :: Prism
-      (Tagged (o, i) Bit)
-      (Tagged (o, i') Bit)
-      (Tagged i ())
-      (Tagged i' ())
-_I' = from _Tagged . _I . _Tagged
+makeExhaustivePrisms ''Bit
 
 type Binary = [Bit]
 

src/Kanren/Data/Scheme.hs

@@ -1,4 +1,3 @@
-{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE OverloadedLists #-}
@@ -16,9 +15,7 @@ module Kanren.Data.Scheme (
   evalo,
 ) where
 
-import Control.Lens (Prism, from)
 import Control.Lens.TH (makePrisms)
-import Data.Tagged (Tagged)
 import GHC.Exts (IsList, IsString (..))
 import GHC.Generics (Generic)
 import GHC.IsList (IsList (..))
@@ -27,7 +24,6 @@ import Control.DeepSeq
 import Kanren.Core
 import Kanren.Goal
 import Kanren.LogicalBase
-import Kanren.Match
 import Kanren.TH
 
 type Symbol = Atomic String
@@ -68,10 +64,12 @@ instance IsList SExpr where
 instance IsString SExpr where
   fromString = SSymbol . Atomic
 
-makeLogic ''SExpr
-makeLogic ''Value
+makeLogical ''SExpr
+makeLogical ''Value
 makePrisms ''LogicSExpr
 makePrisms ''LogicValue
+makeExhaustivePrisms ''LogicSExpr
+makeExhaustivePrisms ''LogicValue
 
 instance Normalizable SExpr where
   normalize f (LogicSSymbol x) = LogicSSymbol <$> normalize' f x
@@ -80,30 +78,6 @@ instance Normalizable SExpr where
 
 deriving instance NFData LogicSExpr
 
-_LogicSSymbol'
-  :: Prism
-      (Tagged (s, n, c) LogicSExpr)
-      (Tagged (s', n, c) LogicSExpr)
-      (Tagged s (Term Symbol))
-      (Tagged s' (Term Symbol))
-_LogicSSymbol' = from _Tagged . _LogicSSymbol . _Tagged
-
-_LogicSNil'
-  :: Prism
-      (Tagged (s, n, c) LogicSExpr)
-      (Tagged (s, n', c) LogicSExpr)
-      (Tagged n ())
-      (Tagged n' ())
-_LogicSNil' = from _Tagged . _LogicSNil . _Tagged
-
-_LogicSCons'
-  :: Prism
-      (Tagged (s, n, c) LogicSExpr)
-      (Tagged (s, n, c') LogicSExpr)
-      (Tagged c (Term SExpr, Term SExpr))
-      (Tagged c' (Term SExpr, Term SExpr))
-_LogicSCons' = from _Tagged . _LogicSCons . _Tagged
-
 instance Show LogicSExpr where
   show (LogicSSymbol (Value (Atomic symbol))) = symbol
   show (LogicSSymbol var) = show var

src/Kanren/Example/Matche.hs

@@ -1,4 +1,3 @@
-{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TemplateHaskell #-}
@@ -55,7 +54,7 @@ data Nat
   | S Nat
   deriving (Show, Generic)
 
-makeLogic ''Nat
+makeLogical ''Nat
 makePrisms ''LogicNat
 
 _Z' :: Prism (Tagged (z, s) LogicNat) (Tagged (z', s) LogicNat) (Tagged z ()) (Tagged z' ())

src/Kanren/Example/Tree.hs

@@ -1,4 +1,3 @@
-{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -16,11 +15,11 @@ import Kanren.Core
 import Kanren.Goal
 import Kanren.LogicalBase ()
 import Kanren.Match
-import Kanren.TH (makeLogic)
+import Kanren.TH
 
 data Tree a = Empty | Node a (Tree a) (Tree a)
   deriving (Show, Generic)
-makeLogic ''Tree
+makeLogical ''Tree
 makePrisms ''LogicTree
 
 treeo :: Term (Tree Int) -> Goal ()

src/Kanren/LogicalBase.hs

@@ -1,4 +1,3 @@
-{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -57,41 +56,23 @@ module Kanren.LogicalBase (
   _LogicRight',
 ) where
 
-import Control.Lens (Prism, from)
 import Control.Lens.TH (makePrisms)
-import Data.Tagged (Tagged)
 import Data.Void (Void)
 import GHC.Exts (IsList (..))
 import GHC.Generics (Generic)
 
 import Control.DeepSeq (NFData)
 import Kanren.Core
 import Kanren.GenericLogical
-import Kanren.Match (_Tagged)
-import Kanren.TH (makeLogic)
+import Kanren.TH (makeExhaustivePrisms, makeLogical)
 
 instance Logical Int
 instance Logical Char
 instance Logical Void
 
 instance Logical Bool
 makePrisms ''Bool
-
-_False'
-  :: Prism
-      (Tagged (false, true) Bool)
-      (Tagged (false', true) Bool)
-      (Tagged false ())
-      (Tagged false' ())
-_False' = from _Tagged . _False . _Tagged
-
-_True'
-  :: Prism
-      (Tagged (false, true) Bool)
-      (Tagged (false, true') Bool)
-      (Tagged true ())
-      (Tagged true' ())
-_True' = from _Tagged . _True . _Tagged
+makeExhaustivePrisms ''Bool
 
 instance (Logical a, Logical b) => Logical (a, b) where
   type Logic (a, b) = (Term a, Term b)
@@ -134,61 +115,16 @@ instance IsList (LogicList a) where
   toList (LogicCons x xs) = x : toList xs -- NOTE: toList for (Term [a]) is partial
 
 makePrisms ''LogicList
+makeExhaustivePrisms ''LogicList
 
-_LogicNil'
-  :: Prism
-      (Tagged (nil, cons) (LogicList a))
-      (Tagged (nil', cons) (LogicList a))
-      (Tagged nil ())
-      (Tagged nil' ())
-_LogicNil' = from _Tagged . _LogicNil . _Tagged
-
-_LogicCons'
-  :: Prism
-      (Tagged (nil, cons) (LogicList a))
-      (Tagged (nil, cons') (LogicList a'))
-      (Tagged cons (Term a, Term [a]))
-      (Tagged cons' (Term a', Term [a']))
-_LogicCons' = from _Tagged . _LogicCons . _Tagged
-
-makeLogic ''Maybe
+makeLogical ''Maybe
 makePrisms ''LogicMaybe
+makeExhaustivePrisms ''LogicMaybe
 deriving instance (Eq (Logic a)) => Eq (LogicMaybe a)
 deriving instance (Show (Logic a)) => Show (LogicMaybe a)
 
-_LogicNothing'
-  :: Prism
-      (Tagged (nothing, just) (LogicMaybe a))
-      (Tagged (nothing', just) (LogicMaybe a))
-      (Tagged nothing ())
-      (Tagged nothing' ())
-_LogicNothing' = from _Tagged . _LogicNothing . _Tagged
-
-_LogicJust'
-  :: Prism
-      (Tagged (nothing, just) (LogicMaybe a))
-      (Tagged (nothing, just') (LogicMaybe a'))
-      (Tagged just (Term a))
-      (Tagged just' (Term a'))
-_LogicJust' = from _Tagged . _LogicJust . _Tagged
-
-makeLogic ''Either
+makeLogical ''Either
 makePrisms ''LogicEither
+makeExhaustivePrisms ''LogicEither
 deriving instance (Eq (Logic a), Eq (Logic b)) => Eq (LogicEither a b)
 deriving instance (Show (Logic a), Show (Logic b)) => Show (LogicEither a b)
-
-_LogicLeft'
-  :: Prism
-      (Tagged (left, right) (LogicEither a b))
-      (Tagged (left', right) (LogicEither a' b))
-      (Tagged left (Term a))
-      (Tagged left' (Term a'))
-_LogicLeft' = from _Tagged . _LogicLeft . _Tagged
-
-_LogicRight'
-  :: Prism
-      (Tagged (left, right) (LogicEither a b))
-      (Tagged (left, right') (LogicEither a b'))
-      (Tagged right (Term b))
-      (Tagged right' (Term b'))
-_LogicRight' = from _Tagged . _LogicRight . _Tagged

src/Kanren/Match.hs

@@ -165,22 +165,24 @@ module Kanren.Match (
   -- we'll spend the next few paragraphs explaining it.
   --
   -- The magic that allows us to perform the exhaustiveness check is in the new
-  -- prisms. In general, their type signature is
+  -- prisms. They have the following type:
   --
-  -- > Prism (Tagged (…, c , …) (Logic a))
-  -- >       (Tagged (…, c', …) (Logic a))
-  -- >       (Tagged c  b)
-  -- >       (Tagged c' b)
+  -- > ExhaustivePrism (Logic s) (…, c, …) (…, c', …) a c c'
+  --
+  -- …which is actually just an alias for the more verbose type
+  --
+  -- > Prism (Tagged (…, c , …) (Logic s))
+  -- >       (Tagged (…, c', …) (Logic s))
+  -- >       (Tagged c  a)
+  -- >       (Tagged c' a)
   --
   -- The source type is now 'Tagged' with a tuple that contains a variable for
   -- each variant of the type. The focus is also 'Tagged' with the variable for
   -- the variant that this prism focuses on. Take a look at @_LogicVariable'@:
   --
-  -- > _LogicVariable' :: Prism
-  -- >   (Tagged (v , ab, ap) LogicExpr)
-  -- >   (Tagged (v', ab, ap) LogicExpr)
-  -- >   (Tagged v  (Term String))
-  -- >   (Tagged v' (Term String))
+  -- > _LogicVariable' :: ExhaustivePrism
+  --     LogicExpr (v, ab, ap) (v', ab, ap)
+  --     (Term String) v v'
   -- > _LogicVariable' = from _Tagged . _LogicVariable . _Tagged
   --
   -- These new prisms are easily implemented using regular prisms and the
@@ -243,16 +245,25 @@ module Kanren.Match (
   enter',
   on',
   matche',
+  ExhaustivePrism,
   _Tagged,
   _Value',
 ) where
 
-import           Control.Lens (Iso, Prism, Prism', from, iso, prism', review,
-                               reviewing)
-import           Data.Tagged  (Tagged (Tagged, unTagged))
+import Control.Lens (
+  Iso,
+  Prism,
+  Prism',
+  from,
+  iso,
+  prism',
+  review,
+  reviewing,
+ )
+import Data.Tagged (Tagged (Tagged, unTagged))
 
-import           Kanren.Core
-import           Kanren.Goal
+import Kanren.Core
+import Kanren.Goal
 
 -- | One case for non-exhaustive pattern matching.
 --
@@ -314,6 +325,13 @@ instance
   (Exhausted a, Exhausted b, Exhausted c, Exhausted d)
   => Exhausted (a, b, c, d)
 
+-- | A prism which is suitable for exhaustive pattern matching.
+--
+-- Although the type definition might allow changing the type of the focus, this
+-- is not neccesary for exhaustive pattern matching and so not covered here.
+type ExhaustivePrism s m m' a t t' =
+  Prism (Tagged m s) (Tagged m' s) (Tagged t a) (Tagged t' a)
+
 -- | Begin exhaustive pattern matching by attaching initial tags to the term.
 -- Do keep in mind that these tags do not exist at runtime.
 enter' :: (Matched m a -> Goal x) -> Term a -> Goal x
@@ -328,11 +346,7 @@ enter' f = delay . f . Tagged
 -- @Remaining@ and @Checked@ are private types on purpose.
 on'
   :: (Logical a, Fresh v)
-  => Prism
-      (Tagged m (Logic a))
-      (Tagged m' (Logic a))
-      (Tagged Remaining v)
-      (Tagged Checked v)
+  => ExhaustivePrism (Logic a) m m' v Remaining Checked
   -- ^ The pattern, which also participates in the exhaustiveness check
   -> (v -> Goal x)
   -- ^ The handler
@@ -374,10 +388,5 @@ _Tagged = iso Tagged unTagged
 --
 -- This prism serves the same purpose as '_Value', but is adapted for exhaustive
 -- pattern matching.
-_Value'
-  :: Prism
-      (Tagged m (Term a))
-      (Tagged m' (Term a))
-      (Tagged m (Logic a))
-      (Tagged m' (Logic a))
+_Value' :: ExhaustivePrism (Term a) m m' (Logic a) m m'
 _Value' = from _Tagged . _Value . _Tagged