diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2017-06-15 22:22:39 -0400 |
|---|---|---|
| committer |  Andres Erbsen <andreser@mit.edu> | 2017-06-15 22:22:39 -0400 |
| commit | fb1ea0af216dfd0dcb1b31cf069890081bdd0198 (patch) | |
| tree | 78a5a2cb8b4d1c74a8d292d68bd56826776c5768 /src | |
| parent | ecf8d0ce9ad7dda0d19978aea38fd47c98ec41af (diff) | |
Finish karatsuba mul, add display file (#199)
This closes #182.
Diffstat (limited to 'src')
| -rw-r--r-- | src/Specific/IntegrationTestKaratsubaMul.v | 36 | ||||
| -rw-r--r-- | src/Specific/IntegrationTestKaratsubaMulDisplay.v | 4 |
2 files changed, 6 insertions, 34 deletions
diff --git a/src/Specific/IntegrationTestKaratsubaMul.v b/src/Specific/IntegrationTestKaratsubaMul.v index ca25596ec..9dc49ca00 100644 --- a/src/Specific/IntegrationTestKaratsubaMul.v +++ b/src/Specific/IntegrationTestKaratsubaMul.v @@ -63,40 +63,8 @@ Section BoundedField25p5. apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). (* jgross start here! *) (*Set Ltac Profiling.*) - Ltac ReflectiveTactics.solve_side_conditions ::= idtac. Time refine_reflectively. - Import ReflectiveTactics. - { Time do_reify. } - Import Compilers.Syntax. - Require Import Crypto.Util.Tactics.SubstLet. - Require Import Crypto.Util.Tactics.UnifyAbstractReflexivity. - { Time unify_abstract_vm_compute_rhs_reflexivity. } - { Time unify_abstract_vm_compute_rhs_reflexivity. } - { Time unify_abstract_vm_compute_rhs_reflexivity. } - { Time unify_abstract_vm_compute_rhs_reflexivity. } - { Time unify_abstract_vm_compute_rhs_reflexivity. } - { Time unify_abstract_rhs_reflexivity. } - Require Import CNotations. - { Show. Time unify_abstract_renamify_rhs_reflexivity. } - { Time shelve; subst_let; clear; abstract vm_cast_no_check (eq_refl true). } - { Time shelve; subst_let; clear; vm_compute; reflexivity. } - { Time shelve; unify_abstract_compute_rhs_reflexivity. } - { Time shelve; unify_abstract_cbv_interp_rhs_reflexivity. } - { Time abstract handle_bounds_from_hyps. } - { Time handle_boundedness_side_condition. } - Unshelve. - all:shelve_unifiable. - cbv [Interpretation.Bounds.is_tighter_thanb Relations.interp_flat_type_relb_pointwise Relations.interp_flat_type_rel_pointwise_gen_Prop Syntax.tuple Syntax.tuple' fst snd codomain bounds Interpretation.Bounds.is_tighter_thanb']. - (*((r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange && - (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange && - (r[0 ~> 72057594037927936] <=? r[0 ~> 81064793292668928])%zrange && - (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange && - (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange && - (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange && - (r[0 ~> 72057594037927936] <=? r[0 ~> 81064793292668928])%zrange && - (r[0 ~> 72057594037927935] <=? r[0 ~> 81064793292668928])%zrange)%bool = - true *) - Decidable.vm_decide. - Time Admitted. + (*Show Ltac Profile.*) + Time Defined. End BoundedField25p5. diff --git a/src/Specific/IntegrationTestKaratsubaMulDisplay.v b/src/Specific/IntegrationTestKaratsubaMulDisplay.v new file mode 100644 index 000000000..96312713b --- /dev/null +++ b/src/Specific/IntegrationTestKaratsubaMulDisplay.v @@ -0,0 +1,4 @@ +Require Import Crypto.Specific.IntegrationTestKaratsubaMul. +Require Import Crypto.Specific.IntegrationTestDisplayCommon. + +Check display mul. |