diff options
| -rw-r--r-- | src/Experiments/NewPipeline/AbstractInterpretation.v | 25 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/AbstractInterpretationProofs.v | 16 |
2 files changed, 4 insertions, 37 deletions
diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/Experiments/NewPipeline/AbstractInterpretation.v index 8f55400a3..e6ca7ebc8 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretation.v +++ b/src/Experiments/NewPipeline/AbstractInterpretation.v @@ -913,25 +913,8 @@ Module Compilers. : @expr var t := @eta_expand_with_bound' base.type ident var abstract_domain' annotate bottom' t e st. - Section extract. - Local Notation bottom := (@bottom base.type abstract_domain' bottom'). - Definition ident_extract {t} (idc : ident t) : abstract_domain t - := match idc in ident.ident t return abstract_domain t with - | ident.Literal _ _ as idc - | ident.nil _ as idc - | ident.cons _ as idc - | ident.pair _ _ as idc - => abstract_interp_ident _ idc - | ident.Z_cast _ as idc - | ident.Z_cast2 _ as idc - => (* fast-path for cast: don't bother with the abstract state of the argument *) - fun _ => abstract_interp_ident _ idc (bottom' _) - | _ => bottom - end. - - Definition extract {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t) - := @extract_gen base.type ident abstract_domain' (@ident_extract) t e bound. - End extract. + Definition extract {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t) + := @extract_gen base.type ident abstract_domain' abstract_interp_ident t e bound. End with_var. End ident. @@ -999,9 +982,9 @@ Module Compilers. Definition EtaExpandWithListInfoFromBound {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t := EtaExpandWithBound e (type.map_for_each_lhs_of_arrow (@ZRange.type.option.strip_ranges) bound). Definition extract {t} (e : expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t) - := @partial.ident.extract abstract_domain' bottom' abstract_interp_ident t e bound. + := @partial.ident.extract abstract_domain' abstract_interp_ident t e bound. Definition Extract {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t) - := @partial.ident.extract abstract_domain' bottom' abstract_interp_ident t (e _) bound. + := @partial.ident.extract abstract_domain' abstract_interp_ident t (e _) bound. End specialized. End partial. diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v index f806aea25..8a5905d92 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v +++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v @@ -759,22 +759,6 @@ Module Compilers. Qed. Section extract. - Local Notation ident_extract := (@ident.ident_extract abstract_domain' bottom' abstract_interp_ident). - Global Instance ident_extract_Proper {t} - : Proper (eq ==> abstract_domain_R) (@ident_extract t). - Proof. - intros idc idc' ?; subst idc'. - destruct idc; cbn [ident.ident_extract]; - repeat first [ refine (abstract_interp_ident_Proper _ _ _ eq_refl) - | eapply bottom_Proper - | eapply bottom'_Proper - | progress cbn [type.related abstract_domain'_R] - | progress cbv [respectful] - | progress intros - | refine (abstract_interp_ident_Proper (type.arrow (type.base _) (type.base _)) _ _ eq_refl _ _ _) - | progress cbv [type.related abstract_domain_R] ]. - Qed. - (* Definition extract {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t) := @extract_gen base.type ident abstract_domain' (@ident_extract) t e bound. |