Skip to content

Commit

Permalink
refactor ActorU and ClassD
Browse files Browse the repository at this point in the history
  • Loading branch information
crusso committed Feb 1, 2025
1 parent 33f1e40 commit 9259ddd
Show file tree
Hide file tree
Showing 13 changed files with 33 additions and 32 deletions.
6 changes: 3 additions & 3 deletions src/docs/extract.ml
Original file line number Diff line number Diff line change
Expand Up @@ -184,13 +184,13 @@ struct
{
it =
Syntax.ClassD
( shared_pat,
exp_opt,
( exp_opt,
shared_pat,
obj_sort,
name,
type_args,
ctor,
_,
obj_sort,
_,
fields );
_;
Expand Down
2 changes: 1 addition & 1 deletion src/docs/namespace.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
2 changes: 1 addition & 1 deletion src/languageServer/declaration_index.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions src/lowering/desugar.ml
Original file line number Diff line number Diff line change
Expand Up @@ -901,7 +901,7 @@ 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, exp_opt, id, tbs, p, _t_opt, s, self_id, dfs) ->
| S.ClassD (exp_opt, sp, s, id, tbs, p, _t_opt, self_id, dfs) ->
let id' = {id with note = ()} in
let sort, _, _, _, _ = Type.as_func n.S.note_typ in
let op = match sp.it with
Expand Down Expand Up @@ -1224,7 +1224,7 @@ 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, exp_opt, typ_id, _tbs, p, _, self_id, fields) ->
| S.ActorClassU (exp_opt, sp, typ_id, _tbs, p, _, self_id, fields) ->
let fun_typ = u.note.S.note_typ in
let op = match sp.it with
| T.Local -> None
Expand Down
7 changes: 4 additions & 3 deletions src/mo_def/arrange.ml
Original file line number Diff line number Diff line change
Expand Up @@ -270,14 +270,15 @@ 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, eo, x, tp, p, rt, s, i', dfs) ->
| ClassD (eo, sp, s, x, tp, p, rt, i, dfs) ->
"ClassD" $$
shared_pat sp ::
(match eo with None -> Atom "_" | Some e -> exp e) ::
shared_pat sp ::
obj_sort s ::
id x :: List.map typ_bind tp @ [
pat p;
(match rt with None -> Atom "_" | Some t -> typ t);
obj_sort s; id i'
id i
] @ List.map dec_field dfs))

