← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to contrib/xml/acic2Xml.ml4

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
contrib/xml/acic2Xml.ml4
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *   The HELM Project         /   The EU MoWGLI Project       *)
 
6
(*         *   University of Bologna                                    *)
 
7
(************************************************************************)
 
8
(*          This file is distributed under the terms of the             *)
 
9
(*           GNU Lesser General Public License Version 2.1              *)
 
10
(*                                                                      *)
 
11
(*                 Copyright (C) 2000-2004, HELM Team.                  *)
 
12
(*                       http://helm.cs.unibo.it                        *)
 
13
(************************************************************************)
 
14
 
 
15
(*CSC codice cut & paste da cicPp e xmlcommand *)
 
16
 
 
17
exception ImpossiblePossible;;
 
18
exception NotImplemented;;
 
19
let dtdname = "http://mowgli.cs.unibo.it/dtd/cic.dtd";;
 
20
let typesdtdname = "http://mowgli.cs.unibo.it/dtd/cictypes.dtd";;
 
21
 
 
22
let rec find_last_id =
 
23
 function
 
24
    [] -> Util.anomaly "find_last_id: empty list"
 
25
  | [id,_,_] -> id
 
26
  | _::tl -> find_last_id tl
 
27
;;
 
28
 
 
29
let export_existential = string_of_int
 
30
 
 
31
let print_term ids_to_inner_sorts =
 
32
 let rec aux =
 
33
  let module A = Acic in
 
34
  let module N = Names in
 
35
  let module X = Xml in
 
36
    function
 
37
       A.ARel (id,n,idref,b) ->
 
38
        let sort = Hashtbl.find ids_to_inner_sorts id in
 
39
         X.xml_empty "REL"
 
40
          ["value",(string_of_int n) ; "binder",(N.string_of_id b) ;
 
41
           "id",id ; "idref",idref; "sort",sort]
 
42
     | A.AVar (id,uri) ->
 
43
        let sort = Hashtbl.find ids_to_inner_sorts id in
 
44
         X.xml_empty "VAR" ["uri", uri ; "id",id ; "sort",sort]
 
45
     | A.AEvar (id,n,l) ->
 
46
        let sort = Hashtbl.find ids_to_inner_sorts id in
 
47
         X.xml_nempty "META" 
 
48
           ["no",(export_existential n) ; "id",id ; "sort",sort]
 
49
          (List.fold_left
 
50
            (fun i t ->
 
51
              [< i ; X.xml_nempty "substitution" [] (aux t) >]
 
52
            ) [< >] (List.rev l))
 
53
     | A.ASort (id,s) ->
 
54
        let string_of_sort =
 
55
         match Term.family_of_sort s with
 
56
            Term.InProp -> "Prop"
 
57
          | Term.InSet  -> "Set"
 
58
          | Term.InType -> "Type"
 
59
        in
 
60
         X.xml_empty "SORT" ["value",string_of_sort ; "id",id]
 
61
     | A.AProds (prods,t) ->
 
62
        let last_id = find_last_id prods in
 
63
        let sort = Hashtbl.find ids_to_inner_sorts last_id in
 
64
         X.xml_nempty "PROD" ["type",sort]
 
65
          [< List.fold_left
 
66
              (fun i (id,binder,s) ->
 
67
                let sort =
 
68
                 Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)
 
69
                in
 
70
                 let attrs =
 
71
                  ("id",id)::("type",sort)::
 
72
                  match binder with
 
73
                     Names.Anonymous -> []
 
74
                   | Names.Name b -> ["binder",Names.string_of_id b]
 
75
                 in
 
76
                  [< X.xml_nempty "decl" attrs (aux s) ; i >]
 
77
              ) [< >] prods ;
 
78
             X.xml_nempty "target" [] (aux t)
 
79
          >]
 
80
     | A.ACast (id,v,t) ->
 
81
        let sort = Hashtbl.find ids_to_inner_sorts id in
 
82
         X.xml_nempty "CAST" ["id",id ; "sort",sort]
 
83
          [< X.xml_nempty "term" [] (aux v) ;
 
84
             X.xml_nempty "type" [] (aux t)
 
85
          >]
 
