Changed IntExpression to take in abstract type

Summary:
+ We would like to move towards an abstract type for `IntExpression`s to make sure that all polynomials are only expressed in fully normalized form.
+ Currently, an `IntExpression` is of `'a Polynomial.t`, which is transparent. This allows for all kinds of redundant states, like the monomial list (informally) `[1, [x, 1]]`, which is better represented as a `Variable x`, and `[5, []]`, which is better represented as `Literal (Integer 5)`. This is also a gigantic pain because these errors tend to be "hidden", and the error messages you get for mistaking alternate representations are terrible.
+ We have added an abstract type `'a RecordIntExpression.t`, which is the new input to an `IntExpression`. Everywhere the `IntExpression` constructor was used, we now use `IntExpression.create`, which implicitly constructs proper values of the abstract type for use.
It is a common occurrence to pattern match on an `IntExpression _` to extract out the polynomial, and perform some polynomial-only operation on it, so in addition we have added support for the private type `'a RecordIntExpression.t`, which is now supported at all call-sites. This means that we may deconstruct an `IntExpression` to obtain a `Polynomial.t`, but we cannot construct an `IntExpression` using the constructor itself (preserving normalization).
Currently, no normalization is happening, but this change is to stage for later normalization features. In addition, we have a sum type `'a variant`, which is necessary because `IntExpression` regards the type of `RecordIntExpression.t` as abstract, so we must have `RecordIntExpression.t` implement its own normalizing constructor, with a sum to tag whether it is actually a polynomial, or some other type. This will be expanded on in future diffs.

There's some redundant stuff that will need to be taken away in a future diff. For instance, we should get rid of some useless branches and re-evaluate everything to do with `type_to_int_expression`.

- **Why `module IntExpression`?**
Firstly, we need some function of signature `'a Polynomial.t -> type_t` - this function will take a polynomial and return its normalized form (which may be `IntExpression`, `Literal`, or `Variable`). Necessarily, since `RecordIntExpression` comes *before* `type_t` and we are not using recursive modules, this must be in a different module. `IntExpression` is this module.

- **Why `'a variant`?**
`'a variant` is here because, as stated before, `IntExpression` contains the function `create : 'a Polynomial.t -> type_t`. However, the type of `RecordIntExpression` is *abstract* to the module `IntExpression`, because we want to enforce that the entirety of `type.ml` regards `RecordIntExpression.t` as abstract, so we don't have any representation invariant violations. Thus, `RecordIntExpression` must itself implement its own normalization function, with a way of signalling to `IntExpression` whether the output it produced is normalized as a polynomial, or needs to be changed to a `Literal` or something.

- **Why not just have `RecordIntExpression` have a function that turns a polynomial into a pseudo-normalized polynomial, and then have `IntExpression` pattern match on it to produce the proper value?**
In other words, why not have `RecordIntExpression.normalize : 'a Polynomial.t -> 'a Polynomial.t`, and have `create` do the work of recognizing if its a literal or not.
The problem is that `RecordIntExpression` must produce the abstract type that `IntExpression` (the constructor) takes in, since it comes before the type definition of `type_t`. Then, `IntExpression.create` has the burden of creating the value of type `RecordIntExpression.t` - which it can't, since it's an abstract type.
So `RecordIntExpression.t` *has* to give a way to produce values of type `RecordIntExpression.t`, and because those values are abstract, it must tag them with whether or not they should be normalized.
- **Why the `private` constructor for `RecordIntExpression.t`?**
It is entirely possible to implement `RecordIntExpression.polynomial_of : 'a t -> 'a Polynomial.t`. However, this induces extreme headache in the existing codebase when trying to pattern match on `IntExpression` variants of the `type_t` type.
Without a private constructor, this means that to pattern match on an empty polynomial, you must do `| IntExpression int_expression -> match int_expression of | [] -> ...`, or something similar, as opposed to `| IntExpression (Data []) -> ...`. It's just a lot of syntactic burden. This can be alleviated later by reducing the amount of points where we have to pattern match on `IntExpressions`, by changing `solve_less_or_equal` to do all of its simplification first, rather than recursively inside of the function. Right now, however, this is less bloat.

Reviewed By: grievejia

Differential Revision: D28890690

fbshipit-source-id: ef1d81aec74922d9c74f4e34b998d5e07f0fd63d

Author: Brandon Wu

source/analysis/test/typeTest.ml

@@ -1996,7 +1996,7 @@ let test_replace_all _ =
     polynomial_create_from_variables_list variable_list |> Type.polynomial_to_type
   in
   let divide_to_type numerator denominator =
