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 flavour_of = function
+ | `Definition -> Xml.xml_empty "flavour" [None, "value", "definition"]
+ | `Fact -> Xml.xml_empty "flavour" [None, "value", "fact"]
+ | `Lemma -> Xml.xml_empty "flavour" [None, "value", "lemma"]
+ | `Remark -> Xml.xml_empty "flavour" [None, "value", "remark"]
+ | `Theorem -> Xml.xml_empty "flavour" [None, "value", "theorem"]
+ | `Variant -> Xml.xml_empty "flavour" [None, "value", "variant"]
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
+ | `Flavour f -> flavour_of f
+ in
+ let xml_attrs =
+ List.fold_right
+ (fun attr res -> [< xml_attr_of attr ; res >]) attributes [<>]
in
- let xml_attrs = List.map xml_attr_of attributes in
- Xml.xml_empty "attributes" xml_attrs
+ Xml.xml_nempty "attributes" [] xml_attrs
let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
let find_sort id =