(* ========================================================================== *)
(* FLYSPECK - CODE FORMALIZATION                                              *)
(*                                                                            *)
(* Software: Graph Generator                                                     *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-09-28                                                           *)
(* ========================================================================== *)

(* Code to control the graph generator *)

module Graph_control = struct

let graph_dir = flyspeck_dir ^ "/../graph_generator";;
let graph_src = graph_dir ^ "/src";;
let graph_classes = graph_dir ^ "/classes";;

let graph_out = Filename.temp_file "graph_out" ".txt";; (*  "/tmp/graph_out.txt";; *)
let render_out = Filename.temp_file "render_out" ".txt";; (* "/tmp/render_out.txt";; *)

let tmp_graph_properties = Filename.temp_file "graph" ".properties";;
let tmp_graph_properties = "/tmp/graph.properties";;  (* Still hard-wired into java code *)

(* duplicated code *)
let unsplit d f = function
  | (x::xs) ->  List.fold_left (fun s t -> s^d^(f t)) (f x) xs
  | [] -> "";;

let join_comma  = unsplit "," (fun x-> x);;

let join_lines  = unsplit "\n" (fun x-> x);;

let join_space  = unsplit " " (fun x-> x);;

let output_filestring tmpfile a = 
  let outs = open_out tmpfile in
  let _ = try (Printf.fprintf outs "%s" a) 
  with _ as t -> (close_out outs; raise t) in
   close_out outs ;;

(* duplicated code *)



type graph_generator_properties = 
  { 
    properties_id : string;
    ignore_archive : bool;
    exclude_degree2 : bool;
    exclude_pent_qrtet : bool;
    exclude_2_in_quad : bool;
    exclude_1_in_tri : bool;
    vertex_count_min : int;
    vertex_count_max : int;
    node_card_max : int;
    node_card_max_at_exceptional_vertex : int;
    squander_target : int;
    score_target : int;
    table_weight_d : int list;
    table_weight_a : (int*int) list;
    table_weight_b : (int*int*int) list;
  };;  

let string_of_properties (x:graph_generator_properties) =
  let p = Printf.sprintf in
  let b t = if t then "true" else "false" in
  let weightd = zip (0-- (List.length x.table_weight_d -1)) (x.table_weight_d) in
    join_lines 
      ([
	 p"#This properties files is machine generated";
	 p"#Graph Generator %s" (flyspeck_version());
	 p"#Properties file: %s" (x.properties_id);
	 p"ignoreArchive=%s" (b x.ignore_archive);
	 p"excludeDegree2=%s" (b x.exclude_degree2);
	 p"excludePentQRTet=%s" (b x.exclude_pent_qrtet);
	 p"exclude2inQuad=%s" (b x.exclude_2_in_quad);
	 p"exclude1inTri=%s" (b x.exclude_1_in_tri);
	 p"vertexCountMin=%d" x.vertex_count_min;
	 p"vertexCountMax=%d" x.vertex_count_max;
	 p"nodeCardMax=%d" x.node_card_max;
	 p"nodeCardMaxAtExceptionalVertex=%d" x.node_card_max_at_exceptional_vertex;
	 p"squanderTarget=%d" x.squander_target;
	 p"scoreTarget=%d" x.score_target;
	 (join_lines (map (fun (m,n) -> p"tableWeightD%d=%d" m n) weightd));
	 (join_lines (map (fun (m,n) -> p"tableWeightA%d=%d" m n) x.table_weight_a));
	 (join_lines (map (fun (a,b,v) -> p"tableWeightB%d%d=%d" a b v) x.table_weight_b))
       ]);;

let flyspeck_properties = 
  {
    properties_id = "flyspeck properties";
    ignore_archive=true;
    exclude_degree2=true;
    exclude_pent_qrtet=true; (* because degrees must be at least 2 *)
    exclude_2_in_quad=false;
    exclude_1_in_tri=false;
    vertex_count_min=13;
    vertex_count_max=15;
    node_card_max=7;
    node_card_max_at_exceptional_vertex=6;
    squander_target=15410;
    score_target= -1;
    table_weight_d = [0;0;0;0;2060;4819;7120;15410;15410];
    table_weight_a = [(5,6300)];
    (* exclude b02 because degrees are at least 3.  b50 is a special calculation *)
    table_weight_b = [(0,3,6180);(0,4,9700);(1,2,6560);(1,3,6180);
		      (2,1,7970);(2,2,4120);(2,3,12851);
		      (3,1,3110);(3,2,8170);(4,0,3470);(4,1,3660);
		      (5,0,400);(5,1,11360);(6,0,6860);(7,0,14500);];
  };;

let bauer_nipkow_deprecated_properties = 
  {
    properties_id = "flyspeck properties from the Bauer Nipkow Isabelle classification Fall 2010."^
      " table_weight_d is out of date in the 7578 entry." ^
      " This should produce (9,1105,15991,1657) graphs in the pass with n=3,4,5,6, respectively";
    ignore_archive=true;
    exclude_degree2=true;
    exclude_pent_qrtet=true; (* because degrees must be at least 2 *)
    exclude_2_in_quad=false;
    exclude_1_in_tri=false;
    vertex_count_min=13;
    vertex_count_max=15;
    node_card_max=7;
    node_card_max_at_exceptional_vertex=6;
    squander_target=15410;
    score_target= -1;
    table_weight_d = [0;0;0;0;2060;4819;7578;15410;15410];
    table_weight_a = [(5,6300)];
    (* exclude b02 because degrees are at least 3.  b50 is a special calculation *)
    table_weight_b = [(0,3,6180);(0,4,9700);(1,2,6560);(1,3,6180);
		      (2,1,7970);(2,2,4120);(2,3,12851);
		      (3,1,3110);(3,2,8170);(4,0,3470);(4,1,3660);
		      (5,0,400);(5,1,11360);(6,0,6860);(7,0,14500);];
  };;

