-- |
-- Module     : Unbound.Generics.LocallyNameless.Subst
-- Copyright  : (c) 2014, Aleksey Kliger
-- License    : BSD3 (See LICENSE)
-- Maintainer : Aleksey Kliger
-- Stability  : experimental
--
-- A typeclass for types that may participate in capture-avoiding substitution
--
-- The minimal definition is empty, provided your type is an instance of 'GHC.Generics.Generic'
-- 
-- @
-- type Var = Name Factor
-- data Expr = SumOf [Summand]
--           deriving (Show, Generic)
-- data Summand = ProductOf [Factor]
--           deriving (Show, Generic)
-- instance Subst Var Expr
-- instance Subst Var Summand
-- @
-- 
-- The default instance just propagates the substitution into the constituent factors.
-- 
-- If you identify the variable occurrences by implementing the 'isvar' function, the derived 'subst' function
-- will be able to substitute a factor for a variable.
-- 
-- @
-- data Factor = V Var
--             | C Int
--             | Subexpr Expr
--           deriving (Show, Generic)
-- instance Subst Var Factor where
--   isvar (V v) = Just (SubstName v)
--   isvar _     = Nothing
-- @
--
{-# LANGUAGE DefaultSignatures
             , FlexibleContexts
             , FlexibleInstances
             , GADTs
             , MultiParamTypeClasses
             , ScopedTypeVariables
             , TypeOperators
 #-}
module Unbound.Generics.LocallyNameless.Subst (
  SubstName(..)
  , SubstCoerce(..)
  , Subst(..)
  , substBind
  , instantiate
  ) where

import GHC.Generics

import Data.List (find)

import Unbound.Generics.LocallyNameless.Name
import Unbound.Generics.LocallyNameless.Alpha
import Unbound.Generics.LocallyNameless.Embed
import Unbound.Generics.LocallyNameless.Shift
import Unbound.Generics.LocallyNameless.Ignore
import Unbound.Generics.LocallyNameless.Bind
import Unbound.Generics.LocallyNameless.Rebind
import Unbound.Generics.LocallyNameless.Rec

-- | See 'isVar'
data SubstName a b where
  SubstName :: (a ~ b) => Name a -> SubstName a b

-- | See 'isCoerceVar'  
data SubstCoerce a b where  
  SubstCoerce :: Name b -> (b -> Maybe a) -> SubstCoerce a b

-- | Immediately substitute for the bound variables of a pattern
-- in a binder, without first naming the variables.
-- NOTE: this operation does not check that the number of terms passed in
-- match the number of variables in the pattern. (Or that they are of appropriate type.)
instantiate :: (Alpha a, Alpha b, Alpha p , Subst a b) => Bind p b -> [a] -> b
instantiate :: forall a b p.
(Alpha a, Alpha b, Alpha p, Subst a b) =>
Bind p b -> [a] -> b
instantiate Bind p b
bnd [a]
u = Bind p b -> [a] -> b
forall a b p. Subst a b => Bind p b -> [a] -> b
instantiate_ Bind p b
bnd [a]
u

-- | A version of 'instantiate' with a more general type
instantiate_ :: Subst a b => Bind p b -> [a] -> b
instantiate_ :: forall a b p. Subst a b => Bind p b -> [a] -> b
instantiate_ (B p
_p b
t) [a]
u = AlphaCtx -> [a] -> b -> b
forall b a. Subst b a => AlphaCtx -> [b] -> a -> a
substBvs AlphaCtx
initialCtx [a]
u b
t


-- | Instances of @'Subst' b a@ are terms of type @a@ that may contain
-- variables of type @b@ that may participate in capture-avoiding
-- substitution.
class Subst b a where
  -- | This is the only method that must be implemented
  isvar :: a -> Maybe (SubstName a b)
  isvar a
_ = Maybe (SubstName a b)
forall a. Maybe a
Nothing

  -- | This is an alternative version to 'isvar', useable in the case 
  --   that the substituted argument doesn't have *exactly* the same type
  --   as the term it should be substituted into.
  --   The default implementation always returns 'Nothing'.
  isCoerceVar :: a -> Maybe (SubstCoerce a b)
  isCoerceVar a
_ = Maybe (SubstCoerce a b)
forall a. Maybe a
Nothing

  -- | @'subst' nm e tm@ substitutes @e@ for @nm@ in @tm@.  It has
  -- a default generic implementation in terms of @isvar@
  subst :: Name b -> b -> a -> a
  default subst :: (Generic a, GSubst b (Rep a)) => Name b -> b -> a -> a
  subst Name b
n b
u a
x =
    if (Name b -> Bool
forall a. Name a -> Bool
isFreeName Name b
n)
    then case (a -> Maybe (SubstName a b)
forall b a. Subst b a => a -> Maybe (SubstName a b)
isvar a
x :: Maybe (SubstName a b)) of
      Just (SubstName Name a
m) | Name a
m Name a -> Name a -> Bool
forall a. Eq a => a -> a -> Bool
== Name b
Name a
n -> b
a
u
      Maybe (SubstName a b)
_ -> case (a -> Maybe (SubstCoerce a b)
forall b a. Subst b a => a -> Maybe (SubstCoerce a b)
isCoerceVar a
x :: Maybe (SubstCoerce a b)) of
        Just (SubstCoerce Name b
m b -> Maybe a
f) | Name b
m Name b -> Name b -> Bool
forall a. Eq a => a -> a -> Bool
== Name b
n -> a -> (a -> a) -> Maybe a -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe a
x a -> a
forall a. a -> a
id (b -> Maybe a
f b
u)
        Maybe (SubstCoerce a b)
_ -> Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> Rep a Any -> a
forall a b. (a -> b) -> a -> b
$ Name b -> b -> Rep a Any -> Rep a Any
forall c. Name b -> b -> Rep a c -> Rep a c
forall b (f :: * -> *) c. GSubst b f => Name b -> b -> f c -> f c
gsubst Name b
n b
u (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
x)
    else [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot substitute for bound variable " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name b -> [Char]
forall a. Show a => a -> [Char]
show Name b
n

  substs :: [(Name b, b)] -> a -> a
  default substs :: (Generic a, GSubst b (Rep a)) => [(Name b, b)] -> a -> a
  substs [(Name b, b)]
ss a
x
    | ((Name b, b) -> Bool) -> [(Name b, b)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Name b -> Bool
forall a. Name a -> Bool
isFreeName (Name b -> Bool) -> ((Name b, b) -> Name b) -> (Name b, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name b, b) -> Name b
forall a b. (a, b) -> a
fst) [(Name b, b)]
ss =
      case (a -> Maybe (SubstName a b)
forall b a. Subst b a => a -> Maybe (SubstName a b)
isvar a
x :: Maybe (SubstName a b)) of
        Just (SubstName Name a
m) | Just (Name a
_, b
u) <- ((Name a, b) -> Bool) -> [(Name a, b)] -> Maybe (Name a, b)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Name a -> Name a -> Bool
forall a. Eq a => a -> a -> Bool
==Name a
m) (Name a -> Bool) -> ((Name a, b) -> Name a) -> (Name a, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name a, b) -> Name a
forall a b. (a, b) -> a
fst) [(Name b, b)]
[(Name a, b)]
ss -> b
a
u
        Maybe (SubstName a b)
