From: Ferruccio Guidi Date: Sat, 31 May 2003 18:59:06 +0000 (+0000) Subject: new syntax for "property" enabled: X-Git-Tag: V7_3_new_exportation_merged~30 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=99bd3d38d021bb5c618883e8a484891f227082c3;p=helm.git new syntax for "property" enabled: now many "isfalse" clauses are accepted --- diff --git a/helm/ocaml/mathql_interpreter/mQIExecute.ml b/helm/ocaml/mathql_interpreter/mQIExecute.ml index 2f5ca7eb6..efb8feb1c 100644 --- a/helm/ocaml/mathql_interpreter/mQIExecute.ml +++ b/helm/ocaml/mathql_interpreter/mQIExecute.ml @@ -187,7 +187,7 @@ let execute out m x = let f = if b then U.mql_prod else U.set_union in let g a s = (fst a, f (snd a) (eval_grp c z)) :: s in List.fold_right g (eval_query c x) [] - | M.Property q0 q1 q2 mc ct cf el pat y -> + | M.Property q0 q1 q2 mc ct cfl el pat y -> let subj, mct = if q0 then [], (pat, q2 @ mc, eval_val c y) else (q2 @ mc), (pat, [], eval_val c y) @@ -197,7 +197,7 @@ let execute out m x = in let eval_cons (pat, p, y) = (pat, q2 @ p, eval_val c y) in let cons_true = mct :: List.map eval_cons ct in - let cons_false = List.map eval_cons cf in + let cons_false = List.map (List.map eval_cons) cfl in let eval_exp (p, po) = (q2 @ p, po) in let exp = List.map eval_exp el in let t = U.start_time () in diff --git a/helm/ocaml/mathql_interpreter/mQIProperty.ml b/helm/ocaml/mathql_interpreter/mQIProperty.ml index c30c18d47..56a9d6421 100644 --- a/helm/ocaml/mathql_interpreter/mQIProperty.ml +++ b/helm/ocaml/mathql_interpreter/mQIProperty.ml @@ -51,7 +51,7 @@ let cl_print l = (* PostgreSQL backend ******************************************************) -let pg_query table cols ct cf = +let pg_query table cols ct cfl = let rec iter f sep = function | [] -> "" | [head] -> f head @@ -62,17 +62,20 @@ let pg_query table cols ct cf = let pg_con (pat, col, v) = if col <> "" then let f s = col ^ " ~ " ^ P.quote ("^" ^ s ^ "$") in - if pat then "(" ^ iter f " or " v ^ ")" - else col ^ " in (" ^ pg_msval v ^ ")" + if pat then "(" ^ iter f " or " v ^ ")" + else match v with + | [s] -> col ^ " = " ^ (P.quote s) + | v -> col ^ " in (" ^ pg_msval v ^ ")" else "true" in let pg_cons l = iter pg_con " and " l in let pg_cons_not l = "not (" ^ pg_cons l ^ ")" in - let pg_where = match ct, cf with - | [], [] -> "" - | lt, [] -> " where " ^ pg_cons lt - | [], lf -> " where " ^ pg_cons_not lf - | lt, lf -> " where " ^ pg_cons lt ^ " and " ^ pg_cons_not lf + let pg_cons_not_l ll = iter pg_cons_not " and " ll in + let pg_where = match ct, cfl with + | [], [] -> "" + | lt, [] -> " where " ^ pg_cons lt + | [], llf -> " where " ^ pg_cons_not_l llf + | lt, llf -> " where " ^ pg_cons lt ^ " and " ^ pg_cons_not_l llf in if cols = [] then [] else begin let q = "select " ^ pg_cols ^ " from " ^ table ^ pg_where ^ @@ -93,7 +96,7 @@ let pg_result distinct subj el res = in compose mk_avs res -let get_table mc ct cf el = +let get_table mc ct cfl el = let fst = function | [] -> None | head :: tail -> Some head @@ -112,7 +115,7 @@ let get_table mc ct cf el = | [] -> prev | (p, _) :: tail -> get_e (comp prev (fst p)) tail in - get_e (get_c (get_c (fst mc) ct) cf) el + get_e (get_c (get_c (fst mc) ct) (List.concat cfl)) el let rec decolon s = let l = String.length s in @@ -123,38 +126,37 @@ let rec decolon s = let conv = function | [] -> "source" - | ["objectname"] -> "value" + | ["objectName"] -> "value" | [t] -> "" | [_; t] -> decolon t | _ -> not_supported "conv" -let postgres_single mc ct cf el t = - let table = match t with Some t -> decolon t | None -> "objectname" in +let postgres_single mc ct cfl el t = + let table = match t with Some t -> decolon t | None -> "objectName" in let first = conv mc in let mk_con l = List.map (fun (pat, p, v) -> (pat, conv p, v)) l in let cons_true = mk_con ct in - let cons_false = mk_con cf in + let cons_false = List.map mk_con cfl in let other_cols = List.map (fun (p, _) -> conv p) el in let cols = if first = "" then other_cols else first :: other_cols in pg_result false first el (pg_query table cols cons_true cons_false) let deadline = 100 -let postgres refine mc ct cf el = - if refine <> M.RefineExact then not_supported "postgres"; - cl_print ct; - let table = get_table mc ct cf el in +let postgres refine mc ct cfl el = + if refine <> M.RefineExact then not_supported "postgres"; + let table = get_table mc ct cfl el in let rec postgres_aux ct = match ct with | (pat, p, v) :: tail when List.length v > deadline -> let single s = postgres_aux ((pat, p, [s]) :: tail) in U.mql_iter single v | _ -> - postgres_single mc ct cf el table + postgres_single mc ct cfl el table in postgres_aux ct (* Galax backend ***********************************************************) -let galax refine mc ct cf el = not_supported "Galax" +let galax refine mc ct cfl el = not_supported "Galax" (* funzioni vecchie ********************************************************) diff --git a/helm/ocaml/mathql_interpreter/mQIProperty.mli b/helm/ocaml/mathql_interpreter/mQIProperty.mli index 90ac3cba6..d47fc34c4 100644 --- a/helm/ocaml/mathql_interpreter/mQIProperty.mli +++ b/helm/ocaml/mathql_interpreter/mQIProperty.mli @@ -26,9 +26,9 @@ open MathQL val postgres: refine -> path -> - (bool * path * value) list -> (bool * path * value) list -> + (bool * path * value) list -> (bool * path * value) list list -> exp_list -> result val galax: refine -> path -> - (bool * path * value) list -> (bool * path * value) list -> + (bool * path * value) list -> (bool * path * value) list list -> exp_list -> result