@@ -63,13 +63,14 @@ import Unbound.Generics.LocallyNameless.Ignore
63
63
import Unbound.Generics.LocallyNameless.Bind
64
64
import Unbound.Generics.LocallyNameless.Rebind
65
65
import Unbound.Generics.LocallyNameless.Rec
66
+ import Unbound.Generics.LocallyNameless.Internal.GSubst
66
67
67
68
-- | See 'isVar'
68
69
data SubstName a b where
69
70
SubstName :: (a ~ b ) => Name a -> SubstName a b
70
71
71
- -- | See 'isCoerceVar'
72
- data SubstCoerce a b where
72
+ -- | See 'isCoerceVar'
73
+ data SubstCoerce a b where
73
74
SubstCoerce :: Name b -> (b -> Maybe a ) -> SubstCoerce a b
74
75
75
76
-- | Immediately substitute for the bound variables of a pattern
@@ -92,7 +93,7 @@ class Subst b a where
92
93
isvar :: a -> Maybe (SubstName a b )
93
94
isvar _ = Nothing
94
95
95
- -- | This is an alternative version to 'isvar', useable in the case
96
+ -- | This is an alternative version to 'isvar', useable in the case
96
97
-- that the substituted argument doesn't have *exactly* the same type
97
98
-- as the term it should be substituted into.
98
99
-- The default implementation always returns 'Nothing'.
@@ -118,7 +119,7 @@ class Subst b a where
118
119
| all (isFreeName . fst ) ss =
119
120
case (isvar x :: Maybe (SubstName a b )) of
120
121
Just (SubstName m) | Just (_, u) <- find ((== m) . fst ) ss -> u
121
- _ -> case isCoerceVar x :: Maybe (SubstCoerce a b ) of
122
+ _ -> case isCoerceVar x :: Maybe (SubstCoerce a b ) of
122
123
Just (SubstCoerce m f) | Just (_, u) <- find ((== m) . fst ) ss -> maybe x id (f u)
123
124
_ -> to $ gsubsts ss (from x)
124
125
| otherwise =
@@ -135,48 +136,11 @@ class Subst b a where
135
136
Just (SubstName (Bn j k)) | ctxLevel ctx == j, fromInteger k < length bs -> bs !! fromInteger k
136
137
_ -> to $ gsubstBvs ctx bs (from x)
137
138
138
- ---- generic structural substitution.
139
-
140
- class GSubst b f where
141
- gsubst :: Name b -> b -> f c -> f c
142
- gsubsts :: [(Name b , b )] -> f c -> f c
143
- gsubstBvs :: AlphaCtx -> [b ] -> f c -> f c
144
-
145
139
instance Subst b c => GSubst b (K1 i c ) where
146
140
gsubst nm val = K1 . subst nm val . unK1
147
141
gsubsts ss = K1 . substs ss . unK1
148
142
gsubstBvs ctx b = K1 . substBvs ctx b . unK1
149
143
150
- instance GSubst b f => GSubst b (M1 i c f ) where
151
- gsubst nm val = M1 . gsubst nm val . unM1
152
- gsubsts ss = M1 . gsubsts ss . unM1
153
- gsubstBvs c b = M1 . gsubstBvs c b . unM1
154
-
155
- instance GSubst b U1 where
156
- gsubst _nm _val _ = U1
157
- gsubsts _ss _ = U1
158
- gsubstBvs _c _b _ = U1
159
-
160
- instance GSubst b V1 where
161
- gsubst _nm _val = id
162
- gsubsts _ss = id
163
- gsubstBvs _c _b = id
164
-
165
- instance (GSubst b f , GSubst b g ) => GSubst b (f :*: g ) where
166
- gsubst nm val (f :*: g) = gsubst nm val f :*: gsubst nm val g
167
- gsubsts ss (f :*: g) = gsubsts ss f :*: gsubsts ss g
168
- gsubstBvs c b (f :*: g) = gsubstBvs c b f :*: gsubstBvs c b g
169
-
170
- instance (GSubst b f , GSubst b g ) => GSubst b (f :+: g ) where
171
- gsubst nm val (L1 f) = L1 $ gsubst nm val f
172
- gsubst nm val (R1 g) = R1 $ gsubst nm val g
173
-
174
- gsubsts ss (L1 f) = L1 $ gsubsts ss f
175
- gsubsts ss (R1 g) = R1 $ gsubsts ss g
176
-
177
- gsubstBvs c b (L1 f) = L1 $ gsubstBvs c b f
178
- gsubstBvs c b (R1 g) = R1 $ gsubstBvs c b g
179
-
180
144
-- these have a Generic instance, but
181
145
-- it's self-refential (ie: Rep Int = D1 (C1 (S1 (Rec0 Int))))
182
146
-- so our structural GSubst instances get stuck in an infinite loop.
@@ -187,7 +151,7 @@ instance Subst b Char where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
187
151
instance Subst b Float where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
188
152
instance Subst b Double where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
189
153
190
- -- huh, apparently there's no instance Generic Integer.
154
+ -- huh, apparently there's no instance Generic Integer.
191
155
instance Subst b Integer where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
192
156
193
157
instance (Subst c a , Subst c b ) => Subst c (a ,b )
0 commit comments