Improve documentation in .Primitive modules (#1479)

Author: MatthewDaggitt

README.agda

@@ -17,14 +17,32 @@ module README where
 ------------------------------------------------------------------------
 
 -- This version of the library has been tested using Agda 2.6.1 and
--- 2.6.1.1.
+-- 2.6.1.3.
 
 -- The library comes with a .agda-lib file, for use with the library
 -- management system.
 
 -- Currently the library does not support the JavaScript compiler
 -- backend.
 
+------------------------------------------------------------------------
+-- Stability guarantees
+------------------------------------------------------------------------
+
+-- We do our best to adhere to the spirit of semantic versioning in that
+-- minor versions should not break people's code. This applies to the
+-- the entire library with one exception: modules with names that end in
+-- either ".Core" or ".Primitive".
+
+-- The former have (mostly) been created to avoid mutual recursion
+-- between modules and the latter to bind primitive operations to the
+-- more efficient operations supplied by the relevant backend.
+
+-- These modules may undergo backwards incompatible changes between
+-- minor versions and therefore are imported directly at your own risk.
+-- Instead their contents should be accessed by their parent module,
+-- whose interface will remain stable.
+
 ------------------------------------------------------------------------
 -- High-level overview of contents
 ------------------------------------------------------------------------
@@ -247,15 +265,6 @@ import README.Text.Regex
 
 import README.Text.Tabular
 
-------------------------------------------------------------------------
--- Core modules
-------------------------------------------------------------------------
-
--- Some modules have names ending in ".Core". These modules are
--- internal, and have (mostly) been created to avoid mutual recursion
--- between modules. They should not be imported directly; their
--- contents are reexported by other modules.
-
 ------------------------------------------------------------------------
 -- All library modules
 ------------------------------------------------------------------------

src/IO/Primitive.agda

@@ -4,6 +4,8 @@
 -- Primitive IO: simple bindings to Haskell types and functions
 ------------------------------------------------------------------------
 
+-- NOTE: the contents of this module should be accessed via `IO`.
+
 {-# OPTIONS --without-K #-}
 
 module IO.Primitive where

src/IO/Primitive/Finite.agda

@@ -9,6 +9,9 @@
 
 module IO.Primitive.Finite where
 
+-- NOTE: the contents of this module should be accessed via `IO` or
+-- `IO.Finite`.
+
 open import Agda.Builtin.IO
 open import Agda.Builtin.String
 open import Agda.Builtin.Unit using () renaming (⊤ to Unit)

src/IO/Primitive/Infinite.agda

@@ -9,6 +9,9 @@
 
 module IO.Primitive.Infinite where
 
+-- NOTE: the contents of this module should be accessed via `IO` or
+-- `IO.Infinite`.
+
 open import Codata.Musical.Costring
 open import Agda.Builtin.String
 open import Agda.Builtin.Unit renaming (⊤ to Unit)