_ -> case a -> Maybe (SubstCoerce a b)
forall b a. Subst b a => a -> Maybe (SubstCoerce a b)
isCoerceVar a
x :: Maybe (SubstCoerce a b) of 
            Just (SubstCoerce Name b
m b -> Maybe a
f) | Just (Name b
_, b
u) <- ((Name b, b) -> Bool) -> [(Name b, b)] -> Maybe (Name b, b)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Name b -> Name b -> Bool
forall a. Eq a => a -> a -> Bool
==Name b
m) (Name b -> Bool) -> ((Name b, b) -> Name b) -> (Name b, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name b, b) -> Name b
forall a b. (a, b) -> a
fst) [(Name b, b)]
ss -> a -> (a -> a) -> Maybe a -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe a
x a -> a
forall a. a -> a
id (b -> Maybe a
f b
u)
            Maybe (SubstCoerce a b)
_ -> Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> Rep a Any -> a
forall a b. (a -> b) -> a -> b
$ [(Name b, b)] -> Rep a Any -> Rep a Any
forall c. [(Name b, b)] -> Rep a c -> Rep a c
forall b (f :: * -> *) c. GSubst b f => [(Name b, b)] -> f c -> f c
gsubsts [(Name b, b)]
ss (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
x)
    | Bool
otherwise =
      [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot substitute for bound variable in: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Name b] -> [Char]
forall a. Show a => a -> [Char]
show (((Name b, b) -> Name b) -> [(Name b, b)] -> [Name b]
forall a b. (a -> b) -> [a] -> [b]
map (Name b, b) -> Name b
forall a b. (a, b) -> a
fst [(Name b, b)]
ss)

   -- Bound variable substitution (replace a single pattern variable with a list of terms)
   -- Similar to open, but replaces with b's instead of with names
   -- Does not check whether enough b's are provided: will ignore extra if there are too many
   -- and skip the substitution if there are too few.
  substBvs :: AlphaCtx -> [b] -> a -> a
  default substBvs :: (Generic a, GSubst b (Rep a)) => AlphaCtx -> [b] -> a -> a
  substBvs AlphaCtx
