X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql%2FmQueryTParser.mly;h=7f1c6e91bfaa2e0a0993cfd6f23881e6214968b1;hb=57a47d11437c168d5ee1c6024ae7a48df8a302ba;hp=9bfcd4e0c77cb42aeeb5a345d2c8c9c676f90d34;hpb=8adca9e9d6f3b7c605e570dadb4bb82a16b3d050;p=helm.git diff --git a/helm/ocaml/mathql/mQueryTParser.mly b/helm/ocaml/mathql/mQueryTParser.mly index 9bfcd4e0c..7f1c6e91b 100644 --- a/helm/ocaml/mathql/mQueryTParser.mly +++ b/helm/ocaml/mathql/mQueryTParser.mly @@ -34,61 +34,33 @@ /******************************************************************************/ %{ - open MathQL %} %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 LC RC CM SC LP RP AT PC DL FS DQ EOF + %token AND ATTR ATTRIB DIFF EQ FALSE FUN IN INTER NOT OR PAT REF REFOF + %token REL SELECT SUB SUPER TRUE UNION WHERE + %left DIFF %left OR UNION %left AND INTER %nonassoc NOT %start qstr ref query - %type qstr - %type ref - %type query + %type qstr + %type query %% - 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 } + | QT { "" } + | 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: + val: | MCONCL { MQMConclusion } | CONCL { MQConclusion } | STR { MQCons $1 }