X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql%2FmQueryTParser.mly;h=1ebadd29a53ea356fe8f283a4a3d26c18e35b208;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=0b375fcfea5c5ea20c9e4dcaa53b642de5d2802f;hpb=3c57d335904d0480f3145ccdcf663206cffd5567;p=helm.git diff --git a/helm/ocaml/mathql/mQueryTParser.mly b/helm/ocaml/mathql/mQueryTParser.mly index 0b375fcfe..1ebadd29a 100644 --- a/helm/ocaml/mathql/mQueryTParser.mly +++ b/helm/ocaml/mathql/mQueryTParser.mly @@ -34,86 +34,169 @@ /******************************************************************************/ %{ - 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 ID STR - %token 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 qstr - %type ref - %type query + %nonassoc REL + %nonassoc NOT EX IN ATTR + + %start qstr query result + %type qstr + %type query + %type 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 }