RoundTrip/t63 failure

[yuriy0]

 ~/hakaru
 $ pretty tests/RoundTrip/t63.0.hk
fn x2 real:
x1 <~ uniform(nat2real(0), nat2real(1))
x0 <~ uniform(nat2real(0), nat2real(1))
if nat2real(0) < x2 / x1 - x0 && x2 / x1 - x0 < nat2real(1):
  weight(1/ real2prob(x1), return ())
else: reject. measure(unit)

 ~/hakaru
 $ hk-maple tests/RoundTrip/t63.0.hk
fn x2 real:
if +1/1 <= x2 && x2 < +2/1:
  weight
    (real2prob
       (log(2/1) * (+2/1) + log(real2prob(x2)) * (-2/1) + (-2/1) + x2),
     return ())
else:
  if +0/1 < x2 && x2 < +1/1:
    weight(real2prob(x2 * (-1/1) + log(2/1) * (+2/1)), return ())
  else: reject. measure(unit)

 ~/hakaru
 $ pretty tests/RoundTrip/t63.expected.hk
fn x1 real:
if x1 <= +0/1: reject. measure(unit)
else:
  weight
    (if x1 < +1/1: real2prob(log(2/1) * (+2/1) + (-1/1))
     else:
       if x1 < +2/1:
         real2prob
           (log(2/1) * (+2/1) + (-2/1) + x1 + log(real2prob(x1)) * (-2/1))
       else: 0/1,
     return ()) <|>
  (if x1 < +1/1: weight(real2prob(x1 * (-1/1) + (+1/1)), return ())
   else: reject. measure(unit))

 ~/hakaru
 $ hk-maple tests/RoundTrip/t63.expected.hk
fn x1 real:
if x1 <= +0/1: reject. measure(unit)
else:
  weight
    (if x1 < +1/1: real2prob(log(2/1) * (+2/1) + (-1/1))
     else:
       if x1 < +2/1:
         real2prob
           (log(2/1) * (+2/1) + (-2/1) + x1 + log(real2prob(x1)) * (-2/1))
       else: 0/1,
     return ()) <|>
  (if x1 < +1/1: weight(real2prob(x1 * (-1/1) + (+1/1)), return ())
   else: reject. measure(unit))

The simplified output and expected output are (in terms of sampling) the same program, but expected contains and if inside a weight and another inside a weight, whereas the simplified output puts all the weights inside the ifs.

I don't think there's a way to get precisely the expected output; we solve two uniforms in t63.0 and after that happens, there's no way to get one of the ifs inside a weight and one outside. I think t63.0 should simplify to itself (it does) and t63.expected should simplify to the current output.

[ccshan]

I don't mind at all the different nesting of weight and if, but it's too bad that the <|> in t63.expected (summing two measures over unit) does not go away (because the identical applyintegrands can be factored out and the weights summed).

[yuriy0]

it's too bad that the <|> in t63.expected (summing two measures over unit) does not go away

Indeed, but that is because of the different nesting of weight and if; the simplifier tries (successfully!) not to interchange weights of ifs and ifs of weights. Perhaps it is appropriate to do so when the bodies of contain the same applyintegrand? Or more generally, any subterms which differ only by weights? If so, which nesting is preferred? I think the 'strongest' factorization would produce a weight of ifs.

[JacquesCarette]

The two outer split of the <|> are the same - doesn't that mean that they could be merged?

[yuriy0]

The two outer split of the <|> are the same - doesn't that mean that they could be merged?

Yes, but

the simplifier tries (successfully!) not to interchange weights of ifs and ifs of weights

Again, this may be a special case where we can perform the interchange. But the conditions of the two Partitions are not identical; in particular, the conditions of one are a subset of the other. I think this could be too strong in general (but I could try it!).

[JacquesCarette]

One can always 'split' a Partition into having more cases (still disjoint and complete) but with the same body. That makes joining partitions (such as these) easy.