needs "../formal_lp/hypermap/ineqs/lp_ineqs_defs.hl";;
needs "../formal_lp/hypermap/ineqs/lp_gen_theory-compiled.hl";;

module Lp_gen_ineqs = struct

open Lp_ineqs_def;;
open Hypermap_and_fan;;
open Hypermap_iso;;
open List_hypermap;;
open Lp_gen_theory;;

(* mod-file variables and definitions *)

let var_inst_list =
  let sets =
      "dart", `:real^3#real^3`;
      "face", `:real^3#real^3->bool`;
      "node", `:real^3`;
    ] in
  let mk_mod name set = mk_var (name, mk_fun_ty (assoc set sets) `:real`) in
      `hypermap_of_fan (V,E)`, `H:(real^3#real^3)hypermap`;
      `FST:real^3#real^3->real^3`, `node_mod:real^3#real^3->real^3`;
      `azim_dart (V,E)`, mk_mod "azim_mod" "dart";
      `azim2_fan (V,E)`, mk_mod "azim2_mod" "dart";
      `azim3_fan (V,E)`, mk_mod "azim3_mod" "dart";
      `rhazim_fan (V,E)`, mk_mod "rhazim_mod" "dart";
      `rhazim2_fan (V,E)`, mk_mod "rhazim2_mod" "dart";
      `rhazim3_fan (V,E)`, mk_mod "rhazim3_mod" "dart";
      `ln_fan`, mk_mod "ln_mod" "node";
      `yn_fan`, mk_mod "yn_mod" "node";
      `rho_fan`, mk_mod "rho_mod" "node";
      `ye_fan`, mk_mod "ye_mod" "dart";
      `y1_fan`, mk_mod "y1_mod" "dart";
      `y2_fan`, mk_mod "y2_mod" "dart";
      `y3_fan (V,E)`, mk_mod "y3_mod" "dart";
      `y4_fan (V,E)`, mk_mod "y4_mod" "dart";
      `y5_fan (V,E)`, mk_mod "y5_mod" "dart";
      `y6_fan`, mk_mod "y6_mod" "dart";
      `y8_fan (V,E)`, mk_mod "y8_mod" "dart";
      `y9_fan (V,E)`, mk_mod "y9_mod" "dart";
      `y4'_fan (V,E)`, mk_mod "y4'_mod" "dart";
      `sol_fan (V,E)`, mk_mod "sol_mod" "face";
      `tau_fan (V,E)`, mk_mod "tau_mod" "face";


(* For a term in the form `!x. x IN set H ==> P x` returns a theorem
   hyp_iso g (G,H), !x. x IN set H ==> P x |- !y. y IN set G ==> P (g y) *)
