helm/ocaml/mathql_interpreter/mathql.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   *)
  31 (*                     Domenico Lordi  <lordi@cs.unibo.it>                    *)
  32 (*                                 30/04/2002                                 *)
  33 (*                                                                            *)
  34 (*                                                                            *)
  35 (******************************************************************************)
  36
  37 exception MQInvalidURI of string
  38 exception MQConnectionFailed of string
  39 exception MQInvalidConnection of string
  40
  41 (* Input types **************************************************************)
  42 (* main type is mquery                                                      *)
  43
  44 type mqrvar = string                         (* name *)
  45
  46 type mqsvar = string                         (* name *)
  47
  48 type mquptoken =
  49    | MQString of string                      (* a constant string *)
  50    | MQSlash                                 (* a slash: '/' *)
  51    | MQAnyChr                                (* Any single character: '?' *)
  52    | MQAst                                   (* single asterisk: '*' *)
  53    | MQAstAst                                (* double asterisk: '**' *)
  54
  55 type mqup = mquptoken list                   (* uri pattern (helper) *)
  56
  57 type mqfi = int option * int option
  58
  59 type mqtref = string * mqup * mqfi           (* HELM preamble,
  60                                                 uri pattern,
  61                                                 fragment identifier *)
  62
  63 type mqpattern = mqtref                      (* constant pattern *)
  64
  65 type mqfunc =
  66    | MQName                                  (* NAME *)
  67    | MQTheory
  68    | MQTitle
  69    | MQContributor
  70    | MQCreator
  71    | MQPublisher
  72    | MQSubject
  73    | MQDescription
  74    | MQDate
  75    | MQType
  76    | MQFormat
  77    | MQIdentifier
  78    | MQLanguage
  79    | MQRelation
  80    | MQSource
  81    | MQCoverage
  82    | MQRights
  83    | MQInstitution
  84    | MQContact
  85    | MQFirstVersion
  86    | MQModified
  87
  88 type mqstring =
  89    | MQCons of string                        (* constant *)
  90    | MQFunc of mqfunc * mqrvar               (* function, rvar *)
  91    | MQRVar of mqrvar                        (* rvar *)
  92    | MQSVar of mqsvar                        (* svar *)
  93    | MQMConclusion                           (* main conclusion *)
  94    | MQConclusion                            (* inner conclusion *)
  95
  96 type mqorder =
  97    | MQAsc
  98    | MQDesc
  99
 100 type mqbool =
 101    | MQTrue
 102    | MQFalse
 103    | MQAnd of mqbool * mqbool
 104    | MQOr of mqbool * mqbool
 105    | MQNot of mqbool
 106    | MQIs of mqstring * mqstring             (* operands *)
 107    | MQSetEqual of mqlist * mqlist           (* the two lists denote the *)
 108                                              (* same set                 *)
 109    | MQSubset of mqlist * mqlist             (* the two lists denote two   *)
 110                                              (* sets, the first one        *)
 111                                              (* subsect of the second one. *)
 112
 113 and mqlist =
 114    | MQSelect of mqrvar * mqlist * mqbool    (* rvar, list, boolean *)
 115    | MQUse of mqlist * mqsvar                (* list, Position attribute *)
 116    | MQUsedBy of mqlist * mqsvar             (* list, Position attribute *)
 117    | MQPattern of mqpattern                  (* pattern *)
 118    | MQUnion of mqlist * mqlist              (*  *)
 119    | MQDiff of mqlist * mqlist               (*  *)
 120    | MQIntersect of mqlist * mqlist          (*  *)
 121    | MQSortedBy of mqlist * mqorder * mqfunc (*  *)
 122    | MQRVarOccur of mqrvar
 123
 124 type mquery =
 125    | MQList of mqlist
 126
 127 (* Output types *************************************************************)
 128 (* main type is mqresult                                                    *)
 129
 130 type mquref = UriManager.uri * mqfi          (* uri, fragment identifier *)
 131
 132 type mqrefs = mqtref list                    (* list of references (helper) *)
 133
 134 type mqresult =
 135    | MQRefs of mqrefs