- D.T_element "Definition" ->
- let id = string_of_attr (n # attribute "name")
- and params =
- option_uri_list_of_attr (n#attribute "params") (n#attribute "paramMode")
- and (value, typ) =
- let sons = n#sub_nodes in
- match sons with
- [v ; t] when
- v#node_type = D.T_element "body" &&
- t#node_type = D.T_element "type" ->
- let v' = get_content v
- and t' = get_content t in
- (v'#extension#to_cic_term, t'#extension#to_cic_term)
- | _ -> raise (IllFormedXml 6)
- and xid = string_of_attr (n#attribute "id") in
- C.ADefinition (xid, id, value, typ, params)
- | D.T_element "Axiom" ->
- let id = string_of_attr (n # attribute "name")
- and params = uri_list_of_attr (n # attribute "params")
- and typ =
- (get_content (get_content n))#extension#to_cic_term
- and xid = string_of_attr (n#attribute "id") in
- C.AAxiom (xid, id, typ, params)
- | D.T_element "CurrentProof" ->
- let name = string_of_attr (n#attribute "name")
- and xid = string_of_attr (n#attribute "id") in
- let sons = n#sub_nodes in
- let (conjs, value, typ) = get_conjs_value_type sons in
- C.ACurrentProof (xid, name, conjs, value, typ)
+ D.T_element "ConstantType" ->
+ let name = string_of_attr (n # attribute "name") in
+ let params = uri_list_of_attr (n#attribute "params") in
+ let xid = string_of_attr (n#attribute "id") in
+ let typ = (get_content n)#extension#to_cic_term [] in
+ (match nbody with
+ None ->
+ (* Axiom *)
+ C.AConstant (xid, None, name, None, typ, params, obj_attrs)
+ | Some nbody' ->
+ let nbodytype = nbody'#node_type in
+ match nbodytype with
+ D.T_element "ConstantBody" ->
+(*CSC: the attribute "for" is ignored and not checked
+ let for_ = string_of_attr (nbody'#attribute "for") in
+*)
+ let paramsbody = uri_list_of_attr (nbody'#attribute "params") in
+ 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,
+ obj_attrs)
+ else
+ raise (IllFormedXml 6)
+ | D.T_element "CurrentProof" ->
+(*CSC: the attribute "of" is ignored and not checked
+ let for_ = string_of_attr (nbody'#attribute "of") in
+*)
+ 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,
+ obj_attrs)
+ | D.T_element _
+ | D.T_data
+ | _ -> raise (IllFormedXml 6)
+ )