Add semantics of Hoare logic assertions.

1 files changed, 34 insertions, 19 deletions

diff --git a/src/Helium/Semantics/Axiomatic/Assertion.agda b/src/Helium/Semantics/Axiomatic/Assertion.agda
index 70feb2b..8d66886 100644
--- a/src/Helium/Semantics/Axiomatic/Assertion.agda
+++ b/src/Helium/Semantics/Axiomatic/Assertion.agda
@@ -16,17 +16,21 @@ module Helium.Semantics.Axiomatic.Assertion
 open RawPseudocode rawPseudocode
 
 open import Data.Bool as Bool using (Bool)
+open import Data.Empty.Polymorphic using (⊥)
 open import Data.Fin as Fin using (suc)
 open import Data.Fin.Patterns
 open import Data.Nat using (ℕ; suc)
-open import Data.Product using (proj₁; proj₂)
+import Data.Nat.Properties as ℕₚ
+open import Data.Product using (∃; _×_; _,_; proj₁; proj₂)
+open import Data.Sum using (_⊎_)
+open import Data.Unit.Polymorphic using (⊤)
 open import Data.Vec as Vec using (Vec; []; _∷_; _++_)
 open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
+open import Function using (_$_)
 open import Helium.Data.Pseudocode.Core
 open import Helium.Semantics.Axiomatic.Core rawPseudocode
 open import Helium.Semantics.Axiomatic.Term rawPseudocode as Term using (Term)
-open import Level using (_⊔_; lift)
-open import Relation.Nullary using (does)
+open import Level using (_⊔_; Lift; lift; lower) renaming (suc to ℓsuc)
 
 private
   variable
@@ -34,19 +38,17 @@ private
     m n o    : ℕ
     Γ Δ Σ ts : Vec Type m
 
-infixl 7 _[_]↦_
-
 open Term.Term
 
-data Assertion (Σ : Vec Type o) (Γ : Vec Type n) (Δ : Vec Type m) : Set (b₁ ⊔ i₁ ⊔ r₁) where
-  _[_]↦_ : ∀ {m t} → Term Σ Γ Δ (asType t m) → Term Σ Γ Δ (fin m) → Term Σ Γ Δ (elemType t) → Assertion Σ Γ Δ
+data Assertion (Σ : Vec Type o) (Γ : Vec Type n) (Δ : Vec Type m) : Set (ℓsuc (b₁ ⊔ i₁ ⊔ r₁))
+
+data Assertion Σ Γ Δ where
   all    : Assertion Σ Γ (t ∷ Δ) → Assertion Σ Γ Δ
   some   : Assertion Σ Γ (t ∷ Δ) → Assertion Σ Γ Δ
   pred   : Term Σ Γ Δ bool → Assertion Σ Γ Δ
-  comb   : ∀ {n} → (Vec Bool n → Bool) → Vec (Assertion Σ Γ Δ) n → Assertion Σ Γ Δ
+  comb   : ∀ {n} → (Vec (Set (b₁ ⊔ i₁ ⊔ r₁)) n → Set (b₁ ⊔ i₁ ⊔ r₁)) → Vec (Assertion Σ Γ Δ) n → Assertion Σ Γ Δ
 
 elimVar : Assertion Σ (t ∷ Γ) Δ → Term Σ Γ Δ t → Assertion Σ Γ Δ
-elimVar (ref [ i ]↦ val) t = Term.elimVar ref t [ Term.elimVar i t ]↦ Term.elimVar val t
 elimVar (all P)          t = all (elimVar P (Term.wknMeta t))
 elimVar (some P)         t = some (elimVar P (Term.wknMeta t))
 elimVar (pred p)         t = pred (Term.elimVar p t)
@@ -57,7 +59,6 @@ elimVar (comb f Ps)      t = comb f (helper Ps t)
   helper (P ∷ Ps) t = elimVar P t ∷ helper Ps t
 
 wknVar : Assertion Σ Γ Δ → Assertion Σ (t ∷ Γ) Δ
-wknVar (ref [ i ]↦ val) = Term.wknVar ref [ Term.wknVar i ]↦ Term.wknVar val
 wknVar (all P)          = all (wknVar P)
 wknVar (some P)         = some (wknVar P)
 wknVar (pred p)         = pred (Term.wknVar p)
@@ -68,7 +69,6 @@ wknVar (comb f Ps)      = comb f (helper Ps)
   helper (P ∷ Ps) = wknVar P ∷ helper Ps
 
 wknVars : (ts : Vec Type n) → Assertion Σ Γ Δ → Assertion Σ (ts ++ Γ) Δ
-wknVars τs (ref [ i ]↦ val) = Term.wknVars τs ref [ Term.wknVars τs i ]↦ Term.wknVars τs val
 wknVars τs (all P)          = all (wknVars τs P)
 wknVars τs (some P)         = some (wknVars τs P)
 wknVars τs (pred p)         = pred (Term.wknVars τs p)
@@ -79,7 +79,6 @@ wknVars τs (comb f Ps)      = comb f (helper Ps)
   helper (P ∷ Ps) = wknVars τs P ∷ helper Ps
 
 addVars : Assertion Σ [] Δ → Assertion Σ Γ Δ
