(* file combining all the function data *)

(*

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

*)


flyspeck_needs "../formal_lp/formal_interval/interval_m/recurse.hl";;
flyspeck_needs "../formal_lp/formal_interval/interval_m/verifier.hl";;


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

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

let delta_x_poly = 
  let tm = (rand o concl o SPEC_ALL) Sphere.delta_x in
    expr_to_vector_fun tm;;

let delta_y_poly =
  let tm = (rand o concl o SPEC_ALL o REWRITE_RULE[Sphere.delta_x]) Sphere.delta_y in
    expr_to_vector_fun tm;;

let delta_x4_poly =
  let tm = (rand o concl o SPEC_ALL) Sphere.delta_x4 in
    expr_to_vector_fun tm;;

let delta_y4_poly =
  let tm = (rand o concl o SPECL[`y1*y1`; `y2*y2`; `y3*y3`; `y4*y4`; `y5*y5`; `y6*y6`]) Sphere.delta_x4 in
    expr_to_vector_fun tm;;


let tf_delta_x = build_taylor pp delta_x_poly;;
let tf_delta_y = build_taylor pp delta_y_poly;;
let tf_delta_x4 = build_taylor pp delta_x4_poly;;
let tf_delta_y4 = build_taylor pp delta_y4_poly;;

let x = replicate 1.0 8 and
    y = replicate 2.0 8 and
    z = replicate 3.0 8 and
    w = replicate 1.0 8;;

evalf4 tf_delta_x w x y z;;
evalf4 tf_delta_y w x y z;;
evalf4 tf_delta_x4 w x y z;;


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


let four_y1_delta_y_poly = 
  let x_var, tm = dest_abs delta_y_poly in
    mk_abs (x_var, mk_binop mul_op_real `&4` (mk_binop mul_op_real `(x:real^6)$1 * x$1` tm));;

let neg_delta_y4_poly =
  let x_var, tm = dest_abs delta_y4_poly in
    mk_abs (x_var, mk_comb (neg_op_real, tm));;

let four_y1_delta_y = build_taylor pp four_y1_delta_y_poly;;
let neg_delta_y4 = build_taylor pp neg_delta_y4_poly;;
dih_y_taylor;;

let pi_taylor = build_taylor 10 `\x:real^1. pi`;;
let neg_pi_taylor = build_taylor 10 `\x:real^1. --pi`;;
let pi2_taylor = build_taylor 10 `\x:real^1. pi / &2`;;


let f = tf_product x1 (tf_product x1 x3);;
let f = Uni_compose (uinv, x2);;
evalf0 f 0 x y;;
evalf0 f 2 x y;;

(* dih_y *)
let dih_y_taylor =
  let denom = Uni_compose (uinv, Uni_compose (usqrt, four_y1_delta_y)) in
    Plus (pi2_taylor, Uni_compose (uatan, tf_product neg_delta_y4 denom));;


(* sol_y *)

Sphere.sol_y;;
let sol_y_taylor =
  let dih1 = dih_y_taylor and
      dih2 = Composite (dih_y_taylor, x2, x3, x1, x5, x6, x4, unit, unit) and
      dih3 = Composite (dih_y_taylor, x3, x1, x2, x6, x4, x5, unit, unit) in
    Plus (dih1, Plus (dih2, Plus (dih3, neg_pi_taylor)));;


let pi_val= 3.1415926535897932;;
let sol0_val = 0.5512855984325308;;
let const1_val = sol0_val /. pi_val;;
let const1_plus1 = const1_val +. 1.0;;


let ly_taylor = build_taylor pp `\x:real^1. #2.52 / #0.52 - x$1 * inv(#0.52)`;;
let lnazim_y_taylor =
  tf_product ly_taylor dih_y_taylor;;

