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@26
|
58 if xn = xn' then
|
adamc@26
|
59 #1 rep
|
adamc@26
|
60 else
|
adamc@26
|
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@26
|
81 val decls : t -> L'.decl list
|
adamc@26
|
82
|
adamc@26
|
83 val enter : t -> t
|
adamc@26
|
84 val used : t * int -> t
|
adamc@26
|
85 val leave : t -> t
|
adamc@26
|
86 val listUsed : t -> int list
|
adamc@26
|
87 end = struct
|
adamc@26
|
88
|
adamc@26
|
89 type t = int * L'.decl list * IS.set
|
adamc@26
|
90
|
adamc@26
|
91 val empty = (0, [], IS.empty)
|
adamc@26
|
92
|
adamc@26
|
93 fun exp (fc, ds, vm) (v as (_, _, _, (_, loc))) = (fc, (L'.DVal v, loc) :: ds, vm)
|
adamc@26
|
94
|
adamc@26
|
95 fun func (fc, ds, vm) (x, dom, ran, e as (_, loc)) =
|
adamc@26
|
96 ((fc+1, (L'.DFun (fc, x, dom, ran, e), loc) :: ds, vm), fc)
|
adamc@26
|
97
|
adamc@26
|
98 fun decls (_, ds, _) = rev ds
|
adamc@26
|
99
|
adamc@26
|
100 fun enter (fc, ds, vm) = (fc, ds, IS.map (fn n => n + 1) vm)
|
adamc@26
|
101 fun used ((fc, ds, vm), n) = (fc, ds, IS.add (vm, n))
|
adamc@26
|
102 fun leave (fc, ds, vm) = (fc, ds, IS.map (fn n => n - 1) (IS.delete (vm, 0) handle NotFound => vm))
|
adamc@26
|
103
|
adamc@26
|
104 fun listUsed (_, _, vm) = IS.listItems vm
|
adamc@26
|
105
|
adamc@26
|
106 end
|
adamc@26
|
107
|
adamc@26
|
108
|
adamc@26
|
109 fun ccExp env ((e, loc), D) =
|
adamc@26
|
110 case e of
|
adamc@26
|
111 L.EPrim p => ((L'.EPrim p, loc), D)
|
adamc@26
|
112 | L.ERel n => ((L'.ERel n, loc), Ds.used (D, n))
|
adamc@26
|
113 | L.ENamed n => ((L'.ENamed n, loc), D)
|
adamc@52
|
114 | L.EFfi mx => ((L'.EFfi mx, loc), D)
|
adamc@52
|
115 | L.EFfiApp (m, x, es) =>
|
adamc@52
|
116 let
|
adamc@52
|
117 val (es, D) = ListUtil.foldlMap (ccExp env) D es
|
adamc@52
|
118 in
|
adamc@52
|
119 ((L'.EFfiApp (m, x, es), loc), D)
|
adamc@52
|
120 end
|
adamc@26
|
121 | L.EApp (e1, e2) =>
|
adamc@26
|
122 let
|
adamc@26
|
123 val (e1, D) = ccExp env (e1, D)
|
adamc@26
|
124 val (e2, D) = ccExp env (e2, D)
|
adamc@26
|
125 in
|
adamc@29
|
126 ((L'.ELet ([("closure", (L'.TTop, loc), e1),
|
adamc@29
|
127 ("arg", (L'.TTop, loc), liftExpInExp 0 e2),
|
adamc@29
|
128 ("code", (L'.TTop, loc), (L'.EField ((L'.ERel 1, loc), "func"), loc)),
|
adamc@29
|
129 ("env", (L'.TTop, loc), (L'.EField ((L'.ERel 2, loc), "env"), loc))],
|
adamc@26
|
130 (L'.EApp ((L'.ERel 1, loc),
|
adamc@29
|
131 (L'.ERecord [("env", (L'.ERel 0, loc), (L'.TTop, loc)),
|
adamc@29
|
132 ("arg", (L'.ERel 2, loc), (L'.TTop, loc))], loc)), loc)), loc), D)
|
adamc@26
|
133 end
|
adamc@26
|
134 | L.EAbs (x, dom, ran, e) =>
|
adamc@26
|
135 let
|
adamc@26
|
136 val dom = ccTyp dom
|
adamc@26
|
137 val ran = ccTyp ran
|
adamc@26
|
138 val (e, D) = ccExp (E.pushERel env x dom) (e, Ds.enter D)
|
adamc@26
|
139 val ns = Ds.listUsed D
|
adamc@26
|
140 val ns = List.filter (fn n => n <> 0) ns
|
adamc@26
|
141 val D = Ds.leave D
|
adamc@26
|
142
|
adamc@26
|
143 (*val () = Print.preface ("Before", FlatPrint.p_exp FlatEnv.basis e)
|
adamc@26
|
144 val () = List.app (fn (x, t) => preface ("Bound", box [string x,
|
adamc@26
|
145 space,
|
adamc@26
|
146 string ":",
|
adamc@26
|
147 space,
|
adamc@26
|
148 FlatPrint.p_typ env t]))
|
adamc@26
|
149 (E.listERels env)
|
adamc@26
|
150 val () = List.app (fn n => preface ("Free", FlatPrint.p_exp (E.pushERel env x dom)
|
adamc@26
|
151 (L'.ERel n, loc))) ns*)
|
adamc@26
|
152 val body = foldl (fn (n, e) =>
|
adamc@26
|
153 subExpInExp (n, (L'.EField ((L'.ERel 1, loc), "fv" ^ Int.toString n), loc)) e)
|
adamc@26
|
154 e ns
|
adamc@26
|
155 (*val () = Print.preface (" After", FlatPrint.p_exp FlatEnv.basis body)*)
|
adamc@29
|
156 val body = (L'.ELet ([("env", (L'.TTop, loc), (L'.EField ((L'.ERel 0, loc), "env"), loc)),
|
adamc@29
|
157 ("arg", (L'.TTop, loc), (L'.EField ((L'.ERel 1, loc), "arg"), loc))],
|
adamc@26
|
158 body), loc)
|
adamc@26
|
159
|
adamc@26
|
160 val envT = (L'.TRecord (map (fn n => ("fv" ^ Int.toString n, #2 (E.lookupERel env (n-1)))) ns), loc)
|
adamc@26
|
161 val (D, fi) = Ds.func D (x, (L'.TRecord [("env", envT), ("arg", dom)], loc), ran, body)
|
adamc@26
|
162 in
|
adamc@29
|
163 ((L'.ERecord [("code", (L'.ECode fi, loc), (L'.TTop, loc)),
|
adamc@26
|
164 ("env", (L'.ERecord (map (fn n => ("fv" ^ Int.toString n,
|
adamc@29
|
165 (L'.ERel (n-1), loc),
|
adamc@29
|
166 #2 (E.lookupERel env (n-1)))) ns), loc),
|
adamc@29
|
167 envT)], loc), D)
|
adamc@26
|
168 end
|
adamc@26
|
169
|
adamc@26
|
170 | L.ERecord xes =>
|
adamc@26
|
171 let
|
adamc@29
|
172 val (xes, D) = ListUtil.foldlMap (fn ((x, e, t), D) =>
|
adamc@26
|
173 let
|
adamc@26
|
174 val (e, D) = ccExp env (e, D)
|
adamc@26
|
175 in
|
adamc@29
|
176 ((x, e, ccTyp t), D)
|
adamc@26
|
177 end) D xes
|
adamc@26
|
178 in
|
adamc@26
|
179 ((L'.ERecord xes, loc), D)
|
adamc@26
|
180 end
|
adamc@26
|
181 | L.EField (e1, x) =>
|
adamc@26
|
182 let
|
adamc@26
|
183 val (e1, D) = ccExp env (e1, D)
|
adamc@26
|
184 in
|
adamc@26
|
185 ((L'.EField (e1, x), loc), D)
|
adamc@26
|
186 end
|
adamc@26
|
187
|
adamc@26
|
188 fun ccDecl ((d, loc), D) =
|
adamc@26
|
189 case d of
|
adamc@26
|
190 L.DVal (x, n, t, e) =>
|
adamc@26
|
191 let
|
adamc@26
|
192 val t = ccTyp t
|
adamc@56
|
193 val (e, D) = ccExp E.empty (e, D)
|
adamc@26
|
194 in
|
adamc@26
|
195 Ds.exp D (x, n, t, e)
|
adamc@26
|
196 end
|
adamc@26
|
197
|
adamc@26
|
198 fun cloconv ds =
|
adamc@26
|
199 let
|
adamc@26
|
200 val D = foldl ccDecl Ds.empty ds
|
adamc@26
|
201 in
|
adamc@26
|
202 Ds.decls D
|
adamc@26
|
203 end
|
adamc@26
|
204
|
adamc@26
|
205 end
|