src/Tools/IsaPlanner/zipper.ML
author wenzelm
Thu May 31 20:55:29 2007 +0200 (2007-05-31)
changeset 23171 861f63a35d31
child 23175 267ba70e7a9d
permissions -rw-r--r--
moved IsaPlanner from Provers to Tools;
     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 or-choices *)
   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 McBridge-speak, 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);