diff options
-rw-r--r-- | doc/kernel.dep.ps | 65 | ||||
-rw-r--r-- | doc/parsing.dep.ps | 310 | ||||
-rw-r--r-- | doc/pretyping.dep.ps | 91 |
3 files changed, 251 insertions, 215 deletions
diff --git a/doc/kernel.dep.ps b/doc/kernel.dep.ps index 3604e5ea6..1dcc8f873 100644 --- a/doc/kernel.dep.ps +++ b/doc/kernel.dep.ps @@ -3,7 +3,7 @@ %%For: Gros nain %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 576 91 +%%BoundingBox: 36 36 577 91 %%EndComments %%BeginProlog save @@ -139,41 +139,41 @@ def % /arrowwidth 5 def %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 576 91 +%%PageBoundingBox: 36 36 577 91 gsave -35 35 541 56 boxprim clip newpath +35 35 542 56 boxprim clip newpath 36 36 translate 0 0 1 beginpage -0.3994 set_scale +0.3982 set_scale 0 0 translate 0 rotate 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font % Univ gsave 10 dict begin -1229 74 27 18 ellipse_path +1231 101 27 18 ellipse_path stroke gsave 10 dict begin -1229 75 moveto (Univ) 28 14.00 -0.50 alignedtext +1231 102 moveto (Univ) 28 14.00 -0.50 alignedtext end grestore end grestore % Names gsave 10 dict begin -1322 74 29 18 ellipse_path +1326 101 29 18 ellipse_path stroke gsave 10 dict begin -1322 75 moveto (Names) 38 14.00 -0.50 alignedtext +1326 102 moveto (Names) 38 14.00 -0.50 alignedtext end grestore end grestore % Univ -> Names -newpath 1256 74 moveto -1264 74 1273 74 1282 74 curveto +newpath 1258 101 moveto +1267 101 1277 101 1286 101 curveto stroke -newpath 1282 72 moveto -1292 74 lineto -1282 77 lineto +newpath 1286 99 moveto +1296 101 lineto +1286 104 lineto closepath gsave 0 setgray stroke grestore fill @@ -282,12 +282,31 @@ end grestore end grestore % Term -> Univ -newpath 1166 74 moveto -1174 74 1183 74 1192 74 curveto +newpath 1164 81 moveto +1174 84 1186 88 1197 91 curveto stroke -newpath 1192 72 moveto -1202 74 lineto -1192 77 lineto +newpath 1197 88 moveto +1206 94 lineto +1196 93 lineto +closepath +gsave 0 setgray stroke grestore fill + +% Esubst +gsave 10 dict begin +1231 47 29 18 ellipse_path +stroke +gsave 10 dict begin +1231 48 moveto (Esubst) 37 14.00 -0.50 alignedtext +end grestore +end grestore + +% Term -> Esubst +newpath 1164 67 moveto +1174 64 1185 61 1196 58 curveto +stroke +newpath 1195 56 moveto +1205 55 lineto +1196 61 lineto closepath gsave 0 setgray stroke grestore fill @@ -359,12 +378,12 @@ gsave 0 setgray stroke grestore fill % Cooking -> Reduction newpath 300 116 moveto -336 113 393 108 426 102 curveto -426 102 444 95 462 87 curveto +336 114 393 109 426 102 curveto +437 99 453 94 468 88 curveto stroke -newpath 461 85 moveto -471 84 lineto -462 90 lineto +newpath 464 87 moveto +474 85 lineto +466 92 lineto closepath gsave 0 setgray stroke grestore fill diff --git a/doc/parsing.dep.ps b/doc/parsing.dep.ps index 5ee8ccaa0..3507cf4a9 100644 --- a/doc/parsing.dep.ps +++ b/doc/parsing.dep.ps @@ -3,7 +3,7 @@ %%For: Gros nain %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 576 225 +%%BoundingBox: 36 36 576 186 %%EndComments %%BeginProlog save @@ -139,367 +139,365 @@ def % /arrowwidth 5 def %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 576 225 +%%PageBoundingBox: 36 36 576 186 gsave -35 35 541 190 boxprim clip newpath +35 35 541 151 boxprim clip newpath 36 36 translate 0 0 1 beginpage -0.7050 set_scale +0.6818 set_scale 0 0 translate 0 rotate 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font % Pcoq gsave 10 dict begin -643 141 27 18 ellipse_path +669 72 27 18 ellipse_path stroke gsave 10 dict begin -643 142 moveto (Pcoq) 28 14.00 -0.50 alignedtext +669 73 moveto (Pcoq) 28 14.00 -0.50 alignedtext end grestore end grestore % Coqast gsave 10 dict begin -736 141 30 18 ellipse_path +762 72 30 18 ellipse_path stroke gsave 10 dict begin -736 142 moveto (Coqast) 38 14.00 -0.50 alignedtext +762 73 moveto (Coqast) 38 14.00 -0.50 alignedtext end grestore end grestore % Pcoq -> Coqast -newpath 670 141 moveto -678 141 687 141 696 141 curveto +newpath 696 72 moveto +704 72 713 72 722 72 curveto stroke -newpath 696 139 moveto -706 141 lineto -696 144 lineto +newpath 722 70 moveto +732 72 lineto +722 75 lineto closepath gsave 0 setgray stroke grestore fill % Extend gsave 10 dict begin -460 141 30 18 ellipse_path +486 124 30 18 ellipse_path stroke gsave 10 dict begin -460 142 moveto (Extend) 39 14.00 -0.50 alignedtext +486 125 moveto (Extend) 39 14.00 -0.50 alignedtext end grestore end grestore % Ast gsave 10 dict begin -553 141 27 18 ellipse_path +579 72 27 18 ellipse_path stroke gsave 10 dict begin -553 142 moveto (Ast) 19 14.00 -0.50 alignedtext +579 73 moveto (Ast) 19 14.00 -0.50 alignedtext end grestore end grestore % Extend -> Ast -newpath 490 141 moveto -498 141 507 141 516 141 curveto +newpath 508 112 moveto +520 105 536 96 550 88 curveto stroke -newpath 516 139 moveto -526 141 lineto -516 144 lineto +newpath 548 86 moveto +558 84 lineto +550 91 lineto closepath gsave 0 setgray stroke grestore fill % Ast -> Pcoq -newpath 580 141 moveto -588 141 597 141 606 141 curveto +newpath 606 72 moveto +614 72 623 72 632 72 curveto stroke -newpath 606 139 moveto -616 141 lineto -606 144 lineto +newpath 632 70 moveto +642 72 lineto +632 75 lineto closepath gsave 0 setgray stroke grestore fill % Termast gsave 10 dict begin -354 195 33 18 ellipse_path +380 18 33 18 ellipse_path stroke gsave 10 dict begin -354 196 moveto (Termast) 45 14.00 -0.50 alignedtext +380 19 moveto (Termast) 45 14.00 -0.50 alignedtext end grestore end grestore % Termast -> Ast -newpath 386 190 moveto -417 186 463 178 490 171 curveto -490 171 507 163 523 155 curveto +newpath 413 22 moveto +443 25 489 32 516 40 curveto +526 43 540 50 553 57 curveto stroke -newpath 521 153 moveto -531 151 lineto -523 158 lineto +newpath 551 53 moveto +559 60 lineto +549 58 lineto closepath gsave 0 setgray stroke grestore fill % Search gsave 10 dict begin -30 60 29 18 ellipse_path +30 46 29 18 ellipse_path stroke gsave 10 dict begin -30 61 moveto (Search) 37 14.00 -0.50 alignedtext +30 47 moveto (Search) 37 14.00 -0.50 alignedtext end grestore end grestore % Astterm gsave 10 dict begin -354 33 33 18 ellipse_path +258 72 33 18 ellipse_path stroke gsave 10 dict begin -354 34 moveto (Astterm) 45 14.00 -0.50 alignedtext +258 73 moveto (Astterm) 45 14.00 -0.50 alignedtext end grestore end grestore % Search -> Astterm -newpath 57 53 moveto -92 45 151 31 186 26 curveto -217 22 248 25 278 26 curveto -288 27 301 28 314 29 curveto -stroke -newpath 311 26 moveto -321 30 lineto -311 31 lineto +newpath 59 49 moveto +99 54 171 62 216 67 curveto +stroke +newpath 215 64 moveto +225 68 lineto +215 69 lineto closepath gsave 0 setgray stroke grestore fill % Pretty gsave 10 dict begin -123 110 27 18 ellipse_path +136 22 27 18 ellipse_path stroke gsave 10 dict begin -123 111 moveto (Pretty) 33 14.00 -0.50 alignedtext +136 23 moveto (Pretty) 33 14.00 -0.50 alignedtext end grestore end grestore % Search -> Pretty -newpath 53 72 moveto -65 79 80 87 94 94 curveto +newpath 58 40 moveto +71 37 87 33 101 30 curveto stroke -newpath 95 92 moveto -102 99 lineto -92 96 lineto +newpath 100 28 moveto +110 28 lineto +101 33 lineto closepath gsave 0 setgray stroke grestore fill -% Astterm -> Ast -newpath 387 35 moveto -418 38 465 44 490 57 curveto -509 67 527 95 540 116 curveto +% Astterm -> Termast +newpath 284 61 moveto +302 53 327 42 346 34 curveto stroke -newpath 542 114 moveto -544 124 lineto -537 116 lineto +newpath 344 32 moveto +354 30 lineto +346 37 lineto closepath gsave 0 setgray stroke grestore fill % Printer gsave 10 dict begin -232 164 29 18 ellipse_path +258 18 29 18 ellipse_path stroke gsave 10 dict begin -232 165 moveto (Printer) 38 14.00 -0.50 alignedtext +258 19 moveto (Printer) 38 14.00 -0.50 alignedtext end grestore end grestore % Pretty -> Printer -newpath 145 121 moveto -161 129 183 139 201 149 curveto +newpath 163 21 moveto +179 20 200 20 218 19 curveto stroke -newpath 201 146 moveto -209 153 lineto -199 151 lineto +newpath 218 17 moveto +228 19 lineto +218 22 lineto closepath gsave 0 setgray stroke grestore fill % Printer -> Termast -newpath 259 171 moveto -275 175 296 180 315 185 curveto +newpath 288 18 moveto +303 18 321 18 337 18 curveto stroke -newpath 315 182 moveto -324 187 lineto -314 187 lineto +newpath 337 16 moveto +347 18 lineto +337 21 lineto closepath gsave 0 setgray stroke grestore fill % Esyntax gsave 10 dict begin -354 141 33 18 ellipse_path +380 180 33 18 ellipse_path stroke gsave 10 dict begin -354 142 moveto (Esyntax) 45 14.00 -0.50 alignedtext +380 181 moveto (Esyntax) 45 14.00 -0.50 alignedtext end grestore end grestore % Printer -> Esyntax -newpath 260 159 moveto -276 156 296 152 313 149 curveto -stroke -newpath 313 147 moveto -323 147 lineto -314 151 lineto +newpath 284 27 moveto +293 31 301 36 304 42 curveto +325 76 321 121 340 156 curveto +342 160 345 163 350 165 curveto +stroke +newpath 348 161 moveto +356 168 lineto +346 166 lineto closepath gsave 0 setgray stroke grestore fill % Esyntax -> Extend -newpath 387 141 moveto -398 141 410 141 421 141 curveto +newpath 404 167 moveto +419 159 439 149 455 140 curveto stroke -newpath 420 139 moveto -430 141 lineto -420 144 lineto +newpath 453 138 moveto +463 136 lineto +455 143 lineto closepath gsave 0 setgray stroke grestore fill % G_zsyntax gsave 10 dict begin -232 110 40 18 ellipse_path +136 136 40 18 ellipse_path stroke gsave 10 dict begin -232 111 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext +136 137 moveto (G_zsyntax) 59 14.00 -0.50 alignedtext end grestore end grestore % G_zsyntax -> Astterm -newpath 259 97 moveto -266 93 273 89 278 86 curveto -291 77 302 65 314 57 curveto -317 55 319 54 322 52 curveto -stroke -newpath 321 49 moveto -331 46 lineto -324 54 lineto +newpath 162 122 moveto +180 112 206 99 226 88 curveto +stroke +newpath 224 86 moveto +234 84 lineto +226 91 lineto closepath gsave 0 setgray stroke grestore fill % G_zsyntax -> Esyntax -newpath 267 119 moveto -282 123 300 127 315 131 curveto +newpath 170 146 moveto +185 150 201 154 212 156 curveto +247 163 302 170 340 175 curveto stroke -newpath 315 128 moveto -324 133 lineto -314 133 lineto +newpath 338 172 moveto +348 176 lineto +338 177 lineto closepath gsave 0 setgray stroke grestore fill % G_rsyntax gsave 10 dict begin -232 56 39 18 ellipse_path +136 200 39 18 ellipse_path stroke gsave 10 dict begin -232 57 moveto (G_rsyntax) 58 14.00 -0.50 alignedtext +136 201 moveto (G_rsyntax) 58 14.00 -0.50 alignedtext end grestore end grestore % G_rsyntax -> Astterm -newpath 269 49 moveto -283 47 299 43 313 41 curveto -stroke -newpath 313 39 moveto -323 39 lineto -314 43 lineto +newpath 157 185 moveto +164 179 172 172 176 166 curveto +192 144 195 115 212 96 curveto +212 96 218 93 225 89 curveto +stroke +newpath 224 87 moveto +234 85 lineto +226 91 lineto closepath gsave 0 setgray stroke grestore fill % G_rsyntax -> Esyntax -newpath 260 69 moveto -267 72 274 76 278 80 curveto -292 90 301 106 314 117 curveto -317 119 319 120 322 122 curveto -stroke -newpath 324 120 moveto -331 128 lineto -321 125 lineto +newpath 175 197 moveto +220 193 292 187 338 184 curveto +stroke +newpath 337 182 moveto +347 183 lineto +337 187 lineto closepath gsave 0 setgray stroke grestore fill % G_natsyntax gsave 10 dict begin -232 218 45 18 ellipse_path +258 126 45 18 ellipse_path stroke gsave 10 dict begin -232 219 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext +258 127 moveto (G_natsyntax) 70 14.00 -0.50 alignedtext end grestore end grestore % G_natsyntax -> Termast -newpath 273 210 moveto -286 208 301 205 314 203 curveto -stroke -newpath 313 201 moveto -323 201 lineto -314 206 lineto +newpath 288 113 moveto +295 109 300 106 304 102 curveto +321 85 325 59 340 42 curveto +343 39 345 37 348 36 curveto +stroke +newpath 347 34 moveto +357 31 lineto +349 38 lineto closepath gsave 0 setgray stroke grestore fill % G_natsyntax -> Esyntax -newpath 261 204 moveto -267 200 274 197 278 194 curveto -291 185 302 173 314 165 curveto -314 165 318 163 323 159 curveto -stroke -newpath 322 157 moveto -332 154 lineto -324 161 lineto +newpath 288 139 moveto +306 147 328 157 346 165 curveto +stroke +newpath 346 162 moveto +355 168 lineto +345 167 lineto closepath gsave 0 setgray stroke grestore fill -% Stdlib +% Coqlib gsave 10 dict begin -354 249 27 18 ellipse_path +380 126 29 18 ellipse_path stroke gsave 10 dict begin -354 250 moveto (Stdlib) 33 14.00 -0.50 alignedtext +380 127 moveto (Coqlib) 38 14.00 -0.50 alignedtext end grestore end grestore -% G_natsyntax -> Stdlib -newpath 271 228 moveto -287 232 305 236 320 240 curveto +% G_natsyntax -> Coqlib +newpath 304 126 moveto +316 126 329 126 340 126 curveto stroke -newpath 320 237 moveto -329 243 lineto -319 242 lineto +newpath 340 124 moveto +350 126 lineto +340 129 lineto closepath gsave 0 setgray stroke grestore fill % Egrammar gsave 10 dict begin -354 87 40 18 ellipse_path +380 72 40 18 ellipse_path stroke gsave 10 dict begin -354 88 moveto (Egrammar) 58 14.00 -0.50 alignedtext +380 73 moveto (Egrammar) 58 14.00 -0.50 alignedtext end grestore end grestore % Egrammar -> Extend -newpath 381 101 moveto -395 109 413 118 429 125 curveto +newpath 407 85 moveto +421 93 439 101 454 108 curveto stroke -newpath 429 122 moveto -437 129 lineto -427 127 lineto +newpath 454 105 moveto +462 112 lineto +452 110 lineto closepath gsave 0 setgray stroke grestore fill % Lexer gsave 10 dict begin -460 87 27 18 ellipse_path +486 70 27 18 ellipse_path stroke gsave 10 dict begin -460 88 moveto (Lexer) 32 14.00 -0.50 alignedtext +486 71 moveto (Lexer) 32 14.00 -0.50 alignedtext end grestore end grestore % Egrammar -> Lexer -newpath 394 87 moveto -404 87 414 87 423 87 curveto +newpath 420 71 moveto +430 71 440 71 449 71 curveto stroke -newpath 423 85 moveto -433 87 lineto -423 90 lineto +newpath 449 69 moveto +459 71 lineto +449 74 lineto closepath gsave 0 setgray stroke grestore fill endpage diff --git a/doc/pretyping.dep.ps b/doc/pretyping.dep.ps index e18d3dd57..c54821490 100644 --- a/doc/pretyping.dep.ps +++ b/doc/pretyping.dep.ps @@ -3,7 +3,7 @@ %%For: Gros nain %%Title: G %%Pages: (atend) -%%BoundingBox: 36 36 576 238 +%%BoundingBox: 36 36 576 216 %%EndComments %%BeginProlog save @@ -139,12 +139,12 @@ def % /arrowwidth 5 def %%EndSetup %%Page: 1 1 -%%PageBoundingBox: 36 36 576 238 +%%PageBoundingBox: 36 36 576 216 gsave -35 35 541 203 boxprim clip newpath +35 35 541 181 boxprim clip newpath 36 36 translate 0 0 1 beginpage -0.7219 set_scale +0.6444 set_scale 0 0 translate 0 rotate 0.000 0.000 0.000 graphcolor 14.00 /Times-Roman set_font @@ -196,6 +196,34 @@ newpath 541 244 moveto closepath gsave 0 setgray stroke grestore fill +% Tacred +gsave 10 dict begin +712 72 29 18 ellipse_path +stroke +gsave 10 dict begin +712 73 moveto (Tacred) 38 14.00 -0.50 alignedtext +end grestore +end grestore + +% Cbv +gsave 10 dict begin +811 72 27 18 ellipse_path +stroke +gsave 10 dict begin +811 73 moveto (Cbv) 23 14.00 -0.50 alignedtext +end grestore +end grestore + +% Tacred -> Cbv +newpath 742 72 moveto +752 72 764 72 774 72 curveto +stroke +newpath 774 70 moveto +784 72 lineto +774 75 lineto +closepath +gsave 0 setgray stroke grestore fill + % Syntax_def gsave 10 dict begin 588 207 42 18 ellipse_path @@ -245,18 +273,28 @@ end grestore % Recordops -> Classops newpath 485 112 moveto 491 108 496 105 500 102 curveto -514 92 523 77 536 69 curveto -540 66 546 64 551 61 curveto +514 93 523 78 536 69 curveto +541 66 548 63 555 60 curveto +stroke +newpath 551 59 moveto +561 57 lineto +553 64 lineto +closepath +gsave 0 setgray stroke grestore fill + +% Classops -> Tacred +newpath 620 52 moveto +637 55 657 60 675 64 curveto stroke -newpath 550 59 moveto -560 56 lineto -552 63 lineto +newpath 675 61 moveto +684 66 lineto +674 66 lineto closepath gsave 0 setgray stroke grestore fill % Classops -> Rawterm -newpath 614 57 moveto -627 63 640 69 640 69 curveto +newpath 616 56 moveto +625 60 635 64 640 69 curveto 656 83 678 109 694 129 curveto stroke newpath 695 126 moveto @@ -267,39 +305,20 @@ gsave 0 setgray stroke grestore fill % Retyping gsave 10 dict begin -712 72 36 18 ellipse_path +712 18 36 18 ellipse_path stroke gsave 10 dict begin -712 73 moveto (Retyping) 51 14.00 -0.50 alignedtext +712 19 moveto (Retyping) 51 14.00 -0.50 alignedtext end grestore end grestore % Classops -> Retyping -newpath 620 52 moveto -635 55 653 59 669 63 curveto -stroke -newpath 670 61 moveto -679 65 lineto -669 65 lineto -closepath -gsave 0 setgray stroke grestore fill - -% Tacred -gsave 10 dict begin -712 18 29 18 ellipse_path -stroke -gsave 10 dict begin -712 19 moveto (Tacred) 38 14.00 -0.50 alignedtext -end grestore -end grestore - -% Classops -> Tacred newpath 620 38 moveto -637 35 657 30 675 26 curveto +635 35 653 31 669 27 curveto stroke -newpath 674 24 moveto -684 24 lineto -675 29 lineto +newpath 669 25 moveto +679 25 lineto +670 29 lineto closepath gsave 0 setgray stroke grestore fill |