OCamlPro / flambda-task-force

13 stars 1 forks source link

Handle some simple Match in Match cases in inline_and_simplify #144

Open chambart opened 8 years ago

chambart commented 8 years ago
let f x =
  match x with
  | None ->
    (match x with
    | None -> ...
    | Some _ -> ...)

could be simplified. The simple version involves adding some more information to the approximation of x. Note that the Some/None case in fact is not a simple one as this is compiled to if x then ... else ..., hence dropping the information about the structure of x

chambart commented 8 years ago

Some simple version propagating it through the environment (not the approximation): https://github.com/chambart/ocaml-1/tree/match_in_match

When entering a branch of a match or an if, the environment remembers which variable where tested and to which value. This works reasonably well on switch, but is often useless on if: An if_then_else constructor often test the variable to a certain value: if x = 3 then ... else .... Since the test expression is duplicated for each if, it is a new variable each time hence not benefiting from the optimization.

To do a better job, we need to either:

This may probably ask for a postpone to a future release.

chambart commented 8 years ago

After playing a bit more with that, I tried adding some relational information to some booleans, here are some examples of how it behaves:

let f x =
  match x with
  | None -> begin
    match x with
    | None -> 1
    | Some _ -> 2
    end
  | Some v -> begin
    match x with
    | None -> 3
    | Some _ -> v
    end

This didn't need any more than direct information about the taken branch:

(let
  (f/1199 =
     (function x/1200
       (if x/1200 (if x/1200 (field 0 x/1200) 3) (if x/1200 2 1))))

hence it works well:

(if x_6/2210 (field 0 x_6/2210) 1)

The added approximation allows to refine x in

let f x =
  if x = 3 then
    x
  else
    x
(if (== x_6/1204 3) 3 x_6/1204)

But we can propagate only singleton information in the approximation currently hence:

type t = A | B

let f t =
  match t with
  | A ->
    (match t with
     | A -> 1
     | B -> 2)
  | B ->
    (match t with
     | A -> 3
     | B -> 4)

give

(if (!= t_6/2212 0) (if (!= t_6/2212 0) 4 3) 1)

The approximation correctly tells that in the ifnot branch, t_6 is not not 0 hence is 0, but in the ifso branch there is no representation for t_6 is either a bloc or an integer different from 0. In that case this could be solved by propagating the shape of the type t to flambda: if we know that t can only contain 1 or 0 then not 0 is also a representable singleton.

For more complex pattern matchings, it would require some representation for interval constraints.