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 NotImplemented;;
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
34 "http://mowgli.cs.unibo.it/dtd/" ^ dtd
37 let param_attribute_of_params params =
38 String.concat " " (List.map UriManager.string_of_uri params)
41 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
42 let print_term ?ids_to_inner_sorts =
43 let find_sort name id =
44 match ids_to_inner_sorts with
46 | Some ids_to_inner_sorts ->
47 [None,name,Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id)]
52 let module U = UriManager in
54 C.ARel (id,idref,n,b) ->
55 let sort = find_sort "sort" id in
58 [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ;
60 | C.AVar (id,uri,exp_named_subst) ->
61 let sort = find_sort "sort" id in
64 (sort @ [None,"uri",U.string_of_uri uri;None,"id",id]))
67 let sort = find_sort "sort" id in
69 (sort @ [None,"no",(string_of_int n) ; None,"id",id])
74 [< i ; X.xml_nempty "substitution" [] (aux t') >]
76 [< i ; X.xml_empty "substitution" [] >]
79 let string_of_sort s =
80 Cic2acic.string_of_sort (Cic2acic.sort_of_sort s)
82 X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id]
83 | C.AImplicit _ -> raise NotImplemented
84 | C.AProd (last_id,_,_,_) as prods ->
88 let prods,t' = eat_prods t in
92 let prods,t = eat_prods prods in
93 let sort = find_sort "type" last_id in
94 X.xml_nempty "PROD" sort
96 (fun i (id,binder,s) ->
97 let sort = find_sort "type" (Cic2acic.source_id_of_id id) in
99 sort @ ((None,"id",id)::
102 | C.Name b -> [None,"binder",b])
104 [< i ; X.xml_nempty "decl" attrs (aux s) >]
106 X.xml_nempty "target" [] (aux t)
108 | C.ACast (id,v,t) ->
109 let sort = find_sort "sort" id in
110 X.xml_nempty "CAST" (sort @ [None,"id",id])
111 [< X.xml_nempty "term" [] (aux v) ;
112 X.xml_nempty "type" [] (aux t)
114 | C.ALambda (last_id,_,_,_) as lambdas ->
115 let rec eat_lambdas =
117 C.ALambda (id,n,s,t) ->
118 let lambdas,t' = eat_lambdas t in
122 let lambdas,t = eat_lambdas lambdas in
123 let sort = find_sort "sort" last_id in
124 X.xml_nempty "LAMBDA" sort
126 (fun i (id,binder,s) ->
127 let sort = find_sort "type" (Cic2acic.source_id_of_id id) in
129 sort @ ((None,"id",id)::
132 | C.Name b -> [None,"binder",b])
134 [< i ; X.xml_nempty "decl" attrs (aux s) >]
136 X.xml_nempty "target" [] (aux t)
138 | C.ALetIn (xid,C.Anonymous,s,t) ->
140 | C.ALetIn (last_id,C.Name _,_,_) as letins ->
143 C.ALetIn (id,n,s,t) ->
144 let letins,t' = eat_letins t in
148 let letins,t = eat_letins letins in
149 let sort = find_sort "sort" last_id in
150 X.xml_nempty "LETIN" sort
152 (fun i (id,binder,s) ->
153 let sort = find_sort "sort" id in
155 sort @ ((None,"id",id)::
158 | C.Name b -> [None,"binder",b])
160 [< i ; X.xml_nempty "def" attrs (aux s) >]
162 X.xml_nempty "target" [] (aux t)
165 let sort = find_sort "sort" id in
166 X.xml_nempty "APPLY" (sort @ [None,"id",id])
167 [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
169 | C.AConst (id,uri,exp_named_subst) ->
170 let sort = find_sort "sort" id in
173 (sort @ [None,"uri",(U.string_of_uri uri) ; None,"id",id])
175 | C.AMutInd (id,uri,i,exp_named_subst) ->
177 (X.xml_empty "MUTIND"
178 [None, "uri", (U.string_of_uri uri) ;
179 None, "noType", (string_of_int i) ;
182 | C.AMutConstruct (id,uri,i,j,exp_named_subst) ->
183 let sort = find_sort "sort" id in
185 (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) ;
192 | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
193 let sort = find_sort "sort" id in
194 X.xml_nempty "MUTCASE"
196 [None,"uriType",(U.string_of_uri uri) ;
197 None,"noType", (string_of_int typeno) ;
199 [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
200 X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
202 (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
205 | C.AFix (id, no, funs) ->
206 let sort = find_sort "sort" id in
208 (sort @ [None,"noFun", (string_of_int no) ; None,"id",id])
210 (fun (id,fi,ai,ti,bi) i ->
211 [< X.xml_nempty "FixFunction"
212 [None,"id",id ; None,"name", fi ;
213 None,"recIndex", (string_of_int ai)]
214 [< X.xml_nempty "type" [] [< aux ti >] ;
215 X.xml_nempty "body" [] [< aux bi >]
221 | C.ACoFix (id,no,funs) ->
222 let sort = find_sort "sort" id in
224 (sort @ [None,"noFun", (string_of_int no) ; None,"id",id])
226 (fun (id,fi,ti,bi) i ->
227 [< X.xml_nempty "CofixFunction" [None,"id",id ; None,"name", fi]
228 [< X.xml_nempty "type" [] [< aux ti >] ;
229 X.xml_nempty "body" [] [< aux bi >]
235 and aux_subst buri target subst =
236 (*CSC: I have now no way to assign an ID to the explicit named substitution *)
241 Xml.xml_nempty "instantiate"
242 (match id with None -> [] | Some id -> [None,"id",id])
248 Str.split (Str.regexp "/") (UriManager.string_of_uri buri) in
250 Str.split (Str.regexp "/") (UriManager.string_of_uri uri) in
251 let rec find_relUri buri_frags uri_frags =
252 match buri_frags,uri_frags with
253 [_], _ -> String.concat "/" uri_frags
254 | he1::tl1, he2::tl2 ->
257 | _,_ -> assert false (* uri is not relative to buri *)
259 find_relUri buri_frags uri_frags
261 [< i ; Xml.xml_nempty "arg" [None,"relUri", relUri] (aux arg) >]
268 let xml_of_attrs attributes =
269 let class_of = function
270 | `Coercion -> Xml.xml_empty "class" [None,"value","coercion"]
272 Xml.xml_nempty "class" [None,"value","elim"]
274 "SORT" [None,"value",
275 (Cic2acic.string_of_sort (Cic2acic.sort_of_sort s)) ;
276 None,"id","elimination_sort"] >]
277 | `Record field_names ->
278 Xml.xml_nempty "class" [None,"value","record"]
280 (fun (name,coercion) res ->
281 [< Xml.xml_empty "field"
282 [None,"name",if coercion then name ^ " coercion" else name];
285 | `Projection -> Xml.xml_empty "class" [None,"value","projection"]
287 let flavour_of = function
288 | `Definition -> Xml.xml_empty "flavour" [None, "value", "definition"]
289 | `Fact -> Xml.xml_empty "flavour" [None, "value", "fact"]
290 | `Lemma -> Xml.xml_empty "flavour" [None, "value", "lemma"]
291 | `Remark -> Xml.xml_empty "flavour" [None, "value", "remark"]
292 | `Theorem -> Xml.xml_empty "flavour" [None, "value", "theorem"]
293 | `Variant -> Xml.xml_empty "flavour" [None, "value", "variant"]
295 let xml_attr_of = function
296 | `Generated -> Xml.xml_empty "generated" []
297 | `Class c -> class_of c
298 | `Flavour f -> flavour_of f
302 (fun attr res -> [< xml_attr_of attr ; res >]) attributes [<>]
304 Xml.xml_nempty "attributes" [] xml_attrs
306 let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
307 let module C = Cic in
308 let module X = Xml in
309 let module U = UriManager in
310 let dtdname = dtdname ~ask_dtd_to_the_getter "cic.dtd" in
312 C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params,obj_attrs) ->
313 let params' = param_attribute_of_params params in
314 let xml_attrs = xml_of_attrs obj_attrs in
315 let xml_for_current_proof_body =
316 (*CSC: Should the CurrentProof also have the list of variables it depends on? *)
317 (*CSC: I think so. Not implemented yet. *)
318 X.xml_nempty "CurrentProof"
319 [None,"of",UriManager.string_of_uri uri ; None,"id", id]
322 (fun i (cid,n,canonical_context,t) ->
324 X.xml_nempty "Conjecture"
325 [None,"id",cid ; None,"no",(string_of_int n)]
329 Some (n,C.ADecl t) ->
333 [None,"id",hid;None,"name",n']
334 | C.Anonymous -> [None,"id",hid])
335 (print_term ?ids_to_inner_sorts t)
336 | Some (n,C.ADef t) ->
340 [None,"id",hid;None,"name",n']
341 | C.Anonymous -> [None,"id",hid])
342 (print_term ?ids_to_inner_sorts t)
343 | None -> X.xml_empty "Hidden" [None,"id",hid]
347 ) [< >] canonical_context ;
348 X.xml_nempty "Goal" []
349 (print_term ?ids_to_inner_sorts t)
353 X.xml_nempty "body" [] (print_term ?ids_to_inner_sorts bo) >]
355 let xml_for_current_proof_type =
356 X.xml_nempty "ConstantType"
357 [None,"name",n ; None,"params",params' ; None,"id", id]
358 (print_term ?ids_to_inner_sorts ty)
361 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
362 X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^ dtdname ^ "\">\n");
363 xml_for_current_proof_body
366 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
367 X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
368 xml_for_current_proof_type
372 | C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) ->
373 let params' = param_attribute_of_params params in
374 let xml_attrs = xml_of_attrs obj_attrs in
381 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
383 ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ;
384 X.xml_nempty "ConstantBody"
385 [None,"for",UriManager.string_of_uri uri ;
386 None,"params",params' ; None,"id", id]
387 [< print_term ?ids_to_inner_sorts bo >]
391 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
392 X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
393 X.xml_nempty "ConstantType"
394 [None,"name",n ; None,"params",params' ; None,"id", id]
395 [< xml_attrs; print_term ?ids_to_inner_sorts ty >]
399 | C.AVariable (id,n,bo,ty,params,obj_attrs) ->
400 let params' = param_attribute_of_params params in
401 let xml_attrs = xml_of_attrs obj_attrs in
406 X.xml_nempty "body" [] [< print_term ?ids_to_inner_sorts bo >]
409 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
410 X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
411 X.xml_nempty "Variable"
412 [None,"name",n ; None,"params",params' ; None,"id", id]
414 X.xml_nempty "type" [] (print_term ?ids_to_inner_sorts ty)
419 | C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) ->
420 let params' = param_attribute_of_params params in
421 let xml_attrs = xml_of_attrs obj_attrs in
422 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
424 ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
425 X.xml_nempty "InductiveDefinition"
426 [None,"noParams",string_of_int nparams ;
428 None,"params",params']
431 (fun i (id,typename,finite,arity,cons) ->
433 X.xml_nempty "InductiveType"
434 [None,"id",id ; None,"name",typename ;
435 None,"inductive",(string_of_bool finite)
437 [< X.xml_nempty "arity" []
438 (print_term ?ids_to_inner_sorts arity) ;
442 X.xml_nempty "Constructor"
444 (print_term ?ids_to_inner_sorts lc)
456 print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types
457 ~ask_dtd_to_the_getter
459 let module C2A = Cic2acic in
460 let module X = Xml in
461 let dtdname = dtdname ~ask_dtd_to_the_getter "cictypes.dtd" in
462 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
464 ("<!DOCTYPE InnerTypes SYSTEM \"" ^ dtdname ^ "\">\n") ;
465 X.xml_nempty "InnerTypes" [None,"of",UriManager.string_of_uri curi]
467 (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
469 X.xml_nempty "TYPE" [None,"of",id]
470 [< X.xml_nempty "synthesized" []
471 [< print_term ~ids_to_inner_sorts synty >] ;
474 | Some expty' -> X.xml_nempty "expected" []
475 [< print_term ~ids_to_inner_sorts expty' >]
478 ) ids_to_inner_types [<>]