(********** types for gui objects **********)

(* (top-left corner of) (x, y) of top-left and bottom-right *)
type coord_t = int * int * int * int

(* object identifier *)
type id_t = String of string * coord_t
	  | H of id_t list * coord_t
	  | V of id_t * id_t * id_t * coord_t

let get_coord id = match id with
  String (_, coord) | H (_, coord) | V (_, _, _, coord) -> coord

let add_coord (x0, y0, x1, y1) (dx, dy) =
  (x0 + dx, y0 + dy, x1 + dx, y1 + dy)

let rec move (x, y) id = match id with
    String (str, coord) -> String (str, add_coord coord (x, y))
  | H (ids, coord) -> H (List.map (move (x, y)) ids, add_coord coord (x, y)) 
  | V (id1, id2, id3, coord) ->
      V (move (x, y) id1, move (x, y) id2, move (x, y) id3,
         add_coord coord (x, y))

let inside (x, y) id =
  let (x0, y0, x1, y1) = get_coord id in
  x0 <= x && x < x1 && y0 <= y && y < y1

(********** functions used by users **********)
(* drawing function : string list -> id_t *)
let create_str str = String (str, (0, 0, String.length str, 1))

(* re-arrange items horizontally *)
let rec combine_list x ids gap max_y = match ids with
    [] -> []
  | id :: rest ->
      let (x0, y0, x1, y1) = get_coord id in
      move (x - x0, max_y - (y1 - y0)) id
      :: combine_list (x + (x1 - x0) + gap) rest gap max_y

let rec get_max_x ids = match ids with
    [] -> 0
  | [id] ->
      let (_, _, x1, _) = get_coord id in
      x1
  | id :: rest -> get_max_x rest

let rec get_max_y ids max_y = match ids with
    [] -> max_y
  | id :: rest ->
      let (_, y0, _, y1) = get_coord id in
      get_max_y rest (max max_y (y1 - y0))

let combine_des ids gap =
  let max_y = get_max_y ids 1 in
  let lst = combine_list 0 ids gap max_y in
  let max_x = get_max_x lst in
  H (lst, (0, 0, max_x, max_y))

let combineH ids = combine_des ids 0

(* arrange two items vertically *)
let combineV up_id under_id =
  let (_, _, x1u, y1u) = get_coord up_id in
  let (_, _, x1d, y1d) = get_coord under_id in
  V (up_id,
     move (0, y1u) (create_str (String.make (max x1u x1d) '-')),
     move (0, y1u + 1) under_id,
     (0, 0, max x1u x1d, y1u + y1d + 1))

(* arrange an axiom *)
let combineV_axm id = combineV (create_str "") id

let rec collect_strings id = match id with
    String (str, (x0, y0, x1, y1)) -> [(y0, (x0, x1, str))]
  | H (ids, _) -> List.flatten (List.map collect_strings ids)
  | V (id1, id2, id3, _) ->
      collect_strings id1 @ collect_strings id2 @ collect_strings id3

let display id =
  let rec display_line lst x = match lst with
      [] -> ()
    | (_, (x0, x1, str)) :: rest ->
	print_string (String.make (x0 - x) ' ');
	print_string str;
	display_line rest x1 in
  let rec display_all lst y =
    if lst = [] then () else
    let (lst_n, lst_rest) = List.partition (fun (y1, _) -> y1 = y) lst in
    let lst_n = List.sort (fun (_, (x1, _, _)) (_, (x2, _, _)) -> x1 - x2)
			  lst_n in
    display_line lst_n 0;
    print_newline ();
    display_all lst_rest (y + 1) in
  let lst = collect_strings id in
  display_all lst 0


(* a type user neeed to define *)
(* ユーザが推論規則を定義するときに使う型 *)
type 'a prule_t = 
    Infer of 'a * 'a prule_t list
  | Axiom of 'a


(* 以下、多分、いずれ不要になる *)
type mode_t = OCC | SUB | CLEAR
let mode = ref OCC