283 |
283 |
284 fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l |
284 fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l |
285 | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t |
285 | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t |
286 | bot_left_leaf_of x = x; |
286 | bot_left_leaf_of x = x; |
287 |
287 |
|
288 (* Avoid considering replacing terms which have a var at the head as |
|
289 they always succeed trivially, and uninterestingly. *) |
288 fun valid_match_start z = |
290 fun valid_match_start z = |
289 (case bot_left_leaf_of (Z.trm z) of |
291 (case bot_left_leaf_of (Z.trm z) of |
290 Const _ => true |
292 Var _ => false |
291 | Free _ => true |
293 | _ => true); |
292 | Abs _ => true (* allowed to look inside abs... search decides if we actually consider the abstraction itself *) |
294 |
293 | _ => false); (* avoid vars - always suceeds uninterestingly. *) |
|
294 |
|
295 (* search from top, left to right, then down *) |
295 (* search from top, left to right, then down *) |
296 val search_lr_all = ZipperSearch.all_bl_ur; |
296 val search_lr_all = ZipperSearch.all_bl_ur; |
297 |
297 |
298 (* search from top, left to right, then down *) |
298 (* search from top, left to right, then down *) |
299 fun search_lr_valid validf = |
299 fun search_lr_valid validf = |