-addVars (ref [ i ]↦ val) = Term.addVars ref [ Term.addVars i ]↦ Term.addVars val
 addVars (all P)          = all (addVars P)
 addVars (some P)         = some (addVars P)
 addVars (pred p)         = pred (Term.addVars p)
@@ -90,7 +89,6 @@ addVars (comb f Ps)      = comb f (helper Ps)
   helper (P ∷ Ps) = addVars P ∷ helper Ps
 
 wknMetaAt : ∀ i → Assertion Σ Γ Δ → Assertion Σ Γ (Vec.insert Δ i t)
-wknMetaAt i (ref [ j ]↦ val) = Term.wknMetaAt i ref [ Term.wknMetaAt i j ]↦ Term.wknMetaAt i val
 wknMetaAt i (all P)          = all (wknMetaAt (suc i) P)
 wknMetaAt i (some P)         = some (wknMetaAt (suc i) P)
 wknMetaAt i (pred p)         = pred (Term.wknMetaAt i p)
@@ -108,7 +106,6 @@ wknMetas (_ ∷ ts) P = wknMetaAt 0F (wknMetas ts P)
 module _ (2≉0 : Term.2≉0) where
   -- NOTE: better to induct on e here than in Term?
   subst : Assertion Σ Γ Δ → {e : Code.Expression Σ Γ t} → Code.CanAssign Σ e → Term Σ Γ Δ t → Assertion Σ Γ Δ
-  subst (ref [ i ]↦ val) e t = Term.subst 2≉0 ref e t [ Term.subst 2≉0 i e t ]↦ Term.subst 2≉0 val e t
   subst (all P)          e t = all (subst P e (Term.wknMeta t))
   subst (some P)         e t = some (subst P e (Term.wknMeta t))
   subst (pred p)         e t = pred (Term.subst 2≉0 p e t)
@@ -123,16 +120,16 @@ module Construct where
   infixl 5 _∨_
 
   true : Assertion Σ Γ Δ
-  true = comb (λ _ → Bool.true) []
+  true = comb (λ _ → ⊤) []
 
   false : Assertion Σ Γ Δ
-  false = comb (λ _ → Bool.false) []
+  false = comb (λ _ → ⊥) []
 
   _∧_ : Assertion Σ Γ Δ → Assertion Σ Γ Δ → Assertion Σ Γ Δ
-  P ∧ Q = comb (λ { (p ∷ q ∷ []) → p Bool.∧ q }) (P ∷ Q ∷ [])
+  P ∧ Q = comb (λ { (P ∷ Q ∷ []) → P × Q }) (P ∷ Q ∷ [])
 
   _∨_ : Assertion Σ Γ Δ → Assertion Σ Γ Δ → Assertion Σ Γ Δ
-  P ∨ Q = comb (λ { (p ∷ q ∷ []) → p Bool.∨ q }) (P ∷ Q ∷ [])
+  P ∨ Q = comb (λ { (P ∷ Q ∷ []) → P ⊎ Q }) (P ∷ Q ∷ [])
 
   equal : Term Σ Γ Δ t → Term Σ Γ Δ t → Assertion Σ Γ Δ
   equal {t = bool} x y = pred Term.[ bool ][ x ≟ y ]
@@ -143,6 +140,24 @@ module Construct where
   equal {t = bits n} x y = pred Term.[ bits n ][ x ≟ y ]
   equal {t = tuple _ []} x y = true
   equal {t = tuple _ (t ∷ ts)} x y = equal {t = t} (Term.func₁ proj₁ x) (Term.func₁ proj₁ y) ∧ equal (Term.func₁ proj₂ x) (Term.func₁ proj₂ y)
-  equal {t = array t n} x y = all (some (Term.wknMeta (Term.wknMeta x) [ meta 1F ]↦ meta 0F ∧ Term.wknMeta (Term.wknMeta y) [ meta 1F ]↦ meta 0F))
+  equal {t = array t 0} x y = true
+  equal {t = array t (suc n)} x y = all (equal {t = t} (index x) (index y))
+    where
+    index = λ v → Term.unbox (array t) $
+                  Term.func₁ proj₁ $
+                  Term.cut (array t)
+                    (Term.cast (array t) (ℕₚ.+-comm 1 n) (Term.wknMeta v))
+                    (meta 0F)
 
 open Construct public
+
+⟦_⟧ : Assertion Σ Γ Δ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Δ ⟧ₜ′ → Set (b₁ ⊔ i₁ ⊔ r₁)
+⟦_⟧′ : Vec (Assertion Σ Γ Δ) n → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Δ ⟧ₜ′ → Vec (Set (b₁ ⊔ i₁ ⊔ r₁)) n
+
+⟦ all P ⟧ σ γ δ = ∀ x → ⟦ P ⟧ σ γ (x , δ)
+⟦ some P ⟧ σ γ δ = ∃ λ x → ⟦ P ⟧ σ γ (x , δ)
+⟦ pred p ⟧ σ γ δ = Lift (b₁ ⊔ i₁ ⊔ r₁) (Bool.T (lower (Term.⟦ p ⟧ σ γ δ)))
+⟦ comb f Ps ⟧ σ γ δ = f (⟦ Ps ⟧′ σ γ δ)
+
+⟦ [] ⟧′     σ γ δ = []
+⟦ P ∷ Ps ⟧′ σ γ δ = ⟦ P ⟧ σ γ δ ∷ ⟦ Ps ⟧′ σ γ δ