From: Claudio Sacerdoti Coen Date: Mon, 20 May 2002 13:51:31 +0000 (+0000) Subject: mathql.ml is now part of ocaml/mathql_interpreter X-Git-Tag: V_0_3_0_debian_8~96 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4d04f9f79e41245f6ed83ff0e45e9b5a97ecee1a;p=helm.git mathql.ml is now part of ocaml/mathql_interpreter --- diff --git a/helm/gTopLevel/mathql.ml b/helm/gTopLevel/mathql.ml deleted file mode 100644 index 2279551c6..000000000 --- a/helm/gTopLevel/mathql.ml +++ /dev/null @@ -1,104 +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 *) -(* Domenico Lordi *) -(* 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 * string * mqfi (* HELM preamble, - uri pattern, - extension, - fragment identifier *) - -type mqpattern = mqtref (* constant pattern *) - -type mqfunc = - | MQName (* NAME *) - -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 mqbool = - | MQTrue - | MQFalse - | MQAnd of mqbool * mqbool - | MQOr of mqbool * mqbool - | MQNot of mqbool - | MQIs of mqstring * mqstring (* operands *) - -type mqlist = - | MQSelect of mqrvar * mqlist * mqbool (* rvar, list, boolean *) - | MQUse of mqlist * mqsvar (* list, Position attribute *) - | MQPattern of mqpattern (* pattern *) - | MQUnion of mqlist * mqlist (* *) - | MQIntersect of mqlist * mqlist (* *) - -type mquery = - | MQList of mqlist - -(* Output types *************************************************************) -(* main type is mqresult *) - -(* TODO: usare le uri in questo formato *) -type mquref = UriManager.uri * mqfi (* uri, fragment identifier *) - -type mqrefs = mqtref list (* list of references (helper) *) - -type mqresult = - | MQRefs of mqrefs