Mercurial > urweb

annotate src/elab_print.sml @ 109:813e5a52063d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove closure conversion in favor of zany fun with modules, which also replaces 'page'
author Adam Chlipala <adamc@hcoop.net>
date Sun, 13 Jul 2008 10:17:06 -0400
parents f0f59e918cac
children 3739af9e727a
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@3 28 (* Pretty-printing elaborated Laconic/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@3 41 fun p_kind' par (k, _) =
adamc@3 42 case k of
adamc@3 43 KType => string "Type"
adamc@3 44 | KArrow (k1, k2) => parenIf par (box [p_kind' true k1,
adamc@3 45 space,
adamc@3 46 string "->",
adamc@3 47 space,
adamc@3 48 p_kind k2])
adamc@3 49 | KName => string "Name"
adamc@3 50 | KRecord k => box [string "{", p_kind k, string "}"]
adamc@82 51 | KUnit => string "Unit"
adamc@3 52
adamc@3 53 | KError => string "<ERROR>"
adamc@76 54 | KUnif (_, _, ref (SOME k)) => p_kind' par k
adamc@76 55 | KUnif (_, s, _) => string ("<UNIF:" ^ s ^ ">")
adamc@3 56
adamc@3 57 and p_kind k = p_kind' false k
adamc@3 58
adamc@3 59 fun p_explicitness e =
adamc@3 60 case e of
adamc@3 61 Explicit => string "::"
adamc@3 62 | Implicit => string ":::"
adamc@3 63
adamc@3 64 fun p_con' par env (c, _) =
adamc@3 65 case c of
adamc@3 66 TFun (t1, t2) => parenIf par (box [p_con' true env t1,
adamc@3 67 space,
adamc@3 68 string "->",
adamc@3 69 space,
adamc@3 70 p_con env t2])
adamc@3 71 | TCFun (e, x, k, c) => parenIf par (box [string x,
adamc@3 72 space,
adamc@3 73 p_explicitness e,
adamc@3 74 space,
adamc@3 75 p_kind k,
adamc@3 76 space,
adamc@3 77 string "->",
adamc@3 78 space,
adamc@3 79 p_con (E.pushCRel env x k) c])
adamc@85 80 | TDisjoint (c1, c2, c3) => parenIf par (box [p_con env c1,
adamc@85 81 space,
adamc@85 82 string "~",
adamc@85 83 space,
adamc@85 84 p_con env c2,
adamc@85 85 space,
adamc@85 86 string "->",
adamc@85 87 space,
adamc@85 88 p_con env c3])
adamc@3 89 | TRecord (CRecord (_, xcs), _) => box [string "{",
adamc@3 90 p_list (fn (x, c) =>
adamc@20 91 box [p_name env x,
adamc@3 92 space,
adamc@3 93 string ":",
adamc@3 94 space,
adamc@3 95 p_con env c]) xcs,
adamc@3 96 string "}"]
adamc@3 97 | TRecord c => box [string "$",
adamc@3 98 p_con' true env c]
adamc@3 99
adamc@11 100 | CRel n =>
adamc@71 101 ((if !debug then
adamc@71 102 string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n)
adamc@71 103 else
adamc@71 104 string (#1 (E.lookupCRel env n)))
adamc@71 105 handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n))
adamc@11 106 | CNamed n =>
adamc@34 107 ((if !debug then
adamc@34 108 string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n)
adamc@34 109 else
adamc@34 110 string (#1 (E.lookupCNamed env n)))
adamc@34 111 handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n))
adamc@34 112 | CModProj (m1, ms, x) =>
adamc@34 113 let
adamc@88 114 val m1x = #1 (E.lookupStrNamed env m1)
adamc@88 115 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
adamc@88 116
adamc@34 117 val m1s = if !debug then
adamc@34 118 m1x ^ "__" ^ Int.toString m1
adamc@34 119 else
adamc@34 120 m1x
adamc@34 121 in
adamc@34 122 p_list_sep (string ".") string (m1x :: ms @ [x])
adamc@88 123 end
adamc@3 124
adamc@3 125 | CApp (c1, c2) => parenIf par (box [p_con env c1,
adamc@3 126 space,
adamc@3 127 p_con' true env c2])
adamc@8 128 | CAbs (x, k, c) => parenIf par (box [string "fn",
adamc@8 129 space,
adamc@8 130 string x,
adamc@8 131 space,
adamc@8 132 string "::",
adamc@8 133 space,
adamc@8 134 p_kind k,
adamc@8 135 space,
adamc@8 136 string "=>",
adamc@8 137 space,
adamc@8 138 p_con (E.pushCRel env x k) c])
adamc@84 139 | CDisjoint (c1, c2, c3) => parenIf par (box [p_con env c1,
adamc@84 140 space,
adamc@84 141 string "~",
adamc@84 142 space,
adamc@84 143 p_con env c2,
adamc@84 144 space,
adamc@84 145 string "=>",
adamc@84 146 space,
adamc@84 147 p_con env c3])
adamc@3 148
adamc@3 149 | CName s => box [string "#", string s]
adamc@3 150
adamc@12 151 | CRecord (k, xcs) =>
adamc@12 152 if !debug then
adamc@12 153 parenIf par (box [string "[",
adamc@12 154 p_list (fn (x, c) =>
adamc@12 155 box [p_con env x,
adamc@12 156 space,
adamc@12 157 string "=",
adamc@12 158 space,
adamc@12 159 p_con env c]) xcs,
adamc@12 160 string "]::",
adamc@12 161 p_kind k])
adamc@12 162 else
adamc@12 163 parenIf par (box [string "[",
adamc@12 164 p_list (fn (x, c) =>
adamc@12 165 box [p_con env x,
adamc@12 166 space,
adamc@12 167 string "=",
adamc@12 168 space,
adamc@12 169 p_con env c]) xcs,
adamc@12 170 string "]"])
adamc@3 171 | CConcat (c1, c2) => parenIf par (box [p_con' true env c1,
adamc@3 172 space,
adamc@3 173 string "++",
adamc@3 174 space,
adamc@3 175 p_con env c2])
adamc@67 176 | CFold _ => string "fold"
adamc@3 177
adamc@82 178 | CUnit => string "()"
adamc@82 179
adamc@3 180 | CError => string "<ERROR>"
adamc@76 181 | CUnif (_, _, _, ref (SOME c)) => p_con' par env c
adamc@76 182 | CUnif (_, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"),
adamc@76 183 p_kind k,
adamc@76 184 string ">"]
adamc@3 185
adamc@3 186 and p_con env = p_con' false env
adamc@3 187
adamc@20 188 and p_name env (all as (c, _)) =
adamc@20 189 case c of
adamc@20 190 CName s => string s
adamc@20 191 | _ => p_con env all
adamc@20 192
adamc@9 193 fun p_exp' par env (e, _) =
adamc@9 194 case e of
adamc@14 195 EPrim p => Prim.p_t p
adamc@14 196 | ERel n =>
adamc@88 197 ((if !debug then
adamc@88 198 string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n)
adamc@88 199 else
adamc@88 200 string (#1 (E.lookupERel env n)))
adamc@88 201 handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n))
adamc@11 202 | ENamed n =>
adamc@88 203 ((if !debug then
adamc@88 204 string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
adamc@88 205 else
adamc@88 206 string (#1 (E.lookupENamed env n)))
adamc@88 207 handle E.UnboundRel _ => string ("UNBOUND_NAMED" ^ Int.toString n))
adamc@34 208 | EModProj (m1, ms, x) =>
adamc@34 209 let
adamc@88 210 val m1x = #1 (E.lookupStrNamed env m1)
adamc@88 211 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
adamc@88 212
adamc@34 213 val m1s = if !debug then
adamc@34 214 m1x ^ "__" ^ Int.toString m1
adamc@34 215 else
adamc@34 216 m1x
adamc@34 217 in
adamc@34 218 p_list_sep (string ".") string (m1x :: ms @ [x])
adamc@34 219 end
adamc@34 220
adamc@9 221 | EApp (e1, e2) => parenIf par (box [p_exp env e1,
adamc@9 222 space,
adamc@9 223 p_exp' true env e2])
adamc@26 224 | EAbs (x, t, _, e) => parenIf par (box [string "fn",
adamc@26 225 space,
adamc@26 226 string x,
adamc@26 227 space,
adamc@26 228 string ":",
adamc@26 229 space,
adamc@26 230 p_con env t,
adamc@26 231 space,
adamc@26 232 string "=>",
adamc@26 233 space,
adamc@26 234 p_exp (E.pushERel env x t) e])
adamc@9 235 | ECApp (e, c) => parenIf par (box [p_exp env e,
adamc@9 236 space,
adamc@9 237 string "[",
adamc@9 238 p_con env c,
adamc@9 239 string "]"])
adamc@9 240 | ECAbs (exp, x, k, e) => parenIf par (box [string "fn",
adamc@9 241 space,
adamc@9 242 string x,
adamc@9 243 space,
adamc@9 244 p_explicitness exp,
adamc@9 245 space,
adamc@9 246 p_kind k,
adamc@9 247 space,
adamc@9 248 string "=>",
adamc@9 249 space,
adamc@9 250 p_exp (E.pushCRel env x k) e])
adamc@9 251
adamc@12 252 | ERecord xes => box [string "{",
adamc@29 253 p_list (fn (x, e, _) =>
adamc@21 254 box [p_name env x,
adamc@12 255 space,
adamc@12 256 string "=",
adamc@12 257 space,
adamc@12 258 p_exp env e]) xes,
adamc@12 259 string "}"]
adamc@12 260 | EField (e, c, {field, rest}) =>
adamc@12 261 if !debug then
adamc@12 262 box [p_exp' true env e,
adamc@12 263 string ".",
adamc@12 264 p_con' true env c,
adamc@12 265 space,
adamc@12 266 string "[",
adamc@12 267 p_con env field,
adamc@12 268 space,
adamc@12 269 string " in ",
adamc@12 270 space,
adamc@12 271 p_con env rest,
adamc@12 272 string "]"]
adamc@12 273 else
adamc@12 274 box [p_exp' true env e,
adamc@12 275 string ".",
adamc@12 276 p_con' true env c]
adamc@72 277 | EFold _ => string "fold"
adamc@71 278
adamc@9 279 | EError => string "<ERROR>"
adamc@9 280
adamc@9 281 and p_exp env = p_exp' false env
adamc@9 282
adamc@31 283 fun p_named x n =
adamc@31 284 if !debug then
adamc@31 285 box [string x,
adamc@31 286 string "__",
adamc@31 287 string (Int.toString n)]
adamc@31 288 else
adamc@31 289 string x
adamc@31 290
adamc@31 291 fun p_sgn_item env (sgi, _) =
adamc@31 292 case sgi of
adamc@31 293 SgiConAbs (x, n, k) => box [string "con",
adamc@31 294 space,
adamc@31 295 p_named x n,
adamc@31 296 space,
adamc@31 297 string "::",
adamc@31 298 space,
adamc@31 299 p_kind k]
adamc@31 300 | SgiCon (x, n, k, c) => box [string "con",
adamc@31 301 space,
adamc@31 302 p_named x n,
adamc@31 303 space,
adamc@31 304 string "::",
adamc@31 305 space,
adamc@31 306 p_kind k,
adamc@31 307 space,
adamc@31 308 string "=",
adamc@31 309 space,
adamc@31 310 p_con env c]
adamc@31 311 | SgiVal (x, n, c) => box [string "val",
adamc@31 312 space,
adamc@31 313 p_named x n,
adamc@31 314 space,
adamc@31 315 string ":",
adamc@31 316 space,
adamc@31 317 p_con env c]
adamc@31 318 | SgiStr (x, n, sgn) => box [string "structure",
adamc@31 319 space,
adamc@31 320 p_named x n,
adamc@31 321 space,
adamc@31 322 string ":",
adamc@31 323 space,
adamc@31 324 p_sgn env sgn]
adamc@59 325 | SgiSgn (x, n, sgn) => box [string "signature",
adamc@59 326 space,
adamc@59 327 p_named x n,
adamc@59 328 space,
adamc@59 329 string "=",
adamc@59 330 space,
adamc@59 331 p_sgn env sgn]
adamc@88 332 | SgiConstraint (c1, c2) => box [string "constraint",
adamc@88 333 space,
adamc@88 334 p_con env c1,
adamc@88 335 space,
adamc@88 336 string "~",
adamc@88 337 space,
adamc@88 338 p_con env c2]
adamc@31 339
adamc@31 340 and p_sgn env (sgn, _) =
adamc@31 341 case sgn of
adamc@31 342 SgnConst sgis => box [string "sig",
adamc@31 343 newline,
adamc@32 344 let
adamc@32 345 val (psgis, _) = ListUtil.foldlMap (fn (sgi, env) =>
adamc@32 346 (p_sgn_item env sgi,
adamc@32 347 E.sgiBinds env sgi))
adamc@32 348 env sgis
adamc@32 349 in
adamc@32 350 p_list_sep newline (fn x => x) psgis
adamc@32 351 end,
adamc@31 352 newline,
adamc@31 353 string "end"]
adamc@88 354 | SgnVar n => ((string (#1 (E.lookupSgnNamed env n)))
adamc@88 355 handle E.UnboundNamed _ => string ("UNBOUND_SGN_" ^ Int.toString n))
adamc@41 356 | SgnFun (x, n, sgn, sgn') => box [string "functor",
adamc@41 357 space,
adamc@41 358 string "(",
adamc@41 359 string x,
adamc@41 360 space,
adamc@41 361 string ":",
adamc@41 362 space,
adamc@41 363 p_sgn env sgn,
adamc@41 364 string ")",
adamc@41 365 space,
adamc@41 366 string ":",
adamc@41 367 space,
adamc@41 368 p_sgn (E.pushStrNamedAs env x n sgn) sgn']
adamc@42 369 | SgnWhere (sgn, x, c) => box [p_sgn env sgn,
adamc@42 370 space,
adamc@42 371 string "where",
adamc@42 372 space,
adamc@42 373 string "con",
adamc@42 374 space,
adamc@42 375 string x,
adamc@42 376 space,
adamc@42 377 string "=",
adamc@42 378 space,
adamc@42 379 p_con env c]
adamc@59 380 | SgnProj (m1, ms, x) =>
adamc@59 381 let
adamc@88 382 val m1x = #1 (E.lookupStrNamed env m1)
adamc@88 383 handle E.UnboundNamed _ => "UNBOUND_SGN_" ^ Int.toString m1
adamc@88 384
adamc@59 385 val m1s = if !debug then
adamc@59 386 m1x ^ "__" ^ Int.toString m1
adamc@59 387 else
adamc@59 388 m1x
adamc@88 389 in
adamc@59 390 p_list_sep (string ".") string (m1x :: ms @ [x])
adamc@59 391 end
adamc@31 392 | SgnError => string "<ERROR>"
adamc@31 393
adamc@3 394 fun p_decl env ((d, _) : decl) =
adamc@3 395 case d of
adamc@31 396 DCon (x, n, k, c) => box [string "con",
adamc@31 397 space,
adamc@31 398 p_named x n,
adamc@31 399 space,
adamc@31 400 string "::",
adamc@31 401 space,
adamc@31 402 p_kind k,
adamc@31 403 space,
adamc@31 404 string "=",
adamc@31 405 space,
adamc@31 406 p_con env c]
adamc@31 407 | DVal (x, n, t, e) => box [string "val",
adamc@31 408 space,
adamc@31 409 p_named x n,
adamc@31 410 space,
adamc@31 411 string ":",
adamc@31 412 space,
adamc@31 413 p_con env t,
adamc@31 414 space,
adamc@31 415 string "=",
adamc@31 416 space,
adamc@31 417 p_exp env e]
adamc@31 418
adamc@31 419 | DSgn (x, n, sgn) => box [string "signature",
adamc@31 420 space,
adamc@31 421 p_named x n,
adamc@31 422 space,
adamc@31 423 string "=",
adamc@31 424 space,
adamc@31 425 p_sgn env sgn]
adamc@31 426 | DStr (x, n, sgn, str) => box [string "structure",
adamc@31 427 space,
adamc@31 428 p_named x n,
adamc@31 429 space,
adamc@31 430 string ":",
adamc@31 431 space,
adamc@31 432 p_sgn env sgn,
adamc@31 433 space,
adamc@31 434 string "=",
adamc@31 435 space,
adamc@31 436 p_str env str]
adamc@48 437 | DFfiStr (x, n, sgn) => box [string "extern",
adamc@48 438 space,
adamc@48 439 string "structure",
adamc@48 440 space,
adamc@48 441 p_named x n,
adamc@48 442 space,
adamc@48 443 string ":",
adamc@48 444 space,
adamc@48 445 p_sgn env sgn]
adamc@88 446 | DConstraint (c1, c2) => box [string "constraint",
adamc@88 447 space,
adamc@88 448 p_con env c1,
adamc@88 449 space,
adamc@88 450 string "~",
adamc@88 451 space,
adamc@88 452 p_con env c2]
adamc@109 453 | DExport (_, sgn, str) => box [string "export",
adamc@109 454 p_str env str,
adamc@109 455 space,
adamc@109 456 string ":",
adamc@109 457 space,
adamc@109 458 p_sgn env sgn]
adamc@31 459
adamc@31 460 and p_str env (str, _) =
adamc@31 461 case str of
adamc@31 462 StrConst ds => box [string "struct",
adamc@31 463 newline,
adamc@32 464 p_file env ds,
adamc@31 465 newline,
adamc@31 466 string "end"]
adamc@88 467 | StrVar n => ((string (#1 (E.lookupStrNamed env n)))
adamc@88 468 handle E.UnboundNamed _ => string ("UNBOUND_STR_" ^ Int.toString n))
adamc@34 469 | StrProj (str, s) => box [p_str env str,
adamc@34 470 string ".",
adamc@34 471 string s]
adamc@41 472 | StrFun (x, n, sgn, sgn', str) =>
adamc@41 473 let
adamc@41 474 val env' = E.pushStrNamedAs env x n sgn
adamc@41 475 in
adamc@41 476 box [string "functor",
adamc@41 477 space,
adamc@41 478 string "(",
adamc@41 479 string x,
adamc@41 480 space,
adamc@41 481 string ":",
adamc@41 482 space,
adamc@41 483 p_sgn env sgn,
adamc@41 484 string ")",
adamc@41 485 space,
adamc@41 486 string ":",
adamc@41 487 space,
adamc@41 488 p_sgn env' sgn',
adamc@41 489 space,
adamc@41 490 string "=>",
adamc@41 491 space,
adamc@41 492 p_str env' str]
adamc@41 493 end
adamc@44 494 | StrApp (str1, str2) => box [p_str env str1,
adamc@44 495 string "(",
adamc@44 496 p_str env str2,
adamc@44 497 string ")"]
adamc@31 498 | StrError => string "<ERROR>"
adamc@3 499
adamc@32 500 and p_file env file =
adamc@3 501 let
adamc@31 502 val (pds, _) = ListUtil.foldlMap (fn (d, env) =>
adamc@31 503 (p_decl env d,
adamc@31 504 E.declBinds env d))
adamc@31 505 env file
adamc@3 506 in
adamc@3 507 p_list_sep newline (fn x => x) pds
adamc@3 508 end
adamc@3 509
adamc@3 510 end