-
Notifications
You must be signed in to change notification settings - Fork 18
/
Subst.hs
238 lines (202 loc) · 9.15 KB
/
Subst.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
-- |
-- 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 bnd u = instantiate_ bnd u
-- | A version of 'instantiate' with a more general type
instantiate_ :: Subst a b => Bind p b -> [a] -> b
instantiate_ (B _p t) u = substBvs initialCtx u 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 _ = 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 _ = 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 n u x =
if (isFreeName n)
then case (isvar x :: Maybe (SubstName a b)) of
Just (SubstName m) | m == n -> u
_ -> case (isCoerceVar x :: Maybe (SubstCoerce a b)) of
Just (SubstCoerce m f) | m == n -> maybe x id (f u)
_ -> to $ gsubst n u (from x)
else error $ "Cannot substitute for bound variable " ++ show n
substs :: [(Name b, b)] -> a -> a
default substs :: (Generic a, GSubst b (Rep a)) => [(Name b, b)] -> a -> a
substs ss x
| all (isFreeName . fst) ss =
case (isvar x :: Maybe (SubstName a b)) of
Just (SubstName m) | Just (_, u) <- find ((==m) . fst) ss -> u
_ -> case isCoerceVar x :: Maybe (SubstCoerce a b) of
Just (SubstCoerce m f) | Just (_, u) <- find ((==m) . fst) ss -> maybe x id (f u)
_ -> to $ gsubsts ss (from x)
| otherwise =
error $ "Cannot substitute for bound variable in: " ++ show (map fst 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 ctx bs x =
case (isvar x :: Maybe (SubstName a b)) of
Just (SubstName (Bn j k)) | ctxLevel ctx == j, fromInteger k < length bs -> bs !! fromInteger k
_ -> to $ gsubstBvs ctx bs (from 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 nm val = K1 . subst nm val . unK1
gsubsts ss = K1 . substs ss . unK1
gsubstBvs ctx b = K1 . substBvs ctx b . unK1
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
-- 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 _ _ = id ; substs _ = id ; substBvs _ _ = id
instance Subst b Bool where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
instance Subst b () where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
instance Subst b Char where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
instance Subst b Float where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
instance Subst b Double where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
-- huh, apparently there's no instance Generic Integer.
instance Subst b Integer where subst _ _ = id ; substs _ = id ; substBvs _ _ = 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 _ _ = id ; substs _ = id ; substBvs _ _ = id
instance Subst b AnyName where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
instance (Subst c a) => Subst c (Embed a) where
substBvs c us (Embed x)
| isTermCtx c = Embed (substBvs (termCtx c) us x)
| otherwise = error "Internal error: substBvs on Embed"
instance (Subst c e) => Subst c (Shift e) where
subst x b (Shift e) = Shift (subst x b e)
substs ss (Shift e) = Shift (substs ss e)
substBvs c b (Shift e) = Shift (substBvs (decrLevelCtx c) b e)
instance (Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b) where
substBvs c b (B p t) = B (substBvs (patternCtx c) b p) (substBvs (incrLevelCtx c) b t)
instance (Subst c p1, Subst c p2) => Subst c (Rebind p1 p2) where
substBvs c us (Rebnd p q) = Rebnd (substBvs c us p) (substBvs (incrLevelCtx c) us q)
instance (Subst c p) => Subst c (Rec p) where
substBvs c us (Rec p) = Rec (substBvs (incrLevelCtx c) us p)
instance (Alpha p, Subst c p) => Subst c (TRec p) where
substBvs c us (TRec p) = TRec (substBvs (patternCtx (incrLevelCtx c)) us p)
instance Subst a (Ignore b) where
subst _ _ = id
substs _ = id
substBvs _ _ = 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 b u = instantiate_ b [u]