Move Alloc_mode and Value_mode to Btype

lambda/translcore.ml

@@ -85,12 +85,12 @@ let extract_float = function
   | _ -> fatal_error "Translcore.extract_float"
 
 let transl_alloc_mode alloc_mode : Lambda.alloc_mode =
-  match Types.Alloc_mode.constrain_lower alloc_mode with
+  match Btype.Alloc_mode.constrain_lower alloc_mode with
   | Global -> Alloc_heap
   | Local -> Alloc_local
 
 let transl_value_mode mode =
-  let alloc_mode = Types.Value_mode.regional_to_global_alloc mode in
+  let alloc_mode = Btype.Value_mode.regional_to_global_alloc mode in
   transl_alloc_mode alloc_mode
 
 let transl_apply_position position =
@@ -343,7 +343,7 @@ and transl_exp0 ~in_new_scope ~scopes e =
         let funct =
           { funct with
             exp_desc = Texp_apply(funct, argl, Nontail);
-            exp_mode = Value_mode.of_alloc rmode }
+            exp_mode = Btype.Value_mode.of_alloc rmode }
         in
         event_after ~scopes e
           (transl_apply ~scopes ~tailcall ~inlined ~specialised
@@ -450,8 +450,8 @@ and transl_exp0 ~in_new_scope ~scopes e =
       end
   | Texp_setfield(arg, _, lbl, newval) ->
       let mode =
-        let arg_mode = Types.Value_mode.regional_to_local_alloc arg.exp_mode in
-        match Types.Alloc_mode.constrain_lower arg_mode with
+        let arg_mode = Btype.Value_mode.regional_to_local_alloc arg.exp_mode in
+        match Btype.Alloc_mode.constrain_lower arg_mode with
         | Global -> Assignment
         | Local -> Local_assignment
       in

toplevel/topdirs.ml

@@ -22,6 +22,7 @@ open Types
 open Cmo_format
 open Trace
 open Toploop
+module Alloc_mode = Btype.Alloc_mode
 
 (* The standard output formatter *)
 let std_out = std_formatter

typing/btype.ml

@@ -820,3 +820,355 @@ let undo_compress (changes, _old) =
             ty.desc <- desc; r := !next
         | _ -> ())
         log
