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
|
Require Import Coq.ZArith.ZArith.
Require Import Coq.MSets.MSetPositive.
Require Import Coq.FSets.FMapPositive.
Require Import Crypto.Util.ListUtil Coq.Lists.List.
Require Import Crypto.Language.
Require Import Crypto.Util.Notations.
Import ListNotations. Local Open Scope Z_scope.
Module Compilers.
Export Language.Compilers.
Import invert_expr.
Import defaults.
Module Subst01.
Section with_counter.
Context {t : Type}
(one : t)
(incr : t -> t).
Local Notation PositiveMap_incr idx m
:= (PositiveMap.add idx (match PositiveMap.find idx m with
| Some n => incr n
| None => one
end) m).
Section with_ident.
Context {base_type : Type}.
Local Notation type := (type.type base_type).
Context {ident : type -> Type}.
Local Notation expr := (@expr.expr base_type ident).
(** N.B. This does not work well when let-binders are not at top-level *)
Fixpoint compute_live_counts' {t} (e : @expr (fun _ => positive) t) (cur_idx : positive) (live : PositiveMap.t _)
: positive * PositiveMap.t _
:= match e with
| expr.Var t v => (cur_idx, PositiveMap_incr v live)
| expr.Ident t idc => (cur_idx, live)
| expr.App s d f x
=> let '(idx, live) := @compute_live_counts' _ f cur_idx live in
let '(idx, live) := @compute_live_counts' _ x idx live in
(idx, live)
| expr.Abs s d f
=> let '(idx, live) := @compute_live_counts' _ (f cur_idx) (Pos.succ cur_idx) live in
(cur_idx, live)
| expr.LetIn tx tC ex eC
=> let '(idx, live) := @compute_live_counts' tC (eC cur_idx) (Pos.succ cur_idx) live in
if PositiveMap.mem cur_idx live
then @compute_live_counts' tx ex idx live
else (idx, live)
end.
Definition compute_live_counts {t} e : PositiveMap.t _ := snd (@compute_live_counts' t e 1 (PositiveMap.empty _)).
Definition ComputeLiveCounts {t} (e : expr.Expr t) := compute_live_counts (e _).
Section with_var.
Context (doing_subst : forall T1 T2, T1 -> T2 -> T1)
{var : type -> Type}
(should_subst : t -> bool)
(live : PositiveMap.t t).
Fixpoint subst0n' {t} (e : @expr (@expr var) t) (cur_idx : positive)
: positive * @expr var t
:= match e with
| expr.Var t v => (cur_idx, v)
| expr.Ident t idc => (cur_idx, expr.Ident idc)
| expr.App s d f x
=> let '(idx, f') := @subst0n' _ f cur_idx in
let '(idx, x') := @subst0n' _ x idx in
(idx, expr.App f' x')
| expr.Abs s d f
=> (cur_idx, expr.Abs (fun v => snd (@subst0n' _ (f (expr.Var v)) (Pos.succ cur_idx))))
| expr.LetIn tx tC ex eC
=> let '(idx, ex') := @subst0n' tx ex cur_idx in
let eC' := fun v => snd (@subst0n' tC (eC v) (Pos.succ cur_idx)) in
if match PositiveMap.find cur_idx live with
| Some n => should_subst n
| None => true
end
then (Pos.succ cur_idx, eC' (doing_subst _ _ ex' (Pos.succ cur_idx, PositiveMap.elements live)))
else (Pos.succ cur_idx, expr.LetIn ex' (fun v => eC' (expr.Var v)))
end.
Definition subst0n {t} e : expr t
:= snd (@subst0n' t e 1).
End with_var.
Definition Subst0n (doing_subst : forall T1 T2, T1 -> T2 -> T1) (should_subst : t -> bool) {t} (e : expr.Expr t) : expr.Expr t
:= fun var => subst0n doing_subst should_subst (ComputeLiveCounts e) (e _).
End with_ident.
End with_counter.
Section for_01.
Inductive one_or_more := one | more.
Local Notation t := one_or_more.
Let incr : t -> t := fun _ => more.
Let should_subst : t -> bool
:= fun v => match v with
| one => true
| more => false
end.
Definition Subst01 {base_type ident} {t} (e : expr.Expr t) : expr.Expr t
:= @Subst0n _ one incr base_type ident (fun _ _ x _ => x) should_subst t e.
End for_01.
End Subst01.
Module DeadCodeElimination.
Section with_ident.
Context {base_type : Type}.
Local Notation type := (type.type base_type).
Context {ident : type -> Type}.
Local Notation expr := (@expr.expr base_type ident).
Definition OUGHT_TO_BE_UNUSED {T1 T2} (v : T1) (v' : T2) := v.
Global Opaque OUGHT_TO_BE_UNUSED.
Definition EliminateDead {t} (e : expr.Expr t) : expr.Expr t
:= @Subst01.Subst0n unit tt (fun _ => tt) base_type ident (@OUGHT_TO_BE_UNUSED) (fun _ => false) t e.
End with_ident.
End DeadCodeElimination.
End Compilers.
|
