(* Copyright (C) 2000, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://cs.unibo.it/helm/.
 *)

(*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
 *)

exception Found

module U = AvsUtil
module M = MathQL
module I = M.I
module P = MQueryUtil 
module C = MQIConn
module L = MQILib
module F = MQueryIO

(* contexts *****************************************************************)

type svar_context = (M.svar * M.result) list

type avar_context = (M.avar * (string * M.group list)) list

type group_context = (M.avar * M.group) list

type context = {svars: svar_context;   
                avars: avar_context;   
                groups: group_context (* auxiliary context *)  
               }
	       
(* execute ******************************************************************)

let execute h x =
   let warn q = 
     if C.set h C.Warn then 
     begin
        C.log h "MQIExecute: waring: reference to undefined variables: ";
	F.text_of_query (C.log h) "\n" q
     end
   in
   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) = 
	    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
            try c, I.grp_read (List.assoc i c.groups) p 
	    with Not_found -> warn (M.Dot (i, p)); c, I.empty 
	 end
      | M.Ex (l, y) -> 
         let rec ex_aux h = function
	    | []        -> 
	       let d = {c with groups = h} in
               if snd (eval_query d y) = U.val_false then () else raise Found 
	    | i :: tail -> 
               begin
	          try 
		     let (_, a) = List.assoc i c.avars in 
		     let rec add_group = function
		        | []     -> ()
	                | g :: t -> ex_aux ((i, g) :: h) tail; add_group t 
		     in
		     add_group a
	          with Not_found -> ()
	       end
         in
	 begin try ex_aux [] l; c, U.val_false with Found -> c, U.val_true end
      | M.SVar i -> 
         begin
            try c, List.assoc i c.svars 
	    with Not_found -> warn (M.SVar i); c, I.empty
	 end  
      | M.AVar i -> 
         begin
            try 
	       let s, gl = List.assoc i c.avars in
	       c, U.make_x s gl  
	    with Not_found -> warn (M.AVar i); c, I.empty
	 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 -> I.union
	    | M.GenFMeet -> I.intersect
	 in
         let for_aux (d, r) s gl _ =
	    let d = {d with avars = P.add_assoc (i, (s, gl)) d.avars} in
	    let d, s = eval_query d x2 in
	    d, f r s
	 in 
	 let d, r = eval_query c x1 in
	 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
	    | M.GenFMeet -> I.intersect
	 in
         let rec while_aux (d, r) = 
	    let d, b = eval_query d x1 in
	    if b = U.val_false then d, r else 
	    let d, s = eval_query d x2 in
	    while_aux (d, f r s)
	 in
	 while_aux (c, U.val_false)
      | M.Add (b, z, 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.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 (I.optimize 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, 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 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
	 let exp = List.map eval_exp el in
	 let t = P.start_time () in
	 let r = MQIProperty.exec h q1 subj cons_true cons_false exp in 
	 let s = P.stop_time t in
         if C.set h C.Stat then 
	    C.log h (Printf.sprintf "Property: %s,%i\n" s (U.count r));
	 c, r 
      | M.Select (i, x, y) ->
         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.union r (U.make_x sj gl))
	 in
	 let d, r = eval_query c x in
         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 
            p pl xl
      | M.Gen (p, xl) -> 
         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_list c l =
      let aux (p, y) = 
         let _, r = eval_query c y in
         U.x_grp_make_x p r
      in
      U.grp_iter aux l
   and eval_grp c = function
      | M.Attr gs ->
	 let attr_auxs s l = I.grps_make s (eval_list c l) in
	 List.fold_left attr_auxs [] gs
      | M.From i ->
         try snd (List.assoc i c.avars) 
	 with Not_found -> warn (M.AVar i); []
   in
   let c = {svars = []; avars = []; groups = []} in
   let t = P.start_time () 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 
         (C.string_of_flags (C.flags h)));
   r