{-# 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
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