Insert casts before literals during bounds analysis

Unless we explicitly say not to.  The ability to explicitly say not to
is required for, e.g., eta-expansion where we want to replace variable
lists of known length with with cons cells indexing into the variable
list, but don't want to pollute the code with casts.

Uniformity in this way allows rewrite rules to not blow up exponentially
(in the number of wildcards); we previously required a separate rewrite
rule for each way of choosing between wildcard and literal.

To preserve output of the pipeline, we add another pass that just strips
the casts off of literals at the end.

After     | File Name                                    | Before    || Change    | % Change
--------------------------------------------------------------------------------------------
20m27.24s | Total                                        | 22m39.70s || -2m12.46s | -9.74%
--------------------------------------------------------------------------------------------
0m44.27s  | Rewriter.vo                                  | 2m11.58s  || -1m27.31s | -66.35%
1m15.23s  | RewriterRulesInterpGood.vo                   | 1m50.28s  || -0m35.04s | -31.78%
1m40.19s  | RewriterRulesGood.vo                         | 1m58.05s  || -0m17.85s | -15.12%
0m26.99s  | AbstractInterpretationProofs.vo              | 0m16.91s  || +0m10.07s | +59.60%
3m15.98s  | p384_32.c                                    | 3m07.78s  || +0m08.19s | +4.36%
0m42.52s  | ExtractionHaskell/word_by_word_montgomery    | 0m44.60s  || -0m02.07s | -4.66%
0m28.63s  | ExtractionHaskell/unsaturated_solinas        | 0m31.38s  || -0m02.75s | -8.76%
0m21.76s  | ExtractionHaskell/saturated_solinas          | 0m24.56s  || -0m02.79s | -11.40%
0m09.87s  | ExtractionOCaml/unsaturated_solinas          | 0m11.28s  || -0m01.41s | -12.50%
1m59.22s  | RewriterWf2.vo                               | 2m00.09s  || -0m00.87s | -0.72%
1m07.03s  | Fancy/Montgomery256.vo                       | 1m07.31s  || -0m00.28s | -0.41%
0m52.60s  | Fancy/Barrett256.vo                          | 0m53.16s  || -0m00.55s | -1.05%
0m48.17s  | RewriterInterpProofs1.vo                     | 0m48.72s  || -0m00.54s | -1.12%
0m40.16s  | AbstractInterpretationWf.vo                  | 0m40.23s  || -0m00.07s | -0.17%
0m38.35s  | p521_32.c                                    | 0m38.26s  || +0m00.09s | +0.23%
0m31.56s  | p521_64.c                                    | 0m31.53s  || +0m00.02s | +0.09%
0m24.64s  | RewriterWf1.vo                               | 0m24.01s  || +0m00.62s | +2.62%
0m23.54s  | AbstractInterpretationZRangeProofs.vo        | 0m23.64s  || -0m00.10s | -0.42%
0m23.48s  | PushButtonSynthesis/WordByWordMontgomery.vo  | 0m23.26s  || +0m00.21s | +0.94%
0m20.92s  | SlowPrimeSynthesisExamples.vo                | 0m20.62s  || +0m00.30s | +1.45%
0m19.92s  | PushButtonSynthesis/UnsaturatedSolinas.vo    | 0m19.80s  || +0m00.12s | +0.60%
0m16.60s  | ExtractionOCaml/word_by_word_montgomery      | 0m17.56s  || -0m00.95s | -5.46%
0m14.72s  | p448_solinas_64.c                            | 0m14.66s  || +0m00.06s | +0.40%
0m13.70s  | secp256k1_32.c                               | 0m13.45s  || +0m00.25s | +1.85%
0m13.68s  | p256_32.c                                    | 0m13.33s  || +0m00.34s | +2.62%
0m13.28s  | CStringification.vo                          | 0m13.26s  || +0m00.01s | +0.15%
0m11.88s  | p484_64.c                                    | 0m11.74s  || +0m00.14s | +1.19%
0m09.96s  | ExtractionOCaml/word_by_word_montgomery.ml   | 0m10.24s  || -0m00.27s | -2.73%
0m07.47s  | ExtractionOCaml/saturated_solinas            | 0m07.93s  || -0m00.46s | -5.80%
0m06.78s  | BoundsPipeline.vo                            | 0m05.96s  || +0m00.82s | +13.75%
0m06.72s  | ExtractionOCaml/unsaturated_solinas.ml       | 0m07.03s  || -0m00.31s | -4.40%
0m06.38s  | p224_32.c                                    | 0m06.54s  || -0m00.16s | -2.44%
0m06.21s  | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.34s  || -0m00.12s | -2.05%
0m05.45s  | p384_64.c                                    | 0m05.18s  || +0m00.27s | +5.21%
0m04.82s  | ExtractionHaskell/unsaturated_solinas.hs     | 0m04.84s  || -0m00.01s | -0.41%
0m04.80s  | ExtractionOCaml/saturated_solinas.ml         | 0m05.07s  || -0m00.27s | -5.32%
0m03.83s  | ExtractionHaskell/saturated_solinas.hs       | 0m04.07s  || -0m00.24s | -5.89%
0m03.30s  | PushButtonSynthesis/Primitives.vo            | 0m03.31s  || -0m00.01s | -0.30%
0m03.26s  | PushButtonSynthesis/SmallExamples.vo         | 0m03.24s  || +0m00.01s | +0.61%
0m03.08s  | PushButtonSynthesis/SaturatedSolinas.vo      | 0m02.96s  || +0m00.12s | +4.05%
0m02.16s  | curve25519_32.c                              | 0m02.16s  || +0m00.00s | +0.00%
0m01.57s  | curve25519_64.c                              | 0m01.47s  || +0m00.10s | +6.80%
0m01.40s  | CLI.vo                                       | 0m01.32s  || +0m00.07s | +6.06%
0m01.27s  | PushButtonSynthesis/MontgomeryReduction.vo   | 0m01.19s  || +0m00.08s | +6.72%
0m01.26s  | StandaloneHaskellMain.vo                     | 0m01.18s  || +0m00.08s | +6.77%
0m01.22s  | PushButtonSynthesis/BarrettReduction.vo      | 0m01.29s  || -0m00.07s | -5.42%
0m01.13s  | RewriterProofs.vo                            | 0m01.10s  || +0m00.02s | +2.72%
0m01.10s  | secp256k1_64.c                               | 0m01.01s  || +0m00.09s | +8.91%
0m01.08s  | StandaloneOCamlMain.vo                       | 0m01.13s  || -0m00.04s | -4.42%
0m01.06s  | p256_64.c                                    | 0m01.02s  || +0m00.04s | +3.92%
0m01.05s  | AbstractInterpretation.vo                    | 0m01.00s  || +0m00.05s | +5.00%
0m01.00s  | CompilersTestCases.vo                        | 0m01.08s  || -0m00.08s | -7.40%
0m01.00s  | p224_64.c                                    | 0m01.00s  || +0m00.00s | +0.00%

