adamc@26
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@26
|
2 * All rights reserved.
|
adamc@26
|
3 *
|
adamc@26
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@26
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@26
|
6 *
|
adamc@26
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@26
|
8 * this list of conditions and the following disclaimer.
|
adamc@26
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@26
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@26
|
11 * and/or other materials provided with the distribution.
|
adamc@26
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@26
|
13 * derived from this software without specific prior written permission.
|
adamc@26
|
14 *
|
adamc@26
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@26
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@26
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@26
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@26
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@26
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@26
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@26
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@26
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@26
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@26
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@26
|
26 *)
|
adamc@26
|
27
|
adamc@26
|
28 structure Cloconv :> CLOCONV = struct
|
adamc@26
|
29
|
adamc@26
|
30 structure L = Mono
|
adamc@26
|
31 structure L' = Flat
|
adamc@26
|
32
|
adamc@26
|
33 structure IS = IntBinarySet
|
adamc@26
|
34
|
adamc@26
|
35 structure U = FlatUtil
|
adamc@26
|
36 structure E = FlatEnv
|
adamc@26
|
37
|
adamc@26
|
38 open Print.PD
|
adamc@26
|
39 open Print
|
adamc@26
|
40
|
adamc@26
|
41 val liftExpInExp =
|
adamc@26
|
42 U.Exp.mapB {typ = fn t => t,
|
adamc@26
|
43 exp = fn bound => fn e =>
|
adamc@26
|
44 case e of
|
adamc@26
|
45 L'.ERel xn =>
|
adamc@26
|
46 if xn < bound then
|
adamc@26
|
47 e
|
adamc@26
|
48 else
|
adamc@26
|
49 L'.ERel (xn + 1)
|
adamc@26
|
50 | _ => e,
|
adamc@26
|
51 bind = fn (bound, U.Exp.RelE _) => bound + 1
|
adamc@26
|
52 | (bound, _) => bound}
|
adamc@26
|
53 val subExpInExp =
|
adamc@26
|
54 U.Exp.mapB {typ = fn t => t,
|
adamc@26
|
55 exp = fn (xn, rep) => fn e =>
|
adamc@26
|
56 case e of
|
adamc@26
|
57 L'.ERel xn' =>
|
adamc@74
|
58 (case Int.compare (xn', xn) of
|
adamc@74
|
59 EQUAL => #1 rep
|
adamc@74
|
60 | GREATER => L'.ERel (xn' - 1)
|
adamc@74
|
61 | _ => e)
|
adamc@26
|
62 | _ => e,
|
adamc@26
|
63 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
|
adamc@26
|
64 | (ctx, _) => ctx}
|
adamc@26
|
65
|
adamc@26
|
66
|
adamc@26
|
67 fun ccTyp (t, loc) =
|
adamc@26
|
68 case t of
|
adamc@26
|
69 L.TFun (t1, t2) => (L'.TFun (ccTyp t1, ccTyp t2), loc)
|
adamc@26
|
70 | L.TRecord xts => (L'.TRecord (map (fn (x, t) => (x, ccTyp t)) xts), loc)
|
adamc@26
|
71 | L.TNamed n => (L'.TNamed n, loc)
|
adamc@52
|
72 | L.TFfi mx => (L'.TFfi mx, loc)
|
adamc@26
|
73
|
adamc@26
|
74 structure Ds :> sig
|
adamc@26
|
75 type t
|
adamc@26
|
76
|
adamc@26
|
77 val empty : t
|
adamc@26
|
78
|
adamc@26
|
79 val exp : t -> string * int * L'.typ * L'.exp -> t
|
adamc@26
|
80 val func : t -> string * L'.typ * L'.typ * L'.exp -> t * int
|
adamc@101
|
81 val page : t -> (string * L'.typ) list * L'.exp -> t
|
adamc@26
|
82 val decls : t -> L'.decl list
|
adamc@26
|
83
|
adamc@26
|
84 val enter : t -> t
|
adamc@26
|
85 val used : t * int -> t
|
adamc@26
|
86 val leave : t -> t
|
adamc@26
|
87 val listUsed : t -> int list
|
adamc@26
|
88 end = struct
|
adamc@26
|
89
|
adamc@26
|
90 type t = int * L'.decl list * IS.set
|
adamc@26
|
91
|
adamc@26
|
92 val empty = (0, [], IS.empty)
|
adamc@26
|
93
|
adamc@26
|
94 fun exp (fc, ds, vm) (v as (_, _, _, (_, loc))) = (fc, (L'.DVal v, loc) :: ds, vm)
|
adamc@26
|
95
|
adamc@26
|
96 fun func (fc, ds, vm) (x, dom, ran, e as (_, loc)) =
|
adamc@26
|
97 ((fc+1, (L'.DFun (fc, x, dom, ran, e), loc) :: ds, vm), fc)
|
adamc@26
|
98
|
adamc@101
|
99 fun page (fc, ds, vm) (xts, e as (_, loc)) = (fc, (L'.DPage (xts, e), loc) :: ds, vm)
|
adamc@101
|
100
|
adamc@26
|
101 fun decls (_, ds, _) = rev ds
|
adamc@26
|
102
|
adamc@26
|
103 fun enter (fc, ds, vm) = (fc, ds, IS.map (fn n => n + 1) vm)
|
adamc@26
|
104 fun used ((fc, ds, vm), n) = (fc, ds, IS.add (vm, n))
|
adamc@26
|
105 fun leave (fc, ds, vm) = (fc, ds, IS.map (fn n => n - 1) (IS.delete (vm, 0) handle NotFound => vm))
|
adamc@26
|
106
|
adamc@26
|
107 fun listUsed (_, _, vm) = IS.listItems vm
|
adamc@26
|
108
|
adamc@26
|
109 end
|
adamc@26
|
110
|
adamc@26
|
111
|
adamc@26
|
112 fun ccExp env ((e, loc), D) =
|
adamc@26
|
113 case e of
|
adamc@26
|
114 L.EPrim p => ((L'.EPrim p, loc), D)
|
adamc@26
|
115 | L.ERel n => ((L'.ERel n, loc), Ds.used (D, n))
|
adamc@26
|
116 | L.ENamed n => ((L'.ENamed n, loc), D)
|
adamc@52
|
117 | L.EFfi mx => ((L'.EFfi mx, loc), D)
|
adamc@52
|
118 | L.EFfiApp (m, x, es) =>
|
adamc@52
|
119 let
|
adamc@52
|
120 val (es, D) = ListUtil.foldlMap (ccExp env) D es
|
adamc@52
|
121 in
|
adamc@52
|
122 ((L'.EFfiApp (m, x, es), loc), D)
|
adamc@52
|
123 end
|
adamc@26
|
124 | L.EApp (e1, e2) =>
|
adamc@26
|
125 let
|
adamc@26
|
126 val (e1, D) = ccExp env (e1, D)
|
adamc@26
|
127 val (e2, D) = ccExp env (e2, D)
|
adamc@26
|
128 in
|
adamc@29
|
129 ((L'.ELet ([("closure", (L'.TTop, loc), e1),
|
adamc@29
|
130 ("arg", (L'.TTop, loc), liftExpInExp 0 e2),
|
adamc@29
|
131 ("code", (L'.TTop, loc), (L'.EField ((L'.ERel 1, loc), "func"), loc)),
|
adamc@29
|
132 ("env", (L'.TTop, loc), (L'.EField ((L'.ERel 2, loc), "env"), loc))],
|
adamc@26
|
133 (L'.EApp ((L'.ERel 1, loc),
|
adamc@29
|
134 (L'.ERecord [("env", (L'.ERel 0, loc), (L'.TTop, loc)),
|
adamc@29
|
135 ("arg", (L'.ERel 2, loc), (L'.TTop, loc))], loc)), loc)), loc), D)
|
adamc@26
|
136 end
|
adamc@26
|
137 | L.EAbs (x, dom, ran, e) =>
|
adamc@26
|
138 let
|
adamc@26
|
139 val dom = ccTyp dom
|
adamc@26
|
140 val ran = ccTyp ran
|
adamc@26
|
141 val (e, D) = ccExp (E.pushERel env x dom) (e, Ds.enter D)
|
adamc@26
|
142 val ns = Ds.listUsed D
|
adamc@26
|
143 val ns = List.filter (fn n => n <> 0) ns
|
adamc@26
|
144 val D = Ds.leave D
|
adamc@26
|
145
|
adamc@98
|
146 val envT = (L'.TRecord (map (fn n => ("fv" ^ Int.toString n, #2 (E.lookupERel env (n-1)))) ns), loc)
|
adamc@98
|
147
|
adamc@26
|
148 (*val () = Print.preface ("Before", FlatPrint.p_exp FlatEnv.basis e)
|
adamc@26
|
149 val () = List.app (fn (x, t) => preface ("Bound", box [string x,
|
adamc@26
|
150 space,
|
adamc@26
|
151 string ":",
|
adamc@26
|
152 space,
|
adamc@26
|
153 FlatPrint.p_typ env t]))
|
adamc@26
|
154 (E.listERels env)
|
adamc@26
|
155 val () = List.app (fn n => preface ("Free", FlatPrint.p_exp (E.pushERel env x dom)
|
adamc@26
|
156 (L'.ERel n, loc))) ns*)
|
adamc@26
|
157 val body = foldl (fn (n, e) =>
|
adamc@26
|
158 subExpInExp (n, (L'.EField ((L'.ERel 1, loc), "fv" ^ Int.toString n), loc)) e)
|
adamc@26
|
159 e ns
|
adamc@26
|
160 (*val () = Print.preface (" After", FlatPrint.p_exp FlatEnv.basis body)*)
|
adamc@98
|
161 val body = (L'.ELet ([("env", envT, (L'.EField ((L'.ERel 0, loc), "env"), loc)),
|
adamc@98
|
162 ("arg", dom, (L'.EField ((L'.ERel 1, loc), "arg"), loc))],
|
adamc@26
|
163 body), loc)
|
adamc@98
|
164
|
adamc@26
|
165 val (D, fi) = Ds.func D (x, (L'.TRecord [("env", envT), ("arg", dom)], loc), ran, body)
|
adamc@26
|
166 in
|
adamc@29
|
167 ((L'.ERecord [("code", (L'.ECode fi, loc), (L'.TTop, loc)),
|
adamc@26
|
168 ("env", (L'.ERecord (map (fn n => ("fv" ^ Int.toString n,
|
adamc@29
|
169 (L'.ERel (n-1), loc),
|
adamc@29
|
170 #2 (E.lookupERel env (n-1)))) ns), loc),
|
adamc@29
|
171 envT)], loc), D)
|
adamc@26
|
172 end
|
adamc@26
|
173
|
adamc@26
|
174 | L.ERecord xes =>
|
adamc@26
|
175 let
|
adamc@29
|
176 val (xes, D) = ListUtil.foldlMap (fn ((x, e, t), D) =>
|
adamc@26
|
177 let
|
adamc@26
|
178 val (e, D) = ccExp env (e, D)
|
adamc@26
|
179 in
|
adamc@29
|
180 ((x, e, ccTyp t), D)
|
adamc@26
|
181 end) D xes
|
adamc@26
|
182 in
|
adamc@26
|
183 ((L'.ERecord xes, loc), D)
|
adamc@26
|
184 end
|
adamc@26
|
185 | L.EField (e1, x) =>
|
adamc@26
|
186 let
|
adamc@26
|
187 val (e1, D) = ccExp env (e1, D)
|
adamc@26
|
188 in
|
adamc@26
|
189 ((L'.EField (e1, x), loc), D)
|
adamc@26
|
190 end
|
adamc@26
|
191
|
adamc@102
|
192 | L.EStrcat (e1, e2) =>
|
adamc@102
|
193 let
|
adamc@102
|
194 val (e1, D) = ccExp env (e1, D)
|
adamc@102
|
195 val (e2, D) = ccExp env (e2, D)
|
adamc@102
|
196 in
|
adamc@102
|
197 ((L'.EStrcat (e1, e2), loc), D)
|
adamc@102
|
198 end
|
adamc@102
|
199
|
adamc@102
|
200 | L.EWrite e =>
|
adamc@102
|
201 let
|
adamc@102
|
202 val (e, D) = ccExp env (e, D)
|
adamc@102
|
203 in
|
adamc@102
|
204 ((L'.EWrite e, loc), D)
|
adamc@102
|
205 end
|
adamc@94
|
206
|
adamc@26
|
207 fun ccDecl ((d, loc), D) =
|
adamc@26
|
208 case d of
|
adamc@26
|
209 L.DVal (x, n, t, e) =>
|
adamc@26
|
210 let
|
adamc@26
|
211 val t = ccTyp t
|
adamc@56
|
212 val (e, D) = ccExp E.empty (e, D)
|
adamc@26
|
213 in
|
adamc@26
|
214 Ds.exp D (x, n, t, e)
|
adamc@26
|
215 end
|
adamc@101
|
216 | L.DPage (xts, e) =>
|
adamc@101
|
217 let
|
adamc@101
|
218 val xts = map (fn (x, t) => (x, ccTyp t)) xts
|
adamc@101
|
219 val (e, D) = ccExp E.empty (e, D)
|
adamc@101
|
220 in
|
adamc@101
|
221 Ds.page D (xts, e)
|
adamc@101
|
222 end
|
adamc@26
|
223
|
adamc@26
|
224 fun cloconv ds =
|
adamc@26
|
225 let
|
adamc@26
|
226 val D = foldl ccDecl Ds.empty ds
|
adamc@26
|
227 in
|
adamc@26
|
228 Ds.decls D
|
adamc@26
|
229 end
|
adamc@26
|
230
|
adamc@26
|
231 end
|