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