]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql/mQueryTParser.mly
Merge of the new_mathql branch with the main branch:
[helm.git] / helm / ocaml / mathql / mQueryTParser.mly
index 9bfcd4e0c77cb42aeeb5a345d2c8c9c676f90d34..f32a4118756044213a3a89d2cf4c719caf6398ff 100644 (file)
 /******************************************************************************/
 
 %{
-   open MathQL
+   let analyze x =
+      let module M = MathQL in
+      let rec join l1 l2 = match l1, l2 with
+         | [], _                           -> l2
+         | _, []                           -> l1
+         | s1 :: tl1, s2 :: _ when s1 < s2 -> s1 :: join tl1 l2                     
+         | s1 :: _, s2 :: tl2 when s2 < s1 -> s2 :: join l1 tl2 
+         | s1 :: tl1, s2 :: tl2            -> s1 :: join tl1 tl2 
+      in
+      let rec an_val = function
+         | M.Const _             -> []
+         | M.VVar _              -> []
+         | M.Record (rv, _)      -> [rv]
+         | M.Fun (_, x)          -> an_val x
+         | M.Attribute (_, _, x) -> an_val x
+         | M.RefOf x             -> an_set x
+      and an_boole = function
+         | M.False       -> []
+         | M.True        -> []
+         | M.Ex _ _      -> []
+         | M.Not x       -> an_boole x
+         | M.And (x, y)  -> join (an_boole x) (an_boole y)
+         | M.Or (x, y)   -> join (an_boole x) (an_boole y)
+         | M.Sub (x, y)  -> join (an_val x) (an_val y)
+         | M.Meet (x, y) -> join (an_val x) (an_val y)
+         | M.Eq (x, y)   -> join (an_val x) (an_val y)
+      and an_set = function
+         | M.SVar _                -> []
+         | M.RVar _                -> []
+         | M.Relation (_, _, x, _) -> an_set x
+         | M.Pattern x             -> an_val x
+         | M.Ref x                 -> an_val x
+         | M.Union (x, y)          -> join (an_set x) (an_set y)
+         | M.Intersect (x, y)      -> join (an_set x) (an_set y)
+         | M.Diff (x, y)           -> join (an_set x) (an_set y)
+         | M.LetSVar (_, x, y)     -> join (an_set x) (an_set y)
+         | M.LetVVar (_, x, y)     -> join (an_val x) (an_set y)
+         | M.Select (_, x, y)      -> join (an_set x) (an_boole y)
+      in
+      an_boole x
 %}
    %token    <string> ID STR
-   %token    <MathQL.mqtref> REF
-   %token    LPR RPR DLR SQT DQT EOF PROT SLASH FRAG QUEST STAR SSTAR 
-   %token    NAME
-   %token    MCONCL CONCL
-   %token    TRUE FALSE AND OR NOT IS
-   %token    SELECT IN WHERE USE POS USEDBY PATT UNION INTER
+   %token    SL IS LC RC CM SC LP RP AT PC DL FS DQ EOF 
+   %token    AND ATTR ATTRIB BE DIFF EQ EX FALSE FUN IN INTER LET MEET NOT OR
+   %token    PAT REF REFOF REL SELECT SUB SUPER TRUE UNION WHERE
+   %left     DIFF WHERE REFOF  
    %left     OR UNION
    %left     AND INTER
-   %nonassoc NOT
-   %start    qstr ref query
-   %type     <string>        qstr   
-   %type     <MathQL.mqtref> ref   
-   %type     <MathQL.mquery> query   
+   %nonassoc REL
+   %nonassoc NOT EX IN ATTR
+
+   %start    qstr query result
+   %type     <string>        qstr      
+   %type     <MathQL.query>  query
+   %type     <MathQL.result> result 
 %%
-   prot:
-      | STR  { Some $1 }
-      | STAR { None }
-   ;
-   body:
-      |            { []            }
-      | SLASH body { MQBD :: $2    }
-      | QUEST body { MQBQ :: $2    }
-      | SSTAR body { MQBSS :: $2   }
-      | STAR body  { MQBS :: $2    }
-      | STR body   { MQBC $1 :: $2 } 
-   frag:
-      |                  { []          }
-      | SLASH SSTAR frag { MQFSS :: $3 }
-      | SLASH STAR frag  { MQFS :: $3  }
-      | SLASH STR frag   { try let i = int_of_string $2 in
-                               if i < 1 then raise Parsing.Parse_error;
-                              MQFC i :: $3
-                          with e -> raise Parsing.Parse_error
-                         }
-   ;
-   ref:
-      | prot PROT body DQT           { ($1, $3, []) }
-      | prot PROT body FRAG frag DQT { ($1, $3, $5) }
-   ;   
    qstr:
-      | STR SQT { $1 }
+      | DQ       { ""      }
+      | STR qstr { $1 ^ $2 }
+   ;
+   svar:
+      | PC ID { $2 }
    ;
    rvar:
-      | ID { $1 }
+      | AT ID { $2 }
    ;
-   svar:
-      | DLR ID { $2 }
+   vvar:
+      | DL ID { $2 }
    ;
