(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) Jean-Christophe Filliatre                               *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

(* Ropes-based implementation of Buffer *)

type rope = 
  | Str of string
  | App of rope * rope * int (* total length *)

let rope_empty = Str ""

let rope_length = function
  | Str s -> String.length s
  | App (_, _, n) -> n

let rec rope_nth i = function
  | Str s -> 
      String.unsafe_get s i
  | App (l, r, _) ->
      let ll = rope_length l in
      if i < ll then rope_nth i l else rope_nth (i - ll) r

type t = {
  mutable rope : rope;     (* the left part is a rope *)
  mutable buffer : string; (* the right part is a buffer... *)
  mutable position : int;  (* ...with [position] bytes used *)
}

let create n =
  let n = if n < 1 then 1 else n in
  let n = if n > Sys.max_string_length then Sys.max_string_length else n in
  let s = String.create n in
  { rope = rope_empty; buffer = s; position = 0; }

let reset b =
  b.rope <- rope_empty;
  b.position <- 0

let clear = reset

let length b = 
  rope_length b.rope + b.position

(* [blit s i r] blits the contents of rope [r] in string [s] at index [i] *)
let rec blit_rope s i = function
  | Str str -> 
      String.blit str 0 s i (String.length str)
  | App (l, r, _) ->
      let ll = rope_length l in
      blit_rope s i l;
      blit_rope s (i + ll) r

let contents b =
  let r = rope_length b.rope in
  let n = b.position in
  let len = r + n in
  if len > Sys.max_string_length then invalid_arg "Rbuffer.contents";
  let s = String.create len in
  blit_rope s 0 b.rope;
  String.blit b.buffer 0 s r n;
  s

(* [blit_subrope s i ofs len] blits the subrope [r[ofs..ofs+len-1]] in string
   [s] at index [i] *)
let rec blit_subrope s i ofs len = function
  | Str str ->
      assert (ofs >= 0 && ofs + len <= String.length str);
      String.blit str ofs s i len
  | App (l, r, _) ->
      let ll = rope_length l in
      if ofs + len <= ll then 
	blit_subrope s i ofs len l
      else if ofs >= ll then 
	blit_subrope s i (ofs - ll) len r 
      else begin
	let lenl = ll - ofs in
	blit_subrope s i ofs lenl l;
	blit_subrope s (i + lenl) 0 (len - lenl) r
      end

let sub b ofs len =
  let r = rope_length b.rope in
  if len > Sys.max_string_length || 
     ofs < 0 || len < 0 || ofs > r + b.position - len
  then invalid_arg "Buffer.sub";
  let s = String.create len in
  if ofs + len <= r then 
    blit_subrope s 0 ofs len b.rope
  else if ofs >= r then
    String.blit b.buffer (ofs - r) s 0 len
  else begin
    blit_subrope s 0 ofs (r - ofs) b.rope;
    String.blit b.buffer 0 s (r - ofs) (ofs + len - r)
  end;
  s

let nth b i =
  let r = rope_length b.rope in
  if i < 0 || i >= r + b.position then invalid_arg "Buffer.nth";
  if i < r then rope_nth i b.rope else String.unsafe_get b.buffer (i - r)

(* moves the data in [b.buffer], if any, to the rope; ensures [b.position=0] *)
let move_buffer_to_rope b =
  let pos = b.position in
  if pos > 0 then begin
    let n = String.length b.buffer in
    if pos = n then begin
      (* whole buffer goes to the rope; faster to allocate a new buffer *)
      b.rope <- App (b.rope, Str b.buffer, rope_length b.rope + pos);
      b.buffer <- String.create n
    end else begin
      (* part of the buffer goes to the rope; easier to copy it *)
      b.rope <- App (b.rope, Str (String.sub b.buffer 0 pos),
		     rope_length b.rope + pos)
    end;
    b.position <- 0
  end
  
let add_char b c =  
  if b.position = String.length b.buffer then move_buffer_to_rope b;
  let pos = b.position in
  b.buffer.[pos] <- c;
  b.position <- pos + 1

(* allocates space for [len] bytes and returns the corresponding place
   (as a string and an offset within that string) *)
