1(* Title: Tools/IsaPlanner/zipper.ML 2 Author: Lucas Dixon, University of Edinburgh 3 4A notion roughly based on Huet's Zippers for Isabelle terms. 5*) 6 7(* abstract term for no more than pattern matching *) 8signature ABSTRACT_TRM = 9sig 10type typ (* types *) 11type aname (* abstraction names *) 12type fname (* parameter/free variable names *) 13type cname (* constant names *) 14type vname (* meta variable names *) 15type bname (* bound var name *) 16datatype term = Const of cname * typ 17 | Abs of aname * typ * term 18 | Free of fname * typ 19 | Var of vname * typ 20 | Bound of bname 21 | $ of term * term; 22type T = term; 23end; 24 25structure IsabelleTrmWrap : ABSTRACT_TRM= 26struct 27open Term; 28type typ = Term.typ; (* types *) 29type aname = string; (* abstraction names *) 30type fname = string; (* parameter/free variable names *) 31type cname = string; (* constant names *) 32type vname = string * int; (* meta variable names *) 33type bname = int; (* bound var name *) 34type T = term; 35end; 36 37(* Concrete version for the Trm structure *) 38signature TRM_CTXT_DATA = 39sig 40 41 structure Trm : ABSTRACT_TRM 42 datatype dtrm = Abs of Trm.aname * Trm.typ 43 | AppL of Trm.T 44 | AppR of Trm.T; 45 val apply : dtrm -> Trm.T -> Trm.T 46 val eq_pos : dtrm * dtrm -> bool 47end; 48 49(* A trm context = list of derivatives *) 50signature TRM_CTXT = 51sig 52 structure D : TRM_CTXT_DATA 53 type T = D.dtrm list; 54 55 val empty : T; 56 val is_empty : T -> bool; 57 58 val add_abs : D.Trm.aname * D.Trm.typ -> T -> T; 59 val add_appl : D.Trm.T -> T -> T; 60 val add_appr : D.Trm.T -> T -> T; 61 62 val add_dtrm : D.dtrm -> T -> T; 63 64 val eq_path : T * T -> bool 65 66 val add_outerctxt : T -> T -> T 67 68 val apply : T -> D.Trm.T -> D.Trm.T 69 70 val nty_ctxt : T -> (D.Trm.aname * D.Trm.typ) list; 71 val ty_ctxt : T -> D.Trm.typ list; 72 73 val depth : T -> int; 74 val map : (D.dtrm -> D.dtrm) -> T -> T 75 val fold_up : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a 76 val fold_down : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a 77 78end; 79 80(* A zipper = a term looked at, at a particular point in the term *) 81signature ZIPPER = 82sig 83 structure C : TRM_CTXT 84 type T 85 86 val mktop : C.D.Trm.T -> T 87 val mk : (C.D.Trm.T * C.T) -> T 88 89 val goto_top : T -> T 90 val at_top : T -> bool 91 92 val split : T -> T * C.T 93 val add_outerctxt : C.T -> T -> T 94 95 val set_trm : C.D.Trm.T -> T -> T 96 val set_ctxt : C.T -> T -> T 97 98 val ctxt : T -> C.T 99 val trm : T -> C.D.Trm.T 100 val top_trm : T -> C.D.Trm.T 101 102 val zipto : C.T -> T -> T (* follow context down *) 103 104 val nty_ctxt : T -> (C.D.Trm.aname * C.D.Trm.typ) list; 105 val ty_ctxt : T -> C.D.Trm.typ list; 106 107 val depth_of_ctxt : T -> int; 108 val map_on_ctxt : (C.D.dtrm -> C.D.dtrm) -> T -> T 109 val fold_up_ctxt : (C.D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a 110 val fold_down_ctxt : (C.D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a 111 112 (* searching through a zipper *) 113 datatype zsearch = Here of T | LookIn of T; 114 (* lazily search through the zipper *) 115 val lzy_search : (T -> zsearch list) -> T -> T Seq.seq 116 (* lazy search with folded data *) 117 val pf_lzy_search : ('a -> T -> ('a * zsearch list)) 118 -> 'a -> T -> T Seq.seq 119 (* zsearch list is or-choices *) 120 val searchfold : ('a -> T -> (('a * zsearch) list)) 121 -> 'a -> T -> ('a * T) Seq.seq 122 (* limit function to the current focus of the zipper, 123 but give function the zipper's context *) 124 val limit_pcapply : (C.T -> T -> ('a * T) Seq.seq) 125 -> T -> ('a * T) Seq.seq 126 val limit_apply : (T -> T Seq.seq) -> T -> T Seq.seq 127 val limit_capply : (C.T -> T -> T Seq.seq) -> T -> T Seq.seq 128 129 (* moving around zippers with option types *) 130 val omove_up : T -> T option 131 val omove_up_abs : T -> T option 132 val omove_up_app : T -> T option 133 val omove_up_left : T -> T option 134 val omove_up_right : T -> T option 135 val omove_up_left_or_abs : T -> T option 136 val omove_up_right_or_abs : T -> T option 137 val omove_down_abs : T -> T option 138 val omove_down_left : T -> T option 139 val omove_down_right : T -> T option 140 val omove_down_app : T -> (T * T) option 141 142 (* moving around zippers, raising exceptions *) 143 exception move of string * T 144 val move_up : T -> T 145 val move_up_abs : T -> T 146 val move_up_app : T -> T 147 val move_up_left : T -> T 148 val move_up_right : T -> T 149 val move_up_left_or_abs : T -> T 150 val move_up_right_or_abs : T -> T 151 val move_down_abs : T -> T 152 val move_down_left : T -> T 153 val move_down_right : T -> T 154 val move_down_app : T -> T * T 155 156end; 157 158 159(* Zipper data for an generic trm *) 160functor TrmCtxtDataFUN(Trm : ABSTRACT_TRM) 161: TRM_CTXT_DATA 162= struct 163 164 structure Trm = Trm; 165 166 (* a dtrm is, in McBridge-speak, a differentiated term. It represents 167 the different ways a term can occur within its datatype constructors *) 168 datatype dtrm = Abs of Trm.aname * Trm.typ 169 | AppL of Trm.T 170 | AppR of Trm.T; 171 172 (* apply a dtrm to a term, ie put the dtrm above it, building context *) 173 fun apply (Abs (s,ty)) t = Trm.Abs (s,ty,t) 174 | apply (AppL tl) tr = Trm.$ (tl, tr) 175 | apply (AppR tr) tl = Trm.$ (tl, tr); 176 177 fun eq_pos (Abs _, Abs _) = true 178 | eq_pos (AppL _, AppL _) = true 179 | eq_pos (AppR _, AppR _) = true 180 | eq_pos _ = false; 181 182end; 183 184 185(* functor for making term contexts given term data *) 186functor TrmCtxtFUN(D : TRM_CTXT_DATA) 187 : TRM_CTXT = 188struct 189 structure D = D; 190 191 type T = D.dtrm list; 192 193 val empty = []; 194 val is_empty = List.null; 195 196 fun add_abs d l = (D.Abs d) :: l; 197 fun add_appl d l = (D.AppL d) :: l; 198 fun add_appr d l = (D.AppR d) :: l; 199 200 fun add_dtrm d l = d::l; 201 202 fun eq_path ([], []) = true 203 | eq_path ([], _::_) = false 204 | eq_path ( _::_, []) = false 205 | eq_path (h::t, h2::t2) = 206 D.eq_pos(h,h2) andalso eq_path (t, t2); 207 208 (* add context to outside of existing context *) 209 fun add_outerctxt ctop cbottom = cbottom @ ctop; 210 211 (* mkterm : zipper -> trm -> trm *) 212 val apply = Basics.fold D.apply; 213 214 (* named type context *) 215 val nty_ctxt = List.foldr (fn (D.Abs nty,ntys) => nty::ntys 216 | (_,ntys) => ntys) []; 217 (* type context *) 218 val ty_ctxt = List.foldr (fn (D.Abs (_,ty),tys) => ty::tys 219 | (_,tys) => tys) []; 220 221 val depth = length : T -> int; 222 223 val map = List.map : (D.dtrm -> D.dtrm) -> T -> T 224 225 val fold_up = Basics.fold : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a; 226 val fold_down = Basics.fold_rev : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a; 227 228end; 229 230(* zippers in terms of term contexts *) 231functor ZipperFUN(C : TRM_CTXT) 232 : ZIPPER 233= struct 234 235 structure C = C; 236 structure D = C.D; 237 structure Trm = D.Trm; 238 239 type T = C.D.Trm.T * C.T; 240 241 fun mktop t = (t, C.empty) : T 242 243 val mk = I; 244 fun set_trm x = apfst (K x); 245 fun set_ctxt x = apsnd (K x); 246 247 fun goto_top (z as (t,c)) = 248 if C.is_empty c then z else (C.apply c t, C.empty); 249 250 fun at_top (_,c) = C.is_empty c; 251 252 fun split (t,c) = ((t,C.empty) : T, c : C.T) 253 fun add_outerctxt c (t,c2) = (t, C.add_outerctxt c c2) : T 254 255 val ctxt = snd; 256 val trm = fst; 257 val top_trm = trm o goto_top; 258 259 fun nty_ctxt x = C.nty_ctxt (ctxt x); 260 fun ty_ctxt x = C.ty_ctxt (ctxt x); 261 262 fun depth_of_ctxt x = C.depth (ctxt x); 263 fun map_on_ctxt x = apsnd (C.map x); 264 fun fold_up_ctxt f = C.fold_up f o ctxt; 265 fun fold_down_ctxt f = C.fold_down f o ctxt; 266 267 fun omove_up (t,(d::c)) = SOME (D.apply d t, c) 268 | omove_up (z as (_,[])) = NONE; 269 fun omove_up_abs (t,((D.Abs(n,ty))::c)) = SOME (Trm.Abs(n,ty,t), c) 270 | omove_up_abs z = NONE; 271 fun omove_up_app (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c) 272 | omove_up_app (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c) 273 | omove_up_app z = NONE; 274 fun omove_up_left (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c) 275 | omove_up_left z = NONE; 276 fun omove_up_right (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c) 277 | omove_up_right _ = NONE; 278 fun omove_up_left_or_abs (t,(D.AppL tl)::c) = 279 SOME (Trm.$(tl,t), c) 280 | omove_up_left_or_abs (t,(D.Abs (n,ty))::c) = 281 SOME (Trm.Abs(n,ty,t), c) 282 | omove_up_left_or_abs z = NONE; 283 fun omove_up_right_or_abs (t,(D.Abs (n,ty))::c) = 284 SOME (Trm.Abs(n,ty,t), c) 285 | omove_up_right_or_abs (t,(D.AppR tr)::c) = 286 SOME (Trm.$(t,tr), c) 287 | omove_up_right_or_abs _ = NONE; 288 fun omove_down_abs (Trm.Abs(s,ty,t),c) = SOME (t,(D.Abs(s,ty))::c) 289 | omove_down_abs _ = NONE; 290 fun omove_down_left (Trm.$(l,r),c) = SOME (l,(D.AppR r)::c) 291 | omove_down_left _ = NONE; 292 fun omove_down_right (Trm.$(l,r),c) = SOME (r,(D.AppL l)::c) 293 | omove_down_right _ = NONE; 294 fun omove_down_app (Trm.$(l,r),c) = 295 SOME ((l,(D.AppR r)::c),(r,(D.AppL l)::c)) 296 | omove_down_app _ = NONE; 297 298 exception move of string * T 299 fun move_up (t,(d::c)) = (D.apply d t, c) 300 | move_up (z as (_,[])) = raise move ("move_up",z); 301 fun move_up_abs (t,((D.Abs(n,ty))::c)) = (Trm.Abs(n,ty,t), c) 302 | move_up_abs z = raise move ("move_up_abs",z); 303 fun move_up_app (t,(D.AppL tl)::c) = (Trm.$(tl,t), c) 304 | move_up_app (t,(D.AppR tr)::c) = (Trm.$(t,tr), c) 305 | move_up_app z = raise move ("move_up_app",z); 306 fun move_up_left (t,((D.AppL tl)::c)) = (Trm.$(tl,t), c) 307 | move_up_left z = raise move ("move_up_left",z); 308 fun move_up_right (t,(D.AppR tr)::c) = (Trm.$(t,tr), c) 309 | move_up_right z = raise move ("move_up_right",z); 310 fun move_up_left_or_abs (t,(D.AppL tl)::c) = (Trm.$(tl,t), c) 311 | move_up_left_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c) 312 | move_up_left_or_abs z = raise move ("move_up_left_or_abs",z); 313 fun move_up_right_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c) 314 | move_up_right_or_abs (t,(D.AppR tr)::c) = (Trm.$(t,tr), c) 315 | move_up_right_or_abs z = raise move ("move_up_right_or_abs",z); 316 fun move_down_abs (Trm.Abs(s,ty,t),c) = (t,(D.Abs(s,ty))::c) 317 | move_down_abs z = raise move ("move_down_abs",z); 318 fun move_down_left (Trm.$(l,r),c) = (l,(D.AppR r)::c) 319 | move_down_left z = raise move ("move_down_left",z); 320 fun move_down_right (Trm.$(l,r),c) = (r,(D.AppL l)::c) 321 | move_down_right z = raise move ("move_down_right",z); 322 fun move_down_app (Trm.$(l,r),c) = 323 ((l,(D.AppR r)::c),(r,(D.AppL l)::c)) 324 | move_down_app z = raise move ("move_down_app",z); 325 326 (* follow the given path down the given zipper *) 327 (* implicit arguments: C.D.dtrm list, then T *) 328 val zipto = C.fold_down 329 (fn C.D.Abs _ => move_down_abs 330 | C.D.AppL _ => move_down_right 331 | C.D.AppR _ => move_down_left); 332 333 (* Note: interpretted as being examined depth first *) 334 datatype zsearch = Here of T | LookIn of T; 335 336 (* lazy search *) 337 fun lzy_search fsearch = 338 let 339 fun lzyl [] () = NONE 340 | lzyl ((Here z) :: more) () = SOME(z, Seq.make (lzyl more)) 341 | lzyl ((LookIn z) :: more) () = 342 (case lzy z 343 of NONE => NONE 344 | SOME (hz,mz) => 345 SOME (hz, Seq.append mz (Seq.make (lzyl more)))) 346 and lzy z = lzyl (fsearch z) () 347 in Seq.make o lzyl o fsearch end; 348 349 (* path folded lazy search - the search list is defined in terms of 350 the path passed through: the data a is updated with every zipper 351 considered *) 352 fun pf_lzy_search fsearch a0 z = 353 let 354 fun lzyl a [] () = NONE 355 | lzyl a ((Here z) :: more) () = SOME(z, Seq.make (lzyl a more)) 356 | lzyl a ((LookIn z) :: more) () = 357 (case lzy a z 358 of NONE => lzyl a more () 359 | SOME(hz,mz) => SOME(hz,Seq.append mz (Seq.make(lzyl a more)))) 360 and lzy a z = 361 let val (a2, slist) = (fsearch a z) in lzyl a2 slist () end 362 363 val (a,slist) = fsearch a0 z 364 in Seq.make (lzyl a slist) end; 365 366 (* Note: depth first over zsearch results *) 367 fun searchfold fsearch a0 z = 368 let 369 fun lzyl [] () = NONE 370 | lzyl ((a, Here z) :: more) () = 371 SOME((a,z), Seq.make (lzyl more)) 372 | lzyl ((a, LookIn z) :: more) () = 373 (case lzyl (fsearch a z) () of 374 NONE => lzyl more () 375 | SOME (z,mz) => SOME (z,Seq.append mz (Seq.make (lzyl more)))) 376 in Seq.make (lzyl (fsearch a0 z)) end; 377 378 379 fun limit_pcapply f z = 380 let val (z2,c) = split z 381 in Seq.map (apsnd (add_outerctxt c)) (f c z2) end; 382 fun limit_capply (f : C.T -> T -> T Seq.seq) (z : T) = 383 let val ((z2 : T),(c : C.T)) = split z 384 in Seq.map (add_outerctxt c) (f c z2) end 385 386 val limit_apply = limit_capply o K; 387 388end; 389 390(* now build these for Isabelle terms *) 391structure TrmCtxtData = TrmCtxtDataFUN(IsabelleTrmWrap); 392structure TrmCtxt = TrmCtxtFUN(TrmCtxtData); 393structure Zipper = ZipperFUN(TrmCtxt); 394 395 396 397(* For searching through Zippers below the current focus... 398 KEY for naming scheme: 399 400 td = starting at the top down 401 lr = going from left to right 402 rl = going from right to left 403 404 bl = starting at the bottom left 405 br = starting at the bottom right 406 ul = going up then left 407 ur = going up then right 408 ru = going right then up 409 lu = going left then up 410*) 411signature ZIPPER_SEARCH = 412sig 413 structure Z : ZIPPER; 414 415 val leaves_lr : Z.T -> Z.T Seq.seq 416 val leaves_rl : Z.T -> Z.T Seq.seq 417 418 val all_bl_ru : Z.T -> Z.T Seq.seq 419 val all_bl_ur : Z.T -> Z.T Seq.seq 420 val all_td_lr : Z.T -> Z.T Seq.seq 421 val all_td_rl : Z.T -> Z.T Seq.seq 422 423end; 424 425functor ZipperSearchFUN(Zipper : ZIPPER) : ZIPPER_SEARCH 426= struct 427 428structure Z = Zipper; 429structure C = Z.C; 430structure D = C.D; 431structure Trm = D.Trm; 432 433fun sf_leaves_lr z = 434 case Z.trm z 435 of Trm.$ _ => [Z.LookIn (Z.move_down_left z), 436 Z.LookIn (Z.move_down_right z)] 437 | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)] 438 | _ => [Z.Here z]; 439fun sf_leaves_rl z = 440 case Z.trm z 441 of Trm.$ _ => [Z.LookIn (Z.move_down_right z), 442 Z.LookIn (Z.move_down_left z)] 443 | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)] 444 | _ => [Z.Here z]; 445val leaves_lr = Z.lzy_search sf_leaves_lr; 446val leaves_rl = Z.lzy_search sf_leaves_rl; 447 448 449fun sf_all_td_lr z = 450 case Z.trm z 451 of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_left z), 452 Z.LookIn (Z.move_down_right z)] 453 | Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)] 454 | _ => [Z.Here z]; 455fun sf_all_td_rl z = 456 case Z.trm z 457 of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_right z), 458 Z.LookIn (Z.move_down_left z)] 459 | Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)] 460 | _ => [Z.Here z]; 461fun sf_all_bl_ur z = 462 case Z.trm z 463 of Trm.$ _ => [Z.LookIn (Z.move_down_left z), Z.Here z, 464 Z.LookIn (Z.move_down_right z)] 465 | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z), 466 Z.Here z] 467 | _ => [Z.Here z]; 468fun sf_all_bl_ru z = 469 case Z.trm z 470 of Trm.$ _ => [Z.LookIn (Z.move_down_left z), 471 Z.LookIn (Z.move_down_right z), Z.Here z] 472 | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z), Z.Here z] 473 | _ => [Z.Here z]; 474 475val all_td_lr = Z.lzy_search sf_all_td_lr; 476val all_td_rl = Z.lzy_search sf_all_td_rl; 477val all_bl_ur = Z.lzy_search sf_all_bl_ru; 478val all_bl_ru = Z.lzy_search sf_all_bl_ur; 479 480end; 481 482 483structure ZipperSearch = ZipperSearchFUN(Zipper); 484