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