<commit_before>(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
(*  Title:      Pure/IsaPlanner/zipper.ML
    ID:		$Id$
    Author:     <NAME>, University of Edinburgh
                <EMAIL>
    Created:    24 Mar 2006
*)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
(*  DESCRIPTION:
    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 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 : (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 goto_top : T -> T
  val at_top : T -> bool
  val mk : (C.D.Trm.T * C.T) -> T
  val set_trm : C.D.Trm.T -> T -> T
  val set_ctxt : C.T -> T -> T

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

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

  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_on_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 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 = Library.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;<commit_msg>added interface for making term contexts.<commit_after>(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
(*  Title:      Pure/IsaPlanner/zipper.ML
    ID:		$Id$
    Author:     <NAME>, University of Edinburgh
                <EMAIL>
    Created:    24 Mar 2006
*)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
(*  DESCRIPTION:
    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 : (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 goto_top : T -> T
  val at_top : T -> bool
  val mk : (C.D.Trm.T * C.T) -> T
  val set_trm : C.D.Trm.T -> T -> T
  val set_ctxt : C.T -> T -> T

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

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

  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_on_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 = Library.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;
{'fraction_non_alphanumeric': 0.16541653367379508, 'fraction_numerical': 0.0015959144589849984, 'mean_word_length': 2.134817408704352, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 209, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1986331', 'n_tokens_mistral': 4895, 'n_tokens_neox': 4698, 'n_words': 1527}