DTD for attributes revised.

[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 8bf8d5f3b389aac676e64d9a38dbc02991b224d6..056240ef13899e24b08a8adf1b9aac306f94eb64 100644 (file)
--- a/helm/ocaml/cic_transformations/cic2Xml.ml
+++ b/helm/ocaml/cic_transformations/cic2Xml.ml
@@ -261,20 +261,30 @@ let print_term ~ids_to_inner_sorts =
 
 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"
+    | `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 -> None, "generated", "true"
-    | `Class c -> None, "class", class_of c
+    | `Generated -> Xml.xml_empty "generated" []
+    | `Class c -> class_of c
   in
-  let xml_attrs = List.map xml_attr_of attributes in
-  Xml.xml_empty "attributes" xml_attrs
+  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 =