X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2FmQueryStandard.ml;fp=helm%2Focaml%2Fmathql_interpreter%2FmQueryStandard.ml;h=858c28fa0aee014bfef43dcb54c91fc82df2e835;hb=381006cf8b418cfdeaf145ab7df9e8f2b19ae2e6;hp=4bd251b141aa963ff1e8d5c63adb075bdbae9052;hpb=efdc3184ccd0738fe48aa0056fc444fba23329e8;p=helm.git

diff --git a/helm/ocaml/mathql_interpreter/mQueryStandard.ml b/helm/ocaml/mathql_interpreter/mQueryStandard.ml
index 4bd251b14..858c28fa0 100644
--- a/helm/ocaml/mathql_interpreter/mQueryStandard.ml
+++ b/helm/ocaml/mathql_interpreter/mQueryStandard.ml
@@ -26,18 +26,24 @@
 (*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
  *)
 
+module U = AvsUtil
+module M = MathQL
+module I = M.I
 module P = MQueryUtil 
 module C = MQIConn 
-module U = MQIUtil
 module L = MQILib
 
 let init = ()
 
+let test f v1 v2 = U.avs_of_bool (f v1 v2) 
+
+let num_test f v1 v2 = U.avs_of_bool (f (U.int_of_avs v1) (U.int_of_avs v2)) 
+
 (* FALSE / EMPTY ************************************************************)
 
 let false_fun b =
    let s = if b then "false" else "empty" in 
-   L.fun_arity0 [] s U.mql_false
+   L.fun_arity0 [] s U.val_false
 
 let _ = L.fun_register ["empty"] (false_fun false)
 
@@ -45,14 +51,14 @@ let _ = L.fun_register ["false"] (false_fun true)
 
 (* TRUE *********************************************************************)
 
-let true_fun = L.fun_arity0 [] "true" U.mql_true
+let true_fun = L.fun_arity0 [] "true" U.val_true
 
 let _ = L.fun_register ["true"] true_fun
 
 (* NOT **********************************************************************)
 
 let not_fun = 
-   let aux r = if r = U.mql_false then U.mql_true else U.mql_false in
+   let aux r = if r = U.val_false then U.val_true else U.val_false in
    L.fun_arity1 [] "!" aux 
 
 let _ = L.fun_register ["not"] not_fun
@@ -60,7 +66,7 @@ let _ = L.fun_register ["not"] not_fun
 (* COUNT ********************************************************************)
 
 let count_fun =
-   let aux r = [string_of_int (List.length r), []] in
+   let aux r = U.avs_of_int (U.count r) in
    L.fun_arity1 [] "#" aux
 
 let _ = L.fun_register ["count"] count_fun
@@ -68,58 +74,61 @@ let _ = L.fun_register ["count"] count_fun
 (* PEEK *********************************************************************)
 
 let peek_fun =
-   let aux = function [] -> [] | hd :: _ -> [hd] in
+   let aux r = 
+      match (I.peek r) with
+         | I.Empty 
+	 | I.Single _     -> r
+	 | I.Many (s, gl) -> U.make_x s gl
+   in
    L.fun_arity1 [] "peek" aux
 
 let _ = L.fun_register ["peek"] peek_fun
 
 (* DIFF *********************************************************************)
 
-let diff_fun = L.fun_arity2 [] "diff" U.mql_diff
+let diff_fun = L.fun_arity2 [] "diff" I.diff
 
 let _ = L.fun_register ["diff"] diff_fun
 
 (* XOR **********************************************************************)
 
-let xor_fun = L.fun_arity2 [] "xor" U.xor
+let xor_fun =
+   let aux v1 v2 =
+      let b = v1 <> U.val_false in 
+      if b && v2 <> U.val_false then U.val_false else
+      if b then v1 else v2
+   in
+   L.fun_arity2 [] "xor" aux
 
 let _ = L.fun_register ["xor"] xor_fun
 
 (* SUB **********************************************************************)
 
-let sub_fun = L.fun_arity2 [] "sub" U.set_sub
+let sub_fun = L.fun_arity2 [] "sub" (test I.sub)
 
 let _ = L.fun_register ["sub"] sub_fun
 
 (* MEET *********************************************************************)
 
