1 (* Copyright (C) 2000, 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://cs.unibo.it/helm/.
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 Configuration.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 =
47 let module U = UriManager in
49 C.ARel (id,idref,n,b) ->
50 let sort = Hashtbl.find ids_to_inner_sorts id in
52 ["value",(string_of_int n) ; "binder",b ; "id",id ; "idref",idref ;
54 | C.AVar (id,uri,exp_named_subst) ->
55 let sort = Hashtbl.find ids_to_inner_sorts id in
57 (X.xml_empty "VAR" ["uri",U.string_of_uri uri;"id",id;"sort",sort])
60 let sort = Hashtbl.find ids_to_inner_sorts id in
61 X.xml_nempty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort]
66 [< i ; X.xml_nempty "substitution" [] (aux t') >]
68 [< i ; X.xml_empty "substitution" [] >]
77 X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
78 | C.AImplicit _ -> raise NotImplemented
79 | C.AProd (last_id,_,_,_) as prods ->
83 let prods,t' = eat_prods t in
87 let prods,t = eat_prods prods in
88 let sort = Hashtbl.find ids_to_inner_sorts last_id in
89 X.xml_nempty "PROD" ["type",sort]
91 (fun i (id,binder,s) ->
92 let sort = Hashtbl.find ids_to_inner_sorts id in
94 ("id",id)::("type",sort)::
97 | C.Name b -> ["binder",b]
99 [< i ; X.xml_nempty "decl" attrs (aux s) >]
101 X.xml_nempty "target" [] (aux t)
103 | C.ACast (id,v,t) ->
104 let sort = Hashtbl.find ids_to_inner_sorts id in
105 X.xml_nempty "CAST" ["id",id ; "sort",sort]
106 [< X.xml_nempty "term" [] (aux v) ;
107 X.xml_nempty "type" [] (aux t)
109 | C.ALambda (last_id,_,_,_) as lambdas ->
110 let rec eat_lambdas =
112 C.ALambda (id,n,s,t) ->
113 let lambdas,t' = eat_lambdas t in
117 let lambdas,t = eat_lambdas lambdas in
118 let sort = Hashtbl.find ids_to_inner_sorts last_id in
119 X.xml_nempty "LAMBDA" ["sort",sort]
121 (fun i (id,binder,s) ->
122 let sort = Hashtbl.find ids_to_inner_sorts id in
124 ("id",id)::("type",sort)::
127 | C.Name b -> ["binder",b]
129 [< i ; X.xml_nempty "decl" attrs (aux s) >]
131 X.xml_nempty "target" [] (aux t)
133 | C.ALetIn (xid,C.Anonymous,s,t) ->
135 | C.ALetIn (last_id,C.Name _,_,_) as letins ->
138 C.ALetIn (id,n,s,t) ->
139 let letins,t' = eat_letins t in
143 let letins,t = eat_letins letins in
144 let sort = Hashtbl.find ids_to_inner_sorts last_id in
145 X.xml_nempty "LETIN" ["sort",sort]
147 (fun i (id,binder,s) ->
148 let sort = Hashtbl.find ids_to_inner_sorts id in
150 ("id",id)::("sort",sort)::
153 | C.Name b -> ["binder",b]
155 [< i ; X.xml_nempty "def" attrs (aux s) >]
157 X.xml_nempty "target" [] (aux t)
160 let sort = Hashtbl.find ids_to_inner_sorts id in
161 X.xml_nempty "APPLY" ["id",id ; "sort",sort]
162 [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
164 | C.AConst (id,uri,exp_named_subst) ->
165 let sort = Hashtbl.find ids_to_inner_sorts id in
168 ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort]
170 | C.AMutInd (id,uri,i,exp_named_subst) ->
172 (X.xml_empty "MUTIND"
173 ["uri", (U.string_of_uri uri) ;
174 "noType",(string_of_int i) ;
177 | C.AMutConstruct (id,uri,i,j,exp_named_subst) ->
178 let sort = Hashtbl.find ids_to_inner_sorts id in
180 (X.xml_empty "MUTCONSTRUCT"
181 ["uri", (U.string_of_uri uri) ;
182 "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
183 "id",id ; "sort",sort]
185 | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
186 let sort = Hashtbl.find ids_to_inner_sorts id in
187 X.xml_nempty "MUTCASE"
188 ["uriType",(U.string_of_uri uri) ;
189 "noType", (string_of_int typeno) ;
190 "id", id ; "sort",sort]
191 [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
192 X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
194 (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
197 | C.AFix (id, no, funs) ->
198 let sort = Hashtbl.find ids_to_inner_sorts id in
200 ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
202 (fun (id,fi,ai,ti,bi) i ->
203 [< X.xml_nempty "FixFunction"
204 ["id",id ; "name", fi ; "recIndex", (string_of_int ai)]
205 [< X.xml_nempty "type" [] [< aux ti >] ;
206 X.xml_nempty "body" [] [< aux bi >]
212 | C.ACoFix (id,no,funs) ->
213 let sort = Hashtbl.find ids_to_inner_sorts id in
215 ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
217 (fun (id,fi,ti,bi) i ->
218 [< X.xml_nempty "CofixFunction" ["id",id ; "name", fi]
219 [< X.xml_nempty "type" [] [< aux ti >] ;
220 X.xml_nempty "body" [] [< aux bi >]
226 and aux_subst buri target subst =
227 (*CSC: I have now no way to assign an ID to the explicit named substitution *)
232 Xml.xml_nempty "instantiate"
233 (match id with None -> [] | Some id -> ["id",id])
239 Str.split (Str.regexp "/") (UriManager.string_of_uri buri) in
241 Str.split (Str.regexp "/") (UriManager.string_of_uri uri) in
242 let rec find_relUri buri_frags uri_frags =
243 match buri_frags,uri_frags with
244 [_], _ -> String.concat "/" uri_frags
245 | he1::tl1, he2::tl2 ->
248 | _,_ -> assert false (* uri is not relative to buri *)
250 find_relUri buri_frags uri_frags
252 [< i ; Xml.xml_nempty "arg" ["relUri", relUri] (aux arg) >]
259 let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
260 let module C = Cic in
261 let module X = Xml in
262 let module U = UriManager in
263 let dtdname = dtdname ~ask_dtd_to_the_getter "cic.dtd" in
265 C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) ->
266 let params' = param_attribute_of_params params in
267 let xml_for_current_proof_body =
268 (*CSC: Should the CurrentProof also have the list of variables it depends on? *)
269 (*CSC: I think so. Not implemented yet. *)
270 X.xml_nempty "CurrentProof"
271 ["of",UriManager.string_of_uri uri ; "id", id]
273 (fun i (cid,n,canonical_context,t) ->
275 X.xml_nempty "Conjecture"
276 ["id", cid ; "no",(string_of_int n)]
280 Some (n,C.ADecl t) ->
283 C.Name n' -> ["id",hid;"name",n']
284 | C.Anonymous -> ["id",hid])
285 (print_term ids_to_inner_sorts t)
286 | Some (n,C.ADef t) ->
289 C.Name n' -> ["id",hid;"name",n']
290 | C.Anonymous -> ["id",hid])
291 (print_term ids_to_inner_sorts t)
292 | None -> X.xml_empty "Hidden" ["id",hid]
296 ) [< >] canonical_context ;
297 X.xml_nempty "Goal" []
298 (print_term ids_to_inner_sorts t)
302 X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >]
304 let xml_for_current_proof_type =
305 X.xml_nempty "ConstantType" ["name",n ; "params",params' ; "id", id]
306 (print_term ids_to_inner_sorts ty)
309 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
310 X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^ dtdname ^ "\">\n");
311 xml_for_current_proof_body
314 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
315 X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
316 xml_for_current_proof_type
320 | C.AConstant (id,idbody,n,bo,ty,params) ->
321 let params' = param_attribute_of_params params in
328 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
330 ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ;
331 X.xml_nempty "ConstantBody"
332 ["for",UriManager.string_of_uri uri ; "params",params' ;
334 [< print_term ids_to_inner_sorts bo >]
338 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
339 X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
340 X.xml_nempty "ConstantType"
341 ["name",n ; "params",params' ; "id", id]
342 [< print_term ids_to_inner_sorts ty >]
346 | C.AVariable (id,n,bo,ty,params) ->
347 let params' = param_attribute_of_params params in
352 X.xml_nempty "body" [] [< print_term ids_to_inner_sorts bo >]
355 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
356 X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
357 X.xml_nempty "Variable"
358 ["name",n ; "params",params' ; "id", id]
360 X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty)
365 | C.AInductiveDefinition (id,tys,params,nparams) ->
366 let params' = param_attribute_of_params params in
367 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
369 ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
370 X.xml_nempty "InductiveDefinition"
371 ["noParams",string_of_int nparams ;
375 (fun i (id,typename,finite,arity,cons) ->
377 X.xml_nempty "InductiveType"
378 ["id",id ; "name",typename ;
379 "inductive",(string_of_bool finite)
381 [< X.xml_nempty "arity" []
382 (print_term ids_to_inner_sorts arity) ;
386 X.xml_nempty "Constructor"
388 (print_term ids_to_inner_sorts lc)
400 print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types
401 ~ask_dtd_to_the_getter
403 let module C2A = Cic2acic in
404 let module X = Xml in
405 let dtdname = dtdname ~ask_dtd_to_the_getter "cictypes.dtd" in
406 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
408 ("<!DOCTYPE InnerTypes SYSTEM \"" ^ dtdname ^ "\">\n") ;
409 X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
411 (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
413 X.xml_nempty "TYPE" ["of",id]
414 [< print_term ids_to_inner_sorts synty ;
417 | Some expty' -> print_term ids_to_inner_sorts expty'
420 ) ids_to_inner_types [<>]