1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Copied from HOL Light jordan directory *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
11 module Hash_term = struct
15 let prime200 = 1223 in
17 let rec hashll v = match v with
20 (int_of_char (String.get h 0) + prime200*( hashll t)) mod prime in
22 let slt = explode s in
25 let saved_hashstring =
26 ref ((Hashtbl.create 300):(string,int) Hashtbl.t);;
27 let save_hashstring string =
28 Hashtbl.add !saved_hashstring (string) (hash_of_string string);;
29 let mem_hashstring s = Hashtbl.mem !saved_hashstring s;;
30 let remove_hashstring s = Hashtbl.remove !saved_hashstring s;;
31 let find_hashstring s = Hashtbl.find !saved_hashstring s;;
33 let memhash_of_string s =
34 if not(mem_hashstring s) then (save_hashstring s) ;
40 let prime180 = 1069 in
41 let prime190 = 1151 in
42 let prime1200 = 9733 in
43 let rec hashl u = match u with
45 | h::t -> ((hasht h) + prime190*(hashl t)) mod prime1200
47 hasht v = match v with
48 | Tyvar s -> (prime150*memhash_of_string s + prime160) mod prime1200
49 | Tyapp (s,tlt) -> let h = memhash_of_string s in
50 let h2 = (h*h) mod prime1200 in
51 (prime180*h2 + hashl tlt ) mod prime1200 in
54 (* make hash_of_term constant on alpha-equivalence classes of
58 fun v -> mk_var ("??_"^(string_of_int n),type_of v);;
61 let rec raform n env tm =
63 | Var(_,_) -> assocd tm env tm
65 | Comb (s,t) -> mk_comb(raform n env s, raform n env t)
66 | Abs (x,t) -> let x1 = rename_var n x in
67 mk_abs(x1, raform (n+1) ((x,x1)::env) t) in
71 let prime1220 = 9887 in
72 let prime210 = 1291 in
73 let prime220 = 1373 in
74 let prime230 = 1451 in
75 let prime240 = 1511 in
76 let prime250 = 1583 in
77 let prime260 = 1657 in
78 let prime270 = 1733 in
79 let prime280 = 1811 in
80 let rec hasht u = match u with
82 (prime210*(memhash_of_string s) + hash_of_type t) mod prime1220
84 (prime220*(memhash_of_string s) + hash_of_type t) mod prime1220
85 | Comb (s,t) -> let h = hasht s in
86 let h2 = (h*h) mod prime1220 in
87 (prime230*h2 + prime240*hasht t + prime250) mod prime1220
88 | Abs (s,t) -> let h = hasht s in
89 let h2 = (h*h) mod prime1220 in
90 (prime260*h2 + prime270*hasht t + prime280) mod prime1220