Require Import Ascii.
Require Import String.
Require Import ZArith.
Require Import Equivalence.
Require Import EquivDec.
Require Import Compare_dec.

Require Import Qcert.Utils.Digits.
Require Import Qcert.Utils.CoqLibAdd.
Require Import Qcert.Utils.FloatAdd.
Require Import Qcert.Utils.StringAdd.

Preliminaries

Section ToString.
  Local Open Scope string.

  Definition boolToString (b:bool) : string
    := if b then "true" else "false".

  Definition quote_char (a:ascii)
    := match a with
       | """"%char => "\"""
       | _ => String a EmptyString
       end.

  Definition quote_string (s:string)
    := flat_map_string quote_char s.

  Definition stringToStringQuote (quotel:string) (s:string)
    := "" ++ quotel ++ "" ++ quote_string s ++ "" ++ quotel ++ "".

  Definition stringToString (s:string) : string
    := s.

  Global Instance ToString_Z : ToString Z
    := { toString := Z_to_string10}.

  Global Instance ToString_nat : ToString nat
    := { toString := nat_to_string10}.

  Global Instance ToString_float : ToString float
    := { toString := float_to_string}.

  Global Instance ToString_bool : ToString bool
    := { toString := boolToString}.
End ToString.