diff --git a/examples/cancellableCall.aeff b/examples/cancellableCall.aeff index 92bb8a7..8750344 100644 --- a/examples/cancellableCall.aeff +++ b/examples/cancellableCall.aeff @@ -1,7 +1,7 @@ operation call : int * int operation result : int * int operation cancel : int -operation dummy : empty +operation impossible : empty let callWith callCounter = fun x -> @@ -19,10 +19,10 @@ let callWith callCounter = let remote f = promise (call (x, callNo) r -> spawn ( - promise (cancel callNo' dummyR when callNo = callNo' -> - let dummyPromise = promise (dummy empty -> return <>) in - await dummyPromise; - dummyR () + promise (cancel callNo' impossibleR when callNo = callNo' -> + let impossiblePromise = promise (impossible empty -> return <>) in + await impossiblePromise; + impossibleR () ); let y = (unbox f) x in send result (y, callNo) @@ -40,4 +40,4 @@ run result3 () run - remote [| fun x -> 4 * (5 * (6 * x)) |] \ No newline at end of file + remote [| fun x -> 4 * (5 * (6 * x)) |] diff --git a/examples/cancellableCallFunPayload.aeff b/examples/cancellableCallFunPayload.aeff index d3a11f4..0309e5b 100644 --- a/examples/cancellableCallFunPayload.aeff +++ b/examples/cancellableCallFunPayload.aeff @@ -1,11 +1,11 @@ operation call : [| unit -> unit |] operation result : int * int operation cancel : int -operation dummy : empty +operation impossible : empty let waitForCancel callNo = promise (cancel callNo' when callNo = callNo' -> - let p = promise (dummy empty -> return <<()>>) in + let p = promise (impossible empty -> return <<()>>) in await p; return <<()>> ) diff --git a/examples/handleFirstThreeInterrupts.aeff b/examples/handleFirstThreeInterrupts.aeff new file mode 100644 index 0000000..0b239e9 --- /dev/null +++ b/examples/handleFirstThreeInterrupts.aeff @@ -0,0 +1,18 @@ +operation request : int +operation response : int + +run + promise (request x r s -> + if s > 0 then + send response (x + 42); + r (s - 1) + else + return <<()>> + ) at 3 + +run + send request 1; + send request 2; + send request 3; + send request 4; + send request 5 diff --git a/src/webInterface/dune b/src/webInterface/dune index 1d9318e..7d693e5 100644 --- a/src/webInterface/dune +++ b/src/webInterface/dune @@ -51,4 +51,7 @@ (echo "({|Timer|}, {|") (cat ../../examples/ticktock.aeff) (echo "|});") + (echo "({|Handle only first n interrupts|}, {|") + (cat ../../examples/handleFirstThreeInterrupts.aeff) + (echo "|});") (echo "]")))) diff --git a/tests/run_tests.t b/tests/run_tests.t index 0595baf..41b32e6 100644 --- a/tests/run_tests.t +++ b/tests/run_tests.t @@ -395,7 +395,7 @@ operation call : int × int operation result : int × int operation cancel : int - operation dummy : empty + operation impossible : empty val callWith : int ref → int → (unit → int) × (unit → unit) × (int → unit) val remote : [(int → int)] → ⟨α⟩ @@ -410,7 +410,7 @@ ↑ call (240, 2) ↑ result (28800, 2) The process has terminated in the configuration: - run promise (dummy empty _ _ ↦ return ⟨empty⟩) + run promise (impossible empty _ _ ↦ return ⟨empty⟩) @ () as p in ↓result((28800, 2), ↓call((240, 2), @@ -421,7 +421,7 @@ await p until ⟨x⟩ in return x; (fun s' ↦ promise ( - cancel callNo' dummyR _ ↦ + cancel callNo' impossibleR _ ↦ let b = (=) ( @@ -430,77 +430,80 @@ match b with ( true ↦ let - dummyPromise = + impossiblePromise = promise ( - dummy empty _ _ ↦ + impossible empty _ _ ↦ return ⟨empty⟩) @ () as p in return p in await - dummyPromise until + impossiblePromise until ⟨x⟩ in return x; - dummyR () | + impossibleR + () | false ↦ - dummyR ())) + impossibleR + ())) @ s' as p' in return p') () in ↓cancel(0, return ())))))) || - run promise (cancel callNo' dummyR _ ↦ + run promise (cancel callNo' impossibleR _ ↦ let b = (=) (1, callNo') in - match b with (true ↦ let dummyPromise = - promise (dummy empty _ _ ↦ + match b with (true ↦ let impossiblePromise = + promise (impossible empty _ _ ↦ return ⟨empty⟩) @ () as p in return p in - await dummyPromise until ⟨x⟩ in - return x; dummyR () | false ↦ dummyR ())) + await impossiblePromise until ⟨x⟩ in + return x; impossibleR () | + false ↦ impossibleR ())) @ () as p' in return () || - run promise (dummy empty _ _ ↦ return ⟨empty⟩) + run promise (impossible empty _ _ ↦ return ⟨empty⟩) @ () as p in ↓result((28800, 2), ↓call((240, 2), let p = await p until ⟨x⟩ in return x; - (fun s' ↦ promise (cancel callNo' dummyR _ ↦ + (fun s' ↦ promise (cancel callNo' impossibleR _ ↦ let b = (=) (2, callNo') in match b with (true ↦ let - dummyPromise = + impossiblePromise = promise ( - dummy empty _ _ ↦ + impossible empty _ _ ↦ return ⟨empty⟩) @ () as p in return p in - await dummyPromise until + await impossiblePromise until ⟨x⟩ in return x; - dummyR () | + impossibleR () | false ↦ - dummyR ())) + impossibleR ())) @ s' as p' in return p') () in ↓cancel(2, return ()))) || run promise (call (x, callNo) r _ ↦ - Spawn (promise (cancel callNo' dummyR _ ↦ + Spawn (promise (cancel callNo' impossibleR _ ↦ let b = (=) (callNo, callNo') in - match b with (true ↦ let dummyPromise = - promise (dummy empty _ _ ↦ + match b with (true ↦ let impossiblePromise = + promise (impossible empty _ _ ↦ return ⟨empty⟩) @ () as p in return p in - await dummyPromise until + await impossiblePromise until ⟨x⟩ in return x; - dummyR () | - false ↦ dummyR ())) + impossibleR () | + false ↦ impossibleR ())) @ () as p in return p; let y = @@ -514,15 +517,16 @@ @ () as p' in return p' || - run promise (cancel callNo' dummyR _ ↦ + run promise (cancel callNo' impossibleR _ ↦ let b = (=) (2, callNo') in - match b with (true ↦ let dummyPromise = - promise (dummy empty _ _ ↦ + match b with (true ↦ let impossiblePromise = + promise (impossible empty _ _ ↦ return ⟨empty⟩) @ () as p in return p in - await dummyPromise until ⟨x⟩ in - return x; dummyR () | false ↦ dummyR ())) + await impossiblePromise until ⟨x⟩ in + return x; impossibleR () | + false ↦ impossibleR ())) @ () as p in return () || @@ -587,7 +591,7 @@ operation call : [(unit → unit)] operation result : int × int operation cancel : int - operation dummy : empty + operation impossible : empty val waitForCancel : int → ⟨unit⟩ val remoteCall : int ref → [(unit → int)] → (unit → int) × (unit → unit) @@ -609,7 +613,7 @@ let res = g () in ↑result((res, 2), return ())] ↑ result (504, 2) The process has terminated in the configuration: - run promise (dummy empty _ _ ↦ return ⟨()⟩) + run promise (impossible empty _ _ ↦ return ⟨()⟩) @ () as p in ↓result((504, 2), ↓call([fun _ ↦ waitForCancel 2; @@ -632,7 +636,7 @@ run promise (cancel callNo' r _ ↦ let b = (=) (2, callNo') in match b with (true ↦ let p = - promise (dummy empty _ _ ↦ + promise (impossible empty _ _ ↦ return ⟨()⟩) @ () as p in return p in @@ -644,7 +648,7 @@ run promise (cancel callNo' r _ ↦ let b = (=) (0, callNo') in match b with (true ↦ let p = - promise (dummy empty _ _ ↦ + promise (impossible empty _ _ ↦ return ⟨()⟩) @ () as p in return p in @@ -884,6 +888,75 @@ @ () as p' in return p' ====================================================================== + ../examples/handleFirstThreeInterrupts.aeff + ====================================================================== + val (=) : α × α → bool + val (<) : α × α → bool + val (>) : α × α → bool + val (<=) : α × α → bool + val (>=) : α × α → bool + val (<>) : α × α → bool + val (~-) : int → int + val (+) : int × int → int + val (*) : int × int → int + val (-) : int × int → int + val (mod) : int × int → int + val (/) : int × int → int + val ref : α → α ref + val (!) : α ref → α + val (:=) : α ref × α → unit + val toString : α → string + val absurd : α → β + val not : bool → bool + type option + val assoc : α → (α × β) list → β option + val range : int → int → int list + val reverse : α list → α list + val map : (α → β) → α list → β list + val hd : α list → α + val tl : α list → α list + val take : (int → α) → int → α list + val foldLeft : (α → β → α) → α → β list → α + val foldRight : (α → β → β) → α list → β → β + val iter : (α → β) → α list → unit + val forall : (α → bool) → α list → bool + val exists : (α → bool) → α list → bool + val mem : α → α list → bool + val filter : (α → bool) → α list → α list + val complement : α list → α list → α list + val intersection : α list → α list → α list + val zip : α list → β list → (α × β) list + val unzip : (α × β) list → α list × β list + val (@) : α list × α list → α list + val length : α list → int + val nth : α list → int → α + val abs : int → int + val min : α → α → α + val max : α → α → α + val gcd : int → int → int + val lcm : int → int → int + val odd : int → bool + val even : int → bool + val id : α → α + val compose : (α → β) → (γ → α) → γ → β + val (|>) : α → (α → β) → β + val ignore : α → unit + val fst : α × β → α + val snd : α × β → β + val return : α → α + operation request : int + operation response : int + ↑ request 1 + ↑ request 2 + ↑ request 3 + ↑ request 4 + ↑ request 5 + ↑ response 43 + ↑ response 44 + ↑ response 45 + The process has terminated in the configuration: + run (return ()) || run (return ⟨()⟩) + ====================================================================== ../examples/heapPure.aeff ====================================================================== val (=) : α × α → bool