(*               Jean-Francois Monin              *)
(*             Verimag Grenoble - 2004            *)

(** * Strings *)

Parameter string : Set.

(** append string *)
Parameter aps : string -> string -> string.
Parameter int : Set.
Parameter string_of_int : int -> string.
Parameter nullstr : string.

Notation " '#' " := nullstr.
Notation "u  ^^  v" := (aps u v) (at level 5, right associativity).

Definition r_int a i := a ^^ (string_of_int i).

(** * Concrete formats 

Each type [X] to be printed is endowed with a function [r_X]
which appends a printed representation of a value of type [X] 
to the right of a given string. 
This is equivalent to providing a function for converting 
an inhabitant of [X] to a string, but is handier 
and yields shorter definitions. 
Reasoning about functions [r_X], rather than on strings, 
is a simple but important design step of the present developement.
*)

Record Printable : Type := mkpr {X : Set; r_X : string -> X -> string}.

Notation "a  ^/ P /^  x " := (r_X P a x) (at level 10, P at level 99).

Implicit Arguments mkpr [X].

(** %\newcommand{\percent}{{\small%[%]%}}% *)
(**
A printf format specification such as
 "[foo] %\percent% [s bar] %\percent%[i]" is represented by 
a concrete value %\\% 
[(Lit foo (Str (Lit bar (Int Stop))))] 
and is mapped to the type %\\% [string -> int -> A].

In order to leave the type of printable data types open, 
specifications such as [Str] and [Int] are not constructors, 
but special cases of [Data].
*)

Inductive format : Type :=
  | Stop : format
  | Data : Printable -> format -> format
  | Lit : string -> format -> format.


(** %\subsubsection*{Examples}% *)

Definition pstr := mkpr aps.
Definition pint := mkpr r_int.

Definition Str := Data pstr.
Definition Int := Data pint.

(** Lists can easily be taken into account.
*)

(** The following tokens represent respectively ',' %'['% and %']'%. *)
Parameters comma leftbk rightbk : string.

Require Import List.

Fixpoint r_nelist (P : Printable) (a : string) (l : list (X P)) {struct l} :
 string :=
  match l with
  | nil => a ^^ rightbk
  | x :: l => r_nelist P a ^^ (comma ^/P/^  x) l
  end.

Definition r_list (P : Printable) (a : string) (l : list (X P)) : string :=
  match l with
  | nil => a ^^ leftbk ^^ rightbk
  | x :: l => r_nelist P a ^^ (leftbk ^/P/^  x) l
  end.

Definition plist (P : Printable) := mkpr (r_list P).

Definition Lis (P : Printable) := Data (plist P).
Definition Lisi := Lis pint.
Definition Lisii := Lis (plist pint).

(** In the sequel we will use the following concrete example.
*)
Parameters foo bar : string.
Definition example := Lit foo (Str (Lit bar (Int Stop))).