(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: hypermap                                                             *)
(* Author:  Thomas Hales     *)
(* Date: 2011-04-29                                                    *)
(* ========================================================================== *)

(* The tame archive from the Bauer-Nipkow classification.
    The ML files in this directory are identical to those in Isabelle-HOL, Flyspeck-I. *)


(* WARNING!!!!
    HOL Light  printer does not use ellipses in list printing.
    Extremely slow processing and printing.  Had to kill process .  
    Fix before executing outside module.

*)


(* Usage:
You have to open module for reflection to work.
But then printing of lists makes it impossible to look at tmrefK.

See development/thales/printer.ml for a fix to the term printer that
prints ellipses in long lists.
*)

(*

June 6, 2011:
flyspeck_needs "../tame_archive/tame_archive.hl";;
open Tame_archive;;  (* must open because of reflected references *)
time Tame_archive.arc3 ();;  (* 0.18 secs *)
List.length !Tame_archive.ref3;;  (* 9 *)
!Tame_archive.tmref3;;
time Tame_archive.arc4 ();;  (* 22 secs *)
List.length !Tame_archive.ref4;;  (* 1105 *)

time Tame_archive.arc5 ();;  (*   676.555191 secs *)
List.length !Tame_archive.ref5;;  (* 15991 *)

time Tame_archive.arc6 ();;  (*  28 secs *)
List.length !Tame_archive.ref6;;  (* 1657 *)

*)


module Tame_archive  = struct 

let flyspeck_dir = 
  (try Sys.getenv "FLYSPECK_DIR" with Not_found -> Sys.getcwd());;

let archive_dir = 
 Filename.concat (Filename.concat (flyspeck_dir) Filename.parent_dir_name) 
 "tame_archive";;

(* from glpk.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 save_stringarray filename xs = 
  let oc = open_out filename in
    for i=0 to List.length xs -1
    do
      Pervasives.output_string oc (List.nth xs i ^ "\n");
      done;
    close_out oc;;

let convert_archive filename ext =  (* strip // comments, blank lines, quotation marks etc. *)
  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
  let s = load_and_close_channel false ic in
  let _ = Unix.close_process (ic,oc) in
    s;;

let ocaml_of_ml (output_f,input_f,ext) = 
save_stringarray output_f (convert_archive (Filename.concat archive_dir input_f) ext);;


let hol_of_smalllist  = 
  let ty = `:num` in 
    fun ls ->
      let xs = map mk_small_numeral ls in
	mk_list (xs,ty);;

let hol_of_list2 = 
  let ty = `:num list` in
    fun ls -> let x = map hol_of_smalllist ls in mk_list (x,ty);;

let hol_of_list3 =
  let ty = `:(num list) list` in
    fun ls -> let x = map hol_of_list2 ls in mk_list (x,ty);;



let tmp3 = Filename.temp_file "tmp3_" ".hl";; 
let tmp4 = Filename.temp_file "tmp4_" ".hl";; 
let tmp5 = Filename.temp_file "tmp5_" ".hl";; 
let tmp6 = Filename.temp_file "tmp6_" ".hl";; 

map ocaml_of_ml [(tmp3,"Tri.ML",3);(tmp4,"Quad.ML",4);
		(tmp5,"Pent.ML",5);(tmp6,"Hex.ML",6)];;



(* WARNING!!!!
    HOL Light  printer does not use ellipses in list printing.
    Extremely slow processing and printing.  Had to kill process .  
    Fix before executing outside module.

*)


let ref3 = ref [];;
let ref4 = ref [];;
let ref5 = ref [];;
let ref6 = ref [];;

let tmref3 = ref `0`;;
let tmref4 = ref `0`;;
let tmref5 = ref `0`;;
let tmref6 = ref `0`;;

(* loading these files changes the references! *)

let arc3 _ = 
  let _ = loadt tmp3 in
  let _ = (tmref3 :=  hol_of_list3 (!ref3)) in ();;

let arc4 _ = 
  let _ = loadt tmp4 in
  let _ = (tmref4 :=  hol_of_list3 (!ref4)) in ();;

let arc5 _ = 
  let _ = loadt tmp5 in
  let _ = (tmref5 :=  hol_of_list3 (!ref5)) in ();;

let arc6 _ = 
  let _ = loadt tmp6 in
  let _ = (tmref6 :=  hol_of_list3 (!ref6)) in ();;


(*
let archive3 = mk_eq (`archive3:((num list)list)list`, hol_of_list3 !ref3);;

let arc4 = mk_eq (`archive4:((num list)list)list`, hol_of_list3 !ref4);;

let arc5 = mk_eq (`archive5:((num list)list)list`, hol_of_list3 !ref5);;

let arc6 = mk_eq (`archive6:((num list)list)list`, hol_of_list3 !ref6);;


let archive3 = new_definition arc3;; 
let archive4 = new_definition arc4;; 
let archive5 = new_definition arc5;; 
let archive6 = new_definition arc6;; 

let bn_tame_archive = new_definition `bn_tame_archive = 
   APPEND arc3 (APPEND arc4 (APPEND arc5 arc6))`;;
*)

end;;