- removed MQueryMisc. Ratio: it was used only for transformation uri -> term.

  The same feature is now available directly in CicUtil without the need
  of cic_textual_parser URIs

diff --git a/helm/ocaml/mathql/.depend b/helm/ocaml/mathql/.depend
index 30dbaa280593ce19dbc1e581854ae1cd4332912b..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644 (file)
--- a/helm/ocaml/mathql/.depend
+++ b/helm/ocaml/mathql/.depend
@@ -1,2 +0,0 @@
-mQueryMisc.cmo: mQueryMisc.cmi 
-mQueryMisc.cmx: mQueryMisc.cmi 

diff --git a/helm/ocaml/mathql/Makefile b/helm/ocaml/mathql/Makefile
index 6554bf698417bf2c7867cf6a22c1aec984ca4ba3..203d043713521140a51825b023947157d49b9ec2 100644 (file)
--- a/helm/ocaml/mathql/Makefile
+++ b/helm/ocaml/mathql/Makefile
@@ -1,10 +1,10 @@
 PACKAGE = mathql
-REQUIRES = helm-cic helm-cic_textual_parser
+REQUIRES = helm-cic
 PREDICATES =
 
-INTERFACE_FILES = mQueryMisc.mli 
+INTERFACE_FILES =
 
-IMPLEMENTATION_FILES = mathQL.ml mQueryMisc.ml
+IMPLEMENTATION_FILES = mathQL.ml
 
 EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi
 

diff --git a/helm/ocaml/mathql/mQueryMisc.ml b/helm/ocaml/mathql/mQueryMisc.ml
deleted file mode 100644 (file)
index 08474d3..0000000
--- a/helm/ocaml/mathql/mQueryMisc.ml
+++ /dev/null
@@ -1,108 +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,[])
-;;
-

diff --git a/helm/ocaml/mathql/mQueryMisc.mli b/helm/ocaml/mathql/mQueryMisc.mli
deleted file mode 100644 (file)
index 57c24d1..0000000
--- a/helm/ocaml/mathql/mQueryMisc.mli
+++ /dev/null
@@ -1,43 +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
-
-val string_of_cic_textual_parser_uri : CicTextualParser0.uri -> string
-val cic_textual_parser_uri_of_string : string -> CicTextualParser0.uri
-val term_of_cic_textual_parser_uri: CicTextualParser0.uri -> Cic.term
-val wrong_xpointer_format_from_wrong_xpointer_format' : string -> string
-