X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2FmQueryInterpreter.ml;h=b66228581c9a66ab56a6c47e08c51782cd836d0a;hb=cf13d8dc120ae8745b26f8dbadea5af3f3b2193c;hp=a852affdeeaa3bf03df23426f8b63686483c1500;hpb=a32bcc14672dae13e8bb725e54c819958dfdb677;p=helm.git

diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
index a852affde..b66228581 100644
--- a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
+++ b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml
@@ -60,15 +60,17 @@ let execute h x =
    in
    let proj v = List.map fst v in
    let rec eval_query c = function
-      | M.Const r -> r
-      | M.Dot i p -> begin
-         try U.mql_subj (List.assoc p (List.assoc i c.groups)) 
-	 with Not_found -> warn (M.Dot i p); [] end
+      | M.Const r -> c, r
+      | M.Dot i p -> 
+         begin
+            try c, U.mql_subj (List.assoc p (List.assoc i c.groups)) 
+	    with Not_found -> warn (M.Dot i p); c, [] 
+	 end
       | M.Ex l y -> 
          let rec ex_aux h = function
 	    | []        -> 
 	       let d = {c with groups = h} in
-               if eval_query d y = U.mql_false then () else raise Found 
+               if snd (eval_query d y) = U.mql_false then () else raise Found 
 	    | i :: tail -> 
                begin
 	          try 
@@ -81,38 +83,62 @@ let execute h x =
 	          with Not_found -> ()
 	       end
          in
-	 (try ex_aux [] l; U.mql_false with Found -> U.mql_true)
-      | M.SVar i -> begin
-         try List.assoc i c.svars 
-	 with Not_found -> warn (M.SVar i); [] end  
-      | M.AVar i -> begin
-         try [List.assoc i c.avars] 
-	 with Not_found -> warn (M.AVar i); [] end
-      | M.Let i x1 x2 ->
-	 let d = {c with svars = P.add_assoc (i, eval_query c x1) c.svars} in
+	 begin try ex_aux [] l; c, U.mql_false with Found -> c, U.mql_true end
+      | M.SVar i -> 
+         begin
+            try c, List.assoc i c.svars 
+	    with Not_found -> warn (M.SVar i); c, []
+	 end  
+      | M.AVar i -> 
+         begin
+            try c, [List.assoc i c.avars] 
+	    with Not_found -> warn (M.AVar i); c, []
+	 end
+      | M.Let (Some i) x1 x2 ->
+	 let d, r = eval_query c x1 in
+	 let d = {d with svars = P.add_assoc (i, r) d.svars} in
          eval_query d x2
+      | M.Let None x1 x2 ->
+	 let d, r = eval_query c x1 in eval_query d x2
       | M.For k i x1 x2 ->
          let f = match k with
 	    | M.GenFJoin -> U.mql_union
 	    | M.GenFMeet -> U.mql_intersect
 	 in
-         let rec for_aux = function
-	    | []     -> []
+         let rec for_aux (d, r) = match r with
+	    | []     -> d, []
 	    | h :: t ->
-	       let d = {c with avars = P.add_assoc (i, h) c.avars} in
-	       f (eval_query d x2) (for_aux t)
+	       let d = {d with avars = P.add_assoc (i, h) d.avars} in
+	       let d, r = eval_query d x2 in
+	       let d, s = for_aux (d, t) in
+	       d, f r s
 	 in
 	 for_aux (eval_query c x1)
+      | M.While k x1 x2 ->
+         let f = match k with
+	    | M.GenFJoin -> U.mql_union
+	    | M.GenFMeet -> U.mql_intersect
+	 in
+         let rec while_aux (d, r) = 
+	    let d, b = eval_query d x1 in
+	    if b = U.mql_false then d, r else 
+	    let d, s = eval_query d x2 in
+	    while_aux (d, f r s)
+	 in
+	 while_aux (c, U.mql_false)
       | M.Add b z 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) []
+	 let _, r = eval_query c x in
+	 c, List.fold_right g r []
       | M.Property q0 q1 q2 mc ct cfl el pat y ->
+	 let _, r = eval_query c y in
 	 let subj, mct = 
-	    if q0 then [], (pat, q2 @ mc, eval_query c y)
-	          else (q2 @ mc), (pat, [], eval_query c y)  
+	    if q0 then [], (pat, q2 @ mc, r) else (q2 @ mc), (pat, [], r)  
+	 in
+         let eval_cons (pat, p, y) = 
+	    let _, r = eval_query c y in (pat, q2 @ p, r)
 	 in
-         let eval_cons (pat, p, y) = (pat, q2 @ p, eval_query c y) in
 	 let cons_true = mct :: List.map eval_cons ct in
 	 let cons_false = List.map (List.map eval_cons) cfl in
 	 let eval_exp (p, po) = (q2 @ p, po) in
@@ -122,26 +148,30 @@ let execute h x =
 	 let s = P.stop_time t in
          if C.set h C.Stat then 
 	    C.log h (Printf.sprintf "Property: %s,%i\n" s (List.length r));
-	 r 
+	 c, r 
       | M.Select i x y ->
-         let rec select_aux = function
-	    | []     -> []
+         let rec select_aux (d, r) = match r with
+	    | []     -> d, []
 	    | h :: t ->
-	       let d = {c with avars = P.add_assoc (i, h) c.avars} in
-	       if eval_query d y = U.mql_false 
-	          then select_aux t else h :: select_aux t
+	       let d = {d with avars = P.add_assoc (i, h) d.avars} in
+	       let d, r = eval_query d y in
+	       let d, s = select_aux (d, t) in
+	       if r = U.mql_false then d, s else d, (h :: s)
 	 in
 	 select_aux (eval_query c x)
-      | M.Fun p pl xl -> 
-         let e = {L.eval = eval_query c; L.conn = h} in
-         L.fun_eval e (F.text_out_spec (C.log h) "\n") F.text_in_spec 
+      | 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 
             p pl xl
       | M.Gen p xl -> 
-         let e = {L.eval = eval_query c; L.conn = h} in
+         let e = {L.eval = (fun x -> snd (eval_query c x)); L.conn = h} in
 	 eval_query c (L.gen_eval e p xl)
    and eval_grp c = function
       | M.Attr gs ->
-         let attr_aux g (p, y) = U.mql_union g [p, proj (eval_query c y)] in
+         let attr_aux g (p, y) = 
+	    let _, r = eval_query c y in
+	    U.mql_union g [p, proj r]
+	 in
 	 let attr_auxs s l = U.set_union s [List.fold_left attr_aux [] l] in
 	 List.fold_left attr_auxs [] gs
       | M.From i ->
@@ -150,7 +180,7 @@ let execute h x =
    in
    let c = {svars = []; avars = []; groups = []} in
    let t = P.start_time () in
-   let r = eval_query c x in
+   let _, r = eval_query c x in
    let s = P.stop_time t in
    if C.set h C.Stat then 
       C.log h (Printf.sprintf "MQIExecute: %s,%s\n" s