exception IllFormedXml of int;;
exception NotImplemented;;
+ (* TODO ZACK implement attributes parsing from XML. ATM, parsing always
+ * returns the empty list of attributes reported here *)
+let obj_attributes = []
+let get_obj_attributes (n: 'a Pxp_document.node) =
+ obj_attributes
+
(* Utility functions that transform a Pxp attribute into something useful *)
let uri_list_of_attr a =
let module U = UriManager in
let module D = Pxp_document in
let module C = Cic in
+ let obj_attrs = get_obj_attributes n in
let ntype = n#node_type in
match ntype with
D.T_element "ConstantType" ->
(match nbody with
None ->
(* Axiom *)
- C.AConstant (xid, None, name, None, typ, params)
+ C.AConstant (xid, None, name, None, typ, params, obj_attrs)
| Some nbody' ->
let nbodytype = nbody'#node_type in
match nbodytype with
let xidbody = string_of_attr (nbody'#attribute "id") in
let value = (get_content nbody')#extension#to_cic_term [] in
if paramsbody = params then
- C.AConstant (xid, Some xidbody, name, Some value, typ, params)
+ C.AConstant (xid, Some xidbody, name, Some value, typ, params,
+ obj_attrs)
else
raise (IllFormedXml 6)
| D.T_element "CurrentProof" ->
let xidbody = string_of_attr (nbody'#attribute "id") in
let sons = nbody'#sub_nodes in
let (conjs, value) = get_conjs_value sons in
- C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params)
+ C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params,
+ obj_attrs)
| D.T_element _
| D.T_data
| _ -> raise (IllFormedXml 6)
let inductiveTypes = get_inductive_types sons
and params = uri_list_of_attr (n#attribute "params")
and nparams = int_of_attr (n#attribute "noParams") in
- C.AInductiveDefinition (xid, inductiveTypes, params, nparams)
+ C.AInductiveDefinition (xid, inductiveTypes, params, nparams, obj_attrs)
| D.T_element "Variable" ->
let name = string_of_attr (n#attribute "name")
and params = uri_list_of_attr (n#attribute "params")
(None, t'#extension#to_cic_term [])
| _ -> raise (IllFormedXml 6)
in
- C.AVariable (xid,name,body,typ,params)
+ C.AVariable (xid,name,body,typ,params,obj_attrs)
| D.T_element _
| D.T_data
| _ -> raise (IllFormedXml 7)