Toccata

(*
  Ropes

    Boehm, Hans-J; Atkinson, Russ; and Plass, Michael (December 1995).
    "Ropes: an Alternative to Strings".
    Software—Practice & Experience 25 (12):1315–1330.

  Authors: Léon Gondelman (Université Paris Sud)
           Jean-Christophe Filliâtre (CNRS)
*)

(* Immutable strings

   Used both for rope leaves and for specification purposes *)

module String

  use int.Int

  type char
  constant dummy_char: char

  type char_string

  (* axiomatized function length *)
  val function length char_string: int
    ensures { 0 <= result }

  (* string access routine *)
  val function ([]) (s: char_string) (i:int) : char
    requires { 0 <= i < s.length }

  val constant empty: char_string
    ensures { length result = 0 }

  (* extensional equality for strings *)
  predicate (==) (s1 s2: char_string) =
    length s1 = length s2 /\
    forall i:int. 0 <= i < length s1 -> s1[i] = s2[i]

  axiom extensionality:
     forall s1 s2: char_string. s1 == s2 -> s1 = s2

  (* axiomatized concatenation *)
  function app char_string char_string: char_string

  axiom app_def1:
    forall s1 s2: char_string. length (app s1 s2) = length s1 + length s2

  axiom app_def2:
    forall s1 s2: char_string, i: int.
    0 <= i < length s1 -> (app s1 s2)[i] = s1[i]

  axiom app_def3:
    forall s1 s2: char_string, i: int.
    length s1 <= i < length s1 + length s2 ->
    (app s1 s2)[i] = s2[i - length s1]

  lemma app_assoc:
    forall s1 s2 s3: char_string. app s1 (app s2 s3) == app (app s1 s2) s3

  (* axiomatized substring *)
  function sub char_string int int: char_string

  axiom sub_def1:
    forall s: char_string, ofs len: int.
    0 <= len -> 0 <= ofs <= length s -> ofs + len <= length s ->
    length (sub s ofs len) = len

  axiom sub_def2:
    forall s: char_string, ofs len: int.
    0 <= len -> 0 <= ofs <= length s -> ofs + len <= length s ->
    forall i: int. 0 <= i < len -> (sub s ofs len)[i] = s[ofs + i]

  (* substring routine *)
  val sub (s: char_string) (ofs len: int) : char_string
    requires { 0 <= len /\ 0 <= ofs <= length s /\ ofs + len <= length s }
    ensures  { result = sub s ofs len }

end

(* API *)

module Sig

  use int.Int
  use import String as S

  type rope

  function string rope: char_string

  function length rope: int

  val constant empty : rope
    ensures { length result = 0 /\ string result == S.empty }

  val is_empty (r: rope) : bool
    ensures  { result <-> string r == S.empty }

  val of_string (s: char_string) : rope
    requires { 0 <= S.length s }
    ensures  { string result == s}

  (* access to the i-th character *)
  val get (r: rope) (i: int) : char
    requires { 0 <= i < length r }
    ensures  { result = (string r)[i] }

  val concat (r1 r2: rope) : rope
    ensures  { string result == S.app (string r1) (string r2) }

  (* sub-rope construction *)
  val sub (r: rope) (ofs len: int) : rope
    requires { 0 <= len /\ 0 <= ofs <= length r /\ ofs + len <= length r }
    ensures  { string result == S.sub (string r) ofs len }

  val balance (r: rope) : rope
    ensures  { string result == string r }

end

(* Implementation *)

