Mercurial > urweb
comparison src/unpoly.sml @ 1180:ac3dbbc85c6e
Standard library moduls Incl and Mem; tweaks to Especialize and Unpoly
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 06 Mar 2010 16:15:26 -0500 |
parents | 85d194409b17 |
children | 338be96f8533 |
comparison
equal
deleted
inserted
replaced
1179:c58453683bbb | 1180:ac3dbbc85c6e |
---|---|
256 (** Verifying lack of polymorphic recursion *) | 256 (** Verifying lack of polymorphic recursion *) |
257 | 257 |
258 fun kind _ = false | 258 fun kind _ = false |
259 fun con _ = false | 259 fun con _ = false |
260 | 260 |
261 fun exp e = | 261 fun exp (cn, e) = |
262 case e of | 262 case e of |
263 ECApp (e, c) => | 263 orig as ECApp (e, c) => |
264 let | 264 let |
265 fun isIrregular (e, pos) = | 265 fun isIrregular (e, pos) = |
266 case #1 e of | 266 case #1 e of |
267 ENamed n => | 267 ENamed n => |
268 IS.member (ns, n) | 268 IS.member (ns, n) |
269 andalso | 269 andalso |
270 (case #1 c of | 270 (case #1 c of |
271 CRel i => i <> nargs - pos | 271 CRel i => i <> nargs - pos + cn |
272 | _ => true) | 272 | _ => true) |
273 | ECApp (e, _) => isIrregular (e, pos + 1) | 273 | ECApp (e, _) => isIrregular (e, pos + 1) |
274 | _ => false | 274 | _ => false |
275 in | 275 in |
276 isIrregular (e, 1) | 276 isIrregular (e, 1) |
277 end | 277 end |
278 | ECAbs _ => true | |
279 | _ => false | 278 | _ => false |
280 | 279 |
281 val irregular = U.Exp.exists {kind = kind, con = con, exp = exp} | 280 fun bind (cn, b) = |
281 case b of | |
282 U.Exp.RelC _ => cn+1 | |
283 | _ => cn | |
284 | |
285 val irregular = U.Exp.existsB {kind = kind, con = con, exp = exp, bind = bind} 0 | |
282 in | 286 in |
283 if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then | 287 if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then |
284 (d, st) | 288 (print "Poppycock!\n"; (d, st)) |
285 else | 289 else |
286 (d, {funcs = foldl (fn (vi, funcs) => | 290 (d, {funcs = foldl (fn (vi, funcs) => |
287 IM.insert (funcs, #2 vi, {kinds = cargs, | 291 IM.insert (funcs, #2 vi, {kinds = cargs, |
288 defs = vis, | 292 defs = vis, |
289 replacements = M.empty})) | 293 replacements = M.empty})) |