comparison src/especialize.sml @ 485:3ce20b0b6914

Prevent overzealous Especialization
author Adam Chlipala <adamc@hcoop.net>
date Sun, 09 Nov 2008 17:27:34 -0500
parents a0f47540d8ad
children 33d5bd69da00
comparison
equal deleted inserted replaced
484:685b41e85634 485:3ce20b0b6914
133 decl = default} 133 decl = default}
134 IS.empty file 134 IS.empty file
135 135
136 fun exp (e, st : state) = 136 fun exp (e, st : state) =
137 let 137 let
138 fun getApp e = 138 fun getApp' e =
139 case e of 139 case e of
140 ENamed f => SOME (f, [], []) 140 ENamed f => SOME (f, [], [])
141 | EApp (e1, e2) => 141 | EApp (e1, e2) =>
142 (case getApp (#1 e1) of 142 (case getApp' (#1 e1) of
143 NONE => NONE 143 NONE => NONE
144 | SOME (f, xs, xs') => 144 | SOME (f, xs, xs') =>
145 let 145 let
146 val k = 146 val k =
147 if List.null xs' then 147 if List.null xs' then
152 case k of 152 case k of
153 NONE => SOME (f, xs, xs' @ [e2]) 153 NONE => SOME (f, xs, xs' @ [e2])
154 | SOME k => SOME (f, xs @ [k], xs') 154 | SOME k => SOME (f, xs @ [k], xs')
155 end) 155 end)
156 | _ => NONE 156 | _ => NONE
157
158 fun getApp e =
159 case getApp' e of
160 NONE => NONE
161 | SOME (f, xs, xs') =>
162 if List.all (fn (ERecord [], _) => true | _ => false) xs then
163 SOME (f, [], xs @ xs')
164 else
165 SOME (f, xs, xs')
157 in 166 in
158 case getApp e of 167 case getApp e of
159 NONE => (e, st) 168 NONE => (e, st)
160 | SOME (f, [], []) => (e, st) 169 | SOME (f, [], []) => (e, st)
161 | SOME (f, [], xs') => 170 | SOME (f, [], xs') =>
174 functionInside dom 183 functionInside dom
175 orelse hasFunarg (ran, xs) 184 orelse hasFunarg (ran, xs)
176 | _ => false 185 | _ => false
177 in 186 in
178 if List.all (fn (ERel _, _) => false | _ => true) xs' 187 if List.all (fn (ERel _, _) => false | _ => true) xs'
188 andalso List.exists (fn (ERecord [], _) => false | _ => true) xs'
179 andalso not (IS.member (actionable, f)) 189 andalso not (IS.member (actionable, f))
180 andalso hasFunarg (typ, xs') then 190 andalso hasFunarg (typ, xs') then
181 (#1 (foldl (fn (arg, e) => (EApp (e, arg), ErrorMsg.dummySpan)) 191 (#1 (foldl (fn (arg, e) => (EApp (e, arg), ErrorMsg.dummySpan))
182 body xs'), 192 body xs'),
183 st) 193 st)
184 else 194 else
185 (e, st) 195 (e, st)
186 end) 196 end)
187 | SOME (f, xs, xs') => 197 | SOME (f, xs, xs') =>
188 case IM.find (#funcs st, f) of 198 case IM.find (#funcs st, f) of
189 NONE => (e, st) 199 NONE => (e, st)
190 | SOME {name, args, body, typ, tag} => 200 | SOME {name, args, body, typ, tag} =>
191 case KM.find (args, xs) of 201 case KM.find (args, xs) of
192 SOME f' => (#1 (foldl (fn (arg, e) => (EApp (e, arg), ErrorMsg.dummySpan)) 202 SOME f' => (#1 (foldl (fn (arg, e) => (EApp (e, arg), ErrorMsg.dummySpan))
193 (ENamed f', ErrorMsg.dummySpan) xs'), 203 (ENamed f', ErrorMsg.dummySpan) xs'),
194 st) 204 st)
195 | NONE => 205 | NONE =>
196 let 206 let
197 fun subBody (body, typ, xs) = 207 fun subBody (body, typ, xs) =
198 case (#1 body, #1 typ, xs) of 208 case (#1 body, #1 typ, xs) of
199 (_, _, []) => SOME (body, typ) 209 (_, _, []) => SOME (body, typ)
200 | (EAbs (_, _, _, body'), TFun (_, typ'), x :: xs) => 210 | (EAbs (_, _, _, body'), TFun (_, typ'), x :: xs) =>
201 let 211 let
202 val body'' = E.subExpInExp (0, skeyOut x) body' 212 val body'' = E.subExpInExp (0, skeyOut x) body'
203 in 213 in
204 subBody (body'', 214 subBody (body'',
205 typ', 215 typ',
206 xs) 216 xs)
207 end 217 end
208 | _ => NONE 218 | _ => NONE
209 in 219 in
210 case subBody (body, typ, xs) of 220 case subBody (body, typ, xs) of
211 NONE => (e, st) 221 NONE => (e, st)
212 | SOME (body', typ') => 222 | SOME (body', typ') =>
213 let 223 let
214 val f' = #maxName st 224 val f' = #maxName st
215 val funcs = IM.insert (#funcs st, f, {name = name, 225 val funcs = IM.insert (#funcs st, f, {name = name,
216 args = KM.insert (args, 226 args = KM.insert (args,
217 xs, f'), 227 xs, f'),
218 body = body, 228 body = body,
219 typ = typ, 229 typ = typ,
220 tag = tag}) 230 tag = tag})
221 val st = { 231 val st = {
222 maxName = f' + 1, 232 maxName = f' + 1,
223 funcs = funcs, 233 funcs = funcs,
224 decls = #decls st 234 decls = #decls st
225 } 235 }
226 236
227 val (body', st) = specExp st body' 237 val (body', st) = specExp st body'
228 val e' = foldl (fn (arg, e) => (EApp (e, arg), ErrorMsg.dummySpan)) 238 val e' = foldl (fn (arg, e) => (EApp (e, arg), ErrorMsg.dummySpan))
229 (ENamed f', ErrorMsg.dummySpan) xs' 239 (ENamed f', ErrorMsg.dummySpan) xs'
230 in 240 in
231 (#1 e', 241 (#1 e',
232 {maxName = #maxName st, 242 {maxName = #maxName st,
233 funcs = #funcs st, 243 funcs = #funcs st,
234 decls = (name, f', typ', body', tag) :: #decls st}) 244 decls = (name, f', typ', body', tag) :: #decls st})
235 end 245 end
236 end 246 end
237 end 247 end
238 248
239 and specExp st = U.Exp.foldMap {kind = kind, con = con, exp = exp} st 249 and specExp st = U.Exp.foldMap {kind = kind, con = con, exp = exp} st
240 250
241 fun decl (d, st) = (d, st) 251 fun decl (d, st) = (d, st)
242 252