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
149
150
151
152
153
154
155
open Utils
open Ast
module D = Dcalc.Ast
let ( let+ ) x f = Bindlib.box_apply f x
let ( and+ ) x y = Bindlib.box_pair x y
let visitor_map
(t : 'a -> 'm marked_expr -> 'm marked_expr Bindlib.box)
(ctx : 'a)
(e : 'm marked_expr) : 'm marked_expr Bindlib.box =
let default_mark e' = Marked.same_mark_as e' e in
match Marked.unmark e with
| EVar v ->
let+ v = Bindlib.box_var v in
default_mark @@ v
| 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, 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, 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 : 'm marked_expr) : 'm marked_expr Bindlib.box =
let default_mark e' = Marked.mark (Marked.get_mark e) e' in
match Marked.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 : 'm marked_expr) : 'm marked_expr Bindlib.box =
let default_mark e' = Marked.same_mark_as e' e in
match Marked.unmark e with
| EApp (e1, args) -> (
let+ e1 = beta_expr () e1
and+ args = List.map (beta_expr ()) args |> Bindlib.box_list in
match Marked.unmark e1 with
| EAbs (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 : 'm program) : 'm program =
let new_scopes =
Dcalc.Ast.map_exprs_in_scopes ~f:(iota_expr ()) ~varf:(fun v -> v) p.scopes
in
{ p with D.scopes = Bindlib.unbox new_scopes }
let _beta_optimizations (p : 'm program) : 'm program =
let new_scopes =
Dcalc.Ast.map_exprs_in_scopes ~f:(beta_expr ()) ~varf:(fun v -> v) p.scopes
in
{ p with scopes = Bindlib.unbox new_scopes }
let rec peephole_expr (_ : unit) (e : 'm marked_expr) :
'm marked_expr Bindlib.box =
let default_mark e' = Marked.mark (Marked.get_mark e) e' in
match Marked.unmark e with
| EIfThenElse (e1, e2, e3) -> (
let+ e1 = peephole_expr () e1
and+ e2 = peephole_expr () e2
and+ e3 = peephole_expr () e3 in
match Marked.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))
| ECatch (e1, except, e2) -> (
let+ e1 = peephole_expr () e1 and+ e2 = peephole_expr () e2 in
match Marked.unmark e1, Marked.unmark e2 with
| ERaise except', ERaise except'' when except' = except && except = except''
->
default_mark @@ ERaise except
| ERaise except', _ when except' = except -> e2
| _, ERaise except' when except' = except -> e1
| _ -> default_mark @@ ECatch (e1, except, e2))
| _ -> visitor_map peephole_expr () e
let peephole_optimizations (p : 'm program) : 'm program =
let new_scopes =
Dcalc.Ast.map_exprs_in_scopes ~f:(peephole_expr ())
~varf:(fun v -> v)
p.scopes
in
{ p with scopes = Bindlib.unbox new_scopes }
let optimize_program (p : 'm program) : Dcalc.Ast.untyped program =
p |> iota_optimizations |> peephole_optimizations |> untype_program