]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_test/mQGTopParser.mly
Author specification added in head comments;
[helm.git] / helm / ocaml / mathql_test / mQGTopParser.mly
index e36dd5435c6b4c1e3adba2b6c83dedb1afff2e6a..cf2280dadd8f827ddf98a140f44f639c98d5032b 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
@@ -75,8 +88,8 @@
       | STR qstr { $1 ^ $2 }
    ;
    str:
-      | STR   { $1                            }
-      | DL ID { try G.builtin $2 with _ -> "" }
+      | STR   { $1         }
+      | DL ID { builtin $2 }
    ;
    strs:
       | str CM strs { $1 :: $3 }