{-# 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 f (Shift e) = Shift (f e)

instance IsEmbed e => IsEmbed (Shift e) where
  type Embedded (Shift e) = Embedded e
  embedded = iso (\(Shift e) -> e) Shift . embedded
  
instance NFData e => NFData (Shift e) where
  rnf (Shift e) = rnf e `seq` ()

instance Show e => Show (Shift e) where
  showsPrec _ (Shift e) = showString "{" . showsPrec 0 e . showString "}"

instance Alpha e => Alpha (Shift e) where
  isPat (Shift e) = if (isEmbed e) then mempty else inconsistentDisjointSet

  isTerm _ = All False

  isEmbed (Shift e) = isEmbed e

  swaps' ctx perm (Shift e) = Shift (swaps' (decrLevelCtx ctx) perm e)

  freshen' ctx p =
    if isTermCtx ctx
    then error "LocallyNameless.freshen' called on a term"
    else return (p, mempty)

  lfreshen' ctx p kont =
    if isTermCtx ctx
    then error "LocallyNameless.lfreshen' called on a term"
    else kont p mempty

  aeq' ctx (Shift e1) (Shift e2) = aeq' ctx e1 e2

  fvAny' ctx afa (Shift e) = Shift <$> fvAny' ctx afa e

  close ctx b se@(Shift e) =
    if isTermCtx ctx
    then error "LocallyNameless.close on Shift"
    else if isZeroLevelCtx 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.
           se
         else Shift (close (decrLevelCtx ctx) b e)

  open ctx b se@(Shift e) =
    if isTermCtx ctx
    then error "LocallyNameless.open on Shift"
    else if isZeroLevelCtx ctx
         then se
         else Shift (open (decrLevelCtx ctx) b e)

  nthPatFind (Shift e) = nthPatFind e
  namePatFind (Shift e) = namePatFind e


  acompare' ctx (Shift x) (Shift y) = acompare' ctx x y