blob: 22fd16cbbdb6e875dc910aa0b274904d1f4e68cd (
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
|
Require Import Crypto.Language.
Require Import Crypto.LanguageInversion.
Require Import Crypto.LanguageWf.
Require Import Crypto.UnderLetsProofs.
Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs.
Require Import Crypto.Rewriter.
Require Import Crypto.RewriterWf1.
Require Import Crypto.RewriterWf2.
Require Import Crypto.RewriterInterpProofs1.
Require Import Crypto.Util.Tactics.CacheTerm.
Require Import Crypto.Util.Tactics.ConstrFail.
Module Compilers.
Import LanguageWf.Compilers.
Import GENERATEDIdentifiersWithoutTypes.Compilers.
Import GENERATEDIdentifiersWithoutTypesProofs.Compilers.
Import Rewriter.Compilers.RewriteRules.
Import RewriterWf1.Compilers.RewriteRules.
Import RewriterWf2.Compilers.RewriteRules.
Import RewriterInterpProofs1.Compilers.RewriteRules.
Import Rewriter.Compilers.RewriteRules.GoalType.
Import RewriterWf1.Compilers.RewriteRules.GoalType.
Import RewriterWf1.Compilers.RewriteRules.WfTactics.GoalType.
Import RewriterWf1.Compilers.RewriteRules.InterpTactics.GoalType.
Import RewriterWf1.Compilers.RewriteRules.WfTactics.Tactic.
Import RewriterWf1.Compilers.RewriteRules.InterpTactics.Tactic.
Module Import RewriteRules.
Definition VerifiedRewriter_of_Rewriter
(R : RewriterT)
(RWf : Wf_GoalT R)
(RInterp : Interp_GoalT R)
(RProofs : PrimitiveHList.hlist
(@snd bool Prop)
(List.skipn (dummy_count (Rewriter_data R)) (rewrite_rules_specs (Rewriter_data R))))
: VerifiedRewriter.
Proof.
simple refine
(let HWf := _ in
let HInterp_gen := _ in
@Build_VerifiedRewriter (@Rewriter.Compilers.RewriteRules.GoalType.Rewrite R) HWf HInterp_gen (HInterp_gen _));
[ | clear HWf ]; intros.
all: abstract (
rewrite Rewrite_eq; cbv [Make.Rewrite]; rewrite rewrite_head_eq, all_rewrite_rules_eq;
first [ apply Compile.Wf_Rewrite; [ | assumption ];
let wf_do_again := fresh "wf_do_again" in
(intros ? ? ? ? wf_do_again ? ?);
eapply @Compile.wf_assemble_identifier_rewriters;
eauto using
pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct
with nocore;
try reflexivity
| eapply Compile.InterpRewrite; [ | assumption ];
intros; eapply Compile.interp_assemble_identifier_rewriters with (pident_to_typed:=@pattern.ident.to_typed);
eauto using
pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct, pattern.ident.unify_to_typed,
@ident.gen_interp_Proper, eq_refl
with nocore ]).
Defined.
Ltac make_VerifiedRewriter R RWf RInterp RProofs :=
let res := (eval hnf in (@VerifiedRewriter_of_Rewriter R RWf RInterp RProofs)) in
let res := lazymatch res with
| context Res[@Build_VerifiedRewriter ?R]
=> let t := fresh "t" in
let R' := fresh in
let R' := constr:(fun t
=> match R t return _ with
| R' => ltac:(let v := (eval hnf in R') in exact v)
end) in
context Res[@Build_VerifiedRewriter R']
end in
res.
Ltac Build_Rewriter include_interp specs_proofs :=
let specs := lazymatch type of specs_proofs with
| PrimitiveHList.hlist (@snd bool Prop) ?specs => specs
| ?T
=> let expected_type := uconstr:(PrimitiveHList.hlist (@snd bool Prop) ?[specs]) in
constr_fail_with ltac:(fun _ => fail 1 "Invalid type for specs_proofs:" T "Expected:" expected_type)
end in
let R_name := fresh "Rewriter_data" in
let R := Build_RewriterT include_interp specs in
let R := cache_term R R_name in
let Rwf := fresh "Rewriter_Wf" in
let Rwf := cache_proof_with_type_by (Wf_GoalT R) ltac:(idtac; prove_good ()) Rwf in
let RInterp := fresh "Rewriter_Interp" in
let RInterp := cache_proof_with_type_by (Interp_GoalT R) ltac:(idtac; prove_interp_good ()) RInterp in
make_VerifiedRewriter R Rwf RInterp specs_proofs.
Module Export GoalType.
Export RewriterWf1.Compilers.RewriteRules.GoalType.
End GoalType.
Module Export Tactic.
Module Export Settings.
Export Rewriter.Compilers.RewriteRules.Tactic.Settings.
End Settings.
Ltac make_rewriter include_interp specs_proofs :=
let res := Build_Rewriter include_interp specs_proofs in refine res.
Tactic Notation "make_rewriter" constr(include_interp) constr(specs_proofs) :=
make_rewriter include_interp specs_proofs.
End Tactic.
End RewriteRules.
End Compilers.
|
