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;;
30 let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
32 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
33 let print_term curi ~ids_to_inner_sorts =
37 let module U = UriManager in
40 let sort = Hashtbl.find ids_to_inner_sorts id in
42 ["value",(string_of_int n) ; "binder",b ; "id",id ; "sort",sort]
44 let vdepth = U.depth_of_uri uri
45 and cdepth = U.depth_of_uri curi
46 and sort = Hashtbl.find ids_to_inner_sorts id in
48 ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
50 "id",id ; "sort",sort]
52 let sort = Hashtbl.find ids_to_inner_sorts id in
53 X.xml_nempty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort]
58 [< i ; X.xml_nempty "substitution" [] (aux t') >]
60 [< i ; X.xml_empty "substitution" [] >]
69 X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
70 | C.AImplicit _ -> raise NotImplemented
71 | C.AProd (id,C.Anonimous,s,t) ->
72 let ty = Hashtbl.find ids_to_inner_sorts id in
73 X.xml_nempty "PROD" ["id",id ; "type",ty]
74 [< X.xml_nempty "source" [] (aux s) ;
75 X.xml_nempty "target" [] (aux t)
77 | C.AProd (xid,C.Name id,s,t) ->
78 let ty = Hashtbl.find ids_to_inner_sorts xid in
79 X.xml_nempty "PROD" ["id",xid ; "type",ty]
80 [< X.xml_nempty "source" [] (aux s) ;
81 X.xml_nempty "target" ["binder",id] (aux t)
84 let sort = Hashtbl.find ids_to_inner_sorts id in
85 X.xml_nempty "CAST" ["id",id ; "sort",sort]
86 [< X.xml_nempty "term" [] (aux v) ;
87 X.xml_nempty "type" [] (aux t)
89 | C.ALambda (id,C.Anonimous,s,t) ->
90 let sort = Hashtbl.find ids_to_inner_sorts id in
91 X.xml_nempty "LAMBDA" ["id",id ; "sort",sort]
92 [< X.xml_nempty "source" [] (aux s) ;
93 X.xml_nempty "target" [] (aux t)
95 | C.ALambda (xid,C.Name id,s,t) ->
96 let sort = Hashtbl.find ids_to_inner_sorts xid in
97 X.xml_nempty "LAMBDA" ["id",xid ; "sort",sort]
98 [< X.xml_nempty "source" [] (aux s) ;
99 X.xml_nempty "target" ["binder",id] (aux t)
101 | C.ALetIn (xid,C.Anonimous,s,t) ->
103 | C.ALetIn (xid,C.Name id,s,t) ->
104 let sort = Hashtbl.find ids_to_inner_sorts xid in
105 X.xml_nempty "LETIN" ["id",xid ; "sort",sort]
106 [< X.xml_nempty "term" [] (aux s) ;
107 X.xml_nempty "letintarget" ["binder",id] (aux t)
110 let sort = Hashtbl.find ids_to_inner_sorts id in
111 X.xml_nempty "APPLY" ["id",id ; "sort",sort]
112 [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
114 | C.AConst (id,uri,_) ->
115 let sort = Hashtbl.find ids_to_inner_sorts id in
117 ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort]
118 | C.AMutInd (id,uri,_,i) ->
120 ["uri", (U.string_of_uri uri) ;
121 "noType",(string_of_int i) ;
123 | C.AMutConstruct (id,uri,_,i,j) ->
124 let sort = Hashtbl.find ids_to_inner_sorts id in
125 X.xml_empty "MUTCONSTRUCT"
126 ["uri", (U.string_of_uri uri) ;
127 "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
128 "id",id ; "sort",sort]
129 | C.AMutCase (id,uri,_,typeno,ty,te,patterns) ->
130 let sort = Hashtbl.find ids_to_inner_sorts id in
131 X.xml_nempty "MUTCASE"
132 ["uriType",(U.string_of_uri uri) ;
133 "noType", (string_of_int typeno) ;
134 "id", id ; "sort",sort]
135 [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
136 X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
138 (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
141 | C.AFix (id, no, funs) ->
142 let sort = Hashtbl.find ids_to_inner_sorts id in
144 ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
146 (fun (fi,ai,ti,bi) i ->
147 [< X.xml_nempty "FixFunction"
148 ["name", fi; "recIndex", (string_of_int ai)]
149 [< X.xml_nempty "type" [] [< aux ti >] ;
150 X.xml_nempty "body" [] [< aux bi >]
156 | C.ACoFix (id,no,funs) ->
157 let sort = Hashtbl.find ids_to_inner_sorts id in
159 ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
162 [< X.xml_nempty "CofixFunction" ["name", fi]
163 [< X.xml_nempty "type" [] [< aux ti >] ;
164 X.xml_nempty "body" [] [< aux bi >]
174 exception NotImplemented;;
176 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
177 let print_object curi ~ids_to_inner_sorts =
179 let module C = Cic in
180 let module X = Xml in
181 let module U = UriManager in
183 C.ACurrentProof (id,n,conjectures,bo,ty) ->
184 X.xml_nempty "CurrentProof" ["name",n ; "id", id]
186 (fun i (cid,n,canonical_context,t) ->
188 X.xml_nempty "Conjecture"
189 ["id", cid ; "no",(string_of_int n)]
193 Some (n,C.ADecl t) ->
196 C.Name n' -> ["id",hid;"name",n']
197 | C.Anonimous -> ["id",hid])
198 (print_term curi ids_to_inner_sorts t)
199 | Some (n,C.ADef t) ->
202 C.Name n' -> ["id",hid;"name",n']
203 | C.Anonimous -> ["id",hid])
204 (print_term curi ids_to_inner_sorts t)
205 | None -> X.xml_empty "Hidden" ["id",hid]
209 ) [< >] canonical_context ;
210 X.xml_nempty "Goal" []
211 (print_term curi ids_to_inner_sorts t)
215 X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
216 X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty) >]
217 | C.ADefinition (id,n,bo,ty,C.Actual params) ->
223 U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i'
224 ) x "" ^ match i with "" -> "" | i' -> " " ^ i'
227 X.xml_nempty "Definition" ["name",n ; "params",params' ; "id", id]
228 [< X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
229 X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty) >]
230 | C.ADefinition _ -> assert false
231 | _ -> raise NotImplemented
236 let print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types =
237 let module C2A = Cic2acic in
238 let module X = Xml in
239 X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
241 (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
243 X.xml_nempty "TYPE" ["of",id]
244 [< print_term curi ids_to_inner_sorts synty ;
247 | Some expty' -> print_term curi ids_to_inner_sorts expty'
250 ) ids_to_inner_types [<>]