File ‹zippy_lists_positions_collect_mixin_base.ML›

(*  Title:      Zippy/zippy_lists_positions_collect_trace_mixin_base.ML
    Author:     Kevin Kappelmann
*)
signature ZIPPY_LISTS_POSITIONS_COLLECT_TRACE_MIXIN_BASE =
sig
  include ZIPPY_LISTS_POSITIONS_MIXIN_BASE

  structure ZCollect : ZIPPY_COLLECT_TRACE_MIXIN_BASE
  \<^imap>‹‹{i}› => ‹
  sharing type ZCollect.Z{i}.ZM.container = Z{i}.ZM.container
  sharing type ZCollect.Z{i}.ZD.content = Z{i}.ZD.content
  sharing type ZCollect.Z{i}.ZD.zcontext = Z{i}.ZD.zcontext
  sharing type ZCollect.Z{i}.zipper = Z{i}.zipper››
  sharing type ZCollect.M.t = M.t
end

\<^imap>‹‹{j}› => ‹
functor Zippy_Lists_Positions_Collect_Trace_Mixin_Base{j}(A :
   sig
    structure Z : ZIPPY_LISTS_POSITIONS_MIXIN_BASE
    type  @{AllT_args} data
    val update : @{AllT_args} Z.Z{j}.zipper -> (@{AllT_args} data * @{AllT_args} data list) option ->
      @{AllT_args} data
    structure Exn : ZIPPY_EXCEPTION_MIXIN
    sharing type Exn.M.t = Z.M.t
  end) :
  sig
    include ZIPPY_LISTS_POSITIONS_COLLECT_TRACE_MIXIN_BASE
    \<^imap>‹‹{i}› => ‹
    where type @{AllT_args} Z{i}.ZM.container = @{AllT_args} A.Z.Z{i}.ZM.container *
      (@{AllT_args} A.data * @{AllT_args} A.data list) option
    where type @{AllT_args} Z{i}.zipper = @{AllT_args} A.Z.Z{i}.zipper *
      (@{AllT_args} A.data * @{AllT_args} A.data list) option
    where type @{AllT_args} Z{i}.ZD.content = @{AllT_args} A.Z.Z{i}.ZD.content *
      (@{AllT_args} A.data * @{AllT_args} A.data list) option
    where type @{AllT_args} Z{i}.ZD.zcontext = @{AllT_args} A.Z.Z{i}.ZD.zcontext * unit››
    structure SZ : \<^eval>‹pfx_sfx_nargs "SUB_ALTERNATING_ZIPPER"›
    \<^imap>‹‹{i}› => ‹
    where type @{AllT_args} ZSub.Z{i}.ZM.container = @{AllT_args} A.Z.Z{i}.ZM.container
    where type @{AllT_args} ZSub.Z{i}.zipper = @{AllT_args} A.Z.Z{i}.zipper
    where type @{AllT_args} ZSub.Z{i}.ZD.content = @{AllT_args} A.Z.Z{i}.ZD.content
    where type @{AllT_args} ZSub.Z{i}.ZD.zcontext = @{AllT_args} A.Z.Z{i}.ZD.zcontext
    where type @{AllT_args} SZ{i}.Container.container = @{AllT_args} Z{i}.ZM.container
    where type @{AllT_args} SZ{i}.Zipper.container = @{AllT_args} Z{i}.zipper
    where type @{AllT_args} SZ{i}.Content.container = @{AllT_args} Z{i}.ZD.content
    where type @{AllT_args} SZ{i}.ZCtxt.container = @{AllT_args} Z{i}.ZD.zcontext››
    sharing type SZ.ZSub.M.t = M.t
    \<^imap>‹‹{i}› => ‹
    val container{i} : @{AllT_args} ZCollect.trace -> @{AllT_args} A.Z.Z{i}.ZM.container ->
      @{AllT_args} Z{i}.ZM.container
    val init_container{i} : @{AllT_args} A.Z.Z{i}.ZM.container -> @{AllT_args} Z{i}.ZM.container››
  end
  =
struct
open A.Z
structure Z = Zippy_Lists_Collect_Trace_Mixin_Base{j}(A)
open Z
structure ZP =
struct open A.Z.ZP Z
structure SZGPos = \<^eval>‹pfx_sfx_nargs "Sub_Alternating_Zipper_Trans"›(
  structure ASZ1 = SZ; structure ASZ2 = A.Z.ZP.SZGPos)
structure SZLPos = \<^eval>‹pfx_sfx_nargs "Sub_Alternating_Zipper_Trans"›(
  structure ASZ1 = SZ; structure ASZ2 = A.Z.ZP.SZLPos)
structure SZDepth = \<^eval>‹pfx_sfx_nargs "Sub_Alternating_Zipper_Trans"›(
  structure ASZ1 = SZ; structure ASZ2 = A.Z.ZP.SZDepth)
end
end››