and prog p = "Prog" $$ List.map dec p.it
Expand Down
8 changes: 4 additions & 4 deletions src/mo_def/compUnit.ml
Original file line number Diff line number Diff line change
Expand Up @@ -47,9 +47,9 @@ let comp_unit_of_prog as_lib (prog : prog) : comp_unit =
| [{it = ExpD e; _} ] when is_actor_def e ->
let eo, fields, note, at = as_actor_def e in
finish imports { it = ActorU (eo, None, fields); note; at }
| [{it = ClassD (sp, eo, tid, tbs, p, typ_ann, {it = Type.Actor;_}, self_id, fields); _} as d] ->
| [{it = ClassD (eo, sp, {it = Type.Actor;_}, tid, tbs, p, typ_ann, self_id, fields); _} as d] ->
assert (List.length tbs > 0);
finish imports { it = ActorClassU (sp, eo, tid, tbs, p, typ_ann, self_id, fields); note = d.note; at = d.at }
finish imports { it = ActorClassU (eo, sp, 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; _}, _eo, _t, fields); _} as e), _); _}] when as_lib ->
finish imports { it = ModuleU (Some i1, fields); note = e.note; at = e.at }
Expand Down Expand Up @@ -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, eo, i, tbs, p, t, i', efs) ->
[{ it = ClassD (csp, eo, i, tbs, p, t,{ it = Type.Actor; at = no_region; note = ()}, i', efs);
| ActorClassU (eo, csp, i, tbs, p, t, i', efs) ->
[{ it = ClassD (eo, csp, { it = Type.Actor; at = no_region; note = ()}, i, tbs, p, t, i', efs);
at = cub.at;
note = cub.note;}];
| ProgU _
Expand Down
4 changes: 2 additions & 2 deletions src/mo_def/syntax.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 * exp option * typ_id * typ_bind list * pat * typ option * obj_sort * id * dec_field list
exp option * sort_pat * obj_sort * typ_id * typ_bind list * pat * typ option * id * dec_field list


(* Program (pre unit detection) *)
Expand Down Expand Up @@ -252,7 +252,7 @@ and comp_unit_body' =
| 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 * exp option * typ_id * typ_bind list * pat * typ option * id * dec_field list
exp option * sort_pat * 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' = {
Expand Down
2 changes: 1 addition & 1 deletion src/mo_frontend/definedness.ml
Original file line number Diff line number Diff line change
Expand Up @@ -181,7 +181,7 @@ 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, eo, i, tp, p, t, s, i', dfs) ->
| ClassD (eo, csp, s, i, tp, p, t, i', dfs) ->
((M.empty, S.singleton i.it) +++
(* TBR: treatment of eo *)
(match eo with
Expand Down
4 changes: 2 additions & 2 deletions src/mo_frontend/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -210,7 +210,7 @@ let share_dec_field default_stab (df : dec_field) =
and objblock s eo 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, eo, (id, ty), dec_fields)
Expand Down Expand Up @@ -935,7 +935,7 @@ dec_nonvar :
ensure_async_typ t)
else (dfs, tps, t)
in
ClassD(sp, eo, xf "class" $sloc, tps', p, t', s, x, dfs') @? at $sloc }
ClassD(eo, sp, s, xf "class" $sloc, tps', p, t', x, dfs') @? at $sloc }

dec :
| d=dec_var
Expand Down
4 changes: 2 additions & 2 deletions src/mo_frontend/traversals.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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, 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)}
| ClassD (e_o, sp, s, cid, tbs, p, t_o, id, dfs) ->
{ d with it = ClassD (Option.map (over_exp f) e_o, sp, s, cid, tbs, p, t_o, 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 } }
Expand Down
16 changes: 8 additions & 8 deletions src/mo_frontend/typing.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1052,7 +1052,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

Expand Down Expand Up @@ -2420,7 +2420,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

Expand Down Expand Up @@ -2761,7 +2761,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(_, _, { it = T.Actor; _}, id, _, _, _, _, _) ->
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
Expand Down Expand Up @@ -2810,7 +2810,7 @@ and infer_dec env dec : T.typ =
| VarD (_, exp) ->
if not env.pre then ignore (infer_exp env exp);
T.unit
| ClassD (shared_pat, exp_opt, id, typ_binds, pat, typ_opt, obj_sort, self_id, dec_fields) ->
| ClassD (exp_opt, shared_pat, obj_sort, id, typ_binds, pat, typ_opt, self_id, dec_fields) ->
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
Expand Down Expand Up @@ -2956,7 +2956,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;
Expand Down Expand Up @@ -3058,7 +3058,7 @@ 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, exp_opt, id, binds, pat, _typ_opt, obj_sort, self_id, dec_fields) ->
| ClassD (exp_opt, shared_pat, obj_sort, id, binds, pat, _typ_opt, 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
Expand Down Expand Up @@ -3142,7 +3142,7 @@ 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, _exp_opt, id, typ_binds, pat, _, obj_sort, _, _) ->
| ClassD (_exp_opt, _shared_pat, obj_sort, id, typ_binds, pat, _, _, _) ->
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
Expand Down Expand Up @@ -3196,7 +3196,7 @@ let is_actor_dec d =
match d.it with
| ExpD e
| LetD (_, e, _) -> CompUnit.is_actor_def e
| ClassD (shared_pat, exp_opt, id, typ_binds, pat, typ_opt, obj_sort, self_id, dec_fields) ->
| ClassD (exp_opt, shared_pat, obj_sort, id, typ_binds, pat, typ_opt, self_id, dec_fields) ->
obj_sort.it = T.Actor
| _ -> false

Expand Down
4 changes: 2 additions & 2 deletions src/mo_interpreter/interpret.ml
Original file line number Diff line number Diff line change
Expand Up @@ -947,7 +947,7 @@ and declare_dec dec : val_env =
| TypD _ -> V.Env.empty
| LetD (pat, _, _) -> declare_pat pat
| VarD (id, _) -> declare_id id
| ClassD (_, _eo, id, _, _, _, _, _, _) -> declare_id {id with note = ()}
| ClassD (_eo, _, _, id, _, _, _, _, _) -> declare_id {id with note = ()}

and declare_decs decs ve : val_env =
match decs with
Expand Down Expand Up @@ -977,7 +977,7 @@ and interpret_dec env dec (k : V.value V.cont) =
)
| TypD _ ->
k V.unit
| ClassD (shared_pat, _eo, id, _typbinds, pat, _typ_opt, obj_sort, id', dec_fields) ->
| ClassD (_eo, shared_pat, obj_sort, id, _typbinds, pat, _typ_opt, id', dec_fields) ->
(* NB: we ignore the migration expression _eo *)
let f = interpret_func env id.it shared_pat pat (fun env' k' ->
if obj_sort.it <> T.Actor then
Expand Down
2 changes: 1 addition & 1 deletion src/viper/traversals.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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, 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)})
| ClassD (eo, sp, s, cid, tbs, p, t_o, id, dfs) -> { d with it = ClassD (Option.map (over_exp v) eo, sp, s, cid, tbs, over_pat v p, Option.map (over_typ v) t_o, 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 } }
Expand Down

0 comments on commit 9259ddd

Please sign in to comment.