diff options
| author |  jadep <jade.philipoom@gmail.com> | 2019-01-03 13:25:30 -0500 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2019-01-03 13:25:30 -0500 |
| commit | 7e73dfa7cc649634e02c6c7b6d11dac89d1533a1 (patch) | |
| tree | 149b80e73121a3cbed4a6342dcaacebb184b8d26 /src | |
| parent | 3a9825055c10fa02ebfa54e04a2602ae7922d498 (diff) | |
try to fix fancy rewrite rules; current output is incorrect
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/Rewriter.v | 72 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterRulesInterpGood.v | 11 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel2.v | 129 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/fancy_with_casts_rewrite_head.out | 4364 |
4 files changed, 3048 insertions, 1528 deletions
diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v index c1ef61e39..19d921925 100644 --- a/src/Experiments/NewPipeline/Rewriter.v +++ b/src/Experiments/NewPipeline/Rewriter.v @@ -2039,18 +2039,18 @@ Module Compilers. (Z.add_get_carry_concrete 2^256) @@ (?x, ?y) --> (add 0) @@ (y, x) *) make_rewriteo - (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ ??' @ (pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ)))) - (fun '((r1, r2)%core) s rx x rshiftl ry y offset => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) offset) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ ??' @ (pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ)))) + (fun '((r1, r2)%core) s rx x rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) offset) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl rland offset && land_good rland ry mask && range_in_bitwidth rshiftl s && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ #?ℤ @ (pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ)))) - (fun '((r1, r2)%core) s xx rshiftl ry y offset => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) offset) @ (##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ #?ℤ @ (pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ)))) + (fun '((r1, r2)%core) s xx rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) offset) @ (##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && land_good rland ry mask && range_in_bitwidth rshiftl s && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ (pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ)) @ ??')) - (fun '((r1, r2)%core) s rshiftl ry y offset rx x => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) offset) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ (pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ)) @ ??')) + (fun '((r1, r2)%core) s rshiftl rland ry y mask offset rx x => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) offset) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && land_good rland ry mask && range_in_bitwidth rshiftl s && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ (pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ)) @ #?ℤ)) - (fun '((r1, r2)%core) s rshiftl ry y offset xx => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) offset) @ (##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ (pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ)) @ #?ℤ)) + (fun '((r1, r2)%core) s rshiftl rland ry y mask offset xx => cst2 (r1, r2)%core (#(ident.fancy_add (Z.log2 s) offset) @ (##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && land_good rland ry mask && range_in_bitwidth rshiftl s && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo (pcst2 (#pattern.ident.Z_add_get_carry @ #?ℤ @ ??' @ (pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ)))) @@ -2083,30 +2083,30 @@ Module Compilers. (Z.add_with_get_carry_concrete 2^256) @@ (?c, ?x, ?y) --> (addc 0) @@ (c, y, x) *) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ ??' @ pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s rc c rx x rshiftl ry y offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (cst rc c, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) + (fun '((r1, r2)%core) s rc c rx x rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (cst rc c, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && land_good rland ry mask && range_in_bitwidth rshiftl s && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s cc rx x rshiftl ry y offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (##cc, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) + (fun '((r1, r2)%core) s cc rx x rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (##cc, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s && land_good rland ry mask && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s rc c xx rshiftl ry y offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (cst rc c, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) + (fun '((r1, r2)%core) s rc c xx rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (cst rc c, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s && land_good rland ry mask && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s cc xx rshiftl ry y offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (##cc, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) + (fun '((r1, r2)%core) s cc xx rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (##cc, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s && land_good rland ry mask && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ) @ ??')) - (fun '((r1, r2)%core) s rc c rshiftl ry y offset rx x => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (cst rc c, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ) @ ??')) + (fun '((r1, r2)%core) s rc c rshiftl rland ry y mask offset rx x => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (cst rc c, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s && land_good rland ry mask && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ) @ ??')) - (fun '((r1, r2)%core) s cc rshiftl ry y offset rx x => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (##cc, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ) @ ??')) + (fun '((r1, r2)%core) s cc rshiftl rland ry y mask offset rx x => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (##cc, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s && land_good rland ry mask && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ) @ #?ℤ)) - (fun '((r1, r2)%core) s rc c rshiftl ry y offset xx => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (cst rc c, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ) @ #?ℤ)) + (fun '((r1, r2)%core) s rc c rshiftl rland ry y mask offset xx => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (cst rc c, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s && land_good rland ry mask && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo - (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ) @ #?ℤ)) - (fun '((r1, r2)%core) s cc rshiftl ry y offset xx => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (##cc, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ) @ #?ℤ)) + (fun '((r1, r2)%core) s cc rshiftl rland ry y mask offset xx => cst2 (r1, r2)%core (#(ident.fancy_addc (Z.log2 s) offset) @ (##cc, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s && land_good rland ry mask && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo (pcst2 (#pattern.ident.Z_add_with_get_carry @ #?ℤ @ ??' @ ??' @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ))) @@ -2161,11 +2161,11 @@ Module Compilers. (Z.sub_get_borrow_concrete 2^256) @@ (?x, ?y) --> (sub 0) @@ (y, x) *) ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_get_borrow @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s rx x rshiftl ry y offset => cst2 (r1, r2)%core (#(ident.fancy_sub (Z.log2 s) offset) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_sub_get_borrow @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) + (fun '((r1, r2)%core) s rx x rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_sub (Z.log2 s) offset) @ (cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s && land_good rland ry mask && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_get_borrow @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s xx rshiftl ry y offset => cst2 (r1, r2)%core (#(ident.fancy_sub (Z.log2 s) offset) @ (##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_sub_get_borrow @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) + (fun '((r1, r2)%core) s xx rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_sub (Z.log2 s) offset) @ (##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s && land_good rland ry mask && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo (pcst2 (#pattern.ident.Z_sub_get_borrow @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ))) @@ -2189,17 +2189,17 @@ Module Compilers. (Z.sub_with_get_borrow_concrete 2^256) @@ (?c, ?x, ?y) --> (subb 0) @@ (c, y, x) *) ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ ??' @ ??' @ pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s rb b rx x rshiftl ry y offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) offset) @ (cst rb b, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ ??' @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) + (fun '((r1, r2)%core) s rb b rx x rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) offset) @ (cst rb b, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s && land_good rland ry mask && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s bb rx x rshiftl ry y offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) offset) @ (##bb, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ #?ℤ @ ??' @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) + (fun '((r1, r2)%core) s bb rx x rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) offset) @ (##bb, cst rx x, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s && land_good rland ry mask && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ ??' @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s rb b xx rshiftl ry y offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) offset) @ (cst rb b, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ ??' @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) + (fun '((r1, r2)%core) s rb b xx rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) offset) @ (cst rb b, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s && land_good rland ry mask && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo - (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ ??' @ #?ℤ))) - (fun '((r1, r2)%core) s bb xx rshiftl ry y offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) offset) @ (##bb, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s) + (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ #?ℤ @ #?ℤ @ pcst (#pattern.ident.Z_shiftl @ (pcst (#pattern.ident.Z_land @ ??' @ #?ℤ)) @ #?ℤ))) + (fun '((r1, r2)%core) s bb xx rshiftl rland ry y mask offset => cst2 (r1, r2)%core (#(ident.fancy_subb (Z.log2 s) offset) @ (##bb, ##xx, cst ry y)) when (s =? 2^Z.log2 s) && shiftl_good rshiftl ry offset && range_in_bitwidth rshiftl s && land_good rland ry mask && (mask =? Z.ones (Z.log2 s - offset)) && (0 <=? offset) && (offset <=? Z.log2 s)) ; make_rewriteo (pcst2 (#pattern.ident.Z_sub_with_get_borrow @ #?ℤ @ ??' @ ??' @ pcst (#pattern.ident.Z_shiftr @ ??' @ #?ℤ))) diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v index 9b344a577..cf6e3f373 100644 --- a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v +++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v @@ -547,6 +547,7 @@ Module Compilers. | [ |- context[Z.shiftl] ] => rewrite Z.shiftl_mul_pow2 by auto with zarith | [ |- context[Z.shiftr] ] => rewrite Z.shiftr_div_pow2 by auto with zarith | [ |- context[Z.shiftl _ (-_)] ] => rewrite Z.shiftl_opp_r + | [ |- context[Z.land _ (Z.ones _)] ] => rewrite Z.land_ones by auto using Z.log2_nonneg | [ |- context[- - _] ] => rewrite Z.opp_involutive | [ H : ?x = 2^Z.log2 ?x |- context[2^Z.log2 ?x] ] => rewrite <- H | [ H : ?x = 2^?n |- context[Z.land _ (?x - 1)] ] @@ -569,6 +570,12 @@ Module Compilers. => progress (push_Zmod; pull_Zmod) | [ |- _ mod ?x = _ mod ?x ] => apply f_equal2; (lia + nia) + | _ => rewrite !Z.shiftl_mul_pow2 in * by auto using Z.log2_nonneg + | _ => rewrite !Z.land_ones in * by auto using Z.log2_nonneg + | H : ?x mod ?b * ?y <= _ + |- context [ (?x * ?y) mod ?b ] => + rewrite (PullPush.Z.mul_mod_l x y b); + rewrite (Z.mod_small (x mod b * y) b) by omega | [ |- context[-?x + ?y] ] => rewrite !Z.add_opp_l | [ |- context[?n + - ?m] ] => rewrite !Z.add_opp_r | [ |- context[?n - - ?m] ] => rewrite !Z.sub_opp_r @@ -761,7 +768,9 @@ Module Compilers. Time all: fancy_local_t. (* Finished transaction in 0.051 secs (0.052u,0.s) (successful) *) Time all: systematically_handle_casts. (* Finished transaction in 2.004 secs (1.952u,0.052s) (successful) *) Time all: try solve [ repeat interp_good_t_step_arith ]. (* Finished transaction in 26.754 secs (26.455u,0.299s) (successful) *) - Qed. + + all:admit. (* TODO(jgross) : prove these *) + Admitted. End with_cast. End RewriteRules. End Compilers. diff --git a/src/Experiments/NewPipeline/Toplevel2.v b/src/Experiments/NewPipeline/Toplevel2.v index 78342238d..d14d9a1b4 100644 --- a/src/Experiments/NewPipeline/Toplevel2.v +++ b/src/Experiments/NewPipeline/Toplevel2.v @@ -703,6 +703,7 @@ Module Fancy. | ident.snd A B => fun v => snd v | ident.Z_cast r => fun v => v | ident.Z_cast2 (r1, r2) => fun v => v + | ident.Z_land => fun x y => x | _ => make_error end | expr.Abs s d f => make_error @@ -815,6 +816,7 @@ Module Fancy. Local Notation wordmax := (2^256). Local Notation interp := (interp name_eqb wordmax cc_spec). Local Notation uint256 := r[0~>wordmax-1]%zrange. + Local Notation uint128 := r[0~>(2 ^ (Z.log2 wordmax / 2) - 1)]%zrange. Definition cast_oor (r : zrange) (v : Z) := v mod (upper r + 1). Local Notation "'existZ' x" := (existT _ (type.base (base.type.type_base tZ)) x) (at level 200). Local Notation "'existZZ' x" := (existT _ (type.base (base.type.type_base tZ * base.type.type_base tZ)%etype) x) (at level 200). @@ -1620,52 +1622,31 @@ Module Fancy. Context (reg : Type) (error_reg : reg) (reg_eqb : reg -> reg -> bool). Context (reg_eqb_refl : forall r, reg_eqb r r = true). - Lemma interp_ctx_ext e : - forall cc ctx ctx', - (forall n, ctx n = ctx' n) -> - interp name_eqb wordmax cc_spec e cc ctx = interp name_eqb wordmax cc_spec e cc ctx'. - Proof. - induction e; intros; [ cbn; solve [auto] | ]. - cbn. erewrite Tuple.map_ext by eassumption. - apply IHe; [ ]. intros; break_innermost_match; eauto. - Qed. - - Fixpoint reg_depth {t} (e : @expr t) : nat := - match e with - | Ret _ => 0 - | Instr i rd args cont => S (reg_depth cont) - end. - Check interp. + Inductive error_free : @expr reg -> Prop := + | error_free_Ret : forall r, r <> error_reg -> error_free (Ret r) + | error_free_Instr : forall i rd args cont, + error_free cont -> + error_free (Instr i rd args cont) + . Lemma allocate_correct e : forall cc ctx reg_list name_to_reg, - (reg_depth e <= length reg_list)%nat -> + error_free (allocate reg name name_eqb error_reg e reg_list name_to_reg) -> interp reg_eqb wordmax cc_spec (allocate reg name name_eqb error_reg e reg_list name_to_reg) cc ctx = interp name_eqb wordmax cc_spec e cc (fun n : name => ctx (name_to_reg n)). Proof. - induction e; cbn [allocate]; intros; [ reflexivity | ]. - destruct reg_list; intros; cbn [reg_depth] in *; distr_length; [ ]. - cbn. rewrite IHe; try omega. - - + induction e; destruct reg_list; inversion 1; intros; + try reflexivity; try congruence; [ ]. + cbn. rewrite IHe by auto. rewrite Tuple.map_map. - apply interp_ctx_ext; [ ]. intros. - break_innermost_match; try reflexivity. - rewrite reg_eqb_refl in *. congruence. - (* - TODO - name_to_reg is more or less the context -- names that have already been assigned to registers - rd : name (destination name) - n : name (input to ctx) - r : reg (register in which rd now goes) - - if n != rd then name_to_reg n != r? - - rd has been assigned to the name r. - It might be that r has a previous assignment (exists n, name_to_reg n = r and n != rd). - However, we can count on that n never being called, if the reg_list is okay. - *) - + (* + Need to prove that contexts are equivalent and swapping contexts is OK + *) + (* + TODO : either prove this lemma or devise a good way to + prove case-by-case that the output of allocate is + equivalent to the input. + *) Admitted. End with_name. @@ -2329,6 +2310,9 @@ Module Barrett256. cbn; omega. Qed. + (* This expression should have NO ands in it -- search for "&'" should return nothing *) + Print barrett_red256. + (* TODO: don't rely on the C, M, and L flags *) Lemma barrett_red256_fancy_correct : forall xLow xHigh error, @@ -2392,6 +2376,9 @@ Module Barrett256. end. repeat (econstructor; [ solve [sub] | intros ]). + econstructor. + { sub. Print Fancy.valid_scalar. + [ solve [sub] | intros ]. (* For the too-tight RSHI cast, we have to loosen the bounds *) eapply Fancy.valid_LetInZ_loosen; try solve [sub]; [ cbn; omega | | intros; apply loosen_rshi_subgoal; solve [eauto] ]. @@ -2478,68 +2465,6 @@ Module Barrett256. Admitted. - (* - Import Fancy_PreFancy_Equiv. - - Definition interp_equivZZ_256 {s} := - @interp_equivZZ s 256 ltac:(cbv; congruence) 115792089237316195423570985008687907853269984665640564039457584007913129639935 ltac:(reflexivity). - Definition interp_equivZ_256 {s} := - @interp_equivZ s 256 115792089237316195423570985008687907853269984665640564039457584007913129639935 ltac:(lia) ltac:(reflexivity). - - Local Ltac simplify_op_equiv start_ctx := - cbn - [Fancy.spec (*PreFancy.interp_ident*) ident.gen_interp Fancy.cc_spec Z.shiftl]; - repeat match goal with H : start_ctx _ = _ |- _ => rewrite H end; - cbv - [ - Z.rshi Z.cc_m Fancy.CC.cc_m - Z.add_with_get_carry_full Z.add_get_carry_full - Z.sub_get_borrow_full Z.sub_with_get_borrow_full - Z.le Z.lt Z.ltb Z.leb Z.geb Z.eqb Z.land Z.shiftr Z.shiftl - Z.add Z.mul Z.div Z.sub Z.modulo Z.testbit Z.pow Z.ones - fst snd]; cbn [fst snd]; - try (replace (2 ^ (256 / 2) - 1) with (Z.ones 128) by reflexivity; rewrite !Z.land_ones by omega); - autorewrite with to_div_mod; rewrite ?Z.mod_mod, <-?Z.testbit_spec' by omega; - let r := (eval compute in (2 ^ 256)) in - replace (2^256) with r in * by reflexivity; - repeat match goal with - | H : 0 <= ?x < ?m |- context [?x mod ?m] => rewrite (Z.mod_small x m) by apply H - | |- context [?x <? 0] => rewrite (proj2 (Z.ltb_ge x 0)) by (break_match; Z.zero_bounds) - | _ => rewrite Z.mod_small with (b:=2) by (break_match; omega) - | |- context [ (if Z.testbit ?a ?n then 1 else 0) + ?b + ?c] => - replace ((if Z.testbit a n then 1 else 0) + b + c) with (b + c + (if Z.testbit a n then 1 else 0)) by ring - end. - - Local Ltac solve_nonneg ctx := - match goal with x := (Fancy.spec _ _ _) |- _ => subst x end; - simplify_op_equiv ctx; Z.zero_bounds. - - Local Ltac generalize_result := - let v := fresh "v" in intro v; generalize v; clear v; intro v. - - Local Ltac generalize_result_nonneg ctx := - let v := fresh "v" in - let v_nonneg := fresh "v_nonneg" in - intro v; assert (0 <= v) as v_nonneg; [solve_nonneg ctx |generalize v v_nonneg; clear v v_nonneg; intros v v_nonneg]. - - Local Ltac step_abs := - match goal with - | [ |- context G[expr.interp ?ident_interp (expr.Abs ?f) ?x] ] - => let G' := context G[expr.interp ident_interp (f x)] in - change G'; cbv beta - end. - Local Ltac step ctx := - repeat step_abs; - match goal with - | |- Fancy.interp _ _ _ (Fancy.Instr (Fancy.ADD _) _ _ (Fancy.Instr (Fancy.ADDC _) _ _ _)) _ _ = _ => - apply interp_equivZZ_256; [ simplify_op_equiv ctx | simplify_op_equiv ctx | generalize_result_nonneg ctx] - | [ |- _ = expr.interp _ (PreFancy.LetInAppIdentZ _ _ _ _ _ _) ] - => apply interp_equivZ_256; [simplify_op_equiv ctx | generalize_result] - | [ |- _ = expr.interp _ (PreFancy.LetInAppIdentZZ _ _ _ _ _ _) ] - => apply interp_equivZZ_256; [ simplify_op_equiv ctx | simplify_op_equiv ctx | generalize_result] - end. - - Local Opaque PreFancy.interp_cast_mod. - *) - Lemma prod_barrett_red256_correct : forall (cc_start_state : Fancy.CC.state) (* starting carry flags *) (start_context : register -> Z) (* starting register values *) @@ -3363,4 +3288,4 @@ Eval cbv beta iota delta [barrett_red256_alloc] in barrett_red256_alloc. Check prod_barrett_red256_correct. Print Assumptions prod_barrett_red256_correct. (* The equivalence with generated code is admitted as barrett_red256_alloc_equivalent. *) -*) +*)
\ No newline at end of file diff --git a/src/Experiments/NewPipeline/fancy_with_casts_rewrite_head.out b/src/Experiments/NewPipeline/fancy_with_casts_rewrite_head.out index 7abfcbfbf..f3c6cd79f 100644 --- a/src/Experiments/NewPipeline/fancy_with_casts_rewrite_head.out +++ b/src/Experiments/NewPipeline/fancy_with_casts_rewrite_head.out @@ -735,12 +735,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s4 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); - v0 <- type.try_make_transport_cps s8 - ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; fv <- (x10 <- (if ((let (x10, _) := xv in x10) =? @@ -831,10 +829,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s4 - ℤ; - v0 <- type.try_make_transport_cps s8 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x10 <- (if @@ -930,10 +926,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s4 - ℤ; - v0 <- type.try_make_transport_cps s8 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x10 <- (if @@ -1163,14 +1157,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((s4 -> (projT1 args3)) -> (projT1 args0) -> s8)%ptype then - v <- type.try_make_transport_cps s4 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args3); xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); - v0 <- type.try_make_transport_cps s8 - ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; fv <- (x10 <- (if ((let (x10, _) := xv in x10) =? @@ -1259,12 +1251,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((s4 -> (projT1 args3)) -> s8 -> (projT1 args))%ptype then - v <- type.try_make_transport_cps s4 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args3); - v0 <- type.try_make_transport_cps s8 - ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x10 <- (if @@ -1358,12 +1348,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((s4 -> (projT1 args3)) -> s8 -> (projT1 args))%ptype then - v <- type.try_make_transport_cps s4 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args3); - v0 <- type.try_make_transport_cps s8 - ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x10 <- (if @@ -1578,14 +1566,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((s4 -> (projT1 args3)) -> (projT1 args0) -> s8)%ptype then - v <- type.try_make_transport_cps s4 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args3); xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); - v0 <- type.try_make_transport_cps s8 - ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; fv <- (x10 <- (if ((let (x10, _) := xv0 in x10) =? @@ -1662,12 +1648,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((s4 -> (projT1 args3)) -> s8 -> (projT1 args))%ptype then - v <- type.try_make_transport_cps s4 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args3); - v0 <- type.try_make_transport_cps s8 - ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x10 <- (if @@ -1749,12 +1733,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((s4 -> (projT1 args3)) -> s8 -> (projT1 args))%ptype then - v <- type.try_make_transport_cps s4 - ℤ; + v <- type.try_make_transport_cps s4 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args3); - v0 <- type.try_make_transport_cps s8 - ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x10 <- (if @@ -1942,8 +1924,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args2); - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); xv1 <- ident.unify pattern.ident.Literal @@ -2008,12 +1989,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args2); - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); - v0 <- type.try_make_transport_cps s6 - ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; fv <- (x8 <- (if ((let (x8, _) := xv in x8) =? 2 @@ -2081,10 +2060,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args2); - v <- type.try_make_transport_cps s5 - ℤ; - v0 <- type.try_make_transport_cps s6 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x8 <- (if @@ -2144,12 +2121,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args2); - v <- type.try_make_transport_cps s5 - ℤ; - v0 <- type.try_make_transport_cps s6 - ℤ; - v1 <- type.try_make_transport_cps s7 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; + v1 <- type.try_make_transport_cps s7 ℤ; fv <- (x9 <- (if ((let (x9, _) := xv in x9) =? 2 @@ -2235,8 +2209,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args2); - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); xv1 <- ident.unify pattern.ident.Literal @@ -2295,12 +2268,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args2); - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); - v0 <- type.try_make_transport_cps s6 - ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; fv <- (x8 <- (if ((let (x8, _) := xv in x8) =? 1) && @@ -2362,10 +2333,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args2); - v <- type.try_make_transport_cps s5 - ℤ; - v0 <- type.try_make_transport_cps s6 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x8 <- (if @@ -2419,12 +2388,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args2); - v <- type.try_make_transport_cps s5 - ℤ; - v0 <- type.try_make_transport_cps s6 - ℤ; - v1 <- type.try_make_transport_cps s7 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; + v1 <- type.try_make_transport_cps s7 ℤ; fv <- (x9 <- (if ((let (x9, _) := xv in x9) =? 1) && @@ -2499,8 +2465,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (((s5 -> (projT1 args1)) -> (projT1 args0)) -> (projT1 args))%ptype then - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args1); xv0 <- ident.unify pattern.ident.Literal @@ -2559,14 +2524,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (((s5 -> (projT1 args1)) -> (projT1 args0)) -> s6)%ptype then - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args1); xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); - v0 <- type.try_make_transport_cps s6 - ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; fv <- (x8 <- (if ((let (x8, _) := xv in x8) =? 1) && @@ -2626,12 +2589,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (((s5 -> (projT1 args1)) -> s6) -> (projT1 args))%ptype then - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args1); - v0 <- type.try_make_transport_cps s6 - ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x8 <- (if @@ -2683,14 +2644,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype (((s5 -> (projT1 args1)) -> s6) -> s7)%ptype then - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv <- ident.unify pattern.ident.Literal ##(projT2 args1); - v0 <- type.try_make_transport_cps s6 - ℤ; - v1 <- type.try_make_transport_cps s7 - ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; + v1 <- type.try_make_transport_cps s7 ℤ; fv <- (x9 <- (if ((let (x9, _) := xv in x9) =? 1) && @@ -3167,86 +3125,115 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x3 with | (@expr.Ident _ _ _ t3 idc3 @ x5 @ x4)%expr_pat => match x5 with - | @expr.App _ _ _ s5 _ (@expr.Ident _ _ _ t4 idc4) - x6 => + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.Ident + _ _ _ t7 idc7))%expr_pat => match x4 with - | @expr.Ident _ _ _ t5 idc5 => - args <- invert_bind_args idc5 + | @expr.Ident _ _ _ t8 idc8 => + args <- invert_bind_args idc8 Raw.ident.Literal; - args0 <- invert_bind_args idc4 + args0 <- invert_bind_args idc7 + Raw.ident.Literal; + args1 <- invert_bind_args idc6 + Raw.ident.Z_cast; + _ <- invert_bind_args idc5 Raw.ident.Z_land; + args3 <- invert_bind_args idc4 Raw.ident.Z_cast; _ <- invert_bind_args idc3 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc2 + args5 <- invert_bind_args idc2 Raw.ident.Z_cast; - args3 <- invert_bind_args idc1 + args6 <- invert_bind_args idc1 Raw.ident.Literal; - args4 <- invert_bind_args idc0 + args7 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; match pattern.type.unify_extracted_cps - ((ℤ -> ℤ) -> ℤ -> ℤ)%ptype - (((projT1 args4) -> (projT1 args3)) -> - s5 -> (projT1 args))%ptype option - (fun x7 : option => x7) + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> (projT1 args6)) -> + (s8 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x10 : option => x10) with - | Some (_, _, (_, _))%zrange => + | Some (_, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ -> ℤ)%ptype - (((projT1 args4) -> (projT1 args3)) -> - s5 -> (projT1 args))%ptype + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> (projT1 args6)) -> + (s8 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args4); + ##(projT2 args7); xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args3); - v <- type.try_make_transport_cps s5 - ℤ; + ##(projT2 args6); + v <- type.try_make_transport_cps s8 ℤ; xv1 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv2 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x7 <- (let - '(r1, r2)%zrange := - range in - fun (s6 xx : Z) - (rshiftl ry : zrange) - (y : expr ℤ) - (offset : Z) => - if - (s6 =? 2 ^ Z.log2 s6) && - (ZRange.normalize ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s6 - 1])%zrange - then - Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_add - (Z.log2 s6) - offset)%expr @ - ((##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x7, _) := xv in - x7) - (let (x7, _) := xv0 in - x7) args2 args0 - (v (Compile.reflect x6)) - (let (x7, _) := xv1 in - x7); - Some (Base x7)); + fv <- (x10 <- (let + '(r1, r2)%zrange := + range in + fun (s9 xx : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask offset : Z) => + if + (s9 =? 2 ^ Z.log2 s9) && + (ZRange.normalize ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s9 - 1])%zrange && + (mask =? + Z.ones + (Z.log2 s9 - + offset)) + then + Some + (#(Z_cast2 (r1, r2))%expr @ + (#(fancy_add + (Z.log2 s9) + offset)%expr @ + ((##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x10, _) := xv in + x10) + (let (x10, _) := + xv0 in + x10) args5 args3 + args1 + (v + (Compile.reflect x9)) + (let (x10, _) := + xv1 in + x10) + (let (x10, _) := + xv2 in + x10); + Some (Base x10)); Some (fv0 <-- fv; Base fv0)%under_lets else None @@ -3254,10 +3241,61 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s5 _ ($_)%expr _ | @expr.App _ _ - _ s5 _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ - _ s5 _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s5 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.Abs _ + _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.LetIn + _ _ _ _ _ _ _))%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ + _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ + _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ + _ _ _)%expr_pat => None | _ => None end;; match x5 with @@ -3300,8 +3338,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args3); - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -3413,87 +3450,116 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x3 with | (@expr.Ident _ _ _ t3 idc3 @ x5 @ x4)%expr_pat => match x5 with - | @expr.App _ _ _ s5 _ (@expr.Ident _ _ _ t4 idc4) - x6 => + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.Ident + _ _ _ t7 idc7))%expr_pat => match x4 with - | @expr.Ident _ _ _ t5 idc5 => - args <- invert_bind_args idc5 + | @expr.Ident _ _ _ t8 idc8 => + args <- invert_bind_args idc8 Raw.ident.Literal; - args0 <- invert_bind_args idc4 + args0 <- invert_bind_args idc7 + Raw.ident.Literal; + args1 <- invert_bind_args idc6 + Raw.ident.Z_cast; + _ <- invert_bind_args idc5 Raw.ident.Z_land; + args3 <- invert_bind_args idc4 Raw.ident.Z_cast; _ <- invert_bind_args idc3 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc2 + args5 <- invert_bind_args idc2 Raw.ident.Literal; - args3 <- invert_bind_args idc1 + args6 <- invert_bind_args idc1 Raw.ident.Z_cast; - args4 <- invert_bind_args idc0 + args7 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; match pattern.type.unify_extracted_cps - ((ℤ -> ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args4) -> s5 -> (projT1 args)) -> - (projT1 args2))%ptype option - (fun x7 : option => x7) + ((ℤ -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> + (s8 -> (projT1 args0)) -> + (projT1 args)) -> (projT1 args5))%ptype + option (fun x10 : option => x10) with - | Some (_, (_, _), _)%zrange => + | Some (_, (_, _, _), _)%zrange => if type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args4) -> - s5 -> (projT1 args)) -> - (projT1 args2))%ptype + ((ℤ -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> + (s8 -> (projT1 args0)) -> + (projT1 args)) -> (projT1 args5))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args4); - v <- type.try_make_transport_cps s5 - ℤ; + ##(projT2 args7); + v <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args); + ##(projT2 args0); xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args2); - fv <- (x7 <- (let - '(r1, r2)%zrange := - range in - fun (s6 : Z) - (rshiftl ry : zrange) - (y : expr ℤ) - (offset xx : Z) => - if - (s6 =? 2 ^ Z.log2 s6) && - (ZRange.normalize ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s6 - 1])%zrange - then - Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_add - (Z.log2 s6) - offset)%expr @ - ((##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x7, _) := xv in - x7) args3 args0 - (v (Compile.reflect x6)) - (let (x7, _) := xv0 in - x7) - (let (x7, _) := xv1 in - x7); - Some (Base x7)); + ##(projT2 args); + xv2 <- ident.unify + pattern.ident.Literal + ##(projT2 args5); + fv <- (x10 <- (let + '(r1, r2)%zrange := + range in + fun (s9 : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask offset xx : Z) + => + if + (s9 =? 2 ^ Z.log2 s9) && + (ZRange.normalize ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s9 - 1])%zrange && + (mask =? + Z.ones + (Z.log2 s9 - + offset)) + then + Some + (#(Z_cast2 (r1, r2))%expr @ + (#(fancy_add + (Z.log2 s9) + offset)%expr @ + ((##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x10, _) := xv in + x10) args6 args3 + args1 + (v + (Compile.reflect x9)) + (let (x10, _) := + xv0 in + x10) + (let (x10, _) := + xv1 in + x10) + (let (x10, _) := + xv2 in + x10); + Some (Base x10)); Some (fv0 <-- fv; Base fv0)%under_lets else None @@ -3501,10 +3567,61 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s5 _ ($_)%expr _ | @expr.App _ _ - _ s5 _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ - _ s5 _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s5 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.Abs _ + _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.LetIn + _ _ _ _ _ _ _))%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ + _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ + _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ + _ _ _)%expr_pat => None | _ => None end;; match x5 with @@ -3545,8 +3662,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -3652,178 +3768,392 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | @expr.App _ _ _ s3 _ (@expr.Ident _ _ _ t2 idc2) x4 => match x4 with - | (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ @expr.Ident _ _ _ - t5 idc5)%expr_pat => - args <- invert_bind_args idc5 Raw.ident.Literal; - args0 <- invert_bind_args idc4 Raw.ident.Z_cast; + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ @expr.Ident _ _ _ t8 idc8)%expr_pat => + args <- invert_bind_args idc8 Raw.ident.Literal; + args0 <- invert_bind_args idc7 Raw.ident.Literal; + args1 <- invert_bind_args idc6 Raw.ident.Z_cast; + _ <- invert_bind_args idc5 Raw.ident.Z_land; + args3 <- invert_bind_args idc4 Raw.ident.Z_cast; _ <- invert_bind_args idc3 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc2 Raw.ident.Z_cast; - args3 <- invert_bind_args idc1 Raw.ident.Z_cast; - args4 <- invert_bind_args idc0 Raw.ident.Literal; + args5 <- invert_bind_args idc2 Raw.ident.Z_cast; + args6 <- invert_bind_args idc1 Raw.ident.Z_cast; + args7 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; match pattern.type.unify_extracted_cps - ((ℤ -> ℤ) -> ℤ -> ℤ)%ptype - (((projT1 args4) -> s2) -> s6 -> (projT1 args))%ptype - option (fun x8 : option => x8) + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> s2) -> + (s9 -> (projT1 args0)) -> (projT1 args))%ptype + option (fun x11 : option => x11) with - | Some (_, _, (_, _))%zrange => + | Some (_, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ -> ℤ)%ptype - (((projT1 args4) -> s2) -> - s6 -> (projT1 args))%ptype + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> s2) -> + (s9 -> (projT1 args0)) -> (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args4); + ##(projT2 args7); v <- type.try_make_transport_cps s2 ℤ; - v0 <- type.try_make_transport_cps s6 ℤ; + v0 <- type.try_make_transport_cps s9 ℤ; xv0 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (let - '(r1, r2)%zrange := range in - fun (s7 : Z) (rx : zrange) - (x8 : expr ℤ) - (rshiftl ry : zrange) - (y : expr ℤ) (offset : Z) => - if - (s7 =? 2 ^ Z.log2 s7) && - (ZRange.normalize ry << - ZRange.normalize - (ZRange.constant offset) <=? - ZRange.normalize rshiftl)%zrange && - (ZRange.normalize rshiftl <=? - r[0 ~> s7 - 1])%zrange - then - Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_add (Z.log2 s7) - offset)%expr @ - (#(Z_cast rx)%expr @ x8, - #(Z_cast ry)%expr @ y)))%expr_pat - else None) - (let (x8, _) := xv in x8) args3 - (v (Compile.reflect x3)) args2 - args0 (v0 (Compile.reflect x7)) - (let (x8, _) := xv0 in x8); - Some (Base x8)); + fv <- (x11 <- (let + '(r1, r2)%zrange := range in + fun (s10 : Z) (rx : zrange) + (x11 : expr ℤ) + (rshiftl rland ry : zrange) + (y : expr ℤ) + (mask offset : Z) => + if + (s10 =? 2 ^ Z.log2 s10) && + (ZRange.normalize rland << + ZRange.normalize + (ZRange.constant offset) <=? + ZRange.normalize rshiftl)%zrange && + (ZRange.normalize ry &' + ZRange.normalize + (ZRange.constant mask) <=? + ZRange.normalize rland)%zrange && + (ZRange.normalize rshiftl <=? + r[0 ~> s10 - 1])%zrange && + (mask =? + Z.ones (Z.log2 s10 - offset)) + then + Some + (#(Z_cast2 (r1, r2))%expr @ + (#(fancy_add (Z.log2 s10) + offset)%expr @ + (#(Z_cast rx)%expr @ x11, + #(Z_cast ry)%expr @ y)))%expr_pat + else None) + (let (x11, _) := xv in x11) + args6 (v (Compile.reflect x3)) + args5 args3 args1 + (v0 (Compile.reflect x10)) + (let (x11, _) := xv0 in x11) + (let (x11, _) := xv1 in x11); + Some (Base x11)); Some (fv0 <-- fv; Base fv0)%under_lets else None | None => None end - | (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ @expr.Abs _ _ _ _ _ + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ @expr.Abs _ _ _ _ _ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ (_ @ _))%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => + None + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ ($_)%expr)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Abs _ _ _ + _ _ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ (_ @ _))) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.LetIn _ _ + _ _ _ _ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + ($_)%expr _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Abs _ _ _ _ _ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (_ @ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.LetIn _ _ _ _ _ _ _) _ @ _)) @ _)%expr_pat => + None + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ _ @ + _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ _ + _ _ @ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ #(_)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ (_ @ _))%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ @expr.LetIn _ _ _ _ - _ _ _)%expr_pat => None - | (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - ($_)%expr _ @ _)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Abs _ _ _ _ _ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (_ @ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.LetIn _ _ _ _ _ _ _) _ @ _)%expr_pat => None + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ (#(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ _ _ + _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t3 idc3 @ #(_) @ _)%expr_pat | (@expr.Ident _ _ _ t3 idc3 @ ($_)%expr @ _)%expr_pat | (@expr.Ident _ _ _ t3 idc3 @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ (($_)%expr @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ (_ @ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t3 idc3 @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => None | _ => None end;; match x3 with - | (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ @expr.Ident _ _ _ - t5 idc5)%expr_pat => - args <- invert_bind_args idc5 Raw.ident.Literal; - args0 <- invert_bind_args idc4 Raw.ident.Z_cast; + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ @expr.Ident _ _ _ t8 idc8)%expr_pat => + args <- invert_bind_args idc8 Raw.ident.Literal; + args0 <- invert_bind_args idc7 Raw.ident.Literal; + args1 <- invert_bind_args idc6 Raw.ident.Z_cast; + _ <- invert_bind_args idc5 Raw.ident.Z_land; + args3 <- invert_bind_args idc4 Raw.ident.Z_cast; _ <- invert_bind_args idc3 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc2 Raw.ident.Z_cast; - args3 <- invert_bind_args idc1 Raw.ident.Z_cast; - args4 <- invert_bind_args idc0 Raw.ident.Literal; + args5 <- invert_bind_args idc2 Raw.ident.Z_cast; + args6 <- invert_bind_args idc1 Raw.ident.Z_cast; + args7 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_get_carry; match pattern.type.unify_extracted_cps - ((ℤ -> ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args4) -> s6 -> (projT1 args)) -> s3)%ptype - option (fun x8 : option => x8) + ((ℤ -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> + (s9 -> (projT1 args0)) -> (projT1 args)) -> + s3)%ptype option (fun x11 : option => x11) with - | Some (_, (_, _), _)%zrange => + | Some (_, (_, _, _), _)%zrange => if type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args4) -> s6 -> (projT1 args)) -> + ((ℤ -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> + (s9 -> (projT1 args0)) -> (projT1 args)) -> s3)%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args4); - v <- type.try_make_transport_cps s6 ℤ; + ##(projT2 args7); + v <- type.try_make_transport_cps s9 ℤ; xv0 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); v0 <- type.try_make_transport_cps s3 ℤ; - fv <- (x8 <- (let - '(r1, r2)%zrange := range in - fun (s7 : Z) - (rshiftl ry : zrange) - (y : expr ℤ) (offset : Z) - (rx : zrange) (x8 : expr ℤ) - => - if - (s7 =? 2 ^ Z.log2 s7) && - (ZRange.normalize ry << - ZRange.normalize - (ZRange.constant offset) <=? - ZRange.normalize rshiftl)%zrange && - (ZRange.normalize rshiftl <=? - r[0 ~> s7 - 1])%zrange - then - Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_add (Z.log2 s7) - offset)%expr @ - (#(Z_cast rx)%expr @ x8, - #(Z_cast ry)%expr @ y)))%expr_pat - else None) - (let (x8, _) := xv in x8) args3 - args0 (v (Compile.reflect x7)) - (let (x8, _) := xv0 in x8) - args2 (v0 (Compile.reflect x4)); - Some (Base x8)); + fv <- (x11 <- (let + '(r1, r2)%zrange := range in + fun (s10 : Z) + (rshiftl rland ry : zrange) + (y : expr ℤ) + (mask offset : Z) + (rx : zrange) (x11 : expr ℤ) + => + if + (s10 =? 2 ^ Z.log2 s10) && + (ZRange.normalize ry << + ZRange.normalize + (ZRange.constant offset) <=? + ZRange.normalize rshiftl)%zrange && + (ZRange.normalize ry &' + ZRange.normalize + (ZRange.constant mask) <=? + ZRange.normalize rland)%zrange && + (ZRange.normalize rshiftl <=? + r[0 ~> s10 - 1])%zrange && + (mask =? + Z.ones (Z.log2 s10 - offset)) + then + Some + (#(Z_cast2 (r1, r2))%expr @ + (#(fancy_add (Z.log2 s10) + offset)%expr @ + (#(Z_cast rx)%expr @ x11, + #(Z_cast ry)%expr @ y)))%expr_pat + else None) + (let (x11, _) := xv in x11) + args6 args3 args1 + (v (Compile.reflect x10)) + (let (x11, _) := xv0 in x11) + (let (x11, _) := xv1 in x11) + args5 + (v0 (Compile.reflect x4)); + Some (Base x11)); Some (fv0 <-- fv; Base fv0)%under_lets else None | None => None end - | (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ @expr.Abs _ _ _ _ _ + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ @expr.Abs _ _ _ _ _ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ (_ @ _))%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident _ _ + _ t7 idc7)) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => + None + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ ($_)%expr)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Abs _ _ _ + _ _ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ (_ @ _))) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.LetIn _ _ + _ _ _ _ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + ($_)%expr _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.Abs _ _ _ _ _ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (_ @ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 _ + (@expr.LetIn _ _ _ _ _ _ _) _ @ _)) @ _)%expr_pat => + None + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ _ @ + _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ _ + _ _ @ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ #(_)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ (_ @ _))%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t4 idc4) x7 @ @expr.LetIn _ _ _ _ - _ _ _)%expr_pat => None - | (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - ($_)%expr _ @ _)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.Abs _ _ _ _ _ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (_ @ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t3 idc3 @ @expr.App _ _ _ s6 _ - (@expr.LetIn _ _ _ _ _ _ _) _ @ _)%expr_pat => None + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ (#(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ _ _ + _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t3 idc3 @ #(_) @ _)%expr_pat | (@expr.Ident _ _ _ t3 idc3 @ ($_)%expr @ _)%expr_pat | (@expr.Ident _ _ _ t3 idc3 @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ (($_)%expr @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ (_ @ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t3 idc3 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t3 idc3 @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => None | _ => None @@ -4073,86 +4403,115 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x3 with | (@expr.Ident _ _ _ t3 idc3 @ x5 @ x4)%expr_pat => match x5 with - | @expr.App _ _ _ s5 _ (@expr.Ident _ _ _ t4 idc4) - x6 => + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.Ident + _ _ _ t7 idc7))%expr_pat => match x4 with - | @expr.Ident _ _ _ t5 idc5 => - args <- invert_bind_args idc5 + | @expr.Ident _ _ _ t8 idc8 => + args <- invert_bind_args idc8 Raw.ident.Literal; - args0 <- invert_bind_args idc4 + args0 <- invert_bind_args idc7 + Raw.ident.Literal; + args1 <- invert_bind_args idc6 + Raw.ident.Z_cast; + _ <- invert_bind_args idc5 Raw.ident.Z_land; + args3 <- invert_bind_args idc4 Raw.ident.Z_cast; _ <- invert_bind_args idc3 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc2 + args5 <- invert_bind_args idc2 Raw.ident.Z_cast; - args3 <- invert_bind_args idc1 + args6 <- invert_bind_args idc1 Raw.ident.Literal; - args4 <- invert_bind_args idc0 + args7 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_sub_get_borrow; match pattern.type.unify_extracted_cps - ((ℤ -> ℤ) -> ℤ -> ℤ)%ptype - (((projT1 args4) -> (projT1 args3)) -> - s5 -> (projT1 args))%ptype option - (fun x7 : option => x7) + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> (projT1 args6)) -> + (s8 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x10 : option => x10) with - | Some (_, _, (_, _))%zrange => + | Some (_, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ -> ℤ)%ptype - (((projT1 args4) -> (projT1 args3)) -> - s5 -> (projT1 args))%ptype + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> (projT1 args6)) -> + (s8 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args4); + ##(projT2 args7); xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args3); - v <- type.try_make_transport_cps s5 - ℤ; + ##(projT2 args6); + v <- type.try_make_transport_cps s8 ℤ; xv1 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv2 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x7 <- (let - '(r1, r2)%zrange := - range in - fun (s6 xx : Z) - (rshiftl ry : zrange) - (y : expr ℤ) - (offset : Z) => - if - (s6 =? 2 ^ Z.log2 s6) && - (ZRange.normalize ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s6 - 1])%zrange - then - Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_sub - (Z.log2 s6) - offset)%expr @ - ((##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x7, _) := xv in - x7) - (let (x7, _) := xv0 in - x7) args2 args0 - (v (Compile.reflect x6)) - (let (x7, _) := xv1 in - x7); - Some (Base x7)); + fv <- (x10 <- (let + '(r1, r2)%zrange := + range in + fun (s9 xx : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask offset : Z) => + if + (s9 =? 2 ^ Z.log2 s9) && + (ZRange.normalize ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s9 - 1])%zrange && + (ZRange.normalize ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s9 - + offset)) + then + Some + (#(Z_cast2 (r1, r2))%expr @ + (#(fancy_sub + (Z.log2 s9) + offset)%expr @ + ((##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x10, _) := xv in + x10) + (let (x10, _) := + xv0 in + x10) args5 args3 + args1 + (v + (Compile.reflect x9)) + (let (x10, _) := + xv1 in + x10) + (let (x10, _) := + xv2 in + x10); + Some (Base x10)); Some (fv0 <-- fv; Base fv0)%under_lets else None @@ -4160,10 +4519,61 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s5 _ ($_)%expr _ | @expr.App _ _ - _ s5 _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ - _ s5 _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s5 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.Abs _ + _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Ident _ _ _ t6 idc6) x9 @ @expr.LetIn + _ _ _ _ _ _ _))%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s8 + _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ + _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ + _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ + _ _ _)%expr_pat => None | _ => None end;; match x5 with @@ -4206,8 +4616,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args3); - v <- type.try_make_transport_cps s5 - ℤ; + v <- type.try_make_transport_cps s5 ℤ; xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -4366,89 +4775,117 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x4 with | (@expr.Ident _ _ _ t3 idc3 @ x6 @ x5)%expr_pat => match x6 with - | @expr.App _ _ _ s6 _ (@expr.Ident _ _ _ t4 idc4) - x7 => + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Ident + _ _ _ t7 idc7))%expr_pat => match x5 with - | @expr.Ident _ _ _ t5 idc5 => - args <- invert_bind_args idc5 + | @expr.Ident _ _ _ t8 idc8 => + args <- invert_bind_args idc8 Raw.ident.Literal; - args0 <- invert_bind_args idc4 + args0 <- invert_bind_args idc7 + Raw.ident.Literal; + args1 <- invert_bind_args idc6 + Raw.ident.Z_cast; + _ <- invert_bind_args idc5 Raw.ident.Z_land; + args3 <- invert_bind_args idc4 Raw.ident.Z_cast; _ <- invert_bind_args idc3 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc2 + args5 <- invert_bind_args idc2 Raw.ident.Z_cast; - args3 <- invert_bind_args idc1 + args6 <- invert_bind_args idc1 Raw.ident.Z_cast; - args4 <- invert_bind_args idc0 + args7 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_sub_get_borrow; match pattern.type.unify_extracted_cps - ((ℤ -> ℤ) -> ℤ -> ℤ)%ptype - (((projT1 args4) -> s2) -> - s6 -> (projT1 args))%ptype option - (fun x8 : option => x8) + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> s2) -> + (s9 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x11 : option => x11) with - | Some (_, _, (_, _))%zrange => + | Some (_, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ -> ℤ)%ptype - (((projT1 args4) -> s2) -> - s6 -> (projT1 args))%ptype + ((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + (((projT1 args7) -> s2) -> + (s9 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args4); - v <- type.try_make_transport_cps s2 - ℤ; - v0 <- type.try_make_transport_cps s6 - ℤ; + ##(projT2 args7); + v <- type.try_make_transport_cps s2 ℤ; + v0 <- type.try_make_transport_cps s9 ℤ; xv0 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv1 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (let - '(r1, r2)%zrange := - range in - fun (s7 : Z) - (rx : zrange) - (x8 : expr ℤ) - (rshiftl ry : zrange) - (y : expr ℤ) - (offset : Z) => - if - (s7 =? 2 ^ Z.log2 s7) && - (ZRange.normalize ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s7 - 1])%zrange - then - Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_sub - (Z.log2 s7) - offset)%expr @ - (#(Z_cast rx)%expr @ - x8, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x8, _) := xv in - x8) args3 - (v (Compile.reflect x3)) - args2 args0 - (v0 - (Compile.reflect x7)) - (let (x8, _) := xv0 in - x8); - Some (Base x8)); + fv <- (x11 <- (let + '(r1, r2)%zrange := + range in + fun (s10 : Z) + (rx : zrange) + (x11 : expr ℤ) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask offset : Z) => + if + (s10 =? + 2 ^ Z.log2 s10) && + (ZRange.normalize ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s10 - 1])%zrange && + (ZRange.normalize ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s10 - + offset)) + then + Some + (#(Z_cast2 (r1, r2))%expr @ + (#(fancy_sub + (Z.log2 s10) + offset)%expr @ + (#(Z_cast rx)%expr @ + x11, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x11, _) := xv in + x11) args6 + (v + (Compile.reflect x3)) + args5 args3 args1 + (v0 + (Compile.reflect + x10)) + (let (x11, _) := + xv0 in + x11) + (let (x11, _) := + xv1 in + x11); + Some (Base x11)); Some (fv0 <-- fv; Base fv0)%under_lets else None @@ -4456,10 +4893,61 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s6 _ ($_)%expr _ | @expr.App _ _ - _ s6 _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ - _ s6 _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s6 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ (@expr.Ident _ _ _ t6 idc6) x10 @ ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.Abs _ + _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ (@expr.Ident _ _ _ t6 idc6) x10 @ (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ (@expr.Ident _ _ _ t6 idc6) x10 @ @expr.LetIn + _ _ _ _ _ _ _))%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.App _ _ _ s9 + _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ + _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ + _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ + _ _ _)%expr_pat => None | _ => None end;; match x6 with @@ -4499,10 +4987,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s2 - ℤ; - v0 <- type.try_make_transport_cps s6 - ℤ; + v <- type.try_make_transport_cps s2 ℤ; + v0 <- type.try_make_transport_cps s6 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -4633,107 +5119,138 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x4 with | (@expr.Ident _ _ _ t4 idc4 @ x6 @ x5)%expr_pat => match x6 with - | @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t5 idc5) x7 => + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.Ident _ _ _ t8 idc8))%expr_pat => match x5 with - | @expr.Ident _ _ _ t6 idc6 => - args <- invert_bind_args idc6 + | @expr.Ident _ _ _ t9 idc9 => + args <- invert_bind_args idc9 Raw.ident.Literal; - args0 <- invert_bind_args idc5 + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 + Raw.ident.Z_cast; + _ <- invert_bind_args idc6 + Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 + args6 <- invert_bind_args idc2 Raw.ident.Literal; - args4 <- invert_bind_args idc1 + args7 <- invert_bind_args idc1 Raw.ident.Literal; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> (projT1 args4)) -> - (projT1 args3)) -> - s6 -> (projT1 args))%ptype option - (fun x8 : option => x8) + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> (projT1 args7)) -> + (projT1 args6)) -> + (s9 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x11 : option => x11) with - | Some (_, _, _, (_, _))%zrange => + | Some (_, _, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> - (projT1 args4)) -> - (projT1 args3)) -> - s6 -> (projT1 args))%ptype + (((ℤ -> ℤ) -> ℤ) -> + (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> + (projT1 args7)) -> + (projT1 args6)) -> + (s9 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); + ##(projT2 args8); xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args4); + ##(projT2 args7); xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args3); - v <- type.try_make_transport_cps s6 - ℤ; + ##(projT2 args6); + v <- type.try_make_transport_cps s9 ℤ; xv2 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv3 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (let - '(r1, r2)%zrange := - range in - fun (s7 cc xx : Z) - (rshiftl - ry : zrange) - (y : expr ℤ) - (offset : Z) => - if - (s7 =? - 2 ^ Z.log2 s7) && - (ZRange.normalize - ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s7 - 1])%zrange - then - Some - (#(Z_cast2 - (r1, r2))%expr @ - (#(fancy_addc - (Z.log2 s7) - offset)%expr @ - ((##cc)%expr, - (##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x8, _) := - xv in - x8) - (let (x8, _) := - xv0 in - x8) - (let (x8, _) := - xv1 in - x8) args2 args0 - (v - (Compile.reflect - x7)) - (let (x8, _) := - xv2 in - x8); - Some (Base x8)); + fv <- (x11 <- (let + '(r1, r2)%zrange := + range in + fun + (s10 cc xx : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask + offset : Z) => + if + (s10 =? + 2 ^ Z.log2 s10) && + (ZRange.normalize + ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s10 - 1])%zrange && + (ZRange.normalize + ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s10 - + offset)) + then + Some + (#(Z_cast2 + (r1, r2))%expr @ + (#(fancy_addc + (Z.log2 + s10) + offset)%expr @ + ((##cc)%expr, + (##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x11, _) := + xv in + x11) + (let (x11, _) := + xv0 in + x11) + (let (x11, _) := + xv1 in + x11) args5 args3 + args1 + (v + (Compile.reflect + x10)) + (let (x11, _) := + xv2 in + x11) + (let (x11, _) := + xv3 in + x11); + Some (Base x11)); Some (fv0 <-- fv; Base fv0)%under_lets @@ -4742,11 +5259,65 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s6 _ ($_)%expr _ | @expr.App - _ _ _ s6 _ (@expr.Abs _ _ _ _ _ _) _ | - @expr.App _ _ _ s6 _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s6 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ + _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ + _ _ _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t5 idc5 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ + _ _ _)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ + _ _ _ _ _)%expr_pat => None | _ => None end;; match x6 with @@ -4797,8 +5368,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv1 <- ident.unify pattern.ident.Literal ##(projT2 args3); - v <- type.try_make_transport_cps s6 - ℤ; + v <- type.try_make_transport_cps s6 ℤ; xv2 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -4932,108 +5502,136 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x4 with | (@expr.Ident _ _ _ t4 idc4 @ x6 @ x5)%expr_pat => match x6 with - | @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t5 idc5) x7 => + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.Ident _ _ _ t8 idc8))%expr_pat => match x5 with - | @expr.Ident _ _ _ t6 idc6 => - args <- invert_bind_args idc6 + | @expr.Ident _ _ _ t9 idc9 => + args <- invert_bind_args idc9 Raw.ident.Literal; - args0 <- invert_bind_args idc5 + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 + Raw.ident.Z_cast; + _ <- invert_bind_args idc6 + Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 + args5 <- invert_bind_args idc3 Raw.ident.Literal; - args3 <- invert_bind_args idc2 + args6 <- invert_bind_args idc2 Raw.ident.Z_cast; - args4 <- invert_bind_args idc1 + args7 <- invert_bind_args idc1 Raw.ident.Literal; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype - ((((projT1 args5) -> (projT1 args4)) -> - s6 -> (projT1 args)) -> - (projT1 args2))%ptype option - (fun x8 : option => x8) + (((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> (projT1 args7)) -> + (s9 -> (projT1 args0)) -> + (projT1 args)) -> (projT1 args5))%ptype + option (fun x11 : option => x11) with - | Some (_, _, (_, _), _)%zrange => + | Some (_, _, (_, _, _), _)%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype - ((((projT1 args5) -> - (projT1 args4)) -> - s6 -> (projT1 args)) -> - (projT1 args2))%ptype + (((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> + ℤ)%ptype + ((((projT1 args8) -> + (projT1 args7)) -> + (s9 -> (projT1 args0)) -> + (projT1 args)) -> + (projT1 args5))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); + ##(projT2 args8); xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args4); - v <- type.try_make_transport_cps s6 - ℤ; + ##(projT2 args7); + v <- type.try_make_transport_cps s9 ℤ; xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args); + ##(projT2 args0); xv2 <- ident.unify pattern.ident.Literal - ##(projT2 args2); - fv <- (x8 <- (let - '(r1, r2)%zrange := - range in - fun (s7 cc : Z) - (rshiftl - ry : zrange) - (y : expr ℤ) - (offset xx : Z) - => - if - (s7 =? - 2 ^ Z.log2 s7) && - (ZRange.normalize - ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s7 - 1])%zrange - then - Some - (#(Z_cast2 - (r1, r2))%expr @ - (#(fancy_addc - (Z.log2 s7) - offset)%expr @ - ((##cc)%expr, - (##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x8, _) := - xv in - x8) - (let (x8, _) := - xv0 in - x8) args3 args0 - (v - (Compile.reflect - x7)) - (let (x8, _) := - xv1 in - x8) - (let (x8, _) := - xv2 in - x8); - Some (Base x8)); + ##(projT2 args); + xv3 <- ident.unify + pattern.ident.Literal + ##(projT2 args5); + fv <- (x11 <- (let + '(r1, r2)%zrange := + range in + fun (s10 cc : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask offset + xx : Z) => + if + (s10 =? + 2 ^ Z.log2 s10) && + (ZRange.normalize + ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s10 - 1])%zrange && + (ZRange.normalize + ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s10 - + offset)) + then + Some + (#(Z_cast2 + (r1, r2))%expr @ + (#(fancy_addc + (Z.log2 + s10) + offset)%expr @ + ((##cc)%expr, + (##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x11, _) := + xv in + x11) + (let (x11, _) := + xv0 in + x11) args6 args3 + args1 + (v + (Compile.reflect + x10)) + (let (x11, _) := + xv1 in + x11) + (let (x11, _) := + xv2 in + x11) + (let (x11, _) := + xv3 in + x11); + Some (Base x11)); Some (fv0 <-- fv; Base fv0)%under_lets @@ -5042,11 +5640,65 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s6 _ ($_)%expr _ | @expr.App - _ _ _ s6 _ (@expr.Abs _ _ _ _ _ _) _ | - @expr.App _ _ _ s6 _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s6 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ + _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ + _ _ _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t5 idc5 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ + _ _ _)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ + _ _ _ _ _)%expr_pat => None | _ => None end;; match x6 with @@ -5094,8 +5746,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s6 - ℤ; + v <- type.try_make_transport_cps s6 ℤ; xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -5226,208 +5877,445 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | @expr.App _ _ _ s4 _ (@expr.Ident _ _ _ t3 idc3) x5 => match x5 with - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ @expr.Ident _ _ - _ t6 idc6)%expr_pat => - args <- invert_bind_args idc6 Raw.ident.Literal; - args0 <- invert_bind_args idc5 Raw.ident.Z_cast; + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.Ident _ _ + _ t9 idc9)%expr_pat => + args <- invert_bind_args idc9 Raw.ident.Literal; + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 Raw.ident.Z_cast; + _ <- invert_bind_args idc6 Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 Raw.ident.Z_cast; - args4 <- invert_bind_args idc1 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; + args6 <- invert_bind_args idc2 Raw.ident.Z_cast; + args7 <- invert_bind_args idc1 Raw.ident.Literal; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> (projT1 args4)) -> s3) -> - s7 -> (projT1 args))%ptype option - (fun x9 : option => x9) + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> (projT1 args7)) -> s3) -> + (s10 -> (projT1 args0)) -> (projT1 args))%ptype + option (fun x12 : option => x12) with - | Some (_, _, _, (_, _))%zrange => + | Some (_, _, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> (projT1 args4)) -> - s3) -> s7 -> (projT1 args))%ptype + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> (projT1 args7)) -> + s3) -> + (s10 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); + ##(projT2 args8); xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args4); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s7 - ℤ; + ##(projT2 args7); + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s10 ℤ; xv1 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv2 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x9 <- (let - '(r1, r2)%zrange := range in - fun (s8 cc : Z) - (rx : zrange) - (x9 : expr ℤ) - (rshiftl ry : zrange) - (y : expr ℤ) (offset : Z) - => - if - (s8 =? 2 ^ Z.log2 s8) && - (ZRange.normalize ry << - ZRange.normalize - (ZRange.constant offset) <=? - ZRange.normalize rshiftl)%zrange && - (ZRange.normalize rshiftl <=? - r[0 ~> s8 - 1])%zrange - then - Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_addc - (Z.log2 s8) offset)%expr @ - ((##cc)%expr, - #(Z_cast rx)%expr @ x9, - #(Z_cast ry)%expr @ y)))%expr_pat - else None) - (let (x9, _) := xv in x9) - (let (x9, _) := xv0 in x9) - args3 - (v (Compile.reflect x4)) - args2 args0 - (v0 (Compile.reflect x8)) - (let (x9, _) := xv1 in x9); - Some (Base x9)); + fv <- (x12 <- (let + '(r1, r2)%zrange := range + in + fun (s11 cc : Z) + (rx : zrange) + (x12 : expr ℤ) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask offset : Z) => + if + (s11 =? 2 ^ Z.log2 s11) && + (ZRange.normalize ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize rshiftl)%zrange && + (ZRange.normalize rshiftl <=? + r[0 ~> s11 - 1])%zrange && + (ZRange.normalize ry &' + ZRange.normalize + (ZRange.constant mask) <=? + ZRange.normalize rland)%zrange && + (mask =? + Z.ones + (Z.log2 s11 - offset)) + then + Some + (#(Z_cast2 (r1, r2))%expr @ + (#(fancy_addc + (Z.log2 s11) + offset)%expr @ + ((##cc)%expr, + #(Z_cast rx)%expr @ + x12, + #(Z_cast ry)%expr @ y)))%expr_pat + else None) + (let (x12, _) := xv in x12) + (let (x12, _) := xv0 in + x12) args6 + (v (Compile.reflect x4)) + args5 args3 args1 + (v0 (Compile.reflect x11)) + (let (x12, _) := xv1 in + x12) + (let (x12, _) := xv2 in + x12); + Some (Base x12)); Some (fv0 <-- fv; Base fv0)%under_lets else None | None => None end - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ @expr.Abs _ _ _ + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.Abs _ _ _ _ _ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ (_ @ _))%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ @expr.LetIn _ _ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ (_ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => None - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - ($_)%expr _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Abs _ _ _ _ _ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (_ @ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.LetIn _ _ _ _ _ _ _) _ @ _)%expr_pat => + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + ($_)%expr)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Abs _ _ _ _ _ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + (_ @ _))) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.LetIn _ _ _ _ _ _ _)) @ _)%expr_pat => + None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ ($_)%expr _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Abs _ _ _ _ _ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (_ @ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ _ + _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ _ + _ _ _ _ @ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ + _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ + _ _ _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t4 idc4 @ #(_) @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => None | _ => None end;; match x4 with - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ @expr.Ident _ _ - _ t6 idc6)%expr_pat => - args <- invert_bind_args idc6 Raw.ident.Literal; - args0 <- invert_bind_args idc5 Raw.ident.Z_cast; + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.Ident _ _ + _ t9 idc9)%expr_pat => + args <- invert_bind_args idc9 Raw.ident.Literal; + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 Raw.ident.Z_cast; + _ <- invert_bind_args idc6 Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 Raw.ident.Z_cast; - args4 <- invert_bind_args idc1 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; + args6 <- invert_bind_args idc2 Raw.ident.Z_cast; + args7 <- invert_bind_args idc1 Raw.ident.Literal; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype - ((((projT1 args5) -> (projT1 args4)) -> - s7 -> (projT1 args)) -> s4)%ptype option - (fun x9 : option => x9) + (((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> (projT1 args7)) -> + (s10 -> (projT1 args0)) -> (projT1 args)) -> + s4)%ptype option (fun x12 : option => x12) with - | Some (_, _, (_, _), _)%zrange => + | Some (_, _, (_, _, _), _)%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype - ((((projT1 args5) -> (projT1 args4)) -> - s7 -> (projT1 args)) -> s4)%ptype + (((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> (projT1 args7)) -> + (s10 -> (projT1 args0)) -> + (projT1 args)) -> s4)%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); + ##(projT2 args8); xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args4); - v <- type.try_make_transport_cps s7 - ℤ; + ##(projT2 args7); + v <- type.try_make_transport_cps s10 ℤ; xv1 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv2 <- ident.unify pattern.ident.Literal ##(projT2 args); - v0 <- type.try_make_transport_cps s4 - ℤ; - fv <- (x9 <- (let - '(r1, r2)%zrange := range in - fun (s8 cc : Z) - (rshiftl ry : zrange) - (y : expr ℤ) (offset : Z) - (rx : zrange) - (x9 : expr ℤ) => - if - (s8 =? 2 ^ Z.log2 s8) && - (ZRange.normalize ry << - ZRange.normalize - (ZRange.constant offset) <=? - ZRange.normalize rshiftl)%zrange && - (ZRange.normalize rshiftl <=? - r[0 ~> s8 - 1])%zrange - then - Some - (#(Z_cast2 (r1, r2))%expr @ - (#(fancy_addc - (Z.log2 s8) offset)%expr @ - ((##cc)%expr, - #(Z_cast rx)%expr @ x9, - #(Z_cast ry)%expr @ y)))%expr_pat - else None) - (let (x9, _) := xv in x9) - (let (x9, _) := xv0 in x9) - args3 args0 - (v (Compile.reflect x8)) - (let (x9, _) := xv1 in x9) - args2 - (v0 (Compile.reflect x5)); - Some (Base x9)); + v0 <- type.try_make_transport_cps s4 ℤ; + fv <- (x12 <- (let + '(r1, r2)%zrange := range + in + fun (s11 cc : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask offset : Z) + (rx : zrange) + (x12 : expr ℤ) => + if + (s11 =? 2 ^ Z.log2 s11) && + (ZRange.normalize ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize rshiftl)%zrange && + (ZRange.normalize rshiftl <=? + r[0 ~> s11 - 1])%zrange && + (ZRange.normalize ry &' + ZRange.normalize + (ZRange.constant mask) <=? + ZRange.normalize rland)%zrange && + (mask =? + Z.ones + (Z.log2 s11 - offset)) + then + Some + (#(Z_cast2 (r1, r2))%expr @ + (#(fancy_addc + (Z.log2 s11) + offset)%expr @ + ((##cc)%expr, + #(Z_cast rx)%expr @ + x12, + #(Z_cast ry)%expr @ y)))%expr_pat + else None) + (let (x12, _) := xv in x12) + (let (x12, _) := xv0 in + x12) args6 args3 args1 + (v (Compile.reflect x11)) + (let (x12, _) := xv1 in + x12) + (let (x12, _) := xv2 in + x12) args5 + (v0 (Compile.reflect x5)); + Some (Base x12)); Some (fv0 <-- fv; Base fv0)%under_lets else None | None => None end - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ @expr.Abs _ _ _ + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.Abs _ _ _ _ _ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ (_ @ _))%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 @ @expr.LetIn _ _ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ (_ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => None - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - ($_)%expr _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.Abs _ _ _ _ _ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (_ @ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s7 _ - (@expr.LetIn _ _ _ _ _ _ _) _ @ _)%expr_pat => + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + ($_)%expr)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Abs _ _ _ _ _ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + (_ @ _))) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.LetIn _ _ _ _ _ _ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ ($_)%expr _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Abs _ _ _ _ _ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (_ @ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _)) @ _)%expr_pat => + None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ _ + _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ _ + _ _ _ _ @ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ + _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ + _ _ _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t4 idc4 @ #(_) @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => None | _ => None @@ -5465,10 +6353,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args5); xv0 <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s7 - ℤ; + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s7 ℤ; xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x9 <- (let @@ -5570,12 +6456,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ##(projT2 args5); xv0 <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s7 - ℤ; + v <- type.try_make_transport_cps s7 ℤ; xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); - v0 <- type.try_make_transport_cps s4 - ℤ; + v0 <- type.try_make_transport_cps s4 ℤ; fv <- (x9 <- (let '(r1, r2)%zrange := range in fun (s8 cc : Z) @@ -5768,109 +6652,138 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x5 with | (@expr.Ident _ _ _ t4 idc4 @ x7 @ x6)%expr_pat => match x7 with - | @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 => + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8))%expr_pat => match x6 with - | @expr.Ident _ _ _ t6 idc6 => - args <- invert_bind_args idc6 + | @expr.Ident _ _ _ t9 idc9 => + args <- invert_bind_args idc9 Raw.ident.Literal; - args0 <- invert_bind_args idc5 + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 + Raw.ident.Z_cast; + _ <- invert_bind_args idc6 + Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 + args6 <- invert_bind_args idc2 Raw.ident.Literal; - args4 <- invert_bind_args idc1 + args7 <- invert_bind_args idc1 Raw.ident.Z_cast; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> s3) -> - (projT1 args3)) -> - s7 -> (projT1 args))%ptype option - (fun x9 : option => x9) + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> + (projT1 args6)) -> + (s10 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x12 : option => x12) with - | Some (_, _, _, (_, _))%zrange => + | Some (_, _, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> s3) -> - (projT1 args3)) -> - s7 -> (projT1 args))%ptype + (((ℤ -> ℤ) -> ℤ) -> + (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> + (projT1 args6)) -> + (s10 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; + ##(projT2 args8); + v <- type.try_make_transport_cps s3 ℤ; xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args3); - v0 <- type.try_make_transport_cps s7 - ℤ; + ##(projT2 args6); + v0 <- type.try_make_transport_cps s10 ℤ; xv1 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv2 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x9 <- (let - '(r1, r2)%zrange := - range in - fun (s8 : Z) - (rc : zrange) - (c : expr ℤ) - (xx : Z) - (rshiftl - ry : zrange) - (y : expr ℤ) - (offset : Z) => - if - (s8 =? - 2 ^ Z.log2 s8) && - (ZRange.normalize - ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s8 - 1])%zrange - then - Some - (#(Z_cast2 - (r1, r2))%expr @ - (#(fancy_addc - (Z.log2 s8) - offset)%expr @ - (#(Z_cast rc)%expr @ - c, - (##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x9, _) := - xv in - x9) args4 - (v - (Compile.reflect - x4)) - (let (x9, _) := - xv0 in - x9) args2 args0 - (v0 - (Compile.reflect - x8)) - (let (x9, _) := - xv1 in - x9); - Some (Base x9)); + fv <- (x12 <- (let + '(r1, r2)%zrange := + range in + fun (s11 : Z) + (rc : zrange) + (c : expr ℤ) + (xx : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask + offset : Z) => + if + (s11 =? + 2 ^ Z.log2 s11) && + (ZRange.normalize + ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s11 - 1])%zrange && + (ZRange.normalize + ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s11 - + offset)) + then + Some + (#(Z_cast2 + (r1, r2))%expr @ + (#(fancy_addc + (Z.log2 + s11) + offset)%expr @ + (#(Z_cast rc)%expr @ + c, + (##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x12, _) := + xv in + x12) args7 + (v + (Compile.reflect + x4)) + (let (x12, _) := + xv0 in + x12) args5 args3 + args1 + (v0 + (Compile.reflect + x11)) + (let (x12, _) := + xv1 in + x12) + (let (x12, _) := + xv2 in + x12); + Some (Base x12)); Some (fv0 <-- fv; Base fv0)%under_lets @@ -5879,11 +6792,65 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s7 _ ($_)%expr _ | @expr.App - _ _ _ s7 _ (@expr.Abs _ _ _ _ _ _) _ | - @expr.App _ _ _ s7 _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s7 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ + _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ + _ _ _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t5 idc5 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ + _ _ _)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ + _ _ _ _ _)%expr_pat => None | _ => None end;; match x7 with @@ -5927,13 +6894,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv <- ident.unify pattern.ident.Literal ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; + v <- type.try_make_transport_cps s3 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args3); - v0 <- type.try_make_transport_cps s7 - ℤ; + v0 <- type.try_make_transport_cps s7 ℤ; xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -6071,110 +7036,136 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x5 with | (@expr.Ident _ _ _ t4 idc4 @ x7 @ x6)%expr_pat => match x7 with - | @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 => + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8))%expr_pat => match x6 with - | @expr.Ident _ _ _ t6 idc6 => - args <- invert_bind_args idc6 + | @expr.Ident _ _ _ t9 idc9 => + args <- invert_bind_args idc9 Raw.ident.Literal; - args0 <- invert_bind_args idc5 + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 + Raw.ident.Z_cast; + _ <- invert_bind_args idc6 + Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 + args5 <- invert_bind_args idc3 Raw.ident.Literal; - args3 <- invert_bind_args idc2 + args6 <- invert_bind_args idc2 Raw.ident.Z_cast; - args4 <- invert_bind_args idc1 + args7 <- invert_bind_args idc1 Raw.ident.Z_cast; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype - ((((projT1 args5) -> s3) -> - s7 -> (projT1 args)) -> - (projT1 args2))%ptype option - (fun x9 : option => x9) + (((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> + (s10 -> (projT1 args0)) -> + (projT1 args)) -> (projT1 args5))%ptype + option (fun x12 : option => x12) with - | Some (_, _, (_, _), _)%zrange => + | Some (_, _, (_, _, _), _)%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype - ((((projT1 args5) -> s3) -> - s7 -> (projT1 args)) -> - (projT1 args2))%ptype + (((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> + ℤ)%ptype + ((((projT1 args8) -> s3) -> + (s10 -> (projT1 args0)) -> + (projT1 args)) -> + (projT1 args5))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s7 - ℤ; + ##(projT2 args8); + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s10 ℤ; xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args); + ##(projT2 args0); xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args2); - fv <- (x9 <- (let - '(r1, r2)%zrange := - range in - fun (s8 : Z) - (rc : zrange) - (c : expr ℤ) - (rshiftl - ry : zrange) - (y : expr ℤ) - (offset xx : Z) - => - if - (s8 =? - 2 ^ Z.log2 s8) && - (ZRange.normalize - ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s8 - 1])%zrange - then - Some - (#(Z_cast2 - (r1, r2))%expr @ - (#(fancy_addc - (Z.log2 s8) - offset)%expr @ - (#(Z_cast rc)%expr @ - c, - (##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x9, _) := - xv in - x9) args4 - (v - (Compile.reflect - x4)) args3 - args0 - (v0 - (Compile.reflect - x8)) - (let (x9, _) := - xv0 in - x9) - (let (x9, _) := - xv1 in - x9); - Some (Base x9)); + ##(projT2 args); + xv2 <- ident.unify + pattern.ident.Literal + ##(projT2 args5); + fv <- (x12 <- (let + '(r1, r2)%zrange := + range in + fun (s11 : Z) + (rc : zrange) + (c : expr ℤ) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask offset + xx : Z) => + if + (s11 =? + 2 ^ Z.log2 s11) && + (ZRange.normalize + ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s11 - 1])%zrange && + (ZRange.normalize + ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s11 - + offset)) + then + Some + (#(Z_cast2 + (r1, r2))%expr @ + (#(fancy_addc + (Z.log2 + s11) + offset)%expr @ + (#(Z_cast rc)%expr @ + c, + (##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x12, _) := + xv in + x12) args7 + (v + (Compile.reflect + x4)) args6 + args3 args1 + (v0 + (Compile.reflect + x11)) + (let (x12, _) := + xv0 in + x12) + (let (x12, _) := + xv1 in + x12) + (let (x12, _) := + xv2 in + x12); + Some (Base x12)); Some (fv0 <-- fv; Base fv0)%under_lets @@ -6183,11 +7174,65 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s7 _ ($_)%expr _ | @expr.App - _ _ _ s7 _ (@expr.Abs _ _ _ _ _ _) _ | - @expr.App _ _ _ s7 _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s7 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ + _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ + _ _ _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t5 idc5 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ + _ _ _)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ + _ _ _ _ _)%expr_pat => None | _ => None end;; match x7 with @@ -6231,10 +7276,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv <- ident.unify pattern.ident.Literal ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s7 - ℤ; + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s7 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -6369,222 +7412,448 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | @expr.App _ _ _ s5 _ (@expr.Ident _ _ _ t3 idc3) x6 => match x6 with - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ @expr.Ident _ _ - _ t6 idc6)%expr_pat => - args <- invert_bind_args idc6 Raw.ident.Literal; - args0 <- invert_bind_args idc5 Raw.ident.Z_cast; + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.Ident _ _ + _ t9 idc9)%expr_pat => + args <- invert_bind_args idc9 Raw.ident.Literal; + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 Raw.ident.Z_cast; + _ <- invert_bind_args idc6 Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 Raw.ident.Z_cast; - args4 <- invert_bind_args idc1 Raw.ident.Z_cast; - args5 <- invert_bind_args idc0 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; + args6 <- invert_bind_args idc2 Raw.ident.Z_cast; + args7 <- invert_bind_args idc1 Raw.ident.Z_cast; + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> s3) -> s4) -> - s8 -> (projT1 args))%ptype option - (fun x10 : option => x10) + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> s4) -> + (s11 -> (projT1 args0)) -> (projT1 args))%ptype + option (fun x13 : option => x13) with - | Some (_, _, _, (_, _))%zrange => + | Some (_, _, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> s3) -> s4) -> - s8 -> (projT1 args))%ptype + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> s4) -> + (s11 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s4 - ℤ; - v1 <- type.try_make_transport_cps s8 - ℤ; + ##(projT2 args8); + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s4 ℤ; + v1 <- type.try_make_transport_cps s11 ℤ; xv0 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); - fv <- (x10 <- (let + fv <- (x13 <- (let '(r1, r2)%zrange := range in - fun (s9 : Z) (rc : zrange) + fun (s12 : Z) + (rc : zrange) (c : expr ℤ) (rx : zrange) - (x10 : expr ℤ) - (rshiftl ry : zrange) + (x13 : expr ℤ) + (rshiftl rland + ry : zrange) (y : expr ℤ) - (offset : Z) => + (mask offset : Z) => if - (s9 =? 2 ^ Z.log2 s9) && + (s12 =? 2 ^ Z.log2 s12) && (ZRange.normalize ry << ZRange.normalize (ZRange.constant offset) <=? ZRange.normalize rshiftl)%zrange && + (ZRange.normalize ry &' + ZRange.normalize + (ZRange.constant mask) <=? + ZRange.normalize rland)%zrange && (ZRange.normalize rshiftl <=? - r[0 ~> s9 - 1])%zrange + r[0 ~> s12 - 1])%zrange && + (mask =? + Z.ones + (Z.log2 s12 - offset)) then Some (#(Z_cast2 (r1, r2))%expr @ (#(fancy_addc - (Z.log2 s9) + (Z.log2 s12) offset)%expr @ (#(Z_cast rc)%expr @ c, #(Z_cast rx)%expr @ - x10, + x13, #(Z_cast ry)%expr @ y)))%expr_pat else None) - (let (x10, _) := xv in x10) - args4 + (let (x13, _) := xv in x13) + args7 (v (Compile.reflect x4)) - args3 + args6 (v0 (Compile.reflect x5)) - args2 args0 - (v1 (Compile.reflect x9)) - (let (x10, _) := xv0 in - x10); - Some (Base x10)); + args5 args3 args1 + (v1 (Compile.reflect x12)) + (let (x13, _) := xv0 in + x13) + (let (x13, _) := xv1 in + x13); + Some (Base x13)); Some (fv0 <-- fv; Base fv0)%under_lets else None | None => None end - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ @expr.Abs _ _ _ + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.Abs _ _ _ _ _ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ (_ @ _))%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ @expr.LetIn _ _ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ (_ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => None - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - ($_)%expr _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Abs _ _ _ _ _ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (_ @ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.LetIn _ _ _ _ _ _ _) _ @ _)%expr_pat => + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + ($_)%expr)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Abs _ _ _ _ _ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + (_ @ _))) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.LetIn _ _ _ _ _ _ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ ($_)%expr _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Abs _ _ _ _ _ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (_ @ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _)) @ _)%expr_pat => + None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ _ + _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ _ + _ _ _ _ @ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ + _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ + _ _ _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t4 idc4 @ #(_) @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => None | _ => None end;; match x5 with - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ @expr.Ident _ _ - _ t6 idc6)%expr_pat => - args <- invert_bind_args idc6 Raw.ident.Literal; - args0 <- invert_bind_args idc5 Raw.ident.Z_cast; + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.Ident _ _ + _ t9 idc9)%expr_pat => + args <- invert_bind_args idc9 Raw.ident.Literal; + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 Raw.ident.Z_cast; + _ <- invert_bind_args idc6 Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 Raw.ident.Z_cast; - args4 <- invert_bind_args idc1 Raw.ident.Z_cast; - args5 <- invert_bind_args idc0 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; + args6 <- invert_bind_args idc2 Raw.ident.Z_cast; + args7 <- invert_bind_args idc1 Raw.ident.Z_cast; + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_add_with_get_carry; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype - ((((projT1 args5) -> s3) -> - s8 -> (projT1 args)) -> s5)%ptype option - (fun x10 : option => x10) + (((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> + (s11 -> (projT1 args0)) -> (projT1 args)) -> + s5)%ptype option (fun x13 : option => x13) with - | Some (_, _, (_, _), _)%zrange => + | Some (_, _, (_, _, _), _)%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype - ((((projT1 args5) -> s3) -> - s8 -> (projT1 args)) -> s5)%ptype + (((ℤ -> ℤ) -> (ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> + (s11 -> (projT1 args0)) -> + (projT1 args)) -> s5)%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s8 - ℤ; + ##(projT2 args8); + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s11 ℤ; xv0 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); - v1 <- type.try_make_transport_cps s5 - ℤ; - fv <- (x10 <- (let + v1 <- type.try_make_transport_cps s5 ℤ; + fv <- (x13 <- (let '(r1, r2)%zrange := range in - fun (s9 : Z) (rc : zrange) + fun (s12 : Z) + (rc : zrange) (c : expr ℤ) - (rshiftl ry : zrange) + (rshiftl rland + ry : zrange) (y : expr ℤ) - (offset : Z) + (mask offset : Z) (rx : zrange) - (x10 : expr ℤ) => + (x13 : expr ℤ) => if - (s9 =? 2 ^ Z.log2 s9) && + (s12 =? 2 ^ Z.log2 s12) && (ZRange.normalize ry << ZRange.normalize (ZRange.constant offset) <=? ZRange.normalize rshiftl)%zrange && (ZRange.normalize rshiftl <=? - r[0 ~> s9 - 1])%zrange + r[0 ~> s12 - 1])%zrange && + (ZRange.normalize ry &' + ZRange.normalize + (ZRange.constant mask) <=? + ZRange.normalize rland)%zrange && + (mask =? + Z.ones + (Z.log2 s12 - offset)) then Some (#(Z_cast2 (r1, r2))%expr @ (#(fancy_addc - (Z.log2 s9) + (Z.log2 s12) offset)%expr @ (#(Z_cast rc)%expr @ c, #(Z_cast rx)%expr @ - x10, + x13, #(Z_cast ry)%expr @ y)))%expr_pat else None) - (let (x10, _) := xv in x10) - args4 + (let (x13, _) := xv in x13) + args7 (v (Compile.reflect x4)) - args3 args0 - (v0 (Compile.reflect x9)) - (let (x10, _) := xv0 in - x10) args2 + args6 args3 args1 + (v0 (Compile.reflect x12)) + (let (x13, _) := xv0 in + x13) + (let (x13, _) := xv1 in + x13) args5 (v1 (Compile.reflect x6)); - Some (Base x10)); + Some (Base x13)); Some (fv0 <-- fv; Base fv0)%under_lets else None | None => None end - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ @expr.Abs _ _ _ + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.Abs _ _ _ _ _ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ (_ @ _))%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 @ @expr.LetIn _ _ + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ (_ @ _))%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8)) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => None - | (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - ($_)%expr _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.Abs _ _ _ _ _ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (_ @ _) _ @ _)%expr_pat | - (@expr.Ident _ _ _ t4 idc4 @ @expr.App _ _ _ s8 _ - (@expr.LetIn _ _ _ _ _ _ _) _ @ _)%expr_pat => + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + ($_)%expr)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Abs _ _ _ _ _ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + (_ @ _))) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.LetIn _ _ _ _ _ _ _)) @ _)%expr_pat => + None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ ($_)%expr _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Abs _ _ _ _ _ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (_ @ _) _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ _ + _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ _ + _ _ _ _ @ _)) @ _)%expr_pat => None + | (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ #(_)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ _ _ + _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _)) @ + _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _)) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ _ _ + _ _ _) @ _)%expr_pat => None | (@expr.Ident _ _ _ t4 idc4 @ #(_) @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ ($_)%expr @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (($_)%expr @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ (_ @ _ @ _) @ _)%expr_pat | + (@expr.Ident _ _ _ t4 idc4 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | (@expr.Ident _ _ _ t4 idc4 @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => None | _ => None @@ -6619,12 +7888,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s4 - ℤ; - v1 <- type.try_make_transport_cps s8 - ℤ; + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s4 ℤ; + v1 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (x10 <- (let @@ -6730,14 +7996,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s8 - ℤ; + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - v1 <- type.try_make_transport_cps s5 - ℤ; + v1 <- type.try_make_transport_cps s5 ℤ; fv <- (x10 <- (let '(r1, r2)%zrange := range in @@ -6893,107 +8156,138 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x4 with | (@expr.Ident _ _ _ t4 idc4 @ x6 @ x5)%expr_pat => match x6 with - | @expr.App _ _ _ s6 _ - (@expr.Ident _ _ _ t5 idc5) x7 => + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.Ident _ _ _ t8 idc8))%expr_pat => match x5 with - | @expr.Ident _ _ _ t6 idc6 => - args <- invert_bind_args idc6 + | @expr.Ident _ _ _ t9 idc9 => + args <- invert_bind_args idc9 Raw.ident.Literal; - args0 <- invert_bind_args idc5 + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 + Raw.ident.Z_cast; + _ <- invert_bind_args idc6 + Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 + args6 <- invert_bind_args idc2 Raw.ident.Literal; - args4 <- invert_bind_args idc1 + args7 <- invert_bind_args idc1 Raw.ident.Literal; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_sub_with_get_borrow; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> (projT1 args4)) -> - (projT1 args3)) -> - s6 -> (projT1 args))%ptype option - (fun x8 : option => x8) + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> (projT1 args7)) -> + (projT1 args6)) -> + (s9 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x11 : option => x11) with - | Some (_, _, _, (_, _))%zrange => + | Some (_, _, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> - (projT1 args4)) -> - (projT1 args3)) -> - s6 -> (projT1 args))%ptype + (((ℤ -> ℤ) -> ℤ) -> + (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> + (projT1 args7)) -> + (projT1 args6)) -> + (s9 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); + ##(projT2 args8); xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args4); + ##(projT2 args7); xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args3); - v <- type.try_make_transport_cps s6 - ℤ; + ##(projT2 args6); + v <- type.try_make_transport_cps s9 ℤ; xv2 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv3 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x8 <- (let - '(r1, r2)%zrange := - range in - fun (s7 bb xx : Z) - (rshiftl - ry : zrange) - (y : expr ℤ) - (offset : Z) => - if - (s7 =? - 2 ^ Z.log2 s7) && - (ZRange.normalize - ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s7 - 1])%zrange - then - Some - (#(Z_cast2 - (r1, r2))%expr @ - (#(fancy_subb - (Z.log2 s7) - offset)%expr @ - ((##bb)%expr, - (##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x8, _) := - xv in - x8) - (let (x8, _) := - xv0 in - x8) - (let (x8, _) := - xv1 in - x8) args2 args0 - (v - (Compile.reflect - x7)) - (let (x8, _) := - xv2 in - x8); - Some (Base x8)); + fv <- (x11 <- (let + '(r1, r2)%zrange := + range in + fun + (s10 bb xx : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask + offset : Z) => + if + (s10 =? + 2 ^ Z.log2 s10) && + (ZRange.normalize + ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s10 - 1])%zrange && + (ZRange.normalize + ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s10 - + offset)) + then + Some + (#(Z_cast2 + (r1, r2))%expr @ + (#(fancy_subb + (Z.log2 + s10) + offset)%expr @ + ((##bb)%expr, + (##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x11, _) := + xv in + x11) + (let (x11, _) := + xv0 in + x11) + (let (x11, _) := + xv1 in + x11) args5 args3 + args1 + (v + (Compile.reflect + x10)) + (let (x11, _) := + xv2 in + x11) + (let (x11, _) := + xv3 in + x11); + Some (Base x11)); Some (fv0 <-- fv; Base fv0)%under_lets @@ -7002,11 +8296,65 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s6 _ ($_)%expr _ | @expr.App - _ _ _ s6 _ (@expr.Abs _ _ _ _ _ _) _ | - @expr.App _ _ _ s6 _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s6 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Ident _ _ _ t7 idc7) x10 @ + @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s9 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ + _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ + _ _ _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t5 idc5 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ + _ _ _)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ + _ _ _ _ _)%expr_pat => None | _ => None end;; match x6 with @@ -7057,8 +8405,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv1 <- ident.unify pattern.ident.Literal ##(projT2 args3); - v <- type.try_make_transport_cps s6 - ℤ; + v <- type.try_make_transport_cps s6 ℤ; xv2 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -7248,108 +8595,137 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x5 with | (@expr.Ident _ _ _ t4 idc4 @ x7 @ x6)%expr_pat => match x7 with - | @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 => + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8))%expr_pat => match x6 with - | @expr.Ident _ _ _ t6 idc6 => - args <- invert_bind_args idc6 + | @expr.Ident _ _ _ t9 idc9 => + args <- invert_bind_args idc9 Raw.ident.Literal; - args0 <- invert_bind_args idc5 + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 + Raw.ident.Z_cast; + _ <- invert_bind_args idc6 + Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 + args6 <- invert_bind_args idc2 Raw.ident.Z_cast; - args4 <- invert_bind_args idc1 + args7 <- invert_bind_args idc1 Raw.ident.Literal; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_sub_with_get_borrow; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> (projT1 args4)) -> - s3) -> s7 -> (projT1 args))%ptype - option (fun x9 : option => x9) + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> (projT1 args7)) -> + s3) -> + (s10 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x12 : option => x12) with - | Some (_, _, _, (_, _))%zrange => + | Some (_, _, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> - (projT1 args4)) -> s3) -> - s7 -> (projT1 args))%ptype + (((ℤ -> ℤ) -> ℤ) -> + (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> + (projT1 args7)) -> s3) -> + (s10 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); + ##(projT2 args8); xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args4); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s7 - ℤ; + ##(projT2 args7); + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s10 ℤ; xv1 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv2 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x9 <- (let - '(r1, r2)%zrange := - range in - fun (s8 bb : Z) - (rx : zrange) - (x9 : expr ℤ) - (rshiftl - ry : zrange) - (y : expr ℤ) - (offset : Z) => - if - (s8 =? - 2 ^ Z.log2 s8) && - (ZRange.normalize - ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s8 - 1])%zrange - then - Some - (#(Z_cast2 - (r1, r2))%expr @ - (#(fancy_subb - (Z.log2 s8) - offset)%expr @ - ((##bb)%expr, - #(Z_cast rx)%expr @ - x9, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x9, _) := - xv in - x9) - (let (x9, _) := - xv0 in - x9) args3 - (v - (Compile.reflect - x4)) args2 - args0 - (v0 - (Compile.reflect - x8)) - (let (x9, _) := - xv1 in - x9); - Some (Base x9)); + fv <- (x12 <- (let + '(r1, r2)%zrange := + range in + fun (s11 bb : Z) + (rx : zrange) + (x12 : expr ℤ) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask + offset : Z) => + if + (s11 =? + 2 ^ Z.log2 s11) && + (ZRange.normalize + ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s11 - 1])%zrange && + (ZRange.normalize + ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s11 - + offset)) + then + Some + (#(Z_cast2 + (r1, r2))%expr @ + (#(fancy_subb + (Z.log2 + s11) + offset)%expr @ + ((##bb)%expr, + #(Z_cast rx)%expr @ + x12, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x12, _) := + xv in + x12) + (let (x12, _) := + xv0 in + x12) args6 + (v + (Compile.reflect + x4)) args5 + args3 args1 + (v0 + (Compile.reflect + x11)) + (let (x12, _) := + xv1 in + x12) + (let (x12, _) := + xv2 in + x12); + Some (Base x12)); Some (fv0 <-- fv; Base fv0)%under_lets @@ -7358,11 +8734,65 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s7 _ ($_)%expr _ | @expr.App - _ _ _ s7 _ (@expr.Abs _ _ _ _ _ _) _ | - @expr.App _ _ _ s7 _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s7 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ + _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ + _ _ _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t5 idc5 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ + _ _ _)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ + _ _ _ _ _)%expr_pat => None | _ => None end;; match x7 with @@ -7408,10 +8838,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 <- ident.unify pattern.ident.Literal ##(projT2 args4); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s7 - ℤ; + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s7 ℤ; xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -7612,109 +9040,138 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x5 with | (@expr.Ident _ _ _ t4 idc4 @ x7 @ x6)%expr_pat => match x7 with - | @expr.App _ _ _ s7 _ - (@expr.Ident _ _ _ t5 idc5) x8 => + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Ident _ _ _ t8 idc8))%expr_pat => match x6 with - | @expr.Ident _ _ _ t6 idc6 => - args <- invert_bind_args idc6 + | @expr.Ident _ _ _ t9 idc9 => + args <- invert_bind_args idc9 Raw.ident.Literal; - args0 <- invert_bind_args idc5 + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 + Raw.ident.Z_cast; + _ <- invert_bind_args idc6 + Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 + args6 <- invert_bind_args idc2 Raw.ident.Literal; - args4 <- invert_bind_args idc1 + args7 <- invert_bind_args idc1 Raw.ident.Z_cast; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_sub_with_get_borrow; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> s3) -> - (projT1 args3)) -> - s7 -> (projT1 args))%ptype option - (fun x9 : option => x9) + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> + (projT1 args6)) -> + (s10 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x12 : option => x12) with - | Some (_, _, _, (_, _))%zrange => + | Some (_, _, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> s3) -> - (projT1 args3)) -> - s7 -> (projT1 args))%ptype + (((ℤ -> ℤ) -> ℤ) -> + (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> + (projT1 args6)) -> + (s10 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; + ##(projT2 args8); + v <- type.try_make_transport_cps s3 ℤ; xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args3); - v0 <- type.try_make_transport_cps s7 - ℤ; + ##(projT2 args6); + v0 <- type.try_make_transport_cps s10 ℤ; xv1 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv2 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x9 <- (let - '(r1, r2)%zrange := - range in - fun (s8 : Z) - (rb : zrange) - (b3 : expr ℤ) - (xx : Z) - (rshiftl - ry : zrange) - (y : expr ℤ) - (offset : Z) => - if - (s8 =? - 2 ^ Z.log2 s8) && - (ZRange.normalize - ry << - ZRange.normalize - (ZRange.constant - offset) <=? - ZRange.normalize - rshiftl)%zrange && - (ZRange.normalize - rshiftl <=? - r[0 ~> s8 - 1])%zrange - then - Some - (#(Z_cast2 - (r1, r2))%expr @ - (#(fancy_subb - (Z.log2 s8) - offset)%expr @ - (#(Z_cast rb)%expr @ - b3, - (##xx)%expr, - #(Z_cast ry)%expr @ - y)))%expr_pat - else None) - (let (x9, _) := - xv in - x9) args4 - (v - (Compile.reflect - x4)) - (let (x9, _) := - xv0 in - x9) args2 args0 - (v0 - (Compile.reflect - x8)) - (let (x9, _) := - xv1 in - x9); - Some (Base x9)); + fv <- (x12 <- (let + '(r1, r2)%zrange := + range in + fun (s11 : Z) + (rb : zrange) + (b4 : expr ℤ) + (xx : Z) + (rshiftl rland + ry : zrange) + (y : expr ℤ) + (mask + offset : Z) => + if + (s11 =? + 2 ^ Z.log2 s11) && + (ZRange.normalize + ry << + ZRange.normalize + (ZRange.constant + offset) <=? + ZRange.normalize + rshiftl)%zrange && + (ZRange.normalize + rshiftl <=? + r[0 ~> s11 - 1])%zrange && + (ZRange.normalize + ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s11 - + offset)) + then + Some + (#(Z_cast2 + (r1, r2))%expr @ + (#(fancy_subb + (Z.log2 + s11) + offset)%expr @ + (#(Z_cast rb)%expr @ + b4, + (##xx)%expr, + #(Z_cast ry)%expr @ + y)))%expr_pat + else None) + (let (x12, _) := + xv in + x12) args7 + (v + (Compile.reflect + x4)) + (let (x12, _) := + xv0 in + x12) args5 args3 + args1 + (v0 + (Compile.reflect + x11)) + (let (x12, _) := + xv1 in + x12) + (let (x12, _) := + xv2 in + x12); + Some (Base x12)); Some (fv0 <-- fv; Base fv0)%under_lets @@ -7723,11 +9180,65 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s7 _ ($_)%expr _ | @expr.App - _ _ _ s7 _ (@expr.Abs _ _ _ _ _ _) _ | - @expr.App _ _ _ s7 _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s7 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Ident _ _ _ t7 idc7) x11 @ + @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s10 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ + _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ + _ _ _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t5 idc5 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ + _ _ _)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ + _ _ _ _ _)%expr_pat => None | _ => None end;; match x7 with @@ -7771,13 +9282,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv <- ident.unify pattern.ident.Literal ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; + v <- type.try_make_transport_cps s3 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args3); - v0 <- type.try_make_transport_cps s7 - ℤ; + v0 <- type.try_make_transport_cps s7 ℤ; xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); @@ -7971,68 +9480,80 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with match x6 with | (@expr.Ident _ _ _ t4 idc4 @ x8 @ x7)%expr_pat => match x8 with - | @expr.App _ _ _ s8 _ - (@expr.Ident _ _ _ t5 idc5) x9 => + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Ident _ _ _ t8 idc8))%expr_pat => match x7 with - | @expr.Ident _ _ _ t6 idc6 => - args <- invert_bind_args idc6 + | @expr.Ident _ _ _ t9 idc9 => + args <- invert_bind_args idc9 Raw.ident.Literal; - args0 <- invert_bind_args idc5 + args0 <- invert_bind_args idc8 + Raw.ident.Literal; + args1 <- invert_bind_args idc7 + Raw.ident.Z_cast; + _ <- invert_bind_args idc6 + Raw.ident.Z_land; + args3 <- invert_bind_args idc5 Raw.ident.Z_cast; _ <- invert_bind_args idc4 Raw.ident.Z_shiftl; - args2 <- invert_bind_args idc3 + args5 <- invert_bind_args idc3 Raw.ident.Z_cast; - args3 <- invert_bind_args idc2 + args6 <- invert_bind_args idc2 Raw.ident.Z_cast; - args4 <- invert_bind_args idc1 + args7 <- invert_bind_args idc1 Raw.ident.Z_cast; - args5 <- invert_bind_args idc0 + args8 <- invert_bind_args idc0 Raw.ident.Literal; _ <- invert_bind_args idc Raw.ident.Z_sub_with_get_borrow; match pattern.type.unify_extracted_cps - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> s3) -> s4) -> - s8 -> (projT1 args))%ptype option - (fun x10 : option => x10) + (((ℤ -> ℤ) -> ℤ) -> (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> s4) -> + (s11 -> (projT1 args0)) -> + (projT1 args))%ptype option + (fun x13 : option => x13) with - | Some (_, _, _, (_, _))%zrange => + | Some (_, _, _, (_, _, _))%zrange => if type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype - ((((projT1 args5) -> s3) -> s4) -> - s8 -> (projT1 args))%ptype + (((ℤ -> ℤ) -> ℤ) -> + (ℤ -> ℤ) -> ℤ)%ptype + ((((projT1 args8) -> s3) -> s4) -> + (s11 -> (projT1 args0)) -> + (projT1 args))%ptype then xv <- ident.unify pattern.ident.Literal - ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s4 - ℤ; - v1 <- type.try_make_transport_cps s8 - ℤ; + ##(projT2 args8); + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s4 ℤ; + v1 <- type.try_make_transport_cps s11 ℤ; xv0 <- ident.unify pattern.ident.Literal + ##(projT2 args0); + xv1 <- ident.unify + pattern.ident.Literal ##(projT2 args); - fv <- (x10 <- (let + fv <- (x13 <- (let '(r1, r2)%zrange := range in - fun (s9 : Z) + fun (s12 : Z) (rb : zrange) - (b3 : expr ℤ) + (b4 : expr ℤ) (rx : zrange) - (x10 : expr ℤ) - (rshiftl + (x13 : expr ℤ) + (rshiftl rland ry : zrange) (y : expr ℤ) - (offset : Z) => + (mask + offset : Z) => if - (s9 =? - 2 ^ Z.log2 s9) && + (s12 =? + 2 ^ Z.log2 s12) && (ZRange.normalize ry << ZRange.normalize @@ -8042,39 +9563,53 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with rshiftl)%zrange && (ZRange.normalize rshiftl <=? - r[0 ~> s9 - 1])%zrange + r[0 ~> s12 - 1])%zrange && + (ZRange.normalize + ry &' + ZRange.normalize + (ZRange.constant + mask) <=? + ZRange.normalize + rland)%zrange && + (mask =? + Z.ones + (Z.log2 s12 - + offset)) then Some (#(Z_cast2 (r1, r2))%expr @ (#(fancy_subb (Z.log2 - s9) + s12) offset)%expr @ (#(Z_cast rb)%expr @ - b3, + b4, #(Z_cast rx)%expr @ - x10, + x13, #(Z_cast ry)%expr @ y)))%expr_pat else None) - (let (x10, _) := + (let (x13, _) := xv in - x10) args4 + x13) args7 (v (Compile.reflect - x4)) args3 + x4)) args6 (v0 (Compile.reflect - x5)) args2 - args0 + x5)) args5 + args3 args1 (v1 (Compile.reflect - x9)) - (let (x10, _) := + x12)) + (let (x13, _) := xv0 in - x10); - Some (Base x10)); + x13) + (let (x13, _) := + xv1 in + x13); + Some (Base x13)); Some (fv0 <-- fv; Base fv0)%under_lets @@ -8083,11 +9618,65 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with end | _ => None end - | @expr.App _ _ _ s8 _ ($_)%expr _ | @expr.App - _ _ _ s8 _ (@expr.Abs _ _ _ _ _ _) _ | - @expr.App _ _ _ s8 _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s8 _ - (@expr.LetIn _ _ _ _ _ _ _) _ => None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + ($_)%expr))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.Abs _ _ _ _ _ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + (_ @ _)))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Ident _ _ _ t7 idc7) x12 @ + @expr.LetIn _ _ _ _ _ _ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ ($_)%expr _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.Abs _ _ _ _ _ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (_ @ _) _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.App _ _ _ + s11 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _))%expr_pat => + None + | (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ #(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ ($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.Abs _ _ _ + _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Ident _ _ _ t6 idc6 @ @expr.LetIn _ _ + _ _ _ _ _ @ _))%expr_pat => None + | (@expr.Ident _ _ _ t5 idc5 @ #(_))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ ($_)%expr)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.Abs _ _ _ + _ _ _)%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (#(_) @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (($_)%expr @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (($_)%expr @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.Abs _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ (_ @ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ + (@expr.LetIn _ _ _ _ _ _ _ @ _))%expr_pat | + (@expr.Ident _ _ _ t5 idc5 @ @expr.LetIn _ _ + _ _ _ _ _)%expr_pat => None | _ => None end;; match x8 with @@ -8129,12 +9718,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv <- ident.unify pattern.ident.Literal ##(projT2 args5); - v <- type.try_make_transport_cps s3 - ℤ; - v0 <- type.try_make_transport_cps s4 - ℤ; - v1 <- type.try_make_transport_cps s8 - ℤ; + v <- type.try_make_transport_cps s3 ℤ; + v0 <- type.try_make_transport_cps s4 ℤ; + v1 <- type.try_make_transport_cps s8 ℤ; xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); |