Coqでsprintf

sprintf.v

Require Import Ascii String.
Require Import List.
Require Import Arith NArith ZArith Omega.
Require Import Recdef Program.Wf.
Require Import Zdiv.

(* Local Notation "a :: b" := (String a b) : string_scope. *)

Definition Z_to_digit(n:Z):ascii :=
  match n with
  | 0%Z => "0"%char
  | 1%Z => "1"%char
  | 2%Z => "2"%char
  | 3%Z => "3"%char
  | 4%Z => "4"%char
  | 5%Z => "5"%char
  | 6%Z => "6"%char
  | 7%Z => "7"%char
  | 8%Z => "8"%char
  | 9%Z => "9"%char
  | _ => "?"%char
  end.

Program Fixpoint uZ_to_s(n:Z) (H:(0<=n)%Z) (s:string)
    {wf (fun x y => (Zabs_nat x < Zabs_nat y)%nat) n}:string :=
  if Z_eq_dec 0%Z n then
    s
  else
    uZ_to_s (Zdiv n 10)%Z _ (String (Z_to_digit (Zmod n 10%Z)) s)%string.
Next Obligation.
apply Z_div_pos; [omega|tauto].
Defined.
Next Obligation.
apply inj_lt_rev.
do 2 rewrite inj_Zabs_nat.
rewrite (Zabs_eq n); [|tauto].
rewrite Zabs_eq.
apply Z_div_lt; omega.
apply Z_div_pos; omega.
Defined.
Next Obligation.
unfold MR.
intros (n,(x,Hn)).
remember (Zabs_nat n) as nn.
revert n x Heqnn Hn.
induction (lt_wf nn).
exists.
simpl.
intros (y,(H1A,H1B)).
simpl.
intros H2.
apply H0 with (y:=Zabs_nat y).
rewrite Heqnn; apply H2.
reflexivity.
Defined.

Program Definition Z_to_s(n:Z) (s:string):string :=
  match Z_dec' 0%Z n with
  | inleft (left _) => (uZ_to_s n _ s)%string
  | inleft (right _) => (String "-"%char (uZ_to_s (-n) _ s))%string
  | inright _ => (String "0"%char s)%string
  end.
Next Obligation.
omega.
Defined.
Next Obligation.
omega.
Defined.

Definition N_to_s(n:N) (s:string):string := Z_to_s (Z_of_N n) s.

Record TV := {
  TV_T: Type;
  TV_V: TV_T
}.

Fixpoint sprintf_impl(s:string)(f:string -> string):TV :=
  match s with
  | EmptyString => Build_TV _ (f ""%string)
  | String "%" (String "d" st) =>
      Build_TV _ (fun n => TV_V (sprintf_impl st (fun x => f (Z_to_s n x))))
  | String "%" (String "u" st) =>
      Build_TV _ (fun n => TV_V (sprintf_impl st (fun x => f (N_to_s n x))))
  | String "%" (String "s" st) =>
      Build_TV _ (fun k => TV_V (sprintf_impl st (fun x => f (k ++ x)%string)))
  | String "%" (String "%" st) =>
      Build_TV _ (TV_V (sprintf_impl st (fun x => f (String "%" x))))
  | String sh st =>
      Build_TV _ (TV_V (sprintf_impl st (fun x => f (String sh x))))
  end.

Definition sprintf(s:string) := TV_V (sprintf_impl s id).

Eval lazy in (sprintf "").
Eval lazy in (sprintf "Hello, world!").
Eval lazy in (sprintf "%d + %d = %d" 1%Z 2%Z (1+2)%Z).
Eval lazy in (sprintf "Hello, %s!" "Masaki"%string).
(* Eval lazy in (sprintf "%s" 0%Z). (* error *) *)