needs "../formal_lp/arith/arith_hash2.hl";;

(* Based on the code of calc_int.ml *)

let test = Arith_hash2.test;;

let to_numeral = Arith_hash2.NUM_TO_NUMERAL_CONV;;
let from_numeral = Arith_hash2.NUMERAL_TO_NUM_CONV;;
let mk_num = Arith_hash2.mk_numeral_array;;
let dest_num = Arith_hash2.dest_numeral_hash;;
let num_suc = Arith_hash2.NUM_SUC_HASH_CONV;;
let num_add = Arith_hash2.NUM_ADD_HASH_CONV;;
let num_mul = Arith_hash2.NUM_MULT_HASH_CONV;;
let num_gt0 = Arith_hash2.NUM_GT0_HASH_CONV;;


(* Constants *)

let n_var_num = `n:num` and
    m_var_num = `m:num` and
    x_var_real = `x:real` and
    y_var_real = `y:real`;;



let neg_op_real = `(--):real->real` and
    amp_op_real = `(&):num->real` and
    plus_op_real = `(+):real->real->real` and
    minus_op_real = `(-):real->real->real` and
    mul_op_real = `( * ):real->real->real` and
    le_op_real = `(<=):real->real->bool` and
    lt_op_real = `(<):real->real->bool`;;


let my_mk_realintconst n = 
  if n >=/ Int 0 then mk_comb(amp_op_real, mk_num n)
  else mk_comb(neg_op_real, mk_comb(amp_op_real, mk_num (minus_num n)));;


let my_dest_realintconst tm = 
  let ltm, rtm = dest_comb tm in
    if (ltm = neg_op_real) then
      let amp_tm, n_tm = dest_comb rtm in
	if (amp_tm = amp_op_real) then
	  minus_num (dest_num n_tm)
	else
	  failwith "my_dest_realintconst: --(&n) expected"
    else
      if (ltm = amp_op_real) then
	dest_num rtm
      else
	failwith "my_dest_realintconst: &n expected";;



let is_neg_comb tm = is_comb tm && rator tm = neg_op_real;;


let replace_numerals = (rand o concl o DEPTH_CONV from_numeral);;
let REPLACE_NUMERALS = CONV_RULE (DEPTH_CONV from_numeral);;


let zero_const = replace_numerals `&0`;;


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

(* NEG *)

let neg_0 = (REPLACE_NUMERALS o prove)(`-- &0 = &0`, REAL_ARITH_TAC) and
    neg_neg = prove(`--(--(&n)) = &n`, REAL_ARITH_TAC);;


let my_real_int_neg_conv tm =
  let neg_tm, rtm = dest_comb tm in
    if (neg_tm = neg_op_real) then
      if (rtm = zero_const) then
	neg_0
      else
	let neg_tm, rtm = dest_comb rtm in
	let amp_tm, n_tm = dest_comb rtm in
	  if (neg_tm = neg_op_real && amp_tm = amp_op_real) then
	    INST[n_tm, n_var_num] neg_neg
	  else
	    failwith "my_real_int_neg_conv: --(--(&n)) expected"
    else
      failwith "my_real_int_neg_conv: --x expected";;


(*
let tm = `-- -- &12241`;;

(* 1.880 *)
test 100000 REAL_INT_NEG_CONV tm;;
(* 0.292 *)
test 100000 my_real_int_neg_conv tm;;
*)



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

(* ADD *)

let pth1 = prove(`(--(&m) + --(&n) = --(&(m + n)))`, REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_NEG_ADD]) and
    pth2 = prove(`(--(&m) + &(m + n) = &n)`, REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN REAL_ARITH_TAC) and
    pth3 = prove(`(--(&(m + n)) + &m = --(&n))`, REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN REAL_ARITH_TAC) and
    pth4 = prove(`(&(m + n) + --(&m) = &n)`, REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN REAL_ARITH_TAC) and
    pth5 = prove(`(&m + --(&(m + n)) = --(&n))`, REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN REAL_ARITH_TAC) and
    pth6 = prove(`(&m + &n = &(m + n))`, REWRITE_TAC[GSYM REAL_OF_NUM_ADD]);;


