Quelle zipper.ML Sprache: SML

(*  Title:      Tools/IsaPlanner/zipper.ML
    Author:     Lucas Dixon, University of Edinburgh

A notion roughly based on Huet's Zippers for Isabelle terms.
*)

(* abstract term for no more than pattern matching *)
signature ABSTRACT_TRM =
sig
type typ   (* types *)
type aname (* abstraction names *)
type fname (* parameter/free variable names *)
type cname (* constant names *)
type vname (* meta variable names *)
type bname (* bound var name *)
datatype term = Const of cname * typ
           | Abs of aname * typ * term
           | Free of fname * typ
           | Var of vname * typ
           | Bound of bname
           | $ of term * term;
type T = term;
end;

structure IsabelleTrmWrap : ABSTRACT_TRM=
struct
open Term;
type typ   = Term.typ; (* types *)
type aname = string; (* abstraction names *)
type fname = string; (* parameter/free variable names *)
type cname = string; (* constant names *)
type vname = string * int; (* meta variable names *)
type bname = int; (* bound var name *)
type T = term;
end;

(* Concrete version for the Trm structure *)
signature TRM_CTXT_DATA =
sig

  structure Trm : ABSTRACT_TRM
  datatype dtrm = Abs of Trm.aname * Trm.typ
                | AppL of Trm.T
                | AppR of Trm.T;
  val apply : dtrm -> Trm.T -> Trm.T
  val eq_pos : dtrm * dtrm -> bool
end;

(* A trm context = list of derivatives *)
signature TRM_CTXT =
sig
  structure D : TRM_CTXT_DATA
  type T = D.dtrm list;

  val empty : T;
  val is_empty : T -> bool;

  val add_abs : D.Trm.aname * D.Trm.typ -> T -> T;
  val add_appl : D.Trm.T -> T -> T;
  val add_appr : D.Trm.T -> T -> T;

  val add_dtrm : D.dtrm -> T -> T;

  val eq_path : T * T -> bool

  val add_outerctxt : T -> T -> T

  val apply : T -> D.Trm.T -> D.Trm.T

  val nty_ctxt : T -> (D.Trm.aname * D.Trm.typ) list;
  val ty_ctxt : T -> D.Trm.typ list;

  val depth : T -> int;
  val map : (D.dtrm -> D.dtrm) -> T -> T
  val fold_up : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
  val fold_down : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a

end;

