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) *)
38 let module U = UriManager in
41 X.xml_empty "REL" ["value",(string_of_int n);"binder",b;"id",id]
43 let vdepth = U.depth_of_uri uri
44 and cdepth = U.depth_of_uri curi in
46 ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
50 X.xml_empty "META" ["no",(string_of_int n) ; "id",id]
58 X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
59 | C.AImplicit _ -> raise NotImplemented
60 | C.AProd (id,C.Anonimous,s,t) ->
61 X.xml_nempty "PROD" ["id",id]
62 [< X.xml_nempty "source" [] (aux s) ;
63 X.xml_nempty "target" [] (aux t)
65 | C.AProd (xid,C.Name id,s,t) ->
66 X.xml_nempty "PROD" ["id",xid]
67 [< X.xml_nempty "source" [] (aux s) ;
68 X.xml_nempty "target" ["binder",id] (aux t)
71 X.xml_nempty "CAST" ["id",id]
72 [< X.xml_nempty "term" [] (aux v) ;
73 X.xml_nempty "type" [] (aux t)
75 | C.ALambda (id,C.Anonimous,s,t) ->
76 X.xml_nempty "LAMBDA" ["id",id]
77 [< X.xml_nempty "source" [] (aux s) ;
78 X.xml_nempty "target" [] (aux t)
80 | C.ALambda (xid,C.Name id,s,t) ->
81 X.xml_nempty "LAMBDA" ["id",xid]
82 [< X.xml_nempty "source" [] (aux s) ;
83 X.xml_nempty "target" ["binder",id] (aux t)
85 | C.ALetIn (xid,C.Anonimous,s,t) ->
86 assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
87 | C.ALetIn (xid,C.Name id,s,t) ->
88 X.xml_nempty "LETIN" ["id",xid]
89 [< X.xml_nempty "term" [] (aux s) ;
90 X.xml_nempty "letintarget" ["binder",id] (aux t)
93 X.xml_nempty "APPLY" ["id",id]
94 [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
96 | C.AConst (id,uri,_) ->
97 X.xml_empty "CONST" ["uri", (U.string_of_uri uri) ; "id",id]
98 | C.AAbst (id,uri) -> raise NotImplemented
99 | C.AMutInd (id,uri,_,i) ->
101 ["uri", (U.string_of_uri uri) ;
102 "noType",(string_of_int i) ;
104 | C.AMutConstruct (id,uri,_,i,j) ->
105 X.xml_empty "MUTCONSTRUCT"
106 ["uri", (U.string_of_uri uri) ;
107 "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
109 | C.AMutCase (id,uri,_,typeno,ty,te,patterns) ->
110 X.xml_nempty "MUTCASE"
111 ["uriType",(U.string_of_uri uri) ;
112 "noType", (string_of_int typeno) ;
114 [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
115 X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
117 (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
120 | C.AFix (id, no, funs) ->
121 X.xml_nempty "FIX" ["noFun", (string_of_int no) ; "id",id]
123 (fun (fi,ai,ti,bi) i ->
124 [< X.xml_nempty "FixFunction"
125 ["name", fi; "recIndex", (string_of_int ai)]
126 [< X.xml_nempty "type" [] [< aux ti >] ;
127 X.xml_nempty "body" [] [< aux bi >]
133 | C.ACoFix (id,no,funs) ->
134 X.xml_nempty "COFIX" ["noFun", (string_of_int no) ; "id",id]
137 [< X.xml_nempty "CofixFunction" ["name", fi]
138 [< X.xml_nempty "type" [] [< aux ti >] ;
139 X.xml_nempty "body" [] [< aux bi >]
155 string_of_int n ^ ": " ^
156 String.concat " " (List.map UriManager.name_of_uri l) ^
161 let print_mutual_inductive_type curi (typename,inductive,arity,constructors) =
162 let module C = Cic in
163 let module X = Xml in
164 [< X.xml_nempty "InductiveType"
166 "inductive",(string_of_bool inductive)
168 [< X.xml_nempty "arity" [] (print_term curi arity) ;
170 (fun (name,ty,_) i ->
171 [< X.xml_nempty "Constructor" ["name",name]
172 (print_term curi ty) ;
183 let module C = Cic in
184 let module X = Xml in
186 C.ADefinition (xid, id, te, ty, params) ->
187 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
188 X.xml_cdata ("<!DOCTYPE Definition SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
189 X.xml_nempty "Definition"
190 (["name", id ; "id",xid] @
192 C.Possible _ -> raise ImpossiblePossible
193 (*CSC params are kept in inverted order in the internal *)
194 (* representation (the order of application) *)
195 | C.Actual fv' -> ["params",(encode (List.rev fv'))])
196 [< X.xml_nempty "body" [] (print_term curi te) ;
197 X.xml_nempty "type" [] (print_term curi ty) >]
199 | C.AAxiom (xid, id, ty, params) ->
200 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
201 X.xml_cdata ("<!DOCTYPE Axiom SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
203 (*CSC params are kept in inverted order in the internal *)
204 (* representation (the order of application) *)
205 ["name",id ; "params",(encode (List.rev params)) ; "id",xid]
206 [< X.xml_nempty "type" [] (print_term curi ty) >]
208 | C.AVariable (xid, name, bo, ty) ->
209 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
210 X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
211 X.xml_nempty "Variable" ["name",name ; "id",xid]
214 | Some bo -> X.xml_nempty "body" [] (print_term curi bo)
216 X.xml_nempty "type" [] (print_term curi ty)
219 | C.ACurrentProof (xid, name, conjs, bo, ty) ->
220 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
221 X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n");
222 X.xml_nempty "CurrentProof" ["name",name ; "id",xid]
225 [< X.xml_nempty "Conjecture" ["no",(string_of_int j)]
226 [< print_term curi t >] ; i >])
228 X.xml_nempty "body" [] [< print_term curi bo >] ;
229 X.xml_nempty "type" [] [< print_term curi ty >]
232 | C.AInductiveDefinition (xid, tys, params, paramsno) ->
235 (fun (typename,_,_,_) -> typename)
238 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
239 X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
240 dtdname ^ "\">\n\n") ;
241 X.xml_nempty "InductiveDefinition"
242 (*CSC params are kept in inverted order in the internal *)
243 (* representation (the order of application) *)
244 ["noParams",string_of_int paramsno ;
245 "params",(encode (List.rev params)) ;
248 (fun x i -> [< print_mutual_inductive_type curi x ; i >])