{- Computer Aided Formal Reasoning (G53CFR, G54CFR) Thorsten Altenkirch Exercise 7: Evaluation and compilation Deadline: 19/3/10 Use the coursework submission (id: ???) system to submit the coursework after demonstrating it in the lab to me or Darin. Prove the following propositions by completing the sheds { .. }. Note that not all propositions may be provable. If you think that a proposition is unprovable clearly mark this one by adding a line: -- impossible. -} module ex07 where {- This week's exercise is to extend the typed evaluator and compiler we have looked at this week by adding products to it. -} open import Data.Nat open import Data.Bool open import Data.Maybe open import Data.Product hiding (_×_) open import Relation.Nullary open import Relation.Binary.PropositionalEquality {- an untyped language of expressions -} infix 3 _≤E_ infix 4 _+E_ infix 4 _,_ {- We extend Expr by operations for products -} data Expr : Set where nat : ℕ → Expr bool : Bool → Expr _+E_ : Expr → Expr → Expr _≤E_ : Expr → Expr → Expr ifE_then_else_ : Expr → Expr → Expr → Expr _,_ : Expr → Expr → Expr fst : Expr → Expr snd : Expr → Expr {- Examples of expressions: -} e1 : Expr e1 = fst (nat 3 , nat 4) +E nat 7 e2 : Expr -- 3 ≤ 4 + 5 e2 = ifE fst (fst (bool true , nat 3) , nat 4) then nat 0 else nat 1 e3 : Expr -- (3 ≤ 4) + 5 e3 = ifE snd (fst (bool true , nat 3) , nat 4) then nat 0 else nat 1 {- The result of evaluating an expression is a value -} data Val : Set where nat : ℕ → Val bool : Bool → Val _,_ : Val → Val → Val {- implement the evaluator for this language extending the one from the lecture -} ⟦_⟧ : Expr → Maybe Val ⟦ e ⟧ = {!!} {- Evaluation the examples: -} v1 : Maybe Val -- just (nat 10) v1 = ⟦ e1 ⟧ v2 : Maybe Val -- just (nat 0) v2 = ⟦ e2 ⟧ v3 : Maybe Val v3 = ⟦ e3 ⟧ -- nothing {- We do everything again but this time for a typed language. -} infix 6 _×_ {- the types -} data Ty : Set where nat : Ty bool : Ty _×_ : Ty → Ty → Ty {- typed values -} data TVal : Ty → Set where nat : ℕ → TVal nat bool : Bool → TVal bool _,_ : ∀ {σ τ} → TVal σ → TVal τ → TVal (σ × τ) {- Extend the type of typed expressions : -} data TExpr : Ty → Set where nat : ℕ → TExpr nat bool : Bool → TExpr bool _+E_ : TExpr nat → TExpr nat → TExpr nat _≤E_ : TExpr nat → TExpr nat → TExpr bool ifE_then_else_ : {σ : Ty} → TExpr bool → TExpr σ → TExpr σ → TExpr σ -- add extra constructors {- Extend the typed evaluator. -} ⟦_⟧T : {σ : Ty} → TExpr σ → TVal σ ⟦ _ ⟧T = {!!} {- A forgetful map from typed expressions to untyped expressions -} ⌊_⌋ : {σ : Ty} → TExpr σ → Expr ⌊ e ⌋ = {!!} infix 0 _≡Ty?_ {- Show that the extended notion of types is still decidable. This may require some lemmas. -} _≡Ty?_ : (σ τ : Ty) → Dec (σ ≡ τ) σ ≡Ty? σ' = {!!} {- The result of checking an expression e is a record containing: -} record Check (e : Expr) : Set where constructor check field σ : Ty -- a type te : TExpr σ -- a typed expression te≡e : ⌊ te ⌋ ≡ e -- if we forget the types we recover e open Check {- extend the type inference algorithm -} infer : (e : Expr) → Maybe (Check e) infer e = {!!} {- A safe evaluator -} {- We can also forget the types of typed values -} ⌊_⌋v : {σ : Ty} → TVal σ → Val ⌊ v ⌋v = {!!} ⟦_⟧s : Expr → Maybe Val ⟦ e ⟧s = {!!} {- For our examples that safe evaluator produces the same results: -} v1' : Maybe Val v1' = ⟦ e1 ⟧s v2' : Maybe Val v2' = ⟦ e2 ⟧s v3' : Maybe Val v3' = ⟦ e3 ⟧s {- Is this always the case ? -} {- We extend the untyped assembly code -} data Code : Set where push : Val → Code → Code +M : Code → Code ≤M : Code → Code branch : Code → Code → Code stop : Code -- add extra constructors data Stack : Set where ε : Stack _▹_ : Stack → Val → Stack run : Stack → Code → Maybe Stack run s p = {!!} compile : Expr → Code → Code compile e p = {!!} compileRun : Expr → Maybe Val compileRun e = {!!} v1'' : Maybe Val v1'' = compileRun e1 v2'' : Maybe Val v2'' = compileRun e2 v3'' : Maybe Val v3'' = compileRun e3 --- Extend the typed assembly language infixl 4 _▹_ data StackTy : Set where ε : StackTy _▹_ : StackTy → Ty → StackTy data TStack : StackTy → Set where ε : TStack ε _▹_ : ∀ {Γ σ} → TStack Γ → TVal σ → TStack (Γ ▹ σ) 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 Γ Γ -- add extra constructors trun : ∀ {Γ Δ} → TStack Γ → TCode Γ Δ → TStack Δ trun s p = {!!} tcompile : ∀ {Γ Δ σ} → TExpr σ → TCode (Γ ▹ σ) Δ → TCode Γ Δ tcompile e p = {!!} tcompileRun : ∀ {σ} → TExpr σ → TVal σ tcompileRun e = {!!} checkCompileRun : Expr → Maybe Val checkCompileRun e = {!!} v1''' : Maybe Val v1''' = checkCompileRun e1 v2''' : Maybe Val v2''' = checkCompileRun e2 v3''' : Maybe Val v3''' = checkCompileRun e3