let alloc b len =
  let n = String.length b.buffer in
  let pos = b.position in
  let len' = pos + len in
  if len' <= n then begin
    (* fits in the buffer *)
    b.position <- len';
    b.buffer, pos
  end else if len' <= Sys.max_string_length then begin
    (* buffer and len fit in a new string, allocated in the rope *)
    let str = String.create len' in
    String.blit b.buffer 0 str 0 pos;
    b.rope <- App (b.rope, Str str, rope_length b.rope + len');
    b.position <- 0;
    str, pos
  end else begin
    (* buffer and len require two strings, allocated in the rope *)
    let str = String.create len in
    b.rope <- App (b.rope, 
		   App (Str (String.sub b.buffer 0 pos), Str str, len'),
		   rope_length b.rope + len');
    b.position <- 0;
    str, 0
  end

let safe_add_substring b s offset len =
  let str, pos = alloc b len in
  String.blit s offset str pos len

let add_substring b s offset len =
  if offset < 0 || len < 0 || offset > String.length s - len
  then invalid_arg "Buffer.add_substring";
  safe_add_substring b s offset len

let add_string b s =
  safe_add_substring b s 0 (String.length s)

let add_buffer b b2 =
  if b.position > 0 then move_buffer_to_rope b;
  (* now we have b.position = 0 *)
  b.rope <- App (b.rope, b2.rope, rope_length b.rope + rope_length b2.rope);
  add_substring b b2.buffer 0 b2.position

let rec add_channel b ic len =
  if len <= Sys.max_string_length then begin
    let str, pos = alloc b len in
    really_input ic str pos len
  end else begin
    let str, pos = alloc b Sys.max_string_length in
    really_input ic str pos Sys.max_string_length;
    add_channel b ic (len - Sys.max_string_length)
  end

let output_buffer oc b =
  let rec output_rope = function
    | Str s -> output oc s 0 (String.length s)
    | App (l, r, _) -> output_rope l; output_rope r
  in
  output_rope b.rope;
  output oc b.buffer 0 b.position

open Format

let print fmt b =
  let rec print_rope = function
    | Str s -> pp_print_string fmt s
    | App (l, r, _) -> print_rope l; print_rope r
  in
  print_rope b.rope;
  pp_print_string fmt (String.sub b.buffer 0 b.position)

      
(* substitution: the code of [add_substitute] is actually indepedent of
   the buffer data structure (and thus could be written outside);
   as a consequence, what follows is simply a copy of [Buffer]'s code, from
   Pierre Weis and Xavier Leroy, projet Cristal, INRIA Rocquencourt *)

let closing = function
  | '(' -> ')'
  | '{' -> '}'
  | _ -> assert false;;

(* opening and closing: open and close characters, typically ( and )
   k: balance of opening and closing chars
   s: the string where we are searching
   start: the index where we start the search. *)
let advance_to_closing opening closing k s start =
  let rec advance k i lim =
    if i >= lim then raise Not_found else
    if s.[i] = opening then advance (k + 1) (i + 1) lim else
    if s.[i] = closing then
      if k = 0 then i else advance (k - 1) (i + 1) lim
    else advance k (i + 1) lim in
  advance k start (String.length s);;

let advance_to_non_alpha s start =
  let rec advance i lim =
    if i >= lim then lim else
    match s.[i] with
    | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_' |
      'é'|'à'|'á'|'è'|'ù'|'â'|'ê'|
      'î'|'ô'|'û'|'ë'|'ï'|'ü'|'ç'|
      'É'|'À'|'Á'|'È'|'Ù'|'Â'|'Ê'|
      'Î'|'Ô'|'Û'|'Ë'|'Ï'|'Ü'|'Ç' ->
        advance (i + 1) lim
    | _ -> i in
  advance start (String.length s);;

(* We are just at the beginning of an ident in s, starting at start. *)
let find_ident s start =
  match s.[start] with
  (* Parenthesized ident ? *)
  | '(' | '{' as c ->
     let new_start = start + 1 in
     let stop = advance_to_closing c (closing c) 0 s new_start in
     String.sub s new_start (stop - start - 1), stop + 1
  (* Regular ident *)
  | _ ->
     let stop = advance_to_non_alpha s (start + 1) in
     String.sub s start (stop - start), stop;;

(* Substitute $ident, $(ident), or ${ident} in s,
    according to the function mapping f. *)
let add_substitute b f s =
  let lim = String.length s in
  let rec subst previous i =
    if i < lim then begin
      match s.[i] with
      | '$' as current when previous = '\\' ->
         add_char b current;
         subst current (i + 1)
      | '$' ->
         let ident, next_i = find_ident s (i + 1) in
         add_string b (f ident);
         subst ' ' next_i
      | current when previous == '\\' ->
         add_char b '\\';
         add_char b current;
         subst current (i + 1)
      | '\\' as current ->
         subst current (i + 1)
      | current ->
         add_char b current;
         subst current (i + 1)
    end in
  subst ' ' 0;;