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