Syntax highlighting

Author: MaximilianAlgehed

docs/Manual.md

@@ -532,8 +532,8 @@ match p $ \ x y -> x <. y
 In previous sections we provided some types for several of the library functions: `constrained`, `match`,
 
 
-```
-constrained:: HasSpec a => (Term a -> Pred) -> Specification a
+```haskell
+constrained :: HasSpec a => (Term a -> Pred) -> Specification a
 
 match :: (HasSpec a, HasSpec b) =>
          Term (a,b) -> (Term a -> Term b -> Pred) -> Pred
@@ -542,14 +542,14 @@ match :: (HasSpec a, HasSpec b) =>
 It turns out, that these functions would be much more useful with more general types. This also applies to some other
 library functions (`reify`, `caseOn`, etc.) we have not yet introduced. The general type of `constrained` is:
 
-```
-constrained:: (IsPred p, HasSpec a) => (Term a -> p) -> Specification a
+```haskell
+constrained :: (IsPred p, HasSpec a) => (Term a -> p) -> Specification a
 ```
 
 This general type allows the function passed to `constrained` to be any function, that given a Term, returns any type that acts like a `Pred`.
 The class IsPred is defined as follows, and has 4 instances.
 
-```
+```haskell
 class Show p => IsPred p where
   toPred :: p -> Pred
 
@@ -615,7 +615,7 @@ type FunTy (MapList Term (ProductAsList a)) p = t1 -> t2 -> ... -> tn -> p
 
 `assert` lifts a `(Term Bool)` to a `Pred`.  by using the `IsPred` class, we can often get around using it, but it becomes necessary when we want to use the `And` operator, and the operands of `And` are a mix of `Pred`, `(Term Bool), and other operations. Here is a very simple use. Further examples illustrate its use in more challenging contexts.
 
-```
+```haskell
 ex5 :: Specification [Int]
 ex5 = constrained $ \ xs -> assert $ elem_ 7 xs
 ```
@@ -628,7 +628,7 @@ Note that `elem_` is the function symbol corresponding to `Data.List.elem`.
 The library function `forAll` is used to impose a constraint on every element of a container type. There are
 three `Forallable` instances in the Base system.
 
-```
+```haskell
 class Forallable t e | t -> e where
 instance Ord k => Forallable (Map k v) (k, v)
 instance Ord a => Forallable (Set a) a
@@ -637,7 +637,7 @@ instance Forallable [a] a
 
 Here is an example of its use.
 
-```
+```haskell
 ex6 :: Specification [Int]
 ex6 = constrained $ \ xs ->
       forAll xs $ \ x -> [ x <=. 10, x >. 1]
@@ -683,7 +683,7 @@ The first use: `(reifies b a f)`,  says a term `b` can be obtained from a term `
 Here is an example of its use. Internally, it works by forcing the solution of `a` before solving for `b`, applying the `f` to
 the solution for `a`, and then constructing a `(Term b)` obtained from this value.
 
-```
+```haskell
 ex7 :: Specification (Int,[Int])
 ex7 = constrained $ \ pair ->
       match pair $ \ n xs ->
@@ -707,7 +707,7 @@ True
 The second operation `reify` can be defined using `reifies` by placing an existential constraint on the range of the function.
 Here is an example of the use of `reify`
 
-```
+```haskell
 ex8 :: Specification ([Int],[Int])
 ex8 = constrained $ \ pair ->
       match pair $ \ xs1 xs2 ->
@@ -737,7 +737,7 @@ True
 The third operation `assertReified` can be used to place a boolean constraint on the existential.
 Here is an example of its use.
 
