diff options
Diffstat (limited to 'src/PushButtonSynthesis/ReificationCache.v')
-rw-r--r-- | src/PushButtonSynthesis/ReificationCache.v | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/src/PushButtonSynthesis/ReificationCache.v b/src/PushButtonSynthesis/ReificationCache.v new file mode 100644 index 000000000..ba8488820 --- /dev/null +++ b/src/PushButtonSynthesis/ReificationCache.v @@ -0,0 +1,61 @@ +(** * Reification Cache *) +(** This file defines the cache that holds reified versions of + operations, as well as the tactics that reify and apply things + from the cache. *) +Require Import Coq.Relations.Relation_Definitions. +Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Util.Tactics.SubstEvars. +Require Import Crypto.Language. +Require Import Crypto.LanguageWf. + +Import + Language.Compilers + LanguageWf.Compilers. + +Import Compilers.defaults. + +Fixpoint pointwise_equal {t} : relation (type.interp base.interp t) + := match t with + | type.base t => Logic.eq + | type.arrow s d + => fun (f g : type.interp base.interp s -> type.interp base.interp d) + => forall x, pointwise_equal (f x) (g x) + end. + +Definition is_reification_of' {t} (e : Expr t) (v : type.interp base.interp t) : Prop + := pointwise_equal (Interp e) v /\ Wf e. + +Notation is_reification_of rop op + := (ltac:(let T := constr:(@is_reification_of' (reify_type_of op) rop op) in + let T := (eval cbv [pointwise_equal is_reification_of'] in T) in + let T := (eval cbn [type.interp base.interp base.base_interp] in T) in + exact T)) + (only parsing). + +Ltac cache_reify _ := + split; + [ intros; + etransitivity; + [ + | repeat match goal with |- _ = ?f' ?x => is_var x; apply (f_equal (fun f => f _)) end; + Reify_rhs (); + reflexivity ]; + subst_evars; + reflexivity + | prove_Wf () ]. + +Ltac apply_cached_reification op lem := + lazymatch goal with + | [ |- _ = ?RHS ] + => let f := head RHS in + constr_eq f op; + simple apply lem + end. + +Create HintDb reify_gen_cache discriminated. +Create HintDb wf_gen_cache discriminated. + +Module Export Hints. + Hint Resolve conj : reify_gen_cache wf_gen_cache. + Hint Unfold Wf : wf_gen_cache. +End Hints. |