86
     | A.ALambdas (lambdas,t) ->
 
87
        let last_id = find_last_id lambdas in
 
88
        let sort = Hashtbl.find ids_to_inner_sorts last_id in
 
89
         X.xml_nempty "LAMBDA" ["sort",sort]
 
90
          [< List.fold_left
 
91
              (fun i (id,binder,s) ->
 
92
                let sort =
 
93
                 Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)
 
94
                in
 
95
                 let attrs =
 
96
                  ("id",id)::("type",sort)::
 
97
                  match binder with
 
98
                     Names.Anonymous -> []
 
99
                   | Names.Name b -> ["binder",Names.string_of_id b]
 
100
                 in
 
101
                  [< X.xml_nempty "decl" attrs (aux s) ; i >]
 
102
              ) [< >] lambdas ;
 
103
             X.xml_nempty "target" [] (aux t)
 
104
          >]
 
105
     | A.ALetIns (letins,t) ->
 
106
        let last_id = find_last_id letins in
 
107
        let sort = Hashtbl.find ids_to_inner_sorts last_id in
 
108
         X.xml_nempty "LETIN" ["sort",sort]
 
109
          [< List.fold_left
 
110
              (fun i (id,binder,s) ->
 
111
                let sort =
 
112
                 Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)
 
113
                in
 
114
                 let attrs =
 
115
                  ("id",id)::("sort",sort)::
 
116
                  match binder with
 
117
                     Names.Anonymous -> assert false
 
118
                   | Names.Name b -> ["binder",Names.string_of_id b]
 
119
                 in
 
120
                  [< X.xml_nempty "def" attrs (aux s) ; i >]
 
121
              ) [< >] letins ;
 
122
             X.xml_nempty "target" [] (aux t)
 
123
          >]
 
124
     | A.AApp (id,li) ->
 
125
        let sort = Hashtbl.find ids_to_inner_sorts id in
 
126
         X.xml_nempty "APPLY" ["id",id ; "sort",sort]
 
127
          [< (List.fold_left (fun i x -> [< i ; (aux x) >]) [<>] li)
 
128
          >]
 
129
     | A.AConst (id,subst,uri) ->
 
130
        let sort = Hashtbl.find ids_to_inner_sorts id in
 
131
        let attrs = ["uri", uri ; "id",id ; "sort",sort] in
 
132
         aux_subst (X.xml_empty "CONST" attrs) subst
 
133
     | A.AInd (id,subst,uri,i) ->
 
134
        let attrs = ["uri", uri ; "noType",(string_of_int i) ; "id",id] in
 
135
         aux_subst (X.xml_empty "MUTIND" attrs) subst
 
136
     | A.AConstruct (id,subst,uri,i,j) ->
 
137
        let sort = Hashtbl.find ids_to_inner_sorts id in
 
138
        let attrs =
 
139
         ["uri", uri ;
 
140
          "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
 
141
          "id",id ; "sort",sort]
 
142
        in
 
143
         aux_subst (X.xml_empty "MUTCONSTRUCT" attrs) subst
 
144
     | A.ACase (id,uri,typeno,ty,te,patterns) ->
 
145
        let sort = Hashtbl.find ids_to_inner_sorts id in
 
146
         X.xml_nempty "MUTCASE"
 
147
          ["uriType", uri ;
 
148
           "noType", (string_of_int typeno) ;
 
149
           "id", id ; "sort",sort]
 
150
          [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
 
151
             X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
 
152
             List.fold_left
 
153
              (fun i x -> [< i ; X.xml_nempty "pattern" [] [< aux x >] >])
 
154
              [<>] patterns
 
155
          >]
 
156
     | A.AFix (id, no, funs) ->
 
157
        let sort = Hashtbl.find ids_to_inner_sorts id in
 
158
         X.xml_nempty "FIX"
 
159
          ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
 
160
          [< List.fold_left
 
161
              (fun i (id,fi,ai,ti,bi) ->
 
162
                [< i ;
 
163
                   X.xml_nempty "FixFunction"
 
164
                    ["id",id ; "name", (Names.string_of_id fi) ;
 
165
                     "recIndex", (string_of_int ai)]
 
166
                    [< X.xml_nempty "type" [] [< aux ti >] ;
 
167
                       X.xml_nempty "body" [] [< aux bi >]
 
168
                    >]
 
169
                >]
 
170
              ) [<>] funs
 
171
          >]
 
