diff options
Diffstat (limited to 'src/Experiments/NewPipeline')
-rw-r--r-- | src/Experiments/NewPipeline/Rewriter.v | 34 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/RewriterRulesGood.v | 34 |
2 files changed, 30 insertions, 38 deletions
diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v index 93fa108d6..666b0cc21 100644 --- a/src/Experiments/NewPipeline/Rewriter.v +++ b/src/Experiments/NewPipeline/Rewriter.v @@ -520,6 +520,16 @@ Module Compilers. => fun f (x : value' _ _) => @reflect _ d (f @ (@reify _ s x)) end%expr%under_lets. + Fixpoint reify_expr {t} (e : @expr.expr base.type ident value t) + : @expr.expr base.type ident var t + := match e in expr.expr t return expr.expr t with + | expr.Ident t idc => expr.Ident idc + | expr.Var t v => reify v + | expr.Abs s d f => expr.Abs (fun x => @reify_expr _ (f (reflect (expr.Var x)))) + | expr.App s d f x => expr.App (@reify_expr _ f) (@reify_expr _ x) + | expr.LetIn A B x f => expr.LetIn (@reify_expr _ x) (fun xv => @reify_expr _ (f (reflect (expr.Var xv)))) + end. + Definition reify_and_let_binds_cps {with_lets} {t} : value' with_lets t -> forall T, (expr t -> UnderLets T) -> UnderLets T := match t, with_lets return value' with_lets t -> forall T, (expr t -> UnderLets T) -> UnderLets T with | type.base _, false => reify_and_let_binds_base_cps _ @@ -605,19 +615,26 @@ Module Compilers. (@under_with_unification_resultT' _ x evm _ _ F) end. - Fixpoint under_with_unification_resultT'_relation {t p evm K1 K2} + Fixpoint under_with_unification_resultT'_relation_hetero {t p evm K1 K2} + (FH : forall t, value t -> value t -> Prop) (F : K1 -> K2 -> Prop) {struct p} : @with_unification_resultT' t p evm K1 -> @with_unification_resultT' t p evm K2 -> Prop := match p return with_unification_resultT' p evm K1 -> with_unification_resultT' p evm K2 -> Prop with - | pattern.Wildcard t => fun f1 f2 => forall v, F (f1 v) (f2 v) + | pattern.Wildcard t => fun f1 f2 => forall v1 v2, FH _ v1 v2 -> F (f1 v1) (f2 v2) | pattern.Ident t idc => under_type_of_list_relation_cps F | pattern.App s d f x - => @under_with_unification_resultT'_relation + => @under_with_unification_resultT'_relation_hetero _ f evm _ _ - (@under_with_unification_resultT'_relation _ x evm _ _ F) + FH + (@under_with_unification_resultT'_relation_hetero _ x evm _ _ FH F) end. + Definition under_with_unification_resultT'_relation {t p evm K1 K2} + (F : K1 -> K2 -> Prop) + : @with_unification_resultT' t p evm K1 -> @with_unification_resultT' t p evm K2 -> Prop + := @under_with_unification_resultT'_relation_hetero t p evm K1 K2 (fun _ => eq) F. + Definition ident_collect_vars := (fun t idc => fold_right PositiveSet.union PositiveSet.empty (List.map pattern.type.collect_vars (type_vars_of_pident t idc))). Definition with_unification_resultT {t} (p : pattern t) (K : type -> Type) : Type @@ -633,8 +650,15 @@ Module Compilers. := pattern.type.under_forall_vars (fun evm => under_with_unification_resultT' (F evm)). + Definition under_with_unification_resultT_relation_hetero {t p K1 K2} + (FH : forall t, value t -> value t -> Prop) + (F : forall evm, K1 (pattern.type.subst_default t evm) -> K2 (pattern.type.subst_default t evm) -> Prop) + : @with_unification_resultT t p K1 -> @with_unification_resultT t p K2 -> Prop + := pattern.type.under_forall_vars_relation + (fun evm => under_with_unification_resultT'_relation_hetero FH (F evm)). + Definition under_with_unification_resultT_relation {t p K1 K2} - (F : forall evm, K1 (pattern.type.subst_default t evm) -> K2 (pattern.type.subst_default t evm) -> Prop) + (F : forall evm, K1 (pattern.type.subst_default t evm) -> K2 (pattern.type.subst_default t evm) -> Prop) : @with_unification_resultT t p K1 -> @with_unification_resultT t p K2 -> Prop := pattern.type.under_forall_vars_relation (fun evm => under_with_unification_resultT'_relation (F evm)). diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/Experiments/NewPipeline/RewriterRulesGood.v index 4e5c79cae..978c49189 100644 --- a/src/Experiments/NewPipeline/RewriterRulesGood.v +++ b/src/Experiments/NewPipeline/RewriterRulesGood.v @@ -19,6 +19,7 @@ Require Import Crypto.Util.Tactics.RewriteHyp. Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Prod. Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.ListUtil.ForallIn. Require Import Crypto.Util.Option. Require Import Crypto.Util.CPSNotations. Require Import Crypto.Util.HProp. @@ -190,39 +191,6 @@ Module Compilers. (nat_rect (fun _ => @Compile.value base.type ident var2 (type.base A -> type.base B)) O2 S2 n). Proof. induction n; cbn [nat_rect]; auto. Qed. - (** TODO: MOVE ME? *) - Lemma fold_right_impl_Proper {A} {P Q : A -> Prop} ls (concl1 concl2 : Prop) - (Hconcl : concl1 -> concl2) - (HPQ : forall a, In a ls -> Q a -> P a) - : fold_right (fun a (concl : Prop) => P a -> concl) concl1 ls - -> fold_right (fun a (concl : Prop) => Q a -> concl) concl2 ls. - Proof. induction ls as [|x xs IHxs]; cbn [fold_right In] in *; intuition. Qed. - - Lemma forall_In_existT {A P} {Q : forall a : A, P a -> Prop} ls - : fold_right - (fun xp (concl : Prop) - => Q (projT1 xp) (projT2 xp) -> concl) - (forall x p, In (@existT A P x p) ls -> Q x p) - ls. - Proof. - induction ls as [|x xs IHxs]; cbn [fold_right In]; intros; - destruct_head' False; destruct_head'_or. - eapply fold_right_impl_Proper; [ | | refine IHxs ]; intuition (subst; eauto). - Qed. - - (** TODO: MOVE ME? *) - Lemma forall_In_pair_existT {A A' P P'} {Q : forall (a : A) (a' : A'), P a -> P' a' -> Prop} ls - : fold_right - (fun xp_x'p' (concl : Prop) - => Q (projT1 (fst xp_x'p')) (projT1 (snd xp_x'p')) (projT2 (fst xp_x'p')) (projT2 (snd xp_x'p')) -> concl) - (forall x p x' p', In (@existT A P x p, @existT A' P' x' p') ls -> Q x x' p p') - ls. - Proof. - induction ls as [|x xs IHxs]; cbn [fold_right In]; intros; - destruct_head' False; destruct_head'_prod; destruct_head'_or; intros. - eapply fold_right_impl_Proper; [ | | refine IHxs ]; intuition (inversion_prod; subst; eauto). - Qed. - Local Ltac start_good := split; [ reflexivity | ]; lazymatch goal with |