X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2Xml.ml;h=d76df870eb48d9f4cf26bd4e89df2bc23daf0c77;hb=ac0495a94c379731f40968b2e08d8f167f72ed64;hp=57d4fc7e4e086386d05919cc9c349e6248b11cac;hpb=87b98314c08ec399096f87a8e06d30234d7cc498;p=helm.git

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index 57d4fc7e4..d76df870e 100644
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -251,8 +251,6 @@ let print_term ~ids_to_inner_sorts =
    aux
 ;;
 
-exception NotImplemented;;
-
 let print_object uri ~ids_to_inner_sorts =
  let rec aux =
   let module C = Cic in
@@ -341,7 +339,57 @@ let print_object uri ~ids_to_inner_sorts =
          >]
         in
          xmlty, xmlbo
-     | _ -> raise NotImplemented
+     | C.AVariable (id,n,bo,ty,params) ->
+        let params' = param_attribute_of_params params in
+        let xmlbo =
+         match bo with
+            None -> [< >]
+          | Some bo ->
+             X.xml_nempty "body" [] [< print_term ids_to_inner_sorts bo >]
+        in
+        let aobj =
+         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+            X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
+             X.xml_nempty "Variable"
+              ["name",n ; "params",params' ; "id", id]
+              [< xmlbo ;
+                 X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty)
+              >]
+         >]
+        in
+         aobj, None
+     | C.AInductiveDefinition (id,tys,params,nparams) ->
+        let params' = param_attribute_of_params params in
+         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+            X.xml_cdata ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^
+             dtdname ^ "\">\n") ;
+            X.xml_nempty "InductiveDefinition"
+             ["noParams",string_of_int nparams ;
+              "id",id ;
+              "params",params']
+             [< (List.fold_left
+                  (fun i (id,typename,finite,arity,cons) ->
+                    [< i ;
+                       X.xml_nempty "InductiveType"
+                        ["id",id ; "name",typename ;
+                         "inductive",(string_of_bool finite)
+                        ]
+                        [< X.xml_nempty "arity" []
+                            (print_term ids_to_inner_sorts arity) ;
+                           (List.fold_left
+                            (fun i (name,lc) ->
+                              [< i ;
+                                 X.xml_nempty "Constructor"
+                                  ["name",name]
+                                  (print_term ids_to_inner_sorts lc)
+                              >]) [<>] cons
+                           )
+                        >]
+                    >]
+                  ) [< >] tys
+                )
+             >]
+         >], None
  in
   aux
 ;;