From 112a5087efe8658c37390fc5923fddb6bd62e23c Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 30 Apr 2024 19:20:02 -0700 Subject: [PATCH] Tentative start on proving correctness Signed-off-by: Danila Fedorin --- Language/Semantics.agda | 11 +++++++++++ Utils.agda | 4 ++++ 2 files changed, 15 insertions(+) diff --git a/Language/Semantics.agda b/Language/Semantics.agda index c24ac93..b41ca21 100644 --- a/Language/Semantics.agda +++ b/Language/Semantics.agda @@ -2,6 +2,7 @@ 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) @@ -10,6 +11,9 @@ 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 @@ -58,3 +62,10 @@ data _,_⇒ˢ_ : Env → Stmt → Env → Set where ⇒ˢ-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₂ ⟧ diff --git a/Utils.agda b/Utils.agda index 6223787..c6689d0 100644 --- a/Utils.agda +++ b/Utils.agda @@ -81,3 +81,7 @@ concat-∈ : ∀ {a} {A : Set a} {x : A} {l : List A} {ls : List (List A)} → x ∈ l → l ∈ ls → x ∈ foldr _++_ [] ls concat-∈ x∈l (here refl) = ListMemProp.∈-++⁺ˡ x∈l concat-∈ {ls = l' ∷ ls'} x∈l (there l∈ls') = ListMemProp.∈-++⁺ʳ l' (concat-∈ x∈l l∈ls') + +_⇒_ : ∀ {a p₁ p₂} {A : Set a} (P : A → Set p₁) (Q : A → Set p₂) → + Set (a ⊔ℓ p₁ ⊔ℓ p₂) +_⇒_ P Q = ∀ a → P a → Q a