From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 May 2002 17:56:23 +0000 (+0000)
Subject: ...
X-Git-Tag: V_0_3_0_debian_8~66
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=1456c337a60f6677ee742ff7891d43fc382359a9

...
---

diff --git a/helm/ocaml/META.helm-mathql.src b/helm/ocaml/META.helm-mathql.src
index 1985a6be2..fa58fd1ce 100644
--- a/helm/ocaml/META.helm-mathql.src
+++ b/helm/ocaml/META.helm-mathql.src
@@ -1,4 +1,4 @@
-requires="helm-cic_urimanager"
+requires="helm-urimanager"
 version="0.0.1"
 archive(byte)="mathql.cma"
 archive(native)="mathql.cmxa"
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