diff options
Diffstat (limited to 'dev')
37 files changed, 1278 insertions, 8523 deletions
diff --git a/dev/Makefile.oug b/dev/Makefile.oug new file mode 100644 index 00000000..ee69ea80 --- /dev/null +++ b/dev/Makefile.oug @@ -0,0 +1,74 @@ +####################################################################### +# v # The Coq Proof Assistant / The Coq Development Team # +# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # +# \VV/ ############################################################# +# // # This file is distributed under the terms of the # +# # GNU Lesser General Public License Version 2.1 # +####################################################################### + + +#### Source Code Analysis via Oug #### +#### Cf http://home.gna.org/oug #### + + +# To be used from top dir : make -f dev/Makefile.oug ... + +include Makefile.build + +# Oug location: in the path by default, native version + +OUG:=oug.x + +# NB: coq should have been compiled with the same ocaml version as oug + +# NOTA: it seems we obtain more useless elements reported when _not_ +# providing the .mli files, and also when giving a precise start point. +# TO BE INVESTIGATED + +ml_of_cma = $(patsubst %.cmo,%.ml,$(filter %.cmo,$(shell cat $(1:.cma=.mllib.d)))) +local_ml_of_cma = $(filter $(dir $(1))%,$(call ml_of_cma,$(1))) +mli_of_ml = $(foreach ml,$(1),$(wildcard $(ml)i)) + +# Analysis of coqtop, without plugins + +COREML:=config/coq_config.ml $(call ml_of_cma, $(CORECMA)) +COREMLI:=$(call mli_of_ml,$(COREML)) + +core.oug: + $(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(COREML) + +core.useless: core.oug + $(OUG) --load-data $< --no-reduce --print-loc --roots "<Coqtop.start>" --useless-elements $@ + +core_intf.oug: + $(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(COREML) $(COREMLI) + +core_intf.useless: core_intf.oug + $(OUG) --load-data $< --no-reduce --print-loc --roots "<Coqtop.start>" --useless-elements $@ + +# Analysis of coqchk, considering only files in the checker/ subdir + +CHECKERML:=$(call local_ml_of_cma,checker/check.cma) +CHECKERMLI:=$(call mli_of_ml,$(CHECKERML)) + +## BUG: in oug, include dirs have reversed priority compared with ocaml, cannot use CHKLIBS +MYCHKINCL:=$(MLINCLUDES) -I checker + +checker.oug: + $(OUG) --dump-data $@ -rectypes $(MYCHKINCL) $(CHECKERML) #$(CHECKERMLI) + +checker.useless: checker.oug + $(OUG) --load-data $< --no-reduce --print-loc --roots "<Checker.start>" --useless-elements $@ + +# Analysis of extraction + +EXTRACTIONML:=$(call local_ml_of_cma,$(EXTRACTIONCMA)) +EXTRACTIONMLI:=$(call mli_of_ml,$(EXTRACTIONMLI)) + +extraction.oug: + $(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(EXTRACTIONML) #$(EXTRACTIONMLI) + +extraction.useless: extraction.oug + $(OUG) --load-data $< --no-reduce --print-loc --useless-elements $@ + +# More to come ...
\ No newline at end of file @@ -32,16 +32,14 @@ perf-analysis: analysis of perfs measured on the compilation of user contribs cic.dtd: official dtd of the calc. of ind. constr. for im/ex-portation -Documentation of ML interfaces using tex (directory ocamlweb-doc) +Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) ---------------------------------------- - -go in directory and call "make" +"make mli-doc" in coq root directory. Other development tools (directory tools) ----------------------- -univdot: produces a graph of CIC universes Makefile.dir: makefile dedicated to intensive work in a given directory Makefile.subdir: makefile dedicated to intensive work in a given subdirectory Makefile.devel: utilities to automatically launch coq in various states diff --git a/dev/base_include b/dev/base_include index 05e87da1..d1125965 100644 --- a/dev/base_include +++ b/dev/base_include @@ -24,7 +24,6 @@ #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;; #install_printer (* dir_path *) ppdir;; #install_printer (* module_path *) ppmp;; @@ -38,7 +37,6 @@ #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;; @@ -78,7 +76,8 @@ open Pretyping.Default.Cases open Cbv open Classops open Clenv -open Rawterm +open Clenvtac +open Glob_term open Coercion open Coercion.Default open Recordops @@ -110,11 +109,9 @@ open Topconstr open Prettyp open Search -open Clenvtac open Evar_refiner open Logic open Pfedit -open Proof_trees open Proof_type open Redexpr open Refiner @@ -172,7 +169,7 @@ let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; let parse_tac = Pcoq.parse_string Pcoq.Tactic.tactic;; let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; -(* build a term of type rawconstr without type-checking or resolution of +(* build a term of type glob_constr without type-checking or resolution of implicit syntax *) let e s = @@ -190,18 +187,22 @@ open Declarations;; let constbody_of_string s = let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_string s)) in - Option.get b.const_body;; + Option.get (body_of_constant b);; (* Get the current goal *) - +(* let getgoal x = top_goal_of_pftreestate (Pfedit.get_pftreestate x);; let get_nth_goal n = nth_goal_of_pftreestate n (Pfedit.get_pftreestate ());; let current_goal () = get_nth_goal 1;; - +*) let pf_e gl s = Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s);; open Toplevel let go = loop +let _ = + print_string + ("\n\tOcaml toplevel with Coq printers and utilities (use go();; to exit)\n\n"); + flush_all() @@ -6,7 +6,6 @@ install_printer Top_printers.ppidset install_printer Top_printers.ppevarsubst install_printer Top_printers.ppintset install_printer Top_printers.pplab -install_printer Top_printers.ppmbid install_printer Top_printers.ppdir install_printer Top_printers.ppmp install_printer Top_printers.ppkn @@ -18,7 +17,7 @@ install_printer Top_printers.ppclindex install_printer Top_printers.ppbigint install_printer Top_printers.pppattern -install_printer Top_printers.pprawconstr +install_printer Top_printers.ppglob_constr install_printer Top_printers.ppconstr install_printer Top_printers.ppuni @@ -28,16 +27,13 @@ install_printer Top_printers.pptype install_printer Top_printers.ppj 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.ppevm -install_printer Top_printers.ppclenv +install_printer Top_printers.ppgoal install_printer Top_printers.pptac install_printer Top_printers.ppobj install_printer Top_printers.pploc install_printer Top_printers.prsubst install_printer Top_printers.prdelta -install_printer Top_printers.ppconstr +install_printer Top_printers.ppfconstr diff --git a/dev/db_printers.ml b/dev/db_printers.ml index 883103c3..b3edd7d0 100644 --- a/dev/db_printers.ml +++ b/dev/db_printers.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/dev/doc/about-hints b/dev/doc/about-hints new file mode 100644 index 00000000..95712c3c --- /dev/null +++ b/dev/doc/about-hints @@ -0,0 +1,454 @@ +An investigation of how ZArith lemmas could be classified in different +automation classes + +- Reversible lemmas relating operators (to be declared as hints but + needing precedences) +- Equivalent notions (one has to be considered as primitive and the + other rewritten into the canonical one) +- Isomorphisms between structure (one structure has to be considered + as more primitive than the other for a give operator) +- Irreversible simplifications (to be declared with precedences) +- Reversible bottom-up simplifications (to be used in hypotheses) +- Irreversible bottom-up simplifications (to be used in hypotheses + with precedences) +- Rewriting rules (relevant for autorewrite, or for an improved auto) + +Note: this analysis, made in 2001, was previously stored in +theories/ZArith/Zhints.v. It has been moved here to avoid obfuscating +the standard library. + +(**********************************************************************) +(** * Reversible lemmas relating operators *) +(** Probably to be declared as hints but need to define precedences *) + +(** ** Conversion between comparisons/predicates and arithmetic operators *) + +(** Lemmas ending by eq *) +(** +<< +Zegal_left: (x,y:Z)`x = y`->`x+(-y) = 0` +Zabs_eq: (x:Z)`0 <= x`->`|x| = x` +Zeven_div2: (x:Z)(Zeven x)->`x = 2*(Zdiv2 x)` +Zodd_div2: (x:Z)`x >= 0`->(Zodd x)->`x = 2*(Zdiv2 x)+1` +>> +*) + +(** Lemmas ending by Zgt *) +(** +<< +Zgt_left_rev: (x,y:Z)`x+(-y) > 0`->`x > y` +Zgt_left_gt: (x,y:Z)`x > y`->`x+(-y) > 0` +>> +*) + +(** Lemmas ending by Zlt *) +(** +<< +Zlt_left_rev: (x,y:Z)`0 < y+(-x)`->`x < y` +Zlt_left_lt: (x,y:Z)`x < y`->`0 < y+(-x)` +Zlt_O_minus_lt: (n,m:Z)`0 < n-m`->`m < n` +>> +*) + +(** Lemmas ending by Zle *) +(** +<< +Zle_left: (x,y:Z)`x <= y`->`0 <= y+(-x)` +Zle_left_rev: (x,y:Z)`0 <= y+(-x)`->`x <= y` +Zlt_left: (x,y:Z)`x < y`->`0 <= y+(-1)+(-x)` +Zge_left: (x,y:Z)`x >= y`->`0 <= x+(-y)` +Zgt_left: (x,y:Z)`x > y`->`0 <= x+(-1)+(-y)` +>> +*) + +(** ** Conversion between nat comparisons and Z comparisons *) + +(** Lemmas ending by eq *) +(** +<< +inj_eq: (x,y:nat)x=y->`(inject_nat x) = (inject_nat y)` +>> +*) + +(** Lemmas ending by Zge *) +(** +<< +inj_ge: (x,y:nat)(ge x y)->`(inject_nat x) >= (inject_nat y)` +>> +*) + +(** Lemmas ending by Zgt *) +(** +<< +inj_gt: (x,y:nat)(gt x y)->`(inject_nat x) > (inject_nat y)` +>> +*) + +(** Lemmas ending by Zlt *) +(** +<< +inj_lt: (x,y:nat)(lt x y)->`(inject_nat x) < (inject_nat y)` +>> +*) + +(** Lemmas ending by Zle *) +(** +<< +inj_le: (x,y:nat)(le x y)->`(inject_nat x) <= (inject_nat y)` +>> +*) + +(** ** Conversion between comparisons *) + +(** Lemmas ending by Zge *) +(** +<< +not_Zlt: (x,y:Z)~`x < y`->`x >= y` +Zle_ge: (m,n:Z)`m <= n`->`n >= m` +>> +*) + +(** Lemmas ending by Zgt *) +(** +<< +Zle_gt_S: (n,p:Z)`n <= p`->`(Zs p) > n` +not_Zle: (x,y:Z)~`x <= y`->`x > y` +Zlt_gt: (m,n:Z)`m < n`->`n > m` +Zle_S_gt: (n,m:Z)`(Zs n) <= m`->`m > n` +>> +*) + +(** Lemmas ending by Zlt *) +(** +<< +not_Zge: (x,y:Z)~`x >= y`->`x < y` +Zgt_lt: (m,n:Z)`m > n`->`n < m` +Zle_lt_n_Sm: (n,m:Z)`n <= m`->`n < (Zs m)` +>> +*) + +(** Lemmas ending by Zle *) +(** +<< +Zlt_ZERO_pred_le_ZERO: (x:Z)`0 < x`->`0 <= (Zpred x)` +not_Zgt: (x,y:Z)~`x > y`->`x <= y` +Zgt_le_S: (n,p:Z)`p > n`->`(Zs n) <= p` +Zgt_S_le: (n,p:Z)`(Zs p) > n`->`n <= p` +Zge_le: (m,n:Z)`m >= n`->`n <= m` +Zlt_le_S: (n,p:Z)`n < p`->`(Zs n) <= p` +Zlt_n_Sm_le: (n,m:Z)`n < (Zs m)`->`n <= m` +Zlt_le_weak: (n,m:Z)`n < m`->`n <= m` +Zle_refl: (n,m:Z)`n = m`->`n <= m` +>> +*) + +(** ** Irreversible simplification involving several comparaisons *) +(** useful with clear precedences *) + +(** Lemmas ending by Zlt *) +(** +<< +Zlt_le_reg :(a,b,c,d:Z)`a < b`->`c <= d`->`a+c < b+d` +Zle_lt_reg : (a,b,c,d:Z)`a <= b`->`c < d`->`a+c < b+d` +>> +*) + +(** ** What is decreasing here ? *) + +(** Lemmas ending by eq *) +(** +<< +Zplus_minus: (n,m,p:Z)`n = m+p`->`p = n-m` +>> +*) + +(** Lemmas ending by Zgt *) +(** +<< +Zgt_pred: (n,p:Z)`p > (Zs n)`->`(Zpred p) > n` +>> +*) + +(** Lemmas ending by Zlt *) +(** +<< +Zlt_pred: (n,p:Z)`(Zs n) < p`->`n < (Zpred p)` +>> +*) + +(**********************************************************************) +(** * Useful Bottom-up lemmas *) + +(** ** Bottom-up simplification: should be used *) + +(** Lemmas ending by eq *) +(** +<< +Zeq_add_S: (n,m:Z)`(Zs n) = (Zs m)`->`n = m` +Zsimpl_plus_l: (n,m,p:Z)`n+m = n+p`->`m = p` +Zplus_unit_left: (n,m:Z)`n+0 = m`->`n = m` +Zplus_unit_right: (n,m:Z)`n = m+0`->`n = m` +>> +*) + +(** Lemmas ending by Zgt *) +(** +<< +Zsimpl_gt_plus_l: (n,m,p:Z)`p+n > p+m`->`n > m` +Zsimpl_gt_plus_r: (n,m,p:Z)`n+p > m+p`->`n > m` +Zgt_S_n: (n,p:Z)`(Zs p) > (Zs n)`->`p > n` +>> +*) + +(** Lemmas ending by Zlt *) +(** +<< +Zsimpl_lt_plus_l: (n,m,p:Z)`p+n < p+m`->`n < m` +Zsimpl_lt_plus_r: (n,m,p:Z)`n+p < m+p`->`n < m` +Zlt_S_n: (n,m:Z)`(Zs n) < (Zs m)`->`n < m` +>> +*) + +(** Lemmas ending by Zle *) +(** << Zsimpl_le_plus_l: (p,n,m:Z)`p+n <= p+m`->`n <= m` +Zsimpl_le_plus_r: (p,n,m:Z)`n+p <= m+p`->`n <= m` +Zle_S_n: (n,m:Z)`(Zs m) <= (Zs n)`->`m <= n` >> *) + +(** ** Bottom-up irreversible (syntactic) simplification *) + +(** Lemmas ending by Zle *) +(** +<< +Zle_trans_S: (n,m:Z)`(Zs n) <= m`->`n <= m` +>> +*) + +(** ** Other unclearly simplifying lemmas *) + +(** Lemmas ending by Zeq *) +(** +<< +Zmult_eq: (x,y:Z)`x <> 0`->`y*x = 0`->`y = 0` +>> +*) + +(* Lemmas ending by Zgt *) +(** +<< +Zmult_gt: (x,y:Z)`x > 0`->`x*y > 0`->`y > 0` +>> +*) + +(* Lemmas ending by Zlt *) +(** +<< +pZmult_lt: (x,y:Z)`x > 0`->`0 < y*x`->`0 < y` +>> +*) + +(* Lemmas ending by Zle *) +(** +<< +Zmult_le: (x,y:Z)`x > 0`->`0 <= y*x`->`0 <= y` +OMEGA1: (x,y:Z)`x = y`->`0 <= x`->`0 <= y` +>> +*) + + +(**********************************************************************) +(** * Irreversible lemmas with meta-variables *) +(** To be used by EAuto *) + +(* Hints Immediate *) +(** Lemmas ending by eq *) +(** +<< +Zle_antisym: (n,m:Z)`n <= m`->`m <= n`->`n = m` +>> +*) + +(** Lemmas ending by Zge *) +(** +<< +Zge_trans: (n,m,p:Z)`n >= m`->`m >= p`->`n >= p` +>> +*) + +(** Lemmas ending by Zgt *) +(** +<< +Zgt_trans: (n,m,p:Z)`n > m`->`m > p`->`n > p` +Zgt_trans_S: (n,m,p:Z)`(Zs n) > m`->`m > p`->`n > p` +Zle_gt_trans: (n,m,p:Z)`m <= n`->`m > p`->`n > p` +Zgt_le_trans: (n,m,p:Z)`n > m`->`p <= m`->`n > p` +>> +*) + +(** Lemmas ending by Zlt *) +(** +<< +Zlt_trans: (n,m,p:Z)`n < m`->`m < p`->`n < p` +Zlt_le_trans: (n,m,p:Z)`n < m`->`m <= p`->`n < p` +Zle_lt_trans: (n,m,p:Z)`n <= m`->`m < p`->`n < p` +>> +*) + +(** Lemmas ending by Zle *) +(** +<< +Zle_trans: (n,m,p:Z)`n <= m`->`m <= p`->`n <= p` +>> +*) + + +(**********************************************************************) +(** * Unclear or too specific lemmas *) +(** Not to be used ? *) + +(** ** Irreversible and too specific (not enough regular) *) + +(** Lemmas ending by Zle *) +(** +<< +Zle_mult: (x,y:Z)`x > 0`->`0 <= y`->`0 <= y*x` +Zle_mult_approx: (x,y,z:Z)`x > 0`->`z > 0`->`0 <= y`->`0 <= y*x+z` +OMEGA6: (x,y,z:Z)`0 <= x`->`y = 0`->`0 <= x+y*z` +OMEGA7: (x,y,z,t:Z)`z > 0`->`t > 0`->`0 <= x`->`0 <= y`->`0 <= x*z+y*t` +>> +*) + +(** ** Expansion and too specific ? *) + +(** Lemmas ending by Zge *) +(** +<< +Zge_mult_simpl: (a,b,c:Z)`c > 0`->`a*c >= b*c`->`a >= b` +>> +*) + +(** Lemmas ending by Zgt *) +(** +<< +Zgt_mult_simpl: (a,b,c:Z)`c > 0`->`a*c > b*c`->`a > b` +Zgt_square_simpl: (x,y:Z)`x >= 0`->`y >= 0`->`x*x > y*y`->`x > y` +>> +*) + +(** Lemmas ending by Zle *) +(** +<< +Zle_mult_simpl: (a,b,c:Z)`c > 0`->`a*c <= b*c`->`a <= b` +Zmult_le_approx: (x,y,z:Z)`x > 0`->`x > z`->`0 <= y*x+z`->`0 <= y` +>> +*) + +(** ** Reversible but too specific ? *) + +(** Lemmas ending by Zlt *) +(** +<< +Zlt_minus: (n,m:Z)`0 < m`->`n-m < n` +>> +*) + +(**********************************************************************) +(** * Lemmas to be used as rewrite rules *) +(** but can also be used as hints *) + +(** Left-to-right simplification lemmas (a symbol disappears) *) + +(** +<< +Zcompare_n_S: (n,m:Z)(Zcompare (Zs n) (Zs m))=(Zcompare n m) +Zmin_n_n: (n:Z)`(Zmin n n) = n` +Zmult_1_n: (n:Z)`1*n = n` +Zmult_n_1: (n:Z)`n*1 = n` +Zminus_plus: (n,m:Z)`n+m-n = m` +Zle_plus_minus: (n,m:Z)`n+(m-n) = m` +Zopp_Zopp: (x:Z)`(-(-x)) = x` +Zero_left: (x:Z)`0+x = x` +Zero_right: (x:Z)`x+0 = x` +Zplus_inverse_r: (x:Z)`x+(-x) = 0` +Zplus_inverse_l: (x:Z)`(-x)+x = 0` +Zopp_intro: (x,y:Z)`(-x) = (-y)`->`x = y` +Zmult_one: (x:Z)`1*x = x` +Zero_mult_left: (x:Z)`0*x = 0` +Zero_mult_right: (x:Z)`x*0 = 0` +Zmult_Zopp_Zopp: (x,y:Z)`(-x)*(-y) = x*y` +>> +*) + +(** Right-to-left simplification lemmas (a symbol disappears) *) + +(** +<< +Zpred_Sn: (m:Z)`m = (Zpred (Zs m))` +Zs_pred: (n:Z)`n = (Zs (Zpred n))` +Zplus_n_O: (n:Z)`n = n+0` +Zmult_n_O: (n:Z)`0 = n*0` +Zminus_n_O: (n:Z)`n = n-0` +Zminus_n_n: (n:Z)`0 = n-n` +Zred_factor6: (x:Z)`x = x+0` +Zred_factor0: (x:Z)`x = x*1` +>> +*) + +(** Unclear orientation (no symbol disappears) *) + +(** +<< +Zplus_n_Sm: (n,m:Z)`(Zs (n+m)) = n+(Zs m)` +Zmult_n_Sm: (n,m:Z)`n*m+n = n*(Zs m)` +Zmin_SS: (n,m:Z)`(Zs (Zmin n m)) = (Zmin (Zs n) (Zs m))` +Zplus_assoc_l: (n,m,p:Z)`n+(m+p) = n+m+p` +Zplus_assoc_r: (n,m,p:Z)`n+m+p = n+(m+p)` +Zplus_permute: (n,m,p:Z)`n+(m+p) = m+(n+p)` +Zplus_Snm_nSm: (n,m:Z)`(Zs n)+m = n+(Zs m)` +Zminus_plus_simpl: (n,m,p:Z)`n-m = p+n-(p+m)` +Zminus_Sn_m: (n,m:Z)`(Zs (n-m)) = (Zs n)-m` +Zmult_plus_distr_l: (n,m,p:Z)`(n+m)*p = n*p+m*p` +Zmult_minus_distr: (n,m,p:Z)`(n-m)*p = n*p-m*p` +Zmult_assoc_r: (n,m,p:Z)`n*m*p = n*(m*p)` +Zmult_assoc_l: (n,m,p:Z)`n*(m*p) = n*m*p` +Zmult_permute: (n,m,p:Z)`n*(m*p) = m*(n*p)` +Zmult_Sm_n: (n,m:Z)`n*m+m = (Zs n)*m` +Zmult_Zplus_distr: (x,y,z:Z)`x*(y+z) = x*y+x*z` +Zmult_plus_distr: (n,m,p:Z)`(n+m)*p = n*p+m*p` +Zopp_Zplus: (x,y:Z)`(-(x+y)) = (-x)+(-y)` +Zplus_sym: (x,y:Z)`x+y = y+x` +Zplus_assoc: (x,y,z:Z)`x+(y+z) = x+y+z` +Zmult_sym: (x,y:Z)`x*y = y*x` +Zmult_assoc: (x,y,z:Z)`x*(y*z) = x*y*z` +Zopp_Zmult: (x,y:Z)`(-x)*y = (-(x*y))` +Zplus_S_n: (x,y:Z)`(Zs x)+y = (Zs (x+y))` +Zopp_one: (x:Z)`(-x) = x*(-1)` +Zopp_Zmult_r: (x,y:Z)`(-(x*y)) = x*(-y)` +Zmult_Zopp_left: (x,y:Z)`(-x)*y = x*(-y)` +Zopp_Zmult_l: (x,y:Z)`(-(x*y)) = (-x)*y` +Zred_factor1: (x:Z)`x+x = x*2` +Zred_factor2: (x,y:Z)`x+x*y = x*(1+y)` +Zred_factor3: (x,y:Z)`x*y+x = x*(1+y)` +Zred_factor4: (x,y,z:Z)`x*y+x*z = x*(y+z)` +Zminus_Zplus_compatible: (x,y,n:Z)`x+n-(y+n) = x-y` +Zmin_plus: (x,y,n:Z)`(Zmin (x+n) (y+n)) = (Zmin x y)+n` +>> +*) + +(** nat <-> Z *) +(** +<< +inj_S: (y:nat)`(inject_nat (S y)) = (Zs (inject_nat y))` +inj_plus: (x,y:nat)`(inject_nat (plus x y)) = (inject_nat x)+(inject_nat y)` +inj_mult: (x,y:nat)`(inject_nat (mult x y)) = (inject_nat x)*(inject_nat y)` +inj_minus1: + (x,y:nat)(le y x)->`(inject_nat (minus x y)) = (inject_nat x)-(inject_nat y)` +inj_minus2: (x,y:nat)(gt y x)->`(inject_nat (minus x y)) = 0` +>> +*) + +(** Too specific ? *) +(** +<< +Zred_factor5: (x,y:Z)`x*0+y = y` +>> +*) diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index d4014303..3d9cba14 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -1,6 +1,22 @@ + Since July 2007, Coq features a build system overhauled by Pierre Corbineau and Lionel Elie Mamane. +--------------------------------------------------------------------- +WARNING: +In March 2010 this build system has been heavily adapted by Pierre +Letouzey. In particular there no more explicit stage1,2. Stage3 +was removed some time ago when coqdep was splitted into coqdep_boot +and full coqdep. Ideas are still similar to what is describe below, +but: +1) .ml4 are explicitely turned into .ml files, which stay after build +2) we let "make" handle the inclusion of .d without trying to guess + what could be done at what time. Some initial inclusions hence + _fail_, but "make" tries again later and succeed. + +TODO: remove obsolete sections below and better describe the new approach +----------------------------------------------------------------------- + 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 . diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index 9362aeeb..b243ebe2 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -1,12 +1,60 @@ Since July 2007, Coq features a build system overhauled by Pierre Corbineau and Lionel Elie Mamane. +--------------------------------------------------------------------- +WARNING: +In March 2010 this build system has been heavily adapted by Pierre +Letouzey. In particular there no more explicit stage1,2. Stage3 +was removed some time ago when coqdep was splitted into coqdep_boot +and full coqdep. Ideas are still similar to what is describe below, +but: +1) .ml4 are explicitely turned into .ml files, which stay after build +2) we let "make" handle the inclusion of .d without trying to guess + what could be done at what time. Some initial inclusions hence + _fail_, but "make" tries again later and succeed. + +TODO: remove obsolete sections below and better describe the new approach +----------------------------------------------------------------------- + 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. + +FAQ: special features used in this Makefile +------------------------------------------- + +* Order-only dependencies: | + +Dependencies placed after a bar (|) should be built before +the current rule, but having one of them is out-of-date do not +trigger a rebuild of the current rule. +See http://www.gnu.org/software/make/manual/make.htmlPrerequisite-Types + +* Annotation before commands: +/-/@ + +a command starting by - is always successful (errors are ignored) +a command starting by + is runned even if option -n is given to make +a command starting by @ is not echoed before being runned + +* Custom functions + +Definition via "define foo" followed by commands (arg is $(1) etc) +Call via "$(call foo,arg1)" + +* Useful builtin functions + +$(subst ...), $(patsubst ...), $(shell ...), $(foreach ...), $(if ...) + +* Behavior of -include + +If the file given to -include doesn't exist, make tries to build it, +but doesn't care if this build fails. This can be quite surprising, +see in particular the -include in Makefile.stage* + + Stages in build system ---------------------- diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 069f7d42..322530e6 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,4 +1,43 @@ ========================================= += CHANGES BETWEEN COQ V8.3 AND COQ V8.4 = +========================================= + +** Functions in unification.ml have now the evar_map coming just after the env + +** Removal of Tacinterp.constr_of_id ** + +Use instead either global_reference or construct_reference in constrintern.ml. + +** Optimizing calls to Evd functions ** + +Evars are split into defined evars and undefined evars; for +efficiency, when an evar is known to be undefined, it is preferable to +use specific functions about undefined evars since these ones are +generally fewer than the defined ones. + +** Type changes in TACTIC EXTEND rules ** + +Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type +glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first +component is kept, the second one can be obtained via +Tacinterp.eval_tactic. + +** ARGUMENT EXTEND ** + +It is now forbidden to use TYPED simultaneously with {RAW,GLOB}_TYPED +in ARGUMENT EXTEND statements. + +** Renaming of rawconstr to glob_constr ** + +The "rawconstr" type has been renamed to "glob_constr" for +consistency. The "raw" in everything related to former rawconstr has +been changed to "glob". For more details about the rationale and +scripts to migrate code using Coq's internals, see commits 13743, +13744, 13755, 13756, 13757, 13758, 13761 (by glondu, end of December +2010) in Subversion repository. Contribs have been fixed too, and +commit messages there might also be helpful for migrating. + +========================================= = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 = ========================================= diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt index 50b3b45c..2480b8ed 100644 --- a/dev/doc/debugging.txt +++ b/dev/doc/debugging.txt @@ -11,6 +11,12 @@ Debugging from Coq toplevel using Caml trace mechanism 6. Test your Coq command and observe the result of tracing your functions 7. Freely switch from Coq to Ocaml toplevels with 'Drop.' and 'go();;' + You can avoid typing #use "include" (or "base_include") after Drop + by adding the following lines in your $HOME/.ocamlinit : + + if Filename.basename Sys.argv.(0) = "coqtop.byte" + then ignore (Toploop.use_silently Format.std_formatter "include") + Hints: To remove high-level pretty-printing features (coercions, notations, ...), use "Set Printing All". It will affect the #trace printers too. diff --git a/dev/doc/perf-analysis b/dev/doc/perf-analysis index d23bf835..ac54fa6f 100644 --- a/dev/doc/perf-analysis +++ b/dev/doc/perf-analysis @@ -1,13 +1,32 @@ Performance analysis (trunk repository) --------------------------------------- +Jun 7, 2010: delayed re-typing of Ltac instances in matching + (-1% on HighSchoolGeometry, -2% on JordanCurveTheorem) + +Jun 4, 2010: improvement in eauto and type classes inference by removing + systematic preparation of debugging pretty-printing streams (std_ppcmds) + (-7% in ATBR, visible only on V8.3 logs since ATBR is broken in trunk; + -6% in HighSchoolGeometry) + +Apr 19, 2010: small improvement obtained by reducing evar instantiation + from O(n^3) to O(n^2) in the size of the instance (-2% in Compcert, + -2% AreaMethod, -15% in Ssreflect) + +Apr 17, 2010: small improvement obtained by not repeating unification + twice in auto (-2% in Compcert, -2% in Algebra) + +Feb 15, 2010: Global decrease due to unicode inefficiency repaired + +Jan 8, 2010: Global increase due to an inefficiency in unicode treatment + Dec 1, 2009 - Dec 19, 2009: Temporary addition of [forall x, P x] hints to exact (generally not significative but, e.g., +25% on Subst, +8% on ZFC, +5% on AreaMethod) Oct 19, 2009: Change in modules (CoLoR +35%) -Aug 9, 2009: new files added in AreaMethod +Aug 9, 2009: new files added in AreaMethod May 21, 2008: New version of CoRN (needs +84% more time to compile) diff --git a/dev/doc/unification.txt b/dev/doc/unification.txt new file mode 100644 index 00000000..6d05bcf5 --- /dev/null +++ b/dev/doc/unification.txt @@ -0,0 +1,208 @@ +Some notes about the use of unification in Coq +---------------------------------------------- + +There are several applications of unification and pattern-matching + +** Unification of types ** + +- For type inference, inference of implicit arguments + * this basically amounts to solve problems of the form T <= U or T = U + where T and U are types coming from a given typing problem + * this kind of problem has to succeed and all the power of unification is + a priori expected (full beta/delta/iota/zeta/nu/mu, pattern-unification, + pruning, imitation/projection heuristics, ...) + +- For lemma application (apply, auto, ...) + * these are also problems of the form T <= U on types but with T + coming from a lemma and U from the goal + * it is not obvious that we always want unification and not matching + * it is not clear which amounts of delta one wants to use + +** Looking for subterms ** + +- For tactics applying on subterms: induction, destruct, rewrite + +- As part of unification of types in the presence of higher-order + evars (e.g. when applying a lemma of conclusion "?P t") + + +---------------------------------------------------------------------- +Here are examples of features one may want or not when looking for subterms + +A- REWRITING + +1- Full conversion on closed terms + +1a- Full conversion on closed terms in the presence of at least one evars (meta) + +Section A1. +Variable y: nat. +Hypothesis H: forall x, x+2 = 0. +Goal y+(1+1) = 0. +rewrite H. +(* 0 = 0 *) +Abort. + +Goal 2+(1+1) = 0. +rewrite H. +(* 0 = 0 *) +Abort. + +(* This exists since the very beginning of Chet's unification for tactics *) +(* But this fails for setoid rewrite *) + +1b- Full conversion on closed terms without any evars in the lemma + +1b.1- Fails on rewrite (because Unification.w_unify_to_subterm_list replaces + unification by check for a syntactic subterm if terms has no evar/meta) + +Goal 0+1 = 0 -> 0+(1+0) = 0. +intros H; rewrite H. +(* fails *) +Abort. + +1b.2- Works with setoid rewrite + +Require Import Setoid. +Goal 0+1 = 0 -> 0+(1+0) = 0. +intros H; rewrite H at 1. +(* 0 = 0 *) +Abort. + +2- Using known instances in full conversion on closed terms + +Section A2. +Hypothesis H: forall x, x+(2+x) = 0. +Goal 1+(1+2) = 0. +rewrite H. +Abort. +End A2. + +(* This exists since 8.2 (HH) *) + +3- Pattern-unification on Rels + +Section A3a. +Variable F: (nat->nat->nat)->nat. +Goal exists f, F (fun x y => f x y) = 0 -> F (fun x y => plus y x) = 0. +eexists. intro H; rewrite H. +(* 0 = 0 *) +Abort. +End A3a. + +(* Works since pattern unification on Meta applied to Rel was introduced *) +(* in unification.ml (8.1, Sep 2006, HH) *) + +Section A3b. +Variables x y: nat. +Variable H: forall f, f x y = 0. +Goal plus y x = 0. +rewrite H. +(* 0 = 0 *) +Abort. +End A3b. + +(* Works since pattern unification on all Meta was supported *) +(* in unification.ml (8.4, Jun 2011, HH) *) + +4- Unification with open terms + +Section A4. +Hypothesis H: forall x, S x = 0. +Goal S 0 = 0. +rewrite (H _). +(* 0 = 0 *) +Abort. +End A4. + +(* Works since unification on Evar was introduced so as to support rewriting *) +(* with open terms (8.2, MS, r11543, Unification.w_unify_to_subterm_list ) *) + +5- Unification of pre-existing evars + +5a- Basic unification of pre-existing evars + +Section A4. +Variables x y: nat. +Goal exists z, S z = 0 -> S (plus y x) = 0. +eexists. intro H; rewrite H. +(* 0 = 0 *) +Abort. +End A4. + +(* This worked in 8.2 and 8.3 as a side-effect of support for rewriting *) +(* with open terms (8.2, MS, r11543) *) + +5b- Pattern-unification of pre-existing evars in rewriting lemma + +Goal exists f, forall x y, f x y = 0 -> plus y x = 0. +eexists. intros x y H; rewrite H. +(* 0 = 0 *) +Abort. + +(* Works since pattern-unification on Evar was introduced *) +(* in unification.ml (8.3, HH, r12229) *) +(* currently governed by a flag: use_evars_pattern_unification *) + +5c- Pattern-unification of pre-existing evars in goal + +Goal exists f, forall x y, plus x y = 0 -> f y x = 0. +eexists. intros x y H; rewrite H. +(* 0 = 0 *) +Abort. + +(* This worked in 8.2 and 8.3 but was removed for autorewrite in 8.4 *) + +5d- Mixing pattern-unification of pre-existing evars in goal and evars in lemma + +Goal exists f, forall x, (forall y, plus x y = 0) -> forall y:nat, f y x = 0. +eexists. intros x H y. rewrite H. +(* 0 = 0 *) +Abort. + +(* This worked in 8.2 and 8.3 but was removed for autorewrite in 8.4 *) + +6- Multiple non-identical but convertible occurrences + +Tactic rewrite only considers the first one, from left-to-right, e.g.: + +Section A6. +Variable y: nat. +Hypothesis H: forall x, x+2 = 0. +Goal (y+(2+0))+(y+(1+1)) = (y+(1+1))+(y+(2+0)). +rewrite H. +(* 0+(y+(1+1)) = y+(1+1)+0 *) +Abort. +End A6. + +Tactic setoid rewrite first looks for syntactically equal terms and if +not uses the leftmost occurrence modulo delta. + +Require Import Setoid. +Section A6. +Variable y: nat. +Hypothesis H: forall x, x+2 = 0. +Goal (y+(2+0))+(y+2) = (y+2)+(y+(2+0)). +rewrite H at 1 2 3 4. +(* (y+(2+0))+0 = 0+(y+(2+0)) *) +Abort. + +Goal (y+(2+0))+(y+(1+1)) = (y+(1+1))+(y+(2+0)). +rewrite H at 1 2 3 4. +(* 0+(y+(1+1)) = y+(1+1)+0 *) +Abort. +End A6. + +7- Conversion + +Section A6. +Variable y: nat. +Hypothesis H: forall x, S x = 0. +Goal id 1 = 0. +rewrite H. + + +B- ELIMINATION (INDUCTION / CASE ANALYSIS) + +This is simpler because open terms are not allowed and no unification +is involved (8.3). diff --git a/dev/doc/universes.txt b/dev/doc/universes.txt index 65c1e522..a40706e9 100644 --- a/dev/doc/universes.txt +++ b/dev/doc/universes.txt @@ -1,32 +1,26 @@ How to debug universes? -1. There is a command Dump Universes in Coq toplevel +1. There is a command Print Universes in Coq toplevel - Dump Universes. + Print Universes. prints the graph of universes in the form of constraints - Dump Universes "file". + Print Universes "file". produces the "file" containing universe constraints in the form univ1 # univ2 ; where # can be either > >= or = - - The file produced by the latter command can be transformed using - the script univdot to dot format. - For example - univdot file | dot -Tps > file.ps - - produces a graph of universes in ps format. - > arrows are red, >= blue, and = black. + If "file" ends with .gv or .dot, the resulting file will be in + dot format. *) for dot see http://www.research.att.com/sw/tools/graphviz/ 2. There is a printing option - - Termast.print_universes : bool ref - which, when set (in ocaml after Drop), makes all pretty-printed - Type's annotated with the name of the universe. + {Set,Unset} Printing Universes. + + which, when set, makes all pretty-printed Type's annotated with the + name of the universe. diff --git a/dev/include b/dev/include index 251a969b..69ac3c41 100644 --- a/dev/include +++ b/dev/include @@ -1,6 +1,19 @@ (* File to include to install the pretty-printers in the ocaml toplevel *) +(* Typical usage : + + $ coqtop.byte # or even better : rlwrap coqtop.byte + Coq < Drop. + # #use "include";; + + Alternatively, you can avoid typing #use "include" after each Drop + by adding the following lines in your $HOME/.ocamlinit : + + if Filename.basename Sys.argv.(0) = "coqtop.byte" + then ignore (Toploop.use_silently Format.std_formatter "include") +*) + (* For OCaml 3.10.x: clflags.cmi (a ocaml compilation by-product) must be in the library path. On Debian, install ocaml-compiler-libs, and uncomment the following: @@ -14,7 +27,7 @@ #install_printer (* pp_stdcmds *) pppp;; #install_printer (* pattern *) pppattern;; -#install_printer (* rawconstr *) pprawconstr;; +#install_printer (* glob_constr *) ppglob_constr;; #install_printer (* constr *) ppconstr;; #install_printer (* constr_substituted *) ppsconstr;; @@ -24,12 +37,14 @@ #install_printer (* judgement *) ppj;; #install_printer (* hint_db *) print_hint_db;; +(*#install_printer (* hints_path *) pphintspath;;*) #install_printer (* goal *) ppgoal;; -#install_printer (* sigma goal *) ppsigmagoal;; -#install_printer (* proof *) pproof;; -#install_printer (* pftreestate *) pppftreestate;; +(*#install_printer (* sigma goal *) ppsigmagoal;;*) +(*#install_printer (* proof *) pproof;;*) +#install_printer (* Goal.goal *) ppgoalgoal;; #install_printer (* metaset.t *) ppmetas;; #install_printer (* evar_map *) ppevm;; +#install_printer (* ExistentialSet.t *) ppexistentialset;; #install_printer (* clenv *) ppclenv;; #install_printer (* env *) ppenv;; diff --git a/dev/ocamldoc/docintro b/dev/ocamldoc/docintro new file mode 100644 index 00000000..33d20fc8 --- /dev/null +++ b/dev/ocamldoc/docintro @@ -0,0 +1,49 @@ +{!indexlist} + +This is Coq, a proof assistant for the Calculus of Inductive Constructions. +This document describes the implementation of Coq. +It has been automatically generated from the source of +Coq using {{:http://caml.inria.fr/}ocamldoc}. +The source files are organized in several directories ordered like that: + +{ol {- Utility libraries : lib + +describes the various utility libraries used in the code +of Coq.} +{- Kernel : kernel + +describes the Coq kernel, which is a type checker for the Calculus +of Inductive Constructions.} +{- Library : library + +describes the Coq library, which is made of two parts: +- a general mechanism to keep a trace of all operations and of + the state of the system, with backtrack capabilities; +- a global environment for the CCI, with functions to export and + import compiled modules. + +} +{- Pretyping : pretyping + +} +{- Front abstract syntax of terms : interp + +describes the translation from Coq context-dependent +front abstract syntax of terms {v constr_expr v} to and from the +context-free, untyped, globalized form of constructions {v glob_constr v}.} +{- Parsers and printers : parsing + +describes the implementation of the Coq parsers and printers.} +{- Proof engine : proofs + +describes the Coq proof engine, which is also called +the ``refiner'', since it provides a way to build terms by successive +refining steps. Those steps are either primitive rules or higher-level +tactics.} +{- Tacticts : tactics + +describes the Coq main tactics.} +{- Toplevel : toplevel + +describes the highest modules of the Coq system.} +} diff --git a/dev/ocamldoc/html/style.css b/dev/ocamldoc/html/style.css new file mode 100644 index 00000000..c2c45b62 --- /dev/null +++ b/dev/ocamldoc/html/style.css @@ -0,0 +1,220 @@ +a:visited {
+ color: #416DFF; text-decoration: none;
+}
+
+a:link {
+ color: #416DFF; text-decoration: none;
+}
+
+a:hover {
+ color: Red; text-decoration: none; background-color: #5FFF88
+}
+
+a:active {
+ color: Red; text-decoration: underline;
+}
+
+.keyword {
+ font-weight: bold; color: Red
+}
+
+.keywordsign {
+ color: #C04600
+}
+
+.superscript {
+ font-size: 8
+}
+
+.subscript {
+ font-size: 8
+}
+
+.comment {
+ color: Green
+}
+
+.constructor {
+ color: Blue
+}
+
+.type {
+ color: #5C6585
+}
+
+.string {
+ color: Maroon
+}
+
+.warning {
+ color: Red; font-weight: bold
+}
+
+.info {
+ margin-left: 3em; margin-right: 3em
+}
+
+.param_info {
+ margin-top: 4px; margin-left: 3em; margin-right: 3em
+}
+
+.code {
+ color: #465F91;
+}
+
+h1 {
+ font-size: 20pt; text-align: center;
+}
+
+h5, h6, div.h7, div.h8, div.h9 {
+ font-size: 20pt;
+ border: 1px solid #000000;
+ margin-top: 5px;
+ margin-bottom: 2px;
+ text-align: center;
+ padding: 2px;
+}
+
+h5 {
+ background-color: #90FDFF;
+}
+
+h6 {
+ background-color: #016699;
+ color: white;
+}
+
+div.h7 {
+ background-color: #E0FFFF;
+}
+
+div.h8 {
+ background-color: #F0FFFF;
+}
+
+div.h9 {
+ background-color: #FFFFFF;
+}
+
+.typetable, .indextable, .paramstable {
+ border-style: hidden;
+}
+
+.paramstable {
+ padding: 5pt 5pt;
+}
+
+body {
+ background-color: white;
+}
+
+tr {
+ background-color: white;
+}
+
+td.typefieldcomment {
+ background-color: #FFFFFF;
+ font-size: smaller;
+}
+
+pre {
+ margin-bottom: 4px;
+}
+
+div.sig_block {
+ margin-left: 2em;
+}
+
+
+h2 {
+ font-family: Arial, Helvetica, sans-serif;
+ font-size: 16pt;
+ font-weight: normal;
+ border-bottom: 1px solid #dadada;
+ border-top: 1px solid #dadada;
+ color: #101010;
+ background: #eeeeff;
+ margin: 25px 0px 10px 0px;
+ padding: 1px 1px 1px 1px;
+}
+
+h3 {
+ font-family: Arial, Helvetica, sans-serif;
+ font-size: 12pt;
+ color: #016699;
+ font-weight: bold;
+ padding: 15px 0 0 0ex;
+ margin: 5px 0 0 0;
+}
+
+h4 {
+ font-family: Arial, Helvetica, sans-serif;
+ font-size: 10pt;
+ color: #016699;
+ padding: 15px 0 0 0ex;
+ margin: 5px 0 0 0;
+}
+
+/* Here starts the overwrite of default rules to give a better look */
+
+body {
+ font-family: Calibri, Georgia, Garamond, Baskerville, serif;
+ font-size: 12pt;
+ background-color: white;
+}
+
+a:link, a {
+ color: #6895c3 !important;
+}
+
+a:hover {
+ color: #2F4459 !important;
+ background-color: white;
+}
+
+hr {
+ height: 1px;
+ color: #016699;
+ background-color: #016699;
+ border-width: 0;
+}
+
+h1, h1 a:link, h1 a:visited, h1 a {
+ font-family: Cambria, Georgia, Garamond, Baskerville, serif;
+ color: #016699;
+}
+
+.navbar {
+ float: left;
+}
+
+.navbar a, .navbar a:link, .navbar a:visited {
+ color: #016699;
+ font-family: Arial, Helvetica, sans-serif;
+ font-weight: bold;
+ font-size: 80%;
+}
+
+.keyword {
+ color: #c13939;
+}
+
+.constructor {
+ color: #3c8f7e;
+}
+
+pre, code {
+ font-family: "DejaVu Sans Mono", "Bitstream Vera Mono", "Courrier New", monospace;
+ white-space: normal;
+ font-size: 9pt;
+ font-weight: bold;
+}
+
+.type br {
+ display: none;
+}
+
+.info {
+ margin-left: 1em;
+ font-size: 12pt;
+}
diff --git a/dev/ocamlweb-doc/Makefile b/dev/ocamlweb-doc/Makefile deleted file mode 100644 index 3189d7c5..00000000 --- a/dev/ocamlweb-doc/Makefile +++ /dev/null @@ -1,90 +0,0 @@ -include ../../config/Makefile - -LOCALINCLUDES=-I ../../config -I ../../tools -I ../../tools/coqdoc \ - -I ../../scripts -I ../../lib -I ../../kernel -I ../../kernel/byterun -I ../../library \ - -I ../../proofs -I ../../tactics -I ../../pretyping \ - -I ../../interp -I ../../toplevel -I ../../parsing -I ../../ide/utils -I ../../ide \ - -I ../../plugins/omega -I ../../plugins/romega \ - -I ../../plugins/ring -I ../../plugins/dp -I ../../plugins/setoid_ring \ - -I ../../plugins/xml -I ../../plugins/extraction \ - -I ../../plugins/fourier \ - -I ../../plugins/cc \ - -I ../../plugins/funind -I ../../plugins/firstorder \ - -I ../../plugins/field -I ../../plugins/subtac -I ../../plugins/rtauto \ - -I ../../plugins/recdef - -MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) - - -all:: newparse coq.ps minicop.ps -#newsyntax.dvi minicoq.dvi - - -OBJS=lex.cmo ast.cmo parse.cmo syntax.cmo - -newparse: $(OBJS) syntax.mli lex.ml syntax.ml - ocamlc -o newparse $(OBJS) - -%.cmo: %.ml - ocamlc -c $< - -%.cmi: %.mli - ocamlc -c $< - -%.ml: %.mll - ocamllex $< - -%.ml: %.mly - ocamlyacc -v $< - -%.mli: %.mly - ocamlyacc -v $< - -clean:: - rm -f *.cm* *.output syntax.ml syntax.mli lex.ml newparse - -parse.cmo: ast.cmo -syntax.cmi: parse.cmo -syntax.cmo: lex.cmo parse.cmo syntax.cmi -lex.cmo: syntax.cmi -ast.cmo: ast.ml - -newsyntax.dvi: newsyntax.tex - latex $< - latex $< - -coq.dvi: coq.tex - latex coq - latex coq - -coq.tex:: - ocamlweb -p "\usepackage{epsfig}" \ - macros.tex intro.tex \ - ../../lib/{doc.tex,*.mli} ../../kernel/{doc.tex,*.mli} ../../library/{doc.tex,*.mli} \ - ../../pretyping/{doc.tex,*.mli} ../../interp/{doc.tex,*.mli} \ - ../../parsing/{doc.tex,*.mli} ../../proofs/{doc.tex,*.mli} \ - ../../tactics/{doc.tex,*.mli} ../../toplevel/{doc.tex,*.mli} \ - -o coq.tex - - -depend:: kernel.dep.ps library.dep.ps pretyping.dep.ps parsing.dep.ps \ - proofs.dep.ps tactics.dep.ps toplevel.dep.ps interp.dep.ps - -%.dot: ../../% - ocamldoc -rectypes $(MLINCLUDES) -t $* -dot -dot-reduce ../../$*/*.ml ../../$*/*.mli -o $@ - -%.dep.ps: %.dot - dot -Tps $< -o $@ - -clean:: - rm -f *~ *.log *.aux - -.SUFFIXES: .tex .dvi .ps .cmo .cmi .mli .ml .mll .mly - -%.dvi: %.tex - latex $< && latex $< - -%.ps: %.dvi - dvips $< -o $@ - - diff --git a/dev/ocamlweb-doc/ast.ml b/dev/ocamlweb-doc/ast.ml deleted file mode 100644 index 4eb135d8..00000000 --- a/dev/ocamlweb-doc/ast.ml +++ /dev/null @@ -1,47 +0,0 @@ - -type constr_ast = - Pair of constr_ast * constr_ast -| Prod of binder list * constr_ast -| Lambda of binder list * constr_ast -| Let of string * constr_ast * constr_ast -| LetCase of binder list * constr_ast * constr_ast -| IfCase of constr_ast * constr_ast * constr_ast -| Eval of red_fun * constr_ast -| Infix of string * constr_ast * constr_ast -| Prefix of string * constr_ast -| Postfix of string * constr_ast -| Appl of constr_ast * constr_arg list -| ApplExpl of string list * constr_ast list -| Scope of string * constr_ast -| Qualid of string list -| Prop | Set | Type -| Int of string -| Hole -| Meta of string -| Fixp of fix_kind * - (string * binder list * constr_ast * string option * constr_ast) list * - string -| Match of case_item list * constr_ast option * - (pattern list * constr_ast) list - -and red_fun = Simpl - -and binder = string * constr_ast - -and constr_arg = string option * constr_ast - -and fix_kind = Fix | CoFix - -and case_item = constr_ast * (string option * constr_ast option) - -and pattern = - PatAs of pattern * string -| PatType of pattern * constr_ast -| PatConstr of string * pattern list -| PatVar of string - -let mk_cast c t = - if t=Hole then c else Infix(":",c,t) - -let mk_lambda bl t = - if bl=[] then t else Lambda(bl,t) diff --git a/dev/ocamlweb-doc/interp.dep.ps b/dev/ocamlweb-doc/interp.dep.ps deleted file mode 100644 index fda7a33c..00000000 --- a/dev/ocamlweb-doc/interp.dep.ps +++ /dev/null @@ -1,545 +0,0 @@ -%!PS-Adobe-2.0 -%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007) -%%For: (notin) Jean-Marc Notin,,, -%%Title: G -%%Pages: (atend) -%%BoundingBox: (atend) -%%EndComments -save -%%BeginProlog -/DotDict 200 dict def -DotDict begin - -/setupLatin1 { -mark -/EncodingVector 256 array def - EncodingVector 0 - -ISOLatin1Encoding 0 255 getinterval putinterval -EncodingVector 45 /hyphen put - -% Set up ISO Latin 1 character encoding -/starnetISO { - dup dup findfont dup length dict begin - { 1 index /FID ne { def }{ pop pop } ifelse - } forall - /Encoding EncodingVector def - currentdict end definefont -} def -/Times-Roman starnetISO def -/Times-Italic starnetISO def -/Times-Bold starnetISO def -/Times-BoldItalic starnetISO def -/Helvetica starnetISO def -/Helvetica-Oblique starnetISO def -/Helvetica-Bold starnetISO def -/Helvetica-BoldOblique starnetISO def -/Courier starnetISO def -/Courier-Oblique starnetISO def -/Courier-Bold starnetISO def -/Courier-BoldOblique starnetISO def -cleartomark -} bind def - -%%BeginResource: procset graphviz 0 0 -/coord-font-family /Times-Roman def -/default-font-family /Times-Roman def -/coordfont coord-font-family findfont 8 scalefont def - -/InvScaleFactor 1.0 def -/set_scale { - dup 1 exch div /InvScaleFactor exch def - scale -} bind def - -% styles -/solid { [] 0 setdash } bind def -/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def -/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def -/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def -/bold { 2 setlinewidth } bind def -/filled { } bind def -/unfilled { } bind def -/rounded { } bind def -/diagonals { } bind def - -% hooks for setting color -/nodecolor { sethsbcolor } bind def -/edgecolor { sethsbcolor } bind def -/graphcolor { sethsbcolor } bind def -/nopcolor {pop pop pop} bind def - -/beginpage { % i j npages - /npages exch def - /j exch def - /i exch def - /str 10 string def - npages 1 gt { - gsave - coordfont setfont - 0 0 moveto - (\() show i str cvs show (,) show j str cvs show (\)) show - grestore - } if -} bind def - -/set_font { - findfont exch - scalefont setfont -} def - -% draw aligned label in bounding box aligned to current point -/alignedtext { % width adj text - /text exch def - /adj exch def - /width exch def - gsave - width 0 gt { - text stringwidth pop adj mul 0 rmoveto - } if - [] 0 setdash - text show - grestore -} def - -/boxprim { % xcorner ycorner xsize ysize - 4 2 roll - moveto - 2 copy - exch 0 rlineto - 0 exch rlineto - pop neg 0 rlineto - closepath -} bind def - -/ellipse_path { - /ry exch def - /rx exch def - /y exch def - /x exch def - matrix currentmatrix - newpath - x y translate - rx ry scale - 0 0 1 0 360 arc - setmatrix -} bind def - -/endpage { showpage } bind def -/showpage { } def - -/layercolorseq - [ % layer color sequence - darkest to lightest - [0 0 0] - [.2 .8 .8] - [.4 .8 .8] - [.6 .8 .8] - [.8 .8 .8] - ] -def - -/layerlen layercolorseq length def - -/setlayer {/maxlayer exch def /curlayer exch def - layercolorseq curlayer 1 sub layerlen mod get - aload pop sethsbcolor - /nodecolor {nopcolor} def - /edgecolor {nopcolor} def - /graphcolor {nopcolor} def -} bind def - -/onlayer { curlayer ne {invis} if } def - -/onlayers { - /myupper exch def - /mylower exch def - curlayer mylower lt - curlayer myupper gt - or - {invis} if -} def - -/curlayer 0 def - -%%EndResource -%%EndProlog -%%BeginSetup -14 default-font-family set_font -1 setmiterlimit -% /arrowlength 10 def -% /arrowwidth 5 def - -% make sure pdfmark is harmless for PS-interpreters other than Distiller -/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse -% make '<<' and '>>' safe on PS Level 1 devices -/languagelevel where {pop languagelevel}{1} ifelse -2 lt { - userdict (<<) cvn ([) cvn load put - userdict (>>) cvn ([) cvn load put -} if - -%%EndSetup -setupLatin1 -%%Page: 1 1 -%%PageBoundingBox: 36 36 576 753 -%%PageOrientation: Landscape -gsave -36 36 576 753 boxprim clip newpath -0 0 1 beginpage -0.985401 0.985401 set_scale 90 rotate 40.5333 -580.533 translate -0.000 0.000 1.000 graphcolor -newpath -4 -4 moveto --4 544 lineto -724 544 lineto -724 -4 lineto -closepath fill -0.985401 setlinewidth -0.000 0.000 1.000 graphcolor -newpath -4 -4 moveto --4 544 lineto -724 544 lineto -724 -4 lineto -closepath stroke -% Constrextern -gsave -0.502 1.000 0.820 nodecolor -172 417 49.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -172 417 49.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -172 412 moveto 72 -0.5 (Constrextern) alignedtext -grestore -% Reserve -gsave -0.502 1.000 0.820 nodecolor -264 319 35.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -264 319 35.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -264 314 moveto 44 -0.5 (Reserve) alignedtext -grestore -% Constrextern->Reserve -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 188 400 moveto -203 384 225 361 242 343 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 245.049 344.831 moveto -249 335 lineto -239.781 340.221 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 245.049 344.831 moveto -249 335 lineto -239.781 340.221 lineto -closepath stroke -grestore -% Notation -gsave -0.502 1.000 0.820 nodecolor -268 122 37.1753 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -268 122 37.1753 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -268 117 moveto 49 -0.5 (Notation) alignedtext -grestore -% Constrextern->Notation -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 178 399 moveto -194 349 240 209 259 150 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 262.479 150.584 moveto -262 140 lineto -255.774 148.573 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 262.479 150.584 moveto -262 140 lineto -255.774 148.573 lineto -closepath stroke -grestore -% Topconstr -gsave -0.502 1.000 0.820 nodecolor -82 24 41.1755 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -82 24 41.1755 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -82 19 moveto 57 -0.5 (Topconstr) alignedtext -grestore -% Notation->Topconstr -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 243 109 moveto -211 91 154 62 117 43 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 118.441 39.7969 moveto -108 38 lineto -115.042 45.916 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 118.441 39.7969 moveto -108 38 lineto -115.042 45.916 lineto -closepath stroke -grestore -% Ppextend -gsave -0.502 1.000 0.820 nodecolor -278 24 39.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -278 24 39.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -278 19 moveto 52 -0.5 (Ppextend) alignedtext -grestore -% Notation->Ppextend -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 270 104 moveto -272 89 273 68 275 52 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 278.488 52.2987 moveto -276 42 lineto -271.522 51.6021 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 278.488 52.2987 moveto -276 42 lineto -271.522 51.6021 lineto -closepath stroke -grestore -% Constrintern -gsave -0.502 1.000 0.820 nodecolor -472 417 48.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -472 417 48.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -472 412 moveto 70 -0.5 (Constrintern) alignedtext -grestore -% Constrintern->Reserve -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 442 403 moveto -404 385 340 355 299 335 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 300.56 331.863 moveto -290 331 lineto -297.717 338.26 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 300.56 331.863 moveto -290 331 lineto -297.717 338.26 lineto -closepath stroke -grestore -% Implicit_quantifiers -gsave -0.502 1.000 0.820 nodecolor -508 319 69.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -508 319 69.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -508 314 moveto 112 -0.5 (Implicit_quantifiers) alignedtext -grestore -% Constrintern->Implicit_quantifiers -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 479 399 moveto -484 385 492 364 498 347 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 501.479 347.584 moveto -501 337 lineto -494.774 345.573 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 501.479 347.584 moveto -501 337 lineto -494.774 345.573 lineto -closepath stroke -grestore -% Syntax_def -gsave -0.502 1.000 0.820 nodecolor -396 220 45.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -396 220 45.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -396 215 moveto 64 -0.5 (Syntax_def) alignedtext -grestore -% Implicit_quantifiers->Syntax_def -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 488 302 moveto -469 285 442 261 422 244 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 424.546 241.596 moveto -415 237 lineto -419.596 246.546 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 424.546 241.596 moveto -415 237 lineto -419.596 246.546 lineto -closepath stroke -grestore -% Coqlib -gsave -0.502 1.000 0.820 nodecolor -656 515 32.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -656 515 32.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -656 510 moveto 38 -0.5 (Coqlib) alignedtext -grestore -% Genarg -gsave -0.502 1.000 0.820 nodecolor -82 122 33.175 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -82 122 33.175 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -82 117 moveto 41 -0.5 (Genarg) alignedtext -grestore -% Genarg->Topconstr -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 82 104 moveto -82 89 82 69 82 52 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 85.5001 52 moveto -82 42 lineto -78.5001 52 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 85.5001 52 moveto -82 42 lineto -78.5001 52 lineto -closepath stroke -grestore -% Syntax_def->Notation -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 375 204 moveto -354 187 320 161 296 143 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 298.1 140.2 moveto -288 137 lineto -293.9 145.8 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 298.1 140.2 moveto -288 137 lineto -293.9 145.8 lineto -closepath stroke -grestore -% Modintern -gsave -0.502 1.000 0.820 nodecolor -472 515 42.1756 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -472 515 42.1756 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -472 510 moveto 59 -0.5 (Modintern) alignedtext -grestore -% Modintern->Constrintern -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 472 497 moveto -472 482 472 462 472 445 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 475.5 445 moveto -472 435 lineto -468.5 445 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 475.5 445 moveto -472 435 lineto -468.5 445 lineto -closepath stroke -grestore -endpage -showpage -grestore -%%PageTrailer -%%EndPage: 1 -%%Trailer -%%Pages: 1 -%%BoundingBox: 36 36 576 753 -end -restore -%%EOF diff --git a/dev/ocamlweb-doc/intro.tex b/dev/ocamlweb-doc/intro.tex deleted file mode 100644 index 4cec8673..00000000 --- a/dev/ocamlweb-doc/intro.tex +++ /dev/null @@ -1,25 +0,0 @@ - -\ocwsection This is \Coq, a proof assistant for the \CCI. -This document describes the implementation of \Coq. -It has been automatically generated from the source of -\Coq\ using \textsf{ocamlweb}, a literate programming tool for -\textsf{Objective Caml}\footnote{\Coq, \textsf{Objective Caml} and - \textsf{ocamlweb} are all freely available at - \textsf{http://coq.inria.fr/}, \textsf{http://caml.inria.fr/} and - \textsf{http://www.lri.fr/\~{}filliatr/ocamlweb}.}. -The source files are organized in several directories, which are -described here as separate chapters. - -\begin{center} - \begin{tabular}{p{10cm}rr} - Chapter & section & page \\[0.5em] - \hline\\[0.2em] - Utility libraries \dotfill & \refsec{lib} & \pageref{lib} \\[0.5em] - Kernel \dotfill & \refsec{kernel} & \pageref{kernel} \\[0.5em] - Library \dotfill & \refsec{library} & \pageref{library} \\[0.5em] - Pretyping \dotfill & \refsec{pretyping} & \pageref{pretyping} \\[0.5em] - Proof engine \dotfill & \refsec{proofs} & \pageref{proofs} \\[0.5em] - Tactics \dotfill & \refsec{tactics} & \pageref{tactics} \\[0.5em] - Toplevel \dotfill & \refsec{toplevel}& \pageref{toplevel}\\[0.5em] - \end{tabular} -\end{center}
\ No newline at end of file diff --git a/dev/ocamlweb-doc/kernel.dep.ps b/dev/ocamlweb-doc/kernel.dep.ps deleted file mode 100644 index b7b4137b..00000000 --- a/dev/ocamlweb-doc/kernel.dep.ps +++ /dev/null @@ -1,1431 +0,0 @@ -%!PS-Adobe-2.0 -%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007) -%%For: (notin) Jean-Marc Notin,,, -%%Title: G -%%Pages: (atend) -%%BoundingBox: (atend) -%%EndComments -save -%%BeginProlog -/DotDict 200 dict def -DotDict begin - -/setupLatin1 { -mark -/EncodingVector 256 array def - EncodingVector 0 - -ISOLatin1Encoding 0 255 getinterval putinterval -EncodingVector 45 /hyphen put - -% Set up ISO Latin 1 character encoding -/starnetISO { - dup dup findfont dup length dict begin - { 1 index /FID ne { def }{ pop pop } ifelse - } forall - /Encoding EncodingVector def - currentdict end definefont -} def -/Times-Roman starnetISO def -/Times-Italic starnetISO def -/Times-Bold starnetISO def -/Times-BoldItalic starnetISO def -/Helvetica starnetISO def -/Helvetica-Oblique starnetISO def -/Helvetica-Bold starnetISO def -/Helvetica-BoldOblique starnetISO def -/Courier starnetISO def -/Courier-Oblique starnetISO def -/Courier-Bold starnetISO def -/Courier-BoldOblique starnetISO def -cleartomark -} bind def - -%%BeginResource: procset graphviz 0 0 -/coord-font-family /Times-Roman def -/default-font-family /Times-Roman def -/coordfont coord-font-family findfont 8 scalefont def - -/InvScaleFactor 1.0 def -/set_scale { - dup 1 exch div /InvScaleFactor exch def - scale -} bind def - -% styles -/solid { [] 0 setdash } bind def -/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def -/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def -/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def -/bold { 2 setlinewidth } bind def -/filled { } bind def -/unfilled { } bind def -/rounded { } bind def -/diagonals { } bind def - -% hooks for setting color -/nodecolor { sethsbcolor } bind def -/edgecolor { sethsbcolor } bind def -/graphcolor { sethsbcolor } bind def -/nopcolor {pop pop pop} bind def - -/beginpage { % i j npages - /npages exch def - /j exch def - /i exch def - /str 10 string def - npages 1 gt { - gsave - coordfont setfont - 0 0 moveto - (\() show i str cvs show (,) show j str cvs show (\)) show - grestore - } if -} bind def - -/set_font { - findfont exch - scalefont setfont -} def - -% draw aligned label in bounding box aligned to current point -/alignedtext { % width adj text - /text exch def - /adj exch def - /width exch def - gsave - width 0 gt { - text stringwidth pop adj mul 0 rmoveto - } if - [] 0 setdash - text show - grestore -} def - -/boxprim { % xcorner ycorner xsize ysize - 4 2 roll - moveto - 2 copy - exch 0 rlineto - 0 exch rlineto - pop neg 0 rlineto - closepath -} bind def - -/ellipse_path { - /ry exch def - /rx exch def - /y exch def - /x exch def - matrix currentmatrix - newpath - x y translate - rx ry scale - 0 0 1 0 360 arc - setmatrix -} bind def - -/endpage { showpage } bind def -/showpage { } def - -/layercolorseq - [ % layer color sequence - darkest to lightest - [0 0 0] - [.2 .8 .8] - [.4 .8 .8] - [.6 .8 .8] - [.8 .8 .8] - ] -def - -/layerlen layercolorseq length def - -/setlayer {/maxlayer exch def /curlayer exch def - layercolorseq curlayer 1 sub layerlen mod get - aload pop sethsbcolor - /nodecolor {nopcolor} def - /edgecolor {nopcolor} def - /graphcolor {nopcolor} def -} bind def - -/onlayer { curlayer ne {invis} if } def - -/onlayers { - /myupper exch def - /mylower exch def - curlayer mylower lt - curlayer myupper gt - or - {invis} if -} def - -/curlayer 0 def - -%%EndResource -%%EndProlog -%%BeginSetup -14 default-font-family set_font -1 setmiterlimit -% /arrowlength 10 def -% /arrowwidth 5 def - -% make sure pdfmark is harmless for PS-interpreters other than Distiller -/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse -% make '<<' and '>>' safe on PS Level 1 devices -/languagelevel where {pop languagelevel}{1} ifelse -2 lt { - userdict (<<) cvn ([) cvn load put - userdict (>>) cvn ([) cvn load put -} if - -%%EndSetup -setupLatin1 -%%Page: 1 1 -%%PageBoundingBox: 36 36 535 756 -%%PageOrientation: Landscape -gsave -36 36 535 756 boxprim clip newpath -0 0 1 beginpage -0.393658 0.393658 set_scale 90 rotate 95.45 -1355.45 translate -0.000 0.000 1.000 graphcolor -newpath -4 -4 moveto --4 1264 lineto -1825 1264 lineto -1825 -4 lineto -closepath fill -0.393658 setlinewidth -0.000 0.000 1.000 graphcolor -newpath -4 -4 moveto --4 1264 lineto -1825 1264 lineto -1825 -4 lineto -closepath stroke -% Cbytecodes -gsave -0.502 1.000 0.820 nodecolor -1258 234 45.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1258 234 45.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1258 229 moveto 64 -0.5 (Cbytecodes) alignedtext -grestore -% Term -gsave -0.502 1.000 0.820 nodecolor -1093 162 28.1746 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1093 162 28.1746 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1093 157 moveto 31 -0.5 (Term) alignedtext -grestore -% Cbytecodes->Term -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1227 221 moveto -1198 208 1155 189 1125 176 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1126.56 172.863 moveto -1116 172 lineto -1123.72 179.26 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1126.56 172.863 moveto -1116 172 lineto -1123.72 179.26 lineto -closepath stroke -grestore -% Esubst -gsave -0.502 1.000 0.820 nodecolor -1093 90 31.1748 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1093 90 31.1748 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1093 85 moveto 37 -0.5 (Esubst) alignedtext -grestore -% Term->Esubst -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1093 144 moveto -1093 136 1093 127 1093 118 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1096.5 118 moveto -1093 108 lineto -1089.5 118 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1096.5 118 moveto -1093 108 lineto -1089.5 118 lineto -closepath stroke -grestore -% Univ -gsave -0.502 1.000 0.820 nodecolor -580 90 27.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -580 90 27.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -580 85 moveto 28 -0.5 (Univ) alignedtext -grestore -% Term->Univ -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1065 158 moveto -979 145 714 109 616 95 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 616.299 91.5125 moveto -606 94 lineto -615.602 98.4778 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 616.299 91.5125 moveto -606 94 lineto -615.602 98.4778 lineto -closepath stroke -grestore -% Cbytegen -gsave -0.502 1.000 0.820 nodecolor -1148 522 39.1754 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1148 522 39.1754 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1148 517 moveto 53 -0.5 (Cbytegen) alignedtext -grestore -% Pre_env -gsave -0.502 1.000 0.820 nodecolor -1148 450 36.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1148 450 36.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1148 445 moveto 46 -0.5 (Pre_env) alignedtext -grestore -% Cbytegen->Pre_env -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1148 504 moveto -1148 496 1148 487 1148 478 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1151.5 478 moveto -1148 468 lineto -1144.5 478 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1151.5 478 moveto -1148 468 lineto -1144.5 478 lineto -closepath stroke -grestore -% Declarations -gsave -0.502 1.000 0.820 nodecolor -1148 378 48.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1148 378 48.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1148 373 moveto 70 -0.5 (Declarations) alignedtext -grestore -% Pre_env->Declarations -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1148 432 moveto -1148 424 1148 415 1148 406 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1151.5 406 moveto -1148 396 lineto -1144.5 406 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1151.5 406 moveto -1148 396 lineto -1144.5 406 lineto -closepath stroke -grestore -% Cemitcodes -gsave -0.502 1.000 0.820 nodecolor -663 306 45.1757 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -663 306 45.1757 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -663 301 moveto 65 -0.5 (Cemitcodes) alignedtext -grestore -% Cemitcodes->Cbytecodes -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 706 301 moveto -813 287 1088 254 1205 240 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1205.4 243.478 moveto -1215 239 lineto -1204.7 236.512 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1205.4 243.478 moveto -1215 239 lineto -1204.7 236.512 lineto -closepath stroke -grestore -% Copcodes -gsave -0.502 1.000 0.820 nodecolor -786 234 40.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -786 234 40.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -786 229 moveto 54 -0.5 (Copcodes) alignedtext -grestore -% Cemitcodes->Copcodes -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 688 291 moveto -707 281 732 266 752 253 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 753.958 255.916 moveto -761 248 lineto -750.559 249.797 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 753.958 255.916 moveto -761 248 lineto -750.559 249.797 lineto -closepath stroke -grestore -% Mod_subst -gsave -0.502 1.000 0.820 nodecolor -325 234 43.1756 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -325 234 43.1756 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -325 229 moveto 61 -0.5 (Mod_subst) alignedtext -grestore -% Cemitcodes->Mod_subst -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 623 298 moveto -561 284 441 259 374 244 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 374.492 240.529 moveto -364 242 lineto -373.119 247.393 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 374.492 240.529 moveto -364 242 lineto -373.119 247.393 lineto -closepath stroke -grestore -% Mod_subst->Term -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 367 230 moveto -502 217 925 178 1055 166 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1055.4 169.478 moveto -1065 165 lineto -1054.7 162.512 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1055.4 169.478 moveto -1065 165 lineto -1054.7 162.512 lineto -closepath stroke -grestore -% Closure -gsave -0.502 1.000 0.820 nodecolor -713 666 34.1751 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -713 666 34.1751 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -713 661 moveto 43 -0.5 (Closure) alignedtext -grestore -% Environ -gsave -0.502 1.000 0.820 nodecolor -1148 594 36.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1148 594 36.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1148 589 moveto 46 -0.5 (Environ) alignedtext -grestore -% Closure->Environ -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 746 661 moveto -823 648 1016 616 1104 602 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1104.88 605.393 moveto -1114 600 lineto -1103.51 598.529 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1104.88 605.393 moveto -1114 600 lineto -1103.51 598.529 lineto -closepath stroke -grestore -% Environ->Cbytegen -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1148 576 moveto -1148 568 1148 559 1148 550 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1151.5 550 moveto -1148 540 lineto -1144.5 550 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1151.5 550 moveto -1148 540 lineto -1144.5 550 lineto -closepath stroke -grestore -% Conv_oracle -gsave -0.502 1.000 0.820 nodecolor -383 522 48.1758 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -383 522 48.1758 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -383 517 moveto 71 -0.5 (Conv_oracle) alignedtext -grestore -% Names -gsave -0.502 1.000 0.820 nodecolor -288 18 32.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -288 18 32.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -288 13 moveto 38 -0.5 (Names) alignedtext -grestore -% Conv_oracle->Names -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 339 515 moveto -238 497 0 449 0 378 curveto -0 378 0 378 0 162 curveto -0 53 166 26 246 20 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 246.398 23.4778 moveto -256 19 lineto -245.701 16.5125 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 246.398 23.4778 moveto -256 19 lineto -245.701 16.5125 lineto -closepath stroke -grestore -% Cooking -gsave -0.502 1.000 0.820 nodecolor -960 1026 37.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -960 1026 37.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -960 1021 moveto 48 -0.5 (Cooking) alignedtext -grestore -% Typeops -gsave -0.502 1.000 0.820 nodecolor -960 954 37.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -960 954 37.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -960 949 moveto 48 -0.5 (Typeops) alignedtext -grestore -% Cooking->Typeops -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 960 1008 moveto -960 1000 960 991 960 982 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 963.5 982 moveto -960 972 lineto -956.5 982 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 963.5 982 moveto -960 972 lineto -956.5 982 lineto -closepath stroke -grestore -% Entries -gsave -0.502 1.000 0.820 nodecolor -1391 882 33.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1391 882 33.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1391 877 moveto 40 -0.5 (Entries) alignedtext -grestore -% Typeops->Entries -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 995 948 moveto -1074 935 1265 903 1349 889 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1349.88 892.393 moveto -1359 887 lineto -1348.51 885.529 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1349.88 892.393 moveto -1359 887 lineto -1348.51 885.529 lineto -closepath stroke -grestore -% Inductive -gsave -0.502 1.000 0.820 nodecolor -837 882 39.1754 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -837 882 39.1754 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -837 877 moveto 53 -0.5 (Inductive) alignedtext -grestore -% Typeops->Inductive -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 936 940 moveto -918 929 891 914 871 901 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 872.441 897.797 moveto -862 896 lineto -869.042 903.916 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 872.441 897.797 moveto -862 896 lineto -869.042 903.916 lineto -closepath stroke -grestore -% Csymtable -gsave -0.502 1.000 0.820 nodecolor -1148 666 42.1756 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1148 666 42.1756 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1148 661 moveto 59 -0.5 (Csymtable) alignedtext -grestore -% Csymtable->Environ -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1148 648 moveto -1148 640 1148 631 1148 622 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1151.5 622 moveto -1148 612 lineto -1144.5 622 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1151.5 622 moveto -1148 612 lineto -1144.5 622 lineto -closepath stroke -grestore -% Vm -gsave -0.502 1.000 0.820 nodecolor -731 594 27 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -731 594 27 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -731 589 moveto 21 -0.5 (Vm) alignedtext -grestore -% Csymtable->Vm -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1109 659 moveto -1029 645 845 614 767 600 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 767.492 596.529 moveto -757 598 lineto -766.119 603.393 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 767.492 596.529 moveto -757 598 lineto -766.119 603.393 lineto -closepath stroke -grestore -% Vm->Cemitcodes -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 727 576 moveto -716 527 684 392 669 334 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 672.393 333.119 moveto -667 324 lineto -665.529 334.492 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 672.393 333.119 moveto -667 324 lineto -665.529 334.492 lineto -closepath stroke -grestore -% Vm->Conv_oracle -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 705 589 moveto -648 577 510 549 435 533 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 435.492 529.529 moveto -425 531 lineto -434.119 536.393 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 435.492 529.529 moveto -425 531 lineto -434.119 536.393 lineto -closepath stroke -grestore -% Declarations->Cemitcodes -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1103 371 moveto -1013 358 811 328 715 314 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 715.492 310.529 moveto -705 312 lineto -714.119 317.393 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 715.492 310.529 moveto -705 312 lineto -714.119 317.393 lineto -closepath stroke -grestore -% Sign -gsave -0.502 1.000 0.820 nodecolor -1697 306 27 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1697 306 27 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1697 301 moveto 26 -0.5 (Sign) alignedtext -grestore -% Declarations->Sign -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1193 372 moveto -1300 359 1563 324 1660 311 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1660.4 314.478 moveto -1670 310 lineto -1659.7 307.512 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1660.4 314.478 moveto -1670 310 lineto -1659.7 307.512 lineto -closepath stroke -grestore -% Retroknowledge -gsave -0.502 1.000 0.820 nodecolor -1221 306 59.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1221 306 59.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1221 301 moveto 92 -0.5 (Retroknowledge) alignedtext -grestore -% Declarations->Retroknowledge -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1165 361 moveto -1175 352 1186 341 1197 330 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1199.4 332.546 moveto -1204 323 lineto -1194.45 327.596 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1199.4 332.546 moveto -1204 323 lineto -1194.45 327.596 lineto -closepath stroke -grestore -% Sign->Term -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1671 300 moveto -1576 277 1241 197 1130 170 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1130.49 166.529 moveto -1120 168 lineto -1129.12 173.393 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1130.49 166.529 moveto -1120 168 lineto -1129.12 173.393 lineto -closepath stroke -grestore -% Retroknowledge->Cbytecodes -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1230 288 moveto -1234 280 1239 270 1244 261 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1247.2 262.441 moveto -1249 252 lineto -1241.08 259.042 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1247.2 262.441 moveto -1249 252 lineto -1241.08 259.042 lineto -closepath stroke -grestore -% Entries->Sign -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1411 868 moveto -1442 844 1496 795 1496 738 curveto -1496 738 1496 738 1496 450 curveto -1496 370 1604 330 1661 314 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1661.88 317.393 moveto -1671 312 lineto -1660.51 310.529 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1661.88 317.393 moveto -1671 312 lineto -1660.51 310.529 lineto -closepath stroke -grestore -% Indtypes -gsave -0.502 1.000 0.820 nodecolor -539 1026 37.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -539 1026 37.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -539 1021 moveto 48 -0.5 (Indtypes) alignedtext -grestore -% Indtypes->Typeops -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 574 1020 moveto -650 1008 831 977 915 962 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 915.881 965.393 moveto -925 960 lineto -914.508 958.529 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 915.881 965.393 moveto -925 960 lineto -914.508 958.529 lineto -closepath stroke -grestore -% Type_errors -gsave -0.502 1.000 0.820 nodecolor -713 810 47.1758 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -713 810 47.1758 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -713 805 moveto 69 -0.5 (Type_errors) alignedtext -grestore -% Inductive->Type_errors -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 813 868 moveto -794 858 769 843 748 830 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 749.441 826.797 moveto -739 825 lineto -746.042 832.916 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 749.441 826.797 moveto -739 825 lineto -746.042 832.916 lineto -closepath stroke -grestore -% Reduction -gsave -0.502 1.000 0.820 nodecolor -713 738 41.1755 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -713 738 41.1755 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -713 733 moveto 57 -0.5 (Reduction) alignedtext -grestore -% Type_errors->Reduction -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 713 792 moveto -713 784 713 775 713 766 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 716.5 766 moveto -713 756 lineto -709.5 766 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 716.5 766 moveto -713 756 lineto -709.5 766 lineto -closepath stroke -grestore -% Modops -gsave -0.502 1.000 0.820 nodecolor -1404 954 35.1752 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1404 954 35.1752 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1404 949 moveto 45 -0.5 (Modops) alignedtext -grestore -% Modops->Environ -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1439 951 moveto -1511 943 1670 914 1670 810 curveto -1670 810 1670 810 1670 738 curveto -1670 639 1322 606 1194 597 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1194.3 593.512 moveto -1184 596 lineto -1193.6 600.478 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1194.3 593.512 moveto -1184 596 lineto -1193.6 600.478 lineto -closepath stroke -grestore -% Modops->Entries -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1401 936 moveto -1400 928 1398 919 1396 910 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1399.39 909.119 moveto -1394 900 lineto -1392.53 910.492 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1399.39 909.119 moveto -1394 900 lineto -1392.53 910.492 lineto -closepath stroke -grestore -% Mod_typing -gsave -0.502 1.000 0.820 nodecolor -1157 1170 47.1758 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1157 1170 47.1758 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1157 1165 moveto 69 -0.5 (Mod_typing) alignedtext -grestore -% Subtyping -gsave -0.502 1.000 0.820 nodecolor -1404 1026 42.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1404 1026 42.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1404 1021 moveto 58 -0.5 (Subtyping) alignedtext -grestore -% Mod_typing->Subtyping -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1183 1155 moveto -1227 1129 1320 1075 1370 1046 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1371.96 1048.92 moveto -1379 1041 lineto -1368.56 1042.8 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1371.96 1048.92 moveto -1379 1041 lineto -1368.56 1042.8 lineto -closepath stroke -grestore -% Term_typing -gsave -0.502 1.000 0.820 nodecolor -960 1098 50.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -960 1098 50.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -960 1093 moveto 74 -0.5 (Term_typing) alignedtext -grestore -% Mod_typing->Term_typing -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1123 1157 moveto -1090 1145 1040 1127 1005 1114 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1005.58 1110.52 moveto -995 1111 lineto -1003.57 1117.23 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1005.58 1110.52 moveto -995 1111 lineto -1003.57 1117.23 lineto -closepath stroke -grestore -% Subtyping->Typeops -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1365 1020 moveto -1282 1007 1092 975 1005 962 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1005.49 958.529 moveto -995 960 lineto -1004.12 965.393 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1005.49 958.529 moveto -995 960 lineto -1004.12 965.393 lineto -closepath stroke -grestore -% Subtyping->Modops -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1404 1008 moveto -1404 1000 1404 991 1404 982 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1407.5 982 moveto -1404 972 lineto -1400.5 982 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1407.5 982 moveto -1404 972 lineto -1400.5 982 lineto -closepath stroke -grestore -% Term_typing->Cooking -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 960 1080 moveto -960 1072 960 1063 960 1054 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 963.5 1054 moveto -960 1044 lineto -956.5 1054 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 963.5 1054 moveto -960 1044 lineto -956.5 1054 lineto -closepath stroke -grestore -% Term_typing->Indtypes -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 915 1090 moveto -833 1077 665 1048 584 1034 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 584.492 1030.53 moveto -574 1032 lineto -583.119 1037.39 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 584.492 1030.53 moveto -574 1032 lineto -583.119 1037.39 lineto -closepath stroke -grestore -% Reduction->Closure -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 713 720 moveto -713 712 713 703 713 694 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 716.5 694 moveto -713 684 lineto -709.5 694 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 716.5 694 moveto -713 684 lineto -709.5 694 lineto -closepath stroke -grestore -% Reduction->Conv_oracle -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 690 723 moveto -633 686 482 587 415 544 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 417.1 541.2 moveto -407 538 lineto -412.9 546.8 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 417.1 541.2 moveto -407 538 lineto -412.9 546.8 lineto -closepath stroke -grestore -% Safe_typing -gsave -0.502 1.000 0.820 nodecolor -1157 1242 47.1777 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1157 1242 47.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1157 1237 moveto 68 -0.5 (Safe_typing) alignedtext -grestore -% Safe_typing->Mod_typing -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1157 1224 moveto -1157 1216 1157 1207 1157 1198 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1160.5 1198 moveto -1157 1188 lineto -1153.5 1198 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1160.5 1198 moveto -1157 1188 lineto -1153.5 1198 lineto -closepath stroke -grestore -% Univ->Names -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 555 84 moveto -504 71 388 42 327 27 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 327.492 23.5292 moveto -317 25 lineto -326.119 30.3933 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 327.492 23.5292 moveto -317 25 lineto -326.119 30.3933 lineto -closepath stroke -grestore -% Vconv -gsave -0.502 1.000 0.820 nodecolor -1152 810 31.1748 18 ellipse_path fill -0.393658 setlinewidth -filled -0.502 1.000 0.820 nodecolor -1152 810 31.1748 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -1152 805 moveto 37 -0.5 (Vconv) alignedtext -grestore -% Vconv->Csymtable -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1151 792 moveto -1150 767 1149 723 1148 694 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 1151.5 694 moveto -1148 684 lineto -1144.5 694 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 1151.5 694 moveto -1148 684 lineto -1144.5 694 lineto -closepath stroke -grestore -% Vconv->Reduction -gsave -0.393658 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1122 805 moveto -1047 792 852 760 761 746 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 761.492 742.529 moveto -751 744 lineto -760.119 749.393 lineto -closepath fill -0.393658 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 761.492 742.529 moveto -751 744 lineto -760.119 749.393 lineto -closepath stroke -grestore -endpage -showpage -grestore -%%PageTrailer -%%EndPage: 1 -%%Trailer -%%Pages: 1 -%%BoundingBox: 36 36 535 756 -end -restore -%%EOF diff --git a/dev/ocamlweb-doc/lex.mll b/dev/ocamlweb-doc/lex.mll deleted file mode 100644 index 059526d9..00000000 --- a/dev/ocamlweb-doc/lex.mll +++ /dev/null @@ -1,81 +0,0 @@ - -{ - open Lexing - open Syntax - - let chan_out = ref stdout - - let comment_depth = ref 0 - let print s = output_string !chan_out s - - exception Fin_fichier - -} - -let space = [' ' '\t' '\n'] -let letter = ['a'-'z' 'A'-'Z'] -let digit = ['0'-'9'] - -let identifier = letter (letter | digit | ['_' '\''])* -let number = digit+ -let oper = ['-' '+' '/' '*' '|' '>' '<' '=' '%' '#' '$' ':' '\\' '?' - '.' '!' '@' ]+ - -rule token = parse - | "let" {LET} - | "in" {IN} - | "match" {MATCH} - | "with" {WITH} - | "end" {END} - | "and" {AND} - | "fun" {FUN} - | "if" {IF} - | "then" {THEN} - | "else" {ELSE} - | "eval" {EVAL} - | "for" {FOR} - | "Prop" {PROP} - | "Set" {SET} - | "Type" {TYPE} - | "fix" {FIX} - | "cofix" {COFIX} - | "struct" {STRUCT} - | "as" {AS} - - | "Simpl" {SIMPL} - - | "_" {WILDCARD} - | "(" {LPAR} - | ")" {RPAR} - | "{" {LBRACE} - | "}" {RBRACE} - | "!" {BANG} - | "@" {AT} - | ":" {COLON} - | ":=" {COLONEQ} - | "." {DOT} - | "," {COMMA} - | "->" {OPER "->"} - | "=>" {RARROW} - | "|" {BAR} - | "%" {PERCENT} - - | '?' { META(ident lexbuf)} - | number { INT(Lexing.lexeme lexbuf) } - | oper { OPER(Lexing.lexeme lexbuf) } - | identifier { IDENT (Lexing.lexeme lexbuf) } - | "(*" (*"*)"*) { comment_depth := 1; - comment lexbuf; - token lexbuf } - | space+ { token lexbuf} - | eof { EOF } - -and ident = parse - | identifier { Lexing.lexeme lexbuf } - -and comment = parse - | "(*" (*"*)"*) { incr comment_depth; comment lexbuf } - | (*"(*"*) "*)" - { decr comment_depth; if !comment_depth > 0 then comment lexbuf } - | eof { raise Fin_fichier } - | _ { comment lexbuf } diff --git a/dev/ocamlweb-doc/library.dep.ps b/dev/ocamlweb-doc/library.dep.ps deleted file mode 100644 index c9bb351e..00000000 --- a/dev/ocamlweb-doc/library.dep.ps +++ /dev/null @@ -1,773 +0,0 @@ -%!PS-Adobe-2.0 -%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007) -%%For: (notin) Jean-Marc Notin,,, -%%Title: G -%%Pages: (atend) -%%BoundingBox: (atend) -%%EndComments -save -%%BeginProlog -/DotDict 200 dict def -DotDict begin - -/setupLatin1 { -mark -/EncodingVector 256 array def - EncodingVector 0 - -ISOLatin1Encoding 0 255 getinterval putinterval -EncodingVector 45 /hyphen put - -% Set up ISO Latin 1 character encoding -/starnetISO { - dup dup findfont dup length dict begin - { 1 index /FID ne { def }{ pop pop } ifelse - } forall - /Encoding EncodingVector def - currentdict end definefont -} def -/Times-Roman starnetISO def -/Times-Italic starnetISO def -/Times-Bold starnetISO def -/Times-BoldItalic starnetISO def -/Helvetica starnetISO def -/Helvetica-Oblique starnetISO def -/Helvetica-Bold starnetISO def -/Helvetica-BoldOblique starnetISO def -/Courier starnetISO def -/Courier-Oblique starnetISO def -/Courier-Bold starnetISO def -/Courier-BoldOblique starnetISO def -cleartomark -} bind def - -%%BeginResource: procset graphviz 0 0 -/coord-font-family /Times-Roman def -/default-font-family /Times-Roman def -/coordfont coord-font-family findfont 8 scalefont def - -/InvScaleFactor 1.0 def -/set_scale { - dup 1 exch div /InvScaleFactor exch def - scale -} bind def - -% styles -/solid { [] 0 setdash } bind def -/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def -/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def -/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def -/bold { 2 setlinewidth } bind def -/filled { } bind def -/unfilled { } bind def -/rounded { } bind def -/diagonals { } bind def - -% hooks for setting color -/nodecolor { sethsbcolor } bind def -/edgecolor { sethsbcolor } bind def -/graphcolor { sethsbcolor } bind def -/nopcolor {pop pop pop} bind def - -/beginpage { % i j npages - /npages exch def - /j exch def - /i exch def - /str 10 string def - npages 1 gt { - gsave - coordfont setfont - 0 0 moveto - (\() show i str cvs show (,) show j str cvs show (\)) show - grestore - } if -} bind def - -/set_font { - findfont exch - scalefont setfont -} def - -% draw aligned label in bounding box aligned to current point -/alignedtext { % width adj text - /text exch def - /adj exch def - /width exch def - gsave - width 0 gt { - text stringwidth pop adj mul 0 rmoveto - } if - [] 0 setdash - text show - grestore -} def - -/boxprim { % xcorner ycorner xsize ysize - 4 2 roll - moveto - 2 copy - exch 0 rlineto - 0 exch rlineto - pop neg 0 rlineto - closepath -} bind def - -/ellipse_path { - /ry exch def - /rx exch def - /y exch def - /x exch def - matrix currentmatrix - newpath - x y translate - rx ry scale - 0 0 1 0 360 arc - setmatrix -} bind def - -/endpage { showpage } bind def -/showpage { } def - -/layercolorseq - [ % layer color sequence - darkest to lightest - [0 0 0] - [.2 .8 .8] - [.4 .8 .8] - [.6 .8 .8] - [.8 .8 .8] - ] -def - -/layerlen layercolorseq length def - -/setlayer {/maxlayer exch def /curlayer exch def - layercolorseq curlayer 1 sub layerlen mod get - aload pop sethsbcolor - /nodecolor {nopcolor} def - /edgecolor {nopcolor} def - /graphcolor {nopcolor} def -} bind def - -/onlayer { curlayer ne {invis} if } def - -/onlayers { - /myupper exch def - /mylower exch def - curlayer mylower lt - curlayer myupper gt - or - {invis} if -} def - -/curlayer 0 def - -%%EndResource -%%EndProlog -%%BeginSetup -14 default-font-family set_font -1 setmiterlimit -% /arrowlength 10 def -% /arrowwidth 5 def - -% make sure pdfmark is harmless for PS-interpreters other than Distiller -/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse -% make '<<' and '>>' safe on PS Level 1 devices -/languagelevel where {pop languagelevel}{1} ifelse -2 lt { - userdict (<<) cvn ([) cvn load put - userdict (>>) cvn ([) cvn load put -} if - -%%EndSetup -setupLatin1 -%%Page: 1 1 -%%PageBoundingBox: 36 36 576 752 -%%PageOrientation: Landscape -gsave -36 36 576 752 boxprim clip newpath -0 0 1 beginpage -0.985401 0.985401 set_scale 90 rotate 40.5333 -580.533 translate -0.000 0.000 1.000 graphcolor -newpath -4 -4 moveto --4 544 lineto -723 544 lineto -723 -4 lineto -closepath fill -0.985401 setlinewidth -0.000 0.000 1.000 graphcolor -newpath -4 -4 moveto --4 544 lineto -723 544 lineto -723 -4 lineto -closepath stroke -% Declare -gsave -0.502 1.000 0.820 nodecolor -488 436 34.1751 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -488 436 34.1751 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -488 431 moveto 43 -0.5 (Declare) alignedtext -grestore -% Dischargedhypsmap -gsave -0.502 1.000 0.820 nodecolor -488 353 69.1764 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -488 353 69.1764 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -488 348 moveto 113 -0.5 (Dischargedhypsmap) alignedtext -grestore -% Declare->Dischargedhypsmap -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 488 418 moveto -488 407 488 393 488 381 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 491.5 381 moveto -488 371 lineto -484.5 381 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 491.5 381 moveto -488 371 lineto -484.5 381 lineto -closepath stroke -grestore -% Impargs -gsave -0.502 1.000 0.820 nodecolor -201 353 36.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -201 353 36.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -201 348 moveto 46 -0.5 (Impargs) alignedtext -grestore -% Declare->Impargs -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 458 427 moveto -407 412 301 382 242 365 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 242.584 361.521 moveto -232 362 lineto -240.573 368.226 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 242.584 361.521 moveto -232 362 lineto -240.573 368.226 lineto -closepath stroke -grestore -% Decl_kinds -gsave -0.502 1.000 0.820 nodecolor -661 353 44.1757 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -661 353 44.1757 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -661 348 moveto 63 -0.5 (Decl_kinds) alignedtext -grestore -% Declare->Decl_kinds -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 514 424 moveto -543 410 590 388 624 372 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 625.958 374.916 moveto -633 367 lineto -622.559 368.797 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 625.958 374.916 moveto -633 367 lineto -622.559 368.797 lineto -closepath stroke -grestore -% Lib -gsave -0.502 1.000 0.820 nodecolor -219 270 27 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -219 270 27 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -219 265 moveto 20 -0.5 (Lib) alignedtext -grestore -% Dischargedhypsmap->Lib -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 443 339 moveto -390 323 302 296 254 281 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 254.584 277.521 moveto -244 278 lineto -252.573 284.226 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 254.584 277.521 moveto -244 278 lineto -252.573 284.226 lineto -closepath stroke -grestore -% Global -gsave -0.502 1.000 0.820 nodecolor -82 270 32.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -82 270 32.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -82 265 moveto 38 -0.5 (Global) alignedtext -grestore -% Impargs->Global -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 180 338 moveto -161 325 132 305 110 290 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 112.1 287.2 moveto -102 284 lineto -107.9 292.8 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 112.1 287.2 moveto -102 284 lineto -107.9 292.8 lineto -closepath stroke -grestore -% Impargs->Lib -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 205 335 moveto -207 324 210 310 213 298 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 216.471 298.492 moveto -215 288 lineto -209.607 297.119 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 216.471 298.492 moveto -215 288 lineto -209.607 297.119 lineto -closepath stroke -grestore -% Declaremods -gsave -0.502 1.000 0.820 nodecolor -65 353 49.1759 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -65 353 49.1759 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -65 348 moveto 73 -0.5 (Declaremods) alignedtext -grestore -% Declaremods->Global -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 69 335 moveto -71 324 74 310 76 298 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 79.4708 298.492 moveto -78 288 lineto -72.6067 297.119 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 79.4708 298.492 moveto -78 288 lineto -72.6067 297.119 lineto -closepath stroke -grestore -% Declaremods->Lib -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 93 338 moveto -120 324 161 301 189 286 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 190.958 288.916 moveto -198 281 lineto -187.559 282.797 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 190.958 288.916 moveto -198 281 lineto -187.559 282.797 lineto -closepath stroke -grestore -% Summary -gsave -0.502 1.000 0.820 nodecolor -69 103 40.1755 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -69 103 40.1755 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -69 98 moveto 55 -0.5 (Summary) alignedtext -grestore -% Global->Summary -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 81 252 moveto -78 223 74 166 71 131 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 74.4778 130.602 moveto -70 121 lineto -67.5125 131.299 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 74.4778 130.602 moveto -70 121 lineto -67.5125 131.299 lineto -closepath stroke -grestore -% Libnames -gsave -0.502 1.000 0.820 nodecolor -203 103 40.1755 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -203 103 40.1755 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -203 98 moveto 55 -0.5 (Libnames) alignedtext -grestore -% Global->Libnames -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 94 253 moveto -115 224 159 164 184 129 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 186.8 131.1 moveto -190 121 lineto -181.2 126.9 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 186.8 131.1 moveto -190 121 lineto -181.2 126.9 lineto -closepath stroke -grestore -% Nametab -gsave -0.502 1.000 0.820 nodecolor -203 186 38.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -203 186 38.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -203 181 moveto 50 -0.5 (Nametab) alignedtext -grestore -% Lib->Nametab -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 216 252 moveto -214 241 211 226 209 214 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 212.393 213.119 moveto -207 204 lineto -205.529 214.492 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 212.393 213.119 moveto -207 204 lineto -205.529 214.492 lineto -closepath stroke -grestore -% Libobject -gsave -0.502 1.000 0.820 nodecolor -329 186 40.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -329 186 40.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -329 181 moveto 54 -0.5 (Libobject) alignedtext -grestore -% Lib->Libobject -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 237 256 moveto -254 243 280 223 300 208 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 302.1 210.8 moveto -308 202 lineto -297.9 205.2 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 302.1 210.8 moveto -308 202 lineto -297.9 205.2 lineto -closepath stroke -grestore -% Nameops -gsave -0.502 1.000 0.820 nodecolor -203 20 39.1777 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -203 20 39.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -203 15 moveto 52 -0.5 (Nameops) alignedtext -grestore -% Libnames->Nameops -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 203 85 moveto -203 74 203 60 203 48 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 206.5 48 moveto -203 38 lineto -199.5 48 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 206.5 48 moveto -203 38 lineto -199.5 48 lineto -closepath stroke -grestore -% Goptions -gsave -0.502 1.000 0.820 nodecolor -322 353 38.1754 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -322 353 38.1754 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -322 348 moveto 51 -0.5 (Goptions) alignedtext -grestore -% Goptions->Lib -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 303 337 moveto -287 324 263 305 245 291 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 246.831 287.951 moveto -237 284 lineto -242.221 293.219 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 246.831 287.951 moveto -237 284 lineto -242.221 293.219 lineto -closepath stroke -grestore -% Nametab->Summary -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 180 172 moveto -158 159 125 138 101 123 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 102.441 119.797 moveto -92 118 lineto -99.0418 125.916 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 102.441 119.797 moveto -92 118 lineto -99.0418 125.916 lineto -closepath stroke -grestore -% Nametab->Libnames -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 203 168 moveto -203 157 203 143 203 131 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 206.5 131 moveto -203 121 lineto -199.5 131 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 206.5 131 moveto -203 121 lineto -199.5 131 lineto -closepath stroke -grestore -% Libobject->Libnames -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 306 171 moveto -286 158 256 138 235 124 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 236.262 120.635 moveto -226 118 lineto -232.379 126.459 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 236.262 120.635 moveto -226 118 lineto -232.379 126.459 lineto -closepath stroke -grestore -% Library -gsave -0.502 1.000 0.820 nodecolor -65 436 34.1751 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -65 436 34.1751 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -65 431 moveto 43 -0.5 (Library) alignedtext -grestore -% Library->Declaremods -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 65 418 moveto -65 407 65 393 65 381 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 68.5001 381 moveto -65 371 lineto -61.5001 381 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 68.5001 381 moveto -65 371 lineto -61.5001 381 lineto -closepath stroke -grestore -% States -gsave -0.502 1.000 0.820 nodecolor -65 519 29.1747 18 ellipse_path fill -0.985401 setlinewidth -filled -0.502 1.000 0.820 nodecolor -65 519 29.1747 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -65 514 moveto 33 -0.5 (States) alignedtext -grestore -% States->Library -gsave -0.985401 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 65 501 moveto -65 490 65 476 65 464 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 68.5001 464 moveto -65 454 lineto -61.5001 464 lineto -closepath fill -0.985401 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 68.5001 464 moveto -65 454 lineto -61.5001 464 lineto -closepath stroke -grestore -endpage -showpage -grestore -%%PageTrailer -%%EndPage: 1 -%%Trailer -%%Pages: 1 -%%BoundingBox: 36 36 576 752 -end -restore -%%EOF diff --git a/dev/ocamlweb-doc/macros.tex b/dev/ocamlweb-doc/macros.tex deleted file mode 100644 index 6beacf7b..00000000 --- a/dev/ocamlweb-doc/macros.tex +++ /dev/null @@ -1,7 +0,0 @@ - -% macros for coq.tex - -\newcommand{\Coq}{\textsf{Coq}} -\newcommand{\CCI}{Calculus of Inductive Constructions} - -\newcommand{\refsec}[1]{\textbf{\ref{#1}}}
\ No newline at end of file diff --git a/dev/ocamlweb-doc/parse.ml b/dev/ocamlweb-doc/parse.ml deleted file mode 100644 index b145fffd..00000000 --- a/dev/ocamlweb-doc/parse.ml +++ /dev/null @@ -1,183 +0,0 @@ - -open Ast - -type assoc = L | R | N - -let level = function - | "--" -> 70,L - | "=" -> 70,N - | "+" -> 60,L - | "++" -> 60,R - | "+++" -> 60,R - | "-" -> 60,L - | "*" -> 50,L - | "/" -> 50,L - | "**" -> 40,R - | ":" -> (100,R) - | "->" -> (90,R) - | s -> failwith ("unknowm operator '"^s^"'") - -let fixity = function - | "--" -> [L] - | "=" -> [N] - | ("+"|"-"|"*"|"/") -> [L;N] - | "++" -> [R] - | _ -> [L;N;R] - -let ground_oper = function - ("-"|"+") -> true - | _ -> false - -let is_prefix op = List.mem L (fixity op) -let is_infix op = List.mem N (fixity op) -let is_postfix op = List.mem R (fixity op) - -let mk_inf op t1 t2 = - if not (is_infix op) then failwith (op^" not infix"); - Infix(op,t1,t2) - -let mk_post op t = - if not (is_postfix op) then failwith (op^" not postfix"); - Postfix(op,t) - - -(* Pb avec ground_oper: pas de diff entre -1 et -(1) *) -let mk_pre op t = - if not (is_prefix op) then failwith (op^" not prefix"); - if ground_oper op then - match t with - | Int i -> Int (op^i) - | _ -> Prefix(op,t) - else Prefix(op,t) - -(* teste si on peut reduire op suivi d'un op de niveau (n,a) - si la reponse est false, c'est que l'op (n,a) doit se reduire - avant *) -let red_left_op (nl,al) (nr,ar) = - if nl < nr then true - else - if nl = nr then - match al,ar with - | (L|N), L -> true - | R, (R|N) -> false - | R, L -> failwith "conflit d'assoc: ambigu" - | (L|N), (R|N) -> failwith "conflit d'assoc: blocage" - else false - - -type level = int * assoc -type stack = - | PrefixOper of string list - | Term of constr_ast * stack - | Oper of string list * string * constr_ast * stack - -let rec str_ast = function - | Infix(op,t1,t2) -> str_ast t1 ^ " " ^ op ^ " " ^ str_ast t2 - | Postfix(op,t) -> str_ast t ^ " " ^ op - | Prefix(op,t) -> op ^ " " ^ str_ast t - | _ -> "_" - -let rec str_stack = function - | PrefixOper ops -> String.concat " " (List.rev ops) - | Term (t,s) -> str_stack s ^ " (" ^ str_ast t ^ ")" - | Oper(ops,lop,t,s) -> - str_stack (Term(t,s)) ^ " " ^ lop ^ " " ^ - String.concat " " (List.rev ops) - -let pps s = prerr_endline (str_stack s) -let err s stk = failwith (s^": "^str_stack stk) - - -let empty = PrefixOper [] - -let check_fixity_term stk = - match stk with - Term _ -> err "2 termes successifs" stk - | _ -> () - -let shift_term t stk = - check_fixity_term stk; - Term(t,stk) - -let shift_oper op stk = - match stk with - | Oper(ops,lop,t,s) -> Oper(op::ops,lop,t,s) - | Term(t,s) -> Oper([],op,t,s) - | PrefixOper ops -> PrefixOper (op::ops) - -let is_reducible lv stk = - match stk with - | Oper([],iop,_,_) -> red_left_op (level iop) lv - | Oper(op::_,_,_,_) -> red_left_op (level op) lv - | PrefixOper(op::_) -> red_left_op (level op) lv - | _ -> false - -let reduce_head (t,stk) = - match stk with - | Oper([],iop,t1,s) -> - (Infix(iop,t1,t), s) - | Oper(op::ops,lop,t',s) -> - (mk_pre op t, Oper(ops,lop,t',s)) - | PrefixOper(op::ops) -> - (Prefix(op,t), PrefixOper ops) - | _ -> assert false - -let rec reduce_level lv (t,s) = - if is_reducible lv s then reduce_level lv (reduce_head (t, s)) - else (t, s) - -let reduce_post op (t,s) = - let (t',s') = reduce_level (level op) (t,s) in - (mk_post op t', s') - -let reduce_posts stk = - match stk with - Oper(ops,iop,t,s) -> - let pts1 = reduce_post iop (t,s) in - List.fold_right reduce_post ops pts1 - | Term(t,s) -> (t,s) - | PrefixOper _ -> failwith "reduce_posts" - - -let shift_infix op stk = - let (t,s) = reduce_level (level op) (reduce_posts stk) in - Oper([],op,t,s) - -let is_better_infix op stk = - match stk with - | Oper(ops,iop,t,s) -> - is_postfix iop && - List.for_all is_postfix ops && - (not (is_prefix op) || red_left_op (level iop) (level op)) - | Term _ -> false - | _ -> assert false - -let parse_oper op stk = - match stk with - | PrefixOper _ -> - if is_prefix op then shift_oper op stk else failwith "prefix_oper" - | Oper _ -> - if is_infix op then - if is_better_infix op stk then shift_infix op stk - else shift_oper op stk - else if is_prefix op then shift_oper op stk - else if is_postfix op then - let (t,s) = reduce_post op (reduce_posts stk) in - Term(t,s) - else assert false - | Term(t,s) -> - if is_infix op then shift_infix op stk - else if is_postfix op then - let (t2,s2) = reduce_post op (t,s) in Term(t2,s2) - else failwith "infix/postfix" - -let parse_term = shift_term - -let rec close_stack stk = - match stk with - Term(t,PrefixOper []) -> t - | PrefixOper _ -> failwith "expression sans atomes" - | _ -> - let (t,s) = reduce_head (reduce_posts stk) in - close_stack (Term(t,s)) - diff --git a/dev/ocamlweb-doc/parsing.dep.ps b/dev/ocamlweb-doc/parsing.dep.ps deleted file mode 100644 index 723d8c69..00000000 --- a/dev/ocamlweb-doc/parsing.dep.ps +++ /dev/null @@ -1,1115 +0,0 @@ -%!PS-Adobe-2.0 -%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) -%%For: (herbelin) Hugo Herbelin -%%Title: G -%%Pages: (atend) -%%BoundingBox: 35 35 577 314 -%%EndComments -save -%%BeginProlog -/DotDict 200 dict def -DotDict begin - -/setupLatin1 { -mark -/EncodingVector 256 array def - EncodingVector 0 - -ISOLatin1Encoding 0 255 getinterval putinterval - -EncodingVector - dup 306 /AE - dup 301 /Aacute - dup 302 /Acircumflex - dup 304 /Adieresis - dup 300 /Agrave - dup 305 /Aring - dup 303 /Atilde - dup 307 /Ccedilla - dup 311 /Eacute - dup 312 /Ecircumflex - dup 313 /Edieresis - dup 310 /Egrave - dup 315 /Iacute - dup 316 /Icircumflex - dup 317 /Idieresis - dup 314 /Igrave - dup 334 /Udieresis - dup 335 /Yacute - dup 376 /thorn - dup 337 /germandbls - dup 341 /aacute - dup 342 /acircumflex - dup 344 /adieresis - dup 346 /ae - dup 340 /agrave - dup 345 /aring - dup 347 /ccedilla - dup 351 /eacute - dup 352 /ecircumflex - dup 353 /edieresis - dup 350 /egrave - dup 355 /iacute - dup 356 /icircumflex - dup 357 /idieresis - dup 354 /igrave - dup 360 /dcroat - dup 361 /ntilde - dup 363 /oacute - dup 364 /ocircumflex - dup 366 /odieresis - dup 362 /ograve - dup 365 /otilde - dup 370 /oslash - dup 372 /uacute - dup 373 /ucircumflex - dup 374 /udieresis - dup 371 /ugrave - dup 375 /yacute - dup 377 /ydieresis - -% Set up ISO Latin 1 character encoding -/starnetISO { - dup dup findfont dup length dict begin - { 1 index /FID ne { def }{ pop pop } ifelse - } forall - /Encoding EncodingVector def - currentdict end definefont -} def -/Times-Roman starnetISO def -/Times-Italic starnetISO def -/Times-Bold starnetISO def -/Times-BoldItalic starnetISO def -/Helvetica starnetISO def -/Helvetica-Oblique starnetISO def -/Helvetica-Bold starnetISO def -/Helvetica-BoldOblique starnetISO def -/Courier starnetISO def -/Courier-Oblique starnetISO def -/Courier-Bold starnetISO def -/Courier-BoldOblique starnetISO def -cleartomark -} bind def - -%%BeginResource: procset graphviz 0 0 -/coord-font-family /Times-Roman def -/default-font-family /Times-Roman def -/coordfont coord-font-family findfont 8 scalefont def - -/InvScaleFactor 1.0 def -/set_scale { - dup 1 exch div /InvScaleFactor exch def - dup scale -} bind def - -% styles -/solid { [] 0 setdash } bind def -/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def -/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def -/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def -/bold { 2 setlinewidth } bind def -/filled { } bind def -/unfilled { } bind def -/rounded { } bind def -/diagonals { } bind def - -% hooks for setting color -/nodecolor { sethsbcolor } bind def -/edgecolor { sethsbcolor } bind def -/graphcolor { sethsbcolor } bind def -/nopcolor {pop pop pop} bind def - -/beginpage { % i j npages - /npages exch def - /j exch def - /i exch def - /str 10 string def - npages 1 gt { - gsave - coordfont setfont - 0 0 moveto - (\() show i str cvs show (,) show j str cvs show (\)) show - grestore - } if -} bind def - -/set_font { - findfont exch - scalefont setfont -} def - -% draw aligned label in bounding box aligned to current point -/alignedtext { % width adj text - /text exch def - /adj exch def - /width exch def - gsave - width 0 gt { - text stringwidth pop adj mul 0 rmoveto - } if - [] 0 setdash - text show - grestore -} def - -/boxprim { % xcorner ycorner xsize ysize - 4 2 roll - moveto - 2 copy - exch 0 rlineto - 0 exch rlineto - pop neg 0 rlineto - closepath -} bind def - -/ellipse_path { - /ry exch def - /rx exch def - /y exch def - /x exch def - matrix currentmatrix - newpath - x y translate - rx ry scale - 0 0 1 0 360 arc - setmatrix -} bind def - -/endpage { showpage } bind def -/showpage { } def - -/layercolorseq - [ % layer color sequence - darkest to lightest - [0 0 0] - [.2 .8 .8] - [.4 .8 .8] - [.6 .8 .8] - [.8 .8 .8] - ] -def - -/layerlen layercolorseq length def - -/setlayer {/maxlayer exch def /curlayer exch def - layercolorseq curlayer 1 sub layerlen mod get - aload pop sethsbcolor - /nodecolor {nopcolor} def - /edgecolor {nopcolor} def - /graphcolor {nopcolor} def -} bind def - -/onlayer { curlayer ne {invis} if } def - -/onlayers { - /myupper exch def - /mylower exch def - curlayer mylower lt - curlayer myupper gt - or - {invis} if -} def - -/curlayer 0 def - -%%EndResource -%%EndProlog -%%BeginSetup -14 default-font-family set_font -1 setmiterlimit -% /arrowlength 10 def -% /arrowwidth 5 def - -% make sure pdfmark is harmless for PS-interpreters other than Distiller -/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse -% make '<<' and '>>' safe on PS Level 1 devices -/languagelevel where {pop languagelevel}{1} ifelse -2 lt { - userdict (<<) cvn ([) cvn load put - userdict (>>) cvn ([) cvn load put -} if - -%%EndSetup -%%Page: 1 1 -%%PageBoundingBox: 36 36 577 314 -%%PageOrientation: Portrait -gsave -35 35 542 279 boxprim clip newpath -36 36 translate -0 0 1 beginpage -0.6027 set_scale -0 0 translate 0 rotate -0.000 0.000 0.000 graphcolor -14.00 /Times-Roman set_font - -% Pcoq -gsave 10 dict begin -557 280 27 18 ellipse_path -stroke -gsave 10 dict begin -543 275 moveto -(Pcoq) -[7.68 6.24 6.96 6.96] -xshow -end grestore -end grestore - -% Extend -gsave 10 dict begin -664 226 33 18 ellipse_path -stroke -gsave 10 dict begin -643 221 moveto -(Extend) -[8.4 6.96 3.84 6.24 6.96 6.96] -xshow -end grestore -end grestore - -% Pcoq -> Extend -newpath 579 269 moveto -593 261 613 252 630 243 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 632 246 moveto -639 238 lineto -629 240 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 632 246 moveto -639 238 lineto -629 240 lineto -closepath -stroke -end grestore - -% Ast -gsave 10 dict begin -764 172 27 18 ellipse_path -stroke -gsave 10 dict begin -753 167 moveto -(Ast) -[10.08 5.28 3.84] -xshow -end grestore -end grestore - -% Extend -> Ast -newpath 688 213 moveto -701 206 719 196 734 188 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 736 191 moveto -743 183 lineto -733 185 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 736 191 moveto -743 183 lineto -733 185 lineto -closepath -stroke -end grestore - -% Lexer -gsave 10 dict begin -764 226 29 18 ellipse_path -stroke -gsave 10 dict begin -747 221 moveto -(Lexer) -[8.4 5.76 6.48 6.24 4.56] -xshow -end grestore -end grestore - -% Extend -> Lexer -newpath 698 226 moveto -706 226 715 226 724 226 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 724 230 moveto -734 226 lineto -724 223 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 724 230 moveto -734 226 lineto -724 223 lineto -closepath -stroke -end grestore - -% Termast -gsave 10 dict begin -557 172 35 18 ellipse_path -stroke -gsave 10 dict begin -534 167 moveto -(Termast) -[7.2 6.24 4.8 10.8 6.24 5.28 3.84] -xshow -end grestore -end grestore - -% Termast -> Ast -newpath 593 172 moveto -630 172 689 172 727 172 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 727 176 moveto -737 172 lineto -727 169 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 727 176 moveto -737 172 lineto -727 169 lineto -closepath -stroke -end grestore - -% Coqast -gsave 10 dict begin -863 172 32 18 ellipse_path -stroke -gsave 10 dict begin -843 167 moveto -(Coqast) -[9.36 6.96 6.96 6.24 5.28 3.84] -xshow -end grestore -end grestore - -% Ast -> Coqast -newpath 791 172 moveto -800 172 810 172 820 172 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 820 176 moveto -830 172 lineto -820 169 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 820 176 moveto -830 172 lineto -820 169 lineto -closepath -stroke -end grestore - -% Tactic_printer -gsave 10 dict begin -53 126 52 18 ellipse_path -stroke -gsave 10 dict begin -13 121 moveto -(Tactic_printer) -[7.44 6.24 6.24 3.84 3.84 6.24 6.96 6.96 4.8 3.84 6.96 3.84 6.24 4.56] -xshow -end grestore -end grestore - -% Pptactic -gsave 10 dict begin -178 126 36 18 ellipse_path -stroke -gsave 10 dict begin -155 121 moveto -(Pptactic) -[7.68 6.96 4.08 6.24 6.24 3.84 3.84 6.24] -xshow -end grestore -end grestore - -% Tactic_printer -> Pptactic -newpath 106 126 moveto -114 126 123 126 132 126 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 132 130 moveto -142 126 lineto -132 123 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 132 130 moveto -142 126 lineto -132 123 lineto -closepath -stroke -end grestore - -% Printer -gsave 10 dict begin -289 72 32 18 ellipse_path -stroke -gsave 10 dict begin -269 67 moveto -(Printer) -[7.68 4.8 3.84 6.96 3.84 6.24 4.56] -xshow -end grestore -end grestore - -% Pptactic -> Printer -newpath 204 113 moveto -219 105 238 96 255 88 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 256 91 moveto -264 84 lineto -253 85 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 256 91 moveto -264 84 lineto -253 85 lineto -closepath -stroke -end grestore - -% Search -gsave 10 dict begin -178 72 32 18 ellipse_path -stroke -gsave 10 dict begin -159 67 moveto -(Search) -[7.68 6.24 6.24 4.56 6 6.96] -xshow -end grestore -end grestore - -% Search -> Printer -newpath 210 72 moveto -221 72 234 72 246 72 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 246 76 moveto -256 72 lineto -246 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 246 76 moveto -256 72 lineto -246 69 lineto -closepath -stroke -end grestore - -% Printer -> Termast -newpath 316 62 moveto -355 48 430 30 484 58 curveto -518 77 538 117 548 144 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 545 146 moveto -552 154 lineto -552 143 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 545 146 moveto -552 154 lineto -552 143 lineto -closepath -stroke -end grestore - -% Esyntax -gsave 10 dict begin -557 226 36 18 ellipse_path -stroke -gsave 10 dict begin -533 221 moveto -(Esyntax) -[8.4 5.52 6.96 6.96 4.08 6.24 6.96] -xshow -end grestore -end grestore - -% Printer -> Esyntax -newpath 322 71 moveto -370 70 460 72 484 91 curveto -489 95 516 193 520 197 curveto -527 204 532 203 538 204 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 536 207 moveto -547 208 lineto -539 201 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 536 207 moveto -547 208 lineto -539 201 lineto -closepath -stroke -end grestore - -% Ppconstr -gsave 10 dict begin -424 388 37 18 ellipse_path -stroke -gsave 10 dict begin -399 383 moveto -(Ppconstr) -[7.68 6.96 6.24 6.96 6.96 5.28 3.84 4.56] -xshow -end grestore -end grestore - -% Printer -> Ppconstr -newpath 292 90 moveto -300 147 329 319 364 361 curveto -369 367 375 371 382 375 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 380 378 moveto -391 379 lineto -383 372 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 380 378 moveto -391 379 lineto -383 372 lineto -closepath -stroke -end grestore - -% Esyntax -> Extend -newpath 594 226 moveto -602 226 611 226 620 226 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 620 230 moveto -630 226 lineto -620 223 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 620 230 moveto -630 226 lineto -620 223 lineto -closepath -stroke -end grestore - -% Ppconstr -> Pcoq -newpath 454 377 moveto -464 373 475 368 484 361 curveto -506 345 526 322 540 304 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 543 306 moveto -546 296 lineto -537 302 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 543 306 moveto -546 296 lineto -537 302 lineto -closepath -stroke -end grestore - -% Prettyp -gsave 10 dict begin -178 18 33 18 ellipse_path -stroke -gsave 10 dict begin -158 13 moveto -(Prettyp) -[7.68 4.56 6 3.84 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Prettyp -> Printer -newpath 203 30 moveto -218 38 238 47 255 55 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 254 58 moveto -264 60 lineto -257 52 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 254 58 moveto -264 60 lineto -257 52 lineto -closepath -stroke -end grestore - -% Printmod -gsave 10 dict begin -289 18 39 18 ellipse_path -stroke -gsave 10 dict begin -263 13 moveto -(Printmod) -[7.68 4.8 3.84 6.96 3.84 10.8 6.96 6.96] -xshow -end grestore -end grestore - -% Prettyp -> Printmod -newpath 211 18 moveto -220 18 230 18 240 18 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 240 22 moveto -250 18 lineto -240 15 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 240 22 moveto -250 18 lineto -240 15 lineto -closepath -stroke -end grestore - -% G_zsyntax -gsave 10 dict begin -424 172 43 18 ellipse_path -stroke -gsave 10 dict begin -393 167 moveto -(G_zsyntax) -[10.08 6.96 6.24 5.52 6.96 6.96 4.08 6.24 6.96] -xshow -end grestore -end grestore - -% G_zsyntax -> Pcoq -newpath 458 183 moveto -467 188 476 193 484 199 curveto -507 218 501 233 520 253 curveto -523 256 526 259 530 261 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 528 264 moveto -538 267 lineto -532 258 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 528 264 moveto -538 267 lineto -532 258 lineto -closepath -stroke -end grestore - -% G_zsyntax -> Termast -newpath 468 172 moveto -482 172 497 172 511 172 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 511 176 moveto -521 172 lineto -511 169 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 511 176 moveto -521 172 lineto -511 169 lineto -closepath -stroke -end grestore - -% G_zsyntax -> Esyntax -newpath 455 185 moveto -474 193 499 203 520 211 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 518 214 moveto -529 215 lineto -521 208 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 518 214 moveto -529 215 lineto -521 208 lineto -closepath -stroke -end grestore - -% G_string_syntax -gsave 10 dict begin -424 280 59 18 ellipse_path -stroke -gsave 10 dict begin -377 275 moveto -(G_string_syntax) -[10.08 6.96 5.28 3.84 4.8 3.84 6.96 6.96 6.96 5.52 6.96 6.96 4.08 6.24 6.96] -xshow -end grestore -end grestore - -% G_string_syntax -> Pcoq -newpath 484 280 moveto -496 280 509 280 520 280 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 520 284 moveto -530 280 lineto -520 277 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 520 284 moveto -530 280 lineto -520 277 lineto -closepath -stroke -end grestore - -% G_string_syntax -> Esyntax -newpath 460 266 moveto -478 258 501 249 520 242 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 521 245 moveto -529 238 lineto -518 239 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 521 245 moveto -529 238 lineto -518 239 lineto -closepath -stroke -end grestore - -% G_rsyntax -gsave 10 dict begin -424 118 42 18 ellipse_path -stroke -gsave 10 dict begin -394 113 moveto -(G_rsyntax) -[10.08 6.96 4.56 5.52 6.96 6.96 4.08 6.24 6.96] -xshow -end grestore -end grestore - -% G_rsyntax -> Pcoq -newpath 459 128 moveto -468 132 477 138 484 145 curveto -518 183 491 213 520 253 curveto -523 256 526 259 529 262 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 527 265 moveto -537 268 lineto -531 259 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 527 265 moveto -537 268 lineto -531 259 lineto -closepath -stroke -end grestore - -% G_rsyntax -> Termast -newpath 455 131 moveto -474 139 499 149 520 157 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 518 160 moveto -529 161 lineto -521 154 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 518 160 moveto -529 161 lineto -521 154 lineto -closepath -stroke -end grestore - -% G_rsyntax -> Esyntax -newpath 457 129 moveto -467 133 476 139 484 145 curveto -507 164 501 179 520 199 curveto -522 201 525 203 527 205 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 525 208 moveto -535 212 lineto -530 203 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 525 208 moveto -535 212 lineto -530 203 lineto -closepath -stroke -end grestore - -% G_natsyntax -gsave 10 dict begin -424 226 48 18 ellipse_path -stroke -gsave 10 dict begin -388 221 moveto -(G_natsyntax) -[10.08 6.96 6.96 6.24 3.84 5.52 6.96 6.96 4.08 6.24 6.96] -xshow -end grestore -end grestore - -% G_natsyntax -> Pcoq -newpath 457 239 moveto -478 248 504 259 525 266 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 523 269 moveto -534 270 lineto -526 263 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 523 269 moveto -534 270 lineto -526 263 lineto -closepath -stroke -end grestore - -% G_natsyntax -> Termast -newpath 457 213 moveto -476 205 500 195 520 187 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 521 190 moveto -529 183 lineto -518 184 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 521 190 moveto -529 183 lineto -518 184 lineto -closepath -stroke -end grestore - -% G_natsyntax -> Esyntax -newpath 473 226 moveto -485 226 498 226 510 226 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 510 230 moveto -520 226 lineto -510 223 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 510 230 moveto -520 226 lineto -510 223 lineto -closepath -stroke -end grestore - -% G_ascii_syntax -gsave 10 dict begin -424 334 56 18 ellipse_path -stroke -gsave 10 dict begin -380 329 moveto -(G_ascii_syntax) -[10.08 6.96 6.24 5.52 6.24 3.84 3.84 6.96 5.52 6.96 6.96 4.08 6.24 6.96] -xshow -end grestore -end grestore - -% G_ascii_syntax -> Pcoq -newpath 459 320 moveto -479 311 504 301 525 293 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 526 296 moveto -534 289 lineto -523 290 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 526 296 moveto -534 289 lineto -523 290 lineto -closepath -stroke -end grestore - -% G_ascii_syntax -> Esyntax -newpath 462 321 moveto -470 317 478 312 484 307 curveto -507 288 501 273 520 253 curveto -522 251 524 249 527 247 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 529 250 moveto -535 241 lineto -525 244 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 529 250 moveto -535 241 lineto -525 244 lineto -closepath -stroke -end grestore - -% Egrammar -gsave 10 dict begin -424 442 43 18 ellipse_path -stroke -gsave 10 dict begin -394 437 moveto -(Egrammar) -[8.4 7.2 4.56 6.24 10.8 10.8 6.24 4.56] -xshow -end grestore -end grestore - -% Egrammar -> Pcoq -newpath 458 431 moveto -467 427 477 422 484 415 curveto -516 385 537 337 548 308 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 551 309 moveto -551 298 lineto -545 307 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 551 309 moveto -551 298 lineto -545 307 lineto -closepath -stroke -end grestore -endpage -showpage -grestore -%%PageTrailer -%%EndPage: 1 -%%Trailer -%%Pages: 1 -end -restore -%%EOF diff --git a/dev/ocamlweb-doc/preamble.tex b/dev/ocamlweb-doc/preamble.tex deleted file mode 100644 index 2cd21f02..00000000 --- a/dev/ocamlweb-doc/preamble.tex +++ /dev/null @@ -1,8 +0,0 @@ -\documentclass[11pt]{article} -\usepackage[latin1]{inputenc} -\usepackage[T1]{fontenc} -\usepackage{ocamlweb} -\pagestyle{ocamlweb} -\usepackage{fullpage} -\usepackage{epsfig} -\begin{document} diff --git a/dev/ocamlweb-doc/pretyping.dep.ps b/dev/ocamlweb-doc/pretyping.dep.ps deleted file mode 100644 index 02d1b8b5..00000000 --- a/dev/ocamlweb-doc/pretyping.dep.ps +++ /dev/null @@ -1,1259 +0,0 @@ -%!PS-Adobe-2.0 -%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) -%%For: (herbelin) Hugo Herbelin -%%Title: G -%%Pages: (atend) -%%BoundingBox: 35 35 577 146 -%%EndComments -save -%%BeginProlog -/DotDict 200 dict def -DotDict begin - -/setupLatin1 { -mark -/EncodingVector 256 array def - EncodingVector 0 - -ISOLatin1Encoding 0 255 getinterval putinterval - -EncodingVector - dup 306 /AE - dup 301 /Aacute - dup 302 /Acircumflex - dup 304 /Adieresis - dup 300 /Agrave - dup 305 /Aring - dup 303 /Atilde - dup 307 /Ccedilla - dup 311 /Eacute - dup 312 /Ecircumflex - dup 313 /Edieresis - dup 310 /Egrave - dup 315 /Iacute - dup 316 /Icircumflex - dup 317 /Idieresis - dup 314 /Igrave - dup 334 /Udieresis - dup 335 /Yacute - dup 376 /thorn - dup 337 /germandbls - dup 341 /aacute - dup 342 /acircumflex - dup 344 /adieresis - dup 346 /ae - dup 340 /agrave - dup 345 /aring - dup 347 /ccedilla - dup 351 /eacute - dup 352 /ecircumflex - dup 353 /edieresis - dup 350 /egrave - dup 355 /iacute - dup 356 /icircumflex - dup 357 /idieresis - dup 354 /igrave - dup 360 /dcroat - dup 361 /ntilde - dup 363 /oacute - dup 364 /ocircumflex - dup 366 /odieresis - dup 362 /ograve - dup 365 /otilde - dup 370 /oslash - dup 372 /uacute - dup 373 /ucircumflex - dup 374 /udieresis - dup 371 /ugrave - dup 375 /yacute - dup 377 /ydieresis - -% Set up ISO Latin 1 character encoding -/starnetISO { - dup dup findfont dup length dict begin - { 1 index /FID ne { def }{ pop pop } ifelse - } forall - /Encoding EncodingVector def - currentdict end definefont -} def -/Times-Roman starnetISO def -/Times-Italic starnetISO def -/Times-Bold starnetISO def -/Times-BoldItalic starnetISO def -/Helvetica starnetISO def -/Helvetica-Oblique starnetISO def -/Helvetica-Bold starnetISO def -/Helvetica-BoldOblique starnetISO def -/Courier starnetISO def -/Courier-Oblique starnetISO def -/Courier-Bold starnetISO def -/Courier-BoldOblique starnetISO def -cleartomark -} bind def - -%%BeginResource: procset graphviz 0 0 -/coord-font-family /Times-Roman def -/default-font-family /Times-Roman def -/coordfont coord-font-family findfont 8 scalefont def - -/InvScaleFactor 1.0 def -/set_scale { - dup 1 exch div /InvScaleFactor exch def - dup scale -} bind def - -% styles -/solid { [] 0 setdash } bind def -/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def -/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def -/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def -/bold { 2 setlinewidth } bind def -/filled { } bind def -/unfilled { } bind def -/rounded { } bind def -/diagonals { } bind def - -% hooks for setting color -/nodecolor { sethsbcolor } bind def -/edgecolor { sethsbcolor } bind def -/graphcolor { sethsbcolor } bind def -/nopcolor {pop pop pop} bind def - -/beginpage { % i j npages - /npages exch def - /j exch def - /i exch def - /str 10 string def - npages 1 gt { - gsave - coordfont setfont - 0 0 moveto - (\() show i str cvs show (,) show j str cvs show (\)) show - grestore - } if -} bind def - -/set_font { - findfont exch - scalefont setfont -} def - -% draw aligned label in bounding box aligned to current point -/alignedtext { % width adj text - /text exch def - /adj exch def - /width exch def - gsave - width 0 gt { - text stringwidth pop adj mul 0 rmoveto - } if - [] 0 setdash - text show - grestore -} def - -/boxprim { % xcorner ycorner xsize ysize - 4 2 roll - moveto - 2 copy - exch 0 rlineto - 0 exch rlineto - pop neg 0 rlineto - closepath -} bind def - -/ellipse_path { - /ry exch def - /rx exch def - /y exch def - /x exch def - matrix currentmatrix - newpath - x y translate - rx ry scale - 0 0 1 0 360 arc - setmatrix -} bind def - -/endpage { showpage } bind def -/showpage { } def - -/layercolorseq - [ % layer color sequence - darkest to lightest - [0 0 0] - [.2 .8 .8] - [.4 .8 .8] - [.6 .8 .8] - [.8 .8 .8] - ] -def - -/layerlen layercolorseq length def - -/setlayer {/maxlayer exch def /curlayer exch def - layercolorseq curlayer 1 sub layerlen mod get - aload pop sethsbcolor - /nodecolor {nopcolor} def - /edgecolor {nopcolor} def - /graphcolor {nopcolor} def -} bind def - -/onlayer { curlayer ne {invis} if } def - -/onlayers { - /myupper exch def - /mylower exch def - curlayer mylower lt - curlayer myupper gt - or - {invis} if -} def - -/curlayer 0 def - -%%EndResource -%%EndProlog -%%BeginSetup -14 default-font-family set_font -1 setmiterlimit -% /arrowlength 10 def -% /arrowwidth 5 def - -% make sure pdfmark is harmless for PS-interpreters other than Distiller -/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse -% make '<<' and '>>' safe on PS Level 1 devices -/languagelevel where {pop languagelevel}{1} ifelse -2 lt { - userdict (<<) cvn ([) cvn load put - userdict (>>) cvn ([) cvn load put -} if - -%%EndSetup -%%Page: 1 1 -%%PageBoundingBox: 36 36 577 146 -%%PageOrientation: Portrait -gsave -35 35 542 111 boxprim clip newpath -36 36 translate -0 0 1 beginpage -0.3600 set_scale -0 0 translate 0 rotate -0.000 0.000 0.000 graphcolor -14.00 /Times-Roman set_font - -% Unification -gsave 10 dict begin -610 118 45 18 ellipse_path -stroke -gsave 10 dict begin -577 113 moveto -(Unification) -[9.6 6.96 3.84 4.8 3.84 6.24 6.24 3.84 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Evarutil -gsave 10 dict begin -728 72 36 18 ellipse_path -stroke -gsave 10 dict begin -705 67 moveto -(Evarutil) -[8.4 6.72 6.24 4.8 6.96 3.84 3.84 3.84] -xshow -end grestore -end grestore - -% Unification -> Evarutil -newpath 643 105 moveto -657 99 674 93 689 87 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 691 90 moveto -699 83 lineto -688 83 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 691 90 moveto -699 83 lineto -688 83 lineto -closepath -stroke -end grestore - -% Pattern -gsave 10 dict begin -728 210 33 18 ellipse_path -stroke -gsave 10 dict begin -708 205 moveto -(Pattern) -[7.44 6.24 3.84 3.84 6.24 4.8 6.96] -xshow -end grestore -end grestore - -% Unification -> Pattern -newpath 631 134 moveto -650 150 680 173 701 189 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 699 192 moveto -709 195 lineto -703 186 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 699 192 moveto -709 195 lineto -703 186 lineto -closepath -stroke -end grestore - -% Retyping -gsave 10 dict begin -839 118 38 18 ellipse_path -stroke -gsave 10 dict begin -813 113 moveto -(Retyping) -[9.12 6 3.84 6.96 6.96 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Unification -> Retyping -newpath 656 118 moveto -695 118 750 118 790 118 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 790 122 moveto -800 118 lineto -790 115 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 790 122 moveto -800 118 lineto -790 115 lineto -closepath -stroke -end grestore - -% Typing -gsave 10 dict begin -839 64 32 18 ellipse_path -stroke -gsave 10 dict begin -819 59 moveto -(Typing) -[6.96 6.96 6.96 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Evarutil -> Typing -newpath 764 69 moveto -775 68 786 67 797 67 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 797 70 moveto -807 66 lineto -797 64 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 797 70 moveto -807 66 lineto -797 64 lineto -closepath -stroke -end grestore - -% Rawterm -gsave 10 dict begin -1109 110 39 18 ellipse_path -stroke -gsave 10 dict begin -1083 105 moveto -(Rawterm) -[9.36 5.76 10.08 3.84 6.24 4.8 10.8] -xshow -end grestore -end grestore - -% Pattern -> Rawterm -newpath 759 216 moveto -816 226 939 239 1024 191 curveto -1049 176 1038 155 1060 138 curveto -1069 131 1077 130 1084 129 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1085 132 moveto -1094 127 lineto -1084 126 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1085 132 moveto -1094 127 lineto -1084 126 lineto -closepath -stroke -end grestore - -% Inductiveops -gsave 10 dict begin -1109 164 49 18 ellipse_path -stroke -gsave 10 dict begin -1073 159 moveto -(Inductiveops) -[4.56 6.96 6.96 6.96 6.24 3.84 3.84 6.48 6.24 6.96 6.96 5.52] -xshow -end grestore -end grestore - -% Retyping -> Inductiveops -newpath 878 120 moveto -915 122 974 126 1024 137 curveto -1037 139 1051 144 1064 148 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1063 151 moveto -1074 151 lineto -1065 145 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1063 151 moveto -1074 151 lineto -1065 145 lineto -closepath -stroke -end grestore - -% Pretype_errors -gsave 10 dict begin -969 72 54 18 ellipse_path -stroke -gsave 10 dict begin -927 67 moveto -(Pretype_errors) -[7.68 4.56 6 3.84 6.96 6.96 6.24 6.96 6.24 5.04 4.56 6.96 4.56 5.52] -xshow -end grestore -end grestore - -% Typing -> Pretype_errors -newpath 871 66 moveto -881 67 893 68 905 68 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 905 71 moveto -915 69 lineto -905 65 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 905 71 moveto -915 69 lineto -905 65 lineto -closepath -stroke -end grestore - -% Pretype_errors -> Inductiveops -newpath 998 87 moveto -1007 92 1016 98 1024 104 curveto -1042 116 1043 124 1060 137 curveto -1063 139 1067 142 1071 144 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1070 147 moveto -1080 149 lineto -1073 141 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1070 147 moveto -1080 149 lineto -1073 141 lineto -closepath -stroke -end grestore - -% Pretype_errors -> Rawterm -newpath 1011 84 moveto -1029 88 1048 94 1065 98 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1064 101 moveto -1075 101 lineto -1066 95 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1064 101 moveto -1075 101 lineto -1066 95 lineto -closepath -stroke -end grestore - -% Tacred -gsave 10 dict begin -728 18 32 18 ellipse_path -stroke -gsave 10 dict begin -709 13 moveto -(Tacred) -[7.44 6.24 6.24 4.56 6.24 6.96] -xshow -end grestore -end grestore - -% Tacred -> Retyping -newpath 748 32 moveto -754 36 759 41 764 45 curveto -783 63 782 73 800 91 curveto -802 93 805 95 808 97 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 806 100 moveto -816 103 lineto -810 94 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 806 100 moveto -816 103 lineto -810 94 lineto -closepath -stroke -end grestore - -% Tacred -> Typing -newpath 754 29 moveto -769 35 787 43 803 49 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 802 53 moveto -813 53 lineto -805 46 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 802 53 moveto -813 53 lineto -805 46 lineto -closepath -stroke -end grestore - -% Cbv -gsave 10 dict begin -1246 41 27 18 ellipse_path -stroke -gsave 10 dict begin -1234 36 moveto -(Cbv) -[9.36 6.48 6.96] -xshow -end grestore -end grestore - -% Tacred -> Cbv -newpath 760 19 moveto -852 23 1111 35 1209 40 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1209 44 moveto -1219 40 lineto -1209 37 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1209 44 moveto -1219 40 lineto -1209 37 lineto -closepath -stroke -end grestore - -% Evd -gsave 10 dict begin -1361 110 27 18 ellipse_path -stroke -gsave 10 dict begin -1349 105 moveto -(Evd) -[8.4 6.96 6.96] -xshow -end grestore -end grestore - -% Cbv -> Evd -newpath 1266 53 moveto -1284 64 1312 80 1332 93 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1331 96 moveto -1341 98 lineto -1334 90 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1331 96 moveto -1341 98 lineto -1334 90 lineto -closepath -stroke -end grestore - -% Reductionops -gsave 10 dict begin -1246 164 51 18 ellipse_path -stroke -gsave 10 dict begin -1207 159 moveto -(Reductionops) -[9.12 6.24 6.96 6.96 6.24 3.84 3.84 6.96 6.96 6.96 6.96 5.52] -xshow -end grestore -end grestore - -% Inductiveops -> Reductionops -newpath 1158 164 moveto -1167 164 1175 164 1184 164 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1184 168 moveto -1194 164 lineto -1184 161 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1184 168 moveto -1194 164 lineto -1184 161 lineto -closepath -stroke -end grestore - -% Reductionops -> Evd -newpath 1277 150 moveto -1294 142 1313 133 1330 125 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1331 128 moveto -1339 121 lineto -1328 122 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1331 128 moveto -1339 121 lineto -1328 122 lineto -closepath -stroke -end grestore - -% Termops -gsave 10 dict begin -1462 110 37 18 ellipse_path -stroke -gsave 10 dict begin -1437 105 moveto -(Termops) -[7.2 6.24 4.8 10.8 6.96 6.96 5.52] -xshow -end grestore -end grestore - -% Evd -> Termops -newpath 1388 110 moveto -1396 110 1405 110 1414 110 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1414 114 moveto -1424 110 lineto -1414 107 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1414 114 moveto -1424 110 lineto -1414 107 lineto -closepath -stroke -end grestore - -% Recordops -gsave 10 dict begin -485 24 43 18 ellipse_path -stroke -gsave 10 dict begin -455 19 moveto -(Recordops) -[9.12 6.24 6.24 6.96 4.32 6.96 6.96 6.96 5.52] -xshow -end grestore -end grestore - -% Classops -gsave 10 dict begin -610 20 38 18 ellipse_path -stroke -gsave 10 dict begin -584 15 moveto -(Classops) -[9.36 3.84 6.24 5.52 5.52 6.96 6.96 5.52] -xshow -end grestore -end grestore - -% Recordops -> Classops -newpath 528 23 moveto -538 22 550 22 561 22 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 561 25 moveto -571 21 lineto -561 19 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 561 25 moveto -571 21 lineto -561 19 lineto -closepath -stroke -end grestore - -% Classops -> Tacred -newpath 649 19 moveto -661 19 674 19 686 19 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 686 23 moveto -696 19 lineto -686 16 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 686 23 moveto -696 19 lineto -686 16 lineto -closepath -stroke -end grestore - -% Rawterm -> Evd -newpath 1148 110 moveto -1196 110 1277 110 1324 110 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1324 114 moveto -1334 110 lineto -1324 107 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1324 114 moveto -1334 110 lineto -1324 107 lineto -closepath -stroke -end grestore - -% Pretyping -gsave 10 dict begin -40 183 40 18 ellipse_path -stroke -gsave 10 dict begin -13 178 moveto -(Pretyping) -[7.68 4.56 6 3.84 6.96 6.96 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Pretyping -> Pattern -newpath 78 189 moveto -121 194 191 202 251 202 curveto -251 202 251 202 485 202 curveto -556 202 636 205 685 208 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 685 212 moveto -695 208 lineto -685 205 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 685 212 moveto -695 208 lineto -685 205 lineto -closepath -stroke -end grestore - -% Cases -gsave 10 dict begin -146 64 30 18 ellipse_path -stroke -gsave 10 dict begin -129 59 moveto -(Cases) -[9.36 6.24 5.52 6.24 5.52] -xshow -end grestore -end grestore - -% Pretyping -> Cases -newpath 53 166 moveto -68 147 93 115 116 91 curveto -118 89 119 88 121 86 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 124 88 moveto -129 79 lineto -119 83 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 124 88 moveto -129 79 lineto -119 83 lineto -closepath -stroke -end grestore - -% Detyping -gsave 10 dict begin -969 164 39 18 ellipse_path -stroke -gsave 10 dict begin -942 159 moveto -(Detyping) -[10.08 6 3.84 6.96 6.96 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Pretyping -> Detyping -newpath 78 177 moveto -121 172 191 164 251 164 curveto -251 164 251 164 728 164 curveto -794 164 870 164 919 164 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 919 168 moveto -929 164 lineto -919 161 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 919 168 moveto -929 164 lineto -919 161 lineto -closepath -stroke -end grestore - -% Indrec -gsave 10 dict begin -251 271 31 18 ellipse_path -stroke -gsave 10 dict begin -233 266 moveto -(Indrec) -[4.56 6.96 6.96 4.56 6.24 6.24] -xshow -end grestore -end grestore - -% Pretyping -> Indrec -newpath 69 195 moveto -83 202 101 209 116 216 curveto -150 230 188 246 216 257 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 214 260 moveto -225 261 lineto -217 254 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 214 260 moveto -225 261 lineto -217 254 lineto -closepath -stroke -end grestore - -% Coercion -gsave 10 dict begin -251 67 39 18 ellipse_path -stroke -gsave 10 dict begin -225 62 moveto -(Coercion) -[9.36 6.96 6.24 4.56 6.24 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Cases -> Coercion -newpath 176 65 moveto -184 65 193 66 202 66 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 202 70 moveto -212 66 lineto -202 63 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 202 70 moveto -212 66 lineto -202 63 lineto -closepath -stroke -end grestore - -% Detyping -> Inductiveops -newpath 1009 164 moveto -1022 164 1036 164 1050 164 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1050 168 moveto -1060 164 lineto -1050 161 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1050 168 moveto -1060 164 lineto -1050 161 lineto -closepath -stroke -end grestore - -% Detyping -> Rawterm -newpath 999 152 moveto -1020 144 1047 133 1069 125 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1070 128 moveto -1079 122 lineto -1068 122 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1070 128 moveto -1079 122 lineto -1068 122 lineto -closepath -stroke -end grestore - -% Indrec -> Inductiveops -newpath 281 276 moveto -325 283 412 294 485 294 curveto -485 294 485 294 839 294 curveto -937 294 1036 225 1082 188 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1085 190 moveto -1090 181 lineto -1080 185 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1085 190 moveto -1090 181 lineto -1080 185 lineto -closepath -stroke -end grestore - -% Matching -gsave 10 dict begin -610 248 40 18 ellipse_path -stroke -gsave 10 dict begin -582 243 moveto -(Matching) -[12.48 6.24 3.84 6 6.96 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Matching -> Pattern -newpath 643 237 moveto -658 232 675 227 689 222 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 690 225 moveto -699 219 lineto -688 219 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 690 225 moveto -699 219 lineto -688 219 lineto -closepath -stroke -end grestore - -% Matching -> Reductionops -newpath 650 250 moveto -696 253 773 256 839 256 curveto -839 256 839 256 969 256 curveto -1059 256 1159 212 1210 184 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1212 187 moveto -1219 179 lineto -1209 181 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1212 187 moveto -1219 179 lineto -1209 181 lineto -closepath -stroke -end grestore - -% Evarconv -gsave 10 dict begin -366 67 40 18 ellipse_path -stroke -gsave 10 dict begin -339 62 moveto -(Evarconv) -[8.4 6.72 6.24 4.56 6.24 6.96 6.48 6.96] -xshow -end grestore -end grestore - -% Evarconv -> Evarutil -newpath 406 68 moveto -474 69 610 71 682 72 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 682 76 moveto -692 72 lineto -682 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 682 76 moveto -692 72 lineto -682 69 lineto -closepath -stroke -end grestore - -% Evarconv -> Recordops -newpath 397 56 moveto -411 51 428 45 442 39 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 443 42 moveto -452 36 lineto -441 36 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 443 42 moveto -452 36 lineto -441 36 lineto -closepath -stroke -end grestore - -% Coercion -> Evarconv -newpath 290 67 moveto -299 67 307 67 316 67 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 316 71 moveto -326 67 lineto -316 64 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 316 71 moveto -326 67 lineto -316 64 lineto -closepath -stroke -end grestore - -% Clenv -gsave 10 dict begin -146 118 30 18 ellipse_path -stroke -gsave 10 dict begin -129 113 moveto -(Clenv) -[9.36 3.84 6.24 6.48 6.96] -xshow -end grestore -end grestore - -% Clenv -> Unification -newpath 176 118 moveto -252 118 455 118 554 118 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 554 122 moveto -564 118 lineto -554 115 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 554 122 moveto -564 118 lineto -554 115 lineto -closepath -stroke -end grestore - -% Clenv -> Coercion -newpath 170 107 moveto -183 100 200 93 215 85 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 217 88 moveto -224 80 lineto -214 82 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 217 88 moveto -224 80 lineto -214 82 lineto -closepath -stroke -end grestore -endpage -showpage -grestore -%%PageTrailer -%%EndPage: 1 -%%Trailer -%%Pages: 1 -end -restore -%%EOF diff --git a/dev/ocamlweb-doc/proofs.dep.ps b/dev/ocamlweb-doc/proofs.dep.ps deleted file mode 100644 index 4dd045ce..00000000 --- a/dev/ocamlweb-doc/proofs.dep.ps +++ /dev/null @@ -1,649 +0,0 @@ -%!PS-Adobe-2.0 -%%Creator: Graphviz version 2.12 (Tue Oct 23 13:46:12 UTC 2007) -%%For: (notin) Jean-Marc Notin,,, -%%Title: G -%%Pages: (atend) -%%BoundingBox: (atend) -%%EndComments -save -%%BeginProlog -/DotDict 200 dict def -DotDict begin - -/setupLatin1 { -mark -/EncodingVector 256 array def - EncodingVector 0 - -ISOLatin1Encoding 0 255 getinterval putinterval -EncodingVector 45 /hyphen put - -% Set up ISO Latin 1 character encoding -/starnetISO { - dup dup findfont dup length dict begin - { 1 index /FID ne { def }{ pop pop } ifelse - } forall - /Encoding EncodingVector def - currentdict end definefont -} def -/Times-Roman starnetISO def -/Times-Italic starnetISO def -/Times-Bold starnetISO def -/Times-BoldItalic starnetISO def -/Helvetica starnetISO def -/Helvetica-Oblique starnetISO def -/Helvetica-Bold starnetISO def -/Helvetica-BoldOblique starnetISO def -/Courier starnetISO def -/Courier-Oblique starnetISO def -/Courier-Bold starnetISO def -/Courier-BoldOblique starnetISO def -cleartomark -} bind def - -%%BeginResource: procset graphviz 0 0 -/coord-font-family /Times-Roman def -/default-font-family /Times-Roman def -/coordfont coord-font-family findfont 8 scalefont def - -/InvScaleFactor 1.0 def -/set_scale { - dup 1 exch div /InvScaleFactor exch def - scale -} bind def - -% styles -/solid { [] 0 setdash } bind def -/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def -/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def -/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def -/bold { 2 setlinewidth } bind def -/filled { } bind def -/unfilled { } bind def -/rounded { } bind def -/diagonals { } bind def - -% hooks for setting color -/nodecolor { sethsbcolor } bind def -/edgecolor { sethsbcolor } bind def -/graphcolor { sethsbcolor } bind def -/nopcolor {pop pop pop} bind def - -/beginpage { % i j npages - /npages exch def - /j exch def - /i exch def - /str 10 string def - npages 1 gt { - gsave - coordfont setfont - 0 0 moveto - (\() show i str cvs show (,) show j str cvs show (\)) show - grestore - } if -} bind def - -/set_font { - findfont exch - scalefont setfont -} def - -% draw aligned label in bounding box aligned to current point -/alignedtext { % width adj text - /text exch def - /adj exch def - /width exch def - gsave - width 0 gt { - text stringwidth pop adj mul 0 rmoveto - } if - [] 0 setdash - text show - grestore -} def - -/boxprim { % xcorner ycorner xsize ysize - 4 2 roll - moveto - 2 copy - exch 0 rlineto - 0 exch rlineto - pop neg 0 rlineto - closepath -} bind def - -/ellipse_path { - /ry exch def - /rx exch def - /y exch def - /x exch def - matrix currentmatrix - newpath - x y translate - rx ry scale - 0 0 1 0 360 arc - setmatrix -} bind def - -/endpage { showpage } bind def -/showpage { } def - -/layercolorseq - [ % layer color sequence - darkest to lightest - [0 0 0] - [.2 .8 .8] - [.4 .8 .8] - [.6 .8 .8] - [.8 .8 .8] - ] -def - -/layerlen layercolorseq length def - -/setlayer {/maxlayer exch def /curlayer exch def - layercolorseq curlayer 1 sub layerlen mod get - aload pop sethsbcolor - /nodecolor {nopcolor} def - /edgecolor {nopcolor} def - /graphcolor {nopcolor} def -} bind def - -/onlayer { curlayer ne {invis} if } def - -/onlayers { - /myupper exch def - /mylower exch def - curlayer mylower lt - curlayer myupper gt - or - {invis} if -} def - -/curlayer 0 def - -%%EndResource -%%EndProlog -%%BeginSetup -14 default-font-family set_font -1 setmiterlimit -% /arrowlength 10 def -% /arrowwidth 5 def - -% make sure pdfmark is harmless for PS-interpreters other than Distiller -/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse -% make '<<' and '>>' safe on PS Level 1 devices -/languagelevel where {pop languagelevel}{1} ifelse -2 lt { - userdict (<<) cvn ([) cvn load put - userdict (>>) cvn ([) cvn load put -} if - -%%EndSetup -setupLatin1 -%%Page: 1 1 -%%PageBoundingBox: 36 36 576 753 -%%PageOrientation: Landscape -gsave -36 36 576 753 boxprim clip newpath -0 0 1 beginpage -0.870968 0.870968 set_scale 90 rotate 45.3333 -657.333 translate -0.000 0.000 1.000 graphcolor -newpath -4 -4 moveto --4 616 lineto -819 616 lineto -819 -4 lineto -closepath fill -0.870968 setlinewidth -0.000 0.000 1.000 graphcolor -newpath -4 -4 moveto --4 616 lineto -819 616 lineto -819 -4 lineto -closepath stroke -% Clenvtac -gsave -0.502 1.000 0.820 nodecolor -451 522 37.1753 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -451 522 37.1753 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -451 517 moveto 49 -0.5 (Clenvtac) alignedtext -grestore -% Evar_refiner -gsave -0.502 1.000 0.820 nodecolor -439 450 49.1777 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -439 450 49.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -439 445 moveto 72 -0.5 (Evar_refiner) alignedtext -grestore -% Clenvtac->Evar_refiner -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 448 504 moveto -447 496 445 487 444 478 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 447.393 477.119 moveto -442 468 lineto -440.529 478.492 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 447.393 477.119 moveto -442 468 lineto -440.529 478.492 lineto -closepath stroke -grestore -% Tacmach -gsave -0.502 1.000 0.820 nodecolor -711 450 38.1754 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -711 450 38.1754 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -711 445 moveto 51 -0.5 (Tacmach) alignedtext -grestore -% Clenvtac->Tacmach -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 483 513 moveto -530 500 616 476 668 462 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 669.427 465.226 moveto -678 459 lineto -667.416 458.521 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 669.427 465.226 moveto -678 459 lineto -667.416 458.521 lineto -closepath stroke -grestore -% Refiner -gsave -0.502 1.000 0.820 nodecolor -439 378 34.1777 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -439 378 34.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -439 373 moveto 42 -0.5 (Refiner) alignedtext -grestore -% Evar_refiner->Refiner -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 439 432 moveto -439 424 439 415 439 406 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 442.5 406 moveto -439 396 lineto -435.5 406 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 442.5 406 moveto -439 396 lineto -435.5 406 lineto -closepath stroke -grestore -% Tacmach->Refiner -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 678 441 moveto -628 428 533 403 480 389 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 480.584 385.521 moveto -470 386 lineto -478.573 392.226 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 480.584 385.521 moveto -470 386 lineto -478.573 392.226 lineto -closepath stroke -grestore -% Redexpr -gsave -0.502 1.000 0.820 nodecolor -711 378 36.1752 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -711 378 36.1752 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -711 373 moveto 47 -0.5 (Redexpr) alignedtext -grestore -% Tacmach->Redexpr -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 711 432 moveto -711 424 711 415 711 406 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 714.5 406 moveto -711 396 lineto -707.5 406 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 714.5 406 moveto -711 396 lineto -707.5 406 lineto -closepath stroke -grestore -% Decl_mode -gsave -0.502 1.000 0.820 nodecolor -698 594 45.1777 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -698 594 45.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -698 589 moveto 64 -0.5 (Decl_mode) alignedtext -grestore -% Pfedit -gsave -0.502 1.000 0.820 nodecolor -698 522 30.1777 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -698 522 30.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -698 517 moveto 34 -0.5 (Pfedit) alignedtext -grestore -% Decl_mode->Pfedit -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 698 576 moveto -698 568 698 559 698 550 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 701.5 550 moveto -698 540 lineto -694.5 550 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 701.5 550 moveto -698 540 lineto -694.5 550 lineto -closepath stroke -grestore -% Pfedit->Evar_refiner -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 671 514 moveto -628 503 543 479 488 464 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 488.584 460.521 moveto -478 461 lineto -486.573 467.226 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 488.584 460.521 moveto -478 461 lineto -486.573 467.226 lineto -closepath stroke -grestore -% Pfedit->Tacmach -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 701 504 moveto -702 496 704 487 706 478 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 709.471 478.492 moveto -708 468 lineto -702.607 477.119 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 709.471 478.492 moveto -708 468 lineto -702.607 477.119 lineto -closepath stroke -grestore -% Logic -gsave -0.502 1.000 0.820 nodecolor -439 306 29.1747 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -439 306 29.1747 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -439 301 moveto 33 -0.5 (Logic) alignedtext -grestore -% Refiner->Logic -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 439 360 moveto -439 352 439 343 439 334 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 442.5 334 moveto -439 324 lineto -435.5 334 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 442.5 334 moveto -439 324 lineto -435.5 334 lineto -closepath stroke -grestore -% Proof_trees -gsave -0.502 1.000 0.820 nodecolor -439 234 45.1757 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -439 234 45.1757 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -439 229 moveto 65 -0.5 (Proof_trees) alignedtext -grestore -% Logic->Proof_trees -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 439 288 moveto -439 280 439 271 439 262 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 442.5 262 moveto -439 252 lineto -435.5 262 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 442.5 262 moveto -439 252 lineto -435.5 262 lineto -closepath stroke -grestore -% Proof_type -gsave -0.502 1.000 0.820 nodecolor -439 162 44.1757 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -439 162 44.1757 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -439 157 moveto 63 -0.5 (Proof_type) alignedtext -grestore -% Proof_trees->Proof_type -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 439 216 moveto -439 208 439 199 439 190 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 442.5 190 moveto -439 180 lineto -435.5 190 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 442.5 190 moveto -439 180 lineto -435.5 190 lineto -closepath stroke -grestore -% Decl_expr -gsave -0.502 1.000 0.820 nodecolor -439 90 42.1777 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -439 90 42.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -439 85 moveto 58 -0.5 (Decl_expr) alignedtext -grestore -% Proof_type->Decl_expr -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 439 144 moveto -439 136 439 127 439 118 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 442.5 118 moveto -439 108 lineto -435.5 118 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 442.5 118 moveto -439 108 lineto -435.5 118 lineto -closepath stroke -grestore -% Tacexpr -gsave -0.502 1.000 0.820 nodecolor -439 18 36.1777 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -439 18 36.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -439 13 moveto 46 -0.5 (Tacexpr) alignedtext -grestore -% Decl_expr->Tacexpr -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 439 72 moveto -439 64 439 55 439 46 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 442.5 46 moveto -439 36 lineto -435.5 46 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 442.5 46 moveto -439 36 lineto -435.5 46 lineto -closepath stroke -grestore -% Tactic_debug -gsave -0.502 1.000 0.820 nodecolor -133 450 51.1777 18 ellipse_path fill -0.870968 setlinewidth -filled -0.502 1.000 0.820 nodecolor -133 450 51.1777 18 ellipse_path stroke -0.000 0.000 0.000 nodecolor -14.00 /Times-Roman set_font -133 445 moveto 76 -0.5 (Tactic_debug) alignedtext -grestore -% Tactic_debug->Refiner -gsave -0.870968 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 176 440 moveto -234 426 339 401 398 387 curveto -stroke -0.000 0.000 0.000 edgecolor -newpath 398.881 390.393 moveto -408 385 lineto -397.508 383.529 lineto -closepath fill -0.870968 setlinewidth -solid -0.000 0.000 0.000 edgecolor -newpath 398.881 390.393 moveto -408 385 lineto -397.508 383.529 lineto -closepath stroke -grestore -endpage -showpage -grestore -%%PageTrailer -%%EndPage: 1 -%%Trailer -%%Pages: 1 -%%BoundingBox: 36 36 576 753 -end -restore -%%EOF diff --git a/dev/ocamlweb-doc/syntax.mly b/dev/ocamlweb-doc/syntax.mly deleted file mode 100644 index bfc7d5cc..00000000 --- a/dev/ocamlweb-doc/syntax.mly +++ /dev/null @@ -1,224 +0,0 @@ -%{ -open Ast -open Parse -%} - -%token <string> META INT IDENT -%token <string> OPER -%token LPAR RPAR BAR COMMA COLON BANG FUN DOT RARROW LET COLONEQ IN IF -%token THEN ELSE EVAL AT FOR PROP SET TYPE WILDCARD FIX -%token COFIX MATCH WITH END AND LBRACE RBRACE STRUCT AS SIMPL PERCENT -%token EOF - -%start main -%type <Ast.constr_ast> main - -%start constr -%type <Ast.constr_ast> constr - -%start simple_constr -%type <Ast.constr_ast> simple_constr - -%% - -main: - constr EOF { $1 } -; - - -paren_constr: - constr COMMA paren_constr { Pair($1,$3) } - | constr { $1 } -; - -constr: - binder_constr { $1 } - | oper_constr { close_stack $1 } -; - -binder_constr: - BANG ne_binders DOT constr { Prod($2, $4) } - | FUN ne_binders type_cstr RARROW constr { Lambda($2,mk_cast $5 $3) } - | LET IDENT binders type_cstr COLONEQ constr IN constr - { Let($2,mk_lambda $3 (mk_cast $6 $4),$8) } - | LET LPAR comma_binders RPAR COLONEQ constr IN constr - { LetCase($3,$6,$8) } - | IF constr THEN constr ELSE constr { IfCase($2,$4,$6) } - | fix_constr { $1 } - | EVAL rfun IN constr { Eval($2,$4) } -; - -comma_binders: - ne_comma_binders { $1 } - | { [] } -; - -ne_comma_binders: - binder COMMA ne_comma_binders { $1 :: $3 } - | binder { [$1] } -; - -rfun: - SIMPL { Simpl } -; - - -/* 2 Conflits shift/reduce */ -oper_constr: - oper_constr oper appl_constr - { parse_term $3 (parse_oper $2 $1) } - | oper_constr oper binder_constr - { parse_term $3 (parse_oper $2 $1) } - | oper_constr oper { parse_oper $2 $1 } - | { empty } - | appl_constr { parse_term $1 empty } -; - -oper: - OPER {$1} - | COLON {":"} -; - -appl_constr: - simple_constr ne_appl_args { Appl($1,$2) } - | AT global simple_constrs { ApplExpl($2,$3) } - | simple_constr { $1 } -; - -appl_arg: - AT INT COLONEQ simple_constr { (Some $2,$4) } - | simple_constr { (None,$1) } -; - -ne_appl_args: - appl_arg { [$1] } - | appl_arg ne_appl_args { $1::$2 } -; - -simple_constr: - atomic_constr { $1 } - | match_constr { $1 } - | LPAR paren_constr RPAR { $2 } - | simple_constr PERCENT IDENT { Scope($3,$1) } -; - -simple_constrs: - simple_constr simple_constrs { $1::$2 } - | { [] } -; - -atomic_constr: - global { Qualid $1 } - | PROP { Prop } - | SET { Set } - | TYPE { Type } - | INT { Int $1 } - | WILDCARD { Hole } - | META { Meta $1 } -; - -global: - IDENT DOT global { $1 :: $3 } - | IDENT { [$1] } -; - -/* Conflit normal */ -fix_constr: - fix_kw fix_decl - { let (id,_,_,_,_ as fx) = $2 in Fixp($1,[fx],id) } - | fix_kw fix_decl fix_decls FOR IDENT { Fixp($1, $2::$3, $5) } -; - -fix_kw: FIX {Fix} | COFIX {CoFix} -; - -fix_decl: - IDENT binders type_cstr annot COLONEQ constr { ($1,$2,$3,$4,$6) } -; - -fix_decls: - AND fix_decl fix_decls { $2::$3 } - | AND fix_decl { [$2] } -; - -annot: - LBRACE STRUCT IDENT RBRACE { Some $3 } - | { None } -; - -match_constr: - MATCH case_items case_type WITH branches END { Match($2,$3,$5) } -; - -case_items: - case_item { [$1] } - | case_item COMMA case_items { $1::$3 } -; - -case_item: - constr pred_pattern { ($1,$2) } -; - -case_type: - RARROW constr { Some $2 } - | { None } -; - -pred_pattern: - AS IDENT COLON constr { (Some $2, Some $4) } - | AS IDENT { (Some $2, None) } - | COLON constr { (None, Some $2) } - | { (None,None) } -; - -branches: - BAR branch_list { $2 } - | branch_list { $1 } - | { [] } -; - -branch_list: - patterns RARROW constr { [$1, $3] } - | patterns RARROW constr BAR branch_list { ($1,$3)::$5 } -; - -patterns: - pattern { [$1] } - | pattern COMMA patterns { $1::$3 } -; - -pattern: - pattern AS IDENT { PatAs($1,$3) } - | pattern COLON constr { PatType($1,$3) } - | IDENT simple_patterns { PatConstr($1,$2) } - | simple_pattern { $1 } -; - -simple_pattern: - IDENT { PatVar $1 } - | LPAR pattern RPAR { $2 } -; - -simple_patterns: - simple_pattern { [$1] } - | simple_pattern simple_patterns { $1::$2 } -; - -binder: - IDENT { ($1,Hole) } - | LPAR IDENT type_cstr RPAR { ($2,$3) } -; - -binders: - ne_binders { $1 } - | { [] } - -ne_binders: - binder { [$1] } - | binder ne_binders { $1::$2 } -; - -type_cstr: - COLON constr { $2 } - | { Hole } -; diff --git a/dev/ocamlweb-doc/tactics.dep.ps b/dev/ocamlweb-doc/tactics.dep.ps deleted file mode 100644 index f4de22b7..00000000 --- a/dev/ocamlweb-doc/tactics.dep.ps +++ /dev/null @@ -1,991 +0,0 @@ -%!PS-Adobe-2.0 -%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) -%%For: (herbelin) Hugo Herbelin -%%Title: G -%%Pages: (atend) -%%BoundingBox: 35 35 577 165 -%%EndComments -save -%%BeginProlog -/DotDict 200 dict def -DotDict begin - -/setupLatin1 { -mark -/EncodingVector 256 array def - EncodingVector 0 - -ISOLatin1Encoding 0 255 getinterval putinterval - -EncodingVector - dup 306 /AE - dup 301 /Aacute - dup 302 /Acircumflex - dup 304 /Adieresis - dup 300 /Agrave - dup 305 /Aring - dup 303 /Atilde - dup 307 /Ccedilla - dup 311 /Eacute - dup 312 /Ecircumflex - dup 313 /Edieresis - dup 310 /Egrave - dup 315 /Iacute - dup 316 /Icircumflex - dup 317 /Idieresis - dup 314 /Igrave - dup 334 /Udieresis - dup 335 /Yacute - dup 376 /thorn - dup 337 /germandbls - dup 341 /aacute - dup 342 /acircumflex - dup 344 /adieresis - dup 346 /ae - dup 340 /agrave - dup 345 /aring - dup 347 /ccedilla - dup 351 /eacute - dup 352 /ecircumflex - dup 353 /edieresis - dup 350 /egrave - dup 355 /iacute - dup 356 /icircumflex - dup 357 /idieresis - dup 354 /igrave - dup 360 /dcroat - dup 361 /ntilde - dup 363 /oacute - dup 364 /ocircumflex - dup 366 /odieresis - dup 362 /ograve - dup 365 /otilde - dup 370 /oslash - dup 372 /uacute - dup 373 /ucircumflex - dup 374 /udieresis - dup 371 /ugrave - dup 375 /yacute - dup 377 /ydieresis - -% Set up ISO Latin 1 character encoding -/starnetISO { - dup dup findfont dup length dict begin - { 1 index /FID ne { def }{ pop pop } ifelse - } forall - /Encoding EncodingVector def - currentdict end definefont -} def -/Times-Roman starnetISO def -/Times-Italic starnetISO def -/Times-Bold starnetISO def -/Times-BoldItalic starnetISO def -/Helvetica starnetISO def -/Helvetica-Oblique starnetISO def -/Helvetica-Bold starnetISO def -/Helvetica-BoldOblique starnetISO def -/Courier starnetISO def -/Courier-Oblique starnetISO def -/Courier-Bold starnetISO def -/Courier-BoldOblique starnetISO def -cleartomark -} bind def - -%%BeginResource: procset graphviz 0 0 -/coord-font-family /Times-Roman def -/default-font-family /Times-Roman def -/coordfont coord-font-family findfont 8 scalefont def - -/InvScaleFactor 1.0 def -/set_scale { - dup 1 exch div /InvScaleFactor exch def - dup scale -} bind def - -% styles -/solid { [] 0 setdash } bind def -/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def -/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def -/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def -/bold { 2 setlinewidth } bind def -/filled { } bind def -/unfilled { } bind def -/rounded { } bind def -/diagonals { } bind def - -% hooks for setting color -/nodecolor { sethsbcolor } bind def -/edgecolor { sethsbcolor } bind def -/graphcolor { sethsbcolor } bind def -/nopcolor {pop pop pop} bind def - -/beginpage { % i j npages - /npages exch def - /j exch def - /i exch def - /str 10 string def - npages 1 gt { - gsave - coordfont setfont - 0 0 moveto - (\() show i str cvs show (,) show j str cvs show (\)) show - grestore - } if -} bind def - -/set_font { - findfont exch - scalefont setfont -} def - -% draw aligned label in bounding box aligned to current point -/alignedtext { % width adj text - /text exch def - /adj exch def - /width exch def - gsave - width 0 gt { - text stringwidth pop adj mul 0 rmoveto - } if - [] 0 setdash - text show - grestore -} def - -/boxprim { % xcorner ycorner xsize ysize - 4 2 roll - moveto - 2 copy - exch 0 rlineto - 0 exch rlineto - pop neg 0 rlineto - closepath -} bind def - -/ellipse_path { - /ry exch def - /rx exch def - /y exch def - /x exch def - matrix currentmatrix - newpath - x y translate - rx ry scale - 0 0 1 0 360 arc - setmatrix -} bind def - -/endpage { showpage } bind def -/showpage { } def - -/layercolorseq - [ % layer color sequence - darkest to lightest - [0 0 0] - [.2 .8 .8] - [.4 .8 .8] - [.6 .8 .8] - [.8 .8 .8] - ] -def - -/layerlen layercolorseq length def - -/setlayer {/maxlayer exch def /curlayer exch def - layercolorseq curlayer 1 sub layerlen mod get - aload pop sethsbcolor - /nodecolor {nopcolor} def - /edgecolor {nopcolor} def - /graphcolor {nopcolor} def -} bind def - -/onlayer { curlayer ne {invis} if } def - -/onlayers { - /myupper exch def - /mylower exch def - curlayer mylower lt - curlayer myupper gt - or - {invis} if -} def - -/curlayer 0 def - -%%EndResource -%%EndProlog -%%BeginSetup -14 default-font-family set_font -1 setmiterlimit -% /arrowlength 10 def -% /arrowwidth 5 def - -% make sure pdfmark is harmless for PS-interpreters other than Distiller -/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse -% make '<<' and '>>' safe on PS Level 1 devices -/languagelevel where {pop languagelevel}{1} ifelse -2 lt { - userdict (<<) cvn ([) cvn load put - userdict (>>) cvn ([) cvn load put -} if - -%%EndSetup -%%Page: 1 1 -%%PageBoundingBox: 36 36 577 165 -%%PageOrientation: Portrait -gsave -35 35 542 130 boxprim clip newpath -36 36 translate -0 0 1 beginpage -0.4696 set_scale -0 0 translate 0 rotate -0.000 0.000 0.000 graphcolor -14.00 /Times-Roman set_font - -% Extraargs -gsave 10 dict begin -483 110 40 18 ellipse_path -stroke -gsave 10 dict begin -455 105 moveto -(Extraargs) -[8.4 6.96 3.84 4.56 6.24 6.24 4.32 6.96 5.52] -xshow -end grestore -end grestore - -% Setoid_replace -gsave 10 dict begin -615 64 54 18 ellipse_path -stroke -gsave 10 dict begin -573 59 moveto -(Setoid_replace) -[7.68 6 3.84 6.96 3.84 6.96 6.96 4.56 6.24 6.96 3.84 6.24 6.24 6.24] -xshow -end grestore -end grestore - -% Extraargs -> Setoid_replace -newpath 515 99 moveto -531 93 550 87 567 81 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 569 84 moveto -577 77 lineto -566 77 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 569 84 moveto -577 77 lineto -566 77 lineto -closepath -stroke -end grestore - -% Tactics -gsave 10 dict begin -884 110 33 18 ellipse_path -stroke -gsave 10 dict begin -864 105 moveto -(Tactics) -[7.44 6.24 6.24 3.84 3.84 6.24 5.52] -xshow -end grestore -end grestore - -% Setoid_replace -> Tactics -newpath 669 66 moveto -709 68 764 72 810 83 curveto -823 85 837 90 848 94 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 847 98 moveto -858 98 lineto -850 91 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 847 98 moveto -858 98 lineto -850 91 lineto -closepath -stroke -end grestore - -% Termdn -gsave 10 dict begin -998 256 35 18 ellipse_path -stroke -gsave 10 dict begin -976 251 moveto -(Termdn) -[7.2 6.24 4.8 10.8 6.96 6.96] -xshow -end grestore -end grestore - -% Dn -gsave 10 dict begin -1112 256 27 18 ellipse_path -stroke -gsave 10 dict begin -1102 251 moveto -(Dn) -[10.08 6.96] -xshow -end grestore -end grestore - -% Termdn -> Dn -newpath 1033 256 moveto -1047 256 1061 256 1075 256 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1075 260 moveto -1085 256 lineto -1075 253 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1075 260 moveto -1085 256 lineto -1075 253 lineto -closepath -stroke -end grestore - -% Hipattern -gsave 10 dict begin -998 110 40 18 ellipse_path -stroke -gsave 10 dict begin -971 105 moveto -(Hipattern) -[10.08 3.84 6.96 6.24 3.84 3.84 6.24 4.8 6.96] -xshow -end grestore -end grestore - -% Tactics -> Hipattern -newpath 917 110 moveto -927 110 938 110 948 110 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 948 114 moveto -958 110 lineto -948 107 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 948 114 moveto -958 110 lineto -948 107 lineto -closepath -stroke -end grestore - -% Tacticals -gsave 10 dict begin -1112 110 38 18 ellipse_path -stroke -gsave 10 dict begin -1087 105 moveto -(Tacticals) -[7.44 6.24 6.24 3.84 3.84 6.24 6.24 3.84 5.52] -xshow -end grestore -end grestore - -% Hipattern -> Tacticals -newpath 1038 110 moveto -1047 110 1055 110 1064 110 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1064 114 moveto -1074 110 lineto -1064 107 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1064 114 moveto -1074 110 lineto -1064 107 lineto -closepath -stroke -end grestore - -% Tacinterp -gsave 10 dict begin -170 191 39 18 ellipse_path -stroke -gsave 10 dict begin -143 186 moveto -(Tacinterp) -[7.44 6.24 6.24 3.84 6.96 3.84 6.24 4.8 6.96] -xshow -end grestore -end grestore - -% Auto -gsave 10 dict begin -483 218 27 18 ellipse_path -stroke -gsave 10 dict begin -468 213 moveto -(Auto) -[9.6 6.96 3.84 6.96] -xshow -end grestore -end grestore - -% Tacinterp -> Auto -newpath 209 194 moveto -269 200 386 210 445 215 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 445 218 moveto -455 216 lineto -445 212 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 445 218 moveto -455 216 lineto -445 212 lineto -closepath -stroke -end grestore - -% Leminv -gsave 10 dict begin -281 166 35 18 ellipse_path -stroke -gsave 10 dict begin -259 161 moveto -(Leminv) -[8.4 6.24 10.8 3.84 6.48 6.96] -xshow -end grestore -end grestore - -% Tacinterp -> Leminv -newpath 205 183 moveto -216 181 228 178 239 175 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 240 178 moveto -249 173 lineto -239 172 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 240 178 moveto -249 173 lineto -239 172 lineto -closepath -stroke -end grestore - -% Hiddentac -gsave 10 dict begin -615 164 42 18 ellipse_path -stroke -gsave 10 dict begin -585 159 moveto -(Hiddentac) -[10.08 3.84 6.96 6.96 6.24 6.96 4.08 6.24 6.24] -xshow -end grestore -end grestore - -% Auto -> Hiddentac -newpath 507 208 moveto -526 200 553 189 574 181 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 576 184 moveto -584 177 lineto -573 177 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 576 184 moveto -584 177 lineto -573 177 lineto -closepath -stroke -end grestore - -% Dhyp -gsave 10 dict begin -615 218 29 18 ellipse_path -stroke -gsave 10 dict begin -599 213 moveto -(Dhyp) -[10.08 6.48 6.96 6.96] -xshow -end grestore -end grestore - -% Auto -> Dhyp -newpath 511 218 moveto -530 218 555 218 576 218 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 576 222 moveto -586 218 lineto -576 215 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 576 222 moveto -586 218 lineto -576 215 lineto -closepath -stroke -end grestore - -% Inv -gsave 10 dict begin -379 164 27 18 ellipse_path -stroke -gsave 10 dict begin -369 159 moveto -(Inv) -[4.56 6.48 6.96] -xshow -end grestore -end grestore - -% Leminv -> Inv -newpath 316 165 moveto -324 165 333 165 342 165 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 342 169 moveto -352 165 lineto -342 162 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 342 169 moveto -352 165 lineto -342 162 lineto -closepath -stroke -end grestore - -% Refine -gsave 10 dict begin -758 110 32 18 ellipse_path -stroke -gsave 10 dict begin -739 105 moveto -(Refine) -[9.12 6.24 4.8 3.84 6.96 6.24] -xshow -end grestore -end grestore - -% Refine -> Tactics -newpath 790 110 moveto -805 110 824 110 841 110 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 841 114 moveto -851 110 lineto -841 107 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 841 114 moveto -851 110 lineto -841 107 lineto -closepath -stroke -end grestore - -% Nbtermdn -gsave 10 dict begin -758 256 42 18 ellipse_path -stroke -gsave 10 dict begin -729 251 moveto -(Nbtermdn) -[10.08 6.96 3.84 6.24 4.8 10.8 6.96 6.96] -xshow -end grestore -end grestore - -% Btermdn -gsave 10 dict begin -884 256 38 18 ellipse_path -stroke -gsave 10 dict begin -859 251 moveto -(Btermdn) -[9.36 3.84 6.24 4.8 10.8 6.96 6.96] -xshow -end grestore -end grestore - -% Nbtermdn -> Btermdn -newpath 800 256 moveto -812 256 824 256 836 256 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 836 260 moveto -846 256 lineto -836 253 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 836 260 moveto -846 256 lineto -836 253 lineto -closepath -stroke -end grestore - -% Btermdn -> Termdn -newpath 922 256 moveto -932 256 943 256 953 256 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 953 260 moveto -963 256 lineto -953 253 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 953 260 moveto -963 256 lineto -953 253 lineto -closepath -stroke -end grestore - -% Elim -gsave 10 dict begin -483 164 27 18 ellipse_path -stroke -gsave 10 dict begin -468 159 moveto -(Elim) -[8.4 3.84 3.84 10.8] -xshow -end grestore -end grestore - -% Inv -> Elim -newpath 406 164 moveto -418 164 432 164 445 164 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 445 168 moveto -455 164 lineto -445 161 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 445 168 moveto -455 164 lineto -445 161 lineto -closepath -stroke -end grestore - -% Equality -gsave 10 dict begin -483 56 37 18 ellipse_path -stroke -gsave 10 dict begin -459 51 moveto -(Equality) -[8.4 6.72 6.96 6.24 3.84 3.84 3.84 6.96] -xshow -end grestore -end grestore - -% Inv -> Equality -newpath 390 147 moveto -401 130 421 102 442 83 curveto -445 80 448 78 451 76 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 453 79 moveto -459 70 lineto -449 73 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 453 79 moveto -459 70 lineto -449 73 lineto -closepath -stroke -end grestore - -% Elim -> Hiddentac -newpath 511 164 moveto -526 164 545 164 562 164 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 562 168 moveto -572 164 lineto -562 161 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 562 168 moveto -572 164 lineto -562 161 lineto -closepath -stroke -end grestore - -% Equality -> Setoid_replace -newpath 520 58 moveto -530 59 540 60 551 60 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 551 63 moveto -561 61 lineto -551 57 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 551 63 moveto -561 61 lineto -551 57 lineto -closepath -stroke -end grestore - -% Evar_tactics -gsave 10 dict begin -758 164 48 18 ellipse_path -stroke -gsave 10 dict begin -722 159 moveto -(Evar_tactics) -[8.4 6.72 6.24 4.56 6.96 4.08 6.24 6.24 3.84 3.84 6.24 5.52] -xshow -end grestore -end grestore - -% Hiddentac -> Evar_tactics -newpath 658 164 moveto -671 164 685 164 699 164 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 699 168 moveto -709 164 lineto -699 161 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 699 168 moveto -709 164 lineto -699 161 lineto -closepath -stroke -end grestore - -% Evar_tactics -> Tactics -newpath 790 150 moveto -808 142 830 132 849 125 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 850 128 moveto -858 121 lineto -847 122 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 850 128 moveto -858 121 lineto -847 122 lineto -closepath -stroke -end grestore - -% Dhyp -> Tactics -newpath 644 219 moveto -684 220 756 217 810 191 curveto -844 175 855 163 872 137 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 875 138 moveto -877 128 lineto -869 135 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 875 138 moveto -877 128 lineto -869 135 lineto -closepath -stroke -end grestore - -% Dhyp -> Nbtermdn -newpath 642 225 moveto -662 230 689 238 712 244 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 712 247 moveto -722 246 lineto -713 241 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 712 247 moveto -722 246 lineto -713 241 lineto -closepath -stroke -end grestore - -% Contradiction -gsave 10 dict begin -758 18 51 18 ellipse_path -stroke -gsave 10 dict begin -719 13 moveto -(Contradiction) -[9.36 6.96 6.96 3.84 4.56 6.24 6.96 3.84 6.24 3.84 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Contradiction -> Tactics -newpath 784 34 moveto -793 39 802 44 810 50 curveto -827 62 845 76 859 88 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 857 91 moveto -867 95 lineto -862 86 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 857 91 moveto -867 95 lineto -862 86 lineto -closepath -stroke -end grestore - -% Autorewrite -gsave 10 dict begin -47 191 47 18 ellipse_path -stroke -gsave 10 dict begin -13 186 moveto -(Autorewrite) -[9.6 6.96 3.84 6.96 4.56 5.76 10.08 4.8 3.84 3.84 6.24] -xshow -end grestore -end grestore - -% Autorewrite -> Tacinterp -newpath 94 191 moveto -102 191 111 191 120 191 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 120 195 moveto -130 191 lineto -120 188 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 120 195 moveto -130 191 lineto -120 188 lineto -closepath -stroke -end grestore -endpage -showpage -grestore -%%PageTrailer -%%EndPage: 1 -%%Trailer -%%Pages: 1 -end -restore -%%EOF diff --git a/dev/ocamlweb-doc/toplevel.dep.ps b/dev/ocamlweb-doc/toplevel.dep.ps deleted file mode 100644 index e0355aac..00000000 --- a/dev/ocamlweb-doc/toplevel.dep.ps +++ /dev/null @@ -1,971 +0,0 @@ -%!PS-Adobe-2.0 -%%Creator: dot version 2.2 (Wed Jan 19 21:09:25 UTC 2005) -%%For: (herbelin) Hugo Herbelin -%%Title: G -%%Pages: (atend) -%%BoundingBox: 35 35 577 166 -%%EndComments -save -%%BeginProlog -/DotDict 200 dict def -DotDict begin - -/setupLatin1 { -mark -/EncodingVector 256 array def - EncodingVector 0 - -ISOLatin1Encoding 0 255 getinterval putinterval - -EncodingVector - dup 306 /AE - dup 301 /Aacute - dup 302 /Acircumflex - dup 304 /Adieresis - dup 300 /Agrave - dup 305 /Aring - dup 303 /Atilde - dup 307 /Ccedilla - dup 311 /Eacute - dup 312 /Ecircumflex - dup 313 /Edieresis - dup 310 /Egrave - dup 315 /Iacute - dup 316 /Icircumflex - dup 317 /Idieresis - dup 314 /Igrave - dup 334 /Udieresis - dup 335 /Yacute - dup 376 /thorn - dup 337 /germandbls - dup 341 /aacute - dup 342 /acircumflex - dup 344 /adieresis - dup 346 /ae - dup 340 /agrave - dup 345 /aring - dup 347 /ccedilla - dup 351 /eacute - dup 352 /ecircumflex - dup 353 /edieresis - dup 350 /egrave - dup 355 /iacute - dup 356 /icircumflex - dup 357 /idieresis - dup 354 /igrave - dup 360 /dcroat - dup 361 /ntilde - dup 363 /oacute - dup 364 /ocircumflex - dup 366 /odieresis - dup 362 /ograve - dup 365 /otilde - dup 370 /oslash - dup 372 /uacute - dup 373 /ucircumflex - dup 374 /udieresis - dup 371 /ugrave - dup 375 /yacute - dup 377 /ydieresis - -% Set up ISO Latin 1 character encoding -/starnetISO { - dup dup findfont dup length dict begin - { 1 index /FID ne { def }{ pop pop } ifelse - } forall - /Encoding EncodingVector def - currentdict end definefont -} def -/Times-Roman starnetISO def -/Times-Italic starnetISO def -/Times-Bold starnetISO def -/Times-BoldItalic starnetISO def -/Helvetica starnetISO def -/Helvetica-Oblique starnetISO def -/Helvetica-Bold starnetISO def -/Helvetica-BoldOblique starnetISO def -/Courier starnetISO def -/Courier-Oblique starnetISO def -/Courier-Bold starnetISO def -/Courier-BoldOblique starnetISO def -cleartomark -} bind def - -%%BeginResource: procset graphviz 0 0 -/coord-font-family /Times-Roman def -/default-font-family /Times-Roman def -/coordfont coord-font-family findfont 8 scalefont def - -/InvScaleFactor 1.0 def -/set_scale { - dup 1 exch div /InvScaleFactor exch def - dup scale -} bind def - -% styles -/solid { [] 0 setdash } bind def -/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def -/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def -/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def -/bold { 2 setlinewidth } bind def -/filled { } bind def -/unfilled { } bind def -/rounded { } bind def -/diagonals { } bind def - -% hooks for setting color -/nodecolor { sethsbcolor } bind def -/edgecolor { sethsbcolor } bind def -/graphcolor { sethsbcolor } bind def -/nopcolor {pop pop pop} bind def - -/beginpage { % i j npages - /npages exch def - /j exch def - /i exch def - /str 10 string def - npages 1 gt { - gsave - coordfont setfont - 0 0 moveto - (\() show i str cvs show (,) show j str cvs show (\)) show - grestore - } if -} bind def - -/set_font { - findfont exch - scalefont setfont -} def - -% draw aligned label in bounding box aligned to current point -/alignedtext { % width adj text - /text exch def - /adj exch def - /width exch def - gsave - width 0 gt { - text stringwidth pop adj mul 0 rmoveto - } if - [] 0 setdash - text show - grestore -} def - -/boxprim { % xcorner ycorner xsize ysize - 4 2 roll - moveto - 2 copy - exch 0 rlineto - 0 exch rlineto - pop neg 0 rlineto - closepath -} bind def - -/ellipse_path { - /ry exch def - /rx exch def - /y exch def - /x exch def - matrix currentmatrix - newpath - x y translate - rx ry scale - 0 0 1 0 360 arc - setmatrix -} bind def - -/endpage { showpage } bind def -/showpage { } def - -/layercolorseq - [ % layer color sequence - darkest to lightest - [0 0 0] - [.2 .8 .8] - [.4 .8 .8] - [.6 .8 .8] - [.8 .8 .8] - ] -def - -/layerlen layercolorseq length def - -/setlayer {/maxlayer exch def /curlayer exch def - layercolorseq curlayer 1 sub layerlen mod get - aload pop sethsbcolor - /nodecolor {nopcolor} def - /edgecolor {nopcolor} def - /graphcolor {nopcolor} def -} bind def - -/onlayer { curlayer ne {invis} if } def - -/onlayers { - /myupper exch def - /mylower exch def - curlayer mylower lt - curlayer myupper gt - or - {invis} if -} def - -/curlayer 0 def - -%%EndResource -%%EndProlog -%%BeginSetup -14 default-font-family set_font -1 setmiterlimit -% /arrowlength 10 def -% /arrowwidth 5 def - -% make sure pdfmark is harmless for PS-interpreters other than Distiller -/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse -% make '<<' and '>>' safe on PS Level 1 devices -/languagelevel where {pop languagelevel}{1} ifelse -2 lt { - userdict (<<) cvn ([) cvn load put - userdict (>>) cvn ([) cvn load put -} if - -%%EndSetup -%%Page: 1 1 -%%PageBoundingBox: 36 36 577 166 -%%PageOrientation: Portrait -gsave -35 35 542 131 boxprim clip newpath -36 36 translate -0 0 1 beginpage -0.4180 set_scale -0 0 translate 0 rotate -0.000 0.000 0.000 graphcolor -14.00 /Times-Roman set_font - -% Vernac -gsave 10 dict begin -562 145 33 18 ellipse_path -stroke -gsave 10 dict begin -541 140 moveto -(Vernac) -[8.88 6.24 4.8 6.96 6.24 6.24] -xshow -end grestore -end grestore - -% Vernacentries -gsave 10 dict begin -724 158 52 18 ellipse_path -stroke -gsave 10 dict begin -685 153 moveto -(Vernacentries) -[8.88 6.24 4.8 6.96 6.24 6.24 6.24 6.96 3.84 4.8 3.84 6.24 5.52] -xshow -end grestore -end grestore - -% Vernac -> Vernacentries -newpath 595 148 moveto -615 149 640 151 663 153 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 663 156 moveto -673 154 lineto -663 150 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 663 156 moveto -673 154 lineto -663 150 lineto -closepath -stroke -end grestore - -% Vernacinterp -gsave 10 dict begin -862 158 50 18 ellipse_path -stroke -gsave 10 dict begin -825 153 moveto -(Vernacinterp) -[8.88 6.24 4.8 6.96 6.24 6.24 3.84 6.96 3.84 6.24 4.8 6.96] -xshow -end grestore -end grestore - -% Vernacentries -> Vernacinterp -newpath 776 158 moveto -785 158 793 158 802 158 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 802 162 moveto -812 158 lineto -802 155 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 802 162 moveto -812 158 lineto -802 155 lineto -closepath -stroke -end grestore - -% Discharge -gsave 10 dict begin -862 212 42 18 ellipse_path -stroke -gsave 10 dict begin -833 207 moveto -(Discharge) -[10.08 3.84 5.52 6 6.96 6.24 4.32 6.72 6.24] -xshow -end grestore -end grestore - -% Vernacentries -> Discharge -newpath 758 171 moveto -777 179 801 188 822 196 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 820 199 moveto -831 200 lineto -823 193 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 820 199 moveto -831 200 lineto -823 193 lineto -closepath -stroke -end grestore - -% Mltop -gsave 10 dict begin -862 104 31 18 ellipse_path -stroke -gsave 10 dict begin -844 99 moveto -(Mltop) -[12.48 3.84 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Vernacentries -> Mltop -newpath 758 145 moveto -779 137 805 126 826 118 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 828 121 moveto -836 114 lineto -825 114 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 828 121 moveto -836 114 lineto -825 114 lineto -closepath -stroke -end grestore - -% Record -gsave 10 dict begin -862 281 33 18 ellipse_path -stroke -gsave 10 dict begin -842 276 moveto -(Record) -[9.12 6.24 6.24 6.96 4.32 6.96] -xshow -end grestore -end grestore - -% Vernacentries -> Record -newpath 742 175 moveto -760 192 788 217 812 239 curveto -819 246 828 253 835 259 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 833 262 moveto -843 266 lineto -838 257 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 833 262 moveto -843 266 lineto -838 257 lineto -closepath -stroke -end grestore - -% Himsg -gsave 10 dict begin -991 85 32 18 ellipse_path -stroke -gsave 10 dict begin -971 80 moveto -(Himsg) -[10.08 3.84 10.8 5.52 6.96] -xshow -end grestore -end grestore - -% Vernacinterp -> Himsg -newpath 890 143 moveto -897 139 905 135 912 131 curveto -929 123 946 112 960 103 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 962 106 moveto -969 98 lineto -959 100 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 962 106 moveto -969 98 lineto -959 100 lineto -closepath -stroke -end grestore - -% Vernacexpr -gsave 10 dict begin -1246 221 45 18 ellipse_path -stroke -gsave 10 dict begin -1213 216 moveto -(Vernacexpr) -[8.88 6.24 4.8 6.96 6.24 6.24 5.76 6.96 6.96 4.56] -xshow -end grestore -end grestore - -% Vernacinterp -> Vernacexpr -newpath 912 159 moveto -947 160 994 163 1034 169 curveto -1092 178 1158 195 1200 207 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1199 210 moveto -1210 210 lineto -1201 204 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1199 210 moveto -1210 210 lineto -1201 204 lineto -closepath -stroke -end grestore - -% Class -gsave 10 dict begin -1117 238 28 18 ellipse_path -stroke -gsave 10 dict begin -1101 233 moveto -(Class) -[9.36 3.84 6.24 5.52 5.52] -xshow -end grestore -end grestore - -% Discharge -> Class -newpath 902 217 moveto -917 219 933 221 948 223 curveto -992 228 1044 232 1079 235 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1079 238 moveto -1089 236 lineto -1079 232 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1079 238 moveto -1089 236 lineto -1079 232 lineto -closepath -stroke -end grestore - -% Recordobj -gsave 10 dict begin -991 196 42 18 ellipse_path -stroke -gsave 10 dict begin -962 191 moveto -(Recordobj) -[9.12 6.24 6.24 6.96 4.32 6.96 6.96 6.96 3.84] -xshow -end grestore -end grestore - -% Discharge -> Recordobj -newpath 902 207 moveto -914 205 927 204 940 202 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 940 205 moveto -950 201 lineto -940 199 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 940 205 moveto -950 201 lineto -940 199 lineto -closepath -stroke -end grestore - -% Command -gsave 10 dict begin -991 288 42 18 ellipse_path -stroke -gsave 10 dict begin -961 283 moveto -(Command) -[9.36 6.96 10.8 10.8 6.24 6.96 6.96] -xshow -end grestore -end grestore - -% Record -> Command -newpath 895 283 moveto -908 284 923 285 938 285 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 938 288 moveto -948 286 lineto -938 282 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 938 288 moveto -948 286 lineto -938 282 lineto -closepath -stroke -end grestore - -% Toplevel -gsave 10 dict begin -255 72 37 18 ellipse_path -stroke -gsave 10 dict begin -231 67 moveto -(Toplevel) -[7.2 6.96 6.96 3.84 5.76 6.48 6.24 3.84] -xshow -end grestore -end grestore - -% Protectedtoplevel -gsave 10 dict begin -390 72 61 18 ellipse_path -stroke -gsave 10 dict begin -341 67 moveto -(Protectedtoplevel) -[7.68 4.56 6.72 3.84 6.24 6.24 3.84 6.24 6.96 3.84 6.96 6.96 3.84 5.76 6.48 6.24 3.84] -xshow -end grestore -end grestore - -% Toplevel -> Protectedtoplevel -newpath 292 72 moveto -300 72 309 72 318 72 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 318 76 moveto -328 72 lineto -318 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 318 76 moveto -328 72 lineto -318 69 lineto -closepath -stroke -end grestore - -% Protectedtoplevel -> Vernac -newpath 425 87 moveto -455 100 497 117 527 130 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 525 133 moveto -536 134 lineto -528 127 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 525 133 moveto -536 134 lineto -528 127 lineto -closepath -stroke -end grestore - -% Cerrors -gsave 10 dict begin -724 65 34 18 ellipse_path -stroke -gsave 10 dict begin -702 60 moveto -(Cerrors) -[9.36 6.24 5.04 4.56 6.96 4.56 5.52] -xshow -end grestore -end grestore - -% Protectedtoplevel -> Cerrors -newpath 452 71 moveto -518 70 621 67 679 66 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 679 70 moveto -689 66 lineto -679 63 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 679 70 moveto -689 66 lineto -679 63 lineto -closepath -stroke -end grestore - -% Line_oriented_parser -gsave 10 dict begin -562 26 73 18 ellipse_path -stroke -gsave 10 dict begin -501 21 moveto -(Line_oriented_parser) -[8.4 3.84 6.96 6.24 6.96 6.96 4.8 3.84 6.24 6.96 3.84 6.24 6.96 6.96 6.96 6.24 4.56 5.52 6.24 4.56] -xshow -end grestore -end grestore - -% Protectedtoplevel -> Line_oriented_parser -newpath 436 60 moveto -457 55 481 48 502 42 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 503 45 moveto -512 39 lineto -501 39 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 503 45 moveto -512 39 lineto -501 39 lineto -closepath -stroke -end grestore - -% Metasyntax -gsave 10 dict begin -1117 292 46 18 ellipse_path -stroke -gsave 10 dict begin -1083 287 moveto -(Metasyntax) -[12.48 6 4.08 6.24 5.52 6.96 6.96 4.08 6.24 6.96] -xshow -end grestore -end grestore - -% Command -> Metasyntax -newpath 1034 289 moveto -1043 290 1052 290 1061 290 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1061 293 moveto -1071 291 lineto -1061 287 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1061 293 moveto -1071 291 lineto -1061 287 lineto -closepath -stroke -end grestore - -% Command -> Class -newpath 1022 276 moveto -1041 268 1065 259 1084 252 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1085 255 moveto -1093 248 lineto -1082 249 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1085 255 moveto -1093 248 lineto -1082 249 lineto -closepath -stroke -end grestore - -% Cerrors -> Himsg -newpath 758 67 moveto -796 69 859 73 912 77 curveto -924 78 937 79 949 80 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 949 83 moveto -959 81 lineto -949 77 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 949 83 moveto -959 81 lineto -949 77 lineto -closepath -stroke -end grestore - -% Minicoq -gsave 10 dict begin -38 126 37 18 ellipse_path -stroke -gsave 10 dict begin -13 121 moveto -(Minicoq) -[12.48 3.84 6.96 3.84 6.24 6.96 6.96] -xshow -end grestore -end grestore - -% Fhimsg -gsave 10 dict begin -147 126 34 18 ellipse_path -stroke -gsave 10 dict begin -125 121 moveto -(Fhimsg) -[7.68 6.96 3.84 10.8 5.52 6.96] -xshow -end grestore -end grestore - -% Minicoq -> Fhimsg -newpath 76 126 moveto -84 126 93 126 102 126 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 102 130 moveto -112 126 lineto -102 123 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 102 130 moveto -112 126 lineto -102 123 lineto -closepath -stroke -end grestore - -% Metasyntax -> Vernacexpr -newpath 1144 277 moveto -1163 267 1189 252 1210 241 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 1212 244 moveto -1219 236 lineto -1209 238 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 1212 244 moveto -1219 236 lineto -1209 238 lineto -closepath -stroke -end grestore - -% Coqtop -gsave 10 dict begin -38 45 34 18 ellipse_path -stroke -gsave 10 dict begin -17 40 moveto -(Coqtop) -[9.36 6.96 6.96 3.84 6.96 6.96] -xshow -end grestore -end grestore - -% Coqinit -gsave 10 dict begin -147 72 34 18 ellipse_path -stroke -gsave 10 dict begin -126 67 moveto -(Coqinit) -[9.36 6.96 6.96 3.84 6.96 3.84 3.84] -xshow -end grestore -end grestore - -% Coqtop -> Coqinit -newpath 69 53 moveto -81 56 94 59 106 62 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 105 65 moveto -116 65 lineto -107 59 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 105 65 moveto -116 65 lineto -107 59 lineto -closepath -stroke -end grestore - -% Usage -gsave 10 dict begin -147 18 31 18 ellipse_path -stroke -gsave 10 dict begin -129 13 moveto -(Usage) -[10.08 5.52 6.24 6.72 6.24] -xshow -end grestore -end grestore - -% Coqtop -> Usage -newpath 69 37 moveto -81 34 95 31 108 28 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 109 31 moveto -118 25 lineto -107 25 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 109 31 moveto -118 25 lineto -107 25 lineto -closepath -stroke -end grestore - -% Coqinit -> Toplevel -newpath 181 72 moveto -190 72 199 72 208 72 curveto -stroke -gsave 10 dict begin -solid -1 setlinewidth -0.000 0.000 0.000 edgecolor -newpath 208 76 moveto -218 72 lineto -208 69 lineto -closepath -fill -0.000 0.000 0.000 edgecolor -newpath 208 76 moveto -218 72 lineto -208 69 lineto -closepath -stroke -end grestore -endpage -showpage -grestore -%%PageTrailer -%%EndPage: 1 -%%Trailer -%%Pages: 1 -end -restore -%%EOF diff --git a/dev/printers.mllib b/dev/printers.mllib index 889484ee..6a42678e 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -7,18 +7,16 @@ Flags Segmenttree Unicodetable Util +Errors Bigint Hashcons Dyn System Envars -Bstack -Edit -Gset +Store Gmap Fset Fmap -Tlm Gmapl Profile Explore @@ -27,6 +25,7 @@ Rtree Heap Option Dnet +Hashtbl_alt Names Univ @@ -71,7 +70,7 @@ Assumptions Termops Namegen Evd -Rawterm +Glob_term Reductionops Inductiveops Retyping @@ -81,6 +80,7 @@ Evarutil Term_dnet Recordops Evarconv +Arguments_renaming Typing Pattern Matching @@ -94,8 +94,9 @@ Coercion Unification Cases Pretyping -Clenv +Declaremods +Tok Lexer Ppextend Genarg @@ -109,12 +110,17 @@ Syntax_def Implicit_quantifiers Smartlocate Constrintern -Proof_trees +Modintern Tacexpr Proof_type +Goal Logic Refiner +Clenv Evar_refiner +Proofview +Proof +Proof_global Pfedit Tactic_debug Decl_mode diff --git a/dev/tools/change-header b/dev/tools/change-header new file mode 100755 index 00000000..61cc8666 --- /dev/null +++ b/dev/tools/change-header @@ -0,0 +1,55 @@ +#!/bin/sh + +#This script changes the header of .ml* files + +if [ ! $# = 2 ]; then + echo Usage: change-header old-header-file new-header-file + exit 1 +fi + +oldheader=$1 +newheader=$2 + +if [ ! -f $oldheader ]; then echo Cannot read file $oldheader; exit 1; fi +if [ ! -f $newheader ]; then echo Cannot read file $newheader; exit 1; fi + +n=`wc -l $oldheader | sed -e "s/ *\([0-9]*\).*/\1/g"` +nsucc=`expr $n + 1` + +linea='(* -*- coding:utf-8 -*- *)' +lineb='(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)' + +modified=0 +kept=0 + +for i in `find . -name \*.mli -o -name \*.ml -o -name \*.ml4 -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do + headline=`head -n 1 $i` + if `echo $headline | grep "(\* -\*- .* \*)" > /dev/null`; then + # Has emacs header + head -n +$nsucc $i | tail -n $n > $i.head.tmp$$ + hasheadline=1 + nnext=`expr $nsucc + 1` + else + head -n +$n $i > $i.head.tmp$$ + hasheadline=0 + nnext=$nsucc + fi + if diff -a -q $oldheader $i.head.tmp$$ > /dev/null; then + echo "$i: header changed" + if [ $hasheadline = 1 ]; then + echo $headline > $i.tmp$$ + else + touch $i.tmp$$ + fi + cat $newheader >> $i.tmp$$ + tail -n +$nnext $i >> $i.tmp$$ + mv $i.tmp$$ $i + modified=`expr $modified + 1` + else + kept=`expr $kept + 1` + fi + rm $i.head.tmp$$ +done + +echo $modified files updated +echo $kept files unchanged diff --git a/dev/tools/univdot b/dev/tools/univdot deleted file mode 100755 index bb0dd2c8..00000000 --- a/dev/tools/univdot +++ /dev/null @@ -1,49 +0,0 @@ -#!/bin/sh - -usage() { - echo "" - echo "usage: univdot [INPUT] [OUTPUT]" - echo "" - echo "takes the output of Dump Universes \"file\" command" - echo "and transforms it to the dot format" - echo "" - echo "Coq> Dump Universes \"univ.raw\"." - echo "" - echo "user@host> univdot univ.raw | dot -Tps > univ.ps" - echo "" -} - - -# these are dot edge attributes to draw arrows corresponding -# to > >= and = edges of the universe graph - -GT="[color=red]" -GE="[color=blue]" -EQ="[color=black]" - - -# input/output redirection -case $# in - 0) ;; - 1) case $1 in - -h|-help|--help) usage - exit 0 ;; - *) exec < $1 ;; - esac ;; - 2) exec < $1 > $2 ;; - *) usage - exit 0;; -esac - - -# dot header -echo 'digraph G {\ - size="7.5,10" ;\ - rankdir = TB ;' - -sed -e "s/^\([^ =>]\+\) > \([^ =>]\+\)/\1 -> \2 $GT/" \ - -e "s/^\([^ =>]\+\) >= \([^ =>]\+\)/\1 -> \2 $GE/" \ - -e "s/^\([^ =>]\+\) = \([^ =>]\+\)/\1 -> \2 $EQ/" \ -| sed -e "s/\./_/g" - -echo "}"
\ No newline at end of file diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 3a6abd43..3fc90761 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,22 +16,20 @@ open Libnames open Nameops open Sign open Univ -open Proof_trees open Environ open Printer open Tactic_printer -open Refiner open Term open Termops -open Clenv open Cerrors open Evd open Goptions open Genarg open Mod_subst - +open Clenv let _ = Constrextern.print_evar_arguments := true +let _ = Constrextern.print_universes := true let _ = set_bool_option_value ["Printing";"Matching"] false let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found) @@ -58,9 +56,9 @@ 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 ppglob_constr = (fun x -> pp(pr_lglob_constr x)) let pppattern = (fun x -> pp(pr_constr_pattern x)) -let pptype = (fun x -> pp(pr_ltype x)) +let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e))) let ppfconstr c = ppconstr (Closure.term_of_fconstr c) @@ -114,22 +112,31 @@ 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 ppevm evd = pp(pr_evar_map (Some 2) evd) +let ppevmall evd = pp(pr_evar_map None evd) +let pr_existentialset evars = + prlist_with_sep spc pr_meta (ExistentialSet.elements evars) +let ppexistentialset evars = + pp (pr_existentialset evars) let ppclenv clenv = pp(pr_clenv clenv) -let ppgoal g = pp(db_pr_goal g) +let ppgoalgoal gl = pp(Goal.pr_goal gl) +let ppgoal g = pp(Printer.pr_goal g) +(* spiwack: deactivated until a replacement is found let pppftreestate p = pp(print_pftreestate p) +*) -let pr_gls gls = - hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) +(* let ppgoal g = pp(db_pr_goal g) *) +(* let pr_gls gls = *) +(* hov 0 (pr_evar_defs (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) *) -let pr_glls glls = - hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++ - prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) +(* let pr_glls glls = *) +(* hov 0 (pr_evar_defs (sig_sig glls) ++ fnl () ++ *) +(* prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) *) -let ppsigmagoal g = pp(pr_goal (sig_it g)) -let prgls gls = pp(pr_gls gls) -let prglls glls = pp(pr_glls glls) -let pproof p = pp(print_proof Evd.empty empty_named_context p) +(* let ppsigmagoal g = pp(pr_goal (sig_it g)) *) +(* let prgls gls = pp(pr_gls gls) *) +(* let prglls glls = pp(pr_glls glls) *) +(* let pproof p = pp(print_proof Evd.empty empty_named_context p) *) let ppuni u = pp(pr_uni u) @@ -153,6 +160,7 @@ let cast_kind_display k = match k with | VMcast -> "VMcast" | DEFAULTcast -> "DEFAULTcast" + | REVERTcast -> "REVERTcast" let constr_display csr = let rec term_display c = match kind_of_term c with @@ -412,12 +420,12 @@ let _ = (fun () -> in_current_context constr_display c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Pp.pp (Cerrors.explain_exn e) + e -> Pp.pp (Errors.print e) let _ = - extend_vernac_command_grammar "PrintConstr" + extend_vernac_command_grammar "PrintConstr" None [[GramTerminal "PrintConstr"; GramNonTerminal - (dummy_loc,ConstrArgType,Extend.Aentry ("constr","constr"), + (dummy_loc,ConstrArgType,Aentry ("constr","constr"), Some (Names.id_of_string "c"))]] let _ = @@ -429,12 +437,12 @@ let _ = (fun () -> in_current_context print_pure_constr c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Pp.pp (Cerrors.explain_exn e) + e -> Pp.pp (Errors.print e) let _ = - extend_vernac_command_grammar "PrintPureConstr" + extend_vernac_command_grammar "PrintPureConstr" None [[GramTerminal "PrintPureConstr"; GramNonTerminal - (dummy_loc,ConstrArgType,Extend.Aentry ("constr","constr"), + (dummy_loc,ConstrArgType,Aentry ("constr","constr"), Some (Names.id_of_string "c"))]] (* Setting printer of unbound global reference *) diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index 46ba24da..6630be06 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -977,7 +977,6 @@ $$ \nlsep \TERM{Load}~\OPT{\TERM{Verbose}}~\NT{ident} \nlsep \TERM{Load}~\OPT{\TERM{Verbose}}~\NT{string} \nlsep \TERM{Declare}~\TERM{ML}~\TERM{Module}~\PLUS{\NT{string}} -\nlsep \TERM{Dump}~\TERM{Universes}~\OPT{\NT{string}} \nlsep \TERM{Locate}~\NT{locatable} \nlsep \TERM{Add}~\OPT{\TERM{Rec}}~\TERM{LoadPath}~\NT{string}~\OPT{\NT{as-dirpath}} \nlsep \TERM{Remove}~\TERM{LoadPath}~\NT{string} @@ -1179,8 +1178,6 @@ $$ \nlsep \TERM{Show}~\TERM{Intros} %% Correctness: obsolete ? %%\nlsep \TERM{Show}~\TERM{Programs} -\nlsep \TERM{Explain}~\TERM{Proof}~\OPT{\TERM{Tree}}~\STAR{\NT{num}} -%% Go not documented \nlsep \TERM{Hint}~\OPT{\TERM{Local}}~\NT{hint}~\OPT{\NT{inbases}} %% PrintConstr not documented \end{rules} |