#include "share/atspre_staload.hats"

dataprop PAD(int, int, int) =
  | { p, l : nat } Yep(p, l, p - l)
  | { p, l : nat } Nope(p, l, 0)

extern
fun left_pad { p, l : nat | p > 0 && l > 0 } ( pad : ssize_t(p)
                                             , c : charNZ
                                             , s : strnptr(l)
                                             ) : [cushion:nat] (PAD(p, l, cushion) | strnptr(cushion+l))

extern
fun {t:t@ype} fill_list {n:nat} (size : ssize_t(n), c : t) :
  list_vt(t, n)

implement {t} fill_list {n} (size, c) =
  let
    fun loop { i : nat | i <= n } .<i>. ( size : ssize_t(i)
                                        , c : t
                                        , res : list_vt(t, n-i)
                                        ) : list_vt(t, n) =
      if (size = i2ssz(0)) then
        res
      else
        loop(pred(size), c, list_vt_cons(c, res))
  in
    loop(size, c, list_vt_nil())
  end

implement left_pad {p,l} (pad, c, s) =
  let
    val size = strnptr_length(s)
  in
    if (pad > size) then
      let
        val padding = pad - size
        val char_list = fill_list(padding, c)
        val pad_string = string_make_list_vt(char_list)
        val res = strnptr_append(pad_string, s)
      in
        (strnptr_free(pad_string) ; strnptr_free(s) ; (Yep{p,l} | res))
      end
    else
      (Nope{p,l} | s)
  end

implement main0 (argc, argv) =
  let
    val args = listize_argc_argv(argc, argv)
    val _ = if list_vt_length(args) = 3 then
      (let
        val c = '0'
        val s = g1ofg0(args[1]) : [n:nat] string(n)
        val pad = g1ofg0(g0string2int(args[2]))
      in
        if length(s) > 0 && pad > 0 then
          (let
            prval _ = lemma_not_empty(s) where
            { extern
              praxi lemma_not_empty {n:int} (x : string(n)) : [n > 0] void }
            prval _ = lemma_not_zero(pad) where
            { extern
              praxi lemma_not_zero {n:int} (x : int(n)) : [n > 0] void }
            val (pf | res) = left_pad(i2ssz(pad), c, string1_copy(s))
          in
            (println!("padding: ", res) ; strnptr_free(res))
          end)
        else
          print("Usage: left-pad <string-to-pad> <pad-length>\n")
      end)
    else
      print("Usage: left-pad <string-to-pad> <pad-length>\n")
  in
    list_vt_free(args)
  end