Jordan/tactics_fix.ml

   1 (* ------------------------------------------------------------------------- *)
   2 (* A printer for goals etc.                                                  *)
   3 (* ------------------------------------------------------------------------- *)
   4
   5 (* had (rev asl) in this method.  I don't want to reverse the list *)
   6
   7
   8 let hash_of_string =
   9   let prime200 = 1223 in
  10   let prime = 8831 in
  11   let rec hashll v = match v with
  12     | [] -> 0
  13     | h::t ->
  14    (int_of_char (String.get h 0) + prime200*( hashll t)) mod prime in
  15   fun s ->
  16     let slt = explode s in
  17     hashll slt;;
  18
  19 let saved_hashstring =
  20     ref ((Hashtbl.create 300):(string,int) Hashtbl.t);;
  21 let save_hashstring string =
  22     Hashtbl.add !saved_hashstring (string) (hash_of_string string);;
  23 let mem_hashstring s = Hashtbl.mem !saved_hashstring s;;
  24 let remove_hashstring s = Hashtbl.remove !saved_hashstring s;;
  25 let find_hashstring s = Hashtbl.find !saved_hashstring s;;
  26
  27 let memhash_of_string s =
  28    if not(mem_hashstring s) then (save_hashstring s) ;
  29    find_hashstring s;;
  30
  31 let hash_of_type =
  32   let prime150 = 863 in
  33   let prime160 = 941 in
  34   let prime180 = 1069 in
  35   let prime190 = 1151 in
  36   let prime1200 = 9733 in
  37   let rec hashl u = match u with
  38     | [] -> 0
  39     | h::t -> ((hasht h) + prime190*(hashl t)) mod prime1200
  40     and
  41     hasht v = match v with
  42     | Tyvar s -> (prime150*memhash_of_string s + prime160) mod prime1200
  43     | Tyapp (s,tlt) -> let h = memhash_of_string s in
  44                let h2 = (h*h) mod prime1200 in
  45           (prime180*h2 + hashl tlt ) mod prime1200 in
  46   hasht;;
  47
  48 (* make hash_of_term constant on alpha-equivalence classes of
  49    terms *)
  50
  51 let rename_var n =
  52   fun v -> mk_var ("??_"^(string_of_int n),type_of v);;
  53
  54 let paform =
  55   let rec raform n env tm =
  56     match tm with
  57       | Var(_,_) -> assocd tm env tm
  58       | Const(_,_) -> tm
  59       | Comb (s,t) -> mk_comb(raform n env s, raform n env t)
  60       | Abs  (x,t) -> let x1 = rename_var n x in
  61                       mk_abs(x1, raform (n+1) ((x,x1)::env) t) in
  62   raform 0 [];;
  63
  64 let hash_of_term =
  65   let prime1220 = 9887 in
  66   let prime210 = 1291 in
  67   let prime220 = 1373 in
  68   let prime230 = 1451 in
  69   let prime240 = 1511 in
  70   let prime250 = 1583 in
  71   let prime260 = 1657 in
  72   let prime270 = 1733 in
  73   let prime280 = 1811 in
  74   let rec hasht u = match u with
  75     | Var (s,t) ->
  76       (prime210*(memhash_of_string s) + hash_of_type t) mod prime1220
  77     | Const (s,t) ->
  78       (prime220*(memhash_of_string s) + hash_of_type t) mod prime1220
  79     | Comb (s,t) -> let h = hasht s in
  80             let h2 = (h*h) mod prime1220 in
  81              (prime230*h2 + prime240*hasht t + prime250) mod prime1220
  82     | Abs   (s,t) -> let h = hasht s in
  83            let h2 = (h*h) mod prime1220 in
  84              (prime260*h2 + prime270*hasht t + prime280) mod prime1220
  85   in hasht o paform;;
  86
  87 let print_hyp n (s,th) =
  88   open_hbox();
  89   print_string " ";
  90   print_as 4 (string_of_int (hash_of_term (concl th)));
  91   print_string " [";
  92   print_qterm (concl th);
  93   print_string "]";
  94   (if not (s = "") then (print_string (" ("^s^")")) else ());
  95   close_box();
  96   print_newline();;
  97
  98 let rec print_hyps n asl =
  99   if asl = [] then () else
 100   (print_hyp n (hd asl);
 101    print_hyps (n + 1) (tl asl));;
 102
 103 let (print_goal_hashed:goal->unit) =
 104   fun (asl,w) ->
 105     print_newline();
 106     if asl <> [] then (print_hyps 0 (asl); print_newline()) else ();
 107     print_qterm w; print_newline();;
 108
 109 let (print_goalstate_hashed:int->goalstate->unit) =
 110   fun k gs -> let (_,gl,_) = gs in
 111               let n = length gl in
 112               let s = if n = 0 then "No subgoals" else
 113                         (string_of_int k)^" subgoal"^(if k > 1 then "s" else "")
 114                      ^" ("^(string_of_int n)^" total)" in
 115               print_string s; print_newline();
 116               if gl = [] then () else
 117               do_list (print_goal_hashed o C el gl) (rev(0--(k-1)));;
 118
 119 let (print_goalstack_hashed:goalstack->unit) =
 120   fun l ->
 121     if l = [] then print_string "Empty goalstack"
 122     else if tl l = [] then
 123       let (_,gl,_ as gs) = hd l in
 124       print_goalstate_hashed 1 gs
 125     else
 126       let (_,gl,_ as gs) = hd l
 127       and (_,gl0,_) = hd(tl l) in
 128       let p = length gl - length gl0 in
 129       let p' = if p < 1 then 1 else p + 1 in
 130       print_goalstate_hashed p' gs;;
 131
 132 #install_printer print_goal_hashed;;
 133 #install_printer print_goalstack_hashed;;