]> matita.cs.unibo.it Git - helm.git/commitdiff
new syntax for "property" enabled:
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 31 May 2003 18:59:06 +0000 (18:59 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 31 May 2003 18:59:06 +0000 (18:59 +0000)
 now many "isfalse" clauses are accepted

helm/ocaml/mathql_interpreter/mQIExecute.ml
helm/ocaml/mathql_interpreter/mQIProperty.ml
helm/ocaml/mathql_interpreter/mQIProperty.mli

index 2f5ca7eb69e76d2e7ba28d7c138eab94519fb0ea..efb8feb1c7ac7a40d76ad13ce4a5ce368e12b017 100644 (file)
@@ -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
index c30c18d47e16fa59b689a531abd690a05ff27514..56a9d64212d44ea9bd0e4de0472b54da0957402f 100644 (file)
@@ -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  ********************************************************)
 
index 90ac3cba62d13c19ab54b4420f4d0ddb7a1f3344..d47fc34c455a32fd964ab0c11e34efc235d9ed98 100644 (file)
@@ -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