172
     | A.ACoFix (id,no,funs) ->
 
173
        let sort = Hashtbl.find ids_to_inner_sorts id in
 
174
         X.xml_nempty "COFIX"
 
175
          ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
 
176
          [< List.fold_left
 
177
              (fun i (id,fi,ti,bi) ->
 
178
                [< i ;
 
179
                   X.xml_nempty "CofixFunction"
 
180
                    ["id",id ; "name", Names.string_of_id fi]
 
181
                    [< X.xml_nempty "type" [] [< aux ti >] ;
 
182
                       X.xml_nempty "body" [] [< aux bi >]
 
183
                    >]
 
184
                >]
 
185
              ) [<>] funs
 
186
          >]
 
187
 and aux_subst target (id,subst) =
 
188
  if subst = [] then
 
189
   target
 
190
  else
 
191
   Xml.xml_nempty "instantiate"
 
192
    (match id with None -> [] | Some id -> ["id",id])
 
193
    [< target ;
 
194
       List.fold_left
 
195
        (fun i (uri,arg) ->
 
196
          [< i ; Xml.xml_nempty "arg" ["relUri", uri] (aux arg) >]
 
197
        ) [<>] subst
 
198
    >]
 
199
 in
 
200
  aux
 
201
;;
 
202
 
 
203
let param_attribute_of_params params =
 
204
 List.fold_right
 
205
  (fun (path,l) i ->
 
206
    List.fold_right
 
207
     (fun x i ->path ^ "/" ^ x ^ ".var" ^ match i with "" -> "" | i' -> " " ^ i'
 
208
     ) l "" ^ match i with "" -> "" | i' -> " " ^ i'
 
209
  ) params ""
 
210
;;
 
211
 
 
212
let print_object uri ids_to_inner_sorts =
 
213
 let rec aux =
 
214
  let module A = Acic in
 
215
  let module X = Xml in
 
216
    function
 
217
       A.ACurrentProof (id,n,conjectures,bo,ty) ->
 
218
        let xml_for_current_proof_body =
 
219
(*CSC: Should the CurrentProof also have the list of variables it depends on? *)
 
220
(*CSC: I think so. Not implemented yet.                                       *)
 
221
         X.xml_nempty "CurrentProof" ["of",uri ; "id", id]
 
222
          [< List.fold_left
 
223
              (fun i (cid,n,canonical_context,t) ->
 
224
                [< i ;
 
225
                   X.xml_nempty "Conjecture"
 
226
                    ["id", cid ; "no",export_existential n]
 
227
                    [< List.fold_left
 
228
                        (fun i (hid,t) ->
 
229
                          [< (match t with
 
230
                                n,A.Decl t ->
 
231
                                 X.xml_nempty "Decl"
 
232
                                  ["id",hid;"name",Names.string_of_id n]
 
233
                                  (print_term ids_to_inner_sorts t)
 
234
                              | n,A.Def (t,_) ->
 
235
                                 X.xml_nempty "Def"
 
236
                                  ["id",hid;"name",Names.string_of_id n]
 
237
                                  (print_term ids_to_inner_sorts t)
 
238
                             ) ;
 
239
                             i
 
240
                          >]
 
241
                        ) [< >] canonical_context ;
 
242
                       X.xml_nempty "Goal" []
 
243
                        (print_term ids_to_inner_sorts t)
 
244
                    >]
 
245
                >])
 
246
              [<>] (List.rev conjectures) ;
 
247
             X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >]
 
248
        in
 
249
        let xml_for_current_proof_type =
 
250
         X.xml_nempty "ConstantType" ["name",n ; "id", id]
 
251
          (print_term ids_to_inner_sorts ty)
 
252
        in
 
253
        let xmlbo =
 
254
         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 
255
            X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^dtdname ^"\">\n");
 
256
            xml_for_current_proof_body
 
257
         >] in
 
258
        let xmlty =
 
259
         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 
260
            X.xml_cdata
 
261
             ("<!DOCTYPE ConstantType SYSTEM \"" ^ dtdname ^ "\">\n");
 
