Compare commits
No commits in common. "next" and "main" have entirely different histories.
|
@ -1,15 +1,5 @@
|
|||
{-# 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₂
|
||||
)
|
||||
module Lang where
|
||||
|
||||
open import Data.Integer using (ℤ; _+_; +_)
|
||||
open import Data.Nat using (ℕ; suc; _<_)
|
||||
|
@ -20,6 +10,10 @@ 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
|
||||
|
@ -39,7 +33,10 @@ 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'
|
||||
|
@ -100,6 +97,9 @@ 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,6 +109,7 @@ record StackType : Set where
|
|||
frames : List (List ValueType)
|
||||
|
||||
variable
|
||||
st st' st'' : List ValueType
|
||||
F F' F'' : List (List ValueType)
|
||||
σ σ' σ'' : StackType
|
||||
|
||||
|
@ -145,9 +146,6 @@ _⊢_↦|_ σ is st = σ ⊢ is ↦* st ⟨ [] ⟩
|
|||
basict₁ : [] ⟨ [] ⟩ ⊢ (pushint (+ 1) ∷ pushint (+ 2) ∷ pushint (+ 3) ∷ add ∷ add ∷ []) ↦* (tint ∷ []) ⟨ [] ⟩
|
||||
basict₁ = pushint-t thenᵗ pushint-t thenᵗ pushint-t thenᵗ add-t thenᵗ add-t thenᵗ doneᵗ
|
||||
|
||||
basict₄ : [] ⟨ [] ⟩ ⊢ (pushint (+ 1) ∷ loop 3 ∷ pushint (+ 2) ∷ add ∷ end ∷ []) ↦* (tint ∷ []) ⟨ [] ⟩
|
||||
basict₄ = pushint-t thenᵗ loop-t thenᵗ pushint-t thenᵗ add-t thenᵗ end-t thenᵗ doneᵗ
|
||||
|
||||
-- doesn't typecheck: violates type discipline because on break, stack has different type than on end.
|
||||
--
|
||||
-- basict₂ : ([] ⟨ [] ⟩) ⊢ (loop 1 ∷ pushbool true ∷ break ∷ pushint (+ 1) ∷ end ∷ []) ↦* ([] ⟨ [] ⟩)
|
||||
|
@ -187,6 +185,12 @@ 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
|
||||
|
@ -273,4 +277,4 @@ stackToString (bool b ∷ s) = showBool b ++ " :: " ++ stackToString s
|
|||
open import IO
|
||||
open import Level using (0ℓ)
|
||||
|
||||
main = run {0ℓ} (putStrLn (stackToString (proj₁ (static-dynamic _ (⟦⟧ˢ-empty , ⟦⟧ᶠ-empty , basict₄)))))
|
||||
main = run {0ℓ} (putStrLn (stackToString (proj₁ (static-dynamic _ (⟦⟧ˢ-empty , ⟦⟧ᶠ-empty , basict₁)))))
|
|
@ -1,154 +0,0 @@
|
|||
{-# OPTIONS --guardedness #-}
|
||||
module Language.Equivalence where
|
||||
|
||||
open import Language.Nested using () renaming
|
||||
( Instruction to Instructionᵃ; Program to Programᵃ; Env to Envᵃ
|
||||
; pushint to pushintᵃ; pushbool to pushboolᵃ; add to addᵃ
|
||||
; loop to loopᵃ; break to breakᵃ
|
||||
; Triple to Tripleᵃ
|
||||
; _⇒_ to _⇒ᵃ_; _⇒*_ to _⇒*ᵃ_
|
||||
; pushint-eval to pushint-evalᵃ; pushbool-eval to pushbool-evalᵃ; add-eval to add-evalᵃ
|
||||
; break-evalᵗ to break-evalᵗᵃ; break-evalᶠ to break-evalᶠᵃ; empty-eval to empty-evalᵃ
|
||||
; loop-eval⁰ to loop-eval⁰ᵃ; loop-evalⁿ to loop-evalⁿᵃ
|
||||
; doneᵉ to doneᵉᵃ; _thenᵉ_ to _thenᵉᵃ_
|
||||
)
|
||||
open import Language.Flat
|
||||
using
|
||||
(_⇒ₓ_; pushint-skip; pushbool-skip; add-skip; break-skip; loop-skip; end-skip
|
||||
)
|
||||
renaming
|
||||
( Instruction to Instructionᵇ; Program to Programᵇ; Env to Envᵇ
|
||||
; pushint to pushintᵇ; pushbool to pushboolᵇ; add to addᵇ
|
||||
; loop to loopᵇ; break to breakᵇ; end to endᵇ
|
||||
; Triple to Tripleᵇ
|
||||
; _⇒_ to _⇒ᵇ_; _⇒*_ to _⇒*ᵇ_
|
||||
; pushint-eval to pushint-evalᵇ; pushbool-eval to pushbool-evalᵇ; add-eval to add-evalᵇ
|
||||
; break-evalᵗ to break-evalᵗᵇ; break-evalᶠ to break-evalᶠᵇ; end-eval to end-evalᵇ
|
||||
; loop-eval⁰ to loop-eval⁰ᵇ; loop-evalⁿ to loop-evalⁿᵇ
|
||||
; doneᵉ to doneᵉᵇ; _thenᵉ_ to _thenᵉᵇ_
|
||||
)
|
||||
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.List using (List; _∷_; []; length; foldr; _++_)
|
||||
open import Data.List.Properties using (++-assoc)
|
||||
open import Data.Product using (Σ; _×_; _,_)
|
||||
open import Data.Nat using (ℕ)
|
||||
open import Data.Unit using (⊤; tt)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
|
||||
|
||||
variable
|
||||
n n' : ℕ
|
||||
|
||||
iᵃ : Instructionᵃ
|
||||
isᵃ isᵃ' isᵃ'' : Programᵃ
|
||||
Sᵃ Sᵃ' Sᵃ'' : Envᵃ
|
||||
|
||||
iᵇ : Instructionᵇ
|
||||
isᵇ isᵇ' isᵇ'' : Programᵇ
|
||||
Sᵇ Sᵇ' Sᵇ'' : Envᵇ
|
||||
|
||||
|
||||
interleaved mutual
|
||||
⟦_⟧ⁱ : Instructionᵃ → List Instructionᵇ
|
||||
⟦_⟧ⁱˢ : List Instructionᵃ → List Instructionᵇ
|
||||
|
||||
⟦ pushintᵃ z ⟧ⁱ = pushintᵇ z ∷ []
|
||||
⟦ pushboolᵃ b ⟧ⁱ = pushboolᵇ b ∷ []
|
||||
⟦ addᵃ ⟧ⁱ = addᵇ ∷ []
|
||||
⟦ loopᵃ n is ⟧ⁱ = loopᵇ n ∷ (⟦ is ⟧ⁱˢ ++ endᵇ ∷ [])
|
||||
⟦ breakᵃ ⟧ⁱ = breakᵇ ∷ []
|
||||
|
||||
⟦ [] ⟧ⁱˢ = []
|
||||
⟦ i ∷ is ⟧ⁱˢ = ⟦ i ⟧ⁱ ++ ⟦ is ⟧ⁱˢ
|
||||
|
||||
-- Translation always leaves well-balanced programs
|
||||
interleaved mutual
|
||||
lemma₁ : isᵇ ⇒ₓ isᵇ' → (⟦ iᵃ ⟧ⁱ ++ isᵇ) ⇒ₓ isᵇ'
|
||||
lemma₁' : isᵇ ⇒ₓ isᵇ' → (⟦ isᵃ ⟧ⁱˢ ++ isᵇ) ⇒ₓ isᵇ'
|
||||
lemma₂ : (⟦ isᵃ ⟧ⁱˢ ++ endᵇ ∷ isᵇ) ⇒ₓ isᵇ
|
||||
|
||||
lemma₁ {iᵃ = pushintᵃ z} = pushint-skip
|
||||
lemma₁ {iᵃ = pushboolᵃ z} = pushbool-skip
|
||||
lemma₁ {iᵃ = addᵃ} = add-skip
|
||||
lemma₁ {iᵃ = breakᵃ} = break-skip
|
||||
lemma₁ {isᵇ = isᵇ} {iᵃ = loopᵃ n is}
|
||||
rewrite ++-assoc ⟦ is ⟧ⁱˢ (endᵇ ∷ []) isᵇ =
|
||||
loop-skip (lemma₂ {isᵃ = is} {isᵇ = isᵇ})
|
||||
|
||||
lemma₁' {isᵃ = []} isᵇ⇒ₓisᵇ' = isᵇ⇒ₓisᵇ'
|
||||
lemma₁' {isᵇ = isᵇ} {isᵃ = iᵃ ∷ isᵃ} isᵇ⇒ₓisᵇ'
|
||||
rewrite ++-assoc ⟦ iᵃ ⟧ⁱ ⟦ isᵃ ⟧ⁱˢ isᵇ =
|
||||
lemma₁ {iᵃ = iᵃ} (lemma₁' {isᵃ = isᵃ} isᵇ⇒ₓisᵇ')
|
||||
|
||||
lemma₂ {isᵃ = isᵃ} = lemma₁' {isᵃ = isᵃ} end-skip
|
||||
|
||||
-- In flat semantics, we drop the top continuation and seek forward until we find
|
||||
-- an 'end'. In nested semantics, we drop the current instructions and use the
|
||||
-- bit of the top continuation after the 'while'. We need to be able to reconcile
|
||||
-- the two.
|
||||
data ⟦_⟧ᵀ=_ : Programᵃ × Envᵃ → Programᵇ × Envᵇ → Set where
|
||||
⟦⟧ᵀ-empty : ⟦ isᵃ , [] ⟧ᵀ= (⟦ isᵃ ⟧ⁱˢ , [])
|
||||
⟦⟧ᵀ-step : ⟦ isᵃ'' , Sᵃ ⟧ᵀ= (isᵇ , Sᵇ) →
|
||||
⟦ isᵃ , ((loopᵃ n isᵃ' ∷ isᵃ'') ∷ Sᵃ) ⟧ᵀ= ((⟦ isᵃ ⟧ⁱˢ ++ endᵇ ∷ []) ++ isᵇ , (⟦ loopᵃ n isᵃ' ⟧ⁱ ++ isᵇ) ∷ Sᵇ)
|
||||
|
||||
|
||||
step-equivalence : (s , isᵃ , Sᵃ) ⇒ᵃ (s' , isᵃ' , Sᵃ') →
|
||||
⟦ isᵃ , Sᵃ ⟧ᵀ= (isᵇ , Sᵇ) →
|
||||
Σ (Programᵇ × Envᵇ) (λ { (isᵇ' , Sᵇ') → (s , isᵇ , Sᵇ) ⇒ᵇ (s' , isᵇ' , Sᵇ') ×
|
||||
⟦ isᵃ' , Sᵃ' ⟧ᵀ= (isᵇ' , Sᵇ') })
|
||||
step-equivalence pushint-evalᵃ ⟦⟧ᵀ-empty = ((_ , _) , pushint-evalᵇ , ⟦⟧ᵀ-empty)
|
||||
step-equivalence pushint-evalᵃ (⟦⟧ᵀ-step next) = ((_ , _) , pushint-evalᵇ , ⟦⟧ᵀ-step next)
|
||||
step-equivalence pushbool-evalᵃ ⟦⟧ᵀ-empty = ((_ , _) , pushbool-evalᵇ , ⟦⟧ᵀ-empty)
|
||||
step-equivalence pushbool-evalᵃ (⟦⟧ᵀ-step next) = ((_ , _) , pushbool-evalᵇ , ⟦⟧ᵀ-step next)
|
||||
step-equivalence add-evalᵃ ⟦⟧ᵀ-empty = ((_ , _) , add-evalᵇ , ⟦⟧ᵀ-empty)
|
||||
step-equivalence add-evalᵃ (⟦⟧ᵀ-step next) = ((_ , _) , add-evalᵇ , ⟦⟧ᵀ-step next)
|
||||
step-equivalence {isᵃ = loopᵃ n isˡ ∷ isᵃ} loop-eval⁰ᵃ ⟦⟧ᵀ-empty
|
||||
rewrite ++-assoc ⟦ isˡ ⟧ⁱˢ (endᵇ ∷ []) ⟦ isᵃ ⟧ⁱˢ
|
||||
= ((_ , _) , loop-eval⁰ᵇ (lemma₁' {isᵃ = isˡ} end-skip) , ⟦⟧ᵀ-empty)
|
||||
step-equivalence {isᵃ = loopᵃ n isˡ ∷ isᵃ} loop-eval⁰ᵃ (⟦⟧ᵀ-step {isᵇ = isᵇ} rec)
|
||||
rewrite ++-assoc ⟦ isˡ ⟧ⁱˢ (endᵇ ∷ []) ⟦ isᵃ ⟧ⁱˢ
|
||||
rewrite ++-assoc ⟦ isˡ ⟧ⁱˢ (endᵇ ∷ ⟦ isᵃ ⟧ⁱˢ) (endᵇ ∷ [])
|
||||
rewrite ++-assoc ⟦ isˡ ⟧ⁱˢ (endᵇ ∷ ⟦ isᵃ ⟧ⁱˢ ++ endᵇ ∷ []) isᵇ
|
||||
= ((_ , _) , loop-eval⁰ᵇ (lemma₁' {isᵃ = isˡ} end-skip) , (⟦⟧ᵀ-step rec))
|
||||
step-equivalence {isᵃ = loopᵃ n isˡ ∷ isᵃ} loop-evalⁿᵃ ⟦⟧ᵀ-empty
|
||||
= ((_ , _) , loop-evalⁿᵇ , ⟦⟧ᵀ-step ⟦⟧ᵀ-empty)
|
||||
step-equivalence {isᵃ = loopᵃ n isˡ ∷ isᵃ} loop-evalⁿᵃ (⟦⟧ᵀ-step {isᵇ = isᵇ} rec)
|
||||
rewrite ++-assoc (⟦ isˡ ⟧ⁱˢ ++ endᵇ ∷ []) ⟦ isᵃ ⟧ⁱˢ (endᵇ ∷ [])
|
||||
rewrite ++-assoc ⟦ isˡ ⟧ⁱˢ (endᵇ ∷ []) (⟦ isᵃ ⟧ⁱˢ ++ endᵇ ∷ [])
|
||||
rewrite sym (++-assoc ⟦ isˡ ⟧ⁱˢ (endᵇ ∷ []) (⟦ isᵃ ⟧ⁱˢ ++ endᵇ ∷ []))
|
||||
rewrite ++-assoc (⟦ isˡ ⟧ⁱˢ ++ endᵇ ∷ []) (⟦ isᵃ ⟧ⁱˢ ++ endᵇ ∷ []) isᵇ
|
||||
= (_ , loop-evalⁿᵇ , ⟦⟧ᵀ-step (⟦⟧ᵀ-step rec))
|
||||
step-equivalence break-evalᶠᵃ (⟦⟧ᵀ-step next) = ((_ , _) , break-evalᶠᵇ , ⟦⟧ᵀ-step next)
|
||||
step-equivalence {isᵃ = breakᵃ ∷ isᵃ} {Sᵃ = (loopᵃ n isˡ ∷ isᵃ') ∷ Sᵃ} break-evalᵗᵃ (⟦⟧ᵀ-step {isᵇ = isᵇ} next)
|
||||
rewrite ++-assoc ⟦ isᵃ ⟧ⁱˢ (endᵇ ∷ []) isᵇ
|
||||
= ((_ , _) , break-evalᵗᵇ (lemma₁' {isᵃ = isᵃ} end-skip) , next)
|
||||
step-equivalence empty-evalᵃ (⟦⟧ᵀ-step ⟦⟧ᵀ-empty)
|
||||
= ((_ , _) , end-evalᵇ , ⟦⟧ᵀ-empty)
|
||||
step-equivalence {Sᵃ = (loopᵃ n isˡ ∷ isᵃ') ∷ Sᵃ} empty-evalᵃ (⟦⟧ᵀ-step (⟦⟧ᵀ-step {isᵇ = isᵇ} next))
|
||||
rewrite sym (++-assoc (loopᵇ n ∷ ⟦ isˡ ⟧ⁱˢ ++ endᵇ ∷ []) (⟦ isᵃ' ⟧ⁱˢ ++ endᵇ ∷ []) isᵇ)
|
||||
rewrite sym (++-assoc (⟦ isˡ ⟧ⁱˢ ++ endᵇ ∷ []) (⟦ isᵃ' ⟧ⁱˢ) (endᵇ ∷ []))
|
||||
= ((_ , _) , end-evalᵇ , ⟦⟧ᵀ-step next)
|
||||
|
||||
equivalence : (s , isᵃ , Sᵃ) ⇒*ᵃ (s' , isᵃ' , Sᵃ') →
|
||||
⟦ isᵃ , Sᵃ ⟧ᵀ= (isᵇ , Sᵇ) →
|
||||
Σ (Programᵇ × Envᵇ) (λ { (isᵇ' , Sᵇ') → (s , isᵇ , Sᵇ) ⇒*ᵇ (s' , isᵇ' , Sᵇ') ×
|
||||
⟦ isᵃ' , Sᵃ' ⟧ᵀ= (isᵇ' , Sᵇ') })
|
||||
equivalence doneᵉᵃ trans@(⟦⟧ᵀ-empty) = (_ , (doneᵉᵇ , trans))
|
||||
equivalence (isᵃ⇒isᵃ' thenᵉᵃ rest) trans =
|
||||
let (_ , isᵇ⇒isᵇ' , trans') = step-equivalence isᵃ⇒isᵃ' trans in
|
||||
let (_ , isᵇ'⇒*isᵇ'' , trans'') = equivalence rest trans' in
|
||||
(_ , isᵇ⇒isᵇ' thenᵉᵇ isᵇ'⇒*isᵇ'' , trans'')
|
||||
|
||||
equivalence' : (s , isᵃ , []) ⇒*ᵃ (s' , [] , []) →
|
||||
(s , ⟦ isᵃ ⟧ⁱˢ , []) ⇒*ᵇ (s' , [] , [])
|
||||
equivalence' eval with
|
||||
(_ , isᵃ⇒| , ⟦⟧ᵀ-empty) ← equivalence eval ⟦⟧ᵀ-empty = isᵃ⇒|
|
|
@ -1,189 +0,0 @@
|
|||
{-# OPTIONS --guardedness #-}
|
||||
module Language.Nested 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.Bool using (Bool; true; false)
|
||||
open import Data.List using (List; _∷_; []; length)
|
||||
open import Data.Unit using (⊤; tt)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.Product using (Σ; _×_; _,_)
|
||||
open import Data.Maybe using (Maybe; just; nothing)
|
||||
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||||
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
|
||||
|
||||
data Instruction : Set where
|
||||
pushint : ℤ → Instruction
|
||||
pushbool : Bool → Instruction
|
||||
add : Instruction
|
||||
|
||||
loop : ℕ → List Instruction → Instruction
|
||||
break : Instruction
|
||||
|
||||
Program : Set
|
||||
Program = List Instruction
|
||||
|
||||
Env : Set
|
||||
Env = List (List Instruction)
|
||||
|
||||
variable
|
||||
i : Instruction
|
||||
is is' is'' : Program
|
||||
S S' S'' : Env
|
||||
n : ℕ
|
||||
|
||||
Triple : Set
|
||||
Triple = List Value × Program × Env
|
||||
|
||||
data _⇒_ : Triple → Triple → Set where
|
||||
pushint-eval : ( s , (pushint z ∷ is) , S ) ⇒ ( ((int z) ∷ s) , is , S )
|
||||
pushbool-eval : ( s , (pushbool b ∷ is) , S ) ⇒ ( ((bool b) ∷ s) , is , S )
|
||||
add-eval : ( (int z₁ ∷ int z₂ ∷ s) , (add ∷ is), S ) ⇒ ( ((int (z₁ + z₂)) ∷ s) , is , S )
|
||||
|
||||
loop-eval⁰ : (s , loop 0 is' ∷ is , S) ⇒ (s , is , S)
|
||||
loop-evalⁿ : (s , loop (suc n) is' ∷ is , S) ⇒ (s , is' , (loop n is' ∷ is) ∷ S)
|
||||
break-evalᶠ : (bool false ∷ s , break ∷ is , is' ∷ S) ⇒ (s , is , is' ∷ S)
|
||||
break-evalᵗ : (bool true ∷ s , break ∷ is , (loop n is'' ∷ is') ∷ S) ⇒ (s , is' , S)
|
||||
|
||||
empty-eval : (s , [] , is' ∷ S) ⇒ (s , is' , S)
|
||||
|
||||
infixr 30 _thenᵉ_
|
||||
data _⇒*_ : Triple → Triple → Set where
|
||||
doneᵉ : ( s , [] , [] ) ⇒* ( s , [] , [] )
|
||||
_thenᵉ_ : ( s , is , S ) ⇒ ( s' , is' , S' ) →
|
||||
( s' , is' , S' ) ⇒* ( s'' , is'' , S'' ) →
|
||||
( s , is , S ) ⇒* ( s'' , is'' , S'' )
|
||||
|
||||
StackType : Set
|
||||
StackType = List ValueType
|
||||
|
||||
variable
|
||||
F F' F'' : List (List ValueType)
|
||||
σ σ' σ'' : StackType
|
||||
mst : Maybe StackType
|
||||
|
||||
interleaved mutual
|
||||
data _⊢⟨_⟩_↦_ : StackType → Maybe StackType → Instruction → StackType → Set
|
||||
data _⊢⟨_⟩_↦*_ : StackType → Maybe StackType → Program → StackType → Set
|
||||
|
||||
data _⊢⟨_⟩_↦_ where
|
||||
pushint-t : st ⊢⟨ mst ⟩ (pushint z) ↦ (tint ∷ st)
|
||||
pushbool-t : st ⊢⟨ mst ⟩ (pushbool b) ↦ (tbool ∷ st)
|
||||
add-t : (tint ∷ tint ∷ st) ⊢⟨ mst ⟩ add ↦ (tint ∷ st)
|
||||
|
||||
loop-t : st ⊢⟨ just st ⟩ is ↦* st →
|
||||
st ⊢⟨ mst ⟩ loop n is ↦ st
|
||||
break-t : (tbool ∷ st) ⊢⟨ just st ⟩ break ↦ st
|
||||
|
||||
infixr 30 _thenᵗ_
|
||||
data _⊢⟨_⟩_↦*_ where
|
||||
doneᵗ-just : st ⊢⟨ just st ⟩ [] ↦* st
|
||||
doneᵗ-nothing : st ⊢⟨ nothing ⟩ [] ↦* st
|
||||
_thenᵗ_ : st ⊢⟨ mst ⟩ i ↦ st' →
|
||||
st' ⊢⟨ mst ⟩ is ↦* st'' →
|
||||
st ⊢⟨ mst ⟩ (i ∷ is) ↦* st''
|
||||
|
||||
_⊢_↦|_ : StackType → Program → StackType → Set
|
||||
_⊢_↦|_ st is st' = st ⊢⟨ nothing ⟩ is ↦* st'
|
||||
|
||||
basict₄ : [] ⊢ (pushint (+ 1) ∷ loop 3 (pushint (+ 2) ∷ add ∷ []) ∷ pushint (+ 1) ∷ add ∷ []) ↦| (tint ∷ [])
|
||||
basict₄ = pushint-t thenᵗ loop-t (pushint-t thenᵗ add-t thenᵗ doneᵗ-just) thenᵗ pushint-t thenᵗ add-t thenᵗ doneᵗ-nothing
|
||||
|
||||
data _⊢_↦*_ : StackType → (Program × Env) → StackType → Set where
|
||||
program-typed-flat : st ⊢⟨ nothing ⟩ is ↦* st' →
|
||||
st ⊢ (is , []) ↦* st'
|
||||
program-typed-rec : ∀ {stˡ} →
|
||||
st ⊢⟨ just st' ⟩ is ↦* st' →
|
||||
st' ⊢ (loop n is'' ∷ is' , S) ↦* stˡ →
|
||||
st ⊢ (is , (loop n is'' ∷ is') ∷ S) ↦* stˡ
|
||||
|
||||
skip-loop-continuation : st ⊢ (loop n is ∷ is' , S) ↦* st' →
|
||||
st ⊢ (is' , S) ↦* st'
|
||||
skip-loop-continuation (program-typed-flat (loop-t _ thenᵗ rest)) = (program-typed-flat rest)
|
||||
skip-loop-continuation (program-typed-rec (loop-t _ thenᵗ rest) frames) = (program-typed-rec rest frames)
|
||||
|
||||
preservation : ∀ {stˡ} →
|
||||
(s , is , S) ⇒ (s' , is' , S') →
|
||||
⟦ st ⟧ˢ s →
|
||||
st ⊢ (is , S) ↦* stˡ →
|
||||
Σ StackType (λ st' → ⟦ st' ⟧ˢ s' × st' ⊢ (is' , S') ↦* stˡ)
|
||||
preservation pushint-eval ⟦st⟧ (program-typed-flat (pushint-t thenᵗ rest)) = (_ , ⟦⟧ˢ-int ⟦st⟧ , (program-typed-flat rest))
|
||||
preservation pushint-eval ⟦st⟧ (program-typed-rec (pushint-t thenᵗ rest) frames) = (_ , ⟦⟧ˢ-int ⟦st⟧ , (program-typed-rec rest frames))
|
||||
preservation pushbool-eval ⟦st⟧ (program-typed-flat (pushbool-t thenᵗ rest)) = (_ , ⟦⟧ˢ-bool ⟦st⟧ , (program-typed-flat rest))
|
||||
preservation pushbool-eval ⟦st⟧ (program-typed-rec (pushbool-t thenᵗ rest) frames) = (_ , ⟦⟧ˢ-bool ⟦st⟧ , (program-typed-rec rest frames))
|
||||
preservation add-eval (⟦⟧ˢ-int (⟦⟧ˢ-int ⟦st⟧)) (program-typed-flat (add-t thenᵗ rest)) = (_ , ⟦⟧ˢ-int ⟦st⟧ , (program-typed-flat rest))
|
||||
preservation add-eval (⟦⟧ˢ-int (⟦⟧ˢ-int ⟦st⟧)) (program-typed-rec (add-t thenᵗ rest) frames) = (_ , ⟦⟧ˢ-int ⟦st⟧ , (program-typed-rec rest frames))
|
||||
preservation loop-eval⁰ ⟦st⟧ (program-typed-flat ((loop-t _) thenᵗ rest)) = (_ , ⟦st⟧ , (program-typed-flat rest))
|
||||
preservation loop-eval⁰ ⟦st⟧ (program-typed-rec ((loop-t _) thenᵗ rest) frames) = (_ , ⟦st⟧ , (program-typed-rec rest) frames)
|
||||
preservation loop-evalⁿ ⟦st⟧ (program-typed-flat ((loop-t loopt) thenᵗ rest)) = (_ , ⟦st⟧ , (program-typed-rec loopt (program-typed-flat (loop-t loopt thenᵗ rest))))
|
||||
preservation loop-evalⁿ ⟦st⟧ (program-typed-rec ((loop-t loopt) thenᵗ rest) frames) = (_ , ⟦st⟧ , (program-typed-rec loopt (program-typed-rec (loop-t loopt thenᵗ rest) frames)))
|
||||
preservation break-evalᵗ (⟦⟧ˢ-bool ⟦st⟧) (program-typed-rec (break-t thenᵗ rest) frames) = (_ , ⟦st⟧ , skip-loop-continuation frames)
|
||||
preservation break-evalᶠ (⟦⟧ˢ-bool ⟦st⟧) (program-typed-rec (break-t thenᵗ rest) frames) = (_ , ⟦st⟧ , (program-typed-rec rest frames))
|
||||
preservation empty-eval ⟦st⟧ (program-typed-rec (doneᵗ-just) frames) = (_ , ⟦st⟧ , frames)
|
||||
|
||||
progress : ∀ {stˡ} →
|
||||
st ⊢ (is , S) ↦* stˡ →
|
||||
⟦ st ⟧ˢ s →
|
||||
(Σ Triple ((s , is , S) ⇒_)) ⊎ (is ≡ [] × S ≡ [] × ⟦ stˡ ⟧ˢ s)
|
||||
progress (program-typed-flat (pushint-t thenᵗ rest)) ⟦st⟧ = inj₁ (_ , pushint-eval)
|
||||
progress (program-typed-rec (pushint-t thenᵗ rest) frames) ⟦st⟧ = inj₁ (_ , pushint-eval)
|
||||
progress (program-typed-flat (pushbool-t thenᵗ rest)) ⟦st⟧ = inj₁ (_ , pushbool-eval)
|
||||
progress (program-typed-rec (pushbool-t thenᵗ rest) frames) ⟦st⟧ = inj₁ (_ , pushbool-eval)
|
||||
progress (program-typed-flat (add-t thenᵗ rest)) (⟦⟧ˢ-int (⟦⟧ˢ-int ⟦st⟧)) = inj₁ (_ , add-eval)
|
||||
progress (program-typed-rec (add-t thenᵗ rest) frames) (⟦⟧ˢ-int (⟦⟧ˢ-int ⟦st⟧)) = inj₁ (_ , add-eval)
|
||||
progress {is = loop 0 is' ∷ is} (program-typed-flat (loop-t _ thenᵗ rest)) ⟦st⟧ = inj₁ (_ , loop-eval⁰)
|
||||
progress {is = loop 0 is' ∷ is} (program-typed-rec (loop-t _ thenᵗ rest) frames) ⟦st⟧ = inj₁ (_ , loop-eval⁰)
|
||||
progress {is = loop (suc n) is' ∷ is} (program-typed-flat (loop-t _ thenᵗ rest)) ⟦st⟧ = inj₁ (_ , loop-evalⁿ)
|
||||
progress {is = loop (suc n) is' ∷ is} (program-typed-rec (loop-t _ thenᵗ rest) frames) ⟦st⟧ = inj₁ (_ , loop-evalⁿ)
|
||||
progress {s = bool true ∷ s} (program-typed-rec (break-t thenᵗ rest) frames) (⟦⟧ˢ-bool ⟦st⟧) = inj₁ (_ , break-evalᵗ)
|
||||
progress {s = bool false ∷ s} (program-typed-rec (break-t thenᵗ rest) frames) (⟦⟧ˢ-bool ⟦st⟧) = inj₁ (_ , break-evalᶠ)
|
||||
progress {is = []} (program-typed-rec (doneᵗ-just) frames) ⟦st⟧ = inj₁ (_ , empty-eval)
|
||||
progress {is = []} (program-typed-flat (doneᵗ-nothing)) ⟦st⟧ = inj₂ (refl , refl , ⟦st⟧)
|
||||
|
||||
{-# TERMINATING #-} -- evaluation always terminates, but proving it is tedious
|
||||
static-dynamic-help : ∀ {stˡ} →
|
||||
st ⊢ (is , S) ↦* stˡ →
|
||||
⟦ st ⟧ˢ s →
|
||||
Σ (List Value) (λ sˡ → ⟦ stˡ ⟧ˢ sˡ × (s , is , S) ⇒* (sˡ , [] , []))
|
||||
static-dynamic-help {s = s} frames ⟦st⟧
|
||||
with progress frames ⟦st⟧
|
||||
... | inj₁ ((s' , is' , S') , is⇒is') =
|
||||
let (st' , (⟦st'⟧ , frames')) = preservation is⇒is' ⟦st⟧ frames in
|
||||
let (sˡ , (⟦stˡ⟧ , is'⇒*[])) = static-dynamic-help frames' ⟦st'⟧ in
|
||||
(sˡ , (⟦stˡ⟧ , is⇒is' thenᵉ is'⇒*[]))
|
||||
... | inj₂ (refl , refl , ⟦stˡ⟧) = (s , (⟦stˡ⟧ , doneᵉ))
|
||||
|
||||
|
||||
static-dynamic : ∀ {stˡ} →
|
||||
st ⊢ is ↦| stˡ →
|
||||
⟦ st ⟧ˢ s →
|
||||
Σ (List Value) (λ sˡ → ⟦ stˡ ⟧ˢ sˡ × (s , is , []) ⇒* (sˡ , [] , []))
|
||||
static-dynamic st⊢is↦|stˡ = static-dynamic-help (program-typed-flat st⊢is↦|stˡ)
|
||||
|
||||
-- Copied from Flat.agda
|
||||
|
||||
open import Data.Nat.Show using () renaming (show to showℕ)
|
||||
open import Data.Integer.Show using () renaming (show to showℤ)
|
||||
open import Data.Bool.Show using () renaming (show to showBool)
|
||||
open import Data.String using (String; _++_)
|
||||
open import Data.Product using (proj₁)
|
||||
|
||||
stackToString : List Value → String
|
||||
stackToString [] = "[]"
|
||||
stackToString (int i ∷ s) = showℤ i ++ " :: " ++ stackToString s
|
||||
stackToString (bool b ∷ s) = showBool b ++ " :: " ++ stackToString s
|
||||
|
||||
open import IO
|
||||
open import Level using (0ℓ)
|
||||
|
||||
main = run {0ℓ} (putStrLn (stackToString (proj₁ (static-dynamic basict₄ ⟦⟧ˢ-empty))))
|
|
@ -1,24 +0,0 @@
|
|||
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)
|
Loading…
Reference in New Issue
Block a user