-- |
-- Module     : Unbound.Generics.LocallyNameless.Subst
-- Copyright  : (c) 2014, Aleksey Kliger
-- License    : BSD3 (See LICENSE)
-- Maintainer : Aleksey Kliger
-- Stability  : experimental
--
-- A typeclass for generic structural substitution.

{-# LANGUAGE
               FlexibleInstances
             , MultiParamTypeClasses
             , TypeOperators
 #-}

module Unbound.Generics.LocallyNameless.Internal.GSubst (
  GSubst(..)
  ) where

import GHC.Generics

import Unbound.Generics.LocallyNameless.Name
import Unbound.Generics.LocallyNameless.Alpha

---- generic structural substitution.

class GSubst b f where
  gsubst :: Name b -> b -> f c -> f c
  gsubsts :: [(Name b, b)] -> f c -> f c
  gsubstBvs :: AlphaCtx -> [b] -> f c -> f c

instance GSubst b f => GSubst b (M1 i c f) where
  gsubst :: forall c. Name b -> b -> M1 i c f c -> M1 i c f c
gsubst Name b
nm b
val = f c -> M1 i c f c
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f c -> M1 i c f c)
-> (M1 i c f c -> f c) -> M1 i c f c -> M1 i c f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name b -> b -> f c -> f c
forall c. Name b -> b -> f c -> f c
forall b (f :: * -> *) c. GSubst b f => Name b -> b -> f c -> f c
gsubst Name b
nm b
val (f c -> f c) -> (M1 i c f c -> f c) -> M1 i c f c -> f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f c -> f c
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  gsubsts :: forall c. [(Name b, b)] -> M1 i c f c -> M1 i c f c
gsubsts [(Name b, b)]
ss = f c -> M1 i c f c
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f c -> M1 i c f c)
-> (M1 i c f c -> f c) -> M1 i c f c -> M1 i c f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name b, b)] -> f c -> f c
forall c. [(Name b, b)] -> f c -> f c
forall b (f :: * -> *) c. GSubst b f => [(Name b, b)] -> f c -> f c
gsubsts [(Name b, b)]
ss (f c -> f c) -> (M1 i c f c -> f c) -> M1 i c f c -> f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f c -> f c
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  gsubstBvs :: forall c. AlphaCtx -> [b] -> M1 i c f c -> M1 i c f c
gsubstBvs AlphaCtx
c [b]
b = f c -> M1 i c f c
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f c -> M1 i c f c)
-> (M1 i c f c -> f c) -> M1 i c f c -> M1 i c f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlphaCtx -> [b] -> f c -> f c
forall c. AlphaCtx -> [b] -> f c -> f c
forall b (f :: * -> *) c.
GSubst b f =>
AlphaCtx -> [b] -> f c -> f c
gsubstBvs AlphaCtx
c [b]
b (f c -> f c) -> (M1 i c f c -> f c) -> M1 i c f c -> f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f c -> f c
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1

instance GSubst b U1 where
  gsubst :: forall c. Name b -> b -> U1 c -> U1 c
gsubst Name b
_nm b
_val U1 c
_ = U1 c
forall k (p :: k). U1 p
U1
  gsubsts :: forall c. [(Name b, b)] -> U1 c -> U1 c
gsubsts [(Name b, b)]
_ss U1 c
_ = U1 c
forall k (p :: k). U1 p
U1
  gsubstBvs :: forall c. AlphaCtx -> [b] -> U1 c -> U1 c
gsubstBvs AlphaCtx
_c [b]
_b U1 c
_ = U1 c
forall k (p :: k). U1 p
U1

instance GSubst b V1 where
  gsubst :: forall c. Name b -> b -> V1 c -> V1 c
gsubst Name b
_nm b
_val = V1 c -> V1 c
forall a. a -> a
id
  gsubsts :: forall c. [(Name b, b)] -> V1 c -> V1 c
gsubsts [(Name b, b)]
_ss = V1 c -> V1 c
forall a. a -> a
id
  gsubstBvs :: forall c. AlphaCtx -> [b] -> V1 c -> V1 c
gsubstBvs AlphaCtx
_c [b]
_b = V1 c -> V1 c
forall a. a -> a
id

instance (GSubst b f, GSubst b g) => GSubst b (f :*: g) where
  gsubst :: forall c. Name b -> b -> (:*:) f g c -> (:*:) f g c
gsubst Name b
nm b
val (f c
f :*: g c
g) = Name b -> b -> f c -> f c
forall c. Name b -> b -> f c -> f c
forall b (f :: * -> *) c. GSubst b f => Name b -> b -> f c -> f c
gsubst Name b
nm b
val f c
f f c -> g c -> (:*:) f g c
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Name b -> b -> g c -> g c
forall c. Name b -> b -> g c -> g c
forall b (f :: * -> *) c. GSubst b f => Name b -> b -> f c -> f c
gsubst Name b
nm b
val g c
g
  gsubsts :: forall c. [(Name b, b)] -> (:*:) f g c -> (:*:) f g c
