From: Stefano Zacchiroli Date: Fri, 22 Oct 2004 12:38:30 +0000 (+0000) Subject: - removed MQueryMisc. Ratio: it was used only for transformation uri -> term. X-Git-Tag: V_0_0_10~34 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fafcc706c1ecd6a3966a9b9de72c0de9f494dabe;p=helm.git - 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 30dbaa280..e69de29bb 100644 --- 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 6554bf698..203d04371 100644 --- 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 index 08474d394..000000000 --- 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 *) -(* Ferruccio Guidi *) -(* 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 index 57c24d189..000000000 --- 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 *) -(* Ferruccio Guidi *) -(* 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 -