1structure declFuncs =
2struct
3
4local
5open HolKernel Parse
6in
7
8  exception undeclFunc;
9
10  val k = ref 0;
11  val sizeHint = 128
12  val hashtable : ((string, int) Polyhash.hash_table) ref =
13           ref (Polyhash.mkTable(Polyhash.hash, op = ) (sizeHint, undeclFunc))
14
15  structure T = IntMapTable(type key = int  fun getInt n = n);
16
17  type func = {name : string, ftype : hol_type, ir : IRSyntax.exp * annotatedIR.anntIR * IRSyntax.exp,
18        regs : int Binaryset.set, localNum : int, def : thm};
19  val decls : (func T.table) ref = ref (T.empty);
20
21  fun is_decl fun_name =
22        case Polyhash.peek (!hashtable) fun_name of
23                SOME x => true
24         |      NONE => false
25
26  fun getFunc fun_name =
27      let val i = Polyhash.find (!hashtable) fun_name in
28        T.look(!decls,i)
29      end;
30
31  fun putFunc (name,tp,ir,rs,n,f_def) =
32      let
33          val _ = Polyhash.insert (!hashtable) (name, !k)
34      in
35            ( decls := T.enter(!decls,!k, {name = name, ftype = tp, ir = ir, regs = rs, localNum = n, def = f_def});
36              k := !k + 1
37            )
38      end
39
40end (* local structure ... *)
41
42end (* structure *)
43