debian: rebuilt against ocaml 3.08.2

[helm.git] / helm / ocaml / cic_transformations / cic2Xml.ml

diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml
index d945cc82f63d54b2e931424c625dacd9707ba383..5d614db055d92d8cd570f7f93c1b79bb6766296d 100644 (file)
--- a/helm/ocaml/cic_transformations/cic2Xml.ml
+++ b/helm/ocaml/cic_transformations/cic2Xml.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000, HELM Team.
+(* Copyright (C) 2000-2004, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -20,7 +20,7 @@
  * MA  02111-1307, USA.
  * 
  * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
+ * http://helm.cs.unibo.it/
  *)
 
 (*CSC codice cut & paste da cicPp e xmlcommand *)
@@ -30,7 +30,7 @@ exception NotImplemented;;
 
 let dtdname ~ask_dtd_to_the_getter dtd =
  if ask_dtd_to_the_getter then
-  Configuration.getter_url ^ "getdtd?uri=" ^ dtd
+  Helm_registry.get "getter.url" ^ "getdtd?uri=" ^ dtd
  else
   "http://mowgli.cs.unibo.it/dtd/" ^ dtd
 ;;
@@ -72,9 +72,10 @@ let print_term ~ids_to_inner_sorts =
      | C.ASort (id,s) ->
         let string_of_sort =
          function
-            C.Prop -> "Prop"
-          | C.Set  -> "Set"
-          | C.Type -> "Type"
+            C.Prop  -> "Prop"
+          | C.Set   -> "Set"
+          | C.Type _ -> "Type" (* TASSI *)
+         | C.CProp -> "CProp"
         in
          X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id]
      | C.AImplicit _ -> raise NotImplemented
@@ -264,20 +265,25 @@ let print_term ~ids_to_inner_sorts =
    aux
 ;;
 
+  (* TODO ZACK implement attributes pretty printing *)
+let xml_of_attrs attributes = [< >]
+
 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) ->
+       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_for_current_proof_body =
 (*CSC: Should the CurrentProof also have the list of variables it depends on? *)
 (*CSC: I think so. Not implemented yet.                                       *)
          X.xml_nempty "CurrentProof"
           [None,"of",UriManager.string_of_uri uri ; None,"id", id]
-          [< List.fold_left
+          [< xml_attrs;
+            List.fold_left
               (fun i (cid,n,canonical_context,t) ->
                 [< i ;
                    X.xml_nempty "Conjecture"
@@ -308,7 +314,7 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
                         (print_term ids_to_inner_sorts t)
                     >]
                 >])
-              [<>] conjectures ;
+              [< >] conjectures ;
              X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >]
         in
         let xml_for_current_proof_type =
@@ -328,8 +334,9 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
          >]
         in
          xmlty, Some xmlbo
-     | C.AConstant (id,idbody,n,bo,ty,params) ->
+     | 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 xmlbo =
          match bo with
             None -> None
@@ -350,12 +357,13 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
             X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
              X.xml_nempty "ConstantType"
               [None,"name",n ; None,"params",params' ; None,"id", id]
-              [< print_term ids_to_inner_sorts ty >]
+              [< xml_attrs; print_term ids_to_inner_sorts ty >]
          >]
         in
          xmlty, xmlbo
-     | C.AVariable (id,n,bo,ty,params) ->
+     | 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 xmlbo =
          match bo with
             None -> [< >]
@@ -367,14 +375,15 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
             X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
              X.xml_nempty "Variable"
               [None,"name",n ; None,"params",params' ; None,"id", id]
-              [< xmlbo ;
+              [< xml_attrs; xmlbo;
                  X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty)
               >]
          >]
         in
          aobj, None
-     | C.AInductiveDefinition (id,tys,params,nparams) ->
+     | 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
          [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
             X.xml_cdata
              ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
@@ -382,7 +391,8 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
              [None,"noParams",string_of_int nparams ;
               None,"id",id ;
               None,"params",params']
-             [< (List.fold_left
+             [< xml_attrs;
+                (List.fold_left
                   (fun i (id,typename,finite,arity,cons) ->
                     [< i ;
                        X.xml_nempty "InductiveType"