exception IllFormedXml of int;;
-(* The hashtable from the current identifiers to the object or the terms *)
-let ids_to_targets = ref None;;
-
(* The list of tokens of the current section path. *)
(* Used to resolve relative URIs *)
let current_sp = ref [];;
(* The uri of the object been parsed *)
let current_uri = ref (UriManager.uri_of_string "cic:/.xml");;
-(* True if annotation really matter *)
-let process_annotations = ref false;;
-
(* Utility functions to map a markup attribute to something useful *)
let cic_attr_of_xml_attr =
let binder_of_xml_attr =
function
- Pxp_types.Value s -> if !process_annotations then Some s else None
+ Pxp_types.Value s -> s
| _ -> raise (IllFormedXml 17)
;;
-let register_id id node =
- if !process_annotations then
- match !ids_to_targets with
- None -> assert false
- | Some ids_to_targets ->
- Hashtbl.add ids_to_targets id (Cic.Term node)
-;;
-
(* the "interface" of the class linked to each node of the dom tree *)
class virtual cic_term =
| _ -> raise (IllFormedXml 13)
) sons
in
- let res = Cic.AFix (id, ref None, nofun, functions) in
- register_id id res ;
- res
+ Cic.AFix (id, nofun, functions)
end
;;
| _ -> raise (IllFormedXml 15)
) sons
in
- let res = Cic.ACoFix (id, ref None, nofun, functions) in
- register_id id res ;
- res
+ Cic.ACoFix (id, nofun, functions)
end
;;
method to_cic_term =
let n = self#node in
let id = string_of_xml_attr (n#attribute "id") in
- let res = Cic.AImplicit (id, ref None) in
- register_id id res ;
- res
+ Cic.AImplicit id
end
;;
let value = int_of_xml_attr (n#attribute "value")
and binder = binder_of_xml_attr (n#attribute "binder")
and id = string_of_xml_attr (n#attribute "id") in
- let res = Cic.ARel (id,ref None,value,binder) in
- register_id id res ;
- res
+ Cic.ARel (id,value,binder)
end
;;
let n = self#node in
let value = int_of_xml_attr (n#attribute "no")
and id = string_of_xml_attr (n#attribute "id") in
- let res = Cic.AMeta (id,ref None,value) in
- register_id id res ;
- res
+ Cic.AMeta (id,value)
end
;;
in
aux (List.length !current_sp - n,!current_sp)
in
- let res =
- Cic.AVar
- (xid,ref None,
- (UriManager.uri_of_string
- ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var"))
- )
- in
- register_id id res ;
- res
+ Cic.AVar
+ (xid,
+ (UriManager.uri_of_string
+ ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var"))
+ )
| _ -> raise (IllFormedXml 18)
end
;;
and id = string_of_xml_attr (n#attribute "id") in
if List.length children < 2 then raise (IllFormedXml 8)
else
- let res =
- Cic.AAppl
- (id,ref None,List.map (fun x -> x#extension#to_cic_term) children)
- in
- register_id id res ;
- res
+ Cic.AAppl
+ (id,List.map (fun x -> x#extension#to_cic_term) children)
end
;;
ty#node_type = Pxp_document.T_element "type" ->
let term = te#extension#to_cic_term
and typ = ty#extension#to_cic_term in
- let res = Cic.ACast (id,ref None,term,typ) in
- register_id id res ;
- res
+ Cic.ACast (id,term,typ)
| _ -> raise (IllFormedXml 9)
end
;;
let n = self#node in
let sort = cic_sort_of_xml_attr (n#attribute "value")
and id = string_of_xml_attr (n#attribute "id") in
- let res = Cic.ASort (id,ref None,sort) in
- register_id id res ;
- res
+ Cic.ASort (id,sort)
end
;;
let n = self#node in
let value = uri_of_xml_attr (n#attribute "uri")
and id = string_of_xml_attr (n#attribute "id") in
- let res = Cic.AAbst (id,ref None,value) in
- register_id id res ;
- res
+ Cic.AAbst (id,value)
end
;;
let n = self#node in
let value = uri_of_xml_attr (n#attribute "uri")
and id = string_of_xml_attr (n#attribute "id") in
- let res =
- Cic.AConst (id,ref None,value, U.relative_depth !current_uri value 0)
- in
- register_id id res ;
- res
+ Cic.AConst (id,value, U.relative_depth !current_uri value 0)
end
;;
let name = uri_of_xml_attr (n#attribute "uri")
and noType = int_of_xml_attr (n#attribute "noType")
and id = string_of_xml_attr (n#attribute "id") in
- let res =
- Cic.AMutInd
- (id,ref None,name, U.relative_depth !current_uri name 0, noType)
- in
- register_id id res ;
- res
+ Cic.AMutInd
+ (id,name, U.relative_depth !current_uri name 0, noType)
end
;;
and noType = int_of_xml_attr (n#attribute "noType")
and noConstr = int_of_xml_attr (n#attribute "noConstr")
and id = string_of_xml_attr (n#attribute "id") in
- let res =
- Cic.AMutConstruct
- (id, ref None, name, U.relative_depth !current_uri name 0,
- noType, noConstr)
- in
- register_id id res ;
- res
+ Cic.AMutConstruct
+ (id, name, U.relative_depth !current_uri name 0,
+ noType, noConstr)
end
;;
let name = cic_attr_of_xml_attr (t#attribute "binder")
and source = s#extension#to_cic_term
and target = t#extension#to_cic_term in
- let res = Cic.AProd (id,ref None,name,source,target) in
- register_id id res ;
- res
+ Cic.AProd (id,name,source,target)
| _ -> raise (IllFormedXml 10)
end
;;
and inductiveTerm = te#extension#to_cic_term
and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns
in
- let res =
- Cic.AMutCase (id,ref None,ci,U.relative_depth !current_uri ci 0,
- typeno,inductiveType,inductiveTerm,lpattern)
- in
- register_id id res ;
- res
+ Cic.AMutCase (id,ci,U.relative_depth !current_uri ci 0,
+ typeno,inductiveType,inductiveTerm,lpattern)
| _ -> raise (IllFormedXml 11)
end
;;
let name = cic_attr_of_xml_attr (t#attribute "binder")
and source = s#extension#to_cic_term
and target = t#extension#to_cic_term in
- let res = Cic.ALambda (id,ref None,name,source,target) in
- register_id id res ;
- res
+ Cic.ALambda (id,name,source,target)
| _ -> raise (IllFormedXml 12)
end
;;
let name = cic_attr_of_xml_attr (t#attribute "binder")
and source = s#extension#to_cic_term
and target = t#extension#to_cic_term in
- let res = Cic.ALetIn (id,ref None,name,source,target) in
- register_id id res ;
- res
+ Cic.ALetIn (id,name,source,target)
| _ -> raise (IllFormedXml 12)
end
;;