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