--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/IsaPlanner/zipper.ML Sun Jun 11 00:28:18 2006 +0200
@@ -0,0 +1,462 @@
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+(* Title: Pure/IsaPlanner/zipper.ML
+ ID: $Id$
+ Author: Lucas Dixon, University of Edinburgh
+ lucas.dixon@ed.ac.uk
+ Created: 24 Mar 2006
+*)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+(* DESCRIPTION:
+ A notion roughly based on Huet's Zippers for Isabelle terms.
+*)
+
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+
+(* abstract term for no more than pattern matching *)
+signature ABSTRACT_TRM =
+sig
+type typ (* types *)
+type aname (* abstraction names *)
+type fname (* parameter/free variable names *)
+type cname (* constant names *)
+type vname (* meta variable names *)
+type bname (* bound var name *)
+datatype term = Const of (cname * typ)
+ | Abs of (aname * typ * term)
+ | Free of (fname * typ)
+ | Var of (vname * typ)
+ | Bound of bname
+ | $ of term * term;
+type T = term;
+end;
+
+structure IsabelleTrmWrap : ABSTRACT_TRM=
+struct
+open Term;
+type typ = Term.typ; (* types *)
+type aname = string; (* abstraction names *)
+type fname = string; (* parameter/free variable names *)
+type cname = string; (* constant names *)
+type vname = string * int; (* meta variable names *)
+type bname = int; (* bound var name *)
+type T = term;
+end;
+
+(* Concrete version for the Trm structure *)
+signature TRM_CTXT_DATA =
+sig
+
+ structure Trm : ABSTRACT_TRM
+ datatype dtrm = Abs of Trm.aname * Trm.typ
+ | AppL of Trm.T
+ | AppR of Trm.T;
+ val apply : dtrm -> Trm.T -> Trm.T
+ val eq_pos : dtrm * dtrm -> bool
+end;
+
+(* A trm context = list of derivatives *)
+signature TRM_CTXT =
+sig
+ structure D : TRM_CTXT_DATA
+ type T = D.dtrm list
+
+ val empty : T
+ val is_empty : T -> bool
+
+ val eq_path : T * T -> bool
+
+ val add_outerctxt : T -> T -> T
+
+ val apply : T -> D.Trm.T -> D.Trm.T
+
+ val nty_ctxt : T -> (D.Trm.aname * D.Trm.typ) list;
+ val ty_ctxt : T -> D.Trm.typ list;
+
+ val depth : T -> int;
+ val map : (D.dtrm -> D.dtrm) -> T -> T
+ val fold : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
+
+end;
+
+(* A zipper = a term looked at, at a particular point in the term *)
+signature ZIPPER =
+sig
+ structure C : TRM_CTXT
+ type T
+
+ val mktop : C.D.Trm.T -> T
+ val goto_top : T -> T
+ val at_top : T -> bool
+ val mk : (C.D.Trm.T * C.T) -> T
+ val set_trm : C.D.Trm.T -> T -> T
+ val set_ctxt : C.T -> T -> T
+
+ val split : T -> T * C.T
+ val add_outerctxt : C.T -> T -> T
+
+ val ctxt : T -> C.T
+ val trm : T -> C.D.Trm.T
+
+ val nty_ctxt : T -> (C.D.Trm.aname * C.D.Trm.typ) list;
+ val ty_ctxt : T -> C.D.Trm.typ list;
+
+ val depth_of_ctxt : T -> int;
+ val map_on_ctxt : (C.D.dtrm -> C.D.dtrm) -> T -> T
+ val fold_on_ctxt : (C.D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
+
+ (* searching through a zipper *)
+ datatype zsearch = Here of T | LookIn of T;
+ (* lazily search through the zipper *)
+ val lzy_search : (T -> zsearch list) -> T -> T Seq.seq
+ (* lazy search with folded data *)
+ val pf_lzy_search : ('a -> T -> ('a * zsearch list))
+ -> 'a -> T -> T Seq.seq
+ (* zsearch list is or-choices *)
+ val searchfold : ('a -> T -> (('a * zsearch) list))
+ -> 'a -> T -> ('a * T) Seq.seq
+ (* limit function to the current focus of the zipper,
+ but give function the zipper's context *)
+ val limit_pcapply : (C.T -> T -> ('a * T) Seq.seq)
+ -> T -> ('a * T) Seq.seq
+ val limit_apply : (T -> T Seq.seq) -> T -> T Seq.seq
+ val limit_capply : (C.T -> T -> T Seq.seq) -> T -> T Seq.seq
+
+ (* moving around zippers with option types *)
+ val omove_up : T -> T option
+ val omove_up_abs : T -> T option
+ val omove_up_app : T -> T option
+ val omove_up_left : T -> T option
+ val omove_up_right : T -> T option
+ val omove_up_left_or_abs : T -> T option
+ val omove_up_right_or_abs : T -> T option
+ val omove_down_abs : T -> T option
+ val omove_down_left : T -> T option
+ val omove_down_right : T -> T option
+ val omove_down_app : T -> (T * T) option
+
+ (* moving around zippers, raising exceptions *)
+ exception move of string * T
+ val move_up : T -> T
+ val move_up_abs : T -> T
+ val move_up_app : T -> T
+ val move_up_left : T -> T
+ val move_up_right : T -> T
+ val move_up_left_or_abs : T -> T
+ val move_up_right_or_abs : T -> T
+ val move_down_abs : T -> T
+ val move_down_left : T -> T
+ val move_down_right : T -> T
+ val move_down_app : T -> T * T
+
+end;
+
+
+(* Zipper data for an generic trm *)
+functor TrmCtxtDataFUN(Trm : ABSTRACT_TRM)
+: TRM_CTXT_DATA
+= struct
+
+ structure Trm = Trm;
+
+ (* a dtrm is, in McBridge-speak, a differentiated term. It represents
+ the different ways a term can occur within its datatype constructors *)
+ datatype dtrm = Abs of Trm.aname * Trm.typ
+ | AppL of Trm.T
+ | AppR of Trm.T;
+
+ (* apply a dtrm to a term, ie put the dtrm above it, building context *)
+ fun apply (Abs (s,ty)) t = Trm.Abs (s,ty,t)
+ | apply (AppL tl) tr = Trm.$ (tl, tr)
+ | apply (AppR tr) tl = Trm.$ (tl, tr);
+
+ fun eq_pos (Abs _, Abs _) = true
+ | eq_pos (AppL _, AppL _) = true
+ | eq_pos (AppR _, AppR _) = true
+ | eq_pos _ = false;
+
+end;
+
+
+(* functor for making term contexts given term data *)
+functor TrmCtxtFUN(D : TRM_CTXT_DATA)
+ : TRM_CTXT =
+struct
+ structure D = D;
+
+ type T = D.dtrm list;
+
+ val empty = [];
+ val is_empty = List.null;
+
+ fun eq_path ([], []) = true
+ | eq_path ([], _::_) = false
+ | eq_path ( _::_, []) = false
+ | eq_path (h::t, h2::t2) =
+ D.eq_pos(h,h2) andalso eq_path (t, t2);
+
+ (* add context to outside of existing context *)
+ fun add_outerctxt ctop cbottom = cbottom @ ctop;
+
+ (* mkterm : zipper -> trm -> trm *)
+ val apply = Library.fold D.apply;
+
+ (* named type context *)
+ val nty_ctxt = List.foldr (fn (D.Abs nty,ntys) => nty::ntys
+ | (_,ntys) => ntys) [];
+ (* type context *)
+ val ty_ctxt = List.foldr (fn (D.Abs (_,ty),tys) => ty::tys
+ | (_,tys) => tys) [];
+
+ val depth = length : T -> int;
+
+ val map = List.map : (D.dtrm -> D.dtrm) -> T -> T
+
+ val fold = Library.fold : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a;
+
+end;
+
+(* zippers in terms of term contexts *)
+functor ZipperFUN(C : TRM_CTXT)
+ : ZIPPER
+= struct
+
+ structure C = C;
+ structure D = C.D;
+ structure Trm = D.Trm;
+
+ type T = C.D.Trm.T * C.T;
+
+ fun mktop t = (t, C.empty) : T
+
+ val mk = I;
+ val set_trm = apfst o K;
+ val set_ctxt = apsnd o K;
+
+ fun goto_top (z as (t,c)) =
+ if C.is_empty c then z else (C.apply c t, C.empty);
+
+ fun at_top (_,c) = C.is_empty c;
+
+ fun split (t,c) = ((t,C.empty) : T, c : C.T)
+ fun add_outerctxt c (t,c2) = (t, C.add_outerctxt c c2) : T
+
+ val ctxt = snd;
+ val trm = fst;
+
+ val nty_ctxt = C.nty_ctxt o ctxt;
+ val ty_ctxt = C.ty_ctxt o ctxt;
+
+ val depth_of_ctxt = C.depth o ctxt;
+ val map_on_ctxt = apsnd o C.map;
+ fun fold_on_ctxt f = C.fold f o ctxt;
+
+ fun omove_up (t,(d::c)) = SOME (D.apply d t, c)
+ | omove_up (z as (_,[])) = NONE;
+ fun omove_up_abs (t,((D.Abs(n,ty))::c)) = SOME (Trm.Abs(n,ty,t), c)
+ | omove_up_abs z = NONE;
+ fun omove_up_app (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c)
+ | omove_up_app (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c)
+ | omove_up_app z = NONE;
+ fun omove_up_left (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c)
+ | omove_up_left z = NONE;
+ fun omove_up_right (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c)
+ | omove_up_right _ = NONE;
+ fun omove_up_left_or_abs (t,(D.AppL tl)::c) =
+ SOME (Trm.$(tl,t), c)
+ | omove_up_left_or_abs (t,(D.Abs (n,ty))::c) =
+ SOME (Trm.Abs(n,ty,t), c)
+ | omove_up_left_or_abs z = NONE;
+ fun omove_up_right_or_abs (t,(D.Abs (n,ty))::c) =
+ SOME (Trm.Abs(n,ty,t), c)
+ | omove_up_right_or_abs (t,(D.AppR tr)::c) =
+ SOME (Trm.$(t,tr), c)
+ | omove_up_right_or_abs _ = NONE;
+ fun omove_down_abs (Trm.Abs(s,ty,t),c) = SOME (t,(D.Abs(s,ty))::c)
+ | omove_down_abs _ = NONE;
+ fun omove_down_left (Trm.$(l,r),c) = SOME (l,(D.AppR r)::c)
+ | omove_down_left _ = NONE;
+ fun omove_down_right (Trm.$(l,r),c) = SOME (r,(D.AppL l)::c)
+ | omove_down_right _ = NONE;
+ fun omove_down_app (Trm.$(l,r),c) =
+ SOME ((l,(D.AppR r)::c),(r,(D.AppL l)::c))
+ | omove_down_app _ = NONE;
+
+ exception move of string * T
+ fun move_up (t,(d::c)) = (D.apply d t, c)
+ | move_up (z as (_,[])) = raise move ("move_up",z);
+ fun move_up_abs (t,((D.Abs(n,ty))::c)) = (Trm.Abs(n,ty,t), c)
+ | move_up_abs z = raise move ("move_up_abs",z);
+ fun move_up_app (t,(D.AppL tl)::c) = (Trm.$(tl,t), c)
+ | move_up_app (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
+ | move_up_app z = raise move ("move_up_app",z);
+ fun move_up_left (t,((D.AppL tl)::c)) = (Trm.$(tl,t), c)
+ | move_up_left z = raise move ("move_up_left",z);
+ fun move_up_right (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
+ | move_up_right z = raise move ("move_up_right",z);
+ fun move_up_left_or_abs (t,(D.AppL tl)::c) = (Trm.$(tl,t), c)
+ | move_up_left_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c)
+ | move_up_left_or_abs z = raise move ("move_up_left_or_abs",z);
+ fun move_up_right_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c)
+ | move_up_right_or_abs (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
+ | move_up_right_or_abs z = raise move ("move_up_right_or_abs",z);
+ fun move_down_abs (Trm.Abs(s,ty,t),c) = (t,(D.Abs(s,ty))::c)
+ | move_down_abs z = raise move ("move_down_abs",z);
+ fun move_down_left (Trm.$(l,r),c) = (l,(D.AppR r)::c)
+ | move_down_left z = raise move ("move_down_left",z);
+ fun move_down_right (Trm.$(l,r),c) = (r,(D.AppL l)::c)
+ | move_down_right z = raise move ("move_down_right",z);
+ fun move_down_app (Trm.$(l,r),c) =
+ ((l,(D.AppR r)::c),(r,(D.AppL l)::c))
+ | move_down_app z = raise move ("move_down_app",z);
+
+
+ (* Note: interpretted as being examined depth first *)
+ datatype zsearch = Here of T | LookIn of T;
+
+ fun lzy_search fsearch =
+ let
+ fun lzyl [] () = NONE
+ | lzyl ((Here z) :: more) () = SOME(z, Seq.make (lzyl more))
+ | lzyl ((LookIn z) :: more) () =
+ (case lzy z
+ of NONE => NONE
+ | SOME (hz,mz) =>
+ SOME (hz, Seq.append (mz, Seq.make (lzyl more))))
+ and lzy z = lzyl (fsearch z) ()
+ in Seq.make o lzyl o fsearch end;
+
+ (* path folded lazy search - the search list is defined in terms of
+ the path passed through: the data a is updated with every zipper
+ considered *)
+ fun pf_lzy_search fsearch a0 z =
+ let
+ fun lzyl a [] () = NONE
+ | lzyl a ((Here z) :: more) () = SOME(z, Seq.make (lzyl a more))
+ | lzyl a ((LookIn z) :: more) () =
+ (case lzy a z
+ of NONE => lzyl a more ()
+ | SOME(hz,mz) => SOME(hz,Seq.append(mz,Seq.make(lzyl a more))))
+ and lzy a z =
+ let val (a2, slist) = (fsearch a z) in lzyl a2 slist () end
+
+ val (a,slist) = fsearch a0 z
+ in Seq.make (lzyl a slist) end;
+
+ (* Note: depth first over zsearch results *)
+ fun searchfold fsearch a0 z =
+ let
+ fun lzyl [] () = NONE
+ | lzyl ((a, Here z) :: more) () =
+ SOME((a,z), Seq.make (lzyl more))
+ | lzyl ((a, LookIn z) :: more) () =
+ (case lzyl (fsearch a z) () of
+ NONE => lzyl more ()
+ | SOME (z,mz) => SOME (z,Seq.append(mz, Seq.make (lzyl more))))
+ in Seq.make (lzyl (fsearch a0 z)) end;
+
+
+ fun limit_pcapply f z =
+ let val (z2,c) = split z
+ in Seq.map (apsnd (add_outerctxt c)) (f c z2) end;
+ fun limit_capply (f : C.T -> T -> T Seq.seq) (z : T) =
+ let val ((z2 : T),(c : C.T)) = split z
+ in Seq.map (add_outerctxt c) (f c z2) end
+
+ val limit_apply = limit_capply o K;
+
+end;
+
+(* now build these for Isabelle terms *)
+structure TrmCtxtData = TrmCtxtDataFUN(IsabelleTrmWrap);
+structure TrmCtxt = TrmCtxtFUN(TrmCtxtData);
+structure Zipper = ZipperFUN(TrmCtxt);
+
+
+
+(* For searching through Zippers below the current focus...
+ KEY for naming scheme:
+
+ td = starting at the top down
+ lr = going from left to right
+ rl = going from right to left
+
+ bl = starting at the bottom left
+ br = starting at the bottom right
+ ul = going up then left
+ ur = going up then right
+ ru = going right then up
+ lu = going left then up
+*)
+signature ZIPPER_SEARCH =
+sig
+ structure Z : ZIPPER;
+
+ val leaves_lr : Z.T -> Z.T Seq.seq
+ val leaves_rl : Z.T -> Z.T Seq.seq
+
+ val all_bl_ru : Z.T -> Z.T Seq.seq
+ val all_bl_ur : Z.T -> Z.T Seq.seq
+ val all_td_lr : Z.T -> Z.T Seq.seq
+ val all_td_rl : Z.T -> Z.T Seq.seq
+
+end;
+
+functor ZipperSearchFUN(Zipper : ZIPPER) : ZIPPER_SEARCH
+= struct
+
+structure Z = Zipper;
+structure C = Z.C;
+structure D = C.D;
+structure Trm = D.Trm;
+
+fun sf_leaves_lr z =
+ case Z.trm z
+ of Trm.$ _ => [Z.LookIn (Z.move_down_left z),
+ Z.LookIn (Z.move_down_right z)]
+ | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)]
+ | _ => [Z.Here z];
+fun sf_leaves_rl z =
+ case Z.trm z
+ of Trm.$ _ => [Z.LookIn (Z.move_down_right z),
+ Z.LookIn (Z.move_down_left z)]
+ | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)]
+ | _ => [Z.Here z];
+val leaves_lr = Z.lzy_search sf_leaves_lr;
+val leaves_rl = Z.lzy_search sf_leaves_rl;
+
+
+fun sf_all_td_lr z =
+ case Z.trm z
+ of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_left z),
+ Z.LookIn (Z.move_down_right z)]
+ | Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)]
+ | _ => [Z.Here z];
+fun sf_all_td_rl z =
+ case Z.trm z
+ of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_right z),
+ Z.LookIn (Z.move_down_left z)]
+ | Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)]
+ | _ => [Z.Here z];
+fun sf_all_bl_ur z =
+ case Z.trm z
+ of Trm.$ _ => [Z.LookIn (Z.move_down_left z), Z.Here z,
+ Z.LookIn (Z.move_down_right z)]
+ | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z),
+ Z.Here z]
+ | _ => [Z.Here z];
+fun sf_all_bl_ru z =
+ case Z.trm z
+ of Trm.$ _ => [Z.LookIn (Z.move_down_left z),
+ Z.LookIn (Z.move_down_right z), Z.Here z]
+ | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z), Z.Here z]
+ | _ => [Z.Here z];
+
+val all_td_lr = Z.lzy_search sf_all_td_lr;
+val all_td_rl = Z.lzy_search sf_all_td_lr;
+val all_bl_ur = Z.lzy_search sf_all_bl_ru;
+val all_bl_ru = Z.lzy_search sf_all_bl_ur;
+
+end;
+
+
+structure ZipperSearch = ZipperSearchFUN(Zipper);