text_formalization/general/flyspeck_lib.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* HOL LIGHT pervasives                                                       *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2012-04-15                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10 (* This file contains Ocaml library functions *)
  11
  12
  13 module Flyspeck_lib = struct
  14
  15
  16 (*
  17 eval_command comes from
  18
  19 http://solaria.dimino.org/cgi-bin/darcsweb.cgi?r=peps;a=headblob;f=/src/core/peps_top.ml
  20 License: BSD3
  21
  22 If the expression is syntactically correct
  23 and the evaluation raises an exception, then the return value is true.
  24 *)
  25
  26
  27 let eval_command ?(silent=false) command =
  28    let buffer = Buffer.create 512 in
  29    let pp = Format.formatter_of_buffer buffer in
  30    Format.pp_set_margin pp max_int;
  31    try
  32      let _ =
  33        Toploop.execute_phrase (not silent) pp
  34          (!Toploop.parse_toplevel_phrase (Lexing.from_string (command ^ ";;")))
  35      in
  36      (true, Buffer.contents buffer)
  37    with exn ->
  38      let save = !Toploop.parse_use_file in
  39      Toploop.parse_use_file := (fun _ -> raise exn);
  40      Pervasives.ignore (Toploop.use_silently pp "/dev/null");
  41      Toploop.parse_use_file := save;
  42      (false,  Buffer.contents buffer);;
  43
  44 (* eval_command ~silent:false "g `x=y`";; *)
  45
  46
  47 (* process_to_string in strictbuild.hl *)
  48
  49 let svn_version() = "svn("^
  50   (process_to_string ("svnversion -n " ^ flyspeck_dir))^
  51   ","^
  52   (process_to_string("svnversion -n " ^ hollight_dir))^
  53   ")";;
  54
  55
  56 (* duplicated code *)
  57 let unsplit d f = function
  58   | (x::xs) ->  List.fold_left (fun s t -> s^d^(f t)) (f x) xs
  59   | [] -> "";;
  60
  61 let join_comma  = unsplit "," (fun x-> x);;
  62
  63 let join_lines  = unsplit "\n" (fun x-> x);;
  64
  65 let join_space  = unsplit " " (fun x-> x);;
  66
  67 let rec nub = function (* from lpproc.ml *)
  68   | [] -> []
  69   | x::xs -> x::filter ((<>) x) (nub xs);;
  70
  71 (* duplicated code *)
  72
  73 (* System commands *)
  74
  75 let output_filestring tmpfile a =
  76   let outs = open_out tmpfile in
  77   let _ = try (Printf.fprintf outs "%s" a)
  78   with _ as t -> (close_out outs; raise t) in
  79    close_out outs ;;
  80
  81 (* from glpk_link.ml *)
  82
  83 let load_and_close_channel do_close ic =
  84   let rec lf ichan a =
  85     try
  86       lf ic (Pervasives.input_line ic::a)
  87     with End_of_file -> a in
  88     let rs = lf ic [] in
  89       if do_close then Pervasives.close_in ic else ();
  90       rev rs;;
  91
  92 let load_and_close_channel_true ic =
  93   let rec lf ichan a =
  94     try
  95       lf ic (Pervasives.input_line ic::a)
  96     with End_of_file -> a | _ as t -> (Pervasives.close_in ic; raise t) in
  97     let rs = lf ic [] in
  98     let _ = Pervasives.close_in ic in
  99       rev rs;;
 100
 101 let load_file filename =
 102   let ic = Pervasives.open_in filename in load_and_close_channel_true ic;;
 103
 104
 105
 106 (* deprecated
 107 let print_string_as_text  = report;;
 108 *)
 109
 110 let exists_pgm s =
 111   let com = "command -v " ^ s in
 112     not(process_to_string com = "");;
 113
 114
 115 (* numerical *)
 116
 117 let dest_decimal x = match strip_comb x with
 118     | (dec,[a;b]) ->
 119         div_num (dest_numeral a) (dest_numeral b)
 120     | _ -> failwith ("dest_decimal: '" ^ string_of_term x ^ "'") ;;
 121
 122 let string_of_num' x = string_of_float (float_of_num x);;
 123
 124
 125 end;;