diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-02-13 14:01:44 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-02-13 14:27:00 +0000 |
| commit | bfcbca52a117ec207addf629f1cada93e0f12e02 (patch) | |
| tree | e3209a97003a19ffef1d5b1c479fecfe0cd69af4 /Everything.agda | |
| parent | 687f7031131ac12bd382be831114661be785dd0d (diff) | |
Refactor to group instruction definitions together
Diffstat (limited to 'Everything.agda')
| -rw-r--r-- | Everything.agda | 11 |
1 files changed, 4 insertions, 7 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 |