Mercurial > urweb

comparison src/elab_print.sml @ 191:aa54250f58ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parametrized datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Fri, 08 Aug 2008 10:28:32 -0400
parents 8e9f97508f0d
children dd82457fda82
comparison
equal deleted inserted replaced
190:3eb53c957d10 191:aa54250f58ac
214 fun p_pat' par env (p, _) = 214 fun p_pat' par env (p, _) =
215 case p of 215 case p of
216 PWild => string "_" 216 PWild => string "_"
217 | PVar (s, _) => string s 217 | PVar (s, _) => string s
218 | PPrim p => Prim.p_t p 218 | PPrim p => Prim.p_t p
219 | PCon (_, pc, NONE) => p_patCon env pc 219 | PCon (_, pc, _, NONE) => p_patCon env pc
220 | PCon (_, pc, SOME p) => parenIf par (box [p_patCon env pc, 220 | PCon (_, pc, _, SOME p) => parenIf par (box [p_patCon env pc,
221 space, 221 space,
222 p_pat' true env p]) 222 p_pat' true env p])
223 | PRecord xps => 223 | PRecord xps =>
224 box [string "{", 224 box [string "{",
225 p_list_sep (box [string ",", space]) (fn (x, p, _) => 225 p_list_sep (box [string ",", space]) (fn (x, p, _) =>
362 string "__", 362 string "__",
363 string (Int.toString n)] 363 string (Int.toString n)]
364 else 364 else
365 string x 365 string x
366 366
367 fun p_datatype env (x, n, cons) = 367 fun p_datatype env (x, n, xs, cons) =
368 let 368 let
369 val env = E.pushCNamedAs env x n (KType, ErrorMsg.dummySpan) NONE 369 val k = (KType, ErrorMsg.dummySpan)
370 val env = E.pushCNamedAs env x n k NONE
371 val env = foldl (fn (x, env) => E.pushCRel env x k) env xs
370 in 372 in
371 box [string "datatype", 373 box [string "datatype",
372 space, 374 space,
373 string x, 375 string x,
376 p_list_sep (box []) (fn x => box [space, string x]) xs,
374 space, 377 space,
375 string "=", 378 string "=",
376 space, 379 space,
377 p_list_sep (box [space, string "|", space]) 380 p_list_sep (box [space, string "|", space])
378 (fn (x, _, NONE) => string x 381 (fn (x, _, NONE) => string x
399 space, 402 space,
400 string "=", 403 string "=",
401 space, 404 space,
402 p_con env c] 405 p_con env c]
403 | SgiDatatype x => p_datatype env x 406 | SgiDatatype x => p_datatype env x
404 | SgiDatatypeImp (x, _, m1, ms, x', _) => 407 | SgiDatatypeImp (x, _, m1, ms, x', _, _) =>
405 let 408 let
406 val m1x = #1 (E.lookupStrNamed env m1) 409 val m1x = #1 (E.lookupStrNamed env m1)
407 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 410 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
408 in 411 in
409 box [string "datatype", 412 box [string "datatype",
521 space, 524 space,
522 string "=", 525 string "=",
523 space, 526 space,
524 p_con env c] 527 p_con env c]
525 | DDatatype x => p_datatype env x 528 | DDatatype x => p_datatype env x
526 | DDatatypeImp (x, _, m1, ms, x', _) => 529 | DDatatypeImp (x, _, m1, ms, x', _, _) =>
527 let 530 let
528 val m1x = #1 (E.lookupStrNamed env m1) 531 val m1x = #1 (E.lookupStrNamed env m1)
529 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 532 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
530 in 533 in
531 box [string "datatype", 534 box [string "datatype",