1structure FCNet :> FCNet = 2struct 3 4open Lib HolKernel 5type term = Term.term 6 7val ERR = Feedback.mk_HOL_ERR "FCNet"; 8 9(*---------------------------------------------------------------------------* 10 * Tags corresponding to the underlying term constructors. * 11 *---------------------------------------------------------------------------*) 12 13datatype label 14 = V 15 | Cmb 16 | Lam 17 | Cnst of string * string ; (* name * segment *) 18 19(*---------------------------------------------------------------------------* 20 * Term nets. * 21 *---------------------------------------------------------------------------*) 22 23datatype 'a t 24 = LEAF of (term * 'a) list 25 | NODE of (label * 'a t) list; 26 27 28val empty = NODE []; 29 30fun is_empty (NODE[]) = true 31 | is_empty _ = false; 32 33(*---------------------------------------------------------------------------* 34 * Determining the top constructor of a term. * 35 *---------------------------------------------------------------------------*) 36 37local 38 open Term GrammarSpecials HolKernel 39in 40fun label_of tm = 41 case dest_term tm of 42 LAMB _ => Lam 43 | VAR (s, _) => 44 let 45 in 46 case dest_fakeconst_name s of 47 SOME {original = SOME kid, ...} => Cnst (#Name kid, #Thy kid) 48 | _ => V 49 end 50 | CONST{Name,Thy,...} => Cnst(Name,Thy) 51 | _ => Cmb 52end 53 54fun net_assoc label = 55 let fun get (LEAF _) = raise ERR "net_assoc" "LEAF: no children" 56 | get (NODE subnets) = 57 case Lib.assoc1 label subnets 58 of NONE => empty 59 | SOME (_,net) => net 60 in get 61 end; 62 63 64local 65 fun mtch tm (NODE []) = [] 66 | mtch tm net = 67 let val label = label_of tm 68 val Vnet = net_assoc V net 69 val nets = 70 case label 71 of V => [] 72 | Cnst _ => [net_assoc label net] 73 | Lam => mtch (Term.body tm) (net_assoc Lam net) 74 | Cmb => let val (Rator,Rand) = Term.dest_comb tm 75 in itlist(append o mtch Rand) 76 (mtch Rator (net_assoc Cmb net)) [] 77 end 78 in itlist (fn NODE [] => I | net => cons net) nets [Vnet] 79 end 80in 81fun match tm net = 82 if is_empty net then [] 83 else 84 itlist (fn LEAF L => append (map #2 L) | _ => fn y => y) 85 (mtch tm net) [] 86end; 87 88(*--------------------------------------------------------------------------- 89 Finding the elements mapped by a term in a term net. 90 ---------------------------------------------------------------------------*) 91 92fun index x net = let 93 fun appl _ _ (LEAF L) = SOME L 94 | appl defd tm (NODE L) = 95 let val label = label_of tm 96 in case assoc1 label L 97 of NONE => NONE 98 | SOME (_,net) => 99 case label 100 of Lam => appl defd (Term.body tm) net 101 | Cmb => let val (Rator,Rand) = Term.dest_comb tm 102 in appl (Rand::defd) Rator net end 103 | _ => let fun exec_defd [] (NODE _) = raise ERR "appl" 104 "NODE: should be at a LEAF instead" 105 | exec_defd [] (LEAF L) = SOME L 106 | exec_defd (h::rst) net = appl rst h net 107 in 108 exec_defd defd net 109 end 110 end 111in 112 case appl [] x net 113 of SOME L => map #2 L 114 | NONE => [] 115end; 116 117(*---------------------------------------------------------------------------* 118 * Adding to a term net. * 119 *---------------------------------------------------------------------------*) 120 121fun overwrite (p as (a,_)) = 122 let fun over [] = [p] 123 | over ((q as (x,_))::rst) = 124 if (a=x) then p::rst else q::over rst 125 in over 126 end; 127 128fun insert (p as (tm,_)) N = 129let fun enter _ _ (LEAF _) = raise ERR "insert" "LEAF: cannot insert" 130 | enter defd tm (NODE subnets) = 131 let val label = label_of tm 132 val child = 133 case assoc1 label subnets of NONE => empty | SOME (_,net) => net 134 val new_child = 135 case label 136 of Cmb => let val (Rator,Rand) = Term.dest_comb tm 137 in enter (Rand::defd) Rator child end 138 | Lam => enter defd (Term.body tm) child 139 | _ => let fun exec [] (LEAF L) = LEAF(p::L) 140 | exec [] (NODE _) = LEAF[p] 141 | exec (h::rst) net = enter rst h net 142 in 143 exec defd child 144 end 145 in 146 NODE (overwrite (label,new_child) subnets) 147 end 148in enter [] tm N 149end; 150 151 152(*--------------------------------------------------------------------------- 153 Removing an element from a term net. It is not an error if the 154 element is not there. 155 ---------------------------------------------------------------------------*) 156 157fun split_assoc P = 158 let fun split front [] = raise ERR "split_assoc" "not found" 159 | split front (h::t) = 160 if P h then (rev front,h,t) else split (h::front) t 161 in 162 split [] 163 end; 164 165 166fun delete (tm,P) N = 167let fun del [] = [] 168 | del ((p as (x,q))::rst) = 169 if Term.aconv x tm andalso P q then del rst else p::del rst 170 fun remv _ _ (LEAF L) = LEAF(del L) 171 | remv defd tm (NODE L) = 172 let val label = label_of tm 173 fun pred (x,_) = (x=label) 174 val (left,(_,childnet),right) = split_assoc pred L 175 val childnet' = 176 case label 177 of Lam => remv defd (Term.body tm) childnet 178 | Cmb => let val (Rator,Rand) = Term.dest_comb tm 179 in remv (Rand::defd) Rator childnet end 180 | _ => let fun exec_defd [] (NODE _) = raise ERR "remv" 181 "NODE: should be at a LEAF instead" 182 | exec_defd [] (LEAF L) = LEAF(del L) 183 | exec_defd (h::rst) net = remv rst h net 184 in 185 exec_defd defd childnet 186 end 187 val childnetl = 188 case childnet' of NODE [] => [] | LEAF [] => [] | y => [(label,y)] 189 in 190 NODE (List.concat [left,childnetl,right]) 191 end 192in 193 remv [] tm N handle Feedback.HOL_ERR _ => N 194end; 195 196fun filter P = 197 let fun filt (LEAF L) = LEAF(List.filter (fn (x,y) => P y) L) 198 | filt (NODE L) = 199 NODE (itlist (fn (l,n) => fn list => 200 case filt n 201 of LEAF [] => list 202 | NODE [] => list 203 | n' => (l,n')::list) L []) 204 in 205 filt 206 end; 207 208fun listItems0 (LEAF L) = L 209 | listItems0 (NODE L) = rev_itlist (append o listItems0 o #2) L []; 210 211fun union net1 net2 = rev_itlist insert (listItems0 net1) net2; 212 213fun listItems net = map #2 (listItems0 net); 214 215fun map f (LEAF L) = LEAF (List.map (fn (x,y) => (x, f y)) L) 216 | map f (NODE L) = NODE (List.map (fn (l,net) => (l,map f net)) L); 217 218fun itnet f (LEAF L) b = itlist f (List.map #2 L) b 219 | itnet f (NODE L) b = itlist (itnet f) (List.map #2 L) b; 220 221fun size net = itnet (fn x => fn y => y+1) net 0; 222 223 224(*--------------------------------------------------------------------------- 225 Compatibility mode. 226 ---------------------------------------------------------------------------*) 227 228fun get_tip_list (LEAF L) = L 229 | get_tip_list (NODE _) = []; 230 231fun get_edge label = 232 let fun get (NODE edges) = 233 (case Lib.assoc1 label edges 234 of SOME (_,net) => net 235 | NONE => empty) 236 | get (LEAF _) = raise ERR "get_edge" "tips have no edges" 237 in get 238 end; 239 240fun net_update elem = 241let fun update _ _ (LEAF _) = raise ERR "net_update" "cannot update a tip" 242 | update defd tm (net as (NODE edges)) = 243 let fun exec_defd [] net = LEAF (elem::get_tip_list net) 244 | exec_defd (h::rst) net = update rst h net 245 val label = label_of tm 246 val child = get_edge label net 247 val new_child = 248 case label 249 of Cmb => let val (Rator,Rand) = Term.dest_comb tm 250 in update (Rator::defd) Rand child 251 end 252 | Lam => update defd (Term.body tm) child 253 | _ => exec_defd defd child 254 in NODE (overwrite (label,new_child) edges) 255 end 256in update 257end; 258 259fun enter (tm,elem) net = net_update (tm,elem) [] tm net; 260 261fun follow tm net = 262 let val nets = 263 case (label_of tm) 264 of (label as Cnst _) => [get_edge label net] 265 | V => [] 266 | Lam => follow (Term.body tm) (get_edge Lam net) 267 | Cmb => let val (Rator,Rand) = Term.dest_comb tm 268 in Lib.itlist(fn i => fn A => (follow Rator i @ A)) 269 (follow Rand (get_edge Cmb net)) [] 270 end 271 in List.filter (not o is_empty) (get_edge V net::nets) 272 end; 273 274fun lookup tm net = 275 if is_empty net then [] 276 else 277 itlist (fn (LEAF L) => (fn A => (List.map #2 L @ A)) | (NODE _) => I) 278 (follow tm net) []; 279 280(* term match *) 281structure Map = Binarymap 282fun bvar_free (bvmap, tm) = let 283 (* return true if none of the free variables occur as keys in bvmap *) 284 fun recurse bs t = 285 case dest_term t of 286 v as VAR _ => HOLset.member(bs, t) orelse 287 not (isSome (Map.peek(bvmap, t))) 288 | CONST _ => true 289 | COMB(f,x) => recurse bs f andalso recurse bs x 290 | LAMB(v, body) => recurse (HOLset.add(bs, v)) body 291in 292 Map.numItems bvmap = 0 orelse recurse empty_varset tm 293end 294 295type tminfo = {ids : term HOLset.set, n : int, 296 patbvars : (term,int)Map.dict, 297 obbvars : (term,int)Map.dict, 298 theta : (term,term) Lib.subst} 299 300datatype tmpair = TMP of term * term 301 | BVrestore of {patbvars : (term,int)Map.dict, 302 obbvars : (term,int)Map.dict, 303 n : int} 304fun add_id v {ids, patbvars, obbvars, theta, n} = 305 {ids = HOLset.add(ids, v), patbvars = patbvars, obbvars = obbvars, n = n, 306 theta = theta} 307fun add_binding v tm {ids, patbvars, obbvars, theta, n} = 308 {ids = ids, patbvars = patbvars, obbvars = obbvars, n = n, 309 theta = (v |-> tm) :: theta} 310 311fun MERR s = raise ERR "can_match_term" s 312 313fun mlookup x ids = let 314 fun look [] = if HOLset.member(ids, x) then SOME x else NONE 315 | look ({redex,residue}::t) = if aconv x redex then SOME residue else look t 316in 317 look 318end 319 320fun RM patobs (theta0 as (tminfo, tyS)) = 321 case patobs of 322 [] => true 323 | TMP (t1,t2)::rest => let 324 in 325 case (dest_term t1, dest_term t2) of 326 (VAR(_, ty), _) => let 327 in 328 case Map.peek(#patbvars tminfo, t1) of 329 NONE => (* var on left not bound *) let 330 in 331 if bvar_free (#obbvars tminfo, t2) then 332 (* TODO: aconv below should be "aconv wrt fake-consts" *) 333 RM rest ((case mlookup t1 (#ids tminfo) (#theta tminfo) of 334 NONE => if aconv t1 t2 then add_id t1 tminfo 335 else add_binding t1 t2 tminfo 336 | SOME tm' => if aconv tm' t2 then tminfo 337 else MERR "double bind"), 338 Type.raw_match_type ty (type_of t2) tyS) 339 else 340 MERR "Attempt to capture bound variable" 341 end 342 | SOME i => if is_var t2 andalso 343 Map.peek(#obbvars tminfo, t2) = SOME i 344 then 345 RM rest theta0 346 else false 347 end 348 | (CONST{Name=n1,Thy=thy1,Ty=ty1}, CONST{Name=n2,Thy=thy2,Ty=ty2}) => 349 if n1 <> n2 orelse thy1 <> thy2 then false 350 else RM rest (tminfo, Type.raw_match_type ty1 ty2 tyS) 351 | (CONST{Name,Thy,Ty}, VAR(vnm, vty)) => 352 let 353 in 354 case GrammarSpecials.dest_fakeconst_name vnm of 355 SOME {original = SOME {Name=vnm,Thy=vthy}, ...} => 356 if vnm = Name andalso vthy = Thy then 357 RM rest (tminfo, Type.raw_match_type Ty vty tyS) 358 else false 359 | _ => false 360 end 361 | (COMB(f1, x1), COMB(f2, x2)) => 362 RM (TMP (f1, f2) :: TMP (x1, x2) :: rest) theta0 363 | (LAMB(x1, bdy1), LAMB(x2, bdy2)) => let 364 val tyS' = Type.raw_match_type (type_of x1) (type_of x2) tyS 365 val {ids, patbvars, obbvars, n, theta} = tminfo 366 in 367 RM (TMP (bdy1, bdy2) :: 368 BVrestore {patbvars = patbvars, obbvars = obbvars, n = n} :: 369 rest) 370 ({ids = #ids tminfo, n = n + 1, theta = theta, 371 patbvars = Map.insert(patbvars, x1, n), 372 obbvars = Map.insert(obbvars, x2, n)}, tyS') 373 end 374 | _ => false 375 end 376 | BVrestore{patbvars, obbvars, n} :: rest => let 377 val {ids, theta, ...} = tminfo 378 in 379 RM rest ({ids = ids, theta = theta, patbvars = patbvars, 380 obbvars = obbvars, n = n}, tyS) 381 end 382 383val empty_subst = Map.mkDict Term.compare 384fun can_match_term pat t = 385 RM [TMP (pat,t)] ({ids = empty_tmset, n = 0, theta = [], 386 patbvars = empty_subst, obbvars = empty_subst}, 387 ([], [])) handle HOL_ERR _ => false 388 389end (* Net *) 390