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