-```
+```haskell
 ex9 :: Specification Int
 ex9 = constrained $ \x ->
   [ assert $ x <=. 10
@@ -770,7 +770,7 @@ Sometimes we want to choose between several different specifications for the sam
 Let's look at the first. Multiple constuctors from the same type. This uses the `caseOn` library functions and its two
 helper functions `branch` (where each constructor is choosen equally) and `branchW` (where we can give weights, to determine the frequency each constructor is choosen). The type of `caseOn`
 
-```
+```haskell
 caseOn
   :: Term a
      -> FunTy
@@ -785,15 +785,15 @@ unweighted using `(branch ...)`, where the `...` is a function with *m* paramete
 subcomponents of that constructor). First we introduce a sum of products type `Three` and use the GHC.Generics
 instance to derive the HasSpec instance.
 
-```
+```haskell
 data Three = One Int | Two Bool | Three Int deriving (Ord, Eq, Show, Generic)
 instance HasSimpleRep Three
 instance HasSpec Three
 ```
 
 Here is an example using the mechanism with no weights (`branch`), where every branch is equilikely.
 
-```
+```haskell
 ex10 :: Specification Three
 ex10 = constrained $ \ three ->
        caseOn three
@@ -807,7 +807,7 @@ expects the branches to be in the same order the constructors are introduced in
 
 Here is another example using the weighted mechanism (`branchW`).
 
-```
+```haskell
 ex11 :: Specification Three
 ex11 = constrained $ \ three ->
        caseOn three
@@ -824,13 +824,13 @@ The second way to specify disjunctions is to choose `chooseSpec`, where the two
 type, but are distinguished logically by the two input specifications. The type of
 `chooseSpec` is as follows, where the `Int` determines the frequency of each choice.
 
-```
-chooseSpec:: HasSpec a => (Int, Specification a) -> (Int, Specification a) -> Specification a
+```haskell
+chooseSpec :: HasSpec a => (Int, Specification a) -> (Int, Specification a) -> Specification a
 ```
 
 Here is an example.
 
