Skip to content

Commit

Permalink
break out infer_check_bases_fields and use it to check just a few s…
Browse files Browse the repository at this point in the history 
…elect fields in parentheticals
  • Loading branch information
@ggreif
ggreif committed Dec 10, 2024
1 parent 0878d90 commit ec31258
Show file tree
Hide file tree
Showing 2 changed files with 99 additions and 77 deletions.
172 changes: 97 additions & 75 deletions src/mo_frontend/typing.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1213,9 +1213,9 @@ and infer_exp_promote env exp : T.typ =
display_typ_expand t;
t'

and infer_exp' f env exp : T.typ =
and infer_exp_wrapper inf f env exp : T.typ =
assert (exp.note.note_typ = T.Pre);
let t = infer_exp'' env exp in
let t = inf env exp in
assert (t <> T.Pre);
let t' = f t in
if not env.pre then begin
Expand All @@ -1226,6 +1226,8 @@ and infer_exp' f env exp : T.typ =
end;
t'

and infer_exp' f env exp : T.typ = infer_exp_wrapper infer_exp'' f env exp

and infer_exp'' env exp : T.typ =
let context = env.context in
let in_actor = env.in_actor in
Expand Down Expand Up @@ -1388,78 +1390,7 @@ and infer_exp'' env exp : T.typ =
end;
t
| ObjE (exp_bases, exp_fields) ->
let open List in
check_ids env "object" "field"
(map (fun (ef : exp_field) -> ef.it.id) exp_fields);
let fts = map (infer_exp_field env) exp_fields in
let bases = map (fun b -> infer_exp_promote env b, b) exp_bases in
let homonymous_fields ft1 ft2 = T.compare_field ft1 ft2 = 0 in

(* removing explicit fields from the bases *)
let strip (base_t, base) =
let s, base_fts =
try T.as_obj base_t with Invalid_argument _ ->
error env base.at "M0093"
"expected object type, but expression produces type%a"
display_typ_expand base_t in
(* forbid actors as bases *)
if s = T.Actor then
error env base.at "M0178"
"actors cannot serve as bases in record extensions";
T.(Obj (Object, filter (fun ft -> not (exists (homonymous_fields ft) fts)) base_fts))
in
let stripped_bases = map strip bases in

let ambiguous_fields ft1 ft2 =
homonymous_fields ft1 ft2 &&
(* allow equivalent type fields *)
match ft1.T.typ, ft2.T.typ with
(* homonymous type fields are ambiguous when unequal *)
| T.Typ c1, T.Typ c2 -> not (eq env exp.at ft1.T.typ ft2.T.typ)
(* homonymous value fields are always ambiguous *)
| _ -> true
in

(* field disjointness of stripped bases *)
let rec disjoint = function
| [] | [_] -> ()
| (h, h_exp) :: t ->
let avoid ft =
let avoid_fields b b_fts =
if exists (ambiguous_fields ft) b_fts then
begin
let frag_typ, frag_sug = match ft.T.typ with
| T.Typ c -> "type ", ""
| _ -> "", " (consider overwriting)" in
info env h_exp.at "%sfield also present in base, here%s" frag_typ frag_sug;
error env b.at "M0177"
"ambiguous %sfield in base%a"
frag_typ
display_lab ft.T.lab
end in
iter (fun (b_t, b) -> avoid_fields b (T.as_obj b_t |> snd)) t in
iter avoid (T.as_obj h |> snd);
disjoint t in
disjoint (map2 (fun b_t b -> b_t, b) stripped_bases exp_bases);

(* do not allow var fields for now (to avoid aliasing) *)
begin if not (!Flags.experimental_field_aliasing) then
let immutable_base b_typ b_exp =
let constant_field (ft : T.field) =
if T.(is_mut ft.typ) then
begin
info env b_exp.at "overwrite field to resolve error";
error env b_exp.at "M0179"
"base has non-aliasable var field%a"
display_lab ft.T.lab
end
in
iter constant_field (T.as_obj b_typ |> snd)
in
iter2 immutable_base stripped_bases exp_bases
end;
let t_base = T.(fold_left glb (Obj (Object, [])) stripped_bases) in
T.(glb t_base (Obj (Object, sort T.compare_field fts)))
infer_check_bases_fields env [] exp.at exp_bases exp_fields
| DotE (exp1, id) ->
let t1 = infer_exp_promote env exp1 in
let s, tfs =
Expand Down Expand Up @@ -1796,6 +1727,89 @@ and infer_exp_field env rf =
let t1 = if mut.it = Syntax.Var then T.Mut t else t in
T.{ lab = id.it; typ = t1; src = empty_src }

and infer_check_bases_fields env (check_fields : T.field list) exp_at exp_bases exp_fields =
let open List in
check_ids env "object" "field"
(map (fun (ef : exp_field) -> ef.it.id) exp_fields);

