Source file optimizations.ml
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
open Utils
open Ast
let ( let+ ) x f = Bindlib.box_apply f x
let ( and+ ) x y = Bindlib.box_pair x y
let visitor_map (t : 'a -> expr Pos.marked -> expr Pos.marked Bindlib.box) (ctx : 'a)
(e : expr Pos.marked) : expr Pos.marked Bindlib.box =
let default_mark e' = Pos.same_pos_as e' e in
match Pos.unmark e with
| EVar (v, pos) ->
let+ v = Bindlib.box_var v in
(v, pos)
| ETuple (args, n) ->
let+ args = args |> List.map (t ctx) |> Bindlib.box_list in
default_mark @@ ETuple (args, n)
| ETupleAccess (e1, i, n, ts) ->
let+ e1 = t ctx e1 in
default_mark @@ ETupleAccess (e1, i, n, ts)
| EInj (e1, i, n, ts) ->
let+ e1 = t ctx e1 in
default_mark @@ EInj (e1, i, n, ts)
| EMatch (arg, cases, n) ->
let+ arg = t ctx arg and+ cases = cases |> List.map (t ctx) |> Bindlib.box_list in
default_mark @@ EMatch (arg, cases, n)
| EArray args ->
let+ args = args |> List.map (t ctx) |> Bindlib.box_list in
default_mark @@ EArray args
| EAbs ((binder, pos_binder), ts) ->
let vars, body = Bindlib.unmbind binder in
let body = t ctx body in
let+ binder = Bindlib.bind_mvar vars body in
default_mark @@ EAbs ((binder, pos_binder), ts)
| EApp (e1, args) ->
let+ e1 = t ctx e1 and+ args = args |> List.map (t ctx) |> Bindlib.box_list in
default_mark @@ EApp (e1, args)
| EAssert e1 ->
let+ e1 = t ctx e1 in
default_mark @@ EAssert e1
| EIfThenElse (e1, e2, e3) ->
let+ e1 = t ctx e1 and+ e2 = t ctx e2 and+ e3 = t ctx e3 in
default_mark @@ EIfThenElse (e1, e2, e3)
| ECatch (e1, exn, e2) ->
let+ e1 = t ctx e1 and+ e2 = t ctx e2 in
default_mark @@ ECatch (e1, exn, e2)
| ERaise _ | ELit _ | EOp _ -> Bindlib.box e
let rec iota_expr (_ : unit) (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
let default_mark e' = Pos.mark (Pos.get_position e) e' in
match Pos.unmark e with
| EMatch ((EInj (e1, i, n', _ts), _), cases, n) when Dcalc.Ast.EnumName.compare n n' = 0 ->
let+ e1 = visitor_map iota_expr () e1
and+ case = visitor_map iota_expr () (List.nth cases i) in
default_mark @@ EApp (case, [ e1 ])
| EMatch (e', cases, n)
when cases
|> List.mapi (fun i (case, _pos) ->
match case with
| EInj (_ei, i', n', _ts') ->
i = i' && Dcalc.Ast.EnumName.compare n n' = 0
| _ -> false)
|> List.for_all Fun.id ->
visitor_map iota_expr () e'
| _ -> visitor_map iota_expr () e
let rec beta_expr (_ : unit) (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
let default_mark e' = Pos.same_pos_as e' e in
match Pos.unmark e with
| EApp (e1, args) -> (
let+ e1 = beta_expr () e1 and+ args = List.map (beta_expr ()) args |> Bindlib.box_list in
match Pos.unmark e1 with
| EAbs ((binder, _pos_binder), _ts) ->
let (_ : (_, _) Bindlib.mbinder) = binder in
Bindlib.msubst binder (List.map fst args |> Array.of_list)
| _ -> default_mark @@ EApp (e1, args))
| _ -> visitor_map beta_expr () e
let iota_optimizations (p : program) : program =
{
p with
scopes =
List.map
(fun scope_body ->
{
scope_body with
scope_body_expr = Bindlib.unbox (iota_expr () scope_body.scope_body_expr);
})
p.scopes;
}
let _beta_optimizations (p : program) : program =
{
p with
scopes =
List.map
(fun scope_body ->
{
scope_body with
scope_body_expr = Bindlib.unbox (beta_expr () scope_body.scope_body_expr);
})
p.scopes;
}
let rec peephole_expr (_ : unit) (e : expr Pos.marked) : expr Pos.marked Bindlib.box =
let default_mark e' = Pos.mark (Pos.get_position e) e' in
match Pos.unmark e with
| EIfThenElse (e1, e2, e3) -> (
let+ e1 = peephole_expr () e1 and+ e2 = peephole_expr () e2 and+ e3 = peephole_expr () e3 in
match Pos.unmark e1 with
| ELit (LBool true) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool true), _) ]) -> e2
| ELit (LBool false) | EApp ((EOp (Unop (Log _)), _), [ (ELit (LBool false), _) ]) -> e3
| _ -> default_mark @@ EIfThenElse (e1, e2, e3))
| _ -> visitor_map peephole_expr () e
let peephole_optimizations (p : program) : program =
{
p with
scopes =
List.map
(fun scope_body ->
{
scope_body with
scope_body_expr = Bindlib.unbox (peephole_expr () scope_body.scope_body_expr);
})
p.scopes;
}
let optimize_program (p : program) : program = p |> iota_optimizations |> peephole_optimizations