74 lines
3.9 KiB
Agda
74 lines
3.9 KiB
Agda
module Language.Semantics where
|
||
|
||
open import Language.Base
|
||
|
||
open import Agda.Primitive using (lsuc)
|
||
open import Data.Integer using (ℤ; +_) renaming (_+_ to _+ᶻ_; _-_ to _-ᶻ_)
|
||
open import Data.Product using (_×_; _,_)
|
||
open import Data.String using (String)
|
||
open import Data.List as List using (List)
|
||
open import Data.Nat using (ℕ)
|
||
open import Relation.Nullary using (¬_)
|
||
open import Relation.Binary.PropositionalEquality using (_≡_)
|
||
|
||
open import Lattice
|
||
open import Utils using (_⇒_; _∧_; _∨_)
|
||
|
||
data Value : Set where
|
||
↑ᶻ : ℤ → Value
|
||
|
||
Env : Set
|
||
Env = List (String × Value)
|
||
|
||
data _∈_ : (String × Value) → Env → Set where
|
||
here : ∀ (s : String) (v : Value) (ρ : Env) → (s , v) ∈ ((s , v) List.∷ ρ)
|
||
there : ∀ (s s' : String) (v v' : Value) (ρ : Env) → ¬ (s ≡ s') → (s , v) ∈ ρ → (s , v) ∈ ((s' , v') List.∷ ρ)
|
||
|
||
data _,_⇒ᵉ_ : Env → Expr → Value → Set where
|
||
⇒ᵉ-ℕ : ∀ (ρ : Env) (n : ℕ) → ρ , (# n) ⇒ᵉ (↑ᶻ (+ n))
|
||
⇒ᵉ-Var : ∀ (ρ : Env) (x : String) (v : Value) → (x , v) ∈ ρ → ρ , (` x) ⇒ᵉ v
|
||
⇒ᵉ-+ : ∀ (ρ : Env) (e₁ e₂ : Expr) (z₁ z₂ : ℤ) →
|
||
ρ , e₁ ⇒ᵉ (↑ᶻ z₁) → ρ , e₂ ⇒ᵉ (↑ᶻ z₂) →
|
||
ρ , (e₁ + e₂) ⇒ᵉ (↑ᶻ (z₁ +ᶻ z₂))
|
||
⇒ᵉ-- : ∀ (ρ : Env) (e₁ e₂ : Expr) (z₁ z₂ : ℤ) →
|
||
ρ , e₁ ⇒ᵉ (↑ᶻ z₁) → ρ , e₂ ⇒ᵉ (↑ᶻ z₂) →
|
||
ρ , (e₁ - e₂) ⇒ᵉ (↑ᶻ (z₁ -ᶻ z₂))
|
||
|
||
data _,_⇒ᵇ_ : Env → BasicStmt → Env → Set where
|
||
⇒ᵇ-noop : ∀ (ρ : Env) → ρ , noop ⇒ᵇ ρ
|
||
⇒ᵇ-← : ∀ (ρ : Env) (x : String) (e : Expr) (v : Value) →
|
||
ρ , e ⇒ᵉ v → ρ , (x ← e) ⇒ᵇ ((x , v) List.∷ ρ)
|
||
|
||
data _,_⇒ᵇˢ_ : Env → List BasicStmt → Env → Set where
|
||
[] : ∀ {ρ : Env} → ρ , List.[] ⇒ᵇˢ ρ
|
||
_∷_ : ∀ {ρ₁ ρ₂ ρ₃ : Env} {bs : BasicStmt} {bss : List BasicStmt} →
|
||
ρ₁ , bs ⇒ᵇ ρ₂ → ρ₂ , bss ⇒ᵇˢ ρ₃ → ρ₁ , (bs List.∷ bss) ⇒ᵇˢ ρ₃
|
||
|
||
data _,_⇒ˢ_ : Env → Stmt → Env → Set where
|
||
⇒ˢ-⟨⟩ : ∀ (ρ₁ ρ₂ : Env) (bs : BasicStmt) →
|
||
ρ₁ , bs ⇒ᵇ ρ₂ → ρ₁ , ⟨ bs ⟩ ⇒ˢ ρ₂
|
||
⇒ˢ-then : ∀ (ρ₁ ρ₂ ρ₃ : Env) (s₁ s₂ : Stmt) →
|
||
ρ₁ , s₁ ⇒ˢ ρ₂ → ρ₂ , s₂ ⇒ˢ ρ₃ →
|
||
ρ₁ , (s₁ then s₂) ⇒ˢ ρ₃
|
||
⇒ˢ-if-true : ∀ (ρ₁ ρ₂ : Env) (e : Expr) (z : ℤ) (s₁ s₂ : Stmt) →
|
||
ρ₁ , e ⇒ᵉ (↑ᶻ z) → ¬ z ≡ (+ 0) → ρ₁ , s₁ ⇒ˢ ρ₂ →
|
||
ρ₁ , (if e then s₁ else s₂) ⇒ˢ ρ₂
|
||
⇒ˢ-if-false : ∀ (ρ₁ ρ₂ : Env) (e : Expr) (s₁ s₂ : Stmt) →
|
||
ρ₁ , e ⇒ᵉ (↑ᶻ (+ 0)) → ρ₁ , s₂ ⇒ˢ ρ₂ →
|
||
ρ₁ , (if e then s₁ else s₂) ⇒ˢ ρ₂
|
||
⇒ˢ-while-true : ∀ (ρ₁ ρ₂ ρ₃ : Env) (e : Expr) (z : ℤ) (s : Stmt) →
|
||
ρ₁ , e ⇒ᵉ (↑ᶻ z) → ¬ z ≡ (+ 0) → ρ₁ , s ⇒ˢ ρ₂ → ρ₂ , (while e repeat s) ⇒ˢ ρ₃ →
|
||
ρ₁ , (while e repeat s) ⇒ˢ ρ₃
|
||
⇒ˢ-while-false : ∀ (ρ : Env) (e : Expr) (s : Stmt) →
|
||
ρ , e ⇒ᵉ (↑ᶻ (+ 0)) →
|
||
ρ , (while e repeat s) ⇒ˢ ρ
|
||
|
||
record LatticeInterpretation {l} {L : Set l} {_≈_ : L → L → Set l}
|
||
{_⊔_ : L → L → L} {_⊓_ : L → L → L}
|
||
(isLattice : IsLattice L _≈_ _⊔_ _⊓_) : Set (lsuc l) where
|
||
field
|
||
⟦_⟧ : L → Value → Set
|
||
⟦⟧-respects-≈ : ∀ {l₁ l₂ : L} → l₁ ≈ l₂ → ⟦ l₁ ⟧ ⇒ ⟦ l₂ ⟧
|
||
⟦⟧-⊔-∨ : ∀ {l₁ l₂ : L} → (⟦ l₁ ⟧ ∨ ⟦ l₂ ⟧) ⇒ ⟦ l₁ ⊔ l₂ ⟧
|
||
⟦⟧-⊓-∧ : ∀ {l₁ l₂ : L} → (⟦ l₁ ⟧ ∧ ⟦ l₂ ⟧) ⇒ ⟦ l₁ ⊓ l₂ ⟧
|