]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
optimized and patched
[helm.git] / helm / ocaml / mathql_interpreter / mQueryInterpreter.ml
index cc85c78111ae4024b63820fd590e1837de8e02d1..57e1207bcbef3c6187fb1ce5cfe9691c99d2ac9d 100644 (file)
@@ -62,7 +62,9 @@ let execute h x =
    let rec eval_query c = function
       | M.Const r -> 
          let aux2 s g = I.make s (eval_list c g) in
-         let aux (s, gl) = U.iter (aux2 s) gl in  
+         let aux (s, gl) = 
+           if gl = [] then U.avs_of_string s else U.iter (aux2 s) gl
+        in 
          c, U.iter aux r
       | M.Dot (i, p) -> 
          begin
@@ -116,7 +118,7 @@ let execute h x =
            d, f r s
         in 
         let d, r = eval_query c x1 in
-        I.x_iter for_aux (d, I.empty) r
+        I.x_iter for_aux (d, I.empty) (I.optimize r)
       | M.While (k, x1, x2) ->
          let f = match k with
            | M.GenFJoin -> I.union
@@ -133,10 +135,10 @@ let execute h x =
          let f = if b then I.d_union else I.union in
         let agl = eval_grp c z in       
         let aux r sj gl _ = 
-           I.append (f (U.make_x sj gl) (U.make_x sj agl)) r
+           I.union r (f (U.make_x sj gl) (U.make_x sj agl))
         in
         let _, r = eval_query c x in
-        c, I.x_iter aux I.empty r
+        c, I.x_iter aux I.empty (I.optimize r)
       | M.Property (q0, q1, q2, mc, ct, cfl, el, pat, y) ->
         let _, r = eval_query c y in
         let subj, mct = 
@@ -159,10 +161,10 @@ let execute h x =
          let aux (d, r) sj gl _ =
            let d = {d with avars = P.add_assoc (i, (sj, gl)) d.avars} in
            let d, s = eval_query d y in
-           if s = U.val_false then d, r else d, (I.append (U.make_x sj gl) r)
+           if s = U.val_false then d, r else d, (I.union r (U.make_x sj gl))
         in
         let d, r = eval_query c x in
-         I.x_iter aux (d, I.empty) r 
+         I.x_iter aux (d, I.empty) (I.optimize r) 
       | M.Fun (p, pl, xl) ->        
         let e = {L.eval = (fun x -> snd (eval_query c x)); L.conn = h} in
          c, L.fun_eval e (F.text_out_spec (C.log h) "\n") F.text_in_spec