adamc@16
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@16
|
2 * All rights reserved.
|
adamc@16
|
3 *
|
adamc@16
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@16
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@16
|
6 *
|
adamc@16
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@16
|
8 * this list of conditions and the following disclaimer.
|
adamc@16
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@16
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@16
|
11 * and/or other materials provided with the distribution.
|
adamc@16
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@16
|
13 * derived from this software without specific prior written permission.
|
adamc@16
|
14 *
|
adamc@16
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@16
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@16
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@16
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@16
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@16
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@16
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@16
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@16
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@16
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@16
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@16
|
26 *)
|
adamc@16
|
27
|
adamc@16
|
28 structure Corify :> CORIFY = struct
|
adamc@16
|
29
|
adamc@16
|
30 structure EM = ErrorMsg
|
adamc@39
|
31 structure L = Expl
|
adamc@16
|
32 structure L' = Core
|
adamc@16
|
33
|
adamc@39
|
34 structure IM = IntBinaryMap
|
adamc@39
|
35 structure SM = BinaryMapFn(struct
|
adamc@39
|
36 type ord_key = string
|
adamc@39
|
37 val compare = String.compare
|
adamc@39
|
38 end)
|
adamc@39
|
39
|
adamc@39
|
40 local
|
adamc@39
|
41 val count = ref 0
|
adamc@39
|
42 in
|
adamc@39
|
43
|
adamc@39
|
44 fun reset v = count := v
|
adamc@39
|
45
|
adamc@39
|
46 fun alloc () =
|
adamc@39
|
47 let
|
adamc@39
|
48 val r = !count
|
adamc@39
|
49 in
|
adamc@39
|
50 count := r + 1;
|
adamc@39
|
51 r
|
adamc@39
|
52 end
|
adamc@39
|
53
|
adamc@39
|
54 end
|
adamc@39
|
55
|
adamc@39
|
56 structure St : sig
|
adamc@39
|
57 type t
|
adamc@39
|
58
|
adamc@39
|
59 val empty : t
|
adamc@39
|
60
|
adamc@146
|
61 val debug : t -> unit
|
adamc@146
|
62
|
adamc@39
|
63 val enter : t -> t
|
adamc@39
|
64 val leave : t -> {outer : t, inner : t}
|
adamc@185
|
65 val ffi : string -> L'.con SM.map -> string SM.map -> t
|
adamc@39
|
66
|
adamc@73
|
67 datatype core_con =
|
adamc@73
|
68 CNormal of int
|
adamc@73
|
69 | CFfi of string
|
adamc@73
|
70 val bindCon : t -> string -> int -> t * int
|
adamc@73
|
71 val lookupConById : t -> int -> int option
|
adamc@73
|
72 val lookupConByName : t -> string -> core_con
|
adamc@48
|
73
|
adamc@177
|
74 val bindConstructor : t -> string -> int -> L'.patCon -> t
|
adamc@177
|
75 val lookupConstructorByName : t -> string -> L'.patCon
|
adamc@177
|
76 val lookupConstructorById : t -> int -> L'.patCon
|
adamc@177
|
77
|
adamc@73
|
78 datatype core_val =
|
adamc@73
|
79 ENormal of int
|
adamc@73
|
80 | EFfi of string * L'.con
|
adamc@73
|
81 val bindVal : t -> string -> int -> t * int
|
adamc@177
|
82 val bindConstructorVal : t -> string -> int -> t
|
adamc@73
|
83 val lookupValById : t -> int -> int option
|
adamc@73
|
84 val lookupValByName : t -> string -> core_val
|
adamc@39
|
85
|
adamc@39
|
86 val bindStr : t -> string -> int -> t -> t
|
adamc@39
|
87 val lookupStrById : t -> int -> t
|
adamc@39
|
88 val lookupStrByName : string * t -> t
|
adamc@46
|
89
|
adamc@146
|
90 val bindFunctor : t -> string -> int -> string -> int -> L.str -> t
|
adamc@146
|
91 val lookupFunctorById : t -> int -> string * int * L.str
|
adamc@146
|
92 val lookupFunctorByName : string * t -> string * int * L.str
|
adamc@39
|
93 end = struct
|
adamc@39
|
94
|
adamc@48
|
95 datatype flattening =
|
adamc@73
|
96 FNormal of {cons : int SM.map,
|
adamc@177
|
97 constructors : L'.patCon SM.map,
|
adamc@73
|
98 vals : int SM.map,
|
adamc@48
|
99 strs : flattening SM.map,
|
adamc@146
|
100 funs : (string * int * L.str) SM.map}
|
adamc@73
|
101 | FFfi of {mod : string,
|
adamc@185
|
102 vals : L'.con SM.map,
|
adamc@185
|
103 constructors : string SM.map}
|
adamc@39
|
104
|
adamc@39
|
105 type t = {
|
adamc@73
|
106 cons : int IM.map,
|
adamc@177
|
107 constructors : L'.patCon IM.map,
|
adamc@73
|
108 vals : int IM.map,
|
adamc@39
|
109 strs : flattening IM.map,
|
adamc@146
|
110 funs : (string * int * L.str) IM.map,
|
adamc@39
|
111 current : flattening,
|
adamc@39
|
112 nested : flattening list
|
adamc@39
|
113 }
|
adamc@39
|
114
|
adamc@39
|
115 val empty = {
|
adamc@73
|
116 cons = IM.empty,
|
adamc@177
|
117 constructors = IM.empty,
|
adamc@73
|
118 vals = IM.empty,
|
adamc@39
|
119 strs = IM.empty,
|
adamc@46
|
120 funs = IM.empty,
|
adamc@177
|
121 current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty },
|
adamc@39
|
122 nested = []
|
adamc@39
|
123 }
|
adamc@39
|
124
|
adamc@177
|
125 fun debug ({current = FNormal {cons, constructors, vals, strs, funs}, ...} : t) =
|
adamc@146
|
126 print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; "
|
adamc@177
|
127 ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; "
|
adamc@146
|
128 ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; "
|
adamc@146
|
129 ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; "
|
adamc@146
|
130 ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n")
|
adamc@146
|
131 | debug _ = print "Not normal!\n"
|
adamc@146
|
132
|
adamc@73
|
133 datatype core_con =
|
adamc@73
|
134 CNormal of int
|
adamc@73
|
135 | CFfi of string
|
adamc@48
|
136
|
adamc@73
|
137 datatype core_val =
|
adamc@73
|
138 ENormal of int
|
adamc@73
|
139 | EFfi of string * L'.con
|
adamc@73
|
140
|
adamc@177
|
141 fun bindCon {cons, constructors, vals, strs, funs, current, nested} s n =
|
adamc@39
|
142 let
|
adamc@39
|
143 val n' = alloc ()
|
adamc@39
|
144
|
adamc@39
|
145 val current =
|
adamc@48
|
146 case current of
|
adamc@48
|
147 FFfi _ => raise Fail "Binding inside FFfi"
|
adamc@177
|
148 | FNormal {cons, constructors, vals, strs, funs} =>
|
adamc@73
|
149 FNormal {cons = SM.insert (cons, s, n'),
|
adamc@177
|
150 constructors = constructors,
|
adamc@73
|
151 vals = vals,
|
adamc@48
|
152 strs = strs,
|
adamc@48
|
153 funs = funs}
|
adamc@39
|
154 in
|
adamc@73
|
155 ({cons = IM.insert (cons, n, n'),
|
adamc@177
|
156 constructors = constructors,
|
adamc@73
|
157 vals = vals,
|
adamc@39
|
158 strs = strs,
|
adamc@46
|
159 funs = funs,
|
adamc@39
|
160 current = current,
|
adamc@39
|
161 nested = nested},
|
adamc@39
|
162 n')
|
adamc@39
|
163 end
|
adamc@39
|
164
|
adamc@73
|
165 fun lookupConById ({cons, ...} : t) n = IM.find (cons, n)
|
adamc@39
|
166
|
adamc@73
|
167 fun lookupConByName ({current, ...} : t) x =
|
adamc@48
|
168 case current of
|
adamc@73
|
169 FFfi {mod = m, ...} => CFfi m
|
adamc@73
|
170 | FNormal {cons, ...} =>
|
adamc@73
|
171 case SM.find (cons, x) of
|
adamc@73
|
172 NONE => raise Fail "Corify.St.lookupConByName"
|
adamc@73
|
173 | SOME n => CNormal n
|
adamc@39
|
174
|
adamc@177
|
175 fun bindVal {cons, constructors, vals, strs, funs, current, nested} s n =
|
adamc@73
|
176 let
|
adamc@73
|
177 val n' = alloc ()
|
adamc@73
|
178
|
adamc@73
|
179 val current =
|
adamc@73
|
180 case current of
|
adamc@73
|
181 FFfi _ => raise Fail "Binding inside FFfi"
|
adamc@177
|
182 | FNormal {cons, constructors, vals, strs, funs} =>
|
adamc@73
|
183 FNormal {cons = cons,
|
adamc@177
|
184 constructors = constructors,
|
adamc@73
|
185 vals = SM.insert (vals, s, n'),
|
adamc@73
|
186 strs = strs,
|
adamc@73
|
187 funs = funs}
|
adamc@73
|
188 in
|
adamc@73
|
189 ({cons = cons,
|
adamc@177
|
190 constructors = constructors,
|
adamc@73
|
191 vals = IM.insert (vals, n, n'),
|
adamc@73
|
192 strs = strs,
|
adamc@73
|
193 funs = funs,
|
adamc@73
|
194 current = current,
|
adamc@73
|
195 nested = nested},
|
adamc@73
|
196 n')
|
adamc@73
|
197 end
|
adamc@73
|
198
|
adamc@177
|
199 fun bindConstructorVal {cons, constructors, vals, strs, funs, current, nested} s n =
|
adamc@163
|
200 let
|
adamc@163
|
201 val current =
|
adamc@163
|
202 case current of
|
adamc@163
|
203 FFfi _ => raise Fail "Binding inside FFfi"
|
adamc@177
|
204 | FNormal {cons, constructors, vals, strs, funs} =>
|
adamc@163
|
205 FNormal {cons = cons,
|
adamc@177
|
206 constructors = constructors,
|
adamc@163
|
207 vals = SM.insert (vals, s, n),
|
adamc@163
|
208 strs = strs,
|
adamc@163
|
209 funs = funs}
|
adamc@163
|
210 in
|
adamc@163
|
211 {cons = cons,
|
adamc@177
|
212 constructors = constructors,
|
adamc@163
|
213 vals = IM.insert (vals, n, n),
|
adamc@163
|
214 strs = strs,
|
adamc@163
|
215 funs = funs,
|
adamc@163
|
216 current = current,
|
adamc@163
|
217 nested = nested}
|
adamc@163
|
218 end
|
adamc@163
|
219
|
adamc@177
|
220
|
adamc@73
|
221 fun lookupValById ({vals, ...} : t) n = IM.find (vals, n)
|
adamc@73
|
222
|
adamc@73
|
223 fun lookupValByName ({current, ...} : t) x =
|
adamc@73
|
224 case current of
|
adamc@73
|
225 FFfi {mod = m, vals, ...} =>
|
adamc@73
|
226 (case SM.find (vals, x) of
|
adamc@73
|
227 NONE => raise Fail "Corify.St.lookupValByName: no type for FFI val"
|
adamc@73
|
228 | SOME t => EFfi (m, t))
|
adamc@73
|
229 | FNormal {vals, ...} =>
|
adamc@73
|
230 case SM.find (vals, x) of
|
adamc@73
|
231 NONE => raise Fail "Corify.St.lookupValByName"
|
adamc@73
|
232 | SOME n => ENormal n
|
adamc@73
|
233
|
adamc@177
|
234 fun bindConstructor {cons, constructors, vals, strs, funs, current, nested} s n n' =
|
adamc@177
|
235 let
|
adamc@177
|
236 val current =
|
adamc@177
|
237 case current of
|
adamc@177
|
238 FFfi _ => raise Fail "Binding inside FFfi"
|
adamc@177
|
239 | FNormal {cons, constructors, vals, strs, funs} =>
|
adamc@177
|
240 FNormal {cons = cons,
|
adamc@177
|
241 constructors = SM.insert (constructors, s, n'),
|
adamc@177
|
242 vals = vals,
|
adamc@177
|
243 strs = strs,
|
adamc@177
|
244 funs = funs}
|
adamc@177
|
245 in
|
adamc@177
|
246 {cons = cons,
|
adamc@177
|
247 constructors = IM.insert (constructors, n, n'),
|
adamc@177
|
248 vals = vals,
|
adamc@177
|
249 strs = strs,
|
adamc@177
|
250 funs = funs,
|
adamc@177
|
251 current = current,
|
adamc@177
|
252 nested = nested}
|
adamc@177
|
253 end
|
adamc@177
|
254
|
adamc@177
|
255 fun lookupConstructorById ({constructors, ...} : t) n =
|
adamc@177
|
256 case IM.find (constructors, n) of
|
adamc@177
|
257 NONE => raise Fail "Corify.St.lookupConstructorById"
|
adamc@177
|
258 | SOME x => x
|
adamc@177
|
259
|
adamc@177
|
260 fun lookupConstructorByName ({current, ...} : t) x =
|
adamc@177
|
261 case current of
|
adamc@185
|
262 FFfi {mod = m, constructors, ...} =>
|
adamc@185
|
263 (case SM.find (constructors, x) of
|
adamc@185
|
264 NONE => raise Fail "Corify.St.lookupConstructorByName [1]"
|
adamc@185
|
265 | SOME n => L'.PConFfi {mod = m, datatyp = n, con = x})
|
adamc@177
|
266 | FNormal {constructors, ...} =>
|
adamc@177
|
267 case SM.find (constructors, x) of
|
adamc@185
|
268 NONE => raise Fail "Corify.St.lookupConstructorByName [2]"
|
adamc@177
|
269 | SOME n => n
|
adamc@177
|
270
|
adamc@177
|
271 fun enter {cons, constructors, vals, strs, funs, current, nested} =
|
adamc@73
|
272 {cons = cons,
|
adamc@177
|
273 constructors = constructors,
|
adamc@73
|
274 vals = vals,
|
adamc@39
|
275 strs = strs,
|
adamc@46
|
276 funs = funs,
|
adamc@73
|
277 current = FNormal {cons = SM.empty,
|
adamc@177
|
278 constructors = SM.empty,
|
adamc@73
|
279 vals = SM.empty,
|
adamc@48
|
280 strs = SM.empty,
|
adamc@48
|
281 funs = SM.empty},
|
adamc@39
|
282 nested = current :: nested}
|
adamc@39
|
283
|
adamc@73
|
284 fun dummy f = {cons = IM.empty,
|
adamc@177
|
285 constructors = IM.empty,
|
adamc@73
|
286 vals = IM.empty,
|
adamc@39
|
287 strs = IM.empty,
|
adamc@46
|
288 funs = IM.empty,
|
adamc@39
|
289 current = f,
|
adamc@39
|
290 nested = []}
|
adamc@39
|
291
|
adamc@177
|
292 fun leave {cons, constructors, vals, strs, funs, current, nested = m1 :: rest} =
|
adamc@73
|
293 {outer = {cons = cons,
|
adamc@177
|
294 constructors = constructors,
|
adamc@73
|
295 vals = vals,
|
adamc@39
|
296 strs = strs,
|
adamc@46
|
297 funs = funs,
|
adamc@39
|
298 current = m1,
|
adamc@39
|
299 nested = rest},
|
adamc@39
|
300 inner = dummy current}
|
adamc@39
|
301 | leave _ = raise Fail "Corify.St.leave"
|
adamc@39
|
302
|
adamc@185
|
303 fun ffi m vals constructors = dummy (FFfi {mod = m, vals = vals, constructors = constructors})
|
adamc@48
|
304
|
adamc@177
|
305 fun bindStr ({cons, constructors, vals, strs, funs,
|
adamc@177
|
306 current = FNormal {cons = mcons, constructors = mconstructors,
|
adamc@177
|
307 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
|
adamc@46
|
308 x n ({current = f, ...} : t) =
|
adamc@73
|
309 {cons = cons,
|
adamc@177
|
310 constructors = constructors,
|
adamc@73
|
311 vals = vals,
|
adamc@39
|
312 strs = IM.insert (strs, n, f),
|
adamc@46
|
313 funs = funs,
|
adamc@73
|
314 current = FNormal {cons = mcons,
|
adamc@177
|
315 constructors = mconstructors,
|
adamc@73
|
316 vals = mvals,
|
adamc@73
|
317 strs = SM.insert (mstrs, x, f),
|
adamc@73
|
318 funs = mfuns},
|
adamc@39
|
319 nested = nested}
|
adamc@48
|
320 | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr"
|
adamc@39
|
321
|
adamc@39
|
322 fun lookupStrById ({strs, ...} : t) n =
|
adamc@39
|
323 case IM.find (strs, n) of
|
adamc@46
|
324 NONE => raise Fail "Corify.St.lookupStrById"
|
adamc@39
|
325 | SOME f => dummy f
|
adamc@39
|
326
|
adamc@48
|
327 fun lookupStrByName (m, {current = FNormal {strs, ...}, ...} : t) =
|
adamc@48
|
328 (case SM.find (strs, m) of
|
adamc@48
|
329 NONE => raise Fail "Corify.St.lookupStrByName"
|
adamc@48
|
330 | SOME f => dummy f)
|
adamc@48
|
331 | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName"
|
adamc@39
|
332
|
adamc@177
|
333 fun bindFunctor ({cons, constructors, vals, strs, funs,
|
adamc@177
|
334 current = FNormal {cons = mcons, constructors = mconstructors,
|
adamc@177
|
335 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
|
adamc@146
|
336 x n xa na str =
|
adamc@73
|
337 {cons = cons,
|
adamc@177
|
338 constructors = constructors,
|
adamc@73
|
339 vals = vals,
|
adamc@46
|
340 strs = strs,
|
adamc@146
|
341 funs = IM.insert (funs, n, (xa, na, str)),
|
adamc@73
|
342 current = FNormal {cons = mcons,
|
adamc@177
|
343 constructors = mconstructors,
|
adamc@73
|
344 vals = mvals,
|
adamc@48
|
345 strs = mstrs,
|
adamc@146
|
346 funs = SM.insert (mfuns, x, (xa, na, str))},
|
adamc@46
|
347 nested = nested}
|
adamc@146
|
348 | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
|
adamc@46
|
349
|
adamc@46
|
350 fun lookupFunctorById ({funs, ...} : t) n =
|
adamc@46
|
351 case IM.find (funs, n) of
|
adamc@46
|
352 NONE => raise Fail "Corify.St.lookupFunctorById"
|
adamc@46
|
353 | SOME v => v
|
adamc@46
|
354
|
adamc@48
|
355 fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) =
|
adamc@48
|
356 (case SM.find (funs, m) of
|
adamc@48
|
357 NONE => raise Fail "Corify.St.lookupFunctorByName"
|
adamc@48
|
358 | SOME v => v)
|
adamc@48
|
359 | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName"
|
adamc@46
|
360
|
adamc@39
|
361 end
|
adamc@39
|
362
|
adamc@39
|
363
|
adamc@16
|
364 fun corifyKind (k, loc) =
|
adamc@16
|
365 case k of
|
adamc@16
|
366 L.KType => (L'.KType, loc)
|
adamc@16
|
367 | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc)
|
adamc@16
|
368 | L.KName => (L'.KName, loc)
|
adamc@16
|
369 | L.KRecord k => (L'.KRecord (corifyKind k), loc)
|
adamc@87
|
370 | L.KUnit => (L'.KUnit, loc)
|
adamc@16
|
371
|
adamc@39
|
372 fun corifyCon st (c, loc) =
|
adamc@16
|
373 case c of
|
adamc@39
|
374 L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc)
|
adamc@39
|
375 | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc)
|
adamc@39
|
376 | L.TRecord c => (L'.TRecord (corifyCon st c), loc)
|
adamc@16
|
377
|
adamc@16
|
378 | L.CRel n => (L'.CRel n, loc)
|
adamc@39
|
379 | L.CNamed n =>
|
adamc@73
|
380 (case St.lookupConById st n of
|
adamc@39
|
381 NONE => (L'.CNamed n, loc)
|
adamc@39
|
382 | SOME n => (L'.CNamed n, loc))
|
adamc@39
|
383 | L.CModProj (m, ms, x) =>
|
adamc@39
|
384 let
|
adamc@39
|
385 val st = St.lookupStrById st m
|
adamc@39
|
386 val st = foldl St.lookupStrByName st ms
|
adamc@39
|
387 in
|
adamc@73
|
388 case St.lookupConByName st x of
|
adamc@73
|
389 St.CNormal n => (L'.CNamed n, loc)
|
adamc@73
|
390 | St.CFfi m => (L'.CFfi (m, x), loc)
|
adamc@39
|
391 end
|
adamc@34
|
392
|
adamc@39
|
393 | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc)
|
adamc@39
|
394 | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc)
|
adamc@16
|
395
|
adamc@16
|
396 | L.CName s => (L'.CName s, loc)
|
adamc@16
|
397
|
adamc@39
|
398 | L.CRecord (k, xcs) =>
|
adamc@39
|
399 (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc)
|
adamc@39
|
400 | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc)
|
adamc@69
|
401 | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc)
|
adamc@87
|
402 | L.CUnit => (L'.CUnit, loc)
|
adamc@16
|
403
|
adamc@177
|
404 fun corifyPatCon st pc =
|
adamc@177
|
405 case pc of
|
adamc@177
|
406 L.PConVar n => St.lookupConstructorById st n
|
adamc@177
|
407 | L.PConProj (m1, ms, x) =>
|
adamc@177
|
408 let
|
adamc@177
|
409 val st = St.lookupStrById st m1
|
adamc@177
|
410 val st = foldl St.lookupStrByName st ms
|
adamc@177
|
411 in
|
adamc@177
|
412 St.lookupConstructorByName st x
|
adamc@177
|
413 end
|
adamc@177
|
414
|
adamc@177
|
415 fun corifyPat st (p, loc) =
|
adamc@177
|
416 case p of
|
adamc@177
|
417 L.PWild => (L'.PWild, loc)
|
adamc@182
|
418 | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc)
|
adamc@177
|
419 | L.PPrim p => (L'.PPrim p, loc)
|
adamc@177
|
420 | L.PCon (pc, po) => (L'.PCon (corifyPatCon st pc, Option.map (corifyPat st) po), loc)
|
adamc@182
|
421 | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc)
|
adamc@177
|
422
|
adamc@39
|
423 fun corifyExp st (e, loc) =
|
adamc@16
|
424 case e of
|
adamc@16
|
425 L.EPrim p => (L'.EPrim p, loc)
|
adamc@16
|
426 | L.ERel n => (L'.ERel n, loc)
|
adamc@39
|
427 | L.ENamed n =>
|
adamc@73
|
428 (case St.lookupValById st n of
|
adamc@39
|
429 NONE => (L'.ENamed n, loc)
|
adamc@39
|
430 | SOME n => (L'.ENamed n, loc))
|
adamc@39
|
431 | L.EModProj (m, ms, x) =>
|
adamc@39
|
432 let
|
adamc@39
|
433 val st = St.lookupStrById st m
|
adamc@39
|
434 val st = foldl St.lookupStrByName st ms
|
adamc@39
|
435 in
|
adamc@73
|
436 case St.lookupValByName st x of
|
adamc@73
|
437 St.ENormal n => (L'.ENamed n, loc)
|
adamc@73
|
438 | St.EFfi (m, t) =>
|
adamc@49
|
439 case t of
|
adamc@50
|
440 (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) =>
|
adamc@50
|
441 (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc)
|
adamc@50
|
442 | t as (L'.TFun _, _) =>
|
adamc@49
|
443 let
|
adamc@49
|
444 fun getArgs (all as (t, _), args) =
|
adamc@49
|
445 case t of
|
adamc@49
|
446 L'.TFun (dom, ran) => getArgs (ran, dom :: args)
|
adamc@49
|
447 | _ => (all, rev args)
|
adamc@49
|
448
|
adamc@49
|
449 val (result, args) = getArgs (t, [])
|
adamc@49
|
450
|
adamc@50
|
451 val (actuals, _) = foldr (fn (_, (actuals, n)) =>
|
adamc@50
|
452 ((L'.ERel n, loc) :: actuals,
|
adamc@50
|
453 n + 1)) ([], 0) args
|
adamc@50
|
454 val app = (L'.EFfiApp (m, x, actuals), loc)
|
adamc@49
|
455 val (abs, _, _) = foldr (fn (t, (abs, ran, n)) =>
|
adamc@49
|
456 ((L'.EAbs ("arg" ^ Int.toString n,
|
adamc@49
|
457 t,
|
adamc@49
|
458 ran,
|
adamc@49
|
459 abs), loc),
|
adamc@49
|
460 (L'.TFun (t, ran), loc),
|
adamc@49
|
461 n - 1)) (app, result, length args - 1) args
|
adamc@49
|
462 in
|
adamc@49
|
463 abs
|
adamc@49
|
464 end
|
adamc@49
|
465 | _ => (L'.EFfi (m, x), loc)
|
adamc@39
|
466 end
|
adamc@39
|
467 | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc)
|
adamc@39
|
468 | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc)
|
adamc@39
|
469 | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc)
|
adamc@39
|
470 | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc)
|
adamc@16
|
471
|
adamc@110
|
472 | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) =>
|
adamc@110
|
473 (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc)
|
adamc@39
|
474 | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c,
|
adamc@39
|
475 {field = corifyCon st field, rest = corifyCon st rest}), loc)
|
adamc@149
|
476 | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c,
|
adamc@149
|
477 {field = corifyCon st field, rest = corifyCon st rest}), loc)
|
adamc@73
|
478 | L.EFold k => (L'.EFold (corifyKind k), loc)
|
adamc@177
|
479
|
adamc@182
|
480 | L.ECase (e, pes, {disc, result}) =>
|
adamc@182
|
481 (L'.ECase (corifyExp st e,
|
adamc@182
|
482 map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes,
|
adamc@182
|
483 {disc = corifyCon st disc, result = corifyCon st result}),
|
adamc@182
|
484 loc)
|
adamc@177
|
485
|
adamc@109
|
486 | L.EWrite e => (L'.EWrite (corifyExp st e), loc)
|
adamc@16
|
487
|
adamc@39
|
488 fun corifyDecl ((d, loc : EM.span), st) =
|
adamc@39
|
489 case d of
|
adamc@39
|
490 L.DCon (x, n, k, c) =>
|
adamc@39
|
491 let
|
adamc@73
|
492 val (st, n) = St.bindCon st x n
|
adamc@39
|
493 in
|
adamc@39
|
494 ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
|
adamc@39
|
495 end
|
adamc@163
|
496 | L.DDatatype (x, n, xncs) =>
|
adamc@163
|
497 let
|
adamc@163
|
498 val (st, n) = St.bindCon st x n
|
adamc@163
|
499 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
|
adamc@163
|
500 let
|
adamc@177
|
501 val st = St.bindConstructor st x n (L'.PConVar n)
|
adamc@177
|
502 val st = St.bindConstructorVal st x n
|
adamc@163
|
503 val co = Option.map (corifyCon st) co
|
adamc@163
|
504 in
|
adamc@163
|
505 ((x, n, co), st)
|
adamc@163
|
506 end) st xncs
|
adamc@177
|
507
|
adamc@177
|
508 val t = (L'.CNamed n, loc)
|
adamc@177
|
509 val dcons = map (fn (x, n, to) =>
|
adamc@177
|
510 let
|
adamc@177
|
511 val (e, t) =
|
adamc@177
|
512 case to of
|
adamc@185
|
513 NONE => ((L'.ECon (L'.PConVar n, NONE), loc), t)
|
adamc@177
|
514 | SOME t' => ((L'.EAbs ("x", t', t,
|
adamc@185
|
515 (L'.ECon (L'.PConVar n, SOME (L'.ERel 0, loc)), loc)),
|
adamc@177
|
516 loc),
|
adamc@177
|
517 (L'.TFun (t', t), loc))
|
adamc@177
|
518 in
|
adamc@177
|
519 (L'.DVal (x, n, t, e, ""), loc)
|
adamc@177
|
520 end) xncs
|
adamc@163
|
521 in
|
adamc@177
|
522 ((L'.DDatatype (x, n, xncs), loc) :: dcons, st)
|
adamc@163
|
523 end
|
adamc@163
|
524 | L.DDatatypeImp (x, n, m1, ms, s, xncs) =>
|
adamc@163
|
525 let
|
adamc@163
|
526 val (st, n) = St.bindCon st x n
|
adamc@163
|
527 val c = corifyCon st (L.CModProj (m1, ms, s), loc)
|
adamc@163
|
528
|
adamc@177
|
529 val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms
|
adamc@177
|
530 val (_, {inner, ...}) = corifyStr (m, st)
|
adamc@177
|
531
|
adamc@163
|
532 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
|
adamc@163
|
533 let
|
adamc@177
|
534 val n' = St.lookupConstructorByName inner x
|
adamc@177
|
535 val st = St.bindConstructor st x n n'
|
adamc@163
|
536 val (st, n) = St.bindVal st x n
|
adamc@163
|
537 val co = Option.map (corifyCon st) co
|
adamc@163
|
538 in
|
adamc@163
|
539 ((x, n, co), st)
|
adamc@163
|
540 end) st xncs
|
adamc@177
|
541
|
adamc@163
|
542 val cds = map (fn (x, n, co) =>
|
adamc@163
|
543 let
|
adamc@163
|
544 val t = case co of
|
adamc@163
|
545 NONE => c
|
adamc@163
|
546 | SOME t' => (L'.TFun (t', c), loc)
|
adamc@163
|
547 val e = corifyExp st (L.EModProj (m1, ms, x), loc)
|
adamc@163
|
548 in
|
adamc@163
|
549 (L'.DVal (x, n, t, e, x), loc)
|
adamc@163
|
550 end) xncs
|
adamc@163
|
551 in
|
adamc@163
|
552 ((L'.DCon (x, n, (L'.KType, loc), c), loc) :: cds, st)
|
adamc@163
|
553 end
|
adamc@39
|
554 | L.DVal (x, n, t, e) =>
|
adamc@39
|
555 let
|
adamc@73
|
556 val (st, n) = St.bindVal st x n
|
adamc@111
|
557 val s =
|
adamc@111
|
558 if String.isPrefix "wrap_" x then
|
adamc@111
|
559 String.extract (x, 5, NONE)
|
adamc@111
|
560 else
|
adamc@111
|
561 x
|
adamc@39
|
562 in
|
adamc@111
|
563 ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st)
|
adamc@39
|
564 end
|
adamc@125
|
565 | L.DValRec vis =>
|
adamc@125
|
566 let
|
adamc@125
|
567 val (vis, st) = ListUtil.foldlMap
|
adamc@130
|
568 (fn ((x, n, t, e), st) =>
|
adamc@130
|
569 let
|
adamc@130
|
570 val (st, n) = St.bindVal st x n
|
adamc@130
|
571 in
|
adamc@130
|
572 ((x, n, t, e), st)
|
adamc@130
|
573 end)
|
adamc@130
|
574 st vis
|
adamc@130
|
575
|
adamc@130
|
576 val vis = map
|
adamc@130
|
577 (fn (x, n, t, e) =>
|
adamc@130
|
578 let
|
adamc@130
|
579 val s =
|
adamc@130
|
580 if String.isPrefix "wrap_" x then
|
adamc@130
|
581 String.extract (x, 5, NONE)
|
adamc@130
|
582 else
|
adamc@130
|
583 x
|
adamc@130
|
584 in
|
adamc@130
|
585 (x, n, corifyCon st t, corifyExp st e, s)
|
adamc@130
|
586 end)
|
adamc@130
|
587 vis
|
adamc@125
|
588 in
|
adamc@125
|
589 ([(L'.DValRec vis, loc)], st)
|
adamc@125
|
590 end
|
adamc@39
|
591 | L.DSgn _ => ([], st)
|
adamc@16
|
592
|
adamc@146
|
593 | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) =>
|
adamc@146
|
594 ([], St.bindFunctor st x n xa na str)
|
adamc@46
|
595
|
adamc@39
|
596 | L.DStr (x, n, _, str) =>
|
adamc@39
|
597 let
|
adamc@39
|
598 val (ds, {inner, outer}) = corifyStr (str, st)
|
adamc@39
|
599 val st = St.bindStr outer x n inner
|
adamc@39
|
600 in
|
adamc@39
|
601 (ds, st)
|
adamc@39
|
602 end
|
adamc@16
|
603
|
adamc@49
|
604 | L.DFfiStr (m, n, (sgn, _)) =>
|
adamc@49
|
605 (case sgn of
|
adamc@49
|
606 L.SgnConst sgis =>
|
adamc@49
|
607 let
|
adamc@185
|
608 val (ds, cmap, conmap, st) =
|
adamc@185
|
609 foldl (fn ((sgi, _), (ds, cmap, conmap, st)) =>
|
adamc@49
|
610 case sgi of
|
adamc@49
|
611 L.SgiConAbs (x, n, k) =>
|
adamc@49
|
612 let
|
adamc@73
|
613 val (st, n') = St.bindCon st x n
|
adamc@49
|
614 in
|
adamc@49
|
615 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
|
adamc@49
|
616 cmap,
|
adamc@185
|
617 conmap,
|
adamc@49
|
618 st)
|
adamc@49
|
619 end
|
adamc@49
|
620 | L.SgiCon (x, n, k, _) =>
|
adamc@49
|
621 let
|
adamc@73
|
622 val (st, n') = St.bindCon st x n
|
adamc@49
|
623 in
|
adamc@49
|
624 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
|
adamc@49
|
625 cmap,
|
adamc@185
|
626 conmap,
|
adamc@185
|
627 st)
|
adamc@185
|
628 end
|
adamc@185
|
629
|
adamc@185
|
630 | L.SgiDatatype (x, n, xnts) =>
|
adamc@185
|
631 let
|
adamc@185
|
632 val (st, n') = St.bindCon st x n
|
adamc@185
|
633 val (xnts, (st, cmap, conmap)) =
|
adamc@185
|
634 ListUtil.foldlMap
|
adamc@185
|
635 (fn ((x', n, to), (st, cmap, conmap)) =>
|
adamc@185
|
636 let
|
adamc@185
|
637 val st = St.bindConstructor st x' n
|
adamc@185
|
638 (L'.PConFfi {mod = m,
|
adamc@185
|
639 datatyp = x,
|
adamc@185
|
640 con = x'})
|
adamc@185
|
641 val st = St.bindConstructorVal st x' n
|
adamc@185
|
642
|
adamc@185
|
643 val dt = (L'.CNamed n', loc)
|
adamc@185
|
644
|
adamc@185
|
645 val (to, cmap) =
|
adamc@185
|
646 case to of
|
adamc@185
|
647 NONE => (NONE, SM.insert (cmap, x', dt))
|
adamc@185
|
648 | SOME t =>
|
adamc@185
|
649 let
|
adamc@185
|
650 val t = corifyCon st t
|
adamc@185
|
651 in
|
adamc@185
|
652 (SOME t, SM.insert (cmap, x',
|
adamc@185
|
653 (L'.TFun (t, dt), loc)))
|
adamc@185
|
654 end
|
adamc@185
|
655
|
adamc@185
|
656 val conmap = SM.insert (conmap, x', x)
|
adamc@185
|
657 in
|
adamc@185
|
658 ((x', n, to),
|
adamc@185
|
659 (st, cmap, conmap))
|
adamc@185
|
660 end) (st, cmap, conmap) xnts
|
adamc@185
|
661 in
|
adamc@185
|
662 ((L'.DDatatype (x, n', xnts), loc) :: ds,
|
adamc@185
|
663 cmap,
|
adamc@185
|
664 conmap,
|
adamc@49
|
665 st)
|
adamc@49
|
666 end
|
adamc@49
|
667
|
adamc@49
|
668 | L.SgiVal (x, _, c) =>
|
adamc@49
|
669 (ds,
|
adamc@49
|
670 SM.insert (cmap, x, corifyCon st c),
|
adamc@185
|
671 conmap,
|
adamc@49
|
672 st)
|
adamc@185
|
673 | _ => (ds, cmap, conmap, st)) ([], SM.empty, SM.empty, st) sgis
|
adamc@49
|
674
|
adamc@185
|
675 val st = St.bindStr st m n (St.ffi m cmap conmap)
|
adamc@49
|
676 in
|
adamc@49
|
677 (rev ds, st)
|
adamc@49
|
678 end
|
adamc@49
|
679 | _ => raise Fail "Non-const signature for FFI structure")
|
adamc@48
|
680
|
adamc@109
|
681 | L.DExport (en, sgn, str) =>
|
adamc@109
|
682 (case #1 sgn of
|
adamc@109
|
683 L.SgnConst sgis =>
|
adamc@109
|
684 let
|
adamc@109
|
685 fun pathify (str, _) =
|
adamc@109
|
686 case str of
|
adamc@109
|
687 L.StrVar m => SOME (m, [])
|
adamc@109
|
688 | L.StrProj (str, s) =>
|
adamc@109
|
689 Option.map (fn (m, ms) => (m, ms @ [s])) (pathify str)
|
adamc@109
|
690 | _ => NONE
|
adamc@109
|
691 in
|
adamc@109
|
692 case pathify str of
|
adamc@109
|
693 NONE => (ErrorMsg.errorAt loc "Structure is too fancy to export";
|
adamc@109
|
694 ([], st))
|
adamc@109
|
695 | SOME (m, ms) =>
|
adamc@109
|
696 let
|
adamc@109
|
697 fun wrapSgi ((sgi, _), (wds, eds)) =
|
adamc@109
|
698 case sgi of
|
adamc@109
|
699 L.SgiVal (s, _, t as (L.TFun (dom, ran), _)) =>
|
adamc@109
|
700 (case (#1 dom, #1 ran) of
|
adamc@147
|
701 (L.TRecord (L.CRecord (_, []), _),
|
adamc@139
|
702 L.CApp
|
adamc@139
|
703 ((L.CApp
|
adamc@139
|
704 ((L.CApp ((L.CModProj (_, [], "xml"), _),
|
adamc@139
|
705 (L.CRecord (_, [((L.CName "Html", _),
|
adamc@139
|
706 _)]), _)), _), _), _), _)) =>
|
adamc@109
|
707 let
|
adamc@109
|
708 val ran = (L.TRecord (L.CRecord ((L.KType, loc), []), loc), loc)
|
adamc@109
|
709 val e = (L.EModProj (m, ms, s), loc)
|
adamc@109
|
710 val e = (L.EAbs ("vs", dom, ran,
|
adamc@109
|
711 (L.EWrite (L.EApp (e, (L.ERel 0, loc)), loc), loc)), loc)
|
adamc@109
|
712 in
|
adamc@109
|
713 ((L.DVal ("wrap_" ^ s, 0,
|
adamc@109
|
714 (L.TFun (dom, ran), loc),
|
adamc@109
|
715 e), loc) :: wds,
|
adamc@109
|
716 (fn st =>
|
adamc@109
|
717 case #1 (corifyExp st (L.EModProj (en, [], "wrap_" ^ s), loc)) of
|
adamc@144
|
718 L'.ENamed n => (L'.DExport (L'.Link, n), loc)
|
adamc@109
|
719 | _ => raise Fail "Corify: Value to export didn't corify properly")
|
adamc@109
|
720 :: eds)
|
adamc@109
|
721 end
|
adamc@109
|
722 | _ => (wds, eds))
|
adamc@109
|
723 | _ => (wds, eds)
|
adamc@102
|
724
|
adamc@109
|
725 val (wds, eds) = foldl wrapSgi ([], []) sgis
|
adamc@109
|
726 val wrapper = (L.StrConst wds, loc)
|
adamc@109
|
727 val (ds, {inner, outer}) = corifyStr (wrapper, st)
|
adamc@109
|
728 val st = St.bindStr outer "wrapper" en inner
|
adamc@109
|
729
|
adamc@109
|
730 val ds = ds @ map (fn f => f st) eds
|
adamc@109
|
731 in
|
adamc@109
|
732 (ds, st)
|
adamc@109
|
733 end
|
adamc@109
|
734 end
|
adamc@109
|
735 | _ => raise Fail "Non-const signature for 'export'")
|
adamc@48
|
736
|
adamc@39
|
737 and corifyStr ((str, _), st) =
|
adamc@39
|
738 case str of
|
adamc@39
|
739 L.StrConst ds =>
|
adamc@39
|
740 let
|
adamc@39
|
741 val st = St.enter st
|
adamc@39
|
742 val (ds, st) = ListUtil.foldlMapConcat corifyDecl st ds
|
adamc@39
|
743 in
|
adamc@39
|
744 (ds, St.leave st)
|
adamc@39
|
745 end
|
adamc@39
|
746 | L.StrVar n => ([], {inner = St.lookupStrById st n, outer = st})
|
adamc@39
|
747 | L.StrProj (str, x) =>
|
adamc@39
|
748 let
|
adamc@39
|
749 val (ds, {inner, outer}) = corifyStr (str, st)
|
adamc@39
|
750 in
|
adamc@39
|
751 (ds, {inner = St.lookupStrByName (x, inner), outer = outer})
|
adamc@39
|
752 end
|
adamc@46
|
753 | L.StrFun _ => raise Fail "Corify of nested functor definition"
|
adamc@46
|
754 | L.StrApp (str1, str2) =>
|
adamc@46
|
755 let
|
adamc@46
|
756 fun unwind' (str, _) =
|
adamc@46
|
757 case str of
|
adamc@46
|
758 L.StrVar n => St.lookupStrById st n
|
adamc@46
|
759 | L.StrProj (str, x) => St.lookupStrByName (x, unwind' str)
|
adamc@46
|
760 | _ => raise Fail "Corify of fancy functor application [1]"
|
adamc@46
|
761
|
adamc@46
|
762 fun unwind (str, _) =
|
adamc@46
|
763 case str of
|
adamc@46
|
764 L.StrVar n => St.lookupFunctorById st n
|
adamc@46
|
765 | L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str)
|
adamc@46
|
766 | _ => raise Fail "Corify of fancy functor application [2]"
|
adamc@46
|
767
|
adamc@146
|
768 val (xa, na, body) = unwind str1
|
adamc@46
|
769
|
adamc@146
|
770 val (ds1, {inner = inner', outer}) = corifyStr (str2, st)
|
adamc@146
|
771 val (ds2, {inner, outer}) = corifyStr (body, St.bindStr outer xa na inner')
|
adamc@46
|
772 in
|
adamc@146
|
773 (ds1 @ ds2, {inner = St.bindStr inner xa na inner', outer = outer})
|
adamc@46
|
774 end
|
adamc@31
|
775
|
adamc@39
|
776 fun maxName ds = foldl (fn ((d, _), n) =>
|
adamc@39
|
777 case d of
|
adamc@39
|
778 L.DCon (_, n', _, _) => Int.max (n, n')
|
adamc@162
|
779 | L.DDatatype (_, n', _) => Int.max (n, n')
|
adamc@162
|
780 | L.DDatatypeImp (_, n', _, _, _, _) => Int.max (n, n')
|
adamc@124
|
781 | L.DVal (_, n', _, _) => Int.max (n, n')
|
adamc@124
|
782 | L.DValRec vis => foldl (fn ((_, n', _, _), n) => Int.max (n, n)) n vis
|
adamc@39
|
783 | L.DSgn (_, n', _) => Int.max (n, n')
|
adamc@48
|
784 | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str))
|
adamc@100
|
785 | L.DFfiStr (_, n', _) => Int.max (n, n')
|
adamc@109
|
786 | L.DExport _ => n)
|
adamc@39
|
787 0 ds
|
adamc@39
|
788
|
adamc@39
|
789 and maxNameStr (str, _) =
|
adamc@39
|
790 case str of
|
adamc@39
|
791 L.StrConst ds => maxName ds
|
adamc@39
|
792 | L.StrVar n => n
|
adamc@39
|
793 | L.StrProj (str, _) => maxNameStr str
|
adamc@45
|
794 | L.StrFun (_, _, _, _, str) => maxNameStr str
|
adamc@45
|
795 | L.StrApp (str1, str2) => Int.max (maxNameStr str1, maxNameStr str2)
|
adamc@39
|
796
|
adamc@39
|
797 fun corify ds =
|
adamc@39
|
798 let
|
adamc@39
|
799 val () = reset (maxName ds + 1)
|
adamc@146
|
800
|
adamc@39
|
801 val (ds, _) = ListUtil.foldlMapConcat corifyDecl St.empty ds
|
adamc@39
|
802 in
|
adamc@39
|
803 ds
|
adamc@39
|
804 end
|
adamc@16
|
805
|
adamc@16
|
806 end
|