]> matita.cs.unibo.it Git - helm.git/commitdiff
...
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 28 May 2002 17:56:23 +0000 (17:56 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 28 May 2002 17:56:23 +0000 (17:56 +0000)
helm/ocaml/META.helm-mathql.src
helm/ocaml/mathql/mathQL.ml

index 1985a6be2e134b417b36cdb634c7f1e457bb6a70..fa58fd1ce5a5f6621b327674f9b7a11a130b10a5 100644 (file)
@@ -1,4 +1,4 @@
-requires="helm-cic_urimanager"
+requires="helm-urimanager"
 version="0.0.1"
 archive(byte)="mathql.cma"
 archive(native)="mathql.cmxa"
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