From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- dev/base_include | 12 +- dev/db | 4 + dev/doc/build-system.dev.txt | 70 ++ dev/doc/build-system.txt | 299 +++++ dev/doc/changes.txt | 33 + dev/doc/header | 7 - dev/doc/notes-on-conversion | 73 ++ dev/doc/perf-analysis | 80 +- dev/header | 7 + dev/include | 9 + dev/ocamldebug-coq.template | 9 +- dev/ocamlweb-doc/Makefile | 21 +- dev/ocamlweb-doc/interp.dep.ps | 672 ++++++----- dev/ocamlweb-doc/kernel.dep.ps | 2343 +++++++++++++++++++-------------------- dev/ocamlweb-doc/library.dep.ps | 1155 +++++++++---------- dev/ocamlweb-doc/proofs.dep.ps | 857 +++++++------- dev/set_raw_db | 1 + dev/top_printers.ml | 73 +- dev/v8-syntax/syntax-v8.tex | 2 +- 19 files changed, 3129 insertions(+), 2598 deletions(-) create mode 100644 dev/doc/build-system.dev.txt create mode 100644 dev/doc/build-system.txt delete mode 100644 dev/doc/header create mode 100644 dev/doc/notes-on-conversion create mode 100644 dev/header create mode 100644 dev/set_raw_db (limited to 'dev') diff --git a/dev/base_include b/dev/base_include index b7fa38ea..398f60d2 100644 --- a/dev/base_include +++ b/dev/base_include @@ -19,6 +19,7 @@ #install_printer (* identifier *) ppid;; #install_printer (* identifier *) ppidset;; +#install_printer (* Intset.t *) ppintset;; #install_printer (* label *) pplab;; #install_printer (* mod_self_id *) ppmsid;; #install_printer (* mod_bound_id *) ppmbid;; @@ -31,6 +32,9 @@ #install_printer (* constr *) print_pure_constr;; #install_printer (* patch *) ppripos;; #install_printer (* values *) ppvalues;; +#install_printer (* Idpred.t *) pp_idpred;; +#install_printer (* Cpred.t *) pp_cpred;; +#install_printer (* transparent_state *) pp_transparent_state;; #install_printer ppzipper;; #install_printer ppstack;; #install_printer ppatom;; @@ -38,6 +42,7 @@ #install_printer ppvblock;; #install_printer (* bigint *) ppbigint;; #install_printer (* loc *) pploc;; +#install_printer (* substitution *) prsubst;; (* Open main files *) @@ -63,12 +68,14 @@ open Pattern open Cbv open Classops open Pretyping +open Pretyping.Default +open Pretyping.Default.Cases open Cbv open Classops -open Pretyping open Clenv open Rawterm open Coercion +open Coercion.Default open Recordops open Detyping open Reductionops @@ -82,6 +89,7 @@ open Indrec open Typing open Inductiveops open Unification +open Matching open Constrextern open Constrintern @@ -167,7 +175,7 @@ open Declarations;; let constbody_of_string s = let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_sp (path_of_string s))) in - Util.out_some b.const_body;; + Option.get b.const_body;; (* Get the current goal *) diff --git a/dev/db b/dev/db index 784e5bac..6221462a 100644 --- a/dev/db +++ b/dev/db @@ -3,6 +3,7 @@ load_printer "printers.cma" install_printer Top_printers.ppid install_printer Top_printers.ppidset +install_printer Top_printers.ppintset install_printer Top_printers.pplab install_printer Top_printers.ppmsid install_printer Top_printers.ppmbid @@ -20,6 +21,7 @@ install_printer Top_printers.pprawconstr install_printer Top_printers.ppconstr install_printer Top_printers.ppuni install_printer Top_printers.ppuniverses +install_printer Top_printers.ppconstraints install_printer Top_printers.pptype install_printer Top_printers.ppj install_printer Top_printers.ppenv @@ -27,6 +29,7 @@ install_printer Top_printers.ppenv install_printer Top_printers.ppgoal install_printer Top_printers.ppsigmagoal install_printer Top_printers.pproof +install_printer Top_printers.ppmetas install_printer Top_printers.ppevd install_printer Top_printers.ppevm install_printer Top_printers.ppclenv @@ -34,5 +37,6 @@ install_printer Top_printers.ppclenv install_printer Top_printers.pptac install_printer Top_printers.ppobj install_printer Top_printers.pploc +install_printer Top_printers.prsubst diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt new file mode 100644 index 00000000..c825f088 --- /dev/null +++ b/dev/doc/build-system.dev.txt @@ -0,0 +1,70 @@ +Since July 2007, Coq features a build system overhauled by Pierre +Corbineau and Lionel Elie Mamane. + +This file documents internals of the implementation of the build +system. For what a Coq developer needs to know about the build system, +see build-system.txt . + +.ml4 files +---------- + +.ml files corresponding to .ml4 files are created to keep ocamldep +happy only. To ensure they are not used for compilation, they contain +invalid OCaml. + +multi-stage build +----------------- + +Le processus de construction est séparé en trois étapes qui correspondent +aux outils nécessaires pour calculer les dépendances de cette étape: + +stage1: ocamldep, sed , camlp4 sans fichiers de Coq +stage2: camlp4 avec grammar.cma et/ou q_constr.cmo +stage3: coqdep (.vo) + +Le Makefile a été séparé en plusieurs fichiers : + +- Makefile: coquille vide qui délègue les cibles à la bonne étape sauf + clean et les fichiers pour emacs (car ils sont en quelque sorte en + "stage0": aucun calcul de dépendance nécessaire). +- Makefile.common : définitions des variables (essentiellement des + listes de fichiers) +- Makefile.build : les règles de compilation sans inclure de + dépendances +- Makefile.stage* : fichiers qui incluent les dépendances calculables + à cette étape ainsi que Makefile.build. + +The build needs to be cut in stages because make will not take into +account one include when making another include. + +Parallélisation +--------------- + +Le découpage en étapes veut dire que le makefile est un petit peu +moins parallélisable que strictement possible en théorie: par exemple, +certaines choses faites en stage2 pourraient être faites en parallèle +avec des choses de stage1. Nous essayons de minimiser cet effet, mais +nous ne l'avons pas complètement éliminé parce que cela mènerait à un +makefile très complexe. La minimisation est principalement que si on +demande un objet spécifique (par exemple "make parsing/g_constr.cmx"), +il est fait dans l'étape la plus basse possible (simplement), mais si +un objet est fait comme dépendance de la cible demandée (par exemple +dans un "make world"), il est fait le plus tard possible (par exemple, +tout code OCaml non nécessaire pour coqdep ni grammar.cma ni +q_constr.cmo est compilé en stage3 lors d'un "make world"; cela permet +le parallélisme de compilation de code OCaml et de fichiers Coq (.v)). + +Le "(simplement)" ci-dessus veut dire que savoir si un fichier non +nécessaire pour grammar.cma/q_constr.cmo peut en fait être fait en +stage1 est compliqué avec make, alors nous retombons en général sur le +stage2. La séparation entre le stage2 et stage3 est plus facile, donc +l'optimisation ci-dessus s'y applique pleinement. + +En d'autres mots, nous avons au niveau conceptuel deux assignations +d'étape pour chaque fichier: + + - l'étape la plus petite où nous savons qu'il peut être fait. + - l'étape la plus grande où il peut être fait. + +Mais seule la première est gérée explicitement, la seconde est +implicite. diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt new file mode 100644 index 00000000..c9571f7c --- /dev/null +++ b/dev/doc/build-system.txt @@ -0,0 +1,299 @@ +Since July 2007, Coq features a build system overhauled by Pierre +Corbineau and Lionel Elie Mamane. + +This file documents what a Coq developer needs to know about the build +system. If you want to enhance the build system itself (or are curious +about its implementation details), see build-system.dev.txt . + +The build system is not at its optimal state, see TODO section. + +Stages in build system +---------------------- + +The build system is separated into three stages, corresponding to the +tool(s) necessary to compute the dependencies necessary at this stage: + +stage1: ocamldep, sed, camlp4 without Coq extensions +stage2: camlp4 with grammar.cma and/or q_constr.cmo +stage3: coqdep (.vo) + +The file "Makefile" itself serves as minimum stage for targets that +should not need any dependency (such as *clean*). + +Changes (for old-timers) +------------------------ + +The contents of the old Makefile has been mostly split into: + + - variable declarations for file lists in Makefile.common. + + These declarations are now static (for faster Makefile execution), + so their definitions are order-dependent. + + - actual building rules and compiler flags variables in + Makefile.build + + +The handling of globals is now: the globals of FOO.v are in FOO.glob +and the global glob.dump is created by concatenation of all .glob +files. In particular, .glob files are now always created. + +See also section "cleaning targets" + +Reducing build system overhead +------------------------------ + +When you are actively working on a file in a "make a change, make to +test, make a change, make to test", etc mode, here are a few tips to +save precious time: + + - Always ask for what you want directly (e.g. bin/coqtop, + foo/bar.cmo, ...), don't do "make world" and interrupt + it when it has done what you want. This will try to minimise the + stage at which what you ask for is done (instead of maximising it + in order to maximise parallelism of the build process). + + For example, if you only want to test whether bin/coqtop still + builds (and eventually start it to test your bugfix or new + feature), don't do "make world" and interrupt it when bin/coqtop is + built. Use "make bin/coqtop" or "make coqbinaries" or something + like that. This will avoid entering the stage 3, and cut build + system overhead by 50% (1.2s instead of 2.4 on writer's machine). + + - You can turn off rebuilding of the standard library each time + bin/coqtop is rebuilt with NO_RECOMPILE_LIB=1. + + - If you want to avoid all .ml4 files being recompiled only because + grammar.cma was rebuilt, do "make ml4depclean" once and then use + NO_RECOMPILE_ML4=1. + + - The CM_STAGE1=1 option to make will build all .cm* files mentioned + as targets on the command line in stage1. Whether this will work is + your responsibility. It should work for .ml files that don't depend + (nor directly nor indirectly through transitive closure of the + dependencies) on any .ml4 file, or where those dependencies can be + safely ignored in the current situation (e.g. all these .ml4 files + don't need to be recompiled). + + This will avoid entering the stage2 (a reduction of 33% in + overhead, 0.4s on the writer's machine). + + - To jump directly into a stage (e.g. because you know nothing is to + be done in stage 1 or (1 and 2) or because you know that the target + you give can be, in this situation, done in a lower stage than the + build system dares to), use GOTO_STAGE=n. This will jump into stage + n and try to do the targets you gave in that stage. + + - To disable all dependency recalculation, use the NO_RECALC_DEPS=1 + option. It disables REcalculation of dependencies, not calculation + of dependencies. In other words, if a .d file does not exist, it is + still created, but it is not updated every time the source file + (e.g. .ml) is changed. + +General speed improvements: + + - When building both the native and bytecode versions, the + KEEP_ML4_PREPROCESSED=1 option may reduce global compilation time + by running camlp4o only once on every .ml4 file, at the expense of + readability of compilation error messages for .ml4 files. + +Dependencies +------------ + +There are no dependencies in the archive anymore, they are always +bootstrapped. The dependencies of a file FOO are in FOO.d . This +enables partial recalculation of dependencies (only the dependencies +of changed files are recomputed). + +If you add a dependency to a Coq camlp4 extension (grammar.cma or +q_constr.cmo), then see sections ".ml4 files" and "new files". + +Cleaning Targets +---------------- + +Targets for cleaning various parts: + + - distclean: clean everything; must leave only what should end up in + distribution tarball and/or is in a svn checkout. + + - clean: clean everything except effect of "./configure" and documentation. + + - cleanconfig: clean effect of "./configure" only + + - archclean: remove all architecture-dependent generated files + - indepclean: remove all architecture-independent generated files + (not documentation) + + - objclean: clean all generated files, but not Makefile meta-data + (e.g. dependencies), nor debugging/development information nor + other cruft (e.g. editor backup files), nor documentation + + - docclean: clean documentation + +.ml4 files +---------- + +The camlp4-preprocessed version of FOO.ml4 is FOO.ml4-preprocessed and +can be obtained with: + make FOO.ml4-preprocessed + +If a .ml4 file uses a grammar extension from Coq (such as grammar.cma +or q_constr.cmo), it must contain a line like: + (*i camlp4deps: "grammar.cma q_constr.cmo" i*) + +If it uses a standard grammar extension, it must contain a line like: + (*i camlp4use: "pa_ifdef.cmo" i*) + +It can naturally contain both a camlp4deps and a camlp4use line. Both +are used for preprocessing. It is thus _not_ necessary to add a +specific rule for a .ml4 file in the Makefile.build just because it +uses grammar extensions. + +By default, the build system is geared towards development that may +use the Coq grammar extensions, but not development of Coq's grammar +extensions themselves. This means that .ml4 files are compiled +directly (using ocamlc/opt's -pp option), without use of an +intermediary .ml (or .ml4-preprocessed) file. This is so that if a +compilation error occurs, the location in the error message is a +location in the .ml4 file. If you are modifying the grammar +extensions, you may be more interested in the location of the error in +the .ml4-preprocessed file, so that you can see what your new grammar +extension made wrong. In that case, use the KEEP_ML4_PREPROCESSED=1 +option. This will make compilation of a .ml4 file a two-stage process: + +1) create the .ml4-preprocessed file with camlp4o +2) compile it with straight ocamlc/opt without preprocessor + +and will instruct make not to delete .ml4-preprocessed files +automatically just because they are intermediary files, so that you +can inspect them. + +If you add a _new_ grammar extension to Coq: + + - if it can be built at stage1, that is the .ml4 file does not use a + Coq grammar extension itself, then add it, and all .cmo files it + needs to STAGE1_TARGETS and STAGE_ML4 in Makefile.common. See the + handling of grammar.cma and q_constr.cmo for an example. + + - if it cannot be built at stage1, that is the .ml4 file itself needs + to be preprocessed with a Coq camlp4 grammar extension, then, + congratulations, you need to add a new stage between stage1 and + stage2. + +New files +--------- + +For a new file, in most cases, you just have to add it to the proper +file list(s) in Makefile.common, such as ARITHVO or TACTICS. + +The list of all ml4 files is not handled manually anymore. + +Exceptions are: + + - The file is necessary at stage1, that it is necessary to build the + Coq camlp4 grammar extensions. In this case, make sure it ends up + in STAGE1_CMO and (for .ml4 files) STAGE1_ML4. See the handling of + grammar.cma and/or q_constr.cmo for an example. + + - if the file needs to be compiled with -rectypes, add it to + RECTYPESML in Makefile.common. If it is a .ml4 file, implement + RECTYPESML4 or '(*i ocamlflags i*)'; see TODO. + + - the file needs a specific Makefile entry; add it to Makefile.build + + - the files produced from the added file do not match an existing + pattern or entry in "Makefile". (All the common cases of + .ml{,i,l,y,4}, .v, .c, ... files that produces (respectively) + .cm[iox], .vo, .glob, .o, ... files with the same basename are + already covered.) In this case, see section "New targets". + +New targets +----------- + +If you want to add: + + - a new PHONY target to the build system, that is a target that is + not the name of the file it creates, + + - a normal target is not already mapped to a stage by "Makefile" + + then: + + - add the necessary rule to Makefile.build, if any + - add the target to STAGEn_TARGETS, with n being the smallest stage + it can be built at, that is: + * 1 for OCaml code that doesn't use any Coq camlp4 grammar extension + * 2 for OCaml code that uses (directly or indirectly) a Coq + camlp4 grammar extension. Indirectly means a dependency of it + does. + * 3 for Coq (.v) code. + + *or* + + add a pattern matching the target to the pattern lists for the + smallest stage it can be built at in "Makefile". + +TODO +---- + +delegate pa_extend.cmo to camlp4use statements and remove it from +standard camlp4 options. + +maybe manage compilation flags (such as -rectypes or the CoqIDE ones) +from a + (*i ocamlflags: "-rectypes" i*) +statement in the .ml(4) files themselves, like camlp4use. The CoqIDE +files could have + (*i ocamlflags: "${COQIDEFLAGS}" i*) +and COQIDEFLAGS is still defined (and exported by) the Makefile.build. + +Clean up doc/Makefile + +config/Makefile looks like it contains a lot of unused variables, +clean that up (are any maybe used by nightly scripts on +pauillac?). Also, the COQTOP variable from config/Makefile (and used +in contribs) has a very poorly chosen name, because "coqtop" is the +name of a Coq executable! For example, in the Coq makefile it is +immediately clobbered by "bin/coqtop$(EXE)"! Rename it to COQROOT or +COQTREE or COQDIR or ... + +Promote the granular .glob handling to official way of doing things +for Coq developments, that is implement it in coq_makefile and the +contribs. Here are a few hints: + +>> Les fichiers de constantes produits par -dump-glob sont maintenant +>> produits par fichier et sont ensuite concaténés dans +>> glob.dump. Ilsont produits par défaut (avec les bonnes +>> dépendances). + +> C'est une chose que l'on voulait faire aussi. + +(J'ai testé et débogué ce concept sur CoRN dans les derniers mois.) + +> Est-ce que vous sauriez modifier coq_makefile pour qu'il procède de +> la même façon + +Dans cette optique, il serait alors plus propre de changer coqdep pour +qu'il produise directement l'output que nous mettons maintenant dans +les .v.d (qui est celui de coqdoc post-processé avec sed). + +Si cette manière de gérer les glob devient le standard béni +officiellement par "the Coq development team", ne voudrions nous pas +changer coqc pour qu'il produise FOO.glob lors de la compilation de +FOO.v par défaut (sans argument "-dump-glob")? + +> et que la production de a.html par coqdoc n'ait une dépendance qu'en +> les a.v et a.glob correspondant ? + +Je crois que coqdoc exige un glob-dump unique, il convient donc de +concaténer les .glob correspondants. Soit un glob-dump global par +projet (par Makefile), soit un glob-dump global par .v(o), qui +contient son .glob et ceux de tous les .v(o) atteignables par le +graphe des dépendances. CoRN contient déjà un outil de calcul de +partie atteignable du graphe des dépendances (il y est pour un autre +usage, pour calculer les .v à mettre dans les différents tarballs sur +http://corn.cs.ru.nl/download.html; les parties partielles sont +définies par liste de fichiers .v + toutes leurs dépendances +(in)directes), il serait alors adéquat de le mettre dans les tools de +Coq. + diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 90e29496..b7545e09 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,3 +1,36 @@ +========================================= += CHANGES BETWEEN COQ V8.1 AND COQ V8.2 = +========================================= + +A few differences in Coq ML interfaces between Coq V8.1 and V8.2 +================================================================ + +** Datatypes + +List of occurrences moved from "int list" to "Termops.occurrences" (an +alias to "bool * int list"). + +** Functions + +Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply +Tactics: apply_with_bindings -> apply_with_bindings_wo_evars +Eauto.simplest_apply -> Hiddentac.h_simplest_apply +Evarutil.define_evar_as_arrow -> define_evar_as_product + +** Universe names (univ.mli) + + base_univ -> type0_univ (* alias of Set is the Type hierarchy *) + prop_univ -> type1_univ (* the type of Set in the Type hierarchy *) + neutral_univ -> lower_univ (* semantic alias of Prop in the Type hierarchy *) + is_base_univ -> is_type1_univ + is_empty_univ -> is_lower_univ + +** Sort names (term.mli) + + mk_Set -> set_sort + mk_Prop -> prop_sort + type_0 -> type1_sort + ========================================= = CHANGES BETWEEN COQ V8.0 AND COQ V8.1 = ========================================= diff --git a/dev/doc/header b/dev/doc/header deleted file mode 100644 index 57945e47..00000000 --- a/dev/doc/header +++ /dev/null @@ -1,7 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* nat := + match n0 with + | O => S + | S n1 => + fun m : nat => + (fix F0 (n2 : nat) : nat := + match n2 with + | O => F n1 1 + | S n3 => F n1 (F0 n3) + end) m + end) n. + +Notation OMEGA := (ack 4 4). + +Definition f (x:nat) := x. + +(* Evaluation in tactics can somehow be controled *) +Lemma l1 : OMEGA = OMEGA. +reflexivity. (* succeed: identity *) +Qed. (* succeed: identity *) + +Lemma l2 : OMEGA = f OMEGA. +reflexivity. (* fail: conversion wants to convert OMEGA with f OMEGA *) +Abort. (* but it reduces the right side first! *) + +Lemma l3 : f OMEGA = OMEGA. +reflexivity. (* succeed: reduce left side first *) +Qed. (* succeed: expected concl (the one with f) is on the left *) + +Lemma l4 : OMEGA = OMEGA. +assert (f OMEGA = OMEGA) by reflexivity. (* succeed *) +unfold f in H. (* succeed: no type-checking *) +exact H. (* succeed: identity *) +Qed. (* fail: "f" is on the left *) + +(* This example would fail whatever the preferred side is *) +Lemma l5 : OMEGA = f OMEGA. +unfold f. +assert (f OMEGA = OMEGA) by reflexivity. +unfold f in H. +exact H. +Qed. (* needs to convert (f OMEGA = OMEGA) and (OMEGA = f OMEGA) *) + +(**********************************************************************) +(* Analysis of the inefficiency in Nijmegen/LinAlg/LinAlg/subspace_dim.v *) +(* (proof of span_ind_uninject_prop *) + +In the proof, a problem of the form (Equal S t1 t2) +is "simpl"ified, then "red"uced to (Equal S' t1 t1) +where the new t1's are surrounded by invisible coercions. +A reflexivity steps conclude the proof. + +The trick is that Equal projects the equality in the setoid S, and +that (Equal S) itself reduces to some (fun x y => Equal S' (f x) (g y)). + +At the Qed time, the problem to solve is (Equal S t1 t2) = (Equal S' t1 t1) +and the algorithm is to first compare S and S', and t1 and t2. +Unfortunately it does not work, and since t1 and t2 involve concrete +instances of algebraic structures, it takes a lot of time to realize that +it is not convertible. + +The only hope to improve this problem is to observe that S' hides +(behind two indirections) a Setoid constructor. This could be the +argument to solve the problem. + + diff --git a/dev/doc/perf-analysis b/dev/doc/perf-analysis index f4cb3bff..8e481544 100644 --- a/dev/doc/perf-analysis +++ b/dev/doc/perf-analysis @@ -1,13 +1,79 @@ -Performance analysis for V8-0 branch ------------------------------------- +Performance analysis (trunk repository) +--------------------------------------- -Oct 29, 2006: polymorphism on definitions (+ 4%) +May 21, 2008: New version of CoRN + (needs +84% more time to compile) + +Apr 25-29, 2008: Temporary attempt with delta in eauto (Matthieu) + (+28% CoRN) + +Apr 17, 2008: improvement probably due to commit 10807 or 10813 (bug + fixes, control of zeta in rewrite, auto (??)) + (-18% Buchberger, -40% PAutomata, -28% IntMap, -43% CoRN, -13% LinAlg, + but CatsInZFC -0.5% only, PiCalc stable, PersistentUnionFind -1%) + +Mar 11, 2008: + (+19% PersistentUnionFind wrt Mar 3, +21% Angles, + +270% Continuations between 7/3 and 18/4) + +Mar 7, 2008: + (-10% PersistentUnionFind wrt Mar 3) + +Feb 20, 2008: temporary 1-day slow down + (+64% LinAlg) + +Feb 14, 2008: + (-10% PersistentUnionFind, -19% Groups) + +Feb 7, 8, 2008: temporary 2-days long slow down + (+20 LinAlg, +50% BDDs) + +Feb 2, 2008: many updates of the module system + (-13% LinAlg, -50% AMM11262, -5% Goedel, -1% PersistentUnionFind, + -42% ExactRealArithmetic, -41% Icharate, -42% Kildall, -74% SquareMatrices) + +Jan 1, 2008: merge of TypeClasses branch + (+8% PersistentUnionFind, +36% LinAlg, +76% Goedel) + +Nov 16, 17, 2007: + (+18% Cantor, +4% LinAlg, +27% IEEE1394 on 2 days) + +Nov 8, 2007: + (+18% Cantor, +16% LinAlg, +55% Continuations, +200% IEEE1394, +170% CTLTCTL, + +220% SquareMatrices) + +Oct 29, V8.1 (+ 3% geometry but CoRN, Godel, Kildall, Stalmark stables) + +Between Oct 12 and Oct 27, 2007: inefficiency temporarily introduced in the + tactic interpreter (from revision 10222 to 10267) + (+22% CoRN, +10% geometry, ...) + +Sep 16, 2007: + (+16% PersistentUnionFind on 3 days, LinAlg stable, + +Sep 4, 2007: + (+26% PersistentUnionFind, LinAlg stable, + +Jun 6, 2007: optimization of the need for type unification in with-bindings + (-3.5% Stalmark, -6% Kildall) + +May 20, 21, 22, 2007: improved inference of with-bindings (including activation + of unification on types) + (+4% PICALC, +5% Stalmark, +7% Kildall) + +May 11, 2007: added primitive integers (+6% CoLoR, +7% CoRN, +5% FSets, ...) + +Between Feb 22 and March 16, 2007: bench temporarily moved on JMN's + computer (-25% CoRN, -25% Fairisle, ...) + +Oct 29 and Oct 30, 2006: abandoned attempt to add polymorphism on definitions + (+4% in general during these two days) Oct 17, 2006: improvement in new field [r9248] (QArith -3%, geometry: -2%) Oct 5, 2006: fixing wrong unification of Meta below binders - (e.g. CatsInZFC: +10%, CoRN: -2.5%, Godel: +4%, + (e.g. CatsInZFC: +10%, CoRN: -2.5%, Godel: +4%, LinAlg: +7%, DISTRIBUTED_REFERENCE_COUNTING: +10%, CoLoR: +1%) Sep 26, 2006: new field [r9178-9181] @@ -17,11 +83,17 @@ Sep 26, 2006: new field [r9178-9181] Aug 12, 2006: Rocq/AREA_METHOD added (~ 480s) May 30, 2006: Nancy/CoLoR added (~ 319s) +May 23, 2006: new, lighter version of polymorphic inductive types + (CoRN: -27%, back to Mar-24 time) + May 17, 2006: changes in List.v (DISTRIBUTED_REFERENCE_COUNTING: -) May 5, 2006: improvement in closure (array instead of lists) (e.g. CatsInZFC: -10%, CoRN: -3%, +May 23, 2006: polymorphic inductive types (precise, heavy algorithm) + (CoRN: +37%) + Dec 29, 2005: new test and use of -vm in Stalmarck Dec 27, 2005: contrib Karatsuba added (~ 30s) diff --git a/dev/header b/dev/header new file mode 100644 index 00000000..57945e47 --- /dev/null +++ b/dev/header @@ -0,0 +1,7 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* $@ +%.dot: ../../% + ocamldoc -rectypes $(MLINCLUDES) -t $* -dot -dot-reduce ../../$*/*.ml ../../$*/*.mli -o $@ %.dep.ps: %.dot dot -Tps $< -o $@ diff --git a/dev/ocamlweb-doc/interp.dep.ps b/dev/ocamlweb-doc/interp.dep.ps index b0554481..fda7a33c 100644 --- a/dev/ocamlweb-doc/interp.dep.ps +++ b/dev/ocamlweb-doc/interp.dep.ps @@ -1,9 +1,9 @@ %!PS-Adobe-2.0 -%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) -%%For: (herbelin) Hugo Herbelin +%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007) +%%For: (notin) Jean-Marc Notin,,, %%Title: G %%Pages: (atend) -%%BoundingBox: 35 35 577 160 +%%BoundingBox: (atend) %%EndComments save %%BeginProlog @@ -16,57 +16,7 @@ mark 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 +EncodingVector 45 /hyphen put % Set up ISO Latin 1 character encoding /starnetISO { @@ -98,8 +48,8 @@ cleartomark /InvScaleFactor 1.0 def /set_scale { - dup 1 exch div /InvScaleFactor exch def - dup scale + dup 1 exch div /InvScaleFactor exch def + scale } bind def % styles @@ -229,348 +179,359 @@ def } if %%EndSetup +setupLatin1 %%Page: 1 1 -%%PageBoundingBox: 36 36 577 160 -%%PageOrientation: Portrait +%%PageBoundingBox: 36 36 576 753 +%%PageOrientation: Landscape gsave -35 35 542 125 boxprim clip newpath -36 36 translate +36 36 576 753 boxprim clip newpath 0 0 1 beginpage -0.9343 set_scale -0 0 translate 0 rotate -0.000 0.000 0.000 graphcolor +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 - -% Syntax_def -gsave 10 dict begin -303 110 45 18 ellipse_path -stroke -gsave 10 dict begin -271 105 moveto -(Syntax_def) -[7.68 6.96 6.96 4.08 6.24 6.96 6.96 6.96 6.24 4.56] -xshow -end grestore -end grestore - -% Notation -gsave 10 dict begin -422 60 38 18 ellipse_path -stroke -gsave 10 dict begin -397 55 moveto -(Notation) -[9.84 6.72 4.08 6.24 3.84 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Syntax_def -> Notation -newpath 334 97 moveto -350 90 369 83 385 76 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 386 79 moveto -394 72 lineto -383 73 lineto -closepath -fill +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 386 79 moveto -394 72 lineto -383 73 lineto -closepath -stroke -end grestore - -% Ppextend -gsave 10 dict begin -537 60 39 18 ellipse_path +newpath 178 399 moveto +194 349 240 209 259 150 curveto stroke -gsave 10 dict begin -511 55 moveto -(Ppextend) -[7.68 6.96 5.76 6.96 3.84 6.24 6.96 6.96] -xshow -end grestore -end grestore - -% Notation -> Ppextend -newpath 460 60 moveto -469 60 478 60 488 60 curveto -stroke -gsave 10 dict begin +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 -1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 488 64 moveto -498 60 lineto -488 57 lineto -closepath -fill +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 488 64 moveto -498 60 lineto -488 57 lineto -closepath -stroke -end grestore - -% Topconstr -gsave 10 dict begin -537 114 41 18 ellipse_path +newpath 243 109 moveto +211 91 154 62 117 43 curveto stroke -gsave 10 dict begin -509 109 moveto -(Topconstr) -[7.2 6.96 6.96 6.24 6.96 6.96 5.28 3.84 4.56] -xshow -end grestore -end grestore - -% Notation -> Topconstr -newpath 449 73 moveto -464 80 483 89 500 97 curveto -stroke -gsave 10 dict begin +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 -1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 498 100 moveto -509 101 lineto -501 94 lineto -closepath -fill +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 498 100 moveto -509 101 lineto -501 94 lineto -closepath -stroke -end grestore - -% Modintern -gsave 10 dict begin -44 98 43 18 ellipse_path -stroke -gsave 10 dict begin -13 93 moveto -(Modintern) -[12.48 6.96 6.96 3.84 6.96 3.84 6.24 4.8 6.96] -xshow -end grestore -end grestore - -% Constrintern -gsave 10 dict begin -173 98 48 18 ellipse_path +newpath 270 104 moveto +272 89 273 68 275 52 curveto stroke -gsave 10 dict begin -138 93 moveto -(Constrintern) -[9.36 6.96 6.96 5.28 3.84 4.8 3.84 6.96 3.84 6.24 4.8 6.96] -xshow -end grestore -end grestore - -% Modintern -> Constrintern -newpath 88 98 moveto -97 98 106 98 115 98 curveto -stroke -gsave 10 dict begin +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 -1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 115 102 moveto -125 98 lineto -115 95 lineto -closepath -fill +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 115 102 moveto -125 98 lineto -115 95 lineto -closepath -stroke -end grestore - -% Constrintern -> Syntax_def -newpath 220 102 moveto -229 103 239 104 249 105 curveto +newpath 442 403 moveto +404 385 340 355 299 335 curveto stroke -gsave 10 dict begin +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 -1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 249 108 moveto -259 106 lineto -249 102 lineto -closepath -fill +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 249 108 moveto -259 106 lineto -249 102 lineto -closepath +newpath 479 399 moveto +484 385 492 364 498 347 curveto stroke -end grestore - -% Reserve -gsave 10 dict begin -303 56 35 18 ellipse_path -stroke -gsave 10 dict begin -280 51 moveto -(Reserve) -[9.12 6.24 5.52 6.24 4.8 6.48 6.24] -xshow -end grestore -end grestore - -% Constrintern -> Reserve -newpath 210 86 moveto -227 81 246 75 263 69 curveto -stroke -gsave 10 dict begin +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 -1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 264 72 moveto -273 66 lineto -262 66 lineto -closepath -fill +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 264 72 moveto -273 66 lineto -262 66 lineto -closepath -stroke -end grestore - -% Genarg -gsave 10 dict begin -422 114 33 18 ellipse_path -stroke -gsave 10 dict begin -401 109 moveto -(Genarg) -[10.08 6.24 6.96 6.24 4.32 6.96] -xshow -end grestore -end grestore - -% Genarg -> Topconstr -newpath 456 114 moveto -465 114 476 114 486 114 curveto +newpath 488 302 moveto +469 285 442 261 422 244 curveto stroke -gsave 10 dict begin +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 -1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 486 118 moveto -496 114 lineto -486 111 lineto -closepath -fill +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 486 118 moveto -496 114 lineto -486 111 lineto -closepath -stroke -end grestore - -% Coqlib -gsave 10 dict begin -44 21 32 18 ellipse_path -stroke -gsave 10 dict begin -24 16 moveto -(Coqlib) -[9.36 6.96 6.96 3.84 3.84 6.96] -xshow -end grestore -end grestore - -% Constrextern -gsave 10 dict begin -173 21 49 18 ellipse_path +newpath 82 104 moveto +82 89 82 69 82 52 curveto stroke -gsave 10 dict begin -137 16 moveto -(Constrextern) -[9.36 6.96 6.96 5.28 3.84 4.56 5.76 6.96 3.84 6.24 4.8 6.96] -xshow -end grestore -end grestore - -% Coqlib -> Constrextern -newpath 77 21 moveto -88 21 101 21 114 21 curveto -stroke -gsave 10 dict begin +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 -1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 114 25 moveto -124 21 lineto -114 18 lineto -closepath -fill +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 114 25 moveto -124 21 lineto -114 18 lineto -closepath -stroke -end grestore - -% Constrextern -> Notation -newpath 222 19 moveto -257 18 307 20 348 29 curveto -361 31 375 37 388 42 curveto +newpath 375 204 moveto +354 187 320 161 296 143 curveto stroke -gsave 10 dict begin +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 -1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 386 45 moveto -397 46 lineto -389 39 lineto -closepath -fill +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 386 45 moveto -397 46 lineto -389 39 lineto -closepath +newpath 472 497 moveto +472 482 472 462 472 445 curveto stroke -end grestore - -% Constrextern -> Reserve -newpath 213 32 moveto -228 36 246 41 261 45 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth 0.000 0.000 0.000 edgecolor -newpath 260 48 moveto -271 48 lineto -262 42 lineto -closepath -fill +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 260 48 moveto -271 48 lineto -262 42 lineto -closepath -stroke -end grestore +newpath 475.5 445 moveto +472 435 lineto +468.5 445 lineto +closepath stroke +grestore endpage showpage grestore @@ -578,6 +539,7 @@ grestore %%EndPage: 1 %%Trailer %%Pages: 1 +%%BoundingBox: 36 36 576 753 end restore %%EOF diff --git a/dev/ocamlweb-doc/kernel.dep.ps b/dev/ocamlweb-doc/kernel.dep.ps index 3c00121e..b7b4137b 100644 --- a/dev/ocamlweb-doc/kernel.dep.ps +++ b/dev/ocamlweb-doc/kernel.dep.ps @@ -1,9 +1,9 @@ %!PS-Adobe-2.0 -%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) -%%For: (herbelin) Hugo Herbelin +%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007) +%%For: (notin) Jean-Marc Notin,,, %%Title: G %%Pages: (atend) -%%BoundingBox: 35 35 577 127 +%%BoundingBox: (atend) %%EndComments save %%BeginProlog @@ -16,57 +16,7 @@ mark 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 +EncodingVector 45 /hyphen put % Set up ISO Latin 1 character encoding /starnetISO { @@ -98,8 +48,8 @@ cleartomark /InvScaleFactor 1.0 def /set_scale { - dup 1 exch div /InvScaleFactor exch def - dup scale + dup 1 exch div /InvScaleFactor exch def + scale } bind def % styles @@ -229,1219 +179,1245 @@ def } if %%EndSetup +setupLatin1 %%Page: 1 1 -%%PageBoundingBox: 36 36 577 127 -%%PageOrientation: Portrait +%%PageBoundingBox: 36 36 535 756 +%%PageOrientation: Landscape gsave -35 35 542 92 boxprim clip newpath -36 36 translate +36 36 535 756 boxprim clip newpath 0 0 1 beginpage -0.2845 set_scale -0 0 translate 0 rotate -0.000 0.000 0.000 graphcolor +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 - -% Vm -gsave 10 dict begin -801 294 27 18 ellipse_path -stroke -gsave 10 dict begin -789 289 moveto -(Vm) -[10.08 10.8] -xshow -end grestore -end grestore - -% Cemitcodes -gsave 10 dict begin -1427 200 46 18 ellipse_path -stroke -gsave 10 dict begin -1393 195 moveto -(Cemitcodes) -[9.36 6.24 10.8 3.84 3.84 6.24 6.96 6.96 6.24 5.52] -xshow -end grestore -end grestore - -% Vm -> Cemitcodes -newpath 826 287 moveto -871 276 969 254 1053 254 curveto -1053 254 1053 254 1174 254 curveto -1249 254 1332 231 1382 215 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1383 218 moveto -1392 212 lineto -1381 212 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1383 218 moveto -1392 212 lineto -1381 212 lineto -closepath -stroke -end grestore - -% Conv_oracle -gsave 10 dict begin -1053 300 48 18 ellipse_path -stroke -gsave 10 dict begin -1017 295 moveto -(Conv_oracle) -[9.36 6.96 6.48 6.96 6.96 6.96 4.56 6.24 6.24 3.84 6.24] -xshow -end grestore -end grestore - -% Vm -> Conv_oracle -newpath 828 295 moveto -868 296 942 298 995 299 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 995 303 moveto -1005 299 lineto -995 296 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 995 303 moveto -1005 299 lineto -995 296 lineto -closepath -stroke -end grestore - -% Mod_subst -gsave 10 dict begin -1556 146 45 18 ellipse_path -stroke -gsave 10 dict begin -1524 141 moveto -(Mod_subst) -[12.48 6.96 6.96 6.96 5.52 6.96 6.96 5.28 3.84] -xshow -end grestore -end grestore - -% Cemitcodes -> Mod_subst -newpath 1459 187 moveto -1476 180 1497 171 1516 163 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1517 166 moveto -1525 159 lineto -1514 160 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1517 166 moveto -1525 159 lineto -1514 160 lineto -closepath -stroke -end grestore - -% Cbytecodes -gsave 10 dict begin -1556 200 45 18 ellipse_path -stroke -gsave 10 dict begin -1523 195 moveto -(Cbytecodes) -[9.36 6.48 6.96 3.84 6.24 6.24 6.96 6.96 6.24 5.52] -xshow -end grestore -end grestore - -% Cemitcodes -> Cbytecodes -newpath 1474 200 moveto -1482 200 1491 200 1500 200 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1500 204 moveto -1510 200 lineto -1500 197 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1500 204 moveto -1510 200 lineto -1500 197 lineto -closepath -stroke -end grestore - -% Copcodes -gsave 10 dict begin -1556 254 41 18 ellipse_path -stroke -gsave 10 dict begin -1528 249 moveto -(Copcodes) -[9.36 6.96 6.96 6.24 6.96 6.96 6.24 5.52] -xshow -end grestore -end grestore - -% Cemitcodes -> Copcodes -newpath 1459 213 moveto -1476 221 1498 230 1517 237 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1515 240 moveto -1526 241 lineto -1518 234 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1515 240 moveto -1526 241 lineto -1518 234 lineto -closepath -stroke -end grestore - -% Names -gsave 10 dict begin -1865 270 33 18 ellipse_path -stroke -gsave 10 dict begin -1845 265 moveto -(Names) -[9.6 6.24 10.8 6.24 5.52] -xshow -end grestore -end grestore - -% Conv_oracle -> Names -newpath 1102 300 moveto -1151 300 1228 300 1295 300 curveto -1295 300 1295 300 1666 300 curveto -1722 300 1785 288 1825 279 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1826 282 moveto -1835 277 lineto -1825 276 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1826 282 moveto -1835 277 lineto -1825 276 lineto -closepath -stroke -end grestore - -% Vconv -gsave 10 dict begin -552 202 32 18 ellipse_path -stroke -gsave 10 dict begin -533 197 moveto -(Vconv) -[10.08 6.24 6.96 6.48 6.96] -xshow -end grestore -end grestore - -% Csymtable -gsave 10 dict begin -674 202 43 18 ellipse_path -stroke -gsave 10 dict begin -643 197 moveto -(Csymtable) -[9.36 5.52 6.96 10.8 4.08 6.24 6.96 3.84 6.24] -xshow -end grestore -end grestore - -% Vconv -> Csymtable -newpath 584 202 moveto -595 202 608 202 620 202 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 620 206 moveto -630 202 lineto -620 199 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 620 206 moveto -630 202 lineto -620 199 lineto -closepath -stroke -end grestore - -% Inductive -gsave 10 dict begin -674 110 39 18 ellipse_path -stroke -gsave 10 dict begin -647 105 moveto -(Inductive) -[4.56 6.96 6.96 6.96 6.24 3.84 3.84 6.48 6.24] -xshow -end grestore -end grestore - -% Vconv -> Inductive -newpath 571 187 moveto -591 172 622 149 645 132 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 647 135 moveto -653 126 lineto -643 129 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 647 135 moveto -653 126 lineto -643 129 lineto -closepath -stroke -end grestore - -% Csymtable -> Vm -newpath 696 218 moveto -717 234 751 258 775 275 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 773 278 moveto -783 281 lineto -777 272 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 773 278 moveto -783 281 lineto -777 272 lineto -closepath -stroke -end grestore - -% Cbytegen -gsave 10 dict begin -801 164 39 18 ellipse_path -stroke -gsave 10 dict begin -774 159 moveto -(Cbytegen) -[9.36 6.48 6.96 3.84 6.24 6.72 6.24 6.96] -xshow -end grestore -end grestore - -% Csymtable -> Cbytegen -newpath 709 191 moveto -724 187 742 181 758 177 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 759 180 moveto -768 174 lineto -757 174 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 759 180 moveto -768 174 lineto -757 174 lineto -closepath -stroke -end grestore - -% Type_errors -gsave 10 dict begin -801 110 47 18 ellipse_path -stroke -gsave 10 dict begin -767 105 moveto -(Type_errors) -[6.96 6.96 6.96 6.24 6.96 6.24 5.04 4.56 6.96 4.56 5.52] -xshow -end grestore -end grestore - -% Inductive -> Type_errors -newpath 714 110 moveto -724 110 734 110 744 110 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 744 114 moveto -754 110 lineto -744 107 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 744 114 moveto -754 110 lineto -744 107 lineto -closepath -stroke -end grestore - -% Univ -gsave 10 dict begin -1763 241 27 18 ellipse_path -stroke -gsave 10 dict begin -1748 236 moveto -(Univ) -[9.6 6.96 3.84 6.96] -xshow -end grestore -end grestore - -% Univ -> Names -newpath 1788 248 moveto -1800 251 1814 255 1826 259 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1825 262 moveto -1836 262 lineto -1827 256 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1825 262 moveto -1836 262 lineto -1827 256 lineto -closepath -stroke -end grestore - -% Typeops -gsave 10 dict begin -552 110 36 18 ellipse_path -stroke -gsave 10 dict begin -528 105 moveto -(Typeops) -[6.96 6.96 6.96 6.24 6.96 6.96 5.52] -xshow -end grestore -end grestore - -% Typeops -> Inductive -newpath 589 110 moveto -600 110 612 110 624 110 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 624 114 moveto -634 110 lineto -624 107 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 624 114 moveto -634 110 lineto -624 107 lineto -closepath -stroke -end grestore - -% Entries -gsave 10 dict begin -801 56 33 18 ellipse_path -stroke -gsave 10 dict begin -780 51 moveto -(Entries) -[8.4 6.96 3.84 4.8 3.84 6.24 5.52] -xshow -end grestore -end grestore - -% Typeops -> Entries -newpath 581 99 moveto -595 93 614 87 630 83 curveto -673 73 723 66 758 61 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 758 64 moveto -768 60 lineto -758 58 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 758 64 moveto -768 60 lineto -758 58 lineto -closepath -stroke -end grestore - -% Sign -gsave 10 dict begin -1427 100 27 18 ellipse_path -stroke -gsave 10 dict begin -1414 95 moveto -(Sign) -[7.68 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Entries -> Sign -newpath 834 61 moveto -882 68 974 79 1053 79 curveto -1053 79 1053 79 1174 79 curveto -1251 79 1342 89 1390 95 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1390 98 moveto -1400 96 lineto -1390 92 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1390 98 moveto -1400 96 lineto -1390 92 lineto -closepath -stroke -end grestore - -% Reduction -gsave 10 dict begin -926 208 42 18 ellipse_path -stroke -gsave 10 dict begin -897 203 moveto -(Reduction) -[9.12 6.24 6.96 6.96 6.24 3.84 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Type_errors -> Reduction -newpath 829 125 moveto -836 129 842 133 848 137 curveto -868 151 887 170 902 184 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 900 187 moveto -910 191 lineto -905 182 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 900 187 moveto -910 191 lineto -905 182 lineto -closepath -stroke -end grestore - -% Reduction -> Conv_oracle -newpath 948 224 moveto -968 239 999 261 1023 278 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1021 281 moveto -1031 284 lineto -1025 275 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1021 281 moveto -1031 284 lineto -1025 275 lineto -closepath -stroke -end grestore - -% Closure -gsave 10 dict begin -1053 208 35 18 ellipse_path -stroke -gsave 10 dict begin -1031 203 moveto -(Closure) -[9.36 3.84 6.96 5.52 6.96 4.56 6.24] -xshow -end grestore -end grestore - -% Reduction -> Closure -newpath 968 208 moveto -981 208 994 208 1008 208 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1008 212 moveto -1018 208 lineto -1008 205 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1008 212 moveto -1018 208 lineto -1008 205 lineto -closepath -stroke -end grestore - -% Term_typing -gsave 10 dict begin -313 110 49 18 ellipse_path -stroke -gsave 10 dict begin -277 105 moveto -(Term_typing) -[7.2 6.24 4.8 10.8 6.96 3.84 6.96 6.96 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Term_typing -> Cbytegen -newpath 347 123 moveto -363 128 381 134 398 137 curveto -524 161 675 165 752 165 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 752 169 moveto -762 165 lineto -752 162 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 752 169 moveto -762 165 lineto -752 162 lineto -closepath -stroke -end grestore - -% Cooking -gsave 10 dict begin -436 225 37 18 ellipse_path -stroke -gsave 10 dict begin -411 220 moveto -(Cooking) -[9.36 6.96 6.96 6.96 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Term_typing -> Cooking -newpath 331 127 moveto -352 147 387 179 410 202 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 408 205 moveto -418 209 lineto -413 200 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 408 205 moveto -418 209 lineto -413 200 lineto -closepath -stroke -end grestore - -% Indtypes -gsave 10 dict begin -436 110 37 18 ellipse_path -stroke -gsave 10 dict begin -411 105 moveto -(Indtypes) -[4.56 6.96 6.96 3.84 6.96 6.96 6.24 5.52] -xshow -end grestore -end grestore - -% Term_typing -> Indtypes -newpath 362 110 moveto -370 110 379 110 388 110 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 388 114 moveto -398 110 lineto -388 107 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 388 114 moveto -398 110 lineto -388 107 lineto -closepath -stroke -end grestore - -% Environ -gsave 10 dict begin -1174 181 36 18 ellipse_path -stroke -gsave 10 dict begin -1151 176 moveto -(Environ) -[8.4 6.48 6.96 3.84 4.56 6.96 6.96] -xshow -end grestore -end grestore - -% Cbytegen -> Environ -newpath 841 166 moveto -911 169 1054 175 1128 179 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1128 183 moveto -1138 179 lineto -1128 176 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1128 183 moveto -1138 179 lineto -1128 176 lineto -closepath -stroke -end grestore - -% Cooking -> Reduction -newpath 473 227 moveto -485 228 498 229 510 229 curveto -603 231 626 233 718 229 curveto -773 226 834 220 876 214 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 876 217 moveto -886 213 lineto -876 211 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 876 217 moveto -886 213 lineto -876 211 lineto -closepath -stroke -end grestore - -% Indtypes -> Typeops -newpath 474 110 moveto -484 110 495 110 505 110 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 505 114 moveto -515 110 lineto -505 107 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 505 114 moveto -515 110 lineto -505 107 lineto -closepath -stroke -end grestore - -% Term -gsave 10 dict begin -1666 173 28 18 ellipse_path -stroke -gsave 10 dict begin -1651 168 moveto -(Term) -[7.2 6.24 4.8 10.8] -xshow -end grestore -end grestore - -% Term -> Univ -newpath 1685 186 moveto -1699 196 1719 211 1736 222 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1734 225 moveto -1744 228 lineto -1738 219 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1734 225 moveto -1744 228 lineto -1738 219 lineto -closepath -stroke -end grestore - -% Esubst -gsave 10 dict begin -1763 173 32 18 ellipse_path -stroke -gsave 10 dict begin -1743 168 moveto -(Esubst) -[8.4 5.52 6.96 6.96 5.28 3.84] -xshow -end grestore -end grestore - -% Term -> Esubst -newpath 1694 173 moveto -1702 173 1711 173 1720 173 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1720 177 moveto -1730 173 lineto -1720 170 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1720 177 moveto -1730 173 lineto -1720 170 lineto -closepath -stroke -end grestore - -% Subtyping -gsave 10 dict begin -552 56 42 18 ellipse_path -stroke -gsave 10 dict begin -523 51 moveto -(Subtyping) -[7.68 6.96 6.96 3.84 6.96 6.96 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Subtyping -> Inductive -newpath 581 69 moveto -597 77 618 86 636 93 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 634 96 moveto -645 97 lineto -637 90 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 634 96 moveto -645 97 lineto -637 90 lineto -closepath -stroke -end grestore - -% Modops -gsave 10 dict begin -674 18 36 18 ellipse_path -stroke -gsave 10 dict begin -650 13 moveto -(Modops) -[12.48 6.96 6.96 6.96 6.96 5.52] -xshow -end grestore -end grestore - -% Subtyping -> Modops -newpath 586 45 moveto -601 41 618 35 633 31 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 634 34 moveto -643 28 lineto -632 28 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 634 34 moveto -643 28 lineto -632 28 lineto -closepath -stroke -end grestore - -% Modops -> Entries -newpath 705 27 moveto -722 32 743 39 761 44 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 760 47 moveto -771 47 lineto -762 41 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 760 47 moveto -771 47 lineto -762 41 lineto -closepath -stroke -end grestore - -% Modops -> Cbytegen -newpath 686 35 moveto -695 48 707 67 718 83 curveto -735 107 733 118 754 137 curveto -757 140 761 143 765 145 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 763 148 moveto -773 151 lineto -767 142 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 763 148 moveto -773 151 lineto -767 142 lineto -closepath -stroke -end grestore - -% Sign -> Term -newpath 1454 99 moveto -1489 98 1553 100 1602 119 curveto -1626 129 1637 135 1649 148 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1647 151 moveto -1656 156 lineto -1652 146 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1647 151 moveto -1656 156 lineto -1652 146 lineto -closepath -stroke -end grestore - -% Safe_typing -gsave 10 dict begin -47 85 46 18 ellipse_path -stroke -gsave 10 dict begin -13 80 moveto -(Safe_typing) -[7.68 6.24 4.08 6.24 6.96 3.84 6.96 6.96 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Mod_typing -gsave 10 dict begin -179 85 48 18 ellipse_path -stroke -gsave 10 dict begin -143 80 moveto -(Mod_typing) -[12.48 6.96 6.96 6.96 3.84 6.96 6.96 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Safe_typing -> Mod_typing -newpath 94 85 moveto -103 85 111 85 120 85 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 120 89 moveto -130 85 lineto -120 82 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 120 89 moveto -130 85 lineto -120 82 lineto -closepath -stroke -end grestore - -% Mod_typing -> Term_typing -newpath 223 93 moveto -235 95 248 98 260 100 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 260 103 moveto -270 102 lineto -261 97 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 260 103 moveto -270 102 lineto -261 97 lineto -closepath -stroke -end grestore - -% Mod_typing -> Subtyping -newpath 227 81 moveto -297 75 428 65 500 60 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 500 63 moveto -510 59 lineto -500 57 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 500 63 moveto -510 59 lineto -500 57 lineto -closepath -stroke -end grestore - -% Closure -> Environ -newpath 1085 201 moveto -1099 198 1116 194 1131 190 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1132 193 moveto -1141 188 lineto -1131 187 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1132 193 moveto -1141 188 lineto -1131 187 lineto -closepath -stroke -end grestore - -% Mod_subst -> Term -newpath 1594 155 moveto -1606 158 1618 161 1630 164 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1630 167 moveto -1640 166 lineto -1631 161 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1630 167 moveto -1640 166 lineto -1631 161 lineto -closepath -stroke -end grestore - -% Declarations -gsave 10 dict begin -1295 181 49 18 ellipse_path -stroke -gsave 10 dict begin -1259 176 moveto -(Declarations) -[10.08 6.24 6.24 3.84 6.24 4.56 6.24 3.84 3.84 6.96 6.96 5.52] -xshow -end grestore -end grestore - -% Environ -> Declarations -newpath 1210 181 moveto -1218 181 1227 181 1236 181 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1236 185 moveto -1246 181 lineto -1236 178 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1236 185 moveto -1246 181 lineto -1236 178 lineto -closepath -stroke -end grestore - -% Declarations -> Cemitcodes -newpath 1341 188 moveto -1351 189 1363 191 1373 192 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1373 195 moveto -1383 194 lineto -1374 189 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1373 195 moveto -1383 194 lineto -1374 189 lineto -closepath -stroke -end grestore - -% Declarations -> Sign -newpath 1320 165 moveto -1343 152 1375 132 1398 118 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1401 120 moveto -1407 112 lineto -1397 115 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1401 120 moveto -1407 112 lineto -1397 115 lineto -closepath +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 -end grestore - -% Cbytecodes -> Term -newpath 1595 190 moveto -1607 188 1619 185 1630 182 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1631 185 moveto -1640 179 lineto -1629 179 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1631 185 moveto -1640 179 lineto -1629 179 lineto -closepath +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 -end grestore +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 @@ -1449,6 +1425,7 @@ grestore %%EndPage: 1 %%Trailer %%Pages: 1 +%%BoundingBox: 36 36 535 756 end restore %%EOF diff --git a/dev/ocamlweb-doc/library.dep.ps b/dev/ocamlweb-doc/library.dep.ps index 1c68240e..c9bb351e 100644 --- a/dev/ocamlweb-doc/library.dep.ps +++ b/dev/ocamlweb-doc/library.dep.ps @@ -1,9 +1,9 @@ %!PS-Adobe-2.0 -%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) -%%For: (herbelin) Hugo Herbelin +%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007) +%%For: (notin) Jean-Marc Notin,,, %%Title: G %%Pages: (atend) -%%BoundingBox: 35 35 577 207 +%%BoundingBox: (atend) %%EndComments save %%BeginProlog @@ -16,57 +16,7 @@ mark 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 +EncodingVector 45 /hyphen put % Set up ISO Latin 1 character encoding /starnetISO { @@ -98,8 +48,8 @@ cleartomark /InvScaleFactor 1.0 def /set_scale { - dup 1 exch div /InvScaleFactor exch def - dup scale + dup 1 exch div /InvScaleFactor exch def + scale } bind def % styles @@ -229,601 +179,587 @@ def } if %%EndSetup +setupLatin1 %%Page: 1 1 -%%PageBoundingBox: 36 36 577 207 -%%PageOrientation: Portrait +%%PageBoundingBox: 36 36 576 752 +%%PageOrientation: Landscape gsave -35 35 542 172 boxprim clip newpath -36 36 translate +36 36 576 752 boxprim clip newpath 0 0 1 beginpage -0.6750 set_scale -0 0 translate 0 rotate -0.000 0.000 0.000 graphcolor +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 - -% States -gsave 10 dict begin -30 18 30 18 ellipse_path -stroke -gsave 10 dict begin -13 13 moveto -(States) -[7.44 4.08 6.24 3.84 6.24 5.52] -xshow -end grestore -end grestore - -% Library -gsave 10 dict begin -132 18 34 18 ellipse_path -stroke -gsave 10 dict begin -110 13 moveto -(Library) -[8.4 3.84 6.96 4.56 6.24 4.8 6.96] -xshow -end grestore -end grestore - -% States -> Library -newpath 60 18 moveto -69 18 78 18 87 18 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 87 22 moveto -97 18 lineto -87 15 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 87 22 moveto -97 18 lineto -87 15 lineto -closepath -stroke -end grestore - -% Declaremods -gsave 10 dict begin -274 18 50 18 ellipse_path -stroke -gsave 10 dict begin -236 13 moveto -(Declaremods) -[10.08 6.24 6.24 3.84 6.24 4.56 6.24 10.8 6.96 6.96 5.52] -xshow -end grestore -end grestore - -% Library -> Declaremods -newpath 167 18 moveto -181 18 197 18 213 18 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 213 22 moveto -223 18 lineto -213 15 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 213 22 moveto -223 18 lineto -213 15 lineto -closepath -stroke -end grestore - -% Nametab -gsave 10 dict begin -523 134 39 18 ellipse_path -stroke -gsave 10 dict begin -497 129 moveto -(Nametab) -[9.6 6.24 10.8 6 4.08 6.24 6.96] -xshow -end grestore -end grestore - -% Libnames -gsave 10 dict begin -642 134 41 18 ellipse_path -stroke -gsave 10 dict begin -613 129 moveto -(Libnames) -[8.4 3.84 6.96 6.96 6.24 10.8 6.24 5.52] -xshow -end grestore -end grestore - -% Nametab -> Libnames -newpath 562 134 moveto -571 134 580 134 590 134 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 590 138 moveto -600 134 lineto -590 131 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 590 138 moveto -600 134 lineto -590 131 lineto -closepath -stroke -end grestore - -% Summary -gsave 10 dict begin -642 65 40 18 ellipse_path -stroke -gsave 10 dict begin -614 60 moveto -(Summary) -[7.68 6.96 10.8 10.8 6.24 4.8 6.96] -xshow -end grestore -end grestore - -% Nametab -> Summary -newpath 547 120 moveto -565 110 589 96 608 84 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 610 87 moveto -617 79 lineto -607 81 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 610 87 moveto -617 79 lineto -607 81 lineto -closepath -stroke -end grestore - -% Nameops -gsave 10 dict begin -760 134 40 18 ellipse_path -stroke -gsave 10 dict begin -733 129 moveto -(Nameops) -[9.6 6.24 10.8 6.24 6.96 6.96 5.52] -xshow -end grestore -end grestore - -% Libnames -> Nameops -newpath 684 134 moveto -693 134 701 134 710 134 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 710 138 moveto -720 134 lineto -710 131 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 710 138 moveto -720 134 lineto -710 131 lineto -closepath -stroke -end grestore - -% Lib -gsave 10 dict begin -413 153 27 18 ellipse_path -stroke -gsave 10 dict begin -402 148 moveto -(Lib) -[8.4 3.84 6.96] -xshow -end grestore -end grestore - -% Declaremods -> Lib -newpath 315 29 moveto -325 33 336 38 344 45 curveto -359 58 383 99 399 127 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 396 129 moveto -404 136 lineto -402 126 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 396 129 moveto -404 136 lineto -402 126 lineto -closepath -stroke -end grestore - -% Global -gsave 10 dict begin -413 65 32 18 ellipse_path -stroke -gsave 10 dict begin -393 60 moveto -(Global) -[10.08 3.84 6.96 6.96 6.24 3.84] -xshow -end grestore -end grestore - -% Declaremods -> Global -newpath 311 30 moveto -331 37 355 45 375 52 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 374 55 moveto -385 55 lineto -376 49 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 374 55 moveto -385 55 lineto -376 49 lineto -closepath -stroke -end grestore - -% Libobject -gsave 10 dict begin -523 188 40 18 ellipse_path -stroke -gsave 10 dict begin -495 183 moveto -(Libobject) -[8.4 3.84 6.96 6.96 6.96 3.84 6.24 6.24 3.84] -xshow -end grestore -end grestore - -% Libobject -> Libnames -newpath 552 175 moveto -567 168 587 159 604 151 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 605 154 moveto -613 147 lineto -602 148 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 605 154 moveto -613 147 lineto -602 148 lineto -closepath -stroke -end grestore - -% Lib -> Nametab -newpath 439 148 moveto -450 146 464 144 476 142 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 477 145 moveto -486 140 lineto -476 139 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 477 145 moveto -486 140 lineto -476 139 lineto -closepath -stroke -end grestore - -% Lib -> Libobject -newpath 437 161 moveto -450 165 466 170 480 174 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 479 177 moveto -490 177 lineto -481 171 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 479 177 moveto -490 177 lineto -481 171 lineto -closepath -stroke -end grestore - -% Impargs -gsave 10 dict begin -274 126 36 18 ellipse_path -stroke -gsave 10 dict begin -251 121 moveto -(Impargs) -[4.56 10.56 6.96 6.24 4.32 6.96 5.52] -xshow -end grestore -end grestore - -% Impargs -> Lib -newpath 308 133 moveto -329 137 355 142 377 146 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 377 149 moveto -387 148 lineto -378 143 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 377 149 moveto -387 148 lineto -378 143 lineto -closepath -stroke -end grestore - -% Impargs -> Global -newpath 304 116 moveto -316 111 331 105 344 99 curveto -357 94 369 88 381 82 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 382 85 moveto -390 78 lineto -379 79 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 382 85 moveto -390 78 lineto -379 79 lineto -closepath -stroke -end grestore - -% Global -> Libnames -newpath 443 73 moveto -473 81 522 94 564 107 curveto -576 111 589 115 600 119 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 599 122 moveto -610 122 lineto -601 116 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 599 122 moveto -610 122 lineto -601 116 lineto -closepath -stroke -end grestore - -% Global -> Summary -newpath 446 65 moveto -484 65 547 65 591 65 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 591 69 moveto -601 65 lineto -591 62 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 591 69 moveto -601 65 lineto -591 62 lineto -closepath -stroke -end grestore - -% Goptions -gsave 10 dict begin -274 180 39 18 ellipse_path -stroke -gsave 10 dict begin -248 175 moveto -(Goptions) -[10.08 6.96 6.96 3.84 3.84 6.96 6.96 5.52] -xshow -end grestore -end grestore - -% Goptions -> Lib -newpath 310 173 moveto -331 169 356 164 377 160 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 378 163 moveto -387 158 lineto -377 157 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 378 163 moveto -387 158 lineto -377 157 lineto -closepath -stroke -end grestore - -% Dischargedhypsmap -gsave 10 dict begin -274 234 70 18 ellipse_path -stroke -gsave 10 dict begin -217 229 moveto -(Dischargedhypsmap) -[10.08 3.84 5.52 6 6.96 6.24 4.32 6.72 6.24 6.96 6.48 6.96 6.96 5.52 10.8 6.24 6.96] -xshow -end grestore -end grestore - -% Dischargedhypsmap -> Lib -newpath 317 220 moveto -326 216 336 212 344 207 curveto -360 197 376 185 389 175 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 392 177 moveto -397 168 lineto -387 172 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 392 177 moveto -397 168 lineto -387 172 lineto -closepath -stroke -end grestore - -% Declare -gsave 10 dict begin -132 126 35 18 ellipse_path -stroke -gsave 10 dict begin -109 121 moveto -(Declare) -[10.08 6.24 6.24 3.84 6.24 4.56 6.24] -xshow -end grestore -end grestore - -% Declare -> Impargs -newpath 168 126 moveto -186 126 208 126 228 126 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 228 130 moveto -238 126 lineto -228 123 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 228 130 moveto -238 126 lineto -228 123 lineto -closepath -stroke -end grestore - -% Declare -> Dischargedhypsmap -newpath 144 143 moveto -157 161 179 189 204 207 curveto -209 210 215 213 221 216 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 219 219 moveto -230 220 lineto -222 213 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 219 219 moveto -230 220 lineto -222 213 lineto -closepath -stroke -end grestore - -% Decl_kinds -gsave 10 dict begin -274 72 45 18 ellipse_path -stroke -gsave 10 dict begin -241 67 moveto -(Decl_kinds) -[10.08 6.24 6.24 3.84 6.96 6.96 3.84 6.96 6.96 5.52] -xshow -end grestore -end grestore - -% Declare -> Decl_kinds -newpath 161 115 moveto -181 107 209 97 232 88 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 233 91 moveto -241 84 lineto -230 85 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 233 91 moveto -241 84 lineto -230 85 lineto -closepath -stroke -end grestore +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 @@ -831,6 +767,7 @@ grestore %%EndPage: 1 %%Trailer %%Pages: 1 +%%BoundingBox: 36 36 576 752 end restore %%EOF diff --git a/dev/ocamlweb-doc/proofs.dep.ps b/dev/ocamlweb-doc/proofs.dep.ps index 0e78f422..4dd045ce 100644 --- a/dev/ocamlweb-doc/proofs.dep.ps +++ b/dev/ocamlweb-doc/proofs.dep.ps @@ -1,9 +1,9 @@ %!PS-Adobe-2.0 -%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) -%%For: (herbelin) Hugo Herbelin +%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007) +%%For: (notin) Jean-Marc Notin,,, %%Title: G %%Pages: (atend) -%%BoundingBox: 35 35 577 136 +%%BoundingBox: (atend) %%EndComments save %%BeginProlog @@ -16,57 +16,7 @@ mark 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 +EncodingVector 45 /hyphen put % Set up ISO Latin 1 character encoding /starnetISO { @@ -98,8 +48,8 @@ cleartomark /InvScaleFactor 1.0 def /set_scale { - dup 1 exch div /InvScaleFactor exch def - dup scale + dup 1 exch div /InvScaleFactor exch def + scale } bind def % styles @@ -229,403 +179,463 @@ def } if %%EndSetup +setupLatin1 %%Page: 1 1 -%%PageBoundingBox: 36 36 577 136 -%%PageOrientation: Portrait +%%PageBoundingBox: 36 36 576 753 +%%PageOrientation: Landscape gsave -35 35 542 101 boxprim clip newpath -36 36 translate +36 36 576 753 boxprim clip newpath 0 0 1 beginpage -0.6923 set_scale -0 0 translate 0 rotate -0.000 0.000 0.000 graphcolor +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 - -% Tactic_debug -gsave 10 dict begin -163 72 51 18 ellipse_path -stroke -gsave 10 dict begin -125 67 moveto -(Tactic_debug) -[7.44 6.24 6.24 3.84 3.84 6.24 6.96 6.96 6.24 6.96 6.96 6.96] -xshow -end grestore -end grestore - -% Refiner -gsave 10 dict begin -287 72 34 18 ellipse_path -stroke -gsave 10 dict begin -266 67 moveto -(Refiner) -[9.12 6.24 4.8 3.84 6.96 6.24 4.56] -xshow -end grestore -end grestore - -% Tactic_debug -> Refiner -newpath 214 72 moveto -223 72 233 72 243 72 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 243 76 moveto -253 72 lineto -243 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 243 76 moveto -253 72 lineto -243 69 lineto -closepath -stroke -end grestore - -% Logic -gsave 10 dict begin -390 72 30 18 ellipse_path -stroke -gsave 10 dict begin -373 67 moveto -(Logic) -[8.4 6.96 6.96 3.84 6.24] -xshow -end grestore -end grestore - -% Refiner -> Logic -newpath 321 72 moveto -330 72 340 72 350 72 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 350 76 moveto -360 72 lineto -350 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 350 76 moveto -360 72 lineto -350 69 lineto -closepath -stroke -end grestore - -% Tacmach -gsave 10 dict begin -163 126 38 18 ellipse_path -stroke -gsave 10 dict begin -137 121 moveto -(Tacmach) -[7.44 6.24 6.24 10.8 6.24 6 6.96] -xshow -end grestore -end grestore - -% Tacmach -> Refiner -newpath 191 114 moveto -209 106 232 96 251 88 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 253 91 moveto -261 84 lineto -250 84 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 253 91 moveto -261 84 lineto -250 84 lineto -closepath -stroke -end grestore - -% Redexpr -gsave 10 dict begin -287 126 36 18 ellipse_path -stroke -gsave 10 dict begin -263 121 moveto -(Redexpr) -[9.12 6.24 6.96 5.76 6.96 6.96 4.56] -xshow -end grestore -end grestore - -% Tacmach -> Redexpr -newpath 202 126 moveto -214 126 227 126 240 126 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 240 130 moveto -250 126 lineto -240 123 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 240 130 moveto -250 126 lineto -240 123 lineto -closepath -stroke -end grestore - -% Proof_trees -gsave 10 dict begin -502 72 45 18 ellipse_path -stroke -gsave 10 dict begin -469 67 moveto -(Proof_trees) -[7.68 4.56 6.96 6.96 4.56 6.96 3.84 4.56 6.24 6.24 5.52] -xshow -end grestore -end grestore - -% Logic -> Proof_trees -newpath 420 72 moveto -428 72 437 72 446 72 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 446 76 moveto -456 72 lineto -446 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 446 76 moveto -456 72 lineto -446 69 lineto -closepath -stroke -end grestore - -% Proof_type -gsave 10 dict begin -628 72 44 18 ellipse_path -stroke -gsave 10 dict begin -597 67 moveto -(Proof_type) -[7.68 4.56 6.96 6.96 4.56 6.96 3.84 6.96 6.96 6.24] -xshow -end grestore -end grestore - -% Tacexpr -gsave 10 dict begin -744 72 35 18 ellipse_path -stroke -gsave 10 dict begin -721 67 moveto -(Tacexpr) -[7.44 6.24 6.24 5.76 6.96 6.96 4.56] -xshow -end grestore -end grestore - -% Proof_type -> Tacexpr -newpath 672 72 moveto -680 72 689 72 698 72 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 698 76 moveto -708 72 lineto -698 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 698 76 moveto -708 72 lineto -698 69 lineto -closepath -stroke -end grestore - -% Proof_trees -> Proof_type -newpath 548 72 moveto -557 72 565 72 574 72 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 574 76 moveto -584 72 lineto -574 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 574 76 moveto -584 72 lineto -574 69 lineto -closepath -stroke -end grestore - -% Pfedit -gsave 10 dict begin -38 112 29 18 ellipse_path -stroke -gsave 10 dict begin -21 107 moveto -(Pfedit) -[7.68 4.08 6.24 6.96 3.84 3.84] -xshow -end grestore -end grestore - -% Pfedit -> Tacmach -newpath 67 115 moveto -81 117 99 118 115 120 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 115 123 moveto -125 122 lineto -116 117 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 115 123 moveto -125 122 lineto -116 117 lineto -closepath -stroke -end grestore - -% Evar_refiner -gsave 10 dict begin -163 18 49 18 ellipse_path -stroke -gsave 10 dict begin -127 13 moveto -(Evar_refiner) -[8.4 6.72 6.24 4.56 6.96 4.56 6.24 4.8 3.84 6.96 6.24 4.56] -xshow -end grestore -end grestore - -% Pfedit -> Evar_refiner -newpath 53 96 moveto -67 82 90 60 112 45 curveto -116 42 120 40 124 37 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 126 40 moveto -133 32 lineto -123 34 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 126 40 moveto -133 32 lineto -123 34 lineto -closepath -stroke -end grestore - -% Evar_refiner -> Refiner -newpath 195 32 moveto -212 40 233 49 251 57 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 249 60 moveto -260 61 lineto -252 54 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 249 60 moveto -260 61 lineto -252 54 lineto -closepath -stroke -end grestore - -% Clenvtac -gsave 10 dict begin -38 45 38 18 ellipse_path -stroke -gsave 10 dict begin -13 40 moveto -(Clenvtac) -[9.36 3.84 6.24 6.48 6.96 4.08 6.24 6.24] -xshow -end grestore -end grestore - -% Clenvtac -> Tacmach -newpath 58 61 moveto -73 72 93 87 112 99 curveto -117 102 123 105 128 108 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 127 111 moveto -137 113 lineto -130 105 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 127 111 moveto -137 113 lineto -130 105 lineto -closepath +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 -end grestore - -% Clenvtac -> Evar_refiner -newpath 73 37 moveto -85 35 98 32 110 29 curveto +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 -gsave 10 dict begin +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 -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 111 32 moveto -120 27 lineto -110 26 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 111 32 moveto -120 27 lineto -110 26 lineto -closepath +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 -end grestore +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 @@ -633,6 +643,7 @@ grestore %%EndPage: 1 %%Trailer %%Pages: 1 +%%BoundingBox: 36 36 576 753 end restore %%EOF diff --git a/dev/set_raw_db b/dev/set_raw_db new file mode 100644 index 00000000..5caff7e5 --- /dev/null +++ b/dev/set_raw_db @@ -0,0 +1 @@ +install_printer Top_printers.ppconstrdb diff --git a/dev/top_printers.ml b/dev/top_printers.ml index e1ee29e4..afae141b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -32,6 +32,10 @@ open Genarg let _ = Constrextern.print_evar_arguments := true let _ = set_bool_option_value (SecondaryTable ("Printing","Matching")) false +let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found) + +(* std_ppcmds *) +let pppp x = pp x (* name printers *) let ppid id = pp (pr_id id) @@ -44,20 +48,26 @@ let ppcon con = pp(pr_con con) let ppkn kn = pp(pr_kn kn) let ppsp sp = pp(pr_sp sp) let ppqualid qid = pp(pr_qualid qid) +let ppclindex cl = pp(Classops.pr_cl_index cl) (* term printers *) -let ppconstr x = pp(Termops.print_constr x) +let rawdebug = ref false +let ppconstr x = pp (Termops.print_constr x) +let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x) let ppterm = ppconstr let ppsconstr x = ppconstr (Declarations.force x) let ppconstr_univ x = Constrextern.with_universes ppconstr x let pprawconstr = (fun x -> pp(pr_lrawconstr x)) let pppattern = (fun x -> pp(pr_constr_pattern x)) let pptype = (fun x -> pp(pr_ltype x)) + let ppfconstr c = ppconstr (Closure.term_of_fconstr c) let ppbigint n = pp (Bigint.pr_bigint n);; -let ppidset l = pp (prlist_with_sep spc pr_id (Idset.elements l)) +let prset pr l = str "[" ++ prlist_with_sep spc pr l ++ str "]" +let ppintset l = pp (prset int (Intset.elements l)) +let ppidset l = pp (prset pr_id (Idset.elements l)) let pP s = pp (hov 0 s) @@ -81,7 +91,14 @@ let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t) let ppj j = pp (genppj pr_ljudge j) +let prsubst s = pp (Mod_subst.debug_pr_subst s) + +let pp_idpred s = pp (pr_idpred s) +let pp_cpred s = pp (pr_cpred s) +let pp_transparent_state s = pp (pr_transparent_state s) + (* proof printers *) +let ppmetas metas = pp(pr_metaset metas) let ppevm evd = pp(pr_evar_map evd) let ppevd evd = pp(pr_evar_defs evd) let ppclenv clenv = pp(pr_clenv clenv) @@ -103,6 +120,8 @@ let ppuni u = pp(pr_uni u) let ppuniverses u = pp (str"[" ++ pr_universes u ++ str"]") +let ppconstraints c = pp (pr_constraints c) + let ppenv e = pp (str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e (rel_context e) ++ str "]") @@ -240,8 +259,7 @@ let print_pure_constr csr = print_string "end"; close_box() | Fix ((t,i),(lna,tl,bl)) -> - print_string "Fix" -(* "("; print_int i; print_string ")"; + print_string "Fix("; print_int i; print_string ")"; print_cut(); open_vbox 0; let rec print_fix () = @@ -253,7 +271,7 @@ let print_pure_constr csr = box_display bl.(k); close_box (); print_cut() done - in print_string"{"; print_fix(); print_string"}" *) + in print_string"{"; print_fix(); print_string"}" | CoFix(i,(lna,tl,bl)) -> print_string "CoFix("; print_int i; print_string ")"; print_cut(); @@ -404,3 +422,48 @@ let _ = (Gramext.Snterm (Pcoq.Gram.Entry.obj Constr.constr), ConstrArgType), Some "c")]] + +(* Setting printer of unbound global reference *) +open Names +open Nameops +open Libnames + +let encode_path loc prefix mpdir suffix id = + let dir = match mpdir with + | None -> [] + | Some (mp,dir) -> + (repr_dirpath (dirpath_of_string (string_of_mp mp))@ + repr_dirpath dir) in + Qualid (loc, make_qualid + (make_dirpath (List.rev (id_of_string prefix::dir@suffix))) id) + +let raw_string_of_ref loc = function + | ConstRef cst -> + let (mp,dir,id) = repr_con cst in + encode_path loc "CST" (Some (mp,dir)) [] (id_of_label id) + | IndRef (kn,i) -> + let (mp,dir,id) = repr_kn kn in + encode_path loc "IND" (Some (mp,dir)) [id_of_label id] + (id_of_string ("_"^string_of_int i)) + | ConstructRef ((kn,i),j) -> + let (mp,dir,id) = repr_kn kn in + encode_path loc "CSTR" (Some (mp,dir)) + [id_of_label id;id_of_string ("_"^string_of_int i)] + (id_of_string ("_"^string_of_int j)) + | VarRef id -> + encode_path loc "SECVAR" None [] id + +let short_string_of_ref loc = function + | VarRef id -> Ident (loc,id) + | ConstRef cst -> Ident (loc,id_of_label (pi3 (repr_con cst))) + | IndRef (kn,0) -> Ident (loc,id_of_label (pi3 (repr_kn kn))) + | IndRef (kn,i) -> + encode_path loc "IND" None [id_of_label (pi3 (repr_kn kn))] + (id_of_string ("_"^string_of_int i)) + | ConstructRef ((kn,i),j) -> + encode_path loc "CSTR" None + [id_of_label (pi3 (repr_kn kn));id_of_string ("_"^string_of_int i)] + (id_of_string ("_"^string_of_int j)) + +let _ = Constrextern.set_debug_global_reference_printer + (if !rawdebug then raw_string_of_ref else short_string_of_ref) diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index 97973df2..de68ce1e 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -748,7 +748,7 @@ Conflicts exists between integers and constrs. \nlsep \TERM{cc} %% contrib/field \nlsep \TERM{field}~\STAR{\tacconstr} -%% contrib/first-order +%% contrib/firstorder \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}} \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{with}~\PLUS{\NT{reference}} \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{using}~\PLUS{\NT{ident}} -- cgit v1.2.3