Sphere.taum;;
let taum_taylor =
  let azim1 = lnazim_y_taylor and
      azim2 = Composite (lnazim_y_taylor, x2, x3, x1, x5, x6, x4, unit, unit) and
      azim3 = Composite (lnazim_y_taylor, x3, x1, x2, x6, x4, x5, unit, unit) in
  let f1 = Scale (sol_y_taylor, mk_interval (const1_plus1, const1_plus1)) and
      f2 = Plus (azim1, Plus (azim2, azim3)) in
    Plus (f1, Scale (f2, mk_interval (~-.const1_val, ~-.const1_val)));;


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

let rec count_f0_flags r =
  match r with
    | Result_false _ -> failwith "False result"
    | Result_glue (_,_,_,r1,r2) -> count_f0_flags r1 + count_f0_flags r2
    | Result_pass (_,flag,_,_) -> if flag then 1 else 0
    | Result_pass_mono _ -> 0;;

let rec all_mono r =
  match r with
    | Result_false _ -> failwith "False result"
    | Result_glue (mono,_,_,r1,r2) -> List.concat mono @ all_mono r1 @ all_mono r2
    | Result_pass (mono,_,_,_) -> List.concat mono
    | Result_pass_mono _ -> [];;

let rec all_pass r =
  match r with
    | Result_false _ -> failwith "False result"
    | Result_glue (_,_,_,r1,r2) -> all_pass r1 @ all_pass r2
    | Result_pass (_,_,x,z) -> [x,z]
    | Result_pass_mono _ -> [];;


let rec count_pass_mono r =
  match r with
    | Result_false _ -> failwith "False result"
    | Result_glue (_,_,_,r1,r2) -> count_pass_mono r1 + count_pass_mono r2
    | Result_pass (_,_,_,_) -> 0
    | Result_pass_mono _ -> 1;;

let rec count_convex r =
  match r with
    | Result_false _ -> failwith "False result"
    | Result_glue (_,_,flag,r1,r2) -> (if flag then 1 else 0) + count_convex r1 + count_convex r2
    | _ -> 0;;





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

let x = [2.0001; 2.0001; 2.0001; 2.0; 2.0; 2.0; 0.0; 0.0] and
    z = [2.52; 2.52; 2.52; 2.0; 2.0; 2.0; 0.0; 0.0];;

let taum_test1 = run_test taum_taylor x z true 0.0 true true true;;
(* 79 *)
result_size taum_test1;;

let taum_test1_0 = run_test0 taum_taylor x z true 0.0 true true true;;
(* 57281 *)
result_size taum_test1_0;;


count_f0_flags taum_test1;;
length (all_mono taum_test1);;
count_pass_mono taum_test1;;
count_convex taum_test1;;




(***)
let x = [2.0; 2.0; 2.0; 2.0; 2.0; 2.52; 0.0; 0.0] and
    z = [2.52; 2.52; 2.52; 2.0; 2.0; 2.52; 0.0; 0.0];;

(CONV_RULE (NUM_REDUCE_CONV THENC REAL_RAT_REDUCE_CONV) o SPECL[`2`; `1`]) Sphere.tame_table_d;;

let taum_test2 = run_test taum_taylor x z true 0.103 false;;
result_size taum_test2;;

(***)
let x = [2.0; 2.0; 2.0; 2.1771; 2.0; 2.0; 0.0; 0.0] and
    z = [2.52; 2.52; 2.52; 2.52; 2.52; 2.52; 0.0; 0.0];;

let taum_test3 = run_test taum_taylor x z true 0.04 false;;
result_size taum_test3;;




(***)
let x, z =
  replicate 2.0 6 @ [0.;0.], 
  replicate 2.52 6 @ [0.;0.];;
let ineq = Plus (taum_taylor, Scale (dih_y_taylor, mk_interval (0.626, 0.626)));;
let taum_test4 = run_test ineq x z true 0.77 true true true;;
(* 52540 (48014) *)
result_size taum_test4;;

count_f0_flags taum_test4;;
length (all_mono taum_test4);;
count_pass_mono taum_test4;;
count_convex taum_test4;;


