]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_transformations/cic2Xml.ml
056240ef13899e24b08a8adf1b9aac306f94eb64
[helm.git] / helm / ocaml / cic_transformations / cic2Xml.ml
1 (* Copyright (C) 2000-2004, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 (*CSC codice cut & paste da cicPp e xmlcommand *)
27
28 exception NotImplemented;;
29
30 let dtdname ~ask_dtd_to_the_getter dtd =
31  if ask_dtd_to_the_getter then
32   Helm_registry.get "getter.url" ^ "getdtd?uri=" ^ dtd
33  else
34   "http://mowgli.cs.unibo.it/dtd/" ^ dtd
35 ;;
36
37 let param_attribute_of_params params =
38  String.concat " " (List.map UriManager.string_of_uri params)
39 ;;
40
41 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
42 let print_term ~ids_to_inner_sorts =
43  let find_sort id =
44    Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id)
45  in
46  let rec aux =
47   let module C = Cic in
48   let module X = Xml in
49   let module U = UriManager in
50     function
51        C.ARel (id,idref,n,b) ->
52         let sort = find_sort id in
53          X.xml_empty "REL"
54           [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ;
55            None,"idref",idref ; None,"sort",sort]
56      | C.AVar (id,uri,exp_named_subst) ->
57         let sort = find_sort id in
58          aux_subst uri
59           (X.xml_empty "VAR"
60             [None,"uri",U.string_of_uri uri;None,"id",id;None,"sort",sort])
61           exp_named_subst
62      | C.AMeta (id,n,l) ->
63         let sort = find_sort id in
64          X.xml_nempty "META"
65           [None,"no",(string_of_int n) ; None,"id",id ; None,"sort",sort]
66           (List.fold_left
67             (fun i t ->
68               match t with
69                  Some t' ->
70                   [< i ; X.xml_nempty "substitution" [] (aux t') >]
71                | None ->
72                   [< i ; X.xml_empty "substitution" [] >]
73             ) [< >] l)
74      | C.ASort (id,s) ->
75         let string_of_sort s =
76           Cic2acic.string_of_sort (Cic2acic.sort_of_sort s)
77         in
78          X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id]
79      | C.AImplicit _ -> raise NotImplemented
80      | C.AProd (last_id,_,_,_) as prods ->
81         let rec eat_prods =
82          function
83             C.AProd (id,n,s,t) ->
84              let prods,t' = eat_prods t in
85               (id,n,s)::prods,t'
86           | t -> [],t
87         in
88          let prods,t = eat_prods prods in
89           let sort = find_sort last_id in
90            X.xml_nempty "PROD" [None,"type",sort]
91             [< List.fold_left
92                 (fun i (id,binder,s) ->
93                   let sort = find_sort (Cic2acic.source_id_of_id id) in
94                    let attrs =
95                     (None,"id",id)::(None,"type",sort)::
96                     match binder with
97                        C.Anonymous -> []
98                      | C.Name b -> [None,"binder",b]
99                    in
100                     [< i ; X.xml_nempty "decl" attrs (aux s) >]
101                 ) [< >] prods ;
102                X.xml_nempty "target" [] (aux t)
103             >]
104      | C.ACast (id,v,t) ->
105         let sort = find_sort id in
106          X.xml_nempty "CAST" [None,"id",id ; None,"sort",sort]
107           [< X.xml_nempty "term" [] (aux v) ;
108              X.xml_nempty "type" [] (aux t)
109           >]
110      | C.ALambda (last_id,_,_,_) as lambdas ->
111         let rec eat_lambdas =
112          function
113             C.ALambda (id,n,s,t) ->
114              let lambdas,t' = eat_lambdas t in
115               (id,n,s)::lambdas,t'
116           | t -> [],t
117         in
118          let lambdas,t = eat_lambdas lambdas in
119           let sort = find_sort last_id in
120            X.xml_nempty "LAMBDA" [None,"sort",sort]
121             [< List.fold_left
122                 (fun i (id,binder,s) ->
123                   let sort = find_sort (Cic2acic.source_id_of_id id) in
124                    let attrs =
125                     (None,"id",id)::(None,"type",sort)::
126                     match binder with
127                        C.Anonymous -> []
128                      | C.Name b -> [None,"binder",b]
129                    in
130                     [< i ; X.xml_nempty "decl" attrs (aux s) >]
131                 ) [< >] lambdas ;
132                X.xml_nempty "target" [] (aux t)
133             >]
134      | C.ALetIn (xid,C.Anonymous,s,t) ->
135        assert false
136      | C.ALetIn (last_id,C.Name _,_,_) as letins ->
137         let rec eat_letins =
138          function
139             C.ALetIn (id,n,s,t) ->
140              let letins,t' = eat_letins t in
141               (id,n,s)::letins,t'
142           | t -> [],t
143         in
144          let letins,t = eat_letins letins in
145           let sort = find_sort last_id in
146            X.xml_nempty "LETIN" [None,"sort",sort]
147             [< List.fold_left
148                 (fun i (id,binder,s) ->
149                   let sort = find_sort id in
150                    let attrs =
151                     (None,"id",id)::(None,"sort",sort)::
152                     match binder with
153                        C.Anonymous -> []
154                      | C.Name b -> [None,"binder",b]
155                    in
156                     [< i ; X.xml_nempty "def" attrs (aux s) >]
157                 ) [< >] letins ;
158                X.xml_nempty "target" [] (aux t)
159             >]
160      | C.AAppl (id,li) ->
161         let sort = find_sort id in
162          X.xml_nempty "APPLY" [None,"id",id ; None,"sort",sort]
163           [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
164           >]
165      | C.AConst (id,uri,exp_named_subst) ->
166         let sort = find_sort id in
167          aux_subst uri
168           (X.xml_empty "CONST"
169             [None,"uri",(U.string_of_uri uri) ; None,"id",id ; None,"sort",sort]
170           ) exp_named_subst
171      | C.AMutInd (id,uri,i,exp_named_subst) ->
172         aux_subst uri
173          (X.xml_empty "MUTIND"
174            [None, "uri", (U.string_of_uri uri) ;
175             None, "noType", (string_of_int i) ;
176             None, "id", id]
177          ) exp_named_subst
178      | C.AMutConstruct (id,uri,i,j,exp_named_subst) ->
179         let sort = find_sort id in
180          aux_subst uri
181           (X.xml_empty "MUTCONSTRUCT"
182             [None,"uri", (U.string_of_uri uri) ;
183              None,"noType",(string_of_int i) ;
184              None,"noConstr",(string_of_int j) ;
185              None,"id",id ; None,"sort",sort]
186           ) exp_named_subst
187      | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
188         let sort = find_sort id in
189          X.xml_nempty "MUTCASE"
190           [None,"uriType",(U.string_of_uri uri) ;
191            None,"noType", (string_of_int typeno) ;
192            None,"id", id ; None,"sort",sort]
193           [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
194              X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
195              List.fold_right
196               (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
197               patterns [<>]
198           >]
199      | C.AFix (id, no, funs) ->
200         let sort = find_sort id in
201          X.xml_nempty "FIX"
202           [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
203           [< List.fold_right
204               (fun (id,fi,ai,ti,bi) i ->
205                 [< X.xml_nempty "FixFunction"
206                     [None,"id",id ; None,"name", fi ;
207                      None,"recIndex", (string_of_int ai)]
208                     [< X.xml_nempty "type" [] [< aux ti >] ;
209                        X.xml_nempty "body" [] [< aux bi >]
210                     >] ;
211                    i
212                 >]
213               ) funs [<>]
214           >]
215      | C.ACoFix (id,no,funs) ->
216         let sort = find_sort id in
217          X.xml_nempty "COFIX"
218           [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
219           [< List.fold_right
220               (fun (id,fi,ti,bi) i ->
221                 [< X.xml_nempty "CofixFunction" [None,"id",id ; None,"name", fi]
222                     [< X.xml_nempty "type" [] [< aux ti >] ;
223                        X.xml_nempty "body" [] [< aux bi >]
224                     >] ;
225                    i
226                 >]
227               ) funs [<>]
228           >]
229  and aux_subst buri target subst =
230 (*CSC: I have now no way to assign an ID to the explicit named substitution *)
231   let id = None in
232    if subst = [] then
233     target
234    else
235     Xml.xml_nempty "instantiate"
236      (match id with None -> [] | Some id -> [None,"id",id])
237      [< target ;
238         List.fold_left
239          (fun i (uri,arg) ->
240            let relUri =
241             let buri_frags =
242              Str.split (Str.regexp "/") (UriManager.string_of_uri buri) in
243             let uri_frags = 
244              Str.split (Str.regexp "/") (UriManager.string_of_uri uri)  in
245              let rec find_relUri buri_frags uri_frags =
246               match buri_frags,uri_frags with
247                  [_], _ -> String.concat "/" uri_frags
248                | he1::tl1, he2::tl2 ->
249                   assert (he1 = he2) ;
250                   find_relUri tl1 tl2
251                | _,_ -> assert false (* uri is not relative to buri *)
252              in
253               find_relUri buri_frags uri_frags
254            in
255             [< i ; Xml.xml_nempty "arg" [None,"relUri", relUri] (aux arg) >]
256          ) [<>] subst
257      >]
258   in
259    aux
260 ;;
261
262 let xml_of_attrs attributes =
263   let class_of = function
264     | `Coercion -> Xml.xml_empty "class" [None,"value","coercion"]
265     | `Elim s ->
266         Xml.xml_nempty "class" [None,"value","elim"]
267          [< Xml.xml_empty
268              "SORT" [None,"value",
269                       (Cic2acic.string_of_sort (Cic2acic.sort_of_sort s)) ;
270                      None,"id","elimination_sort"] >]
271     | `Record field_names ->
272         Xml.xml_nempty "class" [None,"value","record"]
273          (List.fold_right
274            (fun name res ->
275              [< Xml.xml_empty "field" [None,"name",name]; res >]
276            ) field_names [<>])
277     | `Projection -> Xml.xml_empty "class" [None,"value","projection"]
278   in
279   let xml_attr_of = function
280     | `Generated -> Xml.xml_empty "generated" []
281     | `Class c -> class_of c
282   in
283   let xml_attrs =
284    List.fold_right 
285     (fun attr res -> [< xml_attr_of attr ; res >]) attributes [<>]
286   in
287    Xml.xml_nempty "attributes" [] xml_attrs
288
289 let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
290  let find_sort id =
291    Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id)
292  in
293  let module C = Cic in
294  let module X = Xml in
295  let module U = UriManager in
296   let dtdname = dtdname ~ask_dtd_to_the_getter "cic.dtd" in
297    match obj with
298        C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params,obj_attrs) ->
299         let params' = param_attribute_of_params params in
300         let xml_attrs = xml_of_attrs obj_attrs in
301         let xml_for_current_proof_body =
302 (*CSC: Should the CurrentProof also have the list of variables it depends on? *)
303 (*CSC: I think so. Not implemented yet.                                       *)
304          X.xml_nempty "CurrentProof"
305           [None,"of",UriManager.string_of_uri uri ; None,"id", id]
306           [< xml_attrs;
307             List.fold_left
308               (fun i (cid,n,canonical_context,t) ->
309                 [< i ;
310                    X.xml_nempty "Conjecture"
311                     [None,"id",cid ; None,"no",(string_of_int n)]
312                     [< List.fold_left
313                         (fun i (hid,t) ->
314                           [< (match t with
315                                  Some (n,C.ADecl t) ->
316                                   X.xml_nempty "Decl"
317                                    (match n with
318                                        C.Name n' ->
319                                         [None,"id",hid;None,"name",n']
320                                      | C.Anonymous -> [None,"id",hid])
321                                    (print_term ids_to_inner_sorts t)
322                                | Some (n,C.ADef t) ->
323                                   X.xml_nempty "Def"
324                                    (match n with
325                                        C.Name n' ->
326                                         [None,"id",hid;None,"name",n']
327                                      | C.Anonymous -> [None,"id",hid])
328                                    (print_term ids_to_inner_sorts t)
329                               | None -> X.xml_empty "Hidden" [None,"id",hid]
330                              ) ;
331                              i
332                           >]
333                         ) [< >] canonical_context ;
334                        X.xml_nempty "Goal" []
335                         (print_term ids_to_inner_sorts t)
336                     >]
337                 >])
338               [< >] conjectures ;
339              X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >]
340         in
341         let xml_for_current_proof_type =
342          X.xml_nempty "ConstantType"
343           [None,"name",n ; None,"params",params' ; None,"id", id]
344           (print_term ids_to_inner_sorts ty)
345         in
346         let xmlbo =
347          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
348             X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^ dtdname ^ "\">\n");
349             xml_for_current_proof_body
350          >] in
351         let xmlty =
352          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
353             X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
354             xml_for_current_proof_type
355          >]
356         in
357          xmlty, Some xmlbo
358      | C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) ->
359         let params' = param_attribute_of_params params in
360         let xml_attrs = xml_of_attrs obj_attrs in
361         let xmlbo =
362          match bo with
363             None -> None
364           | Some bo ->
365              Some
366               [< X.xml_cdata
367                   "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
368                  X.xml_cdata
369                   ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ;
370                  X.xml_nempty "ConstantBody"
371                   [None,"for",UriManager.string_of_uri uri ;
372                    None,"params",params' ; None,"id", id]
373                   [< print_term ids_to_inner_sorts bo >]
374               >]
375         in
376         let xmlty =
377          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
378             X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
379              X.xml_nempty "ConstantType"
380               [None,"name",n ; None,"params",params' ; None,"id", id]
381               [< xml_attrs; print_term ids_to_inner_sorts ty >]
382          >]
383         in
384          xmlty, xmlbo
385      | C.AVariable (id,n,bo,ty,params,obj_attrs) ->
386         let params' = param_attribute_of_params params in
387         let xml_attrs = xml_of_attrs obj_attrs in
388         let xmlbo =
389          match bo with
390             None -> [< >]
391           | Some bo ->
392              X.xml_nempty "body" [] [< print_term ids_to_inner_sorts bo >]
393         in
394         let aobj =
395          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
396             X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
397              X.xml_nempty "Variable"
398               [None,"name",n ; None,"params",params' ; None,"id", id]
399               [< xml_attrs; xmlbo;
400                  X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty)
401               >]
402          >]
403         in
404          aobj, None
405      | C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) ->
406         let params' = param_attribute_of_params params in
407         let xml_attrs = xml_of_attrs obj_attrs in
408          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
409             X.xml_cdata
410              ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
411             X.xml_nempty "InductiveDefinition"
412              [None,"noParams",string_of_int nparams ;
413               None,"id",id ;
414               None,"params",params']
415              [< xml_attrs;
416                 (List.fold_left
417                   (fun i (id,typename,finite,arity,cons) ->
418                     [< i ;
419                        X.xml_nempty "InductiveType"
420                         [None,"id",id ; None,"name",typename ;
421                          None,"inductive",(string_of_bool finite)
422                         ]
423                         [< X.xml_nempty "arity" []
424                             (print_term ids_to_inner_sorts arity) ;
425                            (List.fold_left
426                             (fun i (name,lc) ->
427                               [< i ;
428                                  X.xml_nempty "Constructor"
429                                   [None,"name",name]
430                                   (print_term ids_to_inner_sorts lc)
431                               >]) [<>] cons
432                            )
433                         >]
434                     >]
435                   ) [< >] tys
436                 )
437              >]
438          >], None
439 ;;
440
441 let
442  print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types
443   ~ask_dtd_to_the_getter
444 =
445  let module C2A = Cic2acic in
446  let module X = Xml in
447   let dtdname = dtdname ~ask_dtd_to_the_getter "cictypes.dtd" in
448    [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
449       X.xml_cdata
450        ("<!DOCTYPE InnerTypes SYSTEM \"" ^ dtdname ^ "\">\n") ;
451       X.xml_nempty "InnerTypes" [None,"of",UriManager.string_of_uri curi]
452        (Hashtbl.fold
453          (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
454            [< x ;
455               X.xml_nempty "TYPE" [None,"of",id]
456                [< X.xml_nempty "synthesized" []
457                  [< print_term ids_to_inner_sorts synty >] ;
458                  match expty with
459                    None -> [<>]
460                  | Some expty' -> X.xml_nempty "expected" []
461                     [< print_term ids_to_inner_sorts expty' >]
462                >]
463            >]
464          ) ids_to_inner_types [<>]
465        )
466    >]
467 ;;