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

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index 57d4fc7e4..f498effb6 100644
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -28,7 +28,12 @@
 exception ImpossiblePossible;;
 exception NotImplemented;;
 
-let dtdname = "http://localhost:8081/getdtd?uri=cic.dtd";;
+let dtdname ~ask_dtd_to_the_getter dtd =
+ if ask_dtd_to_the_getter then
+  Configuration.getter_url ^ "getdtd?uri=" ^ dtd
+ else
+  "http://mowgli.cs.unibo.it/dtd/" ^ dtd
+;;
 
 let param_attribute_of_params params =
  String.concat " " (List.map UriManager.string_of_uri params)
@@ -251,14 +256,12 @@ 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
-  let module X = Xml in
-  let module U = UriManager in
-    function
+let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
+ let module C = Cic in
+ let module X = Xml in
+ let module U = UriManager in
+  let dtdname = dtdname ~ask_dtd_to_the_getter "cic.dtd" in
+   match obj with
        C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) ->
         let params' = param_attribute_of_params params in
         let xml_for_current_proof_body =
@@ -304,13 +307,12 @@ let print_object uri ~ids_to_inner_sorts =
         in
         let xmlbo =
          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
-            X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^dtdname ^"\">\n");
+            X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^ dtdname ^ "\">\n");
             xml_for_current_proof_body
          >] in
         let xmlty =
          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
-            X.xml_cdata
-             ("<!DOCTYPE ConstantType SYSTEM \"" ^ dtdname ^ "\">\n");
+            X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
             xml_for_current_proof_type
          >]
         in
@@ -334,32 +336,88 @@ let print_object uri ~ids_to_inner_sorts =
         in
         let xmlty =
          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
-            X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^dtdname ^"\">\n");
+            X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
              X.xml_nempty "ConstantType"
               ["name",n ; "params",params' ; "id", id]
               [< print_term ids_to_inner_sorts ty >]
          >]
         in
          xmlty, xmlbo
-     | _ -> raise NotImplemented
- in
-  aux
+     | 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
 ;;
 
-let print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types =
+let
+ print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types
+  ~ask_dtd_to_the_getter
+=
  let module C2A = Cic2acic in
  let module X = Xml in
-  X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
-   (Hashtbl.fold
-     (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
-       [< x ;
-          X.xml_nempty "TYPE" ["of",id]
-           [< print_term ids_to_inner_sorts synty ;
-              match expty with
-                 None -> [<>]
-               | Some expty' -> print_term ids_to_inner_sorts expty'
+  let dtdname = dtdname ~ask_dtd_to_the_getter "cictypes.dtd" in
+   [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+      X.xml_cdata
+       ("<!DOCTYPE InnerTypes SYSTEM \"" ^ dtdname ^ "\">\n") ;
+      X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
+       (Hashtbl.fold
+         (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
+           [< x ;
+              X.xml_nempty "TYPE" ["of",id]
+               [< print_term ids_to_inner_sorts synty ;
+                  match expty with
+                     None -> [<>]
+                   | Some expty' -> print_term ids_to_inner_sorts expty'
+               >]
            >]
-       >]
-     ) ids_to_inner_types [<>]
-   )
+         ) ids_to_inner_types [<>]
+       )
+   >]
 ;;