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

diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml
index d102e7301..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,34 +41,36 @@ 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 *)
-   | MQTheory
-   | MQTitle
+   | MQName         (* Name *)
+   | MQTheory       (* theory *)
+   | MQTitle        (* DC properties *)
    | MQContributor
    | MQCreator
    | MQPublisher
@@ -85,44 +87,44 @@ type mqfunc =
    | MQRights
    | MQInstitution
    | MQContact
-   | MQFirstVersion
+   | MQFirstVersion 
    | MQModified
 
 type mqstring =
-   | MQCons of string                       (* constant *)
-   | MQFunc of mqfunc * mqrvar              (* function, rvar *)
-   | MQSRVar of mqrvar                      (* rvar *)
-   | MQSSVar 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
-   | MQDesc
+   | 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                   *)
-   | 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. *)
+   | 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 =
-   | 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 (*  *)
-   | MQLRVar of mqrvar
-   | MQDiff of mqlist * 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
@@ -130,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