Skip to content

Commit 0180f09

Browse files
No tools to maintain TOC
1 parent 0d17661 commit 0180f09

File tree

1 file changed

+6
-53
lines changed

1 file changed

+6
-53
lines changed

docs/Manual.md

Lines changed: 6 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -5,52 +5,6 @@ The markdown source of this file can be obtained
55
and all the examples in this file can be found
66
[here](https://github.com/input-output-hk/constrained-generators/blob/master/examples/Constrained/Examples/ManualExamples.hs).
77

8-
<!-- markdown-toc start - Don't edit this section. Run M-x markdown-toc-refresh-toc -->
9-
**Table of Contents**
10-
11-
- [Constrained Generators Manual](#constrained-generators-manual)
12-
- [Constrained Generators is a First-Order Logic](#constrained-generators-is-a-first-order-logic)
13-
- [Design Goals of the Library](#design-goals-of-the-library)
14-
- [HasSpec instances](#hasspec-instances)
15-
- [Building logic specifications using Haskell functions](#building-logic-specifications-using-haskell-functions)
16-
- [Another example using conjunction and simple arithmetic](#another-example-using-conjunction-and-simple-arithmetic)
17-
- [Function Symbols](#function-symbols)
18-
- [Predefined HasSpec instances and their function symbols.](#predefined-hasspec-instances-and-their-function-symbols)
19-
- [Function symbols for numeric types](#function-symbols-for-numeric-types)
20-
- [` Function symbols for Bool`](#-function-symbols-for-bool)
21-
- [Function symbols for List](#function-symbols-for-list)
22-
- [Function symbols for Set](#function-symbols-for-set)
23-
- [Function symbols for Map](#function-symbols-for-map)
24-
- [Generating from and checking against specifications](#generating-from-and-checking-against-specifications)
25-
- [How we solve the constraints](#how-we-solve-the-constraints)
26-
- [How to pick the variable order](#how-to-pick-the-variable-order)
27-
- [The total definition requirement ](#the-total-definition-requirement)
28-
- [Using Match to introduce new variables for subcomponents](#using-match-to-introduce-new-variables-for-subcomponents)
29-
- [Overloaded types in the library](#overloaded-types-in-the-library)
30-
- [Library functions to build Term, Pred, Specification](#library-functions-to-build-term-pred-specification)
31-
- [From Term to Pred](#from-term-to-pred)
32-
- [For all elements in a container type (List, Set, Map)](#for-all-elements-in-a-container-type-list-set-map)
33-
- [Reification](#reification)
34-
- [Disjunction, choosing between multiple things with the same type](#disjunction-choosing-between-multiple-things-with-the-same-type)
35-
- [Primed library functions which are compositions with match](#primed-library-functions-which-are-compositions-with-match)
36-
- [Constructors and Selectors](#constructors-and-selectors)
37-
- [Naming introduced lambda bound Term variables](#naming-introduced-lambda-bound-term-variables)
38-
- [Existential quantifiers](#existential-quantifiers)
39-
- [Conditionals](#conditionals)
40-
- [Explanations](#explanations)
41-
- [Operations to define and use Specifications](#operations-to-define-and-use-specifications)
42-
- [Utility functions](#utility-functions)
43-
- [Escape Hatch to QuickCheck Gen monad](#escape-hatch-to-quickcheck-gen-monad)
44-
- [Strategy for constraining a large type with many nested sub-components.](#strategy-for-constraining-a-large-type-with-many-nested-sub-components)
45-
- [Writing HasSpec instances by hand.](#writing-hasspec-instances-by-hand)
46-
- [Strategy 1 using GHC.Generics](#strategy-1-using-ghcgenerics)
47-
- [Strategy 2 writing your own SimpleRep instance](#strategy-2-writing-your-own-simplerep-instance)
48-
- [Strategy 3 defining the SimpleRep instance in terms of another type with a SimpleRep instance](#strategy-3-defining-the-simplerep-instance-in-terms-of-another-type-with-a-simplerep-instance)
49-
- [Strategy 4, bypassing SimpleRep, and write the HasSpec instance by Hand](#strategy-4-bypassing-simplerep-and-write-the-hasspec-instance-by-hand)
50-
- [A look into the internals of the system.](#a-look-into-the-internals-of-the-system)
51-
52-
<!-- markdown-toc end -->
53-
548
## Constrained Generators is a First-Order Logic
559

5610
A First-order typed logic (FOTL) has 4 components, where each component uses types to ensure well-formedness.
@@ -1544,14 +1498,13 @@ class Typeable (SimpleRep a) => HasSimpleRep a where
15441498

15451499
What kind of type lends itself to this strategy?
15461500
1. A type that has internal structure that enforces some internal invariants.
1547-
2. A type that has a -builder- function, that takes simple input, and constructs the internal struture.
1548-
3. A type that has an -accessor- function, that takes the internal structure, and returns the simple input.
1549-
4. A type where the -simple input- has a Sum-of-Products representation.
1501+
2. A type that has a _builder_ function, that takes simple input, and constructs the internal struture.
1502+
3. A type that has an _accessor_ function, that takes the internal structure, and returns the simple input.
1503+
4. A type where the _simple input_ has a Sum-of-Products representation.
15501504

1551-
Often the -builder- function is implemented as a Haskell Pattern. Here is an example that come from the Cardano Ledger.
1505+
Often the _builder_ function is implemented as a Haskell Pattern. Here is an example that come from the Cardano Ledger.
15521506
A lot of complicated stuff is not fully describe here, but the example gives an overview of how it works.
15531507

1554-
15551508
```haskell
15561509
-- NOTE: this is a representation of the `ShelleyTxOut` type. You can't
15571510
-- simply use the generics to derive the `SimpleRep` for `ShelleyTxOut`
@@ -1575,8 +1528,8 @@ instance (Era era, Val (Value era)) => HasSimpleRep (ShelleyTxOut era) where
15751528
instance (EraTxOut era, HasSpec (Value era)) => HasSpec (ShelleyTxOut era)
15761529
```
15771530

1578-
TODO add more explanation about the types. Much of the example of depends on properties of TxOut
1579-
that is not explained.
1531+
<!-- TODO add more explanation about the types. Much of the example of depends
1532+
on properties of TxOut that is not explained. -->
15801533

15811534
## Strategy 3 defining the SimpleRep instance in terms of another type with a SimpleRep instance
15821535

0 commit comments

Comments
 (0)