DTD for attributes revised.

New syntax:
 <attributes>
  <class type="..">
   ...
  </class>
  <generated />
 </attributes>
where the ... are the arguments of the class and the class and generated
elements are optional. For the "elim" class the only argument is the SORT.
For the "record" class the arguments are a list of <field name=".."/>

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 =