diff options
| author |  jadep <jadep@mit.edu> | 2018-12-10 15:47:24 -0500 |
|---|---|---|
| committer |  jadep <jade.philipoom@gmail.com> | 2019-01-03 04:45:18 -0500 |
| commit | 43bededd9eb0ec8491aac4fd24460ffdbae7678d (patch) | |
| tree | dfa259a4873390b2a5a25fc27b7f924473e23d07 /src | |
| parent | ed7bd2abd3e0ef7d7b994113da7187da2debfe31 (diff) | |
fixed up some of the fancy rewrite rules
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel2.v | 47 |
1 files changed, 4 insertions, 43 deletions
diff --git a/src/Experiments/NewPipeline/Toplevel2.v b/src/Experiments/NewPipeline/Toplevel2.v index 117381c8c..5fd932463 100644 --- a/src/Experiments/NewPipeline/Toplevel2.v +++ b/src/Experiments/NewPipeline/Toplevel2.v @@ -3592,7 +3592,6 @@ Module Barrett256. | _ => econstructor end. } { cbn. cbv [muLow M]. - About Fancy.of_prefancy_scalar. Ltac sub := repeat match goal with | _ => progress intros @@ -3604,53 +3603,15 @@ Module Barrett256. | |- Fancy.of_prefancy_scalar _ _ _ _ = _ => cbn; solve [eauto] end. - econstructor; [ solve [sub] | intros ]. - econstructor; [ solve [sub] | intros ]. + repeat (econstructor; [ 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] ]. - econstructor; [ solve [sub] | intros ]. - econstructor; [ solve [sub] | intros ]. - econstructor; [ solve [sub] | intros ]. - econstructor; [ solve [sub] | intros ]. - econstructor; [ solve [sub] | intros ]. - econstructor; [ solve [sub] | intros ]. - econstructor. - { sub. cbn. admit. - (* TODO : This needs to be ADD, not ADDC 0! Fix in fancy rewrite rules! *) } - intros. - econstructor; [ solve [sub] | intros ]. - econstructor. - { sub. cbn. admit. - (* TODO : This needs to be ADD, not ADDC 0! Fix in fancy rewrite rules! *) } - intros. + repeat (econstructor; [ solve [sub] | intros ]). econstructor. { sub. admit. (* TODO: this is the too-tight RSHI cast *) } - econstructor. - { sub. cbn. admit. - (* TODO : This needs to be ADD, not ADDC 0! Fix in fancy rewrite rules! *) } - intros. - econstructor; [ solve [sub] | intros ]. - econstructor; [ solve [sub] | intros ]. - econstructor; [ solve [sub] | intros ]. - econstructor; [ solve [sub] | intros ]. - econstructor; [ solve [sub] | intros ]. - econstructor; [ solve [sub] | intros ]. - econstructor. - { sub. cbn. admit. - (* TODO : This needs to be ADD, not ADDC 0! Fix in fancy rewrite rules! *) } - intros. - econstructor; [ solve [sub] | intros ]. - econstructor. - { sub. cbn. admit. - (* TODO : This needs to be ADD, not ADDC 0! Fix in fancy rewrite rules! *) } - intros. - econstructor; [ solve [sub] | intros ]. - econstructor; [ solve [sub] | intros ]. - econstructor; [ solve [sub] | intros ]. - econstructor; [ solve [sub] | intros ]. - econstructor; [ solve [sub] | intros ]. - econstructor; [ solve [sub] | intros ]. + repeat (econstructor; [ solve [sub] | intros ]). econstructor. sub. } { cbn - [barrett_red256]. cbv [id]. |