262
            xml_for_current_proof_type
 
263
         >]
 
264
        in
 
265
         xmlty, Some xmlbo
 
266
     | A.AConstant (id,n,bo,ty,params) ->
 
267
        let params' = param_attribute_of_params params in
 
268
        let xmlbo =
 
269
         match bo with
 
270
            None -> None
 
271
          | Some bo ->
 
272
             Some
 
273
              [< X.xml_cdata
 
274
                  "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 
275
                 X.xml_cdata
 
276
                  ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ;
 
277
                 X.xml_nempty "ConstantBody"
 
278
                  ["for",uri ; "params",params' ; "id", id]
 
279
                  [< print_term ids_to_inner_sorts bo >]
 
280
              >]
 
281
        in
 
282
        let xmlty =
 
283
         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 
284
            X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^dtdname ^"\">\n");
 
285
             X.xml_nempty "ConstantType"
 
286
              ["name",n ; "params",params' ; "id", id]
 
287
              [< print_term ids_to_inner_sorts ty >]
 
288
         >]
 
289
        in
 
290
         xmlty, xmlbo
 
291
     | A.AVariable (id,n,bo,ty,params) ->
 
292
        let params' = param_attribute_of_params params in
 
293
         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 
294
            X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n") ;
 
295
            X.xml_nempty "Variable" ["name",n ; "params",params' ; "id", id]
 
296
             [< (match bo with
 
297
                    None -> [<>]
 
298
                  | Some bo ->
 
299
                     X.xml_nempty "body" []
 
300
                      (print_term ids_to_inner_sorts bo)
 
301
                ) ;
 
302
                X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty)
 
303
             >]
 
304
         >], None
 
305
     | A.AInductiveDefinition (id,tys,params,nparams) ->
 
306
        let params' = param_attribute_of_params params in
 
307
         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 
308
            X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
 
309
             dtdname ^ "\">\n") ;
 
310
            X.xml_nempty "InductiveDefinition"
 
311
             ["noParams",string_of_int nparams ;
 
312
              "id",id ;
 
313
              "params",params']
 
314
             [< (List.fold_left
 
315
                  (fun i (id,typename,finite,arity,cons) ->
 
316
                    [< i ;
 
317
                       X.xml_nempty "InductiveType"
 
318
                        ["id",id ; "name",Names.string_of_id typename ;
 
319
                         "inductive",(string_of_bool finite)
 
320
                        ]
 
321
                        [< X.xml_nempty "arity" []
 
322
                            (print_term ids_to_inner_sorts arity) ;
 
323
                           (List.fold_left
 
324
                            (fun i (name,lc) ->
 
325
                              [< i ;
 
326
                                 X.xml_nempty "Constructor"
 
327
                                  ["name",Names.string_of_id name]
 
328
                                  (print_term ids_to_inner_sorts lc)
 
329
                              >]) [<>] cons
 
330
                           )
 
331
                        >]
 
332
                    >]
 
333
                  ) [< >] tys
 
334
                )
 
335
             >]
 
336
         >], None
 
337
 in
 
338
  aux
 
339
;;
 
340
 
 
341
let print_inner_types curi ids_to_inner_sorts ids_to_inner_types =
 
342
 let module C2A = Cic2acic in
 
343
 let module X = Xml in
 
344
  [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 
345
     X.xml_cdata ("<!DOCTYPE InnerTypes SYSTEM \"" ^ typesdtdname ^"\">\n");
 
346
      X.xml_nempty "InnerTypes" ["of",curi]
 
347
       (Hashtbl.fold
 
348
         (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
 
349
           [< x ;
 
350
              X.xml_nempty "TYPE" ["of",id]
 
351
               [< X.xml_nempty "synthesized" []
 
352
                   (print_term ids_to_inner_sorts synty) ;
 
353
                  match expty with
 
354
                     None -> [<>]
 
355
                   | Some expty' ->
 
356
                      X.xml_nempty "expected" []
 
357
                       (print_term ids_to_inner_sorts expty')
 
358
               >]
 
359
           >]
 
360
         ) ids_to_inner_types [<>]
 
361
       )
 
362
  >]
 
363
;;