let get_iso_thm =
  let iso_list0 =
      `darts_k 6 (H:(A)hypermap)`, spec_var_th iso_darts_k_trans 0 `6`;
      `darts_k 5 (H:(A)hypermap)`, spec_var_th iso_darts_k_trans 0 `5`;
      `darts_k 4 (H:(A)hypermap)`, spec_var_th iso_darts_k_trans 0 `4`;
      `darts_k 3 (H:(A)hypermap)`, spec_var_th iso_darts_k_trans 0 `3`;
      `dart (H:(A)hypermap)`, iso_dart_trans;
      `face_set (H:(A)hypermap)`, iso_face_trans;
      `node_set (H:(A)hypermap)`, iso_node_trans;
      `V:C->bool`, bij_trans;
    ] in
  let cty = `:C` in
    fun ineq ->
      let x_tm, tm = dest_forall ineq in
      let x_ty =
	try (fst o dest_fun_ty o type_of) x_tm with Failure _ -> type_of x_tm in
      let ty_list = [x_ty, aty; x_ty, cty] in
      let iso_list = map (fun tm, th -> inst ty_list tm, INST_TYPE ty_list th) iso_list0 in
      let set, p_tm' = dest_binary "==>" tm in
      let set_th = assoc (rand set) iso_list in
      let p_tm = mk_abs (x_tm, p_tm') in
      let p_var = mk_var ("P", type_of (rand set)) in
	BETA_RULE (INST[p_tm, p_var] th1), ty_list;;

(* For an inequality term returns an isomorphism theorem *)
let build_iso_th =
  let ths0 = [
    th_rule components_iso_image;
    th_rule hyp_iso_comm_special;
    th_rule hyp_iso_inv_comm;
    th_rule card_face_iso;
    th_rule card_face_dart_iso;
    th_rule sum_node_iso;
    th_rule sum_face_iso;
  ] in
  let sub_ths0 = [
    `d IN darts_k 3 (G:(B)hypermap)`, (INST[`3`, `k:num`] o th_rule) darts_k_subset;
    `d IN darts_k 4 (G:(B)hypermap)`, (INST[`4`, `k:num`] o th_rule) darts_k_subset;
    `d IN darts_k 5 (G:(B)hypermap)`, (INST[`5`, `k:num`] o th_rule) darts_k_subset;
    `d IN darts_k 6 (G:(B)hypermap)`, (INST[`6`, `k:num`] o th_rule) darts_k_subset;
  ] in

    fun ineq ->
      let iso_trans_th, ty_list = get_iso_thm ineq in
      let th0 = UNDISCH_ALL (PURE_REWRITE_RULE[GSYM IMP_IMP] iso_trans_th) in
      let gen_var, rtm = dest_forall(concl th0) in
      let ths = map (INST_TYPE ty_list) ths0 and
	  sub_ths = map (fun tm, th -> inst ty_list tm, INST_TYPE ty_list th) sub_ths0 in
      let ants = lhand rtm in
      let th1 = UNDISCH (SPEC_ALL th0) in
	(* General isomorphism rewrites *)
      let th2 = PURE_REWRITE_RULE ths th1 in
      let th3 =
	  let sub_th = assoc ants sub_ths in
	    PROVE_HYP sub_th th2
	with Failure _ -> th2 in
	GEN gen_var (DISCH ants th3);;

let build_list_th =
  let th_rule = (UNDISCH_ALL o INST_TYPE [`:num`, aty; `:num`, `:D`; `:real^3`, `:C`] o 
  (* |- !d. d IN set_of_list s ==> P d <=> !d. MEM d s ==> P d *)
  let ths_all = map th_rule 
    ] in

  let ths_more =
    th_rule card_face_eq_length_find_face;
    th_rule card_set_of_list_face;
    th_rule card_set_of_list_node;
    th_rule fst_choice_of_list_node;
    UNDISCH_ALL (ISPEC `L:((num)list)list` components_hypermap_of_list);
    th_rule e_list_ext_eq_e_list;
    th_rule fst_iso_trans;
  ] in

  let ths_mem =
      `MEM (d:num#num) (list_of_darts3 L)`, th_rule list_of_darts3_subset;
      `MEM (d:num#num) (list_of_darts4 L)`, th_rule list_of_darts4_subset;
      `MEM (d:num#num) (list_of_darts5 L)`, th_rule list_of_darts5_subset;
      `MEM (d:num#num) (list_of_darts6 L)`, th_rule list_of_darts6_subset;
    ] in

    fun iso_th ->
      (* G -> hypermap_of_list (L:((num)list)list) *)
      let s1 = INST_TYPE [`:real^3#real^3`, aty; `:num#num`, bty; `:real^3`, `:C`; `:num`, `:D`] iso_th in
      let s2 = INST[`hypermap_of_list (L:((num)list)list)`, `G:(num#num)hypermap`; `elements_of_list L:num->bool`, `R:num->bool`] s1 in
	(* Convert conditions in the form !d. d IN set_of_list s to !d. MEM d s *)
      let s3 = PURE_REWRITE_RULE ths_all s2 in
      let gen_var2, rtm = dest_forall (concl s3) in
      let ants2 = lhand rtm in
      let s4 = UNDISCH (SPEC_ALL s3) in
	(* Instantiate all variables *)
      let s5 = INST var_inst_list s4 in
	(* Additional rewrites *)
      let s6 = PURE_REWRITE_RULE ths_more s5 in
      let s7 =
	  let mem_th = assoc ants2 ths_mem in
	    PROVE_HYP mem_th s6
	with Failure _ -> s6 in
      let s8 = GEN gen_var2 (DISCH ants2 s7) in
      let s9 = PURE_REWRITE_RULE list_var_rewrites s8 in
      let s10 = PURE_REWRITE_RULE[ALL_MEM] s9 in
	(* Rewrite the main inequality hypothesis with the COMPONENTS_HYPERMAP_OF_FAN theorem *)
      let gen_hyp = find is_forall (hyp s10) in
      let eq_th = REWRITE_CONV[UNDISCH_ALL (ISPECL [`V:real^3->bool`; `E:(real^3->bool)->bool`] COMPONENTS_HYPERMAP_OF_FAN)] gen_hyp in
      let imp_th = if (rand (concl eq_th) = `T`) then EQT_ELIM eq_th else UNDISCH (MATCH_MP EQ_IMP (SYM eq_th)) in
	PROVE_HYP imp_th s10;;

