Permalink
Browse files

Comments written.

  • Loading branch information...
1 parent 731cf15 commit 824e4614c5eacf5003bca3239486cfce63097e9a @ziman committed Feb 18, 2012
Showing with 17 additions and 0 deletions.
  1. +3 −0 Compiler.agda
  2. +5 −0 Correctness.agda
  3. +2 −0 Denotation.agda
  4. +2 −0 Execution.agda
  5. +2 −0 Expression.agda
  6. +3 −0 TypeUniverse.agda
View
@@ -9,12 +9,15 @@ open import Expression
open import Denotation
open import Code
+-- Create a single-instruction code block.
single : {s t} Instr s t Code s t
single i = i ,, cnil
+-- Translate operators to instructions.
opInstr : {s t u v} Op s t u Instr (s ∷ t ∷ v) (u ∷ v)
opInstr Plus = ADD
+-- Compile expressions to the corresponding code.
compile : {u v} Exp u Code v (u ∷ v)
compile (Lit n) = single (PUSH n)
compile (Bin op l r) = compile r ⊕ compile l ⊕ single (opInstr op)
View
@@ -12,10 +12,13 @@ open import Code
open import Compiler
open import Execution
+-- Correctness of operator translation. Because of the way how the translation
+-- is written, this is not "free" and must be proved for each operator.
op-correct : {u v w q st} {x : el u} {y : el v} (op : Op u v w)
exec-instr (opInstr {u} {v} {w} {q} op) (x :: y :: st) ≡ denOp op x y :: st
op-correct Plus = refl
+-- Exec distributes over ⊕.
compile-distr : {t u v} (code₁ : Code t u) (code₂ : Code u v) (st : Stack t)
exec (code₁ ⊕ code₂) st ≡ exec code₂ (exec code₁ st)
compile-distr cnil cs st = refl
@@ -31,6 +34,8 @@ compile-distr (i ,, is) cs st = begin
where
open ≡-Reasoning
+-- The main correctness theorem: executing compiled code is equivalent
+-- to pushing the correspondent denotation to the stack.
correctness : {u s} (e : Exp u) (st : Stack s) exec (compile e) st ≡ denExp e :: st
correctness (Lit x) _ = refl
correctness (Bin op l r) st = begin
View
@@ -5,9 +5,11 @@ open import Data.Nat
open import TypeUniverse
open import Expression
+-- Denotation of operators.
denOp : {u v w} Op u v w el u el v el w
denOp Plus = _+_
+-- Denotation of expressions.
denExp : {u} Exp u el u
denExp (Lit n) = n
denExp (Bin op l r) = denOp op (denExp l) (denExp r)
View
@@ -9,10 +9,12 @@ open import Denotation
open import Code
open import Compiler
+-- Execute a single instruction.
exec-instr : {s t} Instr s t Stack s Stack t
exec-instr (PUSH x) st = x :: st
exec-instr ADD (x :: y :: st) = (x + y) :: st
+-- Execute a code block above the given stack.
exec : {s t} Code s t Stack s Stack t
exec (i ,, is) = exec is ∘ exec-instr i
exec cnil = id
View
@@ -2,9 +2,11 @@ module Expression where
open import TypeUniverse
+-- The type of (binary) operators.
data Op : U → U → U → Set where
Plus : Op Nat Nat Nat
+-- The type of expressions of the modelled language.
data Exp : U → Set where
Lit : {u} el u Exp u
Bin : {u v w} Op u v w Exp u Exp v Exp w
View
@@ -6,10 +6,12 @@ open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
+-- Types available in the modelled language.
data U : Set where
Nat : U
_⇒_ : U U U
+-- Interpretation of the types into Agda types.
el : U Set
el Nat =
el (x ⇒ y) = el x el y
@@ -21,6 +23,7 @@ private
eq-lemma₂ : {p q r s : U} (p ⇒ q) ≡ (r ⇒ s) q ≡ s
eq-lemma₂ refl = refl
+-- Equality of the types is decidable.
eqDecU : (x y : U) Dec (x ≡ y)
eqDecU Nat Nat = yes refl
eqDecU (p ⇒ q) (r ⇒ s) with eqDecU p r | eqDecU q s

0 comments on commit 824e461

Please sign in to comment.