blob: c2ae24f7cc67cacbe62ffaab0248ad1cffe4050a (
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
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
(** * Push-Button Synthesis: Legacy Synthesis Tactics *)
Require Import Coq.Classes.Morphisms.
Require Import Crypto.LanguageWf.
Require Import Crypto.Language.
Require Import Crypto.PushButtonSynthesis.ReificationCache.
Require Import Crypto.Util.Equality. (* fg_equal_rel *)
Require Import Crypto.Util.Tactics.SubstEvars.
Require Import Crypto.Util.Tactics.GetGoal.
Import
LanguageWf.Compilers
Language.Compilers.
Import Compilers.defaults.
(** TODO: Port Barrett and Montgomery to the new glue style, and remove these tactics. These tactics are only needed for the old-glue-style derivations. *)
Ltac peel_interp_app _ :=
lazymatch goal with
| [ |- ?R' (?InterpE ?arg) (?f ?arg) ]
=> apply fg_equal_rel; [ | reflexivity ];
try peel_interp_app ()
| [ |- ?R' (Interp ?ev) (?f ?x) ]
=> let sv := type of x in
let fx := constr:(f x) in
let dv := type of fx in
let rs := reify_type sv in
let rd := reify_type dv in
etransitivity;
[ apply @expr.Interp_APP_rel_reflexive with (s:=rs) (d:=rd) (R:=R');
typeclasses eauto
| apply fg_equal_rel;
[ try peel_interp_app ()
| try lazymatch goal with
| [ |- ?R (Interp ?ev) (Interp _) ]
=> reflexivity
| [ |- ?R (Interp ?ev) ?c ]
=> let rc := constr:(GallinaReify.Reify c) in
unify ev rc; vm_compute; reflexivity
end ] ]
end.
Ltac pre_cache_reify _ :=
let H' := fresh in
lazymatch goal with
| [ |- ?P /\ Wf ?e ]
=> let P' := fresh in
evar (P' : Prop);
assert (H' : P' /\ Wf e); subst P'
end;
[
| split; [ destruct H' as [H' _] | destruct H' as [_ H']; exact H' ];
cbv [type.app_curried];
let arg := fresh "arg" in
let arg2 := fresh in
intros arg arg2;
cbn [type.and_for_each_lhs_of_arrow type.eqv];
let H := fresh in
intro H;
repeat match type of H with
| and _ _ => let H' := fresh in
destruct H as [H' H];
rewrite <- H'
end;
clear dependent arg2; clear H;
intros _;
peel_interp_app ();
[ lazymatch goal with
| [ |- ?R (Interp ?ev) _ ]
=> (tryif is_evar ev
then let ev' := fresh "ev" in set (ev' := ev)
else idtac)
end;
cbv [pointwise_relation];
repeat lazymatch goal with
| [ H : _ |- _ ] => first [ constr_eq H H'; fail 1
| revert H ]
end;
eexact H'
| .. ] ];
[ intros; clear | .. ].
Ltac do_inline_cache_reify do_if_not_cached :=
pre_cache_reify ();
[ try solve [
cbv beta zeta;
repeat match goal with H := ?e |- _ => is_evar e; subst H end;
try solve [ split; [ solve [ eauto with nocore reify_gen_cache ] | solve [ eauto with wf_gen_cache; prove_Wf () ] ] ];
do_if_not_cached ()
];
cache_reify ()
| .. ].
(* TODO: MOVE ME *)
Ltac vm_compute_lhs_reflexivity :=
lazymatch goal with
| [ |- ?LHS = ?RHS ]
=> let x := (eval vm_compute in LHS) in
(* we cannot use the unify tactic, which just gives "not
unifiable" as the error message, because we want to see the
terms that were not unifable. See also
COQBUG(https://github.com/coq/coq/issues/7291) *)
let _unify := constr:(ltac:(reflexivity) : RHS = x) in
vm_cast_no_check (eq_refl x)
end.
Ltac solve_rop' rop_correct do_if_not_cached machine_wordsizev :=
eapply rop_correct with (machine_wordsize:=machine_wordsizev);
[ do_inline_cache_reify do_if_not_cached
| subst_evars; vm_compute_lhs_reflexivity (* lazy; reflexivity *) ].
Ltac solve_rop_nocache rop_correct :=
solve_rop' rop_correct ltac:(fun _ => idtac).
Ltac solve_rop rop_correct :=
solve_rop'
rop_correct
ltac:(fun _ => let G := get_goal in fail 2 "Could not find a solution in reify_gen_cache for" G).
|
