From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- dev/ocamlweb-doc/Makefile | 90 --- dev/ocamlweb-doc/ast.ml | 47 -- dev/ocamlweb-doc/interp.dep.ps | 545 -------------- dev/ocamlweb-doc/intro.tex | 25 - dev/ocamlweb-doc/kernel.dep.ps | 1431 ------------------------------------- dev/ocamlweb-doc/lex.mll | 81 --- dev/ocamlweb-doc/library.dep.ps | 773 -------------------- dev/ocamlweb-doc/macros.tex | 7 - dev/ocamlweb-doc/parse.ml | 183 ----- dev/ocamlweb-doc/parsing.dep.ps | 1115 ----------------------------- dev/ocamlweb-doc/preamble.tex | 8 - dev/ocamlweb-doc/pretyping.dep.ps | 1259 -------------------------------- dev/ocamlweb-doc/proofs.dep.ps | 649 ----------------- dev/ocamlweb-doc/syntax.mly | 224 ------ dev/ocamlweb-doc/tactics.dep.ps | 991 ------------------------- dev/ocamlweb-doc/toplevel.dep.ps | 971 ------------------------- 16 files changed, 8399 deletions(-) delete mode 100644 dev/ocamlweb-doc/Makefile delete mode 100644 dev/ocamlweb-doc/ast.ml delete mode 100644 dev/ocamlweb-doc/interp.dep.ps delete mode 100644 dev/ocamlweb-doc/intro.tex delete mode 100644 dev/ocamlweb-doc/kernel.dep.ps delete mode 100644 dev/ocamlweb-doc/lex.mll delete mode 100644 dev/ocamlweb-doc/library.dep.ps delete mode 100644 dev/ocamlweb-doc/macros.tex delete mode 100644 dev/ocamlweb-doc/parse.ml delete mode 100644 dev/ocamlweb-doc/parsing.dep.ps delete mode 100644 dev/ocamlweb-doc/preamble.tex delete mode 100644 dev/ocamlweb-doc/pretyping.dep.ps delete mode 100644 dev/ocamlweb-doc/proofs.dep.ps delete mode 100644 dev/ocamlweb-doc/syntax.mly delete mode 100644 dev/ocamlweb-doc/tactics.dep.ps delete mode 100644 dev/ocamlweb-doc/toplevel.dep.ps (limited to 'dev/ocamlweb-doc') diff --git a/dev/ocamlweb-doc/Makefile b/dev/ocamlweb-doc/Makefile deleted file mode 100644 index 3189d7c5..00000000 --- a/dev/ocamlweb-doc/Makefile +++ /dev/null @@ -1,90 +0,0 @@ -include ../../config/Makefile - -LOCALINCLUDES=-I ../../config -I ../../tools -I ../../tools/coqdoc \ - -I ../../scripts -I ../../lib -I ../../kernel -I ../../kernel/byterun -I ../../library \ - -I ../../proofs -I ../../tactics -I ../../pretyping \ - -I ../../interp -I ../../toplevel -I ../../parsing -I ../../ide/utils -I ../../ide \ - -I ../../plugins/omega -I ../../plugins/romega \ - -I ../../plugins/ring -I ../../plugins/dp -I ../../plugins/setoid_ring \ - -I ../../plugins/xml -I ../../plugins/extraction \ - -I ../../plugins/fourier \ - -I ../../plugins/cc \ - -I ../../plugins/funind -I ../../plugins/firstorder \ - -I ../../plugins/field -I ../../plugins/subtac -I ../../plugins/rtauto \ - -I ../../plugins/recdef - -MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) - - -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: ../../% - ocamldoc -rectypes $(MLINCLUDES) -t $* -dot -dot-reduce ../../$*/*.ml ../../$*/*.mli -o $@ - -%.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 deleted file mode 100644 index 4eb135d8..00000000 --- a/dev/ocamlweb-doc/ast.ml +++ /dev/null @@ -1,47 +0,0 @@ - -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 deleted file mode 100644 index fda7a33c..00000000 --- a/dev/ocamlweb-doc/interp.dep.ps +++ /dev/null @@ -1,545 +0,0 @@ -%!PS-Adobe-2.0 -%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007) -%%For: (notin) Jean-Marc Notin,,, -%%Title: G -%%Pages: (atend) -%%BoundingBox: (atend) -%%EndComments -save -%%BeginProlog -/DotDict 200 dict def -DotDict begin - -/setupLatin1 { -mark -/EncodingVector 256 array def - EncodingVector 0 - -ISOLatin1Encoding 0 255 getinterval putinterval -EncodingVector 45 /hyphen put - -% 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 - 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 -setupLatin1 -%%Page: 1 1 -%%PageBoundingBox: 36 36 576 753 -%%PageOrientation: Landscape -gsave -36 36 576 753 boxprim clip newpath -0 0 1 beginpage -0.985401 0.985401 set_scale 90 rotate 40.5333 -580.533 translate -0.000 0.000 1.000 graphcolor -newpath -4 -4 moveto --4 544 lineto -724 544 lineto -724 -4 lineto -closepath fill -0.985401 setlinewidth -0.000 0.000 1.000 graphcolor -newpath -4 -4 moveto --4 544 lineto -724 544 lineto -724 -4 lineto -closepath stroke -% Constrextern -gsave -0.502 1.000 0.820 nodecolor -172 417 49.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -172 417 49.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -172 412 moveto 72 -0.5 (Constrextern) alignedtext -grestore -% Reserve -gsave -0.502 1.000 0.820 nodecolor -264 319 35.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -264 319 35.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -264 314 moveto 44 -0.5 (Reserve) alignedtext -grestore -% Constrextern->Reserve -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 188 400 moveto -203 384 225 361 242 343 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 245.049 344.831 moveto -249 335 lineto -239.781 340.221 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 245.049 344.831 moveto -249 335 lineto -239.781 340.221 lineto -closepath stroke -grestore -% Notation -gsave -0.502 1.000 0.820 nodecolor -268 122 37.1753 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -268 122 37.1753 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -268 117 moveto 49 -0.5 (Notation) alignedtext -grestore -% Constrextern->Notation -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 178 399 moveto -194 349 240 209 259 150 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 262.479 150.584 moveto -262 140 lineto -255.774 148.573 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 262.479 150.584 moveto -262 140 lineto -255.774 148.573 lineto -closepath stroke -grestore -% Topconstr -gsave -0.502 1.000 0.820 nodecolor -82 24 41.1755 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -82 24 41.1755 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -82 19 moveto 57 -0.5 (Topconstr) alignedtext -grestore -% Notation->Topconstr -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 243 109 moveto -211 91 154 62 117 43 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 118.441 39.7969 moveto -108 38 lineto -115.042 45.916 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 118.441 39.7969 moveto -108 38 lineto -115.042 45.916 lineto -closepath stroke -grestore -% Ppextend -gsave -0.502 1.000 0.820 nodecolor -278 24 39.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -278 24 39.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -278 19 moveto 52 -0.5 (Ppextend) alignedtext -grestore -% Notation->Ppextend -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 270 104 moveto -272 89 273 68 275 52 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 278.488 52.2987 moveto -276 42 lineto -271.522 51.6021 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 278.488 52.2987 moveto -276 42 lineto -271.522 51.6021 lineto -closepath stroke -grestore -% Constrintern -gsave -0.502 1.000 0.820 nodecolor -472 417 48.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -472 417 48.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -472 412 moveto 70 -0.5 (Constrintern) alignedtext -grestore -% Constrintern->Reserve -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 442 403 moveto -404 385 340 355 299 335 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 300.56 331.863 moveto -290 331 lineto -297.717 338.26 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 300.56 331.863 moveto -290 331 lineto -297.717 338.26 lineto -closepath stroke -grestore -% Implicit_quantifiers -gsave -0.502 1.000 0.820 nodecolor -508 319 69.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -508 319 69.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -508 314 moveto 112 -0.5 (Implicit_quantifiers) alignedtext -grestore -% Constrintern->Implicit_quantifiers -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 479 399 moveto -484 385 492 364 498 347 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 501.479 347.584 moveto -501 337 lineto -494.774 345.573 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 501.479 347.584 moveto -501 337 lineto -494.774 345.573 lineto -closepath stroke -grestore -% Syntax_def -gsave -0.502 1.000 0.820 nodecolor -396 220 45.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -396 220 45.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -396 215 moveto 64 -0.5 (Syntax_def) alignedtext -grestore -% Implicit_quantifiers->Syntax_def -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 488 302 moveto -469 285 442 261 422 244 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 424.546 241.596 moveto -415 237 lineto -419.596 246.546 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 424.546 241.596 moveto -415 237 lineto -419.596 246.546 lineto -closepath stroke -grestore -% Coqlib -gsave -0.502 1.000 0.820 nodecolor -656 515 32.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -656 515 32.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -656 510 moveto 38 -0.5 (Coqlib) alignedtext -grestore -% Genarg -gsave -0.502 1.000 0.820 nodecolor -82 122 33.175 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -82 122 33.175 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -82 117 moveto 41 -0.5 (Genarg) alignedtext -grestore -% Genarg->Topconstr -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 82 104 moveto -82 89 82 69 82 52 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 85.5001 52 moveto -82 42 lineto -78.5001 52 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 85.5001 52 moveto -82 42 lineto -78.5001 52 lineto -closepath stroke -grestore -% Syntax_def->Notation -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 375 204 moveto -354 187 320 161 296 143 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 298.1 140.2 moveto -288 137 lineto -293.9 145.8 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 298.1 140.2 moveto -288 137 lineto -293.9 145.8 lineto -closepath stroke -grestore -% Modintern -gsave -0.502 1.000 0.820 nodecolor -472 515 42.1756 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -472 515 42.1756 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -472 510 moveto 59 -0.5 (Modintern) alignedtext -grestore -% Modintern->Constrintern -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 472 497 moveto -472 482 472 462 472 445 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 475.5 445 moveto -472 435 lineto -468.5 445 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 475.5 445 moveto -472 435 lineto -468.5 445 lineto -closepath stroke -grestore -endpage -showpage -grestore -%%PageTrailer -%%EndPage: 1 -%%Trailer -%%Pages: 1 -%%BoundingBox: 36 36 576 753 -end -restore -%%EOF diff --git a/dev/ocamlweb-doc/intro.tex b/dev/ocamlweb-doc/intro.tex deleted file mode 100644 index 4cec8673..00000000 --- a/dev/ocamlweb-doc/intro.tex +++ /dev/null @@ -1,25 +0,0 @@ - -\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 deleted file mode 100644 index b7b4137b..00000000 --- a/dev/ocamlweb-doc/kernel.dep.ps +++ /dev/null @@ -1,1431 +0,0 @@ -%!PS-Adobe-2.0 -%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007) -%%For: (notin) Jean-Marc Notin,,, -%%Title: G -%%Pages: (atend) -%%BoundingBox: (atend) -%%EndComments -save -%%BeginProlog -/DotDict 200 dict def -DotDict begin - -/setupLatin1 { -mark -/EncodingVector 256 array def - EncodingVector 0 - -ISOLatin1Encoding 0 255 getinterval putinterval -EncodingVector 45 /hyphen put - -% 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 - 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 -setupLatin1 -%%Page: 1 1 -%%PageBoundingBox: 36 36 535 756 -%%PageOrientation: Landscape -gsave -36 36 535 756 boxprim clip newpath -0 0 1 beginpage -0.393658 0.393658 set_scale 90 rotate 95.45 -1355.45 translate -0.000 0.000 1.000 graphcolor -newpath -4 -4 moveto --4 1264 lineto -1825 1264 lineto -1825 -4 lineto -closepath fill -0.393658 setlinewidth -0.000 0.000 1.000 graphcolor -newpath -4 -4 moveto --4 1264 lineto -1825 1264 lineto -1825 -4 lineto -closepath stroke -% Cbytecodes -gsave -0.502 1.000 0.820 nodecolor -1258 234 45.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1258 234 45.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1258 229 moveto 64 -0.5 (Cbytecodes) alignedtext -grestore -% Term -gsave -0.502 1.000 0.820 nodecolor -1093 162 28.1746 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1093 162 28.1746 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1093 157 moveto 31 -0.5 (Term) alignedtext -grestore -% Cbytecodes->Term -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1227 221 moveto -1198 208 1155 189 1125 176 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1126.56 172.863 moveto -1116 172 lineto -1123.72 179.26 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1126.56 172.863 moveto -1116 172 lineto -1123.72 179.26 lineto -closepath stroke -grestore -% Esubst -gsave -0.502 1.000 0.820 nodecolor -1093 90 31.1748 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1093 90 31.1748 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1093 85 moveto 37 -0.5 (Esubst) alignedtext -grestore -% Term->Esubst -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1093 144 moveto -1093 136 1093 127 1093 118 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1096.5 118 moveto -1093 108 lineto -1089.5 118 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1096.5 118 moveto -1093 108 lineto -1089.5 118 lineto -closepath stroke -grestore -% Univ -gsave -0.502 1.000 0.820 nodecolor -580 90 27.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -580 90 27.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -580 85 moveto 28 -0.5 (Univ) alignedtext -grestore -% Term->Univ -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1065 158 moveto -979 145 714 109 616 95 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 616.299 91.5125 moveto -606 94 lineto -615.602 98.4778 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 616.299 91.5125 moveto -606 94 lineto -615.602 98.4778 lineto -closepath stroke -grestore -% Cbytegen -gsave -0.502 1.000 0.820 nodecolor -1148 522 39.1754 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1148 522 39.1754 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1148 517 moveto 53 -0.5 (Cbytegen) alignedtext -grestore -% Pre_env -gsave -0.502 1.000 0.820 nodecolor -1148 450 36.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1148 450 36.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1148 445 moveto 46 -0.5 (Pre_env) alignedtext -grestore -% Cbytegen->Pre_env -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1148 504 moveto -1148 496 1148 487 1148 478 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1151.5 478 moveto -1148 468 lineto -1144.5 478 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1151.5 478 moveto -1148 468 lineto -1144.5 478 lineto -closepath stroke -grestore -% Declarations -gsave -0.502 1.000 0.820 nodecolor -1148 378 48.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1148 378 48.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1148 373 moveto 70 -0.5 (Declarations) alignedtext -grestore -% Pre_env->Declarations -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1148 432 moveto -1148 424 1148 415 1148 406 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1151.5 406 moveto -1148 396 lineto -1144.5 406 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1151.5 406 moveto -1148 396 lineto -1144.5 406 lineto -closepath stroke -grestore -% Cemitcodes -gsave -0.502 1.000 0.820 nodecolor -663 306 45.1757 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -663 306 45.1757 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -663 301 moveto 65 -0.5 (Cemitcodes) alignedtext -grestore -% Cemitcodes->Cbytecodes -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 706 301 moveto -813 287 1088 254 1205 240 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1205.4 243.478 moveto -1215 239 lineto -1204.7 236.512 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1205.4 243.478 moveto -1215 239 lineto -1204.7 236.512 lineto -closepath stroke -grestore -% Copcodes -gsave -0.502 1.000 0.820 nodecolor -786 234 40.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -786 234 40.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -786 229 moveto 54 -0.5 (Copcodes) alignedtext -grestore -% Cemitcodes->Copcodes -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 688 291 moveto -707 281 732 266 752 253 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 753.958 255.916 moveto -761 248 lineto -750.559 249.797 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 753.958 255.916 moveto -761 248 lineto -750.559 249.797 lineto -closepath stroke -grestore -% Mod_subst -gsave -0.502 1.000 0.820 nodecolor -325 234 43.1756 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -325 234 43.1756 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -325 229 moveto 61 -0.5 (Mod_subst) alignedtext -grestore -% Cemitcodes->Mod_subst -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 623 298 moveto -561 284 441 259 374 244 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 374.492 240.529 moveto -364 242 lineto -373.119 247.393 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 374.492 240.529 moveto -364 242 lineto -373.119 247.393 lineto -closepath stroke -grestore -% Mod_subst->Term -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 367 230 moveto -502 217 925 178 1055 166 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1055.4 169.478 moveto -1065 165 lineto -1054.7 162.512 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1055.4 169.478 moveto -1065 165 lineto -1054.7 162.512 lineto -closepath stroke -grestore -% Closure -gsave -0.502 1.000 0.820 nodecolor -713 666 34.1751 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -713 666 34.1751 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -713 661 moveto 43 -0.5 (Closure) alignedtext -grestore -% Environ -gsave -0.502 1.000 0.820 nodecolor -1148 594 36.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1148 594 36.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1148 589 moveto 46 -0.5 (Environ) alignedtext -grestore -% Closure->Environ -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 746 661 moveto -823 648 1016 616 1104 602 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1104.88 605.393 moveto -1114 600 lineto -1103.51 598.529 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1104.88 605.393 moveto -1114 600 lineto -1103.51 598.529 lineto -closepath stroke -grestore -% Environ->Cbytegen -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1148 576 moveto -1148 568 1148 559 1148 550 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1151.5 550 moveto -1148 540 lineto -1144.5 550 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1151.5 550 moveto -1148 540 lineto -1144.5 550 lineto -closepath stroke -grestore -% Conv_oracle -gsave -0.502 1.000 0.820 nodecolor -383 522 48.1758 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -383 522 48.1758 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -383 517 moveto 71 -0.5 (Conv_oracle) alignedtext -grestore -% Names -gsave -0.502 1.000 0.820 nodecolor -288 18 32.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -288 18 32.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -288 13 moveto 38 -0.5 (Names) alignedtext -grestore -% Conv_oracle->Names -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 339 515 moveto -238 497 0 449 0 378 curveto -0 378 0 378 0 162 curveto -0 53 166 26 246 20 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 246.398 23.4778 moveto -256 19 lineto -245.701 16.5125 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 246.398 23.4778 moveto -256 19 lineto -245.701 16.5125 lineto -closepath stroke -grestore -% Cooking -gsave -0.502 1.000 0.820 nodecolor -960 1026 37.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -960 1026 37.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -960 1021 moveto 48 -0.5 (Cooking) alignedtext -grestore -% Typeops -gsave -0.502 1.000 0.820 nodecolor -960 954 37.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -960 954 37.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -960 949 moveto 48 -0.5 (Typeops) alignedtext -grestore -% Cooking->Typeops -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 960 1008 moveto -960 1000 960 991 960 982 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 963.5 982 moveto -960 972 lineto -956.5 982 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 963.5 982 moveto -960 972 lineto -956.5 982 lineto -closepath stroke -grestore -% Entries -gsave -0.502 1.000 0.820 nodecolor -1391 882 33.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1391 882 33.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1391 877 moveto 40 -0.5 (Entries) alignedtext -grestore -% Typeops->Entries -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 995 948 moveto -1074 935 1265 903 1349 889 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1349.88 892.393 moveto -1359 887 lineto -1348.51 885.529 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1349.88 892.393 moveto -1359 887 lineto -1348.51 885.529 lineto -closepath stroke -grestore -% Inductive -gsave -0.502 1.000 0.820 nodecolor -837 882 39.1754 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -837 882 39.1754 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -837 877 moveto 53 -0.5 (Inductive) alignedtext -grestore -% Typeops->Inductive -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 936 940 moveto -918 929 891 914 871 901 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 872.441 897.797 moveto -862 896 lineto -869.042 903.916 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 872.441 897.797 moveto -862 896 lineto -869.042 903.916 lineto -closepath stroke -grestore -% Csymtable -gsave -0.502 1.000 0.820 nodecolor -1148 666 42.1756 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1148 666 42.1756 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1148 661 moveto 59 -0.5 (Csymtable) alignedtext -grestore -% Csymtable->Environ -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1148 648 moveto -1148 640 1148 631 1148 622 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1151.5 622 moveto -1148 612 lineto -1144.5 622 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1151.5 622 moveto -1148 612 lineto -1144.5 622 lineto -closepath stroke -grestore -% Vm -gsave -0.502 1.000 0.820 nodecolor -731 594 27 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -731 594 27 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -731 589 moveto 21 -0.5 (Vm) alignedtext -grestore -% Csymtable->Vm -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1109 659 moveto -1029 645 845 614 767 600 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 767.492 596.529 moveto -757 598 lineto -766.119 603.393 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 767.492 596.529 moveto -757 598 lineto -766.119 603.393 lineto -closepath stroke -grestore -% Vm->Cemitcodes -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 727 576 moveto -716 527 684 392 669 334 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 672.393 333.119 moveto -667 324 lineto -665.529 334.492 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 672.393 333.119 moveto -667 324 lineto -665.529 334.492 lineto -closepath stroke -grestore -% Vm->Conv_oracle -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 705 589 moveto -648 577 510 549 435 533 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 435.492 529.529 moveto -425 531 lineto -434.119 536.393 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 435.492 529.529 moveto -425 531 lineto -434.119 536.393 lineto -closepath stroke -grestore -% Declarations->Cemitcodes -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1103 371 moveto -1013 358 811 328 715 314 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 715.492 310.529 moveto -705 312 lineto -714.119 317.393 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 715.492 310.529 moveto -705 312 lineto -714.119 317.393 lineto -closepath stroke -grestore -% Sign -gsave -0.502 1.000 0.820 nodecolor -1697 306 27 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1697 306 27 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1697 301 moveto 26 -0.5 (Sign) alignedtext -grestore -% Declarations->Sign -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1193 372 moveto -1300 359 1563 324 1660 311 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1660.4 314.478 moveto -1670 310 lineto -1659.7 307.512 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1660.4 314.478 moveto -1670 310 lineto -1659.7 307.512 lineto -closepath stroke -grestore -% Retroknowledge -gsave -0.502 1.000 0.820 nodecolor -1221 306 59.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1221 306 59.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1221 301 moveto 92 -0.5 (Retroknowledge) alignedtext -grestore -% Declarations->Retroknowledge -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1165 361 moveto -1175 352 1186 341 1197 330 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1199.4 332.546 moveto -1204 323 lineto -1194.45 327.596 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1199.4 332.546 moveto -1204 323 lineto -1194.45 327.596 lineto -closepath stroke -grestore -% Sign->Term -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1671 300 moveto -1576 277 1241 197 1130 170 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1130.49 166.529 moveto -1120 168 lineto -1129.12 173.393 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1130.49 166.529 moveto -1120 168 lineto -1129.12 173.393 lineto -closepath stroke -grestore -% Retroknowledge->Cbytecodes -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1230 288 moveto -1234 280 1239 270 1244 261 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1247.2 262.441 moveto -1249 252 lineto -1241.08 259.042 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1247.2 262.441 moveto -1249 252 lineto -1241.08 259.042 lineto -closepath stroke -grestore -% Entries->Sign -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1411 868 moveto -1442 844 1496 795 1496 738 curveto -1496 738 1496 738 1496 450 curveto -1496 370 1604 330 1661 314 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1661.88 317.393 moveto -1671 312 lineto -1660.51 310.529 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1661.88 317.393 moveto -1671 312 lineto -1660.51 310.529 lineto -closepath stroke -grestore -% Indtypes -gsave -0.502 1.000 0.820 nodecolor -539 1026 37.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -539 1026 37.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -539 1021 moveto 48 -0.5 (Indtypes) alignedtext -grestore -% Indtypes->Typeops -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 574 1020 moveto -650 1008 831 977 915 962 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 915.881 965.393 moveto -925 960 lineto -914.508 958.529 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 915.881 965.393 moveto -925 960 lineto -914.508 958.529 lineto -closepath stroke -grestore -% Type_errors -gsave -0.502 1.000 0.820 nodecolor -713 810 47.1758 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -713 810 47.1758 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -713 805 moveto 69 -0.5 (Type_errors) alignedtext -grestore -% Inductive->Type_errors -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 813 868 moveto -794 858 769 843 748 830 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 749.441 826.797 moveto -739 825 lineto -746.042 832.916 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 749.441 826.797 moveto -739 825 lineto -746.042 832.916 lineto -closepath stroke -grestore -% Reduction -gsave -0.502 1.000 0.820 nodecolor -713 738 41.1755 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -713 738 41.1755 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -713 733 moveto 57 -0.5 (Reduction) alignedtext -grestore -% Type_errors->Reduction -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 713 792 moveto -713 784 713 775 713 766 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 716.5 766 moveto -713 756 lineto -709.5 766 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 716.5 766 moveto -713 756 lineto -709.5 766 lineto -closepath stroke -grestore -% Modops -gsave -0.502 1.000 0.820 nodecolor -1404 954 35.1752 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1404 954 35.1752 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1404 949 moveto 45 -0.5 (Modops) alignedtext -grestore -% Modops->Environ -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1439 951 moveto -1511 943 1670 914 1670 810 curveto -1670 810 1670 810 1670 738 curveto -1670 639 1322 606 1194 597 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1194.3 593.512 moveto -1184 596 lineto -1193.6 600.478 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1194.3 593.512 moveto -1184 596 lineto -1193.6 600.478 lineto -closepath stroke -grestore -% Modops->Entries -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1401 936 moveto -1400 928 1398 919 1396 910 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1399.39 909.119 moveto -1394 900 lineto -1392.53 910.492 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1399.39 909.119 moveto -1394 900 lineto -1392.53 910.492 lineto -closepath stroke -grestore -% Mod_typing -gsave -0.502 1.000 0.820 nodecolor -1157 1170 47.1758 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1157 1170 47.1758 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1157 1165 moveto 69 -0.5 (Mod_typing) alignedtext -grestore -% Subtyping -gsave -0.502 1.000 0.820 nodecolor -1404 1026 42.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1404 1026 42.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1404 1021 moveto 58 -0.5 (Subtyping) alignedtext -grestore -% Mod_typing->Subtyping -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1183 1155 moveto -1227 1129 1320 1075 1370 1046 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1371.96 1048.92 moveto -1379 1041 lineto -1368.56 1042.8 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1371.96 1048.92 moveto -1379 1041 lineto -1368.56 1042.8 lineto -closepath stroke -grestore -% Term_typing -gsave -0.502 1.000 0.820 nodecolor -960 1098 50.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -960 1098 50.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -960 1093 moveto 74 -0.5 (Term_typing) alignedtext -grestore -% Mod_typing->Term_typing -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1123 1157 moveto -1090 1145 1040 1127 1005 1114 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1005.58 1110.52 moveto -995 1111 lineto -1003.57 1117.23 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1005.58 1110.52 moveto -995 1111 lineto -1003.57 1117.23 lineto -closepath stroke -grestore -% Subtyping->Typeops -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1365 1020 moveto -1282 1007 1092 975 1005 962 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1005.49 958.529 moveto -995 960 lineto -1004.12 965.393 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1005.49 958.529 moveto -995 960 lineto -1004.12 965.393 lineto -closepath stroke -grestore -% Subtyping->Modops -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1404 1008 moveto -1404 1000 1404 991 1404 982 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1407.5 982 moveto -1404 972 lineto -1400.5 982 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1407.5 982 moveto -1404 972 lineto -1400.5 982 lineto -closepath stroke -grestore -% Term_typing->Cooking -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 960 1080 moveto -960 1072 960 1063 960 1054 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 963.5 1054 moveto -960 1044 lineto -956.5 1054 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 963.5 1054 moveto -960 1044 lineto -956.5 1054 lineto -closepath stroke -grestore -% Term_typing->Indtypes -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 915 1090 moveto -833 1077 665 1048 584 1034 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 584.492 1030.53 moveto -574 1032 lineto -583.119 1037.39 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 584.492 1030.53 moveto -574 1032 lineto -583.119 1037.39 lineto -closepath stroke -grestore -% Reduction->Closure -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 713 720 moveto -713 712 713 703 713 694 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 716.5 694 moveto -713 684 lineto -709.5 694 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 716.5 694 moveto -713 684 lineto -709.5 694 lineto -closepath stroke -grestore -% Reduction->Conv_oracle -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 690 723 moveto -633 686 482 587 415 544 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 417.1 541.2 moveto -407 538 lineto -412.9 546.8 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 417.1 541.2 moveto -407 538 lineto -412.9 546.8 lineto -closepath stroke -grestore -% Safe_typing -gsave -0.502 1.000 0.820 nodecolor -1157 1242 47.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1157 1242 47.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1157 1237 moveto 68 -0.5 (Safe_typing) alignedtext -grestore -% Safe_typing->Mod_typing -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1157 1224 moveto -1157 1216 1157 1207 1157 1198 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1160.5 1198 moveto -1157 1188 lineto -1153.5 1198 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1160.5 1198 moveto -1157 1188 lineto -1153.5 1198 lineto -closepath stroke -grestore -% Univ->Names -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 555 84 moveto -504 71 388 42 327 27 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 327.492 23.5292 moveto -317 25 lineto -326.119 30.3933 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 327.492 23.5292 moveto -317 25 lineto -326.119 30.3933 lineto -closepath stroke -grestore -% Vconv -gsave -0.502 1.000 0.820 nodecolor -1152 810 31.1748 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1152 810 31.1748 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1152 805 moveto 37 -0.5 (Vconv) alignedtext -grestore -% Vconv->Csymtable -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1151 792 moveto -1150 767 1149 723 1148 694 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1151.5 694 moveto -1148 684 lineto -1144.5 694 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1151.5 694 moveto -1148 684 lineto -1144.5 694 lineto -closepath stroke -grestore -% Vconv->Reduction -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1122 805 moveto -1047 792 852 760 761 746 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 761.492 742.529 moveto -751 744 lineto -760.119 749.393 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 761.492 742.529 moveto -751 744 lineto -760.119 749.393 lineto -closepath stroke -grestore -endpage -showpage -grestore -%%PageTrailer -%%EndPage: 1 -%%Trailer -%%Pages: 1 -%%BoundingBox: 36 36 535 756 -end -restore -%%EOF diff --git a/dev/ocamlweb-doc/lex.mll b/dev/ocamlweb-doc/lex.mll deleted file mode 100644 index 059526d9..00000000 --- a/dev/ocamlweb-doc/lex.mll +++ /dev/null @@ -1,81 +0,0 @@ - -{ - 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 deleted file mode 100644 index c9bb351e..00000000 --- a/dev/ocamlweb-doc/library.dep.ps +++ /dev/null @@ -1,773 +0,0 @@ -%!PS-Adobe-2.0 -%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007) -%%For: (notin) Jean-Marc Notin,,, -%%Title: G -%%Pages: (atend) -%%BoundingBox: (atend) -%%EndComments -save -%%BeginProlog -/DotDict 200 dict def -DotDict begin - -/setupLatin1 { -mark -/EncodingVector 256 array def - EncodingVector 0 - -ISOLatin1Encoding 0 255 getinterval putinterval -EncodingVector 45 /hyphen put - -% 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 - 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 -setupLatin1 -%%Page: 1 1 -%%PageBoundingBox: 36 36 576 752 -%%PageOrientation: Landscape -gsave -36 36 576 752 boxprim clip newpath -0 0 1 beginpage -0.985401 0.985401 set_scale 90 rotate 40.5333 -580.533 translate -0.000 0.000 1.000 graphcolor -newpath -4 -4 moveto --4 544 lineto -723 544 lineto -723 -4 lineto -closepath fill -0.985401 setlinewidth -0.000 0.000 1.000 graphcolor -newpath -4 -4 moveto --4 544 lineto -723 544 lineto -723 -4 lineto -closepath stroke -% Declare -gsave -0.502 1.000 0.820 nodecolor -488 436 34.1751 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -488 436 34.1751 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -488 431 moveto 43 -0.5 (Declare) alignedtext -grestore -% Dischargedhypsmap -gsave -0.502 1.000 0.820 nodecolor -488 353 69.1764 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -488 353 69.1764 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -488 348 moveto 113 -0.5 (Dischargedhypsmap) alignedtext -grestore -% Declare->Dischargedhypsmap -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 488 418 moveto -488 407 488 393 488 381 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 491.5 381 moveto -488 371 lineto -484.5 381 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 491.5 381 moveto -488 371 lineto -484.5 381 lineto -closepath stroke -grestore -% Impargs -gsave -0.502 1.000 0.820 nodecolor -201 353 36.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -201 353 36.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -201 348 moveto 46 -0.5 (Impargs) alignedtext -grestore -% Declare->Impargs -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 458 427 moveto -407 412 301 382 242 365 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 242.584 361.521 moveto -232 362 lineto -240.573 368.226 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 242.584 361.521 moveto -232 362 lineto -240.573 368.226 lineto -closepath stroke -grestore -% Decl_kinds -gsave -0.502 1.000 0.820 nodecolor -661 353 44.1757 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -661 353 44.1757 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -661 348 moveto 63 -0.5 (Decl_kinds) alignedtext -grestore -% Declare->Decl_kinds -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 514 424 moveto -543 410 590 388 624 372 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 625.958 374.916 moveto -633 367 lineto -622.559 368.797 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 625.958 374.916 moveto -633 367 lineto -622.559 368.797 lineto -closepath stroke -grestore -% Lib -gsave -0.502 1.000 0.820 nodecolor -219 270 27 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -219 270 27 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -219 265 moveto 20 -0.5 (Lib) alignedtext -grestore -% Dischargedhypsmap->Lib -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 443 339 moveto -390 323 302 296 254 281 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 254.584 277.521 moveto -244 278 lineto -252.573 284.226 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 254.584 277.521 moveto -244 278 lineto -252.573 284.226 lineto -closepath stroke -grestore -% Global -gsave -0.502 1.000 0.820 nodecolor -82 270 32.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -82 270 32.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -82 265 moveto 38 -0.5 (Global) alignedtext -grestore -% Impargs->Global -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 180 338 moveto -161 325 132 305 110 290 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 112.1 287.2 moveto -102 284 lineto -107.9 292.8 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 112.1 287.2 moveto -102 284 lineto -107.9 292.8 lineto -closepath stroke -grestore -% Impargs->Lib -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 205 335 moveto -207 324 210 310 213 298 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 216.471 298.492 moveto -215 288 lineto -209.607 297.119 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 216.471 298.492 moveto -215 288 lineto -209.607 297.119 lineto -closepath stroke -grestore -% Declaremods -gsave -0.502 1.000 0.820 nodecolor -65 353 49.1759 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -65 353 49.1759 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -65 348 moveto 73 -0.5 (Declaremods) alignedtext -grestore -% Declaremods->Global -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 69 335 moveto -71 324 74 310 76 298 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 79.4708 298.492 moveto -78 288 lineto -72.6067 297.119 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 79.4708 298.492 moveto -78 288 lineto -72.6067 297.119 lineto -closepath stroke -grestore -% Declaremods->Lib -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 93 338 moveto -120 324 161 301 189 286 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 190.958 288.916 moveto -198 281 lineto -187.559 282.797 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 190.958 288.916 moveto -198 281 lineto -187.559 282.797 lineto -closepath stroke -grestore -% Summary -gsave -0.502 1.000 0.820 nodecolor -69 103 40.1755 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -69 103 40.1755 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -69 98 moveto 55 -0.5 (Summary) alignedtext -grestore -% Global->Summary -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 81 252 moveto -78 223 74 166 71 131 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 74.4778 130.602 moveto -70 121 lineto -67.5125 131.299 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 74.4778 130.602 moveto -70 121 lineto -67.5125 131.299 lineto -closepath stroke -grestore -% Libnames -gsave -0.502 1.000 0.820 nodecolor -203 103 40.1755 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -203 103 40.1755 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -203 98 moveto 55 -0.5 (Libnames) alignedtext -grestore -% Global->Libnames -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 94 253 moveto -115 224 159 164 184 129 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 186.8 131.1 moveto -190 121 lineto -181.2 126.9 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 186.8 131.1 moveto -190 121 lineto -181.2 126.9 lineto -closepath stroke -grestore -% Nametab -gsave -0.502 1.000 0.820 nodecolor -203 186 38.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -203 186 38.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -203 181 moveto 50 -0.5 (Nametab) alignedtext -grestore -% Lib->Nametab -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 216 252 moveto -214 241 211 226 209 214 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 212.393 213.119 moveto -207 204 lineto -205.529 214.492 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 212.393 213.119 moveto -207 204 lineto -205.529 214.492 lineto -closepath stroke -grestore -% Libobject -gsave -0.502 1.000 0.820 nodecolor -329 186 40.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -329 186 40.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -329 181 moveto 54 -0.5 (Libobject) alignedtext -grestore -% Lib->Libobject -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 237 256 moveto -254 243 280 223 300 208 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 302.1 210.8 moveto -308 202 lineto -297.9 205.2 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 302.1 210.8 moveto -308 202 lineto -297.9 205.2 lineto -closepath stroke -grestore -% Nameops -gsave -0.502 1.000 0.820 nodecolor -203 20 39.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -203 20 39.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -203 15 moveto 52 -0.5 (Nameops) alignedtext -grestore -% Libnames->Nameops -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 203 85 moveto -203 74 203 60 203 48 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 206.5 48 moveto -203 38 lineto -199.5 48 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 206.5 48 moveto -203 38 lineto -199.5 48 lineto -closepath stroke -grestore -% Goptions -gsave -0.502 1.000 0.820 nodecolor -322 353 38.1754 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -322 353 38.1754 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -322 348 moveto 51 -0.5 (Goptions) alignedtext -grestore -% Goptions->Lib -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 303 337 moveto -287 324 263 305 245 291 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 246.831 287.951 moveto -237 284 lineto -242.221 293.219 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 246.831 287.951 moveto -237 284 lineto -242.221 293.219 lineto -closepath stroke -grestore -% Nametab->Summary -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 180 172 moveto -158 159 125 138 101 123 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 102.441 119.797 moveto -92 118 lineto -99.0418 125.916 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 102.441 119.797 moveto -92 118 lineto -99.0418 125.916 lineto -closepath stroke -grestore -% Nametab->Libnames -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 203 168 moveto -203 157 203 143 203 131 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 206.5 131 moveto -203 121 lineto -199.5 131 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 206.5 131 moveto -203 121 lineto -199.5 131 lineto -closepath stroke -grestore -% Libobject->Libnames -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 306 171 moveto -286 158 256 138 235 124 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 236.262 120.635 moveto -226 118 lineto -232.379 126.459 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 236.262 120.635 moveto -226 118 lineto -232.379 126.459 lineto -closepath stroke -grestore -% Library -gsave -0.502 1.000 0.820 nodecolor -65 436 34.1751 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -65 436 34.1751 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -65 431 moveto 43 -0.5 (Library) alignedtext -grestore -% Library->Declaremods -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 65 418 moveto -65 407 65 393 65 381 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 68.5001 381 moveto -65 371 lineto -61.5001 381 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 68.5001 381 moveto -65 371 lineto -61.5001 381 lineto -closepath stroke -grestore -% States -gsave -0.502 1.000 0.820 nodecolor -65 519 29.1747 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -65 519 29.1747 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -65 514 moveto 33 -0.5 (States) alignedtext -grestore -% States->Library -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 65 501 moveto -65 490 65 476 65 464 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 68.5001 464 moveto -65 454 lineto -61.5001 464 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 68.5001 464 moveto -65 454 lineto -61.5001 464 lineto -closepath stroke -grestore -endpage -showpage -grestore -%%PageTrailer -%%EndPage: 1 -%%Trailer -%%Pages: 1 -%%BoundingBox: 36 36 576 752 -end -restore -%%EOF diff --git a/dev/ocamlweb-doc/macros.tex b/dev/ocamlweb-doc/macros.tex deleted file mode 100644 index 6beacf7b..00000000 --- a/dev/ocamlweb-doc/macros.tex +++ /dev/null @@ -1,7 +0,0 @@ - -% 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 deleted file mode 100644 index b145fffd..00000000 --- a/dev/ocamlweb-doc/parse.ml +++ /dev/null @@ -1,183 +0,0 @@ - -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 deleted file mode 100644 index 723d8c69..00000000 --- a/dev/ocamlweb-doc/parsing.dep.ps +++ /dev/null @@ -1,1115 +0,0 @@ -%!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 deleted file mode 100644 index 2cd21f02..00000000 --- a/dev/ocamlweb-doc/preamble.tex +++ /dev/null @@ -1,8 +0,0 @@ -\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 deleted file mode 100644 index 02d1b8b5..00000000 --- a/dev/ocamlweb-doc/pretyping.dep.ps +++ /dev/null @@ -1,1259 +0,0 @@ -%!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 deleted file mode 100644 index 4dd045ce..00000000 --- a/dev/ocamlweb-doc/proofs.dep.ps +++ /dev/null @@ -1,649 +0,0 @@ -%!PS-Adobe-2.0 -%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007) -%%For: (notin) Jean-Marc Notin,,, -%%Title: G -%%Pages: (atend) -%%BoundingBox: (atend) -%%EndComments -save -%%BeginProlog -/DotDict 200 dict def -DotDict begin - -/setupLatin1 { -mark -/EncodingVector 256 array def - EncodingVector 0 - -ISOLatin1Encoding 0 255 getinterval putinterval -EncodingVector 45 /hyphen put - -% 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 - 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 -setupLatin1 -%%Page: 1 1 -%%PageBoundingBox: 36 36 576 753 -%%PageOrientation: Landscape -gsave -36 36 576 753 boxprim clip newpath -0 0 1 beginpage -0.870968 0.870968 set_scale 90 rotate 45.3333 -657.333 translate -0.000 0.000 1.000 graphcolor -newpath -4 -4 moveto --4 616 lineto -819 616 lineto -819 -4 lineto -closepath fill -0.870968 setlinewidth -0.000 0.000 1.000 graphcolor -newpath -4 -4 moveto --4 616 lineto -819 616 lineto -819 -4 lineto -closepath stroke -% Clenvtac -gsave -0.502 1.000 0.820 nodecolor -451 522 37.1753 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -451 522 37.1753 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -451 517 moveto 49 -0.5 (Clenvtac) alignedtext -grestore -% Evar_refiner -gsave -0.502 1.000 0.820 nodecolor -439 450 49.1777 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -439 450 49.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -439 445 moveto 72 -0.5 (Evar_refiner) alignedtext -grestore -% Clenvtac->Evar_refiner -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 448 504 moveto -447 496 445 487 444 478 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 447.393 477.119 moveto -442 468 lineto -440.529 478.492 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 447.393 477.119 moveto -442 468 lineto -440.529 478.492 lineto -closepath stroke -grestore -% Tacmach -gsave -0.502 1.000 0.820 nodecolor -711 450 38.1754 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -711 450 38.1754 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -711 445 moveto 51 -0.5 (Tacmach) alignedtext -grestore -% Clenvtac->Tacmach -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 483 513 moveto -530 500 616 476 668 462 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 669.427 465.226 moveto -678 459 lineto -667.416 458.521 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 669.427 465.226 moveto -678 459 lineto -667.416 458.521 lineto -closepath stroke -grestore -% Refiner -gsave -0.502 1.000 0.820 nodecolor -439 378 34.1777 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -439 378 34.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -439 373 moveto 42 -0.5 (Refiner) alignedtext -grestore -% Evar_refiner->Refiner -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 439 432 moveto -439 424 439 415 439 406 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 442.5 406 moveto -439 396 lineto -435.5 406 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 442.5 406 moveto -439 396 lineto -435.5 406 lineto -closepath stroke -grestore -% Tacmach->Refiner -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 678 441 moveto -628 428 533 403 480 389 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 480.584 385.521 moveto -470 386 lineto -478.573 392.226 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 480.584 385.521 moveto -470 386 lineto -478.573 392.226 lineto -closepath stroke -grestore -% Redexpr -gsave -0.502 1.000 0.820 nodecolor -711 378 36.1752 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -711 378 36.1752 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -711 373 moveto 47 -0.5 (Redexpr) alignedtext -grestore -% Tacmach->Redexpr -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 711 432 moveto -711 424 711 415 711 406 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 714.5 406 moveto -711 396 lineto -707.5 406 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 714.5 406 moveto -711 396 lineto -707.5 406 lineto -closepath stroke -grestore -% Decl_mode -gsave -0.502 1.000 0.820 nodecolor -698 594 45.1777 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -698 594 45.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -698 589 moveto 64 -0.5 (Decl_mode) alignedtext -grestore -% Pfedit -gsave -0.502 1.000 0.820 nodecolor -698 522 30.1777 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -698 522 30.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -698 517 moveto 34 -0.5 (Pfedit) alignedtext -grestore -% Decl_mode->Pfedit -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 698 576 moveto -698 568 698 559 698 550 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 701.5 550 moveto -698 540 lineto -694.5 550 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 701.5 550 moveto -698 540 lineto -694.5 550 lineto -closepath stroke -grestore -% Pfedit->Evar_refiner -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 671 514 moveto -628 503 543 479 488 464 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 488.584 460.521 moveto -478 461 lineto -486.573 467.226 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 488.584 460.521 moveto -478 461 lineto -486.573 467.226 lineto -closepath stroke -grestore -% Pfedit->Tacmach -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 701 504 moveto -702 496 704 487 706 478 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 709.471 478.492 moveto -708 468 lineto -702.607 477.119 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 709.471 478.492 moveto -708 468 lineto -702.607 477.119 lineto -closepath stroke -grestore -% Logic -gsave -0.502 1.000 0.820 nodecolor -439 306 29.1747 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -439 306 29.1747 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -439 301 moveto 33 -0.5 (Logic) alignedtext -grestore -% Refiner->Logic -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 439 360 moveto -439 352 439 343 439 334 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 442.5 334 moveto -439 324 lineto -435.5 334 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 442.5 334 moveto -439 324 lineto -435.5 334 lineto -closepath stroke -grestore -% Proof_trees -gsave -0.502 1.000 0.820 nodecolor -439 234 45.1757 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -439 234 45.1757 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -439 229 moveto 65 -0.5 (Proof_trees) alignedtext -grestore -% Logic->Proof_trees -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 439 288 moveto -439 280 439 271 439 262 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 442.5 262 moveto -439 252 lineto -435.5 262 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 442.5 262 moveto -439 252 lineto -435.5 262 lineto -closepath stroke -grestore -% Proof_type -gsave -0.502 1.000 0.820 nodecolor -439 162 44.1757 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -439 162 44.1757 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -439 157 moveto 63 -0.5 (Proof_type) alignedtext -grestore -% Proof_trees->Proof_type -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 439 216 moveto -439 208 439 199 439 190 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 442.5 190 moveto -439 180 lineto -435.5 190 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 442.5 190 moveto -439 180 lineto -435.5 190 lineto -closepath stroke -grestore -% Decl_expr -gsave -0.502 1.000 0.820 nodecolor -439 90 42.1777 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -439 90 42.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -439 85 moveto 58 -0.5 (Decl_expr) alignedtext -grestore -% Proof_type->Decl_expr -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 439 144 moveto -439 136 439 127 439 118 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 442.5 118 moveto -439 108 lineto -435.5 118 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 442.5 118 moveto -439 108 lineto -435.5 118 lineto -closepath stroke -grestore -% Tacexpr -gsave -0.502 1.000 0.820 nodecolor -439 18 36.1777 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -439 18 36.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -439 13 moveto 46 -0.5 (Tacexpr) alignedtext -grestore -% Decl_expr->Tacexpr -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 439 72 moveto -439 64 439 55 439 46 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 442.5 46 moveto -439 36 lineto -435.5 46 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 442.5 46 moveto -439 36 lineto -435.5 46 lineto -closepath stroke -grestore -% Tactic_debug -gsave -0.502 1.000 0.820 nodecolor -133 450 51.1777 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -133 450 51.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -133 445 moveto 76 -0.5 (Tactic_debug) alignedtext -grestore -% Tactic_debug->Refiner -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 176 440 moveto -234 426 339 401 398 387 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 398.881 390.393 moveto -408 385 lineto -397.508 383.529 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 398.881 390.393 moveto -408 385 lineto -397.508 383.529 lineto -closepath stroke -grestore -endpage -showpage -grestore -%%PageTrailer -%%EndPage: 1 -%%Trailer -%%Pages: 1 -%%BoundingBox: 36 36 576 753 -end -restore -%%EOF diff --git a/dev/ocamlweb-doc/syntax.mly b/dev/ocamlweb-doc/syntax.mly deleted file mode 100644 index bfc7d5cc..00000000 --- a/dev/ocamlweb-doc/syntax.mly +++ /dev/null @@ -1,224 +0,0 @@ -%{ -open Ast -open Parse -%} - -%token META INT IDENT -%token 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 main - -%start constr -%type constr - -%start simple_constr -%type 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 deleted file mode 100644 index f4de22b7..00000000 --- a/dev/ocamlweb-doc/tactics.dep.ps +++ /dev/null @@ -1,991 +0,0 @@ -%!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 deleted file mode 100644 index e0355aac..00000000 --- a/dev/ocamlweb-doc/toplevel.dep.ps +++ /dev/null @@ -1,971 +0,0 @@ -%!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 -- cgit v1.2.3