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

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


let hash_of_string =
  let prime200 = 1223 in
  let prime = 8831 in
  let rec hashll v = match v with
    | [] -> 0
    | h::t ->
   (int_of_char (String.get h 0) + prime200*( hashll t)) mod prime in
  fun s ->
    let slt = explode s in
    hashll slt;;

let saved_hashstring =
    ref ((Hashtbl.create 300):(string,int) Hashtbl.t);;
let save_hashstring string =
    Hashtbl.add !saved_hashstring (string) (hash_of_string string);;
let mem_hashstring s = Hashtbl.mem !saved_hashstring s;;
let remove_hashstring s = Hashtbl.remove !saved_hashstring s;;
let find_hashstring s = Hashtbl.find !saved_hashstring s;;

let memhash_of_string s =
   if not(mem_hashstring s) then (save_hashstring s) ;
   find_hashstring s;;

let hash_of_type =
  let prime150 = 863 in
  let prime160 = 941 in
  let prime180 = 1069 in
  let prime190 = 1151 in
  let prime1200 = 9733 in
  let rec hashl u = match u with
    | [] -> 0
    | h::t -> ((hasht h) + prime190*(hashl t)) mod prime1200
    and
    hasht v = match v with
    | Tyvar s -> (prime150*memhash_of_string s + prime160) mod prime1200
    | Tyapp (s,tlt) -> let h = memhash_of_string s in
               let h2 = (h*h) mod prime1200 in
          (prime180*h2 + hashl tlt ) mod prime1200 in
  hasht;;

(* make hash_of_term constant on alpha-equivalence classes of
   terms *)

let rename_var n =
  fun v -> mk_var ("??_"^(string_of_int n),type_of v);;

let paform =
  let rec raform n env tm =
    match tm with
      | Var(_,_) -> assocd tm env tm
      | Const(_,_) -> tm
      | Comb (s,t) -> mk_comb(raform n env s, raform n env t)
      | Abs  (x,t) -> let x1 = rename_var n x in
                      mk_abs(x1, raform (n+1) ((x,x1)::env) t) in
  raform 0 [];;

let hash_of_term =
  let prime1220 = 9887 in
  let prime210 = 1291 in
  let prime220 = 1373 in
  let prime230 = 1451 in
  let prime240 = 1511 in
  let prime250 = 1583 in
  let prime260 = 1657 in
  let prime270 = 1733 in
  let prime280 = 1811 in
  let rec hasht u = match u with
    | Var (s,t) ->
      (prime210*(memhash_of_string s) + hash_of_type t) mod prime1220
    | Const (s,t) ->
      (prime220*(memhash_of_string s) + hash_of_type t) mod prime1220
    | Comb (s,t) -> let h = hasht s in
            let h2 = (h*h) mod prime1220 in
             (prime230*h2 + prime240*hasht t + prime250) mod prime1220
    | Abs   (s,t) -> let h = hasht s in
           let h2 = (h*h) mod prime1220 in
             (prime260*h2 + prime270*hasht t + prime280) mod prime1220
  in hasht o paform;;

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 (asl,w) ->
    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;;

#install_printer print_goal_hashed;;
#install_printer print_goalstack_hashed;;