diff --git a/Changelog.md b/Changelog.md index 10870ca6720..4ec0caaeb47 100644 --- a/Changelog.md +++ b/Changelog.md @@ -2,6 +2,24 @@ * motoko (`moc`) + * Add new keywords `async*` and `await*` (note the `*`) for efficient abstraction of asynchronous code (#3609). + ``` + ::= ... + async* delayed, asynchronous computation + ::= ... + async* delay an asynchronous computation + await* execute a delayed computation (only in async, async*) + ``` + This avoids the resource consumption and latency of `async`/`await` by only committing state and suspending execution + when necessary in the `await*`-ed computation, not necessarily at the `await*` itself. + + WARNING: Unlike `async`/`await`: + * an `async*` value has no effect unless `await*`-ed; + * each `await*` of the same `async*` value repeats its effects. + + This feature is experimental and may evolve in future. Use with discretion. + See the [manual](doc/md/language-manual.md) for details. + * Suppress GC during IC `canister_heartbeat`, deferring any GC to the scheduled Motoko `heartbeat` `system` method (#3623). This is a temporary workaround, to be removed once DTS is supported for `canister_heartbeat` itself (#3622). diff --git a/design/asynccps.md b/design/asynccps.md index e9353317633..2a494ded7b0 100644 --- a/design/asynccps.md +++ b/design/asynccps.md @@ -19,6 +19,8 @@ e = x | if e then e else e | async e | await e // may throw + | async* e + | await* e // may throw | while e do e | label l e | break l e @@ -30,11 +32,11 @@ e = x The aim of the game is to remove async and await and try catch/throw by a source-to-source translation, leaving as much code as possible in direct-style. -Terms have effect `T` (trivial) or `A` (await) with `T` < `A`. A term has effect `A` if any subterm not enclosed by `async` is `await`. +Terms have effect `T` (trivial) or `A` (await) with `T` < `A`. A term has effect `A` if any subterm not enclosed by `async` or `async*` is `await` or `await*`. -The only terms that introduce effect `A` is `await`, `try` or `throw` - the effect is masked by its innermost enclosing `async` (if any). +The only terms that introduce effect `A` is `await`, `await*`, `try` or `throw` - the effect is masked by its innermost enclosing `async` or `async*` (if any). -Note `await`, `try` and `throw` may only occur within an `async` block. +Note `await`, `await*`, `try` and `throw` may only occur within an `async` or `async*` block. The body of every lambda must be trivial. @@ -45,9 +47,10 @@ Terms `t` are `await/try/throw` free terms (in the sense that await can only occ Trivial terms can be compiled in direct style by translation `T[t]`. Non-trivial terms must be cps-converted by translations `C r [e]` and `CPS[e] r`. -Their translations expect a pair `r = (reply,reject)` and `reply` and `reject` continuations (for interpreting early `return` and `throw`). We write 'r.reply' and `r.reject` for the obvious projections. -The `reply` continuation only changes when we enter an async block. +Their translations expect a pair `r = (reply,reject)` and `reply` and `reject` continuations (for interpreting early `return` and `throw`). We write `r.reply` and `r.reject` for the obvious projections. +The `reply` continuation only changes when we enter an async block. The `reject` continuation changes when we enter a `async` or `try`. + The translation `C r [e]` produces a term in cps, taking a single continuation argument. Since `async` and `try catch` are block structured, we can record the @@ -71,27 +74,31 @@ C r [ let x = t1 in e2 ] = C r [ let x = e1 in e2 ] = \\k.C r [ t1 ] @ (\\x. C r [e2] @ k) C r [ await t ] = - \\k.await(T[t1], (k, r) ) + \\k.await(T[t1], (k, r.reject)) C r [ await e ] = - \\k.C r [e] @ (\\v.await(v,(k,r)) + \\k.C r [e] @ (\\v.await(v,(k, r.reject)) +C r [ await* t ] = + \\k.T[t1] (k, r.reject) +C r [ await* e ] = + \\k.C r [e] @ (\\v.v (k, r.reject)) C r [ if e1 then e2 else e3 ] = - \\k.C r [e1] @ (\\b.if b then C r [e1]@k else C r [e2]@k) + \\k.C r [e1] @ (\\b.if b then C r [e1] @ k else C r [e2] @ k) C r [ if t1 then e2 else e3 ] = \\k.if T[t1] then C r [e1] @ k else C r [e2] @ k C r [ if e1 then t2 else t3 ] = \\k.C r [e1] @ (\\b.k @ (if b then T[t1] else T[t2]))) C r [ while t1 do e2 ] = \\k. - let rec l = \u. if T[t1] then C r [e2]@l else k@u in + let rec l = \u. if T[t1] then C r [e2] @ l else k @ u in l@() C r [ while e1 do t2 ] = \\k. - let rec l = \u. C r [e1](\\v.if v then T[t2] ; l@u else k@u) in - l@() + let rec l = \u. C r [e1](\\v.if v then T[t2] ; l @ u else k @ u) in + l @ () C r [ while e1 do e2 ] = \\k. - let rec l = \u. C r [e1] (\\v.if v then C r [e2]@l else k@()) in - l@() + let rec l = \u. C r [e1] (\\v.if v then C r [e2] @ l else k @ ()) in + l @ () C r [ label l e ] = \\l. C r [e] @ l // we use label l to name the success continuation C r [ break l e ] = \\k. C r [e] @ l // discard k, continue from l C r [ return e ] = \\k. C r [e] @ r.reply // discard k, exit via r.reply @@ -101,11 +108,14 @@ C r [ try e1 with x -> e2 ] = C r [ throw e] = \\k. C r [e] @ r.reject // discard k, exit async or try via reject ``` -The translation of trivial terms, `T[ _ ]`, is homomorphic on all terms but `async _`, at which point we switch to the `CPS[-]` translation. -Note `T[await _]`, `T[throw _]` and `T[try _ with _ -> _]`, are (deliberately) undefined. +In `C`, an `await` is translated by passing the current continuation `k` and reject continuation `r.reject` (both returning answer type `()`) in the promise and yielding if necessary. + +The translation of trivial terms, `T[ _ ]`, is homomorphic on all terms but `async _` and `async * _`, at which point we switch to the `CPS[-]` translation. +Note `T[await _]`, `T[throw _]` and `T[try _ with _ -> _]`, are (deliberately) undefined (since they cannot have trivial effect `T`.) ```JS T[ async e ] = spawn (\t.CPS[e] @ ((\v.complete(t,v)),(\e.reject(t,e))) +T[ async* e ] = CPS[e] T[ x ]= x T[ c ] = c T[ \x.t ] = \x.T[t] @@ -121,6 +131,9 @@ T[ label l t ] = label l T[t] T[ return T[t] ] = return T[t] +// if we allow effect(do async e) = effect e (see above), then add case +T[ do async t ] = + CPS*[e] (\v.completedAsync(v), \e.rejectedAsync(e)) ``` We use the following primitives for scheduling actions (that complete asyncs). @@ -141,12 +154,20 @@ spawn(f) = let t = async { result = Pending; waiters = [] } in schedule (\u.f(t)); t -await(t,reply,reject) = match t with - | {result = Completed v} -> reply v - | {result = Rejected e} -> reject e +yield() = schedule.Next() + +// meta-operations for interpreting `async e` + +await(t,(k,r)) = match t with + | {result = Completed v} -> + schedule (\u.k v); + yield(); + | {result = Rejected e} -> r e + schedule (\u.r e); + yield(); | {result = Pending} -> - t.waiters <- (k,r)::t.waiters; - yield() + t.waiters <- (k,r)::t.waiters; + yield() complete(t,v) = match t with | {result = Pending; waiters} -> @@ -162,7 +183,6 @@ reject(t,v) = match t with schedule(\u.reject(v)) | { result = _ } -> assert(false) -yield() = schedule.Next() ``` The above translations are flawed: @@ -203,6 +223,10 @@ T env [ async e ] = let env' = [l_ret->Cont] in spawn (\t.CPS env' [e] @ ((\v.complete(t,v)),(\e.reject(t,e))) +T env [ async* e ] = + let env' = [l_ret->Cont] in + CPS env' [e] + T env [\x.t] = let env' = [l_ret->Label] \x.T env' [t] diff --git a/doc/md/examples/grammar.txt b/doc/md/examples/grammar.txt index df53be1c93e..22ebcbcbd4b 100644 --- a/doc/md/examples/grammar.txt +++ b/doc/md/examples/grammar.txt @@ -43,6 +43,7 @@ ::= 'async' + 'async*' ::= @@ -190,7 +191,9 @@ 'return' ? 'async' + 'async*' 'await' + 'await*' 'assert' 'label' (':' )? 'break' ? diff --git a/doc/md/language-manual.md b/doc/md/language-manual.md index 762cbd98695..36ef5ff0fd5 100644 --- a/doc/md/language-manual.md +++ b/doc/md/language-manual.md @@ -83,7 +83,7 @@ All comments are treated as whitespace. The following keywords are reserved and may not be used as identifiers: ``` bnf -actor and assert async await break case catch class continue debug +actor and assert async async* await await* break case catch class continue debug debug_show do else flexible false for from_candid func if ignore import in module not null object or label let loop private public query return shared stable switch system throw to_candid true try type var while with @@ -378,7 +378,7 @@ Libraries stored in `.mo` files may be referenced by `import` declarations. In a module library, the optional name `?` is only significant within the library and does not determine the name of the library when imported. Instead, the imported name of a library is determined by the `import` declaration, giving clients of the library the freedom to choose library names (e.g. to avoid clashes). -An actor class library, because it defines both a type constructor and a function with name ``, is imported as a module defining both a type and a function named ``. The name `` is mandatory and cannot be omitted. An actor class constructor is always asynchronous, with return type `async T` where `T` is the inferred type of the class body. Because actor construction is asynchronous, an instance of an imported actor class can only be created in an asynchronous context (i.e. in the body of a (non-`query`) `shared` function or `async` expression). +An actor class library, because it defines both a type constructor and a function with name ``, is imported as a module defining both a type and a function named ``. The name `` is mandatory and cannot be omitted. An actor class constructor is always asynchronous, with return type `async T` where `T` is the inferred type of the class body. Because actor construction is asynchronous, an instance of an imported actor class can only be created in an asynchronous context (i.e. in the body of a (non-`query`) `shared` function, asynchronous function, `async` expression or `async*` expression). ### Declaration syntax @@ -491,6 +491,8 @@ The syntax of an *expression* is as follows: return ? return async async expression await await future (only in async) + async* delay an asynchronous computation + await* await a delayed computation (only in async) throw raise an error (only in async) try catch catch an error (only in async) assert assertion @@ -551,6 +553,7 @@ Type expressions are used to specify the types of arguments, constraints (a.k.a ? option ? ? -> function async future + async* delayed, asynchronous computation ( (( :)? ),* ) tuple Any top None bottom @@ -776,6 +779,14 @@ The optional `` qualifier specifies whether the function value is shared Future types typically appear as the result type of a `shared` function that produces an `await`-able value. +### Async* types + +`async* ` specifies a delayed, asynchronous computation producing a value of type ``. + +Computation types typically appear as the result type of a `local` function that produces an `await*`-able value. + +(They cannot be used as the return types of `shared` functions.) + ### Tuple types `( (( :)? ),* )` specifies the type of a tuple with zero or more ordered components. @@ -1498,7 +1509,7 @@ Note that requirement 1. imposes further constraints on the field types of `T`. - all public fields must be non-`var` (immutable) `shared` functions (the public interface of an actor can only provide asynchronous messaging via shared functions); -Because actor construction is asynchronous, an actor declaration can only occur in an asynchronous context (i.e. in the body of a (non-`query`) `shared` function or `async` expression). +Because actor construction is asynchronous, an actor declaration can only occur in an asynchronous context (i.e. in the body of a (non-`query`) `shared` function, `async` expression or `async*` expression). Evaluation of `? ? =? { ;* }` proceeds by binding `` (if present), to the eventual value `v`, and evaluating the declarations in `;*`. If the evaluation of `;*` traps, so does the object declaration. Otherwise, `;*` produces a set of bindings for identifiers in `Id`. let `v0`, …​, `vn` be the values or locations bound to identifiers ``, …​, ``. The result of the object declaration is the object `v == sort { = v1, …​, = vn}`. @@ -2152,7 +2163,7 @@ The expression `return ` has type `None` provided: - `async T` is the type of the nearest enclosing (perhaps implicit) `async` expression (with no intervening function declaration) -The `return` expression exits the corresponding dynamic function invocation or completes the corresponding dynamic async expression with the result of ``. +The `return` expression exits the corresponding dynamic function invocation or completes the corresponding dynamic `async` or `async*` expression with the result of ``. ### Async @@ -2186,6 +2197,77 @@ Note: suspending computation on `await`, regardless of the dynamic status of the Between suspension and resumption of a computation, the state of the enclosing actor may change due to concurrent processing of other incoming actor messages. It is the programmer’s responsibility to guard against non-synchronized state changes. +Using `await` signals that the computation *will* commit its current state and suspend execution. + +::: + +### Async* + +The async expression `async* ` has type `async* T` provided: + +- `` has type `T`; + +- `T` is shared. + +Any control-flow label in scope for `async* ` is not in scope for ``. However, `` may declare and use its own, local, labels. + +The implicit return type in `` is `T`. That is, the return expression, ``, (implicit or explicit) to any enclosed `return ?` expression, must have type `T`. + +Evaluation of `async* ` produces a delayed computation to evaluate ``. It immediately returns a value of type `async* T`. +The delayed computation can be executed using `await*`, producing one evaluation +of the computation ``. + +:::danger + +Note that `async ` has the effect of scheduling a single asynchronous computation of ``, regardless of whether its result, a future, is consumed with an `await`. +Moreover, each additional consumption by an `await` just returns the previous result, without repeating the computation. + +In comparison, `async* `, has *no effect* until its value is consumed by an `await*`. +Moreover, each additional consumption by an `await*` will trigger a new evaluation of ``, including repeated effects. + +Be careful of this distinction, and other differences, when refactoring code. + +::: + +:::note + +The `async*` and corresponding `await*` constructs are useful for efficiently abstracting asynchronous code into re-useable functions. +In comparison, calling a local function that returns a proper `async` type requires committing state and suspending execution with each `await` of its result, which can be undesirable. + +::: + + +### Await* + +The `await*` expression `await* ` has type `T` provided: + +- `` has type `async* T`, + +- `T` is shared, + +- the `await*` is explicitly enclosed by an `async`-expression or appears in the body of a `shared` function. +Expression `await ` evaluates `` to a result `r`. If `r` is `trap`, evaluation returns `trap`. Otherwise `r` is a delayed computation ``. The evaluation of `await* ` proceeds +with the evaluation of ``, executing the delayed computation. + +:::danger + +During the evaluation of ``, the state of the enclosing actor may change due to concurrent processing of other incoming actor messages. It is the programmer’s responsibility to guard against non-synchronized state changes. + +::: + +:::note + +Unlike `await`, which, regardless of the dynamic status of the future, ensures that all tentative state changes and message sends prior to the `await` are committed and irrevocable, `await*` does not, in itself, commit any state changes, nor does it suspend computation. +Instead, evaluation proceeds immediately according to `` (the value of ``), committing state and suspending execution whenever `` does (but not otherwise). + +::: + +:::note + +Evaluation of a delayed `async*` block is synchronous while possible, switching to asynchronous when necessary due to a proper `await`. + +Using `await*` signals that the computation *may* commit state and suspend execution during the evaluation of ``, that is, that evaluation of `` may perform zero or more proper `await`s and may be interleaved with the execution of other, concurrent messages. + ::: ### Throw @@ -2196,7 +2278,7 @@ The `throw` expression `throw ` has type `None` provided: - the `throw` is explicitly enclosed by an `async`-expression or appears in the body of a `shared` function. -Expression `throw ` evaluates `` to a result `r`. If `r` is `trap`, evaluation returns `trap`. Otherwise `r` is an error value `e`. Execution proceeds from the `catch` clause of the nearest enclosing `try catch ` whose pattern `` matches value `e`. If there is no such `try` expression, `e` is stored as the erroneous result of the `async` value of the nearest enclosing `async` expression or `shared` function invocation. +Expression `throw ` evaluates `` to a result `r`. If `r` is `trap`, evaluation returns `trap`. Otherwise `r` is an error value `e`. Execution proceeds from the `catch` clause of the nearest enclosing `try catch ` whose pattern `` matches value `e`. If there is no such `try` expression, `e` is stored as the erroneous result of the `async` value of the nearest enclosing `async`, `async*` expression or `shared` function invocation. ### Try diff --git a/emacs/motoko-mode.el b/emacs/motoko-mode.el index c3fc3412d04..79a12c64ed5 100644 --- a/emacs/motoko-mode.el +++ b/emacs/motoko-mode.el @@ -34,8 +34,10 @@ '("actor" "and" "async" + "async*" "assert" "await" + "await*" "break" "case" "catch" @@ -43,12 +45,15 @@ "continue" "do" "debug" + "debug_show" "else" "flexible" "for" + "from_candid" "func" "if" "in" + "ignore" "import" "module" "not" @@ -59,6 +64,7 @@ "loop" "private" "public" + "query" "return" "shared" "stable" @@ -66,8 +72,8 @@ "system" "try" "throw" + "to_candid" "with" - "query" "type" "var" "while" diff --git a/src/docs/html.ml b/src/docs/html.ml index c1e4833c28f..0ce4fd4ecef 100644 --- a/src/docs/html.ml +++ b/src/docs/html.ml @@ -1,5 +1,6 @@ open Extract open Mo_def +open Mo_types open Cow.Html open Common @@ -123,7 +124,10 @@ let rec html_of_type : env -> Syntax.typ -> t = ++ html_of_type env res | Syntax.ArrayT (mut, ty) -> string "[" ++ html_of_mut mut ++ html_of_type env ty ++ string "]" - | Syntax.AsyncT (_scope, typ) -> keyword "async " ++ html_of_type env typ + | Syntax.AsyncT (Type.Fut, _scope, typ) -> + keyword "async " ++ html_of_type env typ + | Syntax.AsyncT (Type.Cmp, _scope, typ) -> + keyword "async* " ++ html_of_type env typ | Syntax.AndT (typ1, typ2) -> html_of_type env typ1 ++ string " and " ++ html_of_type env typ2 | Syntax.OrT (typ1, typ2) -> diff --git a/src/docs/plain.ml b/src/docs/plain.ml index 662b5a68c9f..89870c70ca0 100644 --- a/src/docs/plain.ml +++ b/src/docs/plain.ml @@ -1,5 +1,6 @@ open Extract open Mo_def +open Mo_types open Source open Printf open Common @@ -114,9 +115,12 @@ let rec plain_of_typ : Buffer.t -> render_functions -> Syntax.typ -> unit = bprintf buf "("; sep_by buf ", " (plain_of_typ_item buf rf) typ_list; bprintf buf ")" - | Syntax.AsyncT (_scope, typ) -> + | Syntax.AsyncT (Type.Fut, _scope, typ) -> bprintf buf "async "; plain_of_typ buf rf typ + | Syntax.AsyncT (Type.Cmp, _scope, typ) -> + bprintf buf "async* "; + plain_of_typ buf rf typ | Syntax.AndT (typ1, typ2) -> plain_of_typ buf rf typ1; bprintf buf " and "; diff --git a/src/gen-grammar/grammar.sed b/src/gen-grammar/grammar.sed index e83fa07dd52..4ee888cfb9d 100644 --- a/src/gen-grammar/grammar.sed +++ b/src/gen-grammar/grammar.sed @@ -132,7 +132,9 @@ s/CATASSIGN/\'@=\'/g s/CASE/\'case\'/g s/BREAK/\'break\'/g s/BOOL//g +s/AWAITSTAR/\'await*\'/g s/AWAIT/\'await\'/g +s/ASYNCSTAR/\'async*\'/g s/ASYNC/\'async\'/g s/ASSERT/\'assert\'/g s/ARROW/\'->\'/g diff --git a/src/idllib/escape.ml b/src/idllib/escape.ml index 0a1853aa589..a7de912d98a 100644 --- a/src/idllib/escape.ml +++ b/src/idllib/escape.ml @@ -58,21 +58,26 @@ let is_motoko_keyword = function | "actor" | "and" | "async" + | "async*" | "assert" | "await" + | "await*" | "break" | "case" | "catch" | "class" | "continue" | "debug" - | "debug_show" + | "debug_show" + | "do" | "else" | "false" | "flexible" | "for" + | "from_candid" | "func" | "if" + | "ignore" | "in" | "import" | "module" @@ -93,10 +98,12 @@ let is_motoko_keyword = function | "system" | "try" | "throw" + | "to_candid" | "true" | "type" | "var" | "while" + | "with" -> true | _ -> false diff --git a/src/ir_def/arrange_ir.ml b/src/ir_def/arrange_ir.ml index e0a0be5b07d..6ce7e8983f2 100644 --- a/src/ir_def/arrange_ir.ml +++ b/src/ir_def/arrange_ir.ml @@ -22,7 +22,8 @@ let rec exp e = match e.it with | SwitchE (e, cs) -> "SwitchE" $$ [exp e] @ List.map case cs | LoopE e1 -> "LoopE" $$ [exp e1] | LabelE (i, t, e) -> "LabelE" $$ [id i; typ t; exp e] - | AsyncE (tb, e, t) -> "AsyncE" $$ [typ_bind tb; exp e; typ t] + | AsyncE (Type.Fut, tb, e, t) -> "AsyncE" $$ [typ_bind tb; exp e; typ t] + | AsyncE (Type.Cmp, tb, e, t) -> "AsyncE*" $$ [typ_bind tb; exp e; typ t] | DeclareE (i, t, e1) -> "DeclareE" $$ [id i; exp e1] | DefineE (i, m, e1) -> "DefineE" $$ [id i; mut m; exp e1] | FuncE (x, s, c, tp, as_, ts, e) -> @@ -73,7 +74,8 @@ and prim = function | GetPastArrayOffset _ -> Atom "GetPastArrayOffset" | BreakPrim i -> "BreakPrim" $$ [id i] | RetPrim -> Atom "RetPrim" - | AwaitPrim -> Atom "AwaitPrim" + | AwaitPrim Type.Fut -> Atom "AwaitPrim" + | AwaitPrim Type.Cmp -> Atom "AwaitPrim*" | AssertPrim -> Atom "AssertPrim" | ThrowPrim -> Atom "ThrowPrim" | ShowPrim t -> "ShowPrim" $$ [typ t] @@ -98,8 +100,10 @@ and prim = function | SetCertifiedData -> Atom "SetCertifiedData" | GetCertificate -> Atom "GetCertificate" | OtherPrim s -> Atom s - | CPSAwait t -> "CPSAwait" $$ [typ t] - | CPSAsync t -> "CPSAsync" $$ [typ t] + | CPSAwait (Type.Fut, t) -> "CPSAwait" $$ [typ t] + | CPSAwait (Type.Cmp, t) -> "CPSAwait*" $$ [typ t] + | CPSAsync (Type.Fut, t) -> "CPSAsync" $$ [typ t] + | CPSAsync (Type.Cmp, t) -> "CPSAsync*" $$ [typ t] | ICArgDataPrim -> Atom "ICArgDataPrim" | ICStableSize t -> "ICStableSize" $$ [typ t] | ICPerformGC -> Atom "ICPerformGC" diff --git a/src/ir_def/check_ir.ml b/src/ir_def/check_ir.ml index 104f25eefb9..f31c61f45ea 100644 --- a/src/ir_def/check_ir.ml +++ b/src/ir_def/check_ir.ml @@ -123,6 +123,7 @@ let disjoint_union env at fmt env1 env2 = (* Types *) +(* FIX ME: these error reporting functions are eager and will construct unnecessary type strings !*) let check_sub env at t1 t2 = if not (T.sub t1 t2) then error env at "subtype violation:\n %s\n %s\n" @@ -222,7 +223,7 @@ let rec check_typ env typ : unit = error env no_region "promising function cannot be local:\n %s" (T.string_of_typ_expand typ); | T.Opt typ -> check_typ env typ - | T.Async (typ1, typ2) -> + | T.Async (s, typ1, typ2) -> check_typ env typ1; check_typ env typ2; check env no_region env.flavor.Ir.has_async_typ "async in non-async flavor"; @@ -507,13 +508,13 @@ let rec check_exp env (exp:Ir.exp) : unit = check (env.async <> None) "misplaced throw"; typ exp1 <: T.throw; T.Non <: t (* vacuously true *) - | AwaitPrim, [exp1] -> + | AwaitPrim s, [exp1] -> check env.flavor.has_await "await in non-await flavor"; let t0 = match env.async with | Some c -> T.Con(c, []) | None -> error env exp.at "misplaced await" in let t1 = T.promote (typ exp1) in - let (t2, t3) = try T.as_async_sub t0 t1 + let (t2, t3) = try T.as_async_sub s t0 t1 with Invalid_argument _ -> error env exp1.at "expected async type, but expression has type\n %s" (T.string_of_typ_expand t1) @@ -540,11 +541,9 @@ let rec check_exp env (exp:Ir.exp) : unit = check (T.shared (T.seq ots)) "DeserializeOpt is not defined for operand type"; typ exp1 <: T.blob; T.Opt (T.seq ots) <: t - | CPSAwait cont_typ, [a; kr] -> - check (not (env.flavor.has_await)) "CPSAwait await flavor"; - check (env.flavor.has_async_typ) "CPSAwait in post-async flavor"; + | CPSAwait (s, cont_typ), [a; kr] -> let (_, t1) = - try T.as_async_sub T.Non (T.normalize (typ a)) + try T.as_async_sub s T.Non (T.normalize (typ a)) with _ -> error env exp.at "CPSAwait expect async arg, found %s" (T.string_of_typ (typ a)) in (match cont_typ with @@ -557,20 +556,21 @@ let rec check_exp env (exp:Ir.exp) : unit = t1 <: T.seq ts1; T.seq ts2 <: t; end; - | _ -> error env exp.at "CPSAwait bad cont") - | CPSAsync t0, [exp] -> - check (not (env.flavor.has_await)) "CPSAsync await flavor"; - check (env.flavor.has_async_typ) "CPSAsync in post-async flavor"; - check_typ env t0; + | _ -> error env exp.at "CPSAwait bad cont"); + check (not (env.flavor.has_await)) "CPSAwait await flavor"; + check (env.flavor.has_async_typ) "CPSAwait in post-async flavor"; + | CPSAsync (s, t0), [exp] -> (match typ exp with T.Func(T.Local,T.Returns, [tb], - [ T.Func(T.Local, T.Returns, [], ts1, []); - T.Func(T.Local, T.Returns, [], [t_error], []) ], + [T.Func(T.Local, T.Returns, [], ts1, []); + T.Func(T.Local, T.Returns, [], [t_error], [])], []) -> T.catch <: t_error; - T.Async(t0, Type.open_ [t0] (T.seq ts1)) <: t - | _ -> error env exp.at "CPSAsync unexpected typ") - (* TODO: We can check more here, can we *) + T.Async(s, t0, Type.open_ [t0] (T.seq ts1)) <: t + | _ -> error env exp.at "CPSAsync unexpected typ"); + check (not (env.flavor.has_await)) "CPSAsync await flavor"; + check (env.flavor.has_async_typ) "CPSAsync in post-async flavor"; + check_typ env t; | ICArgDataPrim, [] -> T.blob <: t | ICReplyPrim ts, [exp1] -> @@ -726,7 +726,7 @@ let rec check_exp env (exp:Ir.exp) : unit = check_exp (add_lab env id t0) exp1; typ exp1 <: t0; t0 <: t - | AsyncE (tb, exp1, t0) -> + | AsyncE (s, tb, exp1, t0) -> check env.flavor.has_await "async expression in non-await flavor"; check_typ env t0; let c, tb, ce = check_open_typ_bind env tb in @@ -737,7 +737,8 @@ let rec check_exp env (exp:Ir.exp) : unit = check_exp env' exp1; let t1' = T.open_ [t0] (T.close [c] t1) in t1' <: T.Any; (* vacuous *) - T.Async (t0, t1') <: t + (* check t1' shared when Fut? *) + T.Async (s, t0, t1') <: t | DeclareE (id, t0, exp1) -> check_mut_typ env t0; let val_info = { typ = t0; loc_known = false; const = false } in diff --git a/src/ir_def/construct.ml b/src/ir_def/construct.ml index faa91680c22..08d5d450d8f 100644 --- a/src/ir_def/construct.ml +++ b/src/ir_def/construct.ml @@ -132,28 +132,29 @@ let assertE e = } -let asyncE typ_bind e typ1 = - { it = AsyncE (typ_bind, e, typ1); +let asyncE s typ_bind e typ1 = + { it = AsyncE (s, typ_bind, e, typ1); at = no_region; - note = Note.{ def with typ = T.Async (typ1, typ e); eff = T.Triv } + note = Note.{ def with typ = T.Async (s, typ1, typ e); eff = T.Triv } } -let awaitE e = - { it = PrimE (AwaitPrim, [e]); +let awaitE s e = + let (s, _ , typ) = T.as_async (T.normalize (typ e)) in + { it = PrimE (AwaitPrim s, [e]); at = no_region; - note = Note.{ def with typ = snd (T.as_async (T.normalize (typ e))) ; eff = T.Await } + note = Note.{ def with typ; eff = T.Await } } -let cps_asyncE typ1 typ2 e = - { it = PrimE (CPSAsync typ1, [e]); +let cps_asyncE s typ1 typ2 e = + { it = PrimE (CPSAsync (s, typ1), [e]); at = no_region; - note = Note.{ def with typ = T.Async (typ1, typ2); eff = eff e } + note = Note.{ def with typ = T.Async (s, typ1, typ2); eff = eff e } } -let cps_awaitE cont_typ e1 e2 = +let cps_awaitE s cont_typ e1 e2 = match cont_typ with | T.Func(T.Local, T.Returns, [], _, ts2) -> - { it = PrimE (CPSAwait cont_typ, [e1; e2]); + { it = PrimE (CPSAwait (s, cont_typ), [e1; e2]); at = no_region; note = Note.{ def with typ = T.seq ts2; eff = max_eff (eff e1) (eff e2) } } @@ -306,11 +307,11 @@ let callE exp1 typs exp2 = } } -let ifE exp1 exp2 exp3 typ = +let ifE exp1 exp2 exp3 = { it = IfE (exp1, exp2, exp3); at = no_region; note = Note.{ def with - typ = typ; + typ = T.lub (typ exp2) (typ exp3); eff = max_eff (eff exp1) (max_eff (eff exp2) (eff exp3)) } } @@ -319,9 +320,14 @@ let falseE () = boolE false let trueE () = boolE true let notE : Ir.exp -> Ir.exp = fun e -> primE (RelPrim (T.bool, Operator.EqOp)) [e; falseE ()] -let andE : Ir.exp -> Ir.exp -> Ir.exp = fun e1 e2 -> ifE e1 e2 (falseE ()) T.bool -let orE : Ir.exp -> Ir.exp -> Ir.exp = fun e1 e2 -> ifE e1 (trueE ()) e2 T.bool -let impliesE : Ir.exp -> Ir.exp -> Ir.exp = fun e1 e2 -> orE (notE e1) e2 + +let andE : Ir.exp -> Ir.exp -> Ir.exp = fun e1 e2 -> + ifE e1 e2 (falseE ()) +let orE : Ir.exp -> Ir.exp -> Ir.exp = fun e1 e2 -> + ifE e1 (trueE ()) e2 +let impliesE : Ir.exp -> Ir.exp -> Ir.exp = fun e1 e2 -> + orE (notE e1) e2 + let rec conjE : Ir.exp list -> Ir.exp = function | [] -> trueE () | [x] -> x @@ -570,15 +576,18 @@ let funcD ((id, typ) as f) x exp = let nary_funcD ((id, typ) as f) xs exp = letD f (nary_funcE id typ xs exp) -(* Continuation types *) +(* Continuation types with explicit answer typ *) -let answerT = T.unit +let contT typ ans_typ = T.(Func (Local, Returns, [], as_seq typ, as_seq ans_typ)) -let contT typ = T.Func (T.Local, T.Returns, [], T.as_seq typ, []) +let err_contT ans_typ = T.(Func (Local, Returns, [], [catch], as_seq ans_typ)) -let err_contT = T.Func (T.Local, T.Returns, [], [T.catch], []) +let answerT typ : T.typ = + match typ with + | T.Func (T.Local, T.Returns, [], ts1, ts2) -> T.seq ts2 + | _ -> assert false -let cpsT typ = T.Func (T.Local, T.Returns, [], [contT typ; err_contT], []) +let cpsT typ ans_typ = T.(Func (Local, Returns, [], [contT typ ans_typ; err_contT ans_typ], as_seq ans_typ)) (* Sequence expressions *) @@ -635,13 +644,12 @@ let whileE exp1 exp2 = *) let lab = fresh_id "done" () in labelE lab T.unit ( - loopE ( - ifE exp1 - exp2 - (breakE lab (unitE ())) - T.unit - ) + loopE ( + ifE exp1 + exp2 + (breakE lab (tupE [])) ) + ) let loopWhileE exp1 exp2 = (* loop e1 while e2 @@ -652,15 +660,14 @@ let loopWhileE exp1 exp2 = *) let lab = fresh_id "done" () in labelE lab T.unit ( - loopE ( - thenE exp1 - ( ifE exp2 - (unitE ()) - (breakE lab (unitE ())) - T.unit - ) - ) + loopE ( + thenE exp1 ( + ifE exp2 + (tupE []) + (breakE lab (tupE [])) + ) ) + ) let forE pat exp1 exp2 = (* for (p in e1) e2 diff --git a/src/ir_def/construct.mli b/src/ir_def/construct.mli index 91cfbfc6419..e7fa8a8ff84 100644 --- a/src/ir_def/construct.mli +++ b/src/ir_def/construct.mli @@ -49,10 +49,10 @@ val varE : var -> exp val primE : Ir.prim -> exp list -> exp val selfRefE : typ -> exp val assertE : exp -> exp -val asyncE : typ_bind -> exp -> typ -> exp -val awaitE : exp -> exp -val cps_asyncE : typ -> typ -> exp -> exp -val cps_awaitE : typ -> exp -> exp -> exp +val asyncE : async_sort -> typ_bind -> exp -> typ -> exp +val awaitE : async_sort -> exp -> exp +val cps_asyncE : async_sort -> typ -> typ -> exp -> exp +val cps_awaitE : async_sort -> typ -> exp -> exp -> exp val ic_replyE : typ list -> exp -> exp val ic_rejectE : exp -> exp val ic_callE : exp -> exp -> exp -> exp -> exp @@ -76,7 +76,7 @@ val funcE : string -> func_sort -> control -> exp val callE : exp -> typ list -> exp -> exp -val ifE : exp -> exp -> exp -> typ -> exp +val ifE : exp -> exp -> exp -> exp val dotE : exp -> Type.lab -> typ -> exp val switch_optE : exp -> exp -> pat -> exp -> typ -> exp val switch_variantE : exp -> (id * pat * exp) list -> typ -> exp @@ -118,12 +118,13 @@ val nary_funcD : var -> var list -> exp -> dec val let_no_shadow : var -> exp -> dec list -> dec list -(* Continuations *) +(* Continuations with explicit answer type *) -val answerT : typ -val contT : typ -> typ -val err_contT : typ -val cpsT : typ -> typ +val contT : typ -> typ -> typ +val err_contT : typ -> typ +val answerT : typ -> typ (* answer type of a continuation type *) + +val cpsT : typ -> typ -> typ (* Sequence expressions *) diff --git a/src/ir_def/freevars.ml b/src/ir_def/freevars.ml index c6e2339ad2d..fff078bc313 100644 --- a/src/ir_def/freevars.ml +++ b/src/ir_def/freevars.ml @@ -112,7 +112,7 @@ let rec exp e : f = match e.it with | SwitchE (e, cs) -> exp e ++ cases cs | LoopE e1 -> exp e1 | LabelE (i, t, e) -> exp e - | AsyncE (_, e, _) -> exp e + | AsyncE (_, _, e, _) -> exp e | DeclareE (i, t, e) -> exp e // i | DefineE (i, m, e) -> id i ++ exp e | FuncE (x, s, c, tp, as_, t, e) -> under_lambda (exp e /// args as_) diff --git a/src/ir_def/ir.ml b/src/ir_def/ir.ml index c55d00e056e..b30252ff296 100644 --- a/src/ir_def/ir.ml +++ b/src/ir_def/ir.ml @@ -66,7 +66,7 @@ and exp' = | SwitchE of exp * case list (* switch *) | LoopE of exp (* do-while loop *) | LabelE of id * Type.typ * exp (* label *) - | AsyncE of typ_bind * exp * Type.typ (* async *) + | AsyncE of Type.async_sort * typ_bind * exp * Type.typ (* async/async* *) | DeclareE of id * Type.typ * exp (* local promise *) | DefineE of id * mut * exp (* promise fulfillment *) | FuncE of (* function *) @@ -125,7 +125,7 @@ and prim = | IdxPrim (* array indexing *) | BreakPrim of id (* break *) | RetPrim (* return *) - | AwaitPrim (* await *) + | AwaitPrim of Type.async_sort (* await/await* *) | AssertPrim (* assertion *) | ThrowPrim (* throw *) | ShowPrim of Type.typ (* debug_show *) @@ -159,8 +159,9 @@ and prim = | OtherPrim of string (* Other primitive operation, no custom typing rule *) (* backend stuff *) - | CPSAwait of Type.typ - | CPSAsync of Type.typ + | CPSAwait of Type.async_sort * Type.typ + (* typ is the current continuation type of cps translation *) + | CPSAsync of Type.async_sort * Type.typ | ICPerformGC | ICReplyPrim of Type.typ list | ICRejectPrim @@ -274,7 +275,7 @@ let map_prim t_typ t_id p = | GetPastArrayOffset _ -> p | BreakPrim id -> BreakPrim (t_id id) | RetPrim - | AwaitPrim + | AwaitPrim _ | AssertPrim | ThrowPrim -> p | ShowPrim t -> ShowPrim (t_typ t) @@ -299,8 +300,8 @@ let map_prim t_typ t_id p = | SetCertifiedData | GetCertificate | OtherPrim _ -> p - | CPSAwait t -> CPSAwait (t_typ t) - | CPSAsync t -> CPSAsync (t_typ t) + | CPSAwait (s, t) -> CPSAwait (s, t_typ t) + | CPSAsync (s, t) -> CPSAsync (s, t_typ t) | ICReplyPrim ts -> ICReplyPrim (List.map t_typ ts) | ICArgDataPrim | ICPerformGC diff --git a/src/ir_def/ir_effect.ml b/src/ir_def/ir_effect.ml index b4c8132b882..4784530c8f4 100644 --- a/src/ir_def/ir_effect.ml +++ b/src/ir_def/ir_effect.ml @@ -22,7 +22,7 @@ let effect_exp (exp: exp) : T.eff = eff exp (* infer the effect of an expression, assuming all sub-expressions are correctly effect-annotated es*) let rec infer_effect_prim = function - | ThrowPrim | AwaitPrim -> T.Await + | ThrowPrim | AwaitPrim _ -> T.Await | _ -> T.Triv and infer_effect_exp (exp: exp) : T.eff = diff --git a/src/ir_def/rename.ml b/src/ir_def/rename.ml index fca2400c3b7..9db4a9b95a2 100644 --- a/src/ir_def/rename.ml +++ b/src/ir_def/rename.ml @@ -47,7 +47,7 @@ and exp' rho = function | LoopE e1 -> LoopE (exp rho e1) | LabelE (i, t, e) -> let i',rho' = id_bind rho i in LabelE(i', t, exp rho' e) - | AsyncE (tb, e, t) -> AsyncE (tb, exp rho e, t) + | AsyncE (s, tb, e, t) -> AsyncE (s, tb, exp rho e, t) | DeclareE (i, t, e) -> let i',rho' = id_bind rho i in DeclareE (i', t, exp rho' e) | DefineE (i, m, e) -> DefineE (id rho i, m, exp rho e) diff --git a/src/ir_interpreter/interpret_ir.ml b/src/ir_interpreter/interpret_ir.ml index 3f829869e8e..f93016480fb 100644 --- a/src/ir_interpreter/interpret_ir.ml +++ b/src/ir_interpreter/interpret_ir.ml @@ -363,9 +363,12 @@ and interpret_exp_mut env exp (k : V.value V.cont) = | BreakPrim id, [v1] -> find id env.labs v1 | RetPrim, [v1] -> Option.get env.rets v1 | ThrowPrim, [v1] -> Option.get env.throws v1 - | AwaitPrim, [v1] -> + | AwaitPrim Type.Fut, [v1] -> assert env.flavor.has_await; await env exp.at (V.as_async v1) k (Option.get env.throws) + | AwaitPrim Type.Cmp, [v1] -> + assert env.flavor.has_await; + (V.as_comp v1) k (Option.get env.throws) | AssertPrim, [v1] -> if V.as_bool v1 then k V.unit @@ -495,7 +498,7 @@ and interpret_exp_mut env exp (k : V.value V.cont) = | LabelE (id, _typ, exp1) -> let env' = {env with labs = V.Env.add id k env.labs} in interpret_exp env' exp1 k - | AsyncE (_, exp1, _) -> + | AsyncE (Type.Fut, _, exp1, _) -> assert env.flavor.has_await; async env exp.at @@ -503,6 +506,11 @@ and interpret_exp_mut env exp (k : V.value V.cont) = let env' = { env with labs = V.Env.empty; rets = Some k'; throws = Some r } in interpret_exp env' exp1 k') k + | AsyncE (Type.Cmp, _, exp1, _) -> + assert env.flavor.has_await; + k (V.Comp (fun k' r -> + let env' = { env with labs = V.Env.empty; rets = Some k'; throws = Some r } + in interpret_exp env' exp1 k')) | DeclareE (id, typ, exp1) -> let env = adjoin_vals env (declare_id id) in interpret_exp env exp1 k diff --git a/src/ir_passes/async.ml b/src/ir_passes/async.ml index f7b825af6a9..8796b4f583d 100644 --- a/src/ir_passes/async.ml +++ b/src/ir_passes/async.ml @@ -29,8 +29,7 @@ let selfcallE ts e1 e2 e3 = at = no_region; note = Note.{ def with typ = T.unit } } -let error_ty = - T.(Tup [ Variant [ +let error_ty = T.(Tup [ Variant [ {lab = "error"; typ = unit; depr = None}; {lab = "system"; typ = unit; depr = None} ]; text]) @@ -46,11 +45,16 @@ let fulfillT as_seq typ = T.Func(T.Local, T.Returns, [], as_seq typ, []) let failT = T.Func(T.Local, T.Returns, [], [T.catch], []) -let t_async as_seq t = +let t_async_fut as_seq t = T.Func (T.Local, T.Returns, [], [fulfillT as_seq t; failT], - [T.Opt (T.Func(T.Local, T.Returns, [], [], []))]) + [T.sum [ + ("suspend", T.unit); + ("schedule", T.Func(T.Local, T.Returns, [], [], []))]]) -let new_async_ret as_seq t = [t_async as_seq t; fulfillT as_seq t; failT] +let t_async_cmp as_seq t = + T.Func (T.Local, T.Returns, [], [fulfillT as_seq t; failT], []) + +let new_async_ret as_seq t = [t_async_fut as_seq t; fulfillT as_seq t; failT] let new_asyncT = T.Func ( @@ -63,40 +67,39 @@ let new_asyncT = let new_asyncE () = varE (var "@new_async" new_asyncT) -let new_async t1 = - let call_new_async = callE (new_asyncE ()) [t1] (tupE []) in +let new_async t = + let call_new_async = callE (new_asyncE ()) [t] (unitE()) in let async = fresh_var "async" (typ (projE call_new_async 0)) in let fulfill = fresh_var "fulfill" (typ (projE call_new_async 1)) in let fail = fresh_var "fail" (typ (projE call_new_async 2)) in (async, fulfill, fail), call_new_async -let new_nary_async_reply mode ts1 = +let new_nary_async_reply ts = (* The async implementation isn't n-ary *) - let t1 = T.seq ts1 in - let (unary_async, unary_fulfill, fail), call_new_async = new_async t1 in - let v' = fresh_var "v" t1 in + let t = T.seq ts in + let (unary_async, unary_fulfill, fail), call_new_async = new_async t in + let v' = fresh_var "v" t in (* construct the n-ary async value, coercing the continuation, if necessary *) let nary_async = - match ts1 with - | [t] -> + match ts with + | [t1] -> varE unary_async - | ts -> - let k' = fresh_var "k" (contT t1) in - let r' = fresh_var "r" err_contT in - let seq_of_v' = tupE (List.mapi (fun i _ -> projE (varE v') i) ts) in + | ts1 -> + let k' = fresh_var "k" (contT t T.unit) in + let r' = fresh_var "r" (err_contT T.unit) in [k';r'] -->* ( - varE unary_async -*- (tupE[([v'] -->* (varE k' -*- seq_of_v')); varE r']) + varE unary_async -*- (tupE[([v'] -->* (varE k' -*- varE v')); varE r']) ) in - (* construct the n-ary reply callback that sends a sequence of values to fulfill the async *) + (* construct the n-ary reply callback that take a *sequence* of values to fulfill the async *) let nary_reply = - let vs,seq_of_vs = - match ts1 with - | [t] -> - let v = fresh_var "rep" t in + let vs, seq_of_vs = + match ts with + | [t1] -> + let v = fresh_var "rep" t1 in [v], varE v - | ts -> - let vs = fresh_vars "rep" ts in + | ts1 -> + let vs = fresh_vars "rep" ts1 in vs, tupE (List.map varE vs) in vs -->* (varE unary_fulfill -*- seq_of_vs) @@ -110,11 +113,13 @@ let new_nary_async_reply mode ts1 = blockE [letP (tupP [varP unary_async; varP unary_fulfill; varP fail]) call_new_async] (tupE [nary_async; nary_reply; varE fail]) + let letEta e scope = match e.it with | VarE _ -> scope e (* pure, so reduce *) - | _ -> let f = fresh_var "x" (typ e) in - letD f e :: (scope (varE f)) (* maybe impure; sequence *) + | _ -> + let f = fresh_var "x" (typ e) in + letD f e :: (scope (varE f)) (* maybe impure; sequence *) let isAwaitableFunc exp = match typ exp with @@ -150,7 +155,7 @@ let ensureNamed e f = (* The actual transformation *) -let transform mode prog = +let transform prog = (* the state *) let con_renaming = ref ConRenaming.empty @@ -181,7 +186,8 @@ let transform mode prog = Func (s, c', List.map t_bind tbs, List.map t_typ ts1, List.map t_typ ts2) | Opt t -> Opt (t_typ t) | Variant fs -> Variant (List.map t_field fs) - | Async (_, t) -> t_async nary (t_typ t) (* TBR exploit the index _ *) + | Async (Fut, _, t) -> t_async_fut nary (t_typ t) (* TBR exploit the index _ *) + | Async (Cmp, _, t) -> t_async_cmp nary (t_typ t) (* TBR exploit the index _ *) | Obj (s, fs) -> Obj (s, List.map t_field fs) | Mut t -> Mut (t_typ t) | Any -> Any @@ -235,36 +241,62 @@ let transform mode prog = | VarE id -> exp' | AssignE (exp1, exp2) -> AssignE (t_lexp exp1, t_exp exp2) - | PrimE (CPSAwait _, [a; kr]) -> - (ensureNamed (t_exp kr) (fun vkr -> - let resume = fresh_var "resume" (T.Func(T.Local, T.Returns, [], [], [])) in - (switch_optE ((t_exp a) -*- varE vkr) - (unitE()) (* suspend *) - (varP resume) (* yield and resume *) - (* try await async (); resume() catch e -> r(e) *) - (selfcallE [] (ic_replyE [] (unitE())) (varE resume) (projE (varE vkr) 1)) - T.unit - ))).it - | PrimE (CPSAsync t0, [exp1]) -> - let t0 = t_typ t0 in + | PrimE (CPSAwait (Fut, cont_typ), [a; kr]) -> + begin match cont_typ with + | Func(_, _, [], _, []) -> + (* unit answer type, from await in `async {}` *) + (ensureNamed (t_exp kr) (fun vkr -> + let schedule = fresh_var "schedule" (T.Func(T.Local, T.Returns, [], [], [])) in + switch_variantE ((t_exp a) -*- varE vkr) + [ ("suspend", wildP, + unitE()); (* suspend *) + ("schedule", varP schedule, (* resume later *) + (* try await async (); schedule() catch e -> r(e) *) + (selfcallE [] (ic_replyE [] (unitE())) (varE schedule) (projE (varE vkr) 1))) ] + T.unit + )).it + | _ -> assert false + end + | PrimE (CPSAwait (Cmp, cont_typ), [a; kr]) -> + begin match cont_typ with + | Func(_, _, [], _, []) -> + ((t_exp a) -*- (t_exp kr)).it + | _ -> assert false + end + | PrimE (CPSAsync (Fut, t), [exp1]) -> + let t0 = t_typ t in let tb, ts1 = match typ exp1 with | Func(_,_, [tb], [Func(_, _, [], ts1, []); _], []) -> - tb, List.map t_typ (List.map (T.open_ [t0]) ts1) + tb, List.map t_typ (List.map (T.open_ [t]) ts1) | t -> assert false in - let ((nary_async, nary_reply, reject), def) = new_nary_async_reply mode ts1 in - (blockE [ - letP (tupP [varP nary_async; varP nary_reply; varP reject]) def; - let ic_reply = (* flatten v, here and below? *) - let v = fresh_var "v" (T.seq ts1) in - v --> (ic_replyE ts1 (varE v)) in - let ic_reject = - let e = fresh_var "e" T.catch in - [e] -->* (ic_rejectE (errorMessageE (varE e))) in - let exp' = callE (t_exp exp1) [t0] (tupE [ic_reply; ic_reject]) in - expD (selfcallE ts1 exp' (varE nary_reply) (varE reject)) + let ((nary_async, nary_reply, reject), def) = + new_nary_async_reply ts1 + in + ( blockE [ + letP (tupP [varP nary_async; varP nary_reply; varP reject]) def; + let ic_reply = (* flatten v, here and below? *) + let v = fresh_var "v" (T.seq ts1) in + v --> (ic_replyE ts1 (varE v)) in + let ic_reject = + let e = fresh_var "e" T.catch in + [e] -->* (ic_rejectE (errorMessageE (varE e))) in + let exp' = callE (t_exp exp1) [t0] (tupE [ic_reply; ic_reject]) in + expD (selfcallE ts1 exp' (varE nary_reply) (varE reject)) ] (varE nary_async) ).it + | PrimE (CPSAsync (Cmp, t), [exp1]) -> + let t0 = t_typ t in + let tb, t_ret, t_fail = match typ exp1 with + | Func(_,_, [tb], [t_ret; t_fail], _ ) -> + tb, + t_typ (T.open_ [t] t_ret), + t_typ (T.open_ [t] t_fail) + | t -> assert false + in + let v_ret = fresh_var "v" t_ret in + let v_fail = fresh_var "e" t_fail in + ( [v_ret; v_fail] -->* (callE (t_exp exp1) [t0] (tupE [varE v_ret; varE v_fail]))).it | PrimE (CallPrim typs, [exp1; exp2]) when isAwaitableFunc exp1 -> let ts1,ts2 = match typ exp1 with @@ -275,7 +307,9 @@ let transform mode prog = in let exp1' = t_exp exp1 in let exp2' = t_exp exp2 in - let ((nary_async, nary_reply, reject), def) = new_nary_async_reply mode ts2 in + let ((nary_async, nary_reply, reject), def) = + new_nary_async_reply ts2 + in let _ = letEta in (blockE ( letP (tupP [varP nary_async; varP nary_reply; varP reject]) def :: @@ -291,7 +325,7 @@ let transform mode prog = let exp1' = t_exp exp1 in let exp2' = t_exp exp2 in let exp3' = t_exp exp3 in - let ((nary_async, nary_reply, reject), def) = new_nary_async_reply mode [T.blob] in + let ((nary_async, nary_reply, reject), def) = new_nary_async_reply [T.blob] in let _ = letEta in (blockE ( letP (tupP [varP nary_async; varP nary_reply; varP reject]) def :: @@ -311,10 +345,9 @@ let transform mode prog = | IfE (exp1, exp2, exp3) -> IfE (t_exp exp1, t_exp exp2, t_exp exp3) | SwitchE (exp1, cases) -> - let cases' = List.map - (fun {it = {pat; exp}; at; note} -> - {it = {pat = t_pat pat ;exp = t_exp exp}; at; note}) - cases + let cases' = List.map (fun {it = {pat; exp}; at; note} -> + { it = {pat = t_pat pat ; exp = t_exp exp}; at; note }) + cases in SwitchE (t_exp exp1, cases') | LoopE exp1 -> @@ -340,7 +373,7 @@ let transform mode prog = let args' = t_args args in let typbinds' = t_typ_binds typbinds in let t0, cps = match exp.it with - | PrimE (CPSAsync t0, [cps]) -> t_typ t0, cps + | PrimE (CPSAsync (Type.Fut, t0), [cps]) -> t_typ t0, cps | _ -> assert false in let t1, contT = match typ cps with | Func (_,_, @@ -369,7 +402,7 @@ let transform mode prog = let args' = t_args args in let typbinds' = t_typ_binds typbinds in let t0, cps = match exp.it with - | PrimE (CPSAsync t0, [cps]) -> t_typ t0, cps + | PrimE (CPSAsync (Type.Fut, t0), [cps]) -> t_typ t0, cps (* TBR *) | _ -> assert false in let t1, contT = match typ cps with | Func (_, _, diff --git a/src/ir_passes/async.mli b/src/ir_passes/async.mli index 1e0b2aa12ec..4fc1e632b1c 100644 --- a/src/ir_passes/async.mli +++ b/src/ir_passes/async.mli @@ -1,5 +1,4 @@ (* lower uses of async type appropriately *) open Ir_def -val transform : - Mo_config.Flags.compile_mode -> Ir.prog -> Ir.prog +val transform : Ir.prog -> Ir.prog diff --git a/src/ir_passes/await.ml b/src/ir_passes/await.ml index a3e572bbc1a..cce16dfe318 100644 --- a/src/ir_passes/await.ml +++ b/src/ir_passes/await.ml @@ -8,9 +8,9 @@ module R = Rename module T = Type open Construct -let fresh_cont typ = fresh_var "k" (contT typ) +let fresh_cont typ ans_typ = fresh_var "k" (contT typ ans_typ) -let fresh_err_cont () = fresh_var "r" (err_contT) +let fresh_err_cont ans_typ = fresh_var "r" (err_contT ans_typ) (* continuations, syntactic and meta-level *) @@ -30,10 +30,11 @@ let meta typ exp = let letcont k scope = match k with | ContVar k' -> scope k' (* letcont eta-contraction *) - | MetaCont (typ, cont) -> - let k' = fresh_cont typ in - let v = fresh_var "v" typ in - blockE [funcD k' v (cont v)] (* at this point, I'm really worried about variable capture *) + | MetaCont (typ0, cont) -> + let v = fresh_var "v" typ0 in + let e = cont v in + let k' = fresh_cont typ0 (typ e) in + blockE [funcD k' v e] (* at this point, I'm really worried about variable capture *) (scope k') (* Named labels for break, special labels for return and throw *) @@ -58,6 +59,8 @@ module PatEnv = Env.Make(String) type label_sort = Cont of kont | Label +let typ_cases cases = List.fold_left (fun t case -> T.lub t (typ case.it.exp)) T.Non cases + (* Trivial translation of pure terms (eff = T.Triv) *) let rec t_exp context exp = @@ -99,26 +102,26 @@ and t_exp' context exp' = | Some Label -> (retE (t_exp context exp1)).it | None -> assert false end - | AsyncE (tb, exp1, typ1) -> - let exp1 = R.exp R.Renaming.empty exp1 in (* rename all bound vars apart *) - (* add the implicit return/throw label *) - let k_ret = fresh_cont (typ exp1) in - let k_fail = fresh_err_cont () in - let context' = - LabelEnv.add Return (Cont (ContVar k_ret)) - (LabelEnv.add Throw (Cont (ContVar k_fail)) LabelEnv.empty) - in - (cps_asyncE typ1 (typ exp1) - (forall [tb] ([k_ret; k_fail] -->* - c_exp context' exp1 (ContVar k_ret)))).it + | AsyncE (s, tb, exp1, typ1) -> + let exp1 = R.exp R.Renaming.empty exp1 in (* rename all bound vars apart *) + (* add the implicit return/throw label *) + let k_ret = fresh_cont (typ exp1) T.unit in + let k_fail = fresh_err_cont T.unit in + let context' = + LabelEnv.add Return (Cont (ContVar k_ret)) + (LabelEnv.add Throw (Cont (ContVar k_fail)) LabelEnv.empty) + in + (cps_asyncE s typ1 (typ exp1) + (forall [tb] ([k_ret; k_fail] -->* + c_exp context' exp1 (ContVar k_ret)))).it | TryE _ -> assert false (* these never have effect T.Triv *) | DeclareE (id, typ, exp1) -> DeclareE (id, typ, t_exp context exp1) | DefineE (id, mut ,exp1) -> DefineE (id, mut, t_exp context exp1) - | FuncE (x, s, c, typbinds, pat, typ, exp) -> + | FuncE (x, s, c, typbinds, pat, typs, exp1) -> let context' = LabelEnv.add Return Label LabelEnv.empty in - FuncE (x, s, c, typbinds, pat, typ,t_exp context' exp) + FuncE (x, s, c, typbinds, pat, typs, t_exp context' exp1) | ActorE (ds, ids, { meta; preupgrade; postupgrade; heartbeat; inspect}, t) -> ActorE (t_decs context ds, ids, { meta; @@ -209,9 +212,9 @@ and c_if context k e1 e2 e3 = let e3 = trans_branch e3 in match eff e1 with | T.Triv -> - ifE (t_exp context e1) e2 e3 answerT + ifE (t_exp context e1) e2 e3 | T.Await -> - c_exp context e1 (meta (typ e1) (fun v1 -> ifE (varE v1) e2 e3 answerT)) + c_exp context e1 (meta (typ e1) (fun v1 -> ifE (varE v1) e2 e3)) ) and c_loop context k e1 = @@ -219,7 +222,7 @@ and c_loop context k e1 = | T.Triv -> assert false | T.Await -> - let loop = fresh_var "loop" (contT T.unit) in + let loop = fresh_var "loop" (contT T.unit T.unit) in let v1 = fresh_var "v" T.unit in blockE [funcD loop v1 (c_exp context e1 (ContVar loop))] @@ -271,19 +274,20 @@ and c_exp' context exp k = {it = { pat; exp = exp' }; at; note}) cases in + let typ' = typ_cases cases' in begin match eff exp1 with | T.Triv -> { it = SwitchE(t_exp context exp1, cases'); at = exp.at; - note = Note.{ exp.note with typ = answerT } } + note = Note.{ exp.note with typ = typ' } } | T.Await -> c_exp context exp1 (meta (typ exp1) (fun v1 -> { it = SwitchE(varE v1, cases'); at = exp.at; - note = Note.{ exp.note with typ = answerT } })) + note = Note.{ exp.note with typ = typ' } })) end) | TryE (exp1, cases) -> (* TODO: do we need to reify f? *) @@ -308,14 +312,14 @@ and c_exp' context exp k = at = no_region; note = () }] in - let throw = fresh_err_cont () in + let throw = fresh_err_cont (answerT (typ_of_var k)) in let context' = LabelEnv.add Throw (Cont (ContVar throw)) context in blockE [ let e = fresh_var "e" T.catch in funcD throw e { it = SwitchE (varE e, cases'); at = exp.at; - note = Note.{ def with typ = T.unit; eff = T.Await; (* shouldn't matter *) } + note = Note.{ def with typ = typ_cases cases'; eff = T.Await; (* shouldn't matter *) } } ] (c_exp context' exp1 (ContVar k)) @@ -348,19 +352,19 @@ and c_exp' context exp k = | Some Label | None -> assert false end - | AsyncE (tb, exp1, typ1) -> + | AsyncE (s, tb, exp1, typ1) -> (* add the implicit return label *) - let k_ret = fresh_cont (typ exp1) in - let k_fail = fresh_err_cont () in + let k_ret = fresh_cont (typ exp1) T.unit in + let k_fail = fresh_err_cont T.unit in let context' = LabelEnv.add Return (Cont (ContVar k_ret)) (LabelEnv.add Throw (Cont (ContVar k_fail)) LabelEnv.empty) in k -@- - (cps_asyncE typ1 (typ exp1) + (cps_asyncE s typ1 (typ exp1) (forall [tb] ([k_ret; k_fail] -->* (c_exp context' exp1 (ContVar k_ret))))) - | PrimE (AwaitPrim, [exp1]) -> + | PrimE (AwaitPrim s, [exp1]) -> let r = match LabelEnv.find_opt Throw context with | Some (Cont r) -> r | Some Label @@ -371,10 +375,10 @@ and c_exp' context exp k = let kr = tupE [varE k; varE r] in match eff exp1 with | T.Triv -> - cps_awaitE (typ_of_var k) (t_exp context exp1) kr + cps_awaitE s (typ_of_var k) (t_exp context exp1) kr | T.Await -> c_exp context exp1 - (meta (typ exp1) (fun v1 -> (cps_awaitE (typ_of_var k) (varE v1) kr))) + (meta (typ exp1) (fun v1 -> (cps_awaitE s (typ_of_var k) (varE v1) kr))) )) | DeclareE (id, typ, exp1) -> unary context k (fun v1 -> e (DeclareE (id, typ, varE v1))) exp1 @@ -523,7 +527,7 @@ and t_comp_unit context = function | T.Triv -> ProgU (t_decs context ds) | T.Await -> - let throw = fresh_err_cont () in + let throw = fresh_err_cont T.unit in let context' = LabelEnv.add Throw (Cont (ContVar throw)) context in let e = fresh_var "e" T.catch in ProgU [ diff --git a/src/ir_passes/const.ml b/src/ir_passes/const.ml index c29f992a45f..f4e31a4ee14 100644 --- a/src/ir_passes/const.ml +++ b/src/ir_passes/const.ml @@ -137,7 +137,7 @@ let rec exp lvl (env : env) e : Lbool.t = | DeclareE (id, _, e1) -> exp_ lvl (M.add id no_info env) e1; surely_false - | LoopE e1 | AsyncE (_, e1, _) -> + | LoopE e1 | AsyncE (_, _, e1, _) -> exp_ NotTopLvl env e1; surely_false | AssignE (_, e1) | LabelE (_, _, e1) | DefineE (_, _, e1) -> diff --git a/src/ir_passes/eq.ml b/src/ir_passes/eq.ml index cad399ec339..40db32f1912 100644 --- a/src/ir_passes/eq.ml +++ b/src/ir_passes/eq.ml @@ -241,7 +241,7 @@ and t_exp' env = function LoopE (t_exp env exp1) | LabelE (id, typ, exp1) -> LabelE (id, typ, t_exp env exp1) - | AsyncE (tb, e, typ) -> AsyncE (tb, t_exp env e, typ) + | AsyncE (s, tb, e, typ) -> AsyncE (s, tb, t_exp env e, typ) | DeclareE (id, typ, exp1) -> DeclareE (id, typ, t_exp env exp1) | DefineE (id, mut ,exp1) -> diff --git a/src/ir_passes/erase_typ_field.ml b/src/ir_passes/erase_typ_field.ml index f8db183b88c..fcb5b92af3d 100644 --- a/src/ir_passes/erase_typ_field.ml +++ b/src/ir_passes/erase_typ_field.ml @@ -51,7 +51,7 @@ let transform prog = Func (s, c, List.map t_bind tbs, List.map t_typ ts1, List.map t_typ ts2) | Opt t -> Opt (t_typ t) | Variant fs -> Variant (List.map t_field fs) - | Async (t1, t2) -> Async (t_typ t1, t_typ t2) + | Async (s, t1, t2) -> Async (s, t_typ t1, t_typ t2) | Mut t -> Mut (t_typ t) | Any -> Any | Non -> Non @@ -116,8 +116,8 @@ let transform prog = LoopE (t_exp exp1) | LabelE (id, typ, exp1) -> LabelE (id, t_typ typ, t_exp exp1) - | AsyncE (tb, exp1, typ) -> - AsyncE (t_typ_bind tb, t_exp exp1, t_typ typ) + | AsyncE (s, tb, exp1, typ) -> + AsyncE (s, t_typ_bind tb, t_exp exp1, t_typ typ) | TryE (exp1, cases) -> TryE (t_exp exp1, List.map t_case cases) | DeclareE (id, typ, exp1) -> diff --git a/src/ir_passes/show.ml b/src/ir_passes/show.ml index 1b4049d60e7..74fe9c5d2a5 100644 --- a/src/ir_passes/show.ml +++ b/src/ir_passes/show.ml @@ -283,7 +283,7 @@ and t_exp' env = function LoopE (t_exp env exp1) | LabelE (id, typ, exp1) -> LabelE (id, typ, t_exp env exp1) - | AsyncE (tb, e, typ) -> AsyncE (tb, t_exp env e, typ) + | AsyncE (s, tb, e, typ) -> AsyncE (s, tb, t_exp env e, typ) | DeclareE (id, typ, exp1) -> DeclareE (id, typ, t_exp env exp1) | DefineE (id, mut ,exp1) -> diff --git a/src/ir_passes/tailcall.ml b/src/ir_passes/tailcall.ml index aca610acc4f..3bd4205934a 100644 --- a/src/ir_passes/tailcall.ml +++ b/src/ir_passes/tailcall.ml @@ -111,8 +111,7 @@ and exp' env e : exp' = match e.it with | LabelE (i, t, e) -> let env1 = bind env i None in LabelE(i, t, exp env1 e) | PrimE (RetPrim, [e])-> PrimE (RetPrim, [tailexp { env with tail_pos = true } e]) - (* NB:^ e is always in tailposition, regardless of fst env *) - | AsyncE (tb, e, typ) -> AsyncE (tb, exp { tail_pos = true; info = None } e, typ) + | AsyncE (s, tb, e, typ) -> AsyncE (s, tb, exp { tail_pos = true; info = None } e, typ) | DeclareE (i, t, e) -> let env1 = bind env i None in DeclareE (i, t, tailexp env1 e) | DefineE (i, m, e) -> DefineE (i, m, exp env e) diff --git a/src/lang_utils/error_codes.ml b/src/lang_utils/error_codes.ml index 7f6f76df51e..3788b1f9f0a 100644 --- a/src/lang_utils/error_codes.ml +++ b/src/lang_utils/error_codes.ml @@ -185,4 +185,5 @@ let error_codes : (string * string option) list = "M0179", None; (* Mutable (var) fields from bases must be overwritten explicitly *) "M0180", None; (* Shared function has unexpected type parameters *) "M0181", None; (* Verification mode assertions not allowed *) + "M0183", None; (* Incompatible async sorts *) ] diff --git a/src/lowering/desugar.ml b/src/lowering/desugar.ml index 177944ed0b2..5cd6b151ed8 100644 --- a/src/lowering/desugar.ml +++ b/src/lowering/desugar.ml @@ -217,12 +217,12 @@ and exp' at note = function | S.BreakE (l, e) -> (breakE l.it (exp e)).it | S.RetE e -> (retE (exp e)).it | S.ThrowE e -> I.PrimE (I.ThrowPrim, [exp e]) - | S.AsyncE (tb, e) -> - I.AsyncE (typ_bind tb, exp e, - match note.Note.typ with - | T.Async (t, _) -> t - | _ -> assert false) - | S.AwaitE e -> I.PrimE (I.AwaitPrim, [exp e]) + | S.AsyncE (s, tb, e) -> + I.AsyncE (s, typ_bind tb, exp e, + match note.Note.typ with + | T.Async (_, t, _) -> t + | _ -> assert false) + | S.AwaitE (s, e) -> I.PrimE (I.AwaitPrim s, [exp e]) | S.AssertE (Runtime, e) -> I.PrimE (I.AssertPrim, [exp e]) | S.AssertE (_, e) -> (unitE ()).it | S.AnnotE (e, _) -> assert false @@ -378,8 +378,7 @@ and call_system_func_opt name es obj_typ = (ifE (varE accept) (unitE ()) (primE (Ir.OtherPrim "trap") - [textE "canister_inspect_message explicitly refused message"]) - T.unit) + [textE "canister_inspect_message explicitly refused message"])) | _name -> callE (varE (var id.it p.note)) [] (tupE [])) | _ -> None) es @@ -401,7 +400,7 @@ and export_interface txt = let bind2 = typ_arg scope_con2 Scope scope_bound in ([ letD (var v typ) ( funcE v (Shared Query) Promises [bind1] [] [text] ( - asyncE bind2 (textE txt) (Con (scope_con1, [])) + asyncE Type.Fut bind2 (textE txt) (Con (scope_con1, [])) ) )], [{ it = I.{ name = lab; var = v }; at = no_region; note = typ }]) @@ -418,7 +417,7 @@ and export_footprint self_id expr = let ret_typ = T.Obj(Object,[{lab = "size"; typ = T.nat64; depr = None}]) in ([ letD (var v typ) ( funcE v (Shared Query) Promises [bind1] [] [ret_typ] ( - (asyncE bind2 + (asyncE T.Fut bind2 (blockE [expD (assertE (primE (I.RelPrim (caller, Operator.EqOp)) [primE I.ICCallerPrim []; selfRefE caller])); letD size (primE (I.ICStableSize expr.note.Note.typ) [expr]) @@ -720,9 +719,9 @@ and dec' at n = function let args, wrap, control, _n_res = to_args n.S.note_typ op p in let body = if s.it = T.Actor then - let (_, obj_typ) = T.as_async rng_typ in + let (_, _, obj_typ) = T.as_async rng_typ in let c = Cons.fresh T.default_scope_var (T.Abs ([], T.scope_bound)) in - asyncE (typ_arg c T.Scope T.scope_bound) + asyncE T.Fut (typ_arg c T.Scope T.scope_bound) (* TBR *) (wrap { it = obj_block at s (Some self_id) dfs (T.promote obj_typ); at = at; note = Note.{def with typ = obj_typ } }) @@ -881,12 +880,12 @@ and to_args typ po p : Ir.arg list * (Ir.exp -> Ir.exp) * T.control * T.typ list let wrap_under_async e = if T.is_shared_sort sort then match control, e.it with - | (T.Promises, Ir.AsyncE (tb, e', t)) -> - { e with it = Ir.AsyncE (tb, wrap_po e', t) } + | (T.Promises, Ir.AsyncE (s, tb, e', t)) -> + { e with it = Ir.AsyncE (s, tb, wrap_po e', t) } | T.Returns, Ir.BlockE ( - [{ it = Ir.LetD ({ it = Ir.WildP; _} as pat, ({ it = Ir.AsyncE (tb,e',t); _} as exp)); _ }], + [{ it = Ir.LetD ({ it = Ir.WildP; _} as pat, ({ it = Ir.AsyncE (T.Fut, tb,e',t); _} as exp)); _ }], ({ it = Ir.PrimE (Ir.TupPrim, []); _} as unit)) -> - blockE [letP pat {exp with it = Ir.AsyncE (tb,wrap_po e',t)} ] unit + blockE [letP pat {exp with it = Ir.AsyncE (T.Fut, tb,wrap_po e',t)} ] unit | _, Ir.ActorE _ -> wrap_po e | _ -> assert false else wrap_po e in @@ -923,11 +922,11 @@ let import_compiled_class (lib : S.comp_unit) wasm : import_declaration = let ts1' = List.map (T.open_ cs) ts1 in let ts2' = List.map (T.open_ cs) ts2 in let class_typ = match List.map T.normalize ts2' with - | [T.Async (_ , class_typ)] -> class_typ + | [T.Async (_, _, class_typ)] -> class_typ | _ -> assert false in let t_async = T.codom cntrl (fun () -> assert false) ts2' in - let _, t_actor = T.as_async (T.normalize t_async) in + let _, _, t_actor = T.as_async (T.normalize t_async) in let cs' = T.open_binds tbs in let c', _ = T.as_con (List.hd cs') in let available = fresh_var "available" T.nat in @@ -979,7 +978,7 @@ let import_compiled_class (lib : S.comp_unit) wasm : import_declaration = [typ_arg c T.Scope T.scope_bound] (List.map arg_of_var vs) ts2' - (asyncE + (asyncE T.Fut (* TBR *) (typ_arg c' T.Scope T.scope_bound) (blockE [ letD modeprincipal @@ -993,7 +992,7 @@ let import_compiled_class (lib : S.comp_unit) wasm : import_declaration = letD accepted (primE Ir.SystemCyclesAcceptPrim [varE available]); expD (assignE cycles (varE accepted)) ] (dotE - (awaitE + (awaitE T.Fut (callE (callE (varE ic00_create_canister) [] (unitE())) cs' (varE settings))) "canister_id" T.principal)]); @@ -1014,7 +1013,7 @@ let import_compiled_class (lib : S.comp_unit) wasm : import_declaration = ("wasm_module", blobE wasm); ("arg", primE (Ir.SerializePrim ts1') [seqE (List.map varE vs)]) ]); - expD (awaitE (callE (callE (varE ic00_install_code) [] (unitE()) ) cs' (varE record))) + expD (awaitE T.Fut (callE (callE (varE ic00_install_code) [] (unitE()) ) cs' (varE record))) ] (primE (Ir.CastPrim (T.principal, t_actor)) [varE principal])) (List.hd cs)) @@ -1083,7 +1082,7 @@ let transform_unit_body (u : S.comp_unit_body) : Ir.comp_unit = | T.Func(_s, _c, bds, ts1, [async_rng]) -> assert(1 = List.length bds); let cs = T.open_binds bds in - let (_, rng) = T.as_async (T.normalize (T.open_ cs async_rng)) in + let (_, _, rng) = T.as_async (T.normalize (T.open_ cs async_rng)) in List.map (T.open_ cs) ts1, T.promote rng | _ -> assert false @@ -1140,12 +1139,13 @@ let import_unit (u : S.comp_unit) : import_declaration = let c', _ = T.as_con (List.hd cs') in let body = asyncE + T.Fut (typ_arg c' T.Scope T.scope_bound) { it = I.ActorE (ds, fs, up, actor_t); at = u.at; note = Note.{ def with typ = actor_t } } (List.hd cs) in let class_typ = match List.map T.normalize ts2 with - | [ T.Async(_, t2) ] -> t2 + | [ T.Async(_, _, t2) ] -> t2 | _ -> assert false in let install_arg = fresh_var "install_arg" T.install_arg_typ @@ -1154,7 +1154,7 @@ let import_unit (u : S.comp_unit) : import_declaration = funcE id T.Local T.Returns [typ_arg c T.Scope T.scope_bound] as_ - [T.Async (List.hd cs, actor_t)] + [T.Async (T.Fut, List.hd cs, actor_t)] body in let install = @@ -1168,8 +1168,7 @@ let import_unit (u : S.comp_unit) : import_declaration = tagE "new" (recordE ["settings", nullE()]) ]) installBody (primE (Ir.OtherPrim "trap") - [textE "actor class configuration not supported in interpreter"]) - installBody.note.Note.typ) + [textE "actor class configuration not supported in interpreter"])) in actor_class_mod_exp id class_typ install | I.ProgU ds -> diff --git a/src/mo_def/arrange.ml b/src/mo_def/arrange.ml index 013256fc9c6..4a2a2634503 100644 --- a/src/mo_def/arrange.ml +++ b/src/mo_def/arrange.ml @@ -21,6 +21,7 @@ end module Type_pretty = Mo_types.Type.MakePretty (Mo_types.Type.ElideStamps) + module Make (Cfg : Config) = struct let ($$) head inner = Node (head, inner) @@ -102,8 +103,10 @@ module Make (Cfg : Config) = struct | DebugE e -> "DebugE" $$ [exp e] | BreakE (i, e) -> "BreakE" $$ [id i; exp e] | RetE e -> "RetE" $$ [exp e] - | AsyncE (tb, e) -> "AsyncE" $$ [typ_bind tb; exp e] - | AwaitE e -> "AwaitE" $$ [exp e] + | AsyncE (Type.Fut, tb, e) -> "AsyncE" $$ [typ_bind tb; exp e] + | AsyncE (Type.Cmp, tb, e) -> "AsyncE*" $$ [typ_bind tb; exp e] + | AwaitE (Type.Fut, e) -> "AwaitE" $$ [exp e] + | AwaitE (Type.Cmp, e) -> "AwaitE*" $$ [exp e] | AssertE (Runtime, e) -> "AssertE" $$ [exp e] | AssertE (Static, e) -> "Static_AssertE" $$ [exp e] | AssertE (Invariant, e) -> "Invariant" $$ [exp e] @@ -238,7 +241,8 @@ module Make (Cfg : Config) = struct | VariantT cts -> "VariantT" $$ List.map typ_tag cts | TupT ts -> "TupT" $$ List.concat_map typ_item ts | FuncT (s, tbs, at, rt) -> "FuncT" $$ [func_sort s] @ List.map typ_bind tbs @ [ typ at; typ rt] - | AsyncT (t1, t2) -> "AsyncT" $$ [typ t1; typ t2] + | AsyncT (Type.Fut, t1, t2) -> "AsyncT" $$ [typ t1; typ t2] + | AsyncT (Type.Cmp, t1, t2) -> "AsyncT*" $$ [typ t1; typ t2] | AndT (t1, t2) -> "AndT" $$ [typ t1; typ t2] | OrT (t1, t2) -> "OrT" $$ [typ t1; typ t2] | ParT t -> "ParT" $$ [typ t] diff --git a/src/mo_def/compUnit.ml b/src/mo_def/compUnit.ml index 11641fe72a8..5278c8e65e5 100644 --- a/src/mo_def/compUnit.ml +++ b/src/mo_def/compUnit.ml @@ -8,13 +8,13 @@ open Syntax let is_actor_def e = let open Source in match e.it with - | AwaitE { it = AsyncE (_, {it = ObjBlockE ({ it = Type.Actor; _}, _fields); _ }) ; _ } -> true + | AwaitE (Type.Fut, { it = AsyncE (Type.Fut, _, {it = ObjBlockE ({ it = Type.Actor; _}, _fields); _ }) ; _ }) -> true | _ -> false let as_actor_def e = let open Source in match e.it with - | AwaitE { it = AsyncE (_, {it = ObjBlockE ({ it = Type.Actor; _}, fields); note; at }) ; _ } -> + | AwaitE (Type.Fut, { it = AsyncE (Type.Fut, _, {it = ObjBlockE ({ it = Type.Actor; _}, fields); note; at }) ; _ }) -> fields, note, at | _ -> assert false diff --git a/src/mo_def/syntax.ml b/src/mo_def/syntax.ml index 6225664b5fd..21a48dc1cbc 100644 --- a/src/mo_def/syntax.ml +++ b/src/mo_def/syntax.ml @@ -37,6 +37,8 @@ and path' = | IdH of id | DotH of path * id +and async_sort = Type.async_sort + type typ = (typ', Type.typ) Source.annotated_phrase and typ' = | PathT of path * typ list (* type path *) @@ -47,7 +49,7 @@ and typ' = | VariantT of typ_tag list (* variant *) | TupT of typ_item list (* tuple *) | FuncT of func_sort * typ_bind list * typ * typ (* function *) - | AsyncT of scope * typ (* future *) + | AsyncT of async_sort * scope * typ (* future / computation *) | AndT of typ * typ (* intersection *) | OrT of typ * typ (* union *) | ParT of typ (* parentheses, used to control function arity only *) @@ -183,8 +185,8 @@ and exp' = | BreakE of id * exp (* break *) | RetE of exp (* return *) | DebugE of exp (* debugging *) - | AsyncE of typ_bind * exp (* async *) - | AwaitE of exp (* await *) + | AsyncE of async_sort * typ_bind * exp (* future / computation *) + | AwaitE of async_sort * exp (* await *) | AssertE of assert_kind * exp (* assertion *) | AnnotE of exp * typ (* type annotation *) | ImportE of (string * resolved_import ref) (* import statement *) @@ -314,13 +316,13 @@ let scopeT at = (* Expressions *) -let asyncE tbs e = - AsyncE (tbs, e) @? e.at +let asyncE sort tbs e = + AsyncE (sort, tbs, e) @? e.at let ignore_asyncE tbs e = IgnoreE ( - AnnotE (AsyncE (tbs, e) @? e.at, - AsyncT (scopeT e.at, TupT [] @! e.at) @! e.at) @? e.at ) @? e.at + AnnotE (AsyncE (Type.Fut, tbs, e) @? e.at, + AsyncT (Type.Fut, scopeT e.at, TupT [] @! e.at) @! e.at) @? e.at ) @? e.at let is_asyncE e = match e.it with @@ -330,7 +332,7 @@ let is_asyncE e = let is_ignore_asyncE e = match e.it with | IgnoreE - {it = AnnotE ({it = AsyncE _; _}, - {it = AsyncT (_, {it = TupT []; _}); _}); _} -> + {it = AnnotE ({it = AsyncE (Type.Fut, _, _); _}, + {it = AsyncT (Type.Fut, _, {it = TupT []; _}); _}); _} -> true | _ -> false diff --git a/src/mo_frontend/bi_match.ml b/src/mo_frontend/bi_match.ml index 9d8f1d39b2e..ec59e383266 100644 --- a/src/mo_frontend/bi_match.ml +++ b/src/mo_frontend/bi_match.ml @@ -175,11 +175,13 @@ let bi_match_subs scope_opt tbs subs typ_opt = | None -> None ) else None - | Async (t11, t12), Async (t21, t22) -> - (match bi_equate_typ rel eq inst any t11 t21 with - | Some inst -> - bi_match_typ rel eq inst any t12 t22 - | None -> None) + | Async (s1, t11, t12), Async (s2, t21, t22) -> + if s1 = s2 then + (match bi_equate_typ rel eq inst any t11 t21 with + | Some inst -> + bi_match_typ rel eq inst any t12 t22 + | None -> None) + else None | Mut t1', Mut t2' -> bi_equate_typ rel eq inst any t1' t2' | Typ c1, Typ c2 -> diff --git a/src/mo_frontend/definedness.ml b/src/mo_frontend/definedness.ml index 2328089a5f6..bad8c431cad 100644 --- a/src/mo_frontend/definedness.ml +++ b/src/mo_frontend/definedness.ml @@ -123,8 +123,8 @@ let rec exp msgs e : f = match e.it with | ForE (p, e1, e2) -> exp msgs e1 ++ (exp msgs e2 /// pat msgs p) | LabelE (i, t, e) -> exp msgs e | DebugE e -> exp msgs e - | AsyncE (_, e) -> exp msgs e - | AwaitE e -> exp msgs e + | AsyncE (_, _, e) -> exp msgs e + | AwaitE (_, e) -> exp msgs e | AssertE (_, e) -> exp msgs e | AnnotE (e, t) -> exp msgs e | OptE e -> exp msgs e diff --git a/src/mo_frontend/error_reporting.ml b/src/mo_frontend/error_reporting.ml index 0f8afd5b6c4..27c95fc6c17 100644 --- a/src/mo_frontend/error_reporting.ml +++ b/src/mo_frontend/error_reporting.ml @@ -109,7 +109,9 @@ let terminal2token (type a) (symbol : a terminal) : token = | T_BREAK -> BREAK | T_BOOL -> BOOL false | T_AWAIT -> AWAIT + | T_AWAITSTAR -> AWAITSTAR | T_ASYNC -> ASYNC + | T_ASYNCSTAR -> ASYNCSTAR | T_ASSIGN -> ASSIGN | T_ASSERT -> ASSERT | T_ARROW -> ARROW diff --git a/src/mo_frontend/parser.mly b/src/mo_frontend/parser.mly index 4a877a96dab..ad7b522e428 100644 --- a/src/mo_frontend/parser.mly +++ b/src/mo_frontend/parser.mly @@ -45,7 +45,7 @@ let ensure_async_typ t_opt = match t_opt with | None -> t_opt | Some { it = AsyncT _; _} -> t_opt - | Some t -> Some (AsyncT(scopeT no_region, t) @! no_region) + | Some t -> Some (AsyncT(Type.Fut, scopeT no_region, t) @! no_region) let funcT (sort, tbs, t1, t2) = match sort.it, t2.it with @@ -132,8 +132,8 @@ let desugar_func_body sp x t_opt (is_sugar, e) = false, e (* body declared as EQ e *) else (* body declared as immediate block *) match sp.it, t_opt with - | _, Some {it = AsyncT _; _} -> - true, asyncE (scope_bind x.it e.at) e + | _, Some {it = AsyncT (s, _, _); _} -> + true, asyncE s (scope_bind x.it e.at) e | Type.Shared _, (None | Some { it = TupT []; _}) -> true, ignore_asyncE (scope_bind x.it e.at) e | _, _ -> (true, e) @@ -205,7 +205,7 @@ and objblock s dec_fields = %token LET VAR %token LPAR RPAR LBRACKET RBRACKET LCURLY RCURLY -%token AWAIT ASYNC BREAK CASE CATCH CONTINUE DO LABEL DEBUG +%token AWAIT AWAITSTAR ASYNC ASYNCSTAR BREAK CASE CATCH CONTINUE DO LABEL DEBUG %token IF IGNORE IN ELSE SWITCH LOOP WHILE FOR RETURN TRY THROW WITH %token ARROW ASSIGN %token FUNC TYPE OBJECT ACTOR CLASS PUBLIC PRIVATE SHARED SYSTEM QUERY @@ -419,7 +419,9 @@ typ_pre : | PRIM s=TEXT { PrimT(s) @! at $sloc } | ASYNC t=typ_pre - { AsyncT(scopeT (at $sloc), t) @! at $sloc } + { AsyncT(Type.Fut, scopeT (at $sloc), t) @! at $sloc } + | ASYNCSTAR t=typ_pre + { AsyncT(Type.Cmp, scopeT (at $sloc), t) @! at $sloc } | s=obj_sort tfs=typ_obj { let tfs' = if s.it = Type.Actor then List.map share_typfield tfs else tfs @@ -652,9 +654,13 @@ exp_un(B) : | RETURN e=exp(ob) { RetE(e) @? at $sloc } | ASYNC e=exp_nest - { AsyncE(scope_bind (anon_id "async" (at $sloc)) (at $sloc), e) @? at $sloc } + { AsyncE(Type.Fut, scope_bind (anon_id "async" (at $sloc)) (at $sloc), e) @? at $sloc } + | ASYNCSTAR e=block + { AsyncE(Type.Cmp, scope_bind (anon_id "async*" (at $sloc)) (at $sloc), e) @? at $sloc } | AWAIT e=exp_nest - { AwaitE(e) @? at $sloc } + { AwaitE(Type.Fut, e) @? at $sloc } + | AWAITSTAR e=exp_nest + { AwaitE(Type.Cmp, e) @? at $sloc } | ASSERT e=exp_nest { AssertE(Runtime, e) @? at $sloc } | LABEL x=id rt=annot_opt e=exp_nest @@ -705,7 +711,6 @@ exp_un(B) : | DO QUEST e=block { DoOptE(e) @? at $sloc } - exp_nonvar(B) : | e=exp_nondec(B) { e } @@ -840,7 +845,8 @@ dec_nonvar : let e = if s.it = Type.Actor then AwaitE - (AsyncE(scope_bind (anon_id "async" (at $sloc)) (at $sloc), + (Type.Fut, + AsyncE(Type.Fut, scope_bind (anon_id "async" (at $sloc)) (at $sloc), (objblock s (List.map share_dec_field efs) @? (at $sloc))) @? at $sloc) else objblock s efs diff --git a/src/mo_frontend/printers.ml b/src/mo_frontend/printers.ml index f8bb52ed9d3..3437cb8c528 100644 --- a/src/mo_frontend/printers.ml +++ b/src/mo_frontend/printers.ml @@ -124,7 +124,9 @@ let string_of_symbol = function | X (T T_BREAK) -> "break" | X (T T_BOOL) -> "" | X (T T_AWAIT) -> "await" + | X (T T_AWAITSTAR) -> "await*" | X (T T_ASYNC) -> "async" + | X (T T_ASYNCSTAR) -> "async*" | X (T T_ASSIGN) -> binassign "assign" | X (T T_ASSERT) -> "assert" | X (T T_ARROW) -> "->" diff --git a/src/mo_frontend/source_lexer.mll b/src/mo_frontend/source_lexer.mll index 479bcf53ce6..7d40d79e8cc 100644 --- a/src/mo_frontend/source_lexer.mll +++ b/src/mo_frontend/source_lexer.mll @@ -196,19 +196,23 @@ rule token mode = parse | "actor" { ACTOR } | "and" { AND } | "async" { ASYNC } + | "async*" { ASYNCSTAR } | "assert" { ASSERT } | "await" { AWAIT } + | "await*" { AWAITSTAR } | "break" { BREAK } | "case" { CASE } | "catch" { CATCH } | "class" { CLASS } | "continue" { CONTINUE } | "debug" { DEBUG } + | "debug_show" { DEBUG_SHOW } | "do" { DO } | "else" { ELSE } | "false" { BOOL false } | "flexible" { FLEXIBLE } | "for" { FOR } + | "from_candid" { FROM_CANDID } | "func" { FUNC } | "if" { IF } | "ignore" { IGNORE } @@ -226,22 +230,20 @@ rule token mode = parse | "loop" { LOOP } | "private" { PRIVATE } | "public" { PUBLIC } + | "query" { QUERY } | "return" { RETURN } | "shared" { SHARED } | "stable" { STABLE } + | "switch" { SWITCH } | "system" { SYSTEM } | "try" { TRY } | "throw" { THROW } - | "with" { WITH } - | "debug_show" { DEBUG_SHOW } | "to_candid" { TO_CANDID } - | "from_candid" { FROM_CANDID } - | "query" { QUERY } - | "switch" { SWITCH } | "true" { BOOL true } | "type" { TYPE } | "var" { VAR } | "while" { WHILE } + | "with" { WITH } | "prim" as s { if mode.privileged then PRIM else ID s } | id as s { ID s } diff --git a/src/mo_frontend/source_token.ml b/src/mo_frontend/source_token.ml index ffb647e68e1..728f93ed1e0 100644 --- a/src/mo_frontend/source_token.ml +++ b/src/mo_frontend/source_token.ml @@ -12,7 +12,9 @@ type token = | LCURLY | RCURLY | AWAIT + | AWAITSTAR | ASYNC + | ASYNCSTAR | BREAK | CASE | CATCH @@ -136,7 +138,9 @@ let to_parser_token : | LCURLY -> Ok Parser.LCURLY | RCURLY -> Ok Parser.RCURLY | AWAIT -> Ok Parser.AWAIT + | AWAITSTAR -> Ok Parser.AWAITSTAR | ASYNC -> Ok Parser.ASYNC + | ASYNCSTAR -> Ok Parser.ASYNCSTAR | BREAK -> Ok Parser.BREAK | CASE -> Ok Parser.CASE | CATCH -> Ok Parser.CATCH @@ -259,7 +263,9 @@ let string_of_parser_token = function | Parser.LCURLY -> "LCURLY" | Parser.RCURLY -> "RCURLY" | Parser.AWAIT -> "AWAIT" + | Parser.AWAITSTAR -> "AWAIT*" | Parser.ASYNC -> "ASYNC" + | Parser.ASYNCSTAR -> "ASYNC*" | Parser.BREAK -> "BREAK" | Parser.CASE -> "CASE" | Parser.CATCH -> "CATCH" diff --git a/src/mo_frontend/static.ml b/src/mo_frontend/static.ml index 8d8b54b9b5d..9762b6fc467 100644 --- a/src/mo_frontend/static.ml +++ b/src/mo_frontend/static.ml @@ -69,7 +69,7 @@ let rec exp m e = match e.it with | LabelE _ | BreakE _ | RetE _ - | AsyncE _ + | AsyncE _ (* TBR - Cmp could be static *) | AwaitE _ | LoopE _ | BinE _ diff --git a/src/mo_frontend/traversals.ml b/src/mo_frontend/traversals.ml index 86ba96bd143..979a0e55b73 100644 --- a/src/mo_frontend/traversals.ml +++ b/src/mo_frontend/traversals.ml @@ -20,8 +20,8 @@ let rec over_exp (f : exp -> exp) (exp : exp) : exp = match exp.it with | BreakE (x, exp1) -> f { exp with it = BreakE (x, over_exp f exp1) } | RetE exp1 -> f { exp with it = RetE (over_exp f exp1) } | AnnotE (exp1, x) -> f { exp with it = AnnotE (over_exp f exp1, x) } - | AsyncE (tb, exp1) -> f { exp with it = AsyncE (tb, over_exp f exp1) } - | AwaitE exp1 -> f { exp with it = AwaitE (over_exp f exp1) } + | AsyncE (s, tb, exp1) -> f { exp with it = AsyncE (s, tb, over_exp f exp1) } + | AwaitE (s, exp1) -> f { exp with it = AwaitE (s, over_exp f exp1) } | ThrowE exp1 -> f { exp with it = ThrowE (over_exp f exp1) } | BinE (x, exp1, y, exp2) -> f { exp with it = BinE (x, over_exp f exp1, y, over_exp f exp2) } diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index b15b8c7bcb7..be3b1196848 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -209,7 +209,8 @@ let infer_mut mut : T.typ -> T.typ = let system_funcs tfs = [ - ("heartbeat", T.Func (T.Local, T.Returns, [T.scope_bind], [], [T.Async (T.Var (T.default_scope_var, 0), T.unit)])); + ("heartbeat", T.Func (T.Local, T.Returns, [T.scope_bind], [], + [T.Async (T.Fut, T.Var (T.default_scope_var, 0), T.unit)])); ("preupgrade", T.Func (T.Local, T.Returns, [], [], [])); ("postupgrade", T.Func (T.Local, T.Returns, [], [], [])); ("inspect", @@ -336,7 +337,7 @@ let as_domT t = let as_codomT sort t = match sort, t.Source.it with - | T.Shared _, AsyncT (_, t1) -> + | T.Shared _, AsyncT (T.Fut, _, t1) -> T.Promises, as_domT t1 | _ -> T.Returns, as_domT t @@ -503,14 +504,14 @@ and check_typ' env typ : T.typ = (List.map (fun (tag : typ_tag) -> tag.it.tag) tags); let fs = List.map (check_typ_tag env) tags in T.Variant (List.sort T.compare_field fs) - | AsyncT (typ0, typ) -> + | AsyncT (s, typ0, typ) -> let t0 = check_typ env typ0 in let t = check_typ env typ in if not env.pre && not (T.shared t) then error_shared env t typ.at "M0033" "async has non-shared content type%a" display_typ_expand t; - T.Async (t0, t) + T.Async (s, t0, t) | ObjT (sort, fields) -> check_ids env "object type" "field" (List.filter_map (fun (field : typ_field) -> @@ -762,7 +763,7 @@ let rec is_explicit_exp e = | LitE l -> is_explicit_lit !l | UnE (_, _, e1) | OptE e1 | DoOptE e1 | ProjE (e1, _) | DotE (e1, _) | BangE e1 | IdxE (e1, _) | CallE (e1, _, _) - | LabelE (_, _, e1) | AsyncE (_, e1) | AwaitE e1 -> + | LabelE (_, _, e1) | AsyncE (_, _, e1) | AwaitE (_, e1) -> is_explicit_exp e1 | BinE (_, e1, _, e2) | IfE (_, e1, e2) -> is_explicit_exp e1 || is_explicit_exp e2 @@ -1406,7 +1407,7 @@ and infer_exp'' env exp : T.typ = check_exp_strong env T.throw exp1 end; T.Non - | AsyncE (typ_bind, exp1) -> + | AsyncE (s, typ_bind, exp1) -> error_in [Flags.WASIMode; Flags.WasmMode] env exp1.at "M0086" "async expressions are not supported"; let t1, next_cap = check_AsyncCap env "async expression" exp.at in @@ -1423,12 +1424,12 @@ and infer_exp'' env exp : T.typ = if not (T.shared t') then error_shared env t' exp1.at "M0033" "async type has non-shared content type%a" display_typ_expand t'; - T.Async (t1, t') - | AwaitE exp1 -> + T.Async (s, t1, t') + | AwaitE (s, exp1) -> let t0 = check_AwaitCap env "await" exp.at in let t1 = infer_exp_promote env exp1 in (try - let (t2, t3) = T.as_async_sub t0 t1 in + let (t2, t3) = T.as_async_sub s t0 t1 in if not (T.eq t0 t2) then begin local_error env exp1.at "M0087" "ill-scoped await: expected async type from current scope %s, found async type from other scope %s%s%s" @@ -1440,10 +1441,17 @@ and infer_exp'' env exp : T.typ = scope_info env t2 exp.at; end; t3 - with Invalid_argument _ -> - error env exp1.at "M0088" - "expected async type, but expression has type%a" - display_typ_expand t1 + with Invalid_argument _ -> + error env exp1.at "M0088" + "expected async%s type, but expression has type%a%s" + (if s = T.Fut then "" else "*") + display_typ_expand t1 + (if T.is_async t1 then + (if s = T.Fut then + "\nUse keyword 'await*' (not 'await') to consume this type." + else + "\nUse keyword 'await' (not 'await*') to consume this type.") + else "") ) | AssertE (_, exp1) -> if not env.pre then check_exp_strong env T.bool exp1; @@ -1575,10 +1583,19 @@ and check_exp' env0 t exp : T.typ = display_typ_expand (T.Array t'); List.iter (check_exp env (T.as_immut t')) exps; t - | AsyncE (tb, exp1), T.Async (t1', t') -> + | AsyncE (s1, tb, exp1), T.Async (s2, t1', t') -> error_in [Flags.WASIMode; Flags.WasmMode] env exp1.at "M0086" "async expressions are not supported"; let t1, next_cap = check_AsyncCap env "async expression" exp.at in + if s1 <> s2 then begin + local_error env exp.at "M0183" + "async expression cannot produce expected async type %a.\n%s" + display_typ_expand t + (if s2 = T.Fut then + "Use keyword 'async' (not 'async*') to produce the expected type." + else + "Use keyword 'async*' (not 'async') to produce the expected type.") + end; if not (T.eq t1 t1') then begin local_error env exp.at "M0092" "async at scope%a\ncannot produce expected scope%a%s%s" @@ -2341,7 +2358,7 @@ and infer_dec env dec : T.typ = let t' = infer_obj env''' obj_sort.it dec_fields dec.at in match typ_opt, obj_sort.it with | None, _ -> () - | Some { it = AsyncT (_, typ); at; _ }, T.Actor + | Some { it = AsyncT (T.Fut, _, typ); at; _ }, T.Actor | Some ({ at; _ } as typ), (T.Module | T.Object) -> if at = Source.no_region then warn env dec.at "M0135" @@ -2433,7 +2450,7 @@ and gather_dec env scope dec : Scope.t = | LetD ( {it = VarP id; _}, ({it = ObjBlockE (obj_sort, dec_fields); at; _} | - {it = AwaitE { it = AsyncE (_, {it = ObjBlockE ({ it = Type.Actor; _} as obj_sort, dec_fields); at; _}) ; _ }; _ }) + {it = AwaitE (_,{ it = AsyncE (_, _, {it = ObjBlockE ({ it = Type.Actor; _} as obj_sort, dec_fields); at; _}) ; _ }); _ }) ) -> let decs = List.map (fun df -> df.it.dec) dec_fields in let open Scope in @@ -2515,7 +2532,7 @@ and infer_dec_typdecs env dec : Scope.t = | LetD ( {it = VarP id; _}, ( {it = ObjBlockE (obj_sort, dec_fields); at; _} | - {it = AwaitE { it = AsyncE (_, {it = ObjBlockE ({ it = Type.Actor; _} as obj_sort, dec_fields); at; _}) ; _ }; _ }) + {it = AwaitE (_, { it = AsyncE (_, _, {it = ObjBlockE ({ it = Type.Actor; _} as obj_sort, dec_fields); at; _}) ; _ }); _ }) ) -> let decs = List.map (fun {it = {vis; dec; _}; _} -> dec) dec_fields in let scope = T.Env.find id.it env.objs in @@ -2596,7 +2613,7 @@ and infer_dec_valdecs env dec : Scope.t = | LetD ( {it = VarP id; _} as pat, ( {it = ObjBlockE (obj_sort, dec_fields); at; _} | - {it = AwaitE { it = AsyncE (_, {it = ObjBlockE ({ it = Type.Actor; _} as obj_sort, dec_fields); at; _}) ; _ }; _ }) + {it = AwaitE (_, { it = AsyncE (_, _, {it = ObjBlockE ({ it = Type.Actor; _} as obj_sort, dec_fields); at; _}) ; _ }); _ }) ) -> let decs = List.map (fun df -> df.it.dec) dec_fields in let obj_scope = T.Env.find id.it env.objs in @@ -2638,7 +2655,7 @@ and infer_dec_valdecs env dec : Scope.t = let ts1 = match pat.it with TupP _ -> T.seq_of_tup t1 | _ -> [t1] in let t2 = if obj_sort.it = T.Actor then - T.Async (T.Con (List.hd cs, []), + T.Async (T.Fut, T.Con (List.hd cs, []), T.Con (c, List.map (fun c -> T.Con (c, [])) (List.tl cs))) else T.Con (c, List.map (fun c -> T.Con (c, [])) cs) @@ -2726,7 +2743,7 @@ let check_lib scope lib : Scope.t Diag.result = | T.Func (sort, control, _, ts1, [t2]) -> let t2 = T.normalize (T.open_ ts t2) in (match t2 with - | T.Async (_ , class_typ) -> List.map (T.open_ ts) ts1, class_typ + | T.Async (_, _, class_typ) -> List.map (T.open_ ts) ts1, class_typ | _ -> assert false) | _ -> assert false in diff --git a/src/mo_frontend/variance.ml b/src/mo_frontend/variance.ml index 2482229c645..574381c865e 100644 --- a/src/mo_frontend/variance.ml +++ b/src/mo_frontend/variance.ml @@ -61,7 +61,7 @@ let variances cons t = | Def (_, t) -> go p (open_ ts t)) (* TBR this may fail to terminate *) | Array t | Opt t -> go p t | Mut t -> go Invariant t - | Async (t1, t2) -> + | Async (s, t1, t2) -> go Invariant t1; go p t2 | Tup ts -> List.iter (go p) ts diff --git a/src/mo_idl/mo_to_idl.ml b/src/mo_idl/mo_to_idl.ml index 98506365b9a..5ff38aa4ce8 100644 --- a/src/mo_idl/mo_to_idl.ml +++ b/src/mo_idl/mo_to_idl.ml @@ -187,7 +187,7 @@ let actor progs = (match normalize cub.note.note_typ with | Func (Local, Returns, [tb], ts1, [t2]) -> let args = List.map typ (List.map (open_ [Non]) ts1) in - let (_, rng) = as_async (normalize (open_ [Non] t2)) in + let (_, _, rng) = as_async (normalize (open_ [Non] t2)) in let actor = typ rng in Some (I.ClassT (args, actor) @@ cub.at) | _ -> assert false diff --git a/src/mo_interpreter/interpret.ml b/src/mo_interpreter/interpret.ml index f920d8c2799..48261f47afd 100644 --- a/src/mo_interpreter/interpret.ml +++ b/src/mo_interpreter/interpret.ml @@ -644,16 +644,23 @@ and interpret_exp_mut env exp (k : V.value V.cont) = interpret_exp env exp1 (Option.get env.rets) | ThrowE exp1 -> interpret_exp env exp1 (Option.get env.throws) - | AsyncE (_, exp1) -> + | AsyncE (T.Fut, _, exp1) -> async env exp.at (fun k' r -> let env' = {env with labs = V.Env.empty; rets = Some k'; throws = Some r} in interpret_exp env' exp1 k') k - | AwaitE exp1 -> + | AsyncE (T.Cmp, _, exp1) -> + k (V.Comp (fun k' r -> + let env' = {env with labs = V.Env.empty; rets = Some k'; throws = Some r} + in interpret_exp env' exp1 k')) + | AwaitE (T.Fut, exp1) -> interpret_exp env exp1 (fun v1 -> await env exp.at (V.as_async v1) k) + | AwaitE (T.Cmp, exp1) -> + interpret_exp env exp1 + (fun v1 -> (V.as_comp v1) k (Option.get env.throws)) | AssertE (Runtime, exp1) -> interpret_exp env exp1 (fun v -> if V.as_bool v diff --git a/src/mo_types/arrange_type.ml b/src/mo_types/arrange_type.ml index a1ba6ca645c..b0bf73b8201 100644 --- a/src/mo_types/arrange_type.ml +++ b/src/mo_types/arrange_type.ml @@ -53,7 +53,8 @@ let rec typ = function | Func (s, c, tbs, at, rt) -> "Func" $$ [Atom (func_sort s); Atom (control c)] @ List.map typ_bind tbs @ [ "" $$ (List.map typ at); "" $$ (List.map typ rt)] - | Async (t1, t2) -> "Async" $$ [typ t1; typ t2] + | Async (Fut, t1, t2) -> "Async" $$ [typ t1; typ t2] + | Async (Cmp, t1, t2) -> "Async*" $$ [typ t1; typ t2] | Mut t -> "Mut" $$ [typ t] | Any -> Atom "Any" | Non -> Atom "Non" diff --git a/src/mo_types/expansive.ml b/src/mo_types/expansive.ml index 09c77c48797..86c42c5dd57 100644 --- a/src/mo_types/expansive.ml +++ b/src/mo_types/expansive.ml @@ -109,7 +109,7 @@ let edges_typ cs c (es : EdgeSet.t) t : EdgeSet.t = go_typs i (VertexSet.union exp non) VertexSet.empty es ts | (Opt t1 | Mut t1 | Array t1) -> go_typ i (VertexSet.union exp non) VertexSet.empty es t1 - | Async (t1, t2) -> + | Async (s, t1, t2) -> go_typs i (VertexSet.union exp non) VertexSet.empty es [t1;t2] | Func (s, _c, tbs, ts1, ts2) -> let i1 = i + List.length tbs in diff --git a/src/mo_types/type.ml b/src/mo_types/type.ml index f2b8d190b28..f4e96f00f7e 100644 --- a/src/mo_types/type.ml +++ b/src/mo_types/type.ml @@ -13,6 +13,7 @@ type obj_sort = | Module | Memory (* (codegen only): stable memory serialization format *) +type async_sort = Fut | Cmp type shared_sort = Query | Write type 'a shared = Local | Shared of 'a type func_sort = shared_sort shared @@ -49,7 +50,7 @@ and typ = | Opt of typ (* option *) | Tup of typ list (* tuple *) | Func of func_sort * control * bind list * typ list * typ list (* function *) - | Async of scope * typ (* future *) + | Async of async_sort * scope * typ (* future *) | Mut of typ (* mutable type *) | Any (* top *) | Non (* bottom *) @@ -129,6 +130,13 @@ let compare_control c1 c2 = let d = tag_control c1 - tag_control c2 in if d > 0 then 1 else if d < 0 then -1 else 0 +let compare_async_sort s1 s2 = + match s1, s2 with + | Fut, Fut + | Cmp, Cmp -> 0 + | Fut, Cmp -> -1 + | Cmp, Fut -> 1 + let compare_obj_sort s1 s2 = let d = tag_obj_sort s1 - tag_obj_sort s2 in if d > 0 then 1 else if d < 0 then -1 else 0 @@ -183,9 +191,11 @@ let rec compare_typ (t1 : typ) (t2 : typ) = | ord -> ord) | ord -> ord) | Opt t1, Opt t2 -> compare_typ t1 t2 - | Async (t11, t12) , Async (t21, t22) -> - (match compare_typ t11 t21 with - | 0 -> compare_typ t12 t22 + | Async (s1, t11, t12) , Async (s2, t21, t22) -> + (match compare_async_sort s1 s2 with + | 0 -> (match compare_typ t11 t21 with + | 0 -> compare_typ t12 t22 + | ord -> ord) | ord -> ord) | Obj (s1, fs1), Obj (s2, fs2) -> (match compare_obj_sort s1 s2 with @@ -277,6 +287,7 @@ let set_kind c k = | _ -> raise (Invalid_argument "set_kind") module ConEnv = Env.Make(struct type t = con let compare = Cons.compare end) + module ConSet = ConEnv.Dom @@ -358,7 +369,7 @@ let prim = function let seq = function [t] -> t | ts -> Tup ts let codom c to_scope ts2 = match c with - | Promises -> Async (to_scope(), seq ts2) + | Promises -> Async (Fut, to_scope(), seq ts2) | Returns -> seq ts2 | Replies -> Tup [] @@ -382,7 +393,7 @@ let rec shift i n t = let i' = i + List.length tbs in Func (s, c, List.map (shift_bind i' n) tbs, List.map (shift i' n) ts1, List.map (shift i' n) ts2) | Opt t -> Opt (shift i n t) - | Async (t1, t2) -> Async (shift i n t1, shift i n t2) + | Async (s, t1, t2) -> Async (s, shift i n t1, shift i n t2) | Obj (s, fs) -> Obj (s, List.map (shift_field n i) fs) | Variant fs -> Variant (List.map (shift_field n i) fs) | Mut t -> Mut (shift i n t) @@ -428,7 +439,7 @@ let rec subst sigma t = Func (s, c, List.map (subst_bind sigma') tbs, List.map (subst sigma') ts1, List.map (subst sigma') ts2) | Opt t -> Opt (subst sigma t) - | Async (t1, t2) -> Async (subst sigma t1, subst sigma t2) + | Async (s, t1, t2) -> Async (s, subst sigma t1, subst sigma t2) | Obj (s, fs) -> Obj (s, List.map (subst_field sigma) fs) | Variant fs -> Variant (List.map (subst_field sigma) fs) | Mut t -> Mut (subst sigma t) @@ -483,7 +494,7 @@ let rec open' i ts t = let i' = i + List.length tbs in Func (s, c, List.map (open_bind i' ts) tbs, List.map (open' i' ts) ts1, List.map (open' i' ts) ts2) | Opt t -> Opt (open' i ts t) - | Async (t1, t2) -> Async (open' i ts t1, open' i ts t2) + | Async (s, t1, t2) -> Async (s, open' i ts t1, open' i ts t2) | Obj (s, fs) -> Obj (s, List.map (open_field i ts) fs) | Variant fs -> Variant (List.map (open_field i ts) fs) | Mut t -> Mut (open' i ts t) @@ -573,7 +584,7 @@ let as_tup = function Tup ts -> ts | _ -> invalid "as_tup" let as_unit = function Tup [] -> () | _ -> invalid "as_unit" let as_pair = function Tup [t1; t2] -> t1, t2 | _ -> invalid "as_pair" let as_func = function Func (s, c, tbs, ts1, ts2) -> s, c, tbs, ts1, ts2 | _ -> invalid "as_func" -let as_async = function Async (t1, t2) -> (t1, t2) | _ -> invalid "as_async" +let as_async = function Async (s, t1, t2) -> (s, t1, t2) | _ -> invalid "as_async" let as_mut = function Mut t -> t | _ -> invalid "as_mut" let as_immut = function Mut t -> t | t -> t let as_typ = function Typ c -> c | _ -> invalid "as_typ" @@ -636,8 +647,8 @@ let as_mono_func_sub t = match promote t with | Func (_, _, [], ts1, ts2) -> seq ts1, seq ts2 | Non -> Any, Non | _ -> invalid "as_func_sub" -let as_async_sub default_scope t = match promote t with - | Async (t1, t2) -> (t1, t2) +let as_async_sub s default_scope t = match promote t with + | Async (s0, t1, t2) when s = s0 -> (t1, t2) | Non -> default_scope, Non (* TBR *) | _ -> invalid "as_async_sub" @@ -716,7 +727,7 @@ let rec cons' inTyp t cs = List.fold_right (cons' inTyp) ts (cons_con inTyp c cs) | Opt t | Mut t | Array t -> cons' inTyp t cs - | Async (t1, t2) -> + | Async (_, t1, t2) -> cons' inTyp t2 (cons' inTyp t1 cs) | Tup ts -> List.fold_right (cons' inTyp) ts cs | Func (s, c, tbs, ts1, ts2) -> @@ -776,7 +787,7 @@ let concrete t = | Def (_, t) -> go (open_ ts t) (* TBR this may fail to terminate *) ) | Array t | Opt t | Mut t -> go t - | Async (t1, t2) -> go t2 (* t1 is a phantom type *) + | Async (s, t1, t2) -> go t2 (* t1 is a phantom type *) | Tup ts -> List.for_all go ts | Obj (_, fs) | Variant fs -> List.for_all (fun f -> go f.typ) fs | Func (s, c, tbs, ts1, ts2) -> @@ -950,7 +961,8 @@ let rec rel_typ rel eq t1 t2 = rel_list rel_typ rel eq (List.map (open_ ts) t12) (List.map (open_ ts) t22) | None -> false ) - | Async (t11, t12), Async (t21, t22) -> + | Async (s1, t11, t12), Async (s2, t21, t22) -> + s1 = s2 && eq_typ rel eq t11 t21 && rel_typ rel eq t12 t22 | _, _ -> false @@ -1080,7 +1092,8 @@ let rec compatible_typ co t1 t2 = true | Variant tfs1, Variant tfs2 -> compatible_tags co tfs1 tfs2 - | Async (t11, t12), Async (t21, t22) -> + | Async (s1, t11, t12), Async (s2, t21, t22) -> + s1 = s2 && compatible_typ co t11 t21 && (* TBR *) compatible_typ co t12 t22 | Func _, Func _ -> @@ -1222,8 +1235,8 @@ let rec combine rel lubs glbs t1 t2 = closed (List.map2 (combine rel' lubs glbs) (opened ts11) (opened ts21)), closed (List.map2 (combine rel lubs glbs) (opened ts12) (opened ts22)) ) - | Async (t11, t12), Async (t21, t22) when eq t11 t21 -> - Async (t11, combine rel lubs glbs t12 t22) + | Async (s1, t11, t12), Async (s2, t21, t22) when s1 == s2 && eq t11 t21 -> + Async (s1, t11, combine rel lubs glbs t12 t22) | Con _, _ | _, Con _ -> if sub t1 t2 then @@ -1362,11 +1375,15 @@ let install_arg_typ = let install_typ ts actor_typ = Func(Local, Returns, [], [ install_arg_typ ], - [ Func(Local, Returns, [scope_bind], ts, [Async (Var (default_scope_var, 0), actor_typ)]) ]) + [ Func(Local, Returns, [scope_bind], ts, [Async (Fut, Var (default_scope_var, 0), actor_typ)]) ]) (* Pretty printing *) +let string_of_async_sort = function + | Fut -> "" + | Cmp -> "*" + let string_of_prim = function | Null -> "Null" | Bool -> "Bool" @@ -1448,7 +1465,7 @@ let string_of_con c = Cons.to_string Cfg.show_stamps Cfg.con_sep c let rec can_sugar = function | Func(s, Promises, tbs, ts1, ts2) | Func((Shared _ as s), Returns, tbs, ts1, ([] as ts2)) - | Func(s, Returns, tbs, ts1, ([Async (Var(_, 0),_)] as ts2)) -> + | Func(s, Returns, (_::_ as tbs), ts1, ([Async (_, Var(_, 0),_)] as ts2)) -> List.for_all (fun tb -> can_omit 0 tb.bound) tbs && List.for_all (can_omit 0) ts1 && List.for_all (can_omit 0) ts2 @@ -1461,8 +1478,8 @@ and can_omit n t = | Prim _ | Any | Non -> true | Con (c, ts) -> List.for_all (go i ) ts | Array t | Opt t | Mut t -> go i t - | Async (Var (_, j), t2) when j = i && i <= n -> go i t2 (* t1 is a phantom type *) - | Async (t1, t2) -> go i t1 && go i t2 + | Async (s, Var (_, j), t2) when j = i && i <= n -> go i t2 (* t1 is a phantom type *) + | Async (s, t1, t2) -> go i t1 && go i t2 | Tup ts -> List.for_all (go i ) ts | Obj (_, fs) | Variant fs -> List.for_all (fun f -> go i f.typ) fs | Func (s, c, tbs, ts1, ts2) -> @@ -1528,16 +1545,17 @@ and pp_typ_un vs ppf t = and pp_typ_pre vs ppf t = match t with (* No case for grammar production `PRIM s` *) - | Async (t1, t2) -> + | Async (s, t1, t2) -> if Cfg.show_stamps then match t1 with | Var(_, n) when fst (List.nth vs n) = "" -> - fprintf ppf "@[<2>async@ %a@]" (pp_typ_pre vs) t2 + fprintf ppf "@[<2>async%s@ %a@]" (string_of_async_sort s) (pp_typ_pre vs) t2 | _ -> - fprintf ppf "@[<2>async<%a>@ %a@]" + fprintf ppf "@[<2>async%s<%a>@ %a@]" + (string_of_async_sort s) (pp_typ' vs) t1 (pp_typ_pre vs) t2 - else fprintf ppf "@[<2>async@ %a@]" (pp_typ_pre vs) t2 + else fprintf ppf "@[<2>async%s@ %a@]" (string_of_async_sort s) (pp_typ_pre vs) t2 | Obj ((Module | Actor | Memory) as os, fs) -> pp_typ_obj vs ppf (os, fs) | t -> @@ -1573,8 +1591,8 @@ and pp_typ_nobin vs ppf t = and pp_control_cod sugar c vs ppf ts = match c, ts with (* sugar *) - | Returns, [Async (_,t)] when sugar -> - fprintf ppf "@[<2>async@ %a@]" (pp_typ_pre vs) t + | Returns, [Async (s, _, t)] when sugar -> + fprintf ppf "@[<2>async%s@ %a@]" (string_of_async_sort s) (pp_typ_pre vs) t | Promises, ts -> fprintf ppf "@[<2>async@ %a@]" (sequence (pp_typ_pre vs)) ts | Returns, _ -> diff --git a/src/mo_types/type.mli b/src/mo_types/type.mli index a78774885bf..489694842fd 100644 --- a/src/mo_types/type.mli +++ b/src/mo_types/type.mli @@ -5,6 +5,7 @@ type var = string type control = Returns | Promises | Replies type obj_sort = Object | Actor | Module | Memory +type async_sort = Fut | Cmp type shared_sort = Query | Write type 'a shared = Local | Shared of 'a type func_sort = shared_sort shared @@ -42,7 +43,7 @@ and typ = | Opt of typ (* option *) | Tup of typ list (* tuple *) | Func of func_sort * control * bind list * typ list * typ list (* function *) - | Async of scope * typ (* future *) + | Async of async_sort * scope * typ (* future / computation *) | Mut of typ (* mutable type *) | Any (* top *) | Non (* bottom *) @@ -134,7 +135,7 @@ val as_tup : typ -> typ list val as_unit : typ -> unit val as_pair : typ -> typ * typ val as_func : typ -> func_sort * control * bind list * typ list * typ list -val as_async : typ -> typ * typ +val as_async : typ -> async_sort * typ * typ val as_mut : typ -> typ val as_immut : typ -> typ val as_typ : typ -> con @@ -150,7 +151,7 @@ val as_unit_sub : typ -> unit val as_pair_sub : typ -> typ * typ val as_func_sub : func_sort -> int -> typ -> func_sort * bind list * typ * typ val as_mono_func_sub : typ -> typ * typ -val as_async_sub : typ -> typ -> typ * typ +val as_async_sub : async_sort -> typ -> typ -> typ * typ (* Argument/result sequences *) diff --git a/src/mo_values/value.ml b/src/mo_values/value.ml index 1bc756d117b..eb342bbce23 100644 --- a/src/mo_values/value.ml +++ b/src/mo_values/value.ml @@ -28,6 +28,9 @@ type context = value and func = context -> value -> value cont -> unit +and comp = + value cont -> value cont -> unit + and value = | Null | Bool of bool @@ -51,6 +54,7 @@ and value = | Obj of value Env.t | Func of Call_conv.t * func | Async of async + | Comp of comp | Mut of value ref | Iter of value Seq.t ref (* internal to {b.vals(), t.chars()} iterator *) @@ -100,6 +104,7 @@ let as_pair = function Tup [v1; v2] -> v1, v2 | _ -> invalid "as_pair" let as_obj = function Obj ve -> ve | _ -> invalid "as_obj" let as_func = function Func (cc, f) -> cc, f | _ -> invalid "as_func" let as_async = function Async a -> a | _ -> invalid "as_async" +let as_comp = function Comp c -> c | _ -> invalid "as_comp" let as_mut = function Mut r -> r | _ -> invalid "as_mut" @@ -130,11 +135,11 @@ let rec compare x1 x2 = ) | Mut r1, Mut r2 -> compare !r1 !r2 | Async _, Async _ -> raise (Invalid_argument "Value.compare") + | Comp _, Comp _ -> raise (Invalid_argument "Value.compare") | _ -> generic_compare x1 x2 let equal x1 x2 = compare x1 x2 = 0 - (* (Pseudo)-Identities (for caller and self) *) let next_id = ref 0 @@ -202,6 +207,7 @@ let rec pp_val_nullary d ppf = function fprintf ppf "@[<1>[%a]@]" (pp_print_list ~pp_sep:comma (pp_val d)) (Array.to_list a) | Func (_, _) -> pr ppf "func" + | Comp _ -> pr ppf "async*" | v -> (* "(" ^ string_of_val d v ^ ")" *) fprintf ppf "@[<1>(%a)@]" (pp_val d) v diff --git a/src/mo_values/value.mli b/src/mo_values/value.mli index 7908d75d2cf..d8a957da570 100644 --- a/src/mo_values/value.mli +++ b/src/mo_values/value.mli @@ -18,7 +18,10 @@ type actor_id = string type context = value and func = - context -> value -> value cont -> unit + context -> value -> value cont -> unit + +and comp = + value cont -> value cont -> unit and value = | Null @@ -43,6 +46,7 @@ and value = | Obj of value Env.t | Func of Call_conv.t * func | Async of async + | Comp of comp | Mut of value ref | Iter of value Seq.t ref (* internal to {b.vals(), t.chars()} iterator *) @@ -96,6 +100,7 @@ val as_obj : value -> value Env.t val as_variant : value -> string * value val as_func : value -> Call_conv.t * func val as_async : value -> async +val as_comp : value -> comp val as_mut : value -> value ref diff --git a/src/pipeline/pipeline.ml b/src/pipeline/pipeline.ml index eaeabf1b0ec..93a52c73bc5 100644 --- a/src/pipeline/pipeline.ml +++ b/src/pipeline/pipeline.ml @@ -623,7 +623,7 @@ let await_lowering = transform_if "Await Lowering" Await.transform let async_lowering mode = - transform_if "Async Lowering" (Async.transform mode) + transform_if "Async Lowering" Async.transform let tailcall_optimization = transform_if "Tailcall optimization" Tailcall.transform diff --git a/src/prelude/internals.mo b/src/prelude/internals.mo index 7f70ce5d8bc..b97e6ab85fb 100644 --- a/src/prelude/internals.mo +++ b/src/prelude/internals.mo @@ -283,7 +283,10 @@ func @equal_array(eq : (T, T) -> Bool, a : [T], b : [T]) : Bool { }; type @Cont = T -> () ; -type @Async = (@Cont,@Cont) -> ?(() -> ()); +type @Async = (@Cont,@Cont) -> { + #suspend; + #schedule : () -> (); +}; type @Refund = Nat; type @Result = {#ok : (refund : @Refund, value: T); #error : Error}; @@ -336,7 +339,10 @@ func @new_async() : (@Async, @Cont, @Cont) { }; }; - func enqueue(k : @Cont, r : @Cont) : ?(() -> ()) { + func enqueue(k : @Cont, r : @Cont) : { + #suspend; + #schedule : () -> (); + } { switch result { case null { let ws_ = ws; @@ -351,14 +357,15 @@ func @new_async() : (@Async, @Cont, @Cont) { rs_(e); @reset_cycles(); @reset_refund(); - r(e) }; - null + r(e) + }; + #suspend }; case (? (#ok (r, t))) { - ? (func () { @refund := r; k(t) }); + #schedule (func () { @refund := r; k(t) }); }; case (? (#error e)) { - ? (func () { r(e) }); + #schedule (func () { r(e) }); }; }; }; diff --git a/src/prelude/prelude.ml b/src/prelude/prelude.ml index a6ee84cd678..c599be8df2c 100644 --- a/src/prelude/prelude.ml +++ b/src/prelude/prelude.ml @@ -1,3 +1,4 @@ let prelude = [%blob "prelude.mo"] let internals = [%blob "internals.mo"] let prim_module = [%blob "prim.mo"] + diff --git a/src/viper/trans.ml b/src/viper/trans.ml index 4cdd44839a2..c30bcb7a7c3 100644 --- a/src/viper/trans.ml +++ b/src/viper/trans.ml @@ -207,7 +207,7 @@ and dec_field' ctxt d = NoInfo) | M.(LetD ({it=VarP f;_}, {it=FuncE(x, sp, tp, p, t_opt, sugar, - {it = AsyncE (_, e); _} );_})) -> (* ignore async *) + {it = AsyncE (T.Fut, _, e); _} );_})) -> (* ignore async *) { ctxt with ids = Env.add f.it Method ctxt.ids }, None, fun ctxt' -> @@ -288,7 +288,7 @@ and stmt ctxt (s : M.exp) : seqn = | M.IfE(e, s1, s2) -> !!([], [ !!(IfS(exp ctxt e, stmt ctxt s1, stmt ctxt s2))]) - | M.(AwaitE({ it = AsyncE (_, e); at; _ })) -> (* gross hack *) + | M.(AwaitE(T.Fut, { it = AsyncE (T.Fut, _, e); at; _ })) -> (* gross hack *) let id = fresh_id "$message_async" in let (!!) p = !!! (s.at) p in let (!@) p = !!! at p in @@ -441,7 +441,7 @@ and rets t_opt = | Some t -> (match T.normalize t.note with | T.Tup [] -> [] - | T.Async (_, _) -> [] + | T.Async (T.Fut, _, _) -> [] | _ -> unsupported t.at (Arrange.typ t) ) diff --git a/test/fail/bad-async-sort.mo b/test/fail/bad-async-sort.mo new file mode 100644 index 00000000000..ef7b300f680 --- /dev/null +++ b/test/fail/bad-async-sort.mo @@ -0,0 +1,26 @@ +actor { + func f() : async* Nat { + await* g(); // reject + }; + + func g() : async Nat { + await f(); // reject + }; + + func anon1() : async () { + await async* {}; // reject + }; + + func anon2() : async () { + await* async {}; // reject + }; + + func anon3() : async () { + ignore ((async {}) : async* ()); // reject + }; + + func anon4() : async () { + ignore ((async* {}) : async ()); // reject + }; + +} diff --git a/test/fail/bad-async.mo b/test/fail/bad-async.mo index cc5a7a98d27..28f416c82b3 100644 --- a/test/fail/bad-async.mo +++ b/test/fail/bad-async.mo @@ -6,4 +6,4 @@ actor a { 10 + (await x[0]) }; -}; \ No newline at end of file +}; diff --git a/test/fail/bad-shared-async-star.mo b/test/fail/bad-shared-async-star.mo new file mode 100644 index 00000000000..844c0c7c179 --- /dev/null +++ b/test/fail/bad-shared-async-star.mo @@ -0,0 +1,7 @@ +actor { + + public func bad() : async* Nat { // reject (shared function can't return async*) + 666 + }; + +} diff --git a/test/fail/bad-shared-function-type.mo b/test/fail/bad-shared-function-type.mo new file mode 100644 index 00000000000..711bd68fbda --- /dev/null +++ b/test/fail/bad-shared-function-type.mo @@ -0,0 +1 @@ +type t = shared() -> async* (); // reject (shared function can't return async*) diff --git a/test/fail/ok/bad-async-sort.tc.ok b/test/fail/ok/bad-async-sort.tc.ok new file mode 100644 index 00000000000..7012cfa0cce --- /dev/null +++ b/test/fail/ok/bad-async-sort.tc.ok @@ -0,0 +1,18 @@ +bad-async-sort.mo:3.12-3.15: type error [M0088], expected async* type, but expression has type + async<$f> Nat +Use keyword 'await' (not 'await*') to consume this type. +bad-async-sort.mo:7.10-7.13: type error [M0088], expected async type, but expression has type + async*<$g> Nat +Use keyword 'await*' (not 'await') to consume this type. +bad-async-sort.mo:11.11-11.20: type error [M0088], expected async type, but expression has type + async*<$anon1> () +Use keyword 'await*' (not 'await') to consume this type. +bad-async-sort.mo:15.12-15.20: type error [M0088], expected async* type, but expression has type + async<$anon2> () +Use keyword 'await' (not 'await*') to consume this type. +bad-async-sort.mo:19.14-19.22: type error [M0183], async expression cannot produce expected async type + async*<$anon3> (). +Use keyword 'async*' (not 'async') to produce the expected type. +bad-async-sort.mo:23.14-23.23: type error [M0183], async expression cannot produce expected async type + async<$anon4> (). +Use keyword 'async' (not 'async*') to produce the expected type. diff --git a/test/fail/ok/bad-async-sort.tc.ret.ok b/test/fail/ok/bad-async-sort.tc.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/fail/ok/bad-async-sort.tc.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/fail/ok/bad-shared-async-star.tc.ok b/test/fail/ok/bad-shared-async-star.tc.ok new file mode 100644 index 00000000000..d7406a2239a --- /dev/null +++ b/test/fail/ok/bad-shared-async-star.tc.ok @@ -0,0 +1 @@ +bad-shared-async-star.mo:3.24-3.34: type error [M0035], shared function must have syntactic return type '()' or 'async ' diff --git a/test/fail/ok/bad-shared-async-star.tc.ret.ok b/test/fail/ok/bad-shared-async-star.tc.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/fail/ok/bad-shared-async-star.tc.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/fail/ok/bad-shared-function-type.tc.ok b/test/fail/ok/bad-shared-function-type.tc.ok new file mode 100644 index 00000000000..67a59ffe150 --- /dev/null +++ b/test/fail/ok/bad-shared-function-type.tc.ok @@ -0,0 +1 @@ +bad-shared-function-type.mo:1.22-1.31: type error [M0035], shared function must have syntactic return type '()' or 'async ' diff --git a/test/fail/ok/bad-shared-function-type.tc.ret.ok b/test/fail/ok/bad-shared-function-type.tc.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/fail/ok/bad-shared-function-type.tc.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/run-drun/calc.mo b/test/run-drun/calc.mo new file mode 100644 index 00000000000..f2ca9cda708 --- /dev/null +++ b/test/run-drun/calc.mo @@ -0,0 +1,81 @@ +import P "mo:prim"; + +actor a { + + func power(i:Int, n: Int) : Int { + if (n<=0) i else i*power(i, n-1); + }; + + public /* query */ func pow(i :Int, n:Int) : async Int { + power(i, n); + }; + + public type Expression = { + #const : Int; + #add : (Expression, Expression); + #mul : (Expression, Expression); + #sub : (Expression, Expression); + #pow : (Expression, Expression); + }; + + func eval(exp : Expression) : Int { + switch (exp) { + case (#const(n)) n; + case (#add(e1, e2)) eval(e1) + eval(e2); + case (#mul(e1, e2)) eval(e1) * eval(e2); + case (#sub(e1, e2)) eval(e1) - eval(e2); + case (#pow(e1, e2)) power(eval e1, eval e2); + } + }; + + func evalAsync(exp : Expression) : async Int { + switch (exp) { + case (#const(n)) n; + case (#add(e1, e2)) (await evalAsync(e1)) + (await evalAsync(e2)); + case (#mul(e1, e2)) (await evalAsync(e1)) * (await evalAsync(e2)); + case (#sub(e1, e2)) (await evalAsync(e1)) - (await evalAsync(e2)); + case (#pow(e1, e2)) await (pow(await (evalAsync e1), await (evalAsync e2))); + } + }; + + // Use `await*/async* {}` to avoid context switch at each recursive call + // Could also just do outermost return instead of in each branch. + func evalAsyncStar(exp : Expression) : async* Int { + switch (exp) { + case (#const(n)) n; + case (#add(e1, e2)) (await* evalAsyncStar(e1)) + (await* evalAsyncStar(e2)); + case (#mul(e1, e2)) (await* evalAsyncStar(e1)) * (await* evalAsyncStar(e2)); + case (#sub(e1, e2)) (await* evalAsyncStar(e1)) - (await* evalAsyncStar(e2)); + case (#pow(e1, e2)) await pow(await* (evalAsyncStar e1), await* (evalAsyncStar e2)); + // ^^^^^ only real context switch on call to asynchronous `pow` query + } + }; + + func sum(n : Int) : Expression { + if (n <= 0) + #const 0 + else #add(#const n,sum (n-1)); + }; + + public func evaluate() : async () { + P.debugPrint "Sync"; + P.debugPrint (debug_show(eval(sum(32)))); + P.debugPrint (debug_show(eval(#pow(#const 2,#const 10)))); + }; + + public func evaluateAsync() : async () { + P.debugPrint "Async"; + P.debugPrint (debug_show(await (evalAsync(sum(32))))); + P.debugPrint (debug_show(await (evalAsync(#pow(#const 2,#const 10))))); + }; + + public func evaluateAsyncStar() : async () { + P.debugPrint "AsyncStar"; + P.debugPrint (debug_show(await* (evalAsyncStar(sum(32))))); + P.debugPrint (debug_show(await* (evalAsyncStar(#pow(#const 2,#const 10))))); + }; +}; + +await a.evaluate(); //OR-CALL ingress evaluate "DIDL\x00\x00" +await a.evaluateAsync(); //OR-CALL ingress evaluateAsync "DIDL\x00\x00" +await a.evaluateAsyncStar(); //OR-CALL ingress evaluateAsyncStar "DIDL\x00\x00" diff --git a/test/run-drun/do-async-nary.mo b/test/run-drun/do-async-nary.mo new file mode 100644 index 00000000000..d3df28a765c --- /dev/null +++ b/test/run-drun/do-async-nary.mo @@ -0,0 +1,40 @@ +import P "mo:prim"; +// test n-ary (n=2) async compilation +actor a { + + private func doUnit() : async* ((),()) { + let t = await async (); // await at unit type + return (t,t); + }; + + private func doText() : async* ((),()) { + let t = await async "text"; // await at different type + return ((),()); + }; + + private func doReturn() : async* ((),()) { + return ((),()); + }; + + private func doExit() : async* ((),()) { + ((),()) + }; + + private func doThrow() : async* ((),()) { + throw P.error("oops"); + }; + + public func go() : async () { + let ((),()) = await* doUnit(); + let ((),()) = await* doReturn(); + let ((),()) = await* doExit(); + try { + let ((),()) = await* doThrow(); + assert(false); + } catch (e) { assert P.errorMessage(e) == "oops";}; + } + +}; + + +a.go(); //OR-CALL ingress go "DIDL\x00\x00" diff --git a/test/run-drun/do-async-nested.mo b/test/run-drun/do-async-nested.mo new file mode 100644 index 00000000000..7ae114941bd --- /dev/null +++ b/test/run-drun/do-async-nested.mo @@ -0,0 +1,23 @@ +// test lexically nested async* expressions +actor a { + + public func bar() : async Int { + 666 + }; + + private func foo(n : Nat) : async* Int { + let _ = await* async* { "hello" }; + if (n == 0) { + await* async* { await bar(); } + } + else await* { async* { await* foo(n-1); }; } + }; + + public func go() : async () { + assert 666 == (await* foo(100)); + }; + +}; + +a.go(); //OR-CALL ingress go "DIDL\x00\x00" + diff --git a/test/run-drun/do-async-poly.mo b/test/run-drun/do-async-poly.mo new file mode 100644 index 00000000000..8f6a094b8b5 --- /dev/null +++ b/test/run-drun/do-async-poly.mo @@ -0,0 +1,44 @@ +import P "mo:prim"; +// test polymorphic async compilation +// Currently rejected because type parameters aren't shared. +// If we (in future) allow type parameters in async types, then we should enforce that `T` in async* `T` is a manifest tuple +// so that async arity is invariant under substition. +actor a { + + private func doUnit(t : T) : async* T { + let t = await async null; // await at unit type + return t; + }; + + private func doText(t : T) : async* T { + let t1 = await async "text"; // await at different type + return t; + }; + + private func doReturn(t : T) : async* T { + return t; + }; + + private func doExit(t : T) : async* T { + null; + }; + + private func doThrow(t : T) : async* T { + throw P.error("oops"); + }; + + public func go() : async () { + let u = (); + let ((),) = await* doUnit<()>(u); + let ((),) = await* doReturn<()>(u); + let ((),) = await* doExit<()>(u); + try { + let ((),) = await* doThrow<()>(); + assert(false); + } catch (e) { assert P.errorMessage(e) == "oops";}; + } + +}; + + +a.go(); //OR-CALL ingress go "DIDL\x00\x00" diff --git a/test/run-drun/do-async-rec.mo b/test/run-drun/do-async-rec.mo new file mode 100644 index 00000000000..3352c988889 --- /dev/null +++ b/test/run-drun/do-async-rec.mo @@ -0,0 +1,20 @@ +import P "mo:prim"; + +actor a { + + public func bar() : async Int { + 666 + }; + + private func foo(n : Nat) : async* Int { + if (n == 0) { return await bar();} + else await* foo(n-1); + }; + + public func go() : async () { + assert 666 == (await* foo(100)); + }; + +}; + +a.go(); //OR-CALL ingress go "DIDL\x00\x00" diff --git a/test/run-drun/do-async-unary.mo b/test/run-drun/do-async-unary.mo new file mode 100644 index 00000000000..85f3652ca37 --- /dev/null +++ b/test/run-drun/do-async-unary.mo @@ -0,0 +1,40 @@ +import P "mo:prim"; +// test unary async compilation, using null as token value +actor a { + + private func doUnit() : async* Null { + let t = await async null; // await at unit type + return t; + }; + + private func doText() : async* Null { + let t = await async "text"; // await at different type + return null; + }; + + private func doReturn() : async* Null { + return null; + }; + + private func doExit() : async* Null { + null; + }; + + private func doThrow() : async* Null { + throw P.error("oops"); + }; + + public func go() : async () { + let null = await* doUnit(); + let null = await* doReturn(); + let null = await* doExit(); + try { + let null = await* doThrow(); + assert(false); + } catch (e) { assert P.errorMessage(e) == "oops";}; + } + +}; + + +a.go(); //OR-CALL ingress go "DIDL\x00\x00" diff --git a/test/run-drun/do-async-unit.mo b/test/run-drun/do-async-unit.mo new file mode 100644 index 00000000000..22fb7267085 --- /dev/null +++ b/test/run-drun/do-async-unit.mo @@ -0,0 +1,39 @@ +import P "mo:prim"; +// test nullary async compilation (using unit) +actor a { + + private func doUnit() : async* () { + let t = await async (); // await at unit type + return t; + }; + + private func doText() : async* () { + let t = await async "text"; // await at different type + return; + }; + + private func doReturn() : async* () { + return; + }; + + private func doExit() : async* () { + }; + + private func doThrow() : async* () { + throw P.error("oops"); + }; + + public func go() : async () { + await* doUnit(); + await* doReturn(); + await* doExit(); + try { + await* doThrow(); + assert(false); + } catch (e) { assert P.errorMessage(e) == "oops";}; + } + +}; + + +a.go(); //OR-CALL ingress go "DIDL\x00\x00" diff --git a/test/run-drun/do-async.mo b/test/run-drun/do-async.mo new file mode 100644 index 00000000000..7c5ded08134 --- /dev/null +++ b/test/run-drun/do-async.mo @@ -0,0 +1,53 @@ +import P "mo:prim"; + +actor a { + + public query func int() : async Int { + 666 + }; + + public query func text() : async Text { + "hello" + }; + + private func doInt() : async* Int = async* { + return await int(); + }; + + + private func doText() : async* Int = async* { + let t = await text(); // await at different type + return t.size(); + }; + + private func doReturn() : async* Int = async* { + return 666; + }; + + + private func doExit() : async* Int = async* { + 666; + }; + + private func doThrow() : async* Int = async* { + throw P.error("oops"); + }; + + + public func go() : async () { + let i = await* doInt(); + assert i == 666; + let s = await* doText(); + assert s == 5; + let r = await* doReturn(); + assert r == 666; + let e = await* doExit(); + assert e == 666; + try { + let _ = await* doThrow(); + assert(false); + } catch (e) { assert P.errorMessage(e) == "oops";}; + } +}; + +a.go(); //OR-CALL ingress go "DIDL\x00\x00" diff --git a/test/run-drun/ok/calc.drun-run.ok b/test/run-drun/ok/calc.drun-run.ok new file mode 100644 index 00000000000..09cd6e3e536 --- /dev/null +++ b/test/run-drun/ok/calc.drun-run.ok @@ -0,0 +1,14 @@ +ingress Completed: Reply: 0x4449444c016c01b3c4b1f204680100010a00000000000000000101 +ingress Completed: Reply: 0x4449444c0000 +debug.print: Sync +debug.print: +528 +debug.print: +2_048 +ingress Completed: Reply: 0x4449444c0000 +debug.print: Async +debug.print: +528 +debug.print: +2_048 +ingress Completed: Reply: 0x4449444c0000 +debug.print: AsyncStar +debug.print: +528 +debug.print: +2_048 +ingress Completed: Reply: 0x4449444c0000 diff --git a/test/run-drun/ok/calc.ic-ref-run.ok b/test/run-drun/ok/calc.ic-ref-run.ok new file mode 100644 index 00000000000..aba80055b31 --- /dev/null +++ b/test/run-drun/ok/calc.ic-ref-run.ok @@ -0,0 +1,19 @@ +=> update provisional_create_canister_with_cycles(record {settings = null; amount = null}) +<= replied: (record {hymijyo = principal "rwlgt-iiaaa-aaaaa-aaaaa-cai"}) +=> update install_code(record {arg = blob ""; kca_xin = blob "\00asm\01\00\00\00\0... +<= replied: () +=> update evaluate() +debug.print: Sync +debug.print: +528 +debug.print: +2_048 +<= replied: () +=> update evaluateAsync() +debug.print: Async +debug.print: +528 +debug.print: +2_048 +<= replied: () +=> update evaluateAsyncStar() +debug.print: AsyncStar +debug.print: +528 +debug.print: +2_048 +<= replied: () diff --git a/test/run-drun/ok/calc.run-ir.ok b/test/run-drun/ok/calc.run-ir.ok new file mode 100644 index 00000000000..8c61e6c95ad --- /dev/null +++ b/test/run-drun/ok/calc.run-ir.ok @@ -0,0 +1,9 @@ +Sync ++528 ++2_048 +Async ++528 ++2_048 +AsyncStar ++528 ++2_048 diff --git a/test/run-drun/ok/calc.run-low.ok b/test/run-drun/ok/calc.run-low.ok new file mode 100644 index 00000000000..8c61e6c95ad --- /dev/null +++ b/test/run-drun/ok/calc.run-low.ok @@ -0,0 +1,9 @@ +Sync ++528 ++2_048 +Async ++528 ++2_048 +AsyncStar ++528 ++2_048 diff --git a/test/run-drun/ok/calc.run.ok b/test/run-drun/ok/calc.run.ok new file mode 100644 index 00000000000..8c61e6c95ad --- /dev/null +++ b/test/run-drun/ok/calc.run.ok @@ -0,0 +1,9 @@ +Sync ++528 ++2_048 +Async ++528 ++2_048 +AsyncStar ++528 ++2_048 diff --git a/test/run-drun/ok/do-async-nary.drun-run.ok b/test/run-drun/ok/do-async-nary.drun-run.ok new file mode 100644 index 00000000000..c76c471c7d5 --- /dev/null +++ b/test/run-drun/ok/do-async-nary.drun-run.ok @@ -0,0 +1,3 @@ +ingress Completed: Reply: 0x4449444c016c01b3c4b1f204680100010a00000000000000000101 +ingress Completed: Reply: 0x4449444c0000 +ingress Completed: Reply: 0x4449444c0000 diff --git a/test/run-drun/ok/do-async-nary.ic-ref-run.ok b/test/run-drun/ok/do-async-nary.ic-ref-run.ok new file mode 100644 index 00000000000..133d815b149 --- /dev/null +++ b/test/run-drun/ok/do-async-nary.ic-ref-run.ok @@ -0,0 +1,6 @@ +=> update provisional_create_canister_with_cycles(record {settings = null; amount = null}) +<= replied: (record {hymijyo = principal "rwlgt-iiaaa-aaaaa-aaaaa-cai"}) +=> update install_code(record {arg = blob ""; kca_xin = blob "\00asm\01\00\00\00\0... +<= replied: () +=> update go() +<= replied: () diff --git a/test/run-drun/ok/do-async-nested.drun-run.ok b/test/run-drun/ok/do-async-nested.drun-run.ok new file mode 100644 index 00000000000..c76c471c7d5 --- /dev/null +++ b/test/run-drun/ok/do-async-nested.drun-run.ok @@ -0,0 +1,3 @@ +ingress Completed: Reply: 0x4449444c016c01b3c4b1f204680100010a00000000000000000101 +ingress Completed: Reply: 0x4449444c0000 +ingress Completed: Reply: 0x4449444c0000 diff --git a/test/run-drun/ok/do-async-nested.ic-ref-run.ok b/test/run-drun/ok/do-async-nested.ic-ref-run.ok new file mode 100644 index 00000000000..133d815b149 --- /dev/null +++ b/test/run-drun/ok/do-async-nested.ic-ref-run.ok @@ -0,0 +1,6 @@ +=> update provisional_create_canister_with_cycles(record {settings = null; amount = null}) +<= replied: (record {hymijyo = principal "rwlgt-iiaaa-aaaaa-aaaaa-cai"}) +=> update install_code(record {arg = blob ""; kca_xin = blob "\00asm\01\00\00\00\0... +<= replied: () +=> update go() +<= replied: () diff --git a/test/run-drun/ok/do-async-poly.tc.ok b/test/run-drun/ok/do-async-poly.tc.ok new file mode 100644 index 00000000000..c0b7bf0e780 --- /dev/null +++ b/test/run-drun/ok/do-async-poly.tc.ok @@ -0,0 +1,10 @@ +do-async-poly.mo:8.42-8.43: type error [M0033], async has non-shared content type + T__18 +do-async-poly.mo:13.42-13.43: type error [M0033], async has non-shared content type + T__19 +do-async-poly.mo:18.44-18.45: type error [M0033], async has non-shared content type + T__20 +do-async-poly.mo:22.42-22.43: type error [M0033], async has non-shared content type + T__21 +do-async-poly.mo:26.43-26.44: type error [M0033], async has non-shared content type + T__22 diff --git a/test/run-drun/ok/do-async-poly.tc.ret.ok b/test/run-drun/ok/do-async-poly.tc.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/run-drun/ok/do-async-poly.tc.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/run-drun/ok/do-async-rec.drun-run.ok b/test/run-drun/ok/do-async-rec.drun-run.ok new file mode 100644 index 00000000000..c76c471c7d5 --- /dev/null +++ b/test/run-drun/ok/do-async-rec.drun-run.ok @@ -0,0 +1,3 @@ +ingress Completed: Reply: 0x4449444c016c01b3c4b1f204680100010a00000000000000000101 +ingress Completed: Reply: 0x4449444c0000 +ingress Completed: Reply: 0x4449444c0000 diff --git a/test/run-drun/ok/do-async-rec.ic-ref-run.ok b/test/run-drun/ok/do-async-rec.ic-ref-run.ok new file mode 100644 index 00000000000..133d815b149 --- /dev/null +++ b/test/run-drun/ok/do-async-rec.ic-ref-run.ok @@ -0,0 +1,6 @@ +=> update provisional_create_canister_with_cycles(record {settings = null; amount = null}) +<= replied: (record {hymijyo = principal "rwlgt-iiaaa-aaaaa-aaaaa-cai"}) +=> update install_code(record {arg = blob ""; kca_xin = blob "\00asm\01\00\00\00\0... +<= replied: () +=> update go() +<= replied: () diff --git a/test/run-drun/ok/do-async-unary.drun-run.ok b/test/run-drun/ok/do-async-unary.drun-run.ok new file mode 100644 index 00000000000..c76c471c7d5 --- /dev/null +++ b/test/run-drun/ok/do-async-unary.drun-run.ok @@ -0,0 +1,3 @@ +ingress Completed: Reply: 0x4449444c016c01b3c4b1f204680100010a00000000000000000101 +ingress Completed: Reply: 0x4449444c0000 +ingress Completed: Reply: 0x4449444c0000 diff --git a/test/run-drun/ok/do-async-unary.ic-ref-run.ok b/test/run-drun/ok/do-async-unary.ic-ref-run.ok new file mode 100644 index 00000000000..133d815b149 --- /dev/null +++ b/test/run-drun/ok/do-async-unary.ic-ref-run.ok @@ -0,0 +1,6 @@ +=> update provisional_create_canister_with_cycles(record {settings = null; amount = null}) +<= replied: (record {hymijyo = principal "rwlgt-iiaaa-aaaaa-aaaaa-cai"}) +=> update install_code(record {arg = blob ""; kca_xin = blob "\00asm\01\00\00\00\0... +<= replied: () +=> update go() +<= replied: () diff --git a/test/run-drun/ok/do-async-unit.drun-run.ok b/test/run-drun/ok/do-async-unit.drun-run.ok new file mode 100644 index 00000000000..c76c471c7d5 --- /dev/null +++ b/test/run-drun/ok/do-async-unit.drun-run.ok @@ -0,0 +1,3 @@ +ingress Completed: Reply: 0x4449444c016c01b3c4b1f204680100010a00000000000000000101 +ingress Completed: Reply: 0x4449444c0000 +ingress Completed: Reply: 0x4449444c0000 diff --git a/test/run-drun/ok/do-async-unit.ic-ref-run.ok b/test/run-drun/ok/do-async-unit.ic-ref-run.ok new file mode 100644 index 00000000000..133d815b149 --- /dev/null +++ b/test/run-drun/ok/do-async-unit.ic-ref-run.ok @@ -0,0 +1,6 @@ +=> update provisional_create_canister_with_cycles(record {settings = null; amount = null}) +<= replied: (record {hymijyo = principal "rwlgt-iiaaa-aaaaa-aaaaa-cai"}) +=> update install_code(record {arg = blob ""; kca_xin = blob "\00asm\01\00\00\00\0... +<= replied: () +=> update go() +<= replied: () diff --git a/test/run-drun/ok/do-async.drun-run.ok b/test/run-drun/ok/do-async.drun-run.ok new file mode 100644 index 00000000000..c76c471c7d5 --- /dev/null +++ b/test/run-drun/ok/do-async.drun-run.ok @@ -0,0 +1,3 @@ +ingress Completed: Reply: 0x4449444c016c01b3c4b1f204680100010a00000000000000000101 +ingress Completed: Reply: 0x4449444c0000 +ingress Completed: Reply: 0x4449444c0000 diff --git a/test/run-drun/ok/do-async.ic-ref-run.ok b/test/run-drun/ok/do-async.ic-ref-run.ok new file mode 100644 index 00000000000..133d815b149 --- /dev/null +++ b/test/run-drun/ok/do-async.ic-ref-run.ok @@ -0,0 +1,6 @@ +=> update provisional_create_canister_with_cycles(record {settings = null; amount = null}) +<= replied: (record {hymijyo = principal "rwlgt-iiaaa-aaaaa-aaaaa-cai"}) +=> update install_code(record {arg = blob ""; kca_xin = blob "\00asm\01\00\00\00\0... +<= replied: () +=> update go() +<= replied: () diff --git a/test/run-drun/ok/test-cycles.drun-run.ok b/test/run-drun/ok/test-cycles.drun-run.ok new file mode 100644 index 00000000000..b2eec1622e5 --- /dev/null +++ b/test/run-drun/ok/test-cycles.drun-run.ok @@ -0,0 +1,32 @@ +ingress Completed: Reply: 0x4449444c016c01b3c4b1f204680100010a00000000000000000101 +ingress Completed: Reply: 0x4449444c0000 +debug.print: client: available: 0 +debug.print: client: accept(0): 0 +debug.print: wallet: {cycles = ""} +debug.print: client: setting cycles +debug.print: wallet: {cycles = ""} +debug.print: client: # debit +debug.print: client: # credit-1 +debug.print: client: refunded: 0 +debug.print: client: # credit-2 +debug.print: client: refunded: 0 +debug.print: client: # refund +debug.print: refunding: 250_000 +debug.print: client: refunded: 250_000 +debug.print: client: refund(5) +debug.print: client: refund(4) +debug.print: refunding: 5 +debug.print: refunding: 4 +debug.print: client: refund(3) +debug.print: client: refund(2) +debug.print: refunding: 3 +debug.print: refunding: 2 +debug.print: client: refund(1) +debug.print: refunding: 1 +debug.print: client: refunded: 1 +debug.print: client: refunded: 2 +debug.print: client: refunded: 3 +debug.print: client: refunded: 4 +debug.print: client: refunded: 5 +debug.print: client: 0 +ingress Completed: Reply: 0x4449444c0000 diff --git a/test/run/bad-do-async.mo b/test/run/bad-do-async.mo new file mode 100644 index 00000000000..f8ab7defcb6 --- /dev/null +++ b/test/run/bad-do-async.mo @@ -0,0 +1 @@ +func g () : async* Nat { 1 }; // unsupported when compiling to standalone wasm. diff --git a/test/run/ok/bad-do-async.comp.ok b/test/run/ok/bad-do-async.comp.ok new file mode 100644 index 00000000000..6eb546d8bb3 --- /dev/null +++ b/test/run/ok/bad-do-async.comp.ok @@ -0,0 +1,2 @@ +bad-do-async.mo:1.24-1.29: type error [M0086], async expressions are not supported + (This is a limitation of the current version and flag -wasi-system-api.) diff --git a/test/run/ok/bad-do-async.comp.ret.ok b/test/run/ok/bad-do-async.comp.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/run/ok/bad-do-async.comp.ret.ok @@ -0,0 +1 @@ +Return code 1