-```
+```haskell
 ex12 :: Specification (Int,[Int])
 ex12 = chooseSpec
          (5, constrained $ \ pair ->
@@ -871,7 +871,7 @@ defined interms of the un-primed function and `match`, and the second defined nt
 
 The primed version of `forAll` is `forAll'`
 
-```
+```haskell
 ex13a :: Specification [(Int,Int)]
 ex13a = constrained $ \ xs ->
       forAll xs $ \ x -> match x $ \ a b -> a ==. negate b
@@ -883,7 +883,7 @@ ex13b = constrained $ \ xs ->
 
 The primed version of `constrained` is `constrained'`
 
-```
+```haskell
 ex14a :: Specification (Int,Int,Int)
 ex14a = constrained $ \ triple ->
         match triple $ \ a b c -> [ b ==. a + lit 1, c ==. b + lit 1]
@@ -895,7 +895,7 @@ ex14b = constrained' $ \ a b c -> [ b ==. a + lit 1, c ==. b + lit 1]
 The primed version of `reify` is `reify'`
 
 
-```
+```haskell
 ex15a :: Specification (Int,Int,Int)
 ex15a = constrained $ \ triple ->
           match triple $ \ x1 x2 x3 ->
@@ -918,7 +918,7 @@ In Haskell we can define data types with multiple constructors, and constructors
 The library functions `onCon`, `sel`, and `isJust`, allow us to constrain such types in a way less verbose
 than using the `caseOn` library function. Consider the following
 
-```
+```haskell
 ex16 :: Specification Three
 ex16 = constrained $ \ three ->
        caseOn three
@@ -935,7 +935,7 @@ This requires that the GHC language directive`{-# LANGUAGE DataKinds #-}` be in
 Then apply it to a Term with the type returned by that constructor, followed by a Haskell function with one parameter
 for each subcomponent of that constructor, that returns a Pred. Here is `ex16` redone using three `onCon` predicates.
 
-```
+```haskell
 ex17:: Specification Three
 ex17 = constrained $ \ three ->
     [ onCon @"One" three (\ x -> x==. lit 1)
@@ -948,21 +948,21 @@ The real power of `onCon` is when you only want to constrain one (or a subset) o
 and the other constructors remain unconstrained. Here we only constrain the constructor `Three` and the constructors
 `One` and `Two` remain unconstrained.
 
-```
+```haskell
 ex18:: Specification Three
 ex18 = constrained $ \ three ->
        onCon @"Three" three ( \ x -> x==. lit 3)
 ```
 
 Here is another example where we only constrain the constructor `Just` of the maybe type.
-```
+```haskell
 ex19 :: Specification (Maybe Bool)
 ex19 = constrained $ \ mb -> onCon @"Just" mb (\ x -> x==. lit False)
 ```
 
 Haskell allows the definition of data types with named selectors. Here is an example.
 
-```
+```haskell
 data Dimensions
   where Dimensions ::
           { length :: Int
@@ -975,7 +975,7 @@ instance HasSpec Dimensions
 
 This introduces Haskell functions with types
 
-```
+```haskell
 length :: Dimensions -> Int
 width :: Dimensions -> Int
 depth :: Dimensions -> Int
@@ -986,14 +986,14 @@ instances, the we can use the `sel` library function to create lifted versions o
 the Haskell selector functions like this. Nothe that the lifted `width` uses the trailing
 under score convention: `width_` because it manipulates `Term`s not values.
 
-```
+```haskell
 width_ :: Term Dimensions -> Term Int
 width_ d = sel @1 d
 ```
 
 This requires the `DataKinds` directive, and importing `GHC.Generics` and `GHC.TypeLits` to work.
 
-```
+```haskell
 {-# LANGUAGE DataKinds #-}
 import GHC.Generics
 import GHC.TypeLits
@@ -1003,15 +1003,15 @@ When we type-apply the library function `sel` to a type-level `Natural` number l
 selects the `ith` selector function. The selectors are numbered from `0` to `n-1` . Selection
 can always be expressed using `match` like this:
 
-```
+```haskell
 ex20a :: Specification Dimensions
 ex20a = constrained $ \ d ->
         match d $ \ l w d -> [ l >. lit 10, w ==. lit 5, d <. lit 20]
 ```
 
 which can be reexpressed using `sel` as this.
 
-```
+```haskell
 ex20b :: Specification Dimensions
 ex20b = constrained $ \ d ->
         [sel @0 d >. lit 10
@@ -1022,7 +1022,7 @@ ex20b = constrained $ \ d ->
 When we wish to constrain just a subset of the subcomponents, selectors make it possible
 to write more concise `Specification`s.
 
-```
+```haskell
 ex21 :: Specification Dimensions
 ex21 = constrained $ \ d -> width_ d ==. lit 1
 ```
@@ -1038,7 +1038,7 @@ Term level names that were assigned to the Haskell variables. This means the err
 understand. For example consider the over constrained specification. It is over constrained because
 `left` cannot be simultaneously equal to `right` and `right + lit 1`
 
-```
+```haskell
 ex22a :: Specification (Int,Int)
 ex22a = constrained $ \ pair ->
        match pair $ \ left right ->
@@ -1061,14 +1061,14 @@ Note the error message is in terms of the internal Term name `v1`. Which is not
 
 To make error messages clearer we can name Haskell lambda bound variables using `[var|left|]` instead of just `left`.  In order to do this we must have the following directives in our file.
 
-```
+```haskell
 {-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE ViewPatterns #-}
 ```
 
 Here is the same example using this naming schema.
 
-```
+```haskell
 ex22b :: Specification (Int,Int)
 ex22b = constrained $ \ [var|pair|] ->
          match pair $ \ [var|left|] [var|right|] -> [ left ==. right, left ==. right + lit 1]
@@ -1099,7 +1099,7 @@ another internal number `y`, such that, `x` is equal to `y + y + 1`
 
 Here is an example.
 
-```
+```haskell
 ex22 :: Specification Int
 ex22 = constrained $ \ [var|oddx|] ->
          unsafeExists
@@ -1114,7 +1114,7 @@ that tells how to compute the hidden variable from the values returned by solvin
 The second is the normal use of a Haskell lambda expression to introduce a Term variable
 naming the hidden variable. Here is an example.
 
-```
+```haskell
 ex23 :: Specification Int
 ex23 = ExplainSpec ["odd via (y+y+1)"] $
        constrained $ \ [var|oddx|] ->
@@ -1150,15 +1150,15 @@ If one has a term `x` with type `(Term Bool)` one could use the value of this te
 define a Specification conditional on this term by using the `(caseOn x ...)` library function.
 There are two more concise library function one can use instead.
 
-```
+```haskell
 whenTrue :: IsPred p => Term Bool -> p -> Pred
 ifElse :: (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
 ```
 
 For example consider the data type `Rectangle` where the selector `square` indicates
 that the rectangle has equal length width and length.
 
-```
+```haskell
 data Rectangle = Rectangle { wid :: Int, len :: Int, square :: Bool}
     deriving (Show, Eq,Generic)
 instance HasSimpleRep Rectangle
@@ -1167,7 +1167,7 @@ instance HasSpec Rectangle
 
 We can enforce this in a specification as follows.
 
-```
+```haskell
 ex26 :: Specification Rectangle
 ex26 = constrained' $ \ wid len square ->
  [ assert $ wid >=. lit 0
@@ -1180,7 +1180,7 @@ Note that there are no constraints relating `wid` and `len` if the selector `squ
 The library function `ifElse` allows two separate sets of constraints, one when the
 `square` is `True` and a completely separate set when `square` is `False`
 
-```
+```haskell
 ex27 :: Specification Rectangle
 ex27 = constrained' $ \ wid len square ->
   ifElse square
@@ -1197,15 +1197,15 @@ ex27 = constrained' $ \ wid len square ->
 Explanations allow the writer of a specification to add textual message, that can be used
 if solving a specification fails. These library functions have type
 
-```
+```haskell
 explanation   :: NonEmpty String -> Pred -> Pred
 assertExplain :: IsPred p => NonEmpty String -> p -> Pred
 ExplainSpec   :: [String] -> Specification a -> Specification a
 ```
 
 Here is a specification with no explanations
 
-```
+```haskell
 ex28a :: Specification (Set Int)
 ex28a = constrained $ \ s ->
        [ assert $ member_ (lit 5) s
@@ -1224,7 +1224,7 @@ While combining 2 SetSpecs
 
 By adding an `ExplainSpec` like this
 
-```
+```haskell
 ex28b :: Specification (Set Int)
 ex28b = ExplainSpec ["5 must be in the set"] $
         constrained $ \ s ->
@@ -1245,7 +1245,7 @@ While combining 2 SetSpecs
   (SetSpec must=[ 5 ] elem=TrueSpec @(Int) size=TrueSpec @(Integer))
 ```
 
-```
+```haskell
 ex28c :: Specification (Set Int)
 ex28c =
         constrained $ \ s -> explanation (pure "5 must be in the set")
@@ -1272,7 +1272,7 @@ There are a number of library functions that create specifications directly
 and do not use the `constrained` library function. These are particulary useful
 in conjunction with the library function `satisfies` which converts a `Specification` into a `Pred`
 
-```
+```haskell
 satisfies :: HasSpec a => Term a -> Specification a -> Pred
 equalSpec :: a -> Specification a
 notEqualSpec :: HasSpec a => a -> Specification a
@@ -1286,7 +1286,7 @@ cardinality :: (Number Integer, HasSpec a) => Specification a -> Specification I
 
 Here is an example of the use of `satisfies` in conjunction with `notMemberSpec`
 
-```
+```haskell
 ex29 :: Specification Int
 ex29 = constrained $ \ x ->
        [ assert $ x >=. lit 0