-    Type.IntExpression (Type.Polynomial.divide ~compare_t:Type.compare numerator denominator)
+    Type.IntExpression.create (Type.Polynomial.divide ~compare_t:Type.compare numerator denominator)
   in
   (* TODO: Task T90507423. This needs to be normalized before output. *)
   assert_equal
@@ -2014,14 +2014,14 @@ let test_replace_all _ =
     (Type.Variable.GlobalTransforms.Unary.replace_all
        (fun _ -> Some (Type.literal_integer 7))
        (divide_to_type (Type.Polynomial.create_from_int 7) (Type.Polynomial.create_from_variable x)))
-    (Type.IntExpression (polynomial_create_from_variables_list [1, []]));
+    (Type.IntExpression.create (polynomial_create_from_variables_list [1, []]));
   assert_equal
     (Type.Variable.GlobalTransforms.Unary.replace_all
        (fun _ -> Some (Type.literal_integer 6))
        (divide_to_type
           (Type.Polynomial.create_from_int 10)
           (Type.Polynomial.create_from_variable x)))
-    (Type.IntExpression (polynomial_create_from_variables_list [1, []]));
+    (Type.IntExpression.create (polynomial_create_from_variables_list [1, []]));
   assert_equal
     (Type.Variable.GlobalTransforms.Unary.replace_all
        (function
@@ -2032,7 +2032,7 @@ let test_replace_all _ =
                   (polynomial_create_from_variables_list [1, [y, 1]]))
          | _ -> None)
        (variable_list_to_type [1, [x, 1; y, 1]]))
