X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2FmQILib.ml;h=b1582f9bce63c9d618f624fdde9024a3ed3391ef;hb=9cbce40d56958c466459b028cf250441ec29c9fe;hp=f816590d102b687cf626d05ade27345e0d8954c7;hpb=786284e9dfb25a31aad2161d59cdc5f36657e94a;p=helm.git

diff --git a/helm/ocaml/mathql_interpreter/mQILib.ml b/helm/ocaml/mathql_interpreter/mQILib.ml
index f816590d1..b1582f9bc 100644
--- a/helm/ocaml/mathql_interpreter/mQILib.ml
+++ b/helm/ocaml/mathql_interpreter/mQILib.ml
@@ -28,8 +28,8 @@
 
 module M = MathQL
 module P = MQueryUtil 
+module C = MQIConn 
 module U = MQIUtil
-module C = MQIConn
 
 (* external function specification ******************************************)
 
@@ -37,21 +37,21 @@ type arity_t = Const of int
              | Positive
 	     | Any
 
-type eval_spec = {eval   : M.query -> M.result;
-                  handle : C.handle
+type eval_spec = {eval : M.query -> M.result;
+                  conn : C.handle
 		 }
 
-type txt_out_spec = {out    : string -> unit;
-                     path   : M.path -> unit;
-		     query  : M.query -> unit;
-		     result : M.result -> unit
-		    }
+type text_out_spec = {out    : string -> unit;
+                      path   : M.path -> unit;
+	 	      query  : M.query -> unit;
+		      result : M.result -> unit
+		     }
 
 type fun_spec = {arity_p : arity_t;
                  arity_s : arity_t;
-                 body    : eval_spec -> txt_out_spec ->
+                 body    : eval_spec -> text_out_spec ->
 		           M.path list -> M.query list -> M.result;
-		 txt_out : txt_out_spec -> 
+		 txt_out : text_out_spec -> 
 		           M.path list -> M.query list -> unit
 		}
 
@@ -69,32 +69,33 @@ let int_of_set s =
       | _      -> raise (Failure "int_of_string")
    with Failure "int_of_string" -> raise (NumberError s)
 
-let out_txt2 out commit n x1 x2 =
-   out "(" ; commit x1; out (" " ^ n ^ " "); commit x2; out ")"
+let out_txt2 o n x1 x2 =
+   o.out "(" ; o.query x1; o.out (" " ^ n ^ " "); o.query x2; o.out ")"
 
-let out_txt_ out path commit p xl = 
-   path p; out " {"; P.flat_list out commit ", " xl; out "}"    
+let out_txt_ o p xl =
+   if p <> [] then begin o.path p; o.out " " end;
+   o.out "{"; P.flat_list o.out o.query ", " xl; o.out "}"    
 
-let out_txt_full out path commit p pl xl = 
-   path p; out " {"; P.flat_list out path ", " pl; out "} {";
-   P.flat_list out commit ", " xl; out "}"    
+let out_txt_full o p pl xl = 
+   o.path p; o.out " {"; P.flat_list o.out o.path ", " pl; o.out "} {";
+   P.flat_list o.out o.query ", " xl; o.out "}"    
 
 let arity0 n r =
    let arity_p = Const 0 in
    let arity_s = Const 0 in
    let body _ _ _ _ = U.mql_true in
-   let txt_out s _ _ = s.out n in
+   let txt_out o _ _ = o.out n in
    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 
 let arity1 n f =
    let arity_p = Const 0 in
    let arity_s = Const 1 in
-   let body eval _ _ = function
-      | [x] -> f (eval x)
+   let body e _ _ = function
+      | [x] -> f (e.eval x)
       | _   -> assert false
    in
-   let txt_out out _ commit _ = function
-      | [x] -> out (n ^ " "); commit x
+   let txt_out o _ = function
+      | [x] -> o.out (n ^ " "); o.query x
       | _   -> assert false
    in   
    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
@@ -102,27 +103,29 @@ let arity1 n f =
 let arity2 n f =
    let arity_p = Const 0 in
    let arity_s = Const 2 in
-   let body eval _ _ = function
-      | [x1; x2] -> f (eval x1) (eval x2)
+   let body e _ _ = function
+      | [x1; x2] -> f (e.eval x1) (e.eval x2)
       | _        -> assert false
    in
-   let txt_out out _ commit _ = function
-      | [x1; x2] -> out_txt2 out commit n x1 x2
+   let txt_out o _ = function
+      | [x1; x2] -> out_txt2 o n x1 x2
       | _        -> assert false
    in   
    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 
-let false_fun = arity0 "false" U.mql_false
+let false_fun b =
+   let s = if b then "false" else "empty" in 
+   arity0 s U.mql_false
 
 let true_fun = arity0 "true" U.mql_true
 
 let not_fun = 
    let aux r = if r = U.mql_false then U.mql_true else U.mql_false in
-   arity1 "not" aux 
+   arity1 "!" aux 
 
 let count_fun =
    let aux r = [string_of_int (List.length r), []] in
-   arity1 "count" aux
+   arity1 "#" aux
    
 let diff_fun = arity2 "diff" U.mql_diff
 
@@ -132,34 +135,63 @@ let sub_fun = arity2 "sub" U.set_sub
 
 let meet_fun = arity2 "meet" U.set_meet
 
-let eq_fun = arity2 "eq" U.set_eq
+let eq_fun = arity2 "==" U.set_eq
 
 let le_fun = 
    let le v1 v2 =
       if int_of_set v1 <= int_of_set v2 then U.mql_true else U.mql_false
    in
-   arity2 "le" le
+   arity2 "<=" le
 
 let lt_fun = 
    let lt v1 v2 =
       if int_of_set v1 < int_of_set v2 then U.mql_true else U.mql_false
    in
-   arity2 "lt" lt
+   arity2 "<" lt
 
 let stat_fun =
    let arity_p = Const 0 in
    let arity_s = Const 1 in
-   let body eval h _ = function
+   let body e o _ = function
       | [x] -> 
          let t = P.start_time () in
-	 let r = (eval x) in
+	 let r = (e.eval x) in
 	 let s = P.stop_time t in
-         C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
+         o.out (Printf.sprintf "Stat: %s,%i\n" s (List.length r));
 	 r
       | _   -> assert false
    in
-   let txt_out out _ commit _ = function
-      | [x] -> out "stat "; commit x
+   let txt_out o _ = function
+      | [x] -> o.out "stat "; o.query x
+      | _   -> assert false
+   in   
+   {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
+
+let log_fun xml src =
+   let log_src e o x =
+      let t = P.start_time () in o.query x;
+      let s = P.stop_time t in
+      if C.set e.conn C.Stat then o.out (Printf.sprintf "Log source: %s\n" s);
+      e.eval x 
+   in
+   let log_res e o x =  
+      let s = e.eval x in
+      let t = P.start_time () in o.result s;
+      let r = P.stop_time t in
+      if C.set e.conn C.Stat then o.out (Printf.sprintf "Log: %s\n" r); s
+   in
+   let txt_log o = 
+      if xml then o.out "xml ";
+      if src then o.out "source "
+   in
+   let arity_p = Const 0 in
+   let arity_s = Const 1 in
+   let body e o _ = function
+      | [x] -> if src then log_src e o x else log_res e o x
+      | _   -> assert false
+   in        
+   let txt_out o _ = function
+      | [x] -> o.out "log "; txt_log o; o.query x
       | _   -> assert false
    in   
    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
@@ -171,14 +203,14 @@ let align_fun =
    in   
    let arity_p = Const 0 in
    let arity_s = Const 2 in
-   let body eval _ _ = function
+   let body e _ _ = function
       | [y; x] ->
-         let l = int_of_set (eval y) in
-         U.mql_iter (aux l) (eval x)      
+         let l = int_of_set (e.eval y) in
+         U.mql_iter (aux l) (e.eval x)      
       | _      -> assert false
    in
-   let txt_out out _ commit _ = function
-      | [y; x] -> out "align "; commit y; out " in "; commit x
+   let txt_out o _ = function
+      | [y; x] -> o.out "align "; o.query y; o.out " in "; o.query x
       | _      -> assert false
    in
    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
@@ -186,14 +218,15 @@ let align_fun =
 let if_fun =
    let arity_p = Const 0 in
    let arity_s = Const 3 in
-   let body eval _ _ = function
+   let body e _ _ = function
       | [y; x1; x2] ->
-         if (eval y) = U.mql_false then (eval x2) else (eval x1)
+         if (e.eval y) = U.mql_false then (e.eval x2) else (e.eval x1)
       | _           -> assert false
    in
-   let txt_out out _ commit _ = function
+   let txt_out o _ = function
       | [y; x1; x2] ->
-         out "if "; commit y; out " then "; commit x1; out " else "; commit x2
+         o.out "if "; o.query y; o.out " then "; o.query x1; 
+	 o.out " else "; o.query x2
       | _           -> assert false
    in
    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
@@ -206,21 +239,19 @@ let intersect_fun =
    in
    let arity_p = Const 0 in
    let arity_s = Positive in
-   let body eval _ _ xl = iter eval xl in
-   let txt_out out path commit _ = function
+   let body e _ _ xl = iter e.eval xl in
+   let txt_out o _ = function
       | []           -> assert false
-      | [x1; x2]     -> out_txt2 out commit "intersect" x1 x2
-      | xl           -> out_txt_ out path commit ["intersect"] xl  
+      | [x1; x2]     -> out_txt2 o "/\\" x1 x2
+      | xl           -> out_txt_ o ["intersect"] xl  
    in   
    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 
 let union_fun = 
    let arity_p = Const 0 in
    let arity_s = Any in
-   let body eval _ _ xl = U.mql_iter eval xl in
-   let txt_out out path commit _ = function
-      | [x1; x2]     -> out_txt2 out commit "union" x1 x2
-      | xl           -> out_txt_ out path commit ["union"] xl  
+   let body e _ _ xl = U.mql_iter e.eval xl in
+   let txt_out o _ xl = out_txt_ o [] xl  
    in      
    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 
@@ -233,10 +264,10 @@ let or_fun =
    in
    let arity_p = Const 0 in
    let arity_s = Any in
-   let body eval _ _ xl = iter eval xl in
-   let txt_out out path commit _ = function
-      | [x1; x2]     -> out_txt2 out commit "or" x1 x2
-      | xl           -> out_txt_ out path commit ["or"] xl  
+   let body e _ _ xl = iter e.eval xl in
+   let txt_out o _ = function
+      | [x1; x2]     -> out_txt2 o "||" x1 x2
+      | xl           -> out_txt_ o ["or"] xl  
    in
    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 
@@ -244,39 +275,108 @@ let and_fun =
    let rec iter f = function
       | []           -> U.mql_true
       | head :: tail -> 
-         if f head = U.mql_false then U.mql_false else (iter f tail)
+         if f head = U.mql_false then U.mql_false else iter f tail
+   in
+   let arity_p = Const 0 in
+   let arity_s = Any in
+   let body e _ _ xl = iter e.eval xl in
+   let txt_out o _ = function 
+      | [x1; x2]  -> out_txt2 o "&&" x1 x2
+      | xl        -> out_txt_ o ["and"] xl
+   in
+   {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
+
+let seq_fun = 
+   let rec iter f = function
+      | []           -> U.mql_true
+      | head :: tail -> ignore (f head); iter f tail
    in
    let arity_p = Const 0 in
    let arity_s = Any in
-   let body eval _ _ xl = iter eval xl in
-   let txt_out out path commit _ = function
-      | [x1; x2]     -> out_txt2 out commit "and" x1 x2
-      | xl           -> out_txt_ out path commit ["and"] xl  
+   let body e _ _ xl = iter e.eval xl in
+   let txt_out o _ = function 
+      | [x1; x2]  -> o.query x1; o.out " ;; "; o.query x2
+      | xl        -> out_txt_ o ["seq"] xl
+   in
+   {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
+
+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) g in
+   let arity_p = Const 1 in
+   let arity_s = Const 1 in
+   let body e _ pl xl =
+      match pl, xl with
+         | [p], [x] -> U.mql_iter (proj_set p) (e.eval x)
+	 | _        -> assert false
+   in
+   let txt_out o pl xl =
+      match pl, xl with
+         | [p], [x] -> o.out "proj "; o.path p; o.out " of "; o.query x
+	 | _        -> assert false
+   in
+   {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
+
+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
+   in
+   let keep_av l (s, g) = (s, List.fold_right (keep_set l) g []) in
+   let txt_allbut o = if b then o.out "allbut " in
+   let txt_path_list o l = P.flat_list o.out o.path ", " l in 
+   let arity_p = Any in
+   let arity_s = Const 1 in
+   let body e _ pl xl =
+      match b, pl, xl with
+         | true, [], [x]  -> e.eval x
+         | false, [], [x] -> List.map proj (e.eval x)
+         | _, l, [x]      -> List.map (keep_av l) (e.eval x)
+         | _              -> assert false
+  in
+  let txt_out o pl xl =
+      match pl, xl with
+         | [], [x] -> o.out "keep "; txt_allbut o; o.query x
+	 | l, [x]  -> 
+	    o.out "keep "; txt_allbut o; txt_path_list o l; 
+	    o.out " in "; o.query x
+	 | _      -> assert false
    in
    {arity_p = arity_p; arity_s = arity_s; body = body; txt_out = txt_out}
 
 (* external functions interface *********************************************)
 
 let get_spec = function
-   | ["false"]     -> false_fun
-   | ["true"]      -> true_fun
-   | ["not"]       -> not_fun
-   | ["count"]     -> count_fun
-   | ["stat"]      -> stat_fun
-   | ["diff"]      -> diff_fun
-   | ["xor"]       -> xor_fun
-   | ["sub"]       -> sub_fun
-   | ["meet"]      -> meet_fun
-   | ["eq"]        -> eq_fun
-   | ["le"]        -> le_fun
-   | ["lt"]        -> lt_fun
-   | ["align"]     -> align_fun
-   | ["if"]        -> if_fun 
-   | ["intersect"] -> intersect_fun
-   | ["union"]     -> union_fun
-   | ["or"]        -> or_fun
-   | ["and"]       -> and_fun
-   | p             -> raise (NameError p) 
+   | ["empty"]                 -> false_fun false
+   | ["false"]                 -> false_fun true
+   | ["true"]                  -> true_fun
+   | ["not"]                   -> not_fun
+   | ["count"]                 -> count_fun
+   | ["stat"]                  -> stat_fun
+   | ["log"; "text"; "result"] -> log_fun false false
+   | ["log"; "text"; "source"] -> log_fun false true
+   | ["diff"]                  -> diff_fun
+   | ["xor"]                   -> xor_fun
+   | ["sub"]                   -> sub_fun
+   | ["meet"]                  -> meet_fun
+   | ["eq"]                    -> eq_fun
+   | ["le"]                    -> le_fun
+   | ["lt"]                    -> lt_fun
+   | ["align"]                 -> align_fun
+   | ["if"]                    -> if_fun 
+   | ["intersect"]             -> intersect_fun
+   | ["union"]                 -> union_fun
+   | ["or"]                    -> or_fun
+   | ["and"]                   -> and_fun 
+   | ["seq"]                   -> seq_fun
+   | ["proj"]                  -> proj_fun
+   | ["keep"; "these"]         -> keep_fun false
+   | ["keep"; "allbut"]        -> keep_fun true
+   | p                         -> raise (NameError p) 
    
 let check_arity p m n =
    let aux i = function 
@@ -287,60 +387,8 @@ let check_arity p m n =
    in   
    aux m (get_spec p).arity_p; aux n (get_spec p).arity_s 
 
-let exec eval h p pl xl = (get_spec p).body eval h pl xl
-
-let txt_out out path commit p pl xl =
-   try (get_spec p).txt_out out path commit pl xl 
-   with NameError q when q = p -> out_txt_full out path commit p pl xl
-
-(*
-      | M.Proj (Some p) x -> out "proj "; txt_path out p; out "of "; txt_set x
-      | M.Log a b x       -> out "log "; txt_log a b; txt_set x
-      | M.Keep b l x      -> out "keep "; txt_allbut b; txt_path_list l;
-                             txt_set x
-   let txt_path_list l = P.flat_list out (txt_path out) ", " l in 
-   let txt_log a b = 
-      if a then out "xml ";
-      if b then out "source "
-   in
-   let txt_allbut b = if b then out "allbut " in
-
-      | M.Proj None x -> List.map (fun (r, _) -> (r, [])) (eval_query c x)
-      | M.Proj (Some p) x -> 
-         let proj_group_aux (q, v) = if q = p then subj v else [] in 
-         let proj_group a = U.mql_iter proj_group_aux a in
-         let proj_set (_, g) = U.mql_iter proj_group g in
-         U.mql_iter proj_set (eval_query c x)
-
-
-      | M.Log _ b x ->
-         if b then begin
-	    let t = P.start_time () in
-	    F.text_of_query (C.log h) x "\n";
-	    let s = P.stop_time t in
-	    if C.set h C.Stat then 
-	       C.log h (Printf.sprintf "Log source: %s\n" s);
-	    eval_query c x
-	 end else begin
-            let s = (eval_query c x) in
-	    let t = P.start_time () in
-	    F.text_of_result (C.log h) s "\n"; 
-	    let r = P.stop_time t in
-	    if C.set h C.Stat then 
-	       C.log h (Printf.sprintf "Log: %s\n" r);
-	    s
-	 end
-
-      | M.Keep b l x -> 
-         let keep_path (p, v) t = 
-	    if List.mem p l = b then t else (p, v) :: t in
-	 let keep_grp a = List.fold_right keep_path a [] in
-         let keep_set a g = 
-	    let kg = keep_grp a in
-	    if kg = [] then g else kg :: g
-	 in
-	 let keep_av (s, g) = (s, List.fold_right keep_set g []) in
-	 List.map keep_av (eval_query c x)
-
-
-*)      
+let eval e o p pl xl = (get_spec p).body e o pl xl
+
+let txt_out o p pl xl =
+   try (get_spec p).txt_out o pl xl 
+   with NameError q when q = p -> out_txt_full o p pl xl