X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql%2FmathQL.ml;h=d18ebbc9243afa5d1fc3b87e8718cc68aaf83116;hb=1d2bd140d14561951f8214edf15abe4f40dcb649;hp=d1e89decf9a25f4f7582da4d162bdab11e574be1;hpb=6c04191a9045120d3cf5f6046eee627d6499e5c9;p=helm.git

diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml
index d1e89decf..d18ebbc92 100644
--- a/helm/ocaml/mathql/mathQL.ml
+++ b/helm/ocaml/mathql/mathQL.ml
@@ -20,7 +20,7 @@
  * MA  02111-1307, USA.
  * 
  * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
+ * http://www.cs.unibo.it/helm/.
  *)
 
 (******************************************************************************)
@@ -41,56 +41,90 @@ exception MQInvalidConnection of string
 (* Input types **************************************************************)
 (* main type is mquery                                                      *)
 
-type mqrvar = string                       (* name *)
+type mqrvar = string (* name *)
 
-type mqsvar = string                       (* name *)
+type mqsvar = string (* name *)
 
-type mqpt = string option                  (* PROTOCOL TOKENS *)
-                                           (* Some = constant string *)
-					   (* None = single star: '*' *)
+type mqlvar = string (* name *)
 
-type mqbt =                                (* BODY TOKENS *)
-   | MQBC of string                        (* a constant string *)
-   | MQBD                                  (* a slash: '/' *)
-   | MQBQ                                  (* a question mark: '?' *)
-   | MQBS                                  (* a single star: '*' *)
-   | MQBSS                                 (* a double star: '**' *)
+type mqpt = string option (* PROTOCOL TOKENS *)
+                          (* Some = constant string *)
+                          (* None = single star: '*' *)
 
-type mqft =                                (* FRAGMENT TOKENS *)
-   | MQFC of int                           (* a constant integer *)
-   | MQFS                                  (* a single star: '*' *)
-   | MQFSS                                 (* a double star: '**' *)
+type mqbt =               (* BODY TOKENS *)
+   | MQBC of string       (* a constant string *)
+   | MQBD                 (* a slash: '/' *)
+   | MQBQ                 (* a question mark: '?' *)
+   | MQBS                 (* a single star: '*' *)
+   | MQBSS                (* a double star: '**' *)
 
-type mqtref = mqpt * (mqbt list) * (mqft list) (* tokenized reference *)
+type mqft =               (* FRAGMENT TOKENS *)
+   | MQFC of int          (* a constant integer *)
+   | MQFS                 (* a single star: '*' *)
+   | MQFSS                (* a double star: '**' *)
 
-type mqpattern = mqtref                     (* constant pattern *)
+type mquref = UriManager.uri * (int list) (* uri, fragment identifier *)
+
+type mqtref = mqpt * (mqbt list) * (mqft list) (* tokenized pattern reference *)
 
 type mqfunc =
-   | MQName                                 (* NAME *)
+   | MQName         (* Name *)
+   | MQTheory       (* theory *)
+   | MQTitle        (* DC properties *)
+   | MQContributor
+   | MQCreator
+   | MQPublisher
+   | MQSubject
+   | MQDescription
+   | MQDate
+   | MQType
+   | MQFormat
+   | MQIdentifier
+   | MQLanguage
+   | MQRelation
+   | MQSource
+   | MQCoverage
+   | MQRights
+   | MQInstitution
+   | MQContact
+   | MQFirstVersion 
+   | MQModified
 
 type mqstring =
-   | MQCons of string                       (* constant *)
-   | MQFunc of mqfunc * mqrvar              (* function, rvar *)
-   | MQRVar of mqrvar                       (* rvar *)
-   | MQSVar of mqsvar                       (* svar *)
-   | MQMConclusion                          (* main conclusion *)
-   | MQConclusion                           (* inner conclusion *)
+   | MQCons of string          (* constant *)
+   | MQFunc of mqfunc * mqrvar (* function, rvar *)
+   | MQStringRVar of mqrvar    (* rvar *)
+   | MQStringSVar of mqsvar    (* svar *)
+   | MQMConclusion             (* main conclusion *)
+   | MQConclusion              (* inner conclusion *)
+
+type mqorder =
+   | MQAsc     (* ascending order *)
+   | MQDesc    (* descending order *)
 
 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 *)
+   | MQTrue                        (* true *)
+   | MQFalse                       (* false *)
+   | MQAnd of mqbool * mqbool      (* conjunction *)
+   | MQOr of mqbool * mqbool       (* disjunction *)
+   | MQNot of mqbool               (* negation *)
+   | MQIs of mqstring * mqstring   (* case-sensitive comparison  *)
+   | MQSetEqual of mqlist * mqlist (* the two lists denote the same set *)
+   | MQSubset of mqlist * mqlist   (* the two lists denote two sets, the 1st subset of the 2nd *)
+
+and mqlist =
+   | MQReference of string list              (* reference list *)
+   | MQPattern of mqtref                     (* pattern *)
+   | MQListLVar of mqlvar                    (* lvar *)
+   | MQListRVar of mqrvar                    (* rvar *)
+   | MQSelect of mqrvar * mqlist * mqbool    (* rvar, list, boolean *) 
+   | MQUse of mqlist * mqsvar                (* list, Position attribute *)
+   | MQUsedBy of mqlist * mqsvar             (* list, Position attribute *)
+   | MQUnion of mqlist * mqlist              (* operands *)
+   | MQIntersect of mqlist * mqlist          (* operands *)
+   | MQSortedBy of mqlist * mqorder * mqfunc (* ordering *)
+   | MQDiff of mqlist * mqlist               (* set difference  *)
+   | MQLetIn of mqlvar * mqlist * mqlist     (* explicit lvar assignment *)
 
 type mquery =
    | MQList of mqlist
@@ -98,10 +132,5 @@ type mquery =
 (* Output types *************************************************************)
 (* main type is mqresult                                                    *)
 
-(* TODO: usare le uri in questo formato *)
-type mquref = UriManager.uri * (int list)   (* uri, fragment identifier *)
-
-type mqrefs = string list                   (* list of references (helper) *)
-
 type mqresult =
-   | MQRefs of mqrefs
+   | MQRefs of string list