comparison src/core_util.sml @ 479:ffa18975e661

Broaden set of possible especializations
author Adam Chlipala <adamc@hcoop.net>
date Sat, 08 Nov 2008 14:42:52 -0500
parents 5c9606deacb6
children 9117a7bf229c
comparison
equal deleted inserted replaced
478:6ee1c761818f 479:ffa18975e661
328 | S.Return _ => raise Fail "CoreUtil.Con.foldMap: Impossible" 328 | S.Return _ => raise Fail "CoreUtil.Con.foldMap: Impossible"
329 329
330 end 330 end
331 331
332 structure Exp = struct 332 structure Exp = struct
333
334 open Order
335
336 fun pcCompare (pc1, pc2) =
337 case (pc1, pc2) of
338 (PConVar n1, PConVar n2) => Int.compare (n1, n2)
339 | (PConVar _, _) => LESS
340 | (_, PConVar _) => GREATER
341
342 | (PConFfi {mod = m1, datatyp = d1, con = c1, ...},
343 PConFfi {mod = m2, datatyp = d2, con = c2, ...}) =>
344 join (String.compare (m1, m2),
345 fn () => join (String.compare (d1, d2),
346 fn () => String.compare (c1, c2)))
347
348 fun pCompare ((p1, _), (p2, _)) =
349 case (p1, p2) of
350 (PWild, PWild) => EQUAL
351 | (PWild, _) => LESS
352 | (_, PWild) => GREATER
353
354 | (PVar _, PVar _) => EQUAL
355 | (PVar _, _) => LESS
356 | (_, PVar _) => GREATER
357
358 | (PPrim p1, PPrim p2) => Prim.compare (p1, p2)
359 | (PPrim _, _) => LESS
360 | (_, PPrim _) => GREATER
361
362 | (PCon (_, pc1, _, po1), PCon (_, pc2, _, po2)) =>
363 join (pcCompare (pc1, pc2),
364 fn () => joinO pCompare (po1, po2))
365 | (PCon _, _) => LESS
366 | (_, PCon _) => GREATER
367
368 | (PRecord xps1, PRecord xps2) =>
369 joinL (fn ((x1, p1, _), (x2, p2, _)) =>
370 join (String.compare (x1, x2),
371 fn () => pCompare (p1, p2))) (xps1, xps2)
372
373 fun compare ((e1, _), (e2, _)) =
374 case (e1, e2) of
375 (EPrim p1, EPrim p2) => Prim.compare (p1, p2)
376 | (EPrim _, _) => LESS
377 | (_, EPrim _) => GREATER
378
379 | (ERel n1, ERel n2) => Int.compare (n1, n2)
380 | (ERel _, _) => LESS
381 | (_, ERel _) => GREATER
382
383 | (ENamed n1, ENamed n2) => Int.compare (n1, n2)
384 | (ENamed _, _) => LESS
385 | (_, ENamed _) => GREATER
386
387 | (ECon (_, pc1, _, eo1), ECon (_, pc2, _, eo2)) =>
388 join (pcCompare (pc1, pc2),
389 fn () => joinO compare (eo1, eo2))
390 | (ECon _, _) => LESS
391 | (_, ECon _) => GREATER
392
393 | (EFfi (f1, x1), EFfi (f2, x2)) =>
394 join (String.compare (f1, f2),
395 fn () => String.compare (x1, x2))
396 | (EFfi _, _) => LESS
397 | (_, EFfi _) => GREATER
398
399 | (EFfiApp (f1, x1, es1), EFfiApp (f2, x2, es2)) =>
400 join (String.compare (f1, f2),
401 fn () => join (String.compare (x1, x2),
402 fn () => joinL compare (es1, es2)))
403 | (EFfiApp _, _) => LESS
404 | (_, EFfiApp _) => GREATER
405
406 | (EApp (f1, x1), EApp (f2, x2)) =>
407 join (compare (f1, f2),
408 fn () => compare (x1, x2))
409 | (EApp _, _) => LESS
410 | (_, EApp _) => GREATER
411
412 | (EAbs (_, _, _, e1), EAbs (_, _, _, e2)) => compare (e1, e2)
413 | (EAbs _, _) => LESS
414 | (_, EAbs _) => GREATER
415
416 | (ECApp (f1, x1), ECApp (f2, x2)) =>
417 join (compare (f1, f2),
418 fn () => Con.compare (x1, x2))
419 | (ECApp _, _) => LESS
420 | (_, ECApp _) => GREATER
421
422 | (ECAbs (_, _, e1), ECAbs (_, _, e2)) => compare (e1, e2)
423 | (ECAbs _, _) => LESS
424 | (_, ECAbs _) => GREATER
425
426 | (ERecord xes1, ERecord xes2) =>
427 joinL (fn ((x1, e1, _), (x2, e2, _)) =>
428 join (Con.compare (x1, x2),
429 fn () => compare (e1, e2))) (xes1, xes2)
430 | (ERecord _, _) => LESS
431 | (_, ERecord _) => GREATER
432
433 | (EField (e1, c1, _), EField (e2, c2, _)) =>
434 join (compare (e1, e2),
435 fn () => Con.compare (c1, c2))
436 | (EField _, _) => LESS
437 | (_, EField _) => GREATER
438
439 | (EConcat (x1, _, y1, _), EConcat (x2, _, y2, _)) =>
440 join (compare (x1, x2),
441 fn () => compare (y1, y2))
442 | (EConcat _, _) => LESS
443 | (_, EConcat _) => GREATER
444
445 | (ECut (e1, c1, _), ECut (e2, c2, _)) =>
446 join (compare (e1, e2),
447 fn () => Con.compare (c1, c2))
448 | (ECut _, _) => LESS
449 | (_, ECut _) => GREATER
450
451 | (EFold _, EFold _) => EQUAL
452 | (EFold _, _) => LESS
453 | (_, EFold _) => GREATER
454
455 | (ECase (e1, pes1, _), ECase (e2, pes2, _)) =>
456 join (compare (e1, e2),
457 fn () => joinL (fn ((p1, e1), (p2, e2)) =>
458 join (pCompare (p1, p2),
459 fn () => compare (e1, e2))) (pes1, pes2))
460 | (ECase _, _) => LESS
461 | (_, ECase _) => GREATER
462
463 | (EWrite e1, EWrite e2) => compare (e1, e2)
464 | (EWrite _, _) => LESS
465 | (_, EWrite _) => GREATER
466
467 | (EClosure (n1, es1), EClosure (n2, es2)) =>
468 join (Int.compare (n1, n2),
469 fn () => joinL compare (es1, es2))
470 | (EClosure _, _) => LESS
471 | (_, EClosure _) => GREATER
472
473 | (ELet (_, _, x1, e1), ELet (_, _, x2, e2)) =>
474 join (compare (x1, x2),
475 fn () => compare (e1, e2))
333 476
334 datatype binder = 477 datatype binder =
335 RelC of string * kind 478 RelC of string * kind
336 | NamedC of string * int * kind * con option 479 | NamedC of string * int * kind * con option
337 | RelE of string * con 480 | RelE of string * con
580 exp = fn e => fn () => 723 exp = fn e => fn () =>
581 if exp e then 724 if exp e then
582 S.Return () 725 S.Return ()
583 else 726 else
584 S.Continue (e, ())} k () of 727 S.Continue (e, ())} k () of
728 S.Return _ => true
729 | S.Continue _ => false
730
731 fun existsB {kind, con, exp, bind} ctx k =
732 case mapfoldB {kind = fn k => fn () =>
733 if kind k then
734 S.Return ()
735 else
736 S.Continue (k, ()),
737 con = fn ctx => fn c => fn () =>
738 if con (ctx, c) then
739 S.Return ()
740 else
741 S.Continue (c, ()),
742 exp = fn ctx => fn e => fn () =>
743 if exp (ctx, e) then
744 S.Return ()
745 else
746 S.Continue (e, ()),
747 bind = bind} ctx k () of
585 S.Return _ => true 748 S.Return _ => true
586 | S.Continue _ => false 749 | S.Continue _ => false
587 750
588 fun foldMap {kind, con, exp} s e = 751 fun foldMap {kind, con, exp} s e =
589 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)), 752 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),