Inductive sinstr : Type :=
| SPush : nat -> sinstr
| SLoad : id -> sinstr
| SPlus : sinstr
| SMinus : sinstr
| SMult : sinstr.
(** Write a function to evaluate programs in the stack language. It
takes as input a state, a stack represented as a list of
numbers (top stack item is the head of the list), and a program
represented as a list of instructions, and returns the stack after
executing the program. Test your function on the examples below.
Note that the specification leaves unspecified what to do when
encountering an [SPlus], [SMinus], or [SMult] instruction if the
stack contains less than two elements. In a sense, it is
immaterial what we do, since our compiler will never emit such a
malformed program. *)
Fixpoint s_execute (st : state) (stack : list nat)
(prog : list sinstr)
: list nat :=
match prog with
| [] => stack
| ins :: prog' =>
match ins with
| SPush n => s_execute st (n :: stack) prog'
| SLoad x => s_execute st (st x :: stack) prog'
| SPlus =>
match stack with
| na :: nb :: stack' => s_execute st (nb+na :: stack') prog'
| _ => s_execute st stack prog'
end
| SMinus =>
match stack with
| na :: nb :: stack' => s_execute st (nb-na :: stack') prog'
| _ => s_execute st stack prog'
end
| SMult =>
match stack with
| na :: nb :: stack' => s_execute st (nb*na :: stack') prog'
| _ => s_execute st stack prog'
end
end
end.
Eval compute in
s_execute empty_state []
[SPush 5; SPush 3; SPush 1; SMinus].
Eval compute in
s_execute (update empty_state X 3) [3;4]
[SPush 4; SLoad X; SMult; SPlus].
Fixpoint s_compile (e : aexp) : list sinstr :=
match e with
| ANum n => [SPush n]
| AId id => [SLoad id]
| APlus a1 a2 => (s_compile a1) ++ (s_compile a2) ++ [SPlus]
| AMinus a1 a2 => (s_compile a1) ++ (s_compile a2) ++ [SMinus]
| AMult a1 a2 => (s_compile a1) ++ (s_compile a2) ++ [SMult]
end
.
(** After you've defined [s_compile], prove the following to test
that it works. *)
Example s_compile1 :
s_compile (AMinus (AId X) (AMult (ANum 2) (AId Y)))
= [SLoad X; SPush 2; SLoad Y; SMult; SMinus].
Proof.
simpl. auto.
Qed.
(** **** Exercise: 3 stars, advanced (stack_compiler_correct) *)
(** The task of this exercise is to prove the correctness of the
compiler implemented in the previous exercise. Remember that
the specification left unspecified what to do when encountering an
[SPlus], [SMinus], or [SMult] instruction if the stack contains
less than two elements. (In order to make your correctness proof
easier you may find it useful to go back and change your
implementation!)
Prove the following theorem, stating that the [compile] function
behaves correctly. You will need to start by stating a more
general lemma to get a usable induction hypothesis; the main
theorem will then be a simple corollary of this lemma. *)
Lemma s_compile_correct' : forall (st:state) (l0:list nat) (l1:list sinstr) (l2:list sinstr),
s_execute st l0 (l1++l2) = s_execute st (s_execute st l0 l1) l2.
Proof.
intros. generalize dependent l0. induction l1. simpl. auto. intros. destruct a; try apply IHl1.
destruct l0. simpl; try apply IHl1. destruct l0. simpl; try apply IHl1. apply IHl1.
destruct l0. simpl; try apply IHl1. destruct l0. simpl; try apply IHl1. apply IHl1.
destruct l0. simpl; try apply IHl1. destruct l0. simpl; try apply IHl1. apply IHl1.
Qed.
Theorem s_compile_correct'' : forall (st : state) (e : aexp) (l:list nat),
s_execute st l (s_compile e) = (aeval st e) :: l.
Proof.
intros. generalize dependent st. generalize dependent l. induction e; intros; auto. simpl. rewrite s_compile_correct'.
rewrite s_compile_correct'. rewrite IHe1. rewrite IHe2. auto.
simpl. rewrite s_compile_correct'. rewrite s_compile_correct'. rewrite IHe1. rewrite IHe2. auto.
simpl. rewrite s_compile_correct'. rewrite s_compile_correct'. rewrite IHe1. rewrite IHe2. auto.
Qed.
Theorem s_compile_correct : forall (st : state) (e : aexp),
s_execute st [] (s_compile e) = [ aeval st e ].
Proof.
intros.
assert(H:=s_compile_correct'' st e []). auto.
Qed.
(*-- Check --*)
Check s_compile1 :
s_compile (AMinus (AId X) (AMult (ANum 2) (AId Y)))
= [SLoad X; SPush 2; SLoad Y; SMult; SMinus].
Check s_compile_correct : forall (st : state) (e : aexp),
s_execute st [] (s_compile e) = [ aeval st e ].