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