| _ -> raise DontKnowWhatToDo
;;
-let get_annotation n =
+let get_annotation_from_node n =
String.concat "" (List.map string_of_annotations (n#sub_nodes))
;;
-let annotate_object ann obj =
- let module C = Cic in
- let rann =
- match obj with
- C.ADefinition (_, rann, _, _, _, _) -> rann
- | C.AAxiom (_, rann, _, _, _) -> rann
- | C.AVariable (_, rann, _, _, _) -> rann
- | C.ACurrentProof (_, rann, _, _, _, _) -> rann
- | C.AInductiveDefinition (_, rann, _, _, _) -> rann
- in
- rann := Some ann
-;;
+exception MoreThanOneAnnotationFor of Cic.id;;
-let annotate_term ann term =
- let module C = Cic in
- let rann =
- match term with
- C.ARel (_, rann, _, _) -> rann
- | C.AVar (_, rann, _) -> rann
- | C.AMeta (_, rann, _) -> rann
- | C.ASort (_, rann, _) -> rann
- | C.AImplicit (_, rann) -> rann
- | C.ACast (_, rann, _, _) -> rann
- | C.AProd (_, rann, _, _, _) -> rann
- | C.ALambda (_, rann, _, _, _) -> rann
- | C.ALetIn (_, rann, _, _, _) -> rann
- | C.AAppl (_, rann, _) -> rann
- | C.AConst (_, rann, _, _) -> rann
- | C.AAbst (_, rann, _) -> rann
- | C.AMutInd (_, rann, _, _, _) -> rann
- | C.AMutConstruct (_, rann, _, _, _, _) -> rann
- | C.AMutCase (_, rann, _, _, _, _, _, _) -> rann
- | C.AFix (_, rann, _, _) -> rann
- | C.ACoFix (_, rann, _, _) -> rann
- in
- rann := Some ann
+let set_annotation ids_to_annotations id ann =
+ try
+ ignore (Hashtbl.find ids_to_annotations id) ;
+ raise (MoreThanOneAnnotationFor id)
+ with
+ Not_found -> Hashtbl.add ids_to_annotations id ann
;;
-let annotate ids_to_targets n =
+let get_annotations n =
let module D = Pxp_document in
let module C = Cic in
- let annotate_elem n =
- let ntype = n # node_type in
- match ntype with
- D.T_element "Annotation" ->
- let of_uri = string_of_attr (n # attribute "of") in
- begin
- try
- match Hashtbl.find ids_to_targets of_uri with
- C.Object o -> annotate_object (get_annotation n) o
- | C.Term t -> annotate_term (get_annotation n) t
- with
- Not_found -> assert false
- end
- | D.T_element _ | D.T_data ->
- raise (IllFormedXml 1)
- | _ -> raise DontKnowWhatToDo
- in
- match n # node_type with
- D.T_element "Annotations" ->
- List.iter annotate_elem (n # sub_nodes)
- | _ -> raise (IllFormedXml 2)
+ let ids_to_annotations = Hashtbl.create 503 in
+ let annotate_elem n =
+ let ntype = n # node_type in
+ match ntype with
+ D.T_element "Annotation" ->
+ let of_uri = string_of_attr (n # attribute "of") in
+ set_annotation ids_to_annotations of_uri (get_annotation_from_node n)
+ | D.T_element _ | D.T_data ->
+ raise (IllFormedXml 1)
+ | _ -> raise DontKnowWhatToDo
+ in
+ match n # node_type with
+ D.T_element "Annotations" ->
+ List.iter annotate_elem (n # sub_nodes) ;
+ ids_to_annotations
+ | _ -> raise (IllFormedXml 2)
;;