
let ROWINSERT =
  let lxt = `\x:real. T` in
  fun i const_thm interpsigns_thm -> 
    let isigns_thms = interpsigns_thms2 interpsigns_thm in
    let isigns_thm = hd isigns_thms in
    let set,_,_ = 
      if concl isigns_thm = t_tm then lxt,t_tm,t_tm else 
        dest_interpsign (hd isigns_thms) in
    let const_thm' = MATCH_MP (ISPEC set matinsert_lem0) const_thm in 
    let const_thm'' = PURE_REWRITE_RULE[GSYM interpsign] const_thm' in
    let isigns_thms' = insertat i const_thm'' isigns_thms in 
    let isigns_thms'' = if isigns_thm = TRUTH then butlast isigns_thms' else isigns_thms' in
      mk_interpsigns isigns_thms'';;

let MATINSERT vars i const_thm cont mat_thm =
  let const_thm' = GEN (hd vars) const_thm in
  let rol_thm,all2_thm = interpmat_thms mat_thm in
  let part_thm = PARTITION_LINE_CONV (snd (dest_comb (concl rol_thm))) in
  let isigns_thms = CONJUNCTS(REWRITE_RULE[ALL2;part_thm] all2_thm) in
  let isigns_thms' = map (ROWINSERT i const_thm') isigns_thms in
  let all2_thm' = mk_all2_interpsigns part_thm isigns_thms' in
  let mat_thm' = mk_interpmat_thm rol_thm all2_thm' in
    cont mat_thm';;



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

(* OPT FAILED... slightly slower, even with hashtables *)  

let rec mk_suc = 
  let zero = `0` in
  let suc = `SUC` in
  fun n -> 
    match n with 
      0 -> zero 
    | n -> mk_comb(suc,mk_suc (n-1));;

let rec MK_SUC = 
  let f n = prove(mk_eq(mk_small_numeral n,mk_suc n),ARITH_TAC) in
  let size = 100 in
  let range = 0--size in
  let suc_tbl = Hashtbl.create size in
  map2 (Hashtbl.add suc_tbl) range (map f range);
  fun n -> 
    try Hashtbl.find suc_tbl n with _ -> f n;;

let PL_LENGTH = 
  let pl_tm = `partition_line` in
  let len_tm = `LENGTH:(real -> bool) list -> num` in
  fun pts -> 
    let lpts = mk_comb(len_tm,mk_comb(pl_tm,pts)) in
    let lthm = ARITH_SIMP_CONV[PARTITION_LINE_LENGTH;LENGTH] lpts in
    let pts' = snd(dest_eq(concl lthm)) in
    let n = dest_small_numeral pts' in
    let suc_thm = MK_SUC n in
      TRANS lthm suc_thm;;


let rec MK_LT = 
  let f(n1,n2) = prove(mk_binop nle (mk_suc n1) (mk_suc n2),ARITH_TAC) in
  let size1 = 20 in
  let size2 = 20 in
  let range1 = 0--size1 in
  let range2 = 0--size2 in
  let range = filter (fun (x,y) -> x <= y) (allpairs (fun x y -> x,y) range1 range2) in
  let suc_tbl = Hashtbl.create (size1 * size2) in
  map2 (Hashtbl.add suc_tbl) range (map f range);
  fun (n1,n2) -> 
    try Hashtbl.find suc_tbl (n1,n2) with _ -> f(n1,n2);;


let tvars,ti,tconst,tmat,tcont = ref[],ref 0,ref TRUTH,ref TRUTH,ref (fun x -> fun y -> x);;
(*
let vars,i,const_thm,mat_thm = !ti,!tconst,!tmat
#trace MATINSERT
*)

let MATINSERT2 = 
  let len_tm = `LENGTH:(real -> real) list -> num` in
  let pl_tm = `partition_line` in    
  fun vars i const_thm cont mat_thm -> 
    tvars := vars;
    ti := i;
    tconst := const_thm;
    tmat := mat_thm;
    tcont := cont;
    let sgn,_,_ = get_binop (concl const_thm) in
    let pts,pols,sgns = dest_interpmat (concl mat_thm) in
    let plen = length (dest_list pols) in
    let mp_thm = 
      if sgn = rlt then INTERP_CONST_NEG 
      else if sgn = rgt then INTERP_CONST_POS 
      else if sgn = req then INTERP_CONST_ZERO
      else failwith "MATINSERT: bad sign" in
    let mp_thm' = CONV_RULE 
     (PATH_CONV2["q";"q";"r";"l";"l";"r";"a";"a";"l";"r"] (ALPHA_CONV (hd vars))) mp_thm in
    let all2_thm1 = MATCH_MP mp_thm' const_thm in
    let all2_thm2 = ISPEC (mk_comb(pl_tm,pts)) all2_thm1 in
    let len_thm = PL_LENGTH pts in  
    let i' = mk_suc i in
    let all2_thm3 = REWRITE_RULE[len_thm;PARTITION_LINE_LENGTH;LENGTH;REPLICATE;] all2_thm2 in
    let lt_thm = MK_LT (i,plen) in 
    let i_thm = prove(mk_binop nle i' (mk_comb(len_tm,pols)),REWRITE_TAC[LENGTH] THEN ACCEPT_TAC lt_thm) in 
    let ret = MATCH_MPL[MATINSERT_THM;mat_thm;all2_thm3;i_thm] in 
    let ret' = PURE_REWRITE_RULE[MAP2;INSERTAT;TL;HD;] ret in
      cont ret';; 

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

let MATINSERT vars i const_thm cont mat_thm =
  let start_time = Sys.time() in
  let res = MATINSERT vars i const_thm cont mat_thm in
    matinsert_timer +.= (Sys.time() -. start_time);
    res;;



(*

let vars,i,const_thm, cont,mat_thm =
[ry;rx],
0,
ASSUME `-- &1 < &0`,
I,
ASSUME `interpmat [x_24] [\x. &0 + x * &1] [[Neg]; [Zero]; [Pos]]`

MATINSERT vars i const_thm cont mat_thm


let vars,i,const_thm, cont,mat_thm =
[ry;rx],
0,
ASSUME `&0 + x * &1 < &0`,
I,
ASSUME `interpmat [] [\y. &1] [[Pos]]`

MATINSERT vars i const_thm cont mat_thm


let vars,i,const_thm, cont,mat_thm =
[`x:real`; `a:real`; `b:real`; `c:real`],
0,
ASSUME `&0 + a * &2 < &0`,
I,
ASSUME `interpmat [x_408] [\x. (&0 + b * &1) + x * (&0 + a * &2)] [[Pos]; [Zero]; [Neg]]`

MATINSERT vars i const_thm cont mat_thm

*)
