X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql%2FmQueryUtil.ml;h=22d1f91e5d27bf53d0920840063e62f2408f745e;hb=c172220b965a4d0e95004ae42911a886faac878c;hp=c5a8382fec9d3ce0a537900833c32cae736abce4;hpb=6c04191a9045120d3cf5f6046eee627d6499e5c9;p=helm.git diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml index c5a8382fe..22d1f91e5 100644 --- a/helm/ocaml/mathql/mQueryUtil.ml +++ b/helm/ocaml/mathql/mQueryUtil.ml @@ -23,133 +23,57 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 30/04/2002 *) -(* *) -(* *) -(******************************************************************************) - -open MathQL - -(* string linearization of a reference *) - -let str_btoken = function - | MQBC s -> s - | MQBD -> "/" - | MQBQ -> "?" - | MQBS -> "*" - | MQBSS -> "**" - -let str_ftoken = function - | MQFC i -> "/" ^ string_of_int i - | MQFS -> "/*" - | MQFSS -> "/**" - -let str_prot = function - | Some s -> s - | None -> "*" - -let rec str_body = function - | [] -> "" - | head :: tail -> str_btoken head ^ str_body tail - -let str_frag l = - let rec str_fi start = function - | [] -> "" - | t :: l -> - (if start then "#1" else "") ^ str_ftoken t ^ str_fi false l - in str_fi true l - -let str_tref (p, b, i) = - str_prot p ^ ":/" ^ str_body b ^ str_frag i - -let str_uref (u, i) = - let rec str_fi start = function - | [] -> "" - | i :: l -> - (if start then "#1" else "") ^ string_of_int i ^ str_fi false l - in UriManager.string_of_uri u ^ str_fi true i - -(* raw HTML representation *) - -let key s = "" ^ s ^ " " - -let sym s = s ^ " " - -let sep s = s - -let str s = "'" ^ s ^ "' " - -let pat s = "\"" ^ s ^ "\" " - -let res s = "\"" ^ s ^ "\" " - -let nl () = "
" - -let par () = "

" - -(* HTML representation of a query *) - -let out_rvar s = sym s - -let out_svar s = sep "$" ^ sym s - -let out_tref r = pat (str_tref r) - -let out_pat p = out_tref p +(* AUTOR: Ferruccio Guidi + *) -let out_func = function - | MQName -> key "name" +(* time handling ***********************************************************) -let out_str = function - | MQCons s -> str s - | MQRVar s -> out_rvar s - | MQSVar s -> out_svar s - | MQFunc (f, r) -> out_func f ^ out_rvar r - | MQMConclusion -> key "mainconclusion" - | MQConclusion -> key "conclusion" +type time = float * float -let rec out_bool = function - | MQTrue -> key "true" - | MQFalse -> key "false" - | MQIs (s, t) -> out_str s ^ key "is" ^ out_str t - | MQNot b -> key "not" ^ out_bool b - | MQAnd (b1, b2) -> sep "(" ^ out_bool b1 ^ key "and" ^ out_bool b2 ^ sep ")" - | MQOr (b1, b2) -> sep "(" ^ out_bool b1 ^ key "or" ^ out_bool b2 ^ sep ")" +let start_time () = + (Sys.time (), Unix.time ()) -let rec out_list = function - | MQSelect (r, l, b) -> - key "select" ^ out_rvar r ^ key "in" ^ out_list l ^ key "where" ^ out_bool b - | MQUse (l, v) -> key "use" ^ out_list l ^ key "position" ^ out_svar v - | MQUsedBy (l, v) -> key "usedby" ^ out_list l ^ key "position" ^ out_svar v - | MQPattern p -> key "pattern" ^ out_pat p - | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")" - | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")" - -let out_query = function - | MQList l -> out_list l - -(* HTML representation of a query result *) - -let rec out_list = function - | [] -> "" - | u :: l -> res u ^ nl () ^ out_list l - -let out_result qr = - par () ^ "Result:" ^ nl () ^ - match qr with - | MQRefs l -> out_list l - -(* Converting functions *) - -let tref_uref u = - let s = str_uref u in - MQueryTParser.ref MQueryTLexer.rtoken (Lexing.from_string s) - -let parse_text ch = - let lexbuf = Lexing.from_channel ch in - MQueryTParser.query MQueryTLexer.qtoken lexbuf +let stop_time (s0, u0) = + let s1 = Sys.time () in + let u1 = Unix.time () in + Printf.sprintf "%.2fs,%.2fs" (s1 -. s0) (u1 -. u0) + +(* operations on lists *****************************************************) + +type 'a comparison = Lt + | Gt + | Eq of 'a + +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 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 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