(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* HOL LIGHT pervasives                                                       *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2012-04-15                                                           *)
(* ========================================================================== *)


(* This file contains Ocaml library functions *)


module Flyspeck_lib = struct


(*
eval_command comes from

http://solaria.dimino.org/cgi-bin/darcsweb.cgi?r=peps;a=headblob;f=/src/core/peps_top.ml
License: BSD3

If the expression is syntactically correct 
and the evaluation raises an exception, then the return value is true.
*)


let eval_command ?(silent=false) command =
   let buffer = Buffer.create 512 in
   let pp = Format.formatter_of_buffer buffer in
   Format.pp_set_margin pp max_int;
   try
     let _ =
       Toploop.execute_phrase (not silent) pp
         (!Toploop.parse_toplevel_phrase (Lexing.from_string (command ^ ";;")))
     in
     (true, Buffer.contents buffer)
   with exn ->
     let save = !Toploop.parse_use_file in
     Toploop.parse_use_file := (fun _ -> raise exn);
     Pervasives.ignore (Toploop.use_silently pp "/dev/null");
     Toploop.parse_use_file := save;
     (false,  Buffer.contents buffer);;

(* eval_command ~silent:false "g `x=y`";; *)


(* process_to_string in strictbuild.hl *)

let svn_version() = "svn("^
  (process_to_string ("svnversion -n " ^ flyspeck_dir))^
  ","^
  (process_to_string("svnversion -n " ^ hollight_dir))^
  ")";;


(* 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 rec nub = function (* from lpproc.ml *)
  | [] -> []
  | x::xs -> x::filter ((<>) x) (nub xs);;

(* duplicated code *)

(* System commands *)

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 ;;

(* from glpk_link.ml *)

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_and_close_channel_true ic = 
  let rec lf ichan a = 
    try
      lf ic (Pervasives.input_line ic::a)
    with End_of_file -> a | _ as t -> (Pervasives.close_in ic; raise t) in
    let rs = lf ic [] in
    let _ = Pervasives.close_in ic in
      rev rs;;

let load_file filename = 
  let ic = Pervasives.open_in filename in load_and_close_channel_true ic;;



(* deprecated
let print_string_as_text  = report;;
*)

let exists_pgm s = 
  let com = "command -v " ^ s in 
    not(process_to_string com = "");;


(* numerical *)

let dest_decimal x = match strip_comb x with
    | (dec,[a;b]) ->                     
	div_num (dest_numeral a) (dest_numeral b)
    | _ -> failwith ("dest_decimal: '" ^ string_of_term x ^ "'") ;;

let string_of_num' x = string_of_float (float_of_num x);; 


end;;