PreTalent24.Compiler
From PreTalent24 Require Import Overture.
From Coq.Lists Require Import List.
From Coq.micromega Require Import Lia.
From PreTalent24 Require Import Spl SplVM.
Import ListNotations.
From Coq.Lists Require Import List.
From Coq.micromega Require Import Lia.
From PreTalent24 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).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.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).
| 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.