(* A zipper = a term looked at, at a particular point in the term *)
signature ZIPPER =
sig
  structure C : TRM_CTXT
  type T

  val mktop : C.D.Trm.T -> T
  val mk : (C.D.Trm.T * C.T) -> T

  val goto_top : T -> T
  val at_top : T -> bool

  val split : T -> T * C.T
  val add_outerctxt : C.T -> T -> T

  val set_trm : C.D.Trm.T -> T -> T
  val set_ctxt : C.T -> T -> T

  val ctxt : T -> C.T
  val trm : T -> C.D.Trm.T
  val top_trm : T -> C.D.Trm.T

  val zipto : C.T -> T -> T (* follow context down *)

  val nty_ctxt : T -> (C.D.Trm.aname * C.D.Trm.typ) list;
  val ty_ctxt : T -> C.D.Trm.typ list;

  val depth_of_ctxt : T -> int;
  val map_on_ctxt : (C.D.dtrm -> C.D.dtrm) -> T -> T
  val fold_up_ctxt : (C.D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
  val fold_down_ctxt : (C.D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a

  (* searching through a zipper *)
  datatype zsearch = Here of T | LookIn of T;
  (* lazily search through the zipper *)
  val lzy_search : (T -> zsearch list) -> T -> T Seq.seq
  (* lazy search with folded data *)
  val pf_lzy_search : ('a -> T -> ('a * zsearch list))
                      -> 'a -> T -> T Seq.seq
  (* zsearch list is or-choices *)
  val searchfold : ('a -> T -> (('a * zsearch) list))
                      -> 'a -> T -> ('a * T) Seq.seq
  (* limit function to the current focus of the zipper,
     but give function the zipper's context *)
  val limit_pcapply : (C.T -> T -> ('a * T) Seq.seq)
                      -> T -> ('a * T) Seq.seq
  val limit_apply : (T -> T Seq.seq) -> T -> T Seq.seq
  val limit_capply : (C.T -> T -> T Seq.seq) -> T -> T Seq.seq

  (* moving around zippers with option types *)
  val omove_up : T -> T option
  val omove_up_abs : T -> T option
  val omove_up_app : T -> T option
  val omove_up_left : T -> T option
  val omove_up_right : T -> T option
  val omove_up_left_or_abs : T -> T option
  val omove_up_right_or_abs : T -> T option
  val omove_down_abs : T -> T option
  val omove_down_left : T -> T option
  val omove_down_right : T -> T option
  val omove_down_app : T -> (T * T) option

  (* moving around zippers, raising exceptions *)
  exception move of string * T
  val move_up : T -> T
  val move_up_abs : T -> T
  val move_up_app : T -> T
  val move_up_left : T -> T
  val move_up_right : T -> T
  val move_up_left_or_abs : T -> T
  val move_up_right_or_abs : T -> T
  val move_down_abs : T -> T
  val move_down_left : T -> T
  val move_down_right : T -> T
  val move_down_app : T -> T * T

end;

(* Zipper data for an generic trm *)
functor TrmCtxtDataFUN(Trm : ABSTRACT_TRM)
: TRM_CTXT_DATA
= struct

  structure Trm = Trm;

  (* a dtrm is, in McBridge-speak, a differentiated term. It represents
  the different ways a term can occur within its datatype constructors *)
  datatype dtrm = Abs of Trm.aname * Trm.typ
                | AppL of Trm.T
                | AppR of Trm.T;

  (* apply a dtrm to a term, ie put the dtrm above it, building context *)
  fun apply (Abs (s,ty)) t = Trm.Abs (s,ty,t)
    | apply (AppL tl) tr = Trm.$ (tl, tr)
    | apply (AppR tr) tl = Trm.$ (tl, tr);

  fun eq_pos (Abs _, Abs _) = true
    | eq_pos (AppL _, AppL _) = true
    | eq_pos (AppR _, AppR _) = true
    | eq_pos _ = false;

end;

(* functor for making term contexts given term data *)
functor TrmCtxtFUN(D : TRM_CTXT_DATA)
: TRM_CTXT =
struct
  structure D = D;

  type T = D.dtrm list;

  val empty = [];
  val is_empty = List.null;

  fun add_abs d l = (D.Abs d) :: l;
  fun add_appl d l = (D.AppL d) :: l;
  fun add_appr d l = (D.AppR d) :: l;

  fun add_dtrm d l = d::l;

  fun eq_path ([], []) = true
    | eq_path ([], _::_) = false
    | eq_path ( _::_, []) = false
    | eq_path (h::t, h2::t2) =
      D.eq_pos(h,h2) andalso eq_path (t, t2);

  (* add context to outside of existing context *)
  fun add_outerctxt ctop cbottom = cbottom @ ctop;

  (* mkterm : zipper -> trm -> trm *)
  val apply = Basics.fold D.apply;

  (* named type context *)
  val nty_ctxt = List.foldr (fn (D.Abs nty,ntys) => nty::ntys
                             | (_,ntys) => ntys) [];
  (* type context *)
  val ty_ctxt = List.foldr (fn (D.Abs (_,ty),tys) => ty::tys
                           | (_,tys) => tys) [];

  val depth = length : T -> int;

  val map = List.map : (D.dtrm -> D.dtrm) -> T -> T

  val fold_up = Basics.fold : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a;
  val fold_down = Basics.fold_rev : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a;

end;

(* zippers in terms of term contexts *)
functor ZipperFUN(C : TRM_CTXT)
: ZIPPER
= struct

  structure C = C;
  structure D = C.D;
  structure Trm = D.Trm;

  type T = C.D.Trm.T * C.T;

  fun mktop t = (t, C.empty) : T

  val mk = I;
  fun set_trm x = apfst (K x);
  fun set_ctxt x = apsnd (K x);

  fun goto_top (z as (t,c)) =
      if C.is_empty c then z else (C.apply c t, C.empty);

  fun at_top (_,c) = C.is_empty c;

  fun split (t,c) = ((t,C.empty) : T, c : C.T)
  fun add_outerctxt c (t,c2) = (t, C.add_outerctxt c c2) : T

  val ctxt = snd;
  val trm = fst;
  val top_trm = trm o goto_top;

  fun nty_ctxt x = C.nty_ctxt (ctxt x);
  fun ty_ctxt x = C.ty_ctxt (ctxt x);

  fun depth_of_ctxt x = C.depth (ctxt x);
  fun map_on_ctxt x = apsnd (C.map x);
  fun fold_up_ctxt f = C.fold_up f o ctxt;
  fun fold_down_ctxt f = C.fold_down f o ctxt;

  fun omove_up (t,(d::c)) = SOME (D.apply d t, c)
    | omove_up (z as (_,[])) = NONE;
  fun omove_up_abs (t,((D.Abs(n,ty))::c)) = SOME (Trm.Abs(n,ty,t), c)
    | omove_up_abs z = NONE;
  fun omove_up_app (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c)
    | omove_up_app (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c)
    | omove_up_app z = NONE;
  fun omove_up_left (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c)
    | omove_up_left z = NONE;
  fun omove_up_right (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c)
    | omove_up_right _ = NONE;
  fun omove_up_left_or_abs (t,(D.AppL tl)::c) =
      SOME (Trm.$(tl,t), c)
    | omove_up_left_or_abs (t,(D.Abs (n,ty))::c) =
      SOME (Trm.Abs(n,ty,t), c)
    | omove_up_left_or_abs z = NONE;
  fun omove_up_right_or_abs (t,(D.Abs (n,ty))::c) =
      SOME (Trm.Abs(n,ty,t), c)
    | omove_up_right_or_abs (t,(D.AppR tr)::c) =
      SOME (Trm.$(t,tr), c)
    | omove_up_right_or_abs _ = NONE;
  fun omove_down_abs (Trm.Abs(s,ty,t),c) = SOME (t,(D.Abs(s,ty))::c)
    | omove_down_abs _ = NONE;
  fun omove_down_left (Trm.$(l,r),c) = SOME (l,(D.AppR r)::c)
    | omove_down_left _ = NONE;
  fun omove_down_right (Trm.$(l,r),c) = SOME (r,(D.AppL l)::c)
    | omove_down_right _ = NONE;
  fun omove_down_app (Trm.$(l,r),c) =
      SOME ((l,(D.AppR r)::c),(r,(D.AppL l)::c))
    | omove_down_app _ = NONE;

  exception move of string * T
  fun move_up (t,(d::c)) = (D.apply d t, c)
    | move_up (z as (_,[])) = raise move ("move_up",z);
  fun move_up_abs (t,((D.Abs(n,ty))::c)) = (Trm.Abs(n,ty,t), c)
    | move_up_abs z = raise move ("move_up_abs",z);
  fun move_up_app (t,(D.AppL tl)::c) = (Trm.$(tl,t), c)
    | move_up_app (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
    | move_up_app z = raise move ("move_up_app",z);
  fun move_up_left (t,((D.AppL tl)::c)) = (Trm.$(tl,t), c)
    | move_up_left z = raise move ("move_up_left",z);
  fun move_up_right (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
    | move_up_right z = raise move ("move_up_right",z);
  fun move_up_left_or_abs (t,(D.AppL tl)::c) = (Trm.$(tl,t), c)
    | move_up_left_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c)
    | move_up_left_or_abs z = raise move ("move_up_left_or_abs",z);
  fun move_up_right_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c)
    | move_up_right_or_abs (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
    | move_up_right_or_abs z = raise move ("move_up_right_or_abs",z);
  fun move_down_abs (Trm.Abs(s,ty,t),c) = (t,(D.Abs(s,ty))::c)
    | move_down_abs z = raise move ("move_down_abs",z);
  fun move_down_left (Trm.$(l,r),c) = (l,(D.AppR r)::c)
    | move_down_left z = raise move ("move_down_left",z);
  fun move_down_right (Trm.$(l,r),c) = (r,(D.AppL l)::c)
    | move_down_right z = raise move ("move_down_right",z);
  fun move_down_app (Trm.$(l,r),c) =
      ((l,(D.AppR r)::c),(r,(D.AppL l)::c))
    | move_down_app z = raise move ("move_down_app",z);

  (* follow the given path down the given zipper *)
  (* implicit arguments: C.D.dtrm list, then T *)
  val zipto = C.fold_down
                (fn C.D.Abs _ => move_down_abs
                  | C.D.AppL _ => move_down_right
                  | C.D.AppR _ => move_down_left);

  (* Note: interpretted as being examined depth first *)
  datatype zsearch = Here of T | LookIn of T;

  (* lazy search *)
  fun lzy_search fsearch =
      let
        fun lzyl [] () = NONE
          | lzyl ((Here z) :: more) () = SOME(z, Seq.make (lzyl more))
          | lzyl ((LookIn z) :: more) () =
            (case lzy z
              of NONE => NONE
               | SOME (hz,mz) =>
                 SOME (hz, Seq.append mz (Seq.make (lzyl more))))
        and lzy z = lzyl (fsearch z) ()
      in Seq.make o lzyl o fsearch end;

  (* path folded lazy search - the search list is defined in terms of
  the path passed through: the data a is updated with every zipper
  considered *)
  fun pf_lzy_search fsearch a0 z =
      let
        fun lzyl a [] () = NONE
          | lzyl a ((Here z) :: more) () = SOME(z, Seq.make (lzyl a more))
          | lzyl a ((LookIn z) :: more) () =
            (case lzy a z
              of NONE => lzyl a more ()
               | SOME(hz,mz) => SOME(hz,Seq.append mz (Seq.make(lzyl a more))))
        and lzy a z =
            let val (a2, slist) = (fsearch a z) in lzyl a2 slist () end

        val (a,slist) = fsearch a0 z
      in Seq.make (lzyl a slist) end;

  (* Note: depth first over zsearch results *)
  fun searchfold fsearch a0 z =
      let
        fun lzyl [] () = NONE
          | lzyl ((a, Here z) :: more) () =
            SOME((a,z), Seq.make (lzyl more))
          | lzyl ((a, LookIn z) :: more) () =
            (case lzyl (fsearch a z) () of
               NONE => lzyl more ()
             | SOME (z,mz) => SOME (z,Seq.append mz (Seq.make (lzyl more))))
      in Seq.make (lzyl (fsearch a0 z)) end;

  fun limit_pcapply f z =
      let val (z2,c) = split z
      in Seq.map (apsnd (add_outerctxt c)) (f c z2) end;
  fun limit_capply (f : C.T -> T -> T Seq.seq) (z : T) =
      let val ((z2 : T),(c : C.T)) = split z
      in Seq.map (add_outerctxt c) (f c z2) end

  val limit_apply = limit_capply o K;

end;

(* now build these for Isabelle terms *)
structure TrmCtxtData = TrmCtxtDataFUN(IsabelleTrmWrap);
structure TrmCtxt = TrmCtxtFUN(TrmCtxtData);
structure Zipper = ZipperFUN(TrmCtxt);

(* For searching through Zippers below the current focus...
   KEY for naming scheme:

   td = starting at the top down
   lr = going from left to right
   rl = going from right to left

   bl = starting at the bottom left
   br = starting at the bottom right
   ul = going up then left
   ur = going up then right
   ru = going right then up
   lu = going left then up
*)
signature ZIPPER_SEARCH =
sig
  structure Z : ZIPPER;

  val leaves_lr : Z.T -> Z.T Seq.seq
  val leaves_rl : Z.T -> Z.T Seq.seq

  val all_bl_ru : Z.T -> Z.T Seq.seq
  val all_bl_ur : Z.T -> Z.T Seq.seq
  val all_td_lr : Z.T -> Z.T Seq.seq
  val all_td_rl : Z.T -> Z.T Seq.seq

end;

functor ZipperSearchFUN(Zipper : ZIPPER) : ZIPPER_SEARCH
= struct

structure Z = Zipper;
structure C = Z.C;
structure D = C.D;
structure Trm = D.Trm;

fun sf_leaves_lr z =
    case Z.trm z
     of Trm.$ _ => [Z.LookIn (Z.move_down_left z),
                    Z.LookIn (Z.move_down_right z)]
      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)]
      | _ => [Z.Here z];
fun sf_leaves_rl z =
    case Z.trm z
     of Trm.$ _ => [Z.LookIn (Z.move_down_right z),
                    Z.LookIn (Z.move_down_left z)]
      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)]
      | _ => [Z.Here z];
val leaves_lr = Z.lzy_search sf_leaves_lr;
val leaves_rl = Z.lzy_search sf_leaves_rl;

fun sf_all_td_lr z =
    case Z.trm z
     of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_left z),
                    Z.LookIn (Z.move_down_right z)]
      | Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)]
      | _ => [Z.Here z];
fun sf_all_td_rl z =
    case Z.trm z
     of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_right z),
                    Z.LookIn (Z.move_down_left z)]
      | Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)]
      | _ => [Z.Here z];
fun sf_all_bl_ur z =
    case Z.trm z
     of Trm.$ _ => [Z.LookIn (Z.move_down_left z), Z.Here z,
                    Z.LookIn (Z.move_down_right z)]
      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z),
                      Z.Here z]
      | _ => [Z.Here z];
fun sf_all_bl_ru z =
    case Z.trm z
     of Trm.$ _ => [Z.LookIn (Z.move_down_left z),
                    Z.LookIn (Z.move_down_right z), Z.Here z]
      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z), Z.Here z]
      | _ => [Z.Here z];

val all_td_lr = Z.lzy_search sf_all_td_lr;
val all_td_rl = Z.lzy_search sf_all_td_rl;
val all_bl_ur = Z.lzy_search sf_all_bl_ru;
val all_bl_ru = Z.lzy_search sf_all_bl_ur;

end;

structure ZipperSearch = ZipperSearchFUN(Zipper);

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.2Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.