X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_acic%2Fcic2Xml.ml;h=eb3b93408255d76f677a48948b0aa44762e6e53a;hb=d84e4e696de90b967344ed6aa271f5cb5706d2b8;hp=7e97dea6fb0b5fef93d430632c901f8e043688b7;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/cic_acic/cic2Xml.ml b/components/cic_acic/cic2Xml.ml
index 7e97dea6f..eb3b93408 100644
--- a/components/cic_acic/cic2Xml.ml
+++ b/components/cic_acic/cic2Xml.ml
@@ -267,9 +267,10 @@ let print_term ?ids_to_inner_sorts =
    aux
 ;;
 
-let xml_of_attrs attributes =
+let xml_of_attrs generate_attributes attributes =
   let class_of = function
-    | `Coercion -> Xml.xml_empty "class" [None,"value","coercion"]
+    | `Coercion n -> 
+        Xml.xml_empty "class" [None,"value","coercion";None,"arity",string_of_int n]
     | `Elim s ->
         Xml.xml_nempty "class" [None,"value","elim"]
          [< Xml.xml_empty
@@ -279,20 +280,28 @@ let xml_of_attrs attributes =
     | `Record field_names ->
         Xml.xml_nempty "class" [None,"value","record"]
          (List.fold_right
-           (fun (name,coercion) res ->
+           (fun (name,coercion,arity) res ->
              [< Xml.xml_empty "field" 
-                [None,"name",if coercion then name ^ " coercion" else name]; 
+                [None,"name",
+                  if coercion then 
+                    name ^ " coercion " ^ string_of_int arity 
+                  else 
+                    name]; 
               res >]
            ) field_names [<>])
     | `Projection -> Xml.xml_empty "class" [None,"value","projection"]
+    | `InversionPrinciple -> Xml.xml_empty "class" [None,"value","inversion"]
   in
   let flavour_of = function
     | `Definition -> Xml.xml_empty "flavour" [None, "value", "definition"]
+    | `MutualDefinition ->
+        Xml.xml_empty "flavour" [None, "value", "mutual_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"]
+    | `Axiom -> Xml.xml_empty "flavour" [None, "value", "axiom"]
   in
   let xml_attr_of = function
     | `Generated -> Xml.xml_empty "generated" []
@@ -303,9 +312,10 @@ let xml_of_attrs attributes =
    List.fold_right 
     (fun attr res -> [< xml_attr_of attr ; res >]) attributes [<>]
   in
-   Xml.xml_nempty "attributes" [] xml_attrs
+   if generate_attributes then Xml.xml_nempty "attributes" [] xml_attrs else [<>]
 
-let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
+let print_object uri 
+  ?ids_to_inner_sorts ?(generate_attributes=true) ~ask_dtd_to_the_getter obj =
  let module C = Cic in
  let module X = Xml in
  let module U = UriManager in
@@ -313,7 +323,7 @@ let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
    match obj with
        C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params,obj_attrs) ->
         let params' = param_attribute_of_params params in
-        let xml_attrs = xml_of_attrs obj_attrs in
+        let xml_attrs = xml_of_attrs generate_attributes obj_attrs in
         let xml_for_current_proof_body =
 (*CSC: Should the CurrentProof also have the list of variables it depends on? *)
 (*CSC: I think so. Not implemented yet.                                       *)
@@ -373,7 +383,7 @@ let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
          xmlty, Some xmlbo
      | C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) ->
         let params' = param_attribute_of_params params in
-        let xml_attrs = xml_of_attrs obj_attrs in
+        let xml_attrs = xml_of_attrs generate_attributes obj_attrs in
         let xmlbo =
          match bo with
             None -> None
@@ -400,7 +410,7 @@ let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
          xmlty, xmlbo
      | C.AVariable (id,n,bo,ty,params,obj_attrs) ->
         let params' = param_attribute_of_params params in
-        let xml_attrs = xml_of_attrs obj_attrs in
+        let xml_attrs = xml_of_attrs generate_attributes obj_attrs in
         let xmlbo =
          match bo with
             None -> [< >]
@@ -420,7 +430,7 @@ let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
          aobj, None
      | C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) ->
         let params' = param_attribute_of_params params in
-        let xml_attrs = xml_of_attrs obj_attrs in
+        let xml_attrs = xml_of_attrs generate_attributes obj_attrs in
          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
             X.xml_cdata
              ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;