]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/mathql/mathQL.ml
...
[helm.git] / helm / ocaml / mathql / 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 mqpt = string option                  (* PROTOCOL TOKENS *)
49                                            (* Some = constant string *)
50                                            (* None = single star: '*' *)
51
52 type mqbt =                                (* BODY TOKENS *)
53    | MQBC of string                        (* a constant string *)
54    | MQBD                                  (* a slash: '/' *)
55    | MQBQ                                  (* a question mark: '?' *)
56    | MQBS                                  (* a single star: '*' *)
57    | MQBSS                                 (* a double star: '**' *)
58
59 type mqft =                                (* FRAGMENT TOKENS *)
60    | MQFC of int                           (* a constant integer *)
61    | MQFS                                  (* a single star: '*' *)
62    | MQFSS                                 (* a double star: '**' *)
63
64 type mqtref = mqpt * (mqbt list) * (mqft list) (* tokenized reference *)
65
66 type mqpattern = mqtref                     (* constant pattern *)
67
68 type mqfunc =
69    | MQName                                 (* NAME *)
70    | MQTheory
71    | MQTitle
72    | MQContributor
73    | MQCreator
74    | MQPublisher
75    | MQSubject
76    | MQDescription
77    | MQDate
78    | MQType
79    | MQFormat
80    | MQIdentifier
81    | MQLanguage
82    | MQRelation
83    | MQSource
84    | MQCoverage
85    | MQRights
86    | MQInstitution
87    | MQContact
88    | MQFirstVersion
89    | MQModified
90
91 type mqstring =
92    | MQCons of string                       (* constant *)
93    | MQFunc of mqfunc * mqrvar              (* function, rvar *)
94    | MQRVar of mqrvar                       (* rvar *)
95    | MQSVar of mqsvar                       (* svar *)
96    | MQMConclusion                          (* main conclusion *)
97    | MQConclusion                           (* inner conclusion *)
98
99 type mqorder =
100    | MQAsc
101    | MQDesc
102
103 type mqbool =
104    | MQTrue
105    | MQFalse
106    | MQAnd of mqbool * mqbool
107    | MQOr of mqbool * mqbool
108    | MQNot of mqbool
109    | MQIs of mqstring * mqstring            (* operands                   *)
110    | MQSetEqual of mqlist * mqlist          (* the two lists denote the   *)
111                                             (* same set                   *)
112    | MQSubset of mqlist * mqlist            (* the two lists denote two   *)
113                                             (* sets, the first one        *)
114                                             (* subsect of the second one. *)
115
116 and mqlist =
117    | MQSelect of mqrvar * mqlist * mqbool   (* rvar, list, boolean        *) 
118    | MQUse of mqlist * mqsvar               (* list, Position attribute   *)
119    | MQUsedBy of mqlist * mqsvar            (* list, Position attribute   *)
120    | MQPattern of mqpattern                 (* pattern                    *)
121    | MQUnion of mqlist * mqlist             (* operands                   *)
122    | MQIntersect of mqlist * mqlist         (* operands                   *)
123    | MQSortedBy of mqlist * mqorder * mqfunc (*  *)
124    | MQRVarOccur of mqrvar
125    | MQDiff of mqlist * mqlist               (*  *)
126
127 type mquery =
128    | MQList of mqlist
129    
130 (* Output types *************************************************************)
131 (* main type is mqresult                                                    *)
132
133 (* TODO: usare le uri in questo formato *)
134 type mquref = UriManager.uri * (int list)   (* uri, fragment identifier *)
135
136 type mqrefs = string list                   (* list of references (helper) *)
137
138 type mqresult =
139    | MQRefs of mqrefs