{-# LANGUAGE DefaultSignatures
, FlexibleContexts
, FlexibleInstances
, GADTs
, MultiParamTypeClasses
, ScopedTypeVariables
, TypeOperators
#-}
module Unbound.Generics.LocallyNameless.Subst (
SubstName(..)
, SubstCoerce(..)
, Subst(..)
) 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
data SubstName a b where
SubstName :: (a ~ b) => Name a -> SubstName a b
data SubstCoerce a b where
SubstCoerce :: Name b -> (b -> Maybe a) -> SubstCoerce a b
class Subst b a where
isvar :: a -> Maybe (SubstName a b)
isvar a
_ = Maybe (SubstName a b)
forall a. Maybe a
Nothing
isCoerceVar :: a -> Maybe (SubstCoerce a b)
isCoerceVar a
_ = Maybe (SubstCoerce a b)
forall a. Maybe a
Nothing
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
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 b (f :: * -> *) c. GSubst b f => Name b -> b -> f c -> f c
gsubst Name b
n b
u (a -> Rep a Any
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
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 b (f :: * -> *) c. GSubst b f => [(Name b, b)] -> f c -> f c
gsubsts [(Name b, b)]
ss (a -> Rep a Any
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)
class GSubst b f where
gsubst :: Name b -> b -> f c -> f c
gsubsts :: [(Name b, 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
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 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 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
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
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
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 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 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 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 b (f :: * -> *) c. GSubst b f => [(Name b, b)] -> f c -> f c
gsubsts [(Name b, b)]
ss 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 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 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 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 b (f :: * -> *) c. GSubst b f => [(Name b, b)] -> f c -> f c
gsubsts [(Name b, b)]
ss g c
g
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
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
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
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
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
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
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
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
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
instance (Subst c a) => Subst c (Embed a)
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)
instance (Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b)
instance (Subst c p1, Subst c p2) => Subst c (Rebind p1 p2)
instance (Subst c p) => Subst c (Rec p)
instance (Alpha p, Subst c p) => Subst c (TRec 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