blob: bd39b48a06cff7a354597bcedd1fc17087081bb7 (
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
|
(** * Inline: Remove some [Let] expressions *)
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.SmartMap.
Local Open Scope ctype_scope.
Section language.
Context {base_type_code : Type}
{op : flat_type base_type_code -> flat_type base_type_code -> Type}.
Local Notation flat_type := (flat_type base_type_code).
Local Notation type := (type base_type_code).
Let Tbase := @Tbase base_type_code.
Local Coercion Tbase : base_type_code >-> Syntax.flat_type.
Local Notation exprf := (@exprf base_type_code op).
Local Notation expr := (@expr base_type_code op).
Local Notation Expr := (@Expr base_type_code op).
Section with_var.
Context {var : base_type_code -> Type}.
Inductive inline_directive : flat_type -> Type :=
| default_inline {t} (e : @exprf var t) : inline_directive t
| inline {t} (e : interp_flat_type (fun t => @exprf var (Tbase t)) t) : inline_directive t
| no_inline {t} (e : @exprf var t) : inline_directive t
| partial_inline
{tx tC}
(ex : @exprf var tx)
(eC : interp_flat_type var tx -> interp_flat_type (fun t => @exprf var (Tbase t)) tC)
: inline_directive tC.
Definition exprf_of_inline_directive {t} (v : inline_directive t) : @exprf var t
:= match v with
| default_inline t e => e
| inline t e => SmartPairf e
| no_inline t e => e
| partial_inline _ _ ex eC
=> LetIn ex (fun x => SmartPairf (eC x))
end.
Context (postprocess : forall {t}, @exprf var t -> inline_directive t).
Fixpoint inline_const_genf {t} (e : @exprf (@exprf var) t) : @exprf var t
:= match e in Syntax.exprf _ _ t return @exprf var t with
| LetIn tx ex tC eC
=> match postprocess _ (@inline_const_genf _ ex) in inline_directive t' return (interp_flat_type _ t' -> @exprf var tC) -> @exprf var tC with
| default_inline _ ex
=> match ex in Syntax.exprf _ _ t' return (interp_flat_type _ t' -> @exprf var tC) -> @exprf var tC with
| TT => fun eC => eC tt
| Var _ x => fun eC => eC (Var x)
| ex => fun eC => LetIn ex (fun x => eC (SmartVarVarf x))
end
| no_inline _ ex
=> fun eC => LetIn ex (fun x => eC (SmartVarVarf x))
| inline _ ex => fun eC => eC ex
| partial_inline _ _ ex eC'
=> fun eC => LetIn ex (fun x => eC (eC' x))
end (fun x => @inline_const_genf _ (eC x))
| Var _ x => x
| TT => TT
| Pair _ ex _ ey => Pair (@inline_const_genf _ ex) (@inline_const_genf _ ey)
| Op _ _ op args => Op op (@inline_const_genf _ args)
end.
Definition inline_const_gen {t} (e : @expr (@exprf var) t) : @expr var t
:= match e in Syntax.expr _ _ t return @expr var t with
| Abs _ _ f => Abs (fun x => inline_const_genf (f (SmartVarVarf x)))
end.
Section with_is_const.
Context (is_const : forall s d, op s d -> bool).
Definition postprocess_for_const (t : flat_type) (v : @exprf var t) : inline_directive t
:= if match v with Op _ _ op _ => @is_const _ _ op | _ => false end
then match t return @exprf _ t -> inline_directive t with
| Syntax.Tbase _ => @inline (Tbase _)
| _ => @default_inline _
end v
else default_inline v.
End with_is_const.
End with_var.
Definition inline_constf is_const {var t}
:= @inline_const_genf var (postprocess_for_const is_const) t.
Definition inline_const is_const {var t}
:= @inline_const_gen var (postprocess_for_const is_const) t.
Definition InlineConstGen (postprocess : forall var t, @exprf var t -> @inline_directive var t)
{t} (e : Expr t) : Expr t
:= fun var => inline_const_gen (postprocess _) (e _).
Definition InlineConst is_const {t}
:= @InlineConstGen (fun var => postprocess_for_const is_const) t.
End language.
Global Arguments inline_directive {_} _ _ _, {_ _ _} _.
Global Arguments no_inline {_ _ _ _} _.
Global Arguments inline {_ _ _ _} _.
Global Arguments default_inline {_ _ _ _} _.
Global Arguments partial_inline {_ _ _ _ _} ex eC.
Global Arguments inline_const_genf {_ _ _} postprocess {_} _.
Global Arguments inline_const_gen {_ _ _} postprocess {_} _.
Global Arguments InlineConstGen {_ _} postprocess {_} _ var.
Global Arguments inline_constf {_ _} is_const {_ t} _.
Global Arguments inline_const {_ _} is_const {_ t} _.
Global Arguments InlineConst {_ _} is_const {_} _ var.
|
