Require Import Nat List.
Import List.ListNotations.

(** Syntax of arithmetic expressions *)

Inductive aexp :=
| Aco : nat -> aexp
| Ava : nat -> aexp
| Apl : aexp -> aexp -> aexp
| Amu : aexp -> aexp -> aexp
| Asu : aexp -> aexp -> aexp
.

Definition state := list nat.

Example S1 := [1; 2].
Example S2 := [0; 3].

Fixpoint get (i:nat) (s:state) : nat :=
  match i,s with
  | 0   ,  v :: _   => v
  | S i',  _ :: s'  => get i' s'
  | _   ,  _        => 0
  end.

(** Functional semantics of [aexp] *)
Fixpoint evalA (a: aexp) (s: state) : nat :=
  match a with
  | Aco n => n
  | Ava x => get x s
  | Apl a1 a2 =>  evalA a1 s + evalA a2 s
  | Amu a1 a2 =>  evalA a1 s * evalA a2 s
  | Asu a1 a2 =>  evalA a1 s - evalA a2 s
  end.

Example X := Ava 1.


(* ----------------   Compilation of aexp   ----------------------- *)
(* We want to compile [aexp] language to a stack-based assembly 
   language and prove the correctness of the compiler.
   We define : - le target assembly language (CODE)
               - its semantics (exec)
               - the compiler (compileA)
 *)

(* A small stack-based assembly language (als) *)

Inductive instr_als : Set :=
  | Ipush  : nat -> instr_als
  | Ifetch : nat -> instr_als
  | Iadd   : instr_als
  | Isub   : instr_als
  | Imul   : instr_als.

(* An assembly code is a list of instructions *)

Definition CODE := list instr_als.

(* Its functional (or denotional) semantics *)

(* The stack of values the instruction set works on is also represented
   by a list.
   Pushing 2 then 5 on the empty stack gives 5 :: 2 :: [].
*)

Definition stack := list nat.

Definition push n : stack -> stack := fun st => n :: st.

(* The generic execution of a binary operator that takes the operator as a parameter;
   returns nil if the stack contains less than 2 numbers *)

Definition exec_opbin (op : nat -> nat -> nat) : stack -> stack :=
  fun s => match s with
           | b :: a :: s => op a b :: s
           | _ => nil
           end.

(* Functional semantics of an instruction     *)

Definition exec_i (i : instr_als) (s:state) : stack -> stack :=
  match i with
  | Ipush n => push n
  | Ifetch x => push (get x s)
  | Iadd => exec_opbin Nat.add
  | Isub => exec_opbin Nat.sub
  | Imul => exec_opbin Nat.mul
  end.

(* Functional semantics of a code (made of a list of instructions) *)

Fixpoint exec (c : CODE) (s:state) (p:stack): stack :=
    match c with
      | nil => p
      | i :: c' =>
        let p' := (exec_i i s p) in (* [i] is executed starting from the stack [p] *)
        exec c' s p'                (* Then the remaining code is executed *)
    end.

(* Executions of codes can be composed as follows *)
(* Clumsy variant of theorem [dec_code] below, which is better. *)
Lemma comp_exec : forall c1 c2 s p1 p2 p3,
                  exec c1 s p1 = p2
               -> exec c2 s p2 = p3
               -> exec (c1++c2) s p1 = p3.
Proof.
  (* you may complete here (just to better appreciate the next one) *)
Admitted.

(* The execution of a code can be arbitrarily decomposed *)
(* Pay attention to the quantification of [p] in the induction. *)
Lemma dec_code :  forall c1 c2 s p, exec (c1++c2) s p = exec c2 s (exec c1 s p).
Proof.
  intros c1 c2 s.
  induction c1 as [| i1 c1 Hrec_c1]; simpl; intro p.
  (* COMPLETΕ HERE *)
Admitted.

(*
Compiling an arithmetic expression consists in concatenating the compilation
of sub-expressions.  For example, compiling [Apl a1 a2]  consists in concatenating
the compiled code of [a1] to the code of [a2] and finally the instruction [Iadd].
*)

Fixpoint compileA (a : aexp) : CODE :=
  match a with
    | Aco n      => [Ipush n]
    | Ava x      => [Ifetch x]
    | Apl a1 a2  => compileA a1 ++ compileA a2 ++ [Iadd]
    | Amu a1 a2  => compileA a1 ++ compileA a2 ++ [Imul]
    | Asu a1 a2  => compileA a1 ++ compileA a2 ++ [Isub]
  end.

(* Examples of arithmetic expressions *)

Example ae2px := Apl (Aco 2) X. (* 2 + x *)
Example ae9m2px := Asu (Aco 9) ae2px. (* 9 - (2 + x) *)

(* Examples of compiled codes *)

Compute (compileA ae2px).
Compute ae9m2px.
Compute (compileA ae9m2px).
Compute exec [Ipush 9; Ipush 2; Ifetch 1; Iadd; Isub] nil.

(* Examples of code executions
   with an empty initial stack and a state [S2] where the value of [x] is 3
*)


Compute exec (compileA (Aco 2)) S2 nil.
Compute exec (compileA ae2px) S2 nil.
Compute exec (compileA ae9m2px) S2 nil.

(*
  Correctness theorem of the compilation.
  General version for any initial stack.
*)

Theorem correct_compileA_all_stack :
  forall (a : aexp) (s : state) (p:stack),
    exec (compileA a) s p = exec [Ipush (evalA a s)] s p.
Proof.
  induction a as [n | x | a1 Ha1 a2 Ha2 | a1 Ha1 a2 Ha2 | a1 Ha1 a2 Ha2]; intros s p; cbn.
  - reflexivity.
  - reflexivity.
  (* COMPLETΕ HERE *)
Admitted.

(* The functional semantics (with an empty stack) of the code produced
   by compiling [a] is the same as the function that pushs the
   functional semantics of [a].
*)

Corollary correct_compileA : forall (a : aexp) (s:state),
                             exec (compileA a) s [] = [evalA a s].
Proof.
  (* COMPLETΕ HERE *)
Admitted.


(* Optional exercise *)


(* The next property states that values can be added at the bottom
   of the stack without influence on the execution of the code.

Lemma app_stack :forall c s p1 p1' p2, exec c s p1 = p1' -> exec c s (p1 ++ p2) = p1'++p2.

or, using an equivalent an more more concise formula

Lemma app_stack :forall c s p1 p2, exec c s (p1 ++ p2) = (exec c s p1)++p2.

But this is wrong! *)

(* Find a counter-example. *)

Fact wrong_app_stack : exists c s p1 p2, exec c s (p1 ++ p2) <> (exec c s p1) ++ p2.
  eexists. (* replace by [exists c] where [c] is the program of your counter example *)
  eexists. (* idem for the state, *)
  eexists. (* p1 *)
  eexists. (* and p2 *)
  simpl; intro H.
  Fail discriminate (* with the right witnesses, [discriminate] succeeds *).
Admitted.


(* One can prove that the property [app_stack], that does not hold in general,
   holds for compiled code. *)

(* You can use the following obvious property *)
Remark app_comm_cons {A} : forall (x y:list A) (a:A), a :: (x ++ y) = (a :: x) ++ y.
Proof. reflexivity. Qed.
                                                                               
Lemma app_stack : forall a s p1 p2,
    exec (compileA a) s (p1++p2) = (exec (compileA a) s p1)++p2.
Proof.
  (* COMPLETE HERE *)
Admitted.

(** Extraction *)
Require Import Extraction.
Extraction compileA.
Recursive Extraction compileA.