ctx [b]
bs a
x =
     case (a -> Maybe (SubstName a b)
forall b a. Subst b a => a -> Maybe (SubstName a b)
isvar a
x :: Maybe (SubstName a b)) of
        Just (SubstName (Bn Integer
j Integer
k)) | AlphaCtx -> Integer
ctxLevel AlphaCtx
ctx Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j, Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [b] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
bs -> [b]
[a]
bs [a] -> Int -> a
forall a. HasCallStack => [a] -> Int -> a
!! Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
k
        Maybe (SubstName a b)
_ -> Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> Rep a Any -> a
forall a b. (a -> b) -> a -> b
$ AlphaCtx -> [b] -> Rep a Any -> Rep a Any
forall c. AlphaCtx -> [b] -> Rep a c -> Rep a c
forall b (f :: * -> *) c.
GSubst b f =>
AlphaCtx -> [b] -> f c -> f c
gsubstBvs AlphaCtx
ctx [b]
bs (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
x)

---- 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 Subst b c => GSubst b (K1 i c) where
  gsubst :: forall c. Name b -> b -> K1 i c c -> K1 i c c
gsubst Name b
nm b
val = c -> K1 i c c
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c c) -> (K1 i c c -> c) -> K1 i c c -> K1 i c c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name b -> b -> c -> c
forall b a. Subst b a => Name b -> b -> a -> a
subst Name b
nm b
val (c -> c) -> (K1 i c c -> c) -> K1 i c c -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i c c -> c
forall k i c (p :: k). K1 i c p -> c
unK1
  gsubsts :: forall c. [(Name b, b)] -> K1 i c c -> K1 i c c
gsubsts [(Name b, b)]
ss = c -> K1 i c c
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c c) -> (K1 i c c -> c) -> K1 i c c -> K1 i c c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name b, b)] -> c -> c
forall b a. Subst b a => [(Name b, b)] -> a -> a
substs [(Name b, b)]
ss (c -> c) -> (K1 i c c -> c) -> K1 i c c -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i c c -> c
forall k i c (p :: k). K1 i c p -> c
unK1
  gsubstBvs :: forall c. AlphaCtx -> [b] -> K1 i c c -> K1 i c c
gsubstBvs AlphaCtx
ctx [b]
b = c -> K1 i c c
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c c) -> (K1 i c c -> c) -> K1 i c c -> K1 i c c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlphaCtx -> [b] -> c -> c
forall b a. Subst b a => AlphaCtx -> [b] -> a -> a
substBvs AlphaCtx
ctx [b]
b (c -> c) -> (K1 i c c -> c) -> K1 i c c -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i c c -> c
forall k i c (p :: k). K1 i c p -> c
unK1

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

-- these have a Generic instance, but
-- it's self-refential (ie: Rep Int = D1 (C1 (S1 (Rec0 Int))))
-- so our structural GSubst instances get stuck in an infinite loop.
instance Subst b Int where subst :: Name b -> b -> Int -> Int
subst Name b
_ b
_ = Int -> Int
forall a. a -> a
id ; substs :: [(Name b, b)] -> Int -> Int
substs [(Name b, b)]
_ = Int -> Int
forall a. a -> a
id ; substBvs :: AlphaCtx -> [b] -> Int -> Int
substBvs AlphaCtx
_ [b]
_ = Int -> Int
forall a. a -> a
id
instance Subst b Bool where subst :: Name b -> b -> Bool -> Bool
subst Name b
_ b
_ = Bool -> Bool
forall a. a -> a
id ; substs :: [(Name b, b)] -> Bool -> Bool
substs [(Name b, b)]
_ = Bool -> Bool
forall a. a -> a
id ; substBvs :: AlphaCtx -> [b] -> Bool -> Bool
substBvs AlphaCtx
_ [b]
_ = Bool -> Bool
forall a. a -> a
id
instance Subst b () where subst :: Name b -> b -> () -> ()
subst Name b
_ b
_ = () -> ()
forall a. a -> a
id ; substs :: [(Name b, b)] -> () -> ()
substs [(Name b, b)]
_ = () -> ()
forall a. a -> a
id ; substBvs :: AlphaCtx -> [b] -> () -> ()
substBvs AlphaCtx
_ [b]
_ = () -> ()
forall a. a -> a
id
instance Subst b Char where subst :: Name b -> b -> Char -> Char
subst Name b
_ b
_ = Char -> Char
forall a. a -> a
id ; substs :: [(Name b, b)] -> Char -> Char
substs [(Name b, b)]
_ = Char -> Char
forall a. a -> a
id ; substBvs :: AlphaCtx -> [b] -> Char -> Char
substBvs AlphaCtx
_ [b]
_ = Char -> Char
forall a. a -> a
id
instance Subst b Float where subst :: Name b -> b -> Float -> Float
subst Name b
_ b
_ = Float -> Float
forall a. a -> a
id ; substs :: [(Name b, b)] -> Float -> Float
substs [(Name b, b)]
_ = Float -> Float
forall a. a -> a
id ; substBvs :: AlphaCtx -> [b] -> Float -> Float
substBvs AlphaCtx
_ [b]
_ = Float -> Float
forall a. a -> a
id
instance Subst b Double where subst :: Name b -> b -> Double -> Double
subst Name b
_ b
_ = Double -> Double
forall a. a -> a
id ; substs :: [(Name b, b)] -> Double -> Double
substs [(Name b, b)]
_ = Double -> Double
forall a. a -> a
id ; substBvs :: AlphaCtx -> [b] -> Double -> Double
substBvs AlphaCtx
_ [b]
_ = Double -> Double
forall a. a -> a
id