gsubsts [(Name b, b)]
ss (f c
f :*: g c
g) = [(Name b, b)] -> f c -> f c
forall c. [(Name b, b)] -> f c -> f c
forall b (f :: * -> *) c. GSubst b f => [(Name b, b)] -> f c -> f c
gsubsts [(Name b, b)]
ss f c
f f c -> g c -> (:*:) f g c
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: [(Name b, b)] -> g c -> g c
forall c. [(Name b, b)] -> g c -> g c
forall b (f :: * -> *) c. GSubst b f => [(Name b, b)] -> f c -> f c
gsubsts [(Name b, b)]
ss g c
g
  gsubstBvs :: forall c. AlphaCtx -> [b] -> (:*:) f g c -> (:*:) f g c
gsubstBvs AlphaCtx
c [b]
b (f c
f :*: g c
g) = AlphaCtx -> [b] -> f c -> f c
forall c. AlphaCtx -> [b] -> f c -> f c
forall b (f :: * -> *) c.
GSubst b f =>
AlphaCtx -> [b] -> f c -> f c
gsubstBvs AlphaCtx
c [b]
b f c
f f c -> g c -> (:*:) f g c
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: AlphaCtx -> [b] -> g c -> g c
forall c. AlphaCtx -> [b] -> g c -> g c
forall b (f :: * -> *) c.
GSubst b f =>
AlphaCtx -> [b] -> f c -> f c
gsubstBvs AlphaCtx
c [b]
b g c
g

instance (GSubst b f, GSubst b g) => GSubst b (f :+: g) where
  gsubst :: forall c. Name b -> b -> (:+:) f g c -> (:+:) f g c
gsubst Name b
nm b
val (L1 f c
f) = f c -> (:+:) f g c
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (f c -> (:+:) f g c) -> f c -> (:+:) f g c
forall a b. (a -> b) -> a -> b
$ Name b -> b -> f c -> f c
forall c. Name b -> b -> f c -> f c
forall b (f :: * -> *) c. GSubst b f => Name b -> b -> f c -> f c
gsubst Name b
nm b
val f c
f
  gsubst Name b
nm b
val (R1 g c
g) = g c -> (:+:) f g c
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (g c -> (:+:) f g c) -> g c -> (:+:) f g c
forall a b. (a -> b) -> a -> b
$ Name b -> b -> g c -> g c
forall c. Name b -> b -> g c -> g c
forall b (f :: * -> *) c. GSubst b f => Name b -> b -> f c -> f c
gsubst Name b
nm b
val g c
g

  gsubsts :: forall c. [(Name b, b)] -> (:+:) f g c -> (:+:) f g c
gsubsts [(Name b, b)]
ss (L1 f c
f) = f c -> (:+:) f g c
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (f c -> (:+:) f g c) -> f c -> (:+:) f g c
forall a b. (a -> b) -> a -> b
$ [(Name b, b)] -> f c -> f c
forall c. [(Name b, b)] -> f c -> f c
forall b (f :: * -> *) c. GSubst b f => [(Name b, b)] -> f c -> f c
gsubsts [(Name b, b)]
ss f c
f
  gsubsts [(Name b, b)]
ss (R1 g c
g) = g c -> (:+:) f g c
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (g c -> (:+:) f g c) -> g c -> (:+:) f g c
forall a b. (a -> b) -> a -> b
$ [(Name b, b)] -> g c -> g c
forall c. [(Name b, b)] -> g c -> g c
forall b (f :: * -> *) c. GSubst b f => [(Name b, b)] -> f c -> f c
gsubsts [(Name b, b)]
ss g c
g

  gsubstBvs :: forall c. AlphaCtx -> [b] -> (:+:) f g c -> (:+:) f g c
gsubstBvs AlphaCtx
c [b]
b (L1 f c
f) = f c -> (:+:) f g c
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (f c -> (:+:) f g c) -> f c -> (:+:) f g c
forall a b. (a -> b) -> a -> b
$ AlphaCtx -> [b] -> f c -> f c
forall c. AlphaCtx -> [b] -> f c -> f c
forall b (f :: * -> *) c.
GSubst b f =>
AlphaCtx -> [b] -> f c -> f c
gsubstBvs AlphaCtx
c [b]
b f c
f
  gsubstBvs AlphaCtx
c [b]
b (R1 g c
g) = g c -> (:+:) f g c
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (g c -> (:+:) f g c) -> g c -> (:+:) f g c
forall a b. (a -> b) -> a -> b
$ AlphaCtx -> [b] -> g c -> g c
forall c. AlphaCtx -> [b] -> g c -> g c
forall b (f :: * -> *) c.
GSubst b f =>
AlphaCtx -> [b] -> f c -> f c
gsubstBvs AlphaCtx
c [b]
b g c
g