{-# OPTIONS_HADDOCK show-extensions #-}
-- |
-- Module     : Unbound.Generics.LocallyNameless.Rec
-- Copyright  : (c) 2014, Aleksey Kliger
-- License    : BSD3 (See LICENSE)
-- Maintainer : Aleksey Kliger
-- Stability  : experimental
--
-- The pattern @'Rec' p@ binds the names in @p@ like @p@ itself would,
-- but additionally, the names in @p@ are scope over @p@.
--
-- The term @'TRec' p@ is shorthand for @'Bind' (Rec p) ()@
{-# LANGUAGE DeriveGeneric #-}
module Unbound.Generics.LocallyNameless.Rec
       (
         Rec (Rec)
       , rec
       , unrec
       , TRec (..)
       ) where

import Control.DeepSeq (NFData(..))
import GHC.Generics (Generic)

import Data.Monoid(All(..))

import Unbound.Generics.LocallyNameless.Alpha
import Unbound.Generics.LocallyNameless.Bind

-- | If @p@ is a pattern type, then @Rec p@ is also a pattern type,
-- which is /recursive/ in the sense that @p@ may bind names in terms
-- embedded within itself.  Useful for encoding e.g. lectrec and
-- Agda's dot notation.
newtype Rec p = Rec p
              deriving ((forall x. Rec p -> Rep (Rec p) x)
-> (forall x. Rep (Rec p) x -> Rec p) -> Generic (Rec p)
forall x. Rep (Rec p) x -> Rec p
forall x. Rec p -> Rep (Rec p) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall p x. Rep (Rec p) x -> Rec p
forall p x. Rec p -> Rep (Rec p) x
$cfrom :: forall p x. Rec p -> Rep (Rec p) x
from :: forall x. Rec p -> Rep (Rec p) x
$cto :: forall p x. Rep (Rec p) x -> Rec p
to :: forall x. Rep (Rec p) x -> Rec p
Generic, Rec p -> Rec p -> Bool
(Rec p -> Rec p -> Bool) -> (Rec p -> Rec p -> Bool) -> Eq (Rec p)
forall p. Eq p => Rec p -> Rec p -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall p. Eq p => Rec p -> Rec p -> Bool
== :: Rec p -> Rec p -> Bool
$c/= :: forall p. Eq p => Rec p -> Rec p -> Bool
/= :: Rec p -> Rec p -> Bool
Eq)

instance NFData p => NFData (Rec p) where
  rnf :: Rec p -> ()
rnf (Rec p
p) = p -> ()
forall a. NFData a => a -> ()
rnf p
p () -> () -> ()
forall a b. a -> b -> b
`seq` ()

instance Show a => Show (Rec a) where
  showsPrec :: Int -> Rec a -> ShowS
showsPrec Int
_ (Rec 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
"]"

-- | @TRec@ is a standalone variant of 'Rec': the only difference is
--   that whereas @'Rec' p@ is a pattern type, @TRec p@
--   is a /term type/.  It is isomorphic to @'Bind' ('Rec' p) ()@.
--
--   Note that @TRec@ corresponds to Pottier's /abstraction/ construct
--   from alpha-Caml.  In this context, @'Embed' t@ corresponds to
--   alpha-Caml's @inner t@, and @'Shift' ('Embed' t)@ corresponds to
--   alpha-Caml's @outer t@.
newtype TRec p = TRec (Bind (Rec p) ())
                 deriving ((forall x. TRec p -> Rep (TRec p) x)
-> (forall x. Rep (TRec p) x -> TRec p) -> Generic (TRec p)
forall x. Rep (TRec p) x -> TRec p
forall x. TRec p -> Rep (TRec p) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall p x. Rep (TRec p) x -> TRec p
forall p x. TRec p -> Rep (TRec p) x
$cfrom :: forall p x. TRec p -> Rep (TRec p) x
from :: forall x. TRec p -> Rep (TRec p) x
$cto :: forall p x. Rep (TRec p) x -> TRec p
to :: forall x. Rep (TRec p) x -> TRec p
Generic)

instance Show a => Show (TRec a) where
  showsPrec :: Int -> TRec a -> ShowS
showsPrec Int
_ (TRec (B (Rec a
p) ())) = 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
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"]"


instance Alpha p => Alpha (Rec p) where
  isTerm :: Rec p -> All
isTerm Rec p
_ = Bool -> All
All Bool
False
  isPat :: Rec p -> DisjointSet AnyName
isPat (Rec p
p) = p -> DisjointSet AnyName
forall a. Alpha a => a -> DisjointSet AnyName
isPat p
p

  nthPatFind :: Rec p -> NthPatFind
nthPatFind (Rec p
p) = p -> NthPatFind
forall a. Alpha a => a -> NthPatFind
nthPatFind p
p
  namePatFind :: Rec p -> NamePatFind
namePatFind (Rec p
p) = p -> NamePatFind
forall a. Alpha a => a -> NamePatFind
namePatFind p
p

  open :: AlphaCtx -> NthPatFind -> Rec p -> Rec p
open AlphaCtx
ctx NthPatFind
b (Rec p
p) = p -> Rec p
forall p. p -> Rec p
Rec (AlphaCtx -> NthPatFind -> p -> p
forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) NthPatFind
b p
p)
  close :: AlphaCtx -> NamePatFind -> Rec p -> Rec p
close AlphaCtx
ctx NamePatFind
b (Rec p
p) = p -> Rec p
forall p. p -> Rec p
Rec (AlphaCtx -> NamePatFind -> p -> p
forall a. Alpha a => AlphaCtx -> NamePatFind -> a -> a
close (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) NamePatFind
b p
p)

instance Alpha p => Alpha (TRec p)

-- | Constructor for recursive patterns.
rec :: Alpha p => p -> Rec p
rec :: forall p. Alpha p => p -> Rec p
rec p
p = p -> Rec p
forall p. p -> Rec p
Rec (AlphaCtx -> NamePatFind -> p -> p
forall a. Alpha a => AlphaCtx -> NamePatFind -> a -> a
close (AlphaCtx -> AlphaCtx
patternCtx AlphaCtx
initialCtx) (p -> NamePatFind
forall a. Alpha a => a -> NamePatFind
namePatFind p
p) p
p)

-- | Destructor for recursive patterns.
unrec :: Alpha p => Rec p -> p
unrec :: forall p. Alpha p => Rec p -> p
unrec r :: Rec p
r@(Rec p
p) = AlphaCtx -> NthPatFind -> p -> p
forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open (AlphaCtx -> AlphaCtx
patternCtx AlphaCtx
initialCtx) (Rec p -> NthPatFind
forall a. Alpha a => a -> NthPatFind
nthPatFind Rec p
r) p
p