blob: 148cac04980466ef907efac2d728d3fb5addc864 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
(** * 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
:= (match @is_reification_of' (reify_type_of op) rop op with
| T
=> ltac:(
let T := (eval cbv [pointwise_equal is_reification_of' T] in T) in
let T := (eval cbn [type.interp base.interp base.base_interp] in T) in
exact T)
end)
(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.
|
