Analysis/Sign.agda

@@ -1,19 +1,15 @@
 module Analysis.Sign where
 
-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.Nat using (suc)
+open import Data.Product using (proj₁; _,_)
 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
@@ -65,7 +61,6 @@ open AB.Plain 0ˢ using ()
         ; fixedHeight to fixedHeightᵍ
         ; _≼_ to _≼ᵍ_
         ; _⊔_ to _⊔ᵍ_
-        ; _⊓_ to _⊓ᵍ_
         )
 
 open IsLattice isLatticeᵍ using ()
@@ -111,62 +106,6 @@ 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,7 +2,6 @@ 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)
@@ -11,9 +10,6 @@ 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
 
@@ -62,12 +58,3 @@ 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,14 +1,13 @@
 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 (¬_)
@@ -72,6 +71,16 @@ 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
@@ -82,15 +91,3 @@ 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