{-# OPTIONS_HADDOCK show-extensions #-}
-- |
-- Module     : Unbound.Generics.LocallyNameless.Shift
-- Copyright  : (c) 2015, Aleksey Kliger
-- License    : BSD3 (See LICENSE)
-- Maintainer : Aleksey Kliger
-- Stability  : experimental
--
-- The pattern @'Shift' e@ shifts the scope of the embedded term in @e@ one level outwards.
--
{-# LANGUAGE TypeFamilies #-}
module Unbound.Generics.LocallyNameless.Shift where

import Control.Applicative
import Control.DeepSeq (NFData(..))
import Data.Monoid (Monoid(..), All(..))

import Unbound.Generics.LocallyNameless.Alpha (Alpha(..),
                                               decrLevelCtx, isTermCtx,
                                               isZeroLevelCtx,
                                               inconsistentDisjointSet)
import Unbound.Generics.LocallyNameless.Embed (IsEmbed(..))

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

-- | The type @Shift e@ is an embedding pattern that shifts the scope of the
-- free variables of the embedded term @'Embedded' e@ up by one level.
newtype Shift e = Shift e

instance Functor Shift where
  fmap :: forall a b. (a -> b) -> Shift a -> Shift b
fmap a -> b
f (Shift a
e) = b -> Shift b
forall e. e -> Shift e
Shift (a -> b
f a
e)

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

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

instance Alpha e => Alpha (Shift e) where
  isPat :: Shift e -> DisjointSet AnyName
isPat (Shift e
e) = if (e -> Bool
forall a. Alpha a => a -> Bool
isEmbed e
e) then DisjointSet AnyName
forall a. Monoid a => a
mempty else DisjointSet AnyName
forall a. DisjointSet a
inconsistentDisjointSet

  isTerm :: Shift e -> All
isTerm Shift e
_ = Bool -> All
All Bool
False

  isEmbed :: Shift e -> Bool
isEmbed (Shift e
e) = e -> Bool
forall a. Alpha a => a -> Bool
isEmbed e
e

  swaps' :: AlphaCtx -> Perm AnyName -> Shift e -> Shift e
swaps' AlphaCtx
ctx Perm AnyName
perm (Shift e
e) = e -> Shift e
forall e. e -> Shift e
Shift (AlphaCtx -> Perm AnyName -> e -> e
forall a. Alpha a => AlphaCtx -> Perm AnyName -> a -> a
swaps' (AlphaCtx -> AlphaCtx
decrLevelCtx AlphaCtx
ctx) Perm AnyName
perm e
e)

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

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

  aeq' :: AlphaCtx -> Shift e -> Shift e -> Bool
aeq' AlphaCtx
ctx (Shift e
e1) (Shift e
e2) = AlphaCtx -> e -> e -> Bool
forall a. Alpha a => AlphaCtx -> a -> a -> Bool
aeq' AlphaCtx
ctx e
e1 e
e2

  fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Shift e -> f (Shift e)
fvAny' AlphaCtx
ctx AnyName -> f AnyName
afa (Shift e
e) = e -> Shift e
forall e. e -> Shift e
Shift (e -> Shift e) -> f e -> f (Shift e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AlphaCtx -> (AnyName -> f AnyName) -> e -> f e
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) -> e -> f e
fvAny' AlphaCtx
ctx AnyName -> f AnyName
afa e
e

  close :: AlphaCtx -> NamePatFind -> Shift e -> Shift e
close AlphaCtx
ctx NamePatFind
b se :: Shift e
se@(Shift e
e) =
    if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx
    then String -> Shift e
forall a. HasCallStack => String -> a
error String
"LocallyNameless.close on Shift"
    else if AlphaCtx -> Bool
isZeroLevelCtx AlphaCtx
ctx
         then
           -- consider type A = Rec (Name t, Shift (Embed e), (Embed e))
           --  (ie the 2nd element of the tuple is not allowed to refer to itself,
           --   but the third is)
           -- if we have (x, e1, e2) and we apply 'rec' to it,
           -- we must close the tuple with respect to itself.
           -- in that case, the ctxLevel is 0 and so none of the names in
           -- e1 need be bound.
           -- on the other hand once we go to
           --   Bind P (Bind A B) for some P and B,
           -- the free vars of e1 in A are bound by P.
           Shift e
se
         else e -> Shift e
forall e. e -> Shift e
Shift (AlphaCtx -> NamePatFind -> e -> e
forall a. Alpha a => AlphaCtx -> NamePatFind -> a -> a
close (AlphaCtx -> AlphaCtx
decrLevelCtx AlphaCtx
ctx) NamePatFind
b e
e)

  open :: AlphaCtx -> NthPatFind -> Shift e -> Shift e
open AlphaCtx
ctx NthPatFind
b se :: Shift e
se@(Shift e
e) =
    if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx
    then String -> Shift e
forall a. HasCallStack => String -> a
error String
"LocallyNameless.open on Shift"
    else if AlphaCtx -> Bool
isZeroLevelCtx AlphaCtx
ctx
         then Shift e
se
         else e -> Shift e
forall e. e -> Shift e
Shift (AlphaCtx -> NthPatFind -> e -> e
forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open (AlphaCtx -> AlphaCtx
decrLevelCtx AlphaCtx
ctx) NthPatFind
b e
e)

  nthPatFind :: Shift e -> NthPatFind
nthPatFind (Shift e
e) = e -> NthPatFind
forall a. Alpha a => a -> NthPatFind
nthPatFind e
e
  namePatFind :: Shift e -> NamePatFind
namePatFind (Shift e
e) = e -> NamePatFind
forall a. Alpha a => a -> NamePatFind
namePatFind e
e


  acompare' :: AlphaCtx -> Shift e -> Shift e -> Ordering
acompare' AlphaCtx
ctx (Shift e
x) (Shift e
y) = AlphaCtx -> e -> e -> Ordering
forall a. Alpha a => AlphaCtx -> a -> a -> Ordering
acompare' AlphaCtx
ctx e
x e
y