text_formalization/jordan/hash_term.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Jordan                                                               *)
   5 (* Copied from HOL Light jordan directory *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-07-08                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11 module Hash_term = struct
  12
  13
  14 let hash_of_string =
  15   let prime200 = 1223 in
  16   let prime = 8831 in
  17   let rec hashll v = match v with
  18     | [] -> 0
  19     | h::t ->
  20    (int_of_char (String.get h 0) + prime200*( hashll t)) mod prime in
  21   fun s ->
  22     let slt = explode s in
  23     hashll slt;;
  24
  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;;
  32
  33 let memhash_of_string s =
  34    if not(mem_hashstring s) then (save_hashstring s) ;
  35    find_hashstring s;;
  36
  37 let hash_of_type =
  38   let prime150 = 863 in
  39   let prime160 = 941 in
  40   let prime180 = 1069 in
  41   let prime190 = 1151 in
  42   let prime1200 = 9733 in
  43   let rec hashl u = match u with
  44     | [] -> 0
  45     | h::t -> ((hasht h) + prime190*(hashl t)) mod prime1200
  46     and
  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
  52   hasht;;
  53
  54 (* make hash_of_term constant on alpha-equivalence classes of
  55    terms *)
  56
  57 let rename_var n =
  58   fun v -> mk_var ("??_"^(string_of_int n),type_of v);;
  59
  60 let paform =
  61   let rec raform n env tm =
  62     match tm with
  63       | Var(_,_) -> assocd tm env tm
  64       | Const(_,_) -> 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
  68   raform 0 [];;
  69
  70 let hash_of_term =
  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
  81     | Var (s,t) ->
  82       (prime210*(memhash_of_string s) + hash_of_type t) mod prime1220
  83     | Const (s,t) ->
  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
  91   in hasht o paform;;
  92
  93 end;;