1 files changed, 227 insertions, 0 deletions

diff --git a/src/strip_literal_casts_rewrite_head.out b/src/strip_literal_casts_rewrite_head.out
new file mode 100644
index 000000000..30c18d604
--- /dev/null
+++ b/src/strip_literal_casts_rewrite_head.out
@@ -0,0 +1,227 @@
+strip_literal_casts_rewrite_head = 
+match idc in (Compilers.ident t) return (Compile.value' true t) with
+| @Literal t v => Base (##v)%expr
+| Nat_succ => fun x : expr ℕ => Base (#(Nat_succ)%expr @ x)%expr_pat
+| Nat_pred => fun x : expr ℕ => Base (#(Nat_pred)%expr @ x)%expr_pat
+| Nat_max => fun x x0 : expr ℕ => Base (#(Nat_max)%expr @ x @ x0)%expr_pat
+| Nat_mul => fun x x0 : expr ℕ => Base (#(Nat_mul)%expr @ x @ x0)%expr_pat
+| Nat_add => fun x x0 : expr ℕ => Base (#(Nat_add)%expr @ x @ x0)%expr_pat
+| Nat_sub => fun x x0 : expr ℕ => Base (#(Nat_sub)%expr @ x @ x0)%expr_pat
+| Nat_eqb => fun x x0 : expr ℕ => Base (#(Nat_eqb)%expr @ x @ x0)%expr_pat
+| @nil t => Base []%expr_pat
+| @cons t => fun (x : expr t) (x0 : expr (list t)) => Base (x :: x0)%expr_pat
+| @pair A B => fun (x : expr A) (x0 : expr B) => Base (x, x0)%expr_pat
+| @fst A B => fun x : expr (A * B)%etype => Base (#(fst)%expr @ x)%expr_pat
+| @snd A B => fun x : expr (A * B)%etype => Base (#(snd)%expr @ x)%expr_pat
+| @prod_rect A B T =>
+    fun (x : expr A -> expr B -> UnderLets (expr T))
+      (x0 : expr (A * B)%etype) =>
+    Base
+      (#(prod_rect)%expr @
+       (λ (x1 : var A)(x2 : var B),
+        to_expr (x ($x1) ($x2)))%expr @ x0)%expr_pat
+| @bool_rect T =>
+    fun (x x0 : expr unit -> UnderLets (expr T)) (x1 : expr bool) =>
+    Base
+      (#(bool_rect)%expr @ (λ x2 : var unit,
+                            to_expr (x ($x2)))%expr @
+       (λ x2 : var unit,
+        to_expr (x0 ($x2)))%expr @ x1)%expr_pat
+| @nat_rect P =>
+    fun (x : expr unit -> UnderLets (expr P))
+      (x0 : expr ℕ -> expr P -> UnderLets (expr P)) (x1 : expr ℕ) =>
+    Base
+      (#(nat_rect)%expr @ (λ x2 : var unit,
+                           to_expr (x ($x2)))%expr @
+       (λ (x2 : var ℕ)(x3 : var P),
+        to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat
+| @nat_rect_arrow P Q =>
+    fun (x : expr P -> UnderLets (expr Q))
+      (x0 : expr ℕ ->
+            (expr P -> UnderLets (expr Q)) -> expr P -> UnderLets (expr Q))
+      (x1 : expr ℕ) (x2 : expr P) =>
+    Base
+      (#(nat_rect_arrow)%expr @ (λ x3 : var P,
+                                 to_expr (x ($x3)))%expr @
+       (λ (x3 : var ℕ)(x4 : var (P -> Q)%ptype)(x5 : var P),
+        to_expr
+          (x0 ($x3) (fun x6 : expr P => Base ($x4 @ x6)%expr_pat) ($x5)))%expr @
+       x1 @ x2)%expr_pat
+| @list_rect A P =>
+    fun (x : expr unit -> UnderLets (expr P))
+      (x0 : expr A -> expr (list A) -> expr P -> UnderLets (expr P))
+      (x1 : expr (list A)) =>
+    Base
+      (#(list_rect)%expr @ (λ x2 : var unit,
+                            to_expr (x ($x2)))%expr @
+       (λ (x2 : var A)(x3 : var (list A))(x4 : var P),
+        to_expr (x0 ($x2) ($x3) ($x4)))%expr @ x1)%expr_pat
+| @list_case A P =>
+    fun (x : expr unit -> UnderLets (expr P))
+      (x0 : expr A -> expr (list A) -> UnderLets (expr P))
+      (x1 : expr (list A)) =>
+    Base
+      (#(list_case)%expr @ (λ x2 : var unit,
+                            to_expr (x ($x2)))%expr @
+       (λ (x2 : var A)(x3 : var (list A)),
+        to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat
+| @List_length T =>
+    fun x : expr (list T) => Base (#(List_length)%expr @ x)%expr_pat
+| List_seq => fun x x0 : expr ℕ => Base (#(List_seq)%expr @ x @ x0)%expr_pat
+| @List_firstn A =>
+    fun (x : expr ℕ) (x0 : expr (list A)) =>
+    Base (#(List_firstn)%expr @ x @ x0)%expr_pat
+| @List_skipn A =>
+    fun (x : expr ℕ) (x0 : expr (list A)) =>
+    Base (#(List_skipn)%expr @ x @ x0)%expr_pat
+| @List_repeat A =>
+    fun (x : expr A) (x0 : expr ℕ) =>
+    Base (#(List_repeat)%expr @ x @ x0)%expr_pat
+| @List_combine A B =>
+    fun (x : expr (list A)) (x0 : expr (list B)) =>
+    Base (#(List_combine)%expr @ x @ x0)%expr_pat
+| @List_map A B =>
+    fun (x : expr A -> UnderLets (expr B)) (x0 : expr (list A)) =>
+    Base
+      (#(List_map)%expr @ (λ x1 : var A,
+                           to_expr (x ($x1)))%expr @ x0)%expr_pat
+| @List_app A => fun x x0 : expr (list A) => Base (x ++ x0)%expr
+| @List_rev A =>
+    fun x : expr (list A) => Base (#(List_rev)%expr @ x)%expr_pat
+| @List_flat_map A B =>
+    fun (x : expr A -> UnderLets (expr (list B))) (x0 : expr (list A)) =>
+    Base
+      (#(List_flat_map)%expr @ (λ x1 : var A,
+                                to_expr (x ($x1)))%expr @ x0)%expr_pat
+| @List_partition A =>
+    fun (x : expr A -> UnderLets (expr bool)) (x0 : expr (list A)) =>
+    Base
+      (#(List_partition)%expr @ (λ x1 : var A,
+                                 to_expr (x ($x1)))%expr @ x0)%expr_pat
+| @List_fold_right A B =>
+    fun (x : expr B -> expr A -> UnderLets (expr A)) (x0 : expr A)
+      (x1 : expr (list B)) =>
+    Base
+      (#(List_fold_right)%expr @
+       (λ (x2 : var B)(x3 : var A),
+        to_expr (x ($x2) ($x3)))%expr @ x0 @ x1)%expr_pat
+| @List_update_nth T =>
+    fun (x : expr ℕ) (x0 : expr T -> UnderLets (expr T)) (x1 : expr (list T))
+    =>
+    Base
+      (#(List_update_nth)%expr @ x @ (λ x2 : var T,
+                                      to_expr (x0 ($x2)))%expr @ x1)%expr_pat
+| @List_nth_default T =>
+    fun (x : expr T) (x0 : expr (list T)) (x1 : expr ℕ) =>
+    Base (#(List_nth_default)%expr @ x @ x0 @ x1)%expr_pat
+| Z_add => fun x x0 : expr ℤ => Base (x + x0)%expr
+| Z_mul => fun x x0 : expr ℤ => Base (x * x0)%expr
+| Z_pow => fun x x0 : expr ℤ => Base (#(Z_pow)%expr @ x @ x0)%expr_pat
+| Z_sub => fun x x0 : expr ℤ => Base (x - x0)%expr
+| Z_opp => fun x : expr ℤ => Base (- x)%expr
+| Z_div => fun x x0 : expr ℤ => Base (x / x0)%expr
+| Z_modulo => fun x x0 : expr ℤ => Base (x mod x0)%expr
+| Z_log2 => fun x : expr ℤ => Base (#(Z_log2)%expr @ x)%expr_pat
+| Z_log2_up => fun x : expr ℤ => Base (#(Z_log2_up)%expr @ x)%expr_pat
+| Z_eqb => fun x x0 : expr ℤ => Base (#(Z_eqb)%expr @ x @ x0)%expr_pat
+| Z_leb => fun x x0 : expr ℤ => Base (#(Z_leb)%expr @ x @ x0)%expr_pat
+| Z_geb => fun x x0 : expr ℤ => Base (#(Z_geb)%expr @ x @ x0)%expr_pat
+| Z_of_nat => fun x : expr ℕ => Base (#(Z_of_nat)%expr @ x)%expr_pat
+| Z_to_nat => fun x : expr ℤ => Base (#(Z_to_nat)%expr @ x)%expr_pat
+| Z_shiftr => fun x x0 : expr ℤ => Base (x >> x0)%expr
+| Z_shiftl => fun x x0 : expr ℤ => Base (x << x0)%expr
+| Z_land => fun x x0 : expr ℤ => Base (x &' x0)%expr
+| Z_lor => fun x x0 : expr ℤ => Base (x || x0)%expr
+| Z_bneg => fun x : expr ℤ => Base (#(Z_bneg)%expr @ x)%expr_pat
+| Z_lnot_modulo =>
+    fun x x0 : expr ℤ => Base (#(Z_lnot_modulo)%expr @ x @ x0)%expr_pat
+| Z_mul_split =>
+    fun x x0 x1 : expr ℤ => Base (#(Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat
+| Z_add_get_carry =>
+    fun x x0 x1 : expr ℤ =>
+    Base (#(Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat
+| Z_add_with_carry =>
+    fun x x0 x1 : expr ℤ =>
+    Base (#(Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat
+| Z_add_with_get_carry =>
+    fun x x0 x1 x2 : expr ℤ =>
+    Base (#(Z_add_with_get_carry)%expr @ x @ x0 @ x1 @ x2)%expr_pat
+| Z_sub_get_borrow =>
+    fun x x0 x1 : expr ℤ =>
+    Base (#(Z_sub_get_borrow)%expr @ x @ x0 @ x1)%expr_pat
+| Z_sub_with_get_borrow =>
+    fun x x0 x1 x2 : expr ℤ =>
+    Base (#(Z_sub_with_get_borrow)%expr @ x @ x0 @ x1 @ x2)%expr_pat
+| Z_zselect =>
+    fun x x0 x1 : expr ℤ => Base (#(Z_zselect)%expr @ x @ x0 @ x1)%expr_pat
+| Z_add_modulo =>
+    fun x x0 x1 : expr ℤ =>
+    Base (#(Z_add_modulo)%expr @ x @ x0 @ x1)%expr_pat
+| Z_rshi =>
+    fun x x0 x1 x2 : expr ℤ =>
+    Base (#(Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat
+| Z_cc_m => fun x x0 : expr ℤ => Base (#(Z_cc_m)%expr @ x @ x0)%expr_pat
+| Z_cast range =>
+    fun x : expr ℤ =>
+    (match x with
+     | @expr.Ident _ _ _ t idc =>
+         args <- invert_bind_args idc Raw.ident.Literal;
+         match pattern.type.unify_extracted ℤ (projT1 args) with
+         | Some _ =>
+             if type.type_beq base.type base.type.type_beq ℤ (projT1 args)
+             then
+              xv <- ident.unify pattern.ident.Literal ##(projT2 args);
+              fv <- (x0 <- (if
+                             is_bounded_by_bool (let (x0, _) := xv in x0)
+                               (ZRange.normalize range)
+                            then Some (##(let (x0, _) := xv in x0))%expr
+                            else None);
+                     Some (Base x0));
+              Some (fv0 <-- fv;
+                    Base fv0)%under_lets
+             else None
+         | None => None
+         end
+     | _ => None
+     end;;;
+     Base (#(Z_cast range)%expr @ x)%expr_pat)%option
+| Z_cast2 range =>
+    fun x : expr (ℤ * ℤ)%etype => Base (#(Z_cast2 range)%expr @ x)%expr_pat
+| fancy_add log2wordmax imm =>
+    fun x : expr (ℤ * ℤ)%etype =>
+    Base (#(fancy_add log2wordmax imm)%expr @ x)%expr_pat
+| fancy_addc log2wordmax imm =>
+    fun x : expr (ℤ * ℤ * ℤ)%etype =>
+    Base (#(fancy_addc log2wordmax imm)%expr @ x)%expr_pat
+| fancy_sub log2wordmax imm =>
+    fun x : expr (ℤ * ℤ)%etype =>
+    Base (#(fancy_sub log2wordmax imm)%expr @ x)%expr_pat
+| fancy_subb log2wordmax imm =>
+    fun x : expr (ℤ * ℤ * ℤ)%etype =>
+    Base (#(fancy_subb log2wordmax imm)%expr @ x)%expr_pat
+| fancy_mulll log2wordmax =>
+    fun x : expr (ℤ * ℤ)%etype =>
+    Base (#(fancy_mulll log2wordmax)%expr @ x)%expr_pat
+| fancy_mullh log2wordmax =>
+    fun x : expr (ℤ * ℤ)%etype =>
+    Base (#(fancy_mullh log2wordmax)%expr @ x)%expr_pat
+| fancy_mulhl log2wordmax =>
+    fun x : expr (ℤ * ℤ)%etype =>
+    Base (#(fancy_mulhl log2wordmax)%expr @ x)%expr_pat
+| fancy_mulhh log2wordmax =>
+    fun x : expr (ℤ * ℤ)%etype =>
+    Base (#(fancy_mulhh log2wordmax)%expr @ x)%expr_pat
+| fancy_rshi log2wordmax x =>
+    fun x0 : expr (ℤ * ℤ)%etype =>
+    Base (#(fancy_rshi log2wordmax x)%expr @ x0)%expr_pat
+| fancy_selc =>
+    fun x : expr (ℤ * ℤ * ℤ)%etype => Base (#(fancy_selc)%expr @ x)%expr_pat
+| fancy_selm log2wordmax =>
+    fun x : expr (ℤ * ℤ * ℤ)%etype =>
+    Base (#(fancy_selm log2wordmax)%expr @ x)%expr_pat
+| fancy_sell =>
+    fun x : expr (ℤ * ℤ * ℤ)%etype => Base (#(fancy_sell)%expr @ x)%expr_pat
+| fancy_addm =>
+    fun x : expr (ℤ * ℤ * ℤ)%etype => Base (#(fancy_addm)%expr @ x)%expr_pat
+end
+     : Compile.value' true t