From: Ferruccio Guidi Date: Tue, 18 Jun 2002 17:39:14 +0000 (+0000) Subject: mathQL.ml updated X-Git-Tag: V_0_3_0_debian_8~33 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8adca9e9d6f3b7c605e570dadb4bb82a16b3d050;hp=5568099300dd41b552d5be114b2f2c0b97f3c36c;p=helm.git mathQL.ml updated --- diff --git a/helm/ocaml/mathql/mQueryTParser.mly b/helm/ocaml/mathql/mQueryTParser.mly index 7c715b29d..9bfcd4e0c 100644 --- a/helm/ocaml/mathql/mQueryTParser.mly +++ b/helm/ocaml/mathql/mQueryTParser.mly @@ -92,8 +92,8 @@ | MCONCL { MQMConclusion } | CONCL { MQConclusion } | STR { MQCons $1 } - | rvar { MQSRVar $1 } - | svar { MQSSVar $1 } + | rvar { MQStringRVar $1 } + | svar { MQStringSVar $1 } | func rvar { MQFunc ($1, $2) } ; boole: diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml index 2169564e4..89bd335e1 100644 --- a/helm/ocaml/mathql/mQueryUtil.ml +++ b/helm/ocaml/mathql/mQueryUtil.ml @@ -102,6 +102,8 @@ let out_rvar s = sym s let out_svar s = sep "$" ^ sym s +let out_lvar s = sep "%" ^ sym s + let out_tref r = pat (str_tref r) let out_pat p = out_tref p @@ -134,12 +136,12 @@ let out_func = function | MQModified -> key "modified" let out_str = function - | MQCons s -> str s - | MQSRVar s -> out_rvar s - | MQSSVar s -> out_svar s - | MQFunc (f, r) -> out_func f ^ out_rvar r - | MQMConclusion -> key "mainconclusion" - | MQConclusion -> key "inconclusion" + | MQCons s -> str s + | MQStringRVar s -> out_rvar s + | MQStringSVar s -> out_svar s + | MQFunc (f, r) -> out_func f ^ out_rvar r + | MQMConclusion -> key "mainconclusion" + | MQConclusion -> key "inconclusion" let rec out_bool = function | MQTrue -> key "true" @@ -160,8 +162,12 @@ and out_list = function | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ sub "union" ^ out_list l2 ^ sep ")" | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ sub "intersect" ^ out_list l2 ^ sep ")" | MQDiff (l1, l2) -> sep "(" ^ out_list l1 ^ sub "diff" ^ out_list l2 ^ sep ")" - | MQLRVar s -> out_rvar s + | MQListRVar v -> out_rvar v | MQSortedBy (l, o, f) -> sep "(" ^ out_list l ^ sub "sortedby" ^ out_func f ^ out_order o ^ sep ")" + | MQListLVar v -> out_lvar v + | MQLetIn (v, l1, l2) -> key "let" ^ out_lvar v ^ sub "be" ^ out_list l1 ^ sub "in" ^ out_list l2 + | MQReference s -> key "reference" ^ str s + | MQMinimize l -> key "minimize" ^ out_list l let out_query = function | MQList l -> out_list l diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml index 4ef51add5..90d17c553 100644 --- a/helm/ocaml/mathql/mathQL.ml +++ b/helm/ocaml/mathql/mathQL.ml @@ -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 diff --git a/helm/ocaml/mathql_interpreter/mqint.ml b/helm/ocaml/mathql_interpreter/mqint.ml index 611fdf388..34cfc0986 100644 --- a/helm/ocaml/mathql_interpreter/mqint.ml +++ b/helm/ocaml/mathql_interpreter/mqint.ml @@ -84,7 +84,7 @@ let rec execute_ex env = sortedby_ex (execute_ex env l) o f | MQIntersect (l1, l2) -> intersect_ex (execute_ex env l1) (execute_ex env l2) - | MQLRVar rvar -> [List.assoc rvar env] + | MQListRVar rvar -> [List.assoc rvar env] | MQLetIn (lvar, l1, l2) -> let t = Unix.time () in let res = @@ -97,8 +97,8 @@ let rec execute_ex env = print_endline (string_of_float (Unix.time () -. t) ^ "s") ; flush stdout ; res - | MQLetRef rvar -> - letref_ex rvar + | MQListLVar lvar -> + letref_ex lvar ;; (* Let's initialize the execute in Select, creating a cyclical recursion *) diff --git a/helm/ocaml/mathql_interpreter/select.ml b/helm/ocaml/mathql_interpreter/select.ml index 772f6964e..c9680f6c3 100644 --- a/helm/ocaml/mathql_interpreter/select.ml +++ b/helm/ocaml/mathql_interpreter/select.ml @@ -48,10 +48,10 @@ let stringeval env = | MQFunc (f, rvar) -> let {S.uri = uri} = List.assoc rvar env in apply_func f uri - | MQSRVar rvar -> + | MQStringRVar rvar -> let {S.uri = uri} = List.assoc rvar env in uri - | MQSSVar svar -> + | MQStringSVar svar -> let (_,{S.attributes = attributes}) = List.hd env in List.assoc svar attributes | MQMConclusion ->