Introduce Everything.agda to aid in overall compilation.

7 files changed, 96 insertions, 2 deletions

diff --git a/Everything.agda b/Everything.agda
new file mode 100644
index 0000000..5f0a173
--- /dev/null
+++ b/Everything.agda
@@ -0,0 +1,20 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- All library modules, along with short descriptions.
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+module Everything where
+
+-- Definition of types and operations used by the Armv8-M pseudocode.
+import Helium.Data.Pseudocode
+
+-- Definitions of a subset of Armv8-M instructions.
+import Helium.Instructions
+
+import Helium.Semantics.Denotational
+
+-- Base definitions for the denotational semantics.
+import Helium.Semantics.Denotational.Core
diff --git a/agda-helium.agda-lib b/agda-helium.agda-lib
new file mode 100644
index 0000000..bec951d
--- /dev/null
+++ b/agda-helium.agda-lib
@@ -0,0 +1,3 @@
+name: agda-helium-0.1
+depend: standard-library-1.7.1
+include: src
diff --git a/guix.scm b/guix.scm
new file mode 100644
index 0000000..c4c6565
--- /dev/null
+++ b/guix.scm
@@ -0,0 +1,49 @@
+(use-modules (gnu packages agda)
+             (guix build-system copy)
+             (guix gexp)
+             (guix git-download)
+             ((guix licenses) #:prefix license:)
+             (guix packages)
+             (yellowsquid packages agda))
+(define %source-dir (dirname (current-filename)))
+
+
+
+(define-public agda-helium
+  (package
+    (name "agda-helium")
+    (version "0.1")
+    (home-page "https://git.yellowsquid.uk/yellowsquid/helium.git")
+    (source (local-file %source-dir
+                        #:recursive? #t
+                        #:select? (git-predicate %source-dir)))
+    (build-system copy-build-system)
+    (inputs (list agda-stdlib))
+    (native-inputs (list agda))
+    (arguments
+     `(#:install-plan
+       '(("src" "/share/agda/lib/helium/" #:include-regexp ("\\.agdai?")))
+       #:phases
+       (modify-phases %standard-phases
+         (add-before 'install 'build
+           (lambda* (#:key inputs #:allow-other-keys)
+             (call-with-output-file "libraries"
+               (lambda (port)
+                 (format port
+                         "~a\n"
+                         (string-append
+                          (search-input-file
+                           inputs
+                           "/share/agda/lib/standard-library.agda-lib"))
+                          port)
+                 (display "./agda-helium.agda-lib\n" port)))
+             (invoke "agda"
+                     "--library-file=libraries"
+                     "--library=agda-helium"
+                     "-i."
+                     "Everything.agda"))))))
+    (synopsis "Semantics of the Arm M-profile Vector Extension (MVE) in Agda")
+    (description "")
+    (license license:expat)))
+
+agda-helium
diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Data/Pseudocode.agda
index 9982501..7e6f6dc 100644
--- a/src/Helium/Data/Pseudocode.agda
+++ b/src/Helium/Data/Pseudocode.agda
@@ -1,3 +1,9 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Definition of types and operations used by the Armv8-M pseudocode.
+------------------------------------------------------------------------
+
 {-# OPTIONS --safe --without-K #-}
 
 module Helium.Data.Pseudocode where
diff --git a/src/Helium/Instructions.agda b/src/Helium/Instructions.agda
index 5eba3f0..4bd02ac 100644
--- a/src/Helium/Instructions.agda
+++ b/src/Helium/Instructions.agda
@@ -1,3 +1,9 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Definitions of a subset of Armv8-M instructions.
+------------------------------------------------------------------------
+
 {-# OPTIONS --safe --without-K #-}
 
 module Helium.Instructions where
diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda
index fc93a26..c2a3f4f 100644
--- a/src/Helium/Semantics/Denotational.agda
+++ b/src/Helium/Semantics/Denotational.agda
@@ -1,3 +1,9 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Denotational semantics of Armv8-M instructions.
+------------------------------------------------------------------------
+
 {-# OPTIONS --safe --without-K #-}
 
 open import Helium.Data.Pseudocode
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index 54f0375..359fbd4 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -1,6 +1,10 @@
-{-# OPTIONS --safe --without-K #-}
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Base definitions for the denotational semantics.
+------------------------------------------------------------------------
 
-open import Helium.Data.Pseudocode
+{-# OPTIONS --safe --without-K #-}
 
 module Helium.Semantics.Denotational.Core
   {ℓ′}