X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql%2FmQueryUtil.ml;h=22d1f91e5d27bf53d0920840063e62f2408f745e;hb=605740107642920d90d0c88544d576d7836a1a25;hp=0cf8ebe087653b2d4365c0e33628fafa7a1049eb;hpb=dec50888f98015c937283acc14e2ffceccc04a11;p=helm.git diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml index 0cf8ebe08..22d1f91e5 100644 --- a/helm/ocaml/mathql/mQueryUtil.ml +++ b/helm/ocaml/mathql/mQueryUtil.ml @@ -23,204 +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 xpointer f l = - let sfi = List.fold_left (fun l0 t0 -> l0 ^ "/" ^ f t0) "" l in - if sfi = "" then "" else - if xpointer then "#xpointer(1" ^ sfi ^ ")" else - "#1" ^ sfi - -let str_tref (p, b, i) = - str_prot p ^ ":/" ^ str_body b ^ str_frag false str_ftoken i - -let xp_str_tref (p, b, i) = - str_prot p ^ ":/" ^ str_body b ^ str_frag true str_ftoken i - -let str_uref (u, i) = - UriManager.string_of_uri u ^ str_frag false string_of_int i - -let xp_str_uref (u, i) = - UriManager.string_of_uri u ^ str_frag true string_of_int i - -(* raw HTML representation *) - -let key s = "" ^ s ^ " " - -let sub s = " " ^ s ^ " " - -let sub2 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_lvar s = sep "%" ^ sym s - -let out_tref r = pat (str_tref r) - -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" - | MQDesc -> sub2 "desc" - -let out_func = function - | MQName -> key "name" - | MQTheory -> key "theory" - | MQTitle -> key "title" - | MQContributor -> key "contributor" - | MQCreator -> key "creator" - | MQPublisher -> key "publisher" - | MQSubject -> key "subject" - | MQDescription -> key "description" - | MQDate -> key "date" - | MQType -> key "type" - | MQFormat -> key "format" - | MQIdentifier -> key "identifier" - | MQLanguage -> key "language" - | MQRelation -> key "relation" - | MQSource -> key "source" - | MQCoverage -> key "coverage" - | MQRights -> key "rights" - | MQInstitution -> key "institution" - | MQContact -> key "contact" - | MQFirstVersion -> key "firstversion" - | MQModified -> key "modified" - -let out_str = function - | 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" - | MQFalse -> key "false" - | MQIs (s, t) -> out_str s ^ sub "is" ^ out_str t - | MQNot b -> key "not" ^ out_bool b - | MQAnd (b1, b2) -> sep "(" ^ out_bool b1 ^ sub "and" ^ out_bool b2 ^ sep ")" - | MQOr (b1, b2) -> sep "(" ^ out_bool b1 ^ sub "or" ^ out_bool b2 ^ sep ")" - | MQSubset (l1, l2) -> sep "(" ^ out_list l1 ^ sub "subset" ^ out_list l2 ^ sep ")" - | MQSetEqual (l1, l2) -> sep "(" ^ out_list l1 ^ sub "setequal" ^ out_list l2 ^ sep ")" - -and out_list = function - | MQSelect (r, l, b) -> - 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_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 ")" - | 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" ^ out_sequence str s - -let out_query = function - | MQList l -> out_list l - -(* HTML representation of a query result *) - -let rec out_res_list = function - | [] -> "" - | u :: l -> res u ^ nl () ^ out_res_list l - -let out_result qr = - par () ^ "Result:" ^ nl () ^ - match qr with - | MQRefs l -> out_res_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 - -(* 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) +(* AUTOR: Ferruccio Guidi + *) -*) +(* time handling ***********************************************************) + +type time = float * float + +let start_time () = + (Sys.time (), Unix.time ()) + +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