{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | Logical representations for some @base@ types along with their (orphan)
-- 'Logical' instances.
module Kanren.LogicalBase (
  -- * Primitive types

  -- | There are 'Logical' instances for 'Bool', 'Char', 'Int', and 'Void'. They
  -- don't require a separate logic representation.

  -- ** Prisms for 'Bool'
  _False,
  _True,
  _False',
  _True',

  -- * Tuples

  -- | For tuples, the logical representation is a tuple too, so they don't need a
  -- separate logic type. Currently, there's a 'Logical' instance for 2-tuples
  -- only.

  -- * Lists
  LogicList (..),

  -- ** Prisms for lists
  _LogicNil,
  _LogicCons,
  _LogicNil',
  _LogicCons',

  -- * 'Maybe'
  LogicMaybe (..),

  -- ** Prisms for 'Maybe'
  _LogicNothing,
  _LogicJust,
  _LogicNothing',
  _LogicJust',

  -- * 'Either'
  LogicEither (..),

  -- ** Prisms for 'Either'
  _LogicLeft,
  _LogicRight,
  _LogicLeft',
  _LogicRight',
) where

import Control.Lens.TH (makePrisms)
import Data.Void (Void)
import GHC.Exts (IsList (..))
import GHC.Generics (Generic)

import Control.DeepSeq (NFData)
import Kanren.Core
import Kanren.GenericLogical
import Kanren.TH (makeExhaustivePrisms, makeLogical)

instance Logical Int
instance Logical Char
instance Logical Void

instance Logical Bool
makePrisms ''Bool
makeExhaustivePrisms ''Bool

instance (Logical a, Logical b) => Logical (a, b) where
  type Logic (a, b) = (Term a, Term b)
  unify :: Logic (a, b) -> Logic (a, b) -> State -> Maybe State
unify = Logic (a, b) -> Logic (a, b) -> State -> Maybe State
forall a.
(Generic (Logic a), GLogical (Rep a) (Rep (Logic a))) =>
Logic a -> Logic a -> State -> Maybe State
genericUnify
  walk :: State -> Logic (a, b) -> Logic (a, b)
walk = State -> Logic (a, b) -> Logic (a, b)
forall a.
(Generic (Logic a), GLogical (Rep a) (Rep (Logic a))) =>
State -> Logic a -> Logic a
genericWalk
  occursCheck :: forall b. VarId b -> Logic (a, b) -> State -> Bool
occursCheck = VarId b -> Logic (a, b) -> State -> Bool
forall a b.
(Generic (Logic a), GLogical (Rep a) (Rep (Logic a))) =>
VarId b -> Logic a -> State -> Bool
genericOccursCheck
  inject :: (a, b) -> Logic (a, b)
inject = (a, b) -> Logic (a, b)
forall a.
(Generic a, Generic (Logic a), GLogical (Rep a) (Rep (Logic a))) =>
a -> Logic a
genericInject
  extract :: Logic (a, b) -> Maybe (a, b)
extract = Logic (a, b) -> Maybe (a, b)
forall a.
(Generic a, Generic (Logic a), GLogical (Rep a) (Rep (Logic a))) =>
Logic a -> Maybe a
genericExtract

data LogicList a
  = LogicNil
  | LogicCons (Term a) (Term [a])
  deriving ((forall x. LogicList a -> Rep (LogicList a) x)
-> (forall x. Rep (LogicList a) x -> LogicList a)
-> Generic (LogicList a)
forall x. Rep (LogicList a) x -> LogicList a
forall x. LogicList a -> Rep (LogicList a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (LogicList a) x -> LogicList a
forall a x. LogicList a -> Rep (LogicList a) x
$cfrom :: forall a x. LogicList a -> Rep (LogicList a) x
from :: forall x. LogicList a -> Rep (LogicList a) x
$cto :: forall a x. Rep (LogicList a) x -> LogicList a
to :: forall x. Rep (LogicList a) x -> LogicList a
Generic)
deriving instance (Eq (Logic a)) => Eq (LogicList a)
deriving instance (NFData (Logic a)) => NFData (LogicList a)

-- | This instance tries to print the list as a regular one. In case the tail is
-- unknown, the list is printed as @[...|_.n]@, like in Prolog.
instance (Show (Logic a)) => Show (LogicList a) where
  showsPrec :: Int -> LogicList a -> ShowS
showsPrec Int
_ LogicList a
LogicNil String
s = String
"[]" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
  showsPrec Int
_ (LogicCons Term a
x Term [a]
xs) String
s = Char
'[' Char -> ShowS
forall a. a -> [a] -> [a]
: Term a -> ShowS
forall a. Show a => a -> ShowS
shows Term a
x (Term [a] -> String
show' Term [a]
xs)
   where
    show' :: Term [a] -> String
show' (Var VarId [a]
var) = Char
'|' Char -> ShowS
forall a. a -> [a] -> [a]
: VarId [a] -> ShowS
forall a. Show a => a -> ShowS
shows VarId [a]
var (Char
']' Char -> ShowS
forall a. a -> [a] -> [a]
: String
s)
    show' (Value Logic [a]
LogicList a
LogicNil) = Char
']' Char -> ShowS
forall a. a -> [a] -> [a]
: String
s
    show' (Value (LogicCons Term a
