2 (* Copyright (C) 2000, HELM Team.
4 * This file is part of HELM, an Hypertextual, Electronic
5 * Library of Mathematics, developed at the Computer Science
6 * Department, University of Bologna, Italy.
8 * HELM is free software; you can redistribute it and/or
9 * modify it under the terms of the GNU General Public License
10 * as published by the Free Software Foundation; either version 2
11 * of the License, or (at your option) any later version.
13 * HELM is distributed in the hope that it will be useful,
14 * but WITHOUT ANY WARRANTY; without even the implied warranty of
15 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
16 * GNU General Public License for more details.
18 * You should have received a copy of the GNU General Public License
19 * along with HELM; if not, write to the Free Software
20 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
23 * For details, see the HELM World-Wide-Web page,
24 * http://cs.unibo.it/helm/.
27 (*CSC codice cut & paste da cicPp e xmlcommand *)
29 exception ImpossiblePossible;;
30 exception NotImplemented;;
31 let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
33 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
34 let print_term curi ids_to_inner_sorts =
38 let module U = UriManager in
41 let sort = Hashtbl.find ids_to_inner_sorts id in
43 ["value",(string_of_int n) ; "binder",b ; "id",id ; "sort",sort]
45 let vdepth = U.depth_of_uri uri
46 and cdepth = U.depth_of_uri curi
47 and sort = Hashtbl.find ids_to_inner_sorts id in
49 ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
51 "id",id ; "sort",sort]
53 let sort = Hashtbl.find ids_to_inner_sorts id in
54 X.xml_nempty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort]
59 [< i ; X.xml_nempty "substitution" [] (aux t') >]
61 [< i ; X.xml_empty "substitution" [] >]
70 X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
71 | C.AImplicit _ -> raise NotImplemented
72 | C.AProd (id,C.Anonimous,s,t) ->
73 let ty = Hashtbl.find ids_to_inner_sorts id in
74 X.xml_nempty "PROD" ["id",id ; "type",ty]
75 [< X.xml_nempty "source" [] (aux s) ;
76 X.xml_nempty "target" [] (aux t)
78 | C.AProd (xid,C.Name id,s,t) ->
79 let ty = Hashtbl.find ids_to_inner_sorts xid in
80 X.xml_nempty "PROD" ["id",xid ; "type",ty]
81 [< X.xml_nempty "source" [] (aux s) ;
82 X.xml_nempty "target" ["binder",id] (aux t)
85 let sort = Hashtbl.find ids_to_inner_sorts id in
86 X.xml_nempty "CAST" ["id",id ; "sort",sort]
87 [< X.xml_nempty "term" [] (aux v) ;
88 X.xml_nempty "type" [] (aux t)
90 | C.ALambda (id,C.Anonimous,s,t) ->
91 let sort = Hashtbl.find ids_to_inner_sorts id in
92 X.xml_nempty "LAMBDA" ["id",id ; "sort",sort]
93 [< X.xml_nempty "source" [] (aux s) ;
94 X.xml_nempty "target" [] (aux t)
96 | C.ALambda (xid,C.Name id,s,t) ->
97 let sort = Hashtbl.find ids_to_inner_sorts xid in
98 X.xml_nempty "LAMBDA" ["id",xid ; "sort",sort]
99 [< X.xml_nempty "source" [] (aux s) ;
100 X.xml_nempty "target" ["binder",id] (aux t)
102 | C.ALetIn (xid,C.Anonimous,s,t) ->
104 | C.ALetIn (xid,C.Name id,s,t) ->
105 let sort = Hashtbl.find ids_to_inner_sorts xid in
106 X.xml_nempty "LETIN" ["id",xid ; "sort",sort]
107 [< X.xml_nempty "term" [] (aux s) ;
108 X.xml_nempty "letintarget" ["binder",id] (aux t)
111 let sort = Hashtbl.find ids_to_inner_sorts id in
112 X.xml_nempty "APPLY" ["id",id ; "sort",sort]
113 [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
115 | C.AConst (id,uri,_) ->
116 let sort = Hashtbl.find ids_to_inner_sorts id in
118 ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort]
119 | C.AAbst (id,uri) -> raise NotImplemented
120 | C.AMutInd (id,uri,_,i) ->
122 ["uri", (U.string_of_uri uri) ;
123 "noType",(string_of_int i) ;
125 | C.AMutConstruct (id,uri,_,i,j) ->
126 let sort = Hashtbl.find ids_to_inner_sorts id in
127 X.xml_empty "MUTCONSTRUCT"
128 ["uri", (U.string_of_uri uri) ;
129 "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
130 "id",id ; "sort",sort]
131 | C.AMutCase (id,uri,_,typeno,ty,te,patterns) ->
132 let sort = Hashtbl.find ids_to_inner_sorts id in
133 X.xml_nempty "MUTCASE"
134 ["uriType",(U.string_of_uri uri) ;
135 "noType", (string_of_int typeno) ;
136 "id", id ; "sort",sort]
137 [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
138 X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
140 (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
143 | C.AFix (id, no, funs) ->
144 let sort = Hashtbl.find ids_to_inner_sorts id in
146 ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
148 (fun (fi,ai,ti,bi) i ->
149 [< X.xml_nempty "FixFunction"
150 ["name", fi; "recIndex", (string_of_int ai)]
151 [< X.xml_nempty "type" [] [< aux ti >] ;
152 X.xml_nempty "body" [] [< aux bi >]
158 | C.ACoFix (id,no,funs) ->
159 let sort = Hashtbl.find ids_to_inner_sorts id in
161 ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
164 [< X.xml_nempty "CofixFunction" ["name", fi]
165 [< X.xml_nempty "type" [] [< aux ti >] ;
166 X.xml_nempty "body" [] [< aux bi >]
176 exception NotImplemented;;
178 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
179 let print_object curi ids_to_inner_sorts =
181 let module C = Cic in
182 let module X = Xml in
183 let module U = UriManager in
185 C.ACurrentProof (id,n,conjectures,bo,ty) ->
186 X.xml_nempty "CurrentProof" ["name",n ; "id", id]
188 (fun i (cid,n,canonical_context,t) ->
190 X.xml_nempty "Conjecture"
191 ["id", cid ; "no",(string_of_int n)]
195 Some (n,C.ADecl t) ->
198 C.Name n' -> ["id",hid;"name",n']
199 | C.Anonimous -> ["id",hid])
200 (print_term curi ids_to_inner_sorts t)
201 | Some (n,C.ADef t) ->
204 C.Name n' -> ["id",hid;"name",n']
205 | C.Anonimous -> ["id",hid])
206 (print_term curi ids_to_inner_sorts t)
207 | None -> X.xml_empty "Hidden" ["id",hid]
211 ) [< >] canonical_context ;
212 X.xml_nempty "Goal" []
213 (print_term curi ids_to_inner_sorts t)
217 X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
218 X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty) >]
219 | C.ADefinition (id,n,bo,ty,C.Actual params) ->
225 U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i'
226 ) x "" ^ match i with "" -> "" | i' -> " " ^ i'
229 X.xml_nempty "Definition" ["name",n ; "params",params' ; "id", id]
230 [< X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
231 X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty) >]
232 | C.ADefinition _ -> assert false
233 | _ -> raise NotImplemented
238 let print_inner_types curi ids_to_inner_sorts ids_to_inner_types =
239 let module X = Xml in
240 X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
244 X.xml_nempty "TYPE" ["of",id]
245 (print_term curi ids_to_inner_sorts ty)
247 ) ids_to_inner_types [<>]