blob: 2b15616fedaea356e184e53a9cea607da6c3a3a1 (
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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
|
Require Import Crypto.Util.Sigma.Lift.
Require Import Crypto.Util.Sigma.Associativity.
Require Import Crypto.Util.Sigma.MapProjections.
Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon.
Require Import Crypto.Compilers.Z.Bounds.Interpretation.
Require Import Crypto.Compilers.Eta.
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Util.LetIn.
Require Import Crypto.Util.FixedWordSizes.
Require Import Crypto.Compilers.Syntax.
Require Export Crypto.Util.Notations.
Global Arguments Pos.to_nat !_ / .
Ltac display_helper_gen f make_hole :=
let display_helper f := display_helper_gen f make_hole in
let do_make_hole _ :=
match goal with
| [ |- ?T ] => let h := make_hole T in
refine h
end in
let t := type of f in
lazymatch (eval hnf in t) with
| forall _ : ?A, ?B
=> let x := fresh "x" in
lazymatch (eval hnf in A) with
| @sig ?A ?P
=> lazymatch (eval hnf in A) with
| sig _
=> let f' := constr:(fun x : A => f (exist P x ltac:(do_make_hole ()))) in
display_helper f'
| _
=> refine (fun x : A => _);
let f' := constr:(f (exist P x ltac:(do_make_hole ()))) in
display_helper f'
end
| _
=> lazymatch A with
| prod ?A ?B
=> let f' := constr:(fun (a : A) (b : B) => f (a, b)%core) in
display_helper f'
| _
=> refine (fun x : A => _);
let f' := constr:(f x) in
display_helper f'
end
end
| @sig ?A _
=> lazymatch (eval hnf in A) with
| sig _ => display_helper (proj1_sig f)
| _ => refine (proj1_sig f)
end
| _
=> lazymatch t with
| prod _ _
=> let a := fresh "a" in
let b := fresh "b" in
refine (let (a, b) := f in
pair _ _);
[ display_helper a | display_helper b ]
| _ => refine f
end
end.
Ltac display_helper f := display_helper_gen f ltac:(fun T => open_constr:(_)).
Ltac display_helper_with_admit f :=
constr:(fun admit : forall T, T
=> ltac:(display_helper_gen f ltac:(fun T => constr:(admit T)))).
Ltac try_strip_admit f :=
lazymatch f with
| fun _ : forall T, T => ?P => P
| ?P => P
end.
Ltac refine_display f :=
let do_red F := (eval cbv [f
proj1_sig fst snd
Tuple.map Tuple.map'
Lift.lift1_sig Lift.lift2_sig Lift.lift3_sig Lift.lift4_sig Lift.lift4_sig_sig
MapProjections.proj2_sig_map Associativity.sig_sig_assoc
sig_conj_by_impl2
sig_eq_trans_exist1 sig_R_trans_exist1 sig_eq_trans_rewrite_fun_exist1
sig_R_trans_rewrite_fun_exist1
adjust_tuple2_tuple2_sig
Tuple.tuple Tuple.tuple'
FixedWordSizes.wordT FixedWordSizes.word_case FixedWordSizes.ZToWord FixedWordSizes.word_case_dep
Bounds.actual_logsz Bounds.round_up_to_in_list Bounds.option_min
List.map List.filter List.fold_right List.fold_left
Nat.leb Nat.min
PeanoNat.Nat.log2 PeanoNat.Nat.log2_iter PeanoNat.Nat.pred
Bounds.bounds_to_base_type
interp_flat_type
Z.leb Z.compare Pos.compare Pos.compare_cont
ZRange.lower ZRange.upper
BinPos.Pos.to_nat PeanoNat.Nat.pow
] in F) in
let ret := display_helper_with_admit (proj1_sig f) in
let ret := do_red ret in
let ret := lazymatch ret with
| context[match ?sz with O => _ | _ => _ end] => (eval cbv [sz] in ret)
| _ => ret
end in
let ret := (eval simpl @Z.to_nat in ret) in
let ret := (eval cbv [interp_flat_type] in ret) in
let ret := try_strip_admit ret in
refine ret.
Tactic Notation "display" open_constr(f) :=
refine_display f.
Notation display f := (ltac:(let v := f in display v)) (only parsing).
(** Some helper tactics for actually pulling out the expression *)
Ltac strip_InterpEta term :=
let retype e :=
lazymatch type of e with
| forall var, @Syntax.expr ?base_type_code ?op var ?T
=> constr:(e : @Syntax.Expr base_type_code op T)
| _ => e
end in
lazymatch term with
| fun x : ?T => ?P
=> let maybe_x := fresh x in
let probably_not_x := fresh maybe_x in
let not_x := fresh probably_not_x in
lazymatch
constr:(fun x : T
=> match P with
| not_x => ltac:(let v := (eval cbv delta [not_x] in not_x) in
let v' := strip_InterpEta v in
exact v')
end)
with
| fun _ => ?P => retype P
| ?P => retype P
end
| @Eta.InterpEta _ _ _ _ _ ?e
=> e
| @Eta.InterpEta _ _ _ _ _ ?e _
=> e
| let (a, b) := ?f in _
=> f
| _ => let dummy := match goal with
| _ => fail 1 "strip_InterpEta:" term
end in
I
end.
Ltac extract_Expr f :=
let k := constr:(ltac:(refine_display f)) in
let k := strip_InterpEta k in
k.
Notation extract_Expr f := (ltac:(let v := f in let v := extract_Expr v in refine v)) (only parsing).
|
