Mercurial > urweb

annotate src/expl_print.sml @ 1269:9f4b9315810d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Improve consNeq to detect unequal projected cons
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jun 2010 10:44:57 -0400
parents c316ca3c9ec6
children 56bd4a4f6e66
rev   line source
adamc@38 1 (* Copyright (c) 2008, Adam Chlipala
adamc@38 2 * All rights reserved.
adamc@38 3 *
adamc@38 4 * Redistribution and use in source and binary forms, with or without
adamc@38 5 * modification, are permitted provided that the following conditions are met:
adamc@38 6 *
adamc@38 7 * - Redistributions of source code must retain the above copyright notice,
adamc@38 8 * this list of conditions and the following disclaimer.
adamc@38 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@38 10 * this list of conditions and the following disclaimer in the documentation
adamc@38 11 * and/or other materials provided with the distribution.
adamc@38 12 * - The names of contributors may not be used to endorse or promote products
adamc@38 13 * derived from this software without specific prior written permission.
adamc@38 14 *
adamc@38 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@38 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@38 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@38 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@38 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@38 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@38 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@38 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@38 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@38 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@38 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@38 26 *)
adamc@38 27
adamc@244 28 (* Pretty-printing elaborated Ur/Web *)
adamc@38 29
adamc@38 30 structure ExplPrint :> EXPL_PRINT = struct
adamc@38 31
adamc@38 32 open Print.PD
adamc@38 33 open Print
adamc@38 34
adamc@38 35 open Expl
adamc@38 36
adamc@38 37 structure E = ExplEnv
adamc@38 38
adamc@38 39 val debug = ref false
adamc@38 40
adamc@624 41 fun p_kind' par env (k, _) =
adamc@38 42 case k of
adamc@38 43 KType => string "Type"
adamc@624 44 | KArrow (k1, k2) => parenIf par (box [p_kind' true env k1,
adamc@38 45 space,
adamc@38 46 string "->",
adamc@38 47 space,
adamc@624 48 p_kind env k2])
adamc@38 49 | KName => string "Name"
adamc@624 50 | KRecord k => box [string "{", p_kind env k, string "}"]
adamc@87 51 | KUnit => string "Unit"
adamc@213 52 | KTuple ks => box [string "(",
adamc@624 53 p_list_sep (box [space, string "*", space]) (p_kind env) ks,
adamc@213 54 string ")"]
adamc@38 55
adamc@624 56 | KRel n => ((if !debug then
adamc@624 57 string (E.lookupKRel env n ^ "_" ^ Int.toString n)
adamc@624 58 else
adamc@624 59 string (E.lookupKRel env n))
adamc@624 60 handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n))
adamc@624 61 | KFun (x, k) => box [string x,
adamc@624 62 space,
adamc@624 63 string "-->",
adamc@624 64 space,
adamc@624 65 p_kind (E.pushKRel env x) k]
adamc@624 66
adamc@624 67 and p_kind env = p_kind' false env
adamc@38 68
adamc@38 69 fun p_con' par env (c, _) =
adamc@38 70 case c of
adamc@38 71 TFun (t1, t2) => parenIf par (box [p_con' true env t1,
adamc@38 72 space,
adamc@38 73 string "->",
adamc@38 74 space,
adamc@38 75 p_con env t2])
adamc@38 76 | TCFun (x, k, c) => parenIf par (box [string x,
adamc@38 77 space,
adamc@38 78 string "::",
adamc@38 79 space,
adamc@624 80 p_kind env k,
adamc@38 81 space,
adamc@38 82 string "->",
adamc@38 83 space,
adamc@38 84 p_con (E.pushCRel env x k) c])
adamc@38 85 | TRecord (CRecord (_, xcs), _) => box [string "{",
adamc@38 86 p_list (fn (x, c) =>
adamc@38 87 box [p_name env x,
adamc@38 88 space,
adamc@38 89 string ":",
adamc@38 90 space,
adamc@38 91 p_con env c]) xcs,
adamc@38 92 string "}"]
adamc@38 93 | TRecord c => box [string "$",
adamc@38 94 p_con' true env c]
adamc@38 95
adamc@38 96 | CRel n =>
adamc@449 97 ((if !debug then
adamc@449 98 string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n)
adamc@449 99 else
adamc@449 100 string (#1 (E.lookupCRel env n)))
adamc@449 101 handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n))
adamc@38 102 | CNamed n =>
adamc@38 103 ((if !debug then
adamc@38 104 string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n)
adamc@38 105 else
adamc@38 106 string (#1 (E.lookupCNamed env n)))
adamc@38 107 handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n))
adamc@38 108 | CModProj (m1, ms, x) =>
adamc@38 109 let
adamc@109 110 val m1x = #1 (E.lookupStrNamed env m1)
adamc@480 111 handle E.UnboundNamed _ => "UNBOUND" ^ Int.toString m1
adamc@38 112
adamc@38 113 val m1s = if !debug then
adamc@38 114 m1x ^ "__" ^ Int.toString m1
adamc@38 115 else
adamc@38 116 m1x
adamc@38 117 in
adamc@146 118 p_list_sep (string ".") string (m1s :: ms @ [x])
adamc@38 119 end
adamc@38 120
adamc@38 121 | CApp (c1, c2) => parenIf par (box [p_con env c1,
adamc@38 122 space,
adamc@38 123 p_con' true env c2])
adamc@38 124 | CAbs (x, k, c) => parenIf par (box [string "fn",
adamc@38 125 space,
adamc@38 126 string x,
adamc@38 127 space,
adamc@38 128 string "::",
adamc@38 129 space,
adamc@624 130 p_kind env k,
adamc@38 131 space,
adamc@38 132 string "=>",
adamc@38 133 space,
adamc@38 134 p_con (E.pushCRel env x k) c])
adamc@38 135
adamc@38 136 | CName s => box [string "#", string s]
adamc@38 137
adamc@38 138 | CRecord (k, xcs) =>
adamc@38 139 if !debug then
adamc@38 140 parenIf par (box [string "[",
adamc@38 141 p_list (fn (x, c) =>
adamc@38 142 box [p_con env x,
adamc@38 143 space,
adamc@38 144 string "=",
adamc@38 145 space,
adamc@38 146 p_con env c]) xcs,
adamc@38 147 string "]::",
adamc@624 148 p_kind env k])
adamc@38 149 else
adamc@38 150 parenIf par (box [string "[",
adamc@38 151 p_list (fn (x, c) =>
adamc@38 152 box [p_con env x,
adamc@38 153 space,
adamc@38 154 string "=",
adamc@38 155 space,
adamc@38 156 p_con env c]) xcs,
adamc@38 157 string "]"])
adamc@38 158 | CConcat (c1, c2) => parenIf par (box [p_con' true env c1,
adamc@38 159 space,
adamc@38 160 string "++",
adamc@38 161 space,
adamc@38 162 p_con env c2])
adamc@621 163 | CMap _ => string "map"
adamc@87 164 | CUnit => string "()"
adamc@213 165
adamc@213 166 | CTuple cs => box [string "(",
adamc@213 167 p_list (p_con env) cs,
adamc@213 168 string ")"]
adamc@213 169 | CProj (c, n) => box [p_con env c,
adamc@213 170 string ".",
adamc@213 171 string (Int.toString n)]
adamc@624 172
adamc@624 173 | CKAbs (x, c) => box [string x,
adamc@624 174 space,
adamc@624 175 string "==>",
adamc@624 176 space,
adamc@624 177 p_con (E.pushKRel env x) c]
adamc@624 178 | CKApp (c, k) => box [p_con env c,
adamc@624 179 string "[[",
adamc@624 180 p_kind env k,
adamc@624 181 string "]]"]
adamc@624 182 | TKFun (x, c) => box [string x,
adamc@624 183 space,
adamc@624 184 string "-->",
adamc@624 185 space,
adamc@624 186 p_con (E.pushKRel env x) c]
adamc@38 187
adamc@38 188 and p_con env = p_con' false env
adamc@38 189
adamc@38 190 and p_name env (all as (c, _)) =
adamc@38 191 case c of
adamc@38 192 CName s => string s
adamc@38 193 | _ => p_con env all
adamc@38 194
adamc@176 195 fun p_patCon env pc =
adamc@176 196 case pc of
adamc@176 197 PConVar n =>
adamc@176 198 ((if !debug then
adamc@176 199 string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
adamc@176 200 else
adamc@176 201 string (#1 (E.lookupENamed env n)))
adamc@449 202 handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n))
adamc@176 203 | PConProj (m1, ms, x) =>
adamc@176 204 let
adamc@176 205 val m1x = #1 (E.lookupStrNamed env m1)
adamc@176 206 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
adamc@176 207
adamc@176 208 val m1s = if !debug then
adamc@176 209 m1x ^ "__" ^ Int.toString m1
adamc@176 210 else
adamc@176 211 m1x
adamc@176 212 in
adamc@176 213 p_list_sep (string ".") string (m1x :: ms @ [x])
adamc@176 214 end
adamc@176 215
adamc@176 216 fun p_pat' par env (p, _) =
adamc@176 217 case p of
adamc@176 218 PWild => string "_"
adamc@182 219 | PVar (s, _) => string s
adamc@176 220 | PPrim p => Prim.p_t p
adamc@191 221 | PCon (_, pc, _, NONE) => p_patCon env pc
adamc@796 222 | PCon (_, pc, cs, SOME p) =>
adamc@796 223 if !debug then
adamc@796 224 parenIf par (box [p_patCon env pc,
adamc@796 225 string "[",
adamc@796 226 p_list (p_con env) cs,
adamc@796 227 string "]",
adamc@796 228 space,
adamc@796 229 p_pat' true env p])
adamc@796 230 else
adamc@796 231 parenIf par (box [p_patCon env pc,
adamc@796 232 space,
adamc@796 233 p_pat' true env p])
adamc@796 234
adamc@176 235 | PRecord xps =>
adamc@176 236 box [string "{",
adamc@182 237 p_list_sep (box [string ",", space]) (fn (x, p, _) =>
adamc@176 238 box [string x,
adamc@176 239 space,
adamc@176 240 string "=",
adamc@176 241 space,
adamc@176 242 p_pat env p]) xps,
adamc@176 243 string "}"]
adamc@176 244
adamc@176 245 and p_pat x = p_pat' false x
adamc@176 246
adamc@146 247 fun p_exp' par env (e, loc) =
adamc@38 248 case e of
adamc@38 249 EPrim p => Prim.p_t p
adamc@38 250 | ERel n =>
adamc@449 251 ((if !debug then
adamc@449 252 string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n)
adamc@449 253 else
adamc@449 254 string (#1 (E.lookupERel env n)))
adamc@449 255 handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n))
adamc@38 256 | ENamed n =>
adamc@449 257 ((if !debug then
adamc@449 258 string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
adamc@449 259 else
adamc@449 260 string (#1 (E.lookupENamed env n)))
adamc@449 261 handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n))
adamc@38 262 | EModProj (m1, ms, x) =>
adamc@38 263 let
adamc@38 264 val (m1x, sgn) = E.lookupStrNamed env m1
adamc@480 265 handle E.UnboundNamed _ => ("UNBOUND" ^ Int.toString m1, (SgnConst [], loc))
adamc@38 266
adamc@38 267 val m1s = if !debug then
adamc@38 268 m1x ^ "__" ^ Int.toString m1
adamc@38 269 else
adamc@38 270 m1x
adamc@38 271 in
adamc@146 272 p_list_sep (string ".") string (m1s :: ms @ [x])
adamc@38 273 end
adamc@38 274
adamc@38 275 | EApp (e1, e2) => parenIf par (box [p_exp env e1,
adamc@38 276 space,
adamc@38 277 p_exp' true env e2])
adamc@38 278 | EAbs (x, t, _, e) => parenIf par (box [string "fn",
adamc@38 279 space,
adamc@38 280 string x,
adamc@38 281 space,
adamc@38 282 string ":",
adamc@38 283 space,
adamc@38 284 p_con env t,
adamc@38 285 space,
adamc@38 286 string "=>",
adamc@38 287 space,
adamc@38 288 p_exp (E.pushERel env x t) e])
adamc@38 289 | ECApp (e, c) => parenIf par (box [p_exp env e,
adamc@38 290 space,
adamc@38 291 string "[",
adamc@38 292 p_con env c,
adamc@38 293 string "]"])
adamc@38 294 | ECAbs (x, k, e) => parenIf par (box [string "fn",
adamc@38 295 space,
adamc@38 296 string x,
adamc@38 297 space,
adamc@38 298 string "::",
adamc@38 299 space,
adamc@624 300 p_kind env k,
adamc@38 301 space,
adamc@38 302 string "=>",
adamc@38 303 space,
adamc@38 304 p_exp (E.pushCRel env x k) e])
adamc@38 305
adamc@38 306 | ERecord xes => box [string "{",
adamc@38 307 p_list (fn (x, e, _) =>
adamc@38 308 box [p_name env x,
adamc@38 309 space,
adamc@38 310 string "=",
adamc@38 311 space,
adamc@38 312 p_exp env e]) xes,
adamc@38 313 string "}"]
adamc@38 314 | EField (e, c, {field, rest}) =>
adamc@38 315 if !debug then
adamc@38 316 box [p_exp' true env e,
adamc@38 317 string ".",
adamc@38 318 p_con' true env c,
adamc@38 319 space,
adamc@38 320 string "[",
adamc@38 321 p_con env field,
adamc@38 322 space,
adamc@38 323 string " in ",
adamc@38 324 space,
adamc@38 325 p_con env rest,
adamc@38 326 string "]"]
adamc@38 327 else
adamc@38 328 box [p_exp' true env e,
adamc@38 329 string ".",
adamc@38 330 p_con' true env c]
adamc@445 331 | EConcat (e1, c1, e2, c2) =>
adamc@339 332 parenIf par (if !debug then
adamc@445 333 box [p_exp' true env e1,
adamc@445 334 space,
adamc@445 335 string ":",
adamc@445 336 space,
adamc@445 337 p_con env c1,
adamc@445 338 space,
adamc@445 339 string "++",
adamc@445 340 space,
adamc@445 341 p_exp' true env e2,
adamc@445 342 space,
adamc@445 343 string ":",
adamc@445 344 space,
adamc@445 345 p_con env c2]
adamc@445 346 else
adamc@445 347 box [p_exp' true env e1,
adamc@339 348 space,
adamc@339 349 string "with",
adamc@339 350 space,
adamc@339 351 p_exp' true env e2])
adamc@149 352 | ECut (e, c, {field, rest}) =>
adamc@149 353 parenIf par (if !debug then
adamc@149 354 box [p_exp' true env e,
adamc@149 355 space,
adamc@149 356 string "--",
adamc@149 357 space,
adamc@149 358 p_con' true env c,
adamc@149 359 space,
adamc@149 360 string "[",
adamc@149 361 p_con env field,
adamc@149 362 space,
adamc@149 363 string " in ",
adamc@149 364 space,
adamc@149 365 p_con env rest,
adamc@149 366 string "]"]
adamc@149 367 else
adamc@149 368 box [p_exp' true env e,
adamc@149 369 space,
adamc@149 370 string "--",
adamc@149 371 space,
adamc@149 372 p_con' true env c])
adamc@493 373 | ECutMulti (e, c, {rest}) =>
adamc@493 374 parenIf par (if !debug then
adamc@493 375 box [p_exp' true env e,
adamc@493 376 space,
adamc@493 377 string "---",
adamc@493 378 space,
adamc@493 379 p_con' true env c,
adamc@493 380 space,
adamc@493 381 string "[",
adamc@493 382 p_con env rest,
adamc@493 383 string "]"]
adamc@493 384 else
adamc@493 385 box [p_exp' true env e,
adamc@493 386 space,
adamc@493 387 string "---",
adamc@493 388 space,
adamc@493 389 p_con' true env c])
adamc@38 390
adamc@109 391 | EWrite e => box [string "write(",
adamc@109 392 p_exp env e,
adamc@109 393 string ")"]
adamc@109 394
adamc@288 395 | ECase (e, pes, {disc, result}) =>
adamc@288 396 parenIf par (box [string "case",
adamc@288 397 space,
adamc@288 398 p_exp env e,
adamc@288 399 space,
adamc@288 400 if !debug then
adamc@288 401 box [string "in",
adamc@288 402 space,
adamc@288 403 p_con env disc,
adamc@288 404 space,
adamc@288 405 string "return",
adamc@288 406 space,
adamc@288 407 p_con env result,
adamc@288 408 space]
adamc@288 409 else
adamc@288 410 box [],
adamc@288 411 string "of",
adamc@288 412 space,
adamc@288 413 p_list_sep (box [space, string "|", space])
adamc@288 414 (fn (p, e) => box [p_pat env p,
adamc@288 415 space,
adamc@288 416 string "=>",
adamc@288 417 space,
adamc@288 418 p_exp env e]) pes])
adamc@176 419
adamc@449 420 | ELet (x, t, e1, e2) => box [string "let",
adamc@449 421 space,
adamc@449 422 string x,
adamc@449 423 space,
adamc@449 424 string ":",
adamc@453 425 space,
adamc@449 426 p_con env t,
adamc@449 427 space,
adamc@449 428 string "=",
adamc@449 429 space,
adamc@449 430 p_exp env e1,
adamc@449 431 space,
adamc@449 432 string "in",
adamc@449 433 newline,
adamc@449 434 p_exp (E.pushERel env x t) e2]
adamc@449 435
adamc@624 436 | EKAbs (x, e) => box [string x,
adamc@624 437 space,
adamc@624 438 string "==>",
adamc@624 439 space,
adamc@624 440 p_exp (E.pushKRel env x) e]
adamc@624 441 | EKApp (e, k) => box [p_exp env e,
adamc@624 442 string "[[",
adamc@624 443 p_kind env k,
adamc@624 444 string "]]"]
adamc@449 445
adamc@449 446
adamc@38 447 and p_exp env = p_exp' false env
adamc@38 448
adamc@38 449 fun p_named x n =
adamc@38 450 if !debug then
adamc@38 451 box [string x,
adamc@38 452 string "__",
adamc@38 453 string (Int.toString n)]
adamc@38 454 else
adamc@38 455 string x
adamc@38 456
adamc@191 457 fun p_datatype env (x, n, xs, cons) =
adamc@162 458 let
adamc@191 459 val k = (KType, ErrorMsg.dummySpan)
adamc@191 460 val env = E.pushCNamed env x n k NONE
adamc@191 461 val env = foldl (fn (x, env) => E.pushCRel env x k) env xs
adamc@162 462 in
adamc@806 463 box [string x,
adamc@191 464 p_list_sep (box []) (fn x => box [space, string x]) xs,
adamc@162 465 space,
adamc@162 466 string "=",
adamc@162 467 space,
adamc@162 468 p_list_sep (box [space, string "|", space])
adamc@163 469 (fn (x, n, NONE) => if !debug then (string (x ^ "__" ^ Int.toString n))
adamc@163 470 else string x
adamc@193 471 | (x, n, SOME t) => box [if !debug then (string (x ^ "__" ^ Int.toString n))
adamc@163 472 else string x, space, string "of", space, p_con env t])
adamc@162 473 cons]
adamc@162 474 end
adamc@162 475
adamc@806 476 fun p_sgn_item env (sgiAll as (sgi, _)) =
adamc@38 477 case sgi of
adamc@38 478 SgiConAbs (x, n, k) => box [string "con",
adamc@38 479 space,
adamc@38 480 p_named x n,
adamc@38 481 space,
adamc@38 482 string "::",
adamc@38 483 space,
adamc@624 484 p_kind env k]
adamc@38 485 | SgiCon (x, n, k, c) => box [string "con",
adamc@38 486 space,
adamc@38 487 p_named x n,
adamc@38 488 space,
adamc@38 489 string "::",
adamc@38 490 space,
adamc@624 491 p_kind env k,
adamc@38 492 space,
adamc@38 493 string "=",
adamc@38 494 space,
adamc@38 495 p_con env c]
adamc@806 496 | SgiDatatype x => box [string "datatype",
adamc@806 497 space,
adamc@806 498 p_list_sep (box [space, string "and", space]) (p_datatype (E.sgiBinds env sgiAll)) x]
adamc@191 499 | SgiDatatypeImp (x, _, m1, ms, x', _, _) =>
adamc@162 500 let
adamc@162 501 val m1x = #1 (E.lookupStrNamed env m1)
adamc@162 502 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
adamc@162 503 in
adamc@162 504 box [string "datatype",
adamc@162 505 space,
adamc@162 506 string x,
adamc@162 507 space,
adamc@162 508 string "=",
adamc@162 509 space,
adamc@162 510 string "datatype",
adamc@162 511 space,
adamc@162 512 p_list_sep (string ".") string (m1x :: ms @ [x'])]
adamc@162 513 end
adamc@38 514 | SgiVal (x, n, c) => box [string "val",
adamc@38 515 space,
adamc@38 516 p_named x n,
adamc@38 517 space,
adamc@38 518 string ":",
adamc@38 519 space,
adamc@38 520 p_con env c]
adamc@38 521 | SgiStr (x, n, sgn) => box [string "structure",
adamc@38 522 space,
adamc@38 523 p_named x n,
adamc@38 524 space,
adamc@38 525 string ":",
adamc@38 526 space,
adamc@38 527 p_sgn env sgn]
adamc@64 528 | SgiSgn (x, n, sgn) => box [string "signature",
adamc@64 529 space,
adamc@64 530 p_named x n,
adamc@64 531 space,
adamc@64 532 string "=",
adamc@64 533 space,
adamc@64 534 p_sgn env sgn]
adamc@38 535
adamc@146 536 and p_sgn env (sgn, loc) =
adamc@38 537 case sgn of
adamc@38 538 SgnConst sgis => box [string "sig",
adamc@38 539 newline,
adamc@38 540 let
adamc@38 541 val (psgis, _) = ListUtil.foldlMap (fn (sgi, env) =>
adamc@38 542 (p_sgn_item env sgi,
adamc@38 543 E.sgiBinds env sgi))
adamc@38 544 env sgis
adamc@38 545 in
adamc@38 546 p_list_sep newline (fn x => x) psgis
adamc@38 547 end,
adamc@38 548 newline,
adamc@38 549 string "end"]
adamc@146 550 | SgnVar n => string ((#1 (E.lookupSgnNamed env n))
adamc@480 551 handle E.UnboundNamed _ => "UNBOUND" ^ Int.toString n)
adamc@45 552 | SgnFun (x, n, sgn, sgn') => box [string "functor",
adamc@45 553 space,
adamc@45 554 string "(",
adamc@480 555 p_named x n,
adamc@45 556 space,
adamc@45 557 string ":",
adamc@45 558 space,
adamc@45 559 p_sgn env sgn,
adamc@45 560 string ")",
adamc@45 561 space,
adamc@45 562 string ":",
adamc@45 563 space,
adamc@45 564 p_sgn (E.pushStrNamed env x n sgn) sgn']
adamc@45 565 | SgnWhere (sgn, x, c) => box [p_sgn env sgn,
adamc@45 566 space,
adamc@45 567 string "where",
adamc@45 568 space,
adamc@45 569 string "con",
adamc@45 570 space,
adamc@45 571 string x,
adamc@45 572 space,
adamc@45 573 string "=",
adamc@45 574 space,
adamc@45 575 p_con env c]
adamc@64 576 | SgnProj (m1, ms, x) =>
adamc@64 577 let
adamc@64 578 val (m1x, sgn) = E.lookupStrNamed env m1
adamc@480 579 handle E.UnboundNamed _ => ("UNBOUND" ^ Int.toString m1, (SgnConst [], loc))
adamc@64 580
adamc@64 581 val m1s = if !debug then
adamc@64 582 m1x ^ "__" ^ Int.toString m1
adamc@64 583 else
adamc@64 584 m1x
adamc@64 585 in
adamc@64 586 p_list_sep (string ".") string (m1x :: ms @ [x])
adamc@64 587 end
adamc@38 588
adamc@124 589 fun p_vali env (x, n, t, e) = box [p_named x n,
adamc@124 590 space,
adamc@124 591 string ":",
adamc@124 592 space,
adamc@124 593 p_con env t,
adamc@124 594 space,
adamc@124 595 string "=",
adamc@124 596 space,
adamc@124 597 p_exp env e]
adamc@124 598
adamc@124 599 fun p_decl env (dAll as (d, _) : decl) =
adamc@38 600 case d of
adamc@38 601 DCon (x, n, k, c) => box [string "con",
adamc@38 602 space,
adamc@38 603 p_named x n,
adamc@38 604 space,
adamc@38 605 string "::",
adamc@38 606 space,
adamc@624 607 p_kind env k,
adamc@38 608 space,
adamc@38 609 string "=",
adamc@38 610 space,
adamc@38 611 p_con env c]
adamc@806 612 | DDatatype x => box [string "datatype",
adamc@806 613 space,
adamc@806 614 p_list_sep (box [space, string "and", space]) (p_datatype (E.declBinds env dAll)) x]
adamc@191 615 | DDatatypeImp (x, _, m1, ms, x', _, _) =>
adamc@162 616 let
adamc@162 617 val m1x = #1 (E.lookupStrNamed env m1)
adamc@162 618 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
adamc@162 619 in
adamc@162 620 box [string "datatype",
adamc@162 621 space,
adamc@162 622 string x,
adamc@162 623 space,
adamc@162 624 string "=",
adamc@162 625 space,
adamc@162 626 string "datatype",
adamc@162 627 space,
adamc@162 628 p_list_sep (string ".") string (m1x :: ms @ [x'])]
adamc@162 629 end
adamc@124 630 | DVal vi => box [string "val",
adamc@124 631 space,
adamc@124 632 p_vali env vi]
adamc@124 633 | DValRec vis =>
adamc@124 634 let
adamc@124 635 val env = E.declBinds env dAll
adamc@124 636 in
adamc@124 637 box [string "val",
adamc@124 638 space,
adamc@124 639 string "rec",
adamc@124 640 space,
adamc@124 641 p_list_sep (box [newline, string "and", space]) (p_vali env) vis]
adamc@124 642 end
adamc@38 643
adamc@38 644 | DSgn (x, n, sgn) => box [string "signature",
adamc@38 645 space,
adamc@38 646 p_named x n,
adamc@38 647 space,
adamc@38 648 string "=",
adamc@38 649 space,
adamc@38 650 p_sgn env sgn]
adamc@38 651 | DStr (x, n, sgn, str) => box [string "structure",
adamc@38 652 space,
adamc@38 653 p_named x n,
adamc@38 654 space,
adamc@38 655 string ":",
adamc@38 656 space,
adamc@38 657 p_sgn env sgn,
adamc@38 658 space,
adamc@38 659 string "=",
adamc@38 660 space,
adamc@38 661 p_str env str]
adamc@48 662 | DFfiStr (x, n, sgn) => box [string "extern",
adamc@48 663 space,
adamc@48 664 string "structure",
adamc@48 665 space,
adamc@48 666 p_named x n,
adamc@48 667 space,
adamc@48 668 string ":",
adamc@48 669 space,
adamc@48 670 p_sgn env sgn]
adamc@109 671 | DExport (_, sgn, str) => box [string "export",
adamc@109 672 space,
adamc@109 673 p_str env str,
adamc@109 674 space,
adamc@109 675 string ":",
adamc@109 676 space,
adamc@109 677 p_sgn env sgn]
adamc@707 678 | DTable (_, x, n, c, pe, _, ce, _) => box [string "table",
adamc@707 679 space,
adamc@707 680 p_named x n,
adamc@707 681 space,
adamc@707 682 string ":",
adamc@707 683 space,
adamc@707 684 p_con env c,
adamc@707 685 space,
adamc@707 686 string "keys",
adamc@707 687 space,
adamc@707 688 p_exp env pe,
adamc@707 689 space,
adamc@707 690 string "constraints",
adamc@707 691 space,
adamc@707 692 p_exp env ce]
adamc@338 693 | DSequence (_, x, n) => box [string "sequence",
adamc@338 694 space,
adamc@338 695 p_named x n]
adamc@754 696 | DView (_, x, n, e, _) => box [string "view",
adamc@754 697 space,
adamc@754 698 p_named x n,
adamc@754 699 space,
adamc@754 700 string "as",
adamc@754 701 space,
adamc@754 702 p_exp env e]
adamc@271 703 | DDatabase s => box [string "database",
adamc@271 704 space,
adamc@271 705 string s]
adamc@460 706 | DCookie (_, x, n, c) => box [string "cookie",
adamc@460 707 space,
adamc@460 708 p_named x n,
adamc@460 709 space,
adamc@460 710 string ":",
adamc@460 711 space,
adamc@460 712 p_con env c]
adamc@720 713 | DStyle (_, x, n) => box [string "style",
adamc@720 714 space,
adamc@720 715 p_named x n]
adamc@1075 716 | DTask (e1, e2) => box [string "task",
adamc@1073 717 space,
adamc@1075 718 p_exp env e1,
adamc@1075 719 space,
adamc@1075 720 string "=",
adamc@1075 721 space,
adamc@1075 722 p_exp env e2]
adamc@1199 723 | DPolicy e1 => box [string "policy",
adamc@1199 724 space,
adamc@1199 725 p_exp env e1]
adamc@38 726
adamc@38 727 and p_str env (str, _) =
adamc@38 728 case str of
adamc@38 729 StrConst ds => box [string "struct",
adamc@38 730 newline,
adamc@38 731 p_file env ds,
adamc@38 732 newline,
adamc@38 733 string "end"]
adamc@146 734 | StrVar n =>
adamc@146 735 let
adamc@146 736 val x = #1 (E.lookupStrNamed env n)
adamc@480 737 handle E.UnboundNamed _ => "UNBOUND" ^ Int.toString n
adamc@146 738
adamc@146 739 val s = if !debug then
adamc@146 740 x ^ "__" ^ Int.toString n
adamc@146 741 else
adamc@146 742 x
adamc@146 743 in
adamc@146 744 string s
adamc@146 745 end
adamc@38 746 | StrProj (str, s) => box [p_str env str,
adamc@38 747 string ".",
adamc@38 748 string s]
adamc@45 749 | StrFun (x, n, sgn, sgn', str) =>
adamc@45 750 let
adamc@45 751 val env' = E.pushStrNamed env x n sgn
adamc@45 752 in
adamc@45 753 box [string "functor",
adamc@45 754 space,
adamc@45 755 string "(",
adamc@480 756 p_named x n,
adamc@45 757 space,
adamc@45 758 string ":",
adamc@45 759 space,
adamc@45 760 p_sgn env sgn,
adamc@45 761 string ")",
adamc@45 762 space,
adamc@45 763 string ":",
adamc@45 764 space,
adamc@45 765 p_sgn env' sgn',
adamc@45 766 space,
adamc@45 767 string "=>",
adamc@45 768 space,
adamc@45 769 p_str env' str]
adamc@45 770 end
adamc@45 771 | StrApp (str1, str2) => box [p_str env str1,
adamc@45 772 string "(",
adamc@45 773 p_str env str2,
adamc@45 774 string ")"]
adamc@38 775
adamc@38 776 and p_file env file =
adamc@38 777 let
adamc@38 778 val (pds, _) = ListUtil.foldlMap (fn (d, env) =>
adamc@38 779 (p_decl env d,
adamc@38 780 E.declBinds env d))
adamc@38 781 env file
adamc@38 782 in
adamc@38 783 p_list_sep newline (fn x => x) pds
adamc@38 784 end
adamc@38 785
adamc@38 786 end