]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql/mathQL.ml
mathQL modified, stderr corrected to stdout im mathql_interpreter,
[helm.git] / helm / ocaml / mathql / mathQL.ml
index 82ab6f9da3bec59495864f787ecdf15928d37ed4..d18ebbc9243afa5d1fc3b87e8718cc68aaf83116 100644 (file)
@@ -67,8 +67,6 @@ type mquref = UriManager.uri * (int list) (* uri, fragment identifier *)
 
 type mqtref = mqpt * (mqbt list) * (mqft list) (* tokenized pattern reference *)
 
-type mqref = string (* format for references (helper) *)
-
 type mqfunc =
    | MQName         (* Name *)
    | MQTheory       (* theory *)
@@ -115,8 +113,8 @@ type mqbool =
    | MQSubset of mqlist * mqlist   (* the two lists denote two sets, the 1st subset of the 2nd *)
 
 and mqlist =
-   | MQReference of mqref list               (* reference list *)
-   | MQPattern of mqtref list                (* pattern list *)
+   | MQReference of string list              (* reference list *)
+   | MQPattern of mqtref                     (* pattern *)
    | MQListLVar of mqlvar                    (* lvar *)
    | MQListRVar of mqrvar                    (* rvar *)
    | MQSelect of mqrvar * mqlist * mqbool    (* rvar, list, boolean *) 
@@ -127,8 +125,7 @@ and mqlist =
    | MQSortedBy of mqlist * mqorder * mqfunc (* ordering *)
    | MQDiff of mqlist * mqlist               (* set difference  *)
    | MQLetIn of mqlvar * mqlist * mqlist     (* explicit lvar assignment *)
-   | MQMinimize of mqlist                    (* list minimization *)
-   
+
 type mquery =
    | MQList of mqlist
    
@@ -136,4 +133,4 @@ type mquery =
 (* main type is mqresult                                                    *)
 
 type mqresult =
-   | MQRefs of mqref list
+   | MQRefs of string list