]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql/mathQL.ml
...
[helm.git] / helm / ocaml / mathql / mathQL.ml
index d1e89decf9a25f4f7582da4d162bdab11e574be1..088d598a4562a260c6c039d5ca097c3ba2de5af2 100644 (file)
@@ -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