]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_interpreter/mQueryStandard.ml
HELM dependent Mathql-1.4 library
[helm.git] / helm / ocaml / mathql_interpreter / mQueryStandard.ml
index 858c28fa0aee014bfef43dcb54c91fc82df2e835..02fafb655617dbe5ca7ae0f05db0db429ad3da05 100644 (file)
@@ -160,14 +160,14 @@ let log_fun xml src =
    let log_src e o x =
       let t = P.start_time () in o.L.s_query x;
       let s = P.stop_time t in
-      if C.set e.L.conn C.Stat then o.L.s_out (Printf.sprintf "Log source: %s\n" s);
+      if C.set e.L.conn C.Times then o.L.s_out (Printf.sprintf "Log source: %s\n" s);
       e.L.eval x 
    in
    let log_res e o x =  
       let s = e.L.eval x in
       let t = P.start_time () in o.L.s_result s;
       let r = P.stop_time t in
-      if C.set e.L.conn C.Stat then o.L.s_out (Printf.sprintf "Log: %s\n" r); s
+      if C.set e.L.conn C.Times then o.L.s_out (Printf.sprintf "Log: %s\n" r); s
    in
    let txt_log o = 
       if xml then o.L.s_out "xml ";
@@ -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