Require Import List.
Require Import ZArith.


Inductive E : Set -> Type :=

| EZ : Z -> E Z
| Eadd : E Z -> E Z -> E Z
| Emul : E Z -> E Z -> E Z
| Esub : E Z -> E Z -> E Z
| Ecmp : E Z -> E Z -> E bool

| Ebool : bool -> E bool
| Enot : E bool -> E bool
| Eand : E bool -> E bool -> E bool
| Eor : E bool -> E bool -> E bool
| Eif : forall {a : Set}, E bool -> E a -> E a -> E a
.

SearchAbout Z.

Fixpoint Einterpret {t} (e : E t) : t :=
  match e with
    | EZ n => n
    | Eadd p q => (Einterpret p + Einterpret q)%Z
    | Emul p q => (Einterpret p * Einterpret q)%Z
    | Esub p q => (Einterpret p - Einterpret q)%Z
    | Ecmp p q => if Z_zerop (Einterpret p - Einterpret q) then true else false
    | Ebool b => b
    | Enot b => negb (Einterpret b)
    | Eand p q => andb (Einterpret p) (Einterpret q)
    | Eor p q => andb (Einterpret p) (Einterpret q)
    | Eif _ b m n => if (Einterpret b) then (Einterpret m) else (Einterpret n)
  end.





Inductive etype : Set :=
| etype_bool
| etype_z.

Definition ev_etype e :=
  match e with
    | etype_bool => bool
    | etype_z => Z
  end.


Print eq_rect.
Check eq_rect.

Definition equal_at_etype t (a : option (list Z)) : ev_etype t -> Prop :=
  match a with
    | Some (x :: _) => match t with
                         | etype_bool => fun b => (if Z_zerop x then true else false) = b
                         | etype_z => fun b => x = b
                       end
    | _ => fun _ => False
  end.

Fixpoint etype_of {T} (e : E T) : etype :=
    match e with
    | EZ n => etype_z
    | Eadd p q => etype_z
    | Emul p q => etype_z
    | Esub p q => etype_z
    | Ecmp p q => etype_bool
    | Ebool b => etype_bool
    | Enot b => etype_bool
    | Eand p q => etype_bool
    | Eor p q => etype_bool
    | Eif _ b m n => etype_of m
  end.

Theorem ev_etype_of {T} (e : E T) : T = ev_etype (etype_of e).
induction e; try reflexivity.
simpl; assumption.
Defined.

Definition Einterpret'' {T} (e : E T) : ev_etype (etype_of e).
rewrite <- ev_etype_of.
exact (Einterpret e).
Defined.

Definition Einterpret' {T} (e : E T) : etype * Z.
generalize (Einterpret'' e).
destruct (etype_of e); simpl.
refine (fun b => (etype_bool, if b then 1%Z else 0%Z)).
refine (fun z => (etype_z, z)).
Defined.


Theorem etype_inversion (e : E Z) : etype_of e = etype_z.
Proof.

Lemma etype_inversion' {T} (e : E T) : T = Z -> etype_of e = etype_z.


Lemma bool_ne_Z : bool <> Z.
Proof.
  intro.
  assert (exists a : Z, exists b, exists c,
                                    a <> b /\ a <> c /\ b <> c).
  exists (0%Z).
  exists (1%Z).
  exists (2%Z).
  omega.
  rewrite <- H in H0.
  repeat destruct H0.
  destruct H1.
  destruct x; destruct x0; destruct x1; intuition.
Qed.


induction e; simpl; intuition;
 elimtype False; apply bool_ne_Z; trivial.

Qed.

apply etype_inversion'.
reflexivity.

Qed.

Inductive A : Set :=
| Apush : Z -> A
| Apop
| Aadd
| Asub
| Amul
| Askip : nat -> A
| Askipz : nat -> A.

Require Import Recdef.
Require Import Omega.

Fixpoint programLength (program : list A) : nat :=
  match program with
    | Askip n :: program => 1 + n + programLength program
    | Askipz n :: program => 1 + n + programLength program
    | _ :: program => 1 + programLength program
    | _ => 0
  end.

