X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fmathql%2FmQueryMisc.ml;fp=helm%2Focaml%2Fmathql%2FmQueryMisc.ml;h=0000000000000000000000000000000000000000;hp=fb32d8c2425fb49fbd59f254e855a7c790d2ccf7;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1

diff --git a/helm/ocaml/mathql/mQueryMisc.ml b/helm/ocaml/mathql/mQueryMisc.ml
deleted file mode 100644
index fb32d8c24..000000000
--- a/helm/ocaml/mathql/mQueryMisc.ml
+++ /dev/null
@@ -1,120 +0,0 @@
-(* Copyright (C) 2000-2002, 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/.
- *)
-
-(****************************************************************************)
-(*                                                                          *)
-(*                               PROJECT HELM                               *)
-(*                                                                          *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>             *)
-(*                Ferruccio Guidi        <fguidi@cs.unibo.it>               *)
-(*                                 15/01/2003                               *)
-(*                                                                          *)
-(*                                                                          *)
-(****************************************************************************)
-
-exception IllFormedUri of string;;
-
-let string_of_cic_textual_parser_uri uri =
- let module C = Cic in
- let module CTP = CicTextualParser0 in
-  let uri' =
-   match uri with
-      CTP.ConUri uri -> UriManager.string_of_uri uri
-    | CTP.VarUri uri -> UriManager.string_of_uri uri
-    | CTP.IndTyUri (uri,tyno) ->
-       UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
-    | CTP.IndConUri (uri,tyno,consno) ->
-       UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
-        string_of_int consno
-  in
-   (* 4 = String.length "cic:" *)
-   String.sub uri' 4 (String.length uri' - 4)
-;;
-
-let cic_textual_parser_uri_of_string uri' =
- try
-  (* Constant *)
-  if String.sub uri' (String.length uri' - 4) 4 = ".con" then
-   CicTextualParser0.ConUri (UriManager.uri_of_string uri')
-  else
-   if String.sub uri' (String.length uri' - 4) 4 = ".var" then
-    CicTextualParser0.VarUri (UriManager.uri_of_string uri')
-   else
-    (try
-      (* Inductive Type *)
-      let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
-       CicTextualParser0.IndTyUri (uri'',typeno)
-     with
-        UriManager.IllFormedUri _
-      | CicTextualParser0.LexerFailure _
-      | Invalid_argument _ ->
-         (* Constructor of an Inductive Type *)
-         let uri'',typeno,consno =
-          CicTextualLexer.indconuri_of_uri uri'
-         in
-          CicTextualParser0.IndConUri (uri'',typeno,consno)
-    )
- with
-    UriManager.IllFormedUri _
-  | CicTextualParser0.LexerFailure _
-  | Invalid_argument _ ->
-     raise (IllFormedUri uri')
-;;
-
-(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
-let wrong_xpointer_format_from_wrong_xpointer_format' uri =
- try
-  let index_sharp =  String.index uri '#' in
-  let index_rest = index_sharp + 10 in
-   let baseuri = String.sub uri 0 index_sharp in
-   let rest =
-    String.sub uri index_rest (String.length uri - index_rest - 1)
-   in
-    baseuri ^ "#" ^ rest
- with Not_found -> uri
-;;
-
-let term_of_cic_textual_parser_uri uri =
- let module C = Cic in
- let module CTP = CicTextualParser0 in
-  match uri with
-     CTP.ConUri uri -> C.Const (uri,[])
-   | CTP.VarUri uri -> C.Var (uri,[])
-   | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
-   | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
-;;
-
-(* conversion functions *****************************************************)
-
-type uriref = UriManager.uri * (int list)
-
-let string_of_uriref (uri, fi) =
-   let module UM = UriManager in
-   let str = UM.string_of_uri uri in
-   let xp t = "#xpointer(1/" ^ string_of_int (t + 1) in
-   match fi with
-      | []          -> str 
-      | [t]         -> str ^ xp t ^ ")" 
-      | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")"