{-# OPTIONS_HADDOCK show-extensions #-}
-- |
-- Module     : Unbound.Generics.LocallyNameless.Embed
-- Copyright  : (c) 2014, Aleksey Kliger
-- License    : BSD3 (See LICENSE)
-- Maintainer : Aleksey Kliger
-- Stability  : experimental
--
-- The pattern @'Embed' t@ contains a term @t@.
{-# LANGUAGE DeriveGeneric, TypeFamilies #-}
module Unbound.Generics.LocallyNameless.Embed where

import Control.Applicative (pure, (<$>))
import Control.DeepSeq (NFData(..))
import Data.Monoid (mempty, All(..))
import Data.Profunctor (Profunctor(..))

import GHC.Generics (Generic)

import Unbound.Generics.LocallyNameless.Alpha
import Unbound.Generics.LocallyNameless.Internal.Iso (iso)

-- | @Embed@ allows for terms to be /embedded/ within patterns.  Such
--   embedded terms do not bind names along with the rest of the
--   pattern.  For examples, see the tutorial or examples directories.
--
--   If @t@ is a /term type/, then @Embed t@ is a /pattern type/.
--
--   @Embed@ is not abstract since it involves no binding, and hence
--   it is safe to manipulate directly.  To create and destruct
--   @Embed@ terms, you may use the @Embed@ constructor directly.
--   (You may also use the functions 'embed' and 'unembed', which
--   additionally can construct or destruct any number of enclosing
--   'Shift's at the same time.)
newtype Embed t = Embed t deriving (Embed t -> Embed t -> Bool
(Embed t -> Embed t -> Bool)
-> (Embed t -> Embed t -> Bool) -> Eq (Embed t)
forall t. Eq t => Embed t -> Embed t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall t. Eq t => Embed t -> Embed t -> Bool
== :: Embed t -> Embed t -> Bool
$c/= :: forall t. Eq t => Embed t -> Embed t -> Bool
/= :: Embed t -> Embed t -> Bool
Eq, Eq (Embed t)
Eq (Embed t)
-> (Embed t -> Embed t -> Ordering)
-> (Embed t -> Embed t -> Bool)
-> (Embed t -> Embed t -> Bool)
-> (Embed t -> Embed t -> Bool)
-> (Embed t -> Embed t -> Bool)
-> (Embed t -> Embed t -> Embed t)
-> (Embed t -> Embed t -> Embed t)
-> Ord (Embed t)
Embed t -> Embed t -> Bool
Embed t -> Embed t -> Ordering
Embed t -> Embed t -> Embed t
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {t}. Ord t => Eq (Embed t)
forall t. Ord t => Embed t -> Embed t -> Bool
forall t. Ord t => Embed t -> Embed t -> Ordering
forall t. Ord t => Embed t -> Embed t -> Embed t
$ccompare :: forall t. Ord t => Embed t -> Embed t -> Ordering
compare :: Embed t -> Embed t -> Ordering
$c< :: forall t. Ord t => Embed t -> Embed t -> Bool
< :: Embed t -> Embed t -> Bool
$c<= :: forall t. Ord t => Embed t -> Embed t -> Bool
<= :: Embed t -> Embed t -> Bool
$c> :: forall t. Ord t => Embed t -> Embed t -> Bool
> :: Embed t -> Embed t -> Bool
$c>= :: forall t. Ord t => Embed t -> Embed t -> Bool
>= :: Embed t -> Embed t -> Bool
$cmax :: forall t. Ord t => Embed t -> Embed t -> Embed t
max :: Embed t -> Embed t -> Embed t
$cmin :: forall t. Ord t => Embed t -> Embed t -> Embed t
min :: Embed t -> Embed t -> Embed t
Ord, (forall x. Embed t -> Rep (Embed t) x)
-> (forall x. Rep (Embed t) x -> Embed t) -> Generic (Embed t)
forall x. Rep (Embed t) x -> Embed t
forall x. Embed t -> Rep (Embed t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (Embed t) x -> Embed t
forall t x. Embed t -> Rep (Embed t) x
$cfrom :: forall t x. Embed t -> Rep (Embed t) x
from :: forall x. Embed t -> Rep (Embed t) x
$cto :: forall t x. Rep (Embed t) x -> Embed t
to :: forall x. Rep (Embed t) x -> Embed t
Generic)

class IsEmbed e where
  -- | The term type embedded in the embedding 'e'
  type Embedded e :: *
  -- | Insert or extract the embedded term.
  -- If you're not using the lens library, see 'Unbound.Generics.LocallyNameless.Operations.embed'
  -- and 'Unbound.Generics.LocallyNameless.Operations.unembed'
  -- otherwise 'embedded' is an isomorphism that you can use with lens.
  -- @
  -- embedded :: Iso' (Embedded e) e
  -- @
  embedded :: (Profunctor p, Functor f) => p (Embedded e) (f (Embedded e)) -> p e (f e)

instance IsEmbed (Embed t) where
  type Embedded (Embed t) = t
  embedded :: forall (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (Embedded (Embed t)) (f (Embedded (Embed t)))
-> p (Embed t) (f (Embed t))
embedded = (Embed t -> t) -> (t -> Embed t) -> Iso (Embed t) (Embed t) t t
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso (\(Embed t
t) -> t
t) t -> Embed t
forall t. t -> Embed t
Embed
  
instance NFData t => NFData (Embed t) where
  rnf :: Embed t -> ()
rnf (Embed t
t) = t -> ()
forall a. NFData a => a -> ()
rnf t
t () -> () -> ()
forall a b. a -> b -> b
`seq` ()

instance Show a => Show (Embed a) where
  showsPrec :: Int -> Embed a -> ShowS
showsPrec Int
_ (Embed a
a) = String -> ShowS
showString String
"{" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 a
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"}"

instance Alpha t => Alpha (Embed t) where
  isPat :: Embed t -> DisjointSet AnyName
isPat (Embed t
t) = if All -> Bool
getAll (t -> All
forall a. Alpha a => a -> All
isTerm t
t) then DisjointSet AnyName
forall a. Monoid a => a
mempty else DisjointSet AnyName
forall a. DisjointSet a
inconsistentDisjointSet

  isTerm :: Embed t -> All
isTerm Embed t
_ = Bool -> All
All Bool
False

  isEmbed :: Embed t -> Bool
isEmbed (Embed t
t) = All -> Bool
getAll (t -> All
forall a. Alpha a => a -> All
isTerm t
t)

  swaps' :: AlphaCtx -> Perm AnyName -> Embed t -> Embed t
swaps' AlphaCtx
ctx Perm AnyName
perm (Embed t
t) =
    if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx
    then t -> Embed t
forall t. t -> Embed t
Embed t
t
    else t -> Embed t
forall t. t -> Embed t
Embed (AlphaCtx -> Perm AnyName -> t -> t
forall a. Alpha a => AlphaCtx -> Perm AnyName -> a -> a
swaps' (AlphaCtx -> AlphaCtx
termCtx AlphaCtx
ctx) Perm AnyName
perm t
t)

  freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Embed t -> m (Embed t, Perm AnyName)
freshen' AlphaCtx
ctx Embed t
p =
    if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx
    then String -> m (Embed t, Perm AnyName)
forall a. HasCallStack => String -> a
error String
"LocallyNameless.freshen' called on a term"
    else (Embed t, Perm AnyName) -> m (Embed t, Perm AnyName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Embed t
p, Perm AnyName
forall a. Monoid a => a
mempty)

  lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Embed t -> (Embed t -> Perm AnyName -> m b) -> m b
lfreshen' AlphaCtx
ctx Embed t
p Embed t -> Perm AnyName -> m b
cont =
    if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx
    then String -> m b
forall a. HasCallStack => String -> a
error String
"LocallyNameless.lfreshen' called on a term"
    else Embed t -> Perm AnyName -> m b
cont Embed t
p Perm AnyName
forall a. Monoid a => a
mempty


  aeq' :: AlphaCtx -> Embed t -> Embed t -> Bool
aeq' AlphaCtx
ctx (Embed t
x) (Embed t
y) = AlphaCtx -> t -> t -> Bool
forall a. Alpha a => AlphaCtx -> a -> a -> Bool
aeq' (AlphaCtx -> AlphaCtx
termCtx AlphaCtx
ctx) t
x t
y

  fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Embed t -> f (Embed t)
fvAny' AlphaCtx
ctx AnyName -> f AnyName
afa ex :: Embed t
ex@(Embed t
x) =
    if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx
    then Embed t -> f (Embed t)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Embed t
ex
    else t -> Embed t
forall t. t -> Embed t
Embed (t -> Embed t) -> f t -> f (Embed t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AlphaCtx -> (AnyName -> f AnyName) -> t -> f t
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> a -> f a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> t -> f t
fvAny' (AlphaCtx -> AlphaCtx
termCtx AlphaCtx
ctx) AnyName -> f AnyName
afa t
x

  close :: AlphaCtx -> NamePatFind -> Embed t -> Embed t
close AlphaCtx
ctx NamePatFind
b (Embed t
x) =
    if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx
    then String -> Embed t
forall a. HasCallStack => String -> a
error String
"LocallyNameless.close on Embed"
    else t -> Embed t
forall t. t -> Embed t
Embed (AlphaCtx -> NamePatFind -> t -> t
forall a. Alpha a => AlphaCtx -> NamePatFind -> a -> a
close (AlphaCtx -> AlphaCtx
termCtx AlphaCtx
ctx) NamePatFind
b t
x)

  open :: AlphaCtx -> NthPatFind -> Embed t -> Embed t
open AlphaCtx
ctx NthPatFind
b (Embed t
x) =
    if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx
    then String -> Embed t
forall a. HasCallStack => String -> a
error String
"LocallyNameless.open on Embed"
    else t -> Embed t
forall t. t -> Embed t
Embed (AlphaCtx -> NthPatFind -> t -> t
forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open (AlphaCtx -> AlphaCtx
termCtx AlphaCtx
ctx) NthPatFind
b t
x)

  nthPatFind :: Embed t -> NthPatFind
nthPatFind Embed t
_ = NthPatFind
forall a. Monoid a => a
mempty
  namePatFind :: Embed t -> NamePatFind
namePatFind Embed t
_ = NamePatFind
forall a. Monoid a => a
mempty

  acompare' :: AlphaCtx -> Embed t -> Embed t -> Ordering
acompare' AlphaCtx
ctx (Embed t
x) (Embed t
y) = AlphaCtx -> t -> t -> Ordering
forall a. Alpha a => AlphaCtx -> a -> a -> Ordering
acompare' (AlphaCtx -> AlphaCtx
termCtx AlphaCtx
ctx) t
x t
y