Begin work on axiomatic semantics.

4 files changed, 253 insertions, 35 deletions

diff --git a/src/Helium/Data/Pseudocode/Types.agda b/src/Helium/Data/Pseudocode/Types.agda
index 971ca12..dbd3c6b 100644
--- a/src/Helium/Data/Pseudocode/Types.agda
+++ b/src/Helium/Data/Pseudocode/Types.agda
@@ -146,3 +146,5 @@ record Pseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ :
     ; _/1 = _/1
     ; ⌊_⌋ = ⌊_⌋
     }
+
+  open RawPseudocode rawPseudocode using (module ℤ′; module ℝ′) public
diff --git a/src/Helium/Semantics/Axiomatic/Core.agda b/src/Helium/Semantics/Axiomatic/Core.agda
new file mode 100644
index 0000000..92c67bb
--- /dev/null
+++ b/src/Helium/Semantics/Axiomatic/Core.agda
@@ -0,0 +1,168 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Base definitions for the axiomatic semantics
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+
+module Helium.Semantics.Axiomatic.Core
+  {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
+  (rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
+  where
+
+private
+  open module C = RawPseudocode rawPseudocode
+
+open import Data.Bool using (Bool; T)
+open import Data.Fin as Fin using (zero; suc)
+import Data.Fin.Properties as Finₚ
+-- open import Data.Nat as ℕ using (zero; suc)
+import Data.Nat as ℕ
+import Data.Nat.Properties as ℕₚ
+open import Data.Product using (∃; _×_; _,_; <_,_>)
+open import Data.Sum using (_⊎_)
+open import Data.Unit using (⊤)
+open import Data.Vec using (Vec; _∷_; lookup)
+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.Core rawPseudocode
+open import Level using (_⊔_; Lift)
+open import Relation.Binary.PropositionalEquality using (refl)
+open import Relation.Nullary using (yes; no)
+open import Relation.Unary using (Decidable; _⊆_)
+
+module _ {o} (Σ : Vec Type o) {n} (Γ : Vec Type n) where
+  data Term {m} (Δ : Vec Type m) : Type → Set (b₁ ⊔ i₁ ⊔ r₁) where
+    state : ∀ i → Term Δ (lookup Σ i)
+    var   : ∀ i → Term Δ (lookup Γ i)
+    meta  : ∀ i → Term Δ (lookup Δ i)
+    funct : ∀ {m ts t} → (⟦ tuple m ts ⟧ₜˡ → ⟦ t ⟧ₜˡ) → All (Term Δ) ts → Term Δ t
+
+  infixl 7 _⇒_
+  infixl 6 _∧_
+  infixl 5 _∨_
+
+  data Assertion {m} (Δ : Vec Type m) : Set (b₁ ⊔ i₁ ⊔ r₁) where
+    _∧_  : Assertion Δ → Assertion Δ → Assertion Δ
+    _∨_  : Assertion Δ → Assertion Δ → Assertion Δ
+    _⇒_  : Assertion Δ → Assertion Δ → Assertion Δ
+    all  : ∀ {t} → Assertion (t ∷ Δ) → Assertion Δ
+    some : ∀ {t} → Assertion (t ∷ Δ) → Assertion Δ
+    pred : ∀ {m ts} → (⟦ tuple m ts ⟧ₜˡ → Bool) → All (Term Δ) ts → Assertion Δ
+
+module _ {o} {Σ : Vec Type o} {n} {Γ : Vec Type n} {m} {Δ : Vec Type m} where
+  ⟦_⟧ : ∀ {t} → Term Σ Γ Δ t → ⟦ Σ ⟧ₜˡ′ → ⟦ Γ ⟧ₜˡ′ → ⟦ Δ ⟧ₜˡ′ → ⟦ t ⟧ₜˡ
+  ⟦_⟧′ : ∀ {n ts} → All (Term Σ Γ Δ) ts → ⟦ Σ ⟧ₜˡ′ → ⟦ Γ ⟧ₜˡ′ → ⟦ Δ ⟧ₜˡ′ → ⟦ tuple n ts ⟧ₜˡ
+  ⟦ state i ⟧    σ γ δ = fetchˡ Σ σ i
+  ⟦ var i ⟧      σ γ δ = fetchˡ Γ γ i
+  ⟦ meta i ⟧     σ γ δ = fetchˡ Δ δ i
+  ⟦ funct f ts ⟧ σ γ δ = f (⟦ ts ⟧′ σ γ δ)
+
+  ⟦ [] ⟧′            σ γ δ = _
+  ⟦ (t ∷ []) ⟧′      σ γ δ = ⟦ t ⟧ σ γ δ
+  ⟦ (t ∷ t′ ∷ ts) ⟧′ σ γ δ = ⟦ t ⟧ σ γ δ , ⟦ t′ ∷ ts ⟧′ σ γ δ
+
+  termSubstState : ∀ {t} → Term Σ Γ Δ t → ∀ j → Term Σ Γ Δ (lookup Σ j) → Term Σ Γ Δ t
+  termSubstState (state i)    j t′ with j Fin.≟ i
+  ...                                 | yes refl = t′
+  ...                                 | no _     = state i
+  termSubstState (var i)      j t′ = var i
+  termSubstState (meta i)     j t′ = meta i
+  termSubstState (funct f ts) j t′ = funct f (helper ts)
+    where
+    helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ Γ Δ) ts
+    helper []       = []
+    helper (t ∷ ts) = termSubstState t j t′ ∷ helper ts
+
+  termSubstVar : ∀ {t} → Term Σ Γ Δ t → ∀ j → Term Σ Γ Δ (lookup Γ j) → Term Σ Γ Δ t
+  termSubstVar (state i)     j t′ = state i
+  termSubstVar (var i)       j t′ with j Fin.≟ i
+  ...                                | yes refl = t′
+  ...                                | no _     = var i
+  termSubstVar (meta i)      j t′ = meta i
+  termSubstVar (funct f ts)  j t′ = funct f (helper ts)
+    where
+    helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ Γ Δ) ts
+    helper []       = []
+    helper (t ∷ ts) = termSubstVar t j t′ ∷ helper ts
+
+  termElimVar : ∀ {t t′} → Term Σ (t′ ∷ Γ) Δ t → Term Σ Γ Δ t′ → Term Σ Γ Δ t
+  termElimVar (state i)     t′ = state i
+  termElimVar (var zero)    t′ = t′
+  termElimVar (var (suc i)) t′ = var i
+  termElimVar (meta i)      t′ = meta i
+  termElimVar (funct f ts)  t′ = funct f (helper ts)
+    where
+    helper : ∀ {n ts} → All (Term _ _ _) {n} ts → All (Term _ _ _) ts
+    helper []       = []
+    helper (t ∷ ts) = termElimVar t t′ ∷ helper ts
+
+  termWknVar : ∀ {t t′} → Term Σ Γ Δ t → Term Σ (t′ ∷ Γ) Δ t
+  termWknVar (state i)    = state i
+  termWknVar (var i)      = var (suc i)
+  termWknVar (meta i)     = meta i
+  termWknVar (funct f ts) = funct f (helper ts)
+    where
+    helper : ∀ {n ts} → All (Term _ _ _) {n} ts → All (Term _ _ _) ts
+    helper []       = []
+    helper (t ∷ ts) = termWknVar t ∷ helper ts
+
+  termWknMeta : ∀ {t t′} → Term Σ Γ Δ t → Term Σ Γ (t′ ∷ Δ) t
+  termWknMeta (state i)    = state i
+  termWknMeta (var i)      = var i
+  termWknMeta (meta i)     = meta (suc i)
+  termWknMeta (funct f ts) = funct f (helper ts)
+    where
+    helper : ∀ {n ts} → All (Term _ _ _) {n} ts → All (Term _ _ _) ts
+    helper []       = []
+    helper (t ∷ ts) = termWknMeta t ∷ helper ts
+
+module _ {o} {Σ : Vec Type o} {n} {Γ : Vec Type n} where
+  infix 4 _∋[_] _⊨_
+
+  _∋[_] : ∀ {m Δ} → Assertion Σ Γ {m} Δ → ⟦ Σ ⟧ₜˡ′ × ⟦ Γ ⟧ₜˡ′ × ⟦ Δ ⟧ₜˡ′ → Set (b₁ ⊔ i₁ ⊔ r₁)
+  P ∧ Q ∋[ s ] = P ∋[ s ] × Q ∋[ s ]
+  P ∨ Q ∋[ s ] = P ∋[ s ] ⊎ Q ∋[ s ]
+  P ⇒ Q ∋[ s ] = P ∋[ s ] → Q ∋[ s ]
+  pred P ts ∋[ σ , γ , δ ] = Lift (b₁ ⊔ i₁ ⊔ r₁) $ T $ P (⟦ ts ⟧′ σ γ δ)
+  _∋[_] {Δ = Δ} (all P)  (σ , γ , δ) = ∀ v → P ∋[ σ , γ , consˡ Δ v δ ]
+  _∋[_] {Δ = Δ} (some P) (σ , γ , δ) = ∃ λ v → P ∋[ σ , γ , consˡ Δ v δ ]
+
+  _⊨_ : ∀ {m Δ} → ⟦ Σ ⟧ₜˡ′ × ⟦ Γ ⟧ₜˡ′ × ⟦ Δ ⟧ₜˡ′ → Assertion Σ Γ {m} Δ → Set (b₁ ⊔ i₁ ⊔ r₁)
+  s ⊨ P = P ∋[ s ]
+
+  asstSubstState : ∀ {m Δ} → Assertion Σ Γ {m} Δ → ∀ j → Term Σ Γ Δ (lookup Σ j) → Assertion Σ Γ Δ
+  asstSubstState (P ∧ Q)     j t = asstSubstState P j t ∧ asstSubstState Q j t
+  asstSubstState (P ∨ Q)     j t = asstSubstState P j t ∨ asstSubstState Q j t
+  asstSubstState (P ⇒ Q)     j t = asstSubstState P j t ⇒ asstSubstState Q j t
+  asstSubstState (all P)     j t = all (asstSubstState P j (termWknMeta t))
+  asstSubstState (some P)    j t = some (asstSubstState P j (termWknMeta t))
+  asstSubstState (pred p ts) j t = pred p (All.map (λ t′ → termSubstState t′ j t) ts)
+
+  asstSubstVar : ∀ {m Δ} → Assertion Σ Γ {m} Δ → ∀ j → Term Σ Γ Δ (lookup Γ j) → Assertion Σ Γ Δ
+  asstSubstVar (P ∧ Q)     j t = asstSubstVar P j t ∧ asstSubstVar Q j t
+  asstSubstVar (P ∨ Q)     j t = asstSubstVar P j t ∨ asstSubstVar Q j t
+  asstSubstVar (P ⇒ Q)     j t = asstSubstVar P j t ⇒ asstSubstVar Q j t
+  asstSubstVar (all P)     j t = all (asstSubstVar P j (termWknMeta t))
+  asstSubstVar (some P)    j t = some (asstSubstVar P j (termWknMeta t))
+  asstSubstVar (pred p ts) j t = pred p (All.map (λ t′ → termSubstVar t′ j t) ts)
+
+  asstElimVar : ∀ {m Δ t′} → Assertion Σ (t′ ∷ Γ) {m} Δ → Term Σ Γ Δ t′ → Assertion Σ Γ Δ
+  asstElimVar (P ∧ Q)     t = asstElimVar P t ∧ asstElimVar Q t
+  asstElimVar (P ∨ Q)     t = asstElimVar P t ∨ asstElimVar Q t
+  asstElimVar (P ⇒ Q)     t = asstElimVar P t ⇒ asstElimVar Q t
+  asstElimVar (all P)     t = all (asstElimVar P (termWknMeta t))
+  asstElimVar (some P)    t = some (asstElimVar P (termWknMeta t))
+  asstElimVar (pred p ts) t = pred p (All.map (λ t′ → termElimVar t′ t) ts)
+
+module _ {o} {Σ : Vec Type o} where
+  open Code Σ
+
+  data HoareTriple {n Γ m Δ} : Assertion Σ {n} Γ {m} Δ → Statement Γ → Assertion Σ Γ Δ → Set (b₁ ⊔ i₁ ⊔ r₁) where
+    csqs : ∀ {P₁ P₂ Q₁ Q₂ : Assertion Σ Γ Δ} {s} → (_⊨ P₁) ⊆ (_⊨ P₂) → HoareTriple P₂ s Q₂ → (_⊨ Q₂) ⊆ (_⊨ Q₁) → HoareTriple P₁ s Q₁
+    _∙_  : ∀ {P Q R s₁ s₂} → HoareTriple P s₁ Q → HoareTriple Q s₂ R → HoareTriple P (s₁ ∙ s₂) R
+    skip : ∀ {P} → HoareTriple P skip P
diff --git a/src/Helium/Semantics/Core.agda b/src/Helium/Semantics/Core.agda
new file mode 100644
index 0000000..749e1ca
--- /dev/null
+++ b/src/Helium/Semantics/Core.agda
@@ -0,0 +1,82 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Shared definitions between semantic systems
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+
+module Helium.Semantics.Core
+  {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
+  (rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
+  where
+
+private
+  open module C = RawPseudocode rawPseudocode
+
+open import Data.Bool using (Bool)
+open import Data.Fin using (Fin; zero; suc)
+open import Data.Product using (_×_; _,_)
+open import Data.Unit using (⊤)
+open import Data.Vec using (Vec; []; _∷_; lookup)
+open import Helium.Data.Pseudocode.Core
+open import Level hiding (zero; suc)
+
+⟦_⟧ₗ : Type → Level
+⟦ bool ⟧ₗ       = 0ℓ
+⟦ int ⟧ₗ        = i₁
+⟦ fin n ⟧ₗ      = 0ℓ
+⟦ real ⟧ₗ       = r₁
+⟦ bits n ⟧ₗ     = b₁
+⟦ tuple n ts ⟧ₗ = helper ts
+  where
+  helper : ∀ {n} → Vec Type n → Level
+  helper []       = 0ℓ
+  helper (t ∷ ts) = ⟦ t ⟧ₗ ⊔ helper ts
+⟦ array t n ⟧ₗ  = ⟦ t ⟧ₗ
+
+⟦_⟧ₜ : ∀ t → Set ⟦ t ⟧ₗ
+⟦_⟧ₜ′ : ∀ {n} ts → Set ⟦ tuple n ts ⟧ₗ
+
+⟦ bool ⟧ₜ       = Bool
+⟦ int ⟧ₜ        = ℤ
+⟦ fin n ⟧ₜ      = Fin n
+⟦ real ⟧ₜ       = ℝ
+⟦ bits n ⟧ₜ     = Bits n
+⟦ tuple n ts ⟧ₜ = ⟦ ts ⟧ₜ′
+⟦ array t n ⟧ₜ  = Vec ⟦ t ⟧ₜ n
+
+⟦ [] ⟧ₜ′          = ⊤
+⟦ t ∷ [] ⟧ₜ′      = ⟦ t ⟧ₜ
+⟦ t ∷ t′ ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ t′ ∷ ts ⟧ₜ′
+
+⟦_⟧ₜˡ : Type → Set (b₁ ⊔ i₁ ⊔ r₁)
+⟦_⟧ₜˡ′ : ∀ {n} → Vec Type n → Set (b₁ ⊔ i₁ ⊔ r₁)
+
+⟦ bool ⟧ₜˡ       = Lift (b₁ ⊔ i₁ ⊔ r₁) Bool
+⟦ int ⟧ₜˡ        = Lift (b₁ ⊔ r₁) ℤ
+⟦ fin n ⟧ₜˡ      = Lift (b₁ ⊔ i₁ ⊔ r₁) (Fin n)
+⟦ real ⟧ₜˡ       = Lift (b₁ ⊔ i₁) ℝ
+⟦ bits n ⟧ₜˡ     = Lift (i₁ ⊔ r₁) (Bits n)
+⟦ tuple n ts ⟧ₜˡ = ⟦ ts ⟧ₜˡ′ 
+⟦ array t n ⟧ₜˡ  = Vec ⟦ t ⟧ₜˡ n
+
+⟦ [] ⟧ₜˡ′          = Lift (b₁ ⊔ i₁ ⊔ r₁) ⊤
+⟦ t ∷ [] ⟧ₜˡ′      = ⟦ t ⟧ₜˡ
+⟦ t ∷ t′ ∷ ts ⟧ₜˡ′ = ⟦ t ⟧ₜˡ × ⟦ t′ ∷ ts ⟧ₜˡ′
+
+fetch : ∀ {n} ts → ⟦ tuple n ts ⟧ₜ → ∀ i → ⟦ lookup ts i ⟧ₜ
+fetch (_ ∷ [])     x        zero    = x
+fetch (_ ∷ _ ∷ _)  (x , xs) zero    = x
+fetch (_ ∷ t ∷ ts) (x , xs) (suc i) = fetch (t ∷ ts) xs i
+
+fetchˡ : ∀ {n} ts → ⟦ tuple n ts ⟧ₜˡ → ∀ i → ⟦ lookup ts i ⟧ₜˡ
+fetchˡ (_ ∷ [])     x        zero    = x
+fetchˡ (_ ∷ _ ∷ _)  (x , xs) zero    = x
+fetchˡ (_ ∷ t ∷ ts) (x , xs) (suc i) = fetchˡ (t ∷ ts) xs i
+
+consˡ : ∀ {n t} ts → ⟦ t ⟧ₜˡ → ⟦ tuple n ts ⟧ₜˡ → ⟦ t ∷ ts ⟧ₜˡ′
+consˡ []      x xs = x
+consˡ (_ ∷ _) x xs = x , xs
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index b425252..25f0448 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -29,41 +29,13 @@ open import Data.Vec.Relation.Unary.All using (All; []; _∷_)
 import Data.Vec.Functional as VecF
 open import Function using (case_of_; _∘′_; id)
 open import Helium.Data.Pseudocode.Core
+open import Helium.Semantics.Core rawPseudocode
 import Induction as I
 import Induction.WellFounded as Wf
-open import Level hiding (zero; suc)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
 open import Relation.Nullary using (does)
 open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromWitness)
 
-⟦_⟧ₗ : Type → Level
-⟦ bool ⟧ₗ       = 0ℓ
-⟦ int ⟧ₗ        = i₁
-⟦ fin n ⟧ₗ      = 0ℓ
-⟦ real ⟧ₗ       = r₁
-⟦ bits n ⟧ₗ     = b₁
-⟦ tuple n ts ⟧ₗ = helper ts
-  where
-  helper : ∀ {n} → Vec Type n → Level
-  helper []       = 0ℓ
-  helper (t ∷ ts) = ⟦ t ⟧ₗ ⊔ helper ts
-⟦ array t n ⟧ₗ  = ⟦ t ⟧ₗ
-
-⟦_⟧ₜ : ∀ t → Set ⟦ t ⟧ₗ
-⟦_⟧ₜ′ : ∀ {n} ts → Set ⟦ tuple n ts ⟧ₗ
-
-⟦ bool ⟧ₜ       = Bool
-⟦ int ⟧ₜ        = ℤ
-⟦ fin n ⟧ₜ      = Fin n
-⟦ real ⟧ₜ       = ℝ
-⟦ bits n ⟧ₜ     = Bits n
-⟦ tuple n ts ⟧ₜ = ⟦ ts ⟧ₜ′
-⟦ array t n ⟧ₜ  = Vec ⟦ t ⟧ₜ n
-
-⟦ [] ⟧ₜ′          = ⊤
-⟦ t ∷ [] ⟧ₜ′      = ⟦ t ⟧ₜ
-⟦ t ∷ t′ ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ t′ ∷ ts ⟧ₜ′
-
 -- The case for bitvectors looks odd so that the right-most bit is bit 0.
 𝒦 : ∀ {t} → Literal t → ⟦ t ⟧ₜ
 𝒦 (x ′b)  = x
@@ -73,12 +45,6 @@ open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromW
 𝒦 (xs ′x) = Vec.foldl Bits (λ bs b → (Bool.if b then 1𝔹 else 0𝔹) VecF.∷ bs) VecF.[] xs
 𝒦 (x ′a)  = Vec.replicate (𝒦 x)
 
-
-fetch : ∀ {n} ts → ⟦ tuple n ts ⟧ₜ → ∀ i → ⟦ Vec.lookup ts i ⟧ₜ
-fetch (_ ∷ [])     x        zero    = x
-fetch (_ ∷ _ ∷ _)  (x , xs) zero    = x
-fetch (_ ∷ t ∷ ts) (x , xs) (suc i) = fetch (t ∷ ts) xs i
-
 updateAt : ∀ {n} ts i → ⟦ Vec.lookup ts i ⟧ₜ → ⟦ tuple n ts ⟧ₜ → ⟦ tuple n ts ⟧ₜ
 updateAt (_ ∷ [])     zero    v _        = v
 updateAt (_ ∷ _ ∷ _)  zero    v (_ , xs) = v , xs