(* ========================================================================== *)
(* FLYSPECK - CODE BUILD                                                      *)
(*                                                                            *)
(* Chapter: All Chapters                                                      *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2012-04-12                                                           *)
(* ========================================================================== *)


(* Build of the computational parts of the Flyspeck Project *)

flyspeck_needs "strictbuild.hl";;
flyspeck_needs "general/flyspeck_lib.hl";;

(* Tikz *)
flyspeck_needs  "../kepler_tex/tikz/tikz.ml";;

(* graph generator *)
flyspeck_needs ("/../graph_generator/graph_control.hl");;

(* glpk *)
flyspeck_needs "nonlinear/parse_ineq.hl";;
flyspeck_needs "../glpk/glpk_link.ml";;
flyspeck_needs "../glpk/minorlp/tame_table.ml";;
flyspeck_needs "../glpk/minorlp/OXLZLEZ.ml";;
flyspeck_needs "../glpk/tame_archive/lpproc.ml";;
flyspeck_needs "../glpk/sphere.ml";;
flyspeck_needs "../glpk/tame_archive/hard_lp.ml";;
flyspeck_needs "../glpk/tame_archive/scaffolding.hl";;

flyspeck_needs "../glpk/tame_archive/build_lp.hl";;

(* formal lp see formal_lp/README.txt for installation instructions. *)
(*
needs "../formal_lp/hypermap/verify_all.hl";;
let result = Verify_all.verify_all();;
*)

(* nonlinear inequalities needs *)
flyspeck_needs   "nonlinear/ineq.hl";;
flyspeck_needs   "nonlinear/lemma.hl";; (* indep of Ineq *)
flyspeck_needs   "nonlinear/functional_equation.hl";; (* indep of Ineq *)
flyspeck_needs   "nonlinear/parse_ineq.hl";;
flyspeck_needs   "nonlinear/optimize.hl";;
flyspeck_needs   "nonlinear/auto_lib.hl";;
flyspeck_needs "../glpk/sphere.ml";;
flyspeck_needs "nonlinear/check_completeness.hl";;
flyspeck_needs "nonlinear/scripts.hl";;




module Computational_build = struct

  open Flyspeck_lib;;

(* tex generation Tikz figures. /tmp/x.txt *)

  let tikz_out = Tikz.execute();;

(* graph generator (informal java) *)

  let java_found = exists_pgm "java";;


  let graph_control_out =    Graph_control.execute();;

(* run on April 13, 2012.  Output saved to string_archive.txt *)

(* glpk (informal) *)

  let glpsol_found = exists_pgm "glpsol";;

(* tests consistency of lp computed b table with values in graph_control.flyspeck_properties *)
  let tame_table_out = Tame_table.execute();;  
  let oxlzlez_informal_out = Oxlzlez_informal.execute();;
  let build_lp_out = Build_lp.execute();;

(* cfsqp (informal) *)

(* returns list that fail to compile or that are negative *)
  let cfsqp_out = Scripts.execute_cfsqp();;  


(* nonlinear (informal) *)

  let interval_out = Scripts.execute_interval_allbutdodec true;;

  let check_completeness_out = Check_completeness.execute();;


(* nonlinear informal prep.hl form *)

  let mk_prep_hl = Preprocess.exec();;  (* generate /tmp/prep.hl *)

  let preplist = ref [];;
  let add_inequality t = (preplist:= t::!preplist);;
  let getprep idv = filter (fun t -> (t.idv = idv)) (!preplist);; 

  flyspeck_needs "nonlinear/prep.hl";;  (* load after add_inequality has been defined *)
  List.length !preplist;;

  let testprep_idq ex idq = 
    let (s,tags,ineq) = Optimize.idq_fields idq in
      Auto_lib.execute_interval ex tags s ineq;;

  let testprep ex s = testprep_idq ex (hd (getprep s));;

  let runprep cases = 
    map (fun t -> try (testprep true t) with Failure _ -> ()) cases;;

(*  runprep (map fst Scripts.fast_cases);; *)


 end;;