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 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@@cs.unibo.it> *)
33 (* This module is the objects level of a parser for cic objects from xml *)
34 (* files to the internal representation. It uses the module cicParser3 *)
35 (* cicParser3 (terms level) and it is used only through cicParser2 (top *)
38 (******************************************************************************)
40 exception IllFormedXml of int;;
41 exception NotImplemented;;
43 (* Utility functions that transform a Pxp attribute into something useful *)
45 (* mk_absolute_uris "n1: v1 ... vn n2 : u1 ... un ...." *)
46 (* returns [(n1,[absolute_uri_for_v1 ; ... ; absolute_uri_for_vn]) ; (n2,...) *)
47 let mk_absolute_uris s =
48 let l = (Str.split (Str.regexp ":") s) in
49 let absolute_of_relative n v =
50 let module P3 = CicParser3 in
54 | (n,he::tl) when n > 0 ->
55 "/" ^ he ^ mkburi (n - 1, tl)
56 | _ -> raise (IllFormedXml 12)
58 let m = List.length !P3.current_sp - (int_of_string n) in
59 let buri = mkburi (m, !P3.current_sp) in
60 UriManager.uri_of_string ("cic:" ^ buri ^ v ^ ".var")
66 let vars = (Str.split (Str.regexp " ") vs) in
67 [(int_of_string no, List.map (absolute_of_relative no) vars)]
69 let vars = (Str.split (Str.regexp " ") vs) in
74 let (pvars, no2) = add_prefix tl in
75 ((absolute_of_relative no he)::pvars, no2)
76 | _ -> raise (IllFormedXml 11)
78 let (pvars, no2) = add_prefix vars in
79 (int_of_string no, pvars)::(absolutize (no2::tl))
80 | _ -> raise (IllFormedXml 10)
82 (* last parameter must be applied first *)
86 let option_uri_list_of_attr a1 a2 =
87 let module T = Pxp_types in
90 T.Value s -> mk_absolute_uris s
91 | _ -> raise (IllFormedXml 0)
94 T.Value "POSSIBLE" -> Cic.Possible parameters
95 | T.Implied_value -> Cic.Actual parameters
96 | _ -> raise (IllFormedXml 0)
99 let uri_list_of_attr a =
100 let module T = Pxp_types in
102 T.Value s -> mk_absolute_uris s
103 | _ -> raise (IllFormedXml 0)
106 let string_of_attr a =
107 let module T = Pxp_types in
110 | _ -> raise (IllFormedXml 0)
114 int_of_string (string_of_attr a)
118 bool_of_string (string_of_attr a)
122 let module T = Pxp_types in
123 let module C = Cic in
125 T.Value s -> C.Name s
126 | T.Implied_value -> C.Anonimous
127 | _ -> raise (IllFormedXml 0)
130 (* Other utility functions *)
133 match n#sub_nodes with
135 | _ -> raise (IllFormedXml 1)
138 (* Functions that, given the list of sons of a node of the cic dom (objects *)
139 (* level), retrieve the internal representation associated to the node. *)
140 (* Everytime a cic term subtree is found, it is translated to the internal *)
141 (* representation using the method to_cic_term defined in cicParser3. *)
142 (* Each function raise IllFormedXml if something goes wrong, but this should *)
143 (* be impossible due to the presence of the dtd *)
144 (* The functions should really be obvious looking at their name and the cic *)
147 (* called when a CurrentProof is found *)
148 let get_conjs_value_type l =
149 let rec rget (c, v, t) l =
150 let module D = Pxp_document in
153 | conj::tl when conj#node_type = D.T_element "Conjecture" ->
154 let no = int_of_attr (conj#attribute "no") in
155 let typ,canonical_context =
156 match List.rev (conj#sub_nodes) with
157 [] -> raise (IllFormedXml 13)
158 | typ::canonical_context ->
159 (get_content typ)#extension#to_cic_term,
162 match n#node_type with
163 D.T_element "Decl" ->
164 let name = name_of_attr (n#attribute "name") in
165 let term = (get_content n)#extension#to_cic_term in
166 Some (name,Cic.ADecl term)
167 | D.T_element "Def" ->
168 let name = name_of_attr (n#attribute "name") in
169 let term = (get_content n)#extension#to_cic_term in
170 Some (name,Cic.ADef term)
171 | D.T_element "Hidden" -> None
172 | _ -> raise (IllFormedXml 14)
175 rget ((no, canonical_context, typ)::c, v, t) tl
176 | value::tl when value#node_type = D.T_element "body" ->
177 let v' = (get_content value)#extension#to_cic_term in
179 None -> rget (c, Some v', t) tl
180 | _ -> raise (IllFormedXml 2)
182 | typ::tl when typ#node_type = D.T_element "type" ->
183 let t' = (get_content typ)#extension#to_cic_term in
185 None -> rget (c, v, Some t') tl
186 | _ -> raise (IllFormedXml 3)
188 | _ -> raise (IllFormedXml 4)
190 match rget ([], None, None) l with
191 (revc, Some v, Some t) -> (List.rev revc, v, t)
192 | _ -> raise (IllFormedXml 5)
195 (* used only by get_inductive_types; called one time for each inductive *)
196 (* definitions in a block of inductive definitions *)
197 let get_names_arity_constructors l =
198 let rec rget (a,c) l =
199 let module D = Pxp_document in
202 | arity::tl when arity#node_type = D.T_element "arity" ->
203 let a' = (get_content arity)#extension#to_cic_term in
205 | con::tl when con#node_type = D.T_element "Constructor" ->
206 let id = string_of_attr (con#attribute "name")
207 and ty = (get_content con)#extension#to_cic_term in
208 rget (a,(id,ty,ref None)::c) tl
209 | _ -> raise (IllFormedXml 9)
211 match rget (None,[]) l with
212 (Some a, c) -> (a, List.rev c)
213 | _ -> raise (IllFormedXml 8)
216 (* called when an InductiveDefinition is found *)
217 let rec get_inductive_types =
221 let tyname = string_of_attr (he#attribute "name")
222 and inductive = bool_of_attr (he#attribute "inductive")
224 get_names_arity_constructors (he#sub_nodes)
226 (tyname,inductive,arity,cons)::(get_inductive_types tl) (*CSC 0 a caso *)
229 (* This is the main function and also the only one used directly from *)
230 (* cicParser. Given the root of the dom tree, it returns the internal *)
231 (* representation of the cic object described in the tree *)
232 (* It uses the previous functions and the to_cic_term method defined *)
233 (* in cicParser3 (used for subtrees that encode cic terms) *)
235 let module D = Pxp_document in
236 let module C = Cic in
237 let ntype = n # node_type in
239 D.T_element "Definition" ->
240 let id = string_of_attr (n # attribute "name")
242 option_uri_list_of_attr (n#attribute "params") (n#attribute "paramMode")
244 let sons = n#sub_nodes in
247 v#node_type = D.T_element "body" &&
248 t#node_type = D.T_element "type" ->
249 let v' = get_content v
250 and t' = get_content t in
251 (v'#extension#to_cic_term, t'#extension#to_cic_term)
252 | _ -> raise (IllFormedXml 6)
253 and xid = string_of_attr (n#attribute "id") in
254 C.ADefinition (xid, id, value, typ, params)
255 | D.T_element "Axiom" ->
256 let id = string_of_attr (n # attribute "name")
257 and params = uri_list_of_attr (n # attribute "params")
259 (get_content (get_content n))#extension#to_cic_term
260 and xid = string_of_attr (n#attribute "id") in
261 C.AAxiom (xid, id, typ, params)
262 | D.T_element "CurrentProof" ->
263 let name = string_of_attr (n#attribute "name")
264 and xid = string_of_attr (n#attribute "id") in
265 let sons = n#sub_nodes in
266 let (conjs, value, typ) = get_conjs_value_type sons in
267 C.ACurrentProof (xid, name, conjs, value, typ)
268 | D.T_element "InductiveDefinition" ->
269 let sons = n#sub_nodes
270 and xid = string_of_attr (n#attribute "id") in
271 let inductiveTypes = get_inductive_types sons
272 and params = uri_list_of_attr (n#attribute "params")
273 and nparams = int_of_attr (n#attribute "noParams") in
274 C.AInductiveDefinition (xid, inductiveTypes, params, nparams)
275 | D.T_element "Variable" ->
276 let name = string_of_attr (n#attribute "name")
277 and xid = string_of_attr (n#attribute "id")
279 let sons = n#sub_nodes in
282 b#node_type = D.T_element "body" &&
283 t#node_type = D.T_element "type" ->
284 let b' = get_content b
285 and t' = get_content t in
286 (Some (b'#extension#to_cic_term), t'#extension#to_cic_term)
287 | [t] when t#node_type = D.T_element "type" ->
288 let t' = get_content t in
289 (None, t'#extension#to_cic_term)
290 | _ -> raise (IllFormedXml 6)
292 C.AVariable (xid,name,body,typ)
296 raise (IllFormedXml 7)