comparison src/expl_print.sml @ 162:06a98129b23f

Add datatype import constructor annotations; datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Tue, 29 Jul 2008 12:30:04 -0400
parents 7420fa18d657
children 80192edca30d
comparison
equal deleted inserted replaced
161:a5ae7b3e37a4 162:06a98129b23f
272 string "__", 272 string "__",
273 string (Int.toString n)] 273 string (Int.toString n)]
274 else 274 else
275 string x 275 string x
276 276
277 fun p_datatype env (x, n, cons) =
278 let
279 val env = E.pushCNamed env x n (KType, ErrorMsg.dummySpan) NONE
280 in
281 box [string "datatype",
282 space,
283 string x,
284 space,
285 string "=",
286 space,
287 p_list_sep (box [space, string "|", space])
288 (fn (x, _, NONE) => string x
289 | (x, _, SOME t) => box [string x, space, string "of", space, p_con env t])
290 cons]
291 end
292
277 fun p_sgn_item env (sgi, _) = 293 fun p_sgn_item env (sgi, _) =
278 case sgi of 294 case sgi of
279 SgiConAbs (x, n, k) => box [string "con", 295 SgiConAbs (x, n, k) => box [string "con",
280 space, 296 space,
281 p_named x n, 297 p_named x n,
292 p_kind k, 308 p_kind k,
293 space, 309 space,
294 string "=", 310 string "=",
295 space, 311 space,
296 p_con env c] 312 p_con env c]
313 | SgiDatatype x => p_datatype env x
314 | SgiDatatypeImp (x, _, m1, ms, x', _) =>
315 let
316 val m1x = #1 (E.lookupStrNamed env m1)
317 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
318 in
319 box [string "datatype",
320 space,
321 string x,
322 space,
323 string "=",
324 space,
325 string "datatype",
326 space,
327 p_list_sep (string ".") string (m1x :: ms @ [x'])]
328 end
297 | SgiVal (x, n, c) => box [string "val", 329 | SgiVal (x, n, c) => box [string "val",
298 space, 330 space,
299 p_named x n, 331 p_named x n,
300 space, 332 space,
301 string ":", 333 string ":",
390 p_kind k, 422 p_kind k,
391 space, 423 space,
392 string "=", 424 string "=",
393 space, 425 space,
394 p_con env c] 426 p_con env c]
427 | DDatatype x => p_datatype env x
428 | DDatatypeImp (x, _, m1, ms, x', _) =>
429 let
430 val m1x = #1 (E.lookupStrNamed env m1)
431 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
432 in
433 box [string "datatype",
434 space,
435 string x,
436 space,
437 string "=",
438 space,
439 string "datatype",
440 space,
441 p_list_sep (string ".") string (m1x :: ms @ [x'])]
442 end
395 | DVal vi => box [string "val", 443 | DVal vi => box [string "val",
396 space, 444 space,
397 p_vali env vi] 445 p_vali env vi]
398 | DValRec vis => 446 | DValRec vis =>
399 let 447 let