23175

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

23171

2 
ID: $Id$


3 
Author: Lucas Dixon, University of Edinburgh

23175

4 


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

23171

6 
*)


7 


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


9 
signature ABSTRACT_TRM =


10 
sig


11 
type typ (* types *)


12 
type aname (* abstraction names *)


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


14 
type cname (* constant names *)


15 
type vname (* meta variable names *)


16 
type bname (* bound var name *)


17 
datatype term = Const of cname * typ


18 
 Abs of aname * typ * term


19 
 Free of fname * typ


20 
 Var of vname * typ


21 
 Bound of bname


22 
 $ of term * term;


23 
type T = term;


24 
end;


25 


26 
structure IsabelleTrmWrap : ABSTRACT_TRM=


27 
struct


28 
open Term;


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


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


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


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


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


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


35 
type T = term;


36 
end;


37 


38 
(* Concrete version for the Trm structure *)


39 
signature TRM_CTXT_DATA =


40 
sig


41 


42 
structure Trm : ABSTRACT_TRM


43 
datatype dtrm = Abs of Trm.aname * Trm.typ


44 
 AppL of Trm.T


45 
 AppR of Trm.T;


46 
val apply : dtrm > Trm.T > Trm.T


47 
val eq_pos : dtrm * dtrm > bool


48 
end;


49 


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


51 
signature TRM_CTXT =


52 
sig


53 
structure D : TRM_CTXT_DATA


54 
type T = D.dtrm list;


55 


56 
val empty : T;


57 
val is_empty : T > bool;


58 


59 
val add_abs : D.Trm.aname * D.Trm.typ > T > T;


60 
val add_appl : D.Trm.T > T > T;


61 
val add_appr : D.Trm.T > T > T;


62 


63 
val add_dtrm : D.dtrm > T > T;


64 


65 
val eq_path : T * T > bool


66 


67 
val add_outerctxt : T > T > T


68 


69 
val apply : T > D.Trm.T > D.Trm.T


70 


71 
val nty_ctxt : T > (D.Trm.aname * D.Trm.typ) list;


72 
val ty_ctxt : T > D.Trm.typ list;


73 


74 
val depth : T > int;


75 
val map : (D.dtrm > D.dtrm) > T > T


76 
val fold_up : (D.dtrm > 'a > 'a) > T > 'a > 'a


77 
val fold_down : (D.dtrm > 'a > 'a) > T > 'a > 'a


78 


79 
end;


80 


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


82 
signature ZIPPER =


83 
sig


84 
structure C : TRM_CTXT


85 
type T


86 


87 
val mktop : C.D.Trm.T > T


88 
val mk : (C.D.Trm.T * C.T) > T


89 


90 
val goto_top : T > T


91 
val at_top : T > bool


92 


93 
val split : T > T * C.T


94 
val add_outerctxt : C.T > T > T


95 


96 
val set_trm : C.D.Trm.T > T > T


97 
val set_ctxt : C.T > T > T


98 


99 
val ctxt : T > C.T


100 
val trm : T > C.D.Trm.T


101 
val top_trm : T > C.D.Trm.T


102 


103 
val zipto : C.T > T > T (* follow context down *)


104 


105 
val nty_ctxt : T > (C.D.Trm.aname * C.D.Trm.typ) list;


106 
val ty_ctxt : T > C.D.Trm.typ list;


107 


108 
val depth_of_ctxt : T > int;


109 
val map_on_ctxt : (C.D.dtrm > C.D.dtrm) > T > T


110 
val fold_up_ctxt : (C.D.dtrm > 'a > 'a) > T > 'a > 'a


111 
val fold_down_ctxt : (C.D.dtrm > 'a > 'a) > T > 'a > 'a


112 


113 
(* searching through a zipper *)


114 
datatype zsearch = Here of T  LookIn of T;


115 
(* lazily search through the zipper *)


116 
val lzy_search : (T > zsearch list) > T > T Seq.seq


117 
(* lazy search with folded data *)


118 
val pf_lzy_search : ('a > T > ('a * zsearch list))


119 
> 'a > T > T Seq.seq


120 
(* zsearch list is orchoices *)


121 
val searchfold : ('a > T > (('a * zsearch) list))


