fixed up unboxing proofs to reflect that "unboxed" int8/16 are just u…

…ntagged immediates

middle_end/flambda2/simplify/unboxing/optimistic_unboxing_decision.ml

@@ -40,7 +40,7 @@ let make_optimistic_const_ctor () : U.const_ctors_decision =
 
 let make_optimistic_number_decision tenv param_type
     (decider : Unboxers.number_decider) : U.decision option =
-  match decider.prove_is_a_boxed_or_tagged_number tenv param_type with
+  match decider.prove_is_a_boxed_number tenv param_type with
   | Proved () ->
     let naked_number = Extra_param_and_args.create ~name:decider.param_name in
     Some (Unbox (Number (decider.kind, naked_number)))
@@ -53,8 +53,6 @@ let deciders =
   [ Unboxers.Immediate.decider;
     Unboxers.Float.decider;
     Unboxers.Float32.decider;
-    Unboxers.Int8.decider;
-    Unboxers.Int16.decider;
     Unboxers.Int32.decider;
     Unboxers.Int64.decider;
     Unboxers.Nativeint.decider;

middle_end/flambda2/simplify/unboxing/unboxers.ml

@@ -19,7 +19,7 @@ open! Simplify_import
 type number_decider =
   { param_name : string;
     kind : K.Naked_number_kind.t;
-    prove_is_a_boxed_or_tagged_number : TE.t -> T.t -> unit T.proof_of_property
+    prove_is_a_boxed_number : TE.t -> T.t -> unit T.proof_of_property
   }
 
 type unboxer =
@@ -42,7 +42,7 @@ module Immediate = struct
   let decider =
     { param_name = "naked_immediate";
       kind = K.Naked_number_kind.Naked_immediate;
-      prove_is_a_boxed_or_tagged_number = T.prove_is_a_tagged_immediate
+      prove_is_a_boxed_number = T.prove_is_a_tagged_immediate
     }
 
   let unboxing_prim simple = P.(Unary (Untag_immediate, simple))
@@ -55,45 +55,11 @@ module Immediate = struct
     }
 end
 
-module Int8 = struct
-  let decider =
-    { param_name = "naked_int8";
-      kind = Naked_int8;
-      prove_is_a_boxed_or_tagged_number = T.prove_is_a_tagged_immediate
-    }
-
-  let unboxing_prim simple = P.(Unary (Untag_immediate, simple))
-
-  let unboxer =
-    { var_name = "naked_int8";
-      poison_const = Const.naked_int8 (Numeric_types.Int8.of_int (-0x7d));
-      unboxing_prim;
-      prove_simple = T.meet_tagging_of_simple
-    }
-end
-
-module Int16 = struct
-  let decider =
-    { param_name = "naked_int16";
-      kind = Naked_int16;
-      prove_is_a_boxed_or_tagged_number = T.prove_is_a_tagged_immediate
-    }
-
-  let unboxing_prim simple = P.(Unary (Untag_immediate, simple))
-
-  let unboxer =
-    { var_name = "naked_int16";
-      poison_const = Const.naked_int16 (Numeric_types.Int16.of_int (-0x7d3d));
-      unboxing_prim;
-      prove_simple = T.meet_tagging_of_simple
-    }
-end
-
 module Float32 = struct
   let decider =
     { param_name = "unboxed_float32";
       kind = K.Naked_number_kind.Naked_float32;
-      prove_is_a_boxed_or_tagged_number = T.prove_is_a_boxed_float32
+      prove_is_a_boxed_number = T.prove_is_a_boxed_float32
     }
 
   let unboxing_prim simple = P.(Unary (Unbox_number Naked_float32, simple))
@@ -111,7 +77,7 @@ module Float = struct
   let decider =
     { param_name = "unboxed_float";
       kind = K.Naked_number_kind.Naked_float;
-      prove_is_a_boxed_or_tagged_number = T.prove_is_a_boxed_float
+      prove_is_a_boxed_number = T.prove_is_a_boxed_float
     }
 
   let unboxing_prim simple = P.(Unary (Unbox_number Naked_float, simple))
@@ -128,7 +94,7 @@ module Int32 = struct
   let decider =
     { param_name = "unboxed_int32";
       kind = K.Naked_number_kind.Naked_int32;
-      prove_is_a_boxed_or_tagged_number = T.prove_is_a_boxed_int32
+      prove_is_a_boxed_number = T.prove_is_a_boxed_int32
     }
 
   let unboxing_prim simple = P.(Unary (Unbox_number Naked_int32, simple))
@@ -145,7 +111,7 @@ module Int64 = struct
   let decider =
     { param_name = "unboxed_int64";
       kind = K.Naked_number_kind.Naked_int64;
-      prove_is_a_boxed_or_tagged_number = T.prove_is_a_boxed_int64
+      prove_is_a_boxed_number = T.prove_is_a_boxed_int64
     }
 
   let unboxing_prim simple = P.(Unary (Unbox_number Naked_int64, simple))
