Extract values into a separate module

This commit is contained in:
Danila Fedorin 2024-09-22 22:02:01 -07:00
parent d763d7a639
commit deb4378af2
2 changed files with 34 additions and 17 deletions

View File

@ -1,6 +1,16 @@
{-# OPTIONS --guardedness #-} {-# OPTIONS --guardedness #-}
module Language.Flat where 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.Integer using (; _+_; +_)
open import Data.Nat using (; suc; _<_) open import Data.Nat using (; suc; _<_)
open import Data.Nat.Properties using (m≤n⇒m≤o+n; ≤-trans; +-monoʳ-≤; ≤-refl; n≮n) 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.Empty using (⊥; ⊥-elim)
open import Data.Product using (Σ; _×_; _,_) open import Data.Product using (Σ; _×_; _,_)
data Value : Set where
int : Value
bool : Bool Value
data Instruction : Set where data Instruction : Set where
pushint : Instruction pushint : Instruction
pushbool : Bool Instruction pushbool : Bool Instruction
@ -33,10 +39,7 @@ variable
i : Instruction i : Instruction
is is' is'' : Program is is' is'' : Program
S S' S'' : Env S S' S'' : Env
s s' s'' : List Value
n : n :
b : Bool
z z₁ z₂ :
data _⇒ₓ_ : Program Program Set where data _⇒ₓ_ : Program Program Set where
pushint-skip : is ⇒ₓ is' (pushint z is) ⇒ₓ is' 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 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ᵉ 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 -- A stack type describes the current stack and the continuation types
infix 35 _⟨_⟩ infix 35 _⟨_⟩
record StackType : Set where record StackType : Set where
@ -109,7 +109,6 @@ record StackType : Set where
frames : List (List ValueType) frames : List (List ValueType)
variable variable
st st' st'' : List ValueType
F F' F'' : List (List ValueType) F F' F'' : List (List ValueType)
σ σ' σ'' : StackType σ σ' σ'' : StackType
@ -185,12 +184,6 @@ lemma₂ (loop-t thenᵗ ist⊢is↦|st'') =
(_ , loop-skip is''⇒ₓis' is'₁⇒ₓis'₂ , is'₂↦|st'') (_ , loop-skip is''⇒ₓis' is'₁⇒ₓis'₂ , is'₂↦|st'')
lemma₂ (end-t thenᵗ rest) = (_ , end-skip , rest) 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 -- 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 -- 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 -- what final type the program is evaluated to. This is an unfortunate consequence

24
Language/Values.agda Normal file
View File

@ -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)