bool_of_string (string_of_attr a)
;;
+let name_of_attr a =
+ let module T = Pxp_types in
+ let module C = Cic in
+ match a with
+ T.Value s -> C.Name s
+ | T.Implied_value -> C.Anonimous
+ | _ -> raise (IllFormedXml 0)
+;;
+
(* Other utility functions *)
let get_content n =
| _ -> raise (IllFormedXml 1)
;;
-let register_id id node =
- if !CicParser3.process_annotations then
- match !CicParser3.ids_to_targets with
- None -> assert false
- | Some ids_to_targets ->
- Hashtbl.add ids_to_targets id (Cic.Object node)
-;;
-
(* Functions that, given the list of sons of a node of the cic dom (objects *)
(* level), retrieve the internal representation associated to the node. *)
(* Everytime a cic term subtree is found, it is translated to the internal *)
match l with
[] -> (c, v, t)
| conj::tl when conj#node_type = D.T_element "Conjecture" ->
- let no = int_of_attr (conj#attribute "no")
- and typ = (get_content conj)#extension#to_cic_term in
- rget ((no, typ)::c, v, t) tl
+ let no = int_of_attr (conj#attribute "no") in
+ let xid = string_of_attr (conj#attribute "id") in
+ let typ,canonical_context =
+ match List.rev (conj#sub_nodes) with
+ [] -> raise (IllFormedXml 13)
+ | typ::canonical_context ->
+ (get_content typ)#extension#to_cic_term,
+ List.map
+ (function n ->
+ match n#node_type with
+ D.T_element "Decl" ->
+ let name = name_of_attr (n#attribute "name") in
+ let hid = string_of_attr (n#attribute "id") in
+ let term = (get_content n)#extension#to_cic_term in
+ hid,Some (name,Cic.ADecl term)
+ | D.T_element "Def" ->
+ let name = name_of_attr (n#attribute "name") in
+ let hid = string_of_attr (n#attribute "id") in
+ let term = (get_content n)#extension#to_cic_term in
+ hid,Some (name,Cic.ADef term)
+ | D.T_element "Hidden" ->
+ let hid = string_of_attr (n#attribute "id") in
+ hid,None
+ | _ -> raise (IllFormedXml 14)
+ ) canonical_context
+ in
+ rget ((xid, no, canonical_context, typ)::c, v, t) tl
| value::tl when value#node_type = D.T_element "body" ->
let v' = (get_content value)#extension#to_cic_term in
(match v with
| _ -> raise (IllFormedXml 4)
in
match rget ([], None, None) l with
- (c, Some v, Some t) -> (c, v, t)
+ (revc, Some v, Some t) -> (List.rev revc, v, t)
| _ -> raise (IllFormedXml 5)
;;
(v'#extension#to_cic_term, t'#extension#to_cic_term)
| _ -> raise (IllFormedXml 6)
and xid = string_of_attr (n#attribute "id") in
- let res = C.ADefinition (xid, ref None, id, value, typ, params) in
- register_id xid res ;
- res
+ 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
- let res = C.AAxiom (xid, ref None, id, typ, params) in
- register_id xid res ;
- res
+ 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
- let res = C.ACurrentProof (xid, ref None, name, conjs, value, typ) in
- register_id xid res ;
- res
+ C.ACurrentProof (xid, name, conjs, value, typ)
| D.T_element "InductiveDefinition" ->
let sons = n#sub_nodes
and xid = string_of_attr (n#attribute "id") in
let inductiveTypes = get_inductive_types sons
and params = uri_list_of_attr (n#attribute "params")
and nparams = int_of_attr (n#attribute "noParams") in
- let res =
- C.AInductiveDefinition (xid, ref None, inductiveTypes, params, nparams)
- in
- register_id xid res ;
- res
+ C.AInductiveDefinition (xid, inductiveTypes, params, nparams)
| D.T_element "Variable" ->
let name = string_of_attr (n#attribute "name")
and xid = string_of_attr (n#attribute "id")
(None, t'#extension#to_cic_term)
| _ -> raise (IllFormedXml 6)
in
- let res = C.AVariable (xid,ref None,name,body,typ) in
- register_id xid res ;
- res
+ C.AVariable (xid,name,body,typ)
| D.T_element _
| D.T_data
| _ ->