-   func:
-      | NAME { MQName }
-   ;   
-   str:
-      | MCONCL    { MQMConclusion   }
-      | CONCL     { MQConclusion    }
-      | STR       { MQCons $1       } 
-      | rvar      { MQStringRVar $1 }
-      | svar      { MQStringSVar $1 }
-      | func rvar { MQFunc ($1, $2) }
-   ;
-   boole:
-      | TRUE            { MQTrue         }
-      | FALSE           { MQFalse        }
-      | str IS str      { MQIs ($1, $3)  }
-      | NOT boole       { MQNot $2       }
-      | boole AND boole { MQAnd ($1, $3) }
-      | boole OR boole  { MQOr ($1, $3)  }
-      | LPR boole RPR   { $2             }
+   qstr_list:
+      | STR CM qstr_list { $1 :: $3 }
+      | STR              { [$1]     } 
+   ;
+   vvar_list:
+      | vvar CM vvar_list { $1 :: $3 }
+      | vvar              { [$1]     }
+   ;
+   qstr_path:
+      | STR SL qstr_path { $1 :: $3 }
+      | STR              { [$1]     } 
+   ;
+   ref_op:
+      | SUB   { MathQL.SubOp   }
+      | SUPER { MathQL.SuperOp }
+      |       { MathQL.ExactOp }
+   ;
+   val_exp:
+      | STR                             { MathQL.Const [$1]             } 
+      | FUN STR val_exp                 { MathQL.Fun ($2, $3)           }
+      | ATTRIB ref_op qstr_path val_exp { MathQL.Attribute ($2, $3, $4) }
+      | rvar FS vvar                    { MathQL.Record ($1, $3)        }
+      | vvar                            { MathQL.VVar $1                }
+      | LC qstr_list RC                 { MathQL.Const $2               }
+      | LC RC                           { MathQL.Const []               }
+      | REFOF set_exp                   { MathQL.RefOf $2               }
+      | LP val_exp RP                   { $2                            }
+   ;
+   boole_exp:
+      | TRUE                    { MathQL.True               }
+      | FALSE                   { MathQL.False              }
+      | LP boole_exp RP         { $2                        }
+      | NOT boole_exp           { MathQL.Not $2             }
+      | EX boole_exp            { MathQL.Ex (analyze $2) $2 }
+      | val_exp SUB val_exp     { MathQL.Sub ($1, $3)       }
+      | val_exp MEET val_exp    { MathQL.Meet ($1, $3)      }
+      | val_exp EQ val_exp      { MathQL.Eq ($1, $3)        }
+      | boole_exp AND boole_exp { MathQL.And ($1, $3)       }
+      | boole_exp OR boole_exp  { MathQL.Or ($1, $3)        }
    ;   
-   rlist:
-      | PATT REF                         { MQPattern $2          } 
-      | rlist UNION rlist                { MQUnion ($1, $3)      }
-      | rlist INTER rlist                { MQIntersect ($1, $3)  }
-      | USE rlist POS svar               { MQUse ($2, $4)        }
-      | USEDBY rlist POS svar            { MQUsedBy ($2, $4)     }
-      | SELECT rvar IN rlist WHERE boole { MQSelect ($2, $4, $6) }
-      | LPR rlist RPR                    { $2                    }
+   set_exp:
+      | REF val_exp                                 { MathQL.Ref $2                    }
+      | PAT val_exp                                 { MathQL.Pattern $2                } 
+      | LP set_exp RP                               { $2                               }
+      | SELECT rvar IN set_exp WHERE boole_exp      { MathQL.Select ($2, $4, $6)       }
+      | REL ref_op qstr_path set_exp ATTR vvar_list { MathQL.Relation ($2, $3, $4, $6) }
+      | REL ref_op qstr_path set_exp                { MathQL.Relation ($2, $3, $4, []) }
+      | svar                                        { MathQL.SVar $1                   }
+      | rvar                                        { MathQL.RVar $1                   }
+      | set_exp UNION set_exp                       { MathQL.Union ($1, $3)            }
+      | set_exp INTER set_exp                       { MathQL.Intersect ($1, $3)        }
+      | set_exp DIFF set_exp                        { MathQL.Diff ($1, $3)             }
+      | LET svar BE set_exp IN set_exp              { MathQL.LetSVar ($2, $4, $6)      }      
+      | LET vvar BE val_exp IN set_exp              { MathQL.LetVVar ($2, $4, $6)      }      
    ;
    query:
-      rlist EOF { MQList $1 }
+      | set_exp EOF { $1 }
+   ;
+   attribute:
+      | STR IS qstr_list { ($1, $3) }
+      | STR              { ($1, []) }
+   ;
+   attr_list:
+      | attribute SC attr_list { $1 :: $3 }
+      | attribute              { [$1]     }
    ;
+   group:
+      LC attr_list RC { $2 }
+   ;
+   group_list:
+      | group CM group_list { $1 :: $3 }
+      | group               { [$1]     }
+   ;
+   resource:
+      | STR ATTR group_list { ($1, $3) }
+      | STR                 { ($1, []) }
+   ;
+   resource_list:
+      | resource SC resource_list { $1 :: $3 }
+      | resource                  { [$1]     }
+      |                           { []       }
+   ;   
+   result:
+      | resource_list EOF         { $1 }