X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_test%2FmQGTopParser.mly;h=e36dd5435c6b4c1e3adba2b6c83dedb1afff2e6a;hb=91db309a46f8b6f100a36abbc568deec10a8d1df;hp=8aa01b6c4af0ceb53d50bd508a900ba4fa3000d2;hpb=d59d2f93956bcbe4dd7bb3407e3c53de8b66c003;p=helm.git diff --git a/helm/ocaml/mathql_test/mQGTopParser.mly b/helm/ocaml/mathql_test/mQGTopParser.mly index 8aa01b6c4..e36dd5435 100644 --- a/helm/ocaml/mathql_test/mQGTopParser.mly +++ b/helm/ocaml/mathql_test/mQGTopParser.mly @@ -26,7 +26,6 @@ /* AUTOR: Ferruccio Guidi */ - %{ let f (x, y, z) = x let s (x, y, z) = y @@ -45,11 +44,12 @@ %type CicTextualParser0.interpretation_codomain_item option> interp %token STR - %token DL DQ LC RC CM NOT - %token MOBJ MSORT MREL SOBJ SSORT OREL WOBJ WSORT + %token DL DQ LC RC CM + %token MOBJ MSORT MREL OOBJ OSORT OREL UNIV - %start qstr - %type qstr + %start qstr specs + %type qstr + %type specs %% uri: | CONURI { CicTextualParser0.ConUri $1 } @@ -74,7 +74,7 @@ | DQ { "" } | STR qstr { $1 ^ $2 } ; -/* str: + str: | STR { $1 } | DL ID { try G.builtin $2 with _ -> "" } ; @@ -86,22 +86,16 @@ list: | LC strs RC { $2 } ; - not: - | NOT { true } - | { false } - ; spec: - | MOBJ not list list list { G.MustObj ($2, $3, $4, $5) } - | MSORT not list list list { G.MustSort ($2, $3, $4, $5) } - | MREL not list list { G.MustRel ($2, $3, $4) } - | SOBJ not list list list { G.SOnlyObj ($2, $3, $4, $5) } - | SSORT not list list list { G.SOnlySort ($2, $3, $4, $5) } - | OREL not list list { G.OnlyRel ($2, $3, $4) } - | WOBJ not list list list { G.WOnlyObj ($2, $3, $4, $5) } - | WSORT not list list list { G.WOnlySort ($2, $3, $4, $5) } + | MOBJ list list list { G.MustObj ($2, $3, $4) } + | MSORT list list list { G.MustSort ($2, $3, $4) } + | MREL list list { G.MustRel ($2, $3) } + | OOBJ list list list { G.OnlyObj ($2, $3, $4) } + | OSORT list list list { G.OnlySort ($2, $3, $4) } + | OREL list list { G.OnlyRel ($2, $3) } + | UNIV list { G.Universe $2 } ; specs: | spec specs { $1 :: $2 } | EOF { [] } ; -*/