Finally, a fully working IntegrationTest

2 files changed, 97 insertions, 65 deletions

diff --git a/src/Reflection/Z/Bounds/Pipeline/Glue.v b/src/Reflection/Z/Bounds/Pipeline/Glue.v
index 7621a466b..af6a5548b 100644
--- a/src/Reflection/Z/Bounds/Pipeline/Glue.v
+++ b/src/Reflection/Z/Bounds/Pipeline/Glue.v
@@ -12,84 +12,65 @@ Require Import Crypto.Util.Curry.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Util.BoundedWord.
 Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.SigmaAssoc.
+Require Import Crypto.Util.Tactics.EvarExists.
 
 Module Export Exports.
   Export Crypto.Reflection.Z.Reify. (* export for the tactic redefinitions *)
 End Exports.
 
+(** The [reassoc_sig_and_eexists] tactic operates on a goal convertible with
+<<
+{ f : { a | is_bounded_by bounds a }
+| BoundedWordToZ f = rexprZ (BoundedWordToZ a) ... (BoundedWordToZ z) }
+>>
+    and leaves a goal of the form
+<<
+is_bounded_by bounds (map wordToZ ?f)
+  /\ map wordToZ ?f = rexprZ (map wordToZ (proj1_sig a)) ... (map wordToZ (proj1_sig z))
+>>
+    where [?f] is a context variable set to a new evar.  This tactic
+    relies on the exact definition of [BoundedWordToZ]. *)
+Ltac reassoc_sig_and_eexists :=
+  cbv [BoundedWordToZ];
+  sig_sig_assoc;
+  evar_exists.
+
 (** The [do_curry] tactic takes a goal of the form
 <<
-BoundedWordToZ (?f a b ... z) = F A B ... Z
+_ /\ BoundedWordToZ (?f a b ... z) = F A B ... Z
 >>
     and turns it into a goal of the form
 <<
-BoundedWordToZ (f' (a, b, ..., z)) = F' (A, B, ..., Z)
+_ /\ BoundedWordToZ (f' (a, b, ..., z)) = F' (A, B, ..., Z)
 >>
 
     Note that the number of arguments on the left and on the right DO
     NOT need to be the same.  *)
 Ltac do_curry :=
   lazymatch goal with
-  | [ |- ?BWtoZ ?f_bw = ?f_Z ]
+  | [ |- _ /\ ?BWtoZ ?f_bw = ?f_Z ]
     => let f_bw := head f_bw in
        let f_Z := head f_Z in
        change_with_curried f_Z;
-       let f_bw_name := fresh f_bw in
-       set (f_bw_name := f_bw);
-       change_with_curried f_bw_name
+       change_with_curried f_bw
   end.
 
 (** The [split_BoundedWordToZ] tactic takes a goal of the form
 <<
-BoundedWordToZ f = F
+_ /\ map wordToZ (proj1_sig f) = F ARGS
 >>
-    and splits it into a conjunction, one part about the computational
-    behavior, and another part about the boundedness.
+    and splits [f] and any arguments in ARGS into two parts, part
+    about the computational behavior, and another part about the
+    boundedness.
 
-    This tactic relies on the specific definition of [BoundedWordToZ],
+    This pipeline relies on the specific definition of [BoundedWordToZ],
     and requires [f] to be a context variable which is set to a single
     evar. *)
-Ltac make_evar_for_first_projection :=
+Ltac check_precondition _ :=
   lazymatch goal with
-  | [ |- @map ?N1 ?A ?B wordToZ (@proj1_sig _ ?P ?f) = _ ]
-    => let f1 := fresh f in
-       let f2 := fresh f in
-       let pf := fresh in
-       revert f; refine (_ : let f := exist P _ _ in _);
-       intro f;
-       pose (proj1_sig f) as f1;
-       pose (proj2_sig f : P f1) as f2;
-       change f with (exist P f1 f2);
-       subst f; cbn [proj1_sig proj2_sig] in f1, f2 |- *; revert f2;
-       (** Now we rely on the behavior of Coq's unifier to transform
-           the goal for us; we a goal like [let f' : A := ?f_evar in
-           B], and we want a goal like [A /\ B].  So we refine with a
-           hole named [pf] which is proof of [A /\ B], and then assert
-           that the second projection of the proof (which has type
-           [B]) actually has type [let f' : A := proj1 pf in B].  If
-           done naïvely, this would give a circlular type, which Coq
-           disallows.  However, Coq is happy to zeta-reduce away the
-           circlularity; happily, this is done after Coq unifies [let
-           f' : A := proj1 pf in B] with [let f' : A := ?f_evar in B],
-           hence filling [?f_evar] with the first projection of the
-           proof.  Since Coq instantiates the two existing evars
-           ([?f_evar] and the current goal, which is represented by an
-           evar under the hood) with projections of the new evar
-           (which becomes the new goal)---and let us hope that Coq
-           devs never decide both to turn on judgmental η (currently
-           controlled by primitive projections) for [and], and to
-           prefer η-expansion of evars before dropping context
-           variables (we might also be in trouble if someone adds a
-           [Canonical Structure] for [and])---we get the desired
-           behavior--for now. *)
-       lazymatch goal with
-       | [ |- let f' := _ in ?B ]
-         => refine (let pf := _ in (proj2 pf : let f' := proj1 pf in B))
-       end
-  end.
-Ltac check_split_BoundedWordToZ_precondition :=
-  lazymatch goal with
-  | [ |- BoundedWordToZ _ _ _ ?f = _ ]
+  | [ |- @ZRange.is_bounded_by ?option_bit_width ?count ?bounds (map wordToZ ?f)
+         /\ map wordToZ ?f = _ ]
     => first [ is_var f | fail 1 "The argument to BoundedWordToZ must be a bare context-definition set to an evar, not"
                                f "which is not a variable" ];
        match goal with
@@ -103,19 +84,26 @@ Ltac check_split_BoundedWordToZ_precondition :=
                  f' "which has no body"
        | _ => fail 1 "The argument to BoundedWordToZ must be a context-definition, not" f "which does not appear in the context"
        end
+  | [ |- ?G ]
+    => let expected := uconstr:(@ZRange.is_bounded_by _ _ _ (map wordToZ ?[f])
+                                /\ map wordToZ ?[f] = _) in
+       fail "The post-processed goal should have the form"
+            expected
+            "not"
+            G
   end.
 Ltac split_BoundedWordToZ :=
-  check_split_BoundedWordToZ_precondition;
   (** first revert the context definition which is an evar named [f]
       in the docs above, so that it becomes evar 1 (for
       [instantiate]), and so that [make_evar_for_first_projection]
       works *)
+  check_precondition ();
   lazymatch goal with
-  | [ |- BoundedWordToZ _ _ _ ?f = _ ]
+  | [ |- _ /\ map wordToZ ?f = _ ]
     => revert f
   end;
   repeat match goal with
-         | [ |- context[BoundedWordToZ _ _ _ ?x] ]
+         | [ |- context[map wordToZ (proj1_sig ?x)] ]
            => is_var x;
               first [ clearbody x; fail 1
                     | (** we want to keep the same context variable in
@@ -124,8 +112,8 @@ Ltac split_BoundedWordToZ :=
                     instantiate (1:=ltac:(destruct x)); destruct x ]
          end;
   cbv beta iota; intro; (* put [f] back in the context so that [cbn] doesn't remove this let-in *)
-  unfold BoundedWordToZ; cbn [proj1_sig];
-  make_evar_for_first_projection.
+  cbn [proj1_sig].
+
 (** The [zrange_to_reflective] tactic takes a goal of the form
 <<
 is_bounded_by _ bounds (map wordToZ (?fW args)) /\ map wordToZ (?fW args) = fZ argsZ
@@ -200,6 +188,7 @@ BoundedWordToZ ?f = F (BoundedWordToZ A) (BoundedWordToZ B) ... (BoundedWordToZ
     where [?f] is an evar, and turns it into a goal the that
     reflective automation pipeline can handle. *)
 Ltac refine_to_reflective_glue :=
+  reassoc_sig_and_eexists;
   do_curry;
   split_BoundedWordToZ;
-  zrange_to_reflective.
+  zrange_to_reflective_goal.
diff --git a/src/Specific/IntegrationTest.v b/src/Specific/IntegrationTest.v
index ce25462b0..126a05c49 100644
--- a/src/Specific/IntegrationTest.v
+++ b/src/Specific/IntegrationTest.v
@@ -49,7 +49,7 @@ Section BoundedField25p5.
          cbv beta iota
     end.
 
-  (*(** TODO MOVE ME *)
+  (** TODO MOVE ME *)
   Ltac save_state_and_back_to_sig :=
     [> reflexivity
     | lazymatch goal with
@@ -62,7 +62,7 @@ Section BoundedField25p5.
   Definition sig_f_equal {T A B} (f : A -> B) {x y : T -> A}
              (p : { t : T | x t = y t })
     : { t : T | f (x t) = f (y t) }
-    := exist _ (proj1_sig p) (f_equal f (proj2_sig p)).*)
+    := exist _ (proj1_sig p) (f_equal f (proj2_sig p)).
   (* TODO : change this to field once field isomorphism happens *)
   Definition add :
     { add : feBW -> feBW -> feBW
@@ -72,8 +72,8 @@ Section BoundedField25p5.
     | [ |- { f | forall a b, ?phi (f a b) = @?rhs a b } ]
       => apply lift2_sig with (P:=fun a b f => phi f = rhs a b)
     end.
-    intros. eexists ?[add]. all:cbv [phi].
-    (*eexists_sig_etransitivity. all:cbv [phi].*)
+    intros.
+    eexists_sig_etransitivity. all:cbv [phi].
     rewrite <- (proj2_sig add_sig).
     symmetry; rewrite <- (proj2_sig carry_sig); symmetry.
     set (carry_addZ := fun a b => proj1_sig carry_sig (proj1_sig add_sig a b)).
@@ -84,11 +84,54 @@ Section BoundedField25p5.
       pose carry_addZ' as carry_addZ;
       replace carry_addZ'' with carry_addZ by abstract (cbv beta iota delta [carry_addZ'' proj1_sig add_sig carry_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]; reflexivity);
       clear carry_addZ''.
-    apply f_equal.
+    all:save_state_and_back_to_sig.
+    apply sig_f_equal.
     (* jgross start here! *)
-    Set Ltac Profiling.
-    Time refine_reflectively.
-    Show Ltac Profile.
-  Time Defined.
+    (*Set Ltac Profiling.*)
+    Time refine_reflectively. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *)
+    (*Show Ltac Profile.*)
+    (* total time:     19.632s
+
+ tactic                                   local  total   calls       max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─refine_reflectively -------------------   0.0%  98.4%       1   19.320s
+─ReflectiveTactics.do_reflective_pipelin  -0.0%  96.2%       1   18.884s
+─ReflectiveTactics.solve_side_conditions   1.2%  96.1%       1   18.860s
+─ReflectiveTactics.do_reify ------------  27.7%  44.0%       1    8.640s
+─ReflectiveTactics.abstract_vm_compute_r  12.3%  13.9%       2    2.024s
+─ReflectiveTactics.abstract_vm_compute_r   8.9%  12.2%       2    1.576s
+─Reify_rhs_gen -------------------------   0.8%  11.7%       1    2.300s
+─ReflectiveTactics.renamify_rhs --------  10.4%  11.5%       1    2.260s
+─ReflectiveTactics.abstract_rhs --------   4.6%   5.8%       1    1.148s
+─clear (var_list) ----------------------   5.2%   5.2%      57    0.184s
+─eexact --------------------------------   4.1%   4.1%      68    0.028s
+─prove_interp_compile_correct ----------   0.0%   3.4%       1    0.664s
+─ReflectiveTactics.abstract_cbv_interp_r   2.7%   3.3%       1    0.648s
+─unify (constr) (constr) ---------------   3.2%   3.2%       6    0.248s
+─rewrite ?EtaInterp.InterpExprEta ------   3.1%   3.1%       1    0.612s
+─ReflectiveTactics.abstract_cbv_rhs ----   2.0%   2.7%       1    0.532s
+─Glue.refine_to_reflective_glue --------   0.0%   2.2%       1    0.436s
+─rewrite H -----------------------------   2.1%   2.1%       1    0.420s
+
+ tactic                                   local  total   calls       max
+────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
+─refine_reflectively -------------------   0.0%  98.4%       1   19.320s
+ ├─ReflectiveTactics.do_reflective_pipel  -0.0%  96.2%       1   18.884s
+ │└ReflectiveTactics.solve_side_conditio   1.2%  96.1%       1   18.860s
+ │ ├─ReflectiveTactics.do_reify --------  27.7%  44.0%       1    8.640s
+ │ │ ├─Reify_rhs_gen -------------------   0.8%  11.7%       1    2.300s
+ │ │ │ ├─prove_interp_compile_correct --   0.0%   3.4%       1    0.664s
+ │ │ │ │└rewrite ?EtaInterp.InterpExprEt   3.1%   3.1%       1    0.612s
+ │ │ │ └─rewrite H ---------------------   2.1%   2.1%       1    0.420s
+ │ │ └─eexact --------------------------   4.1%   4.1%      68    0.028s
+ │ ├─ReflectiveTactics.abstract_vm_compu  12.3%  13.9%       2    2.024s
+ │ ├─ReflectiveTactics.abstract_vm_compu   8.9%  12.2%       2    1.576s
+ │ ├─ReflectiveTactics.renamify_rhs ----  10.4%  11.5%       1    2.260s
+ │ ├─ReflectiveTactics.abstract_rhs ----   4.6%   5.8%       1    1.148s
+ │ ├─ReflectiveTactics.abstract_cbv_inte   2.7%   3.3%       1    0.648s
+ │ └─ReflectiveTactics.abstract_cbv_rhs    2.0%   2.7%       1    0.532s
+ └─Glue.refine_to_reflective_glue ------   0.0%   2.2%       1    0.436s
+*)
+  Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *)
 
 End BoundedField25p5.