summaryrefslogtreecommitdiff
path: root/plugins/xml/README
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/xml/README
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'plugins/xml/README')
-rw-r--r--plugins/xml/README254
1 files changed, 254 insertions, 0 deletions
diff --git a/plugins/xml/README b/plugins/xml/README
new file mode 100644
index 00000000..a45dd31a
--- /dev/null
+++ b/plugins/xml/README
@@ -0,0 +1,254 @@
+(******************************************************************************)
+(* 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) *)
+(* *)
+(* 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 with Explicit Named Substitutions 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 (Co)Inductive Constructions.
+
+Nevertheless, there is a feature of the Coq system that can not be
+hidden in a completely satisfactory way: discharging. In Coq it is possible
+to open a section, declare variables and use them in the rest of the section
+as if they were axiom declarations. Once the section is closed, every definition
+and theorem in the section is discharged by abstracting it over the section
+variables. Variable declarations as well as section declarations are entirely
+dropped. Since we are interested in an XML encoding of definitions and
+theorems as close as possible to those directly provided the user, we
+do not want to export discharged forms. Exporting non-discharged theorem
+and definitions together with theorems that rely on the discharged forms
+obliges the tools that work on the XML encoding to implement discharging to
+achieve logical consistency. Moreover, the rendering of the files can be
+misleading, since hyperlinks can be shown between occurrences of the discharge
+form of a definition and the non-discharged definition, that are different
+objects.
+
+To overcome the previous limitations, Claudio Sacerdoti Coen developed in his
+PhD. thesis an extension of CIC, called Calculus of (Co)Inductive Constructions
+with Explicit Named Substitutions, that is a slight extension of CIC where
+discharging is not necessary. The DTD of the exported XML files describes
+constants, inductive types and variables of the Calculus of (Co)Inductive
+Constructions with Explicit Named Substitions. The conversion to the new
+calculus is performed during the exportation phase.
+
+The following example shows a very small Coq development together with its
+version in CIC with Explicit Named Substitutions.
+
+# CIC version: #
+Section S.
+ Variable A : Prop.
+
+ Definition impl := A -> A.
+
+ Theorem t : impl. (* uses the undischarged form of impl *)
+ Proof.
+ exact (fun (a:A) => a).
+ Qed.
+
+End S.
+
+Theorem t' : (impl False). (* uses the discharged form of impl *)
+ Proof.
+ exact (t False). (* uses the discharged form of t *)
+ Qed.
+
+# Corresponding CIC with Explicit Named Substitutions version: #
+Section S.
+ Variable A : Prop.
+
+ Definition impl(A) := A -> A. (* theorems and definitions are
+ explicitly abstracted over the
+ variables. The name is sufficient
+ to completely describe the abstraction *)
+
+ Theorem t(A) : impl. (* impl where A is not instantiated *)
+ Proof.
+ exact (fun (a:A) => a).
+ Qed.
+
+End S.
+
+Theorem t'() : impl{False/A}. (* impl where A is instantiated with False
+ Notice that t' does not depend on A *)
+ Proof.
+ exact t{False/A}. (* t where A is instantiated with False *)
+ Qed.
+
+Further details on the typing and reduction rules of the calculus can be
+found in Claudio Sacerdoti Coen PhD. dissertation, where the consistency
+of the calculus is also proved.
+
+======================================================
+2.3. The CIC with Explicit Named Substitutions XML DTD
+======================================================
+
+A copy of the DTD can be found in the file "cic.dtd".
+
+<ConstantType> is the root element of the files that correspond to
+ constant types.
+<ConstantBody> is the root element of the files that correspond to
+ constant bodies. It is used only for closed definitions and
+ theorems (i.e. when no metavariable occurs in the body
+ or type of the constant)
+<CurrentProof> is the root element of the file that correspond to
+ the body of a constant that depends on metavariables
+ (e.g. unfinished proofs)
+<Variable> is the root element of the files that correspond to variables
+<InductiveTypes> is the root element of the files that correspond to blocks
+ of mutually defined inductive definitions
+
+The elements
+ <LAMBDA>,<CAST>,<PROD>,<REL>,<SORT>,<APPLY>,<VAR>,<META>, <IMPLICIT>,<CONST>,
+ <LETIN>,<MUTIND>,<MUTCONSTRUCT>,<MUTCASE>,<FIX> and <COFIX>
+are used to encode the constructors of CIC. The sort or type attribute of the
+element, if present, is respectively the sort or the type of the term, that
+is a sort because of the typing rules of CIC.
+
+The element <instantiate> correspond to the application of an explicit named
+substitution to its first argument, that is a reference to a definition
+or declaration in the environment.
+
+All the other elements are just syntactic sugar.