]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/mathql_interpreter/mQueryTParser.mly
1025cf3167b1e578e4eb7b897de6b0b293fe9d2f
[helm.git] / helm / ocaml / mathql_interpreter / mQueryTParser.mly
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 /*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
27  */ 
28
29 %{
30    module M = MathQL
31    module L = MQILib
32
33    let make_fun p pl xl = 
34       L.check_arity p (List.length pl) (List.length xl); 
35       M.Fun p pl xl
36
37    let analyze x =
38       let rec join l1 l2 = match l1, l2 with
39          | [], _                           -> l2
40          | _, []                           -> l1
41          | s1 :: tl1, s2 :: _ when s1 < s2 -> s1 :: join tl1 l2
42          | s1 :: _, s2 :: tl2 when s2 < s1 -> s2 :: join l1 tl2
43          | s1 :: tl1, s2 :: tl2            -> s1 :: join tl1 tl2 
44       in
45       let rec iter f = function
46          | []  -> []
47          | head :: tail -> join (f head) (iter f tail)
48       in
49       let rec an_set = function
50          | M.Const _
51          | M.SVar _
52          | M.AVar _
53          | M.Ex _                       -> []
54          | M.Dot rv _                   -> [rv]
55          | M.Let _ x y
56          | M.Select _ x y
57          | M.For _ _ x y                -> iter an_set [x; y]
58          | M.Fun _ _ l                  -> iter an_set l
59          | M.Add _ g x                  -> join (an_grp g) (an_set x)
60          | M.Property _ _ _ _ c d _ _ x -> 
61             join (an_set x) (iter an_con [c; List.concat d])
62       and fc (_, _, v) = an_set v 
63       and an_con c = iter fc c
64       and fg (_, v) = an_set v
65       and an_grp = function
66          | M.Attr g -> iter (iter fg) g
67          | M.From _ -> [] 
68       in
69       an_set x
70       
71    let f (x, y, z) = x
72    let s (x, y, z) = y
73    let t (x, y, z) = z
74 %}
75    %token    <string> ID STR
76    %token    LB RB SL IS LC RC CM SC LP RP AT PC FS DQ EOF 
77    %token    ADD ALIGN AND AS ATTR BE BUT COUNT DIFF DISTR ELSE EMPTY EQ EX  
78    %token    FALSE FOR FROM IF IN INF INTER INV ISF IST KEEP LE LET LOG LT   
79    %token    MAIN MATCH MEET NOT OF OR PAT PROJ PROP SELECT SOURCE STAT SUB 
80    %token    SUP SUPER THEN TRUE UNION WHERE XOR
81    %nonassoc IN SUP INF ELSE LOG STAT KEEP 
82    %left     DIFF   
83    %left     UNION
84    %left     INTER
85    %nonassoc WHERE EX
86    %left     XOR OR
87    %left     AND
88    %nonassoc NOT 
89    %nonassoc SUB MEET EQ LT LE
90    %nonassoc OF PROJ COUNT ALIGN
91    
92    %start    qstr query result
93    %type     <string>        qstr      
94    %type     <MathQL.query>  query
95    %type     <MathQL.result> result 
96 %%
97    qstr:
98       | DQ       { ""      }
99       | STR qstr { $1 ^ $2 }
100    ;
101    svar:
102       | PC ID { $2 }
103    ;
104    avar:
105       | AT ID { $2 }
106    ;
107    strs:
108       | STR CM strs { $1 :: $3 }
109       | STR         { [$1]     } 
110    ;
111    subpath:
112       | STR SL subpath { $1 :: $3 }
113       | STR            { [$1]     } 
114    ;
115    path:
116       | SL subpath { $2 }
117       | SL         { [] }
118    ;   
119    paths:
120       | path CM paths { $1 :: $3 }
121       | path          { [$1]     }
122    inv:
123       | INV { true  }
124       |     { false }
125    ;
126    ref:
127       | SUB   { M.RefineSub   }
128       | SUPER { M.RefineSuper }
129       |       { M.RefineExact }
130    ;
131    qualif:
132       | inv ref path { $1, $2, $3 } 
133    ;
134    cons:
135       | path IN set_exp    { (false, $1, $3) }
136       | path MATCH set_exp { (true, $1, $3)  }
137    ;
138    conss:
139       | cons CM conss { $1 :: $3 }
140       | cons          { [$1]     }
141    ;
142    istrue:
143       | IST conss { $2 }
144       |           { [] }
145    ;
146    isfalse:
147       |                   { []       }
148       | ISF conss isfalse { $2 :: $3 }
149    ;
150    mainc: 
151       | MAIN path { $2 }
152       |           { [] }
153    ;
154    exp:
155       | path AS path { $1, Some $3 }
156       | path         { $1, None    }
157    ;
158    exps:
159       | exp CM exps { $1 :: $3 }
160       | exp         { [$1]     }
161    ;   
162    attrc:
163       | ATTR exps { $2 }
164       |           { [] }
165    ;
166    pattern:
167       | PAT { true  }
168       |     { false }
169    ;
170    ass:
171       | set_exp AS path { ($3, $1) }
172    ;
173    asss:
174       | ass CM asss { $1 :: $3 }
175       | ass         { [$1]     }
176    ;
177    assg:
178       | asss SC assg { $1 :: $3 }
179       | asss         { [$1]     }
180    ;      
181    distr:
182       | DISTR { true  }
183       |       { false }
184    ;
185    allbut:
186       | BUT { "allbut" }
187       |     { "these"  }
188    ;   
189    gen_op:
190       | SUP set_exp { M.GenFJoin, $2 }
191       | INF set_exp { M.GenFMeet, $2 }
192    ;   
193    source:
194       | SOURCE { "source" }
195       |        { "result" }
196    ;
197    xml:
198       | { "text" }
199    ;
200    grp_exp:
201       | assg { M.Attr $1 }
202       | avar { M.From $1 }
203    ;
204    set_exp:
205       | FALSE
206          { make_fun ["false"] [] [] }
207       | TRUE
208          { make_fun ["true"] [] [] }
209       | STR 
210          { M.Const [$1, []] }
211       | LB resources RB 
212          { M.Const $2 }
213       | avar FS path
214          { M.Dot $1 $3 }
215       | LC sets RC
216          { make_fun ["union"] [] $2 }
217       | LC RC
218          { make_fun ["union"] [] [] }
219       | LP set_exp RP
220          { $2 }
221       | STAT set_exp
222          { make_fun ["stat"] [] [$2] }
223       | EX set_exp
224          { M.Ex (analyze $2) $2 }
225       | NOT set_exp
226          { make_fun ["not"] [] [$2] }
227       | PROJ path OF set_exp
228          { make_fun ["proj"] [$2] [$4] }
229       | COUNT set_exp
230          { make_fun ["count"] [] [$2] }
231       | ALIGN set_exp IN set_exp    
232          { make_fun ["align"] [] [$2; $4] }
233       | EMPTY
234          { make_fun ["false"] [] [] }
235       | svar
236          { M.SVar $1 }
237       | avar
238          { M.AVar $1 }
239       | LET svar BE set_exp IN set_exp
240          { M.Let $2 $4 $6 }
241       | FOR avar IN set_exp gen_op             
242          { M.For (fst $5) $2 $4 (snd $5) }
243       | ADD distr grp_exp IN set_exp
244          { M.Add $2 $3 $5 }
245       | IF set_exp THEN set_exp ELSE set_exp
246          { make_fun ["diff"] [] [$2; $4; $6] }
247       | PROP qualif mainc istrue isfalse attrc OF pattern set_exp     
248          { M.Property (f $2) (s $2) (t $2) $3 $4 $5 $6 $8 $9 }
249       | LOG xml source set_exp
250          { make_fun ["log"; $2; $3] [] [$4] }
251       | KEEP allbut paths IN set_exp
252          { make_fun ["keep"; $2] $3 [$5] } 
253       | KEEP allbut set_exp
254          { make_fun ["keep"; $2] [] [$3] } 
255       | SELECT avar FROM set_exp WHERE set_exp
256          { M.Select $2 $4 $6 }
257       | path LC paths RC LC sets RC
258          { make_fun $1 $3 $6 }
259       | path LC sets RC
260          { make_fun $1 [] $3 }    
261       | path LC RC
262          { make_fun $1 [] [] }
263       | set_exp DIFF set_exp
264          { make_fun ["diff"] [] [$1; $3] }
265       | set_exp UNION set_exp
266          { make_fun ["union"] [] [$1; $3] }
267       | set_exp INTER set_exp
268          { make_fun ["intersect"] [] [$1; $3] }
269       | set_exp XOR set_exp
270          { make_fun ["xor"] [] [$1; $3] }
271       | set_exp OR set_exp
272          { make_fun ["or"] [] [$1; $3] }
273       | set_exp AND set_exp
274          { make_fun ["and"] [] [$1; $3] }
275       | set_exp SUB set_exp
276          { make_fun ["sub"] [] [$1; $3] }
277       | set_exp MEET set_exp
278          { make_fun ["meet"] [] [$1; $3] }
279       | set_exp EQ set_exp
280          { make_fun ["eq"] [] [$1; $3] }
281       | set_exp LE set_exp
282          { make_fun ["le"] [] [$1; $3] }
283       | set_exp LT set_exp
284          { make_fun ["lt"] [] [$1; $3] }
285    ;   
286    sets:
287       | set_exp CM sets { $1 :: $3 }
288       | set_exp         { [$1]     }
289    ;
290    query:
291       | set_exp       { $1                }
292       | set_exp error { $1                }
293       | EOF           { raise End_of_file }
294    ;
295    attr:
296       | path IS strs { $1, $3 }
297       | path         { $1, [] }
298    ;
299    attrs:
300       | attr SC attrs { $1 :: $3 }
301       | attr          { [$1]     }
302    ;
303    group:
304       LC attrs RC { $2 }
305    ;
306    groups:
307       | group CM groups { $1 :: $3 }
308       | group           { [$1]     }
309    ;
310    resource:
311       | STR ATTR groups { ($1, $3) }
312       | STR             { ($1, []) }
313    ;
314    resources:
315       | resource SC resources { $1 :: $3 }
316       | resource              { [$1]     }
317       |                       { []       }
318    ;   
319    result:
320       | resources       { $1                }
321       | resources error { $1                }
322       | EOF             { raise End_of_file }