Implement constant analysis

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

Analysis/Constant.agda

@@ -0,0 +1,223 @@
+
+module Analysis.Constant where
+
+open import Data.Integer as Int using (ℤ; +_; -[1+_]; _≟_)
+open import Data.Integer.Show as IntShow using ()
+open import Data.Nat as Nat using (ℕ; suc; zero)
+open import Data.Product using (Σ; proj₁; 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 Equivalence
+open import Language
+open import Lattice
+open import Showable using (Showable; show)
+open import Utils using (_⇒_; _∧_; _∨_)
+open import Analysis.Utils using (eval-combine₂)
+import Analysis.Forward
+
+instance
+    showable : Showable ℤ
+    showable = record
+        { show = IntShow.show
+        }
+
+instance
+    ≡-equiv : IsEquivalence ℤ _≡_
+    ≡-equiv = record
+        { ≈-refl = refl
+        ; ≈-sym = sym
+        ; ≈-trans = trans
+        }
+
+    ≡-Decidable-ℤ : IsDecidable {_} {ℤ} _≡_
+    ≡-Decidable-ℤ = record { R-dec = _≟_ }
+
+-- embelish 'ℕ' with a top and bottom element.
+open import Lattice.AboveBelow ℤ _ as AB
+    using ()
+    renaming
+        ( AboveBelow to ConstLattice
+        ; ≈-dec to ≈ᶜ-dec
+        ; ⊥ to ⊥ᶜ
+        ; ⊤ to ⊤ᶜ
+        ; [_] to [_]ᶜ
+        ; _≈_ to _≈ᶜ_
+        ; ≈-⊥-⊥ to ≈ᶜ-⊥ᶜ-⊥ᶜ
+        ; ≈-⊤-⊤ to ≈ᶜ-⊤ᶜ-⊤ᶜ
+        ; ≈-lift to ≈ᶜ-lift
+        ; ≈-refl to ≈ᶜ-refl
+        )
+-- 'ℕ''s structure is not finite, so just use a 'plain' above-below Lattice.
+open AB.Plain (+ 0) using ()
+    renaming
+        ( isLattice to isLatticeᶜ
+        ; isFiniteHeightLattice to isFiniteHeightLatticeᵍ
+        ; _≼_ to _≼ᶜ_
+        ; _⊔_ to _⊔ᶜ_
+        ; _⊓_ to _⊓ᶜ_
+        ; ≼-trans to ≼ᶜ-trans
+        ; ≼-refl to ≼ᶜ-refl
+        )
+
+plus : ConstLattice → ConstLattice → ConstLattice
+plus ⊥ᶜ _ = ⊥ᶜ
+plus _ ⊥ᶜ = ⊥ᶜ
+plus ⊤ᶜ _ = ⊤ᶜ
+plus _ ⊤ᶜ = ⊤ᶜ
+plus [ z₁ ]ᶜ [ z₂ ]ᶜ = [ z₁ Int.+ z₂ ]ᶜ
+
+-- this is incredibly tedious: 125 cases per monotonicity proof, and tactics
+-- are hard. postulate for now.
+postulate plus-Monoˡ : ∀ (s₂ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (λ s₁ → plus s₁ s₂)
+postulate plus-Monoʳ : ∀ (s₁ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (plus s₁)
+
+plus-Mono₂ : Monotonic₂ _≼ᶜ_ _≼ᶜ_ _≼ᶜ_ plus
+plus-Mono₂ = (plus-Monoˡ , plus-Monoʳ)
+
+minus : ConstLattice → ConstLattice → ConstLattice
+minus ⊥ᶜ _ = ⊥ᶜ
+minus _ ⊥ᶜ = ⊥ᶜ
+minus ⊤ᶜ _ = ⊤ᶜ
+minus _ ⊤ᶜ = ⊤ᶜ
+minus [ z₁ ]ᶜ [ z₂ ]ᶜ = [ z₁ Int.- z₂ ]ᶜ
+
+postulate minus-Monoˡ : ∀ (s₂ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (λ s₁ → minus s₁ s₂)
+postulate minus-Monoʳ : ∀ (s₁ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (minus s₁)
+
+minus-Mono₂ : Monotonic₂ _≼ᶜ_ _≼ᶜ_ _≼ᶜ_ minus
+minus-Mono₂ = (minus-Monoˡ , minus-Monoʳ)
+
+⟦_⟧ᶜ : ConstLattice → Value → Set
+⟦_⟧ᶜ ⊥ᶜ _ = ⊥
+⟦_⟧ᶜ ⊤ᶜ _ = ⊤
+⟦_⟧ᶜ [ z ]ᶜ v = v ≡ ↑ᶻ z
+
+⟦⟧ᶜ-respects-≈ᶜ : ∀ {s₁ s₂ : ConstLattice} → s₁ ≈ᶜ s₂ → ⟦ s₁ ⟧ᶜ ⇒ ⟦ s₂ ⟧ᶜ
+⟦⟧ᶜ-respects-≈ᶜ ≈ᶜ-⊥ᶜ-⊥ᶜ v bot = bot
+⟦⟧ᶜ-respects-≈ᶜ ≈ᶜ-⊤ᶜ-⊤ᶜ v top = top
+⟦⟧ᶜ-respects-≈ᶜ (≈ᶜ-lift { z } { z } refl) v proof = proof
+
+⟦⟧ᶜ-⊔ᶜ-∨ : ∀ {s₁ s₂ : ConstLattice} → (⟦ 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₂ : ∀ {z₁ z₂ : ℤ} → ¬ z₁ ≡ z₂ → ∀ {v} → ¬ ((⟦ [ z₁ ]ᶜ ⟧ᶜ ∧ ⟦ [ z₂ ]ᶜ ⟧ᶜ) v)
+s₁≢s₂⇒¬s₁∧s₂ { z₁ } { z₂ } z₁≢z₂ {v} (v≡z₁ , v≡z₂)
+    with refl ← trans (sym v≡z₁) v≡z₂ = z₁≢z₂ refl
+
+⟦⟧ᶜ-⊓ᶜ-∧ : ∀ {s₁ s₂ : ConstLattice} → (⟦ 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₁
+
+instance
+    latticeInterpretationᶜ : LatticeInterpretation isLatticeᶜ
+    latticeInterpretationᶜ = record
+        { ⟦_⟧ = ⟦_⟧ᶜ
+        ; ⟦⟧-respects-≈ = ⟦⟧ᶜ-respects-≈ᶜ
+        ; ⟦⟧-⊔-∨ = ⟦⟧ᶜ-⊔ᶜ-∨
+        ; ⟦⟧-⊓-∧ = ⟦⟧ᶜ-⊓ᶜ-∧
+        }
+
+module WithProg (prog : Program) where
+    open Program prog
+
+    open import Analysis.Forward.Lattices ConstLattice prog
+    open import Analysis.Forward.Evaluation ConstLattice prog
+    open import Analysis.Forward.Adapters ConstLattice prog
+
+    eval : ∀ (e : Expr) → VariableValues → ConstLattice
+    eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs)
+    eval (e₁ - e₂) vs = minus (eval e₁ vs) (eval e₂ vs)
+    eval (` k) vs
+        with ∈k-decᵛ k (proj₁ (proj₁ vs))
+    ...   | yes k∈vs = proj₁ (locateᵛ {k} {vs} k∈vs)
+    ...   | no _ = ⊤ᶜ
+    eval (# n) _ = [ + n ]ᶜ
+
+    eval-Monoʳ : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ᶜ_ (eval e)
+    eval-Monoʳ (e₁ + e₂) {vs₁} {vs₂} vs₁≼vs₂ =
+        eval-combine₂ (λ {x} {y} {z} →  ≼ᶜ-trans {x} {y} {z})
+                      plus plus-Mono₂ {o₁ = eval e₁ vs₁}
+                      (eval-Monoʳ e₁ vs₁≼vs₂) (eval-Monoʳ e₂ vs₁≼vs₂)
+    eval-Monoʳ (e₁ - e₂) {vs₁} {vs₂} vs₁≼vs₂ =
+        eval-combine₂ (λ {x} {y} {z} →  ≼ᶜ-trans {x} {y} {z})
+                      minus minus-Mono₂ {o₁ = eval e₁ vs₁}
+                      (eval-Monoʳ e₁ vs₁≼vs₂) (eval-Monoʳ e₂ vs₁≼vs₂)
+    eval-Monoʳ (` k) {vs₁@((kvs₁ , _) , _)} {vs₂@((kvs₂ , _), _)} vs₁≼vs₂
+        with ∈k-decᵛ k kvs₁ | ∈k-decᵛ k kvs₂
+    ...   | yes k∈kvs₁ | yes k∈kvs₂ =
+            let
+                (v₁ , k,v₁∈vs₁) = locateᵛ {k} {vs₁} k∈kvs₁
+                (v₂ , k,v₂∈vs₂) = locateᵛ {k} {vs₂} k∈kvs₂
+            in
+                m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ vs₁ vs₂ vs₁≼vs₂ k,v₁∈vs₁ k,v₂∈vs₂
+    ...   | yes k∈kvs₁ | no k∉kvs₂ = ⊥-elim (k∉kvs₂ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₁ vs₂) k∈kvs₁))
+    ...   | no k∉kvs₁ | yes k∈kvs₂ = ⊥-elim (k∉kvs₁ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₂ vs₁) k∈kvs₂))
+    ...   | no k∉kvs₁ | no k∉kvs₂ = IsLattice.≈-refl isLatticeᶜ
+    eval-Monoʳ (# n) _ = ≼ᶜ-refl ([ + n ]ᶜ)
+
+    instance
+        ConstEval : ExprEvaluator
+        ConstEval = record { eval = eval; eval-Monoʳ = eval-Monoʳ }
+
+    -- For debugging purposes, print out the result.
+    output = show (Analysis.Forward.WithProg.result ConstLattice prog)
+
+    -- This should have fewer cases -- the same number as the actual 'plus' above.
+    -- But agda only simplifies on first argument, apparently, so we are stuck
+    -- listing them all.
+    plus-valid : ∀ {g₁ g₂} {z₁ z₂} → ⟦ g₁ ⟧ᶜ (↑ᶻ z₁) → ⟦ g₂ ⟧ᶜ (↑ᶻ z₂) → ⟦ plus g₁ g₂ ⟧ᶜ (↑ᶻ (z₁ Int.+ z₂))
+    plus-valid {⊥ᶜ} {_} ⊥ _ = ⊥
+    plus-valid {[ z ]ᶜ} {⊥ᶜ} _ ⊥ = ⊥
+    plus-valid {⊤ᶜ} {⊥ᶜ} _ ⊥ = ⊥
+    plus-valid {⊤ᶜ} {[ z ]ᶜ} _ _ = tt
+    plus-valid {⊤ᶜ} {⊤ᶜ} _ _ = tt
+    plus-valid {[ z₁ ]ᶜ} {[ z₂ ]ᶜ} refl refl = refl
+    plus-valid {[ z ]ᶜ} {⊤ᶜ} _ _ = tt
+    --
+    -- Same for this one. It should be easier, but Agda won't simplify.
+    minus-valid : ∀ {g₁ g₂} {z₁ z₂} → ⟦ g₁ ⟧ᶜ (↑ᶻ z₁) → ⟦ g₂ ⟧ᶜ (↑ᶻ z₂) → ⟦ minus g₁ g₂ ⟧ᶜ (↑ᶻ (z₁ Int.- z₂))
+    minus-valid {⊥ᶜ} {_} ⊥ _ = ⊥
+    minus-valid {[ z ]ᶜ} {⊥ᶜ} _ ⊥ = ⊥
+    minus-valid {⊤ᶜ} {⊥ᶜ} _ ⊥ = ⊥
+    minus-valid {⊤ᶜ} {[ z ]ᶜ} _ _ = tt
+    minus-valid {⊤ᶜ} {⊤ᶜ} _ _ = tt
+    minus-valid {[ z₁ ]ᶜ} {[ z₂ ]ᶜ} refl refl = refl
+    minus-valid {[ z ]ᶜ} {⊤ᶜ} _ _ = tt
+
+    eval-valid : IsValidExprEvaluator
+    eval-valid (⇒ᵉ-+ ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
+        plus-valid (eval-valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
+    eval-valid (⇒ᵉ-- ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
+        minus-valid (eval-valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
+    eval-valid {vs} (⇒ᵉ-Var ρ x v x,v∈ρ) ⟦vs⟧ρ
+        with ∈k-decᵛ x (proj₁ (proj₁ vs))
+    ...   | yes x∈kvs = ⟦vs⟧ρ (proj₂ (locateᵛ {x} {vs} x∈kvs)) x,v∈ρ
+    ...   | no x∉kvs = tt
+    eval-valid (⇒ᵉ-ℕ ρ n) _ = refl
+
+    instance
+        ConstEvalValid : ValidExprEvaluator ConstEval latticeInterpretationᶜ
+        ConstEvalValid = record { valid = eval-valid }
+
+    analyze-correct = Analysis.Forward.WithProg.analyze-correct ConstLattice prog tt

Analysis/Forward.agda

@@ -8,6 +8,7 @@ module Analysis.Forward
     {{≈ˡ-dec : IsDecidable _≈ˡ_}} where
 
 open import Data.Empty using (⊥-elim)
+open import Data.Unit using (⊤)
 open import Data.String using (String)
 open import Data.Product using (_,_)
 open import Data.List using (_∷_; []; foldr; foldl)
@@ -77,7 +78,7 @@ module WithProg (prog : Program) where
             updateAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
 
         module WithValidInterpretation {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}}
-                                       {{validEvaluator : ValidStmtEvaluator evaluator latticeInterpretationˡ}} where
+                                       {{validEvaluator : ValidStmtEvaluator evaluator latticeInterpretationˡ}} (dummy : ⊤) where
             open ValidStmtEvaluator validEvaluator
 
             eval-fold-valid : ∀ {s bss vs ρ₁ ρ₂} → ρ₁ , bss ⇒ᵇˢ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ foldl (flip (eval s)) vs bss ⟧ᵛ ρ₂

Analysis/Sign.agda

@@ -16,6 +16,7 @@ open import Lattice
 open import Equivalence
 open import Showable using (Showable; show)
 open import Utils using (_⇒_; _∧_; _∨_)
+open import Analysis.Utils using (eval-combine₂)
 import Analysis.Forward
 
 data Sign : Set where
@@ -101,6 +102,9 @@ plus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
 postulate plus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → plus s₁ s₂)
 postulate plus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (plus s₁)
 
+plus-Mono₂ : Monotonic₂ _≼ᵍ_ _≼ᵍ_ _≼ᵍ_ plus
+plus-Mono₂ = (plus-Monoˡ , plus-Monoʳ)
+
 minus : SignLattice → SignLattice → SignLattice
 minus ⊥ᵍ _ = ⊥ᵍ
 minus _ ⊥ᵍ = ⊥ᵍ
@@ -119,6 +123,9 @@ minus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
 postulate minus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → minus s₁ s₂)
 postulate minus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (minus s₁)
 
+minus-Mono₂ : Monotonic₂ _≼ᵍ_ _≼ᵍ_ _≼ᵍ_ minus
+minus-Mono₂ = (minus-Monoˡ , minus-Monoʳ)
+
 ⟦_⟧ᵍ : SignLattice → Value → Set
 ⟦_⟧ᵍ ⊥ᵍ _ = ⊥
 ⟦_⟧ᵍ ⊤ᵍ _ = ⊤
@@ -195,29 +202,13 @@ module WithProg (prog : Program) where
 
     eval-Monoʳ : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ᵍ_ (eval e)
     eval-Monoʳ (e₁ + e₂) {vs₁} {vs₂} vs₁≼vs₂ =
-        let
-            -- TODO: can this be done with less boilerplate?
-            g₁vs₁ = eval e₁ vs₁
-            g₂vs₁ = eval e₂ vs₁
-            g₁vs₂ = eval e₁ vs₂
-            g₂vs₂ = eval e₂ vs₂
-        in
-            ≼ᵍ-trans
-                {plus g₁vs₁ g₂vs₁} {plus g₁vs₂ g₂vs₁} {plus g₁vs₂ g₂vs₂}
-                (plus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Monoʳ e₁ {vs₁} {vs₂} vs₁≼vs₂))
-                (plus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Monoʳ e₂ {vs₁} {vs₂} vs₁≼vs₂))
+        eval-combine₂ (λ {x} {y} {z} →  ≼ᵍ-trans {x} {y} {z})
+                      plus plus-Mono₂ {o₁ = eval e₁ vs₁}
+                      (eval-Monoʳ e₁ vs₁≼vs₂) (eval-Monoʳ e₂ vs₁≼vs₂)
     eval-Monoʳ (e₁ - e₂) {vs₁} {vs₂} vs₁≼vs₂ =
-        let
-            -- TODO: here too -- can this be done with less boilerplate?
-            g₁vs₁ = eval e₁ vs₁
-            g₂vs₁ = eval e₂ vs₁
-            g₁vs₂ = eval e₁ vs₂
-            g₂vs₂ = eval e₂ vs₂
-        in
-            ≼ᵍ-trans
-                {minus g₁vs₁ g₂vs₁} {minus g₁vs₂ g₂vs₁} {minus g₁vs₂ g₂vs₂}
-                (minus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Monoʳ e₁ {vs₁} {vs₂} vs₁≼vs₂))
-                (minus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Monoʳ e₂ {vs₁} {vs₂} vs₁≼vs₂))
+        eval-combine₂ (λ {x} {y} {z} →  ≼ᵍ-trans {x} {y} {z})
+                      minus minus-Mono₂ {o₁ = eval e₁ vs₁}
+                      (eval-Monoʳ e₁ vs₁≼vs₂) (eval-Monoʳ e₂ vs₁≼vs₂)
     eval-Monoʳ (` k) {vs₁@((kvs₁ , _) , _)} {vs₂@((kvs₂ , _), _)} vs₁≼vs₂
         with ∈k-decᵛ k kvs₁ | ∈k-decᵛ k kvs₂
     ...   | yes k∈kvs₁ | yes k∈kvs₂ =
@@ -301,4 +292,8 @@ module WithProg (prog : Program) where
     eval-valid (⇒ᵉ-ℕ ρ 0) _ = refl
     eval-valid (⇒ᵉ-ℕ ρ (suc n')) _ = (n' , refl)
 
-    analyze-correct = Analysis.Forward.WithProg.analyze-correct
+    instance
+        SignEvalValid : ValidExprEvaluator SignEval latticeInterpretationᵍ
+        SignEvalValid = record { valid = eval-valid }
+
+    analyze-correct = Analysis.Forward.WithProg.analyze-correct SignLattice prog tt

Analysis/Utils.agda

@@ -0,0 +1,15 @@
+module Analysis.Utils where
+
+open import Data.Product using (_,_)
+open import Lattice
+
+module _ {o} {O : Set o} {_≼ᴼ_ : O → O → Set o}
+         (≼ᴼ-trans : ∀ {o₁ o₂ o₃} → o₁ ≼ᴼ o₂ → o₂ ≼ᴼ o₃ → o₁ ≼ᴼ o₃)
+         (combine : O → O → O) (combine-Mono₂ : Monotonic₂ _≼ᴼ_ _≼ᴼ_ _≼ᴼ_ combine) where
+
+    eval-combine₂ : {o₁ o₂ o₃ o₄ : O} → o₁ ≼ᴼ o₃ → o₂ ≼ᴼ o₄ →
+                    combine o₁ o₂ ≼ᴼ combine o₃ o₄
+    eval-combine₂ {o₁} {o₂} {o₃} {o₄} o₁≼o₃ o₂≼o₄ =
+        let (combine-Monoˡ , combine-Monoʳ) = combine-Mono₂
+        in ≼ᴼ-trans (combine-Monoˡ o₂ o₁≼o₃)
+                    (combine-Monoʳ o₃ o₂≼o₄)

Lattice.agda

@@ -21,6 +21,18 @@ module _ {a b} {A : Set a} {B : Set b}
     Monotonic : (A → B) → Set (a ⊔ℓ b)
     Monotonic f = ∀ {a₁ a₂ : A} → a₁ ≼₁ a₂ → f a₁ ≼₂ f a₂
 
+    Monotonicˡ : ∀ {c} {C : Set c} → (A → C → B) →  Set (a ⊔ℓ b ⊔ℓ c)
+    Monotonicˡ f = ∀ c →  Monotonic (λ a → f a c)
+
+    Monotonicʳ : ∀ {c} {C : Set c} → (C → A → B) →  Set (a ⊔ℓ b ⊔ℓ c)
+    Monotonicʳ f = ∀ a → Monotonic (f a)
+
+module _ {a b c} {A : Set a} {B : Set b} {C : Set c}
+    (_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) (_≼₃_ : C → C → Set c) where
+
+    Monotonic₂ : (A → B → C) → Set (a ⊔ℓ b ⊔ℓ c)
+    Monotonic₂ f = Monotonicˡ _≼₁_ _≼₃_ f × Monotonicʳ _≼₂_ _≼₃_ f
+
 record IsSemilattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A) : Set a where

Lattice/AboveBelow.agda

@@ -321,7 +321,7 @@ module Plain (x : A) where
             ; isLattice = isLattice
             }
 
-    open IsLattice isLattice using (_≼_; _≺_; ≼-trans; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
+    open IsLattice isLattice using (_≼_; _≺_; ≼-trans; ≼-refl; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
 
     ⊥≺[x] : ∀ (x : A) → ⊥ ≺ [ x ]
     ⊥≺[x] x = (≈-refl , λ ())

Main.agda

@@ -1,11 +1,13 @@
 {-# OPTIONS --guardedness #-}
 module Main where
 
-open import Language
-open import Analysis.Sign
+open import Language hiding (_++_)
 open import Data.Vec using (Vec; _∷_; [])
 open import IO
 open import Level using (0ℓ)
+open import Data.String using (_++_)
+import Analysis.Constant as ConstantAnalysis
+import Analysis.Sign as SignAnalysis
 
 testCode : Stmt
 testCode =
@@ -38,6 +40,7 @@ testProgram = record
     { rootStmt = testCode
     }
 
-open WithProg testProgram using (output; analyze-correct)
+open SignAnalysis.WithProg testProgram using (analyze-correct) renaming (output to output-Sign)
+open ConstantAnalysis.WithProg testProgram using (analyze-correct) renaming (output to output-Const)
 
-main = run {0ℓ} (putStrLn output)
+main = run {0ℓ} (putStrLn (output-Const ++ "\n" ++ output-Sign))