From ffbef6329458347da5805b12c98819cc0ce4ab73 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 25 Nov 2005 11:11:41 +0000 Subject: [PATCH] dependency graphs --- helm/papers/matita/Makefile | 8 + helm/papers/matita/libraries.dot | 104 ++ helm/papers/matita/libraries.ps | 1031 +++++++++++----- helm/papers/matita/librariesCluster.ps | 1513 ++++++++++++++++++++++++ helm/papers/matita/matita2.tex | 2 +- 5 files changed, 2363 insertions(+), 295 deletions(-) create mode 100644 helm/papers/matita/libraries.dot create mode 100644 helm/papers/matita/librariesCluster.ps diff --git a/helm/papers/matita/Makefile b/helm/papers/matita/Makefile index dc95f6691..8cbb80617 100644 --- a/helm/papers/matita/Makefile +++ b/helm/papers/matita/Makefile @@ -32,6 +32,14 @@ SHOW_FORMAT = dvi ######################################################################## +libraries.ps: libraries.dot + dot -Gclusterrank=none -Tps -o $@ $< +librariesCluster.ps: libraries.dot + dot -Tps -o $@ $< +matita2.dvi: libraries.ps librariesCluster.ps + +######################################################################## + AVAILABLE_FORMATS = dvi ps ps.gz pdf html ADVI = advi diff --git a/helm/papers/matita/libraries.dot b/helm/papers/matita/libraries.dot new file mode 100644 index 000000000..c16802a96 --- /dev/null +++ b/helm/papers/matita/libraries.dot @@ -0,0 +1,104 @@ +digraph G { +// clusterrank = none; + fillcolor = "gray93"; + fontsize = 24; + node [fontsize = 24]; + /* libs clusters */ + subgraph cluster_presentation { + label = "Terms at the content and presentation level"; + rank = min; + labelloc = "b"; + labeljust = "r"; + style = "filled"; + color = "white" + acic_content; + cic_acic; + cic_disambiguation; + content_pres; + grafite; + } + subgraph cluster_partially { + label = "Partially specified terms"; + labelloc = "t"; + labeljust = "l"; + style = "filled"; + color = "white" + cic_unification; + tactics; + paramodulation; + } + subgraph cluster_fully { + label = "Fully specified terms"; + labelloc = "b"; + labeljust = "l"; + style = "filled"; + color = "white" + cic; + cic_proof_checking; + getter; + metadata; + urimanager; + whelp; + } + subgraph cluster_utilities { + label = "Utilities"; + rank = max; + labelloc = "b"; + labeljust = "r"; + style = "filled"; + color = "white" + extlib; + hgdome; + hmysql; + registry; + utf8_macros; + xml; + } + /* libs */ + paramodulation -> tactics; + cic_disambiguation -> cic_unification; + cic_disambiguation -> acic_content; + cic_disambiguation -> whelp; + tactics -> whelp; + tactics -> cic_unification; + whelp -> metadata; + metadata -> cic; + metadata -> getter; + metadata -> hmysql; + grafite -> content_pres; + content_pres -> utf8_macros; + content_pres -> acic_content; + acic_content -> cic_acic; + cic_acic -> cic_proof_checking; + cic_unification -> cic_proof_checking; + cic_proof_checking -> getter; + cic_proof_checking -> cic; + cic -> xml; + cic -> urimanager; + getter -> registry; + getter -> urimanager; + hmysql -> registry; + registry -> xml; + hgdome -> xml; + xml -> extlib; + /* apps */ + subgraph applications { + node [shape=plaintext,style=filled,fillcolor=slategray2]; + DrawGraph; + Getter; + Matita; + ProofChecker; + Uwobo; + Whelp; + } + /* apps dep */ + DrawGraph -> getter; + Getter -> getter; + Matita -> cic_disambiguation; + Matita -> tactics; + ProofChecker -> cic_proof_checking; + Uwobo -> acic_content; + Uwobo -> content_pres; + Whelp -> cic_disambiguation; + Whelp -> whelp; +} diff --git a/helm/papers/matita/libraries.ps b/helm/papers/matita/libraries.ps index 2fe948119..e6cbb4d23 100644 --- a/helm/papers/matita/libraries.ps +++ b/helm/papers/matita/libraries.ps @@ -1,9 +1,9 @@ %!PS-Adobe-2.0 -%%Creator: dot version 2.2.1 (Tue Apr 12 00:03:35 UTC 2005) -%%For: (sacerdot) Claudio Sacerdoti Coen,,, +%%Creator: dot version 2.2.1 (Fri Sep 30 13:22:44 UTC 2005) +%%For: (zacchiro) Stefano Zacchiroli,,, %%Title: G %%Pages: (atend) -%%BoundingBox: 35 35 461 649 +%%BoundingBox: 35 35 819 801 %%EndComments save %%BeginProlog @@ -230,714 +230,1157 @@ def %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 461 649 +%%PageBoundingBox: 36 36 819 801 %%PageOrientation: Portrait gsave -35 35 426 614 boxprim clip newpath +35 35 784 766 boxprim clip newpath 36 36 translate 0 0 1 beginpage 0 0 translate 0 rotate 0.000 0.000 0.000 graphcolor -14.00 /Times-Roman set_font +24.00 /Times-Roman set_font -% paramodulation +% acic_content gsave 10 dict begin -164 594 57 18 ellipse_path +536 562 75 25 ellipse_path stroke gsave 10 dict begin -119 589 moveto -(paramodulation) -[6.96 6.24 4.56 6.24 10.8 6.96 6.96 6.96 3.84 6.24 3.84 3.84 6.96 6.96] +475 554 moveto +(acic_content) +[10.56 10.56 6.72 10.56 12 10.56 12 12 6.72 10.56 12 6.72] +xshow +end grestore +end grestore + +% cic_acic +gsave 10 dict begin +487 474 54 25 ellipse_path +stroke +gsave 10 dict begin +447 466 moveto +(cic_acic) +[10.56 6.72 10.56 12 10.56 10.56 6.72 10.56] xshow end grestore end grestore +% acic_content -> cic_acic +newpath 522 537 moveto +517 528 511 518 506 508 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 509 506 moveto +501 499 lineto +503 509 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 509 506 moveto +501 499 lineto +503 509 lineto +closepath +stroke +end grestore + +% cic_proof_checking +gsave 10 dict begin +487 386 110 25 ellipse_path +stroke +gsave 10 dict begin +391 378 moveto +(cic_proof_checking) +[10.56 6.72 10.56 12 12 7.92 12 12 7.92 12 10.56 12 10.56 10.56 12 6.72 12 12] +xshow +end grestore +end grestore + +% cic_acic -> cic_proof_checking +newpath 487 448 moveto +487 440 487 431 487 422 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 491 422 moveto +487 412 lineto +484 422 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 491 422 moveto +487 412 lineto +484 422 lineto +closepath +stroke +end grestore + % cic_disambiguation gsave 10 dict begin -164 522 68 18 ellipse_path +377 650 109 25 ellipse_path stroke gsave 10 dict begin -109 517 moveto +282 642 moveto (cic_disambiguation) -[6.24 3.84 6.24 6.96 6.96 3.84 5.52 6.24 10.8 6.96 3.84 6.96 6.96 6.24 3.84 3.84 6.96 6.96] +[10.56 6.72 10.56 12 12 6.72 9.36 10.56 18.72 12 6.72 12 12 10.56 6.72 6.72 12 12] xshow end grestore end grestore -% paramodulation -> cic_disambiguation -newpath 164 576 moveto -164 568 164 559 164 550 curveto +% cic_disambiguation -> acic_content +newpath 420 626 moveto +441 615 466 601 487 589 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 168 550 moveto -164 540 lineto -161 550 lineto +newpath 489 592 moveto +496 584 lineto +486 586 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 168 550 moveto -164 540 lineto -161 550 lineto +newpath 489 592 moveto +496 584 lineto +486 586 lineto closepath stroke end grestore -% cic_notation +% cic_unification gsave 10 dict begin -48 378 48 18 ellipse_path +355 562 86 25 ellipse_path stroke gsave 10 dict begin -13 373 moveto -(cic_notation) -[6.24 3.84 6.24 6.96 6.96 6.96 3.84 6.24 3.84 3.84 6.96 6.96] +283 554 moveto +(cic_unification) +[10.56 6.72 10.56 12 12 12 6.72 7.92 6.72 10.56 10.56 6.72 6.72 12 12] xshow end grestore end grestore -% cic_disambiguation -> cic_notation -newpath 128 507 moveto -111 498 91 485 77 468 curveto -64 450 56 425 52 406 curveto +% cic_disambiguation -> cic_unification +newpath 371 624 moveto +369 616 366 607 364 598 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 55 405 moveto -50 396 lineto -49 406 lineto +newpath 367 597 moveto +362 588 lineto +361 598 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 55 405 moveto -50 396 lineto -49 406 lineto +newpath 367 597 moveto +362 588 lineto +361 598 lineto closepath stroke end grestore -% tactics +% whelp gsave 10 dict begin -275 450 31 18 ellipse_path +205 562 44 25 ellipse_path stroke gsave 10 dict begin -256 445 moveto -(tactics) -[3.84 6.24 6.24 3.84 3.84 6.24 5.52] +175 554 moveto +(whelp) +[17.28 12 10.56 6.72 12] xshow end grestore end grestore -% cic_disambiguation -> tactics -newpath 190 505 moveto -207 494 228 480 246 469 curveto +% cic_disambiguation -> whelp +newpath 331 627 moveto +305 614 273 597 247 584 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 248 472 moveto -254 463 lineto -244 466 lineto +newpath 248 581 moveto +238 579 lineto +245 587 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 248 472 moveto -254 463 lineto -244 466 lineto +newpath 248 581 moveto +238 579 lineto +245 587 lineto closepath stroke end grestore -% cic_proof_checking +% content_pres gsave 10 dict begin -242 306 68 18 ellipse_path +643 650 76 25 ellipse_path stroke gsave 10 dict begin -186 301 moveto -(cic_proof_checking) -[6.24 3.84 6.24 6.96 6.96 4.56 6.96 6.96 4.56 6.96 6.24 6.96 6.24 6.24 6.96 3.84 6.96 6.96] +581 642 moveto +(content_pres) +[10.56 12 12 6.72 10.56 12 6.72 12 12 7.92 10.56 9.36] xshow end grestore end grestore -% cic_notation -> cic_proof_checking -newpath 82 365 moveto -113 354 158 337 192 325 curveto +% content_pres -> acic_content +newpath 614 626 moveto +602 616 586 603 573 593 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 194 328 moveto -202 321 lineto -191 321 lineto +newpath 575 590 moveto +565 586 lineto +570 595 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 194 328 moveto -202 321 lineto -191 321 lineto +newpath 575 590 moveto +565 586 lineto +570 595 lineto closepath stroke end grestore % utf8_macros gsave 10 dict begin -48 306 48 18 ellipse_path +706 562 75 25 ellipse_path stroke gsave 10 dict begin -12 301 moveto +645 554 moveto (utf8_macros) -[6.96 3.84 4.56 6.96 6.96 10.8 6.24 6.24 4.56 6.96 5.52] +[12 6.72 7.92 12 12 18.72 10.56 10.56 7.92 12 9.36] xshow end grestore end grestore -% cic_notation -> utf8_macros -newpath 48 360 moveto -48 352 48 343 48 334 curveto +% content_pres -> utf8_macros +newpath 661 625 moveto +668 616 676 605 682 595 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 52 334 moveto -48 324 lineto -45 334 lineto +newpath 685 597 moveto +688 587 lineto +679 593 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 52 334 moveto -48 324 lineto -45 334 lineto +newpath 685 597 moveto +688 587 lineto +679 593 lineto closepath stroke end grestore -% metadata +% grafite gsave 10 dict begin -386 378 38 18 ellipse_path +644 738 46 25 ellipse_path stroke gsave 10 dict begin -360 373 moveto -(metadata) -[10.8 6.24 3.84 6.24 6.96 6.24 3.84 6.24] +612 730 moveto +(grafite) +[12 7.92 10.56 7.92 6.72 6.72 10.56] xshow end grestore end grestore -% tactics -> metadata -newpath 296 436 moveto -312 426 336 411 355 399 curveto +% grafite -> content_pres +newpath 644 712 moveto +644 704 643 695 643 686 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 357 402 moveto -363 393 lineto -353 396 lineto +newpath 647 686 moveto +643 676 lineto +640 686 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 357 402 moveto -363 393 lineto -353 396 lineto +newpath 647 686 moveto +643 676 lineto +640 686 lineto closepath stroke end grestore -% cic_unification +% cic_unification -> cic_proof_checking +newpath 367 537 moveto +380 513 400 476 423 448 curveto +431 438 441 427 450 418 curveto +stroke gsave 10 dict begin -275 378 55 18 ellipse_path +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 453 420 moveto +458 411 lineto +448 415 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 453 420 moveto +458 411 lineto +448 415 lineto +closepath stroke +end grestore + +% tactics gsave 10 dict begin -233 373 moveto -(cic_unification) -[6.24 3.84 6.24 6.96 6.96 6.96 3.84 4.56 3.84 6.24 6.24 3.84 3.84 6.96 6.96] +165 650 45 25 ellipse_path +stroke +gsave 10 dict begin +134 642 moveto +(tactics) +[6.72 10.56 10.56 6.72 6.72 10.56 9.36] xshow end grestore end grestore % tactics -> cic_unification -newpath 275 432 moveto -275 424 275 415 275 406 curveto +newpath 201 633 moveto +228 620 267 603 299 588 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 279 406 moveto -275 396 lineto -272 406 lineto +newpath 300 591 moveto +308 584 lineto +297 585 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 279 406 moveto -275 396 lineto -272 406 lineto +newpath 300 591 moveto +308 584 lineto +297 585 lineto closepath stroke end grestore -% cic_transformations +% tactics -> whelp +newpath 176 625 moveto +181 616 185 606 190 596 curveto +stroke gsave 10 dict begin -154 450 68 18 ellipse_path +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 193 598 moveto +194 587 lineto +187 595 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 193 598 moveto +194 587 lineto +187 595 lineto +closepath +stroke +end grestore + +% paramodulation +gsave 10 dict begin +132 738 90 25 ellipse_path +stroke +gsave 10 dict begin +56 730 moveto +(paramodulation) +[12 10.56 7.92 10.56 18.72 12 12 12 6.72 10.56 6.72 6.72 12 12] +xshow +end grestore +end grestore + +% paramodulation -> tactics +newpath 142 713 moveto +145 704 149 694 152 684 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 155 686 moveto +156 675 lineto +149 683 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 155 686 moveto +156 675 lineto +149 683 lineto +closepath +stroke +end grestore + +% cic +gsave 10 dict begin +427 298 28 25 ellipse_path +stroke +gsave 10 dict begin +413 290 moveto +(cic) +[10.56 6.72 10.56] +xshow +end grestore +end grestore + +% urimanager +gsave 10 dict begin +347 210 70 25 ellipse_path stroke gsave 10 dict begin -98 445 moveto -(cic_transformations) -[6.24 3.84 6.24 6.96 3.84 4.56 6.24 6.96 5.52 4.56 6.96 4.56 10.8 6.24 3.84 3.84 6.96 6.96 5.52] +291 202 moveto +(urimanager) +[12 7.92 6.72 18.72 10.56 12 10.56 12 10.56 7.92] xshow end grestore end grestore -% cic_transformations -> cic_notation -newpath 129 433 moveto -115 423 95 410 79 399 curveto +% cic -> urimanager +newpath 409 278 moveto +399 267 387 254 376 241 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 81 396 moveto -71 394 lineto -78 402 lineto +newpath 379 239 moveto +369 234 lineto +374 244 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 81 396 moveto -71 394 lineto -78 402 lineto +newpath 379 239 moveto +369 234 lineto +374 244 lineto closepath stroke end grestore -% cic_omdoc +% xml gsave 10 dict begin -158 378 44 18 ellipse_path +205 122 33 25 ellipse_path stroke gsave 10 dict begin -127 373 moveto -(cic_omdoc) -[6.24 3.84 6.24 6.96 6.96 10.8 6.96 6.96 6.24] +186 114 moveto +(xml) +[12 18.72 6.72] xshow end grestore end grestore -% cic_transformations -> cic_omdoc -newpath 155 432 moveto -156 424 156 415 156 406 curveto +% cic -> xml +newpath 435 273 moveto +441 248 446 209 427 184 curveto +405 156 307 137 249 128 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 159 406 moveto -157 396 lineto -153 406 lineto +newpath 249 125 moveto +239 126 lineto +248 131 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 159 406 moveto -157 396 lineto -153 406 lineto +newpath 249 125 moveto +239 126 lineto +248 131 lineto closepath stroke end grestore -% cic_omdoc -> cic_proof_checking -newpath 177 362 moveto -188 352 202 340 214 330 curveto +% cic_proof_checking -> cic +newpath 470 361 moveto +463 351 455 339 448 328 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 217 332 moveto -222 323 lineto -212 327 lineto +newpath 451 326 moveto +442 320 lineto +445 330 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 217 332 moveto -222 323 lineto -212 327 lineto +newpath 451 326 moveto +442 320 lineto +445 330 lineto closepath stroke end grestore % getter gsave 10 dict begin -292 234 29 18 ellipse_path +318 298 42 25 ellipse_path stroke gsave 10 dict begin -276 229 moveto +290 290 moveto (getter) -[6.96 6.24 3.84 3.84 6.24 4.56] +[12 10.56 6.72 6.72 10.56 7.92] xshow end grestore end grestore % cic_proof_checking -> getter -newpath 254 288 moveto -260 280 267 269 274 259 curveto +newpath 442 363 moveto +416 350 384 333 359 320 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 277 261 moveto -280 251 lineto -271 257 lineto +newpath 360 317 moveto +350 315 lineto +357 323 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 277 261 moveto -280 251 lineto -271 257 lineto +newpath 360 317 moveto +350 315 lineto +357 323 lineto closepath stroke end grestore -% cic +% getter -> urimanager +newpath 326 273 moveto +329 264 332 254 336 245 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 339 246 moveto +339 235 lineto +333 244 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 339 246 moveto +339 235 lineto +333 244 lineto +closepath +stroke +end grestore + +% registry gsave 10 dict begin -208 234 27 18 ellipse_path +205 210 52 25 ellipse_path stroke gsave 10 dict begin -199 229 moveto -(cic) -[6.24 3.84 6.24] +167 202 moveto +(registry) +[7.92 10.56 12 6.72 9.36 6.72 7.92 12] xshow end grestore end grestore -% cic_proof_checking -> cic -newpath 233 288 moveto -229 280 225 270 220 261 curveto +% getter -> registry +newpath 292 278 moveto +277 266 258 251 241 238 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 243 235 moveto +233 232 lineto +239 241 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 243 235 moveto +233 232 lineto +239 241 lineto +closepath +stroke +end grestore + +% metadata +gsave 10 dict begin +205 386 58 25 ellipse_path +stroke +gsave 10 dict begin +161 378 moveto +(metadata) +[18.72 10.56 6.72 10.56 12 10.56 6.72 10.56] +xshow +end grestore +end grestore + +% metadata -> cic +newpath 249 369 moveto +257 366 265 363 273 360 curveto +316 343 327 341 370 324 curveto +377 321 384 318 391 314 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 223 260 moveto -216 252 lineto -217 263 lineto +newpath 393 317 moveto +401 310 lineto +390 310 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 223 260 moveto -216 252 lineto -217 263 lineto +newpath 393 317 moveto +401 310 lineto +390 310 lineto closepath stroke end grestore -% metadata -> cic_proof_checking -newpath 360 365 moveto -339 354 308 339 283 327 curveto +% metadata -> getter +newpath 234 364 moveto +249 352 268 337 283 324 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 284 324 moveto -274 322 lineto -281 330 lineto +newpath 285 327 moveto +291 318 lineto +281 321 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 284 324 moveto -274 322 lineto -281 330 lineto +newpath 285 327 moveto +291 318 lineto +281 321 lineto closepath stroke end grestore % hmysql gsave 10 dict begin -386 234 34 18 ellipse_path +205 298 50 25 ellipse_path stroke gsave 10 dict begin -364 229 moveto +169 290 moveto (hmysql) -[6.96 10.8 6.96 5.52 6.96 3.84] +[12 18.72 12 9.36 12 6.72] xshow end grestore end grestore % metadata -> hmysql -newpath 386 360 moveto -386 335 386 291 386 262 curveto +newpath 205 360 moveto +205 352 205 343 205 334 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 390 262 moveto -386 252 lineto -383 262 lineto +newpath 209 334 moveto +205 324 lineto +202 334 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 390 262 moveto -386 252 lineto -383 262 lineto +newpath 209 334 moveto +205 324 lineto +202 334 lineto closepath stroke end grestore -% cic_unification -> cic_proof_checking -newpath 267 360 moveto -263 352 259 342 254 333 curveto +% whelp -> metadata +newpath 205 536 moveto +205 506 205 456 205 422 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 257 332 moveto -250 324 lineto -251 335 lineto +newpath 209 422 moveto +205 412 lineto +202 422 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 257 332 moveto -250 324 lineto -251 335 lineto +newpath 209 422 moveto +205 412 lineto +202 422 lineto closepath stroke end grestore -% registry +% extlib gsave 10 dict begin -386 162 35 18 ellipse_path +205 34 42 25 ellipse_path stroke gsave 10 dict begin -364 157 moveto -(registry) -[4.56 6.24 6.96 3.84 5.52 3.84 4.56 6.96] +177 26 moveto +(extlib) +[10.56 12 6.72 6.72 6.72 12] xshow end grestore end grestore +% hgdome +gsave 10 dict begin +79 210 54 25 ellipse_path +stroke +gsave 10 dict begin +39 202 moveto +(hgdome) +[12 12 12 12 18.72 10.56] +xshow +end grestore +end grestore + +% hgdome -> xml +newpath 110 189 moveto +128 176 152 159 172 146 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 174 149 moveto +180 140 lineto +170 143 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 174 149 moveto +180 140 lineto +170 143 lineto +closepath +stroke +end grestore + % hmysql -> registry -newpath 386 216 moveto -386 208 386 199 386 190 curveto +newpath 205 272 moveto +205 264 205 255 205 246 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 390 190 moveto -386 180 lineto -383 190 lineto +newpath 209 246 moveto +205 236 lineto +202 246 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 390 190 moveto -386 180 lineto -383 190 lineto +newpath 209 246 moveto +205 236 lineto +202 246 lineto closepath stroke end grestore -% urimanager +% registry -> xml +newpath 205 184 moveto +205 176 205 167 205 158 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 209 158 moveto +205 148 lineto +202 158 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 209 158 moveto +205 148 lineto +202 158 lineto +closepath +stroke +end grestore + +% xml -> extlib +newpath 205 96 moveto +205 88 205 79 205 70 curveto +stroke gsave 10 dict begin -208 162 45 18 ellipse_path +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 209 70 moveto +205 60 lineto +202 70 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 209 70 moveto +205 60 lineto +202 70 lineto +closepath stroke +end grestore + +% DrawGraph gsave 10 dict begin -175 157 moveto -(urimanager) -[6.96 4.56 3.84 10.8 6.24 6.96 6.24 6.96 6.24 4.56] +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 128 404 moveto +0 404 lineto +0 368 lineto +128 368 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 128 404 moveto +0 404 lineto +0 368 lineto +128 368 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +7 378 moveto +(DrawGraph) +[17.28 7.92 10.56 17.28 17.28 7.92 10.56 12 12] xshow end grestore end grestore -% getter -> urimanager -newpath 275 219 moveto -263 209 248 196 235 185 curveto +% DrawGraph -> getter +newpath 113 368 moveto +121 365 129 362 137 360 curveto +193 342 209 345 265 324 curveto +269 322 272 321 276 319 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 237 182 moveto -227 178 lineto -232 187 lineto +newpath 277 322 moveto +285 315 lineto +274 316 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 237 182 moveto -227 178 lineto -232 187 lineto +newpath 277 322 moveto +285 315 lineto +274 316 lineto closepath stroke end grestore -% getter -> registry -newpath 311 220 moveto -325 210 343 195 359 183 curveto +% Getter +gsave 10 dict begin +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 358 404 moveto +282 404 lineto +282 368 lineto +358 368 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 358 404 moveto +282 404 lineto +282 368 lineto +358 368 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +290 378 moveto +(Getter) +[17.28 10.56 6.72 6.72 10.56 7.92] +xshow +end grestore +end grestore + +% Getter -> getter +newpath 320 368 moveto +320 358 319 346 319 334 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 361 186 moveto -367 177 lineto -357 180 lineto +newpath 323 334 moveto +319 324 lineto +316 334 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 361 186 moveto -367 177 lineto -357 180 lineto +newpath 323 334 moveto +319 324 lineto +316 334 lineto closepath stroke end grestore -% logger +% Matita gsave 10 dict begin -302 162 31 18 ellipse_path +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 319 756 moveto +241 756 lineto +241 720 lineto +319 720 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 319 756 moveto +241 756 lineto +241 720 lineto +319 720 lineto +closepath stroke gsave 10 dict begin -284 157 moveto -(logger) -[3.84 6.96 6.96 6.96 6.24 4.56] +0.000 0.000 0.000 nodecolor +248 730 moveto +(Matita) +[21.36 10.56 6.72 6.72 6.72 10.56] xshow end grestore end grestore -% getter -> logger -newpath 295 216 moveto -296 208 297 199 298 190 curveto +% Matita -> cic_disambiguation +newpath 300 720 moveto +313 709 328 695 342 682 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 301 190 moveto -299 180 lineto -295 190 lineto +newpath 345 684 moveto +350 675 lineto +340 679 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 301 190 moveto -299 180 lineto -295 190 lineto +newpath 345 684 moveto +350 675 lineto +340 679 lineto closepath stroke end grestore -% xml +% Matita -> tactics +newpath 256 720 moveto +240 708 219 691 200 677 curveto +stroke gsave 10 dict begin -260 90 27 18 ellipse_path +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 202 674 moveto +192 671 lineto +198 680 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 202 674 moveto +192 671 lineto +198 680 lineto +closepath stroke +end grestore + +% ProofChecker gsave 10 dict begin -248 85 moveto -(xml) -[6.96 10.8 3.84] +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 710 492 moveto +560 492 lineto +560 456 lineto +710 456 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 710 492 moveto +560 492 lineto +560 456 lineto +710 456 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +568 466 moveto +(ProofChecker) +[13.44 7.92 12 12 7.92 16.08 12 10.56 10.56 12 10.56 7.92] xshow end grestore end grestore -% cic -> xml -newpath 189 221 moveto -176 212 161 197 154 180 curveto -147 165 145 157 154 144 curveto -169 119 199 105 224 98 curveto +% ProofChecker -> cic_proof_checking +newpath 605 456 moveto +585 445 559 428 536 415 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 225 101 moveto -234 95 lineto -223 95 lineto +newpath 537 412 moveto +527 410 lineto +534 418 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 225 101 moveto -234 95 lineto -223 95 lineto +newpath 537 412 moveto +527 410 lineto +534 418 lineto closepath stroke end grestore -% cic -> urimanager -newpath 208 216 moveto -208 208 208 199 208 190 curveto +% Uwobo +gsave 10 dict begin +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 579 756 moveto +493 756 lineto +493 720 lineto +579 720 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 579 756 moveto +493 756 lineto +493 720 lineto +579 720 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +500 730 moveto +(Uwobo) +[17.28 17.28 12 12 12] +xshow +end grestore +end grestore + +% Uwobo -> acic_content +newpath 536 720 moveto +536 692 536 635 536 598 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 212 190 moveto -208 180 lineto -205 190 lineto +newpath 540 598 moveto +536 588 lineto +533 598 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 212 190 moveto -208 180 lineto -205 190 lineto +newpath 540 598 moveto +536 588 lineto +533 598 lineto closepath stroke end grestore -% extlib +% Uwobo -> content_pres +newpath 558 720 moveto +572 709 590 694 606 681 curveto +stroke gsave 10 dict begin -260 18 29 18 ellipse_path +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 609 683 moveto +614 674 lineto +604 678 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 609 683 moveto +614 674 lineto +604 678 lineto +closepath stroke +end grestore + +% Whelp gsave 10 dict begin -244 13 moveto -(extlib) -[6.24 6.96 3.84 3.84 3.84 6.96] +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 417 756 moveto +337 756 lineto +337 720 lineto +417 720 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 417 756 moveto +337 756 lineto +337 720 lineto +417 720 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +344 730 moveto +(Whelp) +[22.56 12 10.56 6.72 12] xshow end grestore end grestore -% xml -> extlib -newpath 260 72 moveto -260 64 260 55 260 46 curveto +% Whelp -> cic_disambiguation +newpath 377 720 moveto +377 710 377 698 377 686 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 264 46 moveto -260 36 lineto -257 46 lineto +newpath 381 686 moveto +377 676 lineto +374 686 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 264 46 moveto -260 36 lineto -257 46 lineto +newpath 381 686 moveto +377 676 lineto +374 686 lineto closepath stroke end grestore -% registry -> xml -newpath 362 148 moveto -342 137 312 120 290 107 curveto +% Whelp -> whelp +newpath 343 720 moveto +338 717 333 714 328 712 curveto +296 695 282 701 258 676 curveto +237 653 223 621 214 597 curveto stroke gsave 10 dict begin solid 1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 291 104 moveto -281 102 lineto -288 110 lineto +newpath 217 596 moveto +211 587 lineto +211 598 lineto closepath fill 0.000 0.000 0.000 edgecolor -newpath 291 104 moveto -281 102 lineto -288 110 lineto +newpath 217 596 moveto +211 587 lineto +211 598 lineto closepath stroke end grestore diff --git a/helm/papers/matita/librariesCluster.ps b/helm/papers/matita/librariesCluster.ps new file mode 100644 index 000000000..03d3665d8 --- /dev/null +++ b/helm/papers/matita/librariesCluster.ps @@ -0,0 +1,1513 @@ +%!PS-Adobe-2.0 +%%Creator: dot version 2.2.1 (Fri Sep 30 13:22:44 UTC 2005) +%%For: (zacchiro) Stefano Zacchiroli,,, +%%Title: G +%%Pages: (atend) +%%BoundingBox: 35 35 1332 937 +%%EndComments +save +%%BeginProlog +/DotDict 200 dict def +DotDict begin + +/setupLatin1 { +mark +/EncodingVector 256 array def + EncodingVector 0 + +ISOLatin1Encoding 0 255 getinterval putinterval + +EncodingVector + dup 306 /AE + dup 301 /Aacute + dup 302 /Acircumflex + dup 304 /Adieresis + dup 300 /Agrave + dup 305 /Aring + dup 303 /Atilde + dup 307 /Ccedilla + dup 311 /Eacute + dup 312 /Ecircumflex + dup 313 /Edieresis + dup 310 /Egrave + dup 315 /Iacute + dup 316 /Icircumflex + dup 317 /Idieresis + dup 314 /Igrave + dup 334 /Udieresis + dup 335 /Yacute + dup 376 /thorn + dup 337 /germandbls + dup 341 /aacute + dup 342 /acircumflex + dup 344 /adieresis + dup 346 /ae + dup 340 /agrave + dup 345 /aring + dup 347 /ccedilla + dup 351 /eacute + dup 352 /ecircumflex + dup 353 /edieresis + dup 350 /egrave + dup 355 /iacute + dup 356 /icircumflex + dup 357 /idieresis + dup 354 /igrave + dup 360 /dcroat + dup 361 /ntilde + dup 363 /oacute + dup 364 /ocircumflex + dup 366 /odieresis + dup 362 /ograve + dup 365 /otilde + dup 370 /oslash + dup 372 /uacute + dup 373 /ucircumflex + dup 374 /udieresis + dup 371 /ugrave + dup 375 /yacute + dup 377 /ydieresis + +% Set up ISO Latin 1 character encoding +/starnetISO { + dup dup findfont dup length dict begin + { 1 index /FID ne { def }{ pop pop } ifelse + } forall + /Encoding EncodingVector def + currentdict end definefont +} def +/Times-Roman starnetISO def +/Times-Italic starnetISO def +/Times-Bold starnetISO def +/Times-BoldItalic starnetISO def +/Helvetica starnetISO def +/Helvetica-Oblique starnetISO def +/Helvetica-Bold starnetISO def +/Helvetica-BoldOblique starnetISO def +/Courier starnetISO def +/Courier-Oblique starnetISO def +/Courier-Bold starnetISO def +/Courier-BoldOblique starnetISO def +cleartomark +} bind def + +%%BeginResource: procset graphviz 0 0 +/coord-font-family /Times-Roman def +/default-font-family /Times-Roman def +/coordfont coord-font-family findfont 8 scalefont def + +/InvScaleFactor 1.0 def +/set_scale { + dup 1 exch div /InvScaleFactor exch def + dup scale +} bind def + +% styles +/solid { [] 0 setdash } bind def +/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def +/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def +/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def +/bold { 2 setlinewidth } bind def +/filled { } bind def +/unfilled { } bind def +/rounded { } bind def +/diagonals { } bind def + +% hooks for setting color +/nodecolor { sethsbcolor } bind def +/edgecolor { sethsbcolor } bind def +/graphcolor { sethsbcolor } bind def +/nopcolor {pop pop pop} bind def + +/beginpage { % i j npages + /npages exch def + /j exch def + /i exch def + /str 10 string def + npages 1 gt { + gsave + coordfont setfont + 0 0 moveto + (\() show i str cvs show (,) show j str cvs show (\)) show + grestore + } if +} bind def + +/set_font { + findfont exch + scalefont setfont +} def + +% draw aligned label in bounding box aligned to current point +/alignedtext { % width adj text + /text exch def + /adj exch def + /width exch def + gsave + width 0 gt { + text stringwidth pop adj mul 0 rmoveto + } if + [] 0 setdash + text show + grestore +} def + +/boxprim { % xcorner ycorner xsize ysize + 4 2 roll + moveto + 2 copy + exch 0 rlineto + 0 exch rlineto + pop neg 0 rlineto + closepath +} bind def + +/ellipse_path { + /ry exch def + /rx exch def + /y exch def + /x exch def + matrix currentmatrix + newpath + x y translate + rx ry scale + 0 0 1 0 360 arc + setmatrix +} bind def + +/endpage { showpage } bind def +/showpage { } def + +/layercolorseq + [ % layer color sequence - darkest to lightest + [0 0 0] + [.2 .8 .8] + [.4 .8 .8] + [.6 .8 .8] + [.8 .8 .8] + ] +def + +/layerlen layercolorseq length def + +/setlayer {/maxlayer exch def /curlayer exch def + layercolorseq curlayer 1 sub layerlen mod get + aload pop sethsbcolor + /nodecolor {nopcolor} def + /edgecolor {nopcolor} def + /graphcolor {nopcolor} def +} bind def + +/onlayer { curlayer ne {invis} if } def + +/onlayers { + /myupper exch def + /mylower exch def + curlayer mylower lt + curlayer myupper gt + or + {invis} if +} def + +/curlayer 0 def + +%%EndResource +%%EndProlog +%%BeginSetup +14 default-font-family set_font +1 setmiterlimit +% /arrowlength 10 def +% /arrowwidth 5 def + +% make sure pdfmark is harmless for PS-interpreters other than Distiller +/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse +% make '<<' and '>>' safe on PS Level 1 devices +/languagelevel where {pop languagelevel}{1} ifelse +2 lt { + userdict (<<) cvn ([) cvn load put + userdict (>>) cvn ([) cvn load put +} if + +%%EndSetup +%%Page: 1 1 +%%PageBoundingBox: 36 36 1332 937 +%%PageOrientation: Portrait +gsave +35 35 1297 902 boxprim clip newpath +36 36 translate +0 0 1 beginpage +0 0 translate 0 rotate +0.000 0.000 0.000 graphcolor +24.00 /Times-Roman set_font +% cluster_presentation +gsave 10 dict begin +filled +0.000 0.000 1.000 sethsbcolor +0.000 0.000 0.929 sethsbcolor +newpath 772 488 moveto +1201 488 lineto +1201 856 lineto +772 856 lineto +closepath +fill +0.000 0.000 1.000 sethsbcolor +newpath 772 488 moveto +1201 488 lineto +1201 856 lineto +772 856 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 sethsbcolor +780 498 moveto +(Terms at the content and presentation level) +[14.64 10.56 7.92 18.72 9.36 6 10.56 6.72 6 6.72 12 10.56 6 10.56 12 12 6.72 10.56 12 6.72 6 10.56 12 12 6 12 7.92 10.56 9.36 10.56 12 6.72 10.56 6.72 6.72 12 12 6 6.72 10.56 12 10.56 6.72] +xshow +end grestore +end grestore +% cluster_partially +gsave 10 dict begin +filled +0.000 0.000 1.000 sethsbcolor +0.000 0.000 0.929 sethsbcolor +newpath 330 612 moveto +580 612 lineto +580 892 lineto +330 892 lineto +closepath +fill +0.000 0.000 1.000 sethsbcolor +newpath 330 612 moveto +580 612 lineto +580 892 lineto +330 892 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 sethsbcolor +338 866 moveto +(Partially specified terms) +[13.44 10.56 7.92 6.72 6.72 10.56 6.72 6.72 12 6 9.36 12 10.56 10.56 6.72 7.92 6.72 10.56 12 6 6.72 10.56 7.92 18.72 9.36] +xshow +end grestore +end grestore +% cluster_fully +gsave 10 dict begin +filled +0.000 0.000 1.000 sethsbcolor +0.000 0.000 0.929 sethsbcolor +newpath 232 208 moveto +606 208 lineto +606 592 lineto +232 592 lineto +closepath +fill +0.000 0.000 1.000 sethsbcolor +newpath 232 208 moveto +606 208 lineto +606 592 lineto +232 592 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 sethsbcolor +239 218 moveto +(Fully specified terms) +[13.44 12 6.72 6.72 12 6 9.36 12 10.56 10.56 6.72 7.92 6.72 10.56 12 6 6.72 10.56 7.92 18.72 9.36] +xshow +end grestore +end grestore +% cluster_utilities +gsave 10 dict begin +filled +0.000 0.000 1.000 sethsbcolor +0.000 0.000 0.929 sethsbcolor +newpath 614 16 moveto +902 16 lineto +902 400 lineto +614 400 lineto +closepath +fill +0.000 0.000 1.000 sethsbcolor +newpath 614 16 moveto +902 16 lineto +902 400 lineto +614 400 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 sethsbcolor +816 26 moveto +(Utilities) +[17.28 6.72 6.72 6.72 6.72 6.72 6.72 10.56 9.36] +xshow +end grestore +end grestore + +% acic_content +gsave 10 dict begin +915 646 75 25 ellipse_path +stroke +gsave 10 dict begin +854 638 moveto +(acic_content) +[10.56 10.56 6.72 10.56 12 10.56 12 12 6.72 10.56 12 6.72] +xshow +end grestore +end grestore + +% cic_acic +gsave 10 dict begin +876 558 54 25 ellipse_path +stroke +gsave 10 dict begin +836 550 moveto +(cic_acic) +[10.56 6.72 10.56 12 10.56 10.56 6.72 10.56] +xshow +end grestore +end grestore + +% acic_content -> cic_acic +newpath 904 621 moveto +900 612 895 602 891 592 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 894 591 moveto +887 583 lineto +888 594 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 894 591 moveto +887 583 lineto +888 594 lineto +closepath +stroke +end grestore + +% cic_proof_checking +gsave 10 dict begin +487 454 110 25 ellipse_path +stroke +gsave 10 dict begin +391 446 moveto +(cic_proof_checking) +[10.56 6.72 10.56 12 12 7.92 12 12 7.92 12 10.56 12 10.56 10.56 12 6.72 12 12] +xshow +end grestore +end grestore + +% cic_acic -> cic_proof_checking +newpath 863 533 moveto +854 517 840 498 821 488 curveto +803 477 693 468 604 462 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 604 459 moveto +594 461 lineto +604 465 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 604 459 moveto +594 461 lineto +604 465 lineto +closepath +stroke +end grestore + +% cic_disambiguation +gsave 10 dict begin +890 734 109 25 ellipse_path +stroke +gsave 10 dict begin +795 726 moveto +(cic_disambiguation) +[10.56 6.72 10.56 12 12 6.72 9.36 10.56 18.72 12 6.72 12 12 10.56 6.72 6.72 12 12] +xshow +end grestore +end grestore + +% cic_disambiguation -> acic_content +newpath 897 709 moveto +900 700 903 691 905 682 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 908 683 moveto +908 672 lineto +902 681 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 908 683 moveto +908 672 lineto +902 681 lineto +closepath +stroke +end grestore + +% cic_unification +gsave 10 dict begin +485 646 86 25 ellipse_path +stroke +gsave 10 dict begin +413 638 moveto +(cic_unification) +[10.56 6.72 10.56 12 12 12 6.72 7.92 6.72 10.56 10.56 6.72 6.72 12 12] +xshow +end grestore +end grestore + +% cic_disambiguation -> cic_unification +newpath 810 717 moveto +738 702 636 679 565 663 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 565 660 moveto +555 661 lineto +564 666 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 565 660 moveto +555 661 lineto +564 666 lineto +closepath +stroke +end grestore + +% whelp +gsave 10 dict begin +336 558 44 25 ellipse_path +stroke +gsave 10 dict begin +306 550 moveto +(whelp) +[17.28 12 10.56 6.72 12] +xshow +end grestore +end grestore + +% cic_disambiguation -> whelp +newpath 845 711 moveto +786 682 680 634 584 612 curveto +535 600 397 620 354 592 curveto +354 592 353 592 353 591 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 356 589 moveto +347 583 lineto +350 593 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 356 589 moveto +347 583 lineto +350 593 lineto +closepath +stroke +end grestore + +% content_pres +gsave 10 dict begin +1095 734 76 25 ellipse_path +stroke +gsave 10 dict begin +1033 726 moveto +(content_pres) +[10.56 12 12 6.72 10.56 12 6.72 12 12 7.92 10.56 9.36] +xshow +end grestore +end grestore + +% content_pres -> acic_content +newpath 1051 713 moveto +1026 700 994 685 967 672 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 968 669 moveto +958 667 lineto +965 675 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 968 669 moveto +958 667 lineto +965 675 lineto +closepath +stroke +end grestore + +% utf8_macros +gsave 10 dict begin +818 366 75 25 ellipse_path +stroke +gsave 10 dict begin +757 358 moveto +(utf8_macros) +[12 6.72 7.92 12 12 18.72 10.56 10.56 7.92 12 9.36] +xshow +end grestore +end grestore + +% content_pres -> utf8_macros +newpath 1082 709 moveto +1057 662 1000 562 940 488 curveto +914 454 879 421 854 397 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 856 394 moveto +846 390 lineto +851 399 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 856 394 moveto +846 390 lineto +851 399 lineto +closepath +stroke +end grestore + +% grafite +gsave 10 dict begin +1095 822 46 25 ellipse_path +stroke +gsave 10 dict begin +1063 814 moveto +(grafite) +[12 7.92 10.56 7.92 6.72 6.72 10.56] +xshow +end grestore +end grestore + +% grafite -> content_pres +newpath 1095 796 moveto +1095 788 1095 779 1095 770 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1099 770 moveto +1095 760 lineto +1092 770 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1099 770 moveto +1095 760 lineto +1092 770 lineto +closepath +stroke +end grestore + +% cic_unification -> cic_proof_checking +newpath 485 620 moveto +486 586 486 528 487 490 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 491 490 moveto +487 480 lineto +484 490 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 491 490 moveto +487 480 lineto +484 490 lineto +closepath +stroke +end grestore + +% tactics +gsave 10 dict begin +482 734 45 25 ellipse_path +stroke +gsave 10 dict begin +451 726 moveto +(tactics) +[6.72 10.56 10.56 6.72 6.72 10.56 9.36] +xshow +end grestore +end grestore + +% tactics -> cic_unification +newpath 483 708 moveto +483 700 484 691 484 682 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 488 682 moveto +484 672 lineto +481 682 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 488 682 moveto +484 672 lineto +481 682 lineto +closepath +stroke +end grestore + +% tactics -> whelp +newpath 451 715 moveto +428 701 399 682 389 672 curveto +370 648 356 617 347 593 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 350 591 moveto +343 583 lineto +343 594 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 350 591 moveto +343 583 lineto +343 594 lineto +closepath +stroke +end grestore + +% paramodulation +gsave 10 dict begin +479 822 90 25 ellipse_path +stroke +gsave 10 dict begin +403 814 moveto +(paramodulation) +[12 10.56 7.92 10.56 18.72 12 12 12 6.72 10.56 6.72 6.72 12 12] +xshow +end grestore +end grestore + +% paramodulation -> tactics +newpath 480 796 moveto +480 788 481 779 481 770 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 485 770 moveto +481 760 lineto +478 770 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 485 770 moveto +481 760 lineto +478 770 lineto +closepath +stroke +end grestore + +% cic +gsave 10 dict begin +462 366 28 25 ellipse_path +stroke +gsave 10 dict begin +448 358 moveto +(cic) +[10.56 6.72 10.56] +xshow +end grestore +end grestore + +% urimanager +gsave 10 dict begin +494 278 70 25 ellipse_path +stroke +gsave 10 dict begin +438 270 moveto +(urimanager) +[12 7.92 6.72 18.72 10.56 12 10.56 12 10.56 7.92] +xshow +end grestore +end grestore + +% cic -> urimanager +newpath 471 341 moveto +474 332 478 322 481 312 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 484 314 moveto +485 303 lineto +478 311 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 484 314 moveto +485 303 lineto +478 311 lineto +closepath +stroke +end grestore + +% xml +gsave 10 dict begin +675 174 33 25 ellipse_path +stroke +gsave 10 dict begin +656 166 moveto +(xml) +[12 18.72 6.72] +xshow +end grestore +end grestore + +% cic -> xml +newpath 442 347 moveto +432 336 420 320 414 304 curveto +401 263 386 240 414 208 curveto +428 192 560 181 631 177 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 631 180 moveto +641 176 lineto +631 174 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 631 180 moveto +641 176 lineto +631 174 lineto +closepath +stroke +end grestore + +% cic_proof_checking -> cic +newpath 480 429 moveto +477 420 474 410 472 401 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 475 400 moveto +469 391 lineto +469 402 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 475 400 moveto +469 391 lineto +469 402 lineto +closepath +stroke +end grestore + +% getter +gsave 10 dict begin +323 366 42 25 ellipse_path +stroke +gsave 10 dict begin +295 358 moveto +(getter) +[12 10.56 6.72 6.72 10.56 7.92] +xshow +end grestore +end grestore + +% cic_proof_checking -> getter +newpath 443 430 moveto +418 417 388 400 364 388 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 365 385 moveto +355 383 lineto +362 391 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 365 385 moveto +355 383 lineto +362 391 lineto +closepath +stroke +end grestore + +% getter -> urimanager +newpath 356 349 moveto +380 336 416 318 444 304 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 446 307 moveto +453 299 lineto +443 301 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 446 307 moveto +453 299 lineto +443 301 lineto +closepath +stroke +end grestore + +% registry +gsave 10 dict begin +675 278 52 25 ellipse_path +stroke +gsave 10 dict begin +637 270 moveto +(registry) +[7.92 10.56 12 6.72 9.36 6.72 7.92 12] +xshow +end grestore +end grestore + +% getter -> registry +newpath 362 355 moveto +381 350 404 345 424 340 curveto +507 321 530 327 610 304 curveto +615 302 621 300 626 298 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 627 301 moveto +636 295 lineto +625 295 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 627 301 moveto +636 295 lineto +625 295 lineto +closepath +stroke +end grestore + +% metadata +gsave 10 dict begin +299 454 58 25 ellipse_path +stroke +gsave 10 dict begin +255 446 moveto +(metadata) +[18.72 10.56 6.72 10.56 12 10.56 6.72 10.56] +xshow +end grestore +end grestore + +% metadata -> cic +newpath 336 434 moveto +364 419 401 399 428 385 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 430 388 moveto +437 380 lineto +427 382 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 430 388 moveto +437 380 lineto +427 382 lineto +closepath +stroke +end grestore + +% metadata -> getter +newpath 306 429 moveto +308 420 311 410 313 401 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 316 402 moveto +316 391 lineto +310 400 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 316 402 moveto +316 391 lineto +310 400 lineto +closepath +stroke +end grestore + +% hmysql +gsave 10 dict begin +673 366 50 25 ellipse_path +stroke +gsave 10 dict begin +637 358 moveto +(hmysql) +[12 18.72 12 9.36 12 6.72] +xshow +end grestore +end grestore + +% metadata -> hmysql +newpath 341 436 moveto +349 433 358 430 367 428 curveto +473 402 507 432 610 400 curveto +618 398 625 394 632 391 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 634 394 moveto +641 386 lineto +631 388 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 634 394 moveto +641 386 lineto +631 388 lineto +closepath +stroke +end grestore + +% whelp -> metadata +newpath 327 533 moveto +322 520 316 503 311 488 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 314 487 moveto +308 479 lineto +308 490 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 314 487 moveto +308 479 lineto +308 490 lineto +closepath +stroke +end grestore + +% extlib +gsave 10 dict begin +675 86 42 25 ellipse_path +stroke +gsave 10 dict begin +647 78 moveto +(extlib) +[10.56 12 6.72 6.72 6.72 12] +xshow +end grestore +end grestore + +% hgdome +gsave 10 dict begin +801 278 54 25 ellipse_path +stroke +gsave 10 dict begin +761 270 moveto +(hgdome) +[12 12 12 12 18.72 10.56] +xshow +end grestore +end grestore + +% hgdome -> xml +newpath 783 254 moveto +771 239 754 221 737 208 curveto +730 202 721 197 713 192 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 714 189 moveto +704 187 lineto +711 195 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 714 189 moveto +704 187 lineto +711 195 lineto +closepath +stroke +end grestore + +% hmysql -> registry +newpath 674 340 moveto +674 332 674 323 674 314 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 678 314 moveto +674 304 lineto +671 314 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 678 314 moveto +674 304 lineto +671 314 lineto +closepath +stroke +end grestore + +% registry -> xml +newpath 675 252 moveto +675 239 675 224 675 210 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 679 210 moveto +675 200 lineto +672 210 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 679 210 moveto +675 200 lineto +672 210 lineto +closepath +stroke +end grestore + +% xml -> extlib +newpath 675 148 moveto +675 140 675 131 675 122 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 679 122 moveto +675 112 lineto +672 122 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 679 122 moveto +675 112 lineto +672 122 lineto +closepath +stroke +end grestore + +% DrawGraph +gsave 10 dict begin +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 128 472 moveto +0 472 lineto +0 436 lineto +128 436 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 128 472 moveto +0 472 lineto +0 436 lineto +128 436 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +7 446 moveto +(DrawGraph) +[17.28 7.92 10.56 17.28 17.28 7.92 10.56 12 12] +xshow +end grestore +end grestore + +% DrawGraph -> getter +newpath 114 436 moveto +122 433 130 430 137 428 curveto +184 411 237 394 275 381 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 276 384 moveto +285 378 lineto +274 378 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 276 384 moveto +285 378 lineto +274 378 lineto +closepath +stroke +end grestore + +% Getter +gsave 10 dict begin +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 222 472 moveto +146 472 lineto +146 436 lineto +222 436 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 222 472 moveto +146 472 lineto +146 436 lineto +222 436 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +154 446 moveto +(Getter) +[17.28 10.56 6.72 6.72 10.56 7.92] +xshow +end grestore +end grestore + +% Getter -> getter +newpath 212 436 moveto +233 423 262 405 285 390 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 286 393 moveto +293 385 lineto +283 387 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 286 393 moveto +293 385 lineto +283 387 lineto +closepath +stroke +end grestore + +% Matita +gsave 10 dict begin +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 764 840 moveto +686 840 lineto +686 804 lineto +764 804 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 764 840 moveto +686 840 lineto +686 804 lineto +764 804 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +693 814 moveto +(Matita) +[21.36 10.56 6.72 6.72 6.72 10.56] +xshow +end grestore +end grestore + +% Matita -> cic_disambiguation +newpath 754 804 moveto +759 801 764 798 768 796 curveto +789 784 813 772 833 762 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 835 765 moveto +842 757 lineto +832 759 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 835 765 moveto +842 757 lineto +832 759 lineto +closepath +stroke +end grestore + +% Matita -> tactics +newpath 694 804 moveto +689 801 683 798 677 796 curveto +630 776 574 759 534 748 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 535 745 moveto +524 745 lineto +533 751 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 535 745 moveto +524 745 lineto +533 751 lineto +closepath +stroke +end grestore + +% ProofChecker +gsave 10 dict begin +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 764 576 moveto +614 576 lineto +614 540 lineto +764 540 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 764 576 moveto +614 576 lineto +614 540 lineto +764 540 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +622 550 moveto +(ProofChecker) +[13.44 7.92 12 12 7.92 16.08 12 10.56 10.56 12 10.56 7.92] +xshow +end grestore +end grestore + +% ProofChecker -> cic_proof_checking +newpath 673 540 moveto +659 524 635 501 610 488 curveto +601 483 590 478 580 474 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 581 471 moveto +570 471 lineto +579 477 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 581 471 moveto +570 471 lineto +579 477 lineto +closepath +stroke +end grestore + +% Uwobo +gsave 10 dict begin +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 1295 840 moveto +1209 840 lineto +1209 804 lineto +1295 804 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 1295 840 moveto +1209 840 lineto +1209 804 lineto +1295 804 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +1216 814 moveto +(Uwobo) +[17.28 17.28 12 12 12] +xshow +end grestore +end grestore + +% Uwobo -> acic_content +newpath 1246 804 moveto +1235 778 1214 732 1181 708 curveto +1111 655 1074 662 999 653 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 999 650 moveto +989 652 lineto +999 656 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 999 650 moveto +989 652 lineto +999 656 lineto +closepath +stroke +end grestore + +% Uwobo -> content_pres +newpath 1221 804 moveto +1216 801 1210 798 1205 796 curveto +1165 778 1143 791 1113 767 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1115 764 moveto +1105 760 lineto +1110 769 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1115 764 moveto +1105 760 lineto +1110 769 lineto +closepath +stroke +end grestore + +% Whelp +gsave 10 dict begin +filled +0.584 0.220 0.933 nodecolor +0.584 0.220 0.933 nodecolor +newpath 668 840 moveto +588 840 lineto +588 804 lineto +668 804 lineto +closepath +fill +0.584 0.220 0.933 nodecolor +newpath 668 840 moveto +588 840 lineto +588 804 lineto +668 804 lineto +closepath +stroke +gsave 10 dict begin +0.000 0.000 0.000 nodecolor +595 814 moveto +(Whelp) +[22.56 12 10.56 6.72 12] +xshow +end grestore +end grestore + +% Whelp -> cic_disambiguation +newpath 660 804 moveto +666 801 671 798 677 796 curveto +718 779 764 765 803 755 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 804 758 moveto +813 752 lineto +802 752 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 804 758 moveto +813 752 lineto +802 752 lineto +closepath +stroke +end grestore + +% Whelp -> whelp +newpath 602 804 moveto +596 801 590 798 584 796 curveto +530 776 365 803 326 760 curveto +286 714 305 637 321 592 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 324 594 moveto +325 583 lineto +318 591 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 324 594 moveto +325 583 lineto +318 591 lineto +closepath +stroke +end grestore +endpage +showpage +grestore +%%PageTrailer +%%EndPage: 1 +%%Trailer +%%Pages: 1 +end +restore +%%EOF diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 80d2a04d5..8708e4458 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -116,7 +116,7 @@ Digital Libraries} \begin{figure}[t] \begin{center} - \includegraphics[width=0.9\textwidth]{libraries} + \includegraphics[width=0.9\textwidth]{librariesCluster.ps} \caption{\MATITA{} libraries} \end{center} \label{fig:libraries} -- 2.39.2