-- huh, apparently there's no instance Generic Integer. 
instance Subst b Integer where subst :: Name b -> b -> Integer -> Integer
subst Name b
_ b
_ = Integer -> Integer
forall a. a -> a
id ; substs :: [(Name b, b)] -> Integer -> Integer
substs [(Name b, b)]
_ = Integer -> Integer
forall a. a -> a
id ; substBvs :: AlphaCtx -> [b] -> Integer -> Integer
substBvs AlphaCtx
_ [b]
_ = Integer -> Integer
forall a. a -> a
id

instance (Subst c a, Subst c b) => Subst c (a,b)
instance (Subst c a, Subst c b, Subst c d) => Subst c (a,b,d)
instance (Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a,b,d,e)
instance (Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) =>
   Subst c (a,b,d,e,f)
instance (Subst c a) => Subst c [a]
instance (Subst c a) => Subst c (Maybe a)
instance (Subst c a, Subst c b) => Subst c (Either a b)

instance Subst b (Name a) where subst :: Name b -> b -> Name a -> Name a
subst Name b
_ b
_ = Name a -> Name a
forall a. a -> a
id  ; substs :: [(Name b, b)] -> Name a -> Name a
substs [(Name b, b)]
_ = Name a -> Name a
forall a. a -> a
id ; substBvs :: AlphaCtx -> [b] -> Name a -> Name a
substBvs AlphaCtx
_ [b]
_ = Name a -> Name a
forall a. a -> a
id
instance Subst b AnyName where subst :: Name b -> b -> AnyName -> AnyName
subst Name b
_ b
_ = AnyName -> AnyName
forall a. a -> a
id ; substs :: [(Name b, b)] -> AnyName -> AnyName
substs [(Name b, b)]
_ = AnyName -> AnyName
forall a. a -> a
id ; substBvs :: AlphaCtx -> [b] -> AnyName -> AnyName
substBvs AlphaCtx
_ [b]
_ = AnyName -> AnyName
forall a. a -> a
id

instance (Subst c a) => Subst c (Embed a) where
  substBvs :: AlphaCtx -> [c] -> Embed a -> Embed a
substBvs AlphaCtx
c [c]
us (Embed a
x)
    | AlphaCtx -> Bool
isTermCtx AlphaCtx
c = a -> Embed a
forall t. t -> Embed t
Embed (AlphaCtx -> [c] -> a -> a
forall b a. Subst b a => AlphaCtx -> [b] -> a -> a
substBvs (AlphaCtx -> AlphaCtx
termCtx AlphaCtx
c) [c]
us a
x)
    | Bool
otherwise = [Char] -> Embed a
forall a. HasCallStack => [Char] -> a
error [Char]
"Internal error: substBvs on Embed"

instance (Subst c e) => Subst c (Shift e) where
  subst :: Name c -> c -> Shift e -> Shift e
subst Name c
x c
b (Shift e
e) = e -> Shift e
forall e. e -> Shift e
Shift (Name c -> c -> e -> e
forall b a. Subst b a => Name b -> b -> a -> a
subst Name c
x c
b e
e)
  substs :: [(Name c, c)] -> Shift e -> Shift e
