IsUnionOf (support is ?T)

Summary: This diff adds a new kind of predicate `IsUnionOf` that represents a predicate that passes if any of its sub-predicates pass. It is used to produce a predicate for nullable types.

Reviewed By: enetsee

Differential Revision: D89830544

fbshipit-source-id: 1ef21cd1f8e6358f26f83fede08403cfb95cabfc

Author: viratyosin

hphp/hack/src/oxidized/gen/typing_defs_core.rs

@@ -3,7 +3,7 @@
 // This source code is licensed under the MIT license found in the
 // LICENSE file in the "hack" directory of this source tree.
 //
-// @generated SignedSource<<2c3f5c94b0ef6f31c3ed188a23f5f994>>
+// @generated SignedSource<<f2cf7bdffd426d5ab4b758ae2a8c1210>>
 //
 // To regenerate this file, run:
 //   buck run @fbcode//mode/dev-nosan-lg fbcode//hphp/hack/src:oxidized_regen
@@ -662,6 +662,7 @@ pub enum TypePredicate_ {
     IsTag(TypeTag),
     IsTupleOf(TuplePredicate),
     IsShapeOf(ShapePredicate),
+    IsUnionOf(Vec<TypePredicate>),
 }
 
 #[derive(

hphp/hack/src/typing/type_visitor.ml

@@ -364,7 +364,8 @@ class virtual ['a] locl_type_visitor : ['a] locl_type_visitor_type =
       match snd neg_ty with
       | IsTag tag -> on_tag acc tag
       | IsTupleOf _
-      | IsShapeOf _ ->
+      | IsShapeOf _
+      | IsUnionOf _ ->
         acc
 
     method on_tunapplied_alias acc _ _ = acc

hphp/hack/src/typing/typing_case_types.ml

@@ -458,6 +458,10 @@ module DataType : sig
           right: TagWithReason.t;
         }
 
+    val empty : t
+
+    val union : t -> t -> t
+
     val disjoint : TagWithReason.ctx -> t -> t -> disjoint
 
     val are_disjoint : TagWithReason.ctx -> t -> t -> bool
@@ -817,7 +821,7 @@ end = struct
         (env, to_datatypes ~safe_for_are_disjoint ~trail env cls args)
   end
 
-  let fromPredicate
+  let rec fromPredicate
       ~safe_for_are_disjoint ~trail (env : env) (predicate : type_predicate) :
       env * t =
     let open Tag in
@@ -842,6 +846,12 @@ end = struct
     | IsTag tag -> from_tag tag
     | IsTupleOf _ -> (env, Set.singleton ~reason VecData)
     | IsShapeOf _ -> (env, Set.singleton ~reason DictData)
