Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Make field_kind and commutable abstract types #10541

Merged
merged 4 commits into from
Oct 20, 2021
Merged

Make field_kind and commutable abstract types #10541

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
0240079
make field_kind and commutable abstract types
t6s Jul 26, 2021
07eddeb
use internal GADTs to ensure that Cunknown and FKprivate do not leak
garrigue Oct 18, 2021
0567833
comments
garrigue Oct 18, 2021
ec872d1
add reviewer
garrigue Oct 19, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
4 changes: 4 additions & 0 deletions Changes
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -199,6 +199,10 @@ Working version
(Jacques Garrigue and Takafumi Saikawa,
review by Leo White and Florian Angeletti)

- #10541: Make field_kind and commutable abstract, enforcing correct access
(Jacques Garrigue and Takafumi Saikawa,
review by Thomas Refis and Florian Angeletti)

- #10433: Remove the distinction between 32-bit aligned and 64-bit aligned
64-bit floats in Cmm.memory_chunk.
(Greta Yorsh, review by Xavier Leroy)
Expand Down
Binary file modified boot/ocamlc
View file
Open in desktop
Binary file not shown.
Binary file modified boot/ocamllex
View file
Open in desktop
Binary file not shown.
2 changes: 1 addition & 1 deletion toplevel/topdirs.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -247,7 +247,7 @@ let match_generic_printer_type desc path args printer_type =
let ty_expected =
List.fold_right
(fun ty_arg ty -> Ctype.newty (Tarrow (Asttypes.Nolabel, ty_arg, ty,
Cunknown)))
commu_var ())))
ty_args (Ctype.newconstr printer_type [ty_target]) in
begin try
Ctype.unify !toplevel_env
Expand Down
18 changes: 4 additions & 14 deletions typing/btype.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -129,10 +129,6 @@ let dummy_method = "*dummy method*"

(**** Representative of a type ****)

let rec commu_repr = function
Clink r when !r <> Cunknown -> commu_repr !r
| c -> c

let merge_fixed_explanation fixed1 fixed2 =
match fixed1, fixed2 with
| Some Univar _ as x, _ | _, (Some Univar _ as x) -> x
Expand Down Expand Up @@ -439,14 +435,7 @@ let copy_row f fixed row keep more =
let fixed = if fixed then orig_fixed else None in
create_row ~fields ~more ~fixed ~closed ~name

let rec copy_kind = function
Fvar{contents = Some k} -> copy_kind k
| Fvar _ -> Fvar (ref None)
| Fpresent -> Fpresent
| Fabsent -> assert false

let copy_commu c =
if commu_repr c = Cok then Cok else Clink (ref Cunknown)
let copy_commu c = if is_commu_ok c then commu_ok else commu_var ()

let rec copy_type_desc ?(keep_names=false) f = function
Tvar _ as ty -> if keep_names then ty else Tvar None
Expand All @@ -457,8 +446,9 @@ let rec copy_type_desc ?(keep_names=false) f = function
-> Tobject (f ty, ref (Some(p, List.map f tl)))
| Tobject (ty, _) -> Tobject (f ty, ref None)
| Tvariant _ -> assert false (* too ambiguous *)
| Tfield (p, k, ty1, ty2) -> (* the kind is kept shared *)
Tfield (p, field_kind_repr k, f ty1, f ty2)
| Tfield (p, k, ty1, ty2) ->
Tfield (p, field_kind_internal_repr k, f ty1, f ty2)
(* the kind is kept shared, with indirections removed for performance *)
| Tnil -> Tnil
| Tlink ty -> copy_type_desc f (get_desc ty)
| Tsubst _ -> assert false
Expand Down
4 changes: 0 additions & 4 deletions typing/btype.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,9 +78,6 @@ val is_Tunivar: type_expr -> bool
val is_Tconstr: type_expr -> bool
val dummy_method: label

val commu_repr: commutable -> commutable
(* Return the canonical representative of a commutation lock *)

(**** polymorphic variants ****)

val is_fixed: row_desc -> bool
Expand Down Expand Up @@ -164,7 +161,6 @@ val copy_type_desc:
val copy_row:
(type_expr -> type_expr) ->
bool -> row_desc -> bool -> type_expr -> row_desc
val copy_kind: field_kind -> field_kind

module For_copy : sig

