tame_archive/tame_archive.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: hypermap                                                             *)
   5 (* Author:  Thomas Hales     *)
   6 (* Date: 2011-04-29                                                    *)
   7 (* ========================================================================== *)
   8
   9 (* The tame archive from the Bauer-Nipkow classification.
  10     The ML files in this directory are identical to those in Isabelle-HOL, Flyspeck-I. *)
  11
  12
  13 (* WARNING!!!!
  14     HOL Light  printer does not use ellipses in list printing.
  15     Extremely slow processing and printing.  Had to kill process .
  16     Fix before executing outside module.
  17
  18 *)
  19
  20
  21 (* Usage:
  22 You have to open module for reflection to work.
  23 But then printing of lists makes it impossible to look at tmrefK.
  24
  25 See development/thales/printer.ml for a fix to the term printer that
  26 prints ellipses in long lists.
  27 *)
  28
  29 (*
  30
  31 June 6, 2011:
  32 flyspeck_needs "../tame_archive/tame_archive.hl";;
  33 open Tame_archive;;  (* must open because of reflected references *)
  34 time Tame_archive.arc3 ();;  (* 0.18 secs *)
  35 List.length !Tame_archive.ref3;;  (* 9 *)
  36 !Tame_archive.tmref3;;
  37 time Tame_archive.arc4 ();;  (* 22 secs *)
  38 List.length !Tame_archive.ref4;;  (* 1105 *)
  39
  40 time Tame_archive.arc5 ();;  (*   676.555191 secs *)
  41 List.length !Tame_archive.ref5;;  (* 15991 *)
  42
  43 time Tame_archive.arc6 ();;  (*  28 secs *)
  44 List.length !Tame_archive.ref6;;  (* 1657 *)
  45
  46 *)
  47
  48
  49 module Tame_archive  = struct
  50
  51 let flyspeck_dir =
  52   (try Sys.getenv "FLYSPECK_DIR" with Not_found -> Sys.getcwd());;
  53
  54 let archive_dir =
  55  Filename.concat (Filename.concat (flyspeck_dir) Filename.parent_dir_name)
  56  "tame_archive";;
  57
  58 (* from glpk.ml *)
  59 let load_and_close_channel do_close ic =
  60   let rec lf ichan a =
  61     try
  62       lf ic (Pervasives.input_line ic::a)
  63     with End_of_file -> a in
  64     let rs = lf ic [] in
  65       if do_close then Pervasives.close_in ic else ();
  66       rev rs;;
  67
  68 let save_stringarray filename xs =
  69   let oc = open_out filename in
  70     for i=0 to List.length xs -1
  71     do
  72       Pervasives.output_string oc (List.nth xs i ^ "\n");
  73       done;
  74     close_out oc;;
  75
  76 let convert_archive filename ext =  (* strip // comments, blank lines, quotation marks etc. *)
  77   let (ic,oc) = Unix.open_process(sprintf "cat %s  | sed 's/,/;/g' | sed 's/val [a-zA-Z]*/ref%d/g' | sed 's/]]];/]]];;/g' | sed 's/=/:=/g' | tr 'A-Z' 'a-z' " filename ext) in
  78   let s = load_and_close_channel false ic in
  79   let _ = Unix.close_process (ic,oc) in
  80     s;;
  81
  82 let ocaml_of_ml (output_f,input_f,ext) =
  83 save_stringarray output_f (convert_archive (Filename.concat archive_dir input_f) ext);;
  84
  85
  86 let hol_of_smalllist  =
  87   let ty = `:num` in
  88     fun ls ->
  89       let xs = map mk_small_numeral ls in
  90         mk_list (xs,ty);;
  91
  92 let hol_of_list2 =
  93   let ty = `:num list` in
  94     fun ls -> let x = map hol_of_smalllist ls in mk_list (x,ty);;
  95
  96 let hol_of_list3 =
  97   let ty = `:(num list) list` in
  98     fun ls -> let x = map hol_of_list2 ls in mk_list (x,ty);;
  99
 100
 101
 102 let tmp3 = Filename.temp_file "tmp3_" ".hl";;
 103 let tmp4 = Filename.temp_file "tmp4_" ".hl";;
 104 let tmp5 = Filename.temp_file "tmp5_" ".hl";;
 105 let tmp6 = Filename.temp_file "tmp6_" ".hl";;
 106
 107 map ocaml_of_ml [(tmp3,"Tri.ML",3);(tmp4,"Quad.ML",4);
 108                 (tmp5,"Pent.ML",5);(tmp6,"Hex.ML",6)];;
 109
 110
 111
 112 (* WARNING!!!!
 113     HOL Light  printer does not use ellipses in list printing.
 114     Extremely slow processing and printing.  Had to kill process .
 115     Fix before executing outside module.
 116
 117 *)
 118
 119
 120 let ref3 = ref [];;
 121 let ref4 = ref [];;
 122 let ref5 = ref [];;
 123 let ref6 = ref [];;
 124
 125 let tmref3 = ref `0`;;
 126 let tmref4 = ref `0`;;
 127 let tmref5 = ref `0`;;
 128 let tmref6 = ref `0`;;
 129
 130 (* loading these files changes the references! *)
 131
 132 let arc3 _ =
 133   let _ = loadt tmp3 in
 134   let _ = (tmref3 :=  hol_of_list3 (!ref3)) in ();;
 135
 136 let arc4 _ =
 137   let _ = loadt tmp4 in
 138   let _ = (tmref4 :=  hol_of_list3 (!ref4)) in ();;
 139
 140 let arc5 _ =
 141   let _ = loadt tmp5 in
 142   let _ = (tmref5 :=  hol_of_list3 (!ref5)) in ();;
 143
 144 let arc6 _ =
 145   let _ = loadt tmp6 in
 146   let _ = (tmref6 :=  hol_of_list3 (!ref6)) in ();;
 147
 148
 149 (*
 150 let archive3 = mk_eq (`archive3:((num list)list)list`, hol_of_list3 !ref3);;
 151
 152 let arc4 = mk_eq (`archive4:((num list)list)list`, hol_of_list3 !ref4);;
 153
 154 let arc5 = mk_eq (`archive5:((num list)list)list`, hol_of_list3 !ref5);;
 155
 156 let arc6 = mk_eq (`archive6:((num list)list)list`, hol_of_list3 !ref6);;
 157
 158
 159 let archive3 = new_definition arc3;;
 160 let archive4 = new_definition arc4;;
 161 let archive5 = new_definition arc5;;
 162 let archive6 = new_definition arc6;;
 163
 164 let bn_tame_archive = new_definition `bn_tame_archive =
 165    APPEND arc3 (APPEND arc4 (APPEND arc5 arc6))`;;
 166 *)
 167
 168 end;;