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

Require Import combi.
Require Import concrete_format.

(* -------------------------------------------------- *)

(**
    * Typing formats with type transformers
A simpler typing of [kformat] prevents one to compose formats, 
while there is no such limitation with Damas-Milner typing.
(This may be useful for the extraction of programs which
handle dynamic formats.) 
Therefore, we will use type transformers. 
In some sense, the latter show    
the type inference mechanism of the ML type system at work. 
The idea is that a functional format maps a type $\alpha$ to 
[string->int->]$\alpha$ (in our example).

    ** Type transformers 
*)

Definition idt (A : Set) := A.
Definition datat (P : Printable) (A : Set) := X P -> A.
Definition intt := datat pint.
Definition strt := datat pstr.

(** ** Type transformer associated to a concrete format *)
Fixpoint type_transf_of_fmt (f : format) : Set -> Set :=
  match f with
  | Stop => idt
  | Data P f => (datat P) o (type_transf_of_fmt f)
  | Lit s f => type_transf_of_fmt f
  end.

(** %\subsubsection*{Example (cont'd)}% *)
Eval compute in (type_transf_of_fmt example).
(** = %$\lambda \,\alpha$% [ : Set. string -> int -> ] %$\alpha$% *)

Fixpoint r_sprintf (f : format) : string -> type_transf_of_fmt f string :=
  match f return (string -> type_transf_of_fmt f string) with
  | Stop => fun a=> a
  | Data P f => fun a x=> r_sprintf f (a ^/P/^  x)
  | Lit s f => fun a=> r_sprintf f a ^^ s
  end.

Definition sprintf (f : format) := r_sprintf f #.

(** ** Functional formats

The main argument of [sprintfk] is a function of type [(kt tf)], 
where [tf] can be expressed by means of a format.
 *)

(** CPS version of appending to the right. *)
Definition kt (tf : Set -> Set) :=
  forall A : Set, (string -> A) -> string -> tf A.

(** %\subsubsection*{Example (cont'd)}% *)
Eval compute in (kt (type_transf_of_fmt example)).
(**
[= forall A : Set, (string -> A) -> string -> string->int->A]
*)

(** The main argument of [sprintfk] is a functional format [f].
We only have to know that its type has the form [kt tf].
The fact that [f] may be computed using a concrete format
is not relevant.
*)

Definition sprintfk (tf : Set -> Set) (f : kt tf) : 
  tf string := f string (fun s=> s) #.
Implicit Arguments sprintfk [tf].

(** Functional formats are constructed using primitives formats 
such as [lit], [str], [sint], etc. 
The two latter are themselves special cases of our [kdata], 
which is not admitted in ML, in contrast with [str], [sint], etc. 
However we keep [kdata] here for the sake of generality 
in the reasoning. 
In ML examples, we use only instances of [kdata].
*)

Definition kid : kt idt := fun A k a=> k a.

Definition kdata (P : Printable) : kt (fun A=> X P -> A) :=
  fun (A : Set) (k : string -> A) a x=> k (a ^/P/^  x).

Definition lit (x : string) : kt idt := fun A k a=> k (a ^^ x).

(** ** Examples *)

Definition str := kdata pstr.
Definition sint := kdata pint.

Definition lis (P : Printable) := kdata (plist P).
Definition lisi := lis pint.
Definition lisii := lis (plist pint).

(** ** Translation
Composition of polymorphic functions: 
'o' cannot be used, though the underlying untyped term is the same. 
The type of the result is explicitly computed
and put in the form ([kt] %$\tau$%), where %$\tau$% happens to be
obtained by sequential composition of type transformers.
In this way, the job of Damas-Milner type inference is done explicitly.
*)
Definition seqp (tg tf : Set -> Set) (kg : kt tg) (kf : kt tf) :
  kt (tg o tf) := fun A k=> kg (tf A) (kf A k).
Implicit Arguments seqp [tg tf].
Notation "f 'oo' g" := (seqp f g) (at level 5, right associativity).

Fixpoint kformat (f : format) : kt (type_transf_of_fmt f) :=
  match f return (kt (type_transf_of_fmt f)) with
  | Stop => kid
  | Data P f => (kdata P) oo (kformat f)
  | Lit s f => (lit s) oo (kformat f)
  end.

(** %\subsubsection*{Example (cont'd)}% *)
Remark check_value : kformat example = (lit foo) oo str oo (lit bar) oo sint.
Proof. reflexivity. Qed.

(** Formats can be composed.*)
Remark check_compo :
 kformat example =
 (kformat (Lit foo (Str Stop))) oo (kformat (Lit bar (Int Stop))).
Proof. reflexivity. Qed.

(** A format can even be composed with itself. *)
Check (let kex := kformat example in kex oo kex).

(** ** Correctness of sprintfk w.r.t. sprintf

A brutal attempt to prove that 
[(sprintf f) = (sprintfk (kformat f))] 
holds for all [f] fails, because the accumulator 
changes at each recursive call 
(an induction on [f] would lead us to to prove something on 
[# ^^ s] while the induction hypothesis is on [#]). 
The usual trick is then to replace [#] with 
a variable (let us call it [a]) which is in the scope of the induction. 
We first unfold [sprintf] and [sprintfk] in order to 
work with [r_sprintf] and [kformat]. 
Then, if we try to prove 
%\begin{equation}
\mbox{%[forall a  (r_sprintf f a) = (kformat f (fun s=> s) a)]%}
\label{eq-ext}
\end{equation}%
by induction on [f], 
we face another problem: how to prove 
%$$
\mbox{%[fun x=> r_sprintf f (a ^/P/^ x)] %~=~% [fun x=> kformat f string (fun s=> s) (a ^/P/^ x)]%}
$$%
from the induction hypothesis %(\ref{eq-ext})%? 
This is a typical case where extensionality 
makes life easier. Adding the following axiom 
would allow us to finish the proof in a trivial way. 
*)

Axiom
  extensionality :
    forall (A B : Set) (f g : A -> B),
    (forall x : A, f x = g x) -> (fun x=> f x) = (fun x=> g x).

(** 
But this workaround is not satisfactory. 
A first way out is to prove a weakened extensional 
version of the theorem, informally telling us that 
applying [(r_sprintf f a)] to its arguments yields 
the same string as [(kformat f string (fun s=> s) a)]. 
This is a somewhat tedious exercise in CIC. 
We just need formal definitions of: 
%\begin{itemize}%
%\item% 
an arguments vector paramerized by a format;
%\item% 
the application of dependent functions like 
[(r_sprintf f a)] to such a vector. 
%\end{itemize}%

 *** Intensionalization

However, we can prove the first formulation of the theorem,
provided we work with 
a %\emph{still more intensional}% statement:
%\begin{equation}
\mbox{%[fun a=> r_sprintf f a] %~=~% [fun a=> kformat f (fun s=> s) a]%}
\label{eq-int}
\end{equation}%

%\noindent% 
We call %(\ref{eq-int})% the %\emph{intensionalized}% version 
of %(\ref{eq-ext})%.
More generaly, the intensionalized version of 
$\forall x,\;P=Q$ is $\lambda x\,P = \lambda x\,Q$. 

The proof is by induction on the format [f]. 
In the second case, unfolding [kdata] and [oo] in [kformat] yields something 
similar to what we have in [r_sprintf] ([A] and [k] will be respectively 
equal to [string] and [fun x=> x]).
*)

Remark key_data_kformat :
 forall A k (tf : Set -> Set) (kf : kt tf) (P : Printable),
 ((kdata P) oo kf) A k = fun a x=> kf A k (a ^/P/^ x).
Proof. reflexivity. Qed.

(** This can be expressed with the induction hypothesis [fun a => g a]
    using the combinator$\;$[o2].
*)

Remark key_data :
  forall P (A:Set) (g:string->A), 
  (fun a x => g (a ^/P/^ x)) = (fun a => g a) o2 (r_X P).
Proof. reflexivity. Qed.

(** And similarly in the third induction case, with [o] instead of [o2]. *)
Remark key_lit_kformat :
 forall A k (tf : Set -> Set) (kf : kt tf) (x : string),
 ((lit x) oo kf) A k = fun a=> kf A k (a ^^ x).
Proof. reflexivity. Qed.

Remark key_lit :
  forall s A (g:string->A), 
  (fun a => g (a ^^ s)) = (fun a => g a) o (fun a=> a ^^ s).
Proof. reflexivity. Qed.

(** Using these remarks we get a straightforward proof. 
    We can also inline them in order to get intensionally equal
    definitions of r_sprintf and kformat. *)
Fixpoint r_sprintf1 (f : format) : string -> type_transf_of_fmt f string :=
  match f return (string -> type_transf_of_fmt f string) with
  | Stop => fun a=> a
  | Data P f => (fun a => (r_sprintf1 f a)) o2 (r_X P) 
  | Lit s f => (fun a => (r_sprintf1 f a)) o (fun a=> a ^^ s) 
  end.

(** For [kformat] we actually inline intensionalized versions of
    [key_data_kformat] and of %\\% [key_lit_kformat].
*)

Fixpoint kformat1 (f : format) : kt (type_transf_of_fmt f) :=
  match f return (kt (type_transf_of_fmt f)) with
  | Stop => kid
  | Data P f => fun A k=> (fun a => (kformat1 f A k a)) o2 (r_X P) 
  | Lit s f => fun A k=> (fun a => (kformat1 f A k a)) o (fun a=> a ^^ s)
  end.

Theorem sprintf_kformat :
 forall f : format, 
   (fun a => r_sprintf f a) = (fun a => kformat f string (fun s=> s) a).
Proof.
  change (forall f : format, 
   (fun a => r_sprintf1 f a) = (fun a => kformat1 f string (fun s=> s) a)).
  simple induction f; clear f; simpl.
    unfold kid. reflexivity.
    intros P f hrec. case hrec. reflexivity.
    intros x f hrec. case hrec. reflexivity.
Qed.

(** *** Simplification

  By chance, both members of the desired equality happen to have the form
  $\lambda a.\, g a$, hence we can try a still more intensional version,
  i.e.%\ % an $\eta$-reduced version of %(\ref{eq-int})%:
%\begin{equation}
\mbox{%[r_sprintf f] %~=~% [kformat f (fun s=> s).]%}
\label{eq-int-eta}
\end{equation}%

  %\noindent% 
  The proof is straightforward, we even don't need to recognize 
  combinatorial expressions.
*)

Theorem sprintf_kformat_eta :
 forall f : format, r_sprintf f = kformat f string (fun s=> s).
Proof.
  simple induction f; clear f; simpl.
    unfold kid. reflexivity.
    intros P f hrec. unfold seqp, kdata. case hrec. reflexivity.
    intros s f hrec. unfold seqp, lit. case hrec. reflexivity.
Qed.


(**  *** Wanted corollary

Remark that 
the concrete format [f] is %\emph{not}% an argument of [sprintfk]. *)

Theorem sprintf_sprintfk :
 forall f : format, sprintf f = sprintfk (kformat f).
Proof.
  intro f. unfold sprintf, sprintfk. 
  exact (rew_apply (sprintf_kformat_eta f) #).
Qed.