From: Ferruccio Guidi Date: Wed, 4 Feb 2004 18:45:54 +0000 (+0000) Subject: optimized and patched X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=ad4c175433641f3b6668971bb7b3498c31390e0e optimized and patched --- diff --git a/helm/ocaml/mathql_interpreter/mQILib.ml b/helm/ocaml/mathql_interpreter/mQILib.ml index a474857c5..312e806cd 100644 --- a/helm/ocaml/mathql_interpreter/mQILib.ml +++ b/helm/ocaml/mathql_interpreter/mQILib.ml @@ -41,8 +41,9 @@ type eval_spec = {eval : M.query -> M.result; } type text_out_spec = {out : string -> unit; + sep : string; path : (string -> unit) -> M.path -> unit; - query : (string -> unit) -> string -> M.query -> unit; + query : (string -> unit) -> string -> M.query -> unit; result : (string -> unit) -> string -> M.result -> unit } @@ -82,7 +83,7 @@ let check_arity p i = function let std o = {s_out = o.out; s_path = o.path o.out; - s_query = o.query o.out ""; s_result = o.result o.out "\n" + s_query = o.query o.out o.sep; s_result = o.result o.out o.sep } let out_txt2 o n x1 x2 = diff --git a/helm/ocaml/mathql_interpreter/mQILib.mli b/helm/ocaml/mathql_interpreter/mQILib.mli index bfac2b4ff..a8de33743 100644 --- a/helm/ocaml/mathql_interpreter/mQILib.mli +++ b/helm/ocaml/mathql_interpreter/mQILib.mli @@ -35,6 +35,7 @@ type eval_spec = {eval : MathQL.query -> MathQL.result; } type text_out_spec = {out : string -> unit; + sep : string; path : (string -> unit) -> MathQL.path -> unit; query : (string -> unit) -> string -> MathQL.query -> unit; result : (string -> unit) -> string -> MathQL.result -> unit diff --git a/helm/ocaml/mathql_interpreter/mQIProperty.ml b/helm/ocaml/mathql_interpreter/mQIProperty.ml index 357809a74..1e634d7c1 100644 --- a/helm/ocaml/mathql_interpreter/mQIProperty.ml +++ b/helm/ocaml/mathql_interpreter/mQIProperty.ml @@ -100,7 +100,7 @@ let pg_query h table cols ct cfl = | _ -> [] else exec ("select " ^ pg_cols ^ " from " ^ table ^ pg_where ^ - " order by " ^ List.hd cols ^ " asc") + " order by " ^ List.hd cols ^ " asc") (* desc *) (* Galax backend ***********************************************************) @@ -108,10 +108,7 @@ let gx_query h table cols ct cfl = not_supported "Galax" (* Common functions ********************************************************) -let pg_result distinct subj el res = - let res, compose = - if distinct then List.rev res, U.append_iter else res, U.iter - in +let pg_result subj el res = let get_name = function (p, None) -> p | (_, Some p) -> p in let names = List.map get_name el in let mk_grp l = U.grp_iter2 I.grp_make names l in @@ -119,7 +116,7 @@ let pg_result distinct subj el res = if subj = "" then I.make "" (mk_grp l) else I.make (List.hd l) (mk_grp (List.tl l)) in - compose mk_avs res + U.iter mk_avs res let get_table h mc ct cfl el = let aux_c ts (_, p, _) = A.refine_tables ts (C.tables h p) in @@ -139,7 +136,7 @@ let exec_single h mc ct cfl el table = let cols = if first = "" then other_cols else first :: other_cols in let low_level = if C.set h C.Galax then gx_query else pg_query in let result = low_level h (C.resolve h table) cols cons_true cons_false in - pg_result false first el result + pg_result first el result let deadline = 100 diff --git a/helm/ocaml/mathql_interpreter/mQueryIO.ml b/helm/ocaml/mathql_interpreter/mQueryIO.ml index 14199e513..e99dc0d72 100644 --- a/helm/ocaml/mathql_interpreter/mQueryIO.ml +++ b/helm/ocaml/mathql_interpreter/mQueryIO.ml @@ -55,18 +55,20 @@ let txt_path out p = out "/"; P.flat_list out (txt_str out) "/" p let text_of_result out sep x = let txt_attr _ p l b = txt_path out p; - if l <> [] then begin - out " = "; P.flat_list out (txt_str out) ", " l + begin match l with + | [] -> () + | [s] -> out " = "; txt_str out s + | l -> out " = {"; P.flat_list out (txt_str out) ", " l; out "}" end; - if b then out ("; " ^ sep) + if b then out ("; ") in let txt_group l = out "{"; I.x_grp_iter txt_attr () l; out "}" in let txt_res _ s l b = txt_str out s; if l <> [] then begin - out " = "; P.flat_list out txt_group ", " l + out " attr "; P.flat_list out txt_group ", " l end; - if b then out "; " + if b then out ("; " ^ sep) in I.x_iter txt_res () x; out sep @@ -124,7 +126,7 @@ and text_of_query out sep x = | M.From av -> txt_avar av and txt_set = function | M.Fun (p, pl, xl) -> - let o = {L.out = out; L.path = txt_path; + let o = {L.out = out; L.sep = ""; L.path = txt_path; L.query = text_of_query; L.result = text_of_result } in @@ -158,7 +160,7 @@ and text_of_query out sep x = txt_set x; out sep let text_out_spec out sep = - {L.out = out; L.path = txt_path; + {L.out = out; L.sep = sep; L.path = txt_path; L.query = text_of_query; L.result = text_of_result } diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml index cc85c7811..57e1207bc 100644 --- a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml +++ b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml @@ -62,7 +62,9 @@ let execute h x = let rec eval_query c = function | M.Const r -> let aux2 s g = I.make s (eval_list c g) in - let aux (s, gl) = U.iter (aux2 s) gl in + let aux (s, gl) = + if gl = [] then U.avs_of_string s else U.iter (aux2 s) gl + in c, U.iter aux r | M.Dot (i, p) -> begin @@ -116,7 +118,7 @@ let execute h x = d, f r s in let d, r = eval_query c x1 in - I.x_iter for_aux (d, I.empty) r + I.x_iter for_aux (d, I.empty) (I.optimize r) | M.While (k, x1, x2) -> let f = match k with | M.GenFJoin -> I.union @@ -133,10 +135,10 @@ let execute h x = let f = if b then I.d_union else I.union in let agl = eval_grp c z in let aux r sj gl _ = - I.append (f (U.make_x sj gl) (U.make_x sj agl)) r + I.union r (f (U.make_x sj gl) (U.make_x sj agl)) in let _, r = eval_query c x in - c, I.x_iter aux I.empty r + c, I.x_iter aux I.empty (I.optimize r) | M.Property (q0, q1, q2, mc, ct, cfl, el, pat, y) -> let _, r = eval_query c y in let subj, mct = @@ -159,10 +161,10 @@ let execute h x = let aux (d, r) sj gl _ = let d = {d with avars = P.add_assoc (i, (sj, gl)) d.avars} in let d, s = eval_query d y in - if s = U.val_false then d, r else d, (I.append (U.make_x sj gl) r) + if s = U.val_false then d, r else d, (I.union r (U.make_x sj gl)) in let d, r = eval_query c x in - I.x_iter aux (d, I.empty) r + I.x_iter aux (d, I.empty) (I.optimize r) | M.Fun (p, pl, xl) -> let e = {L.eval = (fun x -> snd (eval_query c x)); L.conn = h} in c, L.fun_eval e (F.text_out_spec (C.log h) "\n") F.text_in_spec diff --git a/helm/ocaml/mathql_interpreter/mQueryStandard.ml b/helm/ocaml/mathql_interpreter/mQueryStandard.ml index 858c28fa0..85a7ffe40 100644 --- a/helm/ocaml/mathql_interpreter/mQueryStandard.ml +++ b/helm/ocaml/mathql_interpreter/mQueryStandard.ml @@ -198,7 +198,7 @@ let render_fun = | [x] -> let rs = ref "" in let out s = rs := ! rs ^ s in - o.L.result out " " (e.L.eval x); + o.L.result out "" (e.L.eval x); I.make ! rs I.grp_empty | _ -> assert false in @@ -240,13 +240,13 @@ let align_fun = let c = String.length v in if c < l then String.make (l - c) ' ' ^ v else v in - let aux l r s gl _ = I.append r (U.make_x (aux2 l s) gl) in + let aux l r s gl _ = I.union r (U.make_x (aux2 l s) gl) in let arity_p = L.Const 0 in let arity_s = L.Const 2 in let body e _ _ _ = function | [y; x] -> let l = U.int_of_avs (e.L.eval y) in - I.x_iter (aux l) I.empty (e.L.eval x) + I.x_iter (aux l) I.empty (I.optimize (e.L.eval x)) | _ -> assert false in let txt_out o _ = function @@ -381,10 +381,12 @@ let _ = L.fun_register ["proj"] proj_fun let keep_fun b = let aux2 s l a q v _ = - if List.mem q l = b then a else I.union a (I.make s (U.grp_make_x q v)) + I.union a (I.make s + (if List.mem q l = b then I.grp_empty else U.grp_make_x q v) + ) in let aux l a s gl _ = - I.append a ( + I.union a ( if l = [] then I.make s I.grp_empty else U.iter (I.x_grp_iter (aux2 s l) I.empty) gl) in @@ -394,9 +396,9 @@ let keep_fun b = let arity_s = L.Const 1 in let body e _ _ pl xl = match b, pl, xl with - | true, [], [x] -> e.L.eval x - | _, l, [x] -> I.x_iter (aux l) I.empty (e.L.eval x) - | _ -> assert false + | true, [], [x] -> e.L.eval x + | _, l, [x] -> I.x_iter (aux l) I.empty (I.optimize (e.L.eval x)) + | _ -> assert false in let txt_out o pl xl = match pl, xl with diff --git a/helm/ocaml/mathql_interpreter/mQueryTParser.mly b/helm/ocaml/mathql_interpreter/mQueryTParser.mly index 54f8f837c..c7df0c9ac 100644 --- a/helm/ocaml/mathql_interpreter/mQueryTParser.mly +++ b/helm/ocaml/mathql_interpreter/mQueryTParser.mly @@ -296,8 +296,8 @@ ; attr: - | path BE strs { U.grp_make_x $1 $3 } - | path { U.grp_make_x $1 [] } + | path BE STR { U.grp_make_x $1 [$3] } + | path BE LC strs RC { U.grp_make_x $1 $4 } ; attrs: | attr SC attrs { I.grp_union $1 $3 }