{- Computer Aided Formal Reasoning (G53CFR, G54CFR) Thorsten Altenkirch Lecture 14: Typed Assembly Language We continue the theme form the last lecture and look at the implementation of a virtual machine and a compiler for the language of expressions. We start with an untyped machine which may fail and has to do runtime checks (in real life the machine may just crash). Then we introduce "Typed Assembly Language" which can be executed without fear and without checking. The compiler from typed expressions to typed assembly language is virtually identical to the untyped one but uses dependent types to certify the invariant that types are preserved. As beofre we use the typechecker together with the compiler (actually the code generation part of a compiler) to compile and run untyped expressions. -} module l14 where open import Data.Nat open import Data.Bool open import Data.Maybe open import Data.Product open import Relation.Nullary open import Relation.Binary.PropositionalEquality open import l13 -- import expressions and values {- We define an untyped assembly language for a stack machine to evaluate untyped expressions. Note that this is tre-structured assembly language - this can be translated using gotos by yet another pass. -} data Code : Set where push : Val → Code → Code -- push a value on the stack +M : Code → Code -- add the top values on the stack ≤M : Code → Code -- compare top values on the stack branch : Code → Code → Code -- branch depending on the top value -- instead of gotos the code is tree-structured stop : Code -- end of computation {- the set of stacks - basically a list of values. However, I prefer to write stacks backward - that is why I am not using stacks. -} infixl 4 _▹_ data Stack : Set where ε : Stack _▹_ : Stack → Val → Stack {- run executes the code, returning the final stack when the computation is finished. Note that we are using the partiality monad and the operations +v and ≤v from the last lecture which check wether their arguments have the right type. Apart from dynamic type errors, run may also fail because there are not enough values on the stack. -} run : Stack → Code → Maybe Stack run s (push v p) = run (s ▹ v) p run ((s ▹ v) ▹ v') (+M p) = v +v v' >>= λ v+v' → run (s ▹ v+v') p run _ (+M _) = nothing run ((s ▹ v) ▹ v') (≤M p) = v ≤v v' >>= λ v≤v' → run (s ▹ v≤v') p run _ (≤M _) = nothing run (s ▹ bool true) (branch p p') = run s p run (s ▹ bool false) (branch p p') = run s p' run (s ▹ _) (branch _ _) = nothing run _ (branch _ _) = nothing run s stop = just s {- The compiler is straightforward. We are using "continuation-passing style", i.e. the compiler gets the code which is to be exceuted after the translation of the expression. This has the advantage that we don't have to concatenate code (and hence is more efficient) and it is also easier to reason about (even though we are not going to prove compiler correctness now. -} compile : Expr → Code → Code compile (nat n) c = push (nat n) c compile (bool b) c = push (bool b) c compile (e +E e') c = compile e (compile e' (+M c)) -- here we exploit the continuation passing style. -- to compile the who expression we first compile e then e' then add +M compile (e ≤E e') c = compile e (compile e' (≤M c)) compile (ifE e then e' else e'') c = compile e (branch (compile e' c) (compile e'' c)) {- combining compile and run. compiler correctness would be to show that compileRun is extensionally equal to ⟦_⟧,i.e. correct : (e : Expr) compileRun e ≡ ⟦ e ⟧ -} compileRun : Expr → Maybe Val compileRun e with run ε (compile e stop) ... | just (_ ▹ v) = just v ... | _ = nothing {- Instead of proving we just test our test cases. -} v1'' : Maybe Val v1'' = compileRun e1 v2'' : Maybe Val v2'' = compileRun e2 v3'' : Maybe Val v3'' = compileRun e3 {- Next we define "typed assembly language". The type of assembly code refers to the type of the stack before and after executing the code. -} {- Stack types are just sequences of value types (defined in the previous lecture. -} data StackTy : Set where ε : StackTy _▹_ : StackTy → Ty → StackTy {- Typed stacks are indexed over stack types. -} data TStack : StackTy → Set where ε : TStack ε _▹_ : ∀ {Γ σ} → TStack Γ → TVal σ → TStack (Γ ▹ σ) {- Typed code is indexed by two stacks: the stack it expects and the stack after executing it. -} data TCode : StackTy → StackTy → Set where push : ∀ {Γ Δ σ} → TVal σ → TCode (Δ ▹ σ) Γ → TCode Δ Γ +M : ∀ {Γ Δ} → TCode (Δ ▹ nat) Γ → TCode (Δ ▹ nat ▹ nat) Γ ≤M : ∀ {Γ Δ} → TCode (Δ ▹ bool) Γ → TCode (Δ ▹ nat ▹ nat) Γ branch : ∀ {Γ Δ} → TCode Δ Γ → TCode Δ Γ → TCode (Δ ▹ bool) Γ stop : ∀ {Γ} → TCode Γ Γ {- the typed machine doesn't need to use the Maybe monad becuase the typing invariants are expressed in the indizies. -} trun : ∀ {Γ Δ} → TStack Γ → TCode Γ Δ → TStack Δ trun s (push v p) = trun (s ▹ v) p trun (s ▹ nat n ▹ nat m) (+M p) = trun (s ▹ (nat (n + m))) p trun (s ▹ nat n ▹ nat m) (≤M p) = trun (s ▹ bool (dec2bool (m ≤? n))) p trun (s ▹ bool true) (branch p p') = trun s p trun (s ▹ bool false) (branch p p') = trun s p' trun s stop = s {- the typed compiler is virtually identical to the untyped compiler but its type makes it clear that the code it generates leaves a value corresponding to the type of the expression on the stack. -} tcompile : ∀ {Γ Δ σ} → TExpr σ → TCode (Γ ▹ σ) Δ → TCode Γ Δ tcompile (nat n) c = push (nat n) c tcompile (bool b) c = push (bool b) c tcompile (e +E e') c = tcompile e (tcompile e' (+M c)) tcompile (e ≤E e') c = tcompile e (tcompile e' (≤M c)) tcompile (ifE e then e' else e'') c = tcompile e (branch (tcompile e' c) (tcompile e'' c)) {- typed compilation followed by running on the typed machine: -} tcompileRun : ∀ {σ} → TExpr σ → TVal σ tcompileRun e with trun ε (tcompile e stop) ... | (_ ▹ v) = v {- combining this with the type checker we obtan yet another way to execute untyped expression in an efficient and fast way. -} checkCompileRun : Expr → Maybe Val checkCompileRun e = infer e >>= λ c → return (⌊ tcompileRun (Check.te c) ⌋v)