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