]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql/mathQL.ml
mathQL.ml updated
[helm.git] / helm / ocaml / mathql / mathQL.ml
index 4ef51add54213bd051a8c0683c6503ad8f9a7d0b..90d17c553a76f3cc7e8b93c1a6ffde6ff2a76b8b 100644 (file)
@@ -41,36 +41,38 @@ 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 mqlvar = string                       (* name *)
+type mqlvar = string (* name *)
 
-type mqpt = string option                  (* PROTOCOL TOKENS *)
-                                           (* Some = constant string *)
-                                           (* None = single star: '*' *)
+type mqpt = string option (* PROTOCOL TOKENS *)
+                          (* Some = constant string *)
+                          (* None = single 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 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 mqft =                                (* FRAGMENT TOKENS *)
-   | MQFC of int                           (* a constant integer *)
-   | MQFS                                  (* a single star: '*' *)
-   | MQFSS                                 (* a double star: '**' *)
+type mqft =               (* FRAGMENT TOKENS *)
+   | MQFC of int          (* a constant integer *)
+   | MQFS                 (* a single star: '*' *)
+   | MQFSS                (* a double star: '**' *)
 
-type mqtref = mqpt * (mqbt list) * (mqft list) (* tokenized reference *)
+type mquref = UriManager.uri * (int list) (* uri, fragment identifier *)
 
-type mqpattern = mqtref                     (* constant pattern *)
+type mqtref = mqpt * (mqbt list) * (mqft list) (* tokenized pattern reference *)
+
+type mqref = string (* format for references (helper) *)
 
 type mqfunc =
-   | MQName                                 (* NAME *)
-   | MQTheory
-   | MQTitle
+   | MQName         (* Name *)
+   | MQTheory       (* theory *)
+   | MQTitle        (* DC properties *)
    | MQContributor
    | MQCreator
    | MQPublisher
@@ -87,56 +89,51 @@ 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               (*  *)
-   | MQLetIn of mqrvar * mqlist * mqlist
-   | MQLetRef of mqrvar
-
+   | MQReference of mqref                    (* reference *)
+   | 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 *)
+   | MQMinimize of mqlist                    (* list minimization *)
+   
 type mquery =
    | MQList of mqlist
    
 (* Output types *************************************************************)
 (* main type is mqresult                                                    *)
 
-type mquref = UriManager.uri * (int list)   (* uri, fragment identifier *)
-
-type mqrefs = string list                   (* list of references (helper) *)
-
 type mqresult =
-   | MQRefs of mqrefs
+   | MQRefs of mqref list