(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Linear Programming Link                                                                  *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-05-19                                                           *)
(* ========================================================================== *)

(* 
This file contains material that does not depend on the details of the LP.
  list processing functions,
  IO operations,
  glpk function calls.
*)

module Glpk_link  = struct

(*

needs new mktop on platforms that do not support dynamic loading of Str.

ocamlmktop unix.cma nums.cma str.cma -o ocampl
./ocampl

glpk needs to be installed, and glpsol needs to be found in the path.

needs lib.ml from HOL Light and flyspeck_lib.hl from Flyspeck.
*)


open Str;;
open List;;
let sprintf = Printf.sprintf;;

let (nextc,resetc) = 
  let counter = ref 0 in
  ((fun () ->
    counter:= !counter + 1;
    !counter),(fun () -> (counter :=0)));;


(* list operations *)
let maxlist0 xs = fold_right max xs 0;; (* NB: value is always at least 0 *)

let get_values key xs = 
  map snd (find_all (function k,_ -> (k=key)) xs);;

(*
let rec sort cmp lis =  (* from HOL Light lib.ml *)
  match lis with
    [] -> []
  | piv::rest ->
      let r,l = partition (cmp piv) rest in
      (sort cmp l) @ (piv::(sort cmp r));;
*)

let sort = Lib.sort;;

let (--) = Lib.(--);;

(*
let rec (--) = fun m n -> if m > n then [] else m::((m + 1) -- n);; (* from HOL Light lib.ml *)
*)

let up i = 0 -- (i-1);;

let rec rotateL i xs = 
  if i=0 then xs 
  else match xs with
    | x::xss -> rotateL ((i-1) mod length xs) (xss @ [x])
    | [] -> [];;

let rotateR i = rotateL (-i);;

let rotation xs = 
  let maxsz = maxlist0 (map length xs) in
  flatten (map (fun i -> map (rotateL i) xs) (up maxsz));;


(* 
   zip from Harrison's lib.ml. 
   List.combine causes a stack overflow :
   let tt = up 30000 in combine tt tt;;
   Stack overflow during evaluation (looping recursion?).

let rec zip l1 l2 =
  match (l1,l2) with
        ([],[]) -> []
      | (h1::t1,h2::t2) -> (h1,h2)::(zip t1 t2)
      | _ -> failwith "zip";;
*)

let zip = Lib.zip;;

let enumerate xs = zip (up (length xs)) xs;;

let whereis i xs = 
  let (p,_) = find (function _,j -> j=i) (enumerate xs) in
    p;;

let wheremod xs x = 
  let ys = rotation xs in 
   (whereis x ys) mod (length xs);;

(* example *)
wheremod [[0;1;2];[3;4;5];[7;8;9]] [8;9;7];;  (* 2 *)


let unsplit = Flyspeck_lib.unsplit;;

let nub = Flyspeck_lib.nub;;

let join_lines = Flyspeck_lib.join_lines;;

