X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fmathql%2FmQueryUtil.ml;h=1051e2a7e63113c0c1b569ea347b09caed804018;hb=a32bcc14672dae13e8bb725e54c819958dfdb677;hp=75e587229f29071c93ca3eb7412809ff93f50898;hpb=856dc227c9781439a31d03f5b68d32a41db63ab9;p=helm.git diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml index 75e587229..1051e2a7e 100644 --- a/helm/ocaml/mathql/mQueryUtil.ml +++ b/helm/ocaml/mathql/mQueryUtil.ml @@ -23,104 +23,83 @@ * 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_str 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 txt_path (p0, p1) = - txt_str p0 ^ (if p1 <> [] then "/" ^ txt_list txt_str "/" p1 else "") +(* operations on lists *****************************************************) -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.RefineExact -> "" - | M.RefineSub -> "sub " - | M.RefineSuper -> "super " - in - let txt_refpath i r p = txt_inv i ^ txt_ref r ^ txt_path p ^ " " in - let rec txt_val = function - | M.Const [s] -> txt_str s - | M.Const l -> "{" ^ txt_list txt_str ", " l ^ "}" - | M.VVar vv -> txt_vvar vv - | M.Record (rv, p) -> txt_rvar rv ^ "." ^ txt_path p - | M.Fun (s, x) -> "fun " ^ txt_str 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_str ", " 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 +type 'a comparison = Lt + | Gt + | Eq of 'a -let text_of_result x sep = - let txt_attr = function - | (p, []) -> txt_path p - | (p, l) -> txt_path p ^ " = " ^ txt_list txt_str ", " l - in - let txt_group l = "{" ^ txt_list txt_attr "; " l ^ "}" in - let txt_res = function - | (s, []) -> txt_str s - | (s, l) -> txt_str s ^ " attr " ^ txt_list txt_group ", " l - in - let txt_set l = txt_list txt_res ("; " ^ sep) l ^ sep in - txt_set x +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 query_of_text lexbuf = - MQueryTParser.query MQueryTLexer.query_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) -let result_of_text lexbuf = - MQueryTParser.result MQueryTLexer.result_token lexbuf +let rec flat_list out f s = function + | [] -> () + | [a] -> f a + | a :: tail -> f a; out s; flat_list out f s tail + +let rec add_assoc ap = function + | [] -> [ap] + | head :: tail when fst head = fst ap -> ap :: tail + | head :: tail -> head :: add_assoc ap tail -(* conversion functions *****************************************************) +(* int of string ************************************************************) -type uriref = UriManager.uri * (int list) +type t = End + | Space + | Figure of int + | Error -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 int_of_string s = + let l = String.length s in + let get_t i = + if i = l then End else + match s.[i] with + | ' ' | '\t' | '\r' | 'n' -> Space + | '0' .. '9' -> Figure (Char.code s.[i] - Char.code '0') + | _ -> Error + in + let rec aux i xv = match get_t i, xv with + | Error, _ + | End, None -> raise (Failure "int_of_string") + | End, Some v -> v + | Space, xv -> aux (succ i) xv + | Figure f, None -> aux (succ i) (Some f) + | Figure f, Some v -> aux (succ i) (Some (10 * v + f)) + in + aux 0 None