@@ -162,7 +128,7 @@ module Nativeint = struct
   let decider =
     { param_name = "unboxed_nativeint";
       kind = K.Naked_number_kind.Naked_nativeint;
-      prove_is_a_boxed_or_tagged_number = T.prove_is_a_boxed_nativeint
+      prove_is_a_boxed_number = T.prove_is_a_boxed_nativeint
     }
 
   let unboxing_prim simple = P.(Unary (Unbox_number Naked_nativeint, simple))
@@ -179,7 +145,7 @@ module Vec128 = struct
   let decider =
     { param_name = "unboxed_vec128";
       kind = K.Naked_number_kind.Naked_vec128;
-      prove_is_a_boxed_or_tagged_number = prove_is_a_boxed_vec128
+      prove_is_a_boxed_number = prove_is_a_boxed_vec128
     }
 
   let unboxing_prim simple = P.(Unary (Unbox_number Naked_vec128, simple))

middle_end/flambda2/simplify/unboxing/unboxers.mli

@@ -19,7 +19,7 @@ open! Simplify_import
 type number_decider =
   { param_name : string;
     kind : K.Naked_number_kind.t;
-    prove_is_a_boxed_or_tagged_number : TE.t -> T.t -> unit T.proof_of_property
+    prove_is_a_boxed_number : TE.t -> T.t -> unit T.proof_of_property
   }
 
 type unboxer =
@@ -66,10 +66,6 @@ module Float32 : Number_S
 
 module Float : Number_S
 
-module Int8 : Number_S
-
-module Int16 : Number_S
-
 module Int32 : Number_S
 
 module Int64 : Number_S

middle_end/flambda2/simplify/unboxing/unboxing_epa.ml

@@ -256,12 +256,6 @@ and compute_extra_args_for_one_decision_and_use_aux ~(pass : U.pass) rewrite_id
   | Unbox (Number (Naked_float, epa)) ->
     compute_extra_arg_for_number Naked_float Unboxers.Float.unboxer epa
       rewrite_id ~typing_env_at_use arg_being_unboxed
-  | Unbox (Number (Naked_int8, epa)) ->
-    compute_extra_arg_for_number Naked_int8 Unboxers.Int8.unboxer epa rewrite_id
-      ~typing_env_at_use arg_being_unboxed
-  | Unbox (Number (Naked_int16, epa)) ->
-    compute_extra_arg_for_number Naked_int16 Unboxers.Int16.unboxer epa
-      rewrite_id ~typing_env_at_use arg_being_unboxed
   | Unbox (Number (Naked_int32, epa)) ->
     compute_extra_arg_for_number Naked_int32 Unboxers.Int32.unboxer epa
       rewrite_id ~typing_env_at_use arg_being_unboxed
@@ -271,7 +265,7 @@ and compute_extra_args_for_one_decision_and_use_aux ~(pass : U.pass) rewrite_id
   | Unbox (Number (Naked_nativeint, epa)) ->
     compute_extra_arg_for_number Naked_nativeint Unboxers.Nativeint.unboxer epa
       rewrite_id ~typing_env_at_use arg_being_unboxed
-  | Unbox (Number (Naked_immediate, epa)) ->
+  | Unbox (Number ((Naked_immediate | Naked_int8 | Naked_int16), epa)) ->
     compute_extra_arg_for_number Naked_immediate Unboxers.Immediate.unboxer epa
       rewrite_id ~typing_env_at_use arg_being_unboxed
   | Unbox (Number (Naked_vec128, epa)) ->

middle_end/flambda2/types/flambda2_types.mli

@@ -645,6 +645,8 @@ type boxed_or_tagged_number = private
 val prove_is_a_boxed_or_tagged_number :
   Typing_env.t -> t -> boxed_or_tagged_number proof_of_property
 
+val prove_nothing : Typing_env.t -> t -> _ proof_of_property
+
 val prove_is_a_tagged_immediate : Typing_env.t -> t -> unit proof_of_property
 
 val prove_is_a_boxed_float32 : Typing_env.t -> t -> unit proof_of_property

middle_end/flambda2/types/provers.ml

@@ -496,6 +496,8 @@ let prove_is_a_boxed_or_tagged_number_value _env
     Proved (Boxed (alloc_mode, Naked_vec128, contents_ty))
   | Mutable_block _ | Closures _ | String _ | Array _ -> Unknown
 
+let prove_nothing _env _ : _ proof_of_property = Unknown
+
 let prove_is_a_boxed_or_tagged_number env t =
   gen_value_to_proof prove_is_a_boxed_or_tagged_number_value env t
 

middle_end/flambda2/types/provers.mli

@@ -98,6 +98,8 @@ type boxed_or_tagged_number = private
 val prove_is_a_boxed_or_tagged_number :
   Typing_env.t -> Type_grammar.t -> boxed_or_tagged_number proof_of_property
 
+val prove_nothing : Typing_env.t -> Type_grammar.t -> _ proof_of_property
+
 val prove_is_a_tagged_immediate :
   Typing_env.t -> Type_grammar.t -> unit proof_of_property