(***********************************************************************)
(*                                                                     *)
(*                               TAToo                                 *)
(*                                                                     *)
(*                  Lucca Hirschi, ?   *)
(*                  ?   *)
(*                                                                     *)
(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
(*  Recherche Scientifique. All rights reserved.  This file is         *)
(*  distributed under the terms of the GNU Lesser General Public       *)
(*  License, with the special exception on linking described in file   *)
(*  ../LICENSE.                                                        *)
(*                                                                     *)
(***********************************************************************)

open XPath.Ast
open Formula.Infix

exception Not_core_XPath
(** Raised whenever the XPath query contains not implemented structures *)

let pr_er = Format.err_formatter

let trans query =
  (* Buidling of the ASTA step by step with a special case for the last
     step. Then add a top most state. Each function modifies asta. *)
  let asta = Asta.empty in
  (* builds asta from the bottom of the query *)
  let rec trans = function
    | [s] -> trans_last s
    | s :: tl ->  trans tl; trans_step s
    | [] -> ()
      
  (* Add THE top most state for top-level query (done in the end) *)
  and trans_init () =
    let top_st = Asta.new_state () in
    let or_top = 
      List.fold_left (fun acc x -> ((`Left *+ x) +| acc))
	(Formula.false_) (Asta.top_states asta)
    in
    Asta.add_quer asta top_st;
    Asta.init_top asta;
    Asta.add_top asta top_st;
    Asta.add_bot asta top_st;	(* for trees which are leaves *)
    Asta.add_tr asta (top_st, Asta.any_label, or_top) true
      
  (* A selecting state is needed *)
  and trans_last (ax,test,pred) =
    let fo_p = trans_pr pred in
    let q,q' = Asta.new_state(), Asta.new_state() in
    Asta.add_selec asta q';
    Asta.add_quer asta q;
    Asta.add_quer asta q';
    Asta.add_top asta q;
    Asta.add_top asta q';
    Asta.add_bot asta q;		(* q' \notin B !! *)
    let Simple lab = test in
    let tr_selec = (q', lab, fo_p)
    and tr_q = (q, Asta.any_label, form_propa_selec q q' ax) in
    Asta.add_tr asta tr_selec true;
    Asta.add_tr asta tr_q true
    
  (* Add a new state and its transitions for the step *)
  and trans_step (ax,test,pred) =
    let fo_p = trans_pr pred
    and q = Asta.new_state() in
    let Simple label = test
    and form_next = (fo_p) *&                    (* (\/ top_next) /\ predicat *)
      (List.fold_left (fun acc x -> (`Left *+ x ) +| acc)
	 Formula.false_ (Asta.top_states asta)) in
    let tr_next = (q, label, form_next)
    and tr_propa = (q, Asta.any_label, form_propa q ax) in
    Asta.add_quer asta q;
    Asta.add_top asta q;
    Asta.add_bot asta q;
    Asta.add_tr asta tr_next true;
    Asta.add_tr asta tr_propa true;
    Asta.init_top asta;
    Asta.add_top asta q
      
  (* Translating of predicates. Either we apply De Morgan rules
     in xPath.parse or here *)
  and trans_pr  = function
    | Expr True -> Formula.true_
    | Expr False -> Formula.false_
    | Or (p_1,p_2) -> trans_pr(p_1) +| trans_pr(p_2)
    | And (p_1,p_2) -> trans_pr(p_1) *& trans_pr(p_2)
    | Not (Expr Path q) -> (trans_pr_path false q)
    | Expr Path q -> (trans_pr_path true q)
    | x -> print_predicate pr_er x; raise Not_core_XPath
     
  (* Builds asta for predicate and gives the formula which must be satsified *)
  and trans_pr_path posi = function
    | Relative [] -> if posi then Formula.true_ else Formula.false_
    | Relative steps -> List.fold_left
      (fun acc x -> if posi then (`Left *+ x) +| acc else (`Left *- x) +| acc)
      Formula.false_ (trans_pr_step_l steps)
    | AbsoluteDoS steps as x -> print pr_er x; raise Not_core_XPath
    | Absolute steps as x -> print pr_er x; raise Not_core_XPath
      
  (* Builds asta for a predicate query and give the formula *)
  and trans_pr_step_l = function
    | [step] -> trans_pr_step [] step
    | step :: tl -> let list_top = trans_pr_step_l tl in
		    trans_pr_step list_top step
    | [] -> failwith "Can not happened! 1"

  (* Add a step on the top of a list of states in a predicate *)
  and trans_pr_step list (ax,test,pred) =
    let form_next =
      if list = []
      then trans_pr pred
      else (trans_pr pred) *&
	(List.fold_left (fun acc x -> (`Left *+ x) +| acc)
	   Formula.false_ list)
    and q = Asta.new_state() 
    and Simple label = test in
    let tr_next = (q,label, form_next)
    and tr_propa = (q, Asta.any_label, form_propa q ax) in
    Asta.add_reco asta q;
    Asta.add_tr asta tr_next false;
    Asta.add_tr asta tr_propa false;
    [q]					(* always one element here, but more with self
					   axis *)
  (* Gives the propagation formula *)
  and form_propa q = function
    | Child -> `Right *+ q
    | Descendant -> (`Left *+ q +| `Right *+ q)
    | x -> print_axis pr_er x; raise Not_core_XPath 

  (* The same with a selecting state *)
  and form_propa_selec q q' = function
    | Child -> `Right *+ q +| `Right *+ q'
    | Descendant -> (`Left *+ q +| `Right *+ q) +| (`Left *+ q' +| `Right *+ q')
    | x -> print_axis pr_er x; raise Not_core_XPath 
      
  in
  (* Match the top-level query *)
  match query with	
    | Absolute steps -> trans steps; trans_init(); asta
    | AbsoluteDoS steps as x -> print pr_er x; raise Not_core_XPath
    | Relative steps as x -> print pr_er x; raise Not_core_XPath