-- |
-- 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 nm val = M1 . gsubst nm val . unM1
  gsubsts ss = M1 . gsubsts ss . unM1
  gsubstBvs c b = M1 . gsubstBvs c b . unM1

instance GSubst b U1 where
  gsubst _nm _val _ = U1
  gsubsts _ss _ = U1
  gsubstBvs _c _b _ = U1

instance GSubst b V1 where
  gsubst _nm _val = id
  gsubsts _ss = id
  gsubstBvs _c _b = id

instance (GSubst b f, GSubst b g) => GSubst b (f :*: g) where
  gsubst nm val (f :*: g) = gsubst nm val f :*: gsubst nm val g
  gsubsts ss (f :*: g) = gsubsts ss f :*: gsubsts ss g
  gsubstBvs c b (f :*: g) = gsubstBvs c b f :*: gsubstBvs c b g

instance (GSubst b f, GSubst b g) => GSubst b (f :+: g) where
  gsubst nm val (L1 f) = L1 $ gsubst nm val f
  gsubst nm val (R1 g) = R1 $ gsubst nm val g

  gsubsts ss (L1 f) = L1 $ gsubsts ss f
  gsubsts ss (R1 g) = R1 $ gsubsts ss g

  gsubstBvs c b (L1 f) = L1 $ gsubstBvs c b f
  gsubstBvs c b (R1 g) = R1 $ gsubstBvs c b g