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