Initial revision

[helm.git] / helm / interface / annotationParser2.ml

diff --git a/helm/interface/annotationParser2.ml b/helm/interface/annotationParser2.ml
new file mode 100644 (file)
index 0000000..5e5042e
--- /dev/null
+++ b/helm/interface/annotationParser2.ml
@@ -0,0 +1,103 @@
+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)
+;;