open Tags

(* borrowed from ge code *)
open StateCPSMonad

(* A few utility functions to handle `open records', lists of variants *)
(* Each `field' is characterized by a triple: injection, projection functions
   and the name. The latter is used for printing error messages.
*)
type ('a,'b) open_rec = ('a -> 'b) * ('b -> 'a option)  * string

let rec lookup ((_,prj,_) as ip:(('a,'b) open_rec) )
   : 'b list -> 'a = 
   function [] -> raise Not_found
   | (h::t) -> (match prj h with Some x -> x | _ -> lookup ip t)

let orec_store ((inj,_,name) as ip:(('a,'b) open_rec)) (v:'a) (s:'b list) 
   : 'b list =
  let () = 
    try let _ = lookup ip s in 
        failwith ("The field of an open record is already present: " ^ name)
    with Not_found -> () in
  (inj v)::s

let orec_find ((_,_,name) as ip:(('a,'b) open_rec)) (s:'b list) : 'a =
  try lookup ip s 
  with Not_found -> failwith ("Failed to locate orec field: " ^ name)

let rec orec_replace ((inj,prj,name) as ip:(('a,'b) open_rec)) (v:'a) (s:'b list) 
   : 'b list =
  match s with
  | [] -> failwith ("The field to be replaced is not there: " ^ name)
  | (h::t) -> (match prj h with 
               | Some _ -> (inj v) :: t
               | _      -> h :: orec_replace ip v t)

let mo_extend (ip:('a,'b) open_rec) (v:'a) : ('c, unit) monad =
  let! s = fetch in store (orec_store ip v s)

let mo_lookup (ip:('a,'b) open_rec) : ('c, 'a) monad =
  let! s = fetch in ret (orec_find ip s)

let mo_replace (ip:('a,'b) open_rec) (v : 'a) : ('c, unit) monad =
  let! s = fetch in store (orec_replace ip v s)
(* end borrow *)

module SortMake (CODE: Coderep.Lang) = struct 

open CODE

module type Value = sig type value end

module type ValueWithDefault = sig
  include Value
  val default : value abstract
end

module type ComparableValue = sig
  include Value
  val compare : value abstract -> value abstract -> (_, bool) cmonad
end

module type ComparableValueWithDefault = sig
  include ValueWithDefault
  include ComparableValue with type value := value
end


(*module type Index = sig type index end*)

module type ValueWrapper = sig type 'a wrap end

(* making the imperative notion of index more abstract *)
module type EltDesc = sig type eltdesc end

module type ValueContainer = sig
(*  type vl (* what is actually in a sstate *)
  type vlc (* how we wrap up a vl *)*)
  type ctnr (*actual container*)
  type ctnrdesc (*description of possibly partial ctnr*)
end

module type TArr = sig
  type sstate (* internal state of storage module *)
  type 'a tarr = 'a
    constraint 'a = < state : 'b ; .. >
    constraint 'b = [> `TArr of sstate abstract ]

  type 'x stor_constraint = unit
    constraint 'x = _ tarr
  type ('pc, 'v) lm = ('pc, 'v) cmonad
    constraint _ = 'pc stor_constraint
end

module CreateContainer (V : Value) = struct
  module type Sig = sig
    type elt = V.value
    include ValueContainer
    include TArr
    type initarg
    type 'a res (*what's passed around; cntr or unit*)

    val init : initarg -> (_ tarr, ctnr res) lm
    val add : elt abstract -> ctnr res abstract -> (_ tarr, ctnr res) lm
    val fin : ctnr res abstract -> ('a, ctnr) lm
    val desc : ctnr res abstract -> (_, ctnrdesc) lm
  end
end

module UseContainer (V : Value) = struct
  module type Sig = sig
    include EltDesc
    include TArr
    type elt = V.value

    val access : eltdesc abstract -> (_, elt) lm
  end
end

module OrderableContainer (V : ComparableValue) = struct
  module type Sig = sig
  include UseContainer(V).Sig

  (* comparison operation using explicit values for traversal convenience *)
  val compareVals : elt abstract -> elt abstract
    (*-> sstate abstract*) -> (_, bool) lm
  end
end

(*module SortableIContainer (V : Value) = struct
  module type Sig = sig
    include OrderableIContainer(V).Sig (*realistically needs compare and get as well*)

    (* container operations [uses indices explicitly, values implicitly] *)
    val swap : index abstract -> index abstract -> ('a,unit) lm
  end
end*)

(*module SortableFContainer (V : Value) = struct
  module type Sig = sig
    include OrderableFContainer(V).Sig (*realistically needs compare and get as well*)

    (* container operations [uses indices explicitly, values implicitly] *)
    val swap : index abstract -> index abstract -> ('a,vl) lm
  end
end*)

module RotatableContainer (V : Value) = struct
  module type Sig = sig
    include CreateContainer(V).Sig (*needs at least startIndex and TArr, but realistically get*)
(*    include UseContainer(V).Sig
      with type elt := elt
      with type sstate := sstate
      with type 'a tarr := 'a tarr
      with type 'x stor_constraint := 'x stor_constraint
      with type ('pc, 'v) lm := ('pc, 'v) lm*)
    include EltDesc

    val access : ctnr res abstract -> eltdesc abstract -> (_, elt) lm
    val rotate : ctnr res abstract -> (_, ctnr res) lm
  end
end

module TaggableContainer (V : Value)(T : Tag) = struct
  module type Sig = sig
    include CreateContainer(V).Sig
    include Tags.TaggingA(T)(CODE).Tagged
  end
end

module TraversableContainer (V : ComparableValue) (L : ValueWrapper)(T : Tag) = struct
  module type Sig = sig
    include OrderableContainer(V).Sig
    include TaggableContainer(V)(T).Sig
      with type elt := elt
      with type sstate := sstate
      with type 'a tarr := 'a tarr
      with type 'x stor_constraint := 'x stor_constraint
      with type ('pc, 'v) lm := ('pc, 'v) lm
    type loopdata = elt L.wrap
    type 'a mres (* monadic result *)
    val traverse :
      ctnrdesc abstract ->
      (eltdesc abstract ->
        loopdata abstract ->
        (<answer: ctnrdesc mres; state: [> `TArr of sstate abstract] as 'a;..>, elt * loopdata) cmonad) ->
      loopdata abstract ->
      (<state: 'a;..>, ctnrdesc) cmonad
    val traverseTwo :
      ctnrdesc abstract ->
      (eltdesc abstract ->
        loopdata abstract ->
        (<answer: ctnrdesc mres; state: [> `TArr of sstate abstract] as 'a;..>, elt) cmonad) option ->
      (eltdesc abstract ->
        eltdesc abstract ->
        loopdata abstract ->
        (<answer: ctnrdesc mres; state: 'a;..>, (elt * elt) * loopdata) cmonad) ->
      loopdata abstract ->
      (<state: 'a;..>, ctnrdesc tag) cmonad
(*    val traverseexercise :
      vl abstract ->
      (eltdesc abstract -> loopdata abstract -> (elt * loopdata) abstract) ->
      loopdata abstract ->
      ('a, vl) lm*)
    val iterativeconverge :
      (ctnrdesc abstract ->
        (<answer: ctnrdesc mres; state: 'a;..>, ctnrdesc tag) cmonad) ->
      ctnrdesc abstract ->
      (<state: 'a;..>, ctnrdesc) cmonad
  end
end

module ValOpt (*: ValueWrapper*) = struct type 'a wrap = 'a option end

module BubbleSortContainer (V : ComparableValue) (L : ValueWrapper)(T : Tag) = struct
  module type Sig = sig
    include TraversableContainer(V)(L)(T).Sig
  end
end

module LineContainer (V : Value) = struct
  module type Sig = sig
    include RotatableContainer(V).Sig
    include ComparableValue
  end
end

(* using a list with ref *)
(*module ListStorageG (Value : Value) (* : ImperativeContainer *) = struct
  type elt = Value.value
  type index = int
  type vl = Value.value list
  type vlc = vl ref
  type eltdesc = elt
  type loopdata = elt
  type ctnrdesc = vl
  type 'a tagged = 'a option
  type sstate = vlc
  type 'a tarr = 'a
    constraint 'a = < state : 'b ; .. >
    constraint 'b = [> `TArr of sstate abstract]
  type 'x stor_constraint = unit
    constraint 'x = _ tarr
  type ('pc, 'v) lm = ('pc, 'v) cmonad
    constraint _ = 'pc stor_constraint
  type initarg = unit
  
  (* let iterateFrom arr f n = genrecloop (f arr) n *)

  let ip = (fun x -> `TArr x), (function `TArr x -> Some x | _ -> None),
    "List Ref"

  let init () = 
    let! adecl = retN (liftRef CList.nil) in
    let! _ = mo_extend ip adecl in
    ret adecl
  let add v _ = (* res is () here *)
    let! a = mo_lookup ip in
    assignM a (CList.cons v (liftGet a))
  let fin _ = 
    let! r = mo_lookup ip in 
    ret (liftGet r)

  let get i =  (* duplication happens because no let insertion *)
    let! arr = mo_lookup ip in
    let! a = retN (liftGet arr) in
    (* let a = liftGet arr in *)
    ret (CList.nth a (Idx.sub (CList.length a) i))
  let set i v =
    let! arr = mo_lookup ip in
    let replace i v o l = fun _ _ ->
      CList.matchList l (*could use if checking the length instead*)
        CList.nil
        (let n = CList.length l in fun h t -> CList.cons (ifL (Logic.equalL i n) v h) (apply o t))
    in let! newArr = (genrecloop (replace i v) (liftGet arr))
    in assignM arr newArr
  let swap i1 i2 =
    let! v1 = get i1 in
    let! tmp = retN v1 in
    let! v2 = get i2 in
       seqM
        (set i1 v2)
        (set i2 tmp)
  let compare i1 i2 _ = 
    let! v1 = get i1 in
    let! v2 = get i2 in
    ret (Idx.less v1 v2)
  let startIndex = Idx.one
  let nextIndex = Idx.succ
  let maxIndex _ = 
    let! arr = mo_lookup ip in
    ret (CList.length (liftGet arr))
  let prevIndex i = 
    let! maxi = maxIndex () in
    ret (
      matchOpt i 
        (Maybe.just maxi)
        (fun n -> ifL (Idx.less Idx.one n) (Maybe.just (Idx.pred n)) Maybe.none))
  let inBounds i h = 
    let! maxi = maxIndex h in
    ret (Idx.ltoe i maxi) (*assuming i > 0*)

(*  rotates in-place, uses only:
    -inBounds
    -nextIndex
    -startIndex
    -swap
*)
  let rotate n h =
(*     let! cond = inBounds n in *)
(*     whenM cond ( *)
    let! cond = inBounds (nextIndex startIndex) h in (*length > 1*)
    whenM cond (
      let rotateN self k =
        whenM (Logic.notequalL k n) ( (*so rotate startIndex = original*)
        let rotate1 self m =
          let l = nextIndex m in
          let! c = inBounds l h in
          whenM c (seqM
            (swap m l)
            (applyM self l)) in (*end rotate1*)
        seqM
          (genrecloop rotate1 startIndex)
          (applyM self (nextIndex k))) in (*end rotateN*)
      genrecloop rotateN startIndex)
(*     ) *)

  let traverse lstdesc f data =
    let gen self tup =
      let (_, i) = Pair.unpair tup in
      CList.matchListM lstdesc
        (ret CList.nil)
        (fun h t ->
        let (v, i2) = Pair.unpair (f (h) i) in
        let! r = (applyM self (Tuple.tup2 t i2)) in
        ret (CList.cons v r))
      in genrecloop gen (Tuple.tup2 lstdesc data)

let traverseTwo lstdesc f data =
    let gen self tup =
      let (_, i) = Pair.unpair tup in
      CList.matchListM lstdesc
        (ret CList.nil)
        (fun h t ->
        let h2 = (ifL (Idx.less Idx.zero (CList.length t)) (Maybe.just (CList.nth t Idx.zero)) Maybe.none) in
        let! iteration = f h h2 i in
        let (v, i2) = Pair.unpair iteration in
        let! r = (applyM self (Tuple.tup2 t i2)) in
        ret (CList.cons v r))
      in
      let! newlst = genrecloop gen (Tuple.tup2 lstdesc data) in
      ret (ifL (Logic.notequalL lstdesc newlst)
        (Maybe.just newlst)
        Maybe.none)

  let traverseexercise lst f data  =
    let gen self tup =
    let (lst, i) = Pair.unpair tup in
    CList.matchListM lst
      (ret CList.nil)
      (fun h t ->
      let (v, i2) = Pair.unpair (f (h) i) in
      let! r = (applyM self (Tuple.tup2 t i2)) in
      ret (CList.cons v r))
    in genrecloop gen (Tuple.tup2 lst data)

  let access x = ret x
  let compare_ x y =
    ret (Idx.less x y)
end*)

(* These are 'statically dimensioned' Arrays, with the dimension fixed at
   generation time. The 'index' counts how many are used. *)
module ArrayStorageG (V : ComparableValueWithDefault) (L : ValueWrapper) (T : Tag)
           (MkTag : TaggingA(T)(CODE).Tagged)
           (* : BubbleSortContainer(V)(L)(T).Sig *) = struct
  type elt = V.value
  type index = int (*kept for local readability*)
  type ctnr = V.value array * (index ref)
(*   type vlc = vl *)
  type eltdesc = index
  type loopdata = elt L.wrap
  type 'a res = unit
  type ctnrdesc = ctnr * (index * index)
  type sstate = ctnr
  type 'a tarr = <state : [> `TArr of sstate abstract]; .. > as 'a
  type 'x stor_constraint = unit
    constraint 'x = _ tarr
  type ('pc, 'v) lm = ('pc, 'v) cmonad
    constraint _ = 'pc stor_constraint
  type initarg = int
  type 'a mres = unit

  include MkTag

  let ip = (fun x -> `TArr x), (function `TArr x -> Some x | _ -> None), "Array"

  let init n =
    let! adecl = retN (Tuple.tup2 ((Array1Dim.init (Size.size n) (V.default)))
                     (liftRef Idx.zero)) in
    let! _ = mo_extend ip adecl in
    ret cunit
  let add v _ =
    let! s = mo_lookup ip in
    let (arr,n) = Pair.unpair s in 
    seqM 
      (* should probably make set monadic *)
      (ret (Array1Dim.set arr (liftGet n) v))
      (assignM n (Idx.succ (liftGet n)))
  let maxIndex _ =
    let! core = mo_lookup ip in
    let (_,n) = Pair.unpair core in
    ret (Idx.pred (liftGet n))
  let fin _ = mo_lookup ip
  let desc _ =
    let! r = fin () in
    let! m = maxIndex () in
    ret (Tuple.tup2 r (Tuple.tup2 Idx.zero m))
  let set i v =
    let! core = mo_lookup ip in
    let (arr,_) = Pair.unpair core in 
    ret (Array1Dim.set arr i v) (* assuming 0 =< i < n*)
  let startIndex = Idx.zero
  let nextIndex = Idx.succ
  let prevIndex i =
    let! maxi = maxIndex () in
    ret (
      matchOpt i 
        (Maybe.just maxi) 
        (fun n -> ifL (Idx.less Idx.one n) (Maybe.just (Idx.pred n)) Maybe.none) )
  let inBounds i h = (*assuming i > 0*)
    let! maxi = maxIndex h in
    ret (Idx.ltoe i maxi)

(*  let swap i1 i2 =
    let! st = mo_lookup ip in
    let (arr, _) = Pair.unpair st in
    let! v1 = get i1 in
    let! tmp = retN v1 in
    let! v2 = get i2 in
    seqM
      (ret (Array1Dim.set arr i1 v2))
      (ret (Array1Dim.set arr i2 tmp))
*)

  let access i =
    let! st = mo_lookup ip in
    let arr = Pair.fst st in
    retN (Array1Dim.get arr i) (*assuming 0 =< i < n*)

  let traverse arrdesc f
         initdata : (<state: 'a;..>, ctnrdesc) cmonad =
    let! desc = retN (Pair.snd arrdesc) in
    let (lower, upper) = Pair.unpair desc in
    let! ir = retN (liftRef lower) in
    let i = liftGet ir in
    let! ldr = retN (liftRef initdata) in
    let loopdata = liftGet ldr in
    let cond = Idx.ltoe i upper in
    seqM
      (whileM cond (
        let! iteration = f i loopdata in
        let (value, newloopdata) = Pair.unpair iteration in
        seqM
          (set i value) (seqM
          (assignM ldr newloopdata)
          (assignM ir (Idx.succ i)))))
      (let! wholearr = fin () in
       let! wa = retN wholearr in
       ret (Tuple.tup2 wa desc))

  let traverseTwo arrdesc f1o f2 initdata =
    let! desc = retN (Pair.snd arrdesc) in
    let! lower = Pair.fstM desc in
    let upper = Pair.snd desc in
    let! ir = retN (liftRef lower) in
    let i = liftGet ir in
    let! ldr = retN (liftRef initdata) in
    let loopdata = liftGet ldr in
    let! changed = retN (liftRef Logic.falseL) in
    let cond = Idx.less i upper in
    let process v =
      seqM
        (let! curr = access i in
        whenM (Logic.notequalL v curr) (seqM
          (set i v)
          (assignM changed Logic.trueL)))
        (assignM ir (Idx.succ i)) in
    let! resultcode =
      let twoeltcase =
       (whileM cond
          (let! i2 = retN (Idx.succ i) in
          let! iteration = f2 i i2 loopdata in
          let! namediter = retN iteration in
          let! v = retN (Pair.fst (Pair.fst namediter)) in
          let! v2 = retN (Pair.snd (Pair.fst namediter)) in
          let newdata = Pair.snd namediter in
          seqM (seqM
            (process v)
            (set i2 v2))
            (assignM ldr newdata))) in
      let return =
        let! newarrdesc = fin () in
        let! arr = retN newarrdesc in
        let  result = tag (Tuple.tup2 arr desc) (liftGet changed) in
        retN result in
      match f1o with
        | None   -> (seqM twoeltcase return)
        | Some f -> seqM (seqM
            twoeltcase
            (let! v = f i loopdata in
              process v))
            return in
      retN resultcode (*explicit naming for deduplication *)

  let traverseexercise arr f data =
    let! ix = retN (liftRef startIndex) in
    let i = liftGet ix in
    let! nr = retN (liftRef data) in
    let n = liftGet nr in
    let! cond = inBounds i arr in
    seqM
      (whileM cond (
        let (v, n2) = Pair.unpair (f (Tuple.tup2 arr i) n) in
        seqM (seqM
          (set i v)
          (assignM nr n2))
          (assignM ix (nextIndex i))))
      (fin ())
      
  let compareVals = V.compare (*possibly higher-level API*)

  let iterativeconverge iter container = (*container = cntr*)
    let! swapping = retN (liftRef Logic.trueL) in
    let! result = retN (liftRef container) in
    seqM
      (whileM (liftGet swapping)
        (let! traversedctnr = iter (liftGet result) in
         process traversedctnr 
           (Some (fun b  -> assignM swapping b))
           (fun a  -> assignM result a)
           (fun () -> unitL) ))

(*
         let  cond_ = get_tag traversedctnr in
         let! cond = retN cond_ in (*explicit naming through retN for deduplication in generated code*)
         (seqM
           (assignM swapping cond)
           (whenM cond (
             let changedctnr = get_a traversedctnr in
             assignM result changedctnr)))) *)
      (ret (liftGet result))

end

module ArrayLineG (V : ComparableValueWithDefault) (* : RotatableContainer(V).Sig *) = struct
  type elt = V.value
  type index = int
  type eltdesc = index
  type ctnr = (V.value, index ref) Prelude.svec
  type value = ctnr
  type ctnrdesc = ctnr * (index * index)
  type 'a res = 'a
  type sstate = ctnr
  type 'a tarr = <state : [> `TArr of sstate abstract]; .. > as 'a
  type 'x stor_constraint = unit
    constraint 'x = _ tarr
  type ('pc, 'v) lm = ('pc, 'v) cmonad
    constraint _ = 'pc stor_constraint
  type initarg = int

  let init n = ret (Vector.vec (Array1Dim.init (Size.size n) (V.default)) (liftRef Idx.zero))

  let add (c : ctnr abstract) (v : elt abstract) : ('pc, ctnr) lm =
    let! arr = retN (Vector.datum c) in
    let! n = retN (Vector.size c) in
    seqM (seqM
      (ret (Array1Dim.set arr (liftGet n) v))
      (assignM n (Idx.succ (liftGet n))))
      (ret c)
  let fin = idM
  let desc c = ret (Tuple.tup2 c (Tuple.tup2 Idx.zero (Array1Dim.length (Vector.datum c))))
  let access (c : ctnr abstract) (i : int abstract) =
    let arr = Vector.datum c in
    retN (Array1Dim.get arr i) (*assuming 0 =< i < n*)

  type rotationrecord = {fst : elt abstract; toshift : ctnr abstract}
  let part1Array ctnr : ('p, rotationrecord) monad =
    let! e = access ctnr Idx.zero in
    ret { fst = e; toshift = ctnr }
  let part2Array (ctnr : ctnr abstract) : ('pc, ctnr) lm =
    let! arr = retN (Vector.datum ctnr) in
    let! n = retN (Vector.size ctnr) in
    let! arr2 = retN (Array1Dim.init (Array1Dim.length arr) (V.default)) in
    ret (seq (Array1Dim.blit arr Idx.one arr2 Idx.zero (Idx.pred (liftGet n)))
             (Vector.vec arr2 (liftRef (Idx.pred (liftGet n)))))
  let part3Array = add

  (* note: all those retN are crucial, else the code generated is wrong! *)
  let rotate (c : ctnr abstract) : ('pc, ctnr) lm =
    let! ctnr = retN c in
    let! record = part1Array ctnr in
    let! newctnr = part2Array record.toshift in
    let! nn = retN newctnr in
    add nn record.fst

  let default = Vector.vec (Array1Dim.init (Size.size 20) (V.default)) (liftRef Idx.zero)
end

(* using a list but without ref *)
(* should not use the state at all *)
module ListStorageG2 (V : ComparableValue) (L : ValueWrapper) (T : Tag)
           (MkTag : TaggingA(T)(CODE).Tagged)
              (* : BubbleSortContainer(V)(L).Sig *) = struct
  type elt = V.value
  type eltdesc = elt
  (*type vl = elt list
  type vlc = vl*)
  type ctnr = elt list
  type ctnrdesc = ctnr
  type value = ctnr
  type  loopdata = elt L.wrap
  type 'a res = 'a
  type sstate = unit (*state unused*)
  type 'a tarr = 'a
    constraint 'a = < state : 'b ; .. >
    constraint 'b = [> `TArr of sstate abstract]

  type 'x stor_constraint = unit
    constraint 'x = _ tarr
  type ('pc, 'v) lm = ('pc, 'v) cmonad
    constraint _ = 'pc stor_constraint

  type initarg = unit

  type 'a mres = 'a

  include MkTag

(*   let ip = (fun x -> `TArr x), (function `TArr x -> Some x | _ -> None), "List" *)

  let init () = ret CList.nil
  let add v l = retN (CList.cons v l)
  let fin = ret
  let desc = ret
  let access x = ret x

  let compareVals = V.compare
  let traverse lstdesc f data =
    let gen self tup =
      let (lst, i) = Pair.unpair tup in
      CList.matchListM lst
        (ret CList.nil)
        (fun h t ->
        let! iteration = f h i in
        let (v, i2) = Pair.unpair iteration in
        let! r = (applyM self (Tuple.tup2 t i2)) in
        ret (CList.cons v r))
      in genrecloop gen (Tuple.tup2 lstdesc data)
  let traverseTwo lstdesc f1o f2 initdata =
    let gen self tup =
      let lst = Pair.fst tup in (*only used once in match*)
      let! data = retN (Pair.snd tup) in
      CList.matchListTwoM lst
        (match f1o with
          | None   -> (Same idM)
          | Some f ->
            (Different
              (ret CList.nil,
              (fun x ->
                let! v = f x data in
                ret (CList.cons v CList.nil))))) (*must also be provided by caller*)
        (fun h h2 t ->
          let! iteration = f2 h h2 data in
          let! namediter = retN iteration in (*explicit naming through retN for deduplication in generated code*)
          let! v = retN (Pair.fst (Pair.fst namediter)) in
          let! v2 = retN (Pair.snd (Pair.fst namediter)) in
          let! newdata = retN (Pair.snd namediter) in
          let! r = applyM self (Tuple.tup2 (CList.cons v2 t) newdata) in
          ret (CList.cons v r)) in
    let! newlstdesc = genrecloop gen (Tuple.tup2 lstdesc initdata) in
    let! namednewlstdesc = retN newlstdesc in (*explicit naming through retN for deduplication in generated code*)
    let  result = tag namednewlstdesc (Logic.notequalL lstdesc namednewlstdesc) in
    retN result

  let traverseexercise lst f data  =
    let gen self tup =
    let (lst, i) = Pair.unpair tup in
    CList.matchListM lst
      (ret CList.nil)
      (fun h t ->
      let (v, i2) = Pair.unpair (f (h) i) in
      let! r = (applyM self (Tuple.tup2 t i2)) in
      ret (CList.cons v r))
    in genrecloop gen (Tuple.tup2 lst data)

  let iterativeconverge iter l =
    let body self lst =
      let! taggedtraversed = iter lst in  (* one loop *)
      process taggedtraversed
        None
        (fun a -> applyM self a)
        (fun () -> ret lst)
(*
      let  tag = get_tag taggedtraversed in
      let! changed = retN tag in
      ifM changed
        (let traversed = get_a taggedtraversed in
        applyM self traversed)
        (ret lst) (*clumsy equivalent of matchopt, maybe need matchvltagged?*)
*)
    in genrecloop body l

  type rotationrecord = {fst : elt abstract; toshift : ctnr abstract}
  let part1List lst = ret { fst = CList.hd lst; toshift = CList.tl lst }
  let part2List = idM
  let part3List t h = ret (CList.append t (CList.cons h CList.nil))

  let rotate lst = CList.matchListM lst
    (ret CList.nil)
    (fun _ _ ->
      let! record = part1List lst in
      let! newlst = part2List record.toshift in
      part3List newlst record.fst)

  let compare lstdescx lstdescy = (*assuming <, and that [] < x::[]*)
    let gen self tup =
      let lstx = Pair.fst tup in
      let! lsty = retN (Pair.snd tup) in
      CList.matchListM lstx
        (CList.matchListM lsty
          (ret Logic.falseL)
          (fun _ _ -> ret Logic.trueL))
        (fun hx tx -> CList.matchListM lsty
          (ret Logic.falseL)
          (fun hy ty ->
            ifM (Logic.equalL hx hy)
              (applyM self (Tuple.tup2 tx ty))
              (let! cond = compareVals hx hy in
              ifM cond
                (ret Logic.trueL)
                (ret Logic.falseL)))) in
    genrecloop gen (Tuple.tup2 lstdescx lstdescy)

  let default = CList.nil
end

module BubbleSortG3 (V:ComparableValue) (T:Tag)(Storage : BubbleSortContainer(V)(ValOpt)(T).Sig) = struct
  let bsiter arr =
    let loopbody2 eltdesc nextdesc _ =
      let! curr = Storage.access eltdesc in
      let! next = Storage.access nextdesc in
      let! unordered = Storage.compareVals curr next in
      ret (Tuple.tup2 (ifL unordered (Tuple.tup2 next curr) (Tuple.tup2 curr next)) Maybe.none) in
    Storage.traverseTwo arr None loopbody2 Maybe.none

  let bubblesort ctnr = Storage.iterativeconverge bsiter ctnr
end

(*module ShiftConnector
  (Line : ImperativeLineContainer)
  (Value: ValueWithDefault with type value = Line.initarg)
  (Src  : UseIContainer with type value = Line.vlc)
  (Dest : sig include CreateIContainer
              include UseIContainer
                with type value := value
                with type sstate := sstate
                with type 'x stor_constraint := 'x stor_constraint
                with type ('pc, 'v) lm := ('pc, 'v) lm end
            with type value = Line.vlc
            with type sstate = Src.sstate)
  = struct
  let DestAdd (*avoid duplication when src=dest*)
  let srcGet = Src.get

end*)

(*module ShiftG
  (V : Value)
  (T: Tag)
  (Line : LineContainer(V).Sig)
  (Src: TraversableContainer(Line)(ValOpt)(T).Sig)
  (Dest: TraversableContainer(Line)(ValOpt)(T).Sig) = struct


  let shift src dest =
    let f line data =
      let! rotation = Line.rotate line in
      let rotated = liftRef rotation in
      whileM (Logic.equalL (liftGet rotated) line) (
      seqM (seqM
        (Dest.add dest (liftGet rotated))
        (assignM rotated (Line.rotate (liftGet rotated))))
        (Tuple.tup2 line data)) in
    Src.traverse src f Maybe.none

end*)


(*module ShiftG
  (Line : LineContainer)
  (Value: ValueWithDefault with type value = Line.initarg)
  (Src  : UseIContainer(struct type value = Line.vlc end).Sig)
  (Dest : sig include CreateIContainer
              include UseIContainer
                with type value := value
                with type sstate := sstate
                with type 'x stor_constraint := 'x stor_constraint
                with type ('pc, 'v) lm := ('pc, 'v) lm end
            with type value = Line.vlc
            with type sstate = Src.sstate)
  = struct
(*   essentially rotate, will probably move *)
(*   let worditeration (line : ImperativeContainer.vlc) self (n : Line.index abstract) =
  let! m = retN (Line.nextIndex n) in
    let! lineto = Dest.get Dest.maxIndex in (*assuming maxindex is the newest line*)
    seqM (
      let! cond = Line.inBounds m in
      (whenM cond
          (lineto.add (Line.get m)) ) )
      (let! max_ind = Line.maxIndex () in
       ifM (Idx.less m max_ind)
        (applyM self m)
        (lineto.add (Line.get Line.startIndex)))*)
  (* loop over shifts of a line, which is assumed to be another ImperativeContainer *)
  let shiftiteration (line : Src.value (*Line.vlc*) abstract) self (n : Line.index abstract) =
    let! dmax = Dest.maxIndex () in
    let! lineto = Dest.get dmax in (*assuming maxindex is the newest line*)
    let! rline = Line.rotate n in (* Important: which line?*)
    seqM (Dest.add rline)
    (let! m = retN (Line.nextIndex n) in
    let! cond = Line.inBounds m in
    whenM cond
      (applyM self m) )

  (* loop over lines in Src *)
  let lineiteration self n =
    let! m = retN (Src.nextIndex n) in
    let! cond = Src.inBounds n in
    whenM cond (*when n is a valid index*)
      (seqM (let! line = Src.get n in seqM
        (let! newline = Line.init Value.default in
        Dest.add newline) (*add new empty line to Dest*)
        (genrecloop (shiftiteration line) Line.startIndex) )
        (applyM self m) )
  (* loop over all lines *)
  let shift () =
  genrecloop lineiteration Src.startIndex
end *)

(*module Rotate (V:Value)(T:Tag)(Storage : BubbleSortContainer(V)(ValOpt)(T).Sig) = struct
  let rotate ctnr = (*Adapted from testilg2tt2r, using traverseTwo*)
    let loopbody2 x1 x2 data = (*essentially rotate for two*)
    let! v2 = Storage.access x2 in
    let! newdata =
      matchM data
        (fun _ -> ret data)
        (let! v1 = Storage.access x1 in
        ret (Maybe.just v1)) in
    ret (Tuple.tup2 (Tuple.tup2 v2 v2) newdata) in
  let loopbody x data =
    matchM data
      idM
      (Storage.access x) in (*one elt ctnr case*)
  let! tagged_ctr = Storage.traverseTwo ctnr (Some loopbody) loopbody2 Maybe.none in
  Storage.process tagged_ctr None ret (fun () -> ret ctnr)
end*)

end