Define interpretation of the sign lattice

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Analysis/Sign.agda

@@ -1,15 +1,19 @@
 module Analysis.Sign where
 
-open import Data.Nat using (suc)
-open import Data.Product using (proj₁; _,_)
+open import Data.Integer using (ℤ; +_; -[1+_])
+open import Data.Nat using (ℕ; suc; zero)
+open import Data.Product using (Σ; proj₁; _,_)
+open import Data.Sum using (inj₁; inj₂)
 open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Unit using (⊤; tt)
 open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst)
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary using (¬_; yes; no)
 
 open import Language
 open import Lattice
 open import Showable using (Showable; show)
+open import Utils using (_⇒_; _∧_; _∨_)
 import Analysis.Forward
 
 data Sign : Set where
@@ -61,6 +65,7 @@ open AB.Plain 0ˢ using ()
         ; fixedHeight to fixedHeightᵍ
         ; _≼_ to _≼ᵍ_
         ; _⊔_ to _⊔ᵍ_
+        ; _⊓_ to _⊓ᵍ_
         )
 
 open IsLattice isLatticeᵍ using ()
@@ -106,6 +111,62 @@ minus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
 postulate minus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → minus s₁ s₂)
 postulate minus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (minus s₁)
 
+⟦_⟧ᵍ : SignLattice → Value → Set
+⟦_⟧ᵍ ⊥ᵍ _ = ⊥
+⟦_⟧ᵍ ⊤ᵍ _ = ⊤
+⟦_⟧ᵍ [ + ]ᵍ v = Σ ℕ (λ n → v ≡ ↑ᶻ (+_ (suc n)))
+⟦_⟧ᵍ [ 0ˢ ]ᵍ v = Σ ℕ (λ n → v ≡ ↑ᶻ (+_ zero))
+⟦_⟧ᵍ [ - ]ᵍ v = Σ ℕ (λ n → v ≡ ↑ᶻ -[1+ n ])
+
+⟦⟧ᵍ-respects-≈ᵍ : ∀ {s₁ s₂ : SignLattice} → s₁ ≈ᵍ s₂ → ⟦ s₁ ⟧ᵍ ⇒ ⟦ s₂ ⟧ᵍ
+⟦⟧ᵍ-respects-≈ᵍ ≈ᵍ-⊥ᵍ-⊥ᵍ v bot = bot
+⟦⟧ᵍ-respects-≈ᵍ ≈ᵍ-⊤ᵍ-⊤ᵍ v top = top
+⟦⟧ᵍ-respects-≈ᵍ (≈ᵍ-lift { + } { + } refl) v proof = proof
+⟦⟧ᵍ-respects-≈ᵍ (≈ᵍ-lift { - } { - } refl) v proof = proof
+⟦⟧ᵍ-respects-≈ᵍ (≈ᵍ-lift { 0ˢ } { 0ˢ } refl) v proof = proof
+
+⟦⟧ᵍ-⊔ᵍ-∨ : ∀ {s₁ s₂ : SignLattice} → (⟦ s₁ ⟧ᵍ ∨ ⟦ s₂ ⟧ᵍ) ⇒ ⟦ s₁ ⊔ᵍ s₂ ⟧ᵍ
+⟦⟧ᵍ-⊔ᵍ-∨ {⊥ᵍ} x (inj₂ px₂) = px₂
+⟦⟧ᵍ-⊔ᵍ-∨ {⊤ᵍ} x _ = tt
+⟦⟧ᵍ-⊔ᵍ-∨ {[ s₁ ]ᵍ} {[ s₂ ]ᵍ} x px
+    with s₁ ≟ᵍ s₂
+...   | no _ = tt
+...   | yes refl
+        with px
+...       | inj₁ px₁ = px₁
+...       | inj₂ px₂ = px₂
+⟦⟧ᵍ-⊔ᵍ-∨ {[ s₁ ]ᵍ} {⊥ᵍ} x (inj₁ px₁) = px₁
+⟦⟧ᵍ-⊔ᵍ-∨ {[ s₁ ]ᵍ} {⊤ᵍ} x _ = tt
+
+s₁≢s₂⇒¬s₁∧s₂ : ∀ {s₁ s₂ : Sign} → ¬ s₁ ≡ s₂ → ∀ {v} → ¬ ((⟦ [ s₁ ]ᵍ ⟧ᵍ ∧ ⟦ [ s₂ ]ᵍ ⟧ᵍ) v)
+s₁≢s₂⇒¬s₁∧s₂ { + } { + } +≢+ _ = ⊥-elim (+≢+ refl)
+s₁≢s₂⇒¬s₁∧s₂ { + } { - } _ ((n , refl) , (m , ()))
+s₁≢s₂⇒¬s₁∧s₂ { + } { 0ˢ } _ ((n , refl) , (m , ()))
+s₁≢s₂⇒¬s₁∧s₂ { 0ˢ } { + } _ ((n , refl) , (m , ()))
+s₁≢s₂⇒¬s₁∧s₂ { 0ˢ } { 0ˢ } +≢+ _ = ⊥-elim (+≢+ refl)
+s₁≢s₂⇒¬s₁∧s₂ { 0ˢ } { - } _ ((n , refl) , (m , ()))
+s₁≢s₂⇒¬s₁∧s₂ { - } { + } _ ((n , refl) , (m , ()))
+s₁≢s₂⇒¬s₁∧s₂ { - } { 0ˢ } _ ((n , refl) , (m , ()))
+s₁≢s₂⇒¬s₁∧s₂ { - } { - } +≢+ _ = ⊥-elim (+≢+ refl)
+
+⟦⟧ᵍ-⊓ᵍ-∧ : ∀ {s₁ s₂ : SignLattice} → (⟦ s₁ ⟧ᵍ ∧ ⟦ s₂ ⟧ᵍ) ⇒ ⟦ s₁ ⊓ᵍ s₂ ⟧ᵍ
+⟦⟧ᵍ-⊓ᵍ-∧ {⊥ᵍ} x (bot , _) = bot
+⟦⟧ᵍ-⊓ᵍ-∧ {⊤ᵍ} x (_ , px₂) = px₂
+⟦⟧ᵍ-⊓ᵍ-∧ {[ s₁ ]ᵍ} {[ s₂ ]ᵍ} x (px₁ , px₂)
+    with s₁ ≟ᵍ s₂
+...   | no s₁≢s₂ = s₁≢s₂⇒¬s₁∧s₂ s₁≢s₂ (px₁ , px₂)
+...   | yes refl = px₁
+⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊥ᵍ} x (_ , bot) = bot
+⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊤ᵍ} x (px₁ , _) = px₁
+
+latticeInterpretationᵍ : LatticeInterpretation isLatticeᵍ
+latticeInterpretationᵍ = record
+    { ⟦_⟧ = ⟦_⟧ᵍ
+    ; ⟦⟧-respects-≈ = ⟦⟧ᵍ-respects-≈ᵍ
+    ; ⟦⟧-⊔-∨ = ⟦⟧ᵍ-⊔ᵍ-∨
+    ; ⟦⟧-⊓-∧ = ⟦⟧ᵍ-⊓ᵍ-∧
+    }
+
 module WithProg (prog : Program) where
     open Program prog
 

