blob: 88e38fbf6200094c5af85a559288dce1a630a366 (
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
|
(** * Definition of the output type of the post-Wf pipeline *)
(** Do not change these definitions unless you're hacking on the
entire reflective pipeline tactic automation. *)
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.SmartMap.
Require Import Crypto.Compilers.Z.Syntax.
Require Import Crypto.Compilers.Z.Bounds.Interpretation.
Require Import Crypto.Util.Sigma.
Require Import Crypto.Util.Prod.
Section with_round_up_list.
Context {allowable_lgsz : list nat}.
Local Notation pick_typeb := (@Bounds.bounds_to_base_type (Bounds.round_up_to_in_list allowable_lgsz)) (only parsing).
Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v).
Record ProcessedReflectivePackage
:= { InputType : _;
input_expr : Expr base_type op InputType;
input_bounds : interp_flat_type Bounds.interp_base_type (domain InputType);
output_bounds :> interp_flat_type Bounds.interp_base_type (codomain InputType);
output_expr :> Expr base_type op (Arrow (pick_type input_bounds) (pick_type output_bounds)) }.
Definition Build_ProcessedReflectivePackage_from_option_sigma
{t} (e : Expr base_type op t)
(input_bounds : interp_flat_type Bounds.interp_base_type (domain t))
(result : option { output_bounds : interp_flat_type Bounds.interp_base_type (codomain t)
& Expr base_type op (Arrow (pick_type input_bounds) (pick_type output_bounds)) })
: option ProcessedReflectivePackage
:= option_map
(fun be
=> let 'existT b e' := be in
{| InputType := t ; input_expr := e ; input_bounds := input_bounds ; output_bounds := b ; output_expr := e' |})
result.
Definition ProcessedReflectivePackage_to_sigT (x : ProcessedReflectivePackage)
: { InputType : _
& Expr base_type op InputType
* { bounds : interp_flat_type Bounds.interp_base_type (domain InputType)
* interp_flat_type Bounds.interp_base_type (codomain InputType)
& Expr base_type op (Arrow (pick_type (fst bounds)) (pick_type (snd bounds))) } }%type
:= let (a, b, c, d, e) := x in
existT _ a (b, (existT _ (c, d) e)).
End with_round_up_list.
Ltac inversion_ProcessedReflectivePackage :=
repeat match goal with
| [ H : _ = _ :> ProcessedReflectivePackage |- _ ]
=> apply (f_equal ProcessedReflectivePackage_to_sigT) in H;
cbv [ProcessedReflectivePackage_to_sigT] in H
end;
inversion_sigma; inversion_prod.
|
