PreTalent25.Compiler
From PreTalent25 Require Import Overture.
From Coq.Lists Require Import List.
From Coq.micromega Require Import Lia.
From PreTalent25 Require Import Spl SplVM.
Import ListNotations.
From Coq.Lists Require Import List.
From Coq.micromega Require Import Lia.
From PreTalent25 Require Import Spl SplVM.
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).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.add23)). (* Should print: (0, [NumEl 5]) *)
Eval compute in runVMProg [] 0 (compile (Spl.if3le5)). (* Should print: (0, [NumEl 2#]) *)
Eval compute in runVMProg [] 0 (compile (Spl.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?
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).
Lemma list_lem {A} (l l' : list A) (a : A) :
l ++ (a :: l') = (l ++ [a]) ++ l'.
Proof. induction l as [|x l IHl]; simpl; [|rewrite IHl]; trivial. Qed.
| num_res_rel n : result_rel (NumRes n) (NumEl n)
| bool_res_rel b : result_rel (BoolRes b) (BoolEl b).
Lemma list_lem {A} (l l' : list A) (a : A) :
l ++ (a :: l') = (l ++ [a]) ++ l'.
Proof. induction l as [|x l IHl]; simpl; [|rewrite IHl]; trivial. Qed.
Exercise (partly in class)
Prove the following Lemma.
Lemma compile_correct_gen s e :
eval e ≠ Err →
∃ se, runVMProg s 0 (compile e) = (0, se :: s) ∧ result_rel (eval e) se.
Proof.
intros He.
revert s; induction e; intros s.
- simpl.
eexists; split.
+ reflexivity.
+ constructor.
- simpl.
eexists; split.
+ reflexivity.
+ constructor.
- simpl in *.
destruct (eval e1).
+ simpl in *. congruence.
+ simpl in *.
destruct (λ H, IHe1 H s) as (se1 & He1 & He1r).
{ congruence. }
destruct b.
* destruct (λ H, IHe2 H s) as (se2 & He2 & He2r).
{ trivial. }
exists se2.
split; trivial.
rewrite runVMProg_app.
rewrite He1.
inversion He1r; subst.
simpl.
rewrite list_lem.
rewrite runVMProg_jump.
{ trivial. }
rewrite last_length; trivial.
* destruct (λ H, IHe3 H s) as (se3 & He3 & He3r).
{ trivial. }
exists se3.
split; trivial.
rewrite runVMProg_app.
rewrite He1.
inversion He1r; subst.
simpl.
rewrite runVMProg_app.
rewrite He3.
simpl.
rewrite runVMProg_jump'.
{ trivial. }
trivial.
+ simpl in *. congruence.
- simpl in *.
destruct (eval e1).
+ simpl in *. congruence.
+ simpl in *.
destruct (λ H, IHe1 H s) as (se1 & He1 & He1r).
{ congruence. }
destruct (eval e2).
* simpl in *. congruence.
* simpl in *.
destruct (λ H, IHe2 H (se1 :: s)) as (se2 & He2 & He2r).
{ congruence. }
exists (BoolEl (b && b0)); split.
-- rewrite runVMProg_app.
rewrite He1.
rewrite runVMProg_app.
rewrite He2.
inversion He1r; subst.
inversion He2r; subst.
simpl. reflexivity.
-- constructor.
* simpl in *. congruence.
+ simpl in *. congruence.
-
Admitted.
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.