let generate_ineq ineq_tm =
  let th1 = build_iso_th ineq_tm in
    build_list_th th1;;


open Lp_gen_ineqs;;

let test_ineq1 = `!d. d IN dart (H:(A)hypermap) ==> rhazim3_mod d <= pi + sol0`;;
let test_ineq2 = `!f. f IN face_set (H:(A)hypermap) ==> sol_mod f <= &4 * pi`;;
let test_ineq3 = `!f. f IN face_set (H:(A)hypermap) ==> (CARD f = 5 ==>
    sum f azim_mod = sol_mod f + &3 * pi)`;;
let test_ineq4 = `!n. n IN node_set (H:(A)hypermap) ==> sum n azim_mod = &2 * pi`;;
let test_ineq5 = `!x. x IN (V:C->bool) ==> ln_mod x = (#2.52 - yn_mod x) / #0.52`;;
let edge_sym = `!d. d IN dart (H:(A)hypermap) ==> ye_mod d = ye_mod (edge_map H d):real`;;
let y1_def = `!d. d IN dart (H:(A)hypermap) ==> y1_mod d = yn_mod (node_mod d:C):real`;;
let y2_def = `!d. d IN dart (H:(A)hypermap) ==> y2_mod d = yn_mod (node_mod (face_map H d):C):real`;;
let y8_def = `!d. d IN dart (H:(A)hypermap) ==> y8_mod d = y5_mod (inverse (face_map H) d):real`;;
let rhazim_sum = `!n. n IN node_set (H:(A)hypermap) ==> sum n rhazim_mod = &2 * pi * rho_mod (node_mod (CHOICE n):C)`;;
let test_ineq6 = `!d. d IN darts_k 4 (H:(A)hypermap) ==>
        (((tau_mod (face H d)) + ((#4.72 * (azim_mod d)) - #6.248)) - #0.0) >= #0.0`;;
let test_ineq7 = `!d. d IN dart (H:(A)hypermap) ==> CARD (face H d) = 3 ==> y4_mod d = y8_mod d:real`;;
let test_ineq8 = `!d. d IN dart (H:(A)hypermap) ==> &2 <= y4'_mod d`;;
let test_ineq9 = `!d. d IN darts_k 3 (H:(A)hypermap) ==> y4_mod d = ye_mod (face_map H d):real`;;
let test_ineq10 = `!d. d IN darts_k 3 (H:(A)hypermap) ==> ye_mod d = ye_mod (edge_map H d):real`;;
let test_ineq11 = `!d. d IN darts_k 5 (H:(A)hypermap) ==> tau_mod (face H d) >= #0.4819`;;
let test_ineq12 = `!d. d IN dart (H:(A)hypermap) ==> 3 < CARD (face H d) ==> #2.52 <= y4_mod d`;;

generate_ineq test_ineq1;;
generate_ineq test_ineq2;;
generate_ineq test_ineq3;;
generate_ineq test_ineq4;;
generate_ineq test_ineq5;;
generate_ineq test_ineq6;;
generate_ineq test_ineq7;;
generate_ineq test_ineq8;;
generate_ineq test_ineq9;;
generate_ineq test_ineq10;;
generate_ineq test_ineq11;;
generate_ineq test_ineq12;;

generate_ineq edge_sym;;
generate_ineq y1_def;;
generate_ineq y2_def;;
generate_ineq y8_def;;
generate_ineq rhazim_sum;;