122 
> 'a > T > ('a * T) Seq.seq


123 
(* limit function to the current focus of the zipper,


124 
but give function the zipper's context *)


125 
val limit_pcapply : (C.T > T > ('a * T) Seq.seq)


126 
> T > ('a * T) Seq.seq


127 
val limit_apply : (T > T Seq.seq) > T > T Seq.seq


128 
val limit_capply : (C.T > T > T Seq.seq) > T > T Seq.seq


129 


130 
(* moving around zippers with option types *)


131 
val omove_up : T > T option


132 
val omove_up_abs : T > T option


133 
val omove_up_app : T > T option


134 
val omove_up_left : T > T option


135 
val omove_up_right : T > T option


136 
val omove_up_left_or_abs : T > T option


137 
val omove_up_right_or_abs : T > T option


138 
val omove_down_abs : T > T option


139 
val omove_down_left : T > T option


140 
val omove_down_right : T > T option


141 
val omove_down_app : T > (T * T) option


142 


143 
(* moving around zippers, raising exceptions *)


144 
exception move of string * T


145 
val move_up : T > T


146 
val move_up_abs : T > T


147 
val move_up_app : T > T


148 
val move_up_left : T > T


149 
val move_up_right : T > T


150 
val move_up_left_or_abs : T > T


151 
val move_up_right_or_abs : T > T


152 
val move_down_abs : T > T


153 
val move_down_left : T > T


154 
val move_down_right : T > T


155 
val move_down_app : T > T * T


156 


157 
end;


158 


159 


160 
(* Zipper data for an generic trm *)


161 
functor TrmCtxtDataFUN(Trm : ABSTRACT_TRM)


162 
: TRM_CTXT_DATA


163 
= struct


164 


165 
structure Trm = Trm;


166 


167 
(* a dtrm is, in McBridgespeak, a differentiated term. It represents


168 
the different ways a term can occur within its datatype constructors *)


169 
datatype dtrm = Abs of Trm.aname * Trm.typ


170 
 AppL of Trm.T


171 
 AppR of Trm.T;


172 


173 
(* apply a dtrm to a term, ie put the dtrm above it, building context *)


174 
fun apply (Abs (s,ty)) t = Trm.Abs (s,ty,t)


175 
 apply (AppL tl) tr = Trm.$ (tl, tr)


176 
 apply (AppR tr) tl = Trm.$ (tl, tr);


177 


178 
fun eq_pos (Abs _, Abs _) = true


179 
 eq_pos (AppL _, AppL _) = true


180 
 eq_pos (AppR _, AppR _) = true


181 
 eq_pos _ = false;


182 


183 
end;


184 


185 


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


187 
functor TrmCtxtFUN(D : TRM_CTXT_DATA)


188 
: TRM_CTXT =


189 
struct


190 
structure D = D;


191 


192 
type T = D.dtrm list;


193 


194 
val empty = [];


195 
val is_empty = List.null;


196 


197 
fun add_abs d l = (D.Abs d) :: l;


198 
fun add_appl d l = (D.AppL d) :: l;


199 
fun add_appr d l = (D.AppR d) :: l;


200 


201 
fun add_dtrm d l = d::l;


202 


203 
fun eq_path ([], []) = true


204 
 eq_path ([], _::_) = false


205 
 eq_path ( _::_, []) = false


206 
 eq_path (h::t, h2::t2) =


207 
D.eq_pos(h,h2) andalso eq_path (t, t2);


208 


209 
(* add context to outside of existing context *)


210 
fun add_outerctxt ctop cbottom = cbottom @ ctop;


211 


212 
(* mkterm : zipper > trm > trm *)


213 
val apply = Basics.fold D.apply;


214 


215 
(* named type context *)


216 
val nty_ctxt = List.foldr (fn (D.Abs nty,ntys) => nty::ntys


217 
 (_,ntys) => ntys) [];


218 
(* type context *)


219 
val ty_ctxt = List.foldr (fn (D.Abs (_,ty),tys) => ty::tys


220 
 (_,tys) => tys) [];


221 


222 
val depth = length : T > int;


223 


224 
val map = List.map : (D.dtrm > D.dtrm) > T > T


225 


226 
val fold_up = Basics.fold : (D.dtrm > 'a > 'a) > T > 'a > 'a;


227 
val fold_down = Basics.fold_rev : (D.dtrm > 'a > 'a) > T > 'a > 'a;


228 


229 
end;


230 


231 
(* zippers in terms of term contexts *)


232 
functor ZipperFUN(C : TRM_CTXT)


233 
: ZIPPER


234 
= struct


235 


236 
structure C = C;


237 
structure D = C.D;


238 
structure Trm = D.Trm;


239 


240 
type T = C.D.Trm.T * C.T;


241 


242 
fun mktop t = (t, C.empty) : T


243 


244 
val mk = I;


245 
fun set_trm x = apfst (K x);


246 
fun set_ctxt x = apsnd (K x);


247 


248 
fun goto_top (z as (t,c)) =


249 
if C.is_empty c then z else (C.apply c t, C.empty);


250 


251 
fun at_top (_,c) = C.is_empty c;


252 


253 
fun split (t,c) = ((t,C.empty) : T, c : C.T)


254 
fun add_outerctxt c (t,c2) = (t, C.add_outerctxt c c2) : T


255 


256 
val ctxt = snd;


257 
val trm = fst;


258 
val top_trm = trm o goto_top;


259 


260 
fun nty_ctxt x = C.nty_ctxt (ctxt x);


261 
fun ty_ctxt x = C.ty_ctxt (ctxt x);


262 


263 
fun depth_of_ctxt x = C.depth (ctxt x);


264 
fun map_on_ctxt x = apsnd (C.map x);


265 
fun fold_up_ctxt f = C.fold_up f o ctxt;


266 
fun fold_down_ctxt f = C.fold_down f o ctxt;


267 


268 
fun omove_up (t,(d::c)) = SOME (D.apply d t, c)


269 
 omove_up (z as (_,[])) = NONE;


270 
fun omove_up_abs (t,((D.Abs(n,ty))::c)) = SOME (Trm.Abs(n,ty,t), c)


271 
 omove_up_abs z = NONE;


272 
fun omove_up_app (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c)


273 
 omove_up_app (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c)


274 
 omove_up_app z = NONE;


275 
fun omove_up_left (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c)


276 
 omove_up_left z = NONE;


277 
fun omove_up_right (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c)


278 
 omove_up_right _ = NONE;


279 
fun omove_up_left_or_abs (t,(D.AppL tl)::c) =


280 
SOME (Trm.$(tl,t), c)


281 
 omove_up_left_or_abs (t,(D.Abs (n,ty))::c) =


282 
SOME (Trm.Abs(n,ty,t), c)


283 
 omove_up_left_or_abs z = NONE;


284 
fun omove_up_right_or_abs (t,(D.Abs (n,ty))::c) =


285 
SOME (Trm.Abs(n,ty,t), c)


286 
 omove_up_right_or_abs (t,(D.AppR tr)::c) =


287 
SOME (Trm.$(t,tr), c)


288 
 omove_up_right_or_abs _ = NONE;


289 
fun omove_down_abs (Trm.Abs(s,ty,t),c) = SOME (t,(D.Abs(s,ty))::c)


290 
 omove_down_abs _ = NONE;


291 
fun omove_down_left (Trm.$(l,r),c) = SOME (l,(D.AppR r)::c)


292 
 omove_down_left _ = NONE;


293 
fun omove_down_right (Trm.$(l,r),c) = SOME (r,(D.AppL l)::c)


294 
 omove_down_right _ = NONE;


295 
fun omove_down_app (Trm.$(l,r),c) =


296 
SOME ((l,(D.AppR r)::c),(r,(D.AppL l)::c))


297 
 omove_down_app _ = NONE;


298 


299 
exception move of string * T


300 
fun move_up (t,(d::c)) = (D.apply d t, c)


301 
 move_up (z as (_,[])) = raise move ("move_up",z);


302 
fun move_up_abs (t,((D.Abs(n,ty))::c)) = (Trm.Abs(n,ty,t), c)


303 
 move_up_abs z = raise move ("move_up_abs",z);


304 
fun move_up_app (t,(D.AppL tl)::c) = (Trm.$(tl,t), c)


305 
 move_up_app (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)


306 
 move_up_app z = raise move ("move_up_app",z);


307 
fun move_up_left (t,((D.AppL tl)::c)) = (Trm.$(tl,t), c)


308 
 move_up_left z = raise move ("move_up_left",z);


309 
fun move_up_right (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)


310 
 move_up_right z = raise move ("move_up_right",z);


311 
fun move_up_left_or_abs (t,(D.AppL tl)::c) = (Trm.$(tl,t), c)


312 
 move_up_left_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c)


313 
 move_up_left_or_abs z = raise move ("move_up_left_or_abs",z);


314 
fun move_up_right_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c)


315 
 move_up_right_or_abs (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)


316 
 move_up_right_or_abs z = raise move ("move_up_right_or_abs",z);


317 
fun move_down_abs (Trm.Abs(s,ty,t),c) = (t,(D.Abs(s,ty))::c)


318 
 move_down_abs z = raise move ("move_down_abs",z);


319 
fun move_down_left (Trm.$(l,r),c) = (l,(D.AppR r)::c)


320 
 move_down_left z = raise move ("move_down_left",z);


321 
fun move_down_right (Trm.$(l,r),c) = (r,(D.AppL l)::c)


322 
 move_down_right z = raise move ("move_down_right",z);


323 
fun move_down_app (Trm.$(l,r),c) =


324 
((l,(D.AppR r)::c),(r,(D.AppL l)::c))


325 
 move_down_app z = raise move ("move_down_app",z);


326 


327 
(* follow the given path down the given zipper *)


328 
(* implicit arguments: C.D.dtrm list, then T *)


329 
val zipto = C.fold_down


330 
(fn C.D.Abs _ => move_down_abs


331 
 C.D.AppL _ => move_down_right


332 
 C.D.AppR _ => move_down_left);


333 


334 
(* Note: interpretted as being examined depth first *)


335 
datatype zsearch = Here of T  LookIn of T;


336 


337 
(* lazy search *)


338 
fun lzy_search fsearch =


339 
let


340 
fun lzyl [] () = NONE


341 
 lzyl ((Here z) :: more) () = SOME(z, Seq.make (lzyl more))


342 
 lzyl ((LookIn z) :: more) () =


343 
(case lzy z


344 
of NONE => NONE


345 
 SOME (hz,mz) =>


346 
SOME (hz, Seq.append mz (Seq.make (lzyl more))))


347 
and lzy z = lzyl (fsearch z) ()


348 
in Seq.make o lzyl o fsearch end;


349 


350 
(* path folded lazy search  the search list is defined in terms of


351 
the path passed through: the data a is updated with every zipper


352 
considered *)


353 
fun pf_lzy_search fsearch a0 z =


354 
let


355 
fun lzyl a [] () = NONE


356 
 lzyl a ((Here z) :: more) () = SOME(z, Seq.make (lzyl a more))


357 
 lzyl a ((LookIn z) :: more) () =


358 
(case lzy a z


359 
of NONE => lzyl a more ()


360 
 SOME(hz,mz) => SOME(hz,Seq.append mz (Seq.make(lzyl a more))))


361 
and lzy a z =


362 
let val (a2, slist) = (fsearch a z) in lzyl a2 slist () end


363 


364 
val (a,slist) = fsearch a0 z


365 
in Seq.make (lzyl a slist) end;


366 


367 
(* Note: depth first over zsearch results *)


368 
fun searchfold fsearch a0 z =


369 
let


370 
fun lzyl [] () = NONE


371 
 lzyl ((a, Here z) :: more) () =


372 
SOME((a,z), Seq.make (lzyl more))


373 
 lzyl ((a, LookIn z) :: more) () =


374 
(case lzyl (fsearch a z) () of


375 
NONE => lzyl more ()


376 
 SOME (z,mz) => SOME (z,Seq.append mz (Seq.make (lzyl more))))


377 
in Seq.make (lzyl (fsearch a0 z)) end;


378 


379 


380 
fun limit_pcapply f z =


381 
let val (z2,c) = split z


382 
in Seq.map (apsnd (add_outerctxt c)) (f c z2) end;


383 
fun limit_capply (f : C.T > T > T Seq.seq) (z : T) =


384 
let val ((z2 : T),(c : C.T)) = split z


385 
in Seq.map (add_outerctxt c) (f c z2) end


386 


387 
val limit_apply = limit_capply o K;


388 


389 
end;


390 


391 
(* now build these for Isabelle terms *)


392 
structure TrmCtxtData = TrmCtxtDataFUN(IsabelleTrmWrap);


393 
structure TrmCtxt = TrmCtxtFUN(TrmCtxtData);


394 
structure Zipper = ZipperFUN(TrmCtxt);


395 


396 


397 


398 
(* For searching through Zippers below the current focus...


399 
KEY for naming scheme:


400 


401 
td = starting at the top down


402 
lr = going from left to right


403 
rl = going from right to left


404 


405 
bl = starting at the bottom left


406 
br = starting at the bottom right


407 
ul = going up then left


408 
ur = going up then right


409 
ru = going right then up


410 
lu = going left then up


411 
*)


412 
signature ZIPPER_SEARCH =


413 
sig


414 
structure Z : ZIPPER;


415 


416 
val leaves_lr : Z.T > Z.T Seq.seq


417 
val leaves_rl : Z.T > Z.T Seq.seq


418 


419 
val all_bl_ru : Z.T > Z.T Seq.seq


420 
val all_bl_ur : Z.T > Z.T Seq.seq


421 
val all_td_lr : Z.T > Z.T Seq.seq


422 
val all_td_rl : Z.T > Z.T Seq.seq


423 


424 
end;


425 


426 
functor ZipperSearchFUN(Zipper : ZIPPER) : ZIPPER_SEARCH


427 
= struct


428 


429 
structure Z = Zipper;


430 
structure C = Z.C;


431 
structure D = C.D;


432 
structure Trm = D.Trm;


433 


434 
fun sf_leaves_lr z =


435 
case Z.trm z


436 
of Trm.$ _ => [Z.LookIn (Z.move_down_left z),


437 
Z.LookIn (Z.move_down_right z)]


438 
 Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)]


