File ‹zippy_collect_trace_mixin_base.ML›

(*  Title:      Zippy/ZIPPY_COLLECT_TRACE_MIXIN_BASE.ML
    Author:     Kevin Kappelmann
*)
signature ZIPPY_COLLECT_TRACE_MIXIN_BASE =
sig
  include ZIPPY_BASE_BASE
  type @{AllT_args} data
  type @{AllT_args} trace = (@{AllT_args} data * @{AllT_args} data list) option

  structure SZCollect : \<^eval>‹pfx_sfx_nargs "SUB_ALTERNATING_DEP_ZIPPER"›
  \<^imap>‹‹{i}› => ‹
  where type @{AllT_args} ZSub.Z{i}.zipper = @{AllT_args} trace
  where type @{AllT_args} ZSub.Z{i}.ZM.container = @{AllT_args} trace
  where type @{AllT_args} ZSub.Z{i}.ZD.content = @{AllT_args} trace
  where type @{AllT_args} ZSub.Z{i}.ZD.zcontext = unit››
  \<^imap>‹‹{i}› => ‹
  sharing type SZCollect.SZ{i}.Zipper.container = Z{i}.zipper
  sharing type SZCollect.SZ{i}.Container.container = Z{i}.ZM.container
  sharing type SZCollect.SZ{i}.Content.container = Z{i}.ZD.content
  sharing type SZCollect.SZ{i}.ZCtxt.container = Z{i}.ZD.zcontext››
  sharing type SZCollect.ZSub.M.t = M.t
end

\<^imap>‹‹{j}› => ‹
functor Zippy_Collect_Trace_Mixin_Base{j}(A :
  sig
    structure Z : ZIPPY_BASE_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_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} 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
type @{AllT_args} data = @{AllT_args} data
type @{AllT_args} trace = (@{AllT_args} data * @{AllT_args} data list) option

structure MB : \<^eval>‹sfx_ParaT_nargs "MORPH_BASE"› = Z

structure ZD = \<^eval>‹sfx_T_nargs "Content_Zipper_Data"›(
  type @{AllT_args} content = @{AllT_args} trace)
local structure SC = \<^eval>‹sfx_ParaT_nargs "Semi_Category"›(Z.K); open SC Z.K Z.M
in
\<^imap>‹‹{i}› => ‹
structure Base{i} =
struct
  structure M = MB
  type @{AllT_args} dep_zip = @{AllT_args} Z.Z{i}.ZM.container * @{AllT_args} Z.Z{i}.zipper
  type @{AllT_args} dep_unzip = @{AllT_args} Z.Z{i}.zipper * @{AllT_args} Z.Z{i}.ZM.container
  type @{AllT_args} dep_up = @{AllT_args} Z.Z{i}.zipper * @{AllT_args} Z.Z{i}.zipper
  type @{AllT_args} dep_down = @{AllT_args} Z.Z{i}.zipper * @{AllT_args} Z.Z{i}.zipper
  type @{AllT_args} dep_left = @{AllT_args} Z.Z{i}.zipper * @{AllT_args} Z.Z{i}.zipper
  type @{AllT_args} dep_right = @{AllT_args} Z.Z{i}.zipper * @{AllT_args} Z.Z{i}.zipper
  type @{AllT_args} container = @{AllT_args} ZD.zipper
  type @{AllT_args} zipper = @{AllT_args} ZD.zipper
  fun move _ = id ()
  val zip = move
  val unzip = move
  val up = move
  val down = move
  val left = move
  val right = move
end
structure DZM{i} = \<^eval>‹sfx_T_nargs "Dep_Zipper_Morphs"›(open Base{i})››
fun pop trace = Option.mapPartial (snd #> List.getItem) trace
fun push z trace = let val data = update z trace
  in Option.map (op ::) trace |> the_default [] |> pair data |> SOME end
structure DZM{j} = \<^eval>‹sfx_T_nargs "Dep_Zipper_Morphs"›(open Base{j}
  fun zip (_, z) = arr (push z)
  fun unzip _ = arr pop
  fun update (_, z) = arr (pop #> push z)
  val up = update
  val down = update
  val left = update
  val right = update)
structure ZCollect = \<^eval>‹pfx_sfx_nargs "Alternating_Dep_Zipper"›(
  structure Z =
  struct
    open MB
    \<^imap>‹‹{i}› => ‹structure Z{i} = DZM{i}››
    \<^imap>‹‹{i}› => ‹
    structure Base{i} =
    struct open MB; type @{AllT_args} from = @{AllT_args} Z{i}.zipper; fun morph _ = id () end
    structure Down{i} =
    struct open Base{i}
      type @{AllT_args} dep =
        @{AllT_args} Z.Z{i}.zipper * @{AllT_args} Z.Z\<^eval>‹succ_mod_nzippers {i} ^ "."›zipper
      type @{AllT_args} to = @{AllT_args} Z\<^eval>‹succ_mod_nzippers {i} ^ "."›zipper
    end
    structure Up{i} =
    struct open Base{i}
      type @{AllT_args} dep =
        @{AllT_args} Z.Z{i}.zipper * @{AllT_args} Z.Z\<^eval>‹pred_mod_nzippers {i} ^ "."›zipper
      type @{AllT_args} to = @{AllT_args} Z\<^eval>‹pred_mod_nzippers {i} ^ "."›zipper
    end››
    structure Down\<^eval>‹pred_mod_nzippers {j}› =
    struct open Down\<^eval>‹pred_mod_nzippers {j}›; fun morph (_, z) = arr (push z) end
    structure Up{j} = struct open Up{j}; fun morph _ = arr pop end
  end
  \<^imap>‹‹{i}› => ‹structure ZD{i} = ZD››)
end

structure Z = \<^eval>‹mk_name ["Pair", pfx_sfx_nargs "Alternating_Zipper_Alternating_Dep_Zipper"]›(
  structure AZ1 = Z; structure AZ2 = ZCollect)
structure ZB = Zippy_Base_Base(\<^eval>‹pfx_sfx_nargs "Alternating_Zipper_Util"›(
  structure Z = Z
  structure AE = \<^eval>‹sfx_ParaT_nargs "Kleisli_Arrow_Exception_Repeat"›(Exn.AE)))
open ZB

structure SZ = Z.SZ1
structure SZCollect = Z.SZ2

fun container cs c = (c, cs)
fun init_container c = container NONE c
\<^imap>‹‹{i}› => ‹
val container{i} = container
val init_container{i} = init_container››

end››