Conjectures and Hypotheses inside every conjecture and in the sequents now

[helm.git] / helm / gTopLevel / cic2Xml.ml

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
index db5fd23c57f942e4ec79aaa7f27fb48bd55b6dd0..ad1d1f8818fb244190075feb9b0223e5db4c77ad 100644 (file)
--- a/helm/gTopLevel/cic2Xml.ml
+++ b/helm/gTopLevel/cic2Xml.ml
@@ -49,9 +49,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 +100,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]
@@ -177,10 +185,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) ;
@@ -203,3 +234,16 @@ let print_object curi ids_to_inner_sorts =
  in
   aux
 ;;
+
+let print_inner_types curi ids_to_inner_sorts ids_to_inner_types =
+ let module X = Xml in
+  X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
+   (Hashtbl.fold
+     (fun id ty x ->
+       [< x ;
+          X.xml_nempty "TYPE" ["of",id]
+           (print_term curi ids_to_inner_sorts ty)
+       >]
+     ) ids_to_inner_types [<>]
+   )
+;;