]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_interpreter/mathql.ml
* New operators (Subset, SetEqual and RVarOccurrence) added to MathQL
[helm.git] / helm / ocaml / mathql_interpreter / mathql.ml
index 01cbf431a21b5103963c9fa716b190f07405600f..e78029036f28f5dcb963d5d01564941fe399c2ff 100644 (file)
@@ -93,6 +93,10 @@ type mqstring =
    | MQMConclusion                           (* main conclusion *)
    | MQConclusion                            (* inner conclusion *)
 
+type mqorder =
+   | MQAsc
+   | MQDesc
+
 type mqbool =
    | MQTrue
    | MQFalse
@@ -100,12 +104,13 @@ type mqbool =
    | MQOr of mqbool * mqbool
    | MQNot of mqbool
    | MQIs of mqstring * mqstring             (* operands *)
+   | MQSetEqual of mqlist * mqlist           (* the two lists denote the *)
+                                             (* same set                 *)
+   | MQSubset of mqlist * mqlist             (* the two lists denote two   *)
+                                             (* sets, the first one        *)
+                                             (* subsect of the second one. *)
 
-type mqorder =
-   | MQAsc
-   | MQDesc
-
-type mqlist =
+and mqlist =
    | MQSelect of mqrvar * mqlist * mqbool    (* rvar, list, boolean *) 
    | MQUse of mqlist * mqsvar                (* list, Position attribute *)
    | MQUsedBy of mqlist * mqsvar             (* list, Position attribute *)
@@ -114,6 +119,7 @@ type mqlist =
    | MQDiff of mqlist * mqlist               (*  *)
    | MQIntersect of mqlist * mqlist          (*  *)
    | MQSortedBy of mqlist * mqorder * mqfunc (*  *)
+   | MQRVarOccur of mqrvar
 
 type mquery =
    | MQList of mqlist