|
395 | 395 | operation call : int × int
|
396 | 396 | operation result : int × int
|
397 | 397 | operation cancel : int
|
398 |
| - operation dummy : empty |
| 398 | + operation impossible : empty |
399 | 399 | val callWith : int ref → int → (unit → int) × (unit → unit) ×
|
400 | 400 | (int → unit)
|
401 | 401 | val remote : [(int → int)] → ⟨α⟩
|
|
410 | 410 | ↑ call (240, 2)
|
411 | 411 | ↑ result (28800, 2)
|
412 | 412 | The process has terminated in the configuration:
|
413 |
| - run promise (dummy empty _ _ ↦ return ⟨empty⟩) |
| 413 | + run promise (impossible empty _ _ ↦ return ⟨empty⟩) |
414 | 414 | @ () as p in
|
415 | 415 | ↓result((28800, 2),
|
416 | 416 | ↓call((240, 2),
|
|
421 | 421 | await p until ⟨x⟩ in
|
422 | 422 | return x;
|
423 | 423 | (fun s' ↦ promise (
|
424 |
| - cancel callNo' dummyR _ ↦ |
| 424 | + cancel callNo' impossibleR _ ↦ |
425 | 425 | let b =
|
426 | 426 | (=)
|
427 | 427 | (
|
|
430 | 430 | match b with (
|
431 | 431 | true ↦
|
432 | 432 | let
|
433 |
| - dummyPromise = |
| 433 | + impossiblePromise = |
434 | 434 | promise (
|
435 |
| - dummy empty _ _ ↦ |
| 435 | + impossible empty _ _ ↦ |
436 | 436 | return
|
437 | 437 | ⟨empty⟩)
|
438 | 438 | @ () as p in
|
439 | 439 | return p in
|
440 | 440 | await
|
441 |
| - dummyPromise until |
| 441 | + impossiblePromise until |
442 | 442 | ⟨x⟩ in
|
443 | 443 | return x;
|
444 |
| - dummyR () | |
| 444 | + impossibleR |
| 445 | + () | |
445 | 446 | false ↦
|
446 |
| - dummyR ())) |
| 447 | + impossibleR |
| 448 | + ())) |
447 | 449 | @ s' as p' in
|
448 | 450 | return p')
|
449 | 451 | () in
|
450 | 452 | ↓cancel(0, return ()))))))
|
451 | 453 | ||
|
452 |
| - run promise (cancel callNo' dummyR _ ↦ |
| 454 | + run promise (cancel callNo' impossibleR _ ↦ |
453 | 455 | let b = (=) (1, callNo') in
|
454 |
| - match b with (true ↦ let dummyPromise = |
455 |
| - promise (dummy empty _ _ ↦ |
| 456 | + match b with (true ↦ let impossiblePromise = |
| 457 | + promise (impossible empty _ _ ↦ |
456 | 458 | return ⟨empty⟩)
|
457 | 459 | @ () as p in
|
458 | 460 | return p in
|
459 |
| - await dummyPromise until ⟨x⟩ in |
460 |
| - return x; dummyR () | false ↦ dummyR ())) |
| 461 | + await impossiblePromise until ⟨x⟩ in |
| 462 | + return x; impossibleR () | |
| 463 | + false ↦ impossibleR ())) |
461 | 464 | @ () as p' in
|
462 | 465 | return ()
|
463 | 466 | ||
|
464 |
| - run promise (dummy empty _ _ ↦ return ⟨empty⟩) |
| 467 | + run promise (impossible empty _ _ ↦ return ⟨empty⟩) |
465 | 468 | @ () as p in
|
466 | 469 | ↓result((28800, 2),
|
467 | 470 | ↓call((240, 2),
|
468 | 471 | let p =
|
469 | 472 | await p until ⟨x⟩ in return x;
|
470 |
| - (fun s' ↦ promise (cancel callNo' dummyR _ ↦ |
| 473 | + (fun s' ↦ promise (cancel callNo' impossibleR _ ↦ |
471 | 474 | let b = (=) (2, callNo') in
|
472 | 475 | match b with (true ↦
|
473 | 476 | let
|
474 |
| - dummyPromise = |
| 477 | + impossiblePromise = |
475 | 478 | promise (
|
476 |
| - dummy empty _ _ ↦ |
| 479 | + impossible empty _ _ ↦ |
477 | 480 | return
|
478 | 481 | ⟨empty⟩)
|
479 | 482 | @ () as p in
|
480 | 483 | return p in
|
481 |
| - await dummyPromise until |
| 484 | + await impossiblePromise until |
482 | 485 | ⟨x⟩ in
|
483 | 486 | return x;
|
484 |
| - dummyR () | |
| 487 | + impossibleR () | |
485 | 488 | false ↦
|
486 |
| - dummyR ())) |
| 489 | + impossibleR ())) |
487 | 490 | @ s' as p' in
|
488 | 491 | return p')
|
489 | 492 | () in ↓cancel(2, return ())))
|
490 | 493 | ||
|
491 | 494 | run promise (call (x, callNo) r _ ↦
|
492 |
| - Spawn (promise (cancel callNo' dummyR _ ↦ |
| 495 | + Spawn (promise (cancel callNo' impossibleR _ ↦ |
493 | 496 | let b = (=) (callNo, callNo') in
|
494 |
| - match b with (true ↦ let dummyPromise = |
495 |
| - promise (dummy empty _ _ ↦ |
| 497 | + match b with (true ↦ let impossiblePromise = |
| 498 | + promise (impossible empty _ _ ↦ |
496 | 499 | return
|
497 | 500 | ⟨empty⟩)
|
498 | 501 | @ () as p in
|
499 | 502 | return p in
|
500 |
| - await dummyPromise until |
| 503 | + await impossiblePromise until |
501 | 504 | ⟨x⟩ in return x;
|
502 |
| - dummyR () | |
503 |
| - false ↦ dummyR ())) |
| 505 | + impossibleR () | |
| 506 | + false ↦ impossibleR ())) |
504 | 507 | @ () as p in
|
505 | 508 | return p;
|
506 | 509 | let y =
|
|
514 | 517 | @ () as p' in
|
515 | 518 | return p'
|
516 | 519 | ||
|
517 |
| - run promise (cancel callNo' dummyR _ ↦ |
| 520 | + run promise (cancel callNo' impossibleR _ ↦ |
518 | 521 | let b = (=) (2, callNo') in
|
519 |
| - match b with (true ↦ let dummyPromise = |
520 |
| - promise (dummy empty _ _ ↦ |
| 522 | + match b with (true ↦ let impossiblePromise = |
| 523 | + promise (impossible empty _ _ ↦ |
521 | 524 | return ⟨empty⟩)
|
522 | 525 | @ () as p in
|
523 | 526 | return p in
|
524 |
| - await dummyPromise until ⟨x⟩ in |
525 |
| - return x; dummyR () | false ↦ dummyR ())) |
| 527 | + await impossiblePromise until ⟨x⟩ in |
| 528 | + return x; impossibleR () | |
| 529 | + false ↦ impossibleR ())) |
526 | 530 | @ () as p in
|
527 | 531 | return ()
|
528 | 532 | ||
|
|
587 | 591 | operation call : [(unit → unit)]
|
588 | 592 | operation result : int × int
|
589 | 593 | operation cancel : int
|
590 |
| - operation dummy : empty |
| 594 | + operation impossible : empty |
591 | 595 | val waitForCancel : int → ⟨unit⟩
|
592 | 596 | val remoteCall : int ref → [(unit → int)] → (unit → int) ×
|
593 | 597 | (unit → unit)
|
|
609 | 613 | let res = g () in ↑result((res, 2), return ())]
|
610 | 614 | ↑ result (504, 2)
|
611 | 615 | The process has terminated in the configuration:
|
612 |
| - run promise (dummy empty _ _ ↦ return ⟨()⟩) |
| 616 | + run promise (impossible empty _ _ ↦ return ⟨()⟩) |
613 | 617 | @ () as p in
|
614 | 618 | ↓result((504, 2),
|
615 | 619 | ↓call([fun _ ↦ waitForCancel 2;
|
|
632 | 636 | run promise (cancel callNo' r _ ↦
|
633 | 637 | let b = (=) (2, callNo') in
|
634 | 638 | match b with (true ↦ let p =
|
635 |
| - promise (dummy empty _ _ ↦ |
| 639 | + promise (impossible empty _ _ ↦ |
636 | 640 | return ⟨()⟩)
|
637 | 641 | @ () as p in
|
638 | 642 | return p in
|
|
644 | 648 | run promise (cancel callNo' r _ ↦
|
645 | 649 | let b = (=) (0, callNo') in
|
646 | 650 | match b with (true ↦ let p =
|
647 |
| - promise (dummy empty _ _ ↦ |
| 651 | + promise (impossible empty _ _ ↦ |
648 | 652 | return ⟨()⟩)
|
649 | 653 | @ () as p in
|
650 | 654 | return p in
|
|
884 | 888 | @ () as p' in
|
885 | 889 | return p'
|
886 | 890 | ======================================================================
|
| 891 | + ../examples/handleFirstThreeInterrupts.aeff |
| 892 | + ====================================================================== |
| 893 | + val (=) : α × α → bool |
| 894 | + val (<) : α × α → bool |
| 895 | + val (>) : α × α → bool |
| 896 | + val (<=) : α × α → bool |
| 897 | + val (>=) : α × α → bool |
| 898 | + val (<>) : α × α → bool |
| 899 | + val (~-) : int → int |
| 900 | + val (+) : int × int → int |
| 901 | + val (*) : int × int → int |
| 902 | + val (-) : int × int → int |
| 903 | + val (mod) : int × int → int |
| 904 | + val (/) : int × int → int |
| 905 | + val ref : α → α ref |
| 906 | + val (!) : α ref → α |
| 907 | + val (:=) : α ref × α → unit |
| 908 | + val toString : α → string |
| 909 | + val absurd : α → β |
| 910 | + val not : bool → bool |
| 911 | + type option |
| 912 | + val assoc : α → (α × β) list → β option |
| 913 | + val range : int → int → int list |
| 914 | + val reverse : α list → α list |
| 915 | + val map : (α → β) → α list → β list |
| 916 | + val hd : α list → α |
| 917 | + val tl : α list → α list |
| 918 | + val take : (int → α) → int → α list |
| 919 | + val foldLeft : (α → β → α) → α → β list → α |
| 920 | + val foldRight : (α → β → β) → α list → β → β |
| 921 | + val iter : (α → β) → α list → unit |
| 922 | + val forall : (α → bool) → α list → bool |
| 923 | + val exists : (α → bool) → α list → bool |
| 924 | + val mem : α → α list → bool |
| 925 | + val filter : (α → bool) → α list → α list |
| 926 | + val complement : α list → α list → α list |
| 927 | + val intersection : α list → α list → α list |
| 928 | + val zip : α list → β list → (α × β) list |
| 929 | + val unzip : (α × β) list → α list × β list |
| 930 | + val (@) : α list × α list → α list |
| 931 | + val length : α list → int |
| 932 | + val nth : α list → int → α |
| 933 | + val abs : int → int |
| 934 | + val min : α → α → α |
| 935 | + val max : α → α → α |
| 936 | + val gcd : int → int → int |
| 937 | + val lcm : int → int → int |
| 938 | + val odd : int → bool |
| 939 | + val even : int → bool |
| 940 | + val id : α → α |
| 941 | + val compose : (α → β) → (γ → α) → γ → β |
| 942 | + val (|>) : α → (α → β) → β |
| 943 | + val ignore : α → unit |
| 944 | + val fst : α × β → α |
| 945 | + val snd : α × β → β |
| 946 | + val return : α → α |
| 947 | + operation request : int |
| 948 | + operation response : int |
| 949 | + ↑ request 1 |
| 950 | + ↑ request 2 |
| 951 | + ↑ request 3 |
| 952 | + ↑ request 4 |
| 953 | + ↑ request 5 |
| 954 | + ↑ response 43 |
| 955 | + ↑ response 44 |
| 956 | + ↑ response 45 |
| 957 | + The process has terminated in the configuration: |
| 958 | + run (return ()) || run (return ⟨()⟩) |
| 959 | + ====================================================================== |
887 | 960 | ../examples/heapPure.aeff
|
888 | 961 | ======================================================================
|
889 | 962 | val (=) : α × α → bool
|
|
0 commit comments