version 0.7.1

[helm.git] / helm / ocaml / cic_transformations / cic2Xml.ml

diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml
index 3be3ba7f115ea5cc7b8cd72e624f6a30c7cdbf07..056240ef13899e24b08a8adf1b9aac306f94eb64 100644 (file)
--- a/helm/ocaml/cic_transformations/cic2Xml.ml
+++ b/helm/ocaml/cic_transformations/cic2Xml.ml
@@ -25,7 +25,6 @@
 
 (*CSC codice cut & paste da cicPp e xmlcommand *)
 
-exception ImpossiblePossible;;
 exception NotImplemented;;
 
 let dtdname ~ask_dtd_to_the_getter dtd =
@@ -260,8 +259,32 @@ 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 -> Xml.xml_empty "class" [None,"value","coercion"]
+    | `Elim s ->
+        Xml.xml_nempty "class" [None,"value","elim"]
+         [< Xml.xml_empty
+             "SORT" [None,"value",
+                      (Cic2acic.string_of_sort (Cic2acic.sort_of_sort s)) ;
+                     None,"id","elimination_sort"] >]
+    | `Record field_names ->
+        Xml.xml_nempty "class" [None,"value","record"]
+         (List.fold_right
+           (fun name res ->
+             [< Xml.xml_empty "field" [None,"name",name]; res >]
+           ) field_names [<>])
+    | `Projection -> Xml.xml_empty "class" [None,"value","projection"]
+  in
+  let xml_attr_of = function
+    | `Generated -> Xml.xml_empty "generated" []
+    | `Class c -> class_of c
+  in
+  let xml_attrs =
+   List.fold_right 
+    (fun attr res -> [< xml_attr_of attr ; res >]) attributes [<>]
+  in
+   Xml.xml_nempty "attributes" [] xml_attrs
 
 let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
  let find_sort id =