diff options
Diffstat (limited to 'dev/ocamlweb-doc')
-rw-r--r-- | dev/ocamlweb-doc/Makefile | 75 | ||||
-rw-r--r-- | dev/ocamlweb-doc/ast.ml | 47 | ||||
-rw-r--r-- | dev/ocamlweb-doc/interp.dep.ps | 583 | ||||
-rw-r--r-- | dev/ocamlweb-doc/intro.tex | 25 | ||||
-rw-r--r-- | dev/ocamlweb-doc/kernel.dep.ps | 1454 | ||||
-rw-r--r-- | dev/ocamlweb-doc/lex.mll | 81 | ||||
-rw-r--r-- | dev/ocamlweb-doc/library.dep.ps | 836 | ||||
-rw-r--r-- | dev/ocamlweb-doc/macros.tex | 7 | ||||
-rw-r--r-- | dev/ocamlweb-doc/parse.ml | 183 | ||||
-rw-r--r-- | dev/ocamlweb-doc/parsing.dep.ps | 1115 | ||||
-rw-r--r-- | dev/ocamlweb-doc/preamble.tex | 8 | ||||
-rw-r--r-- | dev/ocamlweb-doc/pretyping.dep.ps | 1259 | ||||
-rw-r--r-- | dev/ocamlweb-doc/proofs.dep.ps | 638 | ||||
-rw-r--r-- | dev/ocamlweb-doc/syntax.mly | 224 | ||||
-rw-r--r-- | dev/ocamlweb-doc/tactics.dep.ps | 991 | ||||
-rw-r--r-- | dev/ocamlweb-doc/toplevel.dep.ps | 971 |
16 files changed, 8497 insertions, 0 deletions
diff --git a/dev/ocamlweb-doc/Makefile b/dev/ocamlweb-doc/Makefile new file mode 100644 index 00000000..96491017 --- /dev/null +++ b/dev/ocamlweb-doc/Makefile @@ -0,0 +1,75 @@ + +# Makefile for doc/ + +all:: newparse coq.ps minicop.ps +#newsyntax.dvi minicoq.dvi + + +OBJS=lex.cmo ast.cmo parse.cmo syntax.cmo + +newparse: $(OBJS) syntax.mli lex.ml syntax.ml + ocamlc -o newparse $(OBJS) + +%.cmo: %.ml + ocamlc -c $< + +%.cmi: %.mli + ocamlc -c $< + +%.ml: %.mll + ocamllex $< + +%.ml: %.mly + ocamlyacc -v $< + +%.mli: %.mly + ocamlyacc -v $< + +clean:: + rm -f *.cm* *.output syntax.ml syntax.mli lex.ml newparse + +parse.cmo: ast.cmo +syntax.cmi: parse.cmo +syntax.cmo: lex.cmo parse.cmo syntax.cmi +lex.cmo: syntax.cmi +ast.cmo: ast.ml + +newsyntax.dvi: newsyntax.tex + latex $< + latex $< + +coq.dvi: coq.tex + latex coq + latex coq + +coq.tex:: + ocamlweb -p "\usepackage{epsfig}" \ + macros.tex intro.tex \ + ../../lib/{doc.tex,*.mli} ../../kernel/{doc.tex,*.mli} ../../library/{doc.tex,*.mli} \ + ../../pretyping/{doc.tex,*.mli} ../../interp/{doc.tex,*.mli} \ + ../../parsing/{doc.tex,*.mli} ../../proofs/{doc.tex,*.mli} \ + ../../tactics/{doc.tex,*.mli} ../../toplevel/{doc.tex,*.mli} \ + -o coq.tex + + +depend:: kernel.dep.ps library.dep.ps pretyping.dep.ps parsing.dep.ps \ + proofs.dep.ps tactics.dep.ps toplevel.dep.ps interp.dep.ps + +%.dot: ../% + (cd ../$*; ocamldep *.ml *.mli) | ocamldot -lr > $@ + +%.dep.ps: %.dot + dot -Tps $< -o $@ + +clean:: + rm -f *~ *.log *.aux + +.SUFFIXES: .tex .dvi .ps .cmo .cmi .mli .ml .mll .mly + +%.dvi: %.tex + latex $< && latex $< + +%.ps: %.dvi + dvips $< -o $@ + + diff --git a/dev/ocamlweb-doc/ast.ml b/dev/ocamlweb-doc/ast.ml new file mode 100644 index 00000000..2153ef47 --- /dev/null +++ b/dev/ocamlweb-doc/ast.ml @@ -0,0 +1,47 @@ + +type constr_ast = + Pair of constr_ast * constr_ast +| Prod of binder list * constr_ast +| Lambda of binder list * constr_ast +| Let of string * constr_ast * constr_ast +| LetCase of binder list * constr_ast * constr_ast +| IfCase of constr_ast * constr_ast * constr_ast +| Eval of red_fun * constr_ast +| Infix of string * constr_ast * constr_ast +| Prefix of string * constr_ast +| Postfix of string * constr_ast +| Appl of constr_ast * constr_arg list +| ApplExpl of string list * constr_ast list +| Scope of string * constr_ast +| Qualid of string list +| Prop | Set | Type +| Int of string +| Hole +| Meta of string +| Fixp of fix_kind * + (string * binder list * constr_ast * string option * constr_ast) list * + string +| Match of case_item list * constr_ast option * + (pattern list * constr_ast) list + +and red_fun = Simpl + +and binder = string * constr_ast + +and constr_arg = string option * constr_ast + +and fix_kind = Fix | CoFix + +and case_item = constr_ast * (string option * constr_ast option) + +and pattern = + PatAs of pattern * string +| PatType of pattern * constr_ast +| PatConstr of string * pattern list +| PatVar of string + +let mk_cast c t = + if t=Hole then c else Infix(":",c,t) + +let mk_lambda bl t = + if bl=[] then t else Lambda(bl,t) diff --git a/dev/ocamlweb-doc/interp.dep.ps b/dev/ocamlweb-doc/interp.dep.ps new file mode 100644 index 00000000..b0554481 --- /dev/null +++ b/dev/ocamlweb-doc/interp.dep.ps @@ -0,0 +1,583 @@ +%!PS-Adobe-2.0 +%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) +%%For: (herbelin) Hugo Herbelin +%%Title: G +%%Pages: (atend) +%%BoundingBox: 35 35 577 160 +%%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 577 160 +%%PageOrientation: Portrait +gsave +35 35 542 125 boxprim clip newpath +36 36 translate +0 0 1 beginpage +0.9343 set_scale +0 0 translate 0 rotate +0.000 0.000 0.000 graphcolor +14.00 /Times-Roman set_font + +% Syntax_def +gsave 10 dict begin +303 110 45 18 ellipse_path +stroke +gsave 10 dict begin +271 105 moveto +(Syntax_def) +[7.68 6.96 6.96 4.08 6.24 6.96 6.96 6.96 6.24 4.56] +xshow +end grestore +end grestore + +% Notation +gsave 10 dict begin +422 60 38 18 ellipse_path +stroke +gsave 10 dict begin +397 55 moveto +(Notation) +[9.84 6.72 4.08 6.24 3.84 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Syntax_def -> Notation +newpath 334 97 moveto +350 90 369 83 385 76 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 386 79 moveto +394 72 lineto +383 73 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 386 79 moveto +394 72 lineto +383 73 lineto +closepath +stroke +end grestore + +% Ppextend +gsave 10 dict begin +537 60 39 18 ellipse_path +stroke +gsave 10 dict begin +511 55 moveto +(Ppextend) +[7.68 6.96 5.76 6.96 3.84 6.24 6.96 6.96] +xshow +end grestore +end grestore + +% Notation -> Ppextend +newpath 460 60 moveto +469 60 478 60 488 60 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 488 64 moveto +498 60 lineto +488 57 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 488 64 moveto +498 60 lineto +488 57 lineto +closepath +stroke +end grestore + +% Topconstr +gsave 10 dict begin +537 114 41 18 ellipse_path +stroke +gsave 10 dict begin +509 109 moveto +(Topconstr) +[7.2 6.96 6.96 6.24 6.96 6.96 5.28 3.84 4.56] +xshow +end grestore +end grestore + +% Notation -> Topconstr +newpath 449 73 moveto +464 80 483 89 500 97 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 498 100 moveto +509 101 lineto +501 94 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 498 100 moveto +509 101 lineto +501 94 lineto +closepath +stroke +end grestore + +% Modintern +gsave 10 dict begin +44 98 43 18 ellipse_path +stroke +gsave 10 dict begin +13 93 moveto +(Modintern) +[12.48 6.96 6.96 3.84 6.96 3.84 6.24 4.8 6.96] +xshow +end grestore +end grestore + +% Constrintern +gsave 10 dict begin +173 98 48 18 ellipse_path +stroke +gsave 10 dict begin +138 93 moveto +(Constrintern) +[9.36 6.96 6.96 5.28 3.84 4.8 3.84 6.96 3.84 6.24 4.8 6.96] +xshow +end grestore +end grestore + +% Modintern -> Constrintern +newpath 88 98 moveto +97 98 106 98 115 98 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 115 102 moveto +125 98 lineto +115 95 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 115 102 moveto +125 98 lineto +115 95 lineto +closepath +stroke +end grestore + +% Constrintern -> Syntax_def +newpath 220 102 moveto +229 103 239 104 249 105 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 249 108 moveto +259 106 lineto +249 102 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 249 108 moveto +259 106 lineto +249 102 lineto +closepath +stroke +end grestore + +% Reserve +gsave 10 dict begin +303 56 35 18 ellipse_path +stroke +gsave 10 dict begin +280 51 moveto +(Reserve) +[9.12 6.24 5.52 6.24 4.8 6.48 6.24] +xshow +end grestore +end grestore + +% Constrintern -> Reserve +newpath 210 86 moveto +227 81 246 75 263 69 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 264 72 moveto +273 66 lineto +262 66 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 264 72 moveto +273 66 lineto +262 66 lineto +closepath +stroke +end grestore + +% Genarg +gsave 10 dict begin +422 114 33 18 ellipse_path +stroke +gsave 10 dict begin +401 109 moveto +(Genarg) +[10.08 6.24 6.96 6.24 4.32 6.96] +xshow +end grestore +end grestore + +% Genarg -> Topconstr +newpath 456 114 moveto +465 114 476 114 486 114 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 486 118 moveto +496 114 lineto +486 111 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 486 118 moveto +496 114 lineto +486 111 lineto +closepath +stroke +end grestore + +% Coqlib +gsave 10 dict begin +44 21 32 18 ellipse_path +stroke +gsave 10 dict begin +24 16 moveto +(Coqlib) +[9.36 6.96 6.96 3.84 3.84 6.96] +xshow +end grestore +end grestore + +% Constrextern +gsave 10 dict begin +173 21 49 18 ellipse_path +stroke +gsave 10 dict begin +137 16 moveto +(Constrextern) +[9.36 6.96 6.96 5.28 3.84 4.56 5.76 6.96 3.84 6.24 4.8 6.96] +xshow +end grestore +end grestore + +% Coqlib -> Constrextern +newpath 77 21 moveto +88 21 101 21 114 21 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 114 25 moveto +124 21 lineto +114 18 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 114 25 moveto +124 21 lineto +114 18 lineto +closepath +stroke +end grestore + +% Constrextern -> Notation +newpath 222 19 moveto +257 18 307 20 348 29 curveto +361 31 375 37 388 42 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 386 45 moveto +397 46 lineto +389 39 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 386 45 moveto +397 46 lineto +389 39 lineto +closepath +stroke +end grestore + +% Constrextern -> Reserve +newpath 213 32 moveto +228 36 246 41 261 45 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 260 48 moveto +271 48 lineto +262 42 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 260 48 moveto +271 48 lineto +262 42 lineto +closepath +stroke +end grestore +endpage +showpage +grestore +%%PageTrailer +%%EndPage: 1 +%%Trailer +%%Pages: 1 +end +restore +%%EOF diff --git a/dev/ocamlweb-doc/intro.tex b/dev/ocamlweb-doc/intro.tex new file mode 100644 index 00000000..4cec8673 --- /dev/null +++ b/dev/ocamlweb-doc/intro.tex @@ -0,0 +1,25 @@ + +\ocwsection This is \Coq, a proof assistant for the \CCI. +This document describes the implementation of \Coq. +It has been automatically generated from the source of +\Coq\ using \textsf{ocamlweb}, a literate programming tool for +\textsf{Objective Caml}\footnote{\Coq, \textsf{Objective Caml} and + \textsf{ocamlweb} are all freely available at + \textsf{http://coq.inria.fr/}, \textsf{http://caml.inria.fr/} and + \textsf{http://www.lri.fr/\~{}filliatr/ocamlweb}.}. +The source files are organized in several directories, which are +described here as separate chapters. + +\begin{center} + \begin{tabular}{p{10cm}rr} + Chapter & section & page \\[0.5em] + \hline\\[0.2em] + Utility libraries \dotfill & \refsec{lib} & \pageref{lib} \\[0.5em] + Kernel \dotfill & \refsec{kernel} & \pageref{kernel} \\[0.5em] + Library \dotfill & \refsec{library} & \pageref{library} \\[0.5em] + Pretyping \dotfill & \refsec{pretyping} & \pageref{pretyping} \\[0.5em] + Proof engine \dotfill & \refsec{proofs} & \pageref{proofs} \\[0.5em] + Tactics \dotfill & \refsec{tactics} & \pageref{tactics} \\[0.5em] + Toplevel \dotfill & \refsec{toplevel}& \pageref{toplevel}\\[0.5em] + \end{tabular} +\end{center}
\ No newline at end of file diff --git a/dev/ocamlweb-doc/kernel.dep.ps b/dev/ocamlweb-doc/kernel.dep.ps new file mode 100644 index 00000000..3c00121e --- /dev/null +++ b/dev/ocamlweb-doc/kernel.dep.ps @@ -0,0 +1,1454 @@ +%!PS-Adobe-2.0 +%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) +%%For: (herbelin) Hugo Herbelin +%%Title: G +%%Pages: (atend) +%%BoundingBox: 35 35 577 127 +%%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 577 127 +%%PageOrientation: Portrait +gsave +35 35 542 92 boxprim clip newpath +36 36 translate +0 0 1 beginpage +0.2845 set_scale +0 0 translate 0 rotate +0.000 0.000 0.000 graphcolor +14.00 /Times-Roman set_font + +% Vm +gsave 10 dict begin +801 294 27 18 ellipse_path +stroke +gsave 10 dict begin +789 289 moveto +(Vm) +[10.08 10.8] +xshow +end grestore +end grestore + +% Cemitcodes +gsave 10 dict begin +1427 200 46 18 ellipse_path +stroke +gsave 10 dict begin +1393 195 moveto +(Cemitcodes) +[9.36 6.24 10.8 3.84 3.84 6.24 6.96 6.96 6.24 5.52] +xshow +end grestore +end grestore + +% Vm -> Cemitcodes +newpath 826 287 moveto +871 276 969 254 1053 254 curveto +1053 254 1053 254 1174 254 curveto +1249 254 1332 231 1382 215 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1383 218 moveto +1392 212 lineto +1381 212 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1383 218 moveto +1392 212 lineto +1381 212 lineto +closepath +stroke +end grestore + +% Conv_oracle +gsave 10 dict begin +1053 300 48 18 ellipse_path +stroke +gsave 10 dict begin +1017 295 moveto +(Conv_oracle) +[9.36 6.96 6.48 6.96 6.96 6.96 4.56 6.24 6.24 3.84 6.24] +xshow +end grestore +end grestore + +% Vm -> Conv_oracle +newpath 828 295 moveto +868 296 942 298 995 299 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 995 303 moveto +1005 299 lineto +995 296 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 995 303 moveto +1005 299 lineto +995 296 lineto +closepath +stroke +end grestore + +% Mod_subst +gsave 10 dict begin +1556 146 45 18 ellipse_path +stroke +gsave 10 dict begin +1524 141 moveto +(Mod_subst) +[12.48 6.96 6.96 6.96 5.52 6.96 6.96 5.28 3.84] +xshow +end grestore +end grestore + +% Cemitcodes -> Mod_subst +newpath 1459 187 moveto +1476 180 1497 171 1516 163 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1517 166 moveto +1525 159 lineto +1514 160 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1517 166 moveto +1525 159 lineto +1514 160 lineto +closepath +stroke +end grestore + +% Cbytecodes +gsave 10 dict begin +1556 200 45 18 ellipse_path +stroke +gsave 10 dict begin +1523 195 moveto +(Cbytecodes) +[9.36 6.48 6.96 3.84 6.24 6.24 6.96 6.96 6.24 5.52] +xshow +end grestore +end grestore + +% Cemitcodes -> Cbytecodes +newpath 1474 200 moveto +1482 200 1491 200 1500 200 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1500 204 moveto +1510 200 lineto +1500 197 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1500 204 moveto +1510 200 lineto +1500 197 lineto +closepath +stroke +end grestore + +% Copcodes +gsave 10 dict begin +1556 254 41 18 ellipse_path +stroke +gsave 10 dict begin +1528 249 moveto +(Copcodes) +[9.36 6.96 6.96 6.24 6.96 6.96 6.24 5.52] +xshow +end grestore +end grestore + +% Cemitcodes -> Copcodes +newpath 1459 213 moveto +1476 221 1498 230 1517 237 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1515 240 moveto +1526 241 lineto +1518 234 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1515 240 moveto +1526 241 lineto +1518 234 lineto +closepath +stroke +end grestore + +% Names +gsave 10 dict begin +1865 270 33 18 ellipse_path +stroke +gsave 10 dict begin +1845 265 moveto +(Names) +[9.6 6.24 10.8 6.24 5.52] +xshow +end grestore +end grestore + +% Conv_oracle -> Names +newpath 1102 300 moveto +1151 300 1228 300 1295 300 curveto +1295 300 1295 300 1666 300 curveto +1722 300 1785 288 1825 279 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1826 282 moveto +1835 277 lineto +1825 276 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1826 282 moveto +1835 277 lineto +1825 276 lineto +closepath +stroke +end grestore + +% Vconv +gsave 10 dict begin +552 202 32 18 ellipse_path +stroke +gsave 10 dict begin +533 197 moveto +(Vconv) +[10.08 6.24 6.96 6.48 6.96] +xshow +end grestore +end grestore + +% Csymtable +gsave 10 dict begin +674 202 43 18 ellipse_path +stroke +gsave 10 dict begin +643 197 moveto +(Csymtable) +[9.36 5.52 6.96 10.8 4.08 6.24 6.96 3.84 6.24] +xshow +end grestore +end grestore + +% Vconv -> Csymtable +newpath 584 202 moveto +595 202 608 202 620 202 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 620 206 moveto +630 202 lineto +620 199 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 620 206 moveto +630 202 lineto +620 199 lineto +closepath +stroke +end grestore + +% Inductive +gsave 10 dict begin +674 110 39 18 ellipse_path +stroke +gsave 10 dict begin +647 105 moveto +(Inductive) +[4.56 6.96 6.96 6.96 6.24 3.84 3.84 6.48 6.24] +xshow +end grestore +end grestore + +% Vconv -> Inductive +newpath 571 187 moveto +591 172 622 149 645 132 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 647 135 moveto +653 126 lineto +643 129 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 647 135 moveto +653 126 lineto +643 129 lineto +closepath +stroke +end grestore + +% Csymtable -> Vm +newpath 696 218 moveto +717 234 751 258 775 275 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 773 278 moveto +783 281 lineto +777 272 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 773 278 moveto +783 281 lineto +777 272 lineto +closepath +stroke +end grestore + +% Cbytegen +gsave 10 dict begin +801 164 39 18 ellipse_path +stroke +gsave 10 dict begin +774 159 moveto +(Cbytegen) +[9.36 6.48 6.96 3.84 6.24 6.72 6.24 6.96] +xshow +end grestore +end grestore + +% Csymtable -> Cbytegen +newpath 709 191 moveto +724 187 742 181 758 177 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 759 180 moveto +768 174 lineto +757 174 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 759 180 moveto +768 174 lineto +757 174 lineto +closepath +stroke +end grestore + +% Type_errors +gsave 10 dict begin +801 110 47 18 ellipse_path +stroke +gsave 10 dict begin +767 105 moveto +(Type_errors) +[6.96 6.96 6.96 6.24 6.96 6.24 5.04 4.56 6.96 4.56 5.52] +xshow +end grestore +end grestore + +% Inductive -> Type_errors +newpath 714 110 moveto +724 110 734 110 744 110 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 744 114 moveto +754 110 lineto +744 107 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 744 114 moveto +754 110 lineto +744 107 lineto +closepath +stroke +end grestore + +% Univ +gsave 10 dict begin +1763 241 27 18 ellipse_path +stroke +gsave 10 dict begin +1748 236 moveto +(Univ) +[9.6 6.96 3.84 6.96] +xshow +end grestore +end grestore + +% Univ -> Names +newpath 1788 248 moveto +1800 251 1814 255 1826 259 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1825 262 moveto +1836 262 lineto +1827 256 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1825 262 moveto +1836 262 lineto +1827 256 lineto +closepath +stroke +end grestore + +% Typeops +gsave 10 dict begin +552 110 36 18 ellipse_path +stroke +gsave 10 dict begin +528 105 moveto +(Typeops) +[6.96 6.96 6.96 6.24 6.96 6.96 5.52] +xshow +end grestore +end grestore + +% Typeops -> Inductive +newpath 589 110 moveto +600 110 612 110 624 110 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 624 114 moveto +634 110 lineto +624 107 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 624 114 moveto +634 110 lineto +624 107 lineto +closepath +stroke +end grestore + +% Entries +gsave 10 dict begin +801 56 33 18 ellipse_path +stroke +gsave 10 dict begin +780 51 moveto +(Entries) +[8.4 6.96 3.84 4.8 3.84 6.24 5.52] +xshow +end grestore +end grestore + +% Typeops -> Entries +newpath 581 99 moveto +595 93 614 87 630 83 curveto +673 73 723 66 758 61 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 758 64 moveto +768 60 lineto +758 58 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 758 64 moveto +768 60 lineto +758 58 lineto +closepath +stroke +end grestore + +% Sign +gsave 10 dict begin +1427 100 27 18 ellipse_path +stroke +gsave 10 dict begin +1414 95 moveto +(Sign) +[7.68 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Entries -> Sign +newpath 834 61 moveto +882 68 974 79 1053 79 curveto +1053 79 1053 79 1174 79 curveto +1251 79 1342 89 1390 95 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1390 98 moveto +1400 96 lineto +1390 92 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1390 98 moveto +1400 96 lineto +1390 92 lineto +closepath +stroke +end grestore + +% Reduction +gsave 10 dict begin +926 208 42 18 ellipse_path +stroke +gsave 10 dict begin +897 203 moveto +(Reduction) +[9.12 6.24 6.96 6.96 6.24 3.84 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Type_errors -> Reduction +newpath 829 125 moveto +836 129 842 133 848 137 curveto +868 151 887 170 902 184 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 900 187 moveto +910 191 lineto +905 182 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 900 187 moveto +910 191 lineto +905 182 lineto +closepath +stroke +end grestore + +% Reduction -> Conv_oracle +newpath 948 224 moveto +968 239 999 261 1023 278 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1021 281 moveto +1031 284 lineto +1025 275 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1021 281 moveto +1031 284 lineto +1025 275 lineto +closepath +stroke +end grestore + +% Closure +gsave 10 dict begin +1053 208 35 18 ellipse_path +stroke +gsave 10 dict begin +1031 203 moveto +(Closure) +[9.36 3.84 6.96 5.52 6.96 4.56 6.24] +xshow +end grestore +end grestore + +% Reduction -> Closure +newpath 968 208 moveto +981 208 994 208 1008 208 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1008 212 moveto +1018 208 lineto +1008 205 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1008 212 moveto +1018 208 lineto +1008 205 lineto +closepath +stroke +end grestore + +% Term_typing +gsave 10 dict begin +313 110 49 18 ellipse_path +stroke +gsave 10 dict begin +277 105 moveto +(Term_typing) +[7.2 6.24 4.8 10.8 6.96 3.84 6.96 6.96 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Term_typing -> Cbytegen +newpath 347 123 moveto +363 128 381 134 398 137 curveto +524 161 675 165 752 165 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 752 169 moveto +762 165 lineto +752 162 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 752 169 moveto +762 165 lineto +752 162 lineto +closepath +stroke +end grestore + +% Cooking +gsave 10 dict begin +436 225 37 18 ellipse_path +stroke +gsave 10 dict begin +411 220 moveto +(Cooking) +[9.36 6.96 6.96 6.96 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Term_typing -> Cooking +newpath 331 127 moveto +352 147 387 179 410 202 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 408 205 moveto +418 209 lineto +413 200 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 408 205 moveto +418 209 lineto +413 200 lineto +closepath +stroke +end grestore + +% Indtypes +gsave 10 dict begin +436 110 37 18 ellipse_path +stroke +gsave 10 dict begin +411 105 moveto +(Indtypes) +[4.56 6.96 6.96 3.84 6.96 6.96 6.24 5.52] +xshow +end grestore +end grestore + +% Term_typing -> Indtypes +newpath 362 110 moveto +370 110 379 110 388 110 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 388 114 moveto +398 110 lineto +388 107 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 388 114 moveto +398 110 lineto +388 107 lineto +closepath +stroke +end grestore + +% Environ +gsave 10 dict begin +1174 181 36 18 ellipse_path +stroke +gsave 10 dict begin +1151 176 moveto +(Environ) +[8.4 6.48 6.96 3.84 4.56 6.96 6.96] +xshow +end grestore +end grestore + +% Cbytegen -> Environ +newpath 841 166 moveto +911 169 1054 175 1128 179 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1128 183 moveto +1138 179 lineto +1128 176 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1128 183 moveto +1138 179 lineto +1128 176 lineto +closepath +stroke +end grestore + +% Cooking -> Reduction +newpath 473 227 moveto +485 228 498 229 510 229 curveto +603 231 626 233 718 229 curveto +773 226 834 220 876 214 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 876 217 moveto +886 213 lineto +876 211 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 876 217 moveto +886 213 lineto +876 211 lineto +closepath +stroke +end grestore + +% Indtypes -> Typeops +newpath 474 110 moveto +484 110 495 110 505 110 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 505 114 moveto +515 110 lineto +505 107 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 505 114 moveto +515 110 lineto +505 107 lineto +closepath +stroke +end grestore + +% Term +gsave 10 dict begin +1666 173 28 18 ellipse_path +stroke +gsave 10 dict begin +1651 168 moveto +(Term) +[7.2 6.24 4.8 10.8] +xshow +end grestore +end grestore + +% Term -> Univ +newpath 1685 186 moveto +1699 196 1719 211 1736 222 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1734 225 moveto +1744 228 lineto +1738 219 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1734 225 moveto +1744 228 lineto +1738 219 lineto +closepath +stroke +end grestore + +% Esubst +gsave 10 dict begin +1763 173 32 18 ellipse_path +stroke +gsave 10 dict begin +1743 168 moveto +(Esubst) +[8.4 5.52 6.96 6.96 5.28 3.84] +xshow +end grestore +end grestore + +% Term -> Esubst +newpath 1694 173 moveto +1702 173 1711 173 1720 173 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1720 177 moveto +1730 173 lineto +1720 170 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1720 177 moveto +1730 173 lineto +1720 170 lineto +closepath +stroke +end grestore + +% Subtyping +gsave 10 dict begin +552 56 42 18 ellipse_path +stroke +gsave 10 dict begin +523 51 moveto +(Subtyping) +[7.68 6.96 6.96 3.84 6.96 6.96 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Subtyping -> Inductive +newpath 581 69 moveto +597 77 618 86 636 93 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 634 96 moveto +645 97 lineto +637 90 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 634 96 moveto +645 97 lineto +637 90 lineto +closepath +stroke +end grestore + +% Modops +gsave 10 dict begin +674 18 36 18 ellipse_path +stroke +gsave 10 dict begin +650 13 moveto +(Modops) +[12.48 6.96 6.96 6.96 6.96 5.52] +xshow +end grestore +end grestore + +% Subtyping -> Modops +newpath 586 45 moveto +601 41 618 35 633 31 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 634 34 moveto +643 28 lineto +632 28 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 634 34 moveto +643 28 lineto +632 28 lineto +closepath +stroke +end grestore + +% Modops -> Entries +newpath 705 27 moveto +722 32 743 39 761 44 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 760 47 moveto +771 47 lineto +762 41 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 760 47 moveto +771 47 lineto +762 41 lineto +closepath +stroke +end grestore + +% Modops -> Cbytegen +newpath 686 35 moveto +695 48 707 67 718 83 curveto +735 107 733 118 754 137 curveto +757 140 761 143 765 145 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 763 148 moveto +773 151 lineto +767 142 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 763 148 moveto +773 151 lineto +767 142 lineto +closepath +stroke +end grestore + +% Sign -> Term +newpath 1454 99 moveto +1489 98 1553 100 1602 119 curveto +1626 129 1637 135 1649 148 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1647 151 moveto +1656 156 lineto +1652 146 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1647 151 moveto +1656 156 lineto +1652 146 lineto +closepath +stroke +end grestore + +% Safe_typing +gsave 10 dict begin +47 85 46 18 ellipse_path +stroke +gsave 10 dict begin +13 80 moveto +(Safe_typing) +[7.68 6.24 4.08 6.24 6.96 3.84 6.96 6.96 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Mod_typing +gsave 10 dict begin +179 85 48 18 ellipse_path +stroke +gsave 10 dict begin +143 80 moveto +(Mod_typing) +[12.48 6.96 6.96 6.96 3.84 6.96 6.96 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Safe_typing -> Mod_typing +newpath 94 85 moveto +103 85 111 85 120 85 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 120 89 moveto +130 85 lineto +120 82 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 120 89 moveto +130 85 lineto +120 82 lineto +closepath +stroke +end grestore + +% Mod_typing -> Term_typing +newpath 223 93 moveto +235 95 248 98 260 100 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 260 103 moveto +270 102 lineto +261 97 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 260 103 moveto +270 102 lineto +261 97 lineto +closepath +stroke +end grestore + +% Mod_typing -> Subtyping +newpath 227 81 moveto +297 75 428 65 500 60 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 500 63 moveto +510 59 lineto +500 57 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 500 63 moveto +510 59 lineto +500 57 lineto +closepath +stroke +end grestore + +% Closure -> Environ +newpath 1085 201 moveto +1099 198 1116 194 1131 190 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1132 193 moveto +1141 188 lineto +1131 187 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1132 193 moveto +1141 188 lineto +1131 187 lineto +closepath +stroke +end grestore + +% Mod_subst -> Term +newpath 1594 155 moveto +1606 158 1618 161 1630 164 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1630 167 moveto +1640 166 lineto +1631 161 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1630 167 moveto +1640 166 lineto +1631 161 lineto +closepath +stroke +end grestore + +% Declarations +gsave 10 dict begin +1295 181 49 18 ellipse_path +stroke +gsave 10 dict begin +1259 176 moveto +(Declarations) +[10.08 6.24 6.24 3.84 6.24 4.56 6.24 3.84 3.84 6.96 6.96 5.52] +xshow +end grestore +end grestore + +% Environ -> Declarations +newpath 1210 181 moveto +1218 181 1227 181 1236 181 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1236 185 moveto +1246 181 lineto +1236 178 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1236 185 moveto +1246 181 lineto +1236 178 lineto +closepath +stroke +end grestore + +% Declarations -> Cemitcodes +newpath 1341 188 moveto +1351 189 1363 191 1373 192 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1373 195 moveto +1383 194 lineto +1374 189 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1373 195 moveto +1383 194 lineto +1374 189 lineto +closepath +stroke +end grestore + +% Declarations -> Sign +newpath 1320 165 moveto +1343 152 1375 132 1398 118 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1401 120 moveto +1407 112 lineto +1397 115 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1401 120 moveto +1407 112 lineto +1397 115 lineto +closepath +stroke +end grestore + +% Cbytecodes -> Term +newpath 1595 190 moveto +1607 188 1619 185 1630 182 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1631 185 moveto +1640 179 lineto +1629 179 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1631 185 moveto +1640 179 lineto +1629 179 lineto +closepath +stroke +end grestore +endpage +showpage +grestore +%%PageTrailer +%%EndPage: 1 +%%Trailer +%%Pages: 1 +end +restore +%%EOF diff --git a/dev/ocamlweb-doc/lex.mll b/dev/ocamlweb-doc/lex.mll new file mode 100644 index 00000000..617163e7 --- /dev/null +++ b/dev/ocamlweb-doc/lex.mll @@ -0,0 +1,81 @@ + +{ + open Lexing + open Syntax + + let chan_out = ref stdout + + let comment_depth = ref 0 + let print s = output_string !chan_out s + + exception Fin_fichier + +} + +let space = [' ' '\t' '\n'] +let letter = ['a'-'z' 'A'-'Z'] +let digit = ['0'-'9'] + +let identifier = letter (letter | digit | ['_' '\''])* +let number = digit+ +let oper = ['-' '+' '/' '*' '|' '>' '<' '=' '%' '#' '$' ':' '\\' '?' + '.' '!' '@' ]+ + +rule token = parse + | "let" {LET} + | "in" {IN} + | "match" {MATCH} + | "with" {WITH} + | "end" {END} + | "and" {AND} + | "fun" {FUN} + | "if" {IF} + | "then" {THEN} + | "else" {ELSE} + | "eval" {EVAL} + | "for" {FOR} + | "Prop" {PROP} + | "Set" {SET} + | "Type" {TYPE} + | "fix" {FIX} + | "cofix" {COFIX} + | "struct" {STRUCT} + | "as" {AS} + + | "Simpl" {SIMPL} + + | "_" {WILDCARD} + | "(" {LPAR} + | ")" {RPAR} + | "{" {LBRACE} + | "}" {RBRACE} + | "!" {BANG} + | "@" {AT} + | ":" {COLON} + | ":=" {COLONEQ} + | "." {DOT} + | "," {COMMA} + | "->" {OPER "->"} + | "=>" {RARROW} + | "|" {BAR} + | "%" {PERCENT} + + | '?' { META(ident lexbuf)} + | number { INT(Lexing.lexeme lexbuf) } + | oper { OPER(Lexing.lexeme lexbuf) } + | identifier { IDENT (Lexing.lexeme lexbuf) } + | "(*" (*"*)"*) { comment_depth := 1; + comment lexbuf; + token lexbuf } + | space+ { token lexbuf} + | eof { EOF } + +and ident = parse + | identifier { Lexing.lexeme lexbuf } + +and comment = parse + | "(*" (*"*)"*) { incr comment_depth; comment lexbuf } + | (*"(*"*) "*)" + { decr comment_depth; if !comment_depth > 0 then comment lexbuf } + | eof { raise Fin_fichier } + | _ { comment lexbuf } diff --git a/dev/ocamlweb-doc/library.dep.ps b/dev/ocamlweb-doc/library.dep.ps new file mode 100644 index 00000000..1c68240e --- /dev/null +++ b/dev/ocamlweb-doc/library.dep.ps @@ -0,0 +1,836 @@ +%!PS-Adobe-2.0 +%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) +%%For: (herbelin) Hugo Herbelin +%%Title: G +%%Pages: (atend) +%%BoundingBox: 35 35 577 207 +%%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 577 207 +%%PageOrientation: Portrait +gsave +35 35 542 172 boxprim clip newpath +36 36 translate +0 0 1 beginpage +0.6750 set_scale +0 0 translate 0 rotate +0.000 0.000 0.000 graphcolor +14.00 /Times-Roman set_font + +% States +gsave 10 dict begin +30 18 30 18 ellipse_path +stroke +gsave 10 dict begin +13 13 moveto +(States) +[7.44 4.08 6.24 3.84 6.24 5.52] +xshow +end grestore +end grestore + +% Library +gsave 10 dict begin +132 18 34 18 ellipse_path +stroke +gsave 10 dict begin +110 13 moveto +(Library) +[8.4 3.84 6.96 4.56 6.24 4.8 6.96] +xshow +end grestore +end grestore + +% States -> Library +newpath 60 18 moveto +69 18 78 18 87 18 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 87 22 moveto +97 18 lineto +87 15 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 87 22 moveto +97 18 lineto +87 15 lineto +closepath +stroke +end grestore + +% Declaremods +gsave 10 dict begin +274 18 50 18 ellipse_path +stroke +gsave 10 dict begin +236 13 moveto +(Declaremods) +[10.08 6.24 6.24 3.84 6.24 4.56 6.24 10.8 6.96 6.96 5.52] +xshow +end grestore +end grestore + +% Library -> Declaremods +newpath 167 18 moveto +181 18 197 18 213 18 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 213 22 moveto +223 18 lineto +213 15 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 213 22 moveto +223 18 lineto +213 15 lineto +closepath +stroke +end grestore + +% Nametab +gsave 10 dict begin +523 134 39 18 ellipse_path +stroke +gsave 10 dict begin +497 129 moveto +(Nametab) +[9.6 6.24 10.8 6 4.08 6.24 6.96] +xshow +end grestore +end grestore + +% Libnames +gsave 10 dict begin +642 134 41 18 ellipse_path +stroke +gsave 10 dict begin +613 129 moveto +(Libnames) +[8.4 3.84 6.96 6.96 6.24 10.8 6.24 5.52] +xshow +end grestore +end grestore + +% Nametab -> Libnames +newpath 562 134 moveto +571 134 580 134 590 134 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 590 138 moveto +600 134 lineto +590 131 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 590 138 moveto +600 134 lineto +590 131 lineto +closepath +stroke +end grestore + +% Summary +gsave 10 dict begin +642 65 40 18 ellipse_path +stroke +gsave 10 dict begin +614 60 moveto +(Summary) +[7.68 6.96 10.8 10.8 6.24 4.8 6.96] +xshow +end grestore +end grestore + +% Nametab -> Summary +newpath 547 120 moveto +565 110 589 96 608 84 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 610 87 moveto +617 79 lineto +607 81 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 610 87 moveto +617 79 lineto +607 81 lineto +closepath +stroke +end grestore + +% Nameops +gsave 10 dict begin +760 134 40 18 ellipse_path +stroke +gsave 10 dict begin +733 129 moveto +(Nameops) +[9.6 6.24 10.8 6.24 6.96 6.96 5.52] +xshow +end grestore +end grestore + +% Libnames -> Nameops +newpath 684 134 moveto +693 134 701 134 710 134 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 710 138 moveto +720 134 lineto +710 131 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 710 138 moveto +720 134 lineto +710 131 lineto +closepath +stroke +end grestore + +% Lib +gsave 10 dict begin +413 153 27 18 ellipse_path +stroke +gsave 10 dict begin +402 148 moveto +(Lib) +[8.4 3.84 6.96] +xshow +end grestore +end grestore + +% Declaremods -> Lib +newpath 315 29 moveto +325 33 336 38 344 45 curveto +359 58 383 99 399 127 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 396 129 moveto +404 136 lineto +402 126 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 396 129 moveto +404 136 lineto +402 126 lineto +closepath +stroke +end grestore + +% Global +gsave 10 dict begin +413 65 32 18 ellipse_path +stroke +gsave 10 dict begin +393 60 moveto +(Global) +[10.08 3.84 6.96 6.96 6.24 3.84] +xshow +end grestore +end grestore + +% Declaremods -> Global +newpath 311 30 moveto +331 37 355 45 375 52 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 374 55 moveto +385 55 lineto +376 49 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 374 55 moveto +385 55 lineto +376 49 lineto +closepath +stroke +end grestore + +% Libobject +gsave 10 dict begin +523 188 40 18 ellipse_path +stroke +gsave 10 dict begin +495 183 moveto +(Libobject) +[8.4 3.84 6.96 6.96 6.96 3.84 6.24 6.24 3.84] +xshow +end grestore +end grestore + +% Libobject -> Libnames +newpath 552 175 moveto +567 168 587 159 604 151 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 605 154 moveto +613 147 lineto +602 148 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 605 154 moveto +613 147 lineto +602 148 lineto +closepath +stroke +end grestore + +% Lib -> Nametab +newpath 439 148 moveto +450 146 464 144 476 142 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 477 145 moveto +486 140 lineto +476 139 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 477 145 moveto +486 140 lineto +476 139 lineto +closepath +stroke +end grestore + +% Lib -> Libobject +newpath 437 161 moveto +450 165 466 170 480 174 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 479 177 moveto +490 177 lineto +481 171 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 479 177 moveto +490 177 lineto +481 171 lineto +closepath +stroke +end grestore + +% Impargs +gsave 10 dict begin +274 126 36 18 ellipse_path +stroke +gsave 10 dict begin +251 121 moveto +(Impargs) +[4.56 10.56 6.96 6.24 4.32 6.96 5.52] +xshow +end grestore +end grestore + +% Impargs -> Lib +newpath 308 133 moveto +329 137 355 142 377 146 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 377 149 moveto +387 148 lineto +378 143 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 377 149 moveto +387 148 lineto +378 143 lineto +closepath +stroke +end grestore + +% Impargs -> Global +newpath 304 116 moveto +316 111 331 105 344 99 curveto +357 94 369 88 381 82 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 382 85 moveto +390 78 lineto +379 79 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 382 85 moveto +390 78 lineto +379 79 lineto +closepath +stroke +end grestore + +% Global -> Libnames +newpath 443 73 moveto +473 81 522 94 564 107 curveto +576 111 589 115 600 119 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 599 122 moveto +610 122 lineto +601 116 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 599 122 moveto +610 122 lineto +601 116 lineto +closepath +stroke +end grestore + +% Global -> Summary +newpath 446 65 moveto +484 65 547 65 591 65 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 591 69 moveto +601 65 lineto +591 62 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 591 69 moveto +601 65 lineto +591 62 lineto +closepath +stroke +end grestore + +% Goptions +gsave 10 dict begin +274 180 39 18 ellipse_path +stroke +gsave 10 dict begin +248 175 moveto +(Goptions) +[10.08 6.96 6.96 3.84 3.84 6.96 6.96 5.52] +xshow +end grestore +end grestore + +% Goptions -> Lib +newpath 310 173 moveto +331 169 356 164 377 160 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 378 163 moveto +387 158 lineto +377 157 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 378 163 moveto +387 158 lineto +377 157 lineto +closepath +stroke +end grestore + +% Dischargedhypsmap +gsave 10 dict begin +274 234 70 18 ellipse_path +stroke +gsave 10 dict begin +217 229 moveto +(Dischargedhypsmap) +[10.08 3.84 5.52 6 6.96 6.24 4.32 6.72 6.24 6.96 6.48 6.96 6.96 5.52 10.8 6.24 6.96] +xshow +end grestore +end grestore + +% Dischargedhypsmap -> Lib +newpath 317 220 moveto +326 216 336 212 344 207 curveto +360 197 376 185 389 175 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 392 177 moveto +397 168 lineto +387 172 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 392 177 moveto +397 168 lineto +387 172 lineto +closepath +stroke +end grestore + +% Declare +gsave 10 dict begin +132 126 35 18 ellipse_path +stroke +gsave 10 dict begin +109 121 moveto +(Declare) +[10.08 6.24 6.24 3.84 6.24 4.56 6.24] +xshow +end grestore +end grestore + +% Declare -> Impargs +newpath 168 126 moveto +186 126 208 126 228 126 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 228 130 moveto +238 126 lineto +228 123 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 228 130 moveto +238 126 lineto +228 123 lineto +closepath +stroke +end grestore + +% Declare -> Dischargedhypsmap +newpath 144 143 moveto +157 161 179 189 204 207 curveto +209 210 215 213 221 216 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 219 219 moveto +230 220 lineto +222 213 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 219 219 moveto +230 220 lineto +222 213 lineto +closepath +stroke +end grestore + +% Decl_kinds +gsave 10 dict begin +274 72 45 18 ellipse_path +stroke +gsave 10 dict begin +241 67 moveto +(Decl_kinds) +[10.08 6.24 6.24 3.84 6.96 6.96 3.84 6.96 6.96 5.52] +xshow +end grestore +end grestore + +% Declare -> Decl_kinds +newpath 161 115 moveto +181 107 209 97 232 88 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 233 91 moveto +241 84 lineto +230 85 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 233 91 moveto +241 84 lineto +230 85 lineto +closepath +stroke +end grestore +endpage +showpage +grestore +%%PageTrailer +%%EndPage: 1 +%%Trailer +%%Pages: 1 +end +restore +%%EOF diff --git a/dev/ocamlweb-doc/macros.tex b/dev/ocamlweb-doc/macros.tex new file mode 100644 index 00000000..6beacf7b --- /dev/null +++ b/dev/ocamlweb-doc/macros.tex @@ -0,0 +1,7 @@ + +% macros for coq.tex + +\newcommand{\Coq}{\textsf{Coq}} +\newcommand{\CCI}{Calculus of Inductive Constructions} + +\newcommand{\refsec}[1]{\textbf{\ref{#1}}}
\ No newline at end of file diff --git a/dev/ocamlweb-doc/parse.ml b/dev/ocamlweb-doc/parse.ml new file mode 100644 index 00000000..e537b1f2 --- /dev/null +++ b/dev/ocamlweb-doc/parse.ml @@ -0,0 +1,183 @@ + +open Ast + +type assoc = L | R | N + +let level = function + | "--" -> 70,L + | "=" -> 70,N + | "+" -> 60,L + | "++" -> 60,R + | "+++" -> 60,R + | "-" -> 60,L + | "*" -> 50,L + | "/" -> 50,L + | "**" -> 40,R + | ":" -> (100,R) + | "->" -> (90,R) + | s -> failwith ("unknowm operator '"^s^"'") + +let fixity = function + | "--" -> [L] + | "=" -> [N] + | ("+"|"-"|"*"|"/") -> [L;N] + | "++" -> [R] + | _ -> [L;N;R] + +let ground_oper = function + ("-"|"+") -> true + | _ -> false + +let is_prefix op = List.mem L (fixity op) +let is_infix op = List.mem N (fixity op) +let is_postfix op = List.mem R (fixity op) + +let mk_inf op t1 t2 = + if not (is_infix op) then failwith (op^" not infix"); + Infix(op,t1,t2) + +let mk_post op t = + if not (is_postfix op) then failwith (op^" not postfix"); + Postfix(op,t) + + +(* Pb avec ground_oper: pas de diff entre -1 et -(1) *) +let mk_pre op t = + if not (is_prefix op) then failwith (op^" not prefix"); + if ground_oper op then + match t with + | Int i -> Int (op^i) + | _ -> Prefix(op,t) + else Prefix(op,t) + +(* teste si on peut reduire op suivi d'un op de niveau (n,a) + si la reponse est false, c'est que l'op (n,a) doit se reduire + avant *) +let red_left_op (nl,al) (nr,ar) = + if nl < nr then true + else + if nl = nr then + match al,ar with + | (L|N), L -> true + | R, (R|N) -> false + | R, L -> failwith "conflit d'assoc: ambigu" + | (L|N), (R|N) -> failwith "conflit d'assoc: blocage" + else false + + +type level = int * assoc +type stack = + | PrefixOper of string list + | Term of constr_ast * stack + | Oper of string list * string * constr_ast * stack + +let rec str_ast = function + | Infix(op,t1,t2) -> str_ast t1 ^ " " ^ op ^ " " ^ str_ast t2 + | Postfix(op,t) -> str_ast t ^ " " ^ op + | Prefix(op,t) -> op ^ " " ^ str_ast t + | _ -> "_" + +let rec str_stack = function + | PrefixOper ops -> String.concat " " (List.rev ops) + | Term (t,s) -> str_stack s ^ " (" ^ str_ast t ^ ")" + | Oper(ops,lop,t,s) -> + str_stack (Term(t,s)) ^ " " ^ lop ^ " " ^ + String.concat " " (List.rev ops) + +let pps s = prerr_endline (str_stack s) +let err s stk = failwith (s^": "^str_stack stk) + + +let empty = PrefixOper [] + +let check_fixity_term stk = + match stk with + Term _ -> err "2 termes successifs" stk + | _ -> () + +let shift_term t stk = + check_fixity_term stk; + Term(t,stk) + +let shift_oper op stk = + match stk with + | Oper(ops,lop,t,s) -> Oper(op::ops,lop,t,s) + | Term(t,s) -> Oper([],op,t,s) + | PrefixOper ops -> PrefixOper (op::ops) + +let is_reducible lv stk = + match stk with + | Oper([],iop,_,_) -> red_left_op (level iop) lv + | Oper(op::_,_,_,_) -> red_left_op (level op) lv + | PrefixOper(op::_) -> red_left_op (level op) lv + | _ -> false + +let reduce_head (t,stk) = + match stk with + | Oper([],iop,t1,s) -> + (Infix(iop,t1,t), s) + | Oper(op::ops,lop,t',s) -> + (mk_pre op t, Oper(ops,lop,t',s)) + | PrefixOper(op::ops) -> + (Prefix(op,t), PrefixOper ops) + | _ -> assert false + +let rec reduce_level lv (t,s) = + if is_reducible lv s then reduce_level lv (reduce_head (t, s)) + else (t, s) + +let reduce_post op (t,s) = + let (t',s') = reduce_level (level op) (t,s) in + (mk_post op t', s') + +let reduce_posts stk = + match stk with + Oper(ops,iop,t,s) -> + let pts1 = reduce_post iop (t,s) in + List.fold_right reduce_post ops pts1 + | Term(t,s) -> (t,s) + | PrefixOper _ -> failwith "reduce_posts" + + +let shift_infix op stk = + let (t,s) = reduce_level (level op) (reduce_posts stk) in + Oper([],op,t,s) + +let is_better_infix op stk = + match stk with + | Oper(ops,iop,t,s) -> + is_postfix iop && + List.for_all is_postfix ops && + (not (is_prefix op) || red_left_op (level iop) (level op)) + | Term _ -> false + | _ -> assert false + +let parse_oper op stk = + match stk with + | PrefixOper _ -> + if is_prefix op then shift_oper op stk else failwith "prefix_oper" + | Oper _ -> + if is_infix op then + if is_better_infix op stk then shift_infix op stk + else shift_oper op stk + else if is_prefix op then shift_oper op stk + else if is_postfix op then + let (t,s) = reduce_post op (reduce_posts stk) in + Term(t,s) + else assert false + | Term(t,s) -> + if is_infix op then shift_infix op stk + else if is_postfix op then + let (t2,s2) = reduce_post op (t,s) in Term(t2,s2) + else failwith "infix/postfix" + +let parse_term = shift_term + +let rec close_stack stk = + match stk with + Term(t,PrefixOper []) -> t + | PrefixOper _ -> failwith "expression sans atomes" + | _ -> + let (t,s) = reduce_head (reduce_posts stk) in + close_stack (Term(t,s)) + diff --git a/dev/ocamlweb-doc/parsing.dep.ps b/dev/ocamlweb-doc/parsing.dep.ps new file mode 100644 index 00000000..723d8c69 --- /dev/null +++ b/dev/ocamlweb-doc/parsing.dep.ps @@ -0,0 +1,1115 @@ +%!PS-Adobe-2.0 +%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) +%%For: (herbelin) Hugo Herbelin +%%Title: G +%%Pages: (atend) +%%BoundingBox: 35 35 577 314 +%%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 577 314 +%%PageOrientation: Portrait +gsave +35 35 542 279 boxprim clip newpath +36 36 translate +0 0 1 beginpage +0.6027 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 +557 280 27 18 ellipse_path +stroke +gsave 10 dict begin +543 275 moveto +(Pcoq) +[7.68 6.24 6.96 6.96] +xshow +end grestore +end grestore + +% Extend +gsave 10 dict begin +664 226 33 18 ellipse_path +stroke +gsave 10 dict begin +643 221 moveto +(Extend) +[8.4 6.96 3.84 6.24 6.96 6.96] +xshow +end grestore +end grestore + +% Pcoq -> Extend +newpath 579 269 moveto +593 261 613 252 630 243 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 632 246 moveto +639 238 lineto +629 240 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 632 246 moveto +639 238 lineto +629 240 lineto +closepath +stroke +end grestore + +% Ast +gsave 10 dict begin +764 172 27 18 ellipse_path +stroke +gsave 10 dict begin +753 167 moveto +(Ast) +[10.08 5.28 3.84] +xshow +end grestore +end grestore + +% Extend -> Ast +newpath 688 213 moveto +701 206 719 196 734 188 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 736 191 moveto +743 183 lineto +733 185 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 736 191 moveto +743 183 lineto +733 185 lineto +closepath +stroke +end grestore + +% Lexer +gsave 10 dict begin +764 226 29 18 ellipse_path +stroke +gsave 10 dict begin +747 221 moveto +(Lexer) +[8.4 5.76 6.48 6.24 4.56] +xshow +end grestore +end grestore + +% Extend -> Lexer +newpath 698 226 moveto +706 226 715 226 724 226 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 724 230 moveto +734 226 lineto +724 223 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 724 230 moveto +734 226 lineto +724 223 lineto +closepath +stroke +end grestore + +% Termast +gsave 10 dict begin +557 172 35 18 ellipse_path +stroke +gsave 10 dict begin +534 167 moveto +(Termast) +[7.2 6.24 4.8 10.8 6.24 5.28 3.84] +xshow +end grestore +end grestore + +% Termast -> Ast +newpath 593 172 moveto +630 172 689 172 727 172 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 727 176 moveto +737 172 lineto +727 169 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 727 176 moveto +737 172 lineto +727 169 lineto +closepath +stroke +end grestore + +% Coqast +gsave 10 dict begin +863 172 32 18 ellipse_path +stroke +gsave 10 dict begin +843 167 moveto +(Coqast) +[9.36 6.96 6.96 6.24 5.28 3.84] +xshow +end grestore +end grestore + +% Ast -> Coqast +newpath 791 172 moveto +800 172 810 172 820 172 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 820 176 moveto +830 172 lineto +820 169 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 820 176 moveto +830 172 lineto +820 169 lineto +closepath +stroke +end grestore + +% Tactic_printer +gsave 10 dict begin +53 126 52 18 ellipse_path +stroke +gsave 10 dict begin +13 121 moveto +(Tactic_printer) +[7.44 6.24 6.24 3.84 3.84 6.24 6.96 6.96 4.8 3.84 6.96 3.84 6.24 4.56] +xshow +end grestore +end grestore + +% Pptactic +gsave 10 dict begin +178 126 36 18 ellipse_path +stroke +gsave 10 dict begin +155 121 moveto +(Pptactic) +[7.68 6.96 4.08 6.24 6.24 3.84 3.84 6.24] +xshow +end grestore +end grestore + +% Tactic_printer -> Pptactic +newpath 106 126 moveto +114 126 123 126 132 126 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 132 130 moveto +142 126 lineto +132 123 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 132 130 moveto +142 126 lineto +132 123 lineto +closepath +stroke +end grestore + +% Printer +gsave 10 dict begin +289 72 32 18 ellipse_path +stroke +gsave 10 dict begin +269 67 moveto +(Printer) +[7.68 4.8 3.84 6.96 3.84 6.24 4.56] +xshow +end grestore +end grestore + +% Pptactic -> Printer +newpath 204 113 moveto +219 105 238 96 255 88 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 256 91 moveto +264 84 lineto +253 85 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 256 91 moveto +264 84 lineto +253 85 lineto +closepath +stroke +end grestore + +% Search +gsave 10 dict begin +178 72 32 18 ellipse_path +stroke +gsave 10 dict begin +159 67 moveto +(Search) +[7.68 6.24 6.24 4.56 6 6.96] +xshow +end grestore +end grestore + +% Search -> Printer +newpath 210 72 moveto +221 72 234 72 246 72 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 246 76 moveto +256 72 lineto +246 69 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 246 76 moveto +256 72 lineto +246 69 lineto +closepath +stroke +end grestore + +% Printer -> Termast +newpath 316 62 moveto +355 48 430 30 484 58 curveto +518 77 538 117 548 144 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 545 146 moveto +552 154 lineto +552 143 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 545 146 moveto +552 154 lineto +552 143 lineto +closepath +stroke +end grestore + +% Esyntax +gsave 10 dict begin +557 226 36 18 ellipse_path +stroke +gsave 10 dict begin +533 221 moveto +(Esyntax) +[8.4 5.52 6.96 6.96 4.08 6.24 6.96] +xshow +end grestore +end grestore + +% Printer -> Esyntax +newpath 322 71 moveto +370 70 460 72 484 91 curveto +489 95 516 193 520 197 curveto +527 204 532 203 538 204 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 536 207 moveto +547 208 lineto +539 201 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 536 207 moveto +547 208 lineto +539 201 lineto +closepath +stroke +end grestore + +% Ppconstr +gsave 10 dict begin +424 388 37 18 ellipse_path +stroke +gsave 10 dict begin +399 383 moveto +(Ppconstr) +[7.68 6.96 6.24 6.96 6.96 5.28 3.84 4.56] +xshow +end grestore +end grestore + +% Printer -> Ppconstr +newpath 292 90 moveto +300 147 329 319 364 361 curveto +369 367 375 371 382 375 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 380 378 moveto +391 379 lineto +383 372 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 380 378 moveto +391 379 lineto +383 372 lineto +closepath +stroke +end grestore + +% Esyntax -> Extend +newpath 594 226 moveto +602 226 611 226 620 226 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 620 230 moveto +630 226 lineto +620 223 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 620 230 moveto +630 226 lineto +620 223 lineto +closepath +stroke +end grestore + +% Ppconstr -> Pcoq +newpath 454 377 moveto +464 373 475 368 484 361 curveto +506 345 526 322 540 304 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 543 306 moveto +546 296 lineto +537 302 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 543 306 moveto +546 296 lineto +537 302 lineto +closepath +stroke +end grestore + +% Prettyp +gsave 10 dict begin +178 18 33 18 ellipse_path +stroke +gsave 10 dict begin +158 13 moveto +(Prettyp) +[7.68 4.56 6 3.84 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Prettyp -> Printer +newpath 203 30 moveto +218 38 238 47 255 55 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 254 58 moveto +264 60 lineto +257 52 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 254 58 moveto +264 60 lineto +257 52 lineto +closepath +stroke +end grestore + +% Printmod +gsave 10 dict begin +289 18 39 18 ellipse_path +stroke +gsave 10 dict begin +263 13 moveto +(Printmod) +[7.68 4.8 3.84 6.96 3.84 10.8 6.96 6.96] +xshow +end grestore +end grestore + +% Prettyp -> Printmod +newpath 211 18 moveto +220 18 230 18 240 18 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 240 22 moveto +250 18 lineto +240 15 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 240 22 moveto +250 18 lineto +240 15 lineto +closepath +stroke +end grestore + +% G_zsyntax +gsave 10 dict begin +424 172 43 18 ellipse_path +stroke +gsave 10 dict begin +393 167 moveto +(G_zsyntax) +[10.08 6.96 6.24 5.52 6.96 6.96 4.08 6.24 6.96] +xshow +end grestore +end grestore + +% G_zsyntax -> Pcoq +newpath 458 183 moveto +467 188 476 193 484 199 curveto +507 218 501 233 520 253 curveto +523 256 526 259 530 261 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 528 264 moveto +538 267 lineto +532 258 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 528 264 moveto +538 267 lineto +532 258 lineto +closepath +stroke +end grestore + +% G_zsyntax -> Termast +newpath 468 172 moveto +482 172 497 172 511 172 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 511 176 moveto +521 172 lineto +511 169 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 511 176 moveto +521 172 lineto +511 169 lineto +closepath +stroke +end grestore + +% G_zsyntax -> Esyntax +newpath 455 185 moveto +474 193 499 203 520 211 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 518 214 moveto +529 215 lineto +521 208 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 518 214 moveto +529 215 lineto +521 208 lineto +closepath +stroke +end grestore + +% G_string_syntax +gsave 10 dict begin +424 280 59 18 ellipse_path +stroke +gsave 10 dict begin +377 275 moveto +(G_string_syntax) +[10.08 6.96 5.28 3.84 4.8 3.84 6.96 6.96 6.96 5.52 6.96 6.96 4.08 6.24 6.96] +xshow +end grestore +end grestore + +% G_string_syntax -> Pcoq +newpath 484 280 moveto +496 280 509 280 520 280 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 520 284 moveto +530 280 lineto +520 277 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 520 284 moveto +530 280 lineto +520 277 lineto +closepath +stroke +end grestore + +% G_string_syntax -> Esyntax +newpath 460 266 moveto +478 258 501 249 520 242 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 521 245 moveto +529 238 lineto +518 239 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 521 245 moveto +529 238 lineto +518 239 lineto +closepath +stroke +end grestore + +% G_rsyntax +gsave 10 dict begin +424 118 42 18 ellipse_path +stroke +gsave 10 dict begin +394 113 moveto +(G_rsyntax) +[10.08 6.96 4.56 5.52 6.96 6.96 4.08 6.24 6.96] +xshow +end grestore +end grestore + +% G_rsyntax -> Pcoq +newpath 459 128 moveto +468 132 477 138 484 145 curveto +518 183 491 213 520 253 curveto +523 256 526 259 529 262 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 527 265 moveto +537 268 lineto +531 259 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 527 265 moveto +537 268 lineto +531 259 lineto +closepath +stroke +end grestore + +% G_rsyntax -> Termast +newpath 455 131 moveto +474 139 499 149 520 157 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 518 160 moveto +529 161 lineto +521 154 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 518 160 moveto +529 161 lineto +521 154 lineto +closepath +stroke +end grestore + +% G_rsyntax -> Esyntax +newpath 457 129 moveto +467 133 476 139 484 145 curveto +507 164 501 179 520 199 curveto +522 201 525 203 527 205 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 525 208 moveto +535 212 lineto +530 203 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 525 208 moveto +535 212 lineto +530 203 lineto +closepath +stroke +end grestore + +% G_natsyntax +gsave 10 dict begin +424 226 48 18 ellipse_path +stroke +gsave 10 dict begin +388 221 moveto +(G_natsyntax) +[10.08 6.96 6.96 6.24 3.84 5.52 6.96 6.96 4.08 6.24 6.96] +xshow +end grestore +end grestore + +% G_natsyntax -> Pcoq +newpath 457 239 moveto +478 248 504 259 525 266 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 523 269 moveto +534 270 lineto +526 263 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 523 269 moveto +534 270 lineto +526 263 lineto +closepath +stroke +end grestore + +% G_natsyntax -> Termast +newpath 457 213 moveto +476 205 500 195 520 187 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 521 190 moveto +529 183 lineto +518 184 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 521 190 moveto +529 183 lineto +518 184 lineto +closepath +stroke +end grestore + +% G_natsyntax -> Esyntax +newpath 473 226 moveto +485 226 498 226 510 226 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 510 230 moveto +520 226 lineto +510 223 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 510 230 moveto +520 226 lineto +510 223 lineto +closepath +stroke +end grestore + +% G_ascii_syntax +gsave 10 dict begin +424 334 56 18 ellipse_path +stroke +gsave 10 dict begin +380 329 moveto +(G_ascii_syntax) +[10.08 6.96 6.24 5.52 6.24 3.84 3.84 6.96 5.52 6.96 6.96 4.08 6.24 6.96] +xshow +end grestore +end grestore + +% G_ascii_syntax -> Pcoq +newpath 459 320 moveto +479 311 504 301 525 293 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 526 296 moveto +534 289 lineto +523 290 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 526 296 moveto +534 289 lineto +523 290 lineto +closepath +stroke +end grestore + +% G_ascii_syntax -> Esyntax +newpath 462 321 moveto +470 317 478 312 484 307 curveto +507 288 501 273 520 253 curveto +522 251 524 249 527 247 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 529 250 moveto +535 241 lineto +525 244 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 529 250 moveto +535 241 lineto +525 244 lineto +closepath +stroke +end grestore + +% Egrammar +gsave 10 dict begin +424 442 43 18 ellipse_path +stroke +gsave 10 dict begin +394 437 moveto +(Egrammar) +[8.4 7.2 4.56 6.24 10.8 10.8 6.24 4.56] +xshow +end grestore +end grestore + +% Egrammar -> Pcoq +newpath 458 431 moveto +467 427 477 422 484 415 curveto +516 385 537 337 548 308 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 551 309 moveto +551 298 lineto +545 307 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 551 309 moveto +551 298 lineto +545 307 lineto +closepath +stroke +end grestore +endpage +showpage +grestore +%%PageTrailer +%%EndPage: 1 +%%Trailer +%%Pages: 1 +end +restore +%%EOF diff --git a/dev/ocamlweb-doc/preamble.tex b/dev/ocamlweb-doc/preamble.tex new file mode 100644 index 00000000..2cd21f02 --- /dev/null +++ b/dev/ocamlweb-doc/preamble.tex @@ -0,0 +1,8 @@ +\documentclass[11pt]{article} +\usepackage[latin1]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{ocamlweb} +\pagestyle{ocamlweb} +\usepackage{fullpage} +\usepackage{epsfig} +\begin{document} diff --git a/dev/ocamlweb-doc/pretyping.dep.ps b/dev/ocamlweb-doc/pretyping.dep.ps new file mode 100644 index 00000000..02d1b8b5 --- /dev/null +++ b/dev/ocamlweb-doc/pretyping.dep.ps @@ -0,0 +1,1259 @@ +%!PS-Adobe-2.0 +%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) +%%For: (herbelin) Hugo Herbelin +%%Title: G +%%Pages: (atend) +%%BoundingBox: 35 35 577 146 +%%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 577 146 +%%PageOrientation: Portrait +gsave +35 35 542 111 boxprim clip newpath +36 36 translate +0 0 1 beginpage +0.3600 set_scale +0 0 translate 0 rotate +0.000 0.000 0.000 graphcolor +14.00 /Times-Roman set_font + +% Unification +gsave 10 dict begin +610 118 45 18 ellipse_path +stroke +gsave 10 dict begin +577 113 moveto +(Unification) +[9.6 6.96 3.84 4.8 3.84 6.24 6.24 3.84 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Evarutil +gsave 10 dict begin +728 72 36 18 ellipse_path +stroke +gsave 10 dict begin +705 67 moveto +(Evarutil) +[8.4 6.72 6.24 4.8 6.96 3.84 3.84 3.84] +xshow +end grestore +end grestore + +% Unification -> Evarutil +newpath 643 105 moveto +657 99 674 93 689 87 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 691 90 moveto +699 83 lineto +688 83 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 691 90 moveto +699 83 lineto +688 83 lineto +closepath +stroke +end grestore + +% Pattern +gsave 10 dict begin +728 210 33 18 ellipse_path +stroke +gsave 10 dict begin +708 205 moveto +(Pattern) +[7.44 6.24 3.84 3.84 6.24 4.8 6.96] +xshow +end grestore +end grestore + +% Unification -> Pattern +newpath 631 134 moveto +650 150 680 173 701 189 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 699 192 moveto +709 195 lineto +703 186 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 699 192 moveto +709 195 lineto +703 186 lineto +closepath +stroke +end grestore + +% Retyping +gsave 10 dict begin +839 118 38 18 ellipse_path +stroke +gsave 10 dict begin +813 113 moveto +(Retyping) +[9.12 6 3.84 6.96 6.96 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Unification -> Retyping +newpath 656 118 moveto +695 118 750 118 790 118 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 790 122 moveto +800 118 lineto +790 115 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 790 122 moveto +800 118 lineto +790 115 lineto +closepath +stroke +end grestore + +% Typing +gsave 10 dict begin +839 64 32 18 ellipse_path +stroke +gsave 10 dict begin +819 59 moveto +(Typing) +[6.96 6.96 6.96 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Evarutil -> Typing +newpath 764 69 moveto +775 68 786 67 797 67 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 797 70 moveto +807 66 lineto +797 64 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 797 70 moveto +807 66 lineto +797 64 lineto +closepath +stroke +end grestore + +% Rawterm +gsave 10 dict begin +1109 110 39 18 ellipse_path +stroke +gsave 10 dict begin +1083 105 moveto +(Rawterm) +[9.36 5.76 10.08 3.84 6.24 4.8 10.8] +xshow +end grestore +end grestore + +% Pattern -> Rawterm +newpath 759 216 moveto +816 226 939 239 1024 191 curveto +1049 176 1038 155 1060 138 curveto +1069 131 1077 130 1084 129 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1085 132 moveto +1094 127 lineto +1084 126 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1085 132 moveto +1094 127 lineto +1084 126 lineto +closepath +stroke +end grestore + +% Inductiveops +gsave 10 dict begin +1109 164 49 18 ellipse_path +stroke +gsave 10 dict begin +1073 159 moveto +(Inductiveops) +[4.56 6.96 6.96 6.96 6.24 3.84 3.84 6.48 6.24 6.96 6.96 5.52] +xshow +end grestore +end grestore + +% Retyping -> Inductiveops +newpath 878 120 moveto +915 122 974 126 1024 137 curveto +1037 139 1051 144 1064 148 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1063 151 moveto +1074 151 lineto +1065 145 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1063 151 moveto +1074 151 lineto +1065 145 lineto +closepath +stroke +end grestore + +% Pretype_errors +gsave 10 dict begin +969 72 54 18 ellipse_path +stroke +gsave 10 dict begin +927 67 moveto +(Pretype_errors) +[7.68 4.56 6 3.84 6.96 6.96 6.24 6.96 6.24 5.04 4.56 6.96 4.56 5.52] +xshow +end grestore +end grestore + +% Typing -> Pretype_errors +newpath 871 66 moveto +881 67 893 68 905 68 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 905 71 moveto +915 69 lineto +905 65 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 905 71 moveto +915 69 lineto +905 65 lineto +closepath +stroke +end grestore + +% Pretype_errors -> Inductiveops +newpath 998 87 moveto +1007 92 1016 98 1024 104 curveto +1042 116 1043 124 1060 137 curveto +1063 139 1067 142 1071 144 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1070 147 moveto +1080 149 lineto +1073 141 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1070 147 moveto +1080 149 lineto +1073 141 lineto +closepath +stroke +end grestore + +% Pretype_errors -> Rawterm +newpath 1011 84 moveto +1029 88 1048 94 1065 98 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1064 101 moveto +1075 101 lineto +1066 95 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1064 101 moveto +1075 101 lineto +1066 95 lineto +closepath +stroke +end grestore + +% Tacred +gsave 10 dict begin +728 18 32 18 ellipse_path +stroke +gsave 10 dict begin +709 13 moveto +(Tacred) +[7.44 6.24 6.24 4.56 6.24 6.96] +xshow +end grestore +end grestore + +% Tacred -> Retyping +newpath 748 32 moveto +754 36 759 41 764 45 curveto +783 63 782 73 800 91 curveto +802 93 805 95 808 97 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 806 100 moveto +816 103 lineto +810 94 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 806 100 moveto +816 103 lineto +810 94 lineto +closepath +stroke +end grestore + +% Tacred -> Typing +newpath 754 29 moveto +769 35 787 43 803 49 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 802 53 moveto +813 53 lineto +805 46 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 802 53 moveto +813 53 lineto +805 46 lineto +closepath +stroke +end grestore + +% Cbv +gsave 10 dict begin +1246 41 27 18 ellipse_path +stroke +gsave 10 dict begin +1234 36 moveto +(Cbv) +[9.36 6.48 6.96] +xshow +end grestore +end grestore + +% Tacred -> Cbv +newpath 760 19 moveto +852 23 1111 35 1209 40 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1209 44 moveto +1219 40 lineto +1209 37 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1209 44 moveto +1219 40 lineto +1209 37 lineto +closepath +stroke +end grestore + +% Evd +gsave 10 dict begin +1361 110 27 18 ellipse_path +stroke +gsave 10 dict begin +1349 105 moveto +(Evd) +[8.4 6.96 6.96] +xshow +end grestore +end grestore + +% Cbv -> Evd +newpath 1266 53 moveto +1284 64 1312 80 1332 93 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1331 96 moveto +1341 98 lineto +1334 90 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1331 96 moveto +1341 98 lineto +1334 90 lineto +closepath +stroke +end grestore + +% Reductionops +gsave 10 dict begin +1246 164 51 18 ellipse_path +stroke +gsave 10 dict begin +1207 159 moveto +(Reductionops) +[9.12 6.24 6.96 6.96 6.24 3.84 3.84 6.96 6.96 6.96 6.96 5.52] +xshow +end grestore +end grestore + +% Inductiveops -> Reductionops +newpath 1158 164 moveto +1167 164 1175 164 1184 164 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1184 168 moveto +1194 164 lineto +1184 161 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1184 168 moveto +1194 164 lineto +1184 161 lineto +closepath +stroke +end grestore + +% Reductionops -> Evd +newpath 1277 150 moveto +1294 142 1313 133 1330 125 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1331 128 moveto +1339 121 lineto +1328 122 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1331 128 moveto +1339 121 lineto +1328 122 lineto +closepath +stroke +end grestore + +% Termops +gsave 10 dict begin +1462 110 37 18 ellipse_path +stroke +gsave 10 dict begin +1437 105 moveto +(Termops) +[7.2 6.24 4.8 10.8 6.96 6.96 5.52] +xshow +end grestore +end grestore + +% Evd -> Termops +newpath 1388 110 moveto +1396 110 1405 110 1414 110 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1414 114 moveto +1424 110 lineto +1414 107 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1414 114 moveto +1424 110 lineto +1414 107 lineto +closepath +stroke +end grestore + +% Recordops +gsave 10 dict begin +485 24 43 18 ellipse_path +stroke +gsave 10 dict begin +455 19 moveto +(Recordops) +[9.12 6.24 6.24 6.96 4.32 6.96 6.96 6.96 5.52] +xshow +end grestore +end grestore + +% Classops +gsave 10 dict begin +610 20 38 18 ellipse_path +stroke +gsave 10 dict begin +584 15 moveto +(Classops) +[9.36 3.84 6.24 5.52 5.52 6.96 6.96 5.52] +xshow +end grestore +end grestore + +% Recordops -> Classops +newpath 528 23 moveto +538 22 550 22 561 22 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 561 25 moveto +571 21 lineto +561 19 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 561 25 moveto +571 21 lineto +561 19 lineto +closepath +stroke +end grestore + +% Classops -> Tacred +newpath 649 19 moveto +661 19 674 19 686 19 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 686 23 moveto +696 19 lineto +686 16 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 686 23 moveto +696 19 lineto +686 16 lineto +closepath +stroke +end grestore + +% Rawterm -> Evd +newpath 1148 110 moveto +1196 110 1277 110 1324 110 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1324 114 moveto +1334 110 lineto +1324 107 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1324 114 moveto +1334 110 lineto +1324 107 lineto +closepath +stroke +end grestore + +% Pretyping +gsave 10 dict begin +40 183 40 18 ellipse_path +stroke +gsave 10 dict begin +13 178 moveto +(Pretyping) +[7.68 4.56 6 3.84 6.96 6.96 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Pretyping -> Pattern +newpath 78 189 moveto +121 194 191 202 251 202 curveto +251 202 251 202 485 202 curveto +556 202 636 205 685 208 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 685 212 moveto +695 208 lineto +685 205 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 685 212 moveto +695 208 lineto +685 205 lineto +closepath +stroke +end grestore + +% Cases +gsave 10 dict begin +146 64 30 18 ellipse_path +stroke +gsave 10 dict begin +129 59 moveto +(Cases) +[9.36 6.24 5.52 6.24 5.52] +xshow +end grestore +end grestore + +% Pretyping -> Cases +newpath 53 166 moveto +68 147 93 115 116 91 curveto +118 89 119 88 121 86 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 124 88 moveto +129 79 lineto +119 83 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 124 88 moveto +129 79 lineto +119 83 lineto +closepath +stroke +end grestore + +% Detyping +gsave 10 dict begin +969 164 39 18 ellipse_path +stroke +gsave 10 dict begin +942 159 moveto +(Detyping) +[10.08 6 3.84 6.96 6.96 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Pretyping -> Detyping +newpath 78 177 moveto +121 172 191 164 251 164 curveto +251 164 251 164 728 164 curveto +794 164 870 164 919 164 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 919 168 moveto +929 164 lineto +919 161 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 919 168 moveto +929 164 lineto +919 161 lineto +closepath +stroke +end grestore + +% Indrec +gsave 10 dict begin +251 271 31 18 ellipse_path +stroke +gsave 10 dict begin +233 266 moveto +(Indrec) +[4.56 6.96 6.96 4.56 6.24 6.24] +xshow +end grestore +end grestore + +% Pretyping -> Indrec +newpath 69 195 moveto +83 202 101 209 116 216 curveto +150 230 188 246 216 257 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 214 260 moveto +225 261 lineto +217 254 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 214 260 moveto +225 261 lineto +217 254 lineto +closepath +stroke +end grestore + +% Coercion +gsave 10 dict begin +251 67 39 18 ellipse_path +stroke +gsave 10 dict begin +225 62 moveto +(Coercion) +[9.36 6.96 6.24 4.56 6.24 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Cases -> Coercion +newpath 176 65 moveto +184 65 193 66 202 66 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 202 70 moveto +212 66 lineto +202 63 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 202 70 moveto +212 66 lineto +202 63 lineto +closepath +stroke +end grestore + +% Detyping -> Inductiveops +newpath 1009 164 moveto +1022 164 1036 164 1050 164 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1050 168 moveto +1060 164 lineto +1050 161 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1050 168 moveto +1060 164 lineto +1050 161 lineto +closepath +stroke +end grestore + +% Detyping -> Rawterm +newpath 999 152 moveto +1020 144 1047 133 1069 125 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1070 128 moveto +1079 122 lineto +1068 122 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1070 128 moveto +1079 122 lineto +1068 122 lineto +closepath +stroke +end grestore + +% Indrec -> Inductiveops +newpath 281 276 moveto +325 283 412 294 485 294 curveto +485 294 485 294 839 294 curveto +937 294 1036 225 1082 188 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1085 190 moveto +1090 181 lineto +1080 185 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1085 190 moveto +1090 181 lineto +1080 185 lineto +closepath +stroke +end grestore + +% Matching +gsave 10 dict begin +610 248 40 18 ellipse_path +stroke +gsave 10 dict begin +582 243 moveto +(Matching) +[12.48 6.24 3.84 6 6.96 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Matching -> Pattern +newpath 643 237 moveto +658 232 675 227 689 222 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 690 225 moveto +699 219 lineto +688 219 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 690 225 moveto +699 219 lineto +688 219 lineto +closepath +stroke +end grestore + +% Matching -> Reductionops +newpath 650 250 moveto +696 253 773 256 839 256 curveto +839 256 839 256 969 256 curveto +1059 256 1159 212 1210 184 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1212 187 moveto +1219 179 lineto +1209 181 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1212 187 moveto +1219 179 lineto +1209 181 lineto +closepath +stroke +end grestore + +% Evarconv +gsave 10 dict begin +366 67 40 18 ellipse_path +stroke +gsave 10 dict begin +339 62 moveto +(Evarconv) +[8.4 6.72 6.24 4.56 6.24 6.96 6.48 6.96] +xshow +end grestore +end grestore + +% Evarconv -> Evarutil +newpath 406 68 moveto +474 69 610 71 682 72 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 682 76 moveto +692 72 lineto +682 69 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 682 76 moveto +692 72 lineto +682 69 lineto +closepath +stroke +end grestore + +% Evarconv -> Recordops +newpath 397 56 moveto +411 51 428 45 442 39 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 443 42 moveto +452 36 lineto +441 36 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 443 42 moveto +452 36 lineto +441 36 lineto +closepath +stroke +end grestore + +% Coercion -> Evarconv +newpath 290 67 moveto +299 67 307 67 316 67 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 316 71 moveto +326 67 lineto +316 64 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 316 71 moveto +326 67 lineto +316 64 lineto +closepath +stroke +end grestore + +% Clenv +gsave 10 dict begin +146 118 30 18 ellipse_path +stroke +gsave 10 dict begin +129 113 moveto +(Clenv) +[9.36 3.84 6.24 6.48 6.96] +xshow +end grestore +end grestore + +% Clenv -> Unification +newpath 176 118 moveto +252 118 455 118 554 118 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 554 122 moveto +564 118 lineto +554 115 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 554 122 moveto +564 118 lineto +554 115 lineto +closepath +stroke +end grestore + +% Clenv -> Coercion +newpath 170 107 moveto +183 100 200 93 215 85 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 217 88 moveto +224 80 lineto +214 82 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 217 88 moveto +224 80 lineto +214 82 lineto +closepath +stroke +end grestore +endpage +showpage +grestore +%%PageTrailer +%%EndPage: 1 +%%Trailer +%%Pages: 1 +end +restore +%%EOF diff --git a/dev/ocamlweb-doc/proofs.dep.ps b/dev/ocamlweb-doc/proofs.dep.ps new file mode 100644 index 00000000..0e78f422 --- /dev/null +++ b/dev/ocamlweb-doc/proofs.dep.ps @@ -0,0 +1,638 @@ +%!PS-Adobe-2.0 +%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) +%%For: (herbelin) Hugo Herbelin +%%Title: G +%%Pages: (atend) +%%BoundingBox: 35 35 577 136 +%%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 577 136 +%%PageOrientation: Portrait +gsave +35 35 542 101 boxprim clip newpath +36 36 translate +0 0 1 beginpage +0.6923 set_scale +0 0 translate 0 rotate +0.000 0.000 0.000 graphcolor +14.00 /Times-Roman set_font + +% Tactic_debug +gsave 10 dict begin +163 72 51 18 ellipse_path +stroke +gsave 10 dict begin +125 67 moveto +(Tactic_debug) +[7.44 6.24 6.24 3.84 3.84 6.24 6.96 6.96 6.24 6.96 6.96 6.96] +xshow +end grestore +end grestore + +% Refiner +gsave 10 dict begin +287 72 34 18 ellipse_path +stroke +gsave 10 dict begin +266 67 moveto +(Refiner) +[9.12 6.24 4.8 3.84 6.96 6.24 4.56] +xshow +end grestore +end grestore + +% Tactic_debug -> Refiner +newpath 214 72 moveto +223 72 233 72 243 72 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 243 76 moveto +253 72 lineto +243 69 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 243 76 moveto +253 72 lineto +243 69 lineto +closepath +stroke +end grestore + +% Logic +gsave 10 dict begin +390 72 30 18 ellipse_path +stroke +gsave 10 dict begin +373 67 moveto +(Logic) +[8.4 6.96 6.96 3.84 6.24] +xshow +end grestore +end grestore + +% Refiner -> Logic +newpath 321 72 moveto +330 72 340 72 350 72 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 350 76 moveto +360 72 lineto +350 69 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 350 76 moveto +360 72 lineto +350 69 lineto +closepath +stroke +end grestore + +% Tacmach +gsave 10 dict begin +163 126 38 18 ellipse_path +stroke +gsave 10 dict begin +137 121 moveto +(Tacmach) +[7.44 6.24 6.24 10.8 6.24 6 6.96] +xshow +end grestore +end grestore + +% Tacmach -> Refiner +newpath 191 114 moveto +209 106 232 96 251 88 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 253 91 moveto +261 84 lineto +250 84 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 253 91 moveto +261 84 lineto +250 84 lineto +closepath +stroke +end grestore + +% Redexpr +gsave 10 dict begin +287 126 36 18 ellipse_path +stroke +gsave 10 dict begin +263 121 moveto +(Redexpr) +[9.12 6.24 6.96 5.76 6.96 6.96 4.56] +xshow +end grestore +end grestore + +% Tacmach -> Redexpr +newpath 202 126 moveto +214 126 227 126 240 126 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 240 130 moveto +250 126 lineto +240 123 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 240 130 moveto +250 126 lineto +240 123 lineto +closepath +stroke +end grestore + +% Proof_trees +gsave 10 dict begin +502 72 45 18 ellipse_path +stroke +gsave 10 dict begin +469 67 moveto +(Proof_trees) +[7.68 4.56 6.96 6.96 4.56 6.96 3.84 4.56 6.24 6.24 5.52] +xshow +end grestore +end grestore + +% Logic -> Proof_trees +newpath 420 72 moveto +428 72 437 72 446 72 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 446 76 moveto +456 72 lineto +446 69 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 446 76 moveto +456 72 lineto +446 69 lineto +closepath +stroke +end grestore + +% Proof_type +gsave 10 dict begin +628 72 44 18 ellipse_path +stroke +gsave 10 dict begin +597 67 moveto +(Proof_type) +[7.68 4.56 6.96 6.96 4.56 6.96 3.84 6.96 6.96 6.24] +xshow +end grestore +end grestore + +% Tacexpr +gsave 10 dict begin +744 72 35 18 ellipse_path +stroke +gsave 10 dict begin +721 67 moveto +(Tacexpr) +[7.44 6.24 6.24 5.76 6.96 6.96 4.56] +xshow +end grestore +end grestore + +% Proof_type -> Tacexpr +newpath 672 72 moveto +680 72 689 72 698 72 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 698 76 moveto +708 72 lineto +698 69 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 698 76 moveto +708 72 lineto +698 69 lineto +closepath +stroke +end grestore + +% Proof_trees -> Proof_type +newpath 548 72 moveto +557 72 565 72 574 72 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 574 76 moveto +584 72 lineto +574 69 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 574 76 moveto +584 72 lineto +574 69 lineto +closepath +stroke +end grestore + +% Pfedit +gsave 10 dict begin +38 112 29 18 ellipse_path +stroke +gsave 10 dict begin +21 107 moveto +(Pfedit) +[7.68 4.08 6.24 6.96 3.84 3.84] +xshow +end grestore +end grestore + +% Pfedit -> Tacmach +newpath 67 115 moveto +81 117 99 118 115 120 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 115 123 moveto +125 122 lineto +116 117 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 115 123 moveto +125 122 lineto +116 117 lineto +closepath +stroke +end grestore + +% Evar_refiner +gsave 10 dict begin +163 18 49 18 ellipse_path +stroke +gsave 10 dict begin +127 13 moveto +(Evar_refiner) +[8.4 6.72 6.24 4.56 6.96 4.56 6.24 4.8 3.84 6.96 6.24 4.56] +xshow +end grestore +end grestore + +% Pfedit -> Evar_refiner +newpath 53 96 moveto +67 82 90 60 112 45 curveto +116 42 120 40 124 37 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 126 40 moveto +133 32 lineto +123 34 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 126 40 moveto +133 32 lineto +123 34 lineto +closepath +stroke +end grestore + +% Evar_refiner -> Refiner +newpath 195 32 moveto +212 40 233 49 251 57 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 249 60 moveto +260 61 lineto +252 54 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 249 60 moveto +260 61 lineto +252 54 lineto +closepath +stroke +end grestore + +% Clenvtac +gsave 10 dict begin +38 45 38 18 ellipse_path +stroke +gsave 10 dict begin +13 40 moveto +(Clenvtac) +[9.36 3.84 6.24 6.48 6.96 4.08 6.24 6.24] +xshow +end grestore +end grestore + +% Clenvtac -> Tacmach +newpath 58 61 moveto +73 72 93 87 112 99 curveto +117 102 123 105 128 108 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 127 111 moveto +137 113 lineto +130 105 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 127 111 moveto +137 113 lineto +130 105 lineto +closepath +stroke +end grestore + +% Clenvtac -> Evar_refiner +newpath 73 37 moveto +85 35 98 32 110 29 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 111 32 moveto +120 27 lineto +110 26 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 111 32 moveto +120 27 lineto +110 26 lineto +closepath +stroke +end grestore +endpage +showpage +grestore +%%PageTrailer +%%EndPage: 1 +%%Trailer +%%Pages: 1 +end +restore +%%EOF diff --git a/dev/ocamlweb-doc/syntax.mly b/dev/ocamlweb-doc/syntax.mly new file mode 100644 index 00000000..bfc7d5cc --- /dev/null +++ b/dev/ocamlweb-doc/syntax.mly @@ -0,0 +1,224 @@ +%{ +open Ast +open Parse +%} + +%token <string> META INT IDENT +%token <string> OPER +%token LPAR RPAR BAR COMMA COLON BANG FUN DOT RARROW LET COLONEQ IN IF +%token THEN ELSE EVAL AT FOR PROP SET TYPE WILDCARD FIX +%token COFIX MATCH WITH END AND LBRACE RBRACE STRUCT AS SIMPL PERCENT +%token EOF + +%start main +%type <Ast.constr_ast> main + +%start constr +%type <Ast.constr_ast> constr + +%start simple_constr +%type <Ast.constr_ast> simple_constr + +%% + +main: + constr EOF { $1 } +; + + +paren_constr: + constr COMMA paren_constr { Pair($1,$3) } + | constr { $1 } +; + +constr: + binder_constr { $1 } + | oper_constr { close_stack $1 } +; + +binder_constr: + BANG ne_binders DOT constr { Prod($2, $4) } + | FUN ne_binders type_cstr RARROW constr { Lambda($2,mk_cast $5 $3) } + | LET IDENT binders type_cstr COLONEQ constr IN constr + { Let($2,mk_lambda $3 (mk_cast $6 $4),$8) } + | LET LPAR comma_binders RPAR COLONEQ constr IN constr + { LetCase($3,$6,$8) } + | IF constr THEN constr ELSE constr { IfCase($2,$4,$6) } + | fix_constr { $1 } + | EVAL rfun IN constr { Eval($2,$4) } +; + +comma_binders: + ne_comma_binders { $1 } + | { [] } +; + +ne_comma_binders: + binder COMMA ne_comma_binders { $1 :: $3 } + | binder { [$1] } +; + +rfun: + SIMPL { Simpl } +; + + +/* 2 Conflits shift/reduce */ +oper_constr: + oper_constr oper appl_constr + { parse_term $3 (parse_oper $2 $1) } + | oper_constr oper binder_constr + { parse_term $3 (parse_oper $2 $1) } + | oper_constr oper { parse_oper $2 $1 } + | { empty } + | appl_constr { parse_term $1 empty } +; + +oper: + OPER {$1} + | COLON {":"} +; + +appl_constr: + simple_constr ne_appl_args { Appl($1,$2) } + | AT global simple_constrs { ApplExpl($2,$3) } + | simple_constr { $1 } +; + +appl_arg: + AT INT COLONEQ simple_constr { (Some $2,$4) } + | simple_constr { (None,$1) } +; + +ne_appl_args: + appl_arg { [$1] } + | appl_arg ne_appl_args { $1::$2 } +; + +simple_constr: + atomic_constr { $1 } + | match_constr { $1 } + | LPAR paren_constr RPAR { $2 } + | simple_constr PERCENT IDENT { Scope($3,$1) } +; + +simple_constrs: + simple_constr simple_constrs { $1::$2 } + | { [] } +; + +atomic_constr: + global { Qualid $1 } + | PROP { Prop } + | SET { Set } + | TYPE { Type } + | INT { Int $1 } + | WILDCARD { Hole } + | META { Meta $1 } +; + +global: + IDENT DOT global { $1 :: $3 } + | IDENT { [$1] } +; + +/* Conflit normal */ +fix_constr: + fix_kw fix_decl + { let (id,_,_,_,_ as fx) = $2 in Fixp($1,[fx],id) } + | fix_kw fix_decl fix_decls FOR IDENT { Fixp($1, $2::$3, $5) } +; + +fix_kw: FIX {Fix} | COFIX {CoFix} +; + +fix_decl: + IDENT binders type_cstr annot COLONEQ constr { ($1,$2,$3,$4,$6) } +; + +fix_decls: + AND fix_decl fix_decls { $2::$3 } + | AND fix_decl { [$2] } +; + +annot: + LBRACE STRUCT IDENT RBRACE { Some $3 } + | { None } +; + +match_constr: + MATCH case_items case_type WITH branches END { Match($2,$3,$5) } +; + +case_items: + case_item { [$1] } + | case_item COMMA case_items { $1::$3 } +; + +case_item: + constr pred_pattern { ($1,$2) } +; + +case_type: + RARROW constr { Some $2 } + | { None } +; + +pred_pattern: + AS IDENT COLON constr { (Some $2, Some $4) } + | AS IDENT { (Some $2, None) } + | COLON constr { (None, Some $2) } + | { (None,None) } +; + +branches: + BAR branch_list { $2 } + | branch_list { $1 } + | { [] } +; + +branch_list: + patterns RARROW constr { [$1, $3] } + | patterns RARROW constr BAR branch_list { ($1,$3)::$5 } +; + +patterns: + pattern { [$1] } + | pattern COMMA patterns { $1::$3 } +; + +pattern: + pattern AS IDENT { PatAs($1,$3) } + | pattern COLON constr { PatType($1,$3) } + | IDENT simple_patterns { PatConstr($1,$2) } + | simple_pattern { $1 } +; + +simple_pattern: + IDENT { PatVar $1 } + | LPAR pattern RPAR { $2 } +; + +simple_patterns: + simple_pattern { [$1] } + | simple_pattern simple_patterns { $1::$2 } +; + +binder: + IDENT { ($1,Hole) } + | LPAR IDENT type_cstr RPAR { ($2,$3) } +; + +binders: + ne_binders { $1 } + | { [] } + +ne_binders: + binder { [$1] } + | binder ne_binders { $1::$2 } +; + +type_cstr: + COLON constr { $2 } + | { Hole } +; diff --git a/dev/ocamlweb-doc/tactics.dep.ps b/dev/ocamlweb-doc/tactics.dep.ps new file mode 100644 index 00000000..f4de22b7 --- /dev/null +++ b/dev/ocamlweb-doc/tactics.dep.ps @@ -0,0 +1,991 @@ +%!PS-Adobe-2.0 +%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) +%%For: (herbelin) Hugo Herbelin +%%Title: G +%%Pages: (atend) +%%BoundingBox: 35 35 577 165 +%%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 577 165 +%%PageOrientation: Portrait +gsave +35 35 542 130 boxprim clip newpath +36 36 translate +0 0 1 beginpage +0.4696 set_scale +0 0 translate 0 rotate +0.000 0.000 0.000 graphcolor +14.00 /Times-Roman set_font + +% Extraargs +gsave 10 dict begin +483 110 40 18 ellipse_path +stroke +gsave 10 dict begin +455 105 moveto +(Extraargs) +[8.4 6.96 3.84 4.56 6.24 6.24 4.32 6.96 5.52] +xshow +end grestore +end grestore + +% Setoid_replace +gsave 10 dict begin +615 64 54 18 ellipse_path +stroke +gsave 10 dict begin +573 59 moveto +(Setoid_replace) +[7.68 6 3.84 6.96 3.84 6.96 6.96 4.56 6.24 6.96 3.84 6.24 6.24 6.24] +xshow +end grestore +end grestore + +% Extraargs -> Setoid_replace +newpath 515 99 moveto +531 93 550 87 567 81 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 569 84 moveto +577 77 lineto +566 77 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 569 84 moveto +577 77 lineto +566 77 lineto +closepath +stroke +end grestore + +% Tactics +gsave 10 dict begin +884 110 33 18 ellipse_path +stroke +gsave 10 dict begin +864 105 moveto +(Tactics) +[7.44 6.24 6.24 3.84 3.84 6.24 5.52] +xshow +end grestore +end grestore + +% Setoid_replace -> Tactics +newpath 669 66 moveto +709 68 764 72 810 83 curveto +823 85 837 90 848 94 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 847 98 moveto +858 98 lineto +850 91 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 847 98 moveto +858 98 lineto +850 91 lineto +closepath +stroke +end grestore + +% Termdn +gsave 10 dict begin +998 256 35 18 ellipse_path +stroke +gsave 10 dict begin +976 251 moveto +(Termdn) +[7.2 6.24 4.8 10.8 6.96 6.96] +xshow +end grestore +end grestore + +% Dn +gsave 10 dict begin +1112 256 27 18 ellipse_path +stroke +gsave 10 dict begin +1102 251 moveto +(Dn) +[10.08 6.96] +xshow +end grestore +end grestore + +% Termdn -> Dn +newpath 1033 256 moveto +1047 256 1061 256 1075 256 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1075 260 moveto +1085 256 lineto +1075 253 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1075 260 moveto +1085 256 lineto +1075 253 lineto +closepath +stroke +end grestore + +% Hipattern +gsave 10 dict begin +998 110 40 18 ellipse_path +stroke +gsave 10 dict begin +971 105 moveto +(Hipattern) +[10.08 3.84 6.96 6.24 3.84 3.84 6.24 4.8 6.96] +xshow +end grestore +end grestore + +% Tactics -> Hipattern +newpath 917 110 moveto +927 110 938 110 948 110 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 948 114 moveto +958 110 lineto +948 107 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 948 114 moveto +958 110 lineto +948 107 lineto +closepath +stroke +end grestore + +% Tacticals +gsave 10 dict begin +1112 110 38 18 ellipse_path +stroke +gsave 10 dict begin +1087 105 moveto +(Tacticals) +[7.44 6.24 6.24 3.84 3.84 6.24 6.24 3.84 5.52] +xshow +end grestore +end grestore + +% Hipattern -> Tacticals +newpath 1038 110 moveto +1047 110 1055 110 1064 110 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1064 114 moveto +1074 110 lineto +1064 107 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1064 114 moveto +1074 110 lineto +1064 107 lineto +closepath +stroke +end grestore + +% Tacinterp +gsave 10 dict begin +170 191 39 18 ellipse_path +stroke +gsave 10 dict begin +143 186 moveto +(Tacinterp) +[7.44 6.24 6.24 3.84 6.96 3.84 6.24 4.8 6.96] +xshow +end grestore +end grestore + +% Auto +gsave 10 dict begin +483 218 27 18 ellipse_path +stroke +gsave 10 dict begin +468 213 moveto +(Auto) +[9.6 6.96 3.84 6.96] +xshow +end grestore +end grestore + +% Tacinterp -> Auto +newpath 209 194 moveto +269 200 386 210 445 215 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 445 218 moveto +455 216 lineto +445 212 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 445 218 moveto +455 216 lineto +445 212 lineto +closepath +stroke +end grestore + +% Leminv +gsave 10 dict begin +281 166 35 18 ellipse_path +stroke +gsave 10 dict begin +259 161 moveto +(Leminv) +[8.4 6.24 10.8 3.84 6.48 6.96] +xshow +end grestore +end grestore + +% Tacinterp -> Leminv +newpath 205 183 moveto +216 181 228 178 239 175 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 240 178 moveto +249 173 lineto +239 172 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 240 178 moveto +249 173 lineto +239 172 lineto +closepath +stroke +end grestore + +% Hiddentac +gsave 10 dict begin +615 164 42 18 ellipse_path +stroke +gsave 10 dict begin +585 159 moveto +(Hiddentac) +[10.08 3.84 6.96 6.96 6.24 6.96 4.08 6.24 6.24] +xshow +end grestore +end grestore + +% Auto -> Hiddentac +newpath 507 208 moveto +526 200 553 189 574 181 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 576 184 moveto +584 177 lineto +573 177 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 576 184 moveto +584 177 lineto +573 177 lineto +closepath +stroke +end grestore + +% Dhyp +gsave 10 dict begin +615 218 29 18 ellipse_path +stroke +gsave 10 dict begin +599 213 moveto +(Dhyp) +[10.08 6.48 6.96 6.96] +xshow +end grestore +end grestore + +% Auto -> Dhyp +newpath 511 218 moveto +530 218 555 218 576 218 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 576 222 moveto +586 218 lineto +576 215 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 576 222 moveto +586 218 lineto +576 215 lineto +closepath +stroke +end grestore + +% Inv +gsave 10 dict begin +379 164 27 18 ellipse_path +stroke +gsave 10 dict begin +369 159 moveto +(Inv) +[4.56 6.48 6.96] +xshow +end grestore +end grestore + +% Leminv -> Inv +newpath 316 165 moveto +324 165 333 165 342 165 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 342 169 moveto +352 165 lineto +342 162 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 342 169 moveto +352 165 lineto +342 162 lineto +closepath +stroke +end grestore + +% Refine +gsave 10 dict begin +758 110 32 18 ellipse_path +stroke +gsave 10 dict begin +739 105 moveto +(Refine) +[9.12 6.24 4.8 3.84 6.96 6.24] +xshow +end grestore +end grestore + +% Refine -> Tactics +newpath 790 110 moveto +805 110 824 110 841 110 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 841 114 moveto +851 110 lineto +841 107 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 841 114 moveto +851 110 lineto +841 107 lineto +closepath +stroke +end grestore + +% Nbtermdn +gsave 10 dict begin +758 256 42 18 ellipse_path +stroke +gsave 10 dict begin +729 251 moveto +(Nbtermdn) +[10.08 6.96 3.84 6.24 4.8 10.8 6.96 6.96] +xshow +end grestore +end grestore + +% Btermdn +gsave 10 dict begin +884 256 38 18 ellipse_path +stroke +gsave 10 dict begin +859 251 moveto +(Btermdn) +[9.36 3.84 6.24 4.8 10.8 6.96 6.96] +xshow +end grestore +end grestore + +% Nbtermdn -> Btermdn +newpath 800 256 moveto +812 256 824 256 836 256 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 836 260 moveto +846 256 lineto +836 253 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 836 260 moveto +846 256 lineto +836 253 lineto +closepath +stroke +end grestore + +% Btermdn -> Termdn +newpath 922 256 moveto +932 256 943 256 953 256 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 953 260 moveto +963 256 lineto +953 253 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 953 260 moveto +963 256 lineto +953 253 lineto +closepath +stroke +end grestore + +% Elim +gsave 10 dict begin +483 164 27 18 ellipse_path +stroke +gsave 10 dict begin +468 159 moveto +(Elim) +[8.4 3.84 3.84 10.8] +xshow +end grestore +end grestore + +% Inv -> Elim +newpath 406 164 moveto +418 164 432 164 445 164 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 445 168 moveto +455 164 lineto +445 161 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 445 168 moveto +455 164 lineto +445 161 lineto +closepath +stroke +end grestore + +% Equality +gsave 10 dict begin +483 56 37 18 ellipse_path +stroke +gsave 10 dict begin +459 51 moveto +(Equality) +[8.4 6.72 6.96 6.24 3.84 3.84 3.84 6.96] +xshow +end grestore +end grestore + +% Inv -> Equality +newpath 390 147 moveto +401 130 421 102 442 83 curveto +445 80 448 78 451 76 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 453 79 moveto +459 70 lineto +449 73 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 453 79 moveto +459 70 lineto +449 73 lineto +closepath +stroke +end grestore + +% Elim -> Hiddentac +newpath 511 164 moveto +526 164 545 164 562 164 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 562 168 moveto +572 164 lineto +562 161 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 562 168 moveto +572 164 lineto +562 161 lineto +closepath +stroke +end grestore + +% Equality -> Setoid_replace +newpath 520 58 moveto +530 59 540 60 551 60 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 551 63 moveto +561 61 lineto +551 57 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 551 63 moveto +561 61 lineto +551 57 lineto +closepath +stroke +end grestore + +% Evar_tactics +gsave 10 dict begin +758 164 48 18 ellipse_path +stroke +gsave 10 dict begin +722 159 moveto +(Evar_tactics) +[8.4 6.72 6.24 4.56 6.96 4.08 6.24 6.24 3.84 3.84 6.24 5.52] +xshow +end grestore +end grestore + +% Hiddentac -> Evar_tactics +newpath 658 164 moveto +671 164 685 164 699 164 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 699 168 moveto +709 164 lineto +699 161 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 699 168 moveto +709 164 lineto +699 161 lineto +closepath +stroke +end grestore + +% Evar_tactics -> Tactics +newpath 790 150 moveto +808 142 830 132 849 125 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 850 128 moveto +858 121 lineto +847 122 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 850 128 moveto +858 121 lineto +847 122 lineto +closepath +stroke +end grestore + +% Dhyp -> Tactics +newpath 644 219 moveto +684 220 756 217 810 191 curveto +844 175 855 163 872 137 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 875 138 moveto +877 128 lineto +869 135 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 875 138 moveto +877 128 lineto +869 135 lineto +closepath +stroke +end grestore + +% Dhyp -> Nbtermdn +newpath 642 225 moveto +662 230 689 238 712 244 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 712 247 moveto +722 246 lineto +713 241 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 712 247 moveto +722 246 lineto +713 241 lineto +closepath +stroke +end grestore + +% Contradiction +gsave 10 dict begin +758 18 51 18 ellipse_path +stroke +gsave 10 dict begin +719 13 moveto +(Contradiction) +[9.36 6.96 6.96 3.84 4.56 6.24 6.96 3.84 6.24 3.84 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Contradiction -> Tactics +newpath 784 34 moveto +793 39 802 44 810 50 curveto +827 62 845 76 859 88 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 857 91 moveto +867 95 lineto +862 86 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 857 91 moveto +867 95 lineto +862 86 lineto +closepath +stroke +end grestore + +% Autorewrite +gsave 10 dict begin +47 191 47 18 ellipse_path +stroke +gsave 10 dict begin +13 186 moveto +(Autorewrite) +[9.6 6.96 3.84 6.96 4.56 5.76 10.08 4.8 3.84 3.84 6.24] +xshow +end grestore +end grestore + +% Autorewrite -> Tacinterp +newpath 94 191 moveto +102 191 111 191 120 191 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 120 195 moveto +130 191 lineto +120 188 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 120 195 moveto +130 191 lineto +120 188 lineto +closepath +stroke +end grestore +endpage +showpage +grestore +%%PageTrailer +%%EndPage: 1 +%%Trailer +%%Pages: 1 +end +restore +%%EOF diff --git a/dev/ocamlweb-doc/toplevel.dep.ps b/dev/ocamlweb-doc/toplevel.dep.ps new file mode 100644 index 00000000..e0355aac --- /dev/null +++ b/dev/ocamlweb-doc/toplevel.dep.ps @@ -0,0 +1,971 @@ +%!PS-Adobe-2.0 +%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) +%%For: (herbelin) Hugo Herbelin +%%Title: G +%%Pages: (atend) +%%BoundingBox: 35 35 577 166 +%%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 577 166 +%%PageOrientation: Portrait +gsave +35 35 542 131 boxprim clip newpath +36 36 translate +0 0 1 beginpage +0.4180 set_scale +0 0 translate 0 rotate +0.000 0.000 0.000 graphcolor +14.00 /Times-Roman set_font + +% Vernac +gsave 10 dict begin +562 145 33 18 ellipse_path +stroke +gsave 10 dict begin +541 140 moveto +(Vernac) +[8.88 6.24 4.8 6.96 6.24 6.24] +xshow +end grestore +end grestore + +% Vernacentries +gsave 10 dict begin +724 158 52 18 ellipse_path +stroke +gsave 10 dict begin +685 153 moveto +(Vernacentries) +[8.88 6.24 4.8 6.96 6.24 6.24 6.24 6.96 3.84 4.8 3.84 6.24 5.52] +xshow +end grestore +end grestore + +% Vernac -> Vernacentries +newpath 595 148 moveto +615 149 640 151 663 153 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 663 156 moveto +673 154 lineto +663 150 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 663 156 moveto +673 154 lineto +663 150 lineto +closepath +stroke +end grestore + +% Vernacinterp +gsave 10 dict begin +862 158 50 18 ellipse_path +stroke +gsave 10 dict begin +825 153 moveto +(Vernacinterp) +[8.88 6.24 4.8 6.96 6.24 6.24 3.84 6.96 3.84 6.24 4.8 6.96] +xshow +end grestore +end grestore + +% Vernacentries -> Vernacinterp +newpath 776 158 moveto +785 158 793 158 802 158 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 802 162 moveto +812 158 lineto +802 155 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 802 162 moveto +812 158 lineto +802 155 lineto +closepath +stroke +end grestore + +% Discharge +gsave 10 dict begin +862 212 42 18 ellipse_path +stroke +gsave 10 dict begin +833 207 moveto +(Discharge) +[10.08 3.84 5.52 6 6.96 6.24 4.32 6.72 6.24] +xshow +end grestore +end grestore + +% Vernacentries -> Discharge +newpath 758 171 moveto +777 179 801 188 822 196 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 820 199 moveto +831 200 lineto +823 193 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 820 199 moveto +831 200 lineto +823 193 lineto +closepath +stroke +end grestore + +% Mltop +gsave 10 dict begin +862 104 31 18 ellipse_path +stroke +gsave 10 dict begin +844 99 moveto +(Mltop) +[12.48 3.84 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Vernacentries -> Mltop +newpath 758 145 moveto +779 137 805 126 826 118 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 828 121 moveto +836 114 lineto +825 114 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 828 121 moveto +836 114 lineto +825 114 lineto +closepath +stroke +end grestore + +% Record +gsave 10 dict begin +862 281 33 18 ellipse_path +stroke +gsave 10 dict begin +842 276 moveto +(Record) +[9.12 6.24 6.24 6.96 4.32 6.96] +xshow +end grestore +end grestore + +% Vernacentries -> Record +newpath 742 175 moveto +760 192 788 217 812 239 curveto +819 246 828 253 835 259 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 833 262 moveto +843 266 lineto +838 257 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 833 262 moveto +843 266 lineto +838 257 lineto +closepath +stroke +end grestore + +% Himsg +gsave 10 dict begin +991 85 32 18 ellipse_path +stroke +gsave 10 dict begin +971 80 moveto +(Himsg) +[10.08 3.84 10.8 5.52 6.96] +xshow +end grestore +end grestore + +% Vernacinterp -> Himsg +newpath 890 143 moveto +897 139 905 135 912 131 curveto +929 123 946 112 960 103 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 962 106 moveto +969 98 lineto +959 100 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 962 106 moveto +969 98 lineto +959 100 lineto +closepath +stroke +end grestore + +% Vernacexpr +gsave 10 dict begin +1246 221 45 18 ellipse_path +stroke +gsave 10 dict begin +1213 216 moveto +(Vernacexpr) +[8.88 6.24 4.8 6.96 6.24 6.24 5.76 6.96 6.96 4.56] +xshow +end grestore +end grestore + +% Vernacinterp -> Vernacexpr +newpath 912 159 moveto +947 160 994 163 1034 169 curveto +1092 178 1158 195 1200 207 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1199 210 moveto +1210 210 lineto +1201 204 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1199 210 moveto +1210 210 lineto +1201 204 lineto +closepath +stroke +end grestore + +% Class +gsave 10 dict begin +1117 238 28 18 ellipse_path +stroke +gsave 10 dict begin +1101 233 moveto +(Class) +[9.36 3.84 6.24 5.52 5.52] +xshow +end grestore +end grestore + +% Discharge -> Class +newpath 902 217 moveto +917 219 933 221 948 223 curveto +992 228 1044 232 1079 235 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1079 238 moveto +1089 236 lineto +1079 232 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1079 238 moveto +1089 236 lineto +1079 232 lineto +closepath +stroke +end grestore + +% Recordobj +gsave 10 dict begin +991 196 42 18 ellipse_path +stroke +gsave 10 dict begin +962 191 moveto +(Recordobj) +[9.12 6.24 6.24 6.96 4.32 6.96 6.96 6.96 3.84] +xshow +end grestore +end grestore + +% Discharge -> Recordobj +newpath 902 207 moveto +914 205 927 204 940 202 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 940 205 moveto +950 201 lineto +940 199 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 940 205 moveto +950 201 lineto +940 199 lineto +closepath +stroke +end grestore + +% Command +gsave 10 dict begin +991 288 42 18 ellipse_path +stroke +gsave 10 dict begin +961 283 moveto +(Command) +[9.36 6.96 10.8 10.8 6.24 6.96 6.96] +xshow +end grestore +end grestore + +% Record -> Command +newpath 895 283 moveto +908 284 923 285 938 285 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 938 288 moveto +948 286 lineto +938 282 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 938 288 moveto +948 286 lineto +938 282 lineto +closepath +stroke +end grestore + +% Toplevel +gsave 10 dict begin +255 72 37 18 ellipse_path +stroke +gsave 10 dict begin +231 67 moveto +(Toplevel) +[7.2 6.96 6.96 3.84 5.76 6.48 6.24 3.84] +xshow +end grestore +end grestore + +% Protectedtoplevel +gsave 10 dict begin +390 72 61 18 ellipse_path +stroke +gsave 10 dict begin +341 67 moveto +(Protectedtoplevel) +[7.68 4.56 6.72 3.84 6.24 6.24 3.84 6.24 6.96 3.84 6.96 6.96 3.84 5.76 6.48 6.24 3.84] +xshow +end grestore +end grestore + +% Toplevel -> Protectedtoplevel +newpath 292 72 moveto +300 72 309 72 318 72 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 318 76 moveto +328 72 lineto +318 69 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 318 76 moveto +328 72 lineto +318 69 lineto +closepath +stroke +end grestore + +% Protectedtoplevel -> Vernac +newpath 425 87 moveto +455 100 497 117 527 130 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 525 133 moveto +536 134 lineto +528 127 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 525 133 moveto +536 134 lineto +528 127 lineto +closepath +stroke +end grestore + +% Cerrors +gsave 10 dict begin +724 65 34 18 ellipse_path +stroke +gsave 10 dict begin +702 60 moveto +(Cerrors) +[9.36 6.24 5.04 4.56 6.96 4.56 5.52] +xshow +end grestore +end grestore + +% Protectedtoplevel -> Cerrors +newpath 452 71 moveto +518 70 621 67 679 66 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 679 70 moveto +689 66 lineto +679 63 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 679 70 moveto +689 66 lineto +679 63 lineto +closepath +stroke +end grestore + +% Line_oriented_parser +gsave 10 dict begin +562 26 73 18 ellipse_path +stroke +gsave 10 dict begin +501 21 moveto +(Line_oriented_parser) +[8.4 3.84 6.96 6.24 6.96 6.96 4.8 3.84 6.24 6.96 3.84 6.24 6.96 6.96 6.96 6.24 4.56 5.52 6.24 4.56] +xshow +end grestore +end grestore + +% Protectedtoplevel -> Line_oriented_parser +newpath 436 60 moveto +457 55 481 48 502 42 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 503 45 moveto +512 39 lineto +501 39 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 503 45 moveto +512 39 lineto +501 39 lineto +closepath +stroke +end grestore + +% Metasyntax +gsave 10 dict begin +1117 292 46 18 ellipse_path +stroke +gsave 10 dict begin +1083 287 moveto +(Metasyntax) +[12.48 6 4.08 6.24 5.52 6.96 6.96 4.08 6.24 6.96] +xshow +end grestore +end grestore + +% Command -> Metasyntax +newpath 1034 289 moveto +1043 290 1052 290 1061 290 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1061 293 moveto +1071 291 lineto +1061 287 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1061 293 moveto +1071 291 lineto +1061 287 lineto +closepath +stroke +end grestore + +% Command -> Class +newpath 1022 276 moveto +1041 268 1065 259 1084 252 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1085 255 moveto +1093 248 lineto +1082 249 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1085 255 moveto +1093 248 lineto +1082 249 lineto +closepath +stroke +end grestore + +% Cerrors -> Himsg +newpath 758 67 moveto +796 69 859 73 912 77 curveto +924 78 937 79 949 80 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 949 83 moveto +959 81 lineto +949 77 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 949 83 moveto +959 81 lineto +949 77 lineto +closepath +stroke +end grestore + +% Minicoq +gsave 10 dict begin +38 126 37 18 ellipse_path +stroke +gsave 10 dict begin +13 121 moveto +(Minicoq) +[12.48 3.84 6.96 3.84 6.24 6.96 6.96] +xshow +end grestore +end grestore + +% Fhimsg +gsave 10 dict begin +147 126 34 18 ellipse_path +stroke +gsave 10 dict begin +125 121 moveto +(Fhimsg) +[7.68 6.96 3.84 10.8 5.52 6.96] +xshow +end grestore +end grestore + +% Minicoq -> Fhimsg +newpath 76 126 moveto +84 126 93 126 102 126 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 102 130 moveto +112 126 lineto +102 123 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 102 130 moveto +112 126 lineto +102 123 lineto +closepath +stroke +end grestore + +% Metasyntax -> Vernacexpr +newpath 1144 277 moveto +1163 267 1189 252 1210 241 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 1212 244 moveto +1219 236 lineto +1209 238 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 1212 244 moveto +1219 236 lineto +1209 238 lineto +closepath +stroke +end grestore + +% Coqtop +gsave 10 dict begin +38 45 34 18 ellipse_path +stroke +gsave 10 dict begin +17 40 moveto +(Coqtop) +[9.36 6.96 6.96 3.84 6.96 6.96] +xshow +end grestore +end grestore + +% Coqinit +gsave 10 dict begin +147 72 34 18 ellipse_path +stroke +gsave 10 dict begin +126 67 moveto +(Coqinit) +[9.36 6.96 6.96 3.84 6.96 3.84 3.84] +xshow +end grestore +end grestore + +% Coqtop -> Coqinit +newpath 69 53 moveto +81 56 94 59 106 62 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 105 65 moveto +116 65 lineto +107 59 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 105 65 moveto +116 65 lineto +107 59 lineto +closepath +stroke +end grestore + +% Usage +gsave 10 dict begin +147 18 31 18 ellipse_path +stroke +gsave 10 dict begin +129 13 moveto +(Usage) +[10.08 5.52 6.24 6.72 6.24] +xshow +end grestore +end grestore + +% Coqtop -> Usage +newpath 69 37 moveto +81 34 95 31 108 28 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 109 31 moveto +118 25 lineto +107 25 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 109 31 moveto +118 25 lineto +107 25 lineto +closepath +stroke +end grestore + +% Coqinit -> Toplevel +newpath 181 72 moveto +190 72 199 72 208 72 curveto +stroke +gsave 10 dict begin +solid +1 setlinewidth +0.000 0.000 0.000 edgecolor +newpath 208 76 moveto +218 72 lineto +208 69 lineto +closepath +fill +0.000 0.000 0.000 edgecolor +newpath 208 76 moveto +218 72 lineto +208 69 lineto +closepath +stroke +end grestore +endpage +showpage +grestore +%%PageTrailer +%%EndPage: 1 +%%Trailer +%%Pages: 1 +end +restore +%%EOF |