more cleanup pass

Author: MaximilianAlgehed

docs/Manual.md

@@ -53,7 +53,6 @@ and all the examples in this file can be found
 
 ## Constrained Generators is a First-Order Logic
 
-
 A First-order typed logic (FOTL) has 4 components, where each component uses types to ensure well-formedness.
 
 1. **Terms** consisting of
@@ -75,41 +74,45 @@ and _generate values_: `gen :: Specification T -> Gen T`. This supports
 property based testing where a completely random set of values may not be
 useful without having to write explicit random generation logic.
 
-
 ## Design Goals of the Library
 
 The system was designed to have several important properties
 
-1. A Specification determines a `QuickCheck` generator for generating random values subject to constraints.
-2. A Specification determines a check that a particular value meets all the specifications constraints.
-3. If a Specification is over-constrained, the system tries to explain where the conflict occurs.
-4. The system is compositional so specifications can be re-used
+1. A Specification determines a `QuickCheck` generator for generating random
+   values subject to constraints.
+2. A Specification determines a check that a particular value meets all the
+   specifications constraints.
+3. The system is compositional so specifications can be re-used
+4. If a Specification is over-constrained, the system tries to explain where
+   the conflict occurs.
 5. The system is extensible so that it can accomodate new types and functions.
 
-The first part is implemented by the function `genFromSpec`
-
+Point (1) is implemented by the following function
 ```haskell
 genFromSpec :: HasSpec a => Specification a -> QuickCheck.Gen a
 ```
-
-The second is implemented by the function `conformsToSpec`
-
+and (2) by this function:
 ```haskell
 conformsToSpec :: HasSpec a => a -> Specification a -> Bool
 ```
-
-The third is embodied by the error messages when solving a constraint fails
+(3) is captured succinctly by:
+```haskell
+instance Monoid (Specification t) -- This is far from the whole story...
+```
+while (4) is embodied primarily in the error messages given when `genFromSpec`
+fails. Point (5) meanwhile requires a bit of explanation and will in no small part
+be the subject of this document.
 
 The **Constrained Generators** system is implemented as an embeded domain
 specific language in Haskell.  The Terms, Predicates, Connectives, and
 Quantifiers of the first order logic are embedded into three Haskell datatypes
 (`Specification t`, `Term t`, and `Pred`). There is a rich (extendable) library
 of Haskell functions that can be used to define and construct values of these
-types.  The library is implemented in a such a way, that the four parts of the
-logic are defined in ways that are similar to Haskell expressions with type
-Bool.
+types. The library is implemented in a such a way, that the four parts of the
+logic are defined in ways that are similar (but different in important ways we
+will cover below) to Haskell expressions of type Bool.
 
-Let us look at a simple example, and study how this is done. Below is a Haskell
+Let us look at a simple example and study how this is done. Below is a Haskell
 declaration that defines a specification of a pair of Int (`p`) , subject to
 the constraint that the first component (`x`) is less than or equal to the
 second component (`y`) plus 2
@@ -124,9 +127,9 @@ leqPair = constrained $ \ p ->
 The library uses Haskell lambda expressions to introduce variables in the Term
 language of the system, and Haskell functions to build `Term`s and
 `Predicate`s. The Haskell function `lit` takes Haskell values and turns them
-into constants in the Term language. We give monomorphic types to the Haskell
-functions used in the above definitions. We discuss more general types in a
-[later section](#overloaded).
+into constants in the Term language. We'll give partially monomorphized types
+to the Haskell functions used in the above definitions. We discuss more general
+types in a [later section](#overloaded).
 
 ```haskell
 constrained :: HasSpec a => (Term a -> Pred) -> Specification a
@@ -140,13 +143,15 @@ assert :: Term Bool -> Pred
 (<=.) :: OrdLike a => Term a -> Term a -> Term Bool
 ```
 
-The Haskell Constraint `HasSpec a` states that the type `a` has been admitted to the system as one of the types
-that can be subject to constraints. The system comes with a large set of `HasSpec` instances, including ones for:
+The Haskell Constraint `HasSpec a` states that the type `a` has been admitted
+to the system as one of the types that can be subject to constraints. The
+system comes with a large set of `HasSpec` instances for types in `base` and
+`containers`, including ones for:
 
 1. Bool
 2. Tuples
 3. Sums
-4. Numeric types (Int, Integer, Natural, Int8, Int16, Int32, Int64, Word8, Word16, Word32, Word64)
+4. Numeric types (Int, Integer, Natural, Int/Word{8,16,32,64})
 5. Lists
 6. Maps
 7. Sets
@@ -157,19 +162,24 @@ that can be subject to constraints. The system comes with a large set of `HasSpe
 
 ## HasSpec instances
 
-`HasSpec` instances can always be added to admit more types. Any type with a `GHC.Generics(Generic)` instance can be
-given a default instance by using its Sum-of-Products generic definition. In the Cardano Ledger System
-over 200 types in the Ledger code base have been given `HasSpec` instances, either by using the `GHC.Generics` path, or by writing the instances by hand.
+`HasSpec` instances can always be added to admit more types. Any type with a
+`Generic` instance can be given a default instance by using its generic
+definition - provided that the types it uses have `HasSpec` instances. In the
+Cardano Ledger System over 200 types in the Ledger code base have been given
+`HasSpec` instances, either by using the `GHC.Generics` path, or by writing the
+instances by hand (more on this later).
 
 ## Building logic specifications using Haskell functions
 
-Note that `constrained` and `match` take functions, which abstract over terms, and return `Specification` and `Pred`.
-Using the library functions, variables in the Term language are always introduced using Haskell lambda abstractions. And the library
-functions combine these into Terms, Preds, and Specifications.
+Note that `constrained` and `match` take functions, which abstract over terms,
+and return `Specification` and `Pred`. Using the library functions, variables
+in the Term language are always introduced using Haskell lambda abstractions.
+And the library functions combine these into Terms, Preds, and Specifications.
 
 ## Another example using conjunction and simple arithmetic
 
-Suppose we want to put more than one simple condition on the pair of Ints. We would do that using the connective `And` that converts a `[Pred]` into a `Pred`
+Suppose we want to put more than one simple condition on the pair of Ints. We
+would do that using the connective `And` that converts a `[Pred]` into a `Pred`
 
 ```haskell
 sumPair :: Specification (Int, Int)
@@ -183,7 +193,7 @@ sumPair = constrained $ \p ->
 ```
 
 This example also re-illustrates that `(Term Int)` has a (partial) Num instance, and that we can constrain
-multiple (different) variables using simple `Num` methods (`(+)`, `(-)`,  and `negate`). Note also
+multiple (different) variables using simple `Num` methods (`(+)`, `(-)`, `(*)`, and `negate`). Note also
 the operator: `(==.) :: (Eq n, HasSpec n) => Term n -> Term n -> Term Bool`
 
 ## Function Symbols