substs [(Name c, c)]
ss (Shift e
e) = e -> Shift e
forall e. e -> Shift e
Shift ([(Name c, c)] -> e -> e
forall b a. Subst b a => [(Name b, b)] -> a -> a
substs [(Name c, c)]
ss e
e)
  substBvs :: AlphaCtx -> [c] -> Shift e -> Shift e
substBvs AlphaCtx
c [c]
b (Shift e
e) = e -> Shift e
forall e. e -> Shift e
Shift (AlphaCtx -> [c] -> e -> e
forall b a. Subst b a => AlphaCtx -> [b] -> a -> a
substBvs (AlphaCtx -> AlphaCtx
decrLevelCtx AlphaCtx
c) [c]
b e
e)

instance (Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b) where
  substBvs :: AlphaCtx -> [c] -> Bind a b -> Bind a b
substBvs AlphaCtx
c [c]
b (B a
p b
t) = a -> b -> Bind a b
forall p t. p -> t -> Bind p t
B (AlphaCtx -> [c] -> a -> a
forall b a. Subst b a => AlphaCtx -> [b] -> a -> a
substBvs (AlphaCtx -> AlphaCtx
patternCtx AlphaCtx
c) [c]
b a
p) (AlphaCtx -> [c] -> b -> b
forall b a. Subst b a => AlphaCtx -> [b] -> a -> a
substBvs (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
c) [c]
b b
t)

instance (Subst c p1, Subst c p2) => Subst c (Rebind p1 p2) where
  substBvs :: AlphaCtx -> [c] -> Rebind p1 p2 -> Rebind p1 p2
substBvs AlphaCtx
c [c]
us (Rebnd p1
p p2
q) = p1 -> p2 -> Rebind p1 p2
forall p1 p2. p1 -> p2 -> Rebind p1 p2
Rebnd (AlphaCtx -> [c] -> p1 -> p1
forall b a. Subst b a => AlphaCtx -> [b] -> a -> a
substBvs AlphaCtx
c [c]
us p1
p) (AlphaCtx -> [c] -> p2 -> p2
forall b a. Subst b a => AlphaCtx -> [b] -> a -> a
substBvs (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
c) [c]
us p2
q)

instance (Subst c p) => Subst c (Rec p) where
  substBvs :: AlphaCtx -> [c] -> Rec p -> Rec p
substBvs AlphaCtx
c [c]
us (Rec p
p) = p -> Rec p
forall p. p -> Rec p
Rec (AlphaCtx -> [c] -> p -> p
forall b a. Subst b a => AlphaCtx -> [b] -> a -> a
substBvs (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
c) [c]
us p
p)

instance (Alpha p, Subst c p) => Subst c (TRec p) where
  substBvs :: AlphaCtx -> [c] -> TRec p -> TRec p
substBvs AlphaCtx
c [c]
us (TRec Bind (Rec p) ()
p) = Bind (Rec p) () -> TRec p
forall p. Bind (Rec p) () -> TRec p
TRec (AlphaCtx -> [c] -> Bind (Rec p) () -> Bind (Rec p) ()
forall b a. Subst b a => AlphaCtx -> [b] -> a -> a
substBvs (AlphaCtx -> AlphaCtx
patternCtx (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
c)) [c]
us Bind (Rec p) ()
p)

instance Subst a (Ignore b) where
  subst :: Name a -> a -> Ignore b -> Ignore b
subst Name a
_ a
_ = Ignore b -> Ignore b
forall a. a -> a
id
  substs :: [(Name a, a)] -> Ignore b -> Ignore b
substs [(Name a, a)]
_ = Ignore b -> Ignore b
forall a. a -> a
id
  substBvs :: AlphaCtx -> [a] -> Ignore b -> Ignore b
substBvs AlphaCtx
_ [a]
_ = Ignore b -> Ignore b
forall a. a -> a
id

-- | Specialized version of capture-avoiding substitution for that operates on a @'Bind' ('Name' a) t@ term to @'unbind'@
-- the bound name @Name a@ and immediately subsitute a new term for its occurrences.
--
-- This is a specialization of @'instantiate' :: Bind pat term -> [a] -> term@ where the @'Bind' pat term@ has a pattern that is just
-- a single @'Name' a@ and there is a single substitution term of type @a@.  Unlike 'instantiate', this function cannot fail at runtime.
substBind :: Subst a t => Bind (Name a) t -> a -> t
substBind :: forall a t. Subst a t => Bind (Name a) t -> a -> t
substBind Bind (Name a) t
b a
u = Bind (Name a) t -> [a] -> t
forall a b p. Subst a b => Bind p b -> [a] -> b
instantiate_ Bind (Name a) t
b [a
u]