let infer_or_check rf =
let { mut; id; exp } = rf.it in
match List.find_opt (fun ft -> ft.T.lab = id.it) check_fields with
| Some exp_field ->
check_exp_field env rf [exp_field];
exp_field
| _ -> infer_exp_field env rf in

let fts = map infer_or_check exp_fields in
let bases = map (fun b -> infer_exp_promote env b, b) exp_bases in
let homonymous_fields ft1 ft2 = T.compare_field ft1 ft2 = 0 in

(* removing explicit fields from the bases *)
let strip (base_t, base) =
let s, base_fts =
try T.as_obj base_t with Invalid_argument _ ->
error env base.at "M0093"
"expected object type, but expression produces type%a"
display_typ_expand base_t in
(* forbid actors as bases *)
if s = T.Actor then
error env base.at "M0178"
"actors cannot serve as bases in record extensions";
T.(Obj (Object, filter (fun ft -> not (exists (homonymous_fields ft) fts)) base_fts))
in
let stripped_bases = map strip bases in

let ambiguous_fields ft1 ft2 =
homonymous_fields ft1 ft2 &&
(* allow equivalent type fields *)
match ft1.T.typ, ft2.T.typ with
(* homonymous type fields are ambiguous when unequal *)
| T.Typ c1, T.Typ c2 -> not (eq env exp_at ft1.T.typ ft2.T.typ)
(* homonymous value fields are always ambiguous *)
| _ -> true
in

(* field disjointness of stripped bases *)
let rec disjoint = function
| [] | [_] -> ()
| (h, h_exp) :: t ->
let avoid ft =
let avoid_fields b b_fts =
if exists (ambiguous_fields ft) b_fts then
begin
let frag_typ, frag_sug = match ft.T.typ with
| T.Typ c -> "type ", ""
| _ -> "", " (consider overwriting)" in
info env h_exp.at "%sfield also present in base, here%s" frag_typ frag_sug;
error env b.at "M0177"
"ambiguous %sfield in base%a"
frag_typ
display_lab ft.T.lab
end in
iter (fun (b_t, b) -> avoid_fields b (T.as_obj b_t |> snd)) t in
iter avoid (T.as_obj h |> snd);
disjoint t in
disjoint (map2 (fun b_t b -> b_t, b) stripped_bases exp_bases);

(* do not allow var fields for now (to avoid aliasing) *)
begin if not (!Flags.experimental_field_aliasing) then
let immutable_base b_typ b_exp =
let constant_field (ft : T.field) =
if T.(is_mut ft.typ) then
begin
info env b_exp.at "overwrite field to resolve error";
error env b_exp.at "M0179"
"base has non-aliasable var field%a"
display_lab ft.T.lab
end
in
iter constant_field (T.as_obj b_typ |> snd)
in
iter2 immutable_base stripped_bases exp_bases
end;
let t_base = T.(fold_left glb (Obj (Object, [])) stripped_bases) in
T.(glb t_base (Obj (Object, sort T.compare_field fts)))

and check_exp_strong env t exp =
check_exp {env with weak = false} t exp

Expand Down Expand Up @@ -2564,7 +2578,15 @@ and validate_parenthetical env typ_opt = function
end
| _ -> ()
end;
let attrs = infer_exp env par in
(*let [@warning "-8"] ObjE (bases, fields) = par.it in*)
let [@warning "-8"] par_infer env { it = ObjE (bases, fields); _ } =
let checked = T.[ { lab = "cycles"; typ = nat; src = empty_src}
; { lab = "timeout"; typ = nat32; src = empty_src}
] in
infer_check_bases_fields env checked par.at bases fields in
let attrs = infer_exp_wrapper par_infer T.as_immut env par in
(*let attrs = infer_check_bases_fields env checked par.at bases fields in*)
(*let attrs = infer_exp env par in*)
let [@warning "-8"] T.Object, attrs_flds = T.as_obj attrs in
if attrs_flds = [] then warn env par.at "M0203" "redundant empty parenthetical note";
let unrecognised = List.(filter (fun {T.lab; _} -> lab <> "cycles" && lab <> "timeout") attrs_flds |> map (fun {T.lab; _} -> lab)) in
Expand Down
4 changes: 2 additions & 2 deletions test/run-drun/par.mo
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ actor A {
assert 3 == (await (with cycles = 101) closA());
assert 3 == (await (with cycles = 102) closB());

await (with yeah = 8; timeout = 55 : Nat32/* FIXME: checking mode */; cycles = 1000)
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!" });
Expand All @@ -76,7 +76,7 @@ actor A {
};

public func test5() : async () {
await (with timeout = 3 : Nat32/* FIXME: checking mode */) async {
await (with timeout = 3) async {
debugPrint "test5()";
assert 0 : Nat64 != replyDeadline();
}
Expand Down

0 comments on commit ec31258

Please sign in to comment.