]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_generator/mQueryGenerator.ml
This commit was manufactured by cvs2svn to create tag
[helm.git] / helm / ocaml / mathql_generator / mQueryGenerator.ml
index 2d529c9e8aa32f9f23659bebafcc418706bc5378..24720d0aab4c9a4051168f7cd6218147a393ed90 100644 (file)
@@ -23,9 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
 type uri = string
 type position = string
 type depth = string
@@ -39,15 +36,6 @@ type spec = MustObj  of uri list * position list * depth list
          | OnlyRel  of position list * depth list
          | Universe of position list 
 
-type builtin_t = MainHypothesis
-               | InHypothesis
-              | MainConclusion
-              | InConclusion
-              | InBody
-              | Set
-              | Prop
-              | Type
-
 let text_of_builtin s =
    let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
    if s = ns ^ "MainHypothesis" then "$MH" else
@@ -55,9 +43,9 @@ let text_of_builtin s =
    if s = ns ^ "MainConclusion" then "$MC" else
    if s = ns ^ "InConclusion" then "$IC" else
    if s = ns ^ "InBody" then "$IB" else
-   if s =      "Set" then "$SET" else
-   if s =      "Prop" then "$PROP" else
-   if s =      "Type" then "$TYPE" else s
+   if s = ns ^ "Set" then "$SET" else
+   if s = ns ^ "Prop" then "$PROP" else
+   if s = ns ^ "Type" then "$TYPE" else s
 
 let text_of_spec out l =
    let rec iter = function 
@@ -176,14 +164,15 @@ let compose cl =
 let builtin s = 
    let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
    match s with
-      | MainHypothesis -> ns ^ "MainHypothesis"
-      | InHypothesis   -> ns ^ "InHypothesis"
-      | MainConclusion -> ns ^ "MainConclusion"
-      | InConclusion   -> ns ^ "InConclusion"
-      | InBody         -> ns ^ "InBody"
-      | Set            ->      "Set"
-      | Prop           ->      "Prop"
-      | Type           ->      "Type"
+      | "MH"   -> ns ^ "MainHypothesis"
+      | "IH"   -> ns ^ "InHypothesis"
+      | "MC"   -> ns ^ "MainConclusion"
+      | "IC"   -> ns ^ "InConclusion"
+      | "IB"   -> ns ^ "InBody"
+      | "SET"  -> ns ^ "Set"
+      | "PROP" -> ns ^ "Prop"
+      | "TYPE" -> ns ^ "Type"
+      | _      -> raise (Failure "MQueryGenerator.builtin")
 
 (* conversion functions from the old constraints  ***************************)