Add -j flag to use 'join' rather than 'combine' (#14)

This is required for mailboxer. By default we can't have things like

(x, x)

in pairs since the components need to be disjoint. This flag allows us
to switch to using the 'join' combination wherever we previously needed
disjoint environments.

Author: SimonJF

bin/main.ml

@@ -23,12 +23,13 @@ let print_ir (prog, _prety, ir, _ty, _env, _constrs) =
         "=== Intermediate Representation: ===\n%a\n\n"
         (Ir.pp_program) ir
 
-let process filename is_verbose is_debug is_ir mode benchmark_count disable_ql () =
+let process filename is_verbose is_debug is_ir mode benchmark_count disable_ql use_join () =
     Settings.(set verbose is_verbose);
     Settings.(set debug is_debug);
     Settings.(set receive_typing_strategy mode);
     Settings.(set benchmark benchmark_count);
     Settings.(set disable_quasilinearity disable_ql);
+    Settings.(set join_not_combine use_join);
     try
         Frontend.Parse.parse_file filename ()
         |> Frontend.Pipeline.pipeline
@@ -51,6 +52,7 @@ let () =
     $ Arg.(value & opt int (-1) & info ["b"; "benchmark"]
       ~docv:"BENCHMARK" ~doc:"number of repetitions for benchmark; -1 (default) for no benchmarking")
     $ Arg.(value & flag & info ["q"; "disable-quasilinearity"] ~doc:"disable quasilinearity checking")
+    $ Arg.(value & flag & info ["j"; "join-not-combine"] ~doc:"use sequential join for value subterms, rather than requiring disjointness")
     $ const ()) in
   let info = Cmd.info "mbcheck" ~doc:"Typechecker for mailbox calculus" in
   Cmd.v info mbcheck_t

lib/common/settings.ml

@@ -13,6 +13,7 @@ let debug = ref false
 let benchmark = ref (-1)
 let receive_typing_strategy = ref ReceiveTypingStrategy.Interface
 let disable_quasilinearity = ref false
+let join_not_combine = ref false
 
 let set : 'a setting -> 'a -> unit = fun setting value ->
     setting := value

lib/common/settings.mli

@@ -11,6 +11,7 @@ val debug : bool setting
 val benchmark : int setting
 val receive_typing_strategy : ReceiveTypingStrategy.t setting
 val disable_quasilinearity : bool setting
+val join_not_combine : bool setting
 
 val set : 'a setting -> 'a -> unit
 val get : 'a setting -> 'a

lib/typecheck/ty_env.ml

@@ -25,47 +25,6 @@ let union = VarMap.union
 let from_list xs = List.to_seq xs |> VarMap.of_seq
 
 
-(* Combines two environments. The environments should only intersect
-   on unrestricted types. *)
-let combine : Interface_env.t -> t -> t -> t * Constraint_set.t =
-    fun ienv env1 env2 ->
-        (* Types must be *the same* and *unrestricted* *)
-        (* Subtype in both directions *)
-        let join_types var (ty1: Type.t) (ty2: Type.t) =
-            (* The subtyping and constraints are enough to rule out
-               re-use of mailboxes, but it's worth special-casing to
-               get a better error message. *)
-            if Type.contains_mailbox_type ty1 && Type.contains_mailbox_type ty2
-            then
-                Gripers.combine_mailbox_type var
-            else
-                Constraint_set.union_many
-                    [
-                        make_unrestricted ty1;
-                        make_unrestricted ty2;
-                        subtype ienv ty1 ty2;
-                        subtype ienv ty2 ty1
-                    ]
-        in
-        (* Find the overlapping keys, zip up, and join. *)
-        (* Since the subtyping in both directions will ensure equality of types,
-           and that the relevant constraints are generated, it is safe to just
-           use either type in the combined environment. *)
-        let overlap_constrs =
-            bindings env1
-            |> List.filter_map (fun (k, ty1) ->
-                    match lookup_opt k env2 with
-                        | None -> None
-                        | Some ty2 -> Some (join_types k ty1 ty2)
-
-            )
-            |> Constraint_set.union_many
-        in
-        let combined_env =
-            union (fun _ ty1 _ -> Some ty1) env1 env2
-        in
-        (combined_env, overlap_constrs)
-
 (* Joins two sequential or concurrent environments (i.e., where *both*
    actions will happen). *)
 let join : Interface_env.t -> t -> t -> t * Constraint_set.t =
@@ -155,6 +114,53 @@ let join : Interface_env.t -> t -> t -> t * Constraint_set.t =
             ) ([], Constraint_set.empty) isect1 in
         from_list (joined @ disjoint1 @ disjoint2), constrs
 
+(* Combines two environments. The environments should only intersect
+   on unrestricted types. *)
+let combine : Interface_env.t -> t -> t -> t * Constraint_set.t =
+    fun ienv env1 env2 ->
+        let combine_really ienv env1 env2 =
+            (* Types must be *the same* and *unrestricted* *)
+            (* Subtype in both directions *)
+            let join_types var (ty1: Type.t) (ty2: Type.t) =
+                (* The subtyping and constraints are enough to rule out
+                   re-use of mailboxes, but it's worth special-casing to
+                   get a better error message. *)
+                if Type.contains_mailbox_type ty1 && Type.contains_mailbox_type ty2
+                then
+                    Gripers.combine_mailbox_type var
+                else
+                    Constraint_set.union_many
+                        [
+                            make_unrestricted ty1;
+                            make_unrestricted ty2;
+                            subtype ienv ty1 ty2;
+                            subtype ienv ty2 ty1
+                        ]
+            in
+            (* Find the overlapping keys, zip up, and join. *)
+            (* Since the subtyping in both directions will ensure equality of types,
+               and that the relevant constraints are generated, it is safe to just
+               use either type in the combined environment. *)
+            let overlap_constrs =
+                bindings env1
+                |> List.filter_map (fun (k, ty1) ->
+                        match lookup_opt k env2 with
+                            | None -> None
+                            | Some ty2 -> Some (join_types k ty1 ty2)
+
+                )
+                |> Constraint_set.union_many
+            in
+            let combined_env =
+                union (fun _ ty1 _ -> Some ty1) env1 env2
+            in
+            (combined_env, overlap_constrs)
+        in
+        let fn =
+            if Settings.(get join_not_combine) then join else combine_really
+        in
+        fn ienv env1 env2
+
 (* Merges environments resulting from branching control flow. *)
 (* Core idea is that linear types must be used in precisely the same way in
     each branch. Unrestricted types must be used at the same type, but need