diff options
author | 2019-01-08 04:21:38 -0500 | |
---|---|---|
committer | 2019-01-09 22:49:02 -0500 | |
commit | 3ca227f1137e6a3b65bc33f5689e1c230d591595 (patch) | |
tree | e1e5a2dd2a2f34f239d3276227ddbdc69eeeb667 /src/Compilers/Z/RewriteAddToAdcInterp.v | |
parent | 3ec21c64b3682465ca8e159a187689b207c71de4 (diff) |
remove old pipeline
Diffstat (limited to 'src/Compilers/Z/RewriteAddToAdcInterp.v')
-rw-r--r-- | src/Compilers/Z/RewriteAddToAdcInterp.v | 71 |
1 files changed, 0 insertions, 71 deletions
diff --git a/src/Compilers/Z/RewriteAddToAdcInterp.v b/src/Compilers/Z/RewriteAddToAdcInterp.v deleted file mode 100644 index 28953a3fb..000000000 --- a/src/Compilers/Z/RewriteAddToAdcInterp.v +++ /dev/null @@ -1,71 +0,0 @@ -Require Import Crypto.Compilers.Named.PositiveContext. -Require Import Crypto.Compilers.Named.PositiveContext.DefaultsProperties. -Require Import Crypto.Compilers.Named.ContextDefinitions. -Require Import Crypto.Compilers.Named.InterpretToPHOASInterp. -Require Import Crypto.Compilers.Named.CompileWf. -Require Import Crypto.Compilers.Named.CompileInterp. -Require Import Crypto.Compilers.Named.WfFromUnit. -Require Import Crypto.Compilers.Named.DeadCodeEliminationInterp. -Require Import Crypto.Compilers.Named.WfInterp. -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.Z.Syntax. -Require Import Crypto.Compilers.Z.RewriteAddToAdc. -Require Import Crypto.Compilers.Z.Named.RewriteAddToAdcInterp. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.Bool. - -Section language. - Local Notation PContext var := (PositiveContext _ var _ internal_base_type_dec_bl). - - Lemma InterpRewriteAdc - {t} (e : Expr t) (Hwf : Wf e) - : forall x, Compilers.Syntax.Interp interp_op (RewriteAdc e) x = Compilers.Syntax.Interp interp_op e x. - Proof. - intro x; unfold RewriteAdc, option_map; break_innermost_match; try reflexivity; - match goal with |- ?x = ?y => cut (Some x = Some y); [ congruence | ] end; - (etransitivity; [ symmetry; eapply @Interp_InterpToPHOAS with (t:=Arrow _ _) | ]); - repeat - repeat - first [ lazymatch goal with - | [ H : DeadCodeElimination.EliminateDeadCode _ _ = Some ?e |- Syntax.Named.Interp ?e _ = Some _ ] - => let lhs := match goal with |- ?lhs = _ => lhs end in - let v := fresh in - (destruct lhs as [v|] eqn:?); - [ apply f_equal; eapply @InterpEliminateDeadCode with (Name_beq:=BinPos.Pos.eqb); - [ .. | eassumption | try eassumption | try eassumption ]; clear H | ] - | [ |- Syntax.Named.Interp (RewriteAddToAdc.rewrite_expr _ ?e) _ = Some _ ] - => let lhs := match goal with |- ?lhs = _ => lhs end in - let H := fresh in - destruct lhs eqn:H; [ apply (f_equal (@Some _)); eapply @Interp_rewrite_expr in H | ] - | [ H : Compile.compile (?e _) _ = Some ?e'', H' : Syntax.Named.Interp ?e'' ?x = Some ?v' |- ?v' = Compilers.Syntax.Interp ?interp_op' ?e ?x ] - => eapply @Interp_compile with (v:=x) (interp_op:=interp_op') in H - end - | intros; exact (@PositiveContextOk _ _ base_type_beq internal_base_type_dec_bl internal_base_type_dec_lb) - | progress split_andb - | congruence - | tauto - | solve [ auto | eapply @BinPos.Pos.eqb_eq; auto ] - | eapply @Wf_from_unit - | eapply @dec_rel_of_bool_dec_rel - | eapply @internal_base_type_dec_lb - | eapply @internal_base_type_dec_bl - | eapply @InterpEliminateDeadCode; [ .. | eassumption | eassumption | ] - | apply name_list_unique_DefaultNamesFor - | progress intros - | rewrite !@lookupb_empty - | eapply @wf_from_unit with (uContext:=PContext _); [ .. | eassumption ] - | match goal with - | [ H : Syntax.Named.Interp ?e ?x = Some ?a, H' : Syntax.Named.Interp ?e ?x = Some ?b |- _ ] - => assert (a = b) by congruence; (subst a || subst b) - end - | lazymatch goal with - | [ |- Some _ = Some _ ] => fail - | [ |- None = Some _ ] => exfalso; eapply @wf_interp_not_None; [ .. | unfold Syntax.Named.Interp in *; eassumption ] - | [ |- ?x = Some _ ] => destruct x eqn:?; [ apply f_equal | ] - end ]. - Qed. -End language. - -Hint Rewrite @InterpRewriteAdc using solve_wf_side_condition : reflective_interp. |