PreTalent23.Compiler
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.