Refactor to group instruction definitions together

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