[lec13] live coding Agda result

Author: andreasabel

README.md

@@ -59,7 +59,7 @@ Material: plt = course book, dragon = Dragon book. Slides follow closely the plt
 | Tue 10/12 | 13-15 | Type inference and polymorphism | plt 7.7-9, [script](notes/typing.html), [visualization tool](https://github.com/teach-plt/visualize-type-inference) |
 | Thu 12/12 **HC1** | 13-14 | Hands-on with Lab 4 (Haskell) | [live code](live/2024/lab4/Interpreter.hs) |
 | Thu 12/12 | 14-15 | Hands-on with Lab 4 (Java)    | [live code](live/2024/lab4/Interpreter.java) |
-| Tue 17/12 | 13-15 | Dependent types (Agda) | live coding [start](live/2024/agda/JVM-start.agda)  |
+| Tue 17/12 | 13-15 | Dependent types (Agda) | live coding [start](live/2024/agda/JVM-start.agda) [stop](live/2024/agda/JVM.agda) |
 | *Wed 18/12* | *23* | *Lab 3 deadline* |  |
 | Thu 19/12 **SB-H5** | 13-15 | Preparing for the exam | |
 

live/2024/agda/JVM.agda

@@ -0,0 +1,272 @@
+-- Programming Language Technology DAT151/DIT231
+-- 2024-12-17 Agda (version ≥2.6.0)
+-- From Dependent Types to Verified Compilation
+
+-- A correct compiler for Hutton's Razor to a stack machine
+
+-- Similar to an early pen-and-paper proof (register machine):
+--
+--   John McCarthy and James Painter, 1967
+--   Correctness of a Compiler for Arithmetic Expressions
+--   http://jmc.stanford.edu/articles/mcpain/mcpain.pdf
+
+open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning
+
+-- Data types and pattern matching
+---------------------------------------------------------------------------
+
+-- Example of a data type.
+
+data List (A : Set) : Set where
+  []  : List A
+  _∷_ : (x : A) (xs : List A) → List A   -- \ : :   A → List A → List A
+
+-- Natural numbers in unary notation.
+
+data Nat : Set where
+  zero : Nat
+  suc : (n : Nat) → Nat
+
+{-# BUILTIN NATURAL Nat #-}
+
+-- NATURAL gives us decimal notation for Nat.
+
+five = suc 4
+
+infixl 10 _+_
+infixr  6 _∷_
+
+-- Addition.
+
+_+_ : (n m : Nat) → Nat
+zero + m = m
+suc n + m = suc (n + m)
+
+{-
+data Empty : Set where
+
+inh : Empty
+inh = error "hoo"
+-}
+
+plus-0 : (n : Nat) → n + zero ≡ n    --  \ = =
+plus-0 zero = refl {x = 0}
+plus-0 (suc n) = cong suc (plus-0 n)
+
+-- Indexed types: Fin, Vec
+---------------------------------------------------------------------------
+
+-- Bounded numbers: Fin n = { m | m < n }.
+
+data Fin : Nat → Set where
+  zero : {n : Nat} → Fin (suc n)
+  suc  : {n : Nat} (i : Fin n) → Fin (suc n)
+
+-- Example with hidden arguments.
+
+three : Fin 5
+three = suc {n = 4} (suc (suc zero))
+
+-- Vectors (length-indexed lists).
+-- Vec : Set → Nat → Set
+
+data Vec (A : Set) : Nat → Set where
+  []  : Vec A zero
+  _∷_ : {n : Nat} (x : A) (xs : Vec A n) → Vec A (suc n)
+
+-- Automatic quantification over hidden arguments.
+
+variable
+  n : Nat
+  A : Set
+
+-- Reading an element of a vector.
+
+lookup : {n : Nat} {A : Set} (i : Fin n) (xs : Vec A n) → A
+lookup zero    (x ∷ xs) = x
+lookup (suc i) (x ∷ xs) = lookup i xs
+
+-- Expressions and interpretation: "Hutton's razor"
+---------------------------------------------------------------------------
+
+-- We have a single type of (natural) numbers.
+
+Num = Nat
+
+-- Expressions over n variables.
+
+-- A variable is denoted by its number x < n.
+
+data Exp (n : Nat) : Set where
+  var  : (x : Fin n)    → Exp n
+  num  : (w : Num)      → Exp n
+  plus : (e e' : Exp n) → Exp n
+
+-- (x + 3) + y
+ex1 : Exp 2
+ex1 = plus (plus (var zero) (num 3)) (var (suc zero))
+
+-- An environment maps each variable to its value.
+
+Value = Num
+Env   = Vec Num
+
+-- Interpretation of expressions.
+
+eval : (e : Exp n) (γ : Env n) → Value
+eval (var x) γ = lookup x γ
+eval (num w) γ = w
+eval (plus e e₁) γ = eval e γ + eval e₁ γ
+
+v1 = eval ex1 (15 ∷ 1 ∷ [])
+
+-- A fragment of JVM
+---------------------------------------------------------------------------
+
+StackSize = Nat  -- Current stack size
+StoreSize = Nat  -- Local variable store limit
+Addr = Fin       -- Local variable address
+Word = Nat       -- Word (should be 32bit signed int, but we use Nat here)
+
+-- JVM instructions.
+--
+-- n  = number of local variables
+-- m  = stack size before instruction
+-- m' = stack size after instruction
+
+variable
+  k l m m' : StackSize
+
+data Ins (n : StoreSize) : (m m' : StackSize) → Set where
+  load  : (a : Addr n) → Ins n m       (1 + m)  -- Load variable onto stack.
+  add   :                Ins n (2 + m) (1 + m)  -- Add top stack elements.
+  ldc   : (w : Word)   → Ins n m       (1 + m)  -- Load constant onto stack.
+  pop   :                Ins n (1 + m) m        -- Remove top stack element.
+
+-- Instruction sequences.
+-- Note that for instruction concatenation, the index "l" has to match.
+
+data Inss (n : StoreSize) (m : StackSize) : (m' : StackSize) → Set where
+  []  : Inss n m m
+  ins : Ins n m l → Inss n m l
+  _∙_ : (i : Inss n m l) (is : Inss n l k) → Inss n m k
+
+infixr 10 _∙_
+
+-- Compilation of expressions
+---------------------------------------------------------------------------
+
+-- The code for an expression leaves one additional value on the stack.
+
+compile : (e : Exp n) → Inss n m (suc m)
+compile (var x)     = ins (load x)
+compile (num w)     = ins (ldc w)
+compile (plus e e') = compile e ∙ compile e' ∙ ins add
+
+ss1 : Inss 2 0 1
+ss1 = compile ex1
+
+-- JVM small-step semantics
+---------------------------------------------------------------------------
+
+-- JVM machine state (simplified).
+
+Store = Env
+Stack = Vec Word
+
+record State (n : StoreSize) (m : StackSize) : Set where
+  constructor state
+  field
+    V  : Store n
+    S  : Stack m
+open State
+
+-- Executing a JVM instruction.
+
+step : (i : Ins n m m') (s : State n m) → State n m'
+step (load a) (state V S)           = state V (lookup a V ∷ S)
+step add      (state V (v ∷ w ∷ S)) = state V (w + v ∷ S)
+step (ldc w)  (state V S)           = state V (w ∷ S)
+step pop      (state V (_ ∷ S))     = state V S
+
+-- Compiler correctness
+---------------------------------------------------------------------------
+
+-- Executing a series of JVM instructions.
+
+steps : (is : Inss n m m') (s : State n m) → State n m'
+steps (ins i)    s = step i s
+steps []         s = s
+steps (is ∙ is') s = steps is' (steps is s)
+
+r1 = steps ss1 (state (15 ∷ 1 ∷ []) [])
+
+-- Pushing a word onto the stack.
+
+push : Word → State n m → State n (suc m)
+push w (state V S) = state V (w ∷ S)
+
+push-eval : (e : Exp n) (s : State n m) → State n (suc m)
+push-eval e (state V S) = state V (eval e V ∷ S)
+
+
+-- Compiler correctness theorem.
+
+-- Running the instructions for an expression e
+-- leaves the value of e on top of the stack.
+
+sound : (e : Exp n) (s : State n m) →
+
+  steps (compile e) s ≡ push-eval e s
+
+-- Case: variables
+sound (var x)     s = refl
+
+-- Case: number literals.
+sound (num w)     s = refl
+
+-- Case: addition expression.
+sound (plus e e') s = begin
+  steps (compile (plus e e')) s                       ≡⟨ refl ⟩
+  steps (compile e ∙ compile e' ∙ ins add) s          ≡⟨ refl ⟩
+  steps (compile e' ∙ ins add) (steps (compile e) s)  ≡⟨ cong (steps _) (sound e s) ⟩
+  steps (compile e' ∙ ins add) s'                     ≡⟨ refl  ⟩
+  steps (ins add) (steps (compile e') s')             ≡⟨ cong (steps _) (sound e' s) ⟩
+  steps (ins add) (push-eval e' s')                   ≡⟨ {!   !} ⟩
+  push-eval (plus e e') s
+  ∎
+  where s' = push-eval e s
+
+-- steps (compile (plus e e') s)
+--   = steps (compile e ∙ compile e' ∙ ins add) s
+--   = steps (compile e' ∙ ins add) (steps (compile e) s)  -- by ind.hyp.
+--   = steps (compile e' ∙ ins add) (push-eval e s)
+--   = steps (ins add) (steps (compile e') (push-eval e s))
+--   = steps (ins add) (push-eval e' (push-eval e s))
+--   = step add (push-eval e' (push-eval e s))
+--   = step add (push-eval e' (push-eval e (state V S)))   -- s =: state V S
+--   = step add (push-eval e' (state V (eval e V ∷ S)))
+--   = step add (state V (eval e' V ∷ eval e V ∷ S))
+--   = state V ((eval e V + eval e' V) ∷ S)
+--   = state V (eval (plus e e') V ∷ S)
+--   = push-eval (plus e e') (state V S)
+--   = push-eval (plus e e') s
+
+-- -}
+-- -}
+-- -}
+-- -}
+-- -}
+-- -}
+-- -}
+-- -}
+-- -}
+-- -}
+-- -}
+-- -}
+-- -}
+-- -}
+-- -}
+-- -}
+-- -}