Expand Down
91 changes: 43 additions & 48 deletions typing/ctype.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1354,8 +1354,9 @@ let rec copy_sep ~cleanup_scope ~fixed ~free ~bound ~may_share
copy_sep ~cleanup_scope ~fixed ~free ~bound ~may_share:true
visited t1 in
Tpoly (body, tl')
| Tfield (p, k, ty1, ty2) -> (* the kind is kept shared *)
Tfield (p, field_kind_repr k, copy_rec ~may_share:true ty1,
| Tfield (p, k, ty1, ty2) ->
(* the kind is kept shared, see Btype.copy_type_desc *)
Tfield (p, field_kind_internal_repr k, copy_rec ~may_share:true ty1,
copy_rec ~may_share:false ty2)
| _ -> copy_type_desc (copy_rec ~may_share:true) desc
in
Expand Down Expand Up @@ -2278,7 +2279,7 @@ and mcomp_fields type_pairs env ty1 ty2 =
let (fields1, rest1) = flatten_fields ty1 in
let (pairs, miss1, miss2) = associate_fields fields1 fields2 in
let has_present =
List.exists (fun (_, k, _) -> field_kind_repr k = Fpresent) in
List.exists (fun (_, k, _) -> field_kind_repr k = Fpublic) in
mcomp type_pairs env rest1 rest2;
if has_present miss1 && get_desc (object_row ty2) = Tnil
|| has_present miss2 && get_desc (object_row ty1) = Tnil
Expand All @@ -2293,9 +2294,9 @@ and mcomp_kind k1 k2 =
let k1 = field_kind_repr k1 in
let k2 = field_kind_repr k2 in
match k1, k2 with
(Fpresent, Fabsent)
| (Fabsent, Fpresent) -> raise Incompatible
| _ -> ()
(Fpublic, Fabsent)
| (Fabsent, Fpublic) -> raise Incompatible
| _ -> ()

and mcomp_row type_pairs env row1 row2 =
let r1, r2, pairs = merge_row_fields (row_fields row1) (row_fields row2) in
Expand Down Expand Up @@ -2704,10 +2705,11 @@ and unify3 env t1 t1' t2 t2' =
(!Clflags.classic || !umode = Pattern) &&
not (is_optional l1 || is_optional l2) ->
unify env t1 t2; unify env u1 u2;
begin match commu_repr c1, commu_repr c2 with
Clink r, c2 -> set_commu r c2
| c1, Clink r -> set_commu r c1
| _ -> ()
begin match is_commu_ok c1, is_commu_ok c2 with
| false, true -> set_commu_ok c1
| true, false -> set_commu_ok c2
| false, false -> link_commu ~inside:c1 c2
| true, true -> ()
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Comparing with the row_field and kind_field case (and a more statically type version of the code Octachron@4624b71), I think it might help readability to expose a commu_view type:

type commu_view =
| Commu_ok
| Commu_var

Then by pattern matching on the view, it will be clearer than checking that c1 or c2 are not commu_ok is a precondition for link_commu.

end
| (Ttuple tl1, Ttuple tl2) ->
unify_list env tl1 tl2
Expand Down Expand Up @@ -2797,8 +2799,8 @@ and unify3 env t1 t1' t2 t2' =
end
| (Tfield(f,kind,_,rem), Tnil) | (Tnil, Tfield(f,kind,_,rem)) ->
begin match field_kind_repr kind with
Fvar r when f <> dummy_method ->
set_kind r Fabsent;
Fprivate when f <> dummy_method ->
link_kind ~inside:kind field_absent;
if d2 = Tnil then unify env rem t2'
else unify env (newgenty Tnil) rem
| _ ->
Expand Down Expand Up @@ -2902,14 +2904,11 @@ and unify_fields env ty1 ty2 = (* Optimization *)
raise exn

and unify_kind k1 k2 =
let k1 = field_kind_repr k1 in
let k2 = field_kind_repr k2 in
if k1 == k2 then () else
match k1, k2 with
(Fvar r, (Fvar _ | Fpresent)) -> set_kind r k2
| (Fpresent, Fvar r) -> set_kind r k1
| (Fpresent, Fpresent) -> ()
| _ -> assert false
match field_kind_repr k1, field_kind_repr k2 with
(Fprivate, (Fprivate | Fpublic)) -> link_kind ~inside:k1 k2
| (Fpublic, Fprivate) -> link_kind ~inside:k2 k1
| (Fpublic, Fpublic) -> ()
| _ -> assert false

and unify_row env row1 row2 =
let Row {fields = row1_fields; more = rm1;
Expand Down Expand Up @@ -3195,7 +3194,7 @@ exception Filter_arrow_failed of filter_arrow_failure
let filter_arrow env t l =
let function_type level =
let t1 = newvar2 level and t2 = newvar2 level in
let t' = newty2 ~level (Tarrow (l, t1, t2, Cok)) in
let t' = newty2 ~level (Tarrow (l, t1, t2, commu_ok)) in
t', t1, t2
in
let t =
Expand Down Expand Up @@ -3233,7 +3232,7 @@ exception Filter_method_failed of filter_method_failure
let rec filter_method_field env name ty =
let method_type ~level =
let ty1 = newvar2 level and ty2 = newvar2 level in
let ty' = newty2 ~level (Tfield (name, Fpresent, ty1, ty2)) in
let ty' = newty2 ~level (Tfield (name, field_public, ty1, ty2)) in
ty', ty1
in
let ty =
Expand All @@ -3254,9 +3253,8 @@ let rec filter_method_field env name ty =
link_type ty ty';
ty1
| Tfield(n, kind, ty1, ty2) ->
let kind = field_kind_repr kind in
if (n = name) && (kind <> Fabsent) then begin
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Self note: get_desc skips Fabsent Tfield, thus the test was tautological.

unify_kind kind Fpresent;
if n = name then begin
unify_kind kind field_public;
ty1
end else
filter_method_field env name ty2
Expand Down Expand Up @@ -3306,17 +3304,16 @@ let rec filter_method_row env name priv ty =
let row = newvar2 level in
let kind =
match priv with
| Private -> Fvar (ref None)
| Public -> Fpresent
| Private -> field_private ()
| Public -> field_public
in
let ty' = newty2 ~level (Tfield (name, kind, field, row)) in
link_type ty ty';
field, row
| Tfield(n, kind, ty1, ty2) ->
let kind = field_kind_repr kind in
if (n = name) && (kind <> Fabsent) then begin
if n = name then begin
if priv = Public then
unify_kind kind Fpresent;
unify_kind kind field_public;
ty1, ty2
end else begin
let level = get_level ty in
Expand Down Expand Up @@ -3490,7 +3487,7 @@ let update_class_signature env sign =
let meths, implicitly_public =
match priv, field_kind_repr k with
| Public, _ -> meths, implicitly_public
| Private, Fpresent ->
| Private, Fpublic ->
let meths = Meths.add lab (Public, virt, ty') meths in
let implicitly_public = lab :: implicitly_public in
meths, implicitly_public
Expand All @@ -3500,11 +3497,11 @@ let update_class_signature env sign =
| exception Not_found ->
let meths, implicitly_declared =
match field_kind_repr k with
| Fpresent ->
| Fpublic ->
let meths = Meths.add lab (Public, Virtual, ty) meths in
let implicitly_declared = lab :: implicitly_declared in
meths, implicitly_declared
| Fvar _ ->
| Fprivate ->
let meths = Meths.add lab (Private, Virtual, ty) meths in
let implicitly_declared = lab :: implicitly_declared in
meths, implicitly_declared
Expand All @@ -3524,8 +3521,8 @@ let hide_private_methods env sign =
List.iter
(fun (_, k, _) ->
match field_kind_repr k with
| Fvar r -> set_kind r Fabsent
| _ -> ())
| Fprivate -> link_kind ~inside:k field_absent
| _ -> ())
fields

let close_class_signature env sign =
Expand Down Expand Up @@ -3679,14 +3676,11 @@ and moregen_fields inst_nongen type_pairs env ty1 ty2 =
pairs

and moregen_kind k1 k2 =
let k1 = field_kind_repr k1 in
let k2 = field_kind_repr k2 in
if k1 == k2 then () else
match k1, k2 with
(Fvar r, (Fvar _ | Fpresent)) -> set_kind r k2
| (Fpresent, Fpresent) -> ()
| (Fpresent, Fvar _) -> raise Public_method_to_private_method
| (Fabsent, _) | (_, Fabsent) -> assert false
match field_kind_repr k1, field_kind_repr k2 with
(Fprivate, (Fprivate | Fpublic)) -> link_kind ~inside:k1 k2
| (Fpublic, Fpublic) -> ()
| (Fpublic, Fprivate) -> raise Public_method_to_private_method
| (Fabsent, _) | (_, Fabsent) -> assert false

and moregen_row inst_nongen type_pairs env row1 row2 =
let Row {fields = row1_fields; more = rm1; closed = row1_closed} =
Expand Down Expand Up @@ -4041,8 +4035,8 @@ and eqtype_kind k1 k2 =
let k1 = field_kind_repr k1 in
let k2 = field_kind_repr k2 in
match k1, k2 with
| (Fvar _, Fvar _)
| (Fpresent, Fpresent) -> ()
| (Fprivate, Fprivate)
| (Fpublic, Fpublic) -> ()
| _ -> raise_unexplained_for Unify
(* It's probably not possible to hit this case with
real OCaml code *)
Expand Down Expand Up @@ -4497,7 +4491,8 @@ let rec build_subtype env (visited : transient_expr list)
let (t1', c1) = build_subtype env visited loops (not posi) level t1 in
let (t2', c2) = build_subtype env visited loops posi level t2 in
let c = max_change c1 c2 in
if c > Unchanged then (newty (Tarrow(l, t1', t2', Cok)), c)
if c > Unchanged
then (newty (Tarrow(l, t1', t2', commu_ok)), c)
else (t, Unchanged)
| Ttuple tlist ->
let tt = Transient_expr.repr t in
Expand Down Expand Up @@ -4626,7 +4621,7 @@ let rec build_subtype env (visited : transient_expr list)
let (t1', c1) = build_subtype env visited loops posi level t1 in
let (t2', c2) = build_subtype env visited loops posi level t2 in
let c = max_change c1 c2 in
if c > Unchanged then (newty (Tfield(s, Fpresent, t1', t2')), c)
if c > Unchanged then (newty (Tfield(s, field_public, t1', t2')), c)
else (t, Unchanged)
| Tnil ->
if posi then
Expand Down Expand Up @@ -4983,7 +4978,7 @@ let rec nongen_schema_rec env ty =
raise Nongen
end
| Tfield(_, kind, t1, t2) ->
if field_kind_repr kind = Fpresent then
if field_kind_repr kind = Fpublic then
nongen_schema_rec env t1;
nongen_schema_rec env t2
| Tvariant row ->
Expand Down
35 changes: 9 additions & 26 deletions typing/printtyp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -461,28 +461,11 @@ let raw_list pr ppf = function
let kind_vars = ref []
let kind_count = ref 0

let rec safe_kind_repr v = function
Fvar {contents=Some k} ->
if List.memq k v then "Fvar loop" else
safe_kind_repr (k::v) k
| Fvar r ->
let vid =
try List.assq r !kind_vars
with Not_found ->
let c = incr kind_count; !kind_count in
kind_vars := (r,c) :: !kind_vars;
c
in
Printf.sprintf "Fvar {None}@%d" vid
| Fpresent -> "Fpresent"
let string_of_field_kind v =
match field_kind_repr v with
| Fpublic -> "Fpublic"
| Fabsent -> "Fabsent"

let rec safe_commu_repr v = function
Cok -> "Cok"
| Cunknown -> "Cunknown"
| Clink r ->
if List.memq r v then "Clink loop" else
safe_commu_repr (r::v) !r
| Fprivate -> "Fprivate"

let rec safe_repr v t =
match Transient_expr.coerce t with
Expand Down Expand Up @@ -518,7 +501,7 @@ and raw_type_desc ppf = function
| Tarrow(l,t1,t2,c) ->
fprintf ppf "@[<hov1>Tarrow(\"%s\",@,%a,@,%a,@,%s)@]"
(string_of_label l) raw_type t1 raw_type t2
(safe_commu_repr [] c)
(if is_commu_ok c then "Cok" else "Cunknown")
| Ttuple tl ->
fprintf ppf "@[<1>Ttuple@,%a@]" raw_type_list tl
| Tconstr (p, tl, abbrev) ->
Expand All @@ -533,7 +516,7 @@ and raw_type_desc ppf = function
fprintf ppf "(Some(@,%a,@,%a))" path p raw_type_list tl)
| Tfield (f, k, t1, t2) ->
fprintf ppf "@[<hov1>Tfield(@,%s,@,%s,@,%a,@;<0 -1>%a)@]" f
(safe_kind_repr [] k)
(string_of_field_kind k)
raw_type t1 raw_type t2
| Tnil -> fprintf ppf "Tnil"
| Tlink t -> fprintf ppf "@[<1>Tlink@,%a@]" raw_type t
Expand Down Expand Up @@ -822,14 +805,14 @@ let printer_iter_type_expr f ty =
let fields, _ = flatten_fields fi in
List.iter
(fun (_, kind, ty) ->
if field_kind_repr kind = Fpresent then
if field_kind_repr kind = Fpublic then
f ty)
fields
| Some (_, l) ->
List.iter f (List.tl l)
end
| Tfield(_, kind, ty1, ty2) ->
if field_kind_repr kind = Fpresent then
if field_kind_repr kind = Fpublic then
f ty1;
f ty2
| _ ->
Expand Down Expand Up @@ -1219,7 +1202,7 @@ and tree_of_typobject mode fi nm =
List.fold_right
(fun (n, k, t) l ->
match field_kind_repr k with
| Fpresent -> (n, t) :: l
| Fpublic -> (n, t) :: l
| _ -> l)
fields [] in
let sorted_fields =
Expand Down