]> matita.cs.unibo.it Git - helm.git/blob - components/cic_acic/cic2Xml.ml
"that is equivalent to" and "or equivalently" implemented in most situations.
[helm.git] / 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,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,t) ->
146              let letins,t' = eat_letins t in
147               (id,n,s)::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) ->
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) >]
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 attributes =
271   let class_of = function
272     | `Coercion -> Xml.xml_empty "class" [None,"value","coercion"]
273     | `Elim s ->
274         Xml.xml_nempty "class" [None,"value","elim"]
275          [< Xml.xml_empty
276              "SORT" [None,"value",
277                       (Cic2acic.string_of_sort (Cic2acic.sort_of_sort s)) ;
278                      None,"id","elimination_sort"] >]
279     | `Record field_names ->
280         Xml.xml_nempty "class" [None,"value","record"]
281          (List.fold_right
282            (fun (name,coercion) res ->
283              [< Xml.xml_empty "field" 
284                 [None,"name",if coercion then name ^ " coercion" else name]; 
285               res >]
286            ) field_names [<>])
287     | `Projection -> Xml.xml_empty "class" [None,"value","projection"]
288   in
289   let flavour_of = function
290     | `Definition -> Xml.xml_empty "flavour" [None, "value", "definition"]
291     | `Fact -> Xml.xml_empty "flavour" [None, "value", "fact"]
292     | `Lemma -> Xml.xml_empty "flavour" [None, "value", "lemma"]
293     | `Remark -> Xml.xml_empty "flavour" [None, "value", "remark"]
294     | `Theorem -> Xml.xml_empty "flavour" [None, "value", "theorem"]
295     | `Variant -> Xml.xml_empty "flavour" [None, "value", "variant"]
296     | `Axiom -> Xml.xml_empty "flavour" [None, "value", "axiom"]
297   in
298   let xml_attr_of = function
299     | `Generated -> Xml.xml_empty "generated" []
300     | `Class c -> class_of c
301     | `Flavour f -> flavour_of f
302   in
303   let xml_attrs =
304    List.fold_right 
305     (fun attr res -> [< xml_attr_of attr ; res >]) attributes [<>]
306   in
307    Xml.xml_nempty "attributes" [] xml_attrs
308
309 let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
310  let module C = Cic in
311  let module X = Xml in
312  let module U = UriManager in
313   let dtdname = dtdname ~ask_dtd_to_the_getter "cic.dtd" in
314    match obj with
315        C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params,obj_attrs) ->
316         let params' = param_attribute_of_params params in
317         let xml_attrs = xml_of_attrs obj_attrs in
318         let xml_for_current_proof_body =
319 (*CSC: Should the CurrentProof also have the list of variables it depends on? *)
320 (*CSC: I think so. Not implemented yet.                                       *)
321          X.xml_nempty "CurrentProof"
322           [None,"of",UriManager.string_of_uri uri ; None,"id", id]
323           [< xml_attrs;
324             List.fold_left
325               (fun i (cid,n,canonical_context,t) ->
326                 [< i ;
327                    X.xml_nempty "Conjecture"
328                     [None,"id",cid ; None,"no",(string_of_int n)]
329                     [< List.fold_left
330                         (fun i (hid,t) ->
331                           [< (match t with
332                                  Some (n,C.ADecl t) ->
333                                   X.xml_nempty "Decl"
334                                    (match n with
335                                        C.Name n' ->
336                                         [None,"id",hid;None,"name",n']
337                                      | C.Anonymous -> [None,"id",hid])
338                                    (print_term ?ids_to_inner_sorts t)
339                                | Some (n,C.ADef t) ->
340                                   X.xml_nempty "Def"
341                                    (match n with
342                                        C.Name n' ->
343                                         [None,"id",hid;None,"name",n']
344                                      | C.Anonymous -> [None,"id",hid])
345                                    (print_term ?ids_to_inner_sorts t)
346                               | None -> X.xml_empty "Hidden" [None,"id",hid]
347                              ) ;
348                              i
349                           >]
350                         ) [< >] canonical_context ;
351                        X.xml_nempty "Goal" []
352                         (print_term ?ids_to_inner_sorts t)
353                     >]
354                 >])
355               [< >] conjectures ;
356              X.xml_nempty "body" [] (print_term ?ids_to_inner_sorts bo) >]
357         in
358         let xml_for_current_proof_type =
359          X.xml_nempty "ConstantType"
360           [None,"name",n ; None,"params",params' ; None,"id", id]
361           (print_term ?ids_to_inner_sorts ty)
362         in
363         let xmlbo =
364          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
365             X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^ dtdname ^ "\">\n");
366             xml_for_current_proof_body
367          >] in
368         let xmlty =
369          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
370             X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
371             xml_for_current_proof_type
372          >]
373         in
374          xmlty, Some xmlbo
375      | C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) ->
376         let params' = param_attribute_of_params params in
377         let xml_attrs = xml_of_attrs obj_attrs in
378         let xmlbo =
379          match bo with
380             None -> None
381           | Some bo ->
382              Some
383               [< X.xml_cdata
384                   "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
385                  X.xml_cdata
386                   ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ;
387                  X.xml_nempty "ConstantBody"
388                   [None,"for",UriManager.string_of_uri uri ;
389                    None,"params",params' ; None,"id", id]
390                   [< print_term ?ids_to_inner_sorts bo >]
391               >]
392         in
393         let xmlty =
394          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
395             X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
396              X.xml_nempty "ConstantType"
397               [None,"name",n ; None,"params",params' ; None,"id", id]
398               [< xml_attrs; print_term ?ids_to_inner_sorts ty >]
399          >]
400         in
401          xmlty, xmlbo
402      | C.AVariable (id,n,bo,ty,params,obj_attrs) ->
403         let params' = param_attribute_of_params params in
404         let xml_attrs = xml_of_attrs obj_attrs in
405         let xmlbo =
406          match bo with
407             None -> [< >]
408           | Some bo ->
409              X.xml_nempty "body" [] [< print_term ?ids_to_inner_sorts bo >]
410         in
411         let aobj =
412          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
413             X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
414              X.xml_nempty "Variable"
415               [None,"name",n ; None,"params",params' ; None,"id", id]
416               [< xml_attrs; xmlbo;
417                  X.xml_nempty "type" [] (print_term ?ids_to_inner_sorts ty)
418               >]
419          >]
420         in
421          aobj, None
422      | C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) ->
423         let params' = param_attribute_of_params params in
424         let xml_attrs = xml_of_attrs obj_attrs in
425          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
426             X.xml_cdata
427              ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
428             X.xml_nempty "InductiveDefinition"
429              [None,"noParams",string_of_int nparams ;
430               None,"id",id ;
431               None,"params",params']
432              [< xml_attrs;
433                 (List.fold_left
434                   (fun i (id,typename,finite,arity,cons) ->
435                     [< i ;
436                        X.xml_nempty "InductiveType"
437                         [None,"id",id ; None,"name",typename ;
438                          None,"inductive",(string_of_bool finite)
439                         ]
440                         [< X.xml_nempty "arity" []
441                             (print_term ?ids_to_inner_sorts arity) ;
442                            (List.fold_left
443                             (fun i (name,lc) ->
444                               [< i ;
445                                  X.xml_nempty "Constructor"
446                                   [None,"name",name]
447                                   (print_term ?ids_to_inner_sorts lc)
448                               >]) [<>] cons
449                            )
450                         >]
451                     >]
452                   ) [< >] tys
453                 )
454              >]
455          >], None
456 ;;
457
458 let
459  print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types
460   ~ask_dtd_to_the_getter
461 =
462  let module C2A = Cic2acic in
463  let module X = Xml in
464   let dtdname = dtdname ~ask_dtd_to_the_getter "cictypes.dtd" in
465    [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
466       X.xml_cdata
467        ("<!DOCTYPE InnerTypes SYSTEM \"" ^ dtdname ^ "\">\n") ;
468       X.xml_nempty "InnerTypes" [None,"of",UriManager.string_of_uri curi]
469        (Hashtbl.fold
470          (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
471            [< x ;
472               X.xml_nempty "TYPE" [None,"of",id]
473                [< X.xml_nempty "synthesized" []
474                  [< print_term ~ids_to_inner_sorts synty >] ;
475                  match expty with
476                    None -> [<>]
477                  | Some expty' -> X.xml_nempty "expected" []
478                     [< print_term ~ids_to_inner_sorts expty' >]
479                >]
480            >]
481          ) ids_to_inner_types [<>]
482        )
483    >]
484 ;;