+    | IsUnionOf predicates ->
+      let (env, sets) =
+        List.fold_map predicates ~init:env ~f:(fun env pred ->
+            fromPredicate ~safe_for_are_disjoint ~trail env pred)
+      in
+      (env, List.fold sets ~init:Set.empty ~f:Set.union)
 
   type context = {
     safe_for_are_disjoint: bool;
@@ -1240,8 +1250,12 @@ module AtomicDataTypes = struct
       DataType.Class.to_datatypes ~safe_for_are_disjoint ~trail env name
       @@ Tag.generics_for_class_and_tag_generic_l env name args
 
+  let empty = DataType.Set.empty
+
   let complement dt = DataType.Set.diff mixed dt
 
+  let union dt1 dt2 = DataType.Set.union dt1 dt2
+
   let are_disjoint env dt1 dt2 = DataType.Set.are_disjoint env dt1 dt2
 end
 

hphp/hack/src/typing/typing_case_types.mli

@@ -118,9 +118,15 @@ module AtomicDataTypes : sig
   val of_tag :
     safe_for_are_disjoint:bool -> env -> Typing_defs_core.type_tag -> env * t
 
+  (** The empty set of data types *)
+  val empty : t
+
   (** Computes the complement for the set of values contained in [t] *)
   val complement : t -> t
 
+  (** Computes the union of the two given sets **)
+  val union : t -> t -> t
+
   (** Returns true if the given data types are known to have no values in
       common, otherwise returns false *)
   val are_disjoint : env -> t -> t -> bool

hphp/hack/src/typing/typing_defs_core.ml

@@ -265,6 +265,7 @@ and type_predicate_ =
   | IsTag of type_tag
   | IsTupleOf of tuple_predicate
   | IsShapeOf of shape_predicate
+  | IsUnionOf of type_predicate list
 
 and type_predicate =
   (Reason.t[@hash.ignore] [@transform.opaque]) * type_predicate_
@@ -702,6 +703,10 @@ module Pp = struct
       Format.fprintf fmt "(@[<2>IsShapeOf@ ";
       pp_shape_predicate fmt shape_predicate;
       Format.fprintf fmt "@])"
+    | IsUnionOf predicates ->
+      Format.fprintf fmt "(@[<2>IsUnionOf@ ";
+      pp_list pp_type_predicate fmt predicates;
+      Format.fprintf fmt "@])"
 
   and pp_tuple_predicate fmt { tp_required } =
     Format.fprintf fmt "@[<2>{ ";
@@ -827,6 +832,7 @@ let type_predicate__con_ordinal type_predicate_ =
   | IsTag _ -> 0
   | IsTupleOf _ -> 1
   | IsShapeOf _ -> 2
+  | IsUnionOf _ -> 3
 
 let type_tag_con_ordinal type_tag =
   match type_tag with

hphp/hack/src/typing/typing_defs_core.mli

@@ -255,6 +255,7 @@ and type_predicate_ =
   | IsTag of type_tag
   | IsTupleOf of tuple_predicate
   | IsShapeOf of shape_predicate
+  | IsUnionOf of type_predicate list
 
 and type_predicate = (Reason.t[@transform.opaque]) * type_predicate_
 

hphp/hack/src/typing/typing_json.ml

@@ -232,6 +232,11 @@ let rec from_type : env -> show_like_ty:bool -> locl_ty -> json =
                         ])
                    (TShapeMap.bindings sp_fields)) );
           ]
+      | IsUnionOf predicates ->
+        let predicates_json =
+          List.map predicates ~f:(fun p -> obj @@ predicate_json p)
+        in
+        name "isunion" @ [("args", JSON_Array predicates_json)]
       (* TODO: T196048813 optional, open, fuel? *)
     in
     obj @@ kind p "negation" @ predicate_json predicate

hphp/hack/src/typing/typing_print.ml

@@ -1321,6 +1321,13 @@ module Full = struct
             ([text "shape("]
             @ List.intersperse texts ~sep:(text ", ")
             @ [text ")"]) )
+      | IsUnionOf predicates ->
+        let (fuel, texts) =
+          List.fold_map ~init:fuel predicates ~f:predicate_doc
+        in
+        ( fuel,
+          Concat (List.intersperse texts ~sep:(Concat [Space; text "|"; Space]))
+        )
       (* TODO: T196048813 optional, open, fuel? *)
     in
     let (fuel, pdoc) = predicate_doc fuel predicate in
@@ -1786,6 +1793,9 @@ module ErrorString = struct
                   ])
           in
           "shape(" ^ String.concat texts ~sep:", " ^ ")"
+        | IsUnionOf predicates ->
+          let strings = List.map predicates ~f:(fun (_, pred) -> str pred) in
+          String.concat ~sep:" | " strings
         (* TODO: T196048813, dedupe?, optional, open, fuel? *)
       in
       (fuel, "anything but " ^ str @@ snd predicate)

hphp/hack/src/typing/typing_refinement.ml

@@ -132,10 +132,29 @@ module TyPredicate = struct
     | Tnonnull -> Result.Error "nonnull"
     | Tdynamic -> Result.Error "dynamic"
     | Tany _ -> Result.Error "any"
