(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License 
**-----------------------------------------------------------------------
**
** File: eval.ml
** Main author: jahier@imag.fr
*)


open Formula
open Env_state
open Wtree

(****************************************************************************)



let (lookup: env_in -> subst list -> var_name -> atomic_expr option) = 
  fun input pre vn ->  
    try Some(Hashtbl.find input vn)
    with Not_found -> 
      try Some(List.assoc vn pre)
      with Not_found -> None


(****************************************************************************)
(****************************************************************************)

let rec (eval : formula -> env_in -> formula) =
  (*
   ** [eval f input] returns an evaluated version of the formula f. Input
   ** variables (namely, sut outputs) as well as variables ``under a pre'' 
   ** (in the environment memory) are replaced by their values. Then, 
   ** the formula is simplified; e.g., `true and f' is simplified into `f'.
   *)
  fun f input -> 
    match f with
	And(f1, f2) ->  
	  let ef1 = (eval f1 input) in
	    if (ef1 = False) then False
	    else 
	      let ef2 = (eval f2 input) in
		if ef1 = True then ef2
		else if ef2 = False then False
		else if ef2 = True  then ef1
		else And(ef1, ef2)
		  
      | Or(f1, f2) ->  
	  let ef1 = (eval f1 input) in
	    if ef1 = True then True
	    else 
	      let ef2 = (eval f2 input) in
		if ef1 = False then ef2
		else if ef2 = True then True
		else if ef2 = False  then ef1
		else Or(ef1, ef2)

      | Not(f1) -> 
	  let ef1 = (eval f1 input) in
	    if ef1 = True then False
	    else if ef1 = False then True
	    else Not(ef1)

      | True -> True
      | False ->  False

      | Bvar(str) -> 
	  ( match (lookup input env_state.pre str) with 
		Some(Bool(bool)) -> 
		  if bool then True else False
	      | Some(_) -> 
                  print_string (str ^ " is not a boolean!\n");
		  assert false
	      | None -> Bvar(str)
	  )
      | Eq(e1, e2) -> 
	  (
	    let ee1 = eval_expr e1 input in
	    let ee2 = eval_expr e2 input in
	      match (ee1, ee2) with
		  (Ival(i1), Ival(i2)) -> if (i1 = i2) then True else False
		| (Fval(f1), Fval(f2)) -> 
		    if (f1 = f2) then True else False
		| _ -> Eq(ee1, ee2)
	  )
      | Neq(e1, e2) -> 
	  (
	    let ee1 = eval_expr e1 input in
	    let ee2 = eval_expr e2 input in
	      Neq(ee1, ee2)
	  )
      | SupEq(e1, e2) ->
	  (
	    let ee1 = eval_expr e1 input in
	    let ee2 = eval_expr e2 input in
	      match (ee1, ee2) with
		  (Ival(i1), Ival(i2)) -> if (i1 >= i2) then True else False
		| (Fval(f1), Fval(f2)) -> 
		    if (f1 >= f2) then True else False
		| _ -> SupEq(ee1, ee2)
	  )
      | Sup(e1, e2) -> 
	  (
	    let ee1 = eval_expr e1 input in
	    let ee2 = eval_expr e2 input in
	      match (ee1, ee2) with
		  (Ival(i1), Ival(i2)) -> if (i1 > i2) then True else False
		| (Fval(f1), Fval(f2)) -> 
		    if (f1 > f2) then True else False
		| _ -> Sup(ee1, ee2)
	  )
      | InfEq(e1, e2) ->
	  (
	    let ee1 = eval_expr e1 input in
	    let ee2 = eval_expr e2 input in
	      match (ee1, ee2) with
		  (Ival(i1), Ival(i2)) -> if (i1 <= i2) then True else False
		| (Fval(f1), Fval(f2)) -> 
		    if (f1 <= f2) then True else False
		| _ -> InfEq(ee1, ee2)
	  )
      | Inf(e1, e2) -> 
	  (
	    let ee1 = eval_expr e1 input in
	    let ee2 = eval_expr e2 input in
	      match (ee1, ee2) with
		  (Ival(i1), Ival(i2)) -> if (i1 < i2) then True else False
		| (Fval(f1), Fval(f2)) -> 
		    if (f1 < f2) then True else False
		| _ -> Inf(ee1, ee2)
	  )
