diff --git a/doc/md/examples/grammar.txt b/doc/md/examples/grammar.txt index 24440c86f9e..d8d695f8bea 100644 --- a/doc/md/examples/grammar.txt +++ b/doc/md/examples/grammar.txt @@ -214,6 +214,7 @@ 'break' ? 'continue' 'debug' + '(' ? 'with' , ';')> ')' 'if' 'if' 'else' 'try' diff --git a/src/codegen/compile_classical.ml b/src/codegen/compile_classical.ml index 6d5eec8024c..06e681b512f 100644 --- a/src/codegen/compile_classical.ml +++ b/src/codegen/compile_classical.ml @@ -2022,7 +2022,7 @@ module Tagged = struct | T (* (T,+) *) | S (* shared ... -> ... *) type blob_sort = - | B (* Blob *) + | B (* Blob *) | T (* Text *) | P (* Principal *) | A (* actor { ... } *) @@ -2251,6 +2251,15 @@ module Tagged = struct set_tag ^^ go cases + (* like branch_default_with but the tag is known statically *) + let branch_with env retty = function + | [] -> G.i Unreachable + | [_, code] -> code + | (_, code) :: cases -> + let (set_o, get_o) = new_local env "o" in + let prep (t, code) = (t, get_o ^^ code) + in set_o ^^ get_o ^^ branch_default env retty (get_o ^^ code) (List.map prep cases) + let allocation_barrier env = (if !Flags.gc_strategy = Flags.Incremental then E.call_import env "rts" "allocation_barrier" @@ -2412,12 +2421,13 @@ module Opt = struct ( get_x ) (* true literal, no wrapping *) ( get_x ^^ Tagged.branch_default env [I32Type] ( get_x ) (* default tag, no wrapping *) - [ Tagged.Null, + Tagged. + [ Null, (* NB: even ?null does not require allocation: We use a static singleton for that: *) compile_unboxed_const (vanilla_lit env (null_vanilla_lit env)) - ; Tagged.Some, - Tagged.obj env Tagged.Some [get_x] + ; Some, + obj env Some [get_x] ] ) ) @@ -2541,7 +2551,7 @@ module Closure = struct I32Type :: Lib.List.make n_args I32Type, FakeMultiVal.ty (Lib.List.make n_res I32Type))) in (* get the table index *) - Tagged.load_forwarding_pointer env ^^ + (*Tagged.load_forwarding_pointer env ^^ FIXME: NOT needed, accessing immut slots*) Tagged.load_field env (funptr_field env) ^^ (* All done: Call! *) G.i (CallIndirect (nr ty)) ^^ @@ -5500,7 +5510,7 @@ module IC = struct | Flags.(ICMode | RefMode) -> system_call env "call_cycles_add128" | _ -> - E.trap_with env "cannot accept cycles when running locally" + E.trap_with env "cannot add cycles when running locally" let cycles_accept env = match E.mode env with @@ -9385,16 +9395,21 @@ end (* Var *) that requires top-level cps conversion; use new prims instead *) module Internals = struct - let call_prelude_function env ae var = + let call_prelude_function_with_args env ae var args = match VarEnv.lookup_var ae var with | Some (VarEnv.Const (_, Const.Fun (mk_fi, _))) -> compile_unboxed_zero ^^ (* A dummy closure *) + args ^^ G.i (Call (nr (mk_fi ()))) | _ -> assert false + let call_prelude_function env ae var = + call_prelude_function_with_args env ae var G.nop + let add_cycles env ae = call_prelude_function env ae "@add_cycles" let reset_cycles env ae = call_prelude_function env ae "@reset_cycles" let reset_refund env ae = call_prelude_function env ae "@reset_refund" + let pass_cycles env ae = call_prelude_function_with_args env ae "@pass_cycles" end (* This comes late because it also deals with messages *) @@ -10862,7 +10877,7 @@ and compile_prim_invocation (env : E.t) ae p es at = begin match p, es with (* Calls *) - | CallPrim _, [e1; e2] -> + | CallPrim (_, par), [e1; e2] -> let sort, control, _, arg_tys, ret_tys = Type.(as_func (promote e1.note.Note.typ)) in let n_args = List.length arg_tys in let return_arity = match control with @@ -10876,8 +10891,7 @@ and compile_prim_invocation (env : E.t) ae p es at = let call_as_prim = match fun_sr, sort with | SR.Const (_, Const.Fun (mk_fi, Const.PrimWrapper prim)), _ -> begin match n_args, e2.it with - | 0, _ -> true - | 1, _ -> true + | (0 | 1), _ -> true | n, PrimE (TupPrim, es) when List.length es = n -> true | _, _ -> false end @@ -10908,18 +10922,23 @@ and compile_prim_invocation (env : E.t) ae p es at = StackRep.of_arity return_arity, code1 ^^ - compile_unboxed_zero ^^ (* A dummy closure *) + Type.(match as_obj par.note.Note.typ with + | Object, [] -> compile_unboxed_zero (* a dummy closure *) + | _ -> compile_exp_vanilla env ae par) ^^ (* parenthetical *) compile_exp_as env ae (StackRep.of_arity n_args) e2 ^^ (* the args *) G.i (Call (nr (mk_fi ()))) ^^ FakeMultiVal.load env (Lib.List.make return_arity I32Type) | _, Type.Local -> - let (set_clos, get_clos) = new_local env "clos" in + let set_clos, get_clos = new_local env "clos" in StackRep.of_arity return_arity, code1 ^^ StackRep.adjust env fun_sr SR.Vanilla ^^ + Closure.prepare_closure_call env ^^ (* FIXME: move to front elsewhere too *) set_clos ^^ - get_clos ^^ - Closure.prepare_closure_call env ^^ + Type.(match as_obj par.note.Note.typ, ret_tys with + | (Object, []), _ -> get_clos (* just the closure *) + | _, [ret] when is_async_fut ret -> Arr.lit env Tagged.T [compile_exp_vanilla env ae par; get_clos] (* parenthetical: pass a pair *) + | _ -> get_clos) ^^ (* just the closure *) compile_exp_as env ae (StackRep.of_arity n_args) e2 ^^ get_clos ^^ Closure.call_closure env n_args return_arity @@ -10930,8 +10949,10 @@ and compile_prim_invocation (env : E.t) ae p es at = let (set_meth_pair, get_meth_pair) = new_local env "meth_pair" in let (set_arg, get_arg) = new_local env "arg" in let _, _, _, ts, _ = Type.as_func e1.note.Note.typ in - let add_cycles = Internals.add_cycles env ae in - + let add_cycles = Type.(match as_obj par.note.Note.typ with + | Object, [] -> Internals.add_cycles env ae (* legacy *) + | _ -> compile_exp_vanilla env ae par ^^ Object.load_idx env par.note.Note.typ "cycles" ^^ Cycles.add env) (* parenthetical *) + in StackRep.of_arity return_arity, code1 ^^ StackRep.adjust env fun_sr SR.Vanilla ^^ set_meth_pair ^^ @@ -12104,17 +12125,19 @@ and compile_prim_invocation (env : E.t) ae p es at = | ICCallerPrim, [] -> SR.Vanilla, IC.caller env - | ICCallPrim, [f;e;k;r;c] -> + | ICCallPrim setup, [f;e;k;r;c] -> SR.unit, begin (* TBR: Can we do better than using the notes? *) let _, _, _, ts1, _ = Type.as_func f.note.Note.typ in let _, _, _, ts2, _ = Type.as_func k.note.Note.typ in - let (set_meth_pair, get_meth_pair) = new_local env "meth_pair" in - let (set_arg, get_arg) = new_local env "arg" in - let (set_k, get_k) = new_local env "k" in - let (set_r, get_r) = new_local env "r" in - let (set_c, get_c) = new_local env "c" in - let add_cycles = Internals.add_cycles env ae in + let set_meth_pair, get_meth_pair = new_local env "meth_pair" in + let set_arg, get_arg = new_local env "arg" in + let set_k, get_k = new_local env "k" in + let set_r, get_r = new_local env "r" in + let set_c, get_c = new_local env "c" in + let add_cycles = match setup with + | None -> Internals.add_cycles env ae + | Some exp -> compile_exp_vanilla env ae exp ^^ G.i Drop in compile_exp_vanilla env ae f ^^ set_meth_pair ^^ compile_exp_vanilla env ae e ^^ set_arg ^^ compile_exp_vanilla env ae k ^^ set_k ^^ @@ -12122,6 +12145,7 @@ and compile_prim_invocation (env : E.t) ae p es at = compile_exp_vanilla env ae c ^^ set_c ^^ FuncDec.ic_call env ts1 ts2 get_meth_pair get_arg get_k get_r get_c add_cycles end + | ICCallRawPrim, [p;m;a;k;r;c] -> SR.unit, begin let set_meth_pair, get_meth_pair = new_local env "meth_pair" in @@ -12174,6 +12198,26 @@ and compile_prim_invocation (env : E.t) ae p es at = SR.Vanilla, Cycles.available env | SystemCyclesRefundedPrim, [] -> SR.Vanilla, Cycles.refunded env + | ICCyclesPrim, [] -> + SR.Vanilla, + G.i (LocalGet (nr 0l)) ^^ (* closed-over bindings *) + G.if1 I32Type + begin + G.i (LocalGet (nr 0l)) ^^ + Tagged.branch_with env [I32Type] + [ Tagged.Closure, + G.i Drop ^^ + Opt.null_lit env + ; Tagged.(Array T), + Opt.inject_simple env (Arr.load_field env 0l) ^^ + G.i (LocalGet (nr 0l)) ^^ + Arr.load_field env 1l ^^ + G.i (LocalSet (nr 0l)) + ; Tagged.Object, + Opt.inject_simple env G.nop + ] + end + (Opt.null_lit env) | SystemCyclesBurnPrim, [e1] -> SR.Vanilla, compile_exp_vanilla env ae e1 ^^ Cycles.burn env @@ -12349,7 +12393,7 @@ and compile_exp_with_hint (env : E.t) ae sr_hint exp = let return_arity = List.length return_tys in let mk_body env1 ae1 = compile_exp_as env1 ae1 (StackRep.of_arity return_arity) e in FuncDec.lit env ae x sort control captured args mk_body return_tys exp.at - | SelfCallE (ts, exp_f, exp_k, exp_r, exp_c) -> + | SelfCallE (cyc, ts, exp_f, exp_k, exp_r, exp_c) -> SR.unit, let (set_future, get_future) = new_local env "future" in let (set_k, get_k) = new_local env "k" in @@ -12357,7 +12401,11 @@ and compile_exp_with_hint (env : E.t) ae sr_hint exp = let (set_c, get_c) = new_local env "c" in let mk_body env1 ae1 = compile_exp_as env1 ae1 SR.unit exp_f in let captured = Freevars.captured exp_f in - let add_cycles = Internals.add_cycles env ae in + let add_cycles = match cyc.it with + | LitE NullLit -> Internals.add_cycles env ae (* legacy *) + | _ when Type.(sub cyc.note.Note.typ (Opt (Obj (Object, [{ lab = "cycles"; typ = nat; src = empty_src}])))) -> + Internals.pass_cycles env ae (compile_exp_vanilla env ae cyc) + | _ -> Internals.pass_cycles env ae (Opt.null_lit env) in FuncDec.async_body env ae ts captured mk_body exp.at ^^ Tagged.load_forwarding_pointer env ^^ set_future ^^ diff --git a/src/codegen/compile_enhanced.ml b/src/codegen/compile_enhanced.ml index 2a1351135ac..af3c942fb59 100644 --- a/src/codegen/compile_enhanced.ml +++ b/src/codegen/compile_enhanced.ml @@ -12199,7 +12199,7 @@ and compile_prim_invocation (env : E.t) ae p es at = | ICCallerPrim, [] -> SR.Vanilla, IC.caller env - | ICCallPrim, [f;e;k;r;c] -> + | ICCallPrim _FIXME, [f;e;k;r;c] -> SR.unit, begin (* TBR: Can we do better than using the notes? *) let _, _, _, ts1, _ = Type.as_func f.note.Note.typ in @@ -12432,7 +12432,7 @@ and compile_exp_with_hint (env : E.t) ae sr_hint exp = let return_arity = List.length return_tys in let mk_body env1 ae1 = compile_exp_as env1 ae1 (StackRep.of_arity return_arity) e in FuncDec.lit env ae x sort control captured args mk_body return_tys exp.at - | SelfCallE (ts, exp_f, exp_k, exp_r, exp_c) -> + | SelfCallE (cyc_FIXME, ts, exp_f, exp_k, exp_r, exp_c) -> SR.unit, let (set_future, get_future) = new_local env "future" in let (set_k, get_k) = new_local env "k" in diff --git a/src/ir_def/arrange_ir.ml b/src/ir_def/arrange_ir.ml index 02cb40bde7d..6d5e3829eaf 100644 --- a/src/ir_def/arrange_ir.ml +++ b/src/ir_def/arrange_ir.ml @@ -22,14 +22,14 @@ 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 (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] + | AsyncE (par, Type.Fut, tb, e, t) -> "AsyncE" $$ Option.(map exp par |> to_list) @ [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) -> "FuncE" $$ [Atom x; func_sort s; control c] @ List.map typ_bind tp @ args as_ @ [ typ (Type.seq ts); exp e] - | SelfCallE (ts, exp_f, exp_k, exp_r, exp_c) -> - "SelfCallE" $$ [typ (Type.seq ts); exp exp_f; exp exp_k; exp exp_r; exp exp_c] + | SelfCallE (_FIXME, ts, exp_f, exp_k, exp_r, exp_c) -> + "SelfCallE" $$ [exp _FIXME; typ (Type.seq ts); exp exp_f; exp exp_k; exp exp_r; exp exp_c] | ActorE (ds, fs, u, t) -> "ActorE" $$ List.map dec ds @ fields fs @ [system u; typ t] | NewObjE (s, fs, t) -> "NewObjE" $$ (Arrange_type.obj_sort s :: fields fs @ [typ t]) | TryE (e, cs, None) -> "TryE" $$ [exp e] @ List.map case cs @@ -60,7 +60,7 @@ and args = function and arg a = Atom a.it and prim = function - | CallPrim ts -> "CallPrim" $$ List.map typ ts + | CallPrim (ts, _FIXME) -> "CallPrim" $$ List.map typ ts @ [exp _FIXME] | UnPrim (t, uo) -> "UnPrim" $$ [typ t; Arrange_ops.unop uo] | BinPrim (t, bo) -> "BinPrim" $$ [typ t; Arrange_ops.binop bo] | RelPrim (t, ro) -> "RelPrim" $$ [typ t; Arrange_ops.relop ro] @@ -94,28 +94,29 @@ and prim = function | ActorOfIdBlob t -> "ActorOfIdBlob" $$ [typ t] | BlobOfIcUrl -> Atom "BlobOfIcUrl" | IcUrlOfBlob -> Atom "IcUrlOfBlob" - | SelfRef t -> "SelfRef" $$ [typ t] + | SelfRef t -> "SelfRef" $$ [typ t] | SystemTimePrim -> Atom "SystemTimePrim" | SystemCyclesAddPrim -> Atom "SystemCyclesAddPrim" | SystemCyclesAcceptPrim -> Atom "SystemCyclesAcceptPrim" | SystemCyclesAvailablePrim -> Atom "SystemCyclesAvailablePrim" | SystemCyclesBalancePrim -> Atom "SystemCyclesBalancePrim" | SystemCyclesRefundedPrim -> Atom "SystemCyclesRefundedPrim" + | ICCyclesPrim -> Atom "ICCyclesPrim" | SystemCyclesBurnPrim -> Atom "SystemCyclesBurnPrim" | SetCertifiedData -> Atom "SetCertifiedData" | GetCertificate -> Atom "GetCertificate" | OtherPrim s -> Atom s | 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] + | CPSAsync (Type.Fut, t, par) -> "CPSAsync" $$ [typ t] @ [exp par] + | CPSAsync (Type.Cmp, t, _) -> "CPSAsync*" $$ [typ t] | ICArgDataPrim -> Atom "ICArgDataPrim" | ICStableSize t -> "ICStableSize" $$ [typ t] | ICPerformGC -> Atom "ICPerformGC" | ICReplyPrim ts -> "ICReplyPrim" $$ List.map typ ts | ICRejectPrim -> Atom "ICRejectPrim" | ICCallerPrim -> Atom "ICCallerPrim" - | ICCallPrim -> Atom "ICCallPrim" + | ICCallPrim e -> "ICCallPrim" $$ Option.(map exp e |> to_list) | ICCallRawPrim -> Atom "ICCallRawPrim" | ICMethodNamePrim -> Atom "ICMethodNamePrim" | ICStableWrite t -> "ICStableWrite" $$ [typ t] diff --git a/src/ir_def/check_ir.ml b/src/ir_def/check_ir.ml index 0d9f45279a6..6575ff23d8a 100644 --- a/src/ir_def/check_ir.ml +++ b/src/ir_def/check_ir.ml @@ -405,7 +405,7 @@ let rec check_exp env (exp:Ir.exp) : unit = | PrimE (p, es) -> List.iter (check_exp env) es; begin match p, es with - | CallPrim insts, [exp1; exp2] -> + | CallPrim (insts, _FIXMEpars), [exp1; exp2] -> begin match T.promote (typ exp1) with | T.Func (sort, control, tbs, arg_tys, ret_tys) -> check_inst_bounds env tbs insts exp.at; @@ -556,6 +556,11 @@ 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 + + + | ICCyclesPrim, [] -> () (* FIXME *) + + | CPSAwait (s, cont_typ), [a; krb] -> let (_, t1) = try T.as_async_sub s T.Non (T.normalize (typ a)) @@ -574,7 +579,7 @@ let rec check_exp env (exp:Ir.exp) : unit = | _ -> 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] -> + | CPSAsync (s, t0, _FIXME), [exp] -> (match typ exp with | T.Func (T.Local, T.Returns, [tb], T.[Func (Local, Returns, [], ts1, []); @@ -601,7 +606,8 @@ let rec check_exp env (exp:Ir.exp) : unit = T.Non <: t | ICCallerPrim, [] -> T.caller <: t - | ICCallPrim, [exp1; exp2; k; r; c] -> + | ICCallPrim setup, [exp1; exp2; k; r; c] -> + Option.iter (fun e -> typ e <: T.unit) setup; let t1 = T.promote (typ exp1) in begin match t1 with | T.Func (sort, T.Replies, _ (*TBR*), arg_tys, ret_tys) -> @@ -744,7 +750,7 @@ let rec check_exp env (exp:Ir.exp) : unit = check_exp (add_lab env id t0) exp1; typ exp1 <: t0; t0 <: t - | AsyncE (s, tb, exp1, t0) -> + | AsyncE (_FIXME, 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 @@ -803,13 +809,15 @@ let rec check_exp env (exp:Ir.exp) : unit = , tbs, List.map (T.close cs) ts1, List.map (T.close cs) ret_tys ) in fun_ty <: t - | SelfCallE (ts, exp_f, exp_k, exp_r, exp_c) -> + | SelfCallE (cyc, ts, exp_f, exp_k, exp_r, exp_c) -> check (not env.flavor.Ir.has_async_typ) "SelfCallE in async flavor"; + check_exp env cyc; List.iter (check_typ env) ts; check_exp { env with lvl = NotTopLvl } exp_f; check_exp env exp_k; check_exp env exp_r; check_exp env exp_c; + typ cyc <: T.(Opt (Obj (Object, []))); typ exp_f <: T.unit; typ exp_k <: T.(Construct.contT (Tup ts) unit); typ exp_r <: T.(Construct.err_contT unit); diff --git a/src/ir_def/construct.ml b/src/ir_def/construct.ml index 6564490287e..b46207ab118 100644 --- a/src/ir_def/construct.ml +++ b/src/ir_def/construct.ml @@ -62,6 +62,8 @@ let tupP pats = note = T.Tup (List.map (fun p -> p.note) pats); at = no_region } +let tupVarsP vs = List.map varP vs |> tupP + let seqP ps = match ps with | [p] -> p @@ -94,6 +96,8 @@ let primE prim es = | ICStableRead t -> t | ICMethodNamePrim -> T.text | ICPerformGC + | ICStableWrite _ + | SystemCyclesAddPrim -> T.unit | ICStableSize _ -> T.nat64 | IdxPrim | DerefArrayOffset -> T.(as_immut (as_array_sub (List.hd es).note.Note.typ)) @@ -111,6 +115,7 @@ let primE prim es = | SystemCyclesBurnPrim -> T.nat | DeserializePrim ts -> T.seq ts | DeserializeOptPrim ts -> T.Opt (T.seq ts) + | ICCyclesPrim -> T.(Opt (Obj (Object, [{ lab = "cycles"; typ = nat; src = empty_src}]))) | OtherPrim "trap" -> T.Non | OtherPrim "call_perform_status" -> T.(Prim Nat32) | OtherPrim "call_perform_message" -> T.text @@ -151,14 +156,6 @@ let assertE e = } -let asyncE s typ_bind e typ1 = - { it = AsyncE (s, typ_bind, e, typ1); - at = no_region; - note = - Note.{ def with typ = T.Async (s, typ1, typ e); - eff = T.(if s = Fut then Await else Triv) } - } - let awaitE s e = let (s, _ , typ) = T.as_async (T.normalize (typ e)) in { it = PrimE (AwaitPrim s, [e]); @@ -166,8 +163,14 @@ let awaitE s e = note = Note.{ def with typ; eff = T.Await } } -let cps_asyncE s typ1 typ2 e = - { it = PrimE (CPSAsync (s, typ1), [e]); +let nullE () = + { it = LitE NullLit; + at = no_region; + note = Note.{ def with typ = T.(Prim Null) } + } + +let cps_asyncE s typ1 par typ2 e = + { it = PrimE (CPSAsync (s, typ1, if s = Fut then par else nullE ()), [e]); at = no_region; note = Note.{ def with typ = T.Async (s, typ1, typ2); eff = eff e } } @@ -196,10 +199,10 @@ let ic_rejectE e = note = Note.{ def with typ = T.unit; eff = eff e } } -let ic_callE f e k r c = +let ic_callE s f e k r c = let es = [f; e; k; r; c] in let eff = map_max_effs eff es in - { it = PrimE (ICCallPrim, es); + { it = PrimE (ICCallPrim s, es); at = no_region; note = Note.{ def with typ = T.unit; eff } } @@ -299,12 +302,6 @@ let boolE b = note = Note.{ def with typ = T.bool } } -let nullE () = - { it = LitE NullLit; - at = no_region; - note = Note.{ def with typ = T.Prim T.Null } - } - (* Functions *) @@ -322,6 +319,16 @@ let funcE name sort ctrl typ_binds args typs exp = note = Note.{ def with typ; eff = T.Triv }; } +let recordE' = ref (fun _ -> nullE ()) (* gets correctly filled below *) + +let asyncE s typ_bind e typ1 = + { it = AsyncE (None, s, typ_bind, e, typ1); + at = no_region; + note = + Note.{ def with typ = T.Async (s, typ1, typ e); + eff = T.(if s = Fut then Await else Triv) } + } + let callE exp1 typs exp2 = let typ = match T.promote (typ exp1) with | T.Func (_sort, control, _, _, ret_tys) -> @@ -329,7 +336,7 @@ let callE exp1 typs exp2 = | T.Non -> T.Non | _ -> raise (Invalid_argument "callE expect a function") in - let p = CallPrim typs in + let p = CallPrim (typs, !recordE' []) in let es = [exp1; exp2] in { it = PrimE (p, es); at = no_region; @@ -339,6 +346,10 @@ let callE exp1 typs exp2 = } } +let parenthetical par = function + | { it = PrimE (CallPrim (typs, _), es); _ } as e when true -> + { e with it = PrimE (CallPrim (typs, par), es) } + | e -> Printf.eprintf "PAR? %s\n" (Wasm.Sexpr.to_string 180 (Arrange_ir.exp e)); e let ifE exp1 exp2 exp3 = { it = IfE (exp1, exp2, exp3); @@ -361,7 +372,7 @@ let orE : Ir.exp -> Ir.exp -> Ir.exp = fun e1 e2 -> let impliesE : Ir.exp -> Ir.exp -> Ir.exp = fun e1 e2 -> orE (notE e1) e2 let oldE : Ir.exp -> Ir.exp = fun e -> - { it = (primE (CallPrim [typ e]) [e]).it; + { it = (primE (CallPrim ([typ e], !recordE' [])) [e]).it; at = no_region; note = Note.{ def with typ = typ e; @@ -377,7 +388,7 @@ let dotE exp name typ = { it = PrimE (DotPrim name, [exp]); at = no_region; note = Note.{ def with - typ = typ; + typ; eff = eff exp } } @@ -484,6 +495,9 @@ let assignE v exp2 = note = Note.{ def with typ = T.unit; eff = eff exp2 }; } +let assignVarE v exp = + assignE (var v T.(Mut (typ exp |> as_immut))) exp + let labelE l typ exp = { it = LabelE (l, typ, exp); at = no_region; @@ -792,6 +806,8 @@ let objE sort typ_flds flds = let recordE flds = objE T.Object [] flds +let _ = recordE' := recordE + let check_call_perform_status success mk_failure = ifE (callE diff --git a/src/ir_def/construct.mli b/src/ir_def/construct.mli index 26387ef5097..db978d1cf75 100644 --- a/src/ir_def/construct.mli +++ b/src/ir_def/construct.mli @@ -39,6 +39,7 @@ val typ_arg : con -> bind_sort -> typ -> typ_bind val varP : var -> pat val tupP : pat list -> pat +val tupVarsP : var list -> pat val wildP : pat val seqP : pat list -> pat @@ -51,11 +52,11 @@ val selfRefE : typ -> exp val assertE : 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_asyncE : async_sort -> typ -> exp -> 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 -> exp +val ic_callE : exp option -> exp -> exp -> exp -> exp -> exp -> exp val ic_call_rawE : exp -> exp -> exp -> exp -> exp -> exp -> exp val projE : exp -> int -> exp val optE : exp -> exp @@ -90,6 +91,7 @@ val breakE: id -> exp -> exp val retE: exp -> exp val immuteE: exp -> exp val assignE : var -> exp -> exp +val assignVarE : id -> exp -> exp val labelE : id -> typ -> exp -> exp val loopE : exp -> exp val forE : pat -> exp -> exp -> exp @@ -142,6 +144,7 @@ val (-->*) : var list -> exp -> exp (* n-ary local *) val forall : typ_bind list -> exp -> exp (* generalization *) val named : string -> exp -> exp (* renaming a function *) val (-*-) : exp -> exp -> exp (* application *) +val parenthetical : exp -> exp -> exp (* Objects *) diff --git a/src/ir_def/freevars.ml b/src/ir_def/freevars.ml index ae8d8309cf5..14b260e7000 100644 --- a/src/ir_def/freevars.ml +++ b/src/ir_def/freevars.ml @@ -112,14 +112,14 @@ 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 (par, _, _, e, _) -> exps Option.(to_list par) ++ 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_) | ActorE (ds, fs, u, _) -> actor ds fs u | NewObjE (_, fs, _) -> fields fs | TryE (e, cs, cl) -> exp e ++ cases cs ++ (match cl with Some (v, _) -> id v | _ -> M.empty) - | SelfCallE (_, e1, e2, e3, e4) -> under_lambda (exp e1) ++ exps [e2; e3; e4] + | SelfCallE (par, _, e1, e2, e3, e4) -> under_lambda (exp e1) ++ exps [par; e2; e3; e4] and actor ds fs u = close (decs ds +++ fields fs +++ system u) diff --git a/src/ir_def/ir.ml b/src/ir_def/ir.ml index 18b28c8b9ff..c0c7c8ec680 100644 --- a/src/ir_def/ir.ml +++ b/src/ir_def/ir.ml @@ -67,12 +67,12 @@ and exp' = | SwitchE of exp * case list (* switch *) | LoopE of exp (* do-while loop *) | LabelE of id * Type.typ * exp (* label *) - | AsyncE of Type.async_sort * typ_bind * exp * Type.typ (* async/async* *) + | AsyncE of exp option * 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 *) string * Type.func_sort * Type.control * typ_bind list * arg list * Type.typ list * exp - | SelfCallE of Type.typ list * exp * exp * exp * exp (* essentially ICCallPrim (FuncE shared…) *) + | SelfCallE of exp * Type.typ list * exp * exp * exp * exp (* essentially ICCallPrim (FuncE shared…) *) | ActorE of dec list * field list * system * Type.typ (* actor *) | NewObjE of Type.obj_sort * field list * Type.typ (* make an object *) | TryE of exp * case list * (id * Type.typ) option (* try/catch/cleanup *) @@ -116,7 +116,7 @@ and lexp' = all call-by-value. Many passes can treat them uniformly, so they are unified using the PrimE node. *) and prim = - | CallPrim of Type.typ list (* function call *) + | CallPrim of Type.typ list * exp (* function call *) | UnPrim of Type.typ * unop (* unary operator *) | BinPrim of Type.typ * binop (* binary operator *) | RelPrim of Type.typ * relop (* relational operator *) @@ -159,6 +159,7 @@ and prim = | SystemCyclesAvailablePrim | SystemCyclesBalancePrim | SystemCyclesRefundedPrim + | ICCyclesPrim (* cycles to send by parenthetical *) | SystemCyclesBurnPrim | SetCertifiedData | GetCertificate @@ -167,12 +168,12 @@ and prim = (* backend stuff *) | CPSAwait of Type.async_sort * Type.typ (* typ is the current continuation type of cps translation *) - | CPSAsync of Type.async_sort * Type.typ + | CPSAsync of Type.async_sort * Type.typ * exp | ICPerformGC | ICReplyPrim of Type.typ list | ICRejectPrim | ICCallerPrim - | ICCallPrim + | ICCallPrim of exp option | ICCallRawPrim | ICMethodNamePrim | ICArgDataPrim @@ -267,9 +268,9 @@ let replace_obj_pat pfs pats = (* Helper for transforming prims, without missing embedded typs and ids *) -let map_prim t_typ t_id p = +let map_prim t_typ t_id t_exp p = match p with - | CallPrim ts -> CallPrim (List.map t_typ ts) + | CallPrim (ts, par) -> CallPrim (List.map t_typ ts, t_exp par) | UnPrim (ot, op) -> UnPrim (t_typ ot, op) | BinPrim (ot, op) -> BinPrim (t_typ ot, op) | RelPrim (ot, op) -> RelPrim (t_typ ot, op) @@ -309,20 +310,21 @@ let map_prim t_typ t_id p = | SystemCyclesAvailablePrim | SystemCyclesBalancePrim | SystemCyclesRefundedPrim + | ICCyclesPrim | SystemCyclesBurnPrim | SetCertifiedData | GetCertificate | OtherPrim _ -> p | CPSAwait (s, t) -> CPSAwait (s, t_typ t) - | CPSAsync (s, t) -> CPSAsync (s, t_typ t) + | CPSAsync (s, t, par) -> CPSAsync (s, t_typ t, t_exp par) | ICReplyPrim ts -> ICReplyPrim (List.map t_typ ts) | ICArgDataPrim | ICPerformGC | ICRejectPrim | ICCallerPrim - | ICCallPrim | ICCallRawPrim | ICMethodNamePrim -> p + | ICCallPrim setup -> ICCallPrim (Option.map t_exp setup) | ICStableWrite t -> ICStableWrite (t_typ t) | ICStableRead t -> ICStableRead (t_typ t) | ICStableSize t -> ICStableSize (t_typ t) diff --git a/src/ir_def/ir_effect.ml b/src/ir_def/ir_effect.ml index a92185514b3..e03a82ca8ff 100644 --- a/src/ir_def/ir_effect.ml +++ b/src/ir_def/ir_effect.ml @@ -69,9 +69,9 @@ and infer_effect_exp (exp: exp) : T.eff = let e1 = effect_exp exp1 in let e2 = effect_cases cases in max_eff e1 e2 - | AsyncE (T.Fut, _, _, _) -> + | AsyncE (_, T.Fut, _, _, _) -> T.Await - | AsyncE (T.Cmp, _, _, _) -> + | AsyncE (_, T.Cmp, _, _, _) -> T.Triv | TryE _ -> T.Await @@ -81,13 +81,9 @@ and infer_effect_exp (exp: exp) : T.eff = effect_exp exp1 | FuncE _ -> T.Triv - | SelfCallE (_, _, exp1, exp2, exp3) -> - let e1 = effect_exp exp1 in - let e2 = effect_exp exp2 in - let e3 = effect_exp exp3 in - max_eff e1 (max_eff e2 e3) - | ActorE _ -> - T.Triv + | SelfCallE (par, _, _, exp1, exp2, exp3) -> + map_max_effs effect_exp [par; exp1; exp2; exp3] + | ActorE _ | NewObjE _ -> T.Triv @@ -102,7 +98,7 @@ and effect_cases cases = and effect_dec dec = match dec.it with | LetD (_, e) | VarD (_, _, e) -> effect_exp e | RefD (_, _, { it = DotLE (e, _); _ }) -> effect_exp e - | RefD (_, _, _) -> assert false + | RefD _ -> assert false let infer_effect_dec = effect_dec diff --git a/src/ir_def/rename.ml b/src/ir_def/rename.ml index f97594fba41..2a8445f562b 100644 --- a/src/ir_def/rename.ml +++ b/src/ir_def/rename.ml @@ -25,8 +25,8 @@ let arg_bind rho a = let i' = fresh_id a.it in ({a with it = i'}, Renaming.add a.it i' rho) -let rec prim rho p = - Ir.map_prim Fun.id (id rho) p (* rename BreakPrim id etc *) +let rec prim rho = + Ir.map_prim Fun.id (id rho) (exp rho) (* rename BreakPrim id etc *) and exp rho e = {e with it = exp' rho e.it} and exp' rho = function @@ -57,7 +57,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 (s, tb, e, t) -> AsyncE (s, tb, exp rho e, t) + | AsyncE (par, s, tb, e, t) -> AsyncE (Option.map (exp rho) par, 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) @@ -67,8 +67,8 @@ and exp' rho = function FuncE (x, s, c, tp, p', ts, e') | NewObjE (s, fs, t) -> NewObjE (s, fields rho fs, t) | TryE (e, cs, cl) -> TryE (exp rho e, cases rho cs, Option.map (fun (v, t) -> id rho v, t) cl) - | SelfCallE (ts, e1, e2, e3, e4) -> - SelfCallE (ts, exp rho e1, exp rho e2, exp rho e3, exp rho e4) + | SelfCallE (par, ts, e1, e2, e3, e4) -> + SelfCallE (exp rho par, ts, exp rho e1, exp rho e2, exp rho e3, exp rho e4) and lexp rho le = {le with it = lexp' rho le.it} and lexp' rho = function diff --git a/src/ir_interpreter/interpret_ir.ml b/src/ir_interpreter/interpret_ir.ml index 6c0e5301013..7c93c9cf52b 100644 --- a/src/ir_interpreter/interpret_ir.ml +++ b/src/ir_interpreter/interpret_ir.ml @@ -319,7 +319,7 @@ and interpret_exp_mut env exp (k : V.value V.cont) = | PrimE (p, es) -> interpret_exps env es [] (fun vs -> match p, vs with - | CallPrim typs, [v1; v2] -> + | CallPrim (typs, _), [v1; v2] -> let v1 = match v1 with | V.(Tup [Blob aid; Text id]) -> lookup_actor env exp.at aid id | _ -> v1 in @@ -450,7 +450,7 @@ and interpret_exp_mut env exp (k : V.value V.cont) = let reject = Option.get env.rejects in let e = V.Tup [V.Variant ("canister_reject", V.unit); v1] in Scheduler.queue (fun () -> reject e) - | ICCallPrim, [v1; v2; kv; rv; cv] -> + | ICCallPrim _, [v1; v2; kv; rv; cv] -> let v1 = match v1 with | V.(Tup [Blob aid; Text id]) -> lookup_actor env exp.at aid id | _ -> v1 in @@ -460,6 +460,8 @@ and interpret_exp_mut env exp (k : V.value V.cont) = last_region := exp.at; (* in case the following throws *) let vc = context env in f (V.Tup[vc; kv; rv; cv]) v2 k + | ICCyclesPrim, [] -> + k V.Null | ICCallerPrim, [] -> k env.caller | ICStableRead t, [] -> @@ -515,7 +517,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 (Type.Fut, _, exp1, _) -> + | AsyncE (_FIXME, Type.Fut, _, exp1, _) -> assert env.flavor.has_await; async env exp.at @@ -523,7 +525,7 @@ 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, _) -> + | 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 } @@ -541,7 +543,7 @@ and interpret_exp_mut env exp (k : V.value V.cont) = define_id env id v'; k V.unit ) - | SelfCallE (ts, exp_f, exp_k, exp_r, exp_c) -> + | SelfCallE (_FIXME, ts, exp_f, exp_k, exp_r, exp_c) -> assert (not env.flavor.has_async_typ); (* see code for FuncE *) let cc = { sort = T.Shared T.Write; control = T.Replies; n_args = 0; n_res = List.length ts } in diff --git a/src/ir_passes/async.ml b/src/ir_passes/async.ml index b3b52989e7a..503e43030d4 100644 --- a/src/ir_passes/async.ml +++ b/src/ir_passes/async.ml @@ -24,8 +24,8 @@ module ConRenaming = E.Make(struct type t = con let compare = Cons.compare end) (* Helpers *) -let selfcallE ts e1 e2 e3 e4 = - { it = SelfCallE (ts, e1, e2, e3, e4); +let selfcallE (cyc : exp) ts e1 e2 e3 e4 = + { it = SelfCallE (cyc, ts, e1, e2, e3, e4); at = no_region; note = Note.{ def with typ = unit } } @@ -82,6 +82,11 @@ let new_nary_async_reply ts = (* construct the n-ary async value, coercing the continuation, if necessary *) let nary_async = let coerce u = +(*<<<<<<< gabor/parentheticals + let k = fresh_var "k" (contT u T.unit) in + varE (var "@coerce_and_cont" (unary_async --> ([k; fail] -->* (varE unary_async -*- tupE [varE unary_fulfill; varE fail])) |> typ)) + -*- varE unary_async +=======*) let v = fresh_var "v" u in let k = fresh_var "k" (contT u unit) in let r = fresh_var "r" (err_contT unit) in @@ -124,10 +129,9 @@ let new_nary_async_reply ts = fresh_var "cleanup" (typ_of_var clean) in (async, reply, reject, cleanup), - blockE [letP (tupP [varP unary_async; varP unary_fulfill; varP fail; varP clean]) call_new_async] + blockE [letP (tupVarsP [unary_async; unary_fulfill; fail; clean]) call_new_async] (tupE [nary_async; nary_reply; varE fail; varE clean]) - let let_eta e scope = match e.it with | VarE (Const, _) -> scope e (* pure, so reduce *) @@ -156,8 +160,8 @@ let let_seq ts e d_of_vs = (letP p e)::d_of_vs [x] | ts -> let xs = fresh_vars "x" ts in - let p = tupP (List.map varP xs) in - (letP p e)::d_of_vs (xs) + let p = tupVarsP xs in + (letP p e) :: d_of_vs xs (* name e in f unless named already *) let ensureNamed e f = @@ -234,8 +238,6 @@ let transform prog = Type.set_kind clone (t_kind (Cons.kind c)); clone - and t_prim p = Ir.map_prim t_typ (fun id -> id) p - and t_field {lab; typ; src} = { lab; typ = t_typ typ; src } in @@ -248,6 +250,9 @@ let transform prog = }; at = exp.at; } + + and t_prim p = Ir.map_prim t_typ Fun.id t_exp p + and t_exp' (exp:exp) = let exp' = exp.it in match exp' with @@ -268,7 +273,7 @@ let transform prog = (* try await async (); schedule() catch e -> r(e) *) (let v = fresh_var "call" unit in letE v - (selfcallE [] (ic_replyE [] (unitE())) (varE schedule) (projE (varE vkrb) 1) + (selfcallE ((*FIXME: what here? *) nullE ()) [] (ic_replyE [] (unitE())) (varE schedule) (projE (varE vkrb) 1) ([] -->* (projE (varE vkrb) 2 -*- unitE ()))) (check_call_perform_status (varE v) (fun e -> projE (varE vkrb) 1 -*- e)))) ] @@ -282,7 +287,7 @@ let transform prog = (t_exp a -*- t_exp krb).it | _ -> assert false end - | PrimE (CPSAsync (Fut, t), [exp1]) -> + | PrimE (CPSAsync (Fut, t, cyc), [exp1]) -> let t0 = t_typ t in let tb, ts1 = match typ exp1 with | Func(_,_, [tb], [Func(_, _, [], ts1, []); _; _], []) -> @@ -292,20 +297,20 @@ let transform prog = new_nary_async_reply ts1 in ( blockE [ - letP (tupP [varP nary_async; varP nary_reply; varP reject; varP clean]) def; + letP (tupVarsP [nary_async; nary_reply; reject; clean]) 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" catch in + let e = fresh_var "e" T.catch in e --> ic_rejectE (errorMessageE (varE e)) in let ic_cleanup = varE (var "@cleanup" clean_contT) in let exp' = callE (t_exp exp1) [t0] (tupE [ic_reply; ic_reject; ic_cleanup]) in - expD (selfcallE ts1 exp' (varE nary_reply) (varE reject) (varE clean)) + expD (selfcallE cyc ts1 exp' (varE nary_reply) (varE reject) (varE clean)) ] (varE nary_async) ).it - | PrimE (CPSAsync (Cmp, t), [exp1]) -> + | PrimE (CPSAsync (Cmp, t, _), [exp1]) -> let t0 = t_typ t in let tb, t_ret, t_fail, t_clean = match typ exp1 with | Func(_,_, [tb], [t_ret; t_fail; t_clean], _ ) -> @@ -317,7 +322,7 @@ let transform prog = in let v_ret, v_fail, v_clean = fresh_var "v" t_ret, fresh_var "e" t_fail, fresh_var "c" t_clean in ([v_ret; v_fail; v_clean] -->* callE (t_exp exp1) [t0] (List.map varE [v_ret; v_fail; v_clean] |> tupE)).it - | PrimE (CallPrim typs, [exp1; exp2]) when is_awaitable_func exp1 -> + | PrimE (CallPrim (typs, pars), [exp1; exp2]) when is_awaitable_func exp1 -> let ts1,ts2 = match typ exp1 with | Func (Shared _, Promises, tbs, ts1, ts2) -> @@ -330,23 +335,32 @@ let transform prog = let (nary_async, nary_reply, reject, clean), def = new_nary_async_reply ts2 in + let (Object, pars_fs) = T.(as_obj pars.note.typ) in + let hasCycles = Type.(sub pars.note.typ (Obj(Object, [{ lab = "cycles"; typ = nat; src = empty_src}]))) in + assert (pars_fs = [] || hasCycles); (* FIXME: remove *) + + let setup = if hasCycles + then Some (thenE + (natE Mo_values.Numerics.Nat.zero |> assignVarE "@cycles") + (primE SystemCyclesAddPrim [dotE pars "cycles" T.nat])) + else None in + + (blockE ( letP (tupP [varP nary_async; varP nary_reply; varP reject; varP clean]) def :: let_eta exp1' (fun v1 -> let_seq ts1 exp2' (fun vs -> - [expD (ic_callE v1 (seqE (List.map varE vs)) (varE nary_reply) (varE reject) (varE clean))] + [expD (ic_callE setup v1 (seqE (List.map varE vs)) (varE nary_reply) (varE reject) (varE clean))] ) ) ) (varE nary_async)) .it | PrimE (OtherPrim "call_raw", [exp1; exp2; exp3]) -> - let exp1' = t_exp exp1 in - let exp2' = t_exp exp2 in - let exp3' = t_exp exp3 in + let exp1', exp2', exp3' = t_exp exp1, t_exp exp2, t_exp exp3 in let (nary_async, nary_reply, reject, clean), def = new_nary_async_reply [blob] in (blockE ( - letP (tupP [varP nary_async; varP nary_reply; varP reject; varP clean]) def :: + letP (tupVarsP [nary_async; nary_reply; reject; clean]) def :: let_eta exp1' (fun v1 -> let_eta exp2' (fun v2 -> let_eta exp3' (fun v3 -> @@ -391,7 +405,7 @@ let transform prog = let args' = t_args args in let typbinds' = t_typ_binds typbinds in let t0, cps = match exp.it with - | PrimE (CPSAsync (Type.Fut, t0), [cps]) -> t_typ t0, cps + | PrimE (CPSAsync (Fut, t0, _FIXME), [cps]) -> t_typ t0, cps | _ -> assert false in let t1, contT = match typ cps with | Func (_, _, @@ -421,7 +435,7 @@ let transform prog = let args' = t_args args in let typbinds' = t_typ_binds typbinds in let t0, cps = match exp.it with - | PrimE (CPSAsync (Type.Fut, t0), [cps]) -> t_typ t0, cps (* TBR *) + | PrimE (CPSAsync (Fut, t0, _FIXME), [cps]) -> t_typ t0, cps (* TBR *) | _ -> assert false in let t1, contT = match typ cps with | Func (_, _, @@ -435,7 +449,7 @@ let transform prog = v --> tupE [] in (* discard return *) let r = let e = fresh_var "e" catch in - e --> tupE [] in + e --> tupE [] in (* discard error *) let cl = varE (var "@cleanup" clean_contT) in let exp' = callE (t_exp cps) [t0] (tupE [k; r; cl]) in FuncE (x, Shared s', Returns, typbinds', args', ret_tys, exp') diff --git a/src/ir_passes/await.ml b/src/ir_passes/await.ml index 84a2170a8d2..ca5a06b53b6 100644 --- a/src/ir_passes/await.ml +++ b/src/ir_passes/await.ml @@ -88,7 +88,7 @@ let typ_cases cases = List.fold_left (fun t case -> T.lub t (typ case.it.exp)) T let rec t_async context exp = match exp.it with - | AsyncE (s, tb, exp1, typ1) -> + | AsyncE (par_opt, s, tb, exp1, typ1) -> let exp1 = R.exp R.Renaming.empty exp1 in (* rename all bound vars apart *) (*Why?*) (* add the implicit return label *) let k_ret = fresh_cont (typ exp1) T.unit in @@ -99,7 +99,9 @@ let rec t_async context exp = (LabelEnv.add Return (Cont k_ret) (LabelEnv.singleton Throw (Cont k_fail))) in - cps_asyncE s typ1 (typ exp1) + cps_asyncE s typ1 (match par_opt with + | Some par -> assert false; optE par + | None -> primE ICCyclesPrim []) (typ exp1) (forall [tb] ([k_ret; k_fail; k_clean] -->* (c_exp context' exp1 (ContVar k_ret)))) | _ -> assert false @@ -144,9 +146,9 @@ and t_exp' context exp = | Some Label -> (retE (t_exp context exp1)).it | None -> assert false end - | AsyncE (T.Cmp, _, _, _) -> + | AsyncE (_, T.Cmp, _, _, _) -> (t_async context exp).it - | AsyncE (T.Fut, _, _, _) -> + | AsyncE (_, T.Fut, _, _, _) -> assert false (* must have effect T.Await *) | TryE _ -> assert false (* these never have effect T.Triv *) | DeclareE (id, typ, exp1) -> @@ -433,9 +435,9 @@ and c_exp' context exp k = | Some (Cont k') -> c_exp context exp1 (ContVar k') | _ -> assert false end - | AsyncE (T.Cmp, tb, exp1, typ1) -> + | AsyncE (_, T.Cmp, tb, exp1, typ1) -> assert false (* must have effect T.Triv, handled by first case *) - | AsyncE (T.Fut, tb, exp1, typ1) -> + | AsyncE (par_opt, T.Fut, tb, exp1, typ1) -> (* add the implicit return label *) let k_ret = fresh_cont (typ exp1) T.unit in let k_fail = fresh_err_cont T.unit in @@ -450,7 +452,11 @@ and c_exp' context exp k = | _ -> assert false in let cps_async = - cps_asyncE T.Fut typ1 (typ exp1) + cps_asyncE T.Fut typ1 (match par_opt with + | Some par when T.(sub (typ par) (Obj (Object, [{ lab = "cycles"; typ = nat; src = empty_src}]))) + -> optE par + | None -> primE ICCyclesPrim [] + | Some _ -> nullE ()) (typ exp1) (forall [tb] ([k_ret; k_fail; k_clean] -->* (c_exp context' exp1 (ContVar k_ret)))) in let k' = meta (typ cps_async) @@ -644,7 +650,7 @@ and t_comp_unit context = function let e = fresh_var "e" T.catch in ProgU [ funcD throw e (assertE (falseE ())); - expD (c_block context' ds (tupE []) (meta (T.unit) (fun v1 -> tupE []))) + expD (c_block context' ds (tupE []) (meta T.unit (fun v1 -> tupE []))) ] end | ActorU (as_opt, ds, ids, { meta = m; preupgrade; postupgrade; heartbeat; timer; inspect; stable_record; stable_type}, t) -> @@ -673,7 +679,7 @@ and t_ignore_throw context exp = { (blockE [ funcD throw e (tupE[]); ] - (c_exp context' exp (meta (T.unit) (fun v1 -> tupE [])))) + (c_exp context' exp (meta T.unit (fun v1 -> tupE [])))) (* timer logic requires us to preserve any source location, or timer won't be initialized in compile.ml *) with at = exp.at diff --git a/src/ir_passes/const.ml b/src/ir_passes/const.ml index 9bc4591cad1..0f8f5740b13 100644 --- a/src/ir_passes/const.ml +++ b/src/ir_passes/const.ml @@ -136,7 +136,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 (_(*FIXME*), _, _, e1, _) -> exp_ NotTopLvl env e1; surely_false | AssignE (_, e1) | LabelE (_, _, e1) | DefineE (_, _, e1) -> @@ -147,7 +147,8 @@ let rec exp lvl (env : env) e : Lbool.t = exp_ lvl env e2; exp_ lvl env e3; surely_false - | SelfCallE (_, e1, e2, e3, e4) -> + | SelfCallE (par, _, e1, e2, e3, e4) -> + exp_ lvl env par; exp_ NotTopLvl env e1; exp_ lvl env e2; exp_ lvl env e3; diff --git a/src/ir_passes/eq.ml b/src/ir_passes/eq.ml index 52486abcf4b..04ecfaa67bf 100644 --- a/src/ir_passes/eq.ml +++ b/src/ir_passes/eq.ml @@ -240,15 +240,15 @@ and t_exp' env = function LoopE (t_exp env exp1) | LabelE (id, typ, exp1) -> LabelE (id, typ, t_exp env exp1) - | AsyncE (s, tb, e, typ) -> AsyncE (s, tb, t_exp env e, typ) + | AsyncE (par, s, tb, e, typ) -> AsyncE (Option.map (t_exp env) par, s, tb, t_exp env e, typ) | DeclareE (id, typ, exp1) -> DeclareE (id, typ, t_exp env exp1) | DefineE (id, mut ,exp1) -> DefineE (id, mut, t_exp env exp1) | NewObjE (sort, ids, t) -> NewObjE (sort, ids, t) - | SelfCallE (ts, e1, e2, e3, e4) -> - SelfCallE (ts, t_exp env e1, t_exp env e2, t_exp env e3, t_exp env e4) + | SelfCallE (cyc, ts, e1, e2, e3, e4) -> + SelfCallE (t_exp env cyc, ts, t_exp env e1, t_exp env e2, t_exp env e3, t_exp env e4) | ActorE (ds, fields, {meta; preupgrade; postupgrade; heartbeat; timer; inspect; stable_record; stable_type}, typ) -> (* Until Actor expressions become their own units, we repeat what we do in `comp_unit` below *) diff --git a/src/ir_passes/erase_typ_field.ml b/src/ir_passes/erase_typ_field.ml index 2b5daf75d70..f44e4ba52fc 100644 --- a/src/ir_passes/erase_typ_field.ml +++ b/src/ir_passes/erase_typ_field.ml @@ -83,8 +83,6 @@ let transform prog = Type.set_kind clone (t_kind (Cons.kind c)); clone - and t_prim p = Ir.map_prim t_typ Fun.id p - and t_field {lab; typ; src} = { lab; typ = t_typ typ; src } in @@ -97,6 +95,9 @@ let transform prog = }; at = exp.at; } + + and t_prim p = Ir.map_prim t_typ Fun.id t_exp p + and t_exp' (exp : exp) = let exp' = exp.it in match exp' with @@ -116,8 +117,8 @@ let transform prog = LoopE (t_exp exp1) | LabelE (id, typ, exp1) -> LabelE (id, t_typ typ, t_exp exp1) - | AsyncE (s, tb, exp1, typ) -> - AsyncE (s, t_typ_bind tb, t_exp exp1, t_typ typ) + | AsyncE (par, s, tb, exp1, typ) -> + AsyncE (Option.map t_exp par, s, t_typ_bind tb, t_exp exp1, t_typ typ) | TryE (exp1, cases, vt) -> TryE (t_exp exp1, List.map t_case cases, vt) | DeclareE (id, typ, exp1) -> diff --git a/src/ir_passes/show.ml b/src/ir_passes/show.ml index 23f195220d7..5e4d3f85f36 100644 --- a/src/ir_passes/show.ml +++ b/src/ir_passes/show.ml @@ -282,15 +282,15 @@ and t_exp' env = function LoopE (t_exp env exp1) | LabelE (id, typ, exp1) -> LabelE (id, typ, t_exp env exp1) - | AsyncE (s, tb, e, typ) -> AsyncE (s, tb, t_exp env e, typ) + | AsyncE (par, s, tb, e, typ) -> AsyncE (Option.map (t_exp env) par, s, tb, t_exp env e, typ) | DeclareE (id, typ, exp1) -> DeclareE (id, typ, t_exp env exp1) | DefineE (id, mut ,exp1) -> DefineE (id, mut, t_exp env exp1) | NewObjE (sort, ids, t) -> NewObjE (sort, ids, t) - | SelfCallE (ts, e1, e2, e3, e4) -> - SelfCallE (ts, t_exp env e1, t_exp env e2, t_exp env e3, t_exp env e4) + | SelfCallE (cyc, ts, e1, e2, e3, e4) -> + SelfCallE (t_exp env cyc, ts, t_exp env e1, t_exp env e2, t_exp env e3, t_exp env e4) | ActorE (ds, fields, {meta; preupgrade; postupgrade; heartbeat; timer; inspect; stable_record; stable_type}, typ) -> (* Until Actor expressions become their own units, we repeat what we do in `comp_unit` below *) diff --git a/src/ir_passes/tailcall.ml b/src/ir_passes/tailcall.ml index 48fb2631f9a..3cfde9b121b 100644 --- a/src/ir_passes/tailcall.ml +++ b/src/ir_passes/tailcall.ml @@ -94,14 +94,14 @@ and assignEs vars exp : dec list = and exp' env e : exp' = match e.it with | (VarE (_, _) | LitE _) as it -> it | AssignE (e1, e2) -> AssignE (lexp env e1, exp env e2) - | PrimE (CallPrim insts, [e1; e2]) -> + | PrimE (CallPrim (insts, pars), [e1; e2]) -> begin match e1.it, env with | VarE (_, f1), { tail_pos = true; info = Some { func; typ_binds; temps; label; tail_called } } - when f1 = func && are_generic_insts typ_binds insts -> + when f1 = func && are_generic_insts typ_binds insts -> tail_called := true; (blockE (assignEs temps (exp env e2)) (breakE label (unitE ()))).it - | _,_-> PrimE (CallPrim insts, [exp env e1; exp env e2]) + | _,_-> PrimE (CallPrim (insts, exp env pars), [exp env e1; exp env e2]) end | BlockE (ds, e) -> BlockE (block env ds e) | IfE (e1, e2, e3) -> IfE (exp env e1, tailexp env e2, tailexp env e3) @@ -111,7 +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]) - | AsyncE (s, tb, e, typ) -> AsyncE (s, tb, exp { tail_pos = true; info = None } e, typ) + | AsyncE (par, s, tb, e, typ) -> AsyncE (Option.map (exp env) par, 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) @@ -120,13 +120,14 @@ and exp' env e : exp' = match e.it with let env2 = args env1 as_ in let exp0' = tailexp env2 exp0 in FuncE (x, s, c, tbs, as_, ret_tys, exp0') - | SelfCallE (ts, exp1, exp2, exp3, exp4) -> - let env1 = { tail_pos = true; info = None} in + | SelfCallE (par, ts, exp1, exp2, exp3, exp4) -> + let par' = exp env par in + let env1 = { tail_pos = true; info = None } in let exp1' = tailexp env1 exp1 in let exp2' = exp env exp2 in let exp3' = exp env exp3 in let exp4' = exp env exp4 in - SelfCallE (ts, exp1', exp2', exp3', exp4') + SelfCallE (par', ts, exp1', exp2', exp3', exp4') | ActorE (ds, fs, u, t) -> (* TODO: tco other upgrade fields? *) let u = { u with preupgrade = exp env u.preupgrade; postupgrade = exp env u.postupgrade; stable_record = exp env u.stable_record } in @@ -138,7 +139,7 @@ and lexp env le : lexp = {le with it = lexp' env le} and lexp' env le : lexp' = match le.it with | VarLE i -> VarLE i - | DotLE (e, sn) -> DotLE (exp env e, sn) + | DotLE (e, sn) -> DotLE (exp env e, sn) | IdxLE (e1, e2) -> IdxLE (exp env e1, exp env e2) and args env as_ = @@ -258,7 +259,7 @@ and block env ds exp = and comp_unit env = function | LibU _ -> raise (Invalid_argument "cannot compile library") | ProgU ds -> ProgU (snd (decs env ds)) - | ActorU (as_opt, ds, fs, u, t) -> + | ActorU (as_opt, ds, fs, u, t) -> (* TODO: tco other fields of u? *) let u = { u with preupgrade = exp env u.preupgrade; diff --git a/src/lang_utils/error_codes.ml b/src/lang_utils/error_codes.ml index 16cbd291704..f356a27c3bb 100644 --- a/src/lang_utils/error_codes.ml +++ b/src/lang_utils/error_codes.ml @@ -203,4 +203,6 @@ let error_codes : (string * string option) list = "M0197", Some([%blob "lang_utils/error_codes/M0197.md"]); (* `system` capability required *) "M0198", Some([%blob "lang_utils/error_codes/M0198.md"]); (* Unused field pattern warning *) "M0199", Some([%blob "lang_utils/error_codes/M0199.md"]); (* Deprecate experimental stable memory *) + "M0200", Some([%blob "lang_utils/error_codes/M0200.md"]); (* Unrecognised attribute in parenthetical note *) + "M0201", None; (* `cycle` attribute in parenthetical note must be of type `Nat` *) ] diff --git a/src/lang_utils/error_codes/M0200.md b/src/lang_utils/error_codes/M0200.md new file mode 100644 index 00000000000..31d35d0321d --- /dev/null +++ b/src/lang_utils/error_codes/M0200.md @@ -0,0 +1,9 @@ +# M0200 + +This warning means that you are affixing a parenthetical note to a message send (i.e. either +a canister method call of a self-send with `async`) that contains an attribute not recognised +by this version of the Motoko compiler. + +Currently following attributes are recognised in parenthetical notes: + +- `cycles : Nat` diff --git a/src/lowering/desugar.ml b/src/lowering/desugar.ml index d79d3ccb942..8728a9ed956 100644 --- a/src/lowering/desugar.ml +++ b/src/lowering/desugar.ml @@ -123,7 +123,7 @@ and exp' at note = function let tys = List.map (T.open_ vars) res_tys in I.FuncE (name, s, control, tbs', args, tys, wrap (exp e)) (* Primitive functions in the prelude have particular shapes *) - | S.CallE ({it=S.AnnotE ({it=S.PrimE p;_}, _);note;_}, _, e) + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE p;_}, _);note;_}, _, e) when Lib.String.chop_prefix "num_conv" p <> None -> begin match String.split_on_char '_' p with | ["num"; "conv"; s1; s2] -> @@ -132,7 +132,7 @@ and exp' at note = function I.PrimE (I.NumConvTrapPrim (p1, p2), [exp e]) | _ -> assert false end - | S.CallE ({it=S.AnnotE ({it=S.PrimE p;_}, _);note;_}, _, e) + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE p;_}, _);note;_}, _, e) when Lib.String.chop_prefix "num_wrap" p <> None -> begin match String.split_on_char '_' p with | ["num"; "wrap"; s1; s2] -> @@ -141,73 +141,73 @@ and exp' at note = function I.PrimE (I.NumConvWrapPrim (p1, p2), [exp e]) | _ -> assert false end - | S.CallE ({it=S.AnnotE ({it=S.PrimE "decodeUtf8";_},_);_}, _, e) -> + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "decodeUtf8";_},_);_}, _, e) -> I.PrimE (I.DecodeUtf8, [exp e]) - | S.CallE ({it=S.AnnotE ({it=S.PrimE "encodeUtf8";_},_);_}, _, e) -> + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "encodeUtf8";_},_);_}, _, e) -> I.PrimE (I.EncodeUtf8, [exp e]) - | S.CallE ({it=S.AnnotE ({it=S.PrimE "cast";_}, _);note;_}, _, e) -> + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cast";_}, _);note;_}, _, e) -> begin match note.S.note_typ with | T.Func (T.Local, T.Returns, [], ts1, ts2) -> I.PrimE (I.CastPrim (T.seq ts1, T.seq ts2), [exp e]) | _ -> assert false end - | S.CallE ({it=S.AnnotE ({it=S.PrimE "serialize";_}, _);note;_}, _, e) -> + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "serialize";_}, _);note;_}, _, e) -> begin match note.S.note_typ with | T.Func (T.Local, T.Returns, [], ts1, ts2) -> I.PrimE (I.SerializePrim ts1, [exp e]) | _ -> assert false end - | S.CallE ({it=S.AnnotE ({it=S.PrimE "deserialize";_}, _);note;_}, _, e) -> + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "deserialize";_}, _);note;_}, _, e) -> begin match note.S.note_typ with | T.Func (T.Local, T.Returns, [], ts1, ts2) -> I.PrimE (I.DeserializePrim ts2, [exp e]) | _ -> assert false end - | S.CallE ({it=S.AnnotE ({it=S.PrimE "caller";_},_);_}, _, {it=S.TupE es;_}) -> + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "caller";_},_);_}, _, {it=S.TupE es;_}) -> assert (es = []); I.PrimE (I.ICCallerPrim, []) - | S.CallE ({it=S.AnnotE ({it=S.PrimE "time";_},_);_}, _, {it=S.TupE es;_}) -> + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "time";_},_);_}, _, {it=S.TupE es;_}) -> assert (es = []); I.PrimE (I.SystemTimePrim, []) (* Cycles *) - | S.CallE ({it=S.AnnotE ({it=S.PrimE "cyclesBalance";_},_);_}, _, {it=S.TupE es;_}) -> + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesBalance";_},_);_}, _, {it=S.TupE es;_}) -> assert (es = []); I.PrimE (I.SystemCyclesBalancePrim, []) - | S.CallE ({it=S.AnnotE ({it=S.PrimE "cyclesAvailable";_},_);_}, _, {it=S.TupE es;_}) -> + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesAvailable";_},_);_}, _, {it=S.TupE es;_}) -> assert (es = []); I.PrimE (I.SystemCyclesAvailablePrim, []) - | S.CallE ({it=S.AnnotE ({it=S.PrimE "cyclesRefunded";_},_);_}, _, {it=S.TupE es;_}) -> + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesRefunded";_},_);_}, _, {it=S.TupE es;_}) -> assert (es = []); I.PrimE (I.SystemCyclesRefundedPrim, []) - | S.CallE ({it=S.AnnotE ({it=S.PrimE "cyclesAccept";_},_);_}, _, e) -> + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesAccept";_},_);_}, _, e) -> I.PrimE (I.SystemCyclesAcceptPrim, [exp e]) - | S.CallE ({it=S.AnnotE ({it=S.PrimE "cyclesAdd";_},_);_}, _, e) -> + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesAdd";_},_);_}, _, e) -> I.PrimE (I.SystemCyclesAddPrim, [exp e]) - | S.CallE ({it=S.AnnotE ({it=S.PrimE "cyclesBurn";_},_);_}, _, e) -> + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "cyclesBurn";_},_);_}, _, e) -> I.PrimE (I.SystemCyclesBurnPrim, [exp e]) (* Certified data *) - | S.CallE ({it=S.AnnotE ({it=S.PrimE "setCertifiedData";_},_);_}, _, e) -> + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "setCertifiedData";_},_);_}, _, e) -> I.PrimE (I.SetCertifiedData, [exp e]) - | S.CallE ({it=S.AnnotE ({it=S.PrimE "getCertificate";_},_);_}, _, {it=S.TupE es;_}) -> + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE "getCertificate";_},_);_}, _, {it=S.TupE es;_}) -> I.PrimE (I.GetCertificate, []) (* Other *) - | S.CallE ({it=S.AnnotE ({it=S.PrimE p;_},_);_}, _, {it=S.TupE es;_}) -> + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE p;_},_);_}, _, {it=S.TupE es;_}) -> I.PrimE (I.OtherPrim p, exps es) - | S.CallE ({it=S.AnnotE ({it=S.PrimE p;_},_);_}, _, e) -> + | S.CallE (None, {it=S.AnnotE ({it=S.PrimE p;_},_);_}, _, e) -> I.PrimE (I.OtherPrim p, [exp e]) (* Optimizing array.size() *) - | S.CallE ({it=S.DotE (e1, proj); _}, _, {it=S.TupE [];_}) + | S.CallE (None, {it=S.DotE (e1, proj); _}, _, {it=S.TupE [];_}) when T.is_array e1.note.S.note_typ && proj.it = "size" -> I.PrimE (I.OtherPrim "array_len", [exp e1]) - | S.CallE ({it=S.DotE (e1, proj); _}, _, {it=S.TupE [];_}) + | S.CallE (None, {it=S.DotE (e1, proj); _}, _, {it=S.TupE [];_}) when T.(is_prim Text) e1.note.S.note_typ && proj.it = "size" -> I.PrimE (I.OtherPrim "text_len", [exp e1]) - | S.CallE ({it=S.DotE (e1, proj); _}, _, {it=S.TupE [];_}) + | S.CallE (None, {it=S.DotE (e1, proj); _}, _, {it=S.TupE [];_}) when T.(is_prim Blob) e1.note.S.note_typ && proj.it = "size" -> I.PrimE (I.OtherPrim "blob_size", [exp e1]) (* Normal call *) - | S.CallE (e1, inst, e2) -> - I.PrimE (I.CallPrim inst.note, [exp e1; exp e2]) + | S.CallE (par_opt, e1, inst, e2) -> + I.PrimE (I.CallPrim (inst.note, Option.(value ~default:(recordE []) (map exp par_opt))), [exp e1; exp e2]) | S.BlockE [] -> (unitE ()).it | S.BlockE [{it = S.ExpD e; _}] -> (exp e).it | S.BlockE ds -> I.BlockE (block (T.is_unit note.Note.typ) ds) @@ -229,7 +229,7 @@ and exp' at note = function | S.WhileE (e1, e2) -> (whileE (exp e1) (exp e2)).it | S.LoopE (e1, None) -> I.LoopE (exp e1) | S.LoopE (e1, Some e2) -> (loopWhileE (exp e1) (exp e2)).it - | S.ForE (p, {it=S.CallE ({it=S.DotE (arr, proj); _}, _, e1); _}, e2) + | S.ForE (p, {it=S.CallE (None, {it=S.DotE (arr, proj); _}, _, e1); _}, e2) when T.is_array arr.note.S.note_typ && (proj.it = "vals" || proj.it = "keys") -> (transform_for_to_while p arr proj e1 e2).it | S.ForE (p, e1, e2) -> (forE (pat p) (exp e1) (exp e2)).it @@ -238,8 +238,8 @@ 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 (s, tb, e) -> - I.AsyncE (s, typ_bind tb, exp e, + | S.AsyncE (par_opt, s, tb, e) -> + I.AsyncE (Option.map exp par_opt, s, typ_bind tb, exp e, match note.Note.typ with | T.Async (_, t, _) -> t | _ -> assert false) @@ -994,12 +994,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 (s, tb, e', t)) -> - { e with it = Ir.AsyncE (s, tb, wrap_po e', t) } + | (T.Promises, Ir.AsyncE (par, s, tb, e', t)) -> + { e with it = Ir.AsyncE (par, s, tb, wrap_po e', t) } | T.Returns, Ir.BlockE ( - [{ it = Ir.LetD ({ it = Ir.WildP; _} as pat, ({ it = Ir.AsyncE (T.Fut, tb,e',t); _} as exp)); _ }], + [{ it = Ir.LetD ({ it = Ir.WildP; _} as pat, ({ it = Ir.AsyncE (par, T.Fut, tb,e',t); _} as exp)); _ }], ({ it = Ir.PrimE (Ir.TupPrim, []); _} as unit)) -> - blockE [letP pat {exp with it = Ir.AsyncE (T.Fut, tb,wrap_po e',t)} ] unit + blockE [letP pat {exp with it = Ir.AsyncE (par, T.Fut, tb, wrap_po e',t)} ] unit | _, Ir.ActorE _ -> wrap_po e | _ -> assert false else diff --git a/src/mo_def/arrange.ml b/src/mo_def/arrange.ml index 12cb3fecb10..7b413636dbe 100644 --- a/src/mo_def/arrange.ml +++ b/src/mo_def/arrange.ml @@ -93,7 +93,8 @@ module Make (Cfg : Config) = struct Atom (if sugar then "" else "="); exp e' ] - | CallE (e1, ts, e2) -> "CallE" $$ [exp e1] @ inst ts @ [exp e2] + | CallE (None, e1, ts, e2) -> "CallE" $$ [exp e1] @ inst ts @ [exp e2] + | CallE (Some par, e1, ts, e2) -> "CallE()" $$ [exp par] @ [exp e1] @ inst ts @ [exp e2] | BlockE ds -> "BlockE" $$ List.map dec ds | NotE e -> "NotE" $$ [exp e] | AndE (e1, e2) -> "AndE" $$ [exp e1; exp e2] @@ -110,8 +111,9 @@ module Make (Cfg : Config) = struct | DebugE e -> "DebugE" $$ [exp e] | BreakE (i, e) -> "BreakE" $$ [id i; exp e] | RetE e -> "RetE" $$ [exp e] - | AsyncE (Type.Fut, tb, e) -> "AsyncE" $$ [typ_bind tb; exp e] - | AsyncE (Type.Cmp, tb, e) -> "AsyncE*" $$ [typ_bind tb; exp e] + | AsyncE (None, Type.Fut, tb, e) -> "AsyncE" $$ [typ_bind tb; exp e] + | AsyncE (Some par, Type.Fut, tb, e) -> "AsyncE()" $$ [exp par; typ_bind tb; exp e] + | AsyncE (None, 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] diff --git a/src/mo_def/compUnit.ml b/src/mo_def/compUnit.ml index a71aafa29de..2174d7c78d3 100644 --- a/src/mo_def/compUnit.ml +++ b/src/mo_def/compUnit.ml @@ -9,13 +9,13 @@ let (@~) it at = Source.annotate Const it at let is_actor_def e = let open Source in match e.it with - | AwaitE (Type.Fut, { it = AsyncE (Type.Fut, _, {it = ObjBlockE ({ it = Type.Actor; _}, _t, _fields); _ }) ; _ }) -> true + | AwaitE (Type.Fut, { it = AsyncE (_, Type.Fut, _, {it = ObjBlockE ({ it = Type.Actor; _}, _t, _fields); _ }) ; _ }) -> true | _ -> false let as_actor_def e = let open Source in match e.it with - | AwaitE (Type.Fut, { it = AsyncE (Type.Fut, _, {it = ObjBlockE ({ it = Type.Actor; _}, _t, fields); note; at }) ; _ }) -> + | AwaitE (Type.Fut, { it = AsyncE (_, Type.Fut, _, {it = ObjBlockE ({ it = Type.Actor; _}, _t, fields); note; at }) ; _ }) -> fields, note, at | _ -> assert false diff --git a/src/mo_def/syntax.ml b/src/mo_def/syntax.ml index 5917938b628..bc1e7422ce0 100644 --- a/src/mo_def/syntax.ml +++ b/src/mo_def/syntax.ml @@ -173,8 +173,8 @@ and exp' = | ArrayE of mut * exp list (* array *) | IdxE of exp * exp (* array indexing *) | FuncE of string * sort_pat * typ_bind list * pat * typ option * sugar * exp (* function *) - | CallE of exp * inst * exp (* function call *) - | BlockE of dec list (* block (with type after avoidance)*) + | CallE of exp option * exp * inst * exp (* function call *) + | BlockE of dec list (* block (with type after avoidance) *) | NotE of exp (* negation *) | AndE of exp * exp (* conjunction *) | OrE of exp * exp (* disjunction *) @@ -189,7 +189,7 @@ and exp' = | BreakE of id * exp (* break *) | RetE of exp (* return *) | DebugE of exp (* debugging *) - | AsyncE of async_sort * typ_bind * exp (* future / computation *) + | AsyncE of exp option * 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 *) @@ -320,11 +320,11 @@ let scopeT at = (* Expressions *) let asyncE sort tbs e = - AsyncE (sort, tbs, e) @? e.at + AsyncE (None, sort, tbs, e) @? e.at let ignore_asyncE tbs e = IgnoreE ( - AnnotE (AsyncE (Type.Fut, tbs, e) @? e.at, + AnnotE (AsyncE (None, 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 = @@ -335,7 +335,7 @@ let is_asyncE e = let is_ignore_asyncE e = match e.it with | IgnoreE - {it = AnnotE ({it = AsyncE (Type.Fut, _, _); _}, + {it = AnnotE ({it = AsyncE (None, Type.Fut, _, _); _}, {it = AsyncT (Type.Fut, _, {it = TupT []; _}); _}); _} -> true | _ -> false diff --git a/src/mo_frontend/definedness.ml b/src/mo_frontend/definedness.ml index e920c325390..51b4cc3df0a 100644 --- a/src/mo_frontend/definedness.ml +++ b/src/mo_frontend/definedness.ml @@ -82,7 +82,7 @@ let rec exp msgs e : f = match e.it with (* Eager uses are either first-class uses of a variable: *) | VarE i -> M.singleton i.it Eager (* Or anything that is occurring in a call (as this may call a closure): *) - | CallE (e1, ts, e2) -> eagerify (exps msgs [e1; e2]) + | CallE (par_opt, e1, _ts, e2) -> eagerify (Option.to_list par_opt @ [e1; e2] |> exps msgs) (* And break, return, throw can be thought of as calling a continuation: *) | BreakE (_, e) | RetE e @@ -115,6 +115,7 @@ let rec exp msgs e : f = match e.it with | OrE (e1, e2) | ImpliesE (e1, e2) -> exps msgs [e1; e2] | ForE (p, e1, e2) -> exp msgs e1 ++ (exp msgs e2 /// pat msgs p) + | AsyncE (Some par, _, _, e) -> exps msgs [par; e] | UnE (_, _, e) | ShowE (_, e) | FromCandidE e @@ -124,7 +125,7 @@ let rec exp msgs e : f = match e.it with | OldE e | LabelE (_, _, e) | DebugE e - | AsyncE (_, _, e) + | AsyncE (None, _, _, e) | AwaitE (_, e) | AssertE (_, e) | AnnotE (e, _) diff --git a/src/mo_frontend/effect.ml b/src/mo_frontend/effect.ml index 0ed989d7bc6..a989d62ac21 100644 --- a/src/mo_frontend/effect.ml +++ b/src/mo_frontend/effect.ml @@ -49,8 +49,10 @@ let effect_exp (exp:Syntax.exp) : T.eff = eff exp (* infer the effect of an expression, assuming all sub-expressions are correctly effect-annotated es *) let rec infer_effect_exp (exp:Syntax.exp) : T.eff = match exp.it with - | CallE (exp1, inst, exp2) when is_async_call exp1 inst exp2 -> + | CallE (_, exp1, inst, exp2) when is_async_call exp1 inst exp2 -> T.Await + | CallE (Some par, exp1, _, exp2) -> + map_max_effs effect_exp [par; exp1; exp2] | PrimE _ | VarE _ | LitE _ @@ -81,16 +83,14 @@ let rec infer_effect_exp (exp:Syntax.exp) : T.eff = | IdxE (exp1, exp2) | RelE (_, exp1, _, exp2) | AssignE (exp1, exp2) - | CallE (exp1, _, exp2) + | CallE (None, exp1, _, exp2) | AndE (exp1, exp2) | OrE (exp1, exp2) | ImpliesE (exp1, exp2) | WhileE (exp1, exp2) | LoopE (exp1, Some exp2) | ForE (_, exp1, exp2) -> - let t1 = effect_exp exp1 in - let t2 = effect_exp exp2 in - max_eff t1 t2 + map_max_effs effect_exp [exp1; exp2] | DebugE exp1 -> effect_exp exp1 | ToCandidE exps @@ -111,9 +111,9 @@ let rec infer_effect_exp (exp:Syntax.exp) : T.eff = let e1 = effect_exp exp1 in let e2 = effect_cases cases in max_eff e1 e2 - | AsyncE (T.Fut, _, _) -> + | AsyncE (_, T.Fut, _, _) -> T.Await - | AsyncE (T.Cmp, _, _) -> + | AsyncE (_, T.Cmp, _, _) -> T.Triv | ThrowE _ | TryE _ diff --git a/src/mo_frontend/parser.mly b/src/mo_frontend/parser.mly index 85de84694bd..1853ff5d23d 100644 --- a/src/mo_frontend/parser.mly +++ b/src/mo_frontend/parser.mly @@ -605,7 +605,7 @@ exp_post(B) : | e=exp_post(B) DOT x=id { DotE(e, x) @? at $sloc } | e1=exp_post(B) inst=inst e2=exp_nullary(ob) - { CallE(e1, inst, e2) @? at $sloc } + { CallE(None, e1, inst, e2) @? at $sloc } | e1=exp_post(B) BANG { BangE(e1) @? at $sloc } | LPAR SYSTEM e1=exp_post(B) DOT x=id RPAR @@ -675,9 +675,9 @@ exp_un(B) : | RETURN e=exp(ob) { RetE(e) @? at $sloc } | ASYNC e=exp_nest - { AsyncE(Type.Fut, scope_bind (anon_id "async" (at $sloc)) (at $sloc), e) @? at $sloc } + { AsyncE(None, Type.Fut, scope_bind (anon_id "async" (at $sloc)) (at $sloc), e) @? at $sloc } | ASYNCSTAR e=exp_nest - { AsyncE(Type.Cmp, scope_bind (anon_id "async*" (at $sloc)) (at $sloc), e) @? at $sloc } + { AsyncE(None, Type.Cmp, scope_bind (anon_id "async*" (at $sloc)) (at $sloc), e) @? at $sloc } | AWAIT e=exp_nest { AwaitE(Type.Fut, e) @? at $sloc } | AWAITSTAR e=exp_nest @@ -703,6 +703,14 @@ exp_un(B) : BreakE(x', TupE([]) @? no_region) @? at $sloc } | DEBUG e=exp_nest { DebugE(e) @? at $sloc } + | LPAR base=exp_post(ob)? WITH fs=seplist(exp_field, semicolon) RPAR e=exp_nest (* parentheticals to qualify message sends *) + { match e.it with + | CallE (base0_opt, f, is, args) -> + { e with it = CallE (Some (ObjE (Option.(to_list base0_opt @ to_list base), fs) @? e.at), f, is, args) } + | AsyncE (base0_opt, Type.Fut, binds, exp) -> + { e with it = AsyncE (Some (ObjE (Option.(to_list base0_opt @ to_list base), fs) @? e.at), Type.Fut, binds, exp) } + | _ -> e (* FIXME: meh, can we emit a warning? *) + } | IF b=exp_nullary(ob) e1=exp_nest %prec IF_NO_ELSE { IfE(b, e1, TupE([]) @? at $sloc) @? at $sloc } | IF b=exp_nullary(ob) e1=exp_nest ELSE e2=exp_nest @@ -875,7 +883,7 @@ dec_nonvar : let id = if named then Some x else None in AwaitE (Type.Fut, - AsyncE(Type.Fut, scope_bind (anon_id "async" (at $sloc)) (at $sloc), + AsyncE(None, Type.Fut, scope_bind (anon_id "async" (at $sloc)) (at $sloc), objblock s id t (List.map share_dec_field efs) @? at $sloc) @? at $sloc) @? at $sloc else objblock s None t efs @? at $sloc diff --git a/src/mo_frontend/traversals.ml b/src/mo_frontend/traversals.ml index aba776444b3..d00db167f77 100644 --- a/src/mo_frontend/traversals.ml +++ b/src/mo_frontend/traversals.ml @@ -20,7 +20,7 @@ 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 (s, tb, exp1) -> f { exp with it = AsyncE (s, tb, over_exp f exp1) } + | AsyncE (par, s, tb, exp1) -> f { exp with it = AsyncE (Option.map (over_exp f) par, 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) -> @@ -31,8 +31,8 @@ let rec over_exp (f : exp -> exp) (exp : exp) : exp = match exp.it with f { exp with it = RelE (x, over_exp f exp1, y, over_exp f exp2) } | AssignE (exp1, exp2) -> f { exp with it = AssignE (over_exp f exp1, over_exp f exp2) } - | CallE (exp1, x, exp2) -> - f { exp with it = CallE (over_exp f exp1, x, over_exp f exp2) } + | CallE (par_opt, exp1, x, exp2) -> + f { exp with it = CallE (Option.map (over_exp f) par_opt, over_exp f exp1, x, over_exp f exp2) } | AndE (exp1, exp2) -> f { exp with it = AndE (over_exp f exp1, over_exp f exp2) } | OrE (exp1, exp2) -> diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 9001eb6bf47..e519edd72bc 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -1038,8 +1038,8 @@ let rec is_explicit_exp e = true | 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) -> + | ProjE (e1, _) | DotE (e1, _) | BangE e1 | IdxE (e1, _) | CallE (_(*FIXME: correct?*), 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 @@ -1585,7 +1585,8 @@ and infer_exp'' env exp : T.typ = end; let ts1 = match pat.it with TupP _ -> T.seq_of_tup t1 | _ -> [t1] in T.Func (sort, c, T.close_binds cs tbs, List.map (T.close cs) ts1, List.map (T.close cs) ts2) - | CallE (exp1, inst, exp2) -> + | CallE (par_opt, exp1, inst, exp2) -> + if not env.pre then validate_parenthetical env par_opt; infer_call env exp1 inst exp2 exp.at None | BlockE decs -> let t, _ = infer_block env decs exp.at false in @@ -1714,9 +1715,10 @@ and infer_exp'' env exp : T.typ = check_exp_strong env T.throw exp1 end; T.Non - | AsyncE (s, typ_bind, exp1) -> - error_in [Flags.WASIMode; Flags.WasmMode] env exp1.at "M0086" + | AsyncE (par_opt, s, typ_bind, exp1) -> + error_in Flags.[WASIMode; WasmMode] env exp1.at "M0086" "async expressions are not supported"; + if not env.pre then validate_parenthetical env par_opt; (* TODO: in restricted environment? *) let t1, next_cap = check_AsyncCap env "async expression" exp.at in let c, tb, ce, cs = check_typ_bind env typ_bind in let ce_scope = T.Env.add T.default_scope_var c ce in (* pun scope var with c *) @@ -1890,8 +1892,8 @@ 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 (s1, tb, exp1), T.Async (s2, t1', t') -> - error_in [Flags.WASIMode; Flags.WasmMode] env exp1.at "M0086" + | AsyncE (_FIXME, s1, tb, exp1), T.Async (s2, t1', t') -> + error_in Flags.[WASIMode; 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 @@ -1977,7 +1979,8 @@ and check_exp' env0 t exp : T.typ = in check_exp_strong (adjoin_vals env' ve2) t2 exp; t - | CallE (exp1, inst, exp2), _ -> + | CallE (_FIXME, exp1, inst, exp2), _ -> + ignore (Option.map (infer_exp env) _FIXME); let t' = infer_call env exp1 inst exp2 exp.at (Some t) in if not (T.sub t' t) then local_error env0 exp.at "M0096" @@ -2549,6 +2552,19 @@ and infer_obj env s dec_fields at : T.typ = end; t +and validate_parenthetical env = function + | None -> () + | Some par -> + let attrs = infer_exp env par in + let [@warning "-8"] T.Object, attrs_flds = T.as_obj attrs in + let unrecognised = List.(filter (fun {T.lab; _} -> lab <> "cycles") attrs_flds |> map (fun {T.lab; _} -> lab)) in + if unrecognised <> [] then warn env par.at "M0200" "unrecognised attribute %s in parenthetical note" (List.hd unrecognised); + let cyc = List.(filter (fun {T.lab; _} -> lab = "cycles") attrs_flds) in + if cyc <> [] && not T.(sub (List.hd cyc).typ nat) then + local_error env par.at "M0201" + "expected Nat type for attribute cycles, but it has type%a" + display_typ_expand (List.hd cyc).T.typ + and check_system_fields env sort scope tfs dec_fields = List.iter (fun df -> match sort, df.it.vis.it, df.it.dec.it with @@ -2792,7 +2808,7 @@ and infer_val_path env exp : T.typ option = | _ -> None ) | AnnotE (_, typ) -> - Some (check_typ {env with pre = true} typ) + Some (check_typ {env with pre = true} typ) | _ -> None @@ -2811,7 +2827,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 @@ -2899,7 +2915,7 @@ and infer_dec_typdecs env dec : Scope.t = | LetD ( {it = VarP id; _}, ( {it = ObjBlockE (obj_sort, _t, dec_fields); at; _} - | {it = AwaitE (_, { it = AsyncE (_, _, {it = ObjBlockE ({ it = Type.Actor; _} as obj_sort, _t, dec_fields); at; _}) ; _ }); _ }), + | {it = AwaitE (_, { it = AsyncE (_, _, _, {it = ObjBlockE ({ it = Type.Actor; _} as obj_sort, _t, dec_fields); at; _}) ; _ }); _ }), _ ) -> let decs = List.map (fun {it = {vis; dec; _}; _} -> dec) dec_fields in @@ -2985,7 +3001,7 @@ and infer_dec_valdecs env dec : Scope.t = | LetD ( {it = VarP id; _} as pat, ( {it = ObjBlockE (obj_sort, _t, dec_fields); at; _} - | {it = AwaitE (_, { it = AsyncE (_, _, {it = ObjBlockE ({ it = Type.Actor; _} as obj_sort, _t, dec_fields); at; _}) ; _ }); _ }), + | {it = AwaitE (_, { it = AsyncE (_, _, _, {it = ObjBlockE ({ it = Type.Actor; _} as obj_sort, _t, dec_fields); at; _}) ; _ }); _ }), _ ) -> let decs = List.map (fun df -> df.it.dec) dec_fields in diff --git a/src/mo_interpreter/interpret.ml b/src/mo_interpreter/interpret.ml index ec3a30736cb..81dfca40c3f 100644 --- a/src/mo_interpreter/interpret.ml +++ b/src/mo_interpreter/interpret.ml @@ -571,7 +571,7 @@ and interpret_exp_mut env exp (k : V.value V.cont) = | T.Shared _ -> make_message env name exp.note.note_typ v | T.Local -> v in k v' - | CallE (exp1, typs, exp2) -> + | CallE (_FIXME, exp1, typs, exp2) -> interpret_exp env exp1 (fun v1 -> let v1 = begin match v1 with | V.(Tup [Blob aid; Text id]) -> lookup_actor env exp1.at aid id @@ -686,14 +686,14 @@ 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 (T.Fut, _, exp1) -> + | AsyncE (_FIXME, 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 - | AsyncE (T.Cmp, _, exp1) -> + | AsyncE (_FIXME, 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')) diff --git a/src/mo_types/type.ml b/src/mo_types/type.ml index bc8aeb5b451..c8d787708e5 100644 --- a/src/mo_types/type.ml +++ b/src/mo_types/type.ml @@ -580,6 +580,8 @@ let is_unit = function Tup [] -> true | _ -> false let is_pair = function Tup [_; _] -> true | _ -> false let is_func = function Func _ -> true | _ -> false let is_async = function Async _ -> true | _ -> false +let is_async_cmp = function Async (Cmp, _, _) -> true | _ -> false +let is_async_fut = function Async (Fut, _, _) -> true | _ -> false let is_mut = function Mut _ -> true | _ -> false let is_typ = function Typ _ -> true | _ -> false let is_con = function Con _ -> true | _ -> false diff --git a/src/mo_types/type.mli b/src/mo_types/type.mli index 1e52866700c..170c828d653 100644 --- a/src/mo_types/type.mli +++ b/src/mo_types/type.mli @@ -129,6 +129,8 @@ val is_unit : typ -> bool val is_pair : typ -> bool val is_func : typ -> bool val is_async : typ -> bool +val is_async_cmp : typ -> bool +val is_async_fut : typ -> bool val is_mut : typ -> bool val is_typ : typ -> bool val is_con : typ -> bool diff --git a/src/prelude/internals.mo b/src/prelude/internals.mo index b98be29c768..b3785f4f769 100644 --- a/src/prelude/internals.mo +++ b/src/prelude/internals.mo @@ -9,6 +9,16 @@ code, and cannot be shadowed. type @Iter = {next : () -> ?T_}; +// Function called by backend to add funds to call. +// DO NOT RENAME without modifying compilation. +func @pass_cycles(par : ?{ cycles : Nat }) { + let ?{ cycles } = par else return; + @reset_cycles(); + if (cycles != 0) { + (prim "cyclesAdd" : Nat -> ()) cycles; + } +}; + var @cycles : Nat = 0; // Function called by backend to add funds to call. @@ -17,10 +27,11 @@ func @add_cycles() { let cycles = @cycles; @reset_cycles(); if (cycles != 0) { - (prim "cyclesAdd" : Nat -> ()) (cycles); + (prim "cyclesAdd" : Nat -> ()) cycles; } }; + // Function called by backend to zero cycles on context switch. // DO NOT RENAME without modifying compilation. func @reset_cycles() { @@ -309,6 +320,16 @@ func @getSystemRefund() : @Refund { return (prim "cyclesRefunded" : () -> Nat) (); }; +/*<<<<<<< gabor/parentheticals +func @coerce_and_cont(a : @Async<()>) : + (k : () -> (), r : @Cont) -> { + #suspend; + #schedule : () -> () + } = + func(k, r) = a(func() = k(), r); + +func @new_async() : (@Async, @Cont, @Cont) { +=======*/ // trivial cleanup action func @cleanup() { }; diff --git a/src/viper/prep.ml b/src/viper/prep.ml index b2d019eaecf..56a88be69b4 100644 --- a/src/viper/prep.ml +++ b/src/viper/prep.ml @@ -30,18 +30,18 @@ let string_of_mono_goal (g : mono_goal) : string = | _ -> unsupported Source.no_region (Mo_types.Arrange_type.typ t)) g.mg_typs) let mono_calls_visitor (stk : mono_goal Stack.t) : visitor = - { visit_exp = (function - | {it = CallE({it = VarE v; at = v_at; note = v_note},inst,e); at; note} -> - let goal = { mg_id = v.it; mg_typs = inst.note } in - let _ = (if goal.mg_typs = [] then () else Stack.push goal stk) in - let s = string_of_mono_goal goal in - {it = CallE({it = VarE (s @~ v_at); at=v_at; note=v_note}, - {it = None; at=inst.at; note = []}, e); at; note} - | e -> e); - visit_typ = Fun.id; + { visit_typ = Fun.id; visit_pat = Fun.id; visit_dec = Fun.id; visit_inst = Fun.id; + visit_exp = function + | {it = CallE(_, {it = VarE v; at = v_at; note = v_note}, inst, e); _} as exp -> + let goal = { mg_id = v.it; mg_typs = inst.note } in + if goal.mg_typs <> [] then Stack.push goal stk; + let s = string_of_mono_goal goal in + {exp with it = CallE(None, {it = VarE (s @~ v_at); at=v_at; note=v_note}, + {it = None; at=inst.at; note = []}, e)} + | e -> e } let mono_calls_dec_field (df : dec_field) : (mono_goal list * dec_field) = diff --git a/src/viper/trans.ml b/src/viper/trans.ml index ef19b23bd57..3e956b2e892 100644 --- a/src/viper/trans.ml +++ b/src/viper/trans.ml @@ -392,7 +392,7 @@ and dec_field' ctxt d = (* async functions *) | M.(LetD ({it=VarP f;note;_}, {it=FuncE(x, sp, tp, p, t_opt, sugar, - {it = AsyncE (T.Fut, _, e); _} );_}, None)) -> (* ignore async *) + {it = AsyncE (_, T.Fut, _, e); _} );_}, None)) -> (* ignore async *) { ctxt with ids = Env.add f.it (Method, note) ctxt.ids }, None, (* no perm *) None, (* no init *) @@ -577,7 +577,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(T.Fut, { it = AsyncE (T.Fut, _, 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 @@ -665,7 +665,7 @@ and stmt ctxt (s : M.exp) : seqn = | M.AssertE (M.Runtime, e) -> !!([], [ !!(AssumeS (exp ctxt e)) ]) - | M.(CallE({it = VarE m; _}, inst, args)) -> + | M.(CallE(_, {it = VarE m; _}, inst, args)) -> !!([], [ !!(MethodCallS ([], id_ref m, let self_var = self ctxt m.at in @@ -804,7 +804,7 @@ and assign_stmts ctxt at (lval : lvalue) (e : M.exp) : seqn' = match e with | M.({it=TupE [];_}) -> [], [] | M.({it=AnnotE (e, _);_}) -> assign_stmts ctxt at lval e - | M.({it=CallE ({it=M.DotE ({it=M.VarE(m);_}, {it="init";_});_}, _inst, args);_}) + | M.({it=CallE (_, {it=M.DotE ({it=M.VarE(m);_}, {it="init";_});_}, _inst, args);_}) when Imports.find_opt (m.it) ctxt.imports = Some(IM_base_Array) -> begin match args with @@ -818,7 +818,7 @@ and assign_stmts ctxt at (lval : lvalue) (e : M.exp) : seqn' = ) | _ -> unsupported args.at (Arrange.exp args) end - | M.({it = CallE({it = VarE m; _}, inst, args); _}) -> + | M.({it = CallE(_, {it = VarE m; _}, inst, args); _}) -> fld_via_tmp_var ctxt lval t (fun x -> let self_var = self ctxt m.at in [], [ !!(MethodCallS ([x], id_ref m, self_var :: call_args ctxt args)) ]) @@ -879,7 +879,7 @@ and exp ctxt e = end | M.AnnotE(a, b) -> exp ctxt a - | M.CallE ({it=M.DotE (e1, {it="size";_});_}, _inst, {it=M.TupE ([]);at;_}) + | M.CallE (_, {it=M.DotE (e1, {it="size";_});_}, _inst, {it=M.TupE ([]);at;_}) -> sizeE at (exp ctxt e1) | M.LitE r -> begin match !r with @@ -960,7 +960,7 @@ and exp ctxt e = let n = List.length es in ctxt.reqs.tuple_arities := IntSet.add n !(ctxt.reqs.tuple_arities); !!(CallE (tup_con_name n, List.map (exp ctxt) es)) - | M.CallE ({ it = M.DotE ({it=M.VarE(m);_}, {it=predicate_name;_}); _ }, _inst, { it = M.FuncE (_, _, _, pattern, _, _, e); note; _ }) + | M.CallE (_, { it = M.DotE ({it=M.VarE(m);_}, {it=predicate_name;_}); _ }, _inst, { it = M.FuncE (_, _, _, pattern, _, _, e); note; _ }) when Imports.find_opt (m.it) ctxt.imports = Some(IM_Prim) && (predicate_name = "forall" || predicate_name = "exists") -> @@ -983,7 +983,7 @@ and exp ctxt e = | "forall" -> !!(ForallE (typed_binders, e)) | "exists" -> !!(ExistsE (typed_binders, e)) | _ -> assert false) - | M.CallE ({ it = M.DotE ({it=M.VarE(m);_}, {it="Ret";_}); _ }, _, _) + | M.CallE (_, { it = M.DotE ({it=M.VarE(m);_}, {it="Ret";_}); _ }, _, _) when Imports.find_opt (m.it) ctxt.imports = Some(IM_Prim) -> !!(FldE "$Res") | _ -> unsupported e.at (Arrange.exp e) diff --git a/src/viper/traversals.ml b/src/viper/traversals.ml index bdf02154c6e..71411beb16e 100644 --- a/src/viper/traversals.ml +++ b/src/viper/traversals.ml @@ -29,14 +29,14 @@ let rec over_exp (v : visitor) (exp : exp) : exp = | BreakE (x, exp1) -> { exp with it = BreakE (x, over_exp v exp1) } | RetE exp1 -> { exp with it = RetE (over_exp v exp1) } | AnnotE (exp1, t) -> { exp with it = AnnotE (over_exp v exp1, over_typ v t) } - | AsyncE (s, tb, exp1) -> { exp with it = AsyncE (s, tb, over_exp v exp1) } + | AsyncE (par, s, tb, exp1) -> { exp with it = AsyncE (Option.map (over_exp v) par, s, tb, over_exp v exp1) } | AwaitE (s, exp1) -> { exp with it = AwaitE (s, over_exp v exp1) } | ThrowE exp1 -> { exp with it = ThrowE (over_exp v exp1) } | BinE (x, exp1, y, exp2) -> { exp with it = BinE (x, over_exp v exp1, y, over_exp v exp2) } | IdxE (exp1, exp2) -> { exp with it = IdxE (over_exp v exp1, over_exp v exp2) } | RelE (x, exp1, y, exp2) -> { exp with it = RelE (x, over_exp v exp1, y, over_exp v exp2) } | AssignE (exp1, exp2) -> { exp with it = AssignE (over_exp v exp1, over_exp v exp2) } - | CallE (exp1, inst, exp2) -> { exp with it = CallE (over_exp v exp1, over_inst v inst, over_exp v exp2) } + | CallE (exp_opt, exp1, inst, exp2) -> { exp with it = CallE (Option.map (over_exp v) exp_opt, over_exp v exp1, over_inst v inst, over_exp v exp2) } | AndE (exp1, exp2) -> { exp with it = AndE (over_exp v exp1, over_exp v exp2) } | OrE (exp1, exp2) -> { exp with it = OrE (over_exp v exp1, over_exp v exp2) } | ImpliesE (exp1, exp2) -> { exp with it = ImpliesE (over_exp v exp1, over_exp v exp2) } diff --git a/test/fail/cycle-type.mo b/test/fail/cycle-type.mo new file mode 100644 index 00000000000..10ad6fc0f61 --- /dev/null +++ b/test/fail/cycle-type.mo @@ -0,0 +1,7 @@ +actor { + func _bad(a : actor { foo : () -> async () }) : async () { + let defaults = { moot = 9 }; + await (defaults with cycles = 'C') a.foo(); + await (defaults with cycles = "Can't") async (); + } +} diff --git a/test/fail/ok/cycle-type.tc.ok b/test/fail/ok/cycle-type.tc.ok new file mode 100644 index 00000000000..3835db1f923 --- /dev/null +++ b/test/fail/ok/cycle-type.tc.ok @@ -0,0 +1,6 @@ +cycle-type.mo:4.40-4.47: warning [M0200], unrecognised attribute moot in parenthetical note +cycle-type.mo:4.40-4.47: type error [M0201], expected Nat type for attribute cycles, but it has type + Char +cycle-type.mo:5.44-5.52: warning [M0200], unrecognised attribute moot in parenthetical note +cycle-type.mo:5.44-5.52: type error [M0201], expected Nat type for attribute cycles, but it has type + Text diff --git a/test/fail/ok/cycle-type.tc.ret.ok b/test/fail/ok/cycle-type.tc.ret.ok new file mode 100644 index 00000000000..69becfa16f9 --- /dev/null +++ b/test/fail/ok/cycle-type.tc.ret.ok @@ -0,0 +1 @@ +Return code 1 diff --git a/test/run-drun/actor-class-cycles.mo b/test/run-drun/actor-class-cycles.mo index 06c85db266c..cd9048aaf8a 100644 --- a/test/run-drun/actor-class-cycles.mo +++ b/test/run-drun/actor-class-cycles.mo @@ -19,7 +19,8 @@ actor a { Prim.debugPrint(debug_show({ iteration = i })); Prim.debugPrint(debug_show({ balance = round(Cycles.balance()) })); let c = await { - Cycles.add((i + 1) * 10_000_000_000_000); + //Cycles.add((i + 1) * 10_000_000_000_000); FIXME: this should still work without a parenthetical + (with cycles = (i + 1) * 10_000_000_000_000) Lib.C(); }; let {current = cur; initial = init} = await c.balance(); diff --git a/test/run-drun/clone.mo b/test/run-drun/clone.mo index 6a6df77ed03..a4871d65e53 100644 --- a/test/run-drun/clone.mo +++ b/test/run-drun/clone.mo @@ -8,8 +8,8 @@ actor Cloner { // passing itself as first argument, using available funds public shared func makeCloneable(init : Nat): async Lib.Cloneable { let accepted = Cycles.accept(Cycles.available()); - Cycles.add(accepted); - await Lib.Cloneable(makeCloneable, init); + Prim.debugPrint(debug_show {accepted}); + await (with cycles = accepted) Lib.Cloneable(makeCloneable, init); }; public shared func test() : async () { @@ -18,9 +18,8 @@ actor Cloner { await Cycles.provisional_top_up_actor(Cloner, 100_000_000_000_000); // create the original Cloneable object - Cycles.add(10_000_000_000_000); - let c0 : Lib.Cloneable = await makeCloneable(0); - await c0.someMethod(); // prints 1 + let c0 : Lib.Cloneable = await (with cycles = 10_000_000_000_000) makeCloneable(0); + await (with cycles = 42_000_000) c0.someMethod(); // prints 1 Prim.debugPrint(debug_show(Prim.principalOfActor c0)); // create some proper clones diff --git a/test/run-drun/clone/cloneable.mo b/test/run-drun/clone/cloneable.mo index 8dded284eaa..4760052928b 100644 --- a/test/run-drun/clone/cloneable.mo +++ b/test/run-drun/clone/cloneable.mo @@ -16,11 +16,11 @@ actor class Cloneable( public func someMethod() : async () { state += 1; Prim.debugPrint(debug_show(state)); + Prim.debugPrint(debug_show Cycles.available()); }; // our clone methods, indirecting through makeCloneable public func clone(init : Nat) : async Cloneable { - Cycles.add(Cycles.balance() / 2); - await makeCloneable(init : Nat); + await (with cycles = Cycles.balance() / 2) makeCloneable init; } } diff --git a/test/run-drun/ok/clone.drun-run.ok b/test/run-drun/ok/clone.drun-run.ok index 3a37cf62bbf..3530bf68883 100644 --- a/test/run-drun/ok/clone.drun-run.ok +++ b/test/run-drun/ok/clone.drun-run.ok @@ -1,13 +1,20 @@ ingress Completed: Reply: 0x4449444c016c01b3c4b1f204680100010a00000000000000000101 ingress Completed: Reply: 0x4449444c0000 +debug.print: {accepted = 10_000_000_000_000} debug.print: 0 debug.print: 1 +debug.print: 42_000_000 debug.print: rrkah-fqaaa-aaaaa-aaaaq-cai +debug.print: {accepted = 5_000_000_000_000} debug.print: 1 debug.print: 2 +debug.print: 0 debug.print: ryjl3-tyaaa-aaaaa-aaaba-cai +debug.print: {accepted = 2_500_000_000_000} debug.print: 2 debug.print: 3 +debug.print: 0 debug.print: r7inp-6aaaa-aaaaa-aaabq-cai debug.print: 2 +debug.print: 0 ingress Completed: Reply: 0x4449444c0000 diff --git a/test/run-drun/ok/par.drun-run.ok b/test/run-drun/ok/par.drun-run.ok new file mode 100644 index 00000000000..abdd16f542b --- /dev/null +++ b/test/run-drun/ok/par.drun-run.ok @@ -0,0 +1,14 @@ +ingress Completed: Reply: 0x4449444c016c01b3c4b1f204680100010a00000000000000000101 +ingress Completed: Reply: 0x4449444c0000 +debug.print: test() +ingress Completed: Reply: 0x4449444c0000 +debug.print: test2() +ingress Completed: Reply: 0x4449444c0000 +debug.print: test3() +debug.print: oneshot: 0 +debug.print: oneshot: 3_456 +ingress Completed: Reply: 0x4449444c0000 +debug.print: test4() +debug.print: rawable: 0 +debug.print: rawable: 34_567 +ingress Completed: Reply: 0x4449444c0000 diff --git a/test/run-drun/ok/par.tc.ok b/test/run-drun/ok/par.tc.ok new file mode 100644 index 00000000000..3b3c1bb2cd2 --- /dev/null +++ b/test/run-drun/ok/par.tc.ok @@ -0,0 +1 @@ +par.mo:53.9-53.67: warning [M0200], unrecognised attribute timeout in parenthetical note diff --git a/test/run-drun/par.mo b/test/run-drun/par.mo new file mode 100644 index 00000000000..6338980062b --- /dev/null +++ b/test/run-drun/par.mo @@ -0,0 +1,86 @@ +import { call_raw; debugPrint; principalOfActor } = "mo:⛔"; +import Cycles = "cycles/cycles"; + +actor A { + + func foo(next : () -> async ()) : async () { + await (with cycles = 3000) next() + }; + + func bar(next : () -> async ()) : async () = async { + await (with cycles = 4000) next() + }; + + public func oneshot() { + debugPrint ("oneshot: " # debug_show(Cycles.available())); + }; + + public func rawable() : async () { + debugPrint ("rawable: " # debug_show(Cycles.available())); + }; + + public func test() : async () { + debugPrint "test()"; + let message = "Hi!"; + + func closA() : async Nat { + message.size() + }; + + func closB() : async Nat = async { + message.size() + }; +/* + // this is ruled out + func closC() : async Nat = + if (1 == 2) async { + message.size() + } else async { + message.size() + 1 + }; +*/ + +/* //Rule this out? + func closD() : async Nat = (with cycles = 765) async { + message.size() + }; +*/ + + assert 3 == (await (with cycles = 101) closA()); + assert 3 == (await (with cycles = 102) closB()); + + await (with yeah = 8; timeout = 55; cycles = 1000) + foo(func() : async () = async { assert message == "Hi!" }); + await (with cycles = 5000) + bar(func() : async () = async { assert message == "Hi!" }); + }; + + public func test2() : async () { + debugPrint "test2()"; + await (with cycles = 1042) async { assert Cycles.available() == 1042 }; + await (with cycles = 3042) (with cycles = 4042) async { assert Cycles.available() == 3042/*FIXME: WHY?*/ }; + }; + + public func test3() : async () { + debugPrint "test3()"; + oneshot(); + (with cycles = 3456) oneshot(); + }; + + public func test4() : async () { + debugPrint "test4()"; + ignore await call_raw(principalOfActor A, "rawable", "DIDL\00\00"); + Cycles.add(34567); + ignore await /*(with cycles = 3456)*/ call_raw(principalOfActor A, "rawable", "DIDL\00\00"); + } +} + +// testing +//SKIP run +//SKIP run-ir +//SKIP run-low + +//CALL ingress test "DIDL\x00\x00" +//CALL ingress test2 "DIDL\x00\x00" +//CALL ingress test3 "DIDL\x00\x00" +//CALL ingress test4 "DIDL\x00\x00"