-    | Toption _ -> Result.Error "option"
+    | Toption ty_opt -> begin
+      let open Hh_prelude.Result.Let_syntax in
+      let* (next_wildcard_id, pred_opt) = of_ty env next_wildcard_id ty_opt in
+      let pred_null = (get_reason ty, IsTag NullTag) in
+      return (next_wildcard_id, IsUnionOf [pred_opt; pred_null])
+      |> Result.map_error ~f:(fun err -> "option-" ^ err)
+    end
     | Tfun _ -> Result.Error "fun"
     | Tgeneric _ -> Result.Error "generic"
-    | Tunion _ -> Result.Error "union"
+    | Tunion tys -> begin
+      match
+        List.fold_result tys ~init:(next_wildcard_id, []) ~f:(fun acc ty ->
+            let (next_wildcard_id, predicates) = acc in
+            let open Hh_prelude.Result.Let_syntax in
+            let* (next_wildcard_id, predicate) =
+              of_ty env next_wildcard_id ty
+            in
+            return (next_wildcard_id, predicate :: predicates))
+      with
+      | Result.Error err -> Result.Error ("union-" ^ err)
+      | Result.Ok (next_wildcard_id, predicates) ->
+        Result.Ok (next_wildcard_id, IsUnionOf (List.rev predicates))
+    end
     | Tintersection _ -> Result.Error "intersection"
     | Tvec_or_dict _ -> Result.Error "vec_or_dict"
     | Taccess _ -> Result.Error "access"
@@ -270,6 +289,15 @@ module TyPredicate = struct
           IMap.empty
       in
       (env, new_tparams)
+    | (_reason, IsUnionOf predicates) ->
+      let (env, new_tparams) =
+        List.map_env env predicates ~f:(fun env predicate ->
+            let (env, new_tparams) =
+              instantiate_wildcards_for_predicate env predicate p
+            in
+            (env, new_tparams))
+      in
+      (env, List.fold new_tparams ~init:IMap.empty ~f:IMap.union)
 
   let rec to_ty lookup_wildcard predicate =
     let tag_to_ty reason tag =
@@ -312,6 +340,23 @@ module TyPredicate = struct
           sp_fields
       in
       Typing_make_type.shape reason (Typing_make_type.nothing reason) map
+    | (reason, IsUnionOf predicates) -> begin
+      match
+        List.partition_tf predicates ~f:(fun p ->
+            match p with
+            | (_, IsTag NullTag) -> true
+            | _ -> false)
+      with
+      | (_ :: _, [other]) ->
+        Typing_make_type.nullable reason (to_ty lookup_wildcard other)
+      | (_ :: _, others) ->
+        Typing_make_type.nullable reason
+        @@ Typing_make_type.union reason
+        @@ List.map others ~f:(to_ty lookup_wildcard)
+      | ([], _) ->
+        Typing_make_type.union reason
+        @@ List.map predicates ~f:(to_ty lookup_wildcard)
+    end
 
   exception FoundWildcard
 
@@ -564,6 +609,11 @@ module TyPartition = struct
   let meet (partition1, t1, f1) (partition2, t2, f2) =
     (Partition.meet partition1 partition2, UTL.conj t1 t2, UTL.conj f1 f2)
 
+  let union_combine (partition1, t1, f1) (partition2, t2, f2) =
+    ( Partition.union_combine partition1 partition2,
+      UTL.disj t1 t2,
+      UTL.conj f1 f2 )
+
   let product ~f sub_splits_and_assumptions =
     let sub_splits = List.map sub_splits_and_assumptions ~f:fst3 in
     let assumption_pairs =
@@ -770,6 +820,36 @@ and split_ty_by_tag
   else
     (env, TyPartition.mk_span ~env ~predicate ty)
 
