X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql%2FmathQL.ml;fp=helm%2Focaml%2Fmathql%2FmathQL.ml;h=088d598a4562a260c6c039d5ca097c3ba2de5af2;hb=1456c337a60f6677ee742ff7891d43fc382359a9;hp=d1e89decf9a25f4f7582da4d162bdab11e574be1;hpb=1cfcea66d7394a785ec439cd6b03497b276918c4;p=helm.git

diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml
index d1e89decf..088d598a4 100644
--- a/helm/ocaml/mathql/mathQL.ml
+++ b/helm/ocaml/mathql/mathQL.ml
@@ -47,7 +47,7 @@ type mqsvar = string                       (* name *)
 
 type mqpt = string option                  (* PROTOCOL TOKENS *)
                                            (* Some = constant string *)
-					   (* None = single star: '*' *)
+                                           (* None = single star: '*' *)
 
 type mqbt =                                (* BODY TOKENS *)
    | MQBC of string                        (* a constant string *)
@@ -67,6 +67,26 @@ type mqpattern = mqtref                     (* constant pattern *)
 
 type mqfunc =
    | MQName                                 (* NAME *)
+   | MQTheory
+   | MQTitle
+   | MQContributor
+   | MQCreator
+   | MQPublisher
+   | MQSubject
+   | MQDescription
+   | MQDate
+   | MQType
+   | MQFormat
+   | MQIdentifier
+   | MQLanguage
+   | MQRelation
+   | MQSource
+   | MQCoverage
+   | MQRights
+   | MQInstitution
+   | MQContact
+   | MQFirstVersion
+   | MQModified
 
 type mqstring =
    | MQCons of string                       (* constant *)
@@ -76,21 +96,33 @@ type mqstring =
    | MQMConclusion                          (* main conclusion *)
    | MQConclusion                           (* inner conclusion *)
 
+type mqorder =
+   | MQAsc
+   | MQDesc
+
 type mqbool =
    | MQTrue
    | MQFalse
    | MQAnd of mqbool * mqbool
    | MQOr of mqbool * mqbool
    | MQNot of mqbool
-   | MQIs of mqstring * mqstring            (* operands *)
-
-type mqlist =
-   | MQSelect of mqrvar * mqlist * mqbool   (* rvar, list, boolean *) 
-   | MQUse of mqlist * mqsvar               (* list, Position attribute *)
-   | MQUsedBy of mqlist * mqsvar            (* list, Position attribute *)
-   | MQPattern of mqpattern                 (* pattern *)
-   | MQUnion of mqlist * mqlist             (* operands *)
-   | MQIntersect of mqlist * mqlist         (* operands *)
+   | 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. *)
+
+and mqlist =
+   | MQSelect of mqrvar * mqlist * mqbool   (* rvar, list, boolean        *) 
+   | MQUse of mqlist * mqsvar               (* list, Position attribute   *)
+   | MQUsedBy of mqlist * mqsvar            (* list, Position attribute   *)
+   | MQPattern of mqpattern                 (* pattern                    *)
+   | MQUnion of mqlist * mqlist             (* operands                   *)
+   | MQIntersect of mqlist * mqlist         (* operands                   *)
+   | MQSortedBy of mqlist * mqorder * mqfunc (*  *)
+   | MQRVarOccur of mqrvar
+   | MQDiff of mqlist * mqlist               (*  *)
 
 type mquery =
    | MQList of mqlist