Function Ainterpret (stack : list (etype * Z)) (program : list A) {measure programLength program} : option (list (etype * Z)) :=
  match program with
    | nil => Some stack
    | instruction :: program =>
      match instruction with
        | Apush n => Ainterpret ((etype_z, n) :: stack) program
        | Apop => match stack with
                    | nil => None
                    | _ :: stack => Ainterpret stack program
                  end
        | Aadd => match stack with
                    | (_,x) :: (_,y) :: stack => Ainterpret ((etype_z, (x + y)%Z) :: stack) program
                    | _ => None
                  end
        | Asub => match stack with
                    | (_,x) :: (_,y) :: stack => Ainterpret ((etype_z, (x - y)%Z) :: stack) program
                    | _ => None
                  end
        | Amul => match stack with
                    | (_,x) :: (_,y) :: stack => Ainterpret ((etype_z, (x * y)%Z) :: stack) program
                    | _ => None
                  end
        | Askip n => match n with
                       | 0 => Ainterpret stack program
                       | S n => Ainterpret stack (Askip n :: program)
                     end
        | Askipz n => match stack with
                        | nil => None
                        | (_,top) :: stack' =>
                          if Z_zerop top
                          then Ainterpret stack' program
                          else match n with
                                 | 0 => Ainterpret stack' program
                                 | S n => Ainterpret stack' (Askipz n :: program)
                               end
                      end
      end
  end.

intros; simpl.
omega.

intros; simpl.
omega.

intros; simpl.
omega.

intros; simpl.
omega.

intros; simpl.
omega.

intros; simpl.
omega.

intros; simpl.
omega.

intros; simpl.
omega.

intros; simpl.
omega.

intros; simpl.
omega.

Defined.


Print Ainterpret_equation.


Fixpoint compile {t} (e : E t) (l : list A) : list A :=
  match e with
    | EZ z => Apush z :: l
    | Eadd p q => compile p (compile q (Aadd :: l))
    | Esub p q => compile p (compile q (Asub :: l))
    | Emul p q => compile p (compile q (Amul :: l))
    | Ecmp p q => compile p (compile q (Asub :: l))
    | Ebool b => match b with
                   | true => Apush 1 :: l
                   | false => Apush 0 :: l
                 end
    | Enot b => Apush 1 :: (compile b (Asub :: l))
    | Eand p q => compile p (compile q (Amul :: l))
    | Eor p q => compile p (compile q (Aadd :: l))
    | Eif _ b p q =>
      let pl := length (compile p nil) in
      let ql := length (compile q nil) in
      compile b (Askipz (1 + pl) :: compile p (Askip ql :: compile q l))
  end.

Definition stackTop {t} (s : option (list t)) : option t :=
  match s with
    | None => None
    | Some nil => None
    | Some (x :: xs) => Some x
  end.


Fixpoint etype_eq_list (a :  (list (etype * Z))) (b :  (list (etype * Z))) : Prop :=
  match a, b with
    |  nil,  nil => True
    |  ((t1,v1) :: a),  ((t2,v2) :: b) => match t1, t2 with
                                                  | etype_bool, etype_bool => (if Z_zerop v1 then true else false) = (if Z_zerop v2 then true else false)
                                                  | etype_z, etype_z => v1 = v2
                                                  | _, _ => False
                                                end /\ etype_eq_list ( a) ( b)
    | _, _ => False
  end.

Theorem etype_eq_list_refl : forall a, etype_eq_list a a.
Admitted.
Theorem etype_eq_list_symm : forall a b, etype_eq_list a b -> etype_eq_list b a.
Admitted.
Theorem etype_eq_list_trans : forall a b c, etype_eq_list a b -> etype_eq_list b c -> etype_eq_list a c.
Admitted.

Require Import Setoid.

Program Instance etype_eq_list_equivalence : Equivalence etype_eq_list.
Obligation 1.
unfold Reflexive.
apply etype_eq_list_refl.
Defined.
Obligation 2.
unfold Symmetric.
apply etype_eq_list_symm.
Defined.
Obligation 3.
unfold Transitive.
apply etype_eq_list_trans.
Defined.

Theorem correct {T} : forall (e : E T) s l,
                        etype_eq_list
                          (option_rec (fun _ => list (etype * Z)) (fun i => i) nil
                                      (Ainterpret s (compile e l)))
                          (option_rec (fun _ => list (etype * Z)) (fun i => i) nil
                                      (Ainterpret (Einterpret' e :: s) l)).
Proof.
  induction e; intros; simpl.

  rewrite Ainterpret_equation.
  unfold Einterpret'.
  unfold Einterpret''.
  simpl.
  reflexivity.

  unfold Einterpret'.
  unfold Einterpret''.
  simpl.
  rewrite IHe1.
  rewrite IHe2.
  rewrite Ainterpret_equation.
  unfold Einterpret'.
  unfold Einterpret''.
  clear IHe1.
  clear IHe2.

  pose (etype_inversion e2) as e.
  rewrite e at 5.

  rewrite <- (etype_inversion e2) in *.

  rewrite (etype_inversion e1) in *.
  rewrite (etype_inversion e2).

  assert (etype_of e2 = etype_z).



  unfold Einterpret'; simpl.
  unfold equal_at_etype; simpl.
  simpl in IHe1.

Lemma


  simpl.

  destruct t.
; simpl in prf; try (elimtype False; discriminate).

discriminate.