DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add more higher-order primitives

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-04-30 21:56:34 -07:00
parent 112a5087ef
commit be50c76cb1
2 changed files with 13 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Language/Semantics.agda
View File

@ -12,7 +12,7 @@ open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality using (_≡_) open import Relation.Binary.PropositionalEquality using (_≡_)
open import Lattice open import Lattice
open import Utils using (_⇒_) open import Utils using (_⇒_; _∧_; _∨_)
data Value : Set where data Value : Set where
↑ᶻ : ℤ → Value ↑ᶻ : ℤ → Value
@ -69,3 +69,5 @@ record LatticeInterpretation {l} {L : Set l} {_≈_ : L → L → Set l}
field field
⟦_⟧ : L → Value → Set ⟦_⟧ : L → Value → Set
⟦⟧-respects-≈ : ∀ {l₁ l₂ : L} → l₁ ≈ l₂ → ⟦ l₁ ⟧ ⇒ ⟦ l₂ ⟧ ⟦⟧-respects-≈ : ∀ {l₁ l₂ : L} → l₁ ≈ l₂ → ⟦ l₁ ⟧ ⇒ ⟦ l₂ ⟧
⟦⟧-⊔-∨ : ∀ {l₁ l₂ : L} → (⟦ l₁ ⟧ ∨ ⟦ l₂ ⟧) ⇒ ⟦ l₁ ⊔ l₂ ⟧
⟦⟧-⊓-∧ : ∀ {l₁ l₂ : L} → (⟦ l₁ ⟧ ∧ ⟦ l₂ ⟧) ⇒ ⟦ l₁ ⊓ l₂ ⟧

11
Utils.agda
View File

@ -1,13 +1,14 @@
module Utils where module Utils where
open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_) 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.Nat using (ℕ; suc)
open import Data.List using (List; cartesianProduct; []; _∷_; _++_; foldr) renaming (map to mapˡ) 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 using (_∈_)
open import Data.List.Membership.Propositional.Properties as ListMemProp 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.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.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 Function.Definitions using (Injective)
open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl) open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl)
open import Relation.Nullary using (¬_) 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₂) → _⇒_ : ∀ {a p₁ p₂} {A : Set a} (P : A → Set p₁) (Q : A → Set p₂) →
Set (a ⊔ℓ p₁ ⊔ℓ p₂) Set (a ⊔ℓ p₁ ⊔ℓ p₂)
_⇒_ P Q = ∀ a → P a → Q a _⇒_ 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