X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_test%2FmQGTopParser.mly;h=cf2280dadd8f827ddf98a140f44f639c98d5032b;hb=65e3c9976212e04a4678ff9ce9e3c2f436d06d33;hp=8aa01b6c4af0ceb53d50bd508a900ba4fa3000d2;hpb=02f8929bd58c6408545b550bcad0edb8702ca933;p=helm.git

diff --git a/helm/ocaml/mathql_test/mQGTopParser.mly b/helm/ocaml/mathql_test/mQGTopParser.mly
index 8aa01b6c4..cf2280dad 100644
--- a/helm/ocaml/mathql_test/mQGTopParser.mly
+++ b/helm/ocaml/mathql_test/mQGTopParser.mly
@@ -26,12 +26,24 @@
 /*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
  */
 
-
 %{
    let f (x, y, z) = x
    let s (x, y, z) = y
    let t (x, y, z) = z
-   
+
+   let builtin s = 
+      let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
+      match s with
+         | "MH"   -> ns ^ "MainHypothesis"
+         | "IH"   -> ns ^ "InHypothesis"
+         | "MC"   -> ns ^ "MainConclusion"
+         | "IC"   -> ns ^ "InConclusion"
+         | "IB"   -> ns ^ "InBody"
+         | "SET"  ->      "Set"
+         | "PROP" ->      "Prop"
+         | "TYPE" ->      "Type"
+         | _      -> raise Parsing.Parse_error
+
    module G = MQueryGenerator
 %}
    %token <string> ID
@@ -45,11 +57,12 @@
    %type  <CicTextualParser0.interpretation_domain_item -> CicTextualParser0.interpretation_codomain_item option> interp
    
    %token <string> 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  <string>                       qstr
+   %start qstr specs
+   %type  <string>                    qstr
+   %type  <MQueryGenerator.spec list> specs
 %%
    uri:
       | CONURI    { CicTextualParser0.ConUri $1                           }
@@ -74,9 +87,9 @@
       | DQ       { ""      }
       | STR qstr { $1 ^ $2 }
    ;
-/*   str:
-      | STR   { $1                            }
-      | DL ID { try G.builtin $2 with _ -> "" }
+   str:
+      | STR   { $1         }
+      | DL ID { builtin $2 }
    ;
    strs:
       | str CM strs { $1 :: $3 }
@@ -86,22 +99,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        { []       }
    ;
-*/