From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- dev/base_include | 11 +- dev/db | 8 +- dev/doc/build-system.dev.txt | 61 ++++ dev/doc/changes.txt | 115 ++++++- dev/doc/debugging.txt | 13 +- dev/doc/naming-conventions.tex | 606 +++++++++++++++++++++++++++++++++ dev/doc/patch.ocaml-3.10.drop.rectypes | 31 ++ dev/doc/perf-analysis | 8 + dev/doc/versions-history.tex | 351 +++++++++++++++++++ dev/include | 9 +- dev/ocamldebug-coq.template | 18 +- dev/ocamlopt_shared_os5fix.sh | 29 ++ dev/ocamlweb-doc/Makefile | 16 +- dev/ocamlweb-doc/ast.ml | 4 +- dev/ocamlweb-doc/lex.mll | 4 +- dev/ocamlweb-doc/parse.ml | 2 +- dev/printers.mllib | 133 ++++++++ dev/top_printers.ml | 147 ++++---- dev/v8-syntax/syntax-v8.tex | 18 +- dev/vm_printers.ml | 22 +- 20 files changed, 1484 insertions(+), 122 deletions(-) create mode 100644 dev/doc/naming-conventions.tex create mode 100644 dev/doc/patch.ocaml-3.10.drop.rectypes create mode 100644 dev/doc/versions-history.tex create mode 100755 dev/ocamlopt_shared_os5fix.sh create mode 100644 dev/printers.mllib (limited to 'dev') diff --git a/dev/base_include b/dev/base_include index 711dcb2a..3a31230f 100644 --- a/dev/base_include +++ b/dev/base_include @@ -53,6 +53,7 @@ open Names open Term open Typeops +open Term_typing open Univ open Inductive open Indtypes @@ -89,6 +90,7 @@ open Evarutil open Tacred open Evd open Termops +open Namegen open Indrec open Typing open Inductiveops @@ -105,6 +107,8 @@ open Ppextend open Reserve open Syntax_def open Topconstr +open Prettyp +open Search open Clenvtac open Evar_refiner @@ -137,10 +141,15 @@ open Refine open Tacinterp open Tacticals open Tactics +open Eqschemes open Cerrors open Class open Command +open Indschemes +open Ind_tables +open Auto_ind_decl +open Lemmas open Coqinit open Coqtop open Discharge @@ -180,7 +189,7 @@ let constr_of_string s = open Declarations;; let constbody_of_string s = - let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_sp (path_of_string s))) in + let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_string s)) in Option.get b.const_body;; (* Get the current goal *) diff --git a/dev/db b/dev/db index 81878570..22b76605 100644 --- a/dev/db +++ b/dev/db @@ -3,14 +3,15 @@ load_printer "printers.cma" install_printer Top_printers.ppid install_printer Top_printers.ppidset +install_printer Top_printers.ppevarsubst install_printer Top_printers.ppintset install_printer Top_printers.pplab -install_printer Top_printers.ppmsid install_printer Top_printers.ppmbid install_printer Top_printers.ppdir install_printer Top_printers.ppmp install_printer Top_printers.ppkn install_printer Top_printers.ppcon +install_printer Top_printers.ppmind install_printer Top_printers.ppsp install_printer Top_printers.ppqualid install_printer Top_printers.ppclindex @@ -31,7 +32,6 @@ install_printer Top_printers.ppgoal install_printer Top_printers.ppsigmagoal install_printer Top_printers.pproof install_printer Top_printers.ppmetas -install_printer Top_printers.ppevd install_printer Top_printers.ppevm install_printer Top_printers.ppclenv @@ -39,5 +39,5 @@ 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 diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index c825f088..d4014303 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -12,6 +12,7 @@ see build-system.txt . happy only. To ensure they are not used for compilation, they contain invalid OCaml. + multi-stage build ----------------- @@ -37,6 +38,7 @@ Le Makefile a été séparé en plusieurs fichiers : The build needs to be cut in stages because make will not take into account one include when making another include. + Parallélisation --------------- @@ -68,3 +70,62 @@ d'étape pour chaque fichier: Mais seule la première est gérée explicitement, la seconde est implicite. + + +FIND_VCS_CLAUSE +--------------- + +The recommended style of using FIND_VCS_CLAUSE is for example + + find . $(FIND_VCS_CLAUSE) '(' -name '*.example' ')' -print + find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -or -name '*.foo' ')' -print + +1) +The parentheses even in the one-criteria case is so that if one adds +other conditions, e.g. change the first example to the second + + find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print + +one is not tempted to write + + find . $(FIND_VCS_CLAUSE) -name '*.example' -and -not -name '*.bak.example' -print + +because this will not necessarily work as expected; $(FIND_VCS_CLAUSE) +ends with an -or, and how it combines with what comes later depends on +operator precedence and all that. Much safer to override it with +parentheses. + +In short, it protects against the -or one doesn't see. + +2) +As to the -print at the end, yes it is necessary. Here's why. + +You are used to write: + find . -name '*.example' +and it works fine. But the following will not: + find . $(FIND_VCS_CLAUSE) -name '*.example' +it will also list things directly matched by FIND_VCS_CLAUSE +(directories we want to prune, in which we don't want to find +anything). C'est subtil... Il y a effectivement un -print implicite à +la fin, qui fait que la commande habituelle sans print fonctionne +bien, mais dès que l'on introduit d'autres commandes dans le lot (le +-prune de FIND_VCS_CLAUSE), ça se corse à cause d'histoires de +parenthèses du -print implicite par rapport au parenthésage dans la +forme recommandée d'utilisation: + +Si on explicite le -print et les parenthèses implicites, cela devient: + +find . '(' '(' '(' -name .git -or -name debian ')' -prune ')' -or \ + '(' -name '*.example' ')' + ')' + -print + +Le print agit TOUT ce qui précède, soit sur ce qui matche "'(' -name +.git -or -name debian ')'" ET sur ce qui matche "'(' -name '*.example' ')'". + +alors qu'ajouter le print explicite change cela en + +find . '(' '(' -name .git -or -name debian ')' -prune ')' -or \ + '(' '(' -name '*.example' ')' -print ')' + +Le print n'agit plus que sur ce qui matche "'(' -name '*.example' ')'" diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index cae948a0..91255202 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,3 +1,113 @@ +========================================= += CHANGES BETWEEN COQ V8.2 AND COQ V8.3 = +========================================= + +** Light cleaning in evarutil.ml ** + +whd_castappevar is now whd_head_evar +obsolete whd_ise disappears + +** Semantical change of h_induction_destruct ** + +Warning, the order of the isrec and evar_flag was inconsistent and has +been permuted. Tactic induction_destruct in tactics.ml is unchanged. + +** Internal tactics renamed + +There is no more difference between bindings and ebindings. The +following tactics are therefore renamed + +apply_with_ebindings_gen -> apply_with_bindings_gen +left_with_ebindings -> left_with_bindings +right_with_ebindings -> right_with_bindings +split_with_ebindings -> split_with_bindings + +and the following tactics are removed + +apply_with_ebindings (use instead apply_with_bindings) +eapply_with_ebindings (use instead eapply_with_bindings) + +** Obsolete functions in typing.ml + +For mtype_of, msort_of, mcheck, now use type_of, sort_of, check + +** Renaming functions renamed + +concrete_name -> compute_displayed_name_in +concrete_let_name -> compute_displayed_let_name_in +rename_rename_bound_var -> rename_bound_vars_as_displayed +lookup_name_as_renamed -> lookup_name_as_displayed +next_global_ident_away true -> next_ident_away_in_goal +next_global_ident_away false -> next_global_ident_away + +** Cleaning in commmand.ml + +Functions about starting/ending a lemma are in lemmas.ml +Functions about inductive schemes are in indschemes.ml + +Functions renamed: + +declare_one_assumption -> declare_assumption +declare_assumption -> declare_assumptions +Command.syntax_definition -> Metasyntax.add_syntactic_definition +declare_interning_data merged with add_notation_interpretation +compute_interning_datas -> compute_full_internalization_env +implicits_env -> internalization_env +full_implicits_env -> full_internalization_env +build_mutual -> do_mutual_inductive +build_recursive -> do_fixpoint +build_corecursive -> do_cofixpoint +build_induction_scheme -> build_mutual_induction_scheme +build_indrec -> build_induction_scheme +instantiate_type_indrec_scheme -> weaken_sort_scheme +instantiate_indrec_scheme -> modify_sort_scheme +make_case_dep, make_case_nodep -> build_case_analysis_scheme +make_case_gen -> build_case_analysis_scheme_default + +Types: + +decl_notation -> decl_notation option + +** Cleaning in libnames/nametab interfaces + +Functions: + +dirpath_prefix -> pop_dirpath +extract_dirpath_prefix pop_dirpath_n +extend_dirpath -> add_dirpath_suffix +qualid_of_sp -> qualid_of_path +pr_sp -> pr_path +make_short_qualid -> qualid_of_ident +sp_of_syntactic_definition -> path_of_syntactic_definition +sp_of_global -> path_of_global +id_of_global -> basename_of_global +absolute_reference -> global_of_path +locate_syntactic_definition -> locate_syndef +path_of_syntactic_definition -> path_of_syndef +push_syntactic_definition -> push_syndef + +Types: + +section_path -> full_path + +** Cleaning in parsing extensions (commit 12108) + +Many moves and renamings, one new file (Extrawit, that contains wit_tactic). + +** Cleaning in tactical.mli + +tclLAST_HYP -> onLastHyp +tclLAST_DECL -> onLastDecl +tclLAST_NHYPS -> onNLastHypsId +tclNTH_DECL -> onNthDecl +tclNTH_HYP -> onNthHyp +onLastHyp -> onLastHypId +onNLastHyps -> onNLastDecls +onClauses -> onClause +allClauses -> allHypsAndConcl + ++ removal of various unused combinators on type "clause" + ========================================= = CHANGES BETWEEN COQ V8.1 AND COQ V8.2 = ========================================= @@ -8,7 +118,8 @@ A few differences in Coq ML interfaces between Coq V8.1 and V8.2 ** Datatypes List of occurrences moved from "int list" to "Termops.occurrences" (an -alias to "bool * int list"). + alias to "bool * int list") +ETIdent renamed to ETName ** Functions @@ -325,7 +436,7 @@ Proof_type: subproof field in type proof_tree glued with the ref field Tacmach: no more echo from functions of module Refiner -Files contrib/*/g_*.ml4 take the place of files contrib/*/*.v. +Files plugins/*/g_*.ml4 take the place of files plugins/*/*.v. Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd VERNAC COMMAND EXTEND macros File syntax/PPTactic.v moved to parsing/pptactic.ml diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt index e5c83139..50b3b45c 100644 --- a/dev/doc/debugging.txt +++ b/dev/doc/debugging.txt @@ -4,8 +4,8 @@ Debugging from Coq toplevel using Caml trace mechanism 1. Launch bytecode version of Coq (coqtop.byte or coqtop -byte) 2. Access Ocaml toplevel using vernacular command 'Drop.' 3. Install load paths and pretty printers for terms, idents, ... using - Ocaml command '#use "base_include";;' (use '#use "include";;' for a rawer - term pretty printer) + Ocaml command '#use "base_include";;' (use '#use "include";;' for + installing the advanced term pretty printers) 4. Use #trace to tell which function(s) to trace 5. Go back to Coq toplevel with 'go();;' 6. Test your Coq command and observe the result of tracing your functions @@ -15,6 +15,15 @@ Debugging from Coq toplevel using Caml trace mechanism notations, ...), use "Set Printing All". It will affect the #trace printers too. +Note for Ocaml 3.10.x: Ocaml 3.10.x requires that modules compiled +with -rectypes are loaded in an environment with -rectypes set but +there is no way to tell the toplevel to support -rectypes. To make it +works, use "patch -p0 < dev/doc/patch.ocaml-3.10.drop.rectypes" to +hack script/coqmktop.ml, then recompile coqtop.byte. The procedure +above then works as soon as coqtop.byte is called with at least one +argument (add neutral option -byte to ensure at least one argument). + + Debugging from Caml debugger ============================ diff --git a/dev/doc/naming-conventions.tex b/dev/doc/naming-conventions.tex new file mode 100644 index 00000000..e7c8975b --- /dev/null +++ b/dev/doc/naming-conventions.tex @@ -0,0 +1,606 @@ +\documentclass[a4paper]{article} +\usepackage{fullpage} +\usepackage[latin1]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{amsfonts} + +\parindent=0pt +\parskip=10pt + +%%%%%%%%%%%%% +% Macros +\newcommand\itemrule[3]{ +\subsubsection{#1} +\begin{quote} +\begin{tt} +#3 +\end{tt} +\end{quote} +\begin{quote} +Name: \texttt{#2} +\end{quote}} + +\newcommand\formula[1]{\begin{tt}#1\end{tt}} +\newcommand\tactic[1]{\begin{tt}#1\end{tt}} +\newcommand\command[1]{\begin{tt}#1\end{tt}} +\newcommand\term[1]{\begin{tt}#1\end{tt}} +\newcommand\library[1]{\texttt{#1}} +\newcommand\name[1]{\texttt{#1}} + +\newcommand\zero{\texttt{zero}} +\newcommand\op{\texttt{op}} +\newcommand\opPrime{\texttt{op'}} +\newcommand\opSecond{\texttt{op''}} +\newcommand\phimapping{\texttt{phi}} +\newcommand\D{\texttt{D}} +\newcommand\elt{\texttt{elt}} +\newcommand\rel{\texttt{rel}} +\newcommand\relp{\texttt{rel'}} + +%%%%%%%%%%%%% + +\begin{document} + +\begin{center} +\begin{huge} +Proposed naming conventions for the Coq standard library +\end{huge} +\end{center} +\bigskip + +The following document describes a proposition of canonical naming +schemes for the Coq standard library. Obviously and unfortunately, the +current state of the library is not as homogeneous as it would be if +it would systematically follow such a scheme. To tend in this +direction, we however recommend to follow the following suggestions. + +\tableofcontents + +\section{General conventions} + +\subsection{Variable names} + +\begin{itemize} + +\item Variables are preferably quantified at the head of the + statement, even if some premisses do not depend of one of them. For + instance, one would state +\begin{quote} +\begin{tt} + {forall x y z:D, x <= y -> x+z <= y+z} +\end{tt} +\end{quote} +and not +\begin{quote} +\begin{tt} + {forall x y:D, x <= y -> forall z:D, x+z <= y+z} +\end{tt} +\end{quote} + +\item Variables are preferably quantified (and named) in the order of + ``importance'', then of appearance, from left to right, even if + for the purpose of some tactics it would have been more convenient + to have, say, the variables not occurring in the conclusion + first. For instance, one would state +\begin{quote} +\begin{tt} + {forall x y z:D, x+z <= y+z -> x <= y} +\end{tt} +\end{quote} +and not +\begin{quote} +\begin{tt} + {forall z x y:D, x+z <= y+z -> x <= y} +\end{tt} +\end{quote} +nor +\begin{quote} +\begin{tt} + {forall x y z:D, y+x <= z+x -> y <= z} +\end{tt} +\end{quote} + +\item Choice of effective names is domain-dependent. For instance, on + natural numbers, the convention is to use the variables $n$, $m$, + $p$, $q$, $r$, $s$ in this order. + + On generic domains, the convention is to use the letters $x$, $y$, + $z$, $t$. When more than three variables are needed, indexing variables + + It is conventional to use specific names for variables having a + special meaning. For instance, $eps$ or $\epsilon$ can be used to + denote a number intended to be as small as possible. Also, $q$ and + $r$ can be used to denote a quotient and a rest. This is good + practice. + +\end{itemize} + +\subsection{Disjunctive statements} + +A disjunctive statement with a computational content will be suffixed +by \name{\_inf}. For instance, if + +\begin{quote} +\begin{tt} +{forall x y, op x y = zero -> x = zero \/ y = zero} +\end{tt} +\end{quote} +has name \texttt{D\_integral}, then +\begin{quote} +\begin{tt} +{forall x y, op x y = zero -> \{x = zero\} + \{y = zero\}} +\end{tt} +\end{quote} +will have name \texttt{D\_integral\_inf}. + +As an exception, decidability statements, such as +\begin{quote} +\begin{tt} +{forall x y, \{x = y\} + \{x <> y\}} +\end{tt} +\end{quote} +will have a named ended in \texttt{\_dec}. Idem for cotransitivity +lemmas which are inherently computational that are ended in +\texttt{\_cotrans}. + +\subsection{Inductive types constructor names} + +As a general rule, constructor names start with the name of the +inductive type being defined as in \texttt{Inductive Z := Z0 : Z | + Zpos : Z -> Z | Zneg : Z -> Z} to the exception of very standard +types like \texttt{bool}, \texttt{nat}, \texttt{list}... + +For inductive predicates, constructor names also start with the name +of the notion being defined with one or more suffixes separated with +\texttt{\_} for discriminating the different cases as e.g. in + +\begin{verbatim} +Inductive even : nat -> Prop := + | even_O : even 0 + | even_S n : odd n -> even (S n) +with odd : nat -> Prop := + | odd_S n : even n -> odd (S n). +\end{verbatim} + +As a general rule, inductive predicate names should be lowercase (to +the exception of notions referring to a proper name, e.g. \texttt{Bezout}) +and multiple words must be separated by ``{\_}''. + +As an exception, when extending libraries whose general rule is that +predicates names start with a capital letter, the convention of this +library should be kept and the separation between multiple words is +done by making the initial of each work a capital letter (if one of +these words is a proper name, then a ``{\_}'' is added to emphasize +that the capital letter is proper and not an application of the rule +for marking the change of word). + +Inductive predicates that characterize the specification of a function +should be named after the function it specifies followed by +\texttt{\_spec} as in: + +\begin{verbatim} +Inductive nth_spec : list A -> nat -> A -> Prop := + | nth_spec_O a l : nth_spec (a :: l) 0 a + | nth_spec_S n a b l : nth_spec l n a -> nth_spec (b :: l) (S n) a. +\end{verbatim} + +\section{Equational properties of operations} + +\subsection{General conventions} + +If the conclusion is in the other way than listed below, add suffix +\name{\_reverse} to the lemma name. + +\subsection{Specific conventions} + +\itemrule{Associativity of binary operator {\op} on domain {\D}}{Dop\_assoc} +{forall x y z:D, op x (op y z) = op (op x y) z} + + Remark: Symmetric form: \name{Dop\_assoc\_reverse}: + \formula{forall x y z:D, op (op x y) z = op x (op y z)} + +\itemrule{Commutativity of binary operator {\op} on domain {\D}}{Dop\_comm} +{forall x y:D, op x y = op y x} + + Remark: Avoid \formula{forall x y:D, op y x = op x y}, or at worst, call it + \name{Dop\_comm\_reverse} + +\itemrule{Left neutrality of element elt for binary operator {\op}}{Dop\_elt\_l} +{forall x:D, op elt x = x} + + Remark: In English, ``{\elt} is an identity for {\op}'' seems to be + a more common terminology. + +\itemrule{Right neutrality of element elt for binary operator {\op}}{Dop\_elt\_r} +{forall x:D, op x elt = x} + + Remark: By convention, if the identities are reminiscent to zero or one, they + are written 1 and 0 in the name of the property. + +\itemrule{Left absorption of element elt for binary operator {\op}}{Dop\_elt\_l} +{forall x:D, op elt x = elt} + + Remarks: + \begin{itemize} + \item In French school, this property is named "elt est absorbant pour op" + \item English, the property seems generally named "elt is a zero of op" + \item In the context of lattices, this a boundedness property, it may + be called "elt is a bound on D", or referring to a (possibly + arbitrarily oriented) order "elt is a least element of D" or "elt + is a greatest element of D" + \end{itemize} + +\itemrule{Right absorption of element {\elt} for binary operator {\op}}{Dop\_elt\_l [BAD ??]} +{forall x:D, op x elt = elt} + +\itemrule{Left distributivity of binary operator {\op} over {\opPrime} on domain {\D}}{Dop\_op'\_distr\_l} +{forall x y z:D, op (op' x y) z = op' (op x z) (op y z)} + + Remark: Some authors say ``distribution''. + +\itemrule{Right distributivity of binary operator {\op} over {\opPrime} on domain {\D}}{Dop\_op'\_distr\_r} +{forall x y z:D, op z (op' x y) = op' (op z x) (op z y)} + + Remark: Note the order of arguments. + +\itemrule{Distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr} +{forall x y:D, op (op' x y) = op' (op x) (op y)} + +\itemrule{Distributivity of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr} +{forall x y:D, op (op' x y) = op' (op x) (op y)} + + Remark: For a non commutative operation with inversion of arguments, as in + \formula{forall x y z:D, op (op' x y) = op' (op y) (op y z)}, + we may probably still call the property distributivity since there + is no ambiguity. + + Example: \formula{forall n m : Z, -(n+m) = (-n)+(-m)}. + + Example: \formula{forall l l' : list A, rev (l++l') = (rev l)++(rev l')}. + +\itemrule{Left extrusion of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_l} +{forall x y:D, op (op' x y) = op' (op x) y} + + Question: Call it left commutativity ?? left swap ? + +\itemrule{Right extrusion of unary operator {\op} over binary op' on domain {\D}}{Dop\_op'\_distr\_r} +{forall x y:D, op (op' x y) = op' x (op y)} + +\itemrule{Idempotency of binary operator {\op} on domain {\D}}{Dop\_idempotent} +{forall x:D, op x n = x} + +\itemrule{Idempotency of unary operator {\op} on domain {\D}}{Dop\_idempotent} +{forall x:D, op (op x) = op x} + + Remark: This is actually idempotency of {\op} wrt to composition and + identity. + +\itemrule{Idempotency of element elt for binary operator {\op} on domain {\D}}{Dop\_elt\_idempotent} +{op elt elt = elt} + + Remark: Generally useless in CIC for concrete, computable operators + + Remark: The general definition is ``exists n, iter n op x = x''. + +\itemrule{Nilpotency of element elt wrt a ring D with additive neutral +element {\zero} and multiplicative binary operator +{\op}}{Delt\_nilpotent} +{op elt elt = zero} + + Remark: We leave the ring structure of D implicit; the general definition is ``exists n, iter n op elt = zero''. + +\itemrule{Zero-product property in a ring D with additive neutral +element {\zero} and multiplicative binary operator +{\op}}{D\_integral} +{forall x y, op x y = zero -> x = zero \/ y = zero} + + Remark: We leave the ring structure of D implicit; the Coq library + uses either \texttt{\_is\_O} (for \texttt{nat}), \texttt{\_integral} + (for \texttt{Z}, \texttt{Q} and \texttt{R}), \texttt{eq\_mul\_0} (for + \texttt{NZ}). + + Remark: The French school says ``integrité''. + +\itemrule{Nilpotency of binary operator {\op} wrt to its absorbing element +zero in D}{Dop\_nilpotent} {forall x, op x x = zero} + + Remark: Did not find this definition on the web, but it used in + the Coq library (to characterize \name{xor}). + +\itemrule{Involutivity of unary op on D}{Dop\_involutive} +{forall x:D, op (op x) = x} + +\itemrule{Absorption law on the left for binary operator {\op} over binary operator {\op}' on the left}{Dop\_op'\_absorption\_l\_l} +{forall x y:D, op x (op' x y) = x} + +\itemrule{Absorption law on the left for binary operator {\op} over binary operator {\op}' on the right}{Dop\_op'\_absorption\_l\_r} +{forall x y:D, op x (op' y x) = x} + + Remark: Similarly for \name{Dop\_op'\_absorption\_r\_l} and \name{Dop\_op'\_absorption\_r\_r}. + +\itemrule{De Morgan law's for binary operators {\opPrime} and {\opSecond} wrt +to unary op on domain {\D}}{Dop'\_op''\_de\_morgan, +Dop''\_op'\_de\_morgan ?? \mbox{leaving the complementing operation +implicit})} +{forall x y:D, op (op' x y) = op'' (op x) (op y)\\ +forall x y:D, op (op'' x y) = op' (op x) (op y)} + +\itemrule{Left complementation of binary operator {\op} by means of unary {\opPrime} wrt neutral element {\elt} of {\op} on domain {\D}}{Dop\_op'\_opp\_l} +{forall x:D, op (op' x) x = elt} + +Remark: If the name of the opposite function is reminiscent of the +notion of complement (e.g. if it is called \texttt{opp}), one can +simply say {Dop\_opp\_l}. + +\itemrule{Right complementation of binary operator {\op} by means of unary {\op'} wrt neutral element {\elt} of {\op} on domain {\D}}{Dop\_opp\_r} +{forall x:D, op x (op' x) = elt} + +Example: \formula{Radd\_opp\_l: forall r : R, - r + r = 0} + +\itemrule{Associativity of binary operators {\op} and {\op'}}{Dop\_op'\_assoc} +{forall x y z, op x (op' y z) = op (op' x y) z} + +Example: \formula{forall x y z, x + (y - z) = (x + y) - z} + +\itemrule{Right extrusion of binary operator {\opPrime} over binary operator {\op}}{Dop\_op'\_extrusion\_r} +{forall x y z, op x (op' y z) = op' (op x y) z} + +Remark: This requires {\op} and {\opPrime} to have their right and left +argument respectively and their return types identical. + +Example: \formula{forall x y z, x + (y - z) = (x + y) - z} + +Remark: Other less natural combinations are possible, such +as \formula{forall x y z, op x (op' y z) = op' y (op x z)}. + +\itemrule{Left extrusion of binary operator {\opPrime} over binary operator {\op}}{Dop\_op'\_extrusion\_l} +{forall x y z, op (op' x y) z = op' x (op y z)} + +Remark: Operations are not necessarily internal composition laws. It +is only required that {\op} and {\opPrime} have their right and left +argument respectively and their return type identical. + +Remark: When the type are heterogeneous, only one extrusion law is possible and it can simply be named {Dop\_op'\_extrusion}. + +Example: \formula{app\_cons\_extrusion : forall a l l', (a :: l) ++ l' = a :: (l ++ l')}. + +%====================================================================== +%\section{Properties of elements} + +%Remark: Not used in current library + + + +%====================================================================== +\section{Preservation and compatibility properties of operations} + +\subsection{With respect to equality} + +\itemrule{Injectivity of unary operator {\op}}{Dop\_inj} +{forall x y:D, op x = op y -> x = y} + +\itemrule{Left regularity of binary operator {\op}}{Dop\_reg\_l, Dop\_inj\_l, or Dop\_cancel\_l} +{forall x y z:D, op z x = op z y -> x = y} + + Remark: Note the order of arguments. + + Remark: The Coq usage is to called it regularity but the English + standard seems to be cancellation. The recommended form is not + decided yet. + + Remark: Shall a property like $n^p \leq n^q \rightarrow p \leq q$ + (for $n\geq 1$) be called cancellation or should it be reserved for + operators that have an inverse? + +\itemrule{Right regularity of binary operator {\op}}{Dop\_reg\_r, Dop\_inj\_r, Dop\_cancel\_r} +{forall x y z:D, op x z = op y z -> x = y} + +\subsection{With respect to a relation {\rel}} + +\itemrule{Compatibility of unary operator {\op}}{Dop\_rel\_compat} +{forall x y:D, rel x y -> rel (op x) (op y)} + +\itemrule{Left compatibility of binary operator {\op}}{Dop\_rel\_compat\_l} +{forall x y z:D, rel x y -> rel (op z x) (op z y)} + +\itemrule{Right compatibility of binary operator {\op}}{Dop\_rel\_compat\_r} +{forall x y z:D, rel x y -> rel (op x z) (op y z)} + + Remark: For equality, use names of the form \name{Dop\_eq\_compat\_l} or + \name{Dop\_eq\_compat\_r} +(\formula{forall x y z:D, y = x -> op y z = op x z} and +\formula{forall x y z:D, y = x -> op y z = op x z}) + + Remark: Should we admit (or even prefer) the name + \name{Dop\_rel\_monotone}, \name{Dop\_rel\_monotone\_l}, + \name{Dop\_rel\_monotone\_r} when {\rel} is an order ? + +\itemrule{Left regularity of binary operator {\op}}{Dop\_rel\_reg\_l} +{forall x y z:D, rel (op z x) (op z y) -> rel x y} + +\itemrule{Right regularity of binary operator {\op}}{Dop\_rel\_reg\_r} +{forall x y z:D, rel (op x z) (op y z) -> rel x y} + + Question: Would it be better to have \name{z} as first argument, since it + is missing in the conclusion ?? (or admit we shall use the options + ``\texttt{with p}''?) + +\itemrule{Left distributivity of binary operator {\op} over {\opPrime} along relation {\rel} on domain {\D}}{Dop\_op'\_rel\_distr\_l} +{forall x y z:D, rel (op (op' x y) z) (op' (op x z) (op y z))} + + Example: standard property of (not necessarily distributive) lattices + + Remark: In a (non distributive) lattice, by swapping join and meet, + one would like also, +\formula{forall x y z:D, rel (op' (op x z) (op y z)) (op (op' x y) z)}. + How to name it with a symmetric name (use + \name{Dop\_op'\_rel\_distr\_mon\_l} and + \name{Dop\_op'\_rel\_distr\_anti\_l})? + +\itemrule{Commutativity of binary operator {\op} along (equivalence) relation {\rel} on domain {\D}}{Dop\_op'\_rel\_comm} +{forall x y z:D, rel (op x y) (op y x)} + + Example: +\formula{forall l l':list A, Permutation (l++l') (l'++l)} + +\itemrule{Irreducibility of binary operator {\op} on domain {\D}}{Dop\_irreducible} +{forall x y z:D, z = op x y -> z = x $\backslash/$ z = y} + + Question: What about the constructive version ? Call it \name{Dop\_irreducible\_inf} ? +\formula{forall x y z:D, z = op x y -> \{z = x\} + \{z = y\}} + +\itemrule{Primality of binary operator {\op} along relation {\rel} on domain {\D}}{Dop\_rel\_prime} +{forall x y z:D, rel z (op x y) -> rel z x $\backslash/$ rel z y} + + +%====================================================================== +\section{Morphisms} + +\itemrule{Morphism between structures {\D} and {\D'}}{\name{D'\_of\_D}}{D -> D'} + +Remark: If the domains are one-letter long, one can used \texttt{IDD'} as for +\name{INR} or \name{INZ}. + +\itemrule{Morphism {\phimapping} mapping unary operators {\op} to {\op'}}{phi\_op\_op', phi\_op\_op'\_morphism} +{forall x:D, phi (op x) = op' (phi x)} + +Remark: If the operators have the same name in both domains, one use +\texttt{D'\_of\_D\_op} or \texttt{IDD'\_op}. + +Example: \formula{Z\_of\_nat\_mult: forall n m : nat, Z\_of\_nat (n * m) = (Z\_of\_nat n * Z\_of\_nat m)\%Z}. + +Remark: If the operators have different names on distinct domains, one +can use \texttt{op\_op'}. + +\itemrule{Morphism {\phimapping} mapping binary operators {\op} to +{\op'}}{phi\_op\_op', phi\_op\_op'\_morphism} {forall +x y:D, phi (op x y) = op' (phi x) (phi y)} + +Remark: If the operators have the same name in both domains, one use +\texttt{D'\_of\_D\_op} or \texttt{IDD'\_op}. + +Remark: If the operators have different names on distinct domains, one +can use \texttt{op\_op'}. + +\itemrule{Morphism {\phimapping} mapping binary operator {\op} to +binary relation {\rel}}{phi\_op\_rel, phi\_op\_rel\_morphism} +{forall x y:D, phi (op x y) <-> rel (phi x) (phi y)} + +Remark: If the operator and the relation have similar name, one uses +\texttt{phi\_op}. + +Question: How to name each direction? (add \_elim for -> and \_intro +for <- ?? -- as done in Bool.v ??) + +Example: \formula{eq\_true\_neg: \~{} eq\_true b <-> eq\_true (negb b)}. + +%====================================================================== +\section{Preservation and compatibility properties of operations wrt order} + +\itemrule{Compatibility of binary operator {\op} wrt (strict order) {\rel} and (large order) {\rel'}}{Dop\_rel\_rel'\_compat} +{forall x y z t:D, rel x y -> rel' z t -> rel (op x z) (op y t)} + +\itemrule{Compatibility of binary operator {\op} wrt (large order) {\relp} and (strict order) {\rel}}{Dop\_rel'\_rel\_compat} +{forall x y z t:D, rel' x y -> rel z t -> rel (op x z) (op y t)} + + +%====================================================================== +\section{Properties of relations} + +\itemrule{Reflexivity of relation {\rel} on domain {\D}}{Drel\_refl} +{forall x:D, rel x x} + +\itemrule{Symmetry of relation {\rel} on domain {\D}}{Drel\_sym} +{forall x y:D, rel x y -> rel y x} + +\itemrule{Transitivity of relation {\rel} on domain {\D}}{Drel\_trans} +{forall x y z:D, rel x y -> rel y z -> rel x z} + +\itemrule{Antisymmetry of relation {\rel} on domain {\D}}{Drel\_antisym} +{forall x y:D, rel x y -> rel y x -> x = y} + +\itemrule{Irreflexivity of relation {\rel} on domain {\D}}{Drel\_irrefl} +{forall x:D, \~{} rel x x} + +\itemrule{Asymmetry of relation {\rel} on domain {\D}}{Drel\_asym} +{forall x y:D, rel x y -> \~{} rel y x} + +\itemrule{Cotransitivity of relation {\rel} on domain {\D}}{Drel\_cotrans} +{forall x y z:D, rel x y -> \{rel z y\} + \{rel x z\}} + +\itemrule{Linearity of relation {\rel} on domain {\D}}{Drel\_trichotomy} +{forall x y:D, \{rel x y\} + \{x = y\} + \{rel y x\}} + + Questions: Or call it \name{Drel\_total}, or \name{Drel\_linear}, or + \name{Drel\_connected}? Use + $\backslash/$ ? or use a ternary sumbool, or a ternary disjunction, + for nicer elimination. + +\itemrule{Informative decidability of relation {\rel} on domain {\D}}{Drel\_dec (or Drel\_dect, Drel\_dec\_inf ?)} +{forall x y:D, \{rel x y\} + \{\~{} rel x y\}} + + Remark: If equality: \name{D\_eq\_dec} or \name{D\_dec} (not like + \name{eq\_nat\_dec}) + +\itemrule{Non informative decidability of relation {\rel} on domain {\D}}{Drel\_dec\_prop (or Drel\_dec)} +{forall x y:D, rel x y $\backslash/$ \~{} rel x y} + +\itemrule{Inclusion of relation {\rel} in relation {\rel}' on domain {\D}}{Drel\_rel'\_incl (or Drel\_incl\_rel')} +{forall x y:D, rel x y -> rel' x y} + + Remark: Use \name{Drel\_rel'\_weak} for a strict inclusion ?? + +%====================================================================== +\section{Relations between properties} + +\itemrule{Equivalence of properties \texttt{P} and \texttt{Q}}{P\_Q\_iff} +{forall x1 .. xn, P <-> Q} + + Remark: Alternatively use \name{P\_iff\_Q} if it is too difficult to + recover what pertains to \texttt{P} and what pertains to \texttt{Q} + in their concatenation (as e.g. in + \texttt{Godel\_Dummett\_iff\_right\_distr\_implication\_over\_disjunction}). + +%====================================================================== +\section{Arithmetical conventions} + +\begin{minipage}{6in} +\renewcommand{\thefootnote}{\thempfootnote} % For footnotes... +\begin{tabular}{lll} +Zero on domain {\D} & D0 & (notation \verb=0=)\\ +One on domain {\D} & D1 (if explicitly defined) & (notation \verb=1=)\\ +Successor on domain {\D} & Dsucc\\ +Predessor on domain {\D} & Dpred\\ +Addition on domain {\D} & Dadd/Dplus\footnote{Coq historically uses \texttt{plus} and \texttt{mult} for addition and multiplication which are inconsistent notations, the recommendation is to use \texttt{add} and \texttt{mul} except in existng libraries that already use \texttt{plus} and \texttt{mult}} + & (infix notation \verb=+= [50,L])\\ +Multiplication on domain {\D} & Dmul/Dmult\footnotemark[\value{footnote}] & (infix notation \verb=*= [40,L]))\\ +Soustraction on domain {\D} & Dminus & (infix notation \verb=-= [50,L])\\ +Opposite on domain {\D} & Dopp (if any) & (prefix notation \verb=-= [35,R]))\\ +Inverse on domain {\D} & Dinv (if any) & (prefix notation \verb=/= [35,R]))\\ +Power on domain {\D} & Dpower & (infix notation \verb=^= [30,R])\\ +Minimal element on domain {\D} & Dmin\\ +Maximal element on domain {\D} & Dmax\\ +Large less than order on {\D} & Dle & (infix notations \verb!<=! and \verb!>=! [70,N]))\\ +Strict less than order on {\D} & Dlt & (infix notations \verb=<= and \verb=>= [70,N]))\\ +\end{tabular} +\bigskip +\end{minipage} + +\bigskip + +The status of \verb!>=! and \verb!>! is undecided yet. It will eithet +be accepted only as parsing notations or may also accepted as a {\em + definition} for the \verb!<=! and \verb!= 4 & ++ String.sub (Sys.ocaml_version) 0 4 = \"3.10\" ++ then ++ (* ocaml 3.10 does not have #rectypes but needs it *) ++ (* simulate a call with option -rectypes before *) ++ (* jumping to the ocaml toplevel *) ++ for i = 1 to Array.length Sys.argv - 1 do ++ Sys.argv.(i) <- \"-rectypes\" ++ done ++ else ++ () in ++ + Mltop.set_top + {Mltop.load_obj= + (fun f -> if not (Topdirs.load_file ppf f) then failwith \"error\"); + Mltop.use_file=Topdirs.dir_use ppf; + Mltop.add_dir=Topdirs.dir_directory; +- Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n" ++ Mltop.ml_loop=(fun () -> set_rectypes_hack(); Topmain.main()) };;\n" + + (* create a temporary main file to link *) + let create_tmp_main_file modules = diff --git a/dev/doc/perf-analysis b/dev/doc/perf-analysis index 8e481544..d23bf835 100644 --- a/dev/doc/perf-analysis +++ b/dev/doc/perf-analysis @@ -1,6 +1,14 @@ Performance analysis (trunk repository) --------------------------------------- +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 + May 21, 2008: New version of CoRN (needs +84% more time to compile) diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex new file mode 100644 index 00000000..175297f9 --- /dev/null +++ b/dev/doc/versions-history.tex @@ -0,0 +1,351 @@ +\documentclass[a4paper]{book} +\usepackage{fullpage} +\usepackage[latin1]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{amsfonts} + +\newcommand{\feature}[1]{{\em #1}} + +\begin{document} + +\begin{center} +\begin{huge} +An history of Coq versions +\end{huge} +\end{center} +\bigskip + +\centerline{\large 1984-1989: The Calculus of Constructions} +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +version & date & comments \\ +\hline +CoC V1.10& mention of dates from 6 December & implementation language is Caml\\ + & 1984 to 13 February 1985 \\ + +CoC V1.11& mention of dates from 6 December\\ + & 1984 to 19 February 1985\\ + +CoC V2.13& dated 16 December 1985\\ + +CoC V2.13& dated 25 June 1986\\ + +CoC V3.1& dated 20 November 1986 & \feature{auto}\\ + +CoC V3.2& dated 27 November 1986\\ + +CoC V3.3 and V3.4& dated 1 January 1987 & creation of a directory for examples\\ + +CoC V4.1& dated 24 July 1987\\ + +CoC V4.2& dated 10 September 1987\\ + +CoC V4.3& dated 15 September 1987\\ + +CoC V4.4& dated 27 January 1988\\ + +CoC V4.5 and V4.5.5& dated 15 March 1988\\ + +CoC V4.6 and V4.7& dated 1 September 1988\\ + +CoC V4.8& dated 1 December 1988\\ + +CoC V4.8.5& dated 1 February 1989\\ + +CoC V4.9& dated 1 March 1989\\ + +CoC V4.10 and 4.10.1& dated 1 May 1989 & first public release - in English\\ +\end{tabular} + +\bigskip +\bigskip + +\newpage + +\centerline{\large 1989-now: The Calculus of Inductive Constructions} +\mbox{}\\ +\centerline{I- RCS archives in Caml and Caml-Light} +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +version & date & comments \\ +\hline +Coq V5.0 & headers dated 1 January 1990 & internal use \\ + & & \feature{inductive types with primitive recursor}\\ + +Coq V5.1 & ended 12 July 1990 & internal use \\ + +Coq V5.2 & log dated 4 October 1990 & internal use \\ + +Coq V5.3 & log dated 12 October 1990 & internal use \\ + +Coq V5.4 & headers dated 24 October 1990 & internal use, \feature{extraction} (version 1) [3-12-90]\\ + +Coq V5.5 & started 6 December 1990 & internal use \\ + +Coq V5.6 beta & 1991 & first announce of the new Coq based on CIC \\ + & & (in May at TYPES?)\\ + & & \feature{rewrite tactic}\\ + & & use of RCS at least from February 1991\\ + +Coq V5.6& 7 August 1991 & \\ + +Coq V5.6 patch 1& 13 November 1991 & \\ + +Coq V5.6 (last) & mention of 27 November 1992\\ + +Coq V5.7.0& 1992 & translation to Caml-Light \footnotemark\\ + +Coq V5.8& 12 February 1993 & \feature{Program} (version 1), \feature{simpl}\\ + +& & has the xcoq graphical interface\\ + +& & first explicit notion of standard library\\ + +& & includes a MacOS 7-9 version\\ + +Coq V5.8.1& released 28 April 1993 & with xcoq graphical interface and MacOS 7-9 support\\ + +Coq V5.8.2& released 9 July 1993 & with xcoq graphical interface and MacOS 7-9 support\\ + +Coq V5.8.3& released 6 December 1993 % Announce on coq-club + & with xcoq graphical interface and MacOS 7-9 support\\ + + & & 3 branches: Lyon (V5.8.x), Ulm (V5.10.x) and Rocq (V5.9)\\ + +Coq V5.9 alpha& 7 July 1993 & +experimental version based on evars refinement \\ + & & (merge from experimental ``V6.0'' and some pre-V5.8.3 \\ + & & version), not released\\ + +& March 1994 & \feature{tauto} tactic in V5.9 branch\\ + +Coq V5.9 & 27 January 1993 & experimental version based on evars refinement\\ + & & not released\\ +\end{tabular} + +\bigskip +\bigskip + +\footnotetext{archive lost?} + +\newpage + +\centerline{II- Starting with CVS archives in Caml-Light} +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +version & date & comments \\ +\hline +Coq V5.10 ``Murthy'' & 22 January 1994 & +introduction of the ``DOPN'' structure\\ + & & \feature{eapply/prolog} tactics\\ + & & private use of cvs on madiran.inria.fr\\ + +Coq V5.10.1 ``Murthy''& 15 April 1994 \\ + +Coq V5.10.2 ``Murthy''& 19 April 1994 & \feature{mutual inductive types, fixpoint} (from Lyon's branch)\\ + +Coq V5.10.3& 28 April 1994 \\ + +Coq V5.10.5& dated 13 May 1994 & \feature{inversion}, \feature{discriminate}, \feature{injection} \\ + & & \feature{type synthesis of hidden arguments}\\ + & & \feature{separate compilation}, \feature{reset mechanism} \\ + +Coq V5.10.6& dated 30 May 1994\\ +Coq Lyon's archive & in 1994 & cvs server set up on woodstock.ens-lyon.fr\\ + +Coq V5.10.9& announced on 17 August 1994 & + % Announced by Catherine Parent on coqdev + % Version avec une copie de THEORIES pour les inductifs mutuels + \\ + +Coq V5.10.11& announced on 2 February 1995 & \feature{compute}\\ +Coq Rocq's archive & on 16 February 1995 & set up of ``V5.10'' cvs archive on pauillac.inria.fr \\ + & & with first dispatch of files over src/* directories\\ + +Coq V5.10.12& dated 30 January 1995 & on Lyon's cvs\\ + +Coq V5.10.13& dated 9 June 1995 & on Lyon's cvs\\ + +Coq V5.10.14.OO& dated 30 June 1995 & on Lyon's cvs\\ + +Coq V5.10.14.a& announced 5 September 1995 & bug-fix release \\ % Announce on coq-club by BW + +Coq V5.10.14.b& released 2 October 1995 & bug-fix release\\ + & & MS-DOS version released on 30 October 1995\\ + % still available at ftp://ftp.ens-lyon.fr/pub/LIP/COQ/V5.10.14.old/ in May 2009 + % also known in /net/pauillac/constr archive as ``V5.11 old'' \\ + % A copy of Coq V5.10.15 dated 1 January 1996 coming from Lyon's CVS is + % known in /net/pauillac/constr archive as ``V5.11 new old'' \\ + +Coq V5.10.15 & released 20 February 1996 & \feature{Logic, Sorting, new Sets and Relations libraries} \\ + % Announce on coq-club by BW + % dated 15 February 1996 and bound to pauillac's cvs in /net/pauillac/constr archive + & & MacOS 7-9 version released on 1 March 1996 \\ % Announce on coq-club by BW + +Coq V5.11 & dated 1 March 1996 & not released, not in pauillac's CVS, \feature{eauto} \\ +\end{tabular} + +\bigskip +\bigskip + +\newpage + +\centerline{III- A CVS archive in Caml Special Light} +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +version & date & comments \\ +\hline +Coq ``V6'' archive & 20 March 1996 & new cvs repository on pauillac.inria.fr with code ported \\ + & & to Caml Special Light (to later become Objective Caml)\\ + & & has implicit arguments and coercions\\ + +Coq V6.1beta& released 18 November 1996 & \feature{coercions} [23-5-1996], \feature{user-level implicit arguments} [23-5-1996]\\ + & & \feature{omega} [10-9-1996] \\ + & & \feature{natural language proof printing} (stopped from Coq V7) [6-9-1996]\\ + & & \feature{pattern-matching compilation} [7-10-1996]\\ + & & \feature{ring} (version 1, ACSimpl) [11-12-1996]\\ + +Coq V6.1& released December 1996 & \\ + +Coq V6.2beta& released 30 January 1998 & % Announced on coq-club 2-2-1998 by CP + \feature{SearchIsos} (stopped from Coq V7) [9-11-1997]\\ + & & grammar extension mechanism moved to Camlp4 [12-6-1997]\\ + & & \feature{refine tactic}\\ + & & includes a Windows version\\ + +Coq V6.2& released 4 May 1998 & % Announced on coq-club 5-5-1998 by CP + \feature{ring} (version 2) [7-4-1998] \\ + +Coq V6.2.1& released 23 July 1998\\ + +Coq V6.2.2 beta& released 30 January 1998\\ + +Coq V6.2.2& released 23 September 1998\\ + +Coq V6.2.3& released 22 December 1998 & \feature{Real numbers library} [from 13-11-1998] \\ + +Coq V6.2.4& released 8 February 1999\\ + +Coq V6.3& released 27 July 1999 & \feature{autorewrite} [25-3-1999]\\ + & & \feature{Correctness} (deprecated in V8, led to Why) [28-10-1997]\\ + +Coq V6.3.1& released 7 December 1999\\ +\end{tabular} +\medskip +\bigskip + +\newpage +\centerline{IV- New CVS, back to a kernel-centric implementation} +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +version & date & comments \\ +\hline +Coq ``V7'' archive & August 1999 & new cvs archive based on J.-C. Filliâtre's \\ + & & \feature{kernel-centric} architecture \\ + & & more care for outside readers\\ + & & (indentation, ocaml warning protection)\\ +Coq V7.0beta& released 27 December 2000 & \feature{${\cal L}_{\mathit{tac}}$} \\ +Coq V7.0beta2& released 2 February 2001\\ + +Coq V7.0& released 25 April 2001 & \feature{extraction} (version 2) [6-2-2001] \\ + & & \feature{field} (version 1) [19-4-2001], \feature{fourier} [20-4-2001] \\ + +Coq V7.1& released 25 September 2001 & \feature{setoid rewriting} (version 1) [10-7-2001]\\ + +Coq V7.2& released 10 January 2002\\ + +Coq V7.3& released 16 May 2002\\ + +Coq V7.3.1& released 5 October 2002 & \feature{module system} [2-8-2002]\\ + & & \feature{pattern-matching compilation} (version 2) [13-6-2002]\\ + +Coq V7.4& released 6 February 2003 & \feature{notation}, \feature{scopes} [13-10-2002]\\ + +Coq V8.0& released 21 April 2004 & \feature{new concrete syntax}, \feature{Set predicative}, \feature{CoqIDE} [from 4-2-2003]\\ + +Coq V8.0pl1& released 18 July 2004\\ + +Coq V8.0pl2& released 22 January 2005\\ + +Coq V8.0pl3& released 13 January 2006\\ + +Coq V8.0pl4& released 26 January 2007\\ + +Coq ``svn'' archive & 6 March 2006 & cvs archive moved to subversion control management\\ + +Coq V8.1beta& released 12 July 2006 & \feature{bytecode compiler} [20-10-2004] \\ + & & \feature{setoid rewriting} (version 2) [3-9-2004]\\ + & & \feature{functional induction} [1-2-2006]\\ + & & \feature{Strings library} [8-2-2006], \feature{FSets/FMaps library} [15-3-2006] \\ + & & \feature{Program} (version 2, Russell) [5-3-2006] \\ + & & \feature{declarative language} [20-9-2006]\\ + & & \feature{ring} (version 3) [18-11-2005]\\ + +Coq V8.1gamma& released 7 November 2006 & \feature{field} (version 2) [29-9-2006]\\ + +Coq V8.1& released 10 February 2007 & \\ + +Coq V8.1pl1& released 27 July 2007 & \\ +Coq V8.1pl2& released 13 October 2007 & \\ +Coq V8.1pl3& released 13 December 2007 & \\ +Coq V8.1pl4& released 9 October 2008 & \\ + +Coq V8.2 beta1& released 13 June 2008 & \\ +Coq V8.2 beta2& released 19 June 2008 & \\ +Coq V8.2 beta3& released 27 June 2008 & \\ +Coq V8.2 beta4& released 8 August 2008 & \\ + +Coq V8.2 & released 17 February 2009 & \feature{type classes} [10-12-2007], \feature{machine words} [11-5-2007]\\ + & & \feature{big integers} [11-5-2007], \feature{abstract arithmetics} [9-2007]\\ + & & \feature{setoid rewriting} (version 3) [18-12-2007] \\ + & & \feature{micromega solving platform} [19-5-2008]\\ + +& & a first package released on +February 11 was incomplete\\ +\end{tabular} + +\medskip +\bigskip +\newpage + +\centerline{\large Other important dates} +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +version & date & comments \\ +\hline +Lechenadec's version in C& mention of \\ + & 13 January 1985 on \\ + & some vernacular files\\ +Set up of the coq-club mailing list & 28 July 1993\\ + +Coq V6.0 ``evars'' & & experimentation based on evars +refinement started \\ + & & in 1991 by Gilles from V5.6 beta,\\ + & & with work by Hugo in July 1992\\ + +Coq V6.0 ``evars'' ``light'' & July 1993 & Hugo's port of the first +evars-based experimentation \\ + & & to Coq V5.7, version from October/November +1992\\ + +CtCoq & released 25 October 1995 & first beta-version \\ % Announce on coq-club by Janet + +Proto with explicit substitutions & 1997 &\\ + +Coq web site & 15 April 1998 & new site designed by David Delahaye \\ + +Coq web site & January 2004 & web site new style \\ + & & designed by Julien Narboux and Florent Kirchner \\ + +Coq web site & April 2009 & new Drupal-based site \\ + & & designed by Jean-Marc Notin and Denis Cousineau \\ + +\end{tabular} + +\end{document} diff --git a/dev/include b/dev/include index ccb75edd..251a969b 100644 --- a/dev/include +++ b/dev/include @@ -1,12 +1,13 @@ (* File to include to install the pretty-printers in the ocaml toplevel *) -(* clflags.cmi (a ocaml compilation by-product) must be in the library path. +(* 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: #directory "+compiler-libs/utils";; + Clflags.recursive_types := true;; *) -(* Clflags.recursive_types := true;;*) #cd ".";; #use "base_include";; @@ -22,12 +23,13 @@ #install_printer (* type_judgement *) pptype;; #install_printer (* judgement *) ppj;; +#install_printer (* hint_db *) print_hint_db;; #install_printer (* goal *) ppgoal;; #install_printer (* sigma goal *) ppsigmagoal;; #install_printer (* proof *) pproof;; +#install_printer (* pftreestate *) pppftreestate;; #install_printer (* metaset.t *) ppmetas;; #install_printer (* evar_map *) ppevm;; -#install_printer (* evar_defs *) ppevd;; #install_printer (* clenv *) ppclenv;; #install_printer (* env *) ppenv;; @@ -37,4 +39,3 @@ #install_printer (* generic_argument *) pp_generic_argument;; #install_printer (* fconstr *) ppfconstr;; - diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template index 5f49561b..74320588 100644 --- a/dev/ocamldebug-coq.template +++ b/dev/ocamldebug-coq.template @@ -17,13 +17,15 @@ exec $OCAMLDEBUG \ -I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \ -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \ - -I $COQTOP/contrib/extraction -I $COQTOP/contrib/field \ - -I $COQTOP/contrib/fourier -I $COQTOP/contrib/firstorder \ - -I $COQTOP/contrib/interface -I $COQTOP/contrib/cc \ - -I $COQTOP/contrib/omega -I $COQTOP/contrib/romega \ - -I $COQTOP/contrib/ring -I $COQTOP/contrib/xml \ - -I $COQTOP/contrib/subtac -I $COQTOP/contrib/funind \ - -I $COQTOP/contrib/rtauto -I $COQTOP/contrib/setoid_ring \ - -I $COQTOP/contrib/recdef -I $COQTOP/contrib/dp \ + -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ + -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \ + -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \ + -I $COQTOP/plugins/funind -I $COQTOP/plugins/groebner \ + -I $COQTOP/plugins/interface -I $COQTOP/plugins/micromega \ + -I $COQTOP/plugins/omega -I $COQTOP/plugins/quote \ + -I $COQTOP/plugins/ring -I $COQTOP/plugins/romega \ + -I $COQTOP/plugins/rtauto -I $COQTOP/plugins/setoid_ring \ + -I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \ + -I $COQTOP/plugins/xml \ -I $COQTOP/ide \ $* diff --git a/dev/ocamlopt_shared_os5fix.sh b/dev/ocamlopt_shared_os5fix.sh new file mode 100755 index 00000000..f7d31ad8 --- /dev/null +++ b/dev/ocamlopt_shared_os5fix.sh @@ -0,0 +1,29 @@ +#/bin/sh + +### Temporary fix for production of .cmxs on MacOS 10.5 + +OCAMLOPT=$1 +CMXS=$2 + +DIR=`dirname $CMXS` +BASE=`basename $CMXS .cmxs` +CMXA=$DIR/$BASE.cmxa +ARC=$DIR/$BASE.a +# we assume that all object files are at the same place than the rest +OBJS=`ar t $ARC | sed -e "s|^|$DIR/|" | grep -v SYMDEF` + +$OCAMLOPT -dstartup -linkall -shared -o $CMXS $CMXA +# Fix1: add a dummy instruction before the caml generic functions +# Fix2: make all caml generic functions private +rm -f $CMXS $CMXS.startup.fixed.s +cat $CMXS.startup.s | sed \ + -e "s/_caml_shared_startup__code_begin:/_caml_shared_startup__code_begin: ret/" \ + -e "s/.globl _caml_curry/.private_extern _caml_curry/" \ + -e "s/.globl _caml_apply/.private_extern _caml_apply/" \ + -e "s/.globl _caml_tuplify/.private_extern _caml_tuplify/" \ + > $CMXS.startup.fixed.s +# Recompile fixed startup code +as -o $CMXS.startup.o $CMXS.startup.fixed.s +# Build fixed .cmxs (assume all object files are at the same place) +ld -bundle -flat_namespace -undefined warning -read_only_relocs suppress -o $CMXS $OBJS $CMXS.startup.o +rm $CMXS.startup.o $CMXS.startup.s $CMXS.startup.fixed.s \ No newline at end of file diff --git a/dev/ocamlweb-doc/Makefile b/dev/ocamlweb-doc/Makefile index f2c625ed..3189d7c5 100644 --- a/dev/ocamlweb-doc/Makefile +++ b/dev/ocamlweb-doc/Makefile @@ -4,14 +4,14 @@ 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 ../../contrib/omega -I ../../contrib/romega \ - -I ../../contrib/ring -I ../../contrib/dp -I ../../contrib/setoid_ring \ - -I ../../contrib/xml -I ../../contrib/extraction \ - -I ../../contrib/interface -I ../../contrib/fourier \ - -I ../../contrib/cc \ - -I ../../contrib/funind -I ../../contrib/firstorder \ - -I ../../contrib/field -I ../../contrib/subtac -I ../../contrib/rtauto \ - -I ../../contrib/recdef + -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) diff --git a/dev/ocamlweb-doc/ast.ml b/dev/ocamlweb-doc/ast.ml index 2153ef47..4eb135d8 100644 --- a/dev/ocamlweb-doc/ast.ml +++ b/dev/ocamlweb-doc/ast.ml @@ -22,7 +22,7 @@ type constr_ast = (string * binder list * constr_ast * string option * constr_ast) list * string | Match of case_item list * constr_ast option * - (pattern list * constr_ast) list + (pattern list * constr_ast) list and red_fun = Simpl @@ -34,7 +34,7 @@ and fix_kind = Fix | CoFix and case_item = constr_ast * (string option * constr_ast option) -and pattern = +and pattern = PatAs of pattern * string | PatType of pattern * constr_ast | PatConstr of string * pattern list diff --git a/dev/ocamlweb-doc/lex.mll b/dev/ocamlweb-doc/lex.mll index 617163e7..059526d9 100644 --- a/dev/ocamlweb-doc/lex.mll +++ b/dev/ocamlweb-doc/lex.mll @@ -7,7 +7,7 @@ let comment_depth = ref 0 let print s = output_string !chan_out s - + exception Fin_fichier } @@ -77,5 +77,5 @@ and comment = parse | "(*" (*"*)"*) { incr comment_depth; comment lexbuf } | (*"(*"*) "*)" { decr comment_depth; if !comment_depth > 0 then comment lexbuf } - | eof { raise Fin_fichier } + | eof { raise Fin_fichier } | _ { comment lexbuf } diff --git a/dev/ocamlweb-doc/parse.ml b/dev/ocamlweb-doc/parse.ml index e537b1f2..b145fffd 100644 --- a/dev/ocamlweb-doc/parse.ml +++ b/dev/ocamlweb-doc/parse.ml @@ -82,7 +82,7 @@ let rec str_stack = function | 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) + String.concat " " (List.rev ops) let pps s = prerr_endline (str_stack s) let err s stk = failwith (s^": "^str_stack stk) diff --git a/dev/printers.mllib b/dev/printers.mllib new file mode 100644 index 00000000..e8ec10c5 --- /dev/null +++ b/dev/printers.mllib @@ -0,0 +1,133 @@ +Coq_config + +Pp_control +Pp +Compat +Flags +Segmenttree +Unicodetable +Util +Bigint +Hashcons +Dyn +System +Envars +Bstack +Edit +Gset +Gmap +Fset +Fmap +Tlm +Gmapl +Profile +Explore +Predicate +Rtree +Heap +Option +Dnet + +Names +Univ +Esubst +Term +Mod_subst +Sign +Cbytecodes +Copcodes +Cemitcodes +Declarations +Retroknowledge +Pre_env +Cbytegen +Environ +Conv_oracle +Closure +Reduction +Type_errors +Entries +Modops +Inductive +Typeops +Indtypes +Cooking +Term_typing +Subtyping +Mod_typing +Safe_typing + +Summary +Nameops +Libnames +Global +Nametab +Libobject +Lib +Goptions +Decls +Heads +Termops +Namegen +Evd +Rawterm +Reductionops +Inductiveops +Retyping +Cbv +Pretype_errors +Evarutil +Term_dnet +Recordops +Evarconv +Typing +Pattern +Matching +Tacred +Classops +Typeclasses_errors +Typeclasses +Detyping +Indrec +Coercion +Unification +Cases +Pretyping +Clenv + +Lexer +Ppextend +Genarg +Topconstr +Notation +Dumpglob +Reserve +Impargs +Constrextern +Syntax_def +Implicit_quantifiers +Smartlocate +Constrintern +Proof_trees +Tacexpr +Proof_type +Logic +Refiner +Evar_refiner +Pfedit +Tactic_debug +Decl_mode +Ppconstr +Extend +Extrawit +Pcoq +Printer +Pptactic +Ppdecl_proof +Tactic_printer +Egrammar +Himsg +Cerrors +Vernacexpr +Vernacinterp +Top_printers diff --git a/dev/top_printers.ml b/dev/top_printers.ml index d7d2f6d8..23701c23 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -28,10 +28,11 @@ open Cerrors open Evd open Goptions open Genarg +open Mod_subst let _ = Constrextern.print_evar_arguments := true -let _ = set_bool_option_value (SecondaryTable ("Printing","Matching")) false +let _ = set_bool_option_value ["Printing";"Matching"] false let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found) (* std_ppcmds *) @@ -40,13 +41,13 @@ let pppp x = pp x (* name printers *) let ppid id = pp (pr_id id) let pplab l = pp (pr_lab l) -let ppmsid msid = pp (str (debug_string_of_msid msid)) let ppmbid mbid = pp (str (debug_string_of_mbid mbid)) let ppdir dir = pp (pr_dirpath dir) let ppmp mp = pp(str (string_of_mp mp)) -let ppcon con = pp(pr_con con) +let ppcon con = pp(debug_pr_con con) let ppkn kn = pp(pr_kn kn) -let ppsp sp = pp(pr_sp sp) +let ppmind kn = pp(debug_pr_mind kn) +let ppsp sp = pp(pr_path sp) let ppqualid qid = pp(pr_qualid qid) let ppclindex cl = pp(Classops.pr_cl_index cl) @@ -65,17 +66,30 @@ let ppfconstr c = ppconstr (Closure.term_of_fconstr c) let ppbigint n = pp (Bigint.pr_bigint n);; -let prset pr l = str "[" ++ prlist_with_sep spc pr l ++ str "]" +let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]" let ppintset l = pp (prset int (Intset.elements l)) let ppidset l = pp (prset pr_id (Idset.elements l)) +let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]" +let ppidmap pr l = + let pr (id,b) = pr_id id ++ str "=>" ++ pr id b in + pp (prset' pr (Idmap.fold (fun a b l -> (a,b)::l) l [])) + +let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) -> + hov 0 + (Termops.print_constr c ++ + (match copt with None -> mt () | Some c -> spc () ++ str "") ++ + (if id = id0 then mt () + else spc () ++ str "")))) + let pP s = pp (hov 0 s) -let safe_pr_global = function - | ConstRef kn -> pp (str "CONSTREF(" ++ pr_con kn ++ str ")") - | IndRef (kn,i) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ +let safe_pr_global = function + | ConstRef kn -> pp (str "CONSTREF(" ++ debug_pr_con kn ++ str ")") + | IndRef (kn,i) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++ int i ++ str ")") - | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ + | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++ int i ++ str "," ++ int j ++ str ")") | VarRef id -> pp (str "VARREF(" ++ pr_id id ++ str ")") @@ -92,6 +106,7 @@ let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t) let ppj j = pp (genppj pr_ljudge j) let prsubst s = pp (Mod_subst.debug_pr_subst s) +let prdelta s = pp (Mod_subst.debug_pr_delta s) let pp_idpred s = pp (pr_idpred s) let pp_cpred s = pp (pr_cpred s) @@ -100,9 +115,9 @@ let pp_transparent_state s = pp (pr_transparent_state s) (* proof printers *) let ppmetas metas = pp(pr_metaset metas) let ppevm evd = pp(pr_evar_map evd) -let ppevd evd = pp(pr_evar_defs evd) let ppclenv clenv = pp(pr_clenv clenv) let ppgoal g = pp(db_pr_goal g) +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)) @@ -134,7 +149,7 @@ let ppobj obj = Format.print_string (Libobject.object_tag obj) let cnt = ref 0 -let cast_kind_display k = +let cast_kind_display k = match k with | VMcast -> "VMcast" | DEFAULTcast -> "DEFAULTcast" @@ -145,7 +160,7 @@ let constr_display csr = | Meta n -> "Meta("^(string_of_int n)^")" | Var id -> "Var("^(string_of_id id)^")" | Sort s -> "Sort("^(sort_display s)^")" - | Cast (c,k, t) -> + | Cast (c,k, t) -> "Cast("^(term_display c)^","^(cast_kind_display k)^","^(term_display t)^")" | Prod (na,t,c) -> "Prod("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n" @@ -158,9 +173,9 @@ let constr_display csr = | Evar (e,l) -> "Evar("^(string_of_int e)^","^(array_display l)^")" | Const c -> "Const("^(string_of_con c)^")" | Ind (sp,i) -> - "MutInd("^(string_of_kn sp)^","^(string_of_int i)^")" + "MutInd("^(string_of_mind sp)^","^(string_of_int i)^")" | Construct ((sp,i),j) -> - "MutConstruct(("^(string_of_kn sp)^","^(string_of_int i)^")," + "MutConstruct(("^(string_of_mind sp)^","^(string_of_int i)^")," ^(string_of_int j)^")" | Case (ci,p,c,bl) -> "MutCase(,"^(term_display p)^","^(term_display c)^"," @@ -212,25 +227,25 @@ let print_pure_constr csr = print_string "::"; (term_display t); print_string ")"; close_box() | Prod (Name(id),t,c) -> open_hovbox 1; - print_string"("; print_string (string_of_id id); - print_string ":"; box_display t; - print_string ")"; print_cut(); + print_string"("; print_string (string_of_id id); + print_string ":"; box_display t; + print_string ")"; print_cut(); box_display c; close_box() | Prod (Anonymous,t,c) -> print_string"("; box_display t; print_cut(); print_string "->"; - box_display c; print_string ")"; + box_display c; print_string ")"; | Lambda (na,t,c) -> print_string "["; name_display na; print_string ":"; box_display t; print_string "]"; - print_cut(); box_display c; + print_cut(); box_display c; | LetIn (na,b,t,c) -> - print_string "["; name_display na; print_string "="; + print_string "["; name_display na; print_string "="; box_display b; print_cut(); print_string ":"; box_display t; print_string "]"; - print_cut(); box_display c; - | App (c,l) -> - print_string "("; - box_display c; + print_cut(); box_display c; + | App (c,l) -> + print_string "("; + box_display c; Array.iter (fun x -> print_space (); box_display x) l; print_string ")" | Evar (e,l) -> print_string "Evar#"; print_int e; print_string "{"; @@ -257,25 +272,25 @@ let print_pure_constr csr = open_vbox 0; Array.iter (fun x -> print_cut(); box_display x) bl; close_box(); - print_cut(); - print_string "end"; + print_cut(); + print_string "end"; close_box() | Fix ((t,i),(lna,tl,bl)) -> - print_string "Fix("; print_int i; print_string ")"; + print_string "Fix("; print_int i; print_string ")"; print_cut(); open_vbox 0; let rec print_fix () = for k = 0 to (Array.length tl) - 1 do open_vbox 0; - name_display lna.(k); print_string "/"; + name_display lna.(k); print_string "/"; print_int t.(k); print_cut(); print_string ":"; box_display tl.(k) ; print_cut(); print_string ":="; box_display bl.(k); close_box (); print_cut() done - in print_string"{"; print_fix(); print_string"}" + in print_string"{"; print_fix(); print_string"}" | CoFix(i,(lna,tl,bl)) -> - print_string "CoFix("; print_int i; print_string ")"; + print_string "CoFix("; print_int i; print_string ")"; print_cut(); open_vbox 0; let rec print_fix () = @@ -300,27 +315,27 @@ let print_pure_constr csr = | Name id -> print_string (string_of_id id) | Anonymous -> print_string "_" (* Remove the top names for library and Scratch to avoid long names *) - and sp_display sp = + and sp_display sp = (* let dir,l = decode_kn sp in - let ls = - match List.rev (List.map string_of_id (repr_dirpath dir)) with + let ls = + match List.rev (List.map string_of_id (repr_dirpath dir)) with ("Top"::l)-> l - | ("Coq"::_::l) -> l + | ("Coq"::_::l) -> l | l -> l in List.iter (fun x -> print_string x; print_string ".") ls;*) - print_string (string_of_kn sp) - and sp_con_display sp = + print_string (debug_string_of_mind sp) + and sp_con_display sp = (* let dir,l = decode_kn sp in - let ls = - match List.rev (List.map string_of_id (repr_dirpath dir)) with + let ls = + match List.rev (List.map string_of_id (repr_dirpath dir)) with ("Top"::l)-> l - | ("Coq"::_::l) -> l + | ("Coq"::_::l) -> l | l -> l in List.iter (fun x -> print_string x; print_string ".") ls;*) - print_string (string_of_con sp) + print_string (debug_string_of_con sp) in - try + try box_display csr; print_flush() with e -> print_string (Printexc.to_string e);print_flush (); @@ -369,7 +384,7 @@ let pp_generic_argument arg = (* Vernac-level debugging commands *) let in_current_context f c = - let (evmap,sign) = + let (evmap,sign) = try Pfedit.get_current_goal_context () with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) in f (Constrintern.interp_constr evmap sign c) @@ -400,12 +415,10 @@ let _ = e -> Pp.pp (Cerrors.explain_exn e) let _ = extend_vernac_command_grammar "PrintConstr" - [[TacTerm "PrintConstr"; - TacNonTerm - (dummy_loc, - (Gramext.Snterm (Pcoq.Gram.Entry.obj Constr.constr), - ConstrArgType), - Some "c")]] + [[GramTerminal "PrintConstr"; + GramNonTerminal + (dummy_loc,ConstrArgType,Extend.Aentry ("constr","constr"), + Some (Names.id_of_string "c"))]] let _ = try @@ -419,12 +432,10 @@ let _ = e -> Pp.pp (Cerrors.explain_exn e) let _ = extend_vernac_command_grammar "PrintPureConstr" - [[TacTerm "PrintPureConstr"; - TacNonTerm - (dummy_loc, - (Gramext.Snterm (Pcoq.Gram.Entry.obj Constr.constr), - ConstrArgType), - Some "c")]] + [[GramTerminal "PrintPureConstr"; + GramNonTerminal + (dummy_loc,ConstrArgType,Extend.Aentry ("constr","constr"), + Some (Names.id_of_string "c"))]] (* Setting printer of unbound global reference *) open Names @@ -434,38 +445,38 @@ open Libnames let encode_path loc prefix mpdir suffix id = let dir = match mpdir with | None -> [] - | Some (mp,dir) -> + | Some (mp,dir) -> (repr_dirpath (dirpath_of_string (string_of_mp mp))@ repr_dirpath dir) in - Qualid (loc, make_qualid + Qualid (loc, make_qualid (make_dirpath (List.rev (id_of_string prefix::dir@suffix))) id) let raw_string_of_ref loc = function - | ConstRef cst -> + | ConstRef cst -> let (mp,dir,id) = repr_con cst in encode_path loc "CST" (Some (mp,dir)) [] (id_of_label id) | IndRef (kn,i) -> - let (mp,dir,id) = repr_kn kn in - encode_path loc "IND" (Some (mp,dir)) [id_of_label id] + let (mp,dir,id) = repr_mind kn in + encode_path loc "IND" (Some (mp,dir)) [id_of_label id] (id_of_string ("_"^string_of_int i)) - | ConstructRef ((kn,i),j) -> - let (mp,dir,id) = repr_kn kn in + | ConstructRef ((kn,i),j) -> + let (mp,dir,id) = repr_mind kn in encode_path loc "CSTR" (Some (mp,dir)) - [id_of_label id;id_of_string ("_"^string_of_int i)] + [id_of_label id;id_of_string ("_"^string_of_int i)] (id_of_string ("_"^string_of_int j)) - | VarRef id -> + | VarRef id -> encode_path loc "SECVAR" None [] id let short_string_of_ref loc = function | VarRef id -> Ident (loc,id) | ConstRef cst -> Ident (loc,id_of_label (pi3 (repr_con cst))) - | IndRef (kn,0) -> Ident (loc,id_of_label (pi3 (repr_kn kn))) + | IndRef (kn,0) -> Ident (loc,id_of_label (pi3 (repr_mind kn))) | IndRef (kn,i) -> - encode_path loc "IND" None [id_of_label (pi3 (repr_kn kn))] + encode_path loc "IND" None [id_of_label (pi3 (repr_mind kn))] (id_of_string ("_"^string_of_int i)) - | ConstructRef ((kn,i),j) -> - encode_path loc "CSTR" None - [id_of_label (pi3 (repr_kn kn));id_of_string ("_"^string_of_int i)] + | ConstructRef ((kn,i),j) -> + encode_path loc "CSTR" None + [id_of_label (pi3 (repr_mind kn));id_of_string ("_"^string_of_int i)] (id_of_string ("_"^string_of_int j)) let _ = Constrextern.set_debug_global_reference_printer diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index de68ce1e..46ba24da 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -744,28 +744,28 @@ Conflicts exists between integers and constrs. \nlsep \TERM{simplif} \nlsep \TERM{intuition}~\OPT{\NTL{tactic}{0}} \nlsep \TERM{linearintuition}~\OPT{\NT{num}} -%% contrib/cc +%% plugins/cc \nlsep \TERM{cc} -%% contrib/field +%% plugins/field \nlsep \TERM{field}~\STAR{\tacconstr} -%% contrib/firstorder +%% plugins/firstorder \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}} \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{with}~\PLUS{\NT{reference}} \nlsep \TERM{ground}~\OPT{\NTL{tactic}{0}}~\KWD{using}~\PLUS{\NT{ident}} %%\nlsep \TERM{gtauto} \nlsep \TERM{gintuition}~\OPT{\NTL{tactic}{0}} -%% contrib/fourier +%% plugins/fourier \nlsep \TERM{fourierZ} -%% contrib/funind +%% plugins/funind \nlsep \TERM{functional}~\TERM{induction}~\tacconstr~\PLUS{\tacconstr} -%% contrib/jprover +%% plugins/jprover \nlsep \TERM{jp}~\OPT{\NT{num}} -%% contrib/omega +%% plugins/omega \nlsep \TERM{omega} -%% contrib/ring +%% plugins/ring \nlsep \TERM{quote}~\NT{ident}~\OPTGR{\KWD{[}~\PLUS{\NT{ident}}~\KWD{]}} \nlsep \TERM{ring}~\STAR{\tacconstr} -%% contrib/romega +%% plugins/romega \nlsep \TERM{romega} \SEPDEF \DEFNT{orient} diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 1e114489..59545d8a 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -7,10 +7,10 @@ open Vm let ppripos (ri,pos) = (match ri with - | Reloc_annot a -> + | Reloc_annot a -> let sp,i = a.ci.ci_ind in - print_string - ("annot : MutInd("^(string_of_kn sp)^","^(string_of_int i)^")\n") + print_string + ("annot : MutInd("^(string_of_mind sp)^","^(string_of_int i)^")\n") | Reloc_const _ -> print_string "structured constant\n" | Reloc_getglobal kn -> @@ -29,8 +29,8 @@ let ppsort = function let print_idkey idk = - match idk with - | ConstKey sp -> + match idk with + | ConstKey sp -> print_string "Cons("; print_string (string_of_con sp); print_string ")" @@ -38,8 +38,8 @@ let print_idkey idk = | RelKey i -> print_string "~";print_int i let rec ppzipper z = - match z with - | Zapp args -> + match z with + | Zapp args -> let n = nargs args in open_hbox (); for i = 0 to n-2 do @@ -50,7 +50,7 @@ let rec ppzipper z = | Zfix _ -> print_string "Zfix" | Zswitch _ -> print_string "Zswitch" -and ppstack s = +and ppstack s = open_hovbox 0; print_string "["; List.iter (fun z -> ppzipper z;print_string " | ") s; @@ -62,19 +62,19 @@ and ppatom a = | Aid idk -> print_idkey idk | Aiddef(idk,_) -> print_string "&";print_idkey idk | Aind(sp,i) -> print_string "Ind("; - print_string (string_of_kn sp); + print_string (string_of_mind sp); print_string ","; print_int i; print_string ")" and ppwhd whd = - match whd with + match whd with | Vsort s -> ppsort s | Vprod _ -> print_string "product" | Vfun _ -> print_string "function" | Vfix _ -> print_vfix() | Vcofix _ -> print_string "cofix" | Vconstr_const i -> print_string "C(";print_int i;print_string")" - | Vconstr_block b -> ppvblock b + | Vconstr_block b -> ppvblock b | Vatom_stk(a,s) -> open_hbox();ppatom a;close_box(); print_string"@";ppstack s -- cgit v1.2.3