From deb4378af209ae9d3021bb1f617ecb9fc6dbc161 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 22 Sep 2024 22:02:01 -0700
Subject: [PATCH] Extract values into a separate module

---
 Language/Flat.agda   | 27 ++++++++++-----------------
 Language/Values.agda | 24 ++++++++++++++++++++++++
 2 files changed, 34 insertions(+), 17 deletions(-)
 create mode 100644 Language/Values.agda

diff --git a/Language/Flat.agda b/Language/Flat.agda
index f525dba..d02f4a1 100644
--- a/Language/Flat.agda
+++ b/Language/Flat.agda
@@ -1,6 +1,16 @@
 {-# OPTIONS --guardedness #-}
 module Language.Flat where
 
+open import Language.Values using
+    ( Value; int; bool
+    ; ValueType; tint; tbool
+    ; ⟦_⟧ˢ; ⟦⟧ˢ-empty; ⟦⟧ˢ-int; ⟦⟧ˢ-bool
+    ; s; s'; s''
+    ; st; st'; st''
+    ; b; b₁; b₂
+    ; z; z₁; z₂
+    )
+
 open import Data.Integer using (ℤ; _+_; +_)
 open import Data.Nat using (ℕ; suc; _<_)
 open import Data.Nat.Properties using (m≤n⇒m≤o+n; ≤-trans; +-monoʳ-≤; ≤-refl; n≮n)
@@ -10,10 +20,6 @@ open import Data.Unit using (⊤; tt)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Product using (Σ; _×_; _,_)
 
-data Value : Set where
-    int : ℤ → Value
-    bool : Bool → Value
-
 data Instruction : Set where
     pushint : ℤ → Instruction
     pushbool : Bool → Instruction
@@ -33,10 +39,7 @@ variable
     i : Instruction
     is is' is'' : Program
     S S' S'' : Env
-    s s' s'' : List Value
     n : ℕ
-    b : Bool
-    z z₁ z₂ : ℤ
 
 data _⇒ₓ_ : Program → Program → Set where
     pushint-skip : is ⇒ₓ is' → (pushint z ∷ is) ⇒ₓ is'
@@ -97,9 +100,6 @@ basic₂ = loop-evalⁿ thenᵉ pushbool-eval thenᵉ break-evalᵗ (pushint-ski
 basic₃ : ( [] , (loop 1 ∷ pushbool false ∷ break ∷ pushint (+ 1) ∷ end ∷ []) , [] ) ⇒* ( (int (+ 1) ∷ []) , [] , [] )
 basic₃ = loop-evalⁿ thenᵉ pushbool-eval thenᵉ break-evalᶠ thenᵉ pushint-eval thenᵉ end-eval thenᵉ (loop-eval⁰ (pushbool-skip (break-skip (pushint-skip end-skip)))) thenᵉ doneᵉ
 
-data ValueType : Set where
-    tint tbool : ValueType
-
 -- A stack type describes the current stack and the continuation types
 infix 35 _⟨_⟩
 record StackType : Set where
@@ -109,7 +109,6 @@ record StackType : Set where
         frames : List (List ValueType)
 
 variable
-    st st' st'' : List ValueType
     F F' F'' : List (List ValueType)
     σ σ' σ'' : StackType
 
@@ -185,12 +184,6 @@ lemma₂ (loop-t thenᵗ ist⊢is↦|st'') =
     (_ , loop-skip is''⇒ₓis' is'₁⇒ₓis'₂  , is'₂↦|st'')
 lemma₂ (end-t thenᵗ rest) = (_ , end-skip , rest)
 
--- what it means for list of value types to describe a list of values
-data ⟦_⟧ˢ : List ValueType → List Value → Set where
-    ⟦⟧ˢ-empty : ⟦ [] ⟧ˢ []
-    ⟦⟧ˢ-int : ⟦ st ⟧ˢ s → ⟦ tint ∷ st ⟧ˢ (int z ∷ s)
-    ⟦⟧ˢ-bool : ⟦ st ⟧ˢ s → ⟦ tbool ∷ st ⟧ˢ (bool b ∷ s)
-
 -- Parameterize by final stack type. The reason to do this is that we want
 -- all continuations to end in the same type, so that control flow doesn't change
 -- what final type the program is evaluated to. This is an unfortunate consequence
diff --git a/Language/Values.agda b/Language/Values.agda
new file mode 100644
index 0000000..f02f372
--- /dev/null
+++ b/Language/Values.agda
@@ -0,0 +1,24 @@
+module Language.Values where
+
+open import Data.Integer using (ℤ)
+open import Data.Bool using (Bool)
+open import Data.List using (List; []; _∷_)
+
+data Value : Set where
+    int : ℤ → Value
+    bool : Bool → Value
+
+data ValueType : Set where
+    tint tbool : ValueType
+
+variable
+    s s' s'' : List Value
+    st st' st'' : List ValueType
+    b b₁ b₂ : Bool
+    z z₁ z₂ : ℤ
+
+-- what it means for list of value types to describe a list of values
+data ⟦_⟧ˢ : List ValueType → List Value → Set where
+    ⟦⟧ˢ-empty : ⟦ [] ⟧ˢ []
+    ⟦⟧ˢ-int : ⟦ st ⟧ˢ s → ⟦ tint ∷ st ⟧ˢ (int z ∷ s)
+    ⟦⟧ˢ-bool : ⟦ st ⟧ˢ s → ⟦ tbool ∷ st ⟧ˢ (bool b ∷ s)