Start on sign analysis (mostly just imports)

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

Analysis/Sign.agda

@@ -0,0 +1,50 @@
+module Analysis.Sign where
+
+open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+
+open import Language
+open import Lattice
+
+data Sign : Set where
+    + : Sign
+    - : Sign
+    0ˢ : Sign
+
+-- g for siGn; s is used for strings and i is not very descriptive.
+_≟ᵍ_ : IsDecidable (_≡_ {_} {Sign})
+_≟ᵍ_ + + = yes refl
+_≟ᵍ_ + - = no (λ ())
+_≟ᵍ_ + 0ˢ = no (λ ())
+_≟ᵍ_ - + = no (λ ())
+_≟ᵍ_ - - = yes refl
+_≟ᵍ_ - 0ˢ = no (λ ())
+_≟ᵍ_ 0ˢ + = no (λ ())
+_≟ᵍ_ 0ˢ - = no (λ ())
+_≟ᵍ_ 0ˢ 0ˢ = yes refl
+
+module _ (prog : Program) where
+    open Program prog
+
+    -- embelish 'sign' with a top and bottom element.
+    open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵍ_ as AB renaming (AboveBelow to SignLattice; ≈-dec to ≈ᵍ-dec)
+    -- 'sign' has no underlying lattice structure, so use the 'plain' above-below lattice.
+    open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵍ-if-inhabited)
+
+
+    finiteHeightLatticeᵍ = finiteHeightLatticeᵍ-if-inhabited 0ˢ
+
+    -- The variable -> sign map is a finite value-map with keys strings. Use a bundle to avoid explicitly specifying operators.
+    open import Lattice.Bundles.FiniteValueMap String SignLattice _≟ˢ_ renaming (finiteHeightLattice to finiteHeightLatticeᵛ-if-B-finite; FiniteHeightType to FiniteHeightTypeᵛ; _≈_ to _≈ᵛ_; ≈-dec to ≈ᵛ-dec-if-≈ᵍ-dec)
+
+
+    VariableSigns = FiniteHeightTypeᵛ finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
+    finiteHeightLatticeᵛ = finiteHeightLatticeᵛ-if-B-finite finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
+    ≈ᵛ-dec = ≈ᵛ-dec-if-≈ᵍ-dec finiteHeightLatticeᵍ vars-Unique ≈ᵍ-dec
+
+    -- Finally, the map we care about is (state -> (variables -> sign)). Bring that in.
+    open import Lattice.Bundles.FiniteValueMap State VariableSigns _≟_ renaming (finiteHeightLattice to finiteHeightLatticeᵐ-if-B-finite; FiniteHeightType to FiniteHeightTypeᵐ)
+
+    StateVariables = FiniteHeightTypeᵐ finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec
+    finiteHeightLatticeᵐ = finiteHeightLatticeᵐ-if-B-finite finiteHeightLatticeᵛ states-Unique ≈ᵛ-dec