+
+
+module Alloc_mode = struct
+  type nonrec const = Types.alloc_mode_const = Global | Local
+  type t = Types.alloc_mode =
+    | Amode of const
+    | Amodevar of alloc_mode_var
+
+  let global = Amode Global
+  let local = Amode Local
+  let of_const = function
+    | Global -> global
+    | Local -> local
+
+  let min_mode = global
+
+  let max_mode = local
+
+  let le_const a b =
+    match a, b with
+    | Global, _ | _, Local -> true
+    | Local, Global -> false
+
+  let join_const a b =
+    match a, b with
+    | Local, _ | _, Local -> Local
+    | Global, Global -> Global
+
+  let meet_const a b =
+    match a, b with
+    | Global, _ | _, Global -> Global
+    | Local, Local -> Local
+
+  exception NotSubmode
+(*
+  let pp_c ppf = function
+    | Global -> Printf.fprintf ppf "0"
+    | Local -> Printf.fprintf ppf "1"
+  let pp_v ppf v =
+    let i = v.mvid in
+    (if i < 26 then Printf.fprintf ppf "%c" (Char.chr (Char.code 'a' + i))
+    else Printf.fprintf ppf "v%d" i);
+    Printf.fprintf ppf "[%a%a]" pp_c v.lower pp_c v.upper
+*)
+  let submode_cv m v =
+    (* Printf.printf "  %a <= %a\n" pp_c m pp_v v; *)
+    if le_const m v.lower then ()
+    else if not (le_const m v.upper) then raise NotSubmode
+    else begin
+      let m = join_const v.lower m in
+      v.lower <- m;
+      if m = v.upper then v.vlower <- []
+    end
+
+  let rec submode_vc v m =
+    (* Printf.printf "  %a <= %a\n" pp_v v pp_c m; *)
+    if le_const v.upper m then ()
+    else if not (le_const v.lower m) then raise NotSubmode
+    else begin
+      let m = meet_const v.upper m in
+      v.upper <- m;
+      v.vlower |> List.iter (fun a ->
+        (* a <= v <= m *)
+        submode_vc a m;
+        v.lower <- join_const v.lower a.lower;
+      );
+      if v.lower = m then v.vlower <- []
+    end
+
+  let submode_vv a b =
+    (* Printf.printf "  %a <= %a\n" pp_v a pp_v b; *)
+    if le_const a.upper b.lower then ()
+    else if List.memq a b.vlower then ()
+    else begin
+      submode_vc a b.upper;
+      b.vlower <- a :: b.vlower;
+      submode_cv a.lower b;
+    end
+
+  let submode a b =
+    match
+      match a, b with
+      | Amode a, Amode b ->
+         if not (le_const a b) then raise NotSubmode
+      | Amodevar v, Amode c ->
+         (* Printf.printf "%a <= %a\n" pp_v v pp_c c; *)
+         submode_vc v c
+      | Amode c, Amodevar v ->
+         (* Printf.printf "%a <= %a\n" pp_c c pp_v v; *)
+         submode_cv c v
+      | Amodevar a, Amodevar b ->
+         (* Printf.printf "%a <= %a\n" pp_v a pp_v b; *)
+         submode_vv a b
+    with
+    | () -> Ok ()
+    | exception NotSubmode -> Error ()
+
+  let submode_exn t1 t2 =
+    match submode t1 t2 with
+    | Ok () -> ()
+    | Error () -> invalid_arg "submode_exn"
+
+  let equate a b =
+    match submode a b, submode b a with
+    | Ok (), Ok () -> Ok ()
+    | Error (), _ | _, Error () -> Error ()
+
+  let next_id = ref (-1)
+  let fresh () =
+    incr next_id;
+    { upper = Local; lower = Global; vlower = []; mvid = !next_id }
+
+  let rec all_equal v = function
+    | [] -> true
+    | v' :: rest ->
+        if v == v' then all_equal v rest
+        else false
+
+  let joinvars vars =
+    match vars with
+    | [] -> global
+    | v :: rest ->
+      let v =
+        if all_equal v rest then v
+        else begin
+          let v = fresh () in
+          List.iter (fun v' -> submode_vv v' v) vars;
+          v
+        end
+      in
+      Amodevar v
+
+  let join ms =
+    let rec aux vars = function
+      | [] -> joinvars vars
+      | Amode Global :: ms -> aux vars ms
+      | Amode Local :: _ -> local
+      | Amodevar v :: ms -> aux (v :: vars) ms
+    in aux [] ms
+
+  let constrain_upper = function
+    | Amode m -> m
+    | Amodevar v ->
+       submode_cv v.upper v;
+       v.upper
+
+  let compress_vlower v =
+    (* Ensure that each transitive lower bound of v
+       is a direct lower bound of v *)
+    let rec trans v' =
+      if le_const v'.upper v.lower then ()
+      else if List.memq v' v.vlower then ()
+      else begin
+        v.vlower <- v' :: v.vlower;
+        trans_low v'
+      end
+    and trans_low v' =
+      submode_cv v'.lower v;
+      List.iter trans v'.vlower
+    in
+    List.iter trans_low v.vlower
+
+  let constrain_lower = function
+    | Amode m -> m
+    | Amodevar v ->
+        compress_vlower v;
+        submode_vc v v.lower;
+        v.lower
+
+  let newvar () = Amodevar (fresh ())
+
+  let check_const = function
+    | Amode m -> Some m
+    | Amodevar v when v.lower = v.upper ->
+       Some v.lower
+    | Amodevar _ -> None
+
+  let print_const ppf = function
+    | Global -> Format.fprintf ppf "Global"
+    | Local -> Format.fprintf ppf "Local"
+
+  let print_var_id ppf v =
+    Format.fprintf ppf "?%i" v.mvid
+
+  let print_var ppf v =
+    compress_vlower v;
+    if v.lower = v.upper then begin
+      print_const ppf v.lower
+    end else if v.vlower = [] then begin
+      print_var_id ppf v
+    end else begin
+      Format.fprintf ppf "%a[> %a]"
+        print_var_id v
+        (Format.pp_print_list print_var_id) v.vlower
+    end
+
+  let print ppf = function
+    | Amode m -> print_const ppf m
+    | Amodevar v -> print_var ppf v
+
+end
+
+module Value_mode = struct
+
+  type const =
+   | Global
+   | Regional
+   | Local
+
+  let r_as_l : const -> Alloc_mode.const = function
+    | Global -> Global
+    | Regional -> Local
+    | Local -> Local
+  [@@warning "-unused-value-declaration"]
+
+  let r_as_g : const -> Alloc_mode.const = function
+    | Global -> Global
+    | Regional -> Global
+    | Local -> Local
+  [@@warning "-unused-value-declaration"]
+
+  let of_alloc_consts
+        ~(r_as_l : Alloc_mode.const)
+        ~(r_as_g : Alloc_mode.const) =
+    match r_as_l, r_as_g with
+    | Global, Global -> Global
+    | Global, Local -> assert false
+    | Local, Global -> Regional
+    | Local, Local -> Local
+
+  type t = Types.value_mode =
+    { r_as_l : Alloc_mode.t;
+      (* [r_as_l] is the image of the mode under the [r_as_l] function *)
+      r_as_g : Alloc_mode.t;
+      (* [r_as_g] is the image of the mode under the [r_as_g] function.
+         Always less than [r_as_l]. *) }
+
+  let global =
+    let r_as_l = Alloc_mode.global in
+    let r_as_g = Alloc_mode.global in
+    { r_as_l; r_as_g }
+
+  let regional =
+    let r_as_l = Alloc_mode.local in
+    let r_as_g = Alloc_mode.global in
+    { r_as_l; r_as_g }
+
+  let local =
+    let r_as_l = Alloc_mode.local in
+    let r_as_g = Alloc_mode.local in
+    { r_as_l; r_as_g }
+
+  let of_const = function
+    | Global -> global
+    | Regional -> regional
+    | Local -> local
+
+  let max_mode =
+    let r_as_l = Alloc_mode.max_mode in
+    let r_as_g = Alloc_mode.max_mode in
+    { r_as_l; r_as_g }
+
+  let min_mode =
+    let r_as_l = Alloc_mode.min_mode in
+    let r_as_g = Alloc_mode.min_mode in
+    { r_as_l; r_as_g }
+
+  let of_alloc mode =
+    let r_as_l = mode in
+    let r_as_g = mode in
+    { r_as_l; r_as_g }
+
+  let local_to_regional t = { t with r_as_g = Alloc_mode.global }
+
+  let regional_to_global t = { t with r_as_l = t.r_as_g }
+
+  let regional_to_local t = { t with r_as_g = t.r_as_l }
+
+  let global_to_regional t = { t with r_as_l = Alloc_mode.local }
+
+  let regional_to_global_alloc t = t.r_as_g
+
+  let regional_to_local_alloc t = t.r_as_l
+
+  type error = [`Regionality | `Locality]
+
+  let submode t1 t2 =
+    match Alloc_mode.submode t1.r_as_l t2.r_as_l with
+    | Error () -> Error `Regionality
+    | Ok () as ok -> begin
+        match Alloc_mode.submode t1.r_as_g t2.r_as_g with
+        | Ok () -> ok
+        | Error () -> Error `Locality
+      end
+
+  let submode_exn t1 t2 =
+    match submode t1 t2 with
+    | Ok () -> ()
+    | Error _ -> invalid_arg "submode_exn"
+
+  let rec submode_meet t = function
+    | [] -> Ok ()
+    | t' :: rest ->
+      match submode t t' with
+      | Ok () -> submode_meet t rest
+      | Error _ as err -> err
+
+  let join ts =
+    let r_as_l = Alloc_mode.join (List.map (fun t -> t.r_as_l) ts) in
+    let r_as_g = Alloc_mode.join (List.map (fun t -> t.r_as_g) ts) in
+    { r_as_l; r_as_g }
+
+  let constrain_upper t =
+    let r_as_l = Alloc_mode.constrain_upper t.r_as_l in
+    let r_as_g = Alloc_mode.constrain_upper t.r_as_g in
+    of_alloc_consts ~r_as_l ~r_as_g
+
+  let constrain_lower t =
+    let r_as_l = Alloc_mode.constrain_lower t.r_as_l in
+    let r_as_g = Alloc_mode.constrain_lower t.r_as_g in
+    of_alloc_consts ~r_as_l ~r_as_g
+
+  let newvar () =
+    let r_as_l = Alloc_mode.newvar () in
+    let r_as_g = Alloc_mode.newvar () in
+    Alloc_mode.submode_exn r_as_g r_as_l;
+    { r_as_l; r_as_g }
+
+  let check_const t =
+    match Alloc_mode.check_const t.r_as_l with
+    | None -> None
+    | Some r_as_l ->
+      match Alloc_mode.check_const t.r_as_g with
+      | None -> None
+      | Some r_as_g ->
+        Some (of_alloc_consts ~r_as_l ~r_as_g)
+
+  let print_const ppf = function
+    | Global -> Format.fprintf ppf "Global"
+    | Regional -> Format.fprintf ppf "Regional"
+    | Local -> Format.fprintf ppf "Local"
+
+  let print ppf t =
+    match check_const t with
+    | Some const -> print_const ppf const
+    | None ->
+        Format.fprintf ppf
+          "@[<2>r_as_l: %a@ r_as_g: %a@]"
+          Alloc_mode.print t.r_as_l
+          Alloc_mode.print t.r_as_g
+
+end