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