Mercurial > urweb

comparison src/unpoly.sml @ 1180:ac3dbbc85c6e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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}))