(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Jordan                                                               *)
(* Copied from HOL Light jordan directory *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-07-08                                                           *)
(* ========================================================================== *)

(* needs tactics_fix.ml;; 
   tactics_refine.ml ;; 
   lib_ext.ml *)

module Goal_printer = struct

open Refinement;;
open Hash_term;;
open Lib_ext;;
(* This file is in severe need of a rewrite! *)

Parse_ext_override_interface.unambiguous_interface();;
Parse_ext_override_interface.prioritize_real();;

(*

   To restore HOL-light defaults, type
   #install_printer print_goal;;
   #install_printer print_goalstack;;

*)


(* To install:
#install_printer Goal_printer.print_goal_hashed;;
#install_printer Goal_printer.print_goalstack_hashed;;

   To install printer that reverses the assumption list, but no hashing:

   #install_printer Goal_printer.print_rev_goal;;
   #install_printer Goal_printer.print_rev_goalstack;;

*)



(* ------------------------------------------------------------------------- *)
(* A printer for goals etc.                                                  *)
(* ------------------------------------------------------------------------- *)




(* had (rev asl) in this method.  I don't want to reverse the list *)


let print_hyp n (s,th) =
  open_hbox();
  print_string " ";
  print_as 4 (string_of_int (hash_of_term (concl th)));
  print_string " [";
  print_qterm (concl th);
  print_string "]";
  (if not (s = "") then (print_string (" ("^s^")")) else ());
  close_box();
  print_newline();;

let rec print_hyps n asl =
  if asl = [] then () else
  (print_hyp n (hd asl);
   print_hyps (n + 1) (tl asl));;

let (print_goal_hashed:goal->unit) =
  fun gl ->
    let (asl,w)= dest_goal gl in
      print_newline();
      if asl <> [] then (print_hyps 0 (asl); print_newline()) else ();
      print_qterm w; print_newline();;

let (print_goalstate_hashed:int->goalstate->unit) =
  fun k gs -> let (_,gl,_) = gs in
              let n = length gl in
              let s = if n = 0 then "No subgoals" else
                        (string_of_int k)^" subgoal"^(if k > 1 then "s" else "")
                     ^" ("^(string_of_int n)^" total)" in
              print_string s; print_newline();
              if gl = [] then () else
              do_list (print_goal_hashed o C el gl) (rev(0--(k-1)));;

let (print_goalstack_hashed:goalstack->unit) =
  fun l ->
    if l = [] then print_string "Empty goalstack"
    else if tl l = [] then
      let (_,gl,_ as gs) = hd l in
      print_goalstate_hashed 1 gs
    else
      let (_,gl,_ as gs) = hd l
      and (_,gl0,_) = hd(tl l) in
      let p = length gl - length gl0 in
      let p' = if p < 1 then 1 else p + 1 in
      print_goalstate_hashed p' gs;;



(* To install printers:
#install_printer print_rev_goal;;
#install_printer print_rev_goalstack;;
*)


(* ------------------------------------------------------------------------- *)
(* A printer that reverses the assumption list *)
(* ------------------------------------------------------------------------- *)

(*

   Objective version of HOL-light uses (rev asl) in the method print_goal.
   This means that the numbers printed next to the assumptions
   are the reverse of the numbering in the list.

   I want it the opposite way.
   This reverses the numbering on the assumption list,
   so that the printed numbers match the list order.

   To restore HOL-light defaults, type
   #install_printer print_goal;;
   #install_printer print_goalstack;;

*)

let (print_rev_goal:goal->unit) =
  fun gl -> 
    let (asl,w) = dest_goal gl in
      print_goal (mk_goal(rev asl,w));;

let (print_rev_goalstate:int->goalstate->unit) =
  fun k gs -> let (_,gl,_) = gs in
              let n = length gl in
              let s = if n = 0 then "No subgoals" else
                        (string_of_int k)^" subgoal"^(if k > 1 then "s" else "")
                     ^" ("^(string_of_int n)^" total)" in
              print_string s; print_newline();
              if gl = [] then () else
              do_list (print_rev_goal o C el gl) (rev(0--(k-1)));;


let (print_rev_goalstack:goalstack->unit) =
  fun l ->
    if l = [] then print_string "Empty goalstack"
    else if tl l = [] then
      let (_,gl,_ as gs) = hd l in
      print_rev_goalstate 1 gs
    else
      let (_,gl,_ as gs) = hd l
      and (_,gl0,_) = hd(tl l) in
      let p = length gl - length gl0 in
      let p' = if p < 1 then 1 else p + 1 in
      print_rev_goalstate p' gs;;


end;;