PreTalent23.Compiler_in_class
From PreTalent23 Require Import Overture.
From Coq.Lists Require Import List.
From Coq.micromega Require Import Lia.
From PreTalent23 Require Import Spl_before_third_session SplVM_before_third_session.
Import ListNotations.
From Coq.Lists Require Import List.
From Coq.micromega Require Import Lia.
From PreTalent23 Require Import Spl_before_third_session SplVM_before_third_session.
Import ListNotations.
The compiler from SPL to SPLVM and its correctness
Our compiler is a simple recursive function that translates SPL programs to SPLVM programs (lists of SPLVM instructions).Exercise (in class)
Prove the following lemma.
Fixpoint compile (e : expr) : VMProg :=
match e with
| Num n => [PushNum n]
| Bool b => [PushBool b]
| ITE c t f =>
let vm_c := compile c in
let vm_t := compile t in
let vm_f := compile f in
vm_c ++ [CJump (S (length vm_f))] ++ vm_f ++ [Jump (length vm_t)] ++ vm_t
| And e1 e2 =>
let vm_e1 := compile e1 in
let vm_e2 := compile e2 in
vm_e1 ++ vm_e2 ++ [DoAnd]
| Or e1 e2 =>
let vm_e1 := compile e1 in
let vm_e2 := compile e2 in
vm_e1 ++ vm_e2 ++ [DoOr]
| Not e =>
let vm_e := compile e in
vm_e ++ [DoNot]
| Le e1 e2 =>
let vm_e1 := compile e1 in
let vm_e2 := compile e2 in
vm_e1 ++ vm_e2 ++ [DoLe]
| Eq e1 e2 =>
let vm_e1 := compile e1 in
let vm_e2 := compile e2 in
vm_e1 ++ vm_e2 ++ [DoEq]
| Add e1 e2 =>
let vm_e1 := compile e1 in
let vm_e2 := compile e2 in
vm_e1 ++ vm_e2 ++ [DoAdd]
| Sub e1 e2 =>
let vm_e1 := compile e1 in
let vm_e2 := compile e2 in
vm_e1 ++ vm_e2 ++ [DoSub]
| Mul e1 e2 =>
let vm_e1 := compile e1 in
let vm_e2 := compile e2 in
vm_e1 ++ vm_e2 ++ [DoMul]
end.
(* Some test cases for the compilation function above. *)
Eval compute in runVMProg [] 0 (compile (Spl_before_third_session.add23)). (* Should print: (0, [NumEl 5]) *)
Eval compute in runVMProg [] 0 (compile (Spl_before_third_session.if3le5)). (* Should print: (0, [NumEl 2#]) *)
Eval compute in runVMProg [] 0 (compile (Spl_before_third_session.bad_prog)). (* Should print: (0, [NumEl 5; NumEl 3]) *)
Discuss in class
How can the compiler be correct (also see the correctness theorem below) when it is returning a result (the element on the top of the stack) in a case where the eval function returns Err?
Eval compute in runVMProg [] 0 (compile (Spl_before_third_session.sub74)). (* Should print: (0, [NumEl 3]) *)
The result relation
We define the relation that we expect to hold between the results obtained by the eval function on a program and the results we expect to get by running the corresponding virtual machine.
Inductive result_rel : result → stack_elem → Prop :=
| num_res_rel n : result_rel (NumRes n) (NumEl n)
| bool_res_rel b : result_rel (BoolRes b) (BoolEl b).
| num_res_rel n : result_rel (NumRes n) (NumEl n)
| bool_res_rel b : result_rel (BoolRes b) (BoolEl b).
The following theorem states the correctness property for our compiler:
when we run the compiled version of a program on the empty stack we get back a stack that contains
the only the expected result.
Prove the following Theorem.
Exercise (partly in class)
Prove the following Theorem.
Lemma app_cons {A} (l1 l2 : list A) (a : A) : l1 ++ a :: l2 = (l1 ++ [a]) ++ l2.
Proof.
rewrite <- (rev_involutive ((l1 ++ [a]) ++ l2)).
rewrite !rev_app_distr; simpl.
rewrite <- app_assoc; simpl.
rewrite !rev_involutive.
reflexivity.
Qed.
Lemma compile_correct_gen e s :
eval e ≠ Err →
∃ se, runVMProg s 0 (compile e) = (0, se :: s) ∧ result_rel (eval e) se.
Proof.
revert s.
induction e; intros s.
- intros He.
simpl.
eexists. split; [reflexivity|constructor].
- intros He.
simpl.
eexists; split; [reflexivity|constructor].
- intros He.
simpl.
simpl in He.
pose proof He as He'.
apply when_bool_correct1 in He'.
destruct He' as [b1 He'].
rewrite He' in He.
simpl in He.
destruct (IHe1 s) as [se1 [He1c He1r]].
{ rewrite He'; congruence. }
destruct b1.
+ destruct (IHe2 s) as [se2 [He2c He2r]].
{ trivial. }
exists se2.
split.
* rewrite runVMProg_app.
rewrite He1c.
rewrite He' in He1r.
inversion He1r.
subst.
simpl.
rewrite app_cons.
rewrite runVMProg_jump.
-- assumption.
-- rewrite app_length; simpl. lia.
* rewrite He'; simpl.
assumption.
+ destruct (IHe3 s) as [se3 [He3c He3r]].
{ trivial. }
exists se3.
split.
* rewrite runVMProg_app.
rewrite He1c.
rewrite He' in He1r.
inversion He1r.
subst.
simpl.
rewrite runVMProg_app.
rewrite He3c.
simpl.
rewrite <- (app_nil_r (compile e2)).
rewrite runVMProg_jump.
-- simpl. reflexivity.
-- rewrite app_length; simpl. lia.
* rewrite He'; simpl.
assumption.
- intros He.
simpl in He.
pose proof He as He'.
apply when_bool_correct1 in He'.
destruct He' as [b1 He'].
rewrite He' in He.
simpl in He.
pose proof He as He''.
apply when_bool_correct1 in He''.
destruct He'' as [b2 He''].
rewrite He'' in He.
simpl in He.
exists (BoolEl (b1 && b2)).
destruct (IHe1 s) as [se1 [He1c He1r]].
{ rewrite He'; congruence. }
destruct (IHe2 (se1 :: s)) as [se2 [He2c He2r]].
{ rewrite He''; congruence. }
split.
+ simpl.
rewrite runVMProg_app.
rewrite He1c.
rewrite runVMProg_app.
rewrite He2c.
rewrite He' in He1r.
inversion He1r.
rewrite He'' in He2r.
inversion He2r.
simpl.
reflexivity.
+ simpl.
rewrite He'.
simpl.
rewrite He''.
simpl.
constructor.
-
Abort.
Theorem compile_correct e :
eval e ≠ Err →
∃ se, runVMProg [] 0 (compile e) = (0, [se]) ∧ result_rel (eval e) se.
Proof.
Abort.