Mercurial > urweb

comparison src/expl_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 8a70e2919e86
comparison
equal deleted inserted replaced
190:3eb53c957d10 191:aa54250f58ac
179 fun p_pat' par env (p, _) = 179 fun p_pat' par env (p, _) =
180 case p of 180 case p of
181 PWild => string "_" 181 PWild => string "_"
182 | PVar (s, _) => string s 182 | PVar (s, _) => string s
183 | PPrim p => Prim.p_t p 183 | PPrim p => Prim.p_t p
184 | PCon (_, pc, NONE) => p_patCon env pc 184 | PCon (_, pc, _, NONE) => p_patCon env pc
185 | PCon (_, pc, SOME p) => parenIf par (box [p_patCon env pc, 185 | PCon (_, pc, _, SOME p) => parenIf par (box [p_patCon env pc,
186 space, 186 space,
187 p_pat' true env p]) 187 p_pat' true env p])
188 | PRecord xps => 188 | PRecord xps =>
189 box [string "{", 189 box [string "{",
190 p_list_sep (box [string ",", space]) (fn (x, p, _) => 190 p_list_sep (box [string ",", space]) (fn (x, p, _) =>
191 box [string x, 191 box [string x,
192 space, 192 space,
327 string "__", 327 string "__",
328 string (Int.toString n)] 328 string (Int.toString n)]
329 else 329 else
330 string x 330 string x
331 331
332 fun p_datatype env (x, n, cons) = 332 fun p_datatype env (x, n, xs, cons) =
333 let 333 let
334 val env = E.pushCNamed env x n (KType, ErrorMsg.dummySpan) NONE 334 val k = (KType, ErrorMsg.dummySpan)
335 val env = E.pushCNamed env x n k NONE
336 val env = foldl (fn (x, env) => E.pushCRel env x k) env xs
335 in 337 in
336 box [string "datatype", 338 box [string "datatype",
337 space, 339 space,
338 string x, 340 string x,
341 p_list_sep (box []) (fn x => box [space, string x]) xs,
339 space, 342 space,
340 string "=", 343 string "=",
341 space, 344 space,
342 p_list_sep (box [space, string "|", space]) 345 p_list_sep (box [space, string "|", space])
343 (fn (x, n, NONE) => if !debug then (string (x ^ "__" ^ Int.toString n)) 346 (fn (x, n, NONE) => if !debug then (string (x ^ "__" ^ Int.toString n))
366 space, 369 space,
367 string "=", 370 string "=",
368 space, 371 space,
369 p_con env c] 372 p_con env c]
370 | SgiDatatype x => p_datatype env x 373 | SgiDatatype x => p_datatype env x
371 | SgiDatatypeImp (x, _, m1, ms, x', _) => 374 | SgiDatatypeImp (x, _, m1, ms, x', _, _) =>
372 let 375 let
373 val m1x = #1 (E.lookupStrNamed env m1) 376 val m1x = #1 (E.lookupStrNamed env m1)
374 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 377 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
375 in 378 in
376 box [string "datatype", 379 box [string "datatype",
480 space, 483 space,
481 string "=", 484 string "=",
482 space, 485 space,
483 p_con env c] 486 p_con env c]
484 | DDatatype x => p_datatype env x 487 | DDatatype x => p_datatype env x
485 | DDatatypeImp (x, _, m1, ms, x', _) => 488 | DDatatypeImp (x, _, m1, ms, x', _, _) =>
486 let 489 let
487 val m1x = #1 (E.lookupStrNamed env m1) 490 val m1x = #1 (E.lookupStrNamed env m1)
488 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 491 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
489 in 492 in
490 box [string "datatype", 493 box [string "datatype",