Language/Graphs.agda

@@ -15,7 +15,7 @@ open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-s
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst; trans)
 
 open import Lattice
-open import Utils using (x∈xs⇒fx∈fxs; _⊗_; _,_; ∈-cartesianProduct)
+open import Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct)
 
 record Graph : Set where
     constructor MkGraph

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,12 @@ 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₂ ⟧
+        ⟦⟧-⊔-∨ : ∀ {l₁ l₂ : L} → (⟦ l₁ ⟧ ∨ ⟦ l₂ ⟧) ⇒ ⟦ l₁ ⊔ l₂ ⟧
+        ⟦⟧-⊓-∧ : ∀ {l₁ l₂ : L} → (⟦ l₁ ⟧ ∧ ⟦ l₂ ⟧) ⇒ ⟦ l₁ ⊓ l₂ ⟧

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 (¬_)
@@ -71,16 +72,6 @@ data Pairwise {a} {b} {c} {A : Set a} {B : Set b} (P : A → B → Set c) : List
           P x y → Pairwise P xs ys →
           Pairwise P (x ∷ xs) (y ∷ ys)
 
-infixr 2 _⊗_
-data _⊗_ {a p q} {A : Set a} (P : A → Set p) (Q : A → Set q) : A → Set (a ⊔ℓ p ⊔ℓ q) where
-    _,_ : ∀ {val : A} → P val → Q val → (P ⊗ Q) val
-
-proj₁ : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} {a : A} → (P ⊗ Q) a → P a
-proj₁ (v , _) = v
-
-proj₂ : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} {a : A} → (P ⊗ Q) a → Q a
-proj₂ (_ , v) = v
-
 ∈-cartesianProduct : ∀ {a b} {A : Set a} {B : Set b}
                      {x : A} {xs : List A} {y : B} {ys : List B} →
                      x ∈ xs → y ∈ ys → (x Prod., y) ∈ cartesianProduct xs ys
@@ -91,3 +82,15 @@ 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
+
+_∨_ : ∀ {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