dlist.timl

(* Doubly linked lists *)

structure DList = struct

open Basic
open List
open Array

datatype ref 'a = Ref of array 'a {1} --> ref 'a

fun setref ['a] (r : ref 'a, x : 'a) =
    case r of
        Ref content => update (content, #0, x)

fun deref ['a] (r : ref 'a) =
    case r of
        Ref content => sub (content, #0)

fun newref ['a] (x : 'a) =
    Ref (array (#1, x))

datatype dlist 'a : {Nat} {Nat} =
         DLNil {r : Nat} of dlist 'a {r} {1} --> dlist 'a {1 + r} {0}
       | DRNil {l : Nat} of ref (option (dlist 'a {1} {l})) --> dlist 'a {0} {l + 1}
       | DMid {l r : Nat} of ref (option (dlist 'a {r + 2} {l})) * 'a * dlist 'a {r} {l + 2} --> dlist 'a {r + 1} {l + 1}

absidx T_build_dlist_helper : BigO (fn n => $n) with
fun build_dlist_helper ['a] {l r : Nat} (p : ref (option (dlist 'a {r + 1} {l})), l : list 'a {r}) return dlist 'a {r} {l + 1} using T_build_dlist_helper r =
    case l of
        [] => DRNil p
      | hd :: tl =>
        let
          val ref_left = newref NONE
          val tl' = build_dlist_helper (ref_left, tl)
          val node = DMid (p, hd, tl')
          val () = setref (ref_left, SOME node)
        in
          node
        end
end

fun build_dlist ['a] {n : Nat} (l : list 'a {n}) =
    let
      val ref_left = newref NONE
      val l' = build_dlist_helper (ref_left, l)
      val node = DLNil l'
      val () = setref (ref_left, SOME node)
    in
      node
    end

absidx T_fold_to_left : BigO (fn m n => $m * $n) with
fun fold_to_left ['a 'b] {m l r : Nat} (f : 'a * 'b -- $m --> 'b) (acc : 'b) (l : dlist 'a {r} {l}) return 'b using T_fold_to_left m l =
    case l of
        DLNil _ => acc
      | DRNil ref_left =>
        let
          val left = deref ref_left
        in
          case left of
              SOME left => fold_to_left f acc left
            | NONE => acc
        end
      | DMid (ref_left, x, _) =>
        let
          val left = deref ref_left
        in
          case left of
              SOME left => fold_to_left f (f (x, acc)) left
            | NONE => acc
        end
end

absidx T_fold_from_left : BigO (fn m n => $m * $n) with
fun fold_from_left ['a 'b] {m l r : Nat} (f : 'a * 'b -- $m --> 'b) (acc : 'b) (l : dlist 'a {r} {l}) return 'b using T_fold_from_left m l =
    case l of
        DLNil _ => acc
      | DRNil ref_left =>
        let
          val left = deref ref_left
        in
          case left of
              SOME left => fold_from_left f acc left
            | NONE => acc
        end
      | DMid (ref_left, x, _) =>
        let
          val left = deref ref_left
        in
          case left of
              SOME left => f (x, fold_from_left f acc left)
            | NONE => acc
        end
end

absidx T_fold_to_right : BigO (fn m n => $m * $n) with
fun fold_to_right ['a 'b] {m l r : Nat} (f : 'a * 'b -- $m --> 'b) (acc : 'b) (l : dlist 'a {r} {l}) return 'b using T_fold_to_right m r =
    case l of
        DLNil right => fold_to_right f acc right
      | DRNil _ => acc
      | DMid (_, x, right) => fold_to_right f (f (x, acc)) right
end

absidx T_fold_from_right : BigO (fn m n => $m * $n) with
fun fold_from_right ['a 'b] {m l r : Nat} (f : 'a * 'b -- $m --> 'b) (acc : 'b) (l : dlist 'a {r} {l}) return 'b using T_fold_from_right m r =
    case l of
        DLNil right => fold_from_right f acc right
      | DRNil _ => acc
      | DMid (_, x, right) => f (x, fold_from_right f acc right)
end

end