-let meet_fun = L.fun_arity2 [] "meet" U.set_meet
+let meet_fun = L.fun_arity2 [] "meet" (test I.meet)
 
 let _ = L.fun_register ["meet"] meet_fun
 
 (* EQ ***********************************************************************)
 
-let eq_fun = L.fun_arity2 [] "==" U.set_eq
+let eq_fun = L.fun_arity2 [] "==" (test I.eq)
 
 let _ = L.fun_register ["eq"] eq_fun
 
 (* LE ***********************************************************************)
 
-let le_fun = 
-   let le v1 v2 =
-      if U.int_of_set v1 <= U.int_of_set v2 then U.mql_true else U.mql_false
-   in
-   L.fun_arity2 [] "<=" le
+let le_fun = L.fun_arity2 [] "<=" (num_test (<=))
 
 let _ = L.fun_register ["le"] le_fun
 
 (* LT ***********************************************************************)
 
-let lt_fun = 
-   let lt v1 v2 =
-      if U.int_of_set v1 < U.int_of_set v2 then U.mql_true else U.mql_false
-   in
-   L.fun_arity2 [] "<" lt
+let lt_fun = L.fun_arity2 [] "<" (num_test (<))
 
 let _ = L.fun_register ["lt"] lt_fun
 
@@ -133,7 +142,7 @@ let stat_fun =
          let t = P.start_time () in
 	 let r = (e.L.eval x) in
 	 let s = P.stop_time t in
