exception Isign of (thm * ((term * thm) list));;

(* ---------------------------------------------------------------------- *)
(*  Opt                                                                   *)
(* ---------------------------------------------------------------------- *)

let get_mp =
  let unknown = `Unknown` in
  let pos = `Pos` in
  let zero = `Zero` in
  let neg = `Neg` in
    fun upper_sign lower_sign deriv_sign -> 
        (* Pos Pos *)
        if upper_sign = pos && 
           lower_sign = pos && 
           deriv_sign = pos then INFERISIGN_POS_POS_POS
        else if upper_sign = pos && 
           lower_sign = pos && 
           deriv_sign = neg then INFERISIGN_POS_POS_NEG
        (* Pos Neg *)
        else if upper_sign = pos && 
           lower_sign = neg && 
           deriv_sign = pos then INFERISIGN_POS_NEG_POS
        else if upper_sign = pos && 
           lower_sign = neg && 
           deriv_sign = neg then INFERISIGN_POS_NEG_NEG
        (* Pos Zero *)
        else if upper_sign = pos && 
           lower_sign = zero && 
           deriv_sign = pos then INFERISIGN_POS_ZERO_POS
        else if upper_sign = pos && 
           lower_sign = zero && 
           deriv_sign = neg then INFERISIGN_POS_ZERO_NEG
        (* Neg Pos *)
        else if upper_sign = neg && 
           lower_sign = pos && 
           deriv_sign = pos then INFERISIGN_NEG_POS_POS
        else if upper_sign = neg && 
           lower_sign = pos && 
           deriv_sign = neg then INFERISIGN_NEG_POS_NEG
        (* Neg Neg *)
        else if upper_sign = neg && 
           lower_sign = neg && 
           deriv_sign = pos then INFERISIGN_NEG_NEG_POS
        else if upper_sign = neg && 
           lower_sign = neg && 
           deriv_sign = neg then INFERISIGN_NEG_NEG_NEG
        (* Neg Zero *)
        else if upper_sign = neg && 
           lower_sign = zero && 
           deriv_sign = pos then INFERISIGN_NEG_ZERO_POS
        else if upper_sign = neg && 
           lower_sign = zero && 
           deriv_sign = neg then INFERISIGN_NEG_ZERO_NEG
        (* Zero Pos *)
        else if upper_sign = zero && 
           lower_sign = pos && 
           deriv_sign = pos then INFERISIGN_ZERO_POS_POS
        else if upper_sign = zero && 
           lower_sign = pos && 
           deriv_sign = neg then INFERISIGN_ZERO_POS_NEG
        (* Zero Neg *)
        else if upper_sign = zero && 
           lower_sign = neg && 
           deriv_sign = pos then INFERISIGN_ZERO_NEG_POS
        else if upper_sign = zero && 
           lower_sign = neg && 
           deriv_sign = neg then INFERISIGN_ZERO_NEG_NEG
        (* Zero Zero *)
        else if upper_sign = zero && 
           lower_sign = zero && 
           deriv_sign = pos then INFERISIGN_ZERO_ZERO_POS
        else if upper_sign = zero && 
           lower_sign = zero && 
           deriv_sign = neg then INFERISIGN_ZERO_ZERO_NEG
        else failwith "bad signs in thm";;


