needs "../formal_lp/hypermap/ineqs/lp_gen_ineqs.hl";;
needs "../formal_lp/hypermap/ineqs/lp_approx_ineqs.hl";;
needs "../formal_lp/hypermap/ineqs/lp_ineqs_defs.hl";;
needs "../formal_lp/hypermap/ineqs/lp_ineqs_proofs-compiled.hl";;
needs "../formal_lp/hypermap/ineqs/lp_ineqs_proofs2-compiled.hl";;
needs "../formal_lp/hypermap/ineqs/lp_main_estimate-compiled.hl";;
needs "../formal_lp/hypermap/arith_link.hl";;

module Lp_ineqs = struct

open Lp_ineqs_proofs;;

type raw_lp_ineq = {
  name : string;
  tm : term;
  proof: thm option;
  std_only: bool;

type lp_ineq = {
  ineq_th : thm;
  pair_flag : bool;

let raw_ineq_list, add_raw_ineq, find_raw_ineq = 
  let table = ref [] in
    (fun () -> !table),
  (fun name std tm th -> 
     table := {name = name; tm = tm; proof = th; std_only = std} :: !table),
  (fun std_flag name -> find (fun x -> = name && x.std_only = std_flag) !table);;

(* Combine all nonlinear inequalities related to linear programs into one definition *)
let lp_ineqs_def =
  let check_lp_tags =
    let rec check tags =
      match tags with
	| Lp :: _ -> true
	| Tablelp :: _ -> true
	| Lp_aux _ :: _ -> true
	| h :: t -> check t
	| [] -> false in
      fun ineq -> check ineq.tags in
  let ineq_ids = ["6170936724"] in
  let lp_ineqs = filter (fun ineq -> check_lp_tags ineq or mem ineq.idv ineq_ids) !Ineq.ineqs in
  let lp_tms = setify (map (fun t -> t.ineq) lp_ineqs) in
  let lp_tm = end_itlist (curry mk_conj) lp_tms in
    new_definition (mk_eq (`lp_ineqs:bool`, lp_tm));;

let add_lp_ineqs_hyp =
  let imp_th = (UNDISCH o MATCH_MP EQ_IMP) lp_ineqs_def in
  let ths = CONJUNCTS imp_th in
    fun th ->
      itlist PROVE_HYP ths th;;

(* Replaces all general hypotheses with lp_cond *)
let add_lp_hyp =
  let lp_fan_ths = (CONJUNCTS o UNDISCH_ALL o MATCH_MP EQ_IMP o SPEC_ALL) Lp_ineqs_proofs.lp_fan in
  let lp_cond_ths = (CONJUNCTS o UNDISCH_ALL o MATCH_MP EQ_IMP o SPEC_ALL o INST_TYPE[`:num`, aty]) Lp_ineqs_proofs.lp_cond in
  let lp_main_estimate_ths = (CONJUNCTS o UNDISCH_ALL o MATCH_MP EQ_IMP o SPEC_ALL) Lp_main_estimate.lp_main_estimate in
    fun lp_ineq_flag th ->
      let th' = (UNDISCH_ALL o SPEC_ALL) th in
      let th0 = if (not lp_ineq_flag) or is_forall (concl th') or is_binary "ALL" (concl th') then th' else th in
      let th1 = itlist PROVE_HYP lp_fan_ths th0 in
      let th2 = itlist PROVE_HYP lp_cond_ths th1 in
	  let th3 = itlist PROVE_HYP lp_main_estimate_ths th2 in
		add_lp_ineqs_hyp th3;;

let parse_lp_ineq s type_hints =
  let hints = map (fun var, ty -> var, pretype_of_type ty) type_hints in
  let ptm, l = (parse_preterm o lex o explode) s in
    if l = [] then
      (term_of_preterm o retypecheck hints) ptm
      failwith "Unparsed input following term";;

let add_lp_ineq_str (name, std_flag, s_tm, th) =
  let tm = parse_lp_ineq s_tm ["H", `:(A)hypermap`; "V", `:C->bool`; "node_mod", `:A->C`] in
  let proof = match th with
    | None -> None
    | Some th -> Some (PURE_REWRITE_RULE[GSYM IMP_IMP] (add_lp_hyp true th)) in
    add_raw_ineq name std_flag tm proof;;

let mk_lp_ineq =
  let subst_list = [
    `dart (H:(real^3#real^3)hypermap)`, `dart_of_fan (V:real^3->bool,E)`;
    `H:(real^3#real^3)hypermap`, `hypermap_of_fan (V:real^3->bool,E)`;
    `face_map (H:(real^3#real^3)hypermap)`, `f_fan_pair_ext (V:real^3->bool,E)`;
    `azim_mod:real^3#real^3->real`, `azim_dart (V:real^3->bool,E)`;
    `azim2_mod:real^3#real^3->real`, `azim2_fan (V:real^3->bool,E)`;
    `azim3_mod:real^3#real^3->real`, `azim3_fan (V:real^3->bool,E)`;
    `rhazim_mod:real^3#real^3->real`, `rhazim_fan (V:real^3->bool,E)`;
    `rhazim2_mod:real^3#real^3->real`, `rhazim2_fan (V:real^3->bool,E)`;
    `rhazim3_mod:real^3#real^3->real`, `rhazim3_fan (V:real^3->bool,E)`;
    `sol_mod:(real^3#real^3->bool)->real`, `sol_fan (V:real^3->bool,E)`;
    `tau_mod:(real^3#real^3->bool)->real`, `tau_fan (V:real^3->bool,E)`;
    `y1_mod:real^3#real^3->real`, `y1_fan`;
    `y2_mod:real^3#real^3->real`, `y2_fan`;
    `y3_mod:real^3#real^3->real`, `y3_fan (V,E)`;
    `y4_mod:real^3#real^3->real`, `y4_fan (V,E)`;
    `y5_mod:real^3#real^3->real`, `y5_fan (V,E)`;
    `y6_mod:real^3#real^3->real`, `y6_fan`;
    `y7_mod:real^3#real^3->real`, `y7_fan (V,E)`;
    `y8_mod:real^3#real^3->real`, `y8_fan (V,E)`;
    `y9_mod:real^3#real^3->real`, `y9_fan (V,E)`;
    `y4'_mod:real^3#real^3->real`, `y4'_fan (V,E)`;
    `ye_mod:real^3#real^3->real`, `ye_fan`;
    `yn_mod:real^3->real`, `yn_fan`;
  ] in
    fun ineq_th ->
      let proof = PURE_REWRITE_RULE[GSYM IMP_IMP] (add_lp_hyp true ineq_th) in
      let tm0 = concl proof in
      let tm1 = subst subst_list tm0 in
	tm1, proof;;

let add_lp_ineq_th (name, std_flag, ineq_th) =
  let tm1, proof = mk_lp_ineq ineq_th in
    add_raw_ineq name std_flag tm1 (Some proof);;

let gen_raw_ineq_data_str name std_flag str =
  let tm = parse_lp_ineq str ["H", `:(A)hypermap`; "V", `:C->bool`; "node_mod", `:A->C`] in
    {name = name; tm = tm; proof = None; std_only = std_flag};;

let gen_raw_ineq_data name std_flag ineq_th =
  let tm1, proof = mk_lp_ineq ineq_th in
    {name = name; tm = tm1; proof = Some proof; std_only = std_flag};;


(* Generates a general form of an inequality *)
let generate_ineq0 ineq =
  let th0 = Lp_gen_ineqs.generate_ineq in
  let th1 = add_lp_hyp true th0 in
  let proof = 
    match ineq.proof with
      | Some th -> th
      | None -> TRUTH in
    PROVE_HYP proof th1;;

let generate_ineq1 =
let power_th = 
prove(`!f (x:A). (f POWER 2) x = f (f x) /\ (f POWER 3) x = f (f (f x))`,
REWRITE_TAC[Hypermap.POWER_2; Hypermap.THREE; Hypermap.POWER; o_THM]) in let mk_list_th th = let tm, proof = mk_lp_ineq th in generate_ineq0 {name = "tmp";
std_only = false; tm = tm; proof = Some proof} in let strip_ALL th = let ltm, set_tm = dest_comb (concl th) in let p_tm = rand ltm in let var_tm, _ = dest_abs p_tm in let th1 = (BETA_RULE o SPEC var_tm o PURE_REWRITE_RULE[GSYM ALL_MEM]) th in let mem_tm = (fst o dest_imp o concl) th1 in UNDISCH th1, (var_tm, mem_tm) in let th_rule = (UNDISCH_ALL o INST_TYPE [`:num`, aty; `:num`, `:D`; `:real^3`, `:C`] o SPEC_ALL o REWRITE_RULE[GSYM IMP_IMP; RIGHT_IMP_FORALL_THM]) in let def_ths = let defs = map (fst o strip_ALL o mk_list_th) [y1_def; y2_def; y3_def; y4_def; y5_def; y6_def; y9_def] in let r = (fst o strip_ALL o add_lp_hyp true o REWRITE_RULE[GSYM IMP_IMP]) in let extra_defs = map r [ y8_list_def; y4'_list_def; y4'_list_f_def; y4'_list_inv_f_def; y4'_list_ff_def; y4'_list_fff_def; ] in extra_defs @ defs in let mem_ths = [ `MEM (d:num#num) (list_of_darts3 L)`, th_rule Lp_gen_theory.list_of_darts3_subset; `MEM (d:num#num) (list_of_darts4 L)`, th_rule Lp_gen_theory.list_of_darts4_subset; `MEM (d:num#num) (list_of_darts5 L)`, th_rule Lp_gen_theory.list_of_darts5_subset; `MEM (d:num#num) (list_of_darts6 L)`, th_rule Lp_gen_theory.list_of_darts6_subset; ] in let rec simplify tm = if is_imp tm then let ltm, q_tm = dest_comb tm in let imp_tm, p_tm = dest_comb ltm in let p_tm, q_tm = dest_imp tm in let p_th = (PURE_REWRITE_CONV def_ths THENC PURE_REWRITE_CONV[power_th]) p_tm in let q_th = simplify q_tm in MK_COMB (AP_TERM imp_tm p_th, q_th) else REFL tm in fun simplify_all_flag ineq -> let th1 = generate_ineq0 ineq in let th2, (var_tm, mem_tm) = strip_ALL th1 in let eq_th = if simplify_all_flag then (PURE_REWRITE_CONV def_ths THENC PURE_REWRITE_CONV[power_th]) (concl th2) else simplify (concl th2) in let th3 = EQ_MP eq_th th2 in let th4 = try let mem_th = assoc mem_tm mem_ths in PROVE_HYP mem_th th3 with Failure _ -> th3 in let th5 = (GEN var_tm o DISCH mem_tm) th4 in PURE_REWRITE_RULE[ALL_MEM] th5;; let generate_ineq = generate_ineq1 false;; let add_lp_list_ineq, find_ineq = let ineq_table = Array.init 8 (fun i -> Hashtbl.create 10) in let std_ineq_table = Array.init 8 (fun i -> Hashtbl.create 10) in let add std_flag i pair_flag name ineq_th = let table = if std_flag then std_ineq_table.(i) else ineq_table.(i) in Hashtbl.add table name {ineq_th = ineq_th; pair_flag = pair_flag} in
prove(`!n. DECIMAL n 1 = &n`,
REWRITE_TAC[DECIMAL; REAL_DIV_1]) in let pos_thms = let inst = INST[`V:real^3->bool,E:(real^3->bool)->bool`, `fan:(real^3->bool)#((real^3->bool)->bool)`] in map inst Lp_ineqs_def.list_var_pos in let rec rewrite_num_conv real_flag tm = match tm with | Var _ -> REFL tm | Const _ -> REFL tm | Abs (v_tm, b_tm) -> ABS v_tm (rewrite_num_conv real_flag b_tm) | Comb (Const ("NUMERAL", _), _) -> Arith_nat.NUMERAL_TO_NUM_CONV tm | Comb (Const ("real_of_num", _) as ltm, rtm) -> if real_flag then AP_TERM ltm (rewrite_num_conv real_flag rtm) else REFL tm | Comb (Comb (Const ("DECIMAL", _), _), _) -> REFL tm | Comb (ltm, rtm) -> MK_COMB (rewrite_num_conv real_flag ltm, rewrite_num_conv real_flag rtm) in let rewrite_num ineq_th = let th1 = PURE_REWRITE_RULE[DECIMAL_INT] ineq_th in let imp_flag = (is_imp o snd o dest_abs o lhand o concl) th1 in if imp_flag then let th2 = PURE_REWRITE_RULE[IMP_IMP] th1 in let th3 = CONV_RULE ((LAND_CONV o ABS_CONV o RAND_CONV) (rewrite_num_conv true)) th2 in let th4 = CONV_RULE ((LAND_CONV o ABS_CONV o LAND_CONV) (rewrite_num_conv false)) th3 in PURE_REWRITE_RULE[GSYM IMP_IMP] th4 else CONV_RULE (rewrite_num_conv true) th1 in (* add_lp_list_ineq *) (fun (name, std_only, list_ineq_th) -> let approx_ths, neg_approx_ths = Lp_approx_ineqs.generate_ineqs pos_thms [3;4;5;6;7] list_ineq_th in let set_name = (fst o dest_const o rator o rand o concl o hd) approx_ths in let pair_flag, approx_ths, neg_approx_ths = if set_name = "list_dart_pairs" then let r = PURE_REWRITE_RULE[Lp_gen_theory.ALL_list_dart_pairs_split; BETA_THM; FST; SND] in true, map r approx_ths, map r neg_approx_ths else false, approx_ths, neg_approx_ths in let approx_ths = zip (3--7) approx_ths in let neg_approx_ths = if (neg_approx_ths = []) then [] else zip (3--7) neg_approx_ths in let r = rewrite_num in if std_only then let _ = map (fun (i, t) -> add true i pair_flag name (r t)) approx_ths in let _ = map (fun (i, t) -> add true i pair_flag (name^"_neg") (r t)) neg_approx_ths in () else let _ = map (fun (i, t) -> add false i pair_flag name (r t)) approx_ths in let _ = map (fun (i, t) -> add false i pair_flag (name^"_neg") (r t)) neg_approx_ths in ()), (* find_ineq *) (fun std_flag precision name -> if std_flag then try Hashtbl.find std_ineq_table.(precision) name with Not_found -> Hashtbl.find ineq_table.(precision) name else Hashtbl.find ineq_table.(precision) name);;
(* Generates all list inequalities from raw inequalities *) let process_raw_ineqs = let report s = Format.print_string s; Format.print_newline(); Format.print_flush() in let counter = ref 0 and total = ref 0 in let process_ineq ineq = let _ = counter := !counter + 1 in let _ = report (sprintf "Processing: %s (%d / %d)" !counter !total) in let th = generate_ineq ineq in add_lp_list_ineq (, ineq.std_only, th) in fun () -> let ineqs = raw_ineq_list() in let _ = counter := 0 in let _ = total := length ineqs in let _ = map process_ineq (raw_ineq_list()) in ();; end;;