X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql%2FmQueryUtil.ml;h=22d1f91e5d27bf53d0920840063e62f2408f745e;hb=c172220b965a4d0e95004ae42911a886faac878c;hp=09759cc4536dfd8962ae825de25c9375c998895c;hpb=e5c9ea9efcc95afee3be91e8beb754c0cb4301dc;p=helm.git diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml index 09759cc45..22d1f91e5 100644 --- a/helm/ocaml/mathql/mQueryUtil.ml +++ b/helm/ocaml/mathql/mQueryUtil.ml @@ -23,101 +23,57 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 30/04/2002 *) -(* *) -(* *) -(******************************************************************************) +(* AUTOR: Ferruccio Guidi + *) +(* time handling ***********************************************************) -(* text linearization and parsing *******************************************) +type time = float * float -let rec txt_list f s = function - | [] -> "" - | [a] -> f a - | a :: tail -> f a ^ s ^ txt_list f s tail +let start_time () = + (Sys.time (), Unix.time ()) -let txt_qstr s = "\"" ^ s ^ "\"" +let stop_time (s0, u0) = + let s1 = Sys.time () in + let u1 = Unix.time () in + Printf.sprintf "%.2fs,%.2fs" (s1 -. s0) (u1 -. u0) -let text_of_query x = - let module M = MathQL in - let txt_svar sv = "%" ^ sv in - let txt_rvar rv = "@" ^ rv in - let txt_vvar vv = "$" ^ vv in - let txt_inv i = if i then "inverse " else "" in - let txt_ref = function - | M.ExactOp -> "" - | M.SubOp -> "sub " - | M.SuperOp -> "super " - in - let txt_refpath i r p = txt_inv i ^ txt_ref r ^ txt_list txt_qstr "/" p ^ " " in - let rec txt_val = function - | M.Const [s] -> txt_qstr s - | M.Const l -> "{" ^ txt_list txt_qstr ", " l ^ "}" - | M.VVar vv -> txt_vvar vv - | M.Record (rv, vv) -> txt_rvar rv ^ "." ^ txt_vvar vv - | M.Fun (s, x) -> "fun " ^ txt_qstr s ^ " " ^ txt_val x - | M.Attribute (i, r, p, x) -> "attribute " ^ txt_refpath i r p ^ txt_val x - | M.RefOf x -> "refof " ^ txt_set x - and txt_boole = function - | M.False -> "false" - | M.True -> "true" - | M.Ex b x -> "ex " ^ txt_boole x -(* | M.Ex b x -> "ex [" ^ txt_list txt_rvar "," b ^ "] " ^ txt_boole x -*) | M.Not x -> "not " ^ txt_boole x - | M.And (x, y) -> "(" ^ txt_boole x ^ " and " ^ txt_boole y ^ ")" - | M.Or (x, y) -> "(" ^ txt_boole x ^ " or " ^ txt_boole y ^ ")" - | M.Sub (x, y) -> "(" ^ txt_val x ^ " sub " ^ txt_val y ^ ")" - | M.Meet (x, y) -> "(" ^ txt_val x ^ " meet " ^ txt_val y ^ ")" - | M.Eq (x, y) -> "(" ^ txt_val x ^ " eq " ^ txt_val y ^ ")" - and txt_set = function - | M.SVar sv -> txt_svar sv - | M.RVar rv -> txt_rvar rv - | M.Relation (i, r, p, x, []) -> "relation " ^ txt_refpath i r p ^ txt_set x - | M.Relation (i, r, p, x, l) -> "relation " ^ txt_refpath i r p ^ txt_set x ^ " attr " ^ txt_list txt_vvar ", " l - | M.Union (x, y) -> "(" ^ txt_set x ^ " union " ^ txt_set y ^ ")" - | M.Intersect (x, y) -> "(" ^ txt_set x ^ " intersect " ^ txt_set y ^ ")" - | M.Diff (x, y) -> "(" ^ txt_set x ^ " diff " ^ txt_set y ^ ")" - | M.LetSVar (sv, x, y) -> "let " ^ txt_svar sv ^ " be " ^ txt_set x ^ " in " ^ txt_set y - | M.LetVVar (vv, x, y) -> "let " ^ txt_vvar vv ^ " be " ^ txt_val x ^ " in " ^ txt_set y - | M.Select (rv, x, y) -> "select " ^ txt_rvar rv ^ " in " ^ txt_set x ^ " where " ^ txt_boole y - | M.Pattern x -> "pattern " ^ txt_val x - | M.Ref x -> "ref " ^ txt_val x - in - txt_set x +(* operations on lists *****************************************************) -let text_of_result x sep = - let txt_attr = function - | (s, []) -> txt_qstr s - | (s, l) -> txt_qstr s ^ "=" ^ txt_list txt_qstr ", " l - in - let txt_group l = "{" ^ txt_list txt_attr "; " l ^ "}" in - let txt_res = function - | (s, []) -> txt_qstr s - | (s, l) -> txt_qstr s ^ " attr " ^ txt_list txt_group ", " l - in - let txt_set l = txt_list txt_res ("; " ^ sep) l ^ sep in - txt_set x +type 'a comparison = Lt + | Gt + | Eq of 'a -let query_of_text lexbuf = - MQueryTParser.query MQueryTLexer.query_token lexbuf +let list_join f l1 l2 = + let rec aux = function + | [], v + | v, [] -> v + | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin + match f h1 h2 with + | Lt -> h1 :: aux (t1, v2) + | Gt -> h2 :: aux (v1, t2) + | Eq h -> h :: aux (t1, t2) + end + in aux (l1, l2) -let result_of_text lexbuf = - MQueryTParser.result MQueryTLexer.result_token lexbuf +let list_meet f l1 l2 = + let rec aux = function + | [], v + | v, [] -> [] + | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin + match f h1 h2 with + | Lt -> aux (t1, v2) + | Gt -> aux (v1, t2) + | Eq h -> h :: aux (t1, t2) + end + in aux (l1, l2) -(* conversion functions *****************************************************) - -type uriref = UriManager.uri * (int list) +let rec flat_list out f s = function + | [] -> () + | [a] -> f a + | a :: tail -> f a; out s; flat_list out f s tail -let string_of_uriref (uri, fi) = - let module UM = UriManager in - let str = UM.string_of_uri uri in - let xp t = "#xpointer(1/" ^ string_of_int (t + 1) in - match fi with - | [] -> str - | [t] -> str ^ xp t ^ ")" - | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")" +let rec add_assoc ap = function + | [] -> [ap] + | head :: tail when fst head = fst ap -> ap :: tail + | head :: tail -> head :: add_assoc ap tail