Skip to content

Commit

Permalink
address comments
Browse files Browse the repository at this point in the history
  • Loading branch information
riaqn committed Jun 20, 2024
1 parent 54687fd commit c022aa2
Show file tree
Hide file tree
Showing 5 changed files with 42 additions and 40 deletions.
43 changes: 21 additions & 22 deletions ocaml/typing/env.ml
Original file line number Diff line number Diff line change
Expand Up @@ -716,6 +716,8 @@ let mda_mode = Mode.Value.legacy |> Mode.Value.disallow_right

let clda_mode = Mode.Value.legacy |> Mode.Value.disallow_right

let cm_mode = Mode.Value.legacy |> Mode.Value.disallow_right

let empty_structure =
Structure_comps {
comp_values = NameMap.empty;
Expand Down Expand Up @@ -900,16 +902,12 @@ let vda_description vda =
let vda_description = vda.vda_description in
{vda_description with val_modalities = Mode.Modality.Value.undefined}

(** The caller wants the mode of the [value_data] *)
(* CR zqian: call this [normalize_vda_mode] *)
let apply_val_modalities vda =
(* CR zqian: either inline this, or move to [types.ml] *)
let decouple_val_modalities (vd : Subst.Lazy.value_description) =
let modalities = vd.val_modalities in
let vd = {vd with val_modalities = Mode.Modality.Value.id'} in
modalities, vd
let normalize_vda_mode vda =
let vda_description = vda.vda_description in
let modalities = vda_description.val_modalities in
let vda_description =
{vda_description with val_modalities = Mode.Modality.Value.id'}
in
let modalities, vda_description = decouple_val_modalities vda.vda_description in
let vda_mode = Mode.Modality.Value.apply_left modalities vda.vda_mode in
{vda with vda_description; vda_mode}

Expand Down Expand Up @@ -1319,16 +1317,14 @@ let find_cltype path env =
(NameMap.find s sc.comp_cltypes).cltda_declaration
| Papply _ | Pextra_ty _ -> raise Not_found

(* Have two versions, one takes path, one takes identity. The first doesn't run
locks, the second does. *)
let find_value path env =
find_value_full path env |> vda_description

let find_value_without_locks id env =
match IdTbl.find_same_and_locks id env.values with
| Val_bound _, _ :: _ -> assert false
| Val_bound data, [] ->
let data = apply_val_modalities data in
let data = normalize_vda_mode data in
data.vda_description, data.vda_mode
| Val_unbound _, _ -> raise Not_found

Expand Down Expand Up @@ -1849,9 +1845,6 @@ let rec components_of_module_maker
incr pos;
Lazy_backtrack.create addr
in
(* structures are always legacy *)
(* CR zqian: rename this to [module_mode] *)
let mmode = Mode.Value.legacy |> Mode.Value.disallow_right in
List.iter (fun ((item : Subst.Lazy.signature_item), path) ->
match item with
Sig_value(id, decl, _) ->
Expand All @@ -1864,7 +1857,7 @@ let rec components_of_module_maker
let vda_shape = Shape.proj cm_shape (Shape.Item.value id) in
let vda =
{ vda_description = decl'; vda_address = addr;
vda_mode = mmode; vda_shape }
vda_mode = cm_mode; vda_shape }
in
c.comp_values <- NameMap.add (Ident.name id) vda c.comp_values;
| Sig_type(id, decl, _, _) ->
Expand Down Expand Up @@ -3445,8 +3438,13 @@ let lookup_value ~errors ~use ~loc lid env =
let path, locks, vda =
lookup_value_lazy ~errors ~use ~loc lid env
in
(* CR zqian: add comments about the ordering the applying modality and walk_locks *)
let vda = apply_val_modalities vda in
(* First, we apply the modalities to acquire the mode of the value at the
definition site. Then, we walk the locks. That means the surrounding
closure would be closing over the value instead of the module.
This is better ergonomics, but dangers as it doesn't reflect the real
runtime behaviour. With the current set-up, it is sound. *)
let vda = normalize_vda_mode vda in
let vd = Subst.Lazy.force_value_description vda.vda_description in
let vmode =
if use then
Expand Down Expand Up @@ -3799,13 +3797,14 @@ let fold_modules f lid env acc =
acc
end

(* CR zqian: also passes mode in additional vda_description *)
let fold_values f =
find_all wrap_value (fun env -> env.values) (fun sc -> sc.comp_values)
(fun k p ve acc ->
match ve with
| Val_unbound _ -> acc
| Val_bound vda -> f k p (vda |> vda_description) acc)
| Val_bound vda ->
let vda = normalize_vda_mode vda in
f k p vda.vda_description vda.vda_mode acc)
and fold_constructors f =
find_all_simple_list (fun env -> env.constrs) (fun sc -> sc.comp_constrs)
(fun cda acc -> f cda.cda_description acc)
Expand Down Expand Up @@ -3944,7 +3943,7 @@ let spellcheck_name ppf extract env name =
(fun () -> Misc.spellcheck (extract env) name)

let extract_values path env =
fold_values (fun name _ _ acc -> name :: acc) path env []
fold_values (fun name _ _ _ acc -> name :: acc) path env []
let extract_types path env =
fold_types (fun name _ _ acc -> name :: acc) path env []
let extract_modules path env =
Expand All @@ -3961,7 +3960,7 @@ let extract_cltypes path env =
fold_cltypes (fun name _ _ acc -> name :: acc) path env []
let extract_instance_variables env =
fold_values
(fun name _ descr acc ->
(fun name _ descr _ acc ->
match descr.val_kind with
| Val_ivar _ -> name :: acc
| _ -> acc) None env []
Expand Down
4 changes: 2 additions & 2 deletions ocaml/typing/env.mli
Original file line number Diff line number Diff line change
Expand Up @@ -581,8 +581,8 @@ val print_type_expr: (Format.formatter -> Types.type_expr -> unit) ref
(** Folds *)

val fold_values:
(string -> Path.t -> Subst.Lazy.value_description -> 'a -> 'a) ->
Longident.t option -> t -> 'a -> 'a
(string -> Path.t -> Subst.Lazy.value_description -> Mode.Value.l -> 'a -> 'a)
-> Longident.t option -> t -> 'a -> 'a
val fold_types:
(string -> Path.t -> type_declaration -> 'a -> 'a) ->
Longident.t option -> t -> 'a -> 'a
Expand Down
14 changes: 8 additions & 6 deletions ocaml/typing/mode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2291,7 +2291,7 @@ module Modality = struct
| Left user -> user
| Right _ -> assert false

let infer : Mode.lr -> Mode.l -> internal = fun mm m -> Diff (mm, m)
let infer ~md_mode ~mode = Diff (md_mode, mode)

let max = Join_const Const.max
end
Expand Down Expand Up @@ -2395,7 +2395,7 @@ module Modality = struct
| Undefined -> Format.fprintf ppf "undefined"
| Exactly _ -> Format.fprintf ppf "exactly"

let infer mm m = Exactly (mm, m)
let infer ~md_mode ~mode = Exactly (md_mode, mode)

let max = Meet_const Const.max

Expand Down Expand Up @@ -2475,10 +2475,12 @@ module Modality = struct
let print ppf ({ monadic; comonadic } : 'd t) =
Format.fprintf ppf "%a,%a" Monadic.print monadic Comonadic.print comonadic

let infer : Value.lr -> Value.l -> internal =
fun mmode mode ->
let comonadic = Comonadic.infer mmode.comonadic mode.comonadic in
let monadic = Monadic.infer mmode.monadic mode.monadic in
let infer : md_mode:Value.lr -> mode:Value.l -> internal =
fun ~md_mode ~mode ->
let comonadic =
Comonadic.infer ~md_mode:md_mode.comonadic ~mode:mode.comonadic
in
let monadic = Monadic.infer ~md_mode:md_mode.monadic ~mode:mode.monadic in
{ monadic; comonadic }

let zap_to_id : type d. d t -> user =
Expand Down
13 changes: 8 additions & 5 deletions ocaml/typing/mode_intf.mli
Original file line number Diff line number Diff line change
Expand Up @@ -500,18 +500,20 @@ module type S = sig

(* CR zqian: call this [compose]. *)

(** [cons m t] returns the modality that is [m] after [t]. *)
(* CR zqian: call this [compose]. *)

(** [cons m t] returns the modality that is [m] after [t]. *)
val cons : atom -> user -> user

(** [singleton m] returns the modality containing only [m]. *)
val singleton : atom -> user

(* CR zqian: return record, then we don't need [Exist.t]. *)

(* CR zqian: return record, then we don't need [Exist.t]. *)

(** Returns the list of [atom] in the given modality. The list is
commutative. *)
(* CR zqian: return record, then we don't need [Exist.t]. *)
val to_list : user -> atom list

type error =
Expand All @@ -535,8 +537,8 @@ module type S = sig
(** Printing for debugging. *)
val print : Format.formatter -> 'd t -> unit

(* CR zqian: consider spliting the [lr]. Also, label the arguments. *)
val infer : Value.lr -> Value.l -> internal
(* CR zqian: consider spliting the [lr]. *)
val infer : md_mode:Value.lr -> mode:Value.l -> internal

(** Returns a user modality weaker than the given modality. The returned
modality will be pushed to identity modality if possible. The given
Expand All @@ -552,9 +554,10 @@ module type S = sig

(* CR zqian: rename to [to_const_exn]. *)

(* CR zqian: rename to [to_const_exn]. *)

(** Returns a user modality by asserting the given modality is already
user modality and returning it. *)
(* CR zqian: rename to [to_const_exn]. *)
val zap_assert : 'd t -> user

(** The top modality; [sub x max] succeeds for any [x]. *)
Expand Down
8 changes: 3 additions & 5 deletions ocaml/typing/typemod.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2828,6 +2828,7 @@ and type_structure ?(toplevel = None) funct_body anchor env sstr =

let type_str_item
env shape_map ({pstr_loc = loc; pstr_desc = desc} as item) sig_acc =
let md_mode = Mode.Value.legacy in
match Jane_syntax.Structure_item.of_ast item with
| Some jitem -> type_str_item_jst ~loc env shape_map jitem sig_acc
| None ->
Expand Down Expand Up @@ -2886,16 +2887,13 @@ and type_structure ?(toplevel = None) funct_body anchor env sstr =
Signature_names.check_value names first_loc id;
let vd, mode = Env.find_value_without_locks id newenv in
let vd = Subst.Lazy.force_value_description vd in
(* structures are always legacy *)
(* CR zqian: rename this to [module_mode] *)
let mmode = Mode.Value.legacy in
begin match Mode.Value.Comonadic.submode
mode.Mode.comonadic
mmode.Mode.comonadic with
md_mode.Mode.comonadic with
| Ok () -> ()
| Error e -> raise (Error (first_loc, env, Submode_failed e))
end;
let modalities = Mode.Modality.Value.infer mmode mode in
let modalities = Mode.Modality.Value.infer ~md_mode ~mode in
let vd =
{ vd with
val_zero_alloc = zero_alloc;
Expand Down

0 comments on commit c022aa2

Please sign in to comment.