diff options
| -rw-r--r-- | Everything.agda | 11 | ||||
| -rw-r--r-- | src/Helium/Instructions/Base.agda (renamed from src/Helium/Data/Pseudocode.agda) | 4 | ||||
| -rw-r--r-- | src/Helium/Instructions/Core.agda (renamed from src/Helium/Instructions.agda) | 4 |
3 files changed, 8 insertions, 11 deletions
diff --git a/Everything.agda b/Everything.agda index c88f419..f3f1bda 100644 --- a/Everything.agda +++ b/Everything.agda @@ -48,20 +48,17 @@ import Helium.Algebra.Ordered.StrictTotal.Structures -- Some more algebraic structures import Helium.Algebra.Structures --- Definition of instructions using the Armv8-M pseudocode. -import Helium.Data.Pseudocode - -- Definition of the Armv8-M pseudocode. import Helium.Data.Pseudocode.Core -- Definition of types and operations used by the Armv8-M pseudocode. import Helium.Data.Pseudocode.Types --- Definitions of a subset of Armv8-M instructions. -import Helium.Instructions +-- Definition of instructions using the Armv8-M pseudocode. +import Helium.Instructions.Base --- Denotational semantics of Armv8-M instructions. -import Helium.Semantics.Denotational +-- Definitions of the data for a subset of Armv8-M instructions. +import Helium.Instructions.Core -- Base definitions for the denotational semantics. import Helium.Semantics.Denotational.Core diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Instructions/Base.agda index 9f936f2..8ec4073 100644 --- a/src/Helium/Data/Pseudocode.agda +++ b/src/Helium/Instructions/Base.agda @@ -6,7 +6,7 @@ {-# OPTIONS --safe --without-K #-} -module Helium.Data.Pseudocode where +module Helium.Instructions.Base where open import Data.Bool as Bool using (true; false) open import Data.Fin as Fin using (Fin; Fin′; zero; suc; toℕ) @@ -18,7 +18,7 @@ open import Data.Vec.Relation.Unary.All using (All; []; _∷_) open import Function using (_$_) open import Helium.Data.Pseudocode.Core as Core public hiding (module Code) -import Helium.Instructions as Instr +import Helium.Instructions.Core as Instr import Relation.Binary.PropositionalEquality as P open import Relation.Nullary.Decidable.Core using (True) diff --git a/src/Helium/Instructions.agda b/src/Helium/Instructions/Core.agda index ebe3f32..466a396 100644 --- a/src/Helium/Instructions.agda +++ b/src/Helium/Instructions/Core.agda @@ -1,12 +1,12 @@ ------------------------------------------------------------------------ -- Agda Helium -- --- Definitions of a subset of Armv8-M instructions. +-- Definitions of the data for a subset of Armv8-M instructions. ------------------------------------------------------------------------ {-# OPTIONS --safe --without-K #-} -module Helium.Instructions where +module Helium.Instructions.Core where open import Data.Bool open import Data.Fin |