]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_test/mQGTopParser.mly
This commit was manufactured by cvs2svn to create tag
[helm.git] / helm / ocaml / mathql_test / mQGTopParser.mly
index cf2280dadd8f827ddf98a140f44f639c98d5032b..e36dd5435c6b4c1e3adba2b6c83dedb1afff2e6a 100644 (file)
    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
@@ -88,8 +75,8 @@
       | STR qstr { $1 ^ $2 }
    ;
    str:
-      | STR   { $1         }
-      | DL ID { builtin $2 }
+      | STR   { $1                            }
+      | DL ID { try G.builtin $2 with _ -> "" }
    ;
    strs:
       | str CM strs { $1 :: $3 }