+++ /dev/null
-exception IllFormedXml of int;;
-
-(* Utility functions that transform a Pxp attribute into something useful *)
-
-let string_of_attr a =
- let module T = Pxp_types in
- match a with
- T.Value s -> s
- | _ -> raise (IllFormedXml 0)
-;;
-
-exception DontKnowWhatToDo;;
-
-let rec string_of_annotations n =
- let module D = Pxp_document in
- let module T = Pxp_types in
- match n#node_type with
- D.T_element s ->
- "<" ^ s ^
- List.fold_right
- (fun att i ->
- match n#attribute att with
- T.Value s -> " " ^ att ^ "=\"" ^ s ^ "\"" ^ i
- | T.Implied_value -> i
- | T.Valuelist l -> " " ^ att ^ "=\"" ^ String.concat " " l ^ "\"" ^ i
- ) (n#attribute_names) "" ^
- (match n#sub_nodes with
- [] -> "/>"
- | l ->
- ">" ^
- String.concat "" (List.map string_of_annotations l) ^
- "</" ^ s ^ ">"
- )
- | D.T_data -> n#data
- | _ -> raise DontKnowWhatToDo
-;;
-
-let get_annotation 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
-;;
-
-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.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 annotate ids_to_targets 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)
-;;