Require Import ZArith List String Ascii Recdef.
Open Scope Z_scope.
Open Scope string_scope.

Definition prop := Type.

Inductive box : Type :=
  vbox (l : list box) | hbox (l : list box) | hline 
| text (s: string) | center (b : box).

Definition fold (A B:Type)(f: A -> B -> B)(e : B) :=
  fix aux (l:list A) : B :=
    match l with nil => e | a::tl => f a (aux tl) end.

Implicit Arguments fold.

Fixpoint hsize (b : box) : Z :=
  match b with
    vbox l => fold (fun b' x => Zmax (hsize b') x) 0 l
  | hbox l => fold (fun b' x => 1 + (hsize b') + x) 0 l
  | center b => hsize b
  | hline => 0
  | text s => Z_of_nat (length s)
  end.

Fixpoint vsize (b : box) : Z :=
  match b with
    vbox l => fold (fun b' x => (vsize b') + x) 0 l
  | hbox l => fold (fun b' x => Zmax (vsize b') x) 0 l
  | center b => vsize b
  | hline => 1
  | text s => 1
  end.

Definition mkrule0 (conclusion : box) : box :=
  vbox (hline :: conclusion :: nil).

Definition mkrule1 (premise conclusion : box) : box :=
  vbox (premise :: hline :: center conclusion :: nil).

Definition mkrule2 (premise1 premise2 conclusion : box) : box :=
  vbox (hbox (premise1 :: text " " :: premise2 :: nil) :: hline ::
     center conclusion :: nil).

Definition dash := Eval compute in match "-" with String a _ => a | _ => zero end.

Function hline_string (x:Z) {measure Zabs_nat x} : string :=
  if Z_le_dec x 0 then "" else String dash (hline_string (x-1)).
intros x xpos _; apply Zabs_nat_lt; omega.
Defined.

Function space_string (x:Z) {measure Zabs_nat x} : string :=
  if Z_le_dec x 0 then "" else String Space (space_string (x-1)).
intros x xpos _; apply Zabs_nat_lt; omega.
Defined.

Function empty_box (height width : Z) {measure Zabs_nat height}: list string :=
  if Z_le_dec height 0 then nil else 
   space_string width :: empty_box (height - 1) width.
intros height width heightpos _; apply Zabs_nat_lt; omega.
Defined.

Fixpoint map2 (A B C : Type)(f : A -> B -> C) (l1 : list A)
  (l2 : list B) {struct l1} : list C :=
  match l1, l2 with
    a::tl1, b::tl2 => f a b :: map2 A B C f tl1 tl2
  | _, _ => nil
  end.

Implicit Arguments map2.

Definition compute_margins (outer inner : Z) : Z*Z :=
  let a := (outer - inner) / 2 in (a, outer - inner - a).

Fixpoint draw (b:box) (height width:Z) {struct b} : list string :=
  match b with
    vbox l =>
    (empty_box (height - (vsize b)) width ++
    fold (fun b' t => draw b' (vsize b') width ++ t) nil l)%list
  | hbox l =>
    fold (fun b' t => map2 append (map2 append (draw b' height (hsize b'))
                                               (empty_box height 1)) t)
         (empty_box height (width - hsize b)) l
  | hline =>
    (empty_box (height - 1) width ++ hline_string width :: nil)%list
  | center b =>
    let (above, below) := compute_margins height (vsize b) in
    let (left, right) := compute_margins width (hsize b) in
       (empty_box above width ++
       (map2 append (empty_box (vsize b) left)
             (map2 append (draw b (vsize b) (hsize b))
                   (empty_box (vsize b) right))) ++
       empty_box below width)%list
  | text s =>
    (empty_box (height - 1) width ++ 
      (s ++ space_string (width - Z_of_nat (length s)))%string :: nil)%list
  end.

Definition lf := Eval compute in ascii_of_nat 10.

Fixpoint display_aux (l:list string) : string :=
  match l with
    nil => ""
  | a :: tl => String lf (a ++ display_aux tl)
  end.

Definition display (b:box) :=
  display_aux (draw b (vsize b) (hsize b)).

Definition digit_to_string (n : Z) : string :=
   String (Ascii.ascii_of_nat (48 + Zabs_nat n)) "".

Function pos_Z_to_string  (n : Z) {measure Zabs_nat n} : string :=
  if Zle_bool n 0 then "0" else if Zle_bool n 9 then
     digit_to_string n
  else
     pos_Z_to_string (Zdiv n 10) ++ digit_to_string (Zmod n 10).
intros n npos nle9; apply Zabs_nat_lt.
assert (npos' := Zle_cases n 0). rewrite npos in npos'. clear npos.
assert (nle9' := Zle_cases n 9); rewrite nle9 in nle9'; clear nle9.
assert (Hdiv := Z_div_mod n 10).
unfold Zdiv. destruct (Zdiv_eucl n 10) as [q r].
omega.
Defined.

Definition Z_to_string (n : Z) : string :=
  if Zle_bool n (-1) then "-" ++ pos_Z_to_string (- n)
  else pos_Z_to_string n.