Mercurial > urweb

comparison src/corify.sml @ 249:b6b75e6e0898

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Corify transaction wrappers
author Adam Chlipala <adamc@hcoop.net>
date Sun, 31 Aug 2008 09:45:23 -0400
parents 5c50b17f5e4a
children 326fb4686f60
comparison
equal deleted inserted replaced
248:d5b12daa9b47 249:b6b75e6e0898
62 62
63 val enter : t -> t 63 val enter : t -> t
64 val leave : t -> {outer : t, inner : t} 64 val leave : t -> {outer : t, inner : t}
65 val ffi : string -> L'.con SM.map -> (string * string list * L'.con option * L'.datatype_kind) SM.map -> t 65 val ffi : string -> L'.con SM.map -> (string * string list * L'.con option * L'.datatype_kind) SM.map -> t
66 66
67 val basisIs : t * int -> t
68 val lookupBasis : t -> int option
69
67 datatype core_con = 70 datatype core_con =
68 CNormal of int 71 CNormal of int
69 | CFfi of string 72 | CFfi of string
70 val bindCon : t -> string -> int -> t * int 73 val bindCon : t -> string -> int -> t * int
71 val lookupConById : t -> int -> int option 74 val lookupConById : t -> int -> int option
73 76
74 val bindConstructor : t -> string -> int -> L'.patCon -> t 77 val bindConstructor : t -> string -> int -> L'.patCon -> t
75 val lookupConstructorByNameOpt : t -> string -> L'.patCon option 78 val lookupConstructorByNameOpt : t -> string -> L'.patCon option
76 val lookupConstructorByName : t -> string -> L'.patCon 79 val lookupConstructorByName : t -> string -> L'.patCon
77 val lookupConstructorById : t -> int -> L'.patCon 80 val lookupConstructorById : t -> int -> L'.patCon
78 81
79 datatype core_val = 82 datatype core_val =
80 ENormal of int 83 ENormal of int
81 | EFfi of string * L'.con 84 | EFfi of string * L'.con
82 val bindVal : t -> string -> int -> t * int 85 val bindVal : t -> string -> int -> t * int
83 val bindConstructorVal : t -> string -> int -> t 86 val bindConstructorVal : t -> string -> int -> t
84 val lookupValById : t -> int -> int option 87 val lookupValById : t -> int -> int option
85 val lookupValByName : t -> string -> core_val 88 val lookupValByName : t -> string -> core_val
86 89
87 val bindStr : t -> string -> int -> t -> t 90 val bindStr : t -> string -> int -> t -> t
88 val lookupStrById : t -> int -> t 91 val lookupStrById : t -> int -> t
89 val lookupStrByName : string * t -> t 92 val lookupStrByName : string * t -> t
90 93
91 val bindFunctor : t -> string -> int -> string -> int -> L.str -> t 94 val bindFunctor : t -> string -> int -> string -> int -> L.str -> t
92 val lookupFunctorById : t -> int -> string * int * L.str 95 val lookupFunctorById : t -> int -> string * int * L.str
93 val lookupFunctorByName : string * t -> string * int * L.str 96 val lookupFunctorByName : string * t -> string * int * L.str
94 end = struct 97 end = struct
95 98
96 datatype flattening = 99 datatype flattening =
97 FNormal of {cons : int SM.map, 100 FNormal of {cons : int SM.map,
98 constructors : L'.patCon SM.map, 101 constructors : L'.patCon SM.map,
99 vals : int SM.map, 102 vals : int SM.map,
100 strs : flattening SM.map, 103 strs : flattening SM.map,
101 funs : (string * int * L.str) SM.map} 104 funs : (string * int * L.str) SM.map}
102 | FFfi of {mod : string, 105 | FFfi of {mod : string,
103 vals : L'.con SM.map, 106 vals : L'.con SM.map,
104 constructors : (string * string list * L'.con option * L'.datatype_kind) SM.map} 107 constructors : (string * string list * L'.con option * L'.datatype_kind) SM.map}
105 108
106 type t = { 109 type t = {
107 cons : int IM.map, 110 basis : int option,
108 constructors : L'.patCon IM.map, 111 cons : int IM.map,
109 vals : int IM.map, 112 constructors : L'.patCon IM.map,
110 strs : flattening IM.map, 113 vals : int IM.map,
111 funs : (string * int * L.str) IM.map, 114 strs : flattening IM.map,
112 current : flattening, 115 funs : (string * int * L.str) IM.map,
113 nested : flattening list 116 current : flattening,
114 } 117 nested : flattening list
115 118 }
116 val empty = { 119
117 cons = IM.empty, 120 val empty = {
118 constructors = IM.empty, 121 basis = NONE,
119 vals = IM.empty, 122 cons = IM.empty,
120 strs = IM.empty, 123 constructors = IM.empty,
121 funs = IM.empty, 124 vals = IM.empty,
122 current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty }, 125 strs = IM.empty,
123 nested = [] 126 funs = IM.empty,
124 } 127 current = FNormal { cons = SM.empty, constructors = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty },
125 128 nested = []
126 fun debug ({current = FNormal {cons, constructors, vals, strs, funs}, ...} : t) = 129 }
127 print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; " 130
128 ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; " 131 fun debug ({current = FNormal {cons, constructors, vals, strs, funs}, ...} : t) =
129 ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; " 132 print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; "
130 ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; " 133 ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; "
131 ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n") 134 ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; "
132 | debug _ = print "Not normal!\n" 135 ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; "
133 136 ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n")
134 datatype core_con = 137 | debug _ = print "Not normal!\n"
135 CNormal of int 138
136 | CFfi of string 139 fun basisIs ({cons, constructors, vals, strs, funs, current, nested, ...} : t, basis) =
137 140 {basis = SOME basis,
138 datatype core_val = 141 cons = cons,
139 ENormal of int 142 constructors = constructors,
140 | EFfi of string * L'.con 143 vals = vals,
141 144 strs = strs,
142 fun bindCon {cons, constructors, vals, strs, funs, current, nested} s n = 145 funs = funs,
143 let 146 current = current,
144 val n' = alloc () 147 nested = nested}
145 148
146 val current = 149 fun lookupBasis ({basis, ...} : t) = basis
147 case current of 150
148 FFfi _ => raise Fail "Binding inside FFfi" 151 datatype core_con =
149 | FNormal {cons, constructors, vals, strs, funs} => 152 CNormal of int
150 FNormal {cons = SM.insert (cons, s, n'), 153 | CFfi of string
151 constructors = constructors, 154
152 vals = vals, 155 datatype core_val =
153 strs = strs, 156 ENormal of int
154 funs = funs} 157 | EFfi of string * L'.con
155 in 158
156 ({cons = IM.insert (cons, n, n'), 159 fun bindCon {basis, cons, constructors, vals, strs, funs, current, nested} s n =
157 constructors = constructors, 160 let
158 vals = vals, 161 val n' = alloc ()
159 strs = strs, 162
160 funs = funs, 163 val current =
161 current = current, 164 case current of
162 nested = nested}, 165 FFfi _ => raise Fail "Binding inside FFfi"
163 n') 166 | FNormal {cons, constructors, vals, strs, funs} =>
164 end 167 FNormal {cons = SM.insert (cons, s, n'),
165 168 constructors = constructors,
166 fun lookupConById ({cons, ...} : t) n = IM.find (cons, n) 169 vals = vals,
167 170 strs = strs,
168 fun lookupConByName ({current, ...} : t) x = 171 funs = funs}
169 case current of 172 in
170 FFfi {mod = m, ...} => CFfi m 173 ({basis = basis,
171 | FNormal {cons, ...} => 174 cons = IM.insert (cons, n, n'),
172 case SM.find (cons, x) of
173 NONE => raise Fail "Corify.St.lookupConByName"
174 | SOME n => CNormal n
175
176 fun bindVal {cons, constructors, vals, strs, funs, current, nested} s n =
177 let
178 val n' = alloc ()
179
180 val current =
181 case current of
182 FFfi _ => raise Fail "Binding inside FFfi"
183 | FNormal {cons, constructors, vals, strs, funs} =>
184 FNormal {cons = cons,
185 constructors = constructors,
186 vals = SM.insert (vals, s, n'),
187 strs = strs,
188 funs = funs}
189 in
190 ({cons = cons,
191 constructors = constructors,
192 vals = IM.insert (vals, n, n'),
193 strs = strs,
194 funs = funs,
195 current = current,
196 nested = nested},
197 n')
198 end
199
200 fun bindConstructorVal {cons, constructors, vals, strs, funs, current, nested} s n =
201 let
202 val current =
203 case current of
204 FFfi _ => raise Fail "Binding inside FFfi"
205 | FNormal {cons, constructors, vals, strs, funs} =>
206 FNormal {cons = cons,
207 constructors = constructors,
208 vals = SM.insert (vals, s, n),
209 strs = strs,
210 funs = funs}
211 in
212 {cons = cons,
213 constructors = constructors, 175 constructors = constructors,
214 vals = IM.insert (vals, n, n),
215 strs = strs,
216 funs = funs,
217 current = current,
218 nested = nested}
219 end
220
221
222 fun lookupValById ({vals, ...} : t) n = IM.find (vals, n)
223
224 fun lookupValByName ({current, ...} : t) x =
225 case current of
226 FFfi {mod = m, vals, ...} =>
227 (case SM.find (vals, x) of
228 NONE => raise Fail "Corify.St.lookupValByName: no type for FFI val"
229 | SOME t => EFfi (m, t))
230 | FNormal {vals, ...} =>
231 case SM.find (vals, x) of
232 NONE => raise Fail "Corify.St.lookupValByName"
233 | SOME n => ENormal n
234
235 fun bindConstructor {cons, constructors, vals, strs, funs, current, nested} s n n' =
236 let
237 val current =
238 case current of
239 FFfi _ => raise Fail "Binding inside FFfi"
240 | FNormal {cons, constructors, vals, strs, funs} =>
241 FNormal {cons = cons,
242 constructors = SM.insert (constructors, s, n'),
243 vals = vals,
244 strs = strs,
245 funs = funs}
246 in
247 {cons = cons,
248 constructors = IM.insert (constructors, n, n'),
249 vals = vals, 176 vals = vals,
250 strs = strs, 177 strs = strs,
251 funs = funs, 178 funs = funs,
252 current = current, 179 current = current,
253 nested = nested} 180 nested = nested},
254 end 181 n')
255 182 end
256 fun lookupConstructorById ({constructors, ...} : t) n = 183
257 case IM.find (constructors, n) of 184 fun lookupConById ({cons, ...} : t) n = IM.find (cons, n)
258 NONE => raise Fail "Corify.St.lookupConstructorById" 185
259 | SOME x => x 186 fun lookupConByName ({current, ...} : t) x =
260 187 case current of
261 fun lookupConstructorByNameOpt ({current, ...} : t) x = 188 FFfi {mod = m, ...} => CFfi m
262 case current of 189 | FNormal {cons, ...} =>
263 FFfi {mod = m, constructors, ...} => 190 case SM.find (cons, x) of
264 (case SM.find (constructors, x) of 191 NONE => raise Fail "Corify.St.lookupConByName"
265 NONE => NONE 192 | SOME n => CNormal n
266 | SOME (n, xs, to, dk) => SOME (L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk})) 193
267 | FNormal {constructors, ...} => 194 fun bindVal {basis, cons, constructors, vals, strs, funs, current, nested} s n =
268 case SM.find (constructors, x) of 195 let
196 val n' = alloc ()
197
198 val current =
199 case current of
200 FFfi _ => raise Fail "Binding inside FFfi"
201 | FNormal {cons, constructors, vals, strs, funs} =>
202 FNormal {cons = cons,
203 constructors = constructors,
204 vals = SM.insert (vals, s, n'),
205 strs = strs,
206 funs = funs}
207 in
208 ({basis = basis,
209 cons = cons,
210 constructors = constructors,
211 vals = IM.insert (vals, n, n'),
212 strs = strs,
213 funs = funs,
214 current = current,
215 nested = nested},
216 n')
217 end
218
219 fun bindConstructorVal {basis, cons, constructors, vals, strs, funs, current, nested} s n =
220 let
221 val current =
222 case current of
223 FFfi _ => raise Fail "Binding inside FFfi"
224 | FNormal {cons, constructors, vals, strs, funs} =>
225 FNormal {cons = cons,
226 constructors = constructors,
227 vals = SM.insert (vals, s, n),
228 strs = strs,
229 funs = funs}
230 in
231 {basis = basis,
232 cons = cons,
233 constructors = constructors,
234 vals = IM.insert (vals, n, n),
235 strs = strs,
236 funs = funs,
237 current = current,
238 nested = nested}
239 end
240
241
242 fun lookupValById ({vals, ...} : t) n = IM.find (vals, n)
243
244 fun lookupValByName ({current, ...} : t) x =
245 case current of
246 FFfi {mod = m, vals, ...} =>
247 (case SM.find (vals, x) of
248 NONE => raise Fail "Corify.St.lookupValByName: no type for FFI val"
249 | SOME t => EFfi (m, t))
250 | FNormal {vals, ...} =>
251 case SM.find (vals, x) of
252 NONE => raise Fail "Corify.St.lookupValByName"
253 | SOME n => ENormal n
254
255 fun bindConstructor {basis, cons, constructors, vals, strs, funs, current, nested} s n n' =
256 let
257 val current =
258 case current of
259 FFfi _ => raise Fail "Binding inside FFfi"
260 | FNormal {cons, constructors, vals, strs, funs} =>
261 FNormal {cons = cons,
262 constructors = SM.insert (constructors, s, n'),
263 vals = vals,
264 strs = strs,
265 funs = funs}
266 in
267 {basis = basis,
268 cons = cons,
269 constructors = IM.insert (constructors, n, n'),
270 vals = vals,
271 strs = strs,
272 funs = funs,
273 current = current,
274 nested = nested}
275 end
276
277 fun lookupConstructorById ({constructors, ...} : t) n =
278 case IM.find (constructors, n) of
279 NONE => raise Fail "Corify.St.lookupConstructorById"
280 | SOME x => x
281
282 fun lookupConstructorByNameOpt ({current, ...} : t) x =
283 case current of
284 FFfi {mod = m, constructors, ...} =>
285 (case SM.find (constructors, x) of
269 NONE => NONE 286 NONE => NONE
270 | SOME n => SOME n 287 | SOME (n, xs, to, dk) => SOME (L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk}))
271 288 | FNormal {constructors, ...} =>
272 fun lookupConstructorByName ({current, ...} : t) x = 289 case SM.find (constructors, x) of
273 case current of 290 NONE => NONE
274 FFfi {mod = m, constructors, ...} => 291 | SOME n => SOME n
275 (case SM.find (constructors, x) of 292
276 NONE => raise Fail "Corify.St.lookupConstructorByName [1]" 293 fun lookupConstructorByName ({current, ...} : t) x =
277 | SOME (n, xs, to, dk) => L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk}) 294 case current of
278 | FNormal {constructors, ...} => 295 FFfi {mod = m, constructors, ...} =>
279 case SM.find (constructors, x) of 296 (case SM.find (constructors, x) of
280 NONE => raise Fail "Corify.St.lookupConstructorByName [2]" 297 NONE => raise Fail "Corify.St.lookupConstructorByName [1]"
281 | SOME n => n 298 | SOME (n, xs, to, dk) => L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk})
282 299 | FNormal {constructors, ...} =>
283 fun enter {cons, constructors, vals, strs, funs, current, nested} = 300 case SM.find (constructors, x) of
284 {cons = cons, 301 NONE => raise Fail "Corify.St.lookupConstructorByName [2]"
285 constructors = constructors, 302 | SOME n => n
286 vals = vals, 303
287 strs = strs, 304 fun enter {basis, cons, constructors, vals, strs, funs, current, nested} =
288 funs = funs, 305 {basis = basis,
289 current = FNormal {cons = SM.empty, 306 cons = cons,
290 constructors = SM.empty, 307 constructors = constructors,
291 vals = SM.empty, 308 vals = vals,
292 strs = SM.empty, 309 strs = strs,
293 funs = SM.empty}, 310 funs = funs,
294 nested = current :: nested} 311 current = FNormal {cons = SM.empty,
295 312 constructors = SM.empty,
296 fun dummy f = {cons = IM.empty, 313 vals = SM.empty,
297 constructors = IM.empty, 314 strs = SM.empty,
298 vals = IM.empty, 315 funs = SM.empty},
299 strs = IM.empty, 316 nested = current :: nested}
300 funs = IM.empty, 317
301 current = f, 318 fun dummy (b, f) = {basis = b,
302 nested = []} 319 cons = IM.empty,
303 320 constructors = IM.empty,
304 fun leave {cons, constructors, vals, strs, funs, current, nested = m1 :: rest} = 321 vals = IM.empty,
305 {outer = {cons = cons, 322 strs = IM.empty,
306 constructors = constructors, 323 funs = IM.empty,
307 vals = vals, 324 current = f,
308 strs = strs, 325 nested = []}
309 funs = funs, 326
310 current = m1, 327 fun leave {basis, cons, constructors, vals, strs, funs, current, nested = m1 :: rest} =
311 nested = rest}, 328 {outer = {basis = basis,
312 inner = dummy current} 329 cons = cons,
313 | leave _ = raise Fail "Corify.St.leave" 330 constructors = constructors,
314 331 vals = vals,
315 fun ffi m vals constructors = dummy (FFfi {mod = m, vals = vals, constructors = constructors}) 332 strs = strs,
316 333 funs = funs,
317 fun bindStr ({cons, constructors, vals, strs, funs, 334 current = m1,
318 current = FNormal {cons = mcons, constructors = mconstructors, 335 nested = rest},
319 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) 336 inner = dummy (basis, current)}
320 x n ({current = f, ...} : t) = 337 | leave _ = raise Fail "Corify.St.leave"
321 {cons = cons, 338
322 constructors = constructors, 339 fun ffi m vals constructors = dummy (NONE, FFfi {mod = m, vals = vals, constructors = constructors})
323 vals = vals, 340
324 strs = IM.insert (strs, n, f), 341 fun bindStr ({basis, cons, constructors, vals, strs, funs,
325 funs = funs, 342 current = FNormal {cons = mcons, constructors = mconstructors,
326 current = FNormal {cons = mcons, 343 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
327 constructors = mconstructors, 344 x n ({current = f, ...} : t) =
328 vals = mvals, 345 {basis = basis,
329 strs = SM.insert (mstrs, x, f), 346 cons = cons,
330 funs = mfuns}, 347 constructors = constructors,
331 nested = nested} 348 vals = vals,
332 | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr" 349 strs = IM.insert (strs, n, f),
333 350 funs = funs,
334 fun lookupStrById ({strs, ...} : t) n = 351 current = FNormal {cons = mcons,
335 case IM.find (strs, n) of 352 constructors = mconstructors,
336 NONE => raise Fail "Corify.St.lookupStrById" 353 vals = mvals,
337 | SOME f => dummy f 354 strs = SM.insert (mstrs, x, f),
338 355 funs = mfuns},
339 fun lookupStrByName (m, {current = FNormal {strs, ...}, ...} : t) = 356 nested = nested}
340 (case SM.find (strs, m) of 357 | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr"
341 NONE => raise Fail "Corify.St.lookupStrByName" 358
342 | SOME f => dummy f) 359 fun lookupStrById ({basis, strs, ...} : t) n =
343 | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName" 360 case IM.find (strs, n) of
344 361 NONE => raise Fail "Corify.St.lookupStrById"
345 fun bindFunctor ({cons, constructors, vals, strs, funs, 362 | SOME f => dummy (basis, f)
346 current = FNormal {cons = mcons, constructors = mconstructors, 363
347 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t) 364 fun lookupStrByName (m, {basis, current = FNormal {strs, ...}, ...} : t) =
348 x n xa na str = 365 (case SM.find (strs, m) of
349 {cons = cons, 366 NONE => raise Fail "Corify.St.lookupStrByName"
350 constructors = constructors, 367 | SOME f => dummy (basis, f))
351 vals = vals, 368 | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName"
352 strs = strs, 369
353 funs = IM.insert (funs, n, (xa, na, str)), 370 fun bindFunctor ({basis, cons, constructors, vals, strs, funs,
354 current = FNormal {cons = mcons, 371 current = FNormal {cons = mcons, constructors = mconstructors,
355 constructors = mconstructors, 372 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
356 vals = mvals, 373 x n xa na str =
357 strs = mstrs, 374 {basis = basis,
358 funs = SM.insert (mfuns, x, (xa, na, str))}, 375 cons = cons,
359 nested = nested} 376 constructors = constructors,
360 | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor" 377 vals = vals,
361 378 strs = strs,
362 fun lookupFunctorById ({funs, ...} : t) n = 379 funs = IM.insert (funs, n, (xa, na, str)),
363 case IM.find (funs, n) of 380 current = FNormal {cons = mcons,
364 NONE => raise Fail "Corify.St.lookupFunctorById" 381 constructors = mconstructors,
365 | SOME v => v 382 vals = mvals,
366 383 strs = mstrs,
367 fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) = 384 funs = SM.insert (mfuns, x, (xa, na, str))},
368 (case SM.find (funs, m) of 385 nested = nested}
369 NONE => raise Fail "Corify.St.lookupFunctorByName" 386 | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
370 | SOME v => v) 387
371 | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName" 388 fun lookupFunctorById ({funs, ...} : t) n =
372 389 case IM.find (funs, n) of
373 end 390 NONE => raise Fail "Corify.St.lookupFunctorById"
374 391 | SOME v => v
375 392
376 fun corifyKind (k, loc) = 393 fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) =
377 case k of 394 (case SM.find (funs, m) of
378 L.KType => (L'.KType, loc) 395 NONE => raise Fail "Corify.St.lookupFunctorByName"
379 | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc) 396 | SOME v => v)
380 | L.KName => (L'.KName, loc) 397 | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName"
381 | L.KRecord k => (L'.KRecord (corifyKind k), loc) 398
382 | L.KUnit => (L'.KUnit, loc) 399 end
383 | L.KTuple ks => (L'.KTuple (map corifyKind ks), loc) 400
384 401
385 fun corifyCon st (c, loc) = 402 fun corifyKind (k, loc) =
386 case c of 403 case k of
387 L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc) 404 L.KType => (L'.KType, loc)
388 | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc) 405 | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc)
389 | L.TRecord c => (L'.TRecord (corifyCon st c), loc) 406 | L.KName => (L'.KName, loc)
390 407 | L.KRecord k => (L'.KRecord (corifyKind k), loc)
391 | L.CRel n => (L'.CRel n, loc) 408 | L.KUnit => (L'.KUnit, loc)
392 | L.CNamed n => 409 | L.KTuple ks => (L'.KTuple (map corifyKind ks), loc)
393 (case St.lookupConById st n of 410
394 NONE => (L'.CNamed n, loc) 411 fun corifyCon st (c, loc) =
395 | SOME n => (L'.CNamed n, loc)) 412 case c of
396 | L.CModProj (m, ms, x) => 413 L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc)
397 let 414 | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc)
398 val st = St.lookupStrById st m 415 | L.TRecord c => (L'.TRecord (corifyCon st c), loc)
399 val st = foldl St.lookupStrByName st ms 416
400 in 417 | L.CRel n => (L'.CRel n, loc)
401 case St.lookupConByName st x of 418 | L.CNamed n =>
402 St.CNormal n => (L'.CNamed n, loc) 419 (case St.lookupConById st n of
403 | St.CFfi m => (L'.CFfi (m, x), loc) 420 NONE => (L'.CNamed n, loc)
404 end 421 | SOME n => (L'.CNamed n, loc))
405 422 | L.CModProj (m, ms, x) =>
406 | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc) 423 let
407 | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc) 424 val st = St.lookupStrById st m
408 425 val st = foldl St.lookupStrByName st ms
409 | L.CName s => (L'.CName s, loc) 426 in
410 427 case St.lookupConByName st x of
411 | L.CRecord (k, xcs) => 428 St.CNormal n => (L'.CNamed n, loc)
412 (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc) 429 | St.CFfi m => (L'.CFfi (m, x), loc)
413 | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc) 430 end
414 | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc) 431
415 | L.CUnit => (L'.CUnit, loc) 432 | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc)
416 433 | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc)
417 | L.CTuple cs => (L'.CTuple (map (corifyCon st) cs), loc) 434
418 | L.CProj (c, n) => (L'.CProj (corifyCon st c, n), loc) 435 | L.CName s => (L'.CName s, loc)
419 436
420 fun corifyPatCon st pc = 437 | L.CRecord (k, xcs) =>
421 case pc of 438 (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc)
422 L.PConVar n => St.lookupConstructorById st n 439 | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc)
423 | L.PConProj (m1, ms, x) => 440 | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc)
424 let 441 | L.CUnit => (L'.CUnit, loc)
425 val st = St.lookupStrById st m1 442
426 val st = foldl St.lookupStrByName st ms 443 | L.CTuple cs => (L'.CTuple (map (corifyCon st) cs), loc)
427 in 444 | L.CProj (c, n) => (L'.CProj (corifyCon st c, n), loc)
428 St.lookupConstructorByName st x 445
429 end 446 fun corifyPatCon st pc =
430 447 case pc of
431 fun corifyPat st (p, loc) = 448 L.PConVar n => St.lookupConstructorById st n
432 case p of 449 | L.PConProj (m1, ms, x) =>
433 L.PWild => (L'.PWild, loc) 450 let
434 | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc) 451 val st = St.lookupStrById st m1
435 | L.PPrim p => (L'.PPrim p, loc) 452 val st = foldl St.lookupStrByName st ms
436 | L.PCon (dk, pc, ts, po) => (L'.PCon (dk, corifyPatCon st pc, map (corifyCon st) ts, 453 in
437 Option.map (corifyPat st) po), loc) 454 St.lookupConstructorByName st x
438 | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc) 455 end
439 456
440 fun corifyExp st (e, loc) = 457 fun corifyPat st (p, loc) =
441 case e of 458 case p of
442 L.EPrim p => (L'.EPrim p, loc) 459 L.PWild => (L'.PWild, loc)
443 | L.ERel n => (L'.ERel n, loc) 460 | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc)
444 | L.ENamed n => 461 | L.PPrim p => (L'.PPrim p, loc)
445 (case St.lookupValById st n of 462 | L.PCon (dk, pc, ts, po) => (L'.PCon (dk, corifyPatCon st pc, map (corifyCon st) ts,
446 NONE => (L'.ENamed n, loc) 463 Option.map (corifyPat st) po), loc)
447 | SOME n => (L'.ENamed n, loc)) 464 | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc)
448 | L.EModProj (m, ms, x) => 465
449 let 466 fun corifyExp st (e, loc) =
450 val st = St.lookupStrById st m 467 case e of
451 val st = foldl St.lookupStrByName st ms 468 L.EPrim p => (L'.EPrim p, loc)
452 in 469 | L.ERel n => (L'.ERel n, loc)
453 case St.lookupConstructorByNameOpt st x of 470 | L.ENamed n =>
454 SOME (pc as L'.PConFfi {mod = m, datatyp, params, arg, kind, ...}) => 471 (case St.lookupValById st n of
455 let 472 NONE => (L'.ENamed n, loc)
456 val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) params 473 | SOME n => (L'.ENamed n, loc))
457 val e = case arg of 474 | L.EModProj (m, ms, x) =>
458 NONE => (L'.ECon (kind, pc, args, NONE), loc) 475 let
459 | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc), 476 val st = St.lookupStrById st m
460 (L'.ECon (kind, pc, args, SOME (L'.ERel 0, loc)), loc)), loc) 477 val st = foldl St.lookupStrByName st ms
461 478 in
462 val k = (L'.KType, loc) 479 case St.lookupConstructorByNameOpt st x of
463 in 480 SOME (pc as L'.PConFfi {mod = m, datatyp, params, arg, kind, ...}) =>
464 foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e params 481 let
465 end 482 val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) params
466 | _ => 483 val e = case arg of
467 case St.lookupValByName st x of 484 NONE => (L'.ECon (kind, pc, args, NONE), loc)
468 St.ENormal n => (L'.ENamed n, loc) 485 | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc),
469 | St.EFfi (m, t) => 486 (L'.ECon (kind, pc, args, SOME (L'.ERel 0, loc)), loc)), loc)
470 case t of 487
471 (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) => 488 val k = (L'.KType, loc)
472 (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc) 489 in
473 | t as (L'.TFun _, _) => 490 foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e params
474 let 491 end
475 fun getArgs (all as (t, _), args) = 492 | _ =>
476 case t of 493 case St.lookupValByName st x of
477 L'.TFun (dom, ran) => getArgs (ran, dom :: args) 494 St.ENormal n => (L'.ENamed n, loc)
478 | _ => (all, rev args) 495 | St.EFfi (m, t) =>
479 496 case t of
480 val (result, args) = getArgs (t, []) 497 (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) =>
481 498 (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc)
482 val (actuals, _) = foldr (fn (_, (actuals, n)) => 499 | t as (L'.TFun _, _) =>
483 ((L'.ERel n, loc) :: actuals, 500 let
484 n + 1)) ([], 0) args 501 fun getArgs (all as (t, _), args) =
485 val app = (L'.EFfiApp (m, x, actuals), loc) 502 case t of
486 val (abs, _, _) = foldr (fn (t, (abs, ran, n)) => 503 L'.TFun (dom, ran) => getArgs (ran, dom :: args)
487 ((L'.EAbs ("arg" ^ Int.toString n, 504 | _ => (all, rev args)
488 t, 505
489 ran, 506 val (result, args) = getArgs (t, [])
490 abs), loc), 507
491 (L'.TFun (t, ran), loc), 508 val (actuals, _) = foldr (fn (_, (actuals, n)) =>
492 n - 1)) (app, result, length args - 1) args 509 ((L'.ERel n, loc) :: actuals,
493 in 510 n + 1)) ([], 0) args
494 abs 511 val app = (L'.EFfiApp (m, x, actuals), loc)
495 end 512 val (abs, _, _) = foldr (fn (t, (abs, ran, n)) =>
496 | _ => (L'.EFfi (m, x), loc) 513 ((L'.EAbs ("arg" ^ Int.toString n,
497 end 514 t,
498 | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc) 515 ran,
499 | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc) 516 abs), loc),
500 | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc) 517 (L'.TFun (t, ran), loc),
501 | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc) 518 n - 1)) (app, result, length args - 1) args
502 519 in
503 | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => 520 abs
504 (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc) 521 end
505 | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c, 522 | _ => (L'.EFfi (m, x), loc)
506 {field = corifyCon st field, rest = corifyCon st rest}), loc) 523 end
507 | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c, 524 | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc)
508 {field = corifyCon st field, rest = corifyCon st rest}), loc) 525 | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc)
509 | L.EFold k => (L'.EFold (corifyKind k), loc) 526 | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc)
510 527 | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc)
511 | L.ECase (e, pes, {disc, result}) => 528
512 (L'.ECase (corifyExp st e, 529 | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) =>
513 map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes, 530 (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc)
514 {disc = corifyCon st disc, result = corifyCon st result}), 531 | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c,
515 loc) 532 {field = corifyCon st field, rest = corifyCon st rest}), loc)
516 533 | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c,
517 | L.EWrite e => (L'.EWrite (corifyExp st e), loc) 534 {field = corifyCon st field, rest = corifyCon st rest}), loc)
518 535 | L.EFold k => (L'.EFold (corifyKind k), loc)
519 fun corifyDecl ((d, loc : EM.span), st) = 536
520 case d of 537 | L.ECase (e, pes, {disc, result}) =>
521 L.DCon (x, n, k, c) => 538 (L'.ECase (corifyExp st e,
522 let 539 map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes,
523 val (st, n) = St.bindCon st x n 540 {disc = corifyCon st disc, result = corifyCon st result}),
524 in 541 loc)
525 ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) 542
526 end 543 | L.EWrite e => (L'.EWrite (corifyExp st e), loc)
527 | L.DDatatype (x, n, xs, xncs) => 544
528 let 545 fun corifyDecl ((d, loc : EM.span), st) =
529 val (st, n) = St.bindCon st x n 546 case d of
530 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => 547 L.DCon (x, n, k, c) =>
531 let 548 let
532 val st = St.bindConstructor st x n (L'.PConVar n) 549 val (st, n) = St.bindCon st x n
533 val st = St.bindConstructorVal st x n 550 in
534 val co = Option.map (corifyCon st) co 551 ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
535 in 552 end
536 ((x, n, co), st) 553 | L.DDatatype (x, n, xs, xncs) =>
537 end) st xncs 554 let
538 555 val (st, n) = St.bindCon st x n
539 val dk = ElabUtil.classifyDatatype xncs 556 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
540 val t = (L'.CNamed n, loc) 557 let
541 val nxs = length xs - 1 558 val st = St.bindConstructor st x n (L'.PConVar n)
542 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs 559 val st = St.bindConstructorVal st x n
543 val k = (L'.KType, loc) 560 val co = Option.map (corifyCon st) co
544 val dcons = map (fn (x, n, to) => 561 in
545 let 562 ((x, n, co), st)
546 val args = ListUtil.mapi (fn (i, _) => (L'.CRel (nxs - i), loc)) xs 563 end) st xncs
547 val (e, t) = 564
548 case to of 565 val dk = ElabUtil.classifyDatatype xncs
549 NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t) 566 val t = (L'.CNamed n, loc)
550 | SOME t' => ((L'.EAbs ("x", t', t, 567 val nxs = length xs - 1
551 (L'.ECon (dk, L'.PConVar n, args, 568 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
552 SOME (L'.ERel 0, loc)), 569 val k = (L'.KType, loc)
553 loc)), 570 val dcons = map (fn (x, n, to) =>
554 loc), 571 let
555 (L'.TFun (t', t), loc)) 572 val args = ListUtil.mapi (fn (i, _) => (L'.CRel (nxs - i), loc)) xs
556 573 val (e, t) =
557 val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs 574 case to of
558 val e = foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs 575 NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t)
559 in 576 | SOME t' => ((L'.EAbs ("x", t', t,
560 (L'.DVal (x, n, t, e, ""), loc) 577 (L'.ECon (dk, L'.PConVar n, args,
561 end) xncs 578 SOME (L'.ERel 0, loc)),
562 in 579 loc)),
563 ((L'.DDatatype (x, n, xs, xncs), loc) :: dcons, st) 580 loc),
564 end 581 (L'.TFun (t', t), loc))
565 | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => 582
566 let 583 val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
567 val (st, n) = St.bindCon st x n 584 val e = foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs
568 val c = corifyCon st (L.CModProj (m1, ms, s), loc) 585 in
569 586 (L'.DVal (x, n, t, e, ""), loc)
570 val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms 587 end) xncs
571 val (_, {inner, ...}) = corifyStr (m, st) 588 in
572 589 ((L'.DDatatype (x, n, xs, xncs), loc) :: dcons, st)
573 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => 590 end
574 let 591 | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
575 val n' = St.lookupConstructorByName inner x 592 let
576 val st = St.bindConstructor st x n n' 593 val (st, n) = St.bindCon st x n
577 val (st, n) = St.bindVal st x n 594 val c = corifyCon st (L.CModProj (m1, ms, s), loc)
578 val co = Option.map (corifyCon st) co 595
579 in 596 val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms
580 ((x, n, co), st) 597 val (_, {inner, ...}) = corifyStr (m, st)
581 end) st xncs 598
582 599 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
583 val nxs = length xs - 1 600 let
584 val c = ListUtil.foldli (fn (i, _, c) => (L'.CApp (c, (L'.CRel (nxs - i), loc)), loc)) c xs 601 val n' = St.lookupConstructorByName inner x
585 val k = (L'.KType, loc) 602 val st = St.bindConstructor st x n n'
586 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs 603 val (st, n) = St.bindVal st x n
587 604 val co = Option.map (corifyCon st) co
588 val cds = map (fn (x, n, co) => 605 in
589 let 606 ((x, n, co), st)
590 val t = case co of 607 end) st xncs
591 NONE => c 608
592 | SOME t' => (L'.TFun (t', c), loc) 609 val nxs = length xs - 1
593 val e = corifyExp st (L.EModProj (m1, ms, x), loc) 610 val c = ListUtil.foldli (fn (i, _, c) => (L'.CApp (c, (L'.CRel (nxs - i), loc)), loc)) c xs
594 611 val k = (L'.KType, loc)
595 val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs 612 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
596 in 613
597 (L'.DVal (x, n, t, e, x), loc) 614 val cds = map (fn (x, n, co) =>
598 end) xncs 615 let
599 in 616 val t = case co of
600 ((L'.DCon (x, n, k', c), loc) :: cds, st) 617 NONE => c
601 end 618 | SOME t' => (L'.TFun (t', c), loc)
602 | L.DVal (x, n, t, e) => 619 val e = corifyExp st (L.EModProj (m1, ms, x), loc)
603 let 620
604 val (st, n) = St.bindVal st x n 621 val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
605 val s = 622 in
606 if String.isPrefix "wrap_" x then 623 (L'.DVal (x, n, t, e, x), loc)
607 String.extract (x, 5, NONE) 624 end) xncs
608 else 625 in
609 x 626 ((L'.DCon (x, n, k', c), loc) :: cds, st)
610 in 627 end
611 ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st) 628 | L.DVal (x, n, t, e) =>
612 end 629 let
613 | L.DValRec vis => 630 val (st, n) = St.bindVal st x n
614 let 631 val s =
615 val (vis, st) = ListUtil.foldlMap 632 if String.isPrefix "wrap_" x then
616 (fn ((x, n, t, e), st) => 633 String.extract (x, 5, NONE)
617 let 634 else
618 val (st, n) = St.bindVal st x n 635 x
619 in 636 in
620 ((x, n, t, e), st) 637 ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st)
621 end) 638 end
622 st vis 639 | L.DValRec vis =>
623 640 let
624 val vis = map 641 val (vis, st) = ListUtil.foldlMap
625 (fn (x, n, t, e) => 642 (fn ((x, n, t, e), st) =>
626 let
627 val s =
628 if String.isPrefix "wrap_" x then
629 String.extract (x, 5, NONE)
630 else
631 x
632 in
633 (x, n, corifyCon st t, corifyExp st e, s)
634 end)
635 vis
636 in
637 ([(L'.DValRec vis, loc)], st)
638 end
639 | L.DSgn _ => ([], st)
640
641 | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) =>
642 ([], St.bindFunctor st x n xa na str)
643
644 | L.DStr (x, n, _, str) =>
645 let
646 val (ds, {inner, outer}) = corifyStr (str, st)
647 val st = St.bindStr outer x n inner
648 in
649 (ds, st)
650 end
651
652 | L.DFfiStr (m, n, (sgn, _)) =>
653 (case sgn of
654 L.SgnConst sgis =>
655 let
656 val (ds, cmap, conmap, st) =
657 foldl (fn ((sgi, _), (ds, cmap, conmap, st)) =>
658 case sgi of
659 L.SgiConAbs (x, n, k) =>
660 let 643 let
661 val (st, n') = St.bindCon st x n 644 val (st, n) = St.bindVal st x n
662 in 645 in
663 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, 646 ((x, n, t, e), st)
664 cmap, 647 end)
665 conmap, 648 st vis
666 st) 649
667 end 650 val vis = map
668 | L.SgiCon (x, n, k, _) => 651 (fn (x, n, t, e) =>
669 let 652 let
670 val (st, n') = St.bindCon st x n 653 val s =
671 in 654 if String.isPrefix "wrap_" x then
672 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, 655 String.extract (x, 5, NONE)
673 cmap, 656 else
674 conmap, 657 x
675 st) 658 in
676 end 659 (x, n, corifyCon st t, corifyExp st e, s)
677 660 end)
678 | L.SgiDatatype (x, n, xs, xnts) => 661 vis
679 let 662 in
680 val k = (L'.KType, loc) 663 ([(L'.DValRec vis, loc)], st)
681 val dk = ElabUtil.classifyDatatype xnts 664 end
682 val (st, n') = St.bindCon st x n 665 | L.DSgn _ => ([], st)
683 val (xnts, (ds', st, cmap, conmap)) = 666
684 ListUtil.foldlMap 667 | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) =>
685 (fn ((x', n, to), (ds', st, cmap, conmap)) => 668 ([], St.bindFunctor st x n xa na str)
686 let 669
687 val dt = (L'.CNamed n', loc) 670 | L.DStr (x, n, _, str) =>
688 val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs 671 let
689 672 val (ds, {inner, outer}) = corifyStr (str, st)
690 val to = Option.map (corifyCon st) to 673 val st = St.bindStr outer x n inner
691 674 in
692 val pc = L'.PConFfi {mod = m, 675 (ds, st)
693 datatyp = x, 676 end
694 params = xs, 677
695 con = x', 678 | L.DFfiStr (m, n, (sgn, _)) =>
696 arg = to, 679 (case sgn of
697 kind = dk} 680 L.SgnConst sgis =>
698 681 let
699 fun wrapT t = 682 val (ds, cmap, conmap, st) =
700 foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs 683 foldl (fn ((sgi, _), (ds, cmap, conmap, st)) =>
701 fun wrapE e = 684 case sgi of
702 foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs 685 L.SgiConAbs (x, n, k) =>
703 686 let
704 val (cmap, d) = 687 val (st, n') = St.bindCon st x n
705 case to of 688 in
706 NONE => (SM.insert (cmap, x', wrapT dt), 689 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
707 (L'.DVal (x', n, wrapT dt, 690 cmap,
708 wrapE 691 conmap,
709 (L'.ECon (dk, pc, args, NONE), 692 st)
710 loc), 693 end
711 ""), loc)) 694 | L.SgiCon (x, n, k, _) =>
712 | SOME t => 695 let
713 let 696 val (st, n') = St.bindCon st x n
714 val tf = (L'.TFun (t, dt), loc) 697 in
715 val e = wrapE (L'.EAbs ("x", t, tf, 698 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
716 (L'.ECon (dk, pc, args, 699 cmap,
717 SOME (L'.ERel 0, 700 conmap,
718 loc)), 701 st)
719 loc)), loc) 702 end
720 val d = (L'.DVal (x', n, wrapT tf, 703
721 e, ""), loc) 704 | L.SgiDatatype (x, n, xs, xnts) =>
705 let
706 val k = (L'.KType, loc)
707 val dk = ElabUtil.classifyDatatype xnts
708 val (st, n') = St.bindCon st x n
709 val (xnts, (ds', st, cmap, conmap)) =
710 ListUtil.foldlMap
711 (fn ((x', n, to), (ds', st, cmap, conmap)) =>
712 let
713 val dt = (L'.CNamed n', loc)
714 val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs
715
716 val to = Option.map (corifyCon st) to
717
718 val pc = L'.PConFfi {mod = m,
719 datatyp = x,
720 params = xs,
721 con = x',
722 arg = to,
723 kind = dk}
724
725 fun wrapT t =
726 foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
727 fun wrapE e =
728 foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs
729
730 val (cmap, d) =
731 case to of
732 NONE => (SM.insert (cmap, x', wrapT dt),
733 (L'.DVal (x', n, wrapT dt,
734 wrapE
735 (L'.ECon (dk, pc, args, NONE),
736 loc),
737 ""), loc))
738 | SOME t =>
739 let
740 val tf = (L'.TFun (t, dt), loc)
741 val e = wrapE (L'.EAbs ("x", t, tf,
742 (L'.ECon (dk, pc, args,
743 SOME (L'.ERel 0,
744 loc)),
745 loc)), loc)
746 val d = (L'.DVal (x', n, wrapT tf,
747 e, ""), loc)
722 in 748 in
723 (SM.insert (cmap, x', wrapT tf), d) 749 (SM.insert (cmap, x', wrapT tf), d)
724 end 750 end
725 751
726 val st = St.bindConstructor st x' n pc 752 val st = St.bindConstructor st x' n pc
744 st) 770 st)
745 | _ => (ds, cmap, conmap, st)) ([], SM.empty, SM.empty, st) sgis 771 | _ => (ds, cmap, conmap, st)) ([], SM.empty, SM.empty, st) sgis
746 772
747 val st = St.bindStr st m n (St.ffi m cmap conmap) 773 val st = St.bindStr st m n (St.ffi m cmap conmap)
748 in 774 in
749 (rev ds, st) 775 (rev ds, St.basisIs (st, n))
750 end 776 end
751 | _ => raise Fail "Non-const signature for FFI structure") 777 | _ => raise Fail "Non-const signature for FFI structure")
752 778
753 | L.DExport (en, sgn, str) => 779 | L.DExport (en, sgn, str) =>
754 (case #1 sgn of 780 (case #1 sgn of
764 case pathify str of 790 case pathify str of
765 NONE => (ErrorMsg.errorAt loc "Structure is too fancy to export"; 791 NONE => (ErrorMsg.errorAt loc "Structure is too fancy to export";
766 ([], st)) 792 ([], st))
767 | SOME (m, ms) => 793 | SOME (m, ms) =>
768 let 794 let
795 val basis_n = case St.lookupBasis st of
796 NONE => raise Fail "Corify: Don't know number of Basis"
797 | SOME n => n
798
769 fun wrapSgi ((sgi, _), (wds, eds)) = 799 fun wrapSgi ((sgi, _), (wds, eds)) =
770 case sgi of 800 case sgi of
771 L.SgiVal (s, _, t as (L.TFun (dom, ran), _)) => 801 L.SgiVal (s, _, t as (L.TFun (dom, ran), _)) =>
772 (case (#1 dom, #1 ran) of 802 (case (#1 dom, #1 ran) of
773 (L.TRecord (L.CRecord (_, []), _), 803 (L.TRecord _,
774 L.CApp 804 L.CApp ((L.CModProj (basis, [], "transaction"), _),
775 ((L.CApp 805 ran' as
776 ((L.CApp ((L.CModProj (_, [], "xml"), _), 806 (L.CApp
777 (L.CRecord (_, [((L.CName "Html", _), 807 ((L.CApp
778 _)]), _)), _), _), _), _)) => 808 ((L.CApp ((L.CModProj (basis', [], "xml"), _),
809 (L.CRecord (_, [((L.CName "Html", _),
810 _)]), _)), _), _),
811 _), _), _))) =>
779 let 812 let
780 val ran = (L.TRecord (L.CRecord ((L.KType, loc), []), loc), loc) 813 val ran = (L.TRecord (L.CRecord ((L.KType, loc), []), loc), loc)
814 val ranT = (L.CApp ((L.CModProj (basis, [], "transaction"), loc),
815 ran), loc)
781 val e = (L.EModProj (m, ms, s), loc) 816 val e = (L.EModProj (m, ms, s), loc)
782 val e = (L.EAbs ("vs", dom, ran, 817
783 (L.EWrite (L.EApp (e, (L.ERel 0, loc)), loc), loc)), loc) 818 val ef = (L.EModProj (basis, [], "bind"), loc)
819 val ef = (L.ECApp (ef, ran'), loc)
820 val ef = (L.EApp (ef, (L.EApp (e, (L.ERel 0, loc)), loc)), loc)
821
822 val eat = (L.CApp ((L.CModProj (basis, [], "transaction"), loc),
823 ran), loc)
824 val ea = (L.EAbs ("p", ran', eat,
825 (L.EWrite (L.ERel 0, loc), loc)), loc)
826
827 val e = (L.EApp (ef, ea), loc)
828 val e = (L.EAbs ("vs", dom, ran, e), loc)
784 in 829 in
785 ((L.DVal ("wrap_" ^ s, 0, 830 if basis = basis_n andalso basis' = basis_n then
786 (L.TFun (dom, ran), loc), 831 ((L.DVal ("wrap_" ^ s, 0,
787 e), loc) :: wds, 832 (L.TFun (dom, ranT), loc),
788 (fn st => 833 e), loc) :: wds,
789 case #1 (corifyExp st (L.EModProj (en, [], "wrap_" ^ s), loc)) of 834 (fn st =>
790 L'.ENamed n => (L'.DExport (L'.Link, n), loc) 835 case #1 (corifyExp st (L.EModProj (en, [], "wrap_" ^ s), loc)) of
791 | _ => raise Fail "Corify: Value to export didn't corify properly") 836 L'.ENamed n => (L'.DExport (L'.Link, n), loc)
792 :: eds) 837 | _ => raise Fail "Corify: Value to export didn't corify properly")
838 :: eds)
839 else
840 (wds, eds)
793 end 841 end
794 | _ => (wds, eds)) 842 | _ => (wds, eds))
795 | _ => (wds, eds) 843 | _ => (wds, eds)
796 844
797 val (wds, eds) = foldl wrapSgi ([], []) sgis 845 val (wds, eds) = foldl wrapSgi ([], []) sgis
798 val wrapper = (L.StrConst wds, loc) 846 val wrapper = (L.StrConst wds, loc)
799 val (ds, {inner, outer}) = corifyStr (wrapper, st) 847 val (ds, {inner, outer}) = corifyStr (wrapper, st)
800 val st = St.bindStr outer "wrapper" en inner 848 val st = St.bindStr outer "wrapper" en inner
801 849
802 val ds = ds @ map (fn f => f st) eds 850 val ds = ds @ map (fn f => f st) eds
803 in 851 in
804 (ds, st) 852 (ds, st)
805 end 853 end
806 end 854 end
807 | _ => raise Fail "Non-const signature for 'export'") 855 | _ => raise Fail "Non-const signature for 'export'")
808 856
809 | L.DTable (_, x, n, c) => 857 | L.DTable (_, x, n, c) =>
810 let 858 let
811 val (st, n) = St.bindVal st x n 859 val (st, n) = St.bindVal st x n
812 val s = x 860 val s = x
813 in 861 in
814 ([(L'.DTable (x, n, corifyCon st c, s), loc)], st) 862 ([(L'.DTable (x, n, corifyCon st c, s), loc)], st)
815 end 863 end
816 864
817 and corifyStr ((str, _), st) = 865 and corifyStr ((str, _), st) =
818 case str of 866 case str of
819 L.StrConst ds => 867 L.StrConst ds =>
820 let 868 let
863 | L.DSgn (_, n', _) => Int.max (n, n') 911 | L.DSgn (_, n', _) => Int.max (n, n')
864 | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str)) 912 | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str))
865 | L.DFfiStr (_, n', _) => Int.max (n, n') 913 | L.DFfiStr (_, n', _) => Int.max (n, n')
866 | L.DExport _ => n 914 | L.DExport _ => n
867 | L.DTable (_, _, n', _) => Int.max (n, n')) 915 | L.DTable (_, _, n', _) => Int.max (n, n'))
868 0 ds 916 0 ds
869 917
870 and maxNameStr (str, _) = 918 and maxNameStr (str, _) =
871 case str of 919 case str of
872 L.StrConst ds => maxName ds 920 L.StrConst ds => maxName ds
873 | L.StrVar n => n 921 | L.StrVar n => n