1(* ===================================================================== *) 2(* FILE : Net.sml *) 3(* DESCRIPTION : Implementation of term nets, from the group at ICL. *) 4(* Thanks! A term net is a database, keyed by terms. *) 5(* Term nets were initially implemented by Larry Paulson *) 6(* for Cambridge LCF. *) 7(* *) 8(* AUTHOR : Somebody in the ICL group. *) 9(* DATE : August 26, 1991 *) 10(* MODIFIED : Sept 5, 1992, to use deBruijn representation *) 11(* Modified : September 23, 1997, Ken Larsen *) 12(* Reimplemented : July 17, 1999, Konrad Slind *) 13(* ===================================================================== *) 14 15structure Net :> Net = 16struct 17 18open Lib Feedback KernelTypes 19 20val ERR = mk_HOL_ERR "Net"; 21 22val break_abs = Term.break_abs; 23 24(*---------------------------------------------------------------------------* 25 * Tags corresponding to the underlying term constructors. * 26 *---------------------------------------------------------------------------*) 27 28datatype label 29 = V 30 | Cmb 31 | Lam 32 | Cnst of string * string ; (* name * segment *) 33 34(*---------------------------------------------------------------------------* 35 * Term nets. * 36 *---------------------------------------------------------------------------*) 37 38datatype 'a net 39 = LEAF of (term * 'a) list 40 | NODE of (label * 'a net) list; 41 42 43val empty = NODE []; 44 45fun is_empty (NODE[]) = true 46 | is_empty _ = false; 47 48(*---------------------------------------------------------------------------* 49 * Determining the top constructor of a term. The following is a bit * 50 * convoluted, since doing a dest_abs requires a full traversal to replace * 51 * the bound variable with a free one. Therefore we make a separate check * 52 * for abstractions. * 53 *---------------------------------------------------------------------------*) 54 55local open Term 56in 57fun label_of tm = 58 if is_abs tm then Lam else 59 if is_bvar tm orelse is_var tm then V else 60 if is_comb tm then Cmb 61 else let val {Name,Thy,...} = dest_thy_const tm 62 in Cnst (Name,Thy) 63 end 64end 65 66fun net_assoc label = 67 let fun get (LEAF _) = raise ERR "net_assoc" "LEAF: no children" 68 | get (NODE subnets) = 69 case assoc1 label subnets 70 of NONE => empty 71 | SOME (_,net) => net 72 in get 73 end; 74 75 76local 77 fun mtch tm (NODE []) = [] 78 | mtch tm net = 79 let val label = label_of tm 80 val Vnet = net_assoc V net 81 val nets = 82 case label 83 of V => [] 84 | Cnst _ => [net_assoc label net] 85 | Lam => mtch (break_abs tm) (net_assoc Lam net) 86 | Cmb => let val (Rator,Rand) = Term.dest_comb tm 87 in itlist(append o mtch Rand) 88 (mtch Rator (net_assoc Cmb net)) [] 89 end 90 in itlist (fn NODE [] => I | net => cons net) nets [Vnet] 91 end 92in 93fun match tm net = 94 if is_empty net then [] 95 else 96 itlist (fn LEAF L => append (map #2 L) | _ => fn y => y) 97 (mtch tm net) [] 98end; 99 100(*--------------------------------------------------------------------------- 101 Finding the elements mapped by a term in a term net. 102 ---------------------------------------------------------------------------*) 103 104fun index x net = let 105 fun appl _ _ (LEAF L) = SOME L 106 | appl defd tm (NODE L) = 107 let val label = label_of tm 108 in case assoc1 label L 109 of NONE => NONE 110 | SOME (_,net) => 111 case label 112 of Lam => appl defd (break_abs tm) net 113 | Cmb => let val (Rator,Rand) = Term.dest_comb tm 114 in appl (Rand::defd) Rator net end 115 | _ => let fun exec_defd [] (NODE _) = raise ERR "appl" 116 "NODE: should be at a LEAF instead" 117 | exec_defd [] (LEAF L) = SOME L 118 | exec_defd (h::rst) net = appl rst h net 119 in 120 exec_defd defd net 121 end 122 end 123in 124 case appl [] x net 125 of SOME L => map #2 L 126 | NONE => [] 127end; 128 129(*---------------------------------------------------------------------------* 130 * Adding to a term net. * 131 *---------------------------------------------------------------------------*) 132 133fun overwrite (p as (a,_)) = 134 let fun over [] = [p] 135 | over ((q as (x,_))::rst) = 136 if (a=x) then p::rst else q::over rst 137 in over 138 end; 139 140fun insert (p as (tm,_)) N = 141let fun enter _ _ (LEAF _) = raise ERR "insert" "LEAF: cannot insert" 142 | enter defd tm (NODE subnets) = 143 let val label = label_of tm 144 val child = 145 case assoc1 label subnets of NONE => empty | SOME (_,net) => net 146 val new_child = 147 case label 148 of Cmb => let val (Rator,Rand) = Term.dest_comb tm 149 in enter (Rand::defd) Rator child end 150 | Lam => enter defd (break_abs tm) child 151 | _ => let fun exec [] (LEAF L) = LEAF(p::L) 152 | exec [] (NODE _) = LEAF[p] 153 | exec (h::rst) net = enter rst h net 154 in 155 exec defd child 156 end 157 in 158 NODE (overwrite (label,new_child) subnets) 159 end 160in enter [] tm N 161end; 162 163 164(*--------------------------------------------------------------------------- 165 Removing an element from a term net. It is not an error if the 166 element is not there. 167 ---------------------------------------------------------------------------*) 168 169fun split_assoc P = 170 let fun split front [] = raise ERR "split_assoc" "not found" 171 | split front (h::t) = 172 if P h then (rev front,h,t) else split (h::front) t 173 in 174 split [] 175 end; 176 177 178fun delete (tm,P) N = 179let fun del [] = [] 180 | del ((p as (x,q))::rst) = 181 if Term.aconv x tm andalso P q then del rst else p::del rst 182 fun remv _ _ (LEAF L) = LEAF(del L) 183 | remv defd tm (NODE L) = 184 let val label = label_of tm 185 fun pred (x,_) = (x=label) 186 val (left,(_,childnet),right) = split_assoc pred L 187 val childnet' = 188 case label 189 of Lam => remv defd (break_abs tm) childnet 190 | Cmb => let val (Rator,Rand) = Term.dest_comb tm 191 in remv (Rand::defd) Rator childnet end 192 | _ => let fun exec_defd [] (NODE _) = raise ERR "remv" 193 "NODE: should be at a LEAF instead" 194 | exec_defd [] (LEAF L) = LEAF(del L) 195 | exec_defd (h::rst) net = remv rst h net 196 in 197 exec_defd defd childnet 198 end 199 val childnetl = 200 case childnet' of NODE [] => [] | LEAF [] => [] | y => [(label,y)] 201 in 202 NODE (List.concat [left,childnetl,right]) 203 end 204in 205 remv [] tm N handle Feedback.HOL_ERR _ => N 206end; 207 208fun filter P = 209 let fun filt (LEAF L) = LEAF(List.filter (fn (x,y) => P y) L) 210 | filt (NODE L) = 211 NODE (itlist (fn (l,n) => fn list => 212 case filt n 213 of LEAF [] => list 214 | NODE [] => list 215 | n' => (l,n')::list) L []) 216 in 217 filt 218 end; 219 220fun listItems0 (LEAF L) = L 221 | listItems0 (NODE L) = rev_itlist (append o listItems0 o #2) L []; 222 223fun union net1 net2 = rev_itlist insert (listItems0 net1) net2; 224 225fun listItems net = map #2 (listItems0 net); 226 227fun map f (LEAF L) = LEAF (List.map (fn (x,y) => (x, f y)) L) 228 | map f (NODE L) = NODE (List.map (fn (l,net) => (l,map f net)) L); 229 230fun itnet f (LEAF L) b = itlist f (List.map #2 L) b 231 | itnet f (NODE L) b = itlist (itnet f) (List.map #2 L) b; 232 233fun size net = itnet (fn x => fn y => y+1) net 0; 234 235 236(*--------------------------------------------------------------------------- 237 Compatibility mode. 238 ---------------------------------------------------------------------------*) 239 240fun get_tip_list (LEAF L) = L 241 | get_tip_list (NODE _) = []; 242 243fun get_edge label = 244 let fun get (NODE edges) = 245 (case Lib.assoc1 label edges 246 of SOME (_,net) => net 247 | NONE => empty) 248 | get (LEAF _) = raise ERR "get_edge" "tips have no edges" 249 in get 250 end; 251 252fun net_update elem = 253let fun update _ _ (LEAF _) = raise ERR "net_update" "cannot update a tip" 254 | update defd tm (net as (NODE edges)) = 255 let fun exec_defd [] net = LEAF (elem::get_tip_list net) 256 | exec_defd (h::rst) net = update rst h net 257 val label = label_of tm 258 val child = get_edge label net 259 val new_child = 260 case label 261 of Cmb => let val (Rator,Rand) = Term.dest_comb tm 262 in update (Rator::defd) Rand child 263 end 264 | Lam => update defd (break_abs tm) child 265 | _ => exec_defd defd child 266 in NODE (overwrite (label,new_child) edges) 267 end 268in update 269end; 270 271fun enter (tm,elem) net = net_update (tm,elem) [] tm net; 272 273fun follow tm net = 274 let val nets = 275 case (label_of tm) 276 of (label as Cnst _) => [get_edge label net] 277 | V => [] 278 | Lam => follow (break_abs tm) (get_edge Lam net) 279 | Cmb => let val (Rator,Rand) = Term.dest_comb tm 280 in Lib.itlist(fn i => fn A => (follow Rator i @ A)) 281 (follow Rand (get_edge Cmb net)) [] 282 end 283 in List.filter (not o is_empty) (get_edge V net::nets) 284 end; 285 286fun lookup tm net = 287 if is_empty net then [] 288 else 289 itlist (fn (LEAF L) => (fn A => (List.map #2 L @ A)) | (NODE _) => I) 290 (follow tm net) []; 291 292end (* Net *) 293