let tvars,tdiff,tmat,tex = ref [],ref TRUTH,ref TRUTH,ref [];;
(*
  let vars,diff_thm,mat_thm,ex_thms = !tvars,!tdiff,!tmat,!tex
INFERISIGN vars diff_thm mat_thm ex_thms

let vars,diff_thm,mat_thm,ex_thms = vars, pdiff_thm, mat_thm''', ((v1,exthm1)::(v2,exthm2)::ex_thms) 
*)

let rec INFERISIGN =
  let real_app = `APPEND:real list -> real list -> real list` in 
  let sign_app = `APPEND:(sign list) list -> (sign list) list -> (sign list) list` in
  let real_len = `LENGTH:real list -> num` in 
  let sign_len = `LENGTH:(sign list) list -> num` in
  let unknown = `Unknown` in
  let pos = `Pos` in
  let zero = `Zero` in
  let neg = `Neg` in
  let num_mul = `( * ):num -> num -> num` in
  let num_add = `( + ):num -> num -> num` in
  let real_ty = `:real` in
  let one = `1` in
  let two = `2` in
  let f = `F` in
  let imat = `interpmat` in
  let sl_ty = `:sign list` in
  fun vars diff_thm mat_thm ex_thms -> 
    try 
      tvars := vars;
      tdiff := diff_thm;
      tmat := mat_thm; 
      tex := ex_thms; 
      let pts,ps,sgns = dest_interpmat (concl mat_thm) in
      let pts' = dest_list pts in
      if pts' = [] then mat_thm,ex_thms else
      let sgns' = dest_list sgns in
      let sgnl = map dest_list sgns' in
      let i = get_index (fun x -> hd x = unknown) sgnl in
      if i mod 2 = 1 then failwith "bad shifted matrix" else
      let p::p'::_ = dest_list ps in
      let p_thm = ABS (hd vars) (POLY_ENLIST_CONV vars (snd(dest_abs p))) in
      let p'_thm = ONCE_REWRITE_RULE[GSYM diff_thm] (ABS (hd vars) (POLY_ENLIST_CONV vars (snd(dest_abs p')))) in
      let pts1,qts1 = chop_list (i / 2 - 1) pts' in
      let ps_thm = REWRITE_CONV[p_thm;p'_thm] ps in 
      let pts2 = mk_list(pts1,real_ty) in
      let pts3 = mk_comb(mk_comb(real_app,pts2),mk_list(qts1,real_ty)) in
      
let pts_thm = prove(mk_eq(pts,pts3),REWRITE_TAC[APPEND]) in
      let sgns1,rgns1 = chop_list (i - 1) sgns' in
      let sgns2 = mk_list(sgns1,sl_ty) in
      let sgns3 = mk_comb(mk_comb(sign_app,sgns2),mk_list(rgns1,sl_ty)) in
      let sgns_thm = prove(mk_eq(sgns,sgns3),REWRITE_TAC[APPEND]) in
      let len1 = mk_comb(sign_len,sgns2) in
      let len2 = mk_binop num_add (mk_binop num_mul two (mk_comb(real_len,pts2))) one in
      let len_thm = prove(mk_eq(len1,len2),REWRITE_TAC[LENGTH] THEN ARITH_TAC) in
      let mat_thm1 = MK_COMB(MK_COMB((AP_TERM imat pts_thm), ps_thm),sgns_thm) in
      let mat_thm2 = EQ_MP mat_thm1 mat_thm in 
      let upper_sign = hd (ith (i - 1) sgnl) in
      let lower_sign = hd (ith (i + 1) sgnl) in
      let deriv_sign = hd (tl (ith i sgnl)) in
      let mp_thm = get_mp upper_sign lower_sign deriv_sign in
      let mat_thm3 = MATCH_MP (MATCH_MP mp_thm mat_thm2) len_thm in 
      let mat_thm4 = REWRITE_RULE[GSYM p_thm;GSYM p'_thm;APPEND] mat_thm3 in
      let c = concl mat_thm4 in
      if c = f then raise (Isign (mat_thm4,ex_thms)) else
      if not (is_exists c) then 
        INFERISIGN vars diff_thm mat_thm4 ex_thms else
      let x,bod = dest_exists c in
      let x' = new_var real_ty in  
      let assume_thm = ASSUME (subst [x',x] bod) in
        INFERISIGN vars diff_thm assume_thm ((x',mat_thm4)::ex_thms)
  with 
    Failure "get_index" -> mat_thm,ex_thms
  | Failure x -> failwith ("INFERISIGN: " ^ x);;
(* 
let vars,diff_thm,mat_thm,ex_thms =  vars,pdiff_thm, mat_thm''',[]

let mat_thm = ASSUME ` interpmat [x_25; x1; x2; x4; x5; x_26]
     [\x. &1 + x * (&1 + x * (&1 + x * &1)); \x. &1 + x * (&2 + x * &3); 
     \x. &2 + x * (-- &3 + x * &1); \x. -- &4 + x * (&0 + x * &1)]
     [[Neg; Pos; Pos; Pos]; 
      [Neg; Pos; Pos; Pos]; 
      [Unknown; Pos; Pos; Pos]; 
      [Pos; Pos; Pos; Zero]; 
      [Unknown; Neg; Pos; Neg]; 
      [Unknown; Neg; Neg; Neg]; 
      [Unknown; Neg; Pos; Neg];
      [Pos; Zero; Zero; Neg]; 
      [Unknown; Pos; Neg; Neg]; 
      [Pos; Pos; Zero; Zero]; 
      [Unknown; Pos; Pos; Pos];
      [Pos; Pos; Pos; Pos]; 
      [Pos; Pos; Pos; Pos]]`

*)


