Skip to content

Add documentation Manual.md and DesignPrinciples.md #5044

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Add documentation Manual.md and DesignPrinciples.md #5044

wants to merge 3 commits into from

Conversation

TimSheard
Copy link
Contributor

We add two documents that describe the constrained-generators module

  1. Manual.md. Describes how to write constraints using the system. Attempts to document with an example all the library functions for creating Specifications.
  2. DesignPrinciples.md . Describes the important principles that make the implementation work. Builds a simplified version of the system without generics and other bells and whistles in the subdirectory src/Constrained/Min/ , Documents all the important features of the original implementation without the extraneous complications of Generics, Multiple Integral HasSpec instances, Higher order Function Symbols, arbitrary arity (only unary and binary) contexts, embedding explanations, etc.

Incorporates PR #4985, so all documentation is added in one PR, and documents can cross reference each other.

Checklist

  • Commits in meaningful sequence and with useful messages.
  • Tests added or updated when needed.
  • CHANGELOG.md files updated for packages with externally visible changes.
    NOTE: New section is never added with the code changes. (See RELEASING.md).
  • Versions updated in .cabal and CHANGELOG.md files when necessary, according to the
    versioning process.
  • Version bounds in .cabal files updated when necessary.
    NOTE: If bounds change in a cabal file, that package itself must have a version increase. (See RELEASING.md).
  • Code formatted (use scripts/fourmolize.sh).
  • Cabal files formatted (use scripts/cabal-format.sh).
  • CDDL files are up to date (use scripts/gen-cddl.sh)
  • hie.yaml updated (use scripts/gen-hie.sh).
  • Self-reviewed the diff.

@TimSheard TimSheard requested a review from a team as a code owner May 14, 2025 20:34
@TimSheard TimSheard force-pushed the ts-constrained-min-model branch from c0eec76 to a24809b Compare May 14, 2025 20:41
@MaximilianAlgehed
Copy link
Collaborator

@TimSheard it looks like you've formatted this with the old version of fourmolu

@TimSheard TimSheard force-pushed the ts-constrained-min-model branch 2 times, most recently from d1be307 to df8f7d4 Compare May 15, 2025 16:37
@TimSheard TimSheard force-pushed the ts-constrained-min-model branch 2 times, most recently from 457faef to 7094b77 Compare May 16, 2025 18:09
lehins
lehins requested changes May 16, 2025
View reviewed changes
Copy link
Collaborator

@lehins lehins left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am not really keen on adding another 3K lines of code that will be unused in Ledger. We should create a separate sub library in the constraint-generators that will contain all of the example code and manuals.

In other words, could you please follow an example of a testlib from one of our packages to add a separate sub library to constraint-generators that will include all of the code that is being added in this PR.

@TimSheard TimSheard force-pushed the ts-constrained-min-model branch from 4601aee to cf7a5a5 Compare May 19, 2025 14:46
MaximilianAlgehed
MaximilianAlgehed reviewed May 20, 2025
View reviewed changes
Copy link
Collaborator

@MaximilianAlgehed MaximilianAlgehed left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As far as I got today. I'll try to have a look at the minimal implementation after lunch.

libs/constrained-generators/src/Constrained/Base.hs
@@ -749,7 +749,7 @@ class Forallable t e | t -> e where
-- IsPred

class Show p => IsPred p where
toPred :: p -> Pred
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would prefer not to change this and keep Pred wherever possible.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am not sure I understand what you are getting at. Are you suggesting not using IsPred at all in the Minimal implementation?

libs/constrained-generators/constrained-generators.cabal Outdated
Comment on lines 135 to 140
-Wcompat
-Wincomplete-record-updates
-Wincomplete-uni-patterns
-Wpartial-fields
-Wredundant-constraints
-Wunused-packages
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
-Wcompat
-Wincomplete-record-updates
-Wincomplete-uni-patterns
-Wpartial-fields
-Wredundant-constraints
-Wunused-packages