+and split_ty_by_union
+    ~(other_intersected_tys : locl_ty list)
+    ~(expansions : SSet.t)
+    (env : env)
+    (ty : locl_ty)
+    (predicates : type_predicate list) : env * TyPartition.t =
+  (* Split the type by each predicate in the union.
+
+     When splitting T by union predicate (P1 | P2 | ... | Pn):
+     - Left: parts that pass at least one predicate = L1 ∪ L2 ∪ ... ∪ Ln
+     - Right: parts that fail all predicates = R1 ∩ R2 ∩ ... ∩ Rn
+     - Span: parts that may or may not pass = everything else
+
+     This is NOT the same as joining the partitions (which would give L1∪L2, S1∪S2, R1∪R2).
+  *)
+  let (env, partitions) =
+    List.fold_map
+      ~init:env
+      ~f:(fun env pred ->
+        split_ty ~other_intersected_tys ~expansions env ty ~predicate:pred)
+      predicates
+  in
+  (* Combine partitions using the correct algebra for union predicates *)
+  let partition =
+    match partitions with
+    | [] -> TyPartition.mk_bottom
+    | first :: rest -> List.fold rest ~init:first ~f:TyPartition.union_combine
+  in
+  (env, partition)
+
 and split_ty
     ~(other_intersected_tys : locl_ty list)
     ~(expansions : SSet.t)
@@ -797,6 +877,8 @@ and split_ty
         shape_predicate
         predicate
     | IsTag tag -> split_ty_by_tag ~ty_datatype env ety tag predicate
+    | IsUnionOf predicates ->
+      split_ty_by_union ~other_intersected_tys ~expansions env ety predicates
   in
   let split_union ~other_intersected_tys ~expansions env (tys : locl_ty list) =
     let (env, partitions) =
@@ -855,12 +937,21 @@ and split_ty
       partition_f
         DataType.(of_ty ~safe_for_are_disjoint:true env @@ Class (name, args))
     | Tneg (_, predicate) ->
-      let (env, dty) =
+      let rec to_dty env predicate =
         match predicate with
         | IsTag tag -> DataType.of_tag ~safe_for_are_disjoint:false env tag
         | IsTupleOf _ -> DataType.(of_ty ~safe_for_are_disjoint:false env Tuple)
         | IsShapeOf _ -> DataType.(of_ty ~safe_for_are_disjoint:false env Shape)
+        | IsUnionOf preds ->
+          List.fold_left_env
+            env
+            preds
+            ~init:DataType.empty
+            ~f:(fun env dt_acc pred ->
+              let (env, dt) = to_dty env (snd pred) in
+              (env, DataType.union dt_acc dt))
       in
+      let (env, dty) = to_dty env predicate in
       let dty = DataType.complement dty in
       partition_f (env, dty)
     | Tprim Aast.Tnoreturn -> (env, TyPartition.mk_bottom)

hphp/hack/src/utils/core/partition/partition.ml

@@ -235,6 +235,27 @@ end) : S with type atom := Atom.t = struct
           right1 &&& right2 ||| (right1 &&& span2) ||| (right2 &&& span1));
     }
 
+  (*
+    Combines two partitions using the algebra for union predicates.
+
+    When combining partitions P1 and P2 for union predicates (P1 | P2):
+    - left: passes at least one predicate = L1 | L2
+    - right: fails both predicates = R1 & R2
+    - span: uncertain (not definitely left or right) = (S1 & S2) | (S1 & R2) | (R1 & S2)
+
+    This is different from regular join which does component-wise union.
+  *)
+  let union_combine
+      { left = left1; span = span1; right = right1 }
+      { left = left2; span = span2; right = right2 } =
+    {
+      left = Lattice.Infix_ops.(left1 ||| left2);
+      span =
+        Lattice.Infix_ops.(
+          span1 &&& span2 ||| (span1 &&& right2) ||| (right1 &&& span2));
+      right = Lattice.Infix_ops.(right1 &&& right2);
+    }
+
   (* If the partition is fully within the left, span or right we can
      simplify the DNF to be [set], otherwise return [t] unchanged *)
   let simplify t atom =