implemented attributes pretty printing

diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml
index 3be3ba7f115ea5cc7b8cd72e624f6a30c7cdbf07..759f630b4b8abaa0100bac5ff1695ad789ec2e98 100644 (file)
--- a/helm/ocaml/cic_transformations/cic2Xml.ml
+++ b/helm/ocaml/cic_transformations/cic2Xml.ml
@@ -260,8 +260,22 @@ let print_term ~ids_to_inner_sorts =
    aux
 ;;
 
-  (* TODO ZACK implement attributes pretty printing *)
-let xml_of_attrs attributes = [< >]
+let xml_of_attrs attributes =
+  let class_of = function
+    | `Coercion -> "coercion"
+    | `Elim Cic.Prop -> "elimProp"
+    | `Elim Cic.CProp -> "elimCProp"
+    | `Elim Cic.Set -> "elimSet"
+    | `Elim (Cic.Type _) -> "elimType"
+    | `Record -> "record"
+    | `Projection -> "projection"
+  in
+  let xml_attr_of = function
+    | `Generated -> None, "generated", "true"
+    | `Class c -> None, "class", class_of c
+  in
+  let xml_attrs = List.map xml_attr_of attributes in
+  Xml.xml_empty "attributes" xml_attrs
 
 let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
  let find_sort id =