MAJ Claudio pour v8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5554 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 125 insertions, 143 deletions

diff --git a/contrib/xml/README b/contrib/xml/README
index dcdc585332..46c8b42c5b 100644
--- a/contrib/xml/README
+++ b/contrib/xml/README
@@ -1,37 +1,134 @@
 (******************************************************************************)
+(* Copyright (C) 2000-2004, Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>     *)
+(*                          Project Helm   (http://helm.cs.unibo.it)          *)
+(*                          Project MoWGLI (http://mowgli.cs.unibo.it)        *)
 (*                                                                            *)
-(*                   PROJECT HELM (http://www.cs.unibo.it/helm)               *)
+(*                     Coq Exportation to XML                                 *)
 (*                                                                            *)
-(*                     A module to print Coq objects in XML                   *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 20/12/2000                                 *)
 (******************************************************************************)
 
-This module provides commands to export a piece of Coq library in XML format
-and it must be considered beta-software. Only the information relevant
-to proof-checking and proof-rendering is exported, i.e. only the CIC objects.
+This module provides commands to export a piece of Coq library in XML format.
+Only the information relevant to proof-checking and proof-rendering is exported,
+i.e. only the CIC proof objects (lambda-terms).
 
 This document is tructured in the following way:
- 1. Inner-types
- 2. New commands available
- 3. URIs fixing
- 4. Suggested usage
- 5. How to exploit the XML files
+ 1. User documentation
+   1.1. New vernacular commands available
+   1.2. New coqc/coqtop flags and suggested usage
+   1.3. How to exploit the XML files
+ 2. Technical informations
+   2.1. Inner-types
+   2.2. CIC with Explicit Named Substitutions
+   2.3. The CIC XML DTD
+
+================================================================================
+                            USER DOCUMENTATION
+================================================================================
+
+=======================================
+1.1. New vernacular commands available:
+=======================================
+
+The new commands are:
+
+ Print XML qualid.                 It prints in XML (to standard output) the
+                                   object whose qualified name is qualid and
+                                   its inner-types (see Sect. 2.1).
+                                   The inner-types are always printed
+                                   in their own XML file. If the object is a
+                                   constant, its type and body are also printed
+                                   as two distinct XML files.
+                                   The object printed is always the most
+                                   discharged form of the object (see
+                                   the Section command of the Coq manual).
+
+ Print XML File "filename" qualid. Similar to "Print XML qualid". The generated
+                                   files are stored on the hard-disk using the
+                                   base file name "filename".
+
+ Show XML Proof.                   It prints in XML the current proof in
+                                   progress. Its inner-types are also printed.
+
+ Show XML File "filename" Proof.   Similar to "Show XML Proof". The generated
+                                   files are stored on the hard-disk using
+                                   the base file name "filename".
+
+ The verbosity of the previous commands is raised if the configuration
+ parameter verbose of xmlcommand.ml is set to true at compile time.
+
+==============================================
+1.2. New coqc/coqtop flags and suggested usage
+==============================================
+
+ The following flag has been added to coqc and coqtop:
+
+  -xml     export XML files either to the hierarchy rooted in
+           the directory $COQ_XML_LIBRARY_ROOT (if the environment
+           variable is set) or to stdout (if unset)
+
+ If the flag is set, every definition or declaration is immediately
+ exported to XML. The XML files describe the user-provided non-discharged
+ form of the definition or declaration. 
+
+
+ The coq_makefile utility has also been modified to easily allow XML
+ exportation:
+
+   make COQ_XML=-xml   (or, equivalently, setting the environment
+                        variable COQ_XML)
+
+
+ The suggested usage of the module is the following:
+
+   1. add to your own contribution a valid Make file and use coq_makefile
+      to generate the Makefile from the Make file.
+      *WARNING:* Since logical names are used to structure the XML hierarchy,
+      always add to the Make file at least one "-R" option to map physical
+      file names to logical module paths. See the Coq manual for further
+      informations on the -R flag.
+   2. set $COQ_XML_LIBRARY_ROOT to the directory where the XML file hierarchy
+      must be physically rooted.
+   3. compile your contribution with "make COQ_XML=-xml"
+
+
+=================================
+1.3. How to exploit the XML files
+=================================
+
+ Once the information is exported to XML, it becomes possible to implement
+ services that are completely Coq-independent. Projects HELM and MoWGLI
+ already provide rendering, searching and data mining functionalities.
+
+ In particular, the standard library and contributions of Coq can be
+ browsed and searched on the HELM web site:
+
+                  http://helm.cs.unibo.it/library.html
+
+
+ If you want to publish your own contribution so that it is included in the
+ HELM library, use the MoWGLI prototype upload form:
+
+                  http://mowgli.cs.unibo.it
+
+
+================================================================================
+                            TECHNICAL INFORMATIONS
+================================================================================
 
 ==========================
-1. Inner-types
+2.1. Inner-types
 ==========================
 
 In order to do proof-rendering (for example in natural language),
 some redundant typing information is required, i.e. the type of
 at least some of the subterms of the bodies and types. So, each
-one of the new commands described in section 2, print not only
+new command described in section 1.1 print not only
 the object, but also another XML file in which you can find
 the type of all the subterms of the terms of the printed object
 which respect the following conditions:
 
- 1. It's sort is Prop.
+ 1. It's sort is Prop or CProp (the "sort"-like definition used in
+    CoRN to type computationally relevant predicative propositions).
  2. It is not a cast or an atomic term, i.e. it's root is not a CAST, REL,
     VAR, MUTCONSTR or CONST.
  3. If it's root is a LAMBDA, then the root's parent node is not a LAMBDA,
@@ -44,134 +141,19 @@ the types of the inner LAMBDAs requires a lot of disk/memory space: removing
 the 3rd condition leads to XML file that are two times as big as the ones
 exported appling the 3rd condition.
 
-In the rest of this file the types of the subterms satisfing all the
-three conditions are called "inner types".
+==========================================
+2.2. CIC with Explicit Named Substitutions
+==========================================
 
-==========================
-2. New commands available:
-==========================
+The exported files are and XML encoding of the lambda-terms used by the
+Coq system. The implementative details of the Coq system are hidden as much
+as possible, so that the XML DTD is a straightforward encoding of the  
+Calculus of ...
 
-The new commands are:
+#TO BE FINISHED
 
- Print XML qualid.                 It prints in XML the object whose qualified
-                                   name is qualid. It prints also an XML file
-				   made of inner-types.
-                                   Only the most discharged available form of
-				   the term is printed.
-				   WARNING: relative URIs for variables
-				   are broken.
-
- Print XML File "filename" qualid. It prints in XML the object whose qualified
-                                   name is qualid on the file whose name is
-				   filename. It prints also an XML file made
-				   of inner types.
-                                   Only the most discharged available form of
-				   the term is printed.
-				   WARNING: relative URIs for variables
-				   are broken.
+====================
+2.3. The CIC XML DTD
+====================
 
- Show XML Proof.                   It prints in XML the current proof in
-                                   progress. It prints also an XML file made
-				   of inner types.
-				   WARNING: relative URIs for variables
-				   are broken.
-
- Show XML File "filename" Proof.   It prints in XML the current proof in
-                                   progress on the file whose name is filename.
-				   It prints also an XML file made of inner
-				   types.
-				   WARNING: relative URIs for variables
-				   are broken.
-
- Print XML Module id.              It prints in XML all the objects defined
-                                   in the already required module whose name
-				   is id, each one with the corresponding
-				   inner types XML file.
-				   This command is completely working.
-
- Print XML Module Disk "dir" id.   It prints in XML all the objects defined
-                                   in the already required module whose name
-				   is id, each one with the corresponding
-				   inner types XML file. The files are
-				   structured on the disk in a Unix
-				   hierarchy isomorphic to the tree of
-				   sections of Coq: each Unix directory
-				   corresponds to a Coq section. Coq's
-				   root section is exported to a root
-				   dir rooted in the "dir" directory.
-				   This command is completely working.
-
- Print XML Section id.             It behaves as "Print XML Module", but
-                                   it works on a closed section instead
-				   of on an already required module.
-				   WARNING: this command could be deprecated
-				   in the final release.
-
- Print XML Section Disk "dir" id.  It behaves as "Print XML Module Disk", but
-                                   it works on a closed section instead
-				   of on an already required module.
-				   WARNING: this command could be deprecated
-				   in the final release.
-
- Print XML All.                    It prints what is the structure of the
-                                   current environment of Coq with an high
-				   level of verbosity.
-				   WARING: useful only for debugging
-
- If xmlcommand.ml is compiled with the configuration parameter verbose
- set to true, then the verbosity of all the previous commands will be
- increased, except the one of Print XML All (that is always very verbose :-)
-
-===============
-3. URIs fixing
-===============
-
- The previous new commands are all damaged because they produce xml files
- in which all the URIs to other xml files are slightly broken. This will
- be hopefully fixed in the final release of Coq.
- So, to fix the uris, you must do the following operations:
-   1. export with the same root all the modules on which the module
-      you want to repair depends.
-   2. cd to the root and run "./mkindex.pl" to create the index.txt file
-      with the URIs of all the exported XML files.
-   3. copy index.txt to tmp.txt and remove in tmp.txt all the URIs of
-      the XML files that you have already repaired (perhaps none).
-   4. run "./fix_uri.pl index.txt tmp.txt"
-      The script will modify all the files whose URIs are in tmp.txt fixing
-      all the URIs belonging to index.txt. If an URI not belonging to index.txt
-      if found, then the script may fail.
-
-===================
-4. Suggested usage
-===================
-
- 1. Compile to .vo all the .v files you are interested in paying attention
-    to mapping LoadPath to significative absolute names.
- 2. Use "Print XML Module Disk" to export all the compiled modules to XML.
- 3. Fix the URIs.
-
- Example: let's imagine we have already exported all the standard library
-  of Coq in the "examples" directory and that now we want to export the
-  HIGMAN contribution in the Rocq directory of Coq's contrib. Following
-  the previous points, we do:
-
-  1. From the Unix prompt: "coqc -R HIGMAN Rocq.HIGMAN HIGMAN/Higman.v"
-  2. In Coq:
-      Require Export Xml.
-      Require Higman.
-      Print XML Module Disk "examples" Higman.
-  3. From the Unix prompt:
-      "cd examples ; mkindex.pl ; cp index.txt tmp.txt"
-     Then edit tmp.txt removing all the entries but the ones starting
-     with "cic:/Rocq/HIGMAN".
-      "fix_uri.pl index.txt tmp.txt"
-
-===============================
-5. How to exploit the XML files
-===============================
-
- Once the information is exported to XML, it becomes quite easy
- to do many interesting computations on it. If you are interested
- in proof-rendering, see project HELM:
-
-                  http://www.cs.unibo.it/helm
+#TO BE FINISHED