comparison src/core_util.sml @ 1848:e15234fbb163

Basis.tryRpc
author Adam Chlipala <adam@chlipala.net>
date Tue, 16 Apr 2013 10:55:48 -0400
parents 0577be31a435
children b90103106177
comparison
equal deleted inserted replaced
1847:8958b580d026 1848:e15234fbb163
1 (* Copyright (c) 2008-2010, Adam Chlipala 1 (* Copyright (c) 2008-2010, 2013, Adam Chlipala
2 * All rights reserved. 2 * All rights reserved.
3 * 3 *
4 * Redistribution and use in source and binary forms, with or without 4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met: 5 * modification, are permitted provided that the following conditions are met:
6 * 6 *
437 | (PRecord xps1, PRecord xps2) => 437 | (PRecord xps1, PRecord xps2) =>
438 joinL (fn ((x1, p1, _), (x2, p2, _)) => 438 joinL (fn ((x1, p1, _), (x2, p2, _)) =>
439 join (String.compare (x1, x2), 439 join (String.compare (x1, x2),
440 fn () => pCompare (p1, p2))) (xps1, xps2) 440 fn () => pCompare (p1, p2))) (xps1, xps2)
441 441
442 fun fmCompare (fm1, fm2) =
443 case (fm1, fm2) of
444 (None, None) => EQUAL
445 | (None, _) => LESS
446 | (_, None) => GREATER
447
448 | (Error, Error) => EQUAL
449
442 fun compare ((e1, _), (e2, _)) = 450 fun compare ((e1, _), (e2, _)) =
443 case (e1, e2) of 451 case (e1, e2) of
444 (EPrim p1, EPrim p2) => Prim.compare (p1, p2) 452 (EPrim p1, EPrim p2) => Prim.compare (p1, p2)
445 | (EPrim _, _) => LESS 453 | (EPrim _, _) => LESS
446 | (_, EPrim _) => GREATER 454 | (_, EPrim _) => GREATER
545 join (compare (x1, x2), 553 join (compare (x1, x2),
546 fn () => compare (e1, e2)) 554 fn () => compare (e1, e2))
547 | (ELet _, _) => LESS 555 | (ELet _, _) => LESS
548 | (_, ELet _) => GREATER 556 | (_, ELet _) => GREATER
549 557
550 | (EServerCall (n1, es1, _), EServerCall (n2, es2, _)) => 558 | (EServerCall (n1, es1, _, fm1), EServerCall (n2, es2, _, fm2)) =>
551 join (Int.compare (n1, n2), 559 join (Int.compare (n1, n2),
552 fn () => joinL compare (es1, es2)) 560 fn () => join (fmCompare (fm1, fm2),
561 fn () => joinL compare (es1, es2)))
553 | (EServerCall _, _) => LESS 562 | (EServerCall _, _) => LESS
554 | (_, EServerCall _) => GREATER 563 | (_, EServerCall _) => GREATER
555 564
556 | (EKAbs (_, e1), EKAbs (_, e2)) => compare (e1, e2) 565 | (EKAbs (_, e1), EKAbs (_, e2)) => compare (e1, e2)
557 | (EKAbs _, _) => LESS 566 | (EKAbs _, _) => LESS
736 fn e1' => 745 fn e1' =>
737 S.map2 (mfe (bind (ctx, RelE (x, t'))) e2, 746 S.map2 (mfe (bind (ctx, RelE (x, t'))) e2,
738 fn e2' => 747 fn e2' =>
739 (ELet (x, t', e1', e2'), loc)))) 748 (ELet (x, t', e1', e2'), loc))))
740 749
741 | EServerCall (n, es, t) => 750 | EServerCall (n, es, t, fm) =>
742 S.bind2 (ListUtil.mapfold (mfe ctx) es, 751 S.bind2 (ListUtil.mapfold (mfe ctx) es,
743 fn es' => 752 fn es' =>
744 S.map2 (mfc ctx t, 753 S.map2 (mfc ctx t,
745 fn t' => 754 fn t' =>
746 (EServerCall (n, es', t'), loc))) 755 (EServerCall (n, es', t', fm), loc)))
747 756
748 | EKAbs (x, e) => 757 | EKAbs (x, e) =>
749 S.map2 (mfe (bind (ctx, RelK x)) e, 758 S.map2 (mfe (bind (ctx, RelK x)) e,
750 fn e' => 759 fn e' =>
751 (EKAbs (x, e'), loc)) 760 (EKAbs (x, e'), loc))