439 
 _ => [Z.Here z];


440 
fun sf_leaves_rl z =


441 
case Z.trm z


442 
of Trm.$ _ => [Z.LookIn (Z.move_down_right z),


443 
Z.LookIn (Z.move_down_left z)]


444 
 Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)]


445 
 _ => [Z.Here z];


446 
val leaves_lr = Z.lzy_search sf_leaves_lr;


447 
val leaves_rl = Z.lzy_search sf_leaves_rl;


448 


449 


450 
fun sf_all_td_lr z =


451 
case Z.trm z


452 
of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_left z),


453 
Z.LookIn (Z.move_down_right z)]


454 
 Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)]


455 
 _ => [Z.Here z];


456 
fun sf_all_td_rl z =


457 
case Z.trm z


458 
of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_right z),


459 
Z.LookIn (Z.move_down_left z)]


460 
 Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)]


461 
 _ => [Z.Here z];


462 
fun sf_all_bl_ur z =


463 
case Z.trm z


464 
of Trm.$ _ => [Z.LookIn (Z.move_down_left z), Z.Here z,


465 
Z.LookIn (Z.move_down_right z)]


466 
 Trm.Abs _ => [Z.LookIn (Z.move_down_abs z),


467 
Z.Here z]


468 
 _ => [Z.Here z];


469 
fun sf_all_bl_ru z =


470 
case Z.trm z


471 
of Trm.$ _ => [Z.LookIn (Z.move_down_left z),


472 
Z.LookIn (Z.move_down_right z), Z.Here z]


473 
 Trm.Abs _ => [Z.LookIn (Z.move_down_abs z), Z.Here z]


474 
 _ => [Z.Here z];


475 


476 
val all_td_lr = Z.lzy_search sf_all_td_lr;


477 
val all_td_rl = Z.lzy_search sf_all_td_rl;


478 
val all_bl_ur = Z.lzy_search sf_all_bl_ru;


479 
val all_bl_ru = Z.lzy_search sf_all_bl_ur;


480 


481 
end;


482 


483 


484 
structure ZipperSearch = ZipperSearchFUN(Zipper);
