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.Integer using (ℤ; +_; -[1+_])
-open import Data.Product using (proj₁; _,_)
+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