MaximilianAlgehed
MaximilianAlgehed reviewed May 20, 2025
View reviewed changes
docs/constrained-generators/manual.md

The function symbols of `Bool` are:

1. `or_ :: Term Bool -> Term Bool -> Term Bool`
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm still not super keen on us supporting or_ as it behaves quite counterintuitively...

Also, to be consistent with the rest of the design it should be called (||.)

docs/constrained-generators/manual.md
Comment on lines +335 to +339
Now this isn't a very good test either, since the precedent is alway true. A better solution would be to
generate a mix, where the precedent is True most of the time, but sometimes False.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

C.f. my other comment about this not being true.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, I'd like to make this better. Lets talk about that.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

perils of overconstraining
using classify to observe this
using cover.

@TimSheard TimSheard mentioned this pull request May 20, 2025
Closed
6 tasks
MaximilianAlgehed
MaximilianAlgehed reviewed May 21, 2025
View reviewed changes
docs/constrained-generators/manual.md
Where the `classify` statistics are reported.

<a id="weights"></a>
### Classify with weights example.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe talk also about using cover here to actually require a specific distribution. This can be very helpful to make sure you're not over-constraining your generators.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good idea, I'll try and come up with an example.

libs/constrained-generators/testlib/Test/Min/Base.hs Outdated
Comment on lines 149 to 151
class Container t e | t -> e where
fromForAllSpec :: (HasSpec t, HasSpec e) => Spec e -> Spec t
forAllToList :: t -> [e]
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In this code, do we use forAll on anything other than Set? In which case we could simplify this too so that forAll only supports Set and we could explain that you can easily generalize it if you want in text.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We could do that. Or we could make it clear, that in the Minimal implementation it only is used on Set, but in the full implementation it is used in List and Map as well.

libs/constrained-generators/testlib/Test/Min/Model.hs Outdated

data IntegerSym (dom :: [Type]) rng where
PlusW :: IntegerSym '[Integer, Integer] Integer
MinusW :: IntegerSym '[Integer, Integer] Integer
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What about Negate instead?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That would give us more examples of different arities

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Didn't think about that. But we do use both (+.) and (-.) in the some examples.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

go back to negate

libs/constrained-generators/testlib/Test/Min/Model.hs Outdated
GenError xs -> ErrorSpec (catMessageList xs)
FatalError es -> error $ catMessages es

------- Stages of simplifying -------------------------------
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's a shame we need a bunch of this stuff for this "simplified" version of the system to work. I'd like to sit down once we've shrunk the code-base here some more and see if I can get rid of some of this.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The problem is that making a SolverPlan, requires all this stuff. We don't talk about how we do that, only what the result looks like, and how it is used.

@TimSheard TimSheard force-pushed the ts-constrained-min-model branch 2 times, most recently from 4df2893 to 0df0af3 Compare May 22, 2025 16:14
TimSheard added 3 commits June 4, 2025 08:56
@TimSheard
Added sub directory src/Constrained/Min where we keep a minimal versi…
d913091 
…on of the system.

The idea is that is easier to explain, since it doesn't have things like Generics.
It consists of Constrained.Min.Base.hs, Constraied.Min.Syntax.hs, Constrained.Min.Model.hs,
and Constrained.Min.Tuple.hs
Added the file docs/constrained/DesignPrinciples.md that describes this minimal system.
@TimSheard
Describe computeSpecSimplified, the use of SolverPlan and propagageS…
90eeb3a 
…pec.
@TimSheard
Added a second document docs/constrained_generators/manual.md
b40b303 
This is a basic manual about how to write constraints, but does not
go into details about how the system is implemented.
@TimSheard TimSheard force-pushed the ts-constrained-min-model branch from 516a803 to b40b303 Compare June 4, 2025 16:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@MaximilianAlgehed MaximilianAlgehed MaximilianAlgehed left review comments

@lehins lehins lehins requested changes

@neilmayhew neilmayhew Awaiting requested review from neilmayhew

Requested changes must be addressed to merge this pull request.

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@TimSheard @MaximilianAlgehed @lehins