-    (Type.IntExpression
+    (Type.IntExpression.create
        (Type.Polynomial.multiply
           ~compare_t:Type.compare
           (Type.Polynomial.create_from_variable y)
@@ -2045,7 +2045,7 @@ let test_replace_all _ =
        (function
          | variable when not ([%equal: Type.Variable.Unary.t] variable z) -> Some (Type.Variable z)
          | _ -> None)
-       (Type.IntExpression
+       (Type.IntExpression.create
           (Type.Polynomial.add
              ~compare_t:Type.compare
              (Type.Polynomial.divide
@@ -2056,7 +2056,7 @@ let test_replace_all _ =
                 ~compare_t:Type.compare
                 (Type.Polynomial.create_from_int 7)
                 (polynomial_create_from_variables_list [1, [y, 1; z, 1]])))))
-    (Type.IntExpression
+    (Type.IntExpression.create
        (Type.Polynomial.multiply
           ~compare_t:Type.compare
           (Type.Polynomial.create_from_int 2)
@@ -2069,15 +2069,15 @@ let test_replace_all _ =
        (function
          | variable when [%equal: Type.Variable.Unary.t] variable x -> Some (Type.Variable y)
          | _ -> None)
-       (Type.IntExpression
+       (Type.IntExpression.create
           (Type.Polynomial.add
              ~compare_t:Type.compare
              (Type.Polynomial.create_from_int 1)
              (Type.Polynomial.divide
                 ~compare_t:Type.compare
                 (Type.Polynomial.create_from_variable x)
                 (Type.Polynomial.create_from_variable y)))))
-    (Type.IntExpression (polynomial_create_from_variables_list [2, []]));
+    (Type.IntExpression.create (polynomial_create_from_variables_list [2, []]));
   assert_equal
     (Type.Variable.GlobalTransforms.Unary.replace_all
        (fun _ -> Some (Type.literal_integer 0))
@@ -2088,7 +2088,7 @@ let test_replace_all _ =
     (Type.Variable.GlobalTransforms.Unary.replace_all
        (fun _ -> Some (Type.literal_integer 4))
        (variable_list_to_type [2, [x, 3]; 3, [y, 1; z, 1]]))
-    (Type.IntExpression (polynomial_create_from_variables_list [176, []]));
+    (Type.IntExpression.create (polynomial_create_from_variables_list [176, []]));
   assert_equal
     (Type.Variable.GlobalTransforms.Unary.replace_all
        (function
@@ -2256,7 +2256,7 @@ let test_less_or_equal _ =
     polynomial_create_from_variables_list variable_list |> Type.polynomial_to_type
   in
   let divide_to_type numerator denominator =
-    Type.IntExpression (Type.Polynomial.divide ~compare_t:Type.compare numerator denominator)
+    Type.IntExpression.create (Type.Polynomial.divide ~compare_t:Type.compare numerator denominator)
   in
   let very_complicated_type =
     Type.tuple

source/analysis/type.ml

@@ -979,6 +979,24 @@ end = struct
         ]
 end
 
+module RecordIntExpression : sig
+  type 'a t = private Data of 'a Polynomial.t [@@deriving compare, eq, sexp, show, hash]
+
+  type 'a variant =
+    | NonPolynomial of 'a Polynomial.t
+    | Polynomial of 'a t
+
+  val normalize_variant : compare_t:('a -> 'a -> int) -> 'a Polynomial.t -> 'a variant
+end = struct
+  type 'a t = Data of 'a Polynomial.t [@@deriving compare, eq, sexp, show, hash]
+
+  type 'a variant =
+    | NonPolynomial of 'a Polynomial.t
+    | Polynomial of 'a t
+
+  let normalize_variant ~compare_t:_ polynomial = Polynomial (Data polynomial)
+end
+
 open Record.Callable
 module CallableParameter = Record.Callable.RecordParameter
 
@@ -1031,12 +1049,23 @@ module T = struct
     | Tuple of t Record.OrderedTypes.record
     | Union of t list
     | Variable of t Record.Variable.RecordUnary.record
-    | IntExpression of t Polynomial.t
+    | IntExpression of t RecordIntExpression.t
   [@@deriving compare, eq, sexp, show, hash]
 end
 
 include T
 
+type type_t = t [@@deriving compare, eq, sexp, show, hash]
+
+module IntExpression : sig
+  val create : type_t Polynomial.t -> type_t
+end = struct
+  let create polynomial =
+    match RecordIntExpression.normalize_variant ~compare_t:[%compare: type_t] polynomial with
+    | RecordIntExpression.NonPolynomial _ -> failwith "impossible"
+    | RecordIntExpression.Polynomial polynomial -> IntExpression polynomial
+end
+
 let _ = show (* shadowed below *)
 
 type class_data = {
@@ -1046,60 +1075,64 @@ type class_data = {
 }
 [@@deriving sexp]
 
-type type_t = t [@@deriving compare, eq, sexp, show, hash]
-
 let polynomial_to_type polynomial =
   match polynomial with
   | [] -> Literal (Integer 0)
   | [{ Monomial.variables = []; constant_factor }] -> Literal (Integer constant_factor)
   | [{ Monomial.variables = [{ degree = 1; variable = Variable variable }]; constant_factor = 1 }]
     ->
       Variable variable
-  | _ -> IntExpression polynomial
+  | _ -> IntExpression.create polynomial
 
 
 let solve_less_or_equal_polynomial ~left ~right ~solve ~impossible =
   match left, right with
-  | IntExpression polynomial, _ when Polynomial.is_base_case polynomial ->
+  | IntExpression (Data polynomial), _ when Polynomial.is_base_case polynomial ->
       solve ~left:(polynomial_to_type polynomial) ~right
-  | _, IntExpression polynomial when Polynomial.is_base_case polynomial ->
+  | _, IntExpression (Data polynomial) when Polynomial.is_base_case polynomial ->
       solve ~left ~right:(polynomial_to_type polynomial)
-  | ( IntExpression ({ Monomial.constant_factor; variables = [] } :: polynomial),
+  | ( IntExpression (Data ({ Monomial.constant_factor; variables = [] } :: polynomial)),
       Literal (Integer literal) ) ->
-      solve ~left:(IntExpression polynomial) ~right:(Literal (Integer (literal - constant_factor)))
+      solve
+        ~left:(IntExpression.create polynomial)
+        ~right:(Literal (Integer (literal - constant_factor)))
   | ( Literal (Integer literal),
-      IntExpression ({ Monomial.constant_factor; variables = [] } :: polynomial) ) ->
-      solve ~left:(Literal (Integer (literal - constant_factor))) ~right:(IntExpression polynomial)
-  | IntExpression [{ Monomial.constant_factor; variables }], Literal (Integer literal)
+      IntExpression (Data ({ Monomial.constant_factor; variables = [] } :: polynomial)) ) ->
+      solve
+        ~left:(Literal (Integer (literal - constant_factor)))
+        ~right:(IntExpression.create polynomial)
+  | IntExpression (Data [{ Monomial.constant_factor; variables }]), Literal (Integer literal)
     when constant_factor <> 1 ->
       if literal mod constant_factor <> 0 then
         impossible
       else
         solve
-          ~left:(IntExpression [{ constant_factor = 1; variables }])
+          ~left:(IntExpression.create [{ constant_factor = 1; variables }])
           ~right:(Literal (Integer (literal / constant_factor)))
-  | Literal (Integer literal), IntExpression [{ Monomial.constant_factor; variables }]
+  | Literal (Integer literal), IntExpression (Data [{ Monomial.constant_factor; variables }])
     when constant_factor <> 1 ->
       if literal mod constant_factor <> 0 then
         impossible
       else
         solve
           ~left:(Literal (Integer (literal / constant_factor)))
-          ~right:(IntExpression [{ Monomial.constant_factor = 1; variables }])
-  | ( IntExpression (({ variables = []; _ } as left_monomial) :: left_polynomial_tail),
-      IntExpression ({ variables = []; _ } :: _ as right_polynomial) ) ->
+          ~right:(IntExpression.create [{ Monomial.constant_factor = 1; variables }])
+  | ( IntExpression (Data (({ variables = []; _ } as left_monomial) :: left_polynomial_tail)),
+      IntExpression (Data ({ variables = []; _ } :: _ as right_polynomial)) ) ->
       let right_polynomial =
         Polynomial.subtract right_polynomial [left_monomial] ~compare_t:T.compare
       in
-      solve ~left:(IntExpression left_polynomial_tail) ~right:(IntExpression right_polynomial)
+      solve
+        ~left:(IntExpression.create left_polynomial_tail)
+        ~right:(IntExpression.create right_polynomial)
   | IntExpression _, Primitive _ -> solve ~left:(Primitive "int") ~right
   | _ -> impossible
 
 
 let type_to_int_expression = function
-  | Literal (Integer literal) -> Some (IntExpression (Polynomial.create_from_int literal))
-  | Variable variable -> Some (IntExpression (Polynomial.create_from_variable variable))
-  | IntExpression polynomial -> Some (IntExpression polynomial)
+  | Literal (Integer literal) -> Some (IntExpression.create (Polynomial.create_from_int literal))
+  | Variable variable -> Some (IntExpression.create (Polynomial.create_from_variable variable))
+  | IntExpression (Data polynomial) -> Some (IntExpression.create polynomial)
   | Primitive "int" -> Some (Primitive "int")
   | Any -> Some Any
   | _ -> None
@@ -1109,7 +1142,7 @@ let checked_division left right =
   if List.length right = 0 then
     Bottom
   else
-    IntExpression (Polynomial.divide left right ~compare_t:T.compare)
+    IntExpression.create (Polynomial.divide left right ~compare_t:T.compare)
 
 
 let merge_int_expressions ?(divide = false) left right ~operation =
@@ -1123,11 +1156,11 @@ let merge_int_expressions ?(divide = false) left right ~operation =
   | Primitive "int", _
   | _, Primitive "int" ->
       Primitive "int"
-  | IntExpression left, IntExpression right ->
+  | IntExpression (Data left), IntExpression (Data right) ->
       if divide then
         checked_division left right
       else
-        IntExpression (operation left right)
+        IntExpression.create (operation left right)
   | _ -> Bottom
 
 
@@ -1143,9 +1176,9 @@ let local_replace_polynomial polynomial ~replace_variable ~replace_recursive =
         replace_variable variable >>| fun result -> monomial_variable, result
     | Monomial.Divide (dividend, quotient) ->
         let replace_polynomial polynomial =
-          match replace_recursive (IntExpression polynomial) with
+          match replace_recursive (IntExpression.create polynomial) with
           | Some replaced -> replaced
-          | None -> IntExpression polynomial
+          | None -> IntExpression.create polynomial
         in
         let replaced_division =
           merge_int_expressions
@@ -1165,7 +1198,7 @@ let local_replace_polynomial polynomial ~replace_variable ~replace_recursive =
           Polynomial.replace left ~by:right ~variable ~compare_t:T.compare)
     in
     let replaced_expression =
-      List.fold replacements ~init:(IntExpression polynomial) ~f:merge_replace
+      List.fold replacements ~init:(IntExpression.create polynomial) ~f:merge_replace
     in
     Some replaced_expression
 
@@ -1455,9 +1488,9 @@ let rec pp format annotation =
         "typing.Union[%s]"
         (List.map parameters ~f:show |> String.concat ~sep:", ")
   | Variable unary -> Record.Variable.RecordUnary.pp_concise format unary ~pp_type:pp
-  | IntExpression polynomial when Polynomial.is_base_case polynomial ->
+  | IntExpression (Data polynomial) when Polynomial.is_base_case polynomial ->
       pp format (polynomial_to_type polynomial)
-  | IntExpression polynomial ->
+  | IntExpression (Data polynomial) ->
       Format.fprintf
         format
         "pyre_extensions.IntExpression[%s]"
@@ -1542,9 +1575,9 @@ and pp_concise format annotation =
       Format.fprintf format "Optional[%a]" pp_concise parameter
   | Union parameters -> Format.fprintf format "Union[%a]" pp_comma_separated parameters
   | Variable { variable; _ } -> Format.fprintf format "%s" (strip_qualification variable)
-  | IntExpression polynomial when Polynomial.is_base_case polynomial ->
+  | IntExpression (Data polynomial) when Polynomial.is_base_case polynomial ->
       pp_concise format (polynomial_to_type polynomial)
-  | IntExpression polynomial ->
+  | IntExpression (Data polynomial) ->
       Format.fprintf
         format
         "pyre_extensions.IntExpression[%s]"
@@ -1906,9 +1939,9 @@ let rec expression annotation =
         get_item_call "typing.Optional" [expression parameter]
     | Union parameters -> get_item_call "typing.Union" (List.map ~f:expression parameters)
     | Variable { variable; _ } -> create_name variable
-    | IntExpression polynomial when Polynomial.is_base_case polynomial ->
+    | IntExpression (Data polynomial) when Polynomial.is_base_case polynomial ->
         convert_annotation (polynomial_to_type polynomial)
-    | IntExpression polynomial ->
+    | IntExpression (Data polynomial) ->
         let convert_int_expression arguments ~operator =
           Expression.Call
             {
@@ -1946,7 +1979,10 @@ let rec expression annotation =
                            {
                              name = "pyre_extensions.Divide";
                              parameters =
-                               [Single (IntExpression dividend); Single (IntExpression quotient)];
+                               [
+                                 Single (IntExpression.create dividend);
+                                 Single (IntExpression.create quotient);
+                               ];
                            })
                 in
                 if degree = 1 then
@@ -1957,7 +1993,7 @@ let rec expression annotation =
                   in
                   convert_int_expression ~operator:"Multiply" arguments)
           in
-          if List.length variables = 0 then
+          if List.length variables = 1 then
             constant_factor
           else
             convert_int_expression ~operator:"Multiply" (constant_factor :: variables)
@@ -3911,21 +3947,21 @@ end = struct
 
     let rec local_collect = function
       | Variable variable -> [variable]
-      | IntExpression polynomial ->
+      | IntExpression (Data polynomial) ->
           List.concat_map polynomial ~f:(fun { variables; _ } ->
               List.concat_map variables ~f:(fun { variable; _ } ->
                   match variable with
                   | Variable x -> [x]
                   | Divide (dividend, quotient) ->
-                      local_collect (IntExpression dividend)
-                      @ local_collect (IntExpression quotient)))
+                      local_collect (IntExpression.create dividend)
+                      @ local_collect (IntExpression.create quotient)))
           |> List.dedup_and_sort ~compare
       | _ -> []
 
 
     let rec local_replace replacement = function
       | Variable variable -> replacement variable
-      | IntExpression polynomial ->
+      | IntExpression (Data polynomial) ->
           let replace_variable variable =
             match replacement variable with
             | Some replaced_variable ->

source/analysis/type.mli

@@ -262,6 +262,10 @@ module Polynomial : sig
     'a t
 end
 
+module RecordIntExpression : sig
+  type 'a t = private Data of 'a Polynomial.t [@@deriving compare, eq, sexp, show, hash]
+end
+
 module Primitive : sig
   type t = Identifier.t [@@deriving compare, eq, sexp, show, hash]
 
@@ -304,9 +308,13 @@ and t =
   | Tuple of t Record.OrderedTypes.record
   | Union of t list
   | Variable of t Record.Variable.RecordUnary.record
-  | IntExpression of t Polynomial.t
+  | IntExpression of t RecordIntExpression.t
 [@@deriving compare, eq, sexp, show, hash]
 
+module IntExpression : sig
+  val create : t Polynomial.t -> t
+end
+
 type class_data = {
   instantiated: t;
   accessed_through_class: bool;

source/analysis/typeOrder.ml

@@ -179,9 +179,11 @@ module OrderImplementation = struct
               union
             else
               List.map elements ~f:(join order other) |> List.fold ~f:(join order) ~init:Type.Bottom
-        | Type.IntExpression polynomial, other when Type.Polynomial.is_base_case polynomial ->
+        | Type.IntExpression (Data polynomial), other when Type.Polynomial.is_base_case polynomial
+          ->
             join order other (Type.polynomial_to_type polynomial)
-        | other, Type.IntExpression polynomial when Type.Polynomial.is_base_case polynomial ->
+        | other, Type.IntExpression (Data polynomial) when Type.Polynomial.is_base_case polynomial
+          ->
             join order other (Type.polynomial_to_type polynomial)
         | Type.IntExpression _, other
         | other, Type.IntExpression _ ->