1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
|
(******************************************************************************)
(* *)
(* PROJECT HELM (http://www.cs.unibo.it/helm) *)
(* *)
(* 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 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. 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
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.
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.
In the rest of this file the types of the subterms satisfing all the
three conditions are called "inner types".
==========================
2. New commands available:
==========================
The new commands are:
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.
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
|
