blob: 92338dcfb27b7ece4ede36337b45542c2bd8f8da (
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
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Z.Syntax.
Require Import Crypto.Compilers.TypeInversion.
Require Import Crypto.Util.FixCoqMistakes.
Section language.
Section flat.
Context (P : flat_type base_type -> Type).
Local Ltac t :=
let H := fresh in
intro H; intros;
match goal with
| [ p : _ |- _ ] => specialize (H _ p)
end;
cbv beta iota in *;
try specialize (H eq_refl); simpl in *;
try assumption.
Definition preinvert_TbaseTZ (Q : P (Tbase TZ) -> Type)
: (forall t (p : P t), match t return P t -> Type with Tbase TZ => Q | _ => fun _ => True end p)
-> forall p, Q p.
Proof. t. Defined.
Definition preinvert_TbaseTWord (Q : forall t, P (Tbase (TWord t)) -> Type)
: (forall t (p : P t), match t return P t -> Type with Tbase (TWord _) => Q _ | _ => fun _ => True end p)
-> forall t p, Q t p.
Proof. t. Defined.
End flat.
End language.
Ltac preinvert_one_type e :=
lazymatch type of e with
| ?P (Tbase TZ)
=> revert dependent e;
refine (preinvert_TbaseTZ P _ _)
| ?P (Tbase (TWord ?T))
=> is_var T;
move e at top;
revert dependent T;
refine (preinvert_TbaseTWord P _ _)
| _ => Compilers.TypeInversion.preinvert_one_type e
end.
|