let my_real_int_add_conv =
  let dest = dest_binop plus_op_real in
  (fun tm ->
    try let l,r = dest tm in
        if rator l = neg_op_real then
          if rator r = neg_op_real then
            let th1 = INST [rand(rand l), m_var_num; rand(rand r), n_var_num] pth1 in
            let tm1 = rand(rand(rand(concl th1))) in
            let th2 = AP_TERM neg_op_real (AP_TERM amp_op_real (num_add tm1)) in
            TRANS th1 th2
          else
            let m = rand(rand l) and n = rand r in
            let m' = dest_num m and n' = dest_num n in
            if m' <=/ n' then
              let p = mk_num (n' -/ m') in
              let th1 = INST [m,m_var_num; p,n_var_num] pth2 in
              let th2 = num_add (rand(rand(lhand(concl th1)))) in
              let th3 = AP_TERM (rator tm) (AP_TERM amp_op_real (SYM th2)) in
              TRANS th3 th1
            else
              let p = mk_num (m' -/ n') in
              let th1 = INST [n,m_var_num; p,n_var_num] pth3 in
              let th2 = num_add (rand(rand(lhand(lhand(concl th1))))) in
              let th3 = AP_TERM neg_op_real (AP_TERM amp_op_real (SYM th2)) in
              let th4 = AP_THM (AP_TERM plus_op_real th3) (rand tm) in
              TRANS th4 th1
        else
          if rator r = neg_op_real then
            let m = rand l and n = rand(rand r) in
            let m' = dest_num m and n' = dest_num n in
            if n' <=/ m' then
              let p = mk_num (m' -/ n') in
              let th1 = INST [n,m_var_num; p,n_var_num] pth4 in
              let th2 = num_add (rand(lhand(lhand(concl th1)))) in
              let th3 = AP_TERM plus_op_real (AP_TERM amp_op_real (SYM th2)) in
              let th4 = AP_THM th3 (rand tm) in
              TRANS th4 th1
            else
             let p = mk_num (n' -/ m') in
             let th1 = INST [m,m_var_num; p,n_var_num] pth5 in
             let th2 = num_add (rand(rand(rand(lhand(concl th1))))) in
             let th3 = AP_TERM neg_op_real (AP_TERM amp_op_real (SYM th2)) in
             let th4 = AP_TERM (rator tm) th3 in
             TRANS th4 th1
          else
            let th1 = INST [rand l,m_var_num; rand r,n_var_num] pth6 in
            let tm1 = rand(rand(concl th1)) in
            let th2 = AP_TERM amp_op_real (num_add tm1) in
            TRANS th1 th2
    with Failure _ -> failwith "my_real_int_add_conv");;


(*
let tm = `&3252375395 + --(&3454570237434)`;;
let tm' = replace_numerals tm;;

(* 1.192 *)
test 1000 REAL_INT_ADD_CONV tm;;
(* 0.224 *)
test 1000 my_real_int_add_conv tm';;
*)


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

(* SUB *)

let real_sub' = SPEC_ALL real_sub;;

let my_real_int_sub_conv tm =
  let x_tm, y_tm = dest_binop minus_op_real tm in
  let th0 = INST[x_tm, x_var_real; y_tm, y_var_real] real_sub' in
    if (is_neg_comb y_tm) then
      let ltm, rtm = dest_comb(rand(concl th0)) in
      let neg_th = my_real_int_neg_conv rtm in
      let th1 = AP_TERM ltm neg_th in
      let th2 = my_real_int_add_conv (rand(concl th1)) in
	TRANS th0 (TRANS th1 th2)
    else
      let th1 = my_real_int_add_conv (rand(concl th0)) in
	TRANS th0 th1;;


(*
let tm = `-- &35252352362346236236 - (-- &12236236363523)`;;
let tm' = replace_numerals tm;;

(* 1.860 *)
test 1000 REAL_INT_SUB_CONV tm;;
(* 0.348 *)
test 1000 my_real_int_sub_conv tm';;
*)




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

(* MUL *)


let mul_pp = prove(`&m * &n = &(m * n)`, REWRITE_TAC[REAL_OF_NUM_MUL]);;
let mul_nn = prove(`--(&m) * --(&n) = &(m * n)`, REWRITE_TAC[REAL_NEG_MUL2; mul_pp]) and
    mul_np = prove(`--(&m) * &n = --(&(m * n))`, REWRITE_TAC[REAL_MUL_LNEG; mul_pp]) and
    mul_pn = prove(`&m * --(&n) = --(&(m * n))`, REWRITE_TAC[REAL_MUL_RNEG; mul_pp]);;


let my_real_int_mul_conv tm =
  let l, r = dest_binop mul_op_real tm in
    if rator l = neg_op_real then
      if rator r = neg_op_real then
        let th1 = INST [rand(rand l), m_var_num; rand(rand r), n_var_num] mul_nn in
        let tm1 = rand(rand(concl th1)) in
        let th2 = AP_TERM amp_op_real (num_mul tm1) in
          TRANS th1 th2
      else
        let th1 = INST [rand(rand l), m_var_num; rand r, n_var_num] mul_np in
        let tm1 = rand(rand(rand(concl th1))) in
        let th2 = AP_TERM neg_op_real (AP_TERM amp_op_real (num_mul tm1)) in
          TRANS th1 th2
    else
      if rator r = neg_op_real then
        let th1 = INST[rand l, m_var_num; rand(rand r), n_var_num] mul_pn in
        let tm1 = rand(rand(rand(concl th1))) in
        let th2 = AP_TERM neg_op_real (AP_TERM amp_op_real (num_mul tm1)) in
          TRANS th1 th2
      else
        let th1 = INST[rand l, m_var_num; rand r, n_var_num] mul_pp in
        let tm1 = rand(rand(concl th1)) in
        let th2 = AP_TERM amp_op_real (num_mul tm1) in
          TRANS th1 th2;;



(*
let amp x = mk_comb(amp_op_real, x);;
let negate x = mk_comb(neg_op_real, x);;

let x = num_of_string "398537263103485";;
let y = num_of_string "243089539573957";;


let xx = amp (mk_num x) and yy = amp (mk_num y);;
let xxx = amp (mk_numeral x) and yyy = amp (mk_numeral y);;


(* 1.800 *)
test 100 REAL_INT_MUL_CONV (mk_binop mul_op_real (negate xxx) yyy);;

(* 0.108 *)
test 100 my_real_int_mul_conv (mk_binop mul_op_real (negate xx) yy);;

(DEPTH_CONV NUM_TO_NUMERAL_CONV) (concl(REAL_BITS_MUL_CONV (mk_binop mul_op_real xx yy)))

*)