and
  (eval_expr : expr -> env_in -> expr) =
  fun e input -> 
    match e with  
	Sum(e1, e2) ->
	  (
	    let ee1 = eval_expr e1 input in
	    let ee2 = eval_expr e2 input in
	      match (ee1, ee2) with
		  (Ival(i1), Ival(i2)) -> Ival(i1+i2)
		| (Ival(i1), Fval(f2)) -> Fval(float_of_int(i1)+.f2)
		| (Fval(f1), Ival(i2)) -> Fval(f1+.float_of_int(i2))
		| (Fval(f1), Fval(f2)) -> Fval(f1+.f2)
		| _ -> Sum(ee1, ee2)
	  )
      | Diff(e1, e2) ->
	  (
	    let ee1 = eval_expr e1 input in
	    let ee2 = eval_expr e2 input in
	      match (ee1, ee2) with
		  (Ival(i1), Ival(i2)) -> Ival(i1-i2)
		| (Ival(i1), Fval(f2)) -> Fval(float_of_int(i1)-.f2)
		| (Fval(f1), Ival(i2)) -> Fval(f1-.float_of_int(i2))
		| (Fval(f1), Fval(f2)) -> Fval(f1-.f2)
		| _ -> Diff(ee1, ee2)
	  )
      | Prod(e1, e2) ->
	  (
	    let ee1 = eval_expr e1 input in
	    let ee2 = eval_expr e2 input in
	      match (ee1, ee2) with
		  (Ival(i1), Ival(i2)) -> Ival(i1*i2)
		| (Ival(i1), Fval(f2)) -> Fval(float_of_int(i1)*.f2)
		| (Fval(f1), Ival(i2)) -> Fval(f1*.float_of_int(i2))
		| (Fval(f1), Fval(f2)) -> Fval(f1*.f2)
		| _ -> Prod(ee1, ee2)
	  )
      | Quot(e1, e2) ->
	  (
	    let ee1 = eval_expr e1 input in
	    let ee2 = eval_expr e2 input in
	      match (ee1, ee2) with
		  (Ival(i1), Ival(i2)) -> Ival(i1/i2)
		| (Fval(f1), Fval(f2)) -> Fval(f1/.f2)
		| _ -> Quot(ee1, ee2)
	  )
      | Mod(e1, e2)  ->
	  (
	    let ee1 = eval_expr e1 input in
	    let ee2 = eval_expr e2 input in
	      match (ee1, ee2) with
		  (Ival(i1), Ival(i2)) -> Ival(i1 mod i2)
		| (Fval(f1), Fval(f2)) -> Fval(mod_float f1 f2)
		| _ -> Mod(ee1, ee2)
	  )
      | Nvar(str) ->
	  ( match (lookup input env_state.pre str) with 
		Some(Int(i)) -> Ival(i)
	      | Some(Float(f)) -> Fval(f)
	      | Some(Bool(f)) -> 
		  print_string ((string_of_bool f) 
				^ "is a bool, not an int nor a float!\n");
		  assert false
	      | None -> Nvar(str)
	  )
      | Ival(i) -> Ival(i)
      | Fval(f) -> Fval(f)


(****************************************************************************)
(****************************************************************************)

let rec (eval_wtree_list: env_in -> wtree list -> node list list -> 
	   formula_table) =
  fun input wtl nfll -> 
    (**
      Returns a table of formula appearing in `wtl'; the formula are
      evaluated w.r.t. `input'. `nfll' is the list of list of origin nodes
      corresponding to the trees in `wtl' (necessary to get formula associated
      to pair of nodes from env_state.formula_table).
     *)
    let ft = (Hashtbl.create (List.length wtl)) in
      (List.iter2
	 (eval_wtree input ft)
	 wtl
	 nfll);
      ft
and
  (eval_wtree : env_in -> formula_table -> wtree -> node list -> unit) =
  fun input ft wt nl -> 
    List.iter (eval_wnode input ft nl) wt
and
  (eval_wnode : env_in -> formula_table -> node list -> wnode -> unit) =
  fun input ft nlf wn -> 
    match wn with
	L(w, nlt) -> List.iter2 (add_formula input ft) nlf nlt 
      | N(w, wt) -> (eval_wtree input ft wt nlf)
and 
  (add_formula : env_in -> formula_table -> node -> node -> unit) =
  fun input ft nf nt -> 
    let f = Hashtbl.find env_state.formula_table (nf, nt) in
    let fe = eval f input in
      Hashtbl.add ft (nf, nt) fe


(****************************************************************************)
(****************************************************************************)


(* exported *)
let (expr_to_atomic: expr -> atomic_expr) = function
    Ival(i) -> Int(i)
  | Fval(f) -> Float(f)
  | _ -> assert false


(* exported *)
let (formula_to_atomic: formula -> atomic_expr) = function
    True -> Bool(true)
  | False -> Bool(false)
  | _ -> assert false
      
(* exported *)
let (update_pre: env_in -> env_out -> env_loc -> unit) =
  fun input output local -> 
    let (update_one_pre_var : var_name -> subst) =
      fun pre_vn -> 
	let vn = String.sub pre_vn 4 ((String.length pre_vn) -4) in
	let pre_value = 
	  try Hashtbl.find input vn
	  with Not_found -> 
	    try List.assoc vn output
	    with Not_found  -> 
	      try List.assoc vn local
	      with Not_found -> assert false
	in
	  (pre_vn, pre_value)
    in
      env_state.pre <- List.map (update_one_pre_var) env_state.pre_var_names