From 05feb31551afc1eafd1d350c3facc23fdda5bebe Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 15 Jun 2005 16:37:16 +0000 Subject: [PATCH] DTD for attributes revised. New syntax: ... 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 --- helm/ocaml/cic_transformations/cic2Xml.ml | 32 +++++++++++++++-------- 1 file changed, 21 insertions(+), 11 deletions(-) diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml index 8bf8d5f3b..056240ef1 100644 --- 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 = -- 2.39.2