Lecture on Agda 2025: live coding finish

Author: andreasabel

live/2025/agda/JVM.agda

@@ -20,7 +20,9 @@ open ≡-Reasoning
 
 data List (A : Set) : Set where
   []  : List A
-  _∷_ : (x : A) (xs : List A) → List A
+  _∷_ : (x : A) (xs : List A) → List A   -- \ : :
+
+{-# BUILTIN LIST List #-}
 
 -- Natural numbers in unary notation.
 
@@ -40,50 +42,49 @@ infixr  6 _∷_
 -- Addition.
 
 _+_ : (n m : Nat) → Nat
-n + m = {!!}
+zero + m = m
+suc n + m = suc (n + m)
 
-{-
 plus-0 : ∀(n : Nat) → n + 0 ≡ n
-plus-0 n = {!!}
+plus-0 zero = refl
+plus-0 (suc n) = cong suc (plus-0 n)
 
 -- Indexed types: Fin, Vec
 ---------------------------------------------------------------------------
 
-{-
--- Bounded numbers: Fin n = { m | n < m }.
+-- 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 = ?
+three = 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)
 
+v3 : Vec Nat 3
+v3 = 4 ∷ 2 ∷ 1 ∷ []
+
 -- Reading an element of a vector.
 
 lookup : ∀{n A} (i : Fin n) (xs : Vec A n) → A
-lookup i xs = {!!}
-
-{-
+lookup zero    (x ∷ xs) = x
+lookup (suc i) (x ∷ xs) = lookup i xs
 
 -- Automatic quantification over hidden arguments.
 
 variable
   n : Nat
   A : Set
 
-{-
 -- Expressions and interpretation: "Hutton's razor"
 ---------------------------------------------------------------------------
 
@@ -105,13 +106,13 @@ data Exp (n : Nat) : Set where
 Value = Num
 Env   = Vec Num
 
-{-
 -- Interpretation of expressions.
 
 eval : (e : Exp n) (γ : Env n) → Value
-eval e γ = ?
+eval (var x)     γ = lookup x γ
+eval (num w)     γ = w
+eval (plus e e₁) γ = eval e γ + eval e₁ γ
 
-{-
 -- A fragment of JVM
 ---------------------------------------------------------------------------
 
@@ -145,18 +146,16 @@ data Inss (n : StoreSize) (m : StackSize) : (m' : StackSize) → Set where
 
 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)     = ?
-compile (num w)     = ?
-compile (plus e e') = ?
+compile (var x)     = ins (load x)
+compile (num w)     = ins (ldc w)
+compile (plus e e') = compile e ∙ compile e' ∙ ins add
 
-{-
 -- JVM small-step semantics
 ---------------------------------------------------------------------------
 
@@ -172,25 +171,24 @@ record State (n : StoreSize) (m : StackSize) : Set where
     S  : Stack m
 open State
 
-{-
 -- Executing a JVM instruction.
 
 step : (i : Ins n m m') (s : State n m) → State n m'
-step i s = {!!}
-
-{-
+step (load a) (state V S)           = state V (lookup a V ∷ S)
+step add      (state V (a ∷ b ∷ S)) = state V ((b + a) ∷ 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 = {!!}
-steps []         s = {!!}
-steps (is ∙ is') s = {!!}
+steps (ins i)    s = step i s
+steps []         s = s
+steps (is ∙ is') s = steps is' (steps is s)
 
-{-
 -- Pushing a word onto the stack.
 
 push : Word → State n m → State n (suc m)
@@ -210,20 +208,34 @@ sound : (e : Exp n) (s : State n m) →
   steps (compile e) s ≡ push-eval e s
 
 -- Case: variables
-sound (var x)     s = {!!}
+sound (var x)     s = refl
 
 -- Case: number literals.
-sound (num w)     s = {!!}
+sound (num w)     s = refl
 
 -- Case: addition expression.
-sound (plus e e') s = begin
-  steps (compile (plus e e')) s               ≡⟨ {!!} ⟩
-  push-eval (plus e e') s
+sound (plus e e') s@(state V 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 (compile e' ∙ ins add)) (sound e s) ⟩
+   steps (compile e' ∙ ins add) (push-eval e s)         ≡⟨ refl ⟩
+   steps (ins add) (steps (compile e') (push-eval e s)) ≡⟨ cong (steps (ins add)) (sound e' (push-eval e s)) ⟩
+   steps (ins add) (push-eval e' (push-eval e s))       ≡⟨ refl ⟩
+   step add (push-eval e' (push-eval e s))              ≡⟨ refl ⟩
+   step add (push-eval e' (push-eval e (state V S)))    ≡⟨ refl ⟩
+   step add (push-eval e' (state V (eval e V ∷ S)))     ≡⟨ refl ⟩
+   step add (state V (eval e' V ∷ eval e V ∷ S))        ≡⟨ refl ⟩
+   state V ((eval e V + eval e' V) ∷ S)                 ≡⟨ refl ⟩
+   state V (eval (plus e e') V ∷ S)                     ≡⟨ refl ⟩
+   push-eval (plus e e') (state V S)                    ≡⟨ refl ⟩
+   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 (plus e e') 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))