module Rope (* : Sig *)

  use int.Int
  use import String as S

  (* ***** Logical description of rope type **** *)
  type rope =
    | Emp
    | Str char_string int  int  (* Str s ofs len is s[ofs..ofs+len[ *)
    | App rope   rope int  (* concatenation and total length   *)

  let function length (r: rope) : int =
    match r with
    | Emp         -> 0
    | Str _ _ len -> len
    | App _ _ len -> len
    end

  (* invariant predicate for ropes *)
  predicate inv (r: rope) = match r with
    | Emp ->
        true
    | Str s ofs len ->
        0 < len /\ 0 <= ofs < S.length s /\ ofs + len <= S.length s
        (* s[ofs..ofs+len[ is a non-empty substring of s *)
    | App l r len ->
        0 < length l /\ inv l /\ 0 < length r /\ inv r /\
        len = length l + length r
        (* l and r are non-empty strings of the size (|l| + |r|) = len *)
  end

  (* the string model of a rope *)
  function string (r: rope) : char_string = match r with
    | Emp           -> S.empty
    | Str s ofs len -> S.sub s ofs len
    | App l r _     -> S.app (string l) (string r)
  end

  (* length of stored string is equal to the length of the corresponding rope *)
  lemma rope_length_is_string_length:
    forall r: rope. inv r -> S.length (string r) = length r

  (* NB: Here and below pay attention to the use of '==' predicate in
  contracts *)

  (* empty rope *)
  let constant empty : rope = Emp
    ensures { length result = 0 /\ inv result /\ string result == S.empty }

  let is_empty (r: rope) : bool
    requires { inv r }
    ensures  { result <-> string r == S.empty }
  = match r with Emp -> true | _ -> false end

  (* string conversion into a rope *)
  let of_string (s: char_string) : rope
    requires { 0 <= S.length s }
    ensures  { string result == s}
    ensures  { inv result }
  = if S.length s = 0 then Emp else Str s 0 (S.length s)

  (* access to the character of the given index i *)
  let rec get (r: rope) (i: int) : char
    requires { inv r }
    requires { 0 <= i < length r }
    ensures  { result = (string r)[i] }
    variant  { r }
  = match r with
    | Emp ->
        absurd
    | Str s ofs _ ->
       s[ofs + i]
    | App left right _   ->
        let n = length left in
        if i < n then get left i else get right (i - n)
    end

  (* concatenation of two ropes *)
  let concat (r1 r2: rope) : rope
    requires { inv r1 /\ inv r2 }
    ensures  { inv result }
    ensures  { string result == S.app (string r1) (string r2) }
  = match r1, r2 with
    | Emp, r | r, Emp -> r
    | _               -> App r1 r2 (length r1 + length r2)
    end

  (* sub-rope construction *)
  let rec sub (r: rope) (ofs len: int) : rope
    requires { inv r}
    requires { 0 <= len /\ 0 <= ofs <= length r /\ ofs + len <= length r }
    ensures  { inv result }
    ensures  { string result == S.sub (string r) ofs len }
    variant  { r }
  =
  match r with
    | Emp          -> assert { len = 0 }; Emp
    | Str s ofs' _ -> if len = 0 then Emp else Str s (ofs' + ofs) len
    | App r1 r2 _  ->
        let left  = length r1 - ofs in (* max chars to the left  *)
        let right = len - left      in (* max chars to the right *)
        if right <= 0 then sub r1 ofs len
        else if 0 >= left then sub r2 (- left) len
        else concat (sub r1 ofs left) (sub r2 0 right)
    end

end

module Balance

  use String
  use import Rope as R
  use int.Int
  use int.Fibonacci
  use int.MinMax
  use array.Array
  use ref.Ref

  val constant max : int (* e.g. = 100 *)
    ensures { 2 <= result }

  function string_of_array (q: array rope) (l u: int) : char_string

  axiom string_of_array_empty:
    forall q: array rope, l: int.
    0 <= l <= length q -> string_of_array q l l == S.empty

  axiom string_of_array_concat_left:
    forall q: array rope, l u: int. 0 <= l < u <= Array.length q ->
    string_of_array q l u ==
      S.app (string_of_array q (l+1) u) (string q[l])

  let rec lemma string_of_array_concat
    (q: array rope) (l mid u: int) : unit
    requires { 0 <= l <= mid <= u <= Array.length q }
    ensures  { string_of_array q l u ==
      S.app (string_of_array q mid u) (string_of_array q l mid) }
    = variant { mid - l } if l < mid then string_of_array_concat q (l+1) mid u

  let rec lemma string_of_array_concat_right
    (q: array rope) (l u: int)
    requires { 0 <= l < u <= Array.length q }
    ensures { string_of_array q l u ==
                S.app (string q[u-1]) (string_of_array q l (u-1)) }
    = variant { u -l } if l < u-1 then string_of_array_concat_right q (l+1) u

  let lemma string_of_array_length
    (q: array rope) (l u i: int)
    requires { 0 <= l <= i < u <= Array.length q }
    requires { forall j: int. l <= j < u -> inv q[j] }
    ensures  { S.length (string_of_array q l u) >= S.length (string q[i]) }
    = assert { string_of_array q l (i+1) ==
                 S.app (string q[i]) (string_of_array q l i) };
      assert { string_of_array q l u ==
               S.app (string_of_array q (i+1) u) (string_of_array q l (i+1)) }

  let rec lemma string_of_array_eq
    (q1 q2: array rope) (l u: int)
    requires { 0 <= l <= u <= Array.length q1 = Array.length q2 }
    requires { forall j: int. l <= j < u -> q1[j] = q2[j] }
    ensures  { string_of_array q1 l u == string_of_array q2 l u }
    = variant { u - l } if l < u then string_of_array_eq q1 q2 (l+1) u

  lemma string_of_array_frame:
    forall q: array rope, l u: int. 0 <= l <= u <= Array.length q ->
    forall i: int, r: rope. (0 <= i < l \/ u <= i < Array.length q) ->
    string_of_array q l u == string_of_array q[i <- r] l u

  let rec lemma string_of_array_concat_empty
    (q: array rope) (l u: int)
    requires { 0 <= l <= u <= Array.length q }
    requires { forall j: int. l <= j < u -> q[j] = Emp }
    ensures  { string_of_array q l u == S.empty }
    = variant { u - l } if l < u then string_of_array_concat_empty q (l+1) u

  function string_of_queue (q: array rope) : char_string =
    string_of_array q 2 (Array.length q)

  let rec insert (q: array rope) (i: int) (r: rope) : unit
    requires { 2 <= i < length q = max+1 }
    requires { inv r }
    requires { forall j: int. 2 <= j <= max -> inv q[j] }
    requires { S.length (string_of_array q i (max+1)) + R.length r
               < fib (max+1) }
    ensures  { forall j: int. 2 <= j <= max -> inv q[j] }
    ensures  { forall j: int. 2 <= j < i -> q[j] = (old q)[j] }
    ensures  { string_of_array q i (max+1) ==
                 S.app (string_of_array (old q) i (max+1)) (string r) }
    variant  { max - i }
  = let r' = concat q[i] r in
    if R.length r' < fib (i+1) then begin
      q[i] <- r';
      assert {    string_of_array q       (i+1) (max+1)
               == string_of_array (old q) (i+1) (max+1) }
    end else begin
      q[i] <- Emp;
      assert {    string_of_array q       i     (max+1)
               == string_of_array (old q) (i+1) (max+1) };
      assert {   S.app (string_of_array q       i (max+1)) (string r')
              == S.app (string_of_array (old q) i (max+1)) (string r) };
      insert q (i+1) r';
      assert { string_of_array q i (max+1) == string_of_array q (i+1) (max+1) }
    end

  let rec insert_leaves (q: array rope) (r: rope) : unit
    requires { 2 < length q = max+1 }
    requires { inv r }
    requires { forall j: int. 2 <= j <= max -> inv q[j] }
    requires { S.length (string_of_queue q) + R.length r < fib (max+1) }
    ensures  { forall j: int. 2 <= j <= max -> inv q[j] }
    ensures  { string_of_queue q ==
                 S.app (string_of_queue (old q)) (string r) }
    variant  { r }
  = match r with
    | Emp              -> ()
    | Str _ _ _        -> insert q 2 r
    | App left right _ -> insert_leaves q left; insert_leaves q right
  end

  let balance (r: rope) : rope
    requires { inv r }
    requires { R.length r < fib (max+1) }
    ensures  { inv result }
    ensures  { string result == string r }
  = let q = Array.make (max+1) Emp in
    assert { string_of_queue q == S.empty };
    insert_leaves q r;
    assert { string_of_queue q == string r };
    let res = ref Emp in
    for i = 2 to max do
      invariant { inv !res }
      invariant { string !res == string_of_array q 2 i }
      res := concat q[i] !res
    done;
    !res

end