Add all-in-one import for Hoare logic semantics.

2 files changed, 54 insertions, 2 deletions

diff --git a/src/Helium/Semantics/Axiomatic.agda b/src/Helium/Semantics/Axiomatic.agda
new file mode 100644
index 0000000..dfac609
--- /dev/null
+++ b/src/Helium/Semantics/Axiomatic.agda
@@ -0,0 +1,52 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Semantics for the Armv8-M pseudocode using Hoare triples.
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Data.Pseudocode.Algebra using (Pseudocode)
+
+module Helium.Semantics.Axiomatic
+  {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
+  (pseudocode : Pseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
+  where
+
+open import Helium.Data.Pseudocode.Algebra.Properties pseudocode
+
+open import Agda.Builtin.FromNat
+open import Data.Nat using (ℕ)
+import Data.Nat.Literals as ℕₗ
+import Data.Unit
+open import Data.Vec using (Vec)
+open import Helium.Data.Pseudocode.Core
+import Helium.Semantics.Axiomatic.Core rawPseudocode as Core
+import Helium.Semantics.Axiomatic.Assertion rawPseudocode as Assertion
+import Helium.Semantics.Axiomatic.Term rawPseudocode as Term
+import Helium.Semantics.Axiomatic.Triple rawPseudocode as Triple
+
+open Assertion.Construct public
+open Assertion.Assertion public
+
+open Assertion public
+  using (Assertion)
+
+open Term.Term public
+open Term public
+  using (Term)
+
+instance
+  numberℕ : Number ℕ
+  numberℕ = ℕₗ.number
+
+2≉0 : 2 ℝ.≉ 0
+2≉0 = ℝ.>⇒≉ (ℝ.n≉0⇒0<+n 2)
+
+HoareTriple : ∀ {o} {Σ : Vec Type o} {n} {Γ : Vec Type n} {m} {Δ : Vec Type m} → Assertion Σ Γ Δ → Code.Statement Σ Γ → Assertion Σ Γ Δ → Set _
+HoareTriple = Triple.HoareTriple 2≉0
+
+ℰ : ∀ {o} {Σ : Vec Type o} {n} {Γ : Vec Type n} {m} {Δ : Vec Type m} {t : Type} → Code.Expression Σ Γ t → Term Σ Γ Δ t
+ℰ = Term.ℰ 2≉0
+
+open Triple.HoareTriple 2≉0 public
diff --git a/src/Helium/Semantics/Axiomatic/Term.agda b/src/Helium/Semantics/Axiomatic/Term.agda
index 57dad92..eaefb89 100644
--- a/src/Helium/Semantics/Axiomatic/Term.agda
+++ b/src/Helium/Semantics/Axiomatic/Term.agda
@@ -32,7 +32,7 @@ import Helium.Data.Pseudocode.Manipulate as M
 open import Helium.Semantics.Axiomatic.Core rawPseudocode
 open import Level using (_⊔_; lift; lower)
 open import Relation.Binary.PropositionalEquality hiding ([_]) renaming (subst to ≡-subst)
-open import Relation.Nullary using (does; yes; no; ¬_)
+open import Relation.Nullary using (does; yes; no)
 open import Relation.Nullary.Decidable.Core using (True; toWitness)
 open import Relation.Nullary.Negation using (contradiction)
 
@@ -216,7 +216,7 @@ cast τ eq = func₁ (cast′ τ eq)
 [ real ][ t ^ n ] = func₁ (lift ∘ (ℝ′._^′ n) ∘ lower) t
 
 2≉0 : Set _
-2≉0 = ¬ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ
+2≉0 = 2 ℝ′.×′ 1ℝ ℝ.≉ 0ℝ
 
 [_][_>>_] : 2≉0 → Term Σ Γ Δ int → ℕ → Term Σ Γ Δ int
 [ 2≉0 ][ t >> n ] = func₁ (lift ∘ ⌊_⌋ ∘ (ℝ._* 2≉0 ℝ.⁻¹ ℝ′.^′ n) ∘ _/1 ∘ lower) t