Mercurial > urweb

comparison src/elab_print.sml @ 88:7bab29834cd6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Constraints in modules
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 15:58:02 -0400
parents 1f85890c9846
children f0f59e918cac
comparison
equal deleted inserted replaced
87:275aaeb73f1f 88:7bab29834cd6
109 else 109 else
110 string (#1 (E.lookupCNamed env n))) 110 string (#1 (E.lookupCNamed env n)))
111 handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n)) 111 handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n))
112 | CModProj (m1, ms, x) => 112 | CModProj (m1, ms, x) =>
113 let 113 let
114 val (m1x, sgn) = E.lookupStrNamed env m1 114 val m1x = #1 (E.lookupStrNamed env m1)
115 115 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
116
116 val m1s = if !debug then 117 val m1s = if !debug then
117 m1x ^ "__" ^ Int.toString m1 118 m1x ^ "__" ^ Int.toString m1
118 else 119 else
119 m1x 120 m1x
120 in 121 in
121 p_list_sep (string ".") string (m1x :: ms @ [x]) 122 p_list_sep (string ".") string (m1x :: ms @ [x])
122 end 123 end
123 124
124 | CApp (c1, c2) => parenIf par (box [p_con env c1, 125 | CApp (c1, c2) => parenIf par (box [p_con env c1,
125 space, 126 space,
126 p_con' true env c2]) 127 p_con' true env c2])
127 | CAbs (x, k, c) => parenIf par (box [string "fn", 128 | CAbs (x, k, c) => parenIf par (box [string "fn",
191 192
192 fun p_exp' par env (e, _) = 193 fun p_exp' par env (e, _) =
193 case e of 194 case e of
194 EPrim p => Prim.p_t p 195 EPrim p => Prim.p_t p
195 | ERel n => 196 | ERel n =>
196 if !debug then 197 ((if !debug then
197 string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n) 198 string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n)
198 else 199 else
199 string (#1 (E.lookupERel env n)) 200 string (#1 (E.lookupERel env n)))
201 handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n))
200 | ENamed n => 202 | ENamed n =>
201 if !debug then 203 ((if !debug then
202 string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) 204 string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
203 else 205 else
204 string (#1 (E.lookupENamed env n)) 206 string (#1 (E.lookupENamed env n)))
207 handle E.UnboundRel _ => string ("UNBOUND_NAMED" ^ Int.toString n))
205 | EModProj (m1, ms, x) => 208 | EModProj (m1, ms, x) =>
206 let 209 let
207 val (m1x, sgn) = E.lookupStrNamed env m1 210 val m1x = #1 (E.lookupStrNamed env m1)
208 211 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
212
209 val m1s = if !debug then 213 val m1s = if !debug then
210 m1x ^ "__" ^ Int.toString m1 214 m1x ^ "__" ^ Int.toString m1
211 else 215 else
212 m1x 216 m1x
213 in 217 in
323 p_named x n, 327 p_named x n,
324 space, 328 space,
325 string "=", 329 string "=",
326 space, 330 space,
327 p_sgn env sgn] 331 p_sgn env sgn]
332 | SgiConstraint (c1, c2) => box [string "constraint",
333 space,
334 p_con env c1,
335 space,
336 string "~",
337 space,
338 p_con env c2]
328 339
329 and p_sgn env (sgn, _) = 340 and p_sgn env (sgn, _) =
330 case sgn of 341 case sgn of
331 SgnConst sgis => box [string "sig", 342 SgnConst sgis => box [string "sig",
332 newline, 343 newline,
338 in 349 in
339 p_list_sep newline (fn x => x) psgis 350 p_list_sep newline (fn x => x) psgis
340 end, 351 end,
341 newline, 352 newline,
342 string "end"] 353 string "end"]
343 | SgnVar n => string (#1 (E.lookupSgnNamed env n)) 354 | SgnVar n => ((string (#1 (E.lookupSgnNamed env n)))
355 handle E.UnboundNamed _ => string ("UNBOUND_SGN_" ^ Int.toString n))
344 | SgnFun (x, n, sgn, sgn') => box [string "functor", 356 | SgnFun (x, n, sgn, sgn') => box [string "functor",
345 space, 357 space,
346 string "(", 358 string "(",
347 string x, 359 string x,
348 space, 360 space,
365 string "=", 377 string "=",
366 space, 378 space,
367 p_con env c] 379 p_con env c]
368 | SgnProj (m1, ms, x) => 380 | SgnProj (m1, ms, x) =>
369 let 381 let
370 val (m1x, sgn) = E.lookupStrNamed env m1 382 val m1x = #1 (E.lookupStrNamed env m1)
371 383 handle E.UnboundNamed _ => "UNBOUND_SGN_" ^ Int.toString m1
384
372 val m1s = if !debug then 385 val m1s = if !debug then
373 m1x ^ "__" ^ Int.toString m1 386 m1x ^ "__" ^ Int.toString m1
374 else 387 else
375 m1x 388 m1x
376 in 389 in
377 p_list_sep (string ".") string (m1x :: ms @ [x]) 390 p_list_sep (string ".") string (m1x :: ms @ [x])
378 end 391 end
379 | SgnError => string "<ERROR>" 392 | SgnError => string "<ERROR>"
380 393
381 fun p_decl env ((d, _) : decl) = 394 fun p_decl env ((d, _) : decl) =
428 p_named x n, 441 p_named x n,
429 space, 442 space,
430 string ":", 443 string ":",
431 space, 444 space,
432 p_sgn env sgn] 445 p_sgn env sgn]
446 | DConstraint (c1, c2) => box [string "constraint",
447 space,
448 p_con env c1,
449 space,
450 string "~",
451 space,
452 p_con env c2]
433 453
434 and p_str env (str, _) = 454 and p_str env (str, _) =
435 case str of 455 case str of
436 StrConst ds => box [string "struct", 456 StrConst ds => box [string "struct",
437 newline, 457 newline,
438 p_file env ds, 458 p_file env ds,
439 newline, 459 newline,
440 string "end"] 460 string "end"]
441 | StrVar n => string (#1 (E.lookupStrNamed env n)) 461 | StrVar n => ((string (#1 (E.lookupStrNamed env n)))
462 handle E.UnboundNamed _ => string ("UNBOUND_STR_" ^ Int.toString n))
442 | StrProj (str, s) => box [p_str env str, 463 | StrProj (str, s) => box [p_str env str,
443 string ".", 464 string ".",
444 string s] 465 string s]
445 | StrFun (x, n, sgn, sgn', str) => 466 | StrFun (x, n, sgn, sgn', str) =>
446 let 467 let