X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2Xml.ml;h=7c674d0ad7eaab5def678e111e89a441e5372933;hb=c5c48f3d3515f1dd95657245922ec1f340e17f70;hp=115d1ee666bc064ac91c16bcfc509dbbe8d6ecff;hpb=cba2bdcb2944a5d2a4f2e1560262430fd45e61e6;p=helm.git

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index 115d1ee66..7c674d0ad 100644
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -1,4 +1,3 @@
-
 (* Copyright (C) 2000, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
@@ -31,7 +30,7 @@ exception NotImplemented;;
 let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
 
 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_term curi ids_to_inner_sorts =
+let print_term curi ~ids_to_inner_sorts =
  let rec aux =
   let module C = Cic in
   let module X = Xml in
@@ -49,9 +48,17 @@ let print_term curi ids_to_inner_sorts =
           ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
             (U.name_of_uri uri) ;
            "id",id ; "sort",sort]
-     | C.AMeta (id,n) ->
+     | C.AMeta (id,n,l) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_empty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort]
+         X.xml_nempty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort]
+          (List.fold_left
+            (fun i t ->
+              match t with
+                 Some t' ->
+                  [< i ; X.xml_nempty "substitution" [] (aux t') >]
+               | None ->
+                  [< i ; X.xml_empty "substitution" [] >]
+            ) [< >] l)
      | C.ASort (id,s) ->
         let string_of_sort =
          function
@@ -92,7 +99,7 @@ let print_term curi ids_to_inner_sorts =
              X.xml_nempty "target" ["binder",id] (aux t)
           >]
      | C.ALetIn (xid,C.Anonimous,s,t) ->
-       assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
+       assert false
      | C.ALetIn (xid,C.Name id,s,t) ->
         let sort = Hashtbl.find ids_to_inner_sorts xid in
          X.xml_nempty "LETIN" ["id",xid ; "sort",sort]
@@ -108,7 +115,6 @@ let print_term curi ids_to_inner_sorts =
         let sort = Hashtbl.find ids_to_inner_sorts id in
          X.xml_empty "CONST"
           ["uri", (U.string_of_uri uri) ; "id",id ; "sort",sort]
-     | C.AAbst (id,uri) -> raise NotImplemented
      | C.AMutInd (id,uri,_,i) ->
         X.xml_empty "MUTIND"
          ["uri", (U.string_of_uri uri) ;
@@ -168,7 +174,7 @@ let print_term curi ids_to_inner_sorts =
 exception NotImplemented;;
 
 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_object curi ids_to_inner_sorts =
+let print_object curi ~ids_to_inner_sorts =
  let rec aux =
   let module C = Cic in
   let module X = Xml in
@@ -177,10 +183,33 @@ let print_object curi ids_to_inner_sorts =
        C.ACurrentProof (id,n,conjectures,bo,ty) ->
         X.xml_nempty "CurrentProof" ["name",n ; "id", id]
          [< List.fold_left
-             (fun i (n,t) ->
+             (fun i (cid,n,canonical_context,t) ->
                [< i ;
-                  X.xml_nempty "Conjecture" ["no",(string_of_int n)]
-                   (print_term curi ids_to_inner_sorts t)
+                  X.xml_nempty "Conjecture"
+                   ["id", cid ; "no",(string_of_int n)]
+                   [< List.fold_left
+                       (fun i (hid,t) ->
+                         [< (match t with
+                               Some (n,C.ADecl t) ->
+                                X.xml_nempty "Decl"
+                                 (match n with
+                                     C.Name n' -> ["id",hid;"name",n']
+                                   | C.Anonimous -> ["id",hid])
+                                 (print_term curi ids_to_inner_sorts t)
+                             | Some (n,C.ADef t) ->
+                                X.xml_nempty "Def"
+                                 (match n with
+                                     C.Name n' -> ["id",hid;"name",n']
+                                   | C.Anonimous -> ["id",hid])
+                                 (print_term curi ids_to_inner_sorts t)
+                             | None -> X.xml_empty "Hidden" ["id",hid]
+                            ) ;
+                            i
+                         >]
+                       ) [< >] canonical_context ;
+                      X.xml_nempty "Goal" []
+                       (print_term curi ids_to_inner_sorts t)
+                   >]
                >])
              [<>] conjectures ;
             X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
@@ -204,14 +233,19 @@ let print_object curi ids_to_inner_sorts =
   aux
 ;;
 
-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 =
+ let module C2A = Cic2acic in
  let module X = Xml in
   X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
    (Hashtbl.fold
-     (fun id ty x ->
+     (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
        [< x ;
           X.xml_nempty "TYPE" ["of",id]
-           (print_term curi ids_to_inner_sorts ty)
+           [< print_term curi ids_to_inner_sorts synty ;
+              match expty with
+                 None -> [<>]
+               | Some expty' -> print_term curi ids_to_inner_sorts expty'
+           >]
        >]
      ) ids_to_inner_types [<>]
    )