-         o.L.out (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
+         o.L.out (Printf.sprintf "Stat: %s,%i\n" s (U.count r));
 	 r
       | _   -> assert false
    in
@@ -190,7 +199,7 @@ let render_fun =
          let rs = ref "" in
 	 let out s = rs := ! rs ^ s in 
          o.L.result out " " (e.L.eval x);
-	 [! rs, []]
+	 I.make ! rs I.grp_empty
       | _   -> assert false
    in
    let txt_out o _ = function
@@ -208,12 +217,12 @@ let read_fun =
    let arity_s = L.Const 1 in
    let body e o i _ = function
       | [x] -> 
-         let aux av = 
-	    let ich = open_in (fst av) in
+         let aux avs s _ = 
+	    let ich = open_in s in
 	    let r = i.L.result_in (Lexing.from_channel ich) in
-	    close_in ich; r
+	    close_in ich; I.union avs r
 	 in
-	 U.mql_iter aux (e.L.eval x)
+	 I.iter aux I.empty (e.L.eval x)
       | _   -> assert false
    in
    let txt_out o _ = function
@@ -227,16 +236,17 @@ let _ = L.fun_register ["read"] read_fun
 (* ALIGN ********************************************************************)
 
 let align_fun =
-   let aux l (v, g) =
+   let aux2 l v =
       let c = String.length v in
-      if c < l then [(String.make (l - c) ' ' ^ v), g] else [v, g]
-   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 arity_p = L.Const 0 in
    let arity_s = L.Const 2 in
    let body e _ _ _ = function
       | [y; x] ->
-         let l = U.int_of_set (e.L.eval y) in
-         U.mql_iter (aux l) (e.L.eval x)      
+         let l = U.int_of_avs (e.L.eval y) in
+         I.x_iter (aux l) I.empty (e.L.eval x)      
       | _      -> assert false
    in
    let txt_out o _ = function
@@ -256,7 +266,7 @@ let if_fun =
    let arity_s = L.Const 3 in
    let body e _ _ _ = function
       | [y; x1; x2] ->
-         if (e.L.eval y) = U.mql_false then (e.L.eval x2) else (e.L.eval x1)
+         if U.bool_of_avs (e.L.eval y) then (e.L.eval x1) else (e.L.eval x2)
       | _           -> assert false
    in
    let txt_out o _ = function
@@ -276,7 +286,7 @@ let intersect_fun =
    let rec iter f = function
       | []           -> assert false
       | [head]       -> f head
-      | head :: tail -> U.mql_intersect (f head) (iter f tail)  
+      | head :: tail -> I.intersect (f head) (iter f tail)  
    in
    let arity_p = L.Const 0 in
    let arity_s = L.Positive in
@@ -295,7 +305,7 @@ let _ = L.fun_register ["intersect"] intersect_fun
 let union_fun = 
    let arity_p = L.Const 0 in
    let arity_s = L.Any in
-   let body e _ _ _ xl = U.mql_iter e.L.eval xl in
+   let body e _ _ _ xl = U.iter e.L.eval xl in
    let txt_out o _ xl = let o = L.std o in L.out_txt_ o [] xl  
    in      
    {L.arity_p = arity_p; L.arity_s = arity_s; L.body = body; L.txt_out = txt_out}
@@ -306,10 +316,10 @@ let _ = L.fun_register ["union"] union_fun
 
 let or_fun = 
    let rec iter f = function
-      | []           -> U.mql_false
+      | []           -> U.val_false
       | head :: tail -> 
          let r1 = f head in
-	 if r1 = U.mql_false then (iter f tail) else r1
+	 if U.bool_of_avs r1 then r1 else (iter f tail)
    in
    let arity_p = L.Const 0 in
    let arity_s = L.Any in
@@ -326,10 +336,10 @@ let _ = L.fun_register ["or"] or_fun
 
 let and_fun = 
    let rec iter f = function
-      | []           -> U.mql_true
+      | []           -> U.val_true
       | [head]       -> f head
       | head :: tail -> 
-         if f head = U.mql_false then U.mql_false else iter f tail
+         if U.bool_of_avs (f head) then iter f tail else U.val_false 
    in
    let arity_p = L.Const 0 in
    let arity_s = L.Any in
@@ -345,14 +355,15 @@ let _ = L.fun_register ["and"] and_fun
 (* PROJ *********************************************************************)
 
 let proj_fun =
-   let proj_group_aux p (q, v) = if q = p then U.mql_subj v else [] in 
-   let proj_group p a = U.mql_iter (proj_group_aux p) a in
-   let proj_set p (_, g) = U.mql_iter (proj_group p) (List.rev g) in
+   let aux2 p a q v _ = if p = q then I.union a (U.subj v) else a in   
+   let aux p a _ gl _ = 
+      I.union a (U.iter (I.x_grp_iter (aux2 p) I.empty) gl) 
+   in
    let arity_p = L.Const 1 in
    let arity_s = L.Const 1 in
    let body e _ _ pl xl =
       match pl, xl with
-         | [p], [x] -> U.mql_iter (proj_set p) (e.L.eval x)
+         | [p], [x] -> I.x_iter (aux p) I.empty (e.L.eval x)
 	 | _        -> assert false
    in
    let txt_out o pl xl =
@@ -368,15 +379,15 @@ let _ = L.fun_register ["proj"] proj_fun
 
 (* KEEP *********************************************************************)
 
-let keep_fun b =
-   let proj (r, _) = (r, []) in
-   let keep_path l (p, v) t = if List.mem p l = b then t else (p, v) :: t in
-   let keep_grp l a = List.fold_right (keep_path l) a [] in
-   let keep_set l a g = 
-      let kg = keep_grp l a in
-      if kg = [] then g else kg :: g
+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))
    in
-   let keep_av l (s, g) = (s, List.fold_right (keep_set l) g []) in
+   let aux l a s gl _ = 
+      I.append a (
+         if l = [] then I.make s I.grp_empty else 
+	 U.iter (I.x_grp_iter (aux2 s l) I.empty) gl) 
+   in  
    let txt_allbut o = if b then o.L.s_out "allbut " in
    let txt_path_list o l = P.flat_list o.L.s_out o.L.s_path ", " l in 
    let arity_p = L.Any in
@@ -384,8 +395,7 @@ let keep_fun b =
    let body e _ _ pl xl =
       match b, pl, xl with
          | true, [], [x]  -> e.L.eval x
-         | false, [], [x] -> List.map proj (e.L.eval x)
-         | _, l, [x]      -> List.map (keep_av l) (e.L.eval x)
+         | _, l, [x]      -> I.x_iter (aux l) I.empty (e.L.eval x)
          | _              -> assert false
   in
   let txt_out o pl xl =