(******************************************************************************) (* Copyright (C) 2000-2004, Claudio Sacerdoti Coen *) (* Project Helm (http://helm.cs.unibo.it) *) (* Project MoWGLI (http://mowgli.cs.unibo.it) *) (* *) (* Coq Exportation to XML *) (* *) (******************************************************************************) 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. 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 ================================================================================ ========================== 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 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 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, i.e. only the type of the outer LAMBDA of a block of nested LAMBDAs is printed. The rationale for the 3rd condition is that the type of the inner LAMBDAs could be easily computed starting from the type of the outer LAMBDA; moreover, 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. ========================================== 2.2. CIC with Explicit Named Substitutions ========================================== 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 ... #TO BE FINISHED ==================== 2.3. The CIC XML DTD ==================== #TO BE FINISHED