X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql%2FmQueryTParser.mly;h=f32a4118756044213a3a89d2cf4c719caf6398ff;hb=ba824e867afc3eaf081ed1a1d6526d421242a6a0;hp=dea5f4883ff9907b53de1866b48532859e193df6;hpb=6c04191a9045120d3cf5f6046eee627d6499e5c9;p=helm.git diff --git a/helm/ocaml/mathql/mQueryTParser.mly b/helm/ocaml/mathql/mQueryTParser.mly index dea5f4883..f32a41187 100644 --- a/helm/ocaml/mathql/mQueryTParser.mly +++ b/helm/ocaml/mathql/mQueryTParser.mly @@ -34,86 +34,156 @@ /******************************************************************************/ %{ - 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 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 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 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 } ; - func: - | NAME { MQName } - ; - str: - | MCONCL { MQMConclusion } - | CONCL { MQConclusion } - | STR { MQCons $1 } - | rvar { MQRVar $1 } - | svar { MQSVar $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 }