Mercurial > urweb

annotate src/elab_print.sml @ 2262:34ad83d9b729

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