(* ---------------------------------------------------------------------- *)
(*  Timing                                                                *)
(* ---------------------------------------------------------------------- *)

let INFERISIGN vars diff_thm mat_thm ex_thms = 
  let start_time = Sys.time() in
  let res = INFERISIGN vars diff_thm mat_thm ex_thms in
    inferisign_timer +.= (Sys.time() -. start_time);
    res;;

(* {{{ Examples *)

(*
let is_thms = isigns_thms'''

let vars,diff_thm,mat_thm =  
[`w:real`; `z:real`; `y:real`; `x:real`],
ASSUME `poly_diff [&0 + y * (&0 + x * &1); &0 + z * -- &1] = [&0 + z * -- &1]`,
ASSUME `interpmat [x_178; x_179]
     [\w. (&0 + y * (&0 + x * &1)) + w * (&0 + z * -- &1); \w. &0 + z * -- &1]
     [[Pos; Neg]; [Pos; Neg]; [Unknown; Neg]; [Neg; Neg]; [Neg; Neg]]`

INFERISIGN vars pdiff_thm mat_thm

let diff
let vars,diff_thm,mat_thm = 



let vars,diff_thm,mat_thm = 
[`x:real`],
ASSUME `poly_diff [&0; &2; &0; &4] = [&2; &0; &12]`,
ASSUME `interpmat [x_79; x_68; x_80]
        [\x. &0 + x * (&2 + x * (&0 + x * &4)); \x. &2 + x * (&0 + x * &12); 
        \x. &4 + x * (&0 + x * &2)]
        [[Neg; Pos; Pos]; [Neg; Pos; Pos]; [Unknown; Pos; Pos]; [Unknown; Pos; Pos]; [Unknown; Pos; Pos]; [Pos; Pos; Pos]; [Pos; Pos; Pos]]`



let mat_thm = mat_thm'''
let diff_thm = pdiff_thm
INFERISIGN vars pdiff_thm mat_thm'''

let diff_thm = POLY_DIFF_CONV `poly_diff [&1; &1; &1; &1]`;;

let vars = [`x:real`]

let mat_thm = ASSUME
  `interpmat 
     [xminf; x1; x4; x5; xinf]
     [\x. &1 + x * (&1 + x * (&1 + x * &1)); \x. &1 + x * (&2 + x * &3); \x. &2 + x * (-- &3 + x * &1); \x. -- &4 + x * (&0 + x * &1)]
     [[Neg; Pos; Pos; Pos];      
      [Neg; Pos; Pos; Pos];      
      [Unknown; Pos; Pos; Pos];  
      [Neg; Pos; Pos; Zero];     
      [Unknown; Pos; Pos; Neg];  
      [Pos; Pos; Zero; Neg];     
      [Unknown; Pos; Neg; Neg];  
      [Pos; Pos; Zero; Zero];    
      [Unknown; Pos; Pos; Pos];  
      [Pos; Pos; Pos; Pos];      
      [Pos; Pos; Pos; Pos]]`;;     

let mat_thm1,_ = INFERISIGN vars diff_thm mat_thm []

*)
(* }}} *)