]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql/mQueryTParser.mly
Initial revision
[helm.git] / helm / ocaml / mathql / mQueryTParser.mly
index 0b375fcfea5c5ea20c9e4dcaa53b642de5d2802f..1ebadd29a53ea356fe8f283a4a3d26c18e35b208 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.Property (_, _, _, 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
+      
+   let path_of_vvar v = (v, [])
 %}
    %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 GETS EOF 
+   %token    AND ATTR BE DIFF EQ EX FALSE FUN IN INTER INV LET MEET NOT OR PAT
+   %token    PROP 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 }
+   ;
+   strs:
+      | STR CM strs { $1 :: $3 }
+      | STR         { [$1]     } 
+   ;
+   subpath:
+      | STR SL subpath { $1 :: $3 }
+      | STR            { [$1]     } 
    ;
-   func:
-      | NAME { MQName }
+   path:
+      | STR SL subpath { ($1, $3) }
+      | STR            { ($1, []) }
    ;   
-   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             }
+   inv:
+      | INV { true  }
+      |     { false }
+   ;
+   ref:
+      | SUB   { MathQL.RefineSub   }
+      | SUPER { MathQL.RefineSuper }
+      |       { MathQL.RefineExact }
+   ;
+   assign:
+      | vvar GETS path { (path_of_vvar $1, $3) }
+   ;
+   assigns:
+      | assign CM assigns { $1 :: $3 }
+      | assign            { [$1] }
    ;   
-   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                    }
+   val_exp:
+      | STR                       { MathQL.Const [$1]                } 
+      | FUN STR val_exp           { MathQL.Fun ($2, $3)              }
+      | PROP inv ref path val_exp { MathQL.Property ($2, $3, $4, $5) }
+      | rvar FS vvar              { MathQL.Record ($1, path_of_vvar $3) }
+      | vvar                      { MathQL.VVar $1                   }
+      | LC strs 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)        }
+   ;   
+   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 inv ref path val_exp ATTR assigns  { MathQL.Relation ($2, $3, $4, MathQL.Ref $5, $7) }
+      | REL inv ref path val_exp               { MathQL.Relation ($2, $3, $4, MathQL.Ref $5, []) }
+      | 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 }
+   ;
+   attr:
+      | vvar IS strs { (path_of_vvar $1, $3) }
+      | vvar         { (path_of_vvar $1, []) }
    ;
+   attrs:
+      | attr SC attrs { $1 :: $3 }
+      | attr          { [$1]     }
+   ;
+   group:
+      LC attrs RC { $2 }
+   ;
+   groups:
+      | group CM groups { $1 :: $3 }
+      | group           { [$1]     }
+   ;
+   resource:
+      | STR ATTR groups { ($1, $3) }
+      | STR             { ($1, []) }
+   ;
+   resources:
+      | resource SC resources { $1 :: $3 }
+      | resource              { [$1]     }
+      |                       { []       }
+   ;   
+   result:
+      | resources EOF { $1 }