hphp/hack/src/typing/typing_intersection.ml

   1 (*
   2  * Copyright (c) 2015, Facebook, Inc.
   3  * All rights reserved.
   4  *
   5  * This source code is licensed under the MIT license found in the
   6  * LICENSE file in the "hack" directory of this source tree.
   7  *
   8  *)
   9
  10 open Hh_prelude
  11 open Common
  12 open Typing_defs
  13 module Env = Typing_env
  14 module MkType = Typing_make_type
  15 module Reason = Typing_reason
  16 module TySet = Typing_set
  17 module Utils = Typing_utils
  18
  19 exception Nothing
  20
  21 (** Computes the negation of a type when it is known, which is currently the case
  22 for null, nonnull, mixed, nothing, primitives, and classes.
  23 Otherwise approximate up or down according to
  24 `approx` parameter: If approx is `ApproxUp`, return mixed, else if it is `ApproxDown`,
  25 return nothing. *)
  26 let negate_type env r ty ~approx =
  27   let (env, ty) = Env.expand_type env ty in
  28   let neg_ty =
  29     match get_node ty with
  30     | Tprim Aast.Tnull -> MkType.nonnull r
  31     | Tprim tp -> MkType.neg r (Neg_prim tp)
  32     | Tneg (Neg_prim tp) -> MkType.prim_type r tp
  33     | Tneg (Neg_class (_, c)) when Typing_utils.class_has_no_params env c ->
  34       MkType.class_type r c []
  35     | Tnonnull -> MkType.null r
  36     | Tclass (c, Nonexact _, _) -> MkType.neg r (Neg_class c)
  37     | _ ->
  38       if Utils.equal_approx approx Utils.ApproxUp then
  39         MkType.mixed r
  40       else
  41         MkType.nothing r
  42   in
  43   (env, neg_ty)
  44
  45 (** Decompose nullable types into unions with null
  46
  47       decompose_nullable ?A = null | A
  48       decompose_nullable ?(A | ?B) = null | A | B
  49
  50     The implementation has the side-effect of flattening unions if the type is
  51     nullable, e.g.,
  52
  53       decompose_optional ?(A | (B | C)) = null | A | B | C
  54   *)
  55 let decompose_nullable ty =
  56   let rec has_option (ty : 'a ty) : bool =
  57     match deref ty with
  58     | (_, Toption _) -> true
  59     | (_, Tunion tyl) -> List.exists ~f:has_option tyl
  60     | _ -> false
  61   in
  62   let rec peel (ty_acc : 'a ty list) (ty : 'a ty) : 'a ty list =
  63     match deref ty with
  64     | (_, Toption ty) -> peel ty_acc ty
  65     | (_, Tunion tyl) -> List.fold ~init:ty_acc ~f:peel tyl
  66     | _ -> ty :: ty_acc
  67   in
  68   if has_option ty then
  69     let r = get_reason ty in
  70     let null_ty = MkType.null r in
  71     let tyl = peel [null_ty] ty in
  72     let tyl = TySet.elements (TySet.of_list tyl) in
  73     MkType.union r tyl
  74   else
  75     ty
  76
  77 (** Build a union from a list of types. Flatten if any of the types themselves are union.
  78     Also, pull nullable out to a top-level Toption. Undoes decompose atomic.
  79 *)
  80 let recompose_atomic env r tyl =
  81   let rec traverse nullable dynamic tyl_acc tyl =
  82     match tyl with
  83     | [] -> (nullable, dynamic, List.rev tyl_acc)
  84     | ty :: tyl ->
  85       if Utils.is_nothing env ty then
  86         traverse nullable dynamic tyl_acc tyl
  87       else (
  88         match deref ty with
  89         | (r, Toption ty) -> traverse (Some r) dynamic (ty :: tyl_acc) tyl
  90         | (r, Tprim Aast.Tnull) -> traverse (Some r) dynamic tyl_acc tyl
  91         | (r, Tdynamic) -> traverse nullable (Some r) tyl_acc tyl
  92         | (_, Tunion tyl') -> traverse nullable dynamic tyl_acc (tyl' @ tyl)
  93         | _ -> traverse nullable dynamic (ty :: tyl_acc) tyl
  94       )
  95   in
  96   let (nullable_r, dynamic_r, tyl) = traverse None None [] tyl in
  97   Utils.make_union env r tyl nullable_r dynamic_r
  98
  99 (* Destructure an intersection into a list of its sub-types,
 100    decending into sub-intersections.
 101 *)
 102 let destruct_inter_list env tyl =
 103   let orr r_opt r = Some (Option.value r_opt ~default:r) in
 104   let rec dest_inter env ty tyl tyl_res r_inter =
 105     let (env, ty) = Env.expand_type env ty in
 106     match deref ty with
 107     | (r, Tintersection tyl') ->
 108       destruct_inter_list env (tyl' @ tyl) tyl_res (orr r_inter r)
 109     | _ -> destruct_inter_list env tyl (ty :: tyl_res) r_inter
 110   and destruct_inter_list env tyl tyl_res r_union =
 111     match tyl with
 112     | [] -> (env, (tyl_res, r_union))
 113     | ty :: tyl -> dest_inter env ty tyl tyl_res r_union
 114   in
 115   destruct_inter_list env tyl [] None
 116
 117 (** Number of '&' symbols in an intersection representation. E.g. for (A & B),
 118 returns 1, for A, returns 0. *)
 119 let number_of_inter_symbols env ty =
 120   let rec n_inter env tyl n =
 121     match tyl with
 122     | [] -> (env, n)
 123     | ty :: tyl ->
 124       let (env, ty) = Env.expand_type env ty in
 125       begin
 126         match get_node ty with
 127         | Tintersection tyl' ->
 128           n_inter env (tyl' @ tyl) (List.length tyl' - 1 + n)
 129         | Tunion tyl' -> n_inter env (tyl' @ tyl) n
 130         | Toption ty -> n_inter env (ty :: tyl) n
 131         | _ -> n_inter env tyl n
 132       end
 133   in
 134   n_inter env [ty] 0
 135
 136 let collapses env ty1 ty2 ~inter_ty =
 137   let (env, n_inter_inter) = number_of_inter_symbols env inter_ty in
 138   let (env, n_inter1) = number_of_inter_symbols env ty1 in
 139   let (env, n_inter2) = number_of_inter_symbols env ty2 in
 140   (env, n_inter_inter <= n_inter1 + n_inter2)
 141
 142 let make_intersection env r tyl =
 143   let ty = MkType.intersection r tyl in
 144   let (env, ty) = Typing_utils.wrap_union_inter_ty_in_var env r ty in
 145   (env, ty)
 146
 147 (** Computes the intersection (greatest lower bound) of two types.
 148 For the intersection of unions, attempt to simplify by using the distributivity
 149 of intersection over union. Uses the the `collapses` test function to make sure
 150 the resulting type is no greater in size than the trivial `Tintersection [ty1; ty2]`. *)
 151 let rec intersect env ~r ty1 ty2 =
 152   if ty_equal ty1 ty2 then
 153     (env, ty1)
 154   else
 155     let (env, ty1) = Env.expand_type env ty1 in
 156     let (env, ty2) = Env.expand_type env ty2 in
 157     if Utils.is_sub_type_for_union env ty1 ty2 then
 158       (env, ty1)
 159     else if Utils.is_sub_type_for_union env ty2 ty1 then
 160       (env, ty2)
 161     else if Utils.is_type_disjoint env ty1 ty2 then (
 162       let inter_ty = MkType.nothing r in
 163       Typing_log.log_intersection ~level:2 env r ty1 ty2 ~inter_ty;
 164       (env, inter_ty)
 165     ) else
 166       let ty1 = decompose_nullable ty1 in
 167       let ty2 = decompose_nullable ty2 in
 168       let (env, inter_ty) =
 169         try
 170           match (deref ty1, deref ty2) with
 171           | ((_, Ttuple tyl1), (_, Ttuple tyl2))
 172             when Int.equal (List.length tyl1) (List.length tyl2) ->
 173             let (env, inter_tyl) =
 174               List.map2_env env tyl1 tyl2 ~f:(intersect ~r)
 175             in
 176             (env, mk (r, Ttuple inter_tyl))
 177           | ((_, Tshape (shape_kind1, fdm1)), (_, Tshape (shape_kind2, fdm2)))
 178             ->
 179             let (env, shape_kind, fdm) =
 180               intersect_shapes env r (shape_kind1, fdm1) (shape_kind2, fdm2)
 181             in
 182             (env, mk (r, Tshape (shape_kind, fdm)))
 183           | ((_, Tintersection tyl1), (_, Tintersection tyl2)) ->
 184             intersect_lists env r tyl1 tyl2
 185           (* Simplify `supportdyn<t> & u` to `supportdyn<t & u>`. Do not apply if `u` is
 186            * a type variable, else we end up with recursion in constraints. *)
 187           | ((r, Tnewtype (name1, [ty1arg], _)), _)
 188             when String.equal name1 Naming_special_names.Classes.cSupportDyn
 189                  && not (is_tyvar ty2) ->
 190             let (env, ty) = intersect ~r env ty1arg ty2 in
 191             let (env, res) = Typing_utils.simple_make_supportdyn r env ty in
 192             (env, res)
 193           | (_, (r, Tnewtype (name1, [ty2arg], _)))
 194             when String.equal name1 Naming_special_names.Classes.cSupportDyn
 195                  && not (is_tyvar ty1) ->
 196             let (env, ty) = intersect ~r env ty1 ty2arg in
 197             let (env, res) = Typing_utils.simple_make_supportdyn r env ty in
 198             (env, res)
 199           | ((_, Tintersection tyl), _) -> intersect_lists env r [ty2] tyl
 200           | (_, (_, Tintersection tyl)) -> intersect_lists env r [ty1] tyl
 201           | ((r1, Tunion tyl1), (r2, Tunion tyl2)) ->
 202             let (common_tyl, tyl1', tyl2') =
 203               Typing_algebra.factorize_common_types tyl1 tyl2
 204             in
 205             let (env, not_common_tyl) =
 206               intersect_unions env r (r1, tyl1') (r2, tyl2')
 207             in
 208             recompose_atomic env r (common_tyl @ not_common_tyl)
 209           | ((r_union, Tunion tyl), ty)
 210           | (ty, (r_union, Tunion tyl)) ->
 211             let (env, inter_tyl) =
 212               intersect_ty_union env r (mk ty) (r_union, tyl)
 213             in
 214             recompose_atomic env r inter_tyl
 215           | ((_, Tprim Aast.Tnum), (_, Tprim Aast.Tarraykey))
 216           | ((_, Tprim Aast.Tarraykey), (_, Tprim Aast.Tnum)) ->
 217             (env, MkType.int r)
 218           | ( (_, Tneg (Neg_prim (Aast.Tint | Aast.Tarraykey))),
 219               (_, Tprim Aast.Tnum) )
 220           | ( (_, Tprim Aast.Tnum),
 221               (_, Tneg (Neg_prim (Aast.Tint | Aast.Tarraykey))) ) ->
 222             (env, MkType.float r)
 223           | ((_, Tneg (Neg_prim Aast.Tfloat)), (_, Tprim Aast.Tnum))
 224           | ((_, Tprim Aast.Tnum), (_, Tneg (Neg_prim Aast.Tfloat))) ->
 225             (env, MkType.int r)
 226           | ((_, Tneg (Neg_prim Aast.Tstring)), ty_ak)
 227           | (ty_ak, (_, Tneg (Neg_prim Aast.Tstring))) ->
 228             if
 229               (* Ocaml warns about ambiguous or-pattern variables under guard if this is in a when clause*)
 230               Typing_utils.is_sub_type_for_union
 231                 env
 232                 (mk ty_ak)
 233                 (MkType.arraykey Typing_reason.Rnone)
 234             then
 235               intersect env ~r (mk ty_ak) (MkType.int r)
 236             else
 237               make_intersection env r [ty1; ty2]
 238           | ((_, Tneg (Neg_prim (Aast.Tint | Aast.Tnum))), ty_ak)
 239           | (ty_ak, (_, Tneg (Neg_prim (Aast.Tint | Aast.Tnum)))) ->
 240             if
 241               Typing_utils.is_sub_type_for_union
 242                 env
 243                 (mk ty_ak)
 244                 (MkType.arraykey Typing_reason.Rnone)
 245             then
 246               intersect env ~r (mk ty_ak) (MkType.string r)
 247             else
 248               make_intersection env r [ty1; ty2]
 249           | _ -> make_intersection env r [ty1; ty2]
 250         with
 251         | Nothing -> (env, MkType.nothing r)
 252       in
 253       Typing_log.log_intersection ~level:2 env r ty1 ty2 ~inter_ty;
 254       (env, inter_ty)
 255
 256 and intersect_shapes env r (shape_kind1, fdm1) (shape_kind2, fdm2) =
 257   let (env, fdm) =
 258     TShapeMap.merge_env env fdm1 fdm2 ~combine:(fun env _sfn sft1 sft2 ->
 259         match ((shape_kind1, sft1), (shape_kind2, sft2)) with
 260         | ((_, None), (_, None))
 261         | ((_, Some { sft_optional = true; _ }), (Closed_shape, None))
 262         | ((Closed_shape, None), (_, Some { sft_optional = true; _ })) ->
 263           (env, None)
 264         | ((_, Some { sft_optional = false; _ }), (Closed_shape, None))
 265         | ((Closed_shape, None), (_, Some { sft_optional = false; _ })) ->
 266           raise Nothing
 267         | ((_, Some sft), (Open_shape, None))
 268         | ((Open_shape, None), (_, Some sft)) ->
 269           (env, Some sft)
 270         | ( (_, Some { sft_optional = opt1; sft_ty = ty1 }),
 271             (_, Some { sft_optional = opt2; sft_ty = ty2 }) ) ->
 272           let opt = opt1 && opt2 in
 273           let (env, ty) = intersect env ~r ty1 ty2 in
 274           (env, Some { sft_optional = opt; sft_ty = ty }))
 275   in
 276   let shape_kind =
 277     match (shape_kind1, shape_kind2) with
 278     | (Open_shape, Open_shape) -> Open_shape
 279     | _ -> Closed_shape
 280   in
 281   (env, shape_kind, fdm)
 282
 283 and intersect_lists env r tyl1 tyl2 =
 284   let rec intersect_lists env tyl1 tyl2 acc_tyl =
 285     match (tyl1, tyl2) with
 286     | ([], _) -> (env, tyl2 @ acc_tyl)
 287     | (_, []) -> (env, tyl1 @ acc_tyl)
 288     | (ty1 :: tyl1', _) ->
 289       let (env, (inter_ty, missed_inter_tyl2)) =
 290         intersect_ty_tyl env r ty1 tyl2
 291       in
 292       intersect_lists env tyl1' missed_inter_tyl2 (inter_ty :: acc_tyl)
 293   in
 294   let (env, tyl) = intersect_lists env tyl1 tyl2 [] in
 295   make_intersection env r tyl
 296
 297 and intersect_ty_tyl env r ty tyl =
 298   let rec intersect_ty_tyl env ty tyl missed_inter_tyl =
 299     match tyl with
 300     | [] -> (env, (ty, missed_inter_tyl))
 301     | ty' :: tyl' ->
 302       let (env, ty_opt) = try_intersect env r ty ty' in
 303       begin
 304         match ty_opt with
 305         | None -> intersect_ty_tyl env ty tyl' (ty' :: missed_inter_tyl)
 306         | Some inter_ty -> intersect_ty_tyl env inter_ty tyl' missed_inter_tyl
 307       end
 308   in
 309   intersect_ty_tyl env ty tyl []
 310
 311 and try_intersect env r ty1 ty2 =
 312   let (env, ty) = intersect env ~r ty1 ty2 in
 313   let (env, ty) = Env.expand_type env ty in
 314   match get_node ty with
 315   | Tintersection _ -> (env, None)
 316   | _ -> (env, Some ty)
 317
 318 and intersect_unions env r (r1, tyl1) (r2, tyl2) =
 319   (* The order matters. (A | B | C) & (A | B) gets simplified to (A | B)
 320      while (A | B) & (A | B | C) would become A | B | ((A | B) & C), so we
 321      put the longest union first as a heuristic. *)
 322   let ((r1, tyl1), (r2, tyl2)) =
 323     if List.length tyl1 >= List.length tyl2 then
 324       ((r1, tyl1), (r2, tyl2))
 325     else
 326       ((r2, tyl2), (r1, tyl1))
 327   in
 328   let union_ty1 = MkType.union r1 tyl1 in
 329   intersect_ty_union env r union_ty1 (r2, tyl2)
 330
 331 (** For (A1 | .. | An) & B, compute each of the A1 & B, .. , An & B.
 332 Keep those which collapse (see `collapses` function) with B
 333 and leave the others unchanged.
 334 So if I is the set of indices i such that Ai collapses with B,
 335 and J the set of indices such that this is not the case,
 336 the result would be
 337   (|_{i in I} (Ai & B)) | (B & (|_{j in J} Aj))
 338 *)
 339 and intersect_ty_union env r (ty1 : locl_ty) (r_union, tyl2) =
 340   let (env, inter_tyl) =
 341     List.map_env env tyl2 ~f:(fun env ty2 -> intersect env ~r ty1 ty2)
 342   in
 343   let zipped = List.zip_exn tyl2 inter_tyl in
 344   let (collapsed, not_collapsed) =
 345     List.partition_tf zipped ~f:(fun (ty2, inter_ty) ->
 346         snd @@ collapses env ty1 ty2 ~inter_ty)
 347   in
 348   let collapsed = List.map collapsed ~f:snd in
 349   let not_collapsed =
 350     match not_collapsed with
 351     | [] -> []
 352     | [(_ty2, inter_ty)] -> [inter_ty]
 353     | _ ->
 354       let not_collapsed = List.map not_collapsed ~f:fst in
 355       [MkType.intersection r [ty1; MkType.union r_union not_collapsed]]
 356   in
 357   (env, not_collapsed @ collapsed)
 358
 359 let intersect_list env r tyl =
 360   (* We need to match tyl here because we'd mess the reason if tyl was just
 361      [mixed] *)
 362   match tyl with
 363   | [] -> (env, MkType.mixed r)
 364   | ty :: tyl -> List.fold_left_env env tyl ~init:ty ~f:(intersect ~r)
 365
 366 let normalize_intersection env ?on_tyvar tyl =
 367   let orr r_opt r = Some (Option.value r_opt ~default:r) in
 368   let rec normalize_intersection env r tyl tys_acc =
 369     match tyl with
 370     | [] -> (env, r, tys_acc)
 371     | ty :: tyl ->
 372       let (env, ty) = Env.expand_type env ty in
 373       let proceed env ty =
 374         normalize_intersection env r tyl (TySet.add ty tys_acc)
 375       in
 376       begin
 377         match (deref ty, on_tyvar) with
 378         | ((r', Tvar v), Some on_tyvar) ->
 379           let (env, ty') = on_tyvar env r' v in
 380           if ty_equal ty ty' then
 381             proceed env ty
 382           else
 383             normalize_intersection env r (ty' :: tyl) tys_acc
 384         | ((r', Tintersection tyl'), _) ->
 385           normalize_intersection env (orr r r') (tyl' @ tyl) tys_acc
 386         | ((_, Tunion _), _) ->
 387           let (env, ty) = Utils.simplify_unions env ty ?on_tyvar in
 388           let (env, ety) = Env.expand_type env ty in
 389           begin
 390             match get_node ety with
 391             | Tunion _ -> proceed env ty
 392             | _ -> normalize_intersection env r (ty :: tyl) tys_acc
 393           end
 394         | _ -> proceed env ty
 395       end
 396   in
 397   normalize_intersection env None tyl TySet.empty
 398
 399 let simplify_intersections env ?on_tyvar ty =
 400   let r = get_reason ty in
 401   let (env, r', tys) = normalize_intersection env [ty] ?on_tyvar in
 402   let r = Option.value r' ~default:r in
 403   intersect_list env r (TySet.elements tys)
 404
 405 let intersect env ~r ty1 ty2 =
 406   let (env, inter_ty) = intersect env ~r ty1 ty2 in
 407   Typing_log.log_intersection ~level:1 env r ty1 ty2 ~inter_ty;
 408   (env, inter_ty)
 409
 410 let rec intersect_i env r ty1 lty2 =
 411   let ty2 = LoclType lty2 in
 412   if Utils.is_sub_type_for_union_i env ty1 ty2 then
 413     (env, ty1)
 414   else if Utils.is_sub_type_for_union_i env ty2 ty1 then
 415     (env, ty2)
 416   else
 417     let (env, ty) =
 418       match ty1 with
 419       | LoclType lty1 ->
 420         let (env, ty) = intersect env ~r lty1 lty2 in
 421         (env, LoclType ty)
 422       | ConstraintType cty1 ->
 423         (match deref_constraint_type cty1 with
 424         | (r, TCintersection (lty1, cty1)) ->
 425           let (env, lty) = intersect env ~r lty1 lty2 in
 426           ( env,
 427             ConstraintType (mk_constraint_type (r, TCintersection (lty, cty1)))
 428           )
 429         | (r, TCunion (lty1, cty1)) ->
 430           (* Distribute intersection over union.
 431              At the moment local types in TCunion can only be
 432              unions or intersections involving only null and nonnull,
 433              so applying distributivity allows for simplifying the types. *)
 434           let (env, lty) = intersect env ~r lty1 lty2 in
 435           let (env, ty) = intersect_i env r (ConstraintType cty1) lty2 in
 436           (match ty with
 437           | LoclType ty ->
 438             let (env, ty) = Utils.union env lty ty in
 439             (env, LoclType ty)
 440           | ConstraintType cty ->
 441             (env, ConstraintType (mk_constraint_type (r, TCunion (lty, cty)))))
 442         | (_, Thas_member _)
 443         | (_, Thas_type_member _)
 444         | (_, Tcan_index _)
 445         | (_, Tcan_traverse _)
 446         | (_, Tdestructure _) ->
 447           ( env,
 448             ConstraintType (mk_constraint_type (r, TCintersection (lty2, cty1)))
 449           ))
 450     in
 451     match ty with
 452     | LoclType _ -> (env, ty)
 453     | ConstraintType ty -> Utils.simplify_constraint_type env ty
 454
 455 let () = Utils.negate_type_ref := negate_type
 456
 457 let () = Utils.simplify_intersections_ref := simplify_intersections
 458
 459 let () = Utils.intersect_list_ref := intersect_list