let ineq = Plus (taum_taylor, Scale (dih_y_taylor, mk_interval (-0.259, -0.259)));;
let taum_test5 = run_test ineq x z true (-0.32) false;;
(* 37737 *)
result_size taum_test5;;




let x, z =
  replicate 2.0 6 @ [0.;0.], 
  replicate 2.52 6 @ [0.;0.];;

let ineq1_test = run_test dih_y_taylor x z true 0.852 true true true;;
(* 10298 (10142) *)
result_size ineq1_test;;    

let ineq1_test0 = run_test0 dih_y_taylor x z true 0.852 true true true;;
(* 604796 (true false true) 308962 (true true true) *)
result_size ineq1_test0;;



count_f0_flags ineq1_test;;
all_mono ineq1_test;;
count_pass_mono ineq1_test;;
count_convex ineq1_test;;

let pp = 10;;
let n = 6;;
let xx = `[&2;&2;&2;&2;&2;&2]` and
    zz = `[#2.52;#2.52;#2.52;#2.52;#2.52;#2.52]`;;
let xx1 = convert_to_float_list pp true xx and
    zz1 = convert_to_float_list pp false zz;;

m_verify_domain_test n pp eval_delta_x4 ineq1_test xx1 zz1;;

ineq1_test;;

let dd = (evalf dih_y_taylor x x).dd;;
map (fun i -> mth (mth dd i) i) iter8;;


let ineq2_test = run_test dih_y_taylor x z false 1.893 true true false;;
(* 4905 (4886 with derivatives) *)
result_size ineq2_test;;

let ineq2_test0 = run_test0 dih_y_taylor x z false 1.893 true true true;;
(* 35842 (true false true) 35842 (true true true) *)
result_size ineq2_test0;;

let all_p = all_pass ineq2_test;;
let xx, zz = List.nth all_p 134;;
let dd = (evalf dih_y_taylor xx zz).dd;;
map (fun i -> mth (mth dd i) i) iter8;;



count_f0_flags ineq2_test;;
all_mono ineq2_test;;
count_pass_mono ineq2_test;;
count_convex ineq2_test;;

count_f0_flags ineq2_test0;;
length (all_mono ineq2_test0);;
count_pass_mono ineq2_test0;;
count_convex ineq2_test0;;



let rec pass_intervals r =
  match r with
    | Result_false _ -> failwith "False result"
    | Result_glue (_,r1,r2) -> pass_intervals r1 @ pass_intervals r2
    | Result_pass (x,z) -> [x,z];;


let intersect_results r1 r2 =
  let i1 = pass_intervals r1 and
      i2 = pass_intervals r2 in
  let i = intersect i1 i2 in
    length i, i;;

(* 1683 *)
let n1, i1 = intersect_results ineq1_test ineq2_test;;
(* 583 *)
let n2, i2 = intersect_results ineq1_test taum_test4;;
(* 5 *)
let n3, i3 = intersect_results ineq2_test taum_test4;;

(* 14486 *)
let n4, i4 = intersect_results taum_test4 taum_test5;;
maxl (map (maxl o filter (fun x -> x <> 0.) o snd o center_form) (pass_intervals taum_test4));;

let x = 2;;


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


(*
Sphere.dih_x;;
Ineq.I_5735387903;;
Ineq.dart_std3;;

Ineq.getexact "5735387903";;
Ineq.getexact "5490182221";;
Ineq.getexact "2570626711";;
Ineq.getexact "3296257235";;

Ineq.getexact "8519146937";;
Ineq.getexact "4667071578";;
Ineq.getexact "1395142356";;
Ineq.getexact "7394240696";;
Ineq.getexact "7726998381";;
Ineq.getexact "4047599236";;

Ineq.getexact "8248508703";;
Ineq.getexact "7931207804";;

Ineq.getexact "4491491732";;
*)



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