y Term [a]
ys)) = Char
',' Char -> ShowS
forall a. a -> [a] -> [a]
: Term a -> ShowS
forall a. Show a => a -> ShowS
shows Term a
y (Term [a] -> String
show' Term [a]
ys)

instance (Logical a) => Logical [a] where
  type Logic [a] = LogicList a
  unify :: Logic [a] -> Logic [a] -> State -> Maybe State
unify = Logic [a] -> Logic [a] -> State -> Maybe State
forall a.
(Generic (Logic a), GLogical (Rep a) (Rep (Logic a))) =>
Logic a -> Logic a -> State -> Maybe State
genericUnify
  walk :: State -> Logic [a] -> Logic [a]
walk = State -> Logic [a] -> Logic [a]
forall a.
(Generic (Logic a), GLogical (Rep a) (Rep (Logic a))) =>
State -> Logic a -> Logic a
genericWalk
  occursCheck :: forall b. VarId b -> Logic [a] -> State -> Bool
occursCheck = VarId b -> Logic [a] -> State -> Bool
forall a b.
(Generic (Logic a), GLogical (Rep a) (Rep (Logic a))) =>
VarId b -> Logic a -> State -> Bool
genericOccursCheck
  inject :: [a] -> Logic [a]
inject = [a] -> Logic [a]
forall a.
(Generic a, Generic (Logic a), GLogical (Rep a) (Rep (Logic a))) =>
a -> Logic a
genericInject
  extract :: Logic [a] -> Maybe [a]
extract = Logic [a] -> Maybe [a]
forall a.
(Generic a, Generic (Logic a), GLogical (Rep a) (Rep (Logic a))) =>
Logic a -> Maybe a
genericExtract

instance IsList (LogicList a) where
  type Item (LogicList a) = Term a
  fromList :: [Item (LogicList a)] -> LogicList a
fromList [] = LogicList a
forall a. LogicList a
LogicNil
  fromList (Item (LogicList a)
x : [Item (LogicList a)]
xs) = Term a -> Term [a] -> LogicList a
forall a. Term a -> Term [a] -> LogicList a
LogicCons Item (LogicList a)
Term a
x (Logic [a] -> Term [a]
forall a. Logic a -> Term a
Value ([Item (LogicList a)] -> LogicList a
forall l. IsList l => [Item l] -> l
fromList [Item (LogicList a)]
xs))
  toList :: LogicList a -> [Item (LogicList a)]
toList LogicList a
LogicNil = []
  toList (LogicCons Term a
x Term [a]
xs) = Term a
x Term a -> [Term a] -> [Term a]
forall a. a -> [a] -> [a]
: Term [a] -> [Item (Term [a])]
forall l. IsList l => l -> [Item l]
toList Term [a]
xs -- NOTE: toList for (Term [a]) is partial

makePrisms ''LogicList
makeExhaustivePrisms ''LogicList

makeLogical ''Maybe
makePrisms ''LogicMaybe
makeExhaustivePrisms ''LogicMaybe
deriving instance (Eq (Logic a)) => Eq (LogicMaybe a)
deriving instance (Show (Logic a)) => Show (LogicMaybe a)

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)