Mercurial > urweb
comparison src/elab_print.sml @ 156:34ccd7d2bea8
Start of datatype support
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 24 Jul 2008 15:02:03 -0400 |
parents | 7420fa18d657 |
children | 06a98129b23f |
comparison
equal
deleted
inserted
replaced
155:4334bb734187 | 156:34ccd7d2bea8 |
---|---|
307 string "__", | 307 string "__", |
308 string (Int.toString n)] | 308 string (Int.toString n)] |
309 else | 309 else |
310 string x | 310 string x |
311 | 311 |
312 fun p_datatype env (x, n, cons) = | |
313 let | |
314 val env = E.pushCNamedAs env x n (KType, ErrorMsg.dummySpan) NONE | |
315 in | |
316 box [string "datatype", | |
317 space, | |
318 string x, | |
319 space, | |
320 string "=", | |
321 space, | |
322 p_list_sep (box [space, string "|", space]) | |
323 (fn (x, _, NONE) => string x | |
324 | (x, _, SOME t) => box [string x, space, string "of", space, p_con env t]) | |
325 cons] | |
326 end | |
327 | |
312 fun p_sgn_item env (sgi, _) = | 328 fun p_sgn_item env (sgi, _) = |
313 case sgi of | 329 case sgi of |
314 SgiConAbs (x, n, k) => box [string "con", | 330 SgiConAbs (x, n, k) => box [string "con", |
315 space, | 331 space, |
316 p_named x n, | 332 p_named x n, |
327 p_kind k, | 343 p_kind k, |
328 space, | 344 space, |
329 string "=", | 345 string "=", |
330 space, | 346 space, |
331 p_con env c] | 347 p_con env c] |
348 | SgiDatatype x => p_datatype env x | |
349 | SgiDatatypeImp (x, _, m1, ms, x') => | |
350 let | |
351 val m1x = #1 (E.lookupStrNamed env m1) | |
352 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 | |
353 in | |
354 box [string "datatype", | |
355 space, | |
356 string x, | |
357 space, | |
358 string "=", | |
359 space, | |
360 string "datatype", | |
361 space, | |
362 p_list_sep (string ".") string (m1x :: ms @ [x'])] | |
363 end | |
332 | SgiVal (x, n, c) => box [string "val", | 364 | SgiVal (x, n, c) => box [string "val", |
333 space, | 365 space, |
334 p_named x n, | 366 p_named x n, |
335 space, | 367 space, |
336 string ":", | 368 string ":", |
433 p_kind k, | 465 p_kind k, |
434 space, | 466 space, |
435 string "=", | 467 string "=", |
436 space, | 468 space, |
437 p_con env c] | 469 p_con env c] |
470 | DDatatype x => p_datatype env x | |
471 | DDatatypeImp (x, _, m1, ms, x') => | |
472 let | |
473 val m1x = #1 (E.lookupStrNamed env m1) | |
474 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 | |
475 in | |
476 box [string "datatype", | |
477 space, | |
478 string x, | |
479 space, | |
480 string "=", | |
481 space, | |
482 string "datatype", | |
483 space, | |
484 p_list_sep (string ".") string (m1x :: ms @ [x'])] | |
485 end | |
438 | DVal vi => box [string "val", | 486 | DVal vi => box [string "val", |
439 space, | 487 space, |
440 p_vali env vi] | 488 p_vali env vi] |
441 | DValRec vis => | 489 | DValRec vis => |
442 let | 490 let |