diff options
Diffstat (limited to 'src/Specific/IntegrationTest.v')
| -rw-r--r-- | src/Specific/IntegrationTest.v | 61 |
1 files changed, 52 insertions, 9 deletions
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. |