23171

1 
(* ================================= *)


2 
(* Title: Pure/IsaPlanner/zipper.ML


3 
ID: $Id$


4 
Author: Lucas Dixon, University of Edinburgh


5 
lucas.dixon@ed.ac.uk


6 
Created: 24 Mar 2006


7 
*)


8 
(* ================================= *)


9 
(* DESCRIPTION:


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


11 
*)


12 


13 
(* ================================= *)


14 


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


16 
signature ABSTRACT_TRM =


17 
sig


18 
type typ (* types *)


19 
type aname (* abstraction names *)


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


21 
type cname (* constant names *)


22 
type vname (* meta variable names *)


23 
type bname (* bound var name *)


24 
datatype term = Const of cname * typ


25 
 Abs of aname * typ * term


26 
 Free of fname * typ


27 
 Var of vname * typ


28 
 Bound of bname


29 
 $ of term * term;


30 
type T = term;


31 
end;


32 


33 
structure IsabelleTrmWrap : ABSTRACT_TRM=


34 
struct


35 
open Term;


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


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


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


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


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


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


42 
type T = term;


43 
end;


44 


45 
(* Concrete version for the Trm structure *)


46 
signature TRM_CTXT_DATA =


47 
sig


48 


49 
structure Trm : ABSTRACT_TRM


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


51 
 AppL of Trm.T


52 
 AppR of Trm.T;


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


54 
val eq_pos : dtrm * dtrm > bool


55 
end;


56 


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


58 
signature TRM_CTXT =


59 
sig


60 
structure D : TRM_CTXT_DATA


61 
type T = D.dtrm list;


62 


63 
val empty : T;


64 
val is_empty : T > bool;


65 


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


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


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


69 


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


71 


72 
val eq_path : T * T > bool


73 


74 
val add_outerctxt : T > T > T


75 


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


77 


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


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


80 


81 
val depth : T > int;


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


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


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


85 


86 
end;


87 


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


89 
signature ZIPPER =


90 
sig


91 
structure C : TRM_CTXT


92 
type T


93 


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


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


96 


97 
val goto_top : T > T


98 
val at_top : T > bool


99 


100 
val split : T > T * C.T


101 
val add_outerctxt : C.T > T > T


102 


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


104 
val set_ctxt : C.T > T > T


105 


106 
val ctxt : T > C.T


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


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


109 


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


111 


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


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


114 


115 
val depth_of_ctxt : T > int;


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


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


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


119 


120 
(* searching through a zipper *)


121 
datatype zsearch = Here of T  LookIn of T;


122 
(* lazily search through the zipper *)


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


124 
(* lazy search with folded data *)


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


126 
> 'a > T > T Seq.seq


127 
(* zsearch list is orchoices *)


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


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


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


131 
but give function the zipper's context *)


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


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


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


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


136 


137 
(* moving around zippers with option types *)


138 
val omove_up : T > T option


139 
val omove_up_abs : T > T option


140 
val omove_up_app : T > T option


141 
val omove_up_left : T > T option


142 
val omove_up_right : T > T option


143 
val omove_up_left_or_abs : T > T option


144 
val omove_up_right_or_abs : T > T option


145 
val omove_down_abs : T > T option


146 
val omove_down_left : T > T option


147 
val omove_down_right : T > T option


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


149 


150 
(* moving around zippers, raising exceptions *)


151 
exception move of string * T


152 
val move_up : T > T


153 
val move_up_abs : T > T


154 
val move_up_app : T > T


155 
val move_up_left : T > T


156 
val move_up_right : T > T


157 
val move_up_left_or_abs : T > T


158 
val move_up_right_or_abs : T > T


159 
val move_down_abs : T > T


160 
val move_down_left : T > T


161 
val move_down_right : T > T


162 
val move_down_app : T > T * T


163 


164 
end;


165 


166 


167 
(* Zipper data for an generic trm *)


168 
functor TrmCtxtDataFUN(Trm : ABSTRACT_TRM)


169 
: TRM_CTXT_DATA


170 
= struct


171 


172 
structure Trm = Trm;


173 


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


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


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


177 
 AppL of Trm.T


178 
 AppR of Trm.T;


179 


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


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


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


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


184 


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


186 
 eq_pos (AppL _, AppL _) = true


187 
 eq_pos (AppR _, AppR _) = true


188 
 eq_pos _ = false;


189 


190 
end;


191 


192 


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


194 
functor TrmCtxtFUN(D : TRM_CTXT_DATA)


195 
: TRM_CTXT =


196 
struct


197 
structure D = D;


198 


199 
type T = D.dtrm list;


200 


201 
val empty = [];


202 
val is_empty = List.null;


203 


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


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


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


207 


208 
fun add_dtrm d l = d::l;


209 


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


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


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


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


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


215 


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


217 
fun add_outerctxt ctop cbottom = cbottom @ ctop;


218 


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


220 
val apply = Basics.fold D.apply;


221 


222 
(* named type context *)


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


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


225 
(* type context *)


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


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


228 


229 
val depth = length : T > int;


230 


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


232 


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


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


235 


236 
end;


237 


238 
(* zippers in terms of term contexts *)


