1 (* Copyright (C) 2000-2004, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
26 (*CSC codice cut & paste da cicPp e xmlcommand *)
28 exception ImpossiblePossible;;
29 exception NotImplemented;;
31 let dtdname ~ask_dtd_to_the_getter dtd =
32 if ask_dtd_to_the_getter then
33 Helm_registry.get "getter.url" ^ "getdtd?uri=" ^ dtd
35 "http://mowgli.cs.unibo.it/dtd/" ^ dtd
38 let param_attribute_of_params params =
39 String.concat " " (List.map UriManager.string_of_uri params)
42 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
43 let print_term ~ids_to_inner_sorts =
45 Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id)
50 let module U = UriManager in
52 C.ARel (id,idref,n,b) ->
53 let sort = find_sort id in
55 [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ;
56 None,"idref",idref ; None,"sort",sort]
57 | C.AVar (id,uri,exp_named_subst) ->
58 let sort = find_sort id in
61 [None,"uri",U.string_of_uri uri;None,"id",id;None,"sort",sort])
64 let sort = find_sort id in
66 [None,"no",(string_of_int n) ; None,"id",id ; None,"sort",sort]
71 [< i ; X.xml_nempty "substitution" [] (aux t') >]
73 [< i ; X.xml_empty "substitution" [] >]
76 let string_of_sort s =
77 Cic2acic.string_of_sort (Cic2acic.sort_of_sort s)
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 ->
85 let prods,t' = eat_prods t in
89 let prods,t = eat_prods prods in
90 let sort = find_sort last_id in
91 X.xml_nempty "PROD" [None,"type",sort]
93 (fun i (id,binder,s) ->
94 let sort = find_sort (Cic2acic.source_id_of_id id) in
96 (None,"id",id)::(None,"type",sort)::
99 | C.Name b -> [None,"binder",b]
101 [< i ; X.xml_nempty "decl" attrs (aux s) >]
103 X.xml_nempty "target" [] (aux t)
105 | C.ACast (id,v,t) ->
106 let sort = find_sort id in
107 X.xml_nempty "CAST" [None,"id",id ; None,"sort",sort]
108 [< X.xml_nempty "term" [] (aux v) ;
109 X.xml_nempty "type" [] (aux t)
111 | C.ALambda (last_id,_,_,_) as lambdas ->
112 let rec eat_lambdas =
114 C.ALambda (id,n,s,t) ->
115 let lambdas,t' = eat_lambdas t in
119 let lambdas,t = eat_lambdas lambdas in
120 let sort = find_sort last_id in
121 X.xml_nempty "LAMBDA" [None,"sort",sort]
123 (fun i (id,binder,s) ->
124 let sort = find_sort (Cic2acic.source_id_of_id id) in
126 (None,"id",id)::(None,"type",sort)::
129 | C.Name b -> [None,"binder",b]
131 [< i ; X.xml_nempty "decl" attrs (aux s) >]
133 X.xml_nempty "target" [] (aux t)
135 | C.ALetIn (xid,C.Anonymous,s,t) ->
137 | C.ALetIn (last_id,C.Name _,_,_) as letins ->
140 C.ALetIn (id,n,s,t) ->
141 let letins,t' = eat_letins t in
145 let letins,t = eat_letins letins in
146 let sort = find_sort last_id in
147 X.xml_nempty "LETIN" [None,"sort",sort]
149 (fun i (id,binder,s) ->
150 let sort = find_sort id in
152 (None,"id",id)::(None,"sort",sort)::
155 | C.Name b -> [None,"binder",b]
157 [< i ; X.xml_nempty "def" attrs (aux s) >]
159 X.xml_nempty "target" [] (aux t)
162 let sort = find_sort id in
163 X.xml_nempty "APPLY" [None,"id",id ; None,"sort",sort]
164 [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
166 | C.AConst (id,uri,exp_named_subst) ->
167 let sort = find_sort id in
170 [None,"uri",(U.string_of_uri uri) ; None,"id",id ; None,"sort",sort]
172 | C.AMutInd (id,uri,i,exp_named_subst) ->
174 (X.xml_empty "MUTIND"
175 [None, "uri", (U.string_of_uri uri) ;
176 None, "noType", (string_of_int i) ;
179 | C.AMutConstruct (id,uri,i,j,exp_named_subst) ->
180 let sort = find_sort id in
182 (X.xml_empty "MUTCONSTRUCT"
183 [None,"uri", (U.string_of_uri uri) ;
184 None,"noType",(string_of_int i) ;
185 None,"noConstr",(string_of_int j) ;
186 None,"id",id ; None,"sort",sort]
188 | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
189 let sort = find_sort id in
190 X.xml_nempty "MUTCASE"
191 [None,"uriType",(U.string_of_uri uri) ;
192 None,"noType", (string_of_int typeno) ;
193 None,"id", id ; None,"sort",sort]
194 [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
195 X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
197 (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
200 | C.AFix (id, no, funs) ->
201 let sort = find_sort id in
203 [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
205 (fun (id,fi,ai,ti,bi) i ->
206 [< X.xml_nempty "FixFunction"
207 [None,"id",id ; None,"name", fi ;
208 None,"recIndex", (string_of_int ai)]
209 [< X.xml_nempty "type" [] [< aux ti >] ;
210 X.xml_nempty "body" [] [< aux bi >]
216 | C.ACoFix (id,no,funs) ->
217 let sort = find_sort id in
219 [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
221 (fun (id,fi,ti,bi) i ->
222 [< X.xml_nempty "CofixFunction" [None,"id",id ; None,"name", fi]
223 [< X.xml_nempty "type" [] [< aux ti >] ;
224 X.xml_nempty "body" [] [< aux bi >]
230 and aux_subst buri target subst =
231 (*CSC: I have now no way to assign an ID to the explicit named substitution *)
236 Xml.xml_nempty "instantiate"
237 (match id with None -> [] | Some id -> [None,"id",id])
243 Str.split (Str.regexp "/") (UriManager.string_of_uri buri) in
245 Str.split (Str.regexp "/") (UriManager.string_of_uri uri) in
246 let rec find_relUri buri_frags uri_frags =
247 match buri_frags,uri_frags with
248 [_], _ -> String.concat "/" uri_frags
249 | he1::tl1, he2::tl2 ->
252 | _,_ -> assert false (* uri is not relative to buri *)
254 find_relUri buri_frags uri_frags
256 [< i ; Xml.xml_nempty "arg" [None,"relUri", relUri] (aux arg) >]
263 let xml_of_attrs attributes =
264 let class_of = function
265 | `Coercion -> "coercion"
266 | `Elim Cic.Prop -> "elimProp"
267 | `Elim Cic.CProp -> "elimCProp"
268 | `Elim Cic.Set -> "elimSet"
269 | `Elim (Cic.Type _) -> "elimType"
270 | `Record -> "record"
271 | `Projection -> "projection"
273 let xml_attr_of = function
274 | `Generated -> None, "generated", "true"
275 | `Class c -> None, "class", class_of c
277 let xml_attrs = List.map xml_attr_of attributes in
278 Xml.xml_empty "attributes" xml_attrs
280 let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
282 Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id)
284 let module C = Cic in
285 let module X = Xml in
286 let module U = UriManager in
287 let dtdname = dtdname ~ask_dtd_to_the_getter "cic.dtd" in
289 C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params,obj_attrs) ->
290 let params' = param_attribute_of_params params in
291 let xml_attrs = xml_of_attrs obj_attrs in
292 let xml_for_current_proof_body =
293 (*CSC: Should the CurrentProof also have the list of variables it depends on? *)
294 (*CSC: I think so. Not implemented yet. *)
295 X.xml_nempty "CurrentProof"
296 [None,"of",UriManager.string_of_uri uri ; None,"id", id]
299 (fun i (cid,n,canonical_context,t) ->
301 X.xml_nempty "Conjecture"
302 [None,"id",cid ; None,"no",(string_of_int n)]
306 Some (n,C.ADecl t) ->
310 [None,"id",hid;None,"name",n']
311 | C.Anonymous -> [None,"id",hid])
312 (print_term ids_to_inner_sorts t)
313 | Some (n,C.ADef t) ->
317 [None,"id",hid;None,"name",n']
318 | C.Anonymous -> [None,"id",hid])
319 (print_term ids_to_inner_sorts t)
320 | None -> X.xml_empty "Hidden" [None,"id",hid]
324 ) [< >] canonical_context ;
325 X.xml_nempty "Goal" []
326 (print_term ids_to_inner_sorts t)
330 X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >]
332 let xml_for_current_proof_type =
333 X.xml_nempty "ConstantType"
334 [None,"name",n ; None,"params",params' ; None,"id", id]
335 (print_term ids_to_inner_sorts ty)
338 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
339 X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^ dtdname ^ "\">\n");
340 xml_for_current_proof_body
343 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
344 X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
345 xml_for_current_proof_type
349 | C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) ->
350 let params' = param_attribute_of_params params in
351 let xml_attrs = xml_of_attrs obj_attrs in
358 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
360 ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ;
361 X.xml_nempty "ConstantBody"
362 [None,"for",UriManager.string_of_uri uri ;
363 None,"params",params' ; None,"id", id]
364 [< print_term ids_to_inner_sorts bo >]
368 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
369 X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
370 X.xml_nempty "ConstantType"
371 [None,"name",n ; None,"params",params' ; None,"id", id]
372 [< xml_attrs; print_term ids_to_inner_sorts ty >]
376 | C.AVariable (id,n,bo,ty,params,obj_attrs) ->
377 let params' = param_attribute_of_params params in
378 let xml_attrs = xml_of_attrs obj_attrs in
383 X.xml_nempty "body" [] [< print_term ids_to_inner_sorts bo >]
386 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
387 X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
388 X.xml_nempty "Variable"
389 [None,"name",n ; None,"params",params' ; None,"id", id]
391 X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty)
396 | C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) ->
397 let params' = param_attribute_of_params params in
398 let xml_attrs = xml_of_attrs obj_attrs in
399 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
401 ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
402 X.xml_nempty "InductiveDefinition"
403 [None,"noParams",string_of_int nparams ;
405 None,"params",params']
408 (fun i (id,typename,finite,arity,cons) ->
410 X.xml_nempty "InductiveType"
411 [None,"id",id ; None,"name",typename ;
412 None,"inductive",(string_of_bool finite)
414 [< X.xml_nempty "arity" []
415 (print_term ids_to_inner_sorts arity) ;
419 X.xml_nempty "Constructor"
421 (print_term ids_to_inner_sorts lc)
433 print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types
434 ~ask_dtd_to_the_getter
436 let module C2A = Cic2acic in
437 let module X = Xml in
438 let dtdname = dtdname ~ask_dtd_to_the_getter "cictypes.dtd" in
439 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
441 ("<!DOCTYPE InnerTypes SYSTEM \"" ^ dtdname ^ "\">\n") ;
442 X.xml_nempty "InnerTypes" [None,"of",UriManager.string_of_uri curi]
444 (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
446 X.xml_nempty "TYPE" [None,"of",id]
447 [< X.xml_nempty "synthesized" []
448 [< print_term ids_to_inner_sorts synty >] ;
451 | Some expty' -> X.xml_nempty "expected" []
452 [< print_term ids_to_inner_sorts expty' >]
455 ) ids_to_inner_types [<>]