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