(*
let rec nub = function
  | [] -> []
  | x::xs -> x::filter ((!=) x) (nub xs);;

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

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


(* read and write *)

(*
let load_and_close_channel do_close ic = 
  let rec lf ichan a = 
    try
      lf ic (Pervasives.input_line ic::a)
    with End_of_file -> a in
    let rs = lf ic [] in
      if do_close then Pervasives.close_in ic else ();
      rev rs;;

let load_file filename = 
  let ic = Pervasives.open_in filename in load_and_close_channel true ic;;

*)

let load_and_close_channel = Flyspeck_lib.load_and_close_channel;;

let load_file = Flyspeck_lib.load_file;;

let save_stringarray filename xs = 
  let oc = open_out filename in
    for i=0 to length xs -1
    do
      Pervasives.output_string oc (nth xs i ^ "\n");
      done;
    close_out oc;;

let strip_archive filename =  (* strip // comments, blank lines, quotation marks etc. *)
  let (ic,oc) = Unix.open_process(sprintf "cat %s | grep -v '=' | grep -v 'list' | grep -v '^//' | grep -v '^$' | grep '^[^a-z/-]' | sed 's/\"[,;]*//g' | sed 's/_//g' " filename) in
  let s = load_and_close_channel false ic in
  let _ = Unix.close_process (ic,oc) in
    s;;

(* example of java style string from hypermap generator. *)
let pentstring = "13_150834109178 18 3 0 1 2 3 3 2 7 3 3 0 2 4 5 4 0 3 4 6 1 0 4 3 7 2 8 3 8 2 1 4 8 1 6 9 3 9 6 10 3 10 6 4 3 10 4 5 4 5 3 7 11 3 10 5 11 3 11 7 12 3 12 7 8 3 12 8 9 3 9 10 11 3 11 12 9 ";;

(* conversion to list.  e.g. convert_to_list pentstring *)

let convert_to_list  = 
  let split_sp=  Str.split (regexp " +") in
  let strip_ = global_replace (regexp "_") "" in
  let rec movelist n (x,a) = 
    if n=0 then (x,a) else match x with y::ys -> movelist (n-1) (ys, y::a) in
  let getone (x,a) = match x with
    | [] -> ([],a)
    | y::ys -> let (u,v) = movelist y (ys,[]) in (u,v::a) in 
  let rec getall (x,a) =
    if (x=[]) then (x,a) else getall (getone (x,a)) in
  fun s ->
    let h::ss = (split_sp (strip_ s)) in
    let _::ns = map int_of_string ss in
    let (_,a) = getall (ns,[]) in
     (h,rev (map rev a));;


(* Linear programming *)

let display_ampl ampl_datafile ampl_of_bb bb = (* for debugging *)
  let outs = open_out ampl_datafile in
  let _ = ampl_of_bb outs bb in
  let _ = close_out outs in
    Sys.command(sprintf "cat %s" ampl_datafile);;

(* model should name the optimal value "optival" *)

let solve_counter=ref 0;;

let solve com model glpk_outfile varname ampl_of_bb bb = 
  let (ic,oc) = Unix.open_process(com) in 
  let _ = ampl_of_bb oc bb in
  let _ = close_out oc in
  let _ = (solve_counter := !solve_counter + 1) in
  let inp = load_and_close_channel false ic in
  let _ = Unix.close_process (ic,oc) in
  (* test for no feasible solution.  There are two different messages. *) 
(*  let _ = Sys.command("cat "^ glpk_outfile) in (* debug *) *) 
  let com2 = sprintf "grep \"PROBLEM HAS NO.*FEASIBLE SOLUTION\" %s" glpk_outfile in
  let (ic,oc)  =Unix.open_process(com2) in
  let inp2 = load_and_close_channel false ic in
  let _ = Unix.close_process(ic,oc) in
    (inp2,inp);;

let solve_branch_f model glpk_outfile varname ampl_of_bb bb = 
  let com = sprintf "glpsol -m %s -d /dev/stdin | tee %s | grep '^%s' | sed 's/.val//' | sed 's/%s = //' "  model glpk_outfile varname varname in 
  solve com model glpk_outfile varname ampl_of_bb bb;;

let solve_dual_f model glpk_outfile varname ampl_of_bb bb = 
  let com = sprintf "glpsol -m %s -d /dev/stdin --simplex --exact --dual -w /tmp/dual.out --output /tmp/output.out | tee %s | grep '^%s' | sed 's/.val//' | sed 's/%s = //' "  model glpk_outfile varname varname in 
  solve com model glpk_outfile varname ampl_of_bb bb;;

let display_lp model ampl_datafile glpk_outfile ampl_of_bb bb = 
  let oc = open_out ampl_datafile in
  let _ = ampl_of_bb oc bb in
  let _ = close_out oc in
  let com = sprintf "glpsol -m %s -d %s | tee %s" model ampl_datafile glpk_outfile in
  let _ = Sys.command(com) in 
    ();;

let cpx_branch model cpxfile ampl_of_bb bb = (* debug *)
  let com = sprintf "glpsol -m %s --wcpxlp %s -d /dev/stdin | grep '^opti' | sed 's/optival = //' "  model cpxfile in 
  let (ic,oc) = Unix.open_process(com) in 
  let _ = ampl_of_bb oc bb in
  let _ = close_out oc in
  let _ = load_and_close_channel false ic in
  let _ = Unix.close_process (ic,oc) in
  sprintf "cplex file created of lp: %s" cpxfile;;

(* for debugging: reading optimal variables values from the glpk_outfile *)

let get_dumpvar glpk_outfile s = (* read variables from glpk_outfile *)
  let com = sprintf "grep '%s' %s | sed 's/^.*= //'  " s glpk_outfile in
  let (ic,oc) = Unix.open_process(com) in
  let _ = close_out oc in
  let inp = load_and_close_channel false ic in
  let _ = Unix.close_process(ic,oc) in
  inp;;
(* get_dumpvar "yn.0.*=";; *)

end;;