(* Exercice 1 *)

Require Import ZArith.

Open Scope Z_scope.

Inductive expr := Econst (n: Z) | Esub (e1 e2: expr).
Definition prog := expr.
Definition val := Z.

(* L'evaluateur en style direct *)

Fixpoint eval_0 (e: expr) : val :=
  match e with
  | Econst n => n
  | Esub e1 e2 => eval_0 e1 - eval_0 e2
  end.

Definition interp_0 (p: prog) : val := eval_0 p.

(* L'evaluateur en CPS *)

Fixpoint eval_1 {A: Type} (e: expr) (k: val -> A) : A :=
  match e with
  | Econst n => k n
  | Esub e1 e2 => 
      eval_1 e1 (fun v1 => eval_1 e2 (fun v2 => k (v1 - v2)))
  end.

Definition interp_1 (p: prog) : val := eval_1 p (fun v => v).

Lemma eval_1_correct:
  forall (A: Type) e (k: val -> A), eval_1 e k = k (eval_0 e).
Proof.
  induction e; simpl; intros.
  auto.
  rewrite IHe1, IHe2. auto.
Qed.

Theorem interp_1_correct:
  forall p, interp_1 p = interp_0 p.
Proof.
  intros. apply eval_1_correct. 
Qed.

(* Defonctionalisation de l'evaluateur CPS *)

Inductive cont :=
  | Cont_0
  | Cont_1 (e: expr) (k: cont)
  | Cont_2 (v: val) (k: cont).

(*  Cette definition intuitive ne passe pas a cause de la condition de garde:
    qu'est-ce qui garantit la terminaison?

Fixpoint eval_2 (e: expr) (k: cont) {struct e} : val :=
  match e with
  | Econst n => continue_2 k n
  | Esub e1 e2 => eval_2 e1 (Cont_1 e2 k)
  end

with continue_2 (k: cont) (v: val) {struct k} : val :=
  match k with
  | Cont_0 => v
  | Cont_1 e2 k => eval_2 e2 (Cont_2 v k)
  | Cont_2 v1 k => continue_2 k (v1 - v)
  end.
*)

(* Specification par predicats inductifs.  Ces predicats sont les graphes
   des fonctions eval_2 et continue_2 que l'on voudrait definir. *)

Inductive spec_eval_2: expr -> cont -> val -> Prop :=
  | eval_2_const: forall n k v,
      spec_continue_2 k n v ->
      spec_eval_2 (Econst n) k v
  | eval_2_sub: forall e1 e2 k v,
      spec_eval_2 e1 (Cont_1 e2 k) v ->
      spec_eval_2 (Esub e1 e2) k v

with spec_continue_2: cont -> val -> val -> Prop :=
  | continue_2_0: forall v,
      spec_continue_2 Cont_0 v v
  | continue_2_1: forall e2 k v res,
      spec_eval_2 e2 (Cont_2 v k) res ->
      spec_continue_2 (Cont_1 e2 k) v res
  | continue_2_2: forall v1 k v res,
      spec_continue_2 k (v1 - v) res ->
      spec_continue_2 (Cont_2 v1 k) v res.

(* On peut alos montrer un resultat de correction partielle:
   en supposant que eval_2 termine, voici ce que l'on peut dire
   de son resultat. *)

Lemma spec_eval_2_sound:
  forall e k res, spec_eval_2 e k res -> spec_continue_2 k (eval_0 e) res.
Proof.
  induction e; simpl; intros.
- inversion H; subst. auto.
- inversion H; subst. 
  specialize (IHe1 _ _ H4). inversion IHe1; subst.
  specialize (IHe2 _ _ H5). inversion IHe2; subst. 
  auto.
Qed.

Corollary spec_interp_2_sound:
  forall e res, spec_eval_2 e Cont_0 res -> res = eval_0 e.
Proof.
  intros. 
  assert (spec_continue_2 Cont_0 (eval_0 e) res) by (eapply spec_eval_2_sound; eauto).
  inversion H0; subst. auto.
Qed.

(* Une mesure de taille qui va montrer la terminaison *)

Fixpoint size_expr (e: expr): nat :=
  match e with
  | Econst n => 1%nat
  | Esub e1 e2 => (size_expr e1 + size_expr e2 + 1)%nat
  end.

Fixpoint size_cont (k: cont): nat :=
  match k with
  | Cont_0 => 0%nat
  | Cont_1 e2 k => (size_expr e2 + size_cont k)%nat
  | Cont_2 v1 k => (size_cont k)%nat
  end.

(* Implementation fonctionnelle de eval_2.  La mesure utilisee montre
  la terminaison.  "Program Fixpoint" ne traitant pas la recursion
  mutuelle, continue_2 est definie localement dans le cas "Econst n".
  Enfin, on utilise des types "riches" comme resultats, afin
  de montrer directement que eval_2 et continue_2 sont bien fideles
  a leur spec sous forme de predicats. *)

Require Coq.Program.Wf.

Program Fixpoint eval_2 (e: expr) (k: cont)
    {measure (size_expr e + size_cont k)%nat} :
    {res | spec_eval_2 e k res} :=
  match e with
  | Econst n =>
      let fix continue_2 (k1: cont) (v: Z) 
                         (SZ: (size_cont k1 <= size_cont k)%nat)
                     :  {res | spec_continue_2 k1 v res} :=
        match k1 with
        | Cont_0 => v
        | Cont_1 e2 k2 => eval_2 e2 (Cont_2 v k2)
        | Cont_2 v1 k2 => continue_2 k2 (v1 - v) _
        end
      in continue_2 k n _
  | Esub e1 e2 =>
      eval_2 e1 (Cont_1 e2 k)
  end.
Next Obligation. constructor. Defined.
Next Obligation. simpl in *. omega. Defined.
Next Obligation. 
  match goal with |- context[(proj1_sig ?x)] => destruct x as [res P] end.
  constructor; auto.
Defined.
Next Obligation. constructor; auto. Defined.
Next Obligation. 
  match goal with |- context[(proj1_sig ?x)] => destruct x as [res P] end.
  simpl. constructor; auto.
Qed.
Next Obligation. simpl. omega. Qed.
Next Obligation.
  match goal with |- context[(proj1_sig ?x)] => destruct x as [res P] end.
  simpl. constructor; auto.
Qed.

Definition interp_2 (e: expr) : val := proj1_sig (eval_2 e Cont_0).

Theorem interp_2_correct:
  forall p, interp_2 p = interp_0 p.
Proof.
  unfold interp_2, interp_0; intros. 
  destruct (eval_2 p Cont_0) as [res P]; simpl.
  apply spec_interp_2_sound; auto. 
Qed.