X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fcic2Xml.ml;fp=helm%2FgTopLevel%2Fcic2Xml.ml;h=0000000000000000000000000000000000000000;hb=e108abe5c0b4eb841c4ad332229a6c0e57e70079;hp=ad1d1f8818fb244190075feb9b0223e5db4c77ad;hpb=1456c337a60f6677ee742ff7891d43fc382359a9;p=helm.git

diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml
deleted file mode 100644
index ad1d1f881..000000000
--- a/helm/gTopLevel/cic2Xml.ml
+++ /dev/null
@@ -1,249 +0,0 @@
-
-(* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(*CSC codice cut & paste da cicPp e xmlcommand *)
-
-exception ImpossiblePossible;;
-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 rec aux =
-  let module C = Cic in
-  let module X = Xml in
-  let module U = UriManager in
-    function
-       C.ARel (id,n,b) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_empty "REL"
-          ["value",(string_of_int n) ; "binder",b ; "id",id ; "sort",sort]
-     | C.AVar (id,uri) ->
-        let vdepth = U.depth_of_uri uri
-        and cdepth = U.depth_of_uri curi
-        and sort = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_empty "VAR"
-          ["relUri",(string_of_int (cdepth - vdepth)) ^ "," ^
-            (U.name_of_uri uri) ;
-           "id",id ; "sort",sort]
-     | C.AMeta (id,n,l) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
-         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
-            C.Prop -> "Prop"
-          | C.Set  -> "Set"
-          | C.Type -> "Type"
-        in
-         X.xml_empty "SORT" ["value",(string_of_sort s) ; "id",id]
-     | C.AImplicit _ -> raise NotImplemented
-     | C.AProd (id,C.Anonimous,s,t) ->
-        let ty = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_nempty "PROD" ["id",id ; "type",ty]
-          [< X.xml_nempty "source" [] (aux s) ;
-             X.xml_nempty "target" [] (aux t)
-          >]
-     | C.AProd (xid,C.Name id,s,t) ->
-        let ty = Hashtbl.find ids_to_inner_sorts xid in
-         X.xml_nempty "PROD" ["id",xid ; "type",ty]
-          [< X.xml_nempty "source" [] (aux s) ;
-             X.xml_nempty "target" ["binder",id] (aux t)
-          >]
-     | C.ACast (id,v,t) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_nempty "CAST" ["id",id ; "sort",sort]
-          [< X.xml_nempty "term" [] (aux v) ;
-             X.xml_nempty "type" [] (aux t)
-          >]
-     | C.ALambda (id,C.Anonimous,s,t) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_nempty "LAMBDA" ["id",id ; "sort",sort]
-          [< X.xml_nempty "source" [] (aux s) ;
-             X.xml_nempty "target" [] (aux t)
-          >]
-     | C.ALambda (xid,C.Name id,s,t) ->
-        let sort = Hashtbl.find ids_to_inner_sorts xid in
-         X.xml_nempty "LAMBDA" ["id",xid ; "sort",sort]
-          [< X.xml_nempty "source" [] (aux s) ;
-             X.xml_nempty "target" ["binder",id] (aux t)
-          >]
-     | C.ALetIn (xid,C.Anonimous,s,t) ->
-       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]
-          [< X.xml_nempty "term" [] (aux s) ;
-             X.xml_nempty "letintarget" ["binder",id] (aux t)
-          >]
-     | C.AAppl (id,li) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_nempty "APPLY" ["id",id ; "sort",sort]
-          [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
-          >]
-     | C.AConst (id,uri,_) ->
-        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) ;
-          "noType",(string_of_int i) ;
-          "id",id]
-     | C.AMutConstruct (id,uri,_,i,j) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_empty "MUTCONSTRUCT"
-          ["uri", (U.string_of_uri uri) ;
-           "noType",(string_of_int i) ; "noConstr",(string_of_int j) ;
-           "id",id ; "sort",sort]
-     | C.AMutCase (id,uri,_,typeno,ty,te,patterns) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_nempty "MUTCASE"
-          ["uriType",(U.string_of_uri uri) ;
-           "noType", (string_of_int typeno) ;
-           "id", id ; "sort",sort]
-          [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
-             X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
-             List.fold_right
-              (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
-              patterns [<>]
-          >]
-     | C.AFix (id, no, funs) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_nempty "FIX"
-          ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
-          [< List.fold_right
-              (fun (fi,ai,ti,bi) i ->
-                [< X.xml_nempty "FixFunction"
-                    ["name", fi; "recIndex", (string_of_int ai)]
-                    [< X.xml_nempty "type" [] [< aux ti >] ;
-                       X.xml_nempty "body" [] [< aux bi >]
-                    >] ;
-                   i
-                >]
-              ) funs [<>]
-          >]
-     | C.ACoFix (id,no,funs) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_nempty "COFIX"
-          ["noFun", (string_of_int no) ; "id",id ; "sort",sort]
-          [< List.fold_right
-              (fun (fi,ti,bi) i ->
-                [< X.xml_nempty "CofixFunction" ["name", fi]
-                    [< X.xml_nempty "type" [] [< aux ti >] ;
-                       X.xml_nempty "body" [] [< aux bi >]
-                    >] ;
-                   i
-                >]
-              ) funs [<>]
-          >]
- in
-  aux
-;;
-
-exception NotImplemented;;
-
-(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_object curi ids_to_inner_sorts =
- let rec aux =
-  let module C = Cic in
-  let module X = Xml in
-  let module U = UriManager in
-    function
-       C.ACurrentProof (id,n,conjectures,bo,ty) ->
-        X.xml_nempty "CurrentProof" ["name",n ; "id", id]
-         [< List.fold_left
-             (fun i (cid,n,canonical_context,t) ->
-               [< i ;
-                  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) ;
-            X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty)  >]
-     | C.ADefinition (id,n,bo,ty,C.Actual params) ->
-        let params' =
-         List.fold_right
-          (fun (_,x) i ->
-            List.fold_right
-             (fun x i ->
-               U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i'
-             ) x "" ^ match i with "" -> "" | i' -> " " ^ i'
-          ) params ""
-        in
-         X.xml_nempty "Definition" ["name",n ; "params",params' ; "id", id]
-          [< X.xml_nempty "body" [] (print_term curi ids_to_inner_sorts bo) ;
-             X.xml_nempty "type" [] (print_term curi ids_to_inner_sorts ty)  >]
-     | C.ADefinition _ -> assert false
-     | _ -> raise NotImplemented
- 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 [<>]
-   )
-;;