From: Ferruccio Guidi Date: Sat, 22 Jun 2002 17:17:03 +0000 (+0000) Subject: mathQL and mqint updated X-Git-Tag: V_0_3_0_debian_8~22 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3c57d335904d0480f3145ccdcf663206cffd5567;p=helm.git mathQL and mqint updated multiple MQReference and MQPattern added (untested) --- diff --git a/helm/ocaml/mathql/Makefile b/helm/ocaml/mathql/Makefile index 52a5eb155..f9c0eb9d8 100644 --- a/helm/ocaml/mathql/Makefile +++ b/helm/ocaml/mathql/Makefile @@ -4,9 +4,9 @@ PREDICATES = INTERFACE_FILES = mQueryTParser.mli mQueryUtil.mli -IMPLEMENTATION_FILES = mathQL.ml $(INTERFACE_FILES:%.mli=%.ml) \ - mQueryTLexer.ml - +IMPLEMENTATION_FILES = mathQL.ml mQueryTParser.ml mQueryTLexer.ml \ + mQueryUtil.ml + EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi mQueryTLexer.cmi \ mQueryTLexer.mll mQueryTParser.mly diff --git a/helm/ocaml/mathql/mQueryTParser.mly b/helm/ocaml/mathql/mQueryTParser.mly index 9bfcd4e0c..0b375fcfe 100644 --- a/helm/ocaml/mathql/mQueryTParser.mly +++ b/helm/ocaml/mathql/mQueryTParser.mly @@ -106,7 +106,7 @@ | LPR boole RPR { $2 } ; rlist: - | PATT REF { MQPattern $2 } + | PATT REF { MQPattern [$2] } | rlist UNION rlist { MQUnion ($1, $3) } | rlist INTER rlist { MQIntersect ($1, $3) } | USE rlist POS svar { MQUse ($2, $4) } diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml index 89bd335e1..97f94f727 100644 --- a/helm/ocaml/mathql/mQueryUtil.ml +++ b/helm/ocaml/mathql/mQueryUtil.ml @@ -106,7 +106,11 @@ let out_lvar s = sep "%" ^ sym s let out_tref r = pat (str_tref r) -let out_pat p = out_tref p + +let rec out_sequence f = function + | [] -> sep "." + | [s] -> f s + | s :: tail -> f s ^ sep "," ^ out_sequence f tail let out_order = function | MQAsc -> sub2 "asc" @@ -158,7 +162,7 @@ and out_list = function key "select" ^ out_rvar r ^ sub "in" ^ out_list l ^ sub "where" ^ out_bool b | MQUse (l, v) -> key "use" ^ out_list l ^ sub "position" ^ out_svar v | MQUsedBy (l, v) -> key "usedby" ^ out_list l ^ sub "position" ^ out_svar v - | MQPattern p -> key "pattern" ^ out_pat p + | MQPattern p -> key "pattern" ^ out_sequence out_tref p | 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 ")" @@ -166,7 +170,7 @@ and out_list = function | 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 + | MQReference s -> key "reference" ^ out_sequence str s | MQMinimize l -> key "minimize" ^ out_list l let out_query = function @@ -174,14 +178,14 @@ let out_query = function (* HTML representation of a query result *) -let rec out_list = function +let rec out_res_list = function | [] -> "" - | u :: l -> res u ^ nl () ^ out_list l + | u :: l -> res u ^ nl () ^ out_res_list l let out_result qr = par () ^ "Result:" ^ nl () ^ match qr with - | MQRefs l -> out_list l + | MQRefs l -> out_res_list l (* Converting functions *) @@ -192,3 +196,32 @@ let tref_uref u = let parse_text ch = let lexbuf = Lexing.from_channel ch in MQueryTParser.query MQueryTLexer.qtoken lexbuf + +(* implementazione manuale di tref_uref da controllare + +let split s = + try + let i = Str.search_forward (Str.regexp_string ":/") s 0 in + let p = Str.string_before s i in + let q = Str.string_after s (i + 2) in + (p, q) + with + Not_found -> (s, "") + +let encode = function + | Str.Text s -> MQBC s + | Str.Delim s -> + if s = "?" then MQBQ else + if s = "*" then MQBS else + if s = "**" then MQBSS else + if s = "/" then MQBD else MQBC s + +let tref_uref (u, i) = + let s = UriManager.string_of_uri u in + match split s with + | (p, q) -> + let rx = Str.regexp "\?\|\*\*\|\*\|/" in + let l = Str.full_split rx q in + (Some p, List.map encode l, i) + +*) diff --git a/helm/ocaml/mathql/mQueryUtil.mli b/helm/ocaml/mathql/mQueryUtil.mli index 139cb0181..94126555b 100644 --- a/helm/ocaml/mathql/mQueryUtil.mli +++ b/helm/ocaml/mathql/mQueryUtil.mli @@ -39,6 +39,8 @@ val str_tref : MathQL.mqtref -> string (* string linearization of a tok val out_query : MathQL.mquery -> string (* HTML representation of a query *) +val out_result : MathQL.mqresult -> string (* HTML representation of a query result *) + val tref_uref : MathQL.mquref -> MathQL.mqtref (* "tref of uref" conversion *) val parse_text : in_channel -> MathQL.mquery (* textual parsing of a query *) diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml index 90d17c553..82ab6f9da 100644 --- a/helm/ocaml/mathql/mathQL.ml +++ b/helm/ocaml/mathql/mathQL.ml @@ -115,8 +115,8 @@ type mqbool = | MQSubset of mqlist * mqlist (* the two lists denote two sets, the 1st subset of the 2nd *) and mqlist = - | MQReference of mqref (* reference *) - | MQPattern of mqtref (* pattern *) + | MQReference of mqref list (* reference list *) + | MQPattern of mqtref list (* pattern list *) | MQListLVar of mqlvar (* lvar *) | MQListRVar of mqrvar (* rvar *) | MQSelect of mqrvar * mqlist * mqbool (* rvar, list, boolean *) diff --git a/helm/ocaml/mathql_interpreter/mqint.ml b/helm/ocaml/mathql_interpreter/mqint.ml index 3a0a5fb31..0de53503e 100644 --- a/helm/ocaml/mathql_interpreter/mqint.ml +++ b/helm/ocaml/mathql_interpreter/mqint.ml @@ -38,6 +38,7 @@ open Sortedby;; open Use;; open Select;; open Letin;; +open Mathql_semantics;; let prop_pool = ref None;; @@ -91,6 +92,13 @@ let get_prop_id prop = else List.assoc prop (match !prop_pool with Some l -> l | _ -> assert false) ;; +(* automatically performes the union of a given list of patterns *) +let rec pattern_list_ex = function + | [] -> [] + | [(apreamble, apattern, afragid)] -> pattern_ex (apreamble, apattern, afragid) + | (apreamble, apattern, afragid) :: tail -> + union_ex (pattern_ex (apreamble, apattern, afragid)) (pattern_list_ex tail) + (* execute_ex env q *) (* [env] is the attributed uri environment in which the query [q] *) (* must be evaluated *) @@ -104,8 +112,8 @@ let rec execute_ex env = use_ex (execute_ex env alist) asvar (get_prop_id "refObj") (* "F" (*"refObj"*) *) | MQUse (alist, asvar) -> use_ex (execute_ex env alist) asvar (get_prop_id "backPointer") (* "B" (*"backPointer"*) *) - | MQPattern (apreamble, apattern, afragid) -> - pattern_ex (apreamble, apattern, afragid) + | MQPattern l -> + pattern_list_ex l | MQUnion (l1, l2) -> union_ex (execute_ex env l1) (execute_ex env l2) | MQDiff (l1, l2) -> @@ -130,6 +138,14 @@ let rec execute_ex env = res | MQListLVar lvar -> letref_ex lvar + | MQReference l -> (* FG: *) + let rec build_result = function + | [] -> [] + | s :: tail -> + {uri = s ; attributes = [] ; extra = ""} :: build_result tail + in build_result l + | MQMinimize l -> (* FG: sostituire con l'implementazione vera *) + execute_ex env l ;; (* Let's initialize the execute in Select, creating a cyclical recursion *)