string.timl

structure String = struct

(* fun int2str a = __&int2str a *)
(* fun print a = __&print a *)
fun printc a = __&printc a
                
open Array
       
(* datatype string = String {len : Nat} of array byte {len} --> string *)
type string = fn {len : Nat} => array byte {len}

(* new_string "abc" == String (new_array {'a', 'b', 'c'}) *)
val a : string {3} = "abc"
    
fun size {len : Nat} (s : string {len}) return nat {len} = length s

fun concat {len1 len2 : Nat} (s1 : string {len1}, s2 : string {len2}) =
  let
    val len1 = size s1
    val len2 = size s2
    val len = len1 #+ len2
    val s = array (len, int2byte 0)
    val () = for (#0, len1, (), fn {i : Nat | i < len1} (i : nat {i}, _) =>
      update (s, i, sub (s1, i)))
    val () = for (#0, len2, (), fn {i : Nat | i < len2} (i : nat {i}, _) =>
      update (s, len1 #+ i, sub (s2, i)))
  in
    s
  end

fun print {len : Nat} (s : string {len}) =
  let
    val len = size s
    val () = for (#0, len, (), fn {i : Nat | i < len} (i : nat {i}, _) =>
      printc <| sub (s, i))
  in
    ()
  end

(* val a = printc #"a" *)
(* val a = print "abc" *)
(* val () = __&halt a *)

fun assert {len : Nat} (b, msg : string {len}) = if b then () else print "assert failed: "; print msg; print "\n"; __&halt 1
    
fun int2char i = int2byte (i + 48)
                          
fun nat2byte {i : Nat} (i : nat {i}) = int2char <| nat2int i
                          
datatype lemma1 {n : Nat} =
         Lemma1 {n = 0 -> 10 ** n = 1} {n >= 1 -> 10 ** n >= 10} {n >= 1 -> 10 ** n = 10 ** (n-1) * 10} of lemma1 {n}

fun lemma1 {n : Nat} () return lemma1 {n} =
  @Lemma1 {n} {_} {admit} {admit}
          
fun nat2bytes {d : Nat} {i : Nat | 10 ** d <= i /\ i < 10 ** (d+1) \/ i = 0 /\ d = 0} (i : nat {i}) return list byte {d+1} using 6.0 + 8.0 * $d =
  let
    val Lemma1 _ = @lemma1 {d} ()
  in
  ifdec i #< #10 then
    [nat2byte i] : list byte {d+1}
  (* todo: bug. Need to fix precedence here *)
  else int2char (nat2int i mod 10) :: (@nat2bytes {d-1} {_} (i #/ #10)) : list byte {d+1} using 5.0 + 8.0 * $d
  end

(* val a = @nat2bytes {1} {_} #10 *)
(* val () = __&halt a *)
          
(*   10**77 < 2**256 < 10**78   *)
datatype lemma2 {n : Nat} =
         Lemma2 {n < 2 ** 256 -> floor (log10 $n) < 78} {10 ** floor (log10 $n) <= n /\ n < 10 * floor (log10 $n)} of lemma2 {n}

fun lemma2 {n : Nat} () return lemma2 {n} =
  @Lemma2 {n} {admit} {admit}
          
datatype string_from_int = StringFromInt {len : Nat | len <= 78} of string {len} --> string_from_int
                                                                        
fun int2str i return string_from_int using 1400.0 =
  let
    val @SomeNat {n} n = int2nat i
    val Lemma2 _ = @lemma2 {n} ()
  in
    StringFromInt (fromList <| rev <| (@nat2bytes {floor (log10 $n)} {_} n))
  end

end