]> matita.cs.unibo.it Git - helm.git/blob - mQueryTParser.mly
390c214b4a725cdcefc7e3a16a851f65b242444c
[helm.git] / 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 /******************************************************************************/
27 /*                                                                            */
28 /*                               PROJECT HELM                                 */
29 /*                                                                            */
30 /*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   */
31 /*                                 23/05/2002                                 */
32 /*                                                                            */
33 /*                                                                            */
34 /******************************************************************************/
35
36 %{
37    let analyze x =
38       let module M = MathQL in
39       let rec join l1 l2 = match l1, l2 with
40          | [], _                           -> l2
41          | _, []                           -> l1
42          | s1 :: tl1, s2 :: _ when s1 < s2 -> s1 :: join tl1 l2                     
43          | s1 :: _, s2 :: tl2 when s2 < s1 -> s2 :: join l1 tl2 
44          | s1 :: tl1, s2 :: tl2            -> s1 :: join tl1 tl2 
45       in
46       let rec an_val = function
47          | M.Const _               -> []
48          | M.VVar _                -> []
49          | M.Record (rv, _)        -> [rv]
50          | M.Fun (_, x)            -> an_val x
51          | M.Property (_, _, _, x) -> an_val x
52          | M.RefOf x               -> an_set x
53       and an_boole = function
54          | M.False       -> []
55          | M.True        -> []
56          | M.Ex _        -> []
57          | M.Not x       -> an_boole x
58          | M.And (x, y)  -> join (an_boole x) (an_boole y)
59          | M.Or (x, y)   -> join (an_boole x) (an_boole y)
60          | M.Sub (x, y)  -> join (an_val x) (an_val y)
61          | M.Meet (x, y) -> join (an_val x) (an_val y)
62          | M.Eq (x, y)   -> join (an_val x) (an_val y)
63       and an_set = function
64          | M.SVar _                   -> []
65          | M.RVar _                   -> []
66          | M.Relation (_, _, _, x, _) -> an_set x
67          | M.Pattern x                -> an_val x
68          | M.Ref x                    -> an_val x
69          | M.Union (x, y)             -> join (an_set x) (an_set y)
70          | M.Intersect (x, y)         -> join (an_set x) (an_set y)
71          | M.Diff (x, y)              -> join (an_set x) (an_set y)
72          | M.LetSVar (_, x, y)        -> join (an_set x) (an_set y)
73          | M.LetVVar (_, x, y)        -> join (an_val x) (an_set y)
74          | M.Select (_, x, y)         -> join (an_set x) (an_boole y)
75       in
76       an_boole x
77       
78    let path_of_vvar v = (v, [])
79 %}
80    %token    <string> ID STR
81    %token    SL IS LC RC CM SC LP RP AT PC DL FS DQ GETS EOF 
82    %token    AND ATTR BE DIFF EQ EX FALSE FUN IN INTER INV LET MEET NOT OR PAT
83    %token    PROP REF REFOF REL SELECT SUB SUPER TRUE UNION WHERE
84    %left     DIFF WHERE REFOF  
85    %left     OR UNION
86    %left     AND INTER
87    %nonassoc REL 
88    %nonassoc NOT EX IN ATTR
89
90    %start    qstr query result
91    %type     <string>        qstr      
92    %type     <MathQL.query>  query
93    %type     <MathQL.result> result 
94 %%
95    qstr:
96       | DQ       { ""      }
97       | STR qstr { $1 ^ $2 }
98    ;
99    svar:
100       | PC ID { $2 }
101    ;
102    rvar:
103       | AT ID { $2 }
104    ;
105    vvar:
106       | DL ID { $2 }
107    ;
108    strs:
109       | STR CM strs { $1 :: $3 }
110       | STR         { [$1]     } 
111    ;
112    subpath:
113       | STR SL subpath { $1 :: $3 }
114       | STR            { [$1]     } 
115    ;
116    path:
117       | STR SL subpath { ($1, $3) }
118       | STR            { ($1, []) }
119    ;   
120    inv:
121       | INV { true  }
122       |     { false }
123    ;
124    ref:
125       | SUB   { MathQL.RefineSub   }
126       | SUPER { MathQL.RefineSuper }
127       |       { MathQL.RefineExact }
128    ;
129    assign:
130       | vvar GETS path { (path_of_vvar $1, $3) }
131    ;
132    assigns:
133       | assign CM assigns { $1 :: $3 }
134       | assign            { [$1] }
135    ;   
136    val_exp:
137       | STR                       { MathQL.Const [$1]                } 
138       | FUN STR val_exp           { MathQL.Fun ($2, $3)              }
139       | PROP inv ref path val_exp { MathQL.Property ($2, $3, $4, $5) }
140       | rvar FS vvar              { MathQL.Record ($1, path_of_vvar $3) }
141       | vvar                      { MathQL.VVar $1                   }
142       | LC strs RC                { MathQL.Const $2                  }
143       | LC RC                     { MathQL.Const []                  }
144       | REFOF set_exp             { MathQL.RefOf $2                  }
145       | LP val_exp RP             { $2                               }
146    ;
147    boole_exp:
148       | TRUE                    { MathQL.True               }
149       | FALSE                   { MathQL.False              }
150       | LP boole_exp RP         { $2                        }
151       | NOT boole_exp           { MathQL.Not $2             }
152       | EX boole_exp            { MathQL.Ex (analyze $2) $2 }
153       | val_exp SUB val_exp     { MathQL.Sub ($1, $3)       }
154       | val_exp MEET val_exp    { MathQL.Meet ($1, $3)      }
155       | val_exp EQ val_exp      { MathQL.Eq ($1, $3)        }
156       | boole_exp AND boole_exp { MathQL.And ($1, $3)       }
157       | boole_exp OR boole_exp  { MathQL.Or ($1, $3)        }
158    ;   
159    set_exp:
160       | REF val_exp                            { MathQL.Ref $2                    }
161       | PAT val_exp                            { MathQL.Pattern $2                } 
162       | LP set_exp RP                          { $2                               }
163       | SELECT rvar IN set_exp WHERE boole_exp { MathQL.Select ($2, $4, $6)       }
164       | REL inv ref path val_exp ATTR assigns  { MathQL.Relation ($2, $3, $4, MathQL.Ref $5, $7) }
165       | REL inv ref path val_exp               { MathQL.Relation ($2, $3, $4, MathQL.Ref $5, []) }
166       | svar                                   { MathQL.SVar $1                   }
167       | rvar                                   { MathQL.RVar $1                   }
168       | set_exp UNION set_exp                  { MathQL.Union ($1, $3)            }
169       | set_exp INTER set_exp                  { MathQL.Intersect ($1, $3)        }
170       | set_exp DIFF set_exp                   { MathQL.Diff ($1, $3)             }
171       | LET svar BE set_exp IN set_exp         { MathQL.LetSVar ($2, $4, $6)      }      
172       | LET vvar BE val_exp IN set_exp         { MathQL.LetVVar ($2, $4, $6)      }      
173    ;
174    query:
175       | set_exp       { $1                }
176       | set_exp error { $1                }
177       | EOF           { raise End_of_file }
178    ;
179    attr:
180       | vvar IS strs { (path_of_vvar $1, $3) }
181       | vvar         { (path_of_vvar $1, []) }
182    ;
183    attrs:
184       | attr SC attrs { $1 :: $3 }
185       | attr          { [$1]     }
186    ;
187    group:
188       LC attrs RC { $2 }
189    ;
190    groups:
191       | group CM groups { $1 :: $3 }
192       | group           { [$1]     }
193    ;
194    resource:
195       | STR ATTR groups { ($1, $3) }
196       | STR             { ($1, []) }
197    ;
198    resources:
199       | resource SC resources { $1 :: $3 }
200       | resource              { [$1]     }
201       |                       { []       }
202    ;   
203    result:
204       | resources { $1                }
205       | EOF       { raise End_of_file }