23175

1 
(* Title: Tools/IsaPlanner/zipper.ML

23171

2 
Author: Lucas Dixon, University of Edinburgh

23175

3 


4 
A notion roughly based on Huet's Zippers for Isabelle terms.

23171

5 
*)


6 


7 
(* abstract term for no more than pattern matching *)


8 
signature ABSTRACT_TRM =


9 
sig


10 
type typ (* types *)


11 
type aname (* abstraction names *)


12 
type fname (* parameter/free variable names *)


13 
type cname (* constant names *)


14 
type vname (* meta variable names *)


15 
type bname (* bound var name *)


16 
datatype 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;


22 
type T = term;


23 
end;


24 


25 
structure IsabelleTrmWrap : ABSTRACT_TRM=


26 
struct


27 
open Term;


28 
type typ = Term.typ; (* types *)


29 
type aname = string; (* abstraction names *)


30 
type fname = string; (* parameter/free variable names *)


31 
type cname = string; (* constant names *)


32 
type vname = string * int; (* meta variable names *)


33 
type bname = int; (* bound var name *)


34 
type T = term;


35 
end;


36 


37 
(* Concrete version for the Trm structure *)


38 
signature TRM_CTXT_DATA =


39 
sig


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


47 
end;


48 


49 
(* A trm context = list of derivatives *)


50 
signature TRM_CTXT =


51 
sig


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 


78 
end;


79 


80 
(* A zipper = a term looked at, at a particular point in the term *)


81 
signature ZIPPER =


82 
sig


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 orchoices *)


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 


156 
end;


157 


158 


159 
(* Zipper data for an generic trm *)


160 
functor TrmCtxtDataFUN(Trm : ABSTRACT_TRM)


161 
: TRM_CTXT_DATA


162 
= struct


163 


164 
structure Trm = Trm;


165 


166 
(* a dtrm is, in McBridgespeak, 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 


182 
end;


183 


184 


185 
(* functor for making term contexts given term data *)


186 
functor TrmCtxtFUN(D : TRM_CTXT_DATA)


187 
: TRM_CTXT =


188 
struct


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 


228 
end;


229 


230 
(* zippers in terms of term contexts *)


231 
functor 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 


388 
end;


389 


390 
(* now build these for Isabelle terms *)


391 
structure TrmCtxtData = TrmCtxtDataFUN(IsabelleTrmWrap);


392 
structure TrmCtxt = TrmCtxtFUN(TrmCtxtData);


393 
structure 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 
*)


411 
signature ZIPPER_SEARCH =


412 
sig


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 


423 
end;


424 


425 
functor ZipperSearchFUN(Zipper : ZIPPER) : ZIPPER_SEARCH


426 
= struct


427 


428 
structure Z = Zipper;


429 
structure C = Z.C;


430 
structure D = C.D;


431 
structure Trm = D.Trm;


432 


433 
fun 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];


439 
fun 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];


445 
val leaves_lr = Z.lzy_search sf_leaves_lr;


446 
val leaves_rl = Z.lzy_search sf_leaves_rl;


447 


448 


449 
fun 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];


455 
fun 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];


461 
fun 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];


468 
fun 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 


475 
val all_td_lr = Z.lzy_search sf_all_td_lr;


476 
val all_td_rl = Z.lzy_search sf_all_td_rl;


477 
val all_bl_ur = Z.lzy_search sf_all_bl_ru;


478 
val all_bl_ru = Z.lzy_search sf_all_bl_ur;


479 


480 
end;


481 


482 


483 
structure ZipperSearch = ZipperSearchFUN(Zipper);
