X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2Fmathql.ml;fp=helm%2Focaml%2Fmathql_interpreter%2Fmathql.ml;h=0000000000000000000000000000000000000000;hb=1cfcea66d7394a785ec439cd6b03497b276918c4;hp=e78029036f28f5dcb963d5d01564941fe399c2ff;hpb=a86e50c2f080bd288d1a37b27fd4d0ea3044c5df;p=helm.git

diff --git a/helm/ocaml/mathql_interpreter/mathql.ml b/helm/ocaml/mathql_interpreter/mathql.ml
deleted file mode 100644
index e78029036..000000000
--- a/helm/ocaml/mathql_interpreter/mathql.ml
+++ /dev/null
@@ -1,135 +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/.
- *)
-
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   *)
-(*                     Domenico Lordi  <lordi@cs.unibo.it>                    *)
-(*                                 30/04/2002                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
-exception MQInvalidURI of string
-exception MQConnectionFailed of string
-exception MQInvalidConnection of string
-
-(* Input types **************************************************************)
-(* main type is mquery                                                      *)
-
-type mqrvar = string                         (* name *)
-
-type mqsvar = string                         (* name *)
-
-type mquptoken =
-   | MQString of string                      (* a constant string *)
-   | MQSlash                                 (* a slash: '/' *)
-   | MQAnyChr                                (* Any single character: '?' *)
-   | MQAst                                   (* single asterisk: '*' *)
-   | MQAstAst                                (* double asterisk: '**' *)
-
-type mqup = mquptoken list                   (* uri pattern (helper) *)
-
-type mqfi = int option * int option
-
-type mqtref = string * mqup * mqfi           (* HELM preamble,
-                                                uri pattern, 
-					        fragment identifier *)
-
-type mqpattern = mqtref                      (* constant pattern *)
-
-type mqfunc =
-   | MQName                                  (* NAME *)
-   | MQTheory
-   | MQTitle
-   | MQContributor
-   | MQCreator
-   | MQPublisher
-   | MQSubject
-   | MQDescription
-   | MQDate
-   | MQType
-   | MQFormat
-   | MQIdentifier
-   | MQLanguage
-   | MQRelation
-   | MQSource
-   | MQCoverage
-   | MQRights
-   | MQInstitution
-   | MQContact
-   | MQFirstVersion
-   | MQModified
-
-type mqstring =
-   | MQCons of string                        (* constant *)
-   | MQFunc of mqfunc * mqrvar               (* function, rvar *)
-   | MQRVar of mqrvar                        (* rvar *)
-   | MQSVar of mqsvar                        (* svar *)
-   | MQMConclusion                           (* main conclusion *)
-   | MQConclusion                            (* inner conclusion *)
-
-type mqorder =
-   | MQAsc
-   | MQDesc
-
-type mqbool =
-   | MQTrue
-   | MQFalse
-   | MQAnd of mqbool * mqbool
-   | MQOr of mqbool * mqbool
-   | MQNot of mqbool
-   | MQIs of mqstring * mqstring             (* operands *)
-   | MQSetEqual of mqlist * mqlist           (* the two lists denote the *)
-                                             (* same set                 *)
-   | MQSubset of mqlist * mqlist             (* the two lists denote two   *)
-                                             (* sets, the first one        *)
-                                             (* subsect of the second one. *)
-
-and mqlist =
-   | MQSelect of mqrvar * mqlist * mqbool    (* rvar, list, boolean *) 
-   | MQUse of mqlist * mqsvar                (* list, Position attribute *)
-   | MQUsedBy of mqlist * mqsvar             (* list, Position attribute *)
-   | MQPattern of mqpattern                  (* pattern *)
-   | MQUnion of mqlist * mqlist              (*  *)
-   | MQDiff of mqlist * mqlist               (*  *)
-   | MQIntersect of mqlist * mqlist          (*  *)
-   | MQSortedBy of mqlist * mqorder * mqfunc (*  *)
-   | MQRVarOccur of mqrvar
-
-type mquery =
-   | MQList of mqlist
-   
-(* Output types *************************************************************)
-(* main type is mqresult                                                    *)
-
-type mquref = UriManager.uri * mqfi          (* uri, fragment identifier *)
-
-type mqrefs = mqtref list                    (* list of references (helper) *)
-
-type mqresult =
-   | MQRefs of mqrefs