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 19 20type term = Term.term 21 22val ERR = mk_HOL_ERR "Net"; 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. * 50 *---------------------------------------------------------------------------*) 51 52local open Term 53in 54fun label_of tm = 55 if is_abs tm then Lam else 56 if is_var tm then V else 57 if is_comb tm then Cmb 58 else let val {Name,Thy,...} = dest_thy_const tm 59 in Cnst (Name,Thy) 60 end 61end 62 63fun net_assoc label = 64 let fun get (LEAF _) = raise ERR "net_assoc" "LEAF: no children" 65 | get (NODE subnets) = 66 case assoc1 label subnets 67 of NONE => empty 68 | SOME (_,net) => net 69 in get 70 end; 71 72 73local 74 fun mtch tm (NODE []) = [] 75 | mtch tm net = 76 let val label = label_of tm 77 val Vnet = net_assoc V net 78 val nets = 79 case label 80 of V => [] 81 | Cnst _ => [net_assoc label net] 82 | Lam => mtch (Term.body tm) (net_assoc Lam net) 83 | Cmb => let val (Rator,Rand) = Term.dest_comb tm 84 in itlist(append o mtch Rand) 85 (mtch Rator (net_assoc Cmb net)) [] 86 end 87 in itlist (fn NODE [] => I | net => cons net) nets [Vnet] 88 end 89in 90fun match tm net = 91 if is_empty net then [] 92 else 93 itlist (fn LEAF L => append (map #2 L) | _ => fn y => y) 94 (mtch tm net) [] 95end; 96 97(*--------------------------------------------------------------------------- 98 Finding the elements mapped by a term in a term net. 99 ---------------------------------------------------------------------------*) 100 101fun index x net = let 102 fun appl _ _ (LEAF L) = SOME L 103 | appl defd tm (NODE L) = 104 let val label = label_of tm 105 in case assoc1 label L 106 of NONE => NONE 107 | SOME (_,net) => 108 case label 109 of Lam => appl defd (Term.body tm) net 110 | Cmb => let val (Rator,Rand) = Term.dest_comb tm 111 in appl (Rand::defd) Rator net end 112 | _ => let fun exec_defd [] (NODE _) = raise ERR "appl" 113 "NODE: should be at a LEAF instead" 114 | exec_defd [] (LEAF L) = SOME L 115 | exec_defd (h::rst) net = appl rst h net 116 in 117 exec_defd defd net 118 end 119 end 120in 121 case appl [] x net 122 of SOME L => map #2 L 123 | NONE => [] 124end; 125 126(*---------------------------------------------------------------------------* 127 * Adding to a term net. * 128 *---------------------------------------------------------------------------*) 129 130fun overwrite (p as (a,_)) = 131 let fun over [] = [p] 132 | over ((q as (x,_))::rst) = 133 if (a=x) then p::rst else q::over rst 134 in over 135 end; 136 137fun insert (p as (tm,_)) N = 138let fun enter _ _ (LEAF _) = raise ERR "insert" "LEAF: cannot insert" 139 | enter defd tm (NODE subnets) = 140 let val label = label_of tm 141 val child = 142 case assoc1 label subnets of NONE => empty | SOME (_,net) => net 143 val new_child = 144 case label 145 of Cmb => let val (Rator,Rand) = Term.dest_comb tm 146 in enter (Rand::defd) Rator child end 147 | Lam => enter defd (Term.body tm) child 148 | _ => let fun exec [] (LEAF L) = LEAF(p::L) 149 | exec [] (NODE _) = LEAF[p] 150 | exec (h::rst) net = enter rst h net 151 in 152 exec defd child 153 end 154 in 155 NODE (overwrite (label,new_child) subnets) 156 end 157in enter [] tm N 158end; 159 160 161(*--------------------------------------------------------------------------- 162 Removing an element from a term net. It is not an error if the 163 element is not there. 164 ---------------------------------------------------------------------------*) 165 166fun split_assoc P = 167 let fun split front [] = raise ERR "split_assoc" "not found" 168 | split front (h::t) = 169 if P h then (rev front,h,t) else split (h::front) t 170 in 171 split [] 172 end; 173 174 175fun delete (tm,P) N = 176let fun del [] = [] 177 | del ((p as (x,q))::rst) = 178 if Term.aconv x tm andalso P q then del rst else p::del rst 179 fun remv _ _ (LEAF L) = LEAF(del L) 180 | remv defd tm (NODE L) = 181 let val label = label_of tm 182 fun pred (x,_) = (x=label) 183 val (left,(_,childnet),right) = split_assoc pred L 184 val childnet' = 185 case label 186 of Lam => remv defd (Term.body tm) childnet 187 | Cmb => let val (Rator,Rand) = Term.dest_comb tm 188 in remv (Rand::defd) Rator childnet end 189 | _ => let fun exec_defd [] (NODE _) = raise ERR "remv" 190 "NODE: should be at a LEAF instead" 191 | exec_defd [] (LEAF L) = LEAF(del L) 192 | exec_defd (h::rst) net = remv rst h net 193 in 194 exec_defd defd childnet 195 end 196 val childnetl = 197 case childnet' of NODE [] => [] | LEAF [] => [] | y => [(label,y)] 198 in 199 NODE (List.concat [left,childnetl,right]) 200 end 201in 202 remv [] tm N handle Feedback.HOL_ERR _ => N 203end; 204 205fun filter P = 206 let fun filt (LEAF L) = LEAF(List.filter (fn (x,y) => P y) L) 207 | filt (NODE L) = 208 NODE (itlist (fn (l,n) => fn list => 209 case filt n 210 of LEAF [] => list 211 | NODE [] => list 212 | n' => (l,n')::list) L []) 213 in 214 filt 215 end; 216 217fun listItems0 (LEAF L) = L 218 | listItems0 (NODE L) = rev_itlist (append o listItems0 o #2) L []; 219 220fun union net1 net2 = rev_itlist insert (listItems0 net1) net2; 221 222fun listItems net = map #2 (listItems0 net); 223 224fun map f (LEAF L) = LEAF (List.map (fn (x,y) => (x, f y)) L) 225 | map f (NODE L) = NODE (List.map (fn (l,net) => (l,map f net)) L); 226 227fun itnet f (LEAF L) b = itlist f (List.map #2 L) b 228 | itnet f (NODE L) b = itlist (itnet f) (List.map #2 L) b; 229 230fun size net = itnet (fn x => fn y => y+1) net 0; 231 232 233(*--------------------------------------------------------------------------- 234 Compatibility mode. 235 ---------------------------------------------------------------------------*) 236 237fun get_tip_list (LEAF L) = L 238 | get_tip_list (NODE _) = []; 239 240fun get_edge label = 241 let fun get (NODE edges) = 242 (case Lib.assoc1 label edges 243 of SOME (_,net) => net 244 | NONE => empty) 245 | get (LEAF _) = raise ERR "get_edge" "tips have no edges" 246 in get 247 end; 248 249fun net_update elem = 250let fun update _ _ (LEAF _) = raise ERR "net_update" "cannot update a tip" 251 | update defd tm (net as (NODE edges)) = 252 let fun exec_defd [] net = LEAF (elem::get_tip_list net) 253 | exec_defd (h::rst) net = update rst h net 254 val label = label_of tm 255 val child = get_edge label net 256 val new_child = 257 case label 258 of Cmb => let val (Rator,Rand) = Term.dest_comb tm 259 in update (Rator::defd) Rand child 260 end 261 | Lam => update defd (Term.body tm) child 262 | _ => exec_defd defd child 263 in NODE (overwrite (label,new_child) edges) 264 end 265in update 266end; 267 268fun enter (tm,elem) net = net_update (tm,elem) [] tm net; 269 270fun follow tm net = 271 let val nets = 272 case (label_of tm) 273 of (label as Cnst _) => [get_edge label net] 274 | V => [] 275 | Lam => follow (Term.body tm) (get_edge Lam net) 276 | Cmb => let val (Rator,Rand) = Term.dest_comb tm 277 in Lib.itlist(fn i => fn A => (follow Rator i @ A)) 278 (follow Rand (get_edge Cmb net)) [] 279 end 280 in List.filter (not o is_empty) (get_edge V net::nets) 281 end; 282 283fun lookup tm net = 284 if is_empty net then [] 285 else 286 itlist (fn (LEAF L) => (fn A => (List.map #2 L @ A)) | (NODE _) => I) 287 (follow tm net) []; 288 289end (* Net *) 290