let kepler98_deprecated_properties = 
  {
    properties_id = "values from the original 1998 proof of the Kepler conjecture, but relaxed to eliminate score";
    ignore_archive=true;
    exclude_degree2=true;
    exclude_pent_qrtet=true; 
    exclude_2_in_quad=true;
    exclude_1_in_tri=true;
    vertex_count_min=10;
    vertex_count_max=100;
    node_card_max=6;
    node_card_max_at_exceptional_vertex=5;
    squander_target=14800;
    score_target= -1;
    table_weight_d = [0;0;0;0;2378;4896;7414;9932;10916];
    table_weight_a = [(3,1400);(4,1500)];
    table_weight_b = [(0,3,7135);(0,4,10649);(1,2,6950);(1,3,7135);
		      (2,1,8500);(2,2,4756);(2,3,12981);
		      (3,1,3642);(3,2,8334);(4,0,4139);(4,1,3781);
		      (5,0,550);(5,1,11220);(6,0,6339)];
  };;



let fejes_toth_contact_conjecture_properties = 
  {
    properties_id = "Fejes Toth's Contact Conjecture";
    ignore_archive=true;
    exclude_degree2=false;
    exclude_pent_qrtet=true; 
    exclude_2_in_quad=true;
    exclude_1_in_tri=true;
    vertex_count_min=12;
    vertex_count_max=12;
    node_card_max=4;
    node_card_max_at_exceptional_vertex=4;
    squander_target=1541;
    score_target= -1;
    (* table_weight_d = [0;0;0;0;206;480;756;1031;1306];  change sep 23, 2012 *)
    table_weight_d = [0;0;0;0;206;476;746;1016;1286]; 
    table_weight_a = [(0,0);(1,0);(2,0);(3,0)];
    table_weight_b = [(0,3,618);(1,3,618);(2,2,412)];
  };;

let mclaughlin_dodecaheral_conjecture_properties=
{
  properties_id="McLaughlin's Dodecahedral Theorem";
  ignore_archive=true;
  exclude_degree2=false;
  exclude_pent_qrtet=true;
  exclude_2_in_quad=true;
  exclude_1_in_tri=true;
  vertex_count_min=13;
  vertex_count_max=100;
  node_card_max=6;
  node_card_max_at_exceptional_vertex=5;
  squander_target=178;
  score_target= -1;
  table_weight_d = [0;0;0;0;31;76;121;166;200];
  table_weight_a = [(3,0);(4,16)];
  table_weight_b = [(0,3,93);(0,4,125);(1,2,91);(1,3,93);
		    (2,1,133);(2,2,62);(3,1,43);(3,2,118);(4,0,53);(4,1,31);(5,0,4)];
};;

(* deprecated 
let set_properties file_name = 
    Sys.command(Printf.sprintf "cd %s; cp %s /tmp/graph.properties" graph_dir file_name);;
*)

let set_prop_file (x:graph_generator_properties) =
  output_filestring tmp_graph_properties (string_of_properties x);;

let compile () = 
  Sys.command(Printf.sprintf "cd %s; javac -d ../classes graph/Generator.java " graph_src);;

let execute () = 
  Sys.command(Printf.sprintf "cd %s; java -Xms300m -Xmx1g graph/Generator | tee %s" graph_classes graph_out);;

let run(x:graph_generator_properties)=
  let _ = set_prop_file (x) in 
  let _ = compile() in
  let _ = execute() in
    "execution complete.  Results tee'd to " ^ graph_out;;

(* rendering *)

let compile_render () = 
  Sys.command(Printf.sprintf "cd %s; javac -d ../classes render/Gendot.java " graph_src);;

let compile_gentikz () = 
  Sys.command(Printf.sprintf "cd %s; javac -d ../classes render/Gentikz.java " graph_src);;

let execute_render s = 
  let _ = Sys.command(Printf.sprintf "cd %s; java render/Gendot \"%s\" |tee %s" graph_classes s render_out) in
    "execution complete. Results tee'd to " ^ render_out;;

let execute_g prm s = 
  let _ = Sys.command(Printf.sprintf "cd %s; java render/%s \"%s\" |tee %s" graph_classes prm s render_out) in
    "execution complete. Results tee'd to " ^ render_out;;

let execute_gendot = execute_g "Gendot";;

let execute_gentikz = execute_g "Gentikz";;

let example_graph = "0 24 3 0 1 2 3 0 2 3 3 3 2 4 3 4 2 1 3 4 1 5 3 5 1 0 3 5 0 6 3 6 0 7 3 7 0 3 3 7 3 8 3 8 3 9 3 9 3 4 3 9 4 10 3 10 4 5 3 10 5 11 3 11 5 6 3 11 6 12 3 12 6 7 3 12 7 8 3 12 8 13 3 13 8 9 3 11 12 13 3 10 11 13 3 13 9 10 ";;

let example_render() = 
  let _ = compile_render() in
    execute_render example_graph;;

let example_gentikz() = 
  let _ = compile_gentikz() in
    execute_gentikz example_graph;;

let execute() = 
  let _ = example_render() in
  let _ = example_gentikz() in
    run(flyspeck_properties);;


end;;