239 
functor ZipperFUN(C : TRM_CTXT)


240 
: ZIPPER


241 
= struct


242 


243 
structure C = C;


244 
structure D = C.D;


245 
structure Trm = D.Trm;


246 


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


248 


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


250 


251 
val mk = I;


252 
fun set_trm x = apfst (K x);


253 
fun set_ctxt x = apsnd (K x);


254 


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


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


257 


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


259 


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


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


262 


263 
val ctxt = snd;


264 
val trm = fst;


265 
val top_trm = trm o goto_top;


266 


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


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


269 


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


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


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


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


274 


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


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


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


278 
 omove_up_abs z = NONE;


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


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


281 
 omove_up_app z = NONE;


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


283 
 omove_up_left z = NONE;


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


285 
 omove_up_right _ = NONE;


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


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


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


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


290 
 omove_up_left_or_abs z = NONE;


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


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


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


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


295 
 omove_up_right_or_abs _ = NONE;


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


297 
 omove_down_abs _ = NONE;


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


299 
 omove_down_left _ = NONE;


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


301 
 omove_down_right _ = NONE;


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


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


304 
 omove_down_app _ = NONE;


305 


306 
exception move of string * T


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


333 


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


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


336 
val zipto = C.fold_down


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


338 
 C.D.AppL _ => move_down_right


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


340 


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


342 
datatype zsearch = Here of T  LookIn of T;


343 


344 
(* lazy search *)


345 
fun lzy_search fsearch =


346 
let


347 
fun lzyl [] () = NONE


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


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


350 
(case lzy z


351 
of NONE => NONE


352 
 SOME (hz,mz) =>


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


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


355 
in Seq.make o lzyl o fsearch end;


356 


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


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


359 
considered *)


360 
fun pf_lzy_search fsearch a0 z =


361 
let


362 
fun lzyl a [] () = NONE


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


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


365 
(case lzy a z


366 
of NONE => lzyl a more ()


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


368 
and lzy a z =


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


370 


371 
val (a,slist) = fsearch a0 z


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


373 


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


375 
fun searchfold fsearch a0 z =


376 
let


377 
fun lzyl [] () = NONE


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


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


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


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


382 
NONE => lzyl more ()


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


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


385 


386 


387 
fun limit_pcapply f z =


388 
let val (z2,c) = split z


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


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


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


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


393 


394 
val limit_apply = limit_capply o K;


395 


396 
end;


397 


398 
(* now build these for Isabelle terms *)


399 
structure TrmCtxtData = TrmCtxtDataFUN(IsabelleTrmWrap);


400 
structure TrmCtxt = TrmCtxtFUN(TrmCtxtData);


401 
structure Zipper = ZipperFUN(TrmCtxt);


402 


403 


404 


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


406 
KEY for naming scheme:


407 


408 
td = starting at the top down


409 
lr = going from left to right


410 
rl = going from right to left


411 


412 
bl = starting at the bottom left


413 
br = starting at the bottom right


414 
ul = going up then left


415 
ur = going up then right


416 
ru = going right then up


417 
lu = going left then up


418 
*)


419 
signature ZIPPER_SEARCH =


420 
sig


421 
structure Z : ZIPPER;


422 


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


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


425 


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


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


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


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


430 


431 
end;


432 


433 
functor ZipperSearchFUN(Zipper : ZIPPER) : ZIPPER_SEARCH


434 
= struct


435 


436 
structure Z = Zipper;


437 
structure C = Z.C;


438 
structure D = C.D;


439 
structure Trm = D.Trm;


440 


441 
fun sf_leaves_lr z =


442 
case Z.trm z


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


444 
Z.LookIn (Z.move_down_right z)]


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


446 
 _ => [Z.Here z];


447 
fun sf_leaves_rl z =


448 
case Z.trm z


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


450 
Z.LookIn (Z.move_down_left z)]


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


452 
 _ => [Z.Here z];


453 
val leaves_lr = Z.lzy_search sf_leaves_lr;


454 
val leaves_rl = Z.lzy_search sf_leaves_rl;


455 


456 


457 
fun sf_all_td_lr z =


458 
case Z.trm z


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


460 
Z.LookIn (Z.move_down_right z)]


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


462 
 _ => [Z.Here z];


463 
fun sf_all_td_rl z =


464 
case Z.trm z


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


466 
Z.LookIn (Z.move_down_left z)]


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


468 
 _ => [Z.Here z];


469 
fun sf_all_bl_ur z =


470 
case Z.trm z


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


472 
Z.LookIn (Z.move_down_right z)]


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


474 
Z.Here z]


475 
 _ => [Z.Here z];


476 
fun sf_all_bl_ru z =


477 
case Z.trm z


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


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


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


481 
 _ => [Z.Here z];


482 


483 
val all_td_lr = Z.lzy_search sf_all_td_lr;


484 
val all_td_rl = Z.lzy_search sf_all_td_rl;


485 
val all_bl_ur = Z.lzy_search sf_all_bl_ru;


486 
val all_bl_ru = Z.lzy_search sf_all_bl_ur;


487 


488 
end;


489 


490 


491 
structure ZipperSearch = ZipperSearchFUN(Zipper);
