]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_generator/mQueryGenerator.ml
Author specification added in head comments;
[helm.git] / helm / ocaml / mathql_generator / mQueryGenerator.ml
index 24720d0aab4c9a4051168f7cd6218147a393ed90..2d529c9e8aa32f9f23659bebafcc418706bc5378 100644 (file)
@@ -23,6 +23,9 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
 type uri = string
 type position = string
 type depth = string
@@ -36,6 +39,15 @@ 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
@@ -43,9 +55,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 = ns ^ "Set" then "$SET" else
-   if s = ns ^ "Prop" then "$PROP" else
-   if s = ns ^ "Type" then "$TYPE" else s
+   if s =      "Set" then "$SET" else
+   if s =      "Prop" then "$PROP" else
+   if s =      "Type" then "$TYPE" else s
 
 let text_of_spec out l =
    let rec iter = function 
@@ -164,15 +176,14 @@ let compose cl =
 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"  -> ns ^ "Set"
-      | "PROP" -> ns ^ "Prop"
-      | "TYPE" -> ns ^ "Type"
-      | _      -> raise (Failure "MQueryGenerator.builtin")
+      | MainHypothesis -> ns ^ "MainHypothesis"
+      | InHypothesis   -> ns ^ "InHypothesis"
+      | MainConclusion -> ns ^ "MainConclusion"
+      | InConclusion   -> ns ^ "InConclusion"
+      | InBody         -> ns ^ "InBody"
+      | Set            ->      "Set"
+      | Prop           ->      "Prop"
+      | Type           ->      "Type"
 
 (* conversion functions from the old constraints  ***************************)