(* file combining all the function data *)

(*

This gives the verification of a sample inequality drawn from ineq.hl.

*)


flyspeck_needs "../port_interval/types.hl";;
flyspeck_needs "../port_interval/report.hl";;
flyspeck_needs "../port_interval/interval.hl";;
flyspeck_needs "../port_interval/univariate.hl";;
flyspeck_needs "../port_interval/line_interval.hl";;
flyspeck_needs "../port_interval/taylor.hl";;
flyspeck_needs "../port_interval/recurse.hl";;

module Function_data = struct

open Interval;;
open Univariate;;
open Line_interval;;
open Taylor;;
open Recurse;;


(* This was found  in recurse.cc, but doesn't belong there. *)

let deltainf = 
  let ( * ) =  downmul in
  let ( + ) = downadd  in
  let  ( - ) = downsub in
  let ( ~- ) = ( ~-. ) in
    fun x1 x2 x3 x4 x5 x6 ->
      (down();
         ((~- x2)*x3)*x4 +((~-  x1)*x3)*x5 +((~-  x1)*x2)*x6 +((~-  x4)*x5)*x6 +
   x3*(x1 + x2 + x4 + x5)*x6 +  (x3*(~- x3- x6))*x6 +
   x2*x5*(x1 + x3 + x4 + x6) + x2*(x5*(~- x2-x5)) +
        x1*x4*(x2 + x3 + x5 + x6)+ x1*(x4*(~- x1-x4)));;


let tupl x = let n = List.nth x in (n 0,n 1,n 2,n 3,n 4,n 5);;

let delta_x4L =   
  fun x ->
    let (x1,x2,x3,x4,x5,x6) = tupl x in
    let ( + ),( * ) = up(); (upadd,upmul) in
    let fhi,tdhi=
    ( (~-.  x2)*x3 +(~-.  x1)*x4 + x2*x5 + x3*x6 +(~-.  x5)*x6 +
                x1*(~-. x1) + x1*(~-. x4) + x1*(x2 + x3 + x5 + x6),
        [ (~-. 2.0)* x1 + x2 + x3 + (~-.  2.0)* x4 + x5 + x6;
	 x1 + (~-.  1.0) * x3 + x5;
	 x1 + (~-.  1.0) * x2 + x6;
	 (~-. 2.0) * x1;
	 x1 + x2 + (~-. 1.0) * x6;
	 x1 + x3 + (~-. 1.0)* x5;]) in
    let ( + ),( * ) = down(); (downadd,downmul) in
    let flo,tdlo = 
	 (~-. x2)*x3 +(~-.  x1)*x4 + x2*x5 + x3*x6 +(~-.  x5)*x6 +
                x1*(~-. x1) + x1*(~-. x4) + x1*(x2 + x3 + x5 + x6),
        [ (~-. 2.0)* x1 + x2 + x3 + (~-.  2.0)* x4 + x5 + x6;
	 x1 + (~-.  1.0) * x3 + x5;
	 x1 + (~-.  1.0) * x2 + x6;
	 (~-. 2.0) * x1;
	 x1 + x2 + (~-. 1.0) * x6;
	 x1 + x3 + (~-.  1.0)* x5;] in
      mk_line (mk_interval(flo,fhi),map (fun (x,y)->mk_interval(x,y)) (zip tdlo tdhi));;

let delta_x4DD = 
  let m i = let r = float_of_int i in mk_interval(r,r) in
  let intdata = [[-2; 1; 1; -2; 1; 1]; [1; 0; -1; 0; 1; 0]; [1; -1; 0; 0; 0; 1]; 
		 [-2; 0; 0; 0; 0; 0]; [1; 1; 0; 0; 0; -1]; [1; 0; 1; 0; -1; 0]] in
    table2 (fun i j -> m (mth2 intdata i j));;

let delta_x4 = Prim_a (make_primitiveA ( delta_x4L, (fun x z -> delta_x4DD)));;

(* sample based on ineq.hl "JNTEFVP 1"; *)

let sample = 
  let xx = [4.0;4.0;4.0;4.0;4.0;8.0] in
  let zz = let h02 = 6.3504 in [h02;h02;h02;h02;h02;25.4016] in
  let mone = mk_interval(-1.0,-1.0) in
  let mdelta_x4 = Scale(delta_x4,mone) in
  let testmaxat = 6.02525 in
  let ff = Plus(mdelta_x4,Scale(unit,mk_interval(testmaxat,testmaxat))) in
  let truemaxat = 6.02525951999999165 in
  let opt =  {
    only_check_deriv1_negative = false;
    is_using_dihmax =false;
    is_using_bigface126 =false;
    width_cutoff =0.05;
    allow_sharp =false;
    allow_derivatives =true;
    iteration_count =0;
    iteration_limit =0;
    recursion_depth =200;
  } in
    recursive_verifier(0,xx,zz,xx,zz,[ff],opt);;

end;;