From be50c76cb1ce6f91bbc187586babde89e4a26a3d Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 30 Apr 2024 21:56:34 -0700 Subject: [PATCH] Add more higher-order primitives Signed-off-by: Danila Fedorin --- Language/Semantics.agda | 4 +++- Utils.agda | 11 ++++++++++- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/Language/Semantics.agda b/Language/Semantics.agda index b41ca21..bfd813b 100644 --- a/Language/Semantics.agda +++ b/Language/Semantics.agda @@ -12,7 +12,7 @@ open import Relation.Nullary using (¬_) open import Relation.Binary.PropositionalEquality using (_≡_) open import Lattice -open import Utils using (_⇒_) +open import Utils using (_⇒_; _∧_; _∨_) data Value : Set where ↑ᶻ : ℤ → Value @@ -69,3 +69,5 @@ record LatticeInterpretation {l} {L : Set l} {_≈_ : L → L → Set l} 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₂ ⟧ diff --git a/Utils.agda b/Utils.agda index c6689d0..0e76eb7 100644 --- a/Utils.agda +++ b/Utils.agda @@ -1,13 +1,14 @@ module Utils where open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_) -open import Data.Product as Prod using () +open import Data.Product as Prod using (_×_) open import Data.Nat using (ℕ; suc) open import Data.List using (List; cartesianProduct; []; _∷_; _++_; foldr) renaming (map to mapˡ) open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Membership.Propositional.Properties as ListMemProp using () open import Data.List.Relation.Unary.All using (All; []; _∷_; map) open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map +open import Data.Sum using (_⊎_) open import Function.Definitions using (Injective) open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl) open import Relation.Nullary using (¬_) @@ -85,3 +86,11 @@ concat-∈ {ls = l' ∷ ls'} x∈l (there l∈ls') = ListMemProp.∈-++⁺ʳ l' _⇒_ : ∀ {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 + +_∨_ : ∀ {a p₁ p₂} {A : Set a} (P : A → Set p₁) (Q : A → Set p₂) → + A → Set (p₁ ⊔ℓ p₂) +_∨_ P Q a = P a ⊎ Q a + +_∧_ : ∀ {a p₁ p₂} {A : Set a} (P : A → Set p₁) (Q : A → Set p₂) → + A → Set (p₁ ⊔ℓ p₂) +_∧_ P Q a = P a × Q a