provide find_(ty|l|pr)symbol : ident -> (ty|l|pr)symbol

The relevant hash-tables are weak both in keys and values

src/core/decl.ml

@@ -86,9 +86,22 @@ module Spr = Prop.S
 module Mpr = Prop.M
 module Hpr = Prop.H
 
-let pr_equal pr1 pr2 = id_equal pr1.pr_name pr2.pr_name
-
-let create_prsymbol n = { pr_name = id_register n }
+let pr_equal = (==)
+
+let prsymbol_table = Wid.create 63
+
+let create_prsymbol name =
+  let id = id_register name in
+  let pr = { pr_name = id } in
+  let wa = Weak.create 1 in
+  Weak.set wa 0 (Some pr);
+  Wid.set prsymbol_table id wa;
+  pr
+
+let find_prsymbol id =
+  match Weak.get (Wid.find prsymbol_table id) 0 with
+  | Some pr -> pr
+  | None -> raise Not_found
 
 type ind_decl = lsymbol * (prsymbol * fmla) list
 

src/core/decl.mli

@@ -58,6 +58,7 @@ module Mpr : Map.S with type key = prsymbol
 module Hpr : Hashtbl.S with type key = prsymbol
 
 val create_prsymbol : preid -> prsymbol
+val find_prsymbol : ident -> prsymbol
 
 val pr_equal : prsymbol -> prsymbol -> bool
 

src/core/ident.ml

@@ -40,6 +40,7 @@ end)
 module Sid = Id.S
 module Mid = Id.M
 module Hid = Id.H
+module Wid = Id.W
 
 type preid = ident
 

src/core/ident.mli

@@ -33,6 +33,7 @@ and origin =
 module Sid : Set.S with type elt = ident
 module Mid : Map.S with type key = ident
 module Hid : Hashtbl.S with type key = ident
+module Wid : Hashweak.S with type key = ident
 
 val id_equal : ident -> ident -> bool
 

src/core/term.ml

@@ -65,12 +65,27 @@ module Hls = Lsym.H
 
 let ls_equal = (==)
 
-let create_lsymbol name args value = {
-  ls_name   = id_register name;
+let mk_ls name args value = {
+  ls_name   = name;
   ls_args   = args;
   ls_value  = value;
 }
 
+let lsymbol_table = Wid.create 63
+
+let create_lsymbol name args value =
+  let id = id_register name in
+  let ls = mk_ls id args value in
+  let wa = Weak.create 1 in
+  Weak.set wa 0 (Some ls);
+  Wid.set lsymbol_table id wa;
+  ls
+
+let find_lsymbol id =
+  match Weak.get (Wid.find lsymbol_table id) 0 with
+  | Some ls -> ls
+  | None -> raise Not_found
+
 let create_fsymbol nm al vl = create_lsymbol nm al (Some vl)
 let create_psymbol nm al    = create_lsymbol nm al (None)
 

src/core/term.mli

@@ -55,6 +55,8 @@ val create_lsymbol : preid -> ty list -> ty option -> lsymbol
 val create_fsymbol : preid -> ty list -> ty -> lsymbol
 val create_psymbol : preid -> ty list -> lsymbol
 
+val find_lsymbol : ident -> lsymbol
+
 (** {2 Exceptions} *)
 
 exception DuplicateVar of vsymbol

src/core/ty.ml

@@ -75,7 +75,20 @@ let mk_ts name args def = {
   ts_def  = def;
 }
 
-let create_tysymbol name args def = mk_ts (id_register name) args def
+let tysymbol_table = Wid.create 63
+
+let create_tysymbol name args def =
+  let id = id_register name in
+  let ts = mk_ts id args def in
+  let wa = Weak.create 1 in
+  Weak.set wa 0 (Some ts);
+  Wid.set tysymbol_table id wa;
+  ts
+
+let find_tysymbol id =
+  match Weak.get (Wid.find tysymbol_table id) 0 with
+  | Some ts -> ts
+  | None -> raise Not_found
 
 module Hsty = Hashcons.Make (struct
   type t = ty
@@ -209,7 +222,7 @@ let ts_real = create_tysymbol (id_fresh "real") [] None
 let ty_int  = ty_app ts_int  []
 let ty_real = ty_app ts_real []
 
-let ts_tuple n = 
+let ts_tuple n =
   let vl = ref [] in
   for i = 1 to n do vl := create_tvsymbol (id_fresh "a") :: !vl done;
   create_tysymbol (id_fresh ("tuple" ^ string_of_int n)) !vl None

src/core/ty.mli

@@ -70,6 +70,7 @@ exception DuplicateTypeVar of tvsymbol
 exception UnboundTypeVar of tvsymbol
 
 val create_tysymbol : preid -> tvsymbol list -> ty option -> tysymbol
+val find_tysymbol : ident -> tysymbol
 
 val ty_var : tvsymbol -> ty
 val ty_app : tysymbol -> ty list -> ty