diff --git a/doc/md/examples/grammar.txt b/doc/md/examples/grammar.txt index dd92631b14c..5d20ddf28e0 100644 --- a/doc/md/examples/grammar.txt +++ b/doc/md/examples/grammar.txt @@ -14,7 +14,7 @@ ::= 'object' - 'persistent'? 'actor' + 'persistent'? 'actor' ('[' ']')? 'module' ::= diff --git a/src/docs/extract.ml b/src/docs/extract.ml index 92cfffeca63..c25e673cc1d 100644 --- a/src/docs/extract.ml +++ b/src/docs/extract.ml @@ -140,7 +140,7 @@ struct _; } -> ( match rhs with - | Source.{ it = Syntax.ObjBlockE (sort, _, fields); _ } -> + | Source.{ it = Syntax.ObjBlockE (sort, _, _, fields); _ } -> let mk_field_xref xref = mk_xref (Xref.XClass (name, xref)) in Some ( mk_xref (Xref.XType name), @@ -155,7 +155,7 @@ struct ) | Source.{ it = Syntax.VarD ({ it = name; _ }, rhs); _ } -> ( match rhs with - | Source.{ it = Syntax.ObjBlockE (sort, _, fields); _ } -> + | Source.{ it = Syntax.ObjBlockE (sort, _, _, fields); _ } -> let mk_field_xref xref = mk_xref (Xref.XClass (name, xref)) in Some ( mk_xref (Xref.XType name), @@ -184,7 +184,7 @@ struct { it = Syntax.ClassD - (shared_pat, name, type_args, ctor, _, obj_sort, _, fields); + (shared_pat, exp_opt, name, type_args, ctor, _, obj_sort, _, fields); _; } -> let mk_field_xref xref = mk_xref (Xref.XClass (name.it, xref)) in diff --git a/src/docs/namespace.ml b/src/docs/namespace.ml index 29f3d4d47e8..c5861cb03d6 100644 --- a/src/docs/namespace.ml +++ b/src/docs/namespace.ml @@ -32,7 +32,7 @@ let from_module = | Syntax.ExpD _ -> acc | Syntax.LetD ( { it = Syntax.VarP id; _ }, - { it = Syntax.ObjBlockE (_, _, decs); _ }, + { it = Syntax.ObjBlockE (_, _, _, decs); _ }, _ ) -> let mk_nested x = mk_xref (Xref.XNested (id.it, x)) in { @@ -69,7 +69,7 @@ let from_module = (mk_xref (Xref.XValue id.it), None) acc.values; } - | Syntax.ClassD (_, id, _, _, _, _, _, _) -> + | Syntax.ClassD (_, _, id, _, _, _, _, _, _) -> { acc with types = StringMap.add id.it (mk_xref (Xref.XType id.it)) acc.types; diff --git a/src/languageServer/declaration_index.ml b/src/languageServer/declaration_index.ml index fcc9b865e81..8dee6cdd7e4 100644 --- a/src/languageServer/declaration_index.ml +++ b/src/languageServer/declaration_index.ml @@ -251,7 +251,7 @@ let populate_definitions (project_root : string) (libs : Syntax.lib list) let is_type_def dec_field = match dec_field.it.Syntax.dec.it with | Syntax.TypD (typ_id, _, _) -> Some typ_id - | Syntax.ClassD (_, typ_id, _, _, _, _, _, _) -> Some typ_id + | Syntax.ClassD (_, _, typ_id, _, _, _, _, _, _) -> Some typ_id | _ -> None in let extract_binders env (pat : Syntax.pat) = gather_pat env pat in diff --git a/src/lowering/desugar.ml b/src/lowering/desugar.ml index 7049a6d8a6c..f446b2a0def 100644 --- a/src/lowering/desugar.ml +++ b/src/lowering/desugar.ml @@ -90,8 +90,8 @@ and exp' at note = function (breakE "!" (nullE())) (* case ? v : *) (varP v) (varE v) ty).it - | S.ObjBlockE (s, (self_id_opt, _), dfs) -> - obj_block at s self_id_opt dfs note.Note.typ + | S.ObjBlockE (s, exp_opt, (self_id_opt, _), dfs) -> + obj_block at s exp_opt self_id_opt dfs note.Note.typ | S.ObjE (bs, efs) -> obj note.Note.typ efs bs | S.TagE (c, e) -> (tagE c.it (exp e)).it @@ -326,12 +326,12 @@ and mut m = match m.it with | S.Const -> Ir.Const | S.Var -> Ir.Var -and obj_block at s self_id dfs obj_typ = +and obj_block at s exp_opt self_id dfs obj_typ = match s.it with | T.Object | T.Module -> build_obj at s.it self_id dfs obj_typ | T.Actor -> - build_actor at [] self_id dfs obj_typ + build_actor at [] exp_opt self_id dfs obj_typ | T.Memory -> assert false and build_field {T.lab; T.typ;_} = @@ -532,7 +532,7 @@ and export_runtime_information self_id = )], [{ it = I.{ name = lab; var = v }; at = no_region; note = typ }]) -and build_actor at ts self_id es obj_typ = +and build_actor at ts exp_opt self_id es obj_typ = let candid = build_candid ts obj_typ in let fs = build_fields obj_typ in let es = List.filter (fun ef -> is_not_typD ef.it.S.dec) es in @@ -812,7 +812,8 @@ and dec' at n = function end | S.VarD (i, e) -> I.VarD (i.it, e.note.S.note_typ, exp e) | S.TypD _ -> assert false - | S.ClassD (sp, id, tbs, p, _t_opt, s, self_id, dfs) -> + | S.ClassD (sp, exp_opt, id, tbs, p, _t_opt, s, self_id, dfs) -> + (* TODO exp_opt *) let id' = {id with note = ()} in let sort, _, _, _, _ = Type.as_func n.S.note_typ in let op = match sp.it with @@ -839,13 +840,13 @@ and dec' at n = function let (_, _, obj_typ) = T.as_async rng_typ in let c = Cons.fresh T.default_scope_var (T.Abs ([], T.scope_bound)) in 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); + (wrap { it = obj_block at s exp_opt (Some self_id) dfs (T.promote obj_typ); at = at; note = Note.{def with typ = obj_typ } }) (List.hd inst) else wrap - { it = obj_block at s (Some self_id) dfs rng_typ; + { it = obj_block at s exp_opt (Some self_id) dfs rng_typ; at = at; note = Note.{ def with typ = rng_typ } } in @@ -1023,7 +1024,7 @@ let import_compiled_class (lib : S.comp_unit) wasm : import_declaration = let f = lib.note.filename in let { body; _ } = lib.it in let id = match body.it with - | S.ActorClassU (_, id, _, _, _, _, _) -> id.it + | S.ActorClassU (_, _, id, _, _, _, _, _) -> id.it | _ -> assert false in let fun_typ = T.normalize body.note.S.note_typ in @@ -1118,7 +1119,8 @@ let transform_unit_body (u : S.comp_unit_body) : Ir.comp_unit = I.LibU ([], { it = build_obj u.at T.Module self_id fields u.note.S.note_typ; at = u.at; note = typ_note u.note}) - | S.ActorClassU (sp, typ_id, _tbs, p, _, self_id, fields) -> + | S.ActorClassU (sp, exp_opt, typ_id, _tbs, p, _, self_id, fields) -> + (* TODO exp_opt *) let fun_typ = u.note.S.note_typ in let op = match sp.it with | T.Local -> None @@ -1134,7 +1136,7 @@ let transform_unit_body (u : S.comp_unit_body) : Ir.comp_unit = T.promote rng | _ -> assert false in - let actor_expression = build_actor u.at ts (Some self_id) fields obj_typ in + let actor_expression = build_actor u.at ts exp_opt (Some self_id) fields obj_typ in let e = wrap { it = actor_expression; at = no_region; @@ -1145,8 +1147,8 @@ let transform_unit_body (u : S.comp_unit_body) : Ir.comp_unit = I.ActorU (Some args, ds, fs, u, t) | _ -> assert false end - | S.ActorU (self_id, fields) -> - let actor_expression = build_actor u.at [] self_id fields u.note.S.note_typ in + | S.ActorU (exp_opt, self_id, fields) -> + let actor_expression = build_actor u.at [] exp_opt self_id fields u.note.S.note_typ in begin match actor_expression with | I.ActorE (ds, fs, u, t) -> I.ActorU (None, ds, fs, u, t) @@ -1182,7 +1184,7 @@ let import_unit (u : S.comp_unit) : import_declaration = raise (Invalid_argument "Desugar: Cannot import actor") | I.ActorU (Some as_, ds, fs, up, actor_t) -> let id = match body.it with - | S.ActorClassU (_, id, _, _, _, _, _) -> id.it + | S.ActorClassU (_, _, id, _, _, _, _, _) -> id.it | _ -> assert false in let s, cntrl, tbs, ts1, ts2 = T.as_func t in diff --git a/src/mo_def/arrange.ml b/src/mo_def/arrange.ml index 12cb3fecb10..0e26670c865 100644 --- a/src/mo_def/arrange.ml +++ b/src/mo_def/arrange.ml @@ -69,7 +69,10 @@ module Make (Cfg : Config) = struct | FromCandidE e -> "FromCandidE" $$ [exp e] | TupE es -> "TupE" $$ exps es | ProjE (e, i) -> "ProjE" $$ [exp e; Atom (string_of_int i)] - | ObjBlockE (s, nt, dfs) -> "ObjBlockE" $$ [obj_sort s; + | ObjBlockE (s, po, nt, dfs) -> "ObjBlockE" $$ [obj_sort s; + (match po with + | None -> Atom "_" + | Some e -> exp e); match nt with | None, None -> Atom "_" | None, Some t -> typ t @@ -267,8 +270,9 @@ module Make (Cfg : Config) = struct | VarD (x, e) -> "VarD" $$ [id x; exp e] | TypD (x, tp, t) -> "TypD" $$ [id x] @ List.map typ_bind tp @ [typ t] - | ClassD (sp, x, tp, p, rt, s, i', dfs) -> - "ClassD" $$ shared_pat sp :: id x :: List.map typ_bind tp @ [ + | ClassD (sp, po, x, tp, p, rt, s, i', dfs) -> + "ClassD" $$ shared_pat sp :: id x :: List.map typ_bind tp @ [ + (match po with None -> Atom "_" | Some e -> exp e); pat p; (match rt with None -> Atom "_" | Some t -> typ t); obj_sort s; id i' diff --git a/src/mo_def/compUnit.ml b/src/mo_def/compUnit.ml index a71aafa29de..aaf9a9c927b 100644 --- a/src/mo_def/compUnit.ml +++ b/src/mo_def/compUnit.ml @@ -9,20 +9,20 @@ 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; _}, _po, _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 }) ; _ }) -> - fields, note, at + | AwaitE (Type.Fut, { it = AsyncE (Type.Fut, _, {it = ObjBlockE ({ it = Type.Actor;_}, po, _t, fields); note; at }) ; _ }) -> + po, fields, note, at | _ -> assert false let is_module_def e = let open Source in match e.it with - | ObjBlockE ({ it = Type.Module; _}, _, _) -> true + | ObjBlockE ({ it = Type.Module; _}, _, _, _) -> true | _ -> false (* Happens after parsing, before type checking *) @@ -42,20 +42,20 @@ let comp_unit_of_prog as_lib (prog : prog) : comp_unit = go (i :: imports) ds' (* terminal expressions *) - | [{it = ExpD ({it = ObjBlockE ({it = Type.Module; _}, _t, fields); _} as e); _}] when as_lib -> + | [{it = ExpD ({it = ObjBlockE ({it = Type.Module; _}, po, _t, fields); _} as e); _}] when as_lib -> finish imports { it = ModuleU (None, fields); note = e.note; at = e.at } | [{it = ExpD e; _} ] when is_actor_def e -> - let fields, note, at = as_actor_def e in - finish imports { it = ActorU (None, fields); note; at } - | [{it = ClassD (sp, tid, tbs, p, typ_ann, {it = Type.Actor;_}, self_id, fields); _} as d] -> - assert (List.length tbs > 0); - finish imports { it = ActorClassU (sp, tid, tbs, p, typ_ann, self_id, fields); note = d.note; at = d.at } + let po, fields, note, at = as_actor_def e in + finish imports { it = ActorU (po, None, fields); note; at } + | [{it = ClassD (sp, po, tid, tbs, p, typ_ann, {it = Type.Actor;_}, self_id, fields); _} as d] -> + assert (List.length tbs > 0); (* TODO: record _po *) + finish imports { it = ActorClassU (sp, po, tid, tbs, p, typ_ann, self_id, fields); note = d.note; at = d.at } (* let-bound terminal expressions *) - | [{it = LetD ({it = VarP i1; _}, ({it = ObjBlockE ({it = Type.Module; _}, _t, fields); _} as e), _); _}] when as_lib -> + | [{it = LetD ({it = VarP i1; _}, ({it = ObjBlockE ({it = Type.Module; _}, _po, _t, fields); _} as e), _); _}] when as_lib -> finish imports { it = ModuleU (Some i1, fields); note = e.note; at = e.at } | [{it = LetD ({it = VarP i1; _}, e, _); _}] when is_actor_def e -> - let fields, note, at = as_actor_def e in - finish imports { it = ActorU (Some i1, fields); note; at } + let po, fields, note, at = as_actor_def e in (* TODO: record _po *) + finish imports { it = ActorU (po, Some i1, fields); note; at } (* Everything else is a program *) | ds' -> @@ -80,14 +80,14 @@ let obj_decs obj_sort at note id_opt fields = match id_opt with | None -> [ { it = ExpD { - it = ObjBlockE ( { it = obj_sort; at; note = () }, (None, None), fields); + it = ObjBlockE ( { it = obj_sort; at; note = () }, None, (None, None), fields); at; note }; at; note }] | Some id -> [ { it = LetD ( { it = VarP id; at; note = note.note_typ }, - { it = ObjBlockE ({ it = obj_sort; at; note = () }, (None, None), fields); + { it = ObjBlockE ({ it = obj_sort; at; note = () }, None, (None, None), fields); at; note; }, None); at; note @@ -116,8 +116,8 @@ let decs_of_lib (cu : comp_unit) = match cub.it with | ModuleU (id_opt, fields) -> obj_decs Type.Module cub.at cub.note id_opt fields - | ActorClassU (csp, i, tbs, p, t, i', efs) -> - [{ it = ClassD (csp, i, tbs, p, t, { it = Type.Actor; at = no_region; note = ()}, i', efs); + | ActorClassU (csp, po, i, tbs, p, t, i', efs) -> (* TODO : restor po *) + [{ it = ClassD (csp, po, i, tbs, p, t,{ it = Type.Actor; at = no_region; note = ()}, i', efs); at = cub.at; note = cub.note;}]; | ProgU _ diff --git a/src/mo_def/syntax.ml b/src/mo_def/syntax.ml index 5917938b628..87cf9b5485d 100644 --- a/src/mo_def/syntax.ml +++ b/src/mo_def/syntax.ml @@ -165,7 +165,7 @@ and exp' = | OptE of exp (* option injection *) | DoOptE of exp (* option monad *) | BangE of exp (* scoped option projection *) - | ObjBlockE of obj_sort * (id option * typ option) * dec_field list (* object block *) + | ObjBlockE of obj_sort * exp option * (id option * typ option) * dec_field list (* object block *) | ObjE of exp list * exp_field list (* record literal/extension *) | TagE of id * exp (* variant *) | DotE of exp * id (* object projection *) @@ -223,7 +223,7 @@ and dec' = | VarD of id * exp (* mutable *) | TypD of typ_id * typ_bind list * typ (* type *) | ClassD of (* class *) - sort_pat * typ_id * typ_bind list * pat * typ option * obj_sort * id * dec_field list + sort_pat * exp option * typ_id * typ_bind list * pat * typ option * obj_sort * id * dec_field list (* Program (pre unit detection) *) @@ -245,10 +245,10 @@ and import' = pat * string * resolved_import ref type comp_unit_body = (comp_unit_body', typ_note) Source.annotated_phrase and comp_unit_body' = | ProgU of dec list (* main programs *) - | ActorU of id option * dec_field list (* main IC actor *) + | ActorU of exp option * id option * dec_field list (* main IC actor *) | ModuleU of id option * dec_field list (* module library *) | ActorClassU of (* IC actor class, main or library *) - sort_pat * typ_id * typ_bind list * pat * typ option * id * dec_field list + sort_pat * exp option * typ_id * typ_bind list * pat * typ option * id * dec_field list type comp_unit = (comp_unit', prog_note) Source.annotated_phrase and comp_unit' = { diff --git a/src/mo_frontend/definedness.ml b/src/mo_frontend/definedness.ml index e920c325390..573b41590ae 100644 --- a/src/mo_frontend/definedness.ml +++ b/src/mo_frontend/definedness.ml @@ -90,7 +90,8 @@ let rec exp msgs e : f = match e.it with (* Uses are delayed by function expressions *) | FuncE (_, sp, tp, p, t, _, e) -> delayify ((exp msgs e /// pat msgs p) /// shared_pat msgs sp) - | ObjBlockE (s, (self_id_opt, _), dfs) -> + | ObjBlockE (s, eo, (self_id_opt, _), dfs) -> + (* TODO eo *) group msgs (add_self self_id_opt s (dec_fields msgs dfs)) (* The rest remaining cases just collect the uses of subexpressions: *) | LitE _ @@ -177,7 +178,8 @@ and dec msgs d = match d.it with | LetD (p, e, Some f) -> pat msgs p +++ exp msgs e +++ exp msgs f | VarD (i, e) -> (M.empty, S.singleton i.it) +++ exp msgs e | TypD (i, tp, t) -> (M.empty, S.empty) - | ClassD (csp, i, tp, p, t, s, i', dfs) -> + | ClassD (csp, eo, i, tp, p, t, s, i', dfs) -> + (* TODO eo *) (M.empty, S.singleton i.it) +++ delayify ( group msgs (add_self (Some i') s (dec_fields msgs dfs)) /// pat msgs p /// shared_pat msgs csp ) diff --git a/src/mo_frontend/effect.ml b/src/mo_frontend/effect.ml index 0ed989d7bc6..256a4ce4750 100644 --- a/src/mo_frontend/effect.ml +++ b/src/mo_frontend/effect.ml @@ -99,7 +99,8 @@ let rec infer_effect_exp (exp:Syntax.exp) : T.eff = map_max_effs effect_exp exps | BlockE decs -> map_max_effs effect_dec decs - | ObjBlockE (sort, _, dfs) -> + | ObjBlockE (sort, _, _, dfs) -> + (* TODO *) infer_effect_dec_fields dfs | ObjE (bases, efs) -> let bases = map_max_effs effect_exp bases in diff --git a/src/mo_frontend/parser.mly b/src/mo_frontend/parser.mly index daaf62cf7ca..24f54aed881 100644 --- a/src/mo_frontend/parser.mly +++ b/src/mo_frontend/parser.mly @@ -108,7 +108,7 @@ let is_sugared_func_or_module dec = match dec.it with | LetD({it = VarP _; _} as pat, exp, None) -> dec.at = pat.at && pat.at = exp.at && (match exp.it with - | ObjBlockE (sort, _, _) -> + | ObjBlockE (sort, _, _, _) -> sort.it = Type.Module | FuncE _ -> true @@ -207,13 +207,13 @@ let share_dec_field default_stab (df : dec_field) = } -and objblock s id ty dec_fields = +and objblock s po id ty dec_fields = List.iter (fun df -> match df.it.vis.it, df.it.dec.it with - | Public _, ClassD (_, id, _, _, _, _, _, _) when is_anon_id id -> + | Public _, ClassD (_, _, id, _, _, _, _, _, _) when is_anon_id id -> syntax_error df.it.dec.at "M0158" "a public class cannot be anonymous, please provide a name" | _ -> ()) dec_fields; - ObjBlockE(s, (id, ty), dec_fields) + ObjBlockE(s, po, (id, ty), dec_fields) %} @@ -371,13 +371,17 @@ seplist1(X, SEP) : | ACTOR { Type.Actor @@ at $sloc } | MODULE {Type.Module @@ at $sloc } +%inline migration : + | LBRACKET e=exp(ob) RBRACKET { Some e } + | (* empty *) { None } + %inline obj_sort : - | OBJECT { (false, Type.Object @@ at $sloc) } - | po=persistent ACTOR { (po, Type.Actor @@ at $sloc) } - | MODULE { (false, Type.Module @@ at $sloc) } + | OBJECT { (false, Type.Object @@ at $sloc, None) } + | po=persistent ACTOR m=migration { (po, Type.Actor @@ at $sloc, m) } + | MODULE { (false, Type.Module @@ at $sloc, None) } %inline obj_sort_opt : - | (* empty *) { (false, Type.Object @@ no_region) } + | (* empty *) { (false, Type.Object @@ no_region, None) } | ds=obj_sort { ds } %inline query: @@ -887,7 +891,7 @@ dec_nonvar : | TYPE x=typ_id tps=type_typ_params_opt EQ t=typ { TypD(x, tps, t) @? at $sloc } | ds=obj_sort xf=id_opt t=annot_opt EQ? efs=obj_body - { let (persistent, s) = ds in + { let (persistent, s, po) = ds in let sort = Type.(match s.it with | Actor -> "actor" | Module -> "module" | Object -> "object" | _ -> assert false) in @@ -899,9 +903,9 @@ dec_nonvar : AwaitE (Type.Fut, AsyncE(Type.Fut, scope_bind (anon_id "async" (at $sloc)) (at $sloc), - objblock s id t (List.map (share_dec_field default_stab) efs) @? at $sloc) + objblock s po id t (List.map (share_dec_field default_stab) efs) @? at $sloc) @? at $sloc) @? at $sloc - else objblock s None t efs @? at $sloc + else objblock s po None t efs @? at $sloc in let_or_exp named x e.it e.at } | sp=shared_pat_opt FUNC xf=id_opt @@ -914,7 +918,7 @@ dec_nonvar : let_or_exp named x (func_exp x.it sp tps p t is_sugar e) (at $sloc) } | sp=shared_pat_opt ds=obj_sort_opt CLASS xf=typ_id_opt tps=typ_params_opt p=pat_plain t=annot_opt cb=class_body - { let (persistent, s) = ds in + { let (persistent, s, eo) = ds in let x, dfs = cb in let dfs', tps', t' = if s.it = Type.Actor then @@ -925,7 +929,7 @@ dec_nonvar : ensure_async_typ t) else (dfs, tps, t) in - ClassD(sp, xf "class" $sloc, tps', p, t', s, x, dfs') @? at $sloc } + ClassD(sp, eo, xf "class" $sloc, tps', p, t', s, x, dfs') @? at $sloc } dec : | d=dec_var diff --git a/src/mo_frontend/static.ml b/src/mo_frontend/static.ml index 08f3871784d..2faf3c1f60f 100644 --- a/src/mo_frontend/static.ml +++ b/src/mo_frontend/static.ml @@ -44,7 +44,7 @@ let rec exp m e = match e.it with | Const -> List.iter (exp m) es | Var -> err m e.at end - | ObjBlockE (_, _, dfs) -> dec_fields m dfs + | ObjBlockE (_, _eo, _, dfs) -> dec_fields m dfs (* TODO eo *) | ObjE (bases, efs) -> List.iter (exp m) bases; exp_fields m efs (* Variable access. Dangerous, due to loops. *) diff --git a/src/mo_frontend/traversals.ml b/src/mo_frontend/traversals.ml index aba776444b3..8f866009d8f 100644 --- a/src/mo_frontend/traversals.ml +++ b/src/mo_frontend/traversals.ml @@ -54,8 +54,8 @@ let rec over_exp (f : exp -> exp) (exp : exp) : exp = match exp.it with f { exp with it = ArrayE (x, List.map (over_exp f) exps) } | BlockE ds -> f { exp with it = BlockE (List.map (over_dec f) ds) } - | ObjBlockE (x, t, dfs) -> - f { exp with it = ObjBlockE (x, t, List.map (over_dec_field f) dfs) } + | ObjBlockE (x, eo, t, dfs) -> + f { exp with it = ObjBlockE (x, Option.map (over_exp f) eo, t, List.map (over_dec_field f) dfs) } | ObjE (bases, efs) -> f { exp with it = ObjE (List.map (over_exp f) bases, List.map (over_exp_field f) efs) } | IfE (exp1, exp2, exp3) -> @@ -76,8 +76,8 @@ and over_dec (f : exp -> exp) (d : dec) : dec = match d.it with { d with it = VarD (x, over_exp f e)} | LetD (x, e, fail) -> { d with it = LetD (x, over_exp f e, Option.map (over_exp f) fail)} - | ClassD (sp, cid, tbs, p, t_o, s, id, dfs) -> - { d with it = ClassD (sp, cid, tbs, p, t_o, s, id, List.map (over_dec_field f) dfs)} + | ClassD (sp, eo, cid, tbs, p, t_o, s, id, dfs) -> + { d with it = ClassD (sp, Option.map (over_exp f) eo, cid, tbs, p, t_o, s, id, List.map (over_dec_field f) dfs)} and over_dec_field (f : exp -> exp) (df : dec_field) : dec_field = { df with it = { df.it with dec = over_dec f df.it.dec } } diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index eb0c2c36051..28174f385e7 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -1042,7 +1042,8 @@ let rec is_explicit_exp e = | ObjE (bases, efs) -> List.(for_all is_explicit_exp bases && for_all (fun (ef : exp_field) -> is_explicit_exp ef.it.exp) efs) - | ObjBlockE (_, _, dfs) -> + | ObjBlockE (_, _e_opt, _, dfs) -> + (* TODO e_opt *) List.for_all (fun (df : dec_field) -> is_explicit_dec df.it.dec) dfs | ArrayE (_, es) -> List.exists is_explicit_exp es | SwitchE (e1, cs) -> @@ -1059,7 +1060,7 @@ and is_explicit_dec d = match d.it with | ExpD e | LetD (_, e, _) | VarD (_, e) -> is_explicit_exp e | TypD _ -> true - | ClassD (_, _, _, p, _, _, _, dfs) -> + | ClassD (_, _, _, _, p, _, _, _, dfs) -> is_explicit_pat p && List.for_all (fun (df : dec_field) -> is_explicit_dec df.it.dec) dfs @@ -1358,7 +1359,7 @@ and infer_exp'' env exp : T.typ = "expected tuple type, but expression produces type%a" display_typ_expand t1 ) - | ObjBlockE (obj_sort, typ_opt, dec_fields) -> + | ObjBlockE (obj_sort, exp_opt, typ_opt, dec_fields) -> if obj_sort.it = T.Actor then begin error_in [Flags.WASIMode; Flags.WasmMode] env exp.at "M0068" "actors are not supported"; @@ -2426,7 +2427,7 @@ and pub_dec src dec xs : visibility_env = | ExpD _ -> xs | LetD (pat, _, _) -> pub_pat src pat xs | VarD (id, _) -> pub_val_id src id xs - | ClassD (_, id, _, _, _, _, _, _) -> + | ClassD (_, _, id, _, _, _, _, _, _) -> pub_val_id src {id with note = ()} (pub_typ_id src id xs) | TypD (id, _, _) -> pub_typ_id src id xs @@ -2633,7 +2634,7 @@ and infer_block env decs at check_unused : T.typ * Scope.scope = | Flags.(ICMode | RefMode) -> List.fold_left (fun ve' dec -> match dec.it with - | ClassD(_, id, _, _, _, { it = T.Actor; _}, _, _) -> + | ClassD(_, _, id, _, _, _, { it = T.Actor; _}, _, _) -> T.Env.mapi (fun id' (typ, at, kind, avl) -> (typ, at, kind, if id' = id.it then Unavailable else avl)) ve' | _ -> ve') env'.vals decs @@ -2682,7 +2683,8 @@ and infer_dec env dec : T.typ = | VarD (_, exp) -> if not env.pre then ignore (infer_exp env exp); T.unit - | ClassD (shared_pat, id, typ_binds, pat, typ_opt, obj_sort, self_id, dec_fields) -> + | ClassD (shared_pat, exp_opt, id, typ_binds, pat, typ_opt, obj_sort, self_id, dec_fields) -> + (*TODO exp_opt *) let (t, _, _, _) = T.Env.find id.it env.vals in if not env.pre then begin let c = T.Env.find id.it env.typs in @@ -2808,8 +2810,8 @@ and gather_dec env scope dec : Scope.t = (* TODO: generalize beyond let = *) | 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 = ObjBlockE (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 @@ -2827,7 +2829,7 @@ and gather_dec env scope dec : Scope.t = } | LetD (pat, _, _) -> Scope.adjoin_val_env scope (gather_pat env scope.Scope.val_env pat) | VarD (id, _) -> Scope.adjoin_val_env scope (gather_id env scope.Scope.val_env id Scope.Declaration) - | TypD (id, binds, _) | ClassD (_, id, binds, _, _, _, _, _) -> + | TypD (id, binds, _) | ClassD (_, _, id, binds, _, _, _, _, _) -> let open Scope in if T.Env.mem id.it scope.typ_env then error_duplicate env "type " id; @@ -2896,8 +2898,8 @@ and infer_dec_typdecs env dec : Scope.t = (* TODO: generalize beyond let = *) | 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 = ObjBlockE (obj_sort, _exp_opt, _t, dec_fields); at; _} + | {it = AwaitE (_, { it = AsyncE (_, _, {it = ObjBlockE ({ it = Type.Actor; _} as obj_sort, _exp_opt, _t, dec_fields); at; _}) ; _ }); _ }), _ ) -> let decs = List.map (fun {it = {vis; dec; _}; _} -> dec) dec_fields in @@ -2929,7 +2931,8 @@ and infer_dec_typdecs env dec : Scope.t = typ_env = T.Env.singleton id.it c; con_env = infer_id_typdecs env dec.at id c k; } - | ClassD (shared_pat, id, binds, pat, _typ_opt, obj_sort, self_id, dec_fields) -> + | ClassD (shared_pat, exp_opt, id, binds, pat, _typ_opt, obj_sort, self_id, dec_fields) -> + (*TODO exp_opt *) let c = T.Env.find id.it env.typs in let ve0 = check_class_shared_pat {env with pre = true} shared_pat obj_sort in let cs, tbs, te, ce = check_typ_binds {env with pre = true} binds in @@ -2982,8 +2985,8 @@ and infer_dec_valdecs env dec : Scope.t = (* TODO: generalize beyond let = *) | 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 = ObjBlockE (obj_sort, _exp_opt, _t, dec_fields); at; _} + | {it = AwaitE (_, { it = AsyncE (_, _, {it = ObjBlockE ({ it = Type.Actor; _} as obj_sort, _exp_opt, _t, dec_fields); at; _}) ; _ }); _ }), _ ) -> let decs = List.map (fun df -> df.it.dec) dec_fields in @@ -3012,7 +3015,8 @@ and infer_dec_valdecs env dec : Scope.t = typ_env = T.Env.singleton id.it c; con_env = T.ConSet.singleton c; } - | ClassD (_shared_pat, id, typ_binds, pat, _, obj_sort, _, _) -> + | ClassD (_shared_pat, _exp_opt, id, typ_binds, pat, _, obj_sort, _, _) -> + (* TODO exp_opt *) if obj_sort.it = T.Actor then begin error_in [Flags.WASIMode; Flags.WasmMode] env dec.at "M0138" "actor classes are not supported"; if not env.in_prog then @@ -3066,7 +3070,7 @@ let is_actor_dec d = match d.it with | ExpD e | LetD (_, e, _) -> CompUnit.is_actor_def e - | ClassD (shared_pat, id, typ_binds, pat, typ_opt, obj_sort, self_id, dec_fields) -> + | ClassD (shared_pat, exp_opt, id, typ_binds, pat, typ_opt, obj_sort, self_id, dec_fields) -> obj_sort.it = T.Actor | _ -> false @@ -3121,7 +3125,8 @@ let check_lib scope pkg_opt lib : Scope.t Diag.result = warn env r "M0142" "deprecated syntax: an imported library should be a module or named actor class" end; typ - | ActorClassU (sp, id, tbs, p, _, self_id, dec_fields) -> + | ActorClassU (sp, exp_opt, id, tbs, p, _, self_id, dec_fields) -> + (* TODO exp_opt *) if is_anon_id id then error env cub.at "M0143" "bad import: imported actor class cannot be anonymous"; let cs = List.map (fun tb -> Option.get tb.note) tbs in diff --git a/src/mo_interpreter/interpret.ml b/src/mo_interpreter/interpret.ml index ec3a30736cb..06dca26d1df 100644 --- a/src/mo_interpreter/interpret.ml +++ b/src/mo_interpreter/interpret.ml @@ -491,7 +491,8 @@ and interpret_exp_mut env exp (k : V.value V.cont) = | _ -> assert false) | ProjE (exp1, n) -> interpret_exp env exp1 (fun v1 -> k (List.nth (V.as_tup v1) n)) - | ObjBlockE (obj_sort, (self_id_opt, _), dec_fields) -> + | ObjBlockE (obj_sort, exp_opt, (self_id_opt, _), dec_fields) -> + (*TODO*) interpret_obj env obj_sort.it self_id_opt dec_fields k | ObjE (exp_bases, exp_fields) -> let fields fld_env = interpret_exp_fields env exp_fields fld_env (fun env -> k (V.Obj env)) in @@ -946,7 +947,7 @@ and declare_dec dec : val_env = | TypD _ -> V.Env.empty | LetD (pat, _, _) -> declare_pat pat | VarD (id, _) -> declare_id id - | ClassD (_, id, _, _, _, _, _, _) -> declare_id {id with note = ()} + | ClassD (_, _eo, id, _, _, _, _, _, _) -> declare_id {id with note = ()} and declare_decs decs ve : val_env = match decs with @@ -976,7 +977,8 @@ and interpret_dec env dec (k : V.value V.cont) = ) | TypD _ -> k V.unit - | ClassD (shared_pat, id, _typbinds, pat, _typ_opt, obj_sort, id', dec_fields) -> + | ClassD (shared_pat, _eo, id, _typbinds, pat, _typ_opt, obj_sort, id', dec_fields) -> + (* TODO _eo *) let f = interpret_func env id.it shared_pat pat (fun env' k' -> if obj_sort.it <> T.Actor then let env'' = adjoin_vals env' (declare_id id') in @@ -1088,7 +1090,8 @@ let import_lib env lib = match cub.it with | Syntax.ModuleU _ -> Fun.id - | Syntax.ActorClassU (_sp, id, _tbs, _p, _typ, _self_id, _dec_fields) -> + | Syntax.ActorClassU (_sp, _eo, id, _tbs, _p, _typ, _self_id, _dec_fields) -> + (* TODO eo *) fun v -> V.Obj (V.Env.from_list [ (id.it, v); ("system", diff --git a/src/viper/prep.ml b/src/viper/prep.ml index b2d019eaecf..7155c85aecc 100644 --- a/src/viper/prep.ml +++ b/src/viper/prep.ml @@ -137,10 +137,11 @@ let mono_dec_fields (dfs : dec_field list) : dec_field list = let prep_unit (u : comp_unit) : comp_unit = let { imports; body } = u.it in match body.it with - | ActorU(id_opt, decs) -> + | ActorU(id_opt, exp_opt, decs) -> + (* TODO exp_opt (also below) *) let decs' = mono_dec_fields decs in (* let _ = List.map (fun g -> print_endline (string_of_mono_goal g)) goals in *) - let body' = ActorU(id_opt, decs') in + let body' = ActorU(id_opt, exp_opt, decs') in (* let _ = List.map (fun d -> print_endline (Wasm.Sexpr.to_string 80 (Arrange.dec_field d))) decs' in *) { u with it = {imports; body = { body with it = body' } } } | _ -> u diff --git a/src/viper/trans.ml b/src/viper/trans.ml index ef19b23bd57..4df72efd8e0 100644 --- a/src/viper/trans.ml +++ b/src/viper/trans.ml @@ -232,7 +232,8 @@ let rec unit reqs (u : M.comp_unit) : prog Diag.result = and unit' reqs (u : M.comp_unit) : prog = let { M.imports; M.body } = u.it in match body.it with - | M.ActorU(id_opt, decs) -> + | M.ActorU(eo_, id_opt, decs) -> + (* TODO eo *) let ctxt = { self = None; imports = tr_imports imports; diff --git a/src/viper/traversals.ml b/src/viper/traversals.ml index bdf02154c6e..0d8b279bcf8 100644 --- a/src/viper/traversals.ml +++ b/src/viper/traversals.ml @@ -48,7 +48,7 @@ let rec over_exp (v : visitor) (exp : exp) : exp = | TupE exps -> { exp with it = TupE (List.map (over_exp v) exps) } | ArrayE (x, exps) -> { exp with it = ArrayE (x, List.map (over_exp v) exps) } | BlockE ds -> { exp with it = BlockE (List.map (over_dec v) ds) } - | ObjBlockE (x, (n, t), dfs) -> { exp with it = ObjBlockE (x, (n, Option.map (over_typ v) t), List.map (over_dec_field v) dfs) } + | ObjBlockE (x, eo, (n, t), dfs) -> { exp with it = ObjBlockE (x, Option.map (over_exp v) eo, (n, Option.map (over_typ v) t), List.map (over_dec_field v) dfs) } | ObjE (bases, efs) -> { exp with it = ObjE (List.map (over_exp v) bases, List.map (over_exp_field v) efs) } | IfE (exp1, exp2, exp3) -> { exp with it = IfE(over_exp v exp1, over_exp v exp2, over_exp v exp3) } | TryE (exp1, cases, exp2) -> { exp with it = TryE (over_exp v exp1, List.map (over_case v) cases, Option.map (over_exp v) exp2) } @@ -76,7 +76,7 @@ and over_dec (v : visitor) (d : dec) : dec = | ExpD e -> { d with it = ExpD (over_exp v e)} | VarD (x, e) -> { d with it = VarD (x, over_exp v e)} | LetD (p, e, fail) -> { d with it = LetD (over_pat v p, over_exp v e, Option.map (over_exp v) fail)} - | ClassD (sp, cid, tbs, p, t_o, s, id, dfs) -> { d with it = ClassD (sp, cid, tbs, over_pat v p, Option.map (over_typ v) t_o, s, id, List.map (over_dec_field v) dfs)}) + | ClassD (sp, e_o, cid, tbs, p, t_o, s, id, dfs) -> { d with it = ClassD (sp, Option.map (over_exp v) e_o, cid, tbs, over_pat v p, Option.map (over_typ v) t_o, s, id, List.map (over_dec_field v) dfs)}) and over_dec_field (v : visitor) (df : dec_field) : dec_field = { df with it = { df.it with dec = over_dec v df.it.dec } }