Mercurial > urweb

comparison src/unpoly.sml @ 1122:85d194409b17

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Reduce concatenations of the empty record; unpoly non-recursive functions
author Adam Chlipala <adamc@hcoop.net>
date Sun, 10 Jan 2010 13:44:22 -0500
parents 065ce3252090
children ac3dbbc85c6e
comparison
equal deleted inserted replaced
1121:0cee0c8d8c37 1122:85d194409b17
205 | _ => (e, st) 205 | _ => (e, st)
206 206
207 and polyExp (x, st) = U.Exp.foldMap {kind = kind, con = con, exp = exp} st x 207 and polyExp (x, st) = U.Exp.foldMap {kind = kind, con = con, exp = exp} st x
208 208
209 fun decl (d, st : state) = 209 fun decl (d, st : state) =
210 case d of 210 let
211 DValRec (vis as ((x, n, t, e, s) :: rest)) => 211 fun unravel (e, cargs) =
212 let 212 case e of
213 fun unravel (e, cargs) = 213 (ECAbs (_, k, e), _) =>
214 case e of 214 unravel (e, k :: cargs)
215 (ECAbs (_, k, e), _) => 215 | _ => rev cargs
216 unravel (e, k :: cargs) 216 in
217 | _ => rev cargs 217 case d of
218 218 DVal (vi as (x, n, t, e, s)) =>
219 val cargs = unravel (e, []) 219 let
220 220 val cargs = unravel (e, [])
221 fun unravel (e, cargs) = 221
222 case (e, cargs) of 222 val ns = IS.singleton n
223 ((ECAbs (_, k, e), _), k' :: cargs) => 223 in
224 U.Kind.compare (k, k') = EQUAL 224 (d, {funcs = IM.insert (#funcs st, n, {kinds = cargs,
225 andalso unravel (e, cargs) 225 defs = [vi],
226 | (_, []) => true 226 replacements = M.empty}),
227 | _ => false 227 decls = #decls st,
228 in 228 nextName = #nextName st})
229 if List.exists (fn vi => not (unravel (#4 vi, cargs))) rest then 229 end
230 (d, st) 230 | DValRec (vis as ((x, n, t, e, s) :: rest)) =>
231 else 231 let
232 let 232 val cargs = unravel (e, [])
233 val ns = IS.addList (IS.empty, map #2 vis) 233
234 val nargs = length cargs 234 fun unravel (e, cargs) =
235 235 case (e, cargs) of
236 fun deAbs (e, cargs) = 236 ((ECAbs (_, k, e), _), k' :: cargs) =>
237 case (e, cargs) of 237 U.Kind.compare (k, k') = EQUAL
238 ((ECAbs (_, _, e), _), _ :: cargs) => deAbs (e, cargs) 238 andalso unravel (e, cargs)
239 | (_, []) => e 239 | (_, []) => true
240 | _ => raise Fail "Unpoly: deAbs" 240 | _ => false
241 241
242 (** Verifying lack of polymorphic recursion *) 242 fun deAbs (e, cargs) =
243 243 case (e, cargs) of
244 fun kind _ = false 244 ((ECAbs (_, _, e), _), _ :: cargs) => deAbs (e, cargs)
245 fun con _ = false 245 | (_, []) => e
246 246 | _ => raise Fail "Unpoly: deAbs"
247 fun exp e = 247
248 case e of 248 in
249 ECApp (e, c) => 249 if List.exists (fn vi => not (unravel (#4 vi, cargs))) rest then
250 let 250 (d, st)
251 fun isIrregular (e, pos) = 251 else
252 case #1 e of 252 let
253 ENamed n => 253 val ns = IS.addList (IS.empty, map #2 vis)
254 IS.member (ns, n) 254 val nargs = length cargs
255 andalso 255
256 (case #1 c of 256 (** Verifying lack of polymorphic recursion *)
257 CRel i => i <> nargs - pos 257
258 | _ => true) 258 fun kind _ = false
259 | ECApp (e, _) => isIrregular (e, pos + 1) 259 fun con _ = false
260 | _ => false 260
261 in 261 fun exp e =
262 isIrregular (e, 1) 262 case e of
263 end 263 ECApp (e, c) =>
264 | ECAbs _ => true 264 let
265 | _ => false 265 fun isIrregular (e, pos) =
266 266 case #1 e of
267 val irregular = U.Exp.exists {kind = kind, con = con, exp = exp} 267 ENamed n =>
268 in 268 IS.member (ns, n)
269 if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then 269 andalso
270 (d, st) 270 (case #1 c of
271 else 271 CRel i => i <> nargs - pos
272 (d, {funcs = foldl (fn (vi, funcs) => 272 | _ => true)
273 IM.insert (funcs, #2 vi, {kinds = cargs, 273 | ECApp (e, _) => isIrregular (e, pos + 1)
274 defs = vis, 274 | _ => false
275 replacements = M.empty})) 275 in
276 (#funcs st) vis, 276 isIrregular (e, 1)
277 decls = #decls st, 277 end
278 nextName = #nextName st}) 278 | ECAbs _ => true
279 end 279 | _ => false
280 end 280
281 281 val irregular = U.Exp.exists {kind = kind, con = con, exp = exp}
282 | _ => (d, st) 282 in
283 if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then
284 (d, st)
285 else
286 (d, {funcs = foldl (fn (vi, funcs) =>
287 IM.insert (funcs, #2 vi, {kinds = cargs,
288 defs = vis,
289 replacements = M.empty}))
290 (#funcs st) vis,
291 decls = #decls st,
292 nextName = #nextName st})
293 end
294 end
295
296 | _ => (d, st)
297 end
283 298
284 val polyDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl} 299 val polyDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl}
285 300
286 fun unpoly file = 301 fun unpoly file =
287 let 302 let