first pass at implementing some basic csp exercises

[williamdemeo]

So far there's no connection between this implementation of these small, concrete, relational-hom-formulated csp problems and the general types implemented in the FiniteCSP module.

Nonetheless, I'm committing these examples to help guide us as we develop the FiniteCSP module, since the types we define in FiniteCSP should be useful for modeling and solving small, concrete csp exercises such as those in CSPexercises.lagda.

[williamdemeo]

Good ideas. Thanks for the guidance. I'll refactor tomorrow.

On Wed, 28 Jul 2021, 22:15 Jacques Carette, @.***> wrote:

@.**** commented on this pull request.

Looks good. Although I do tend to put exercises and examples outside rather than inside a library, for my user's benefit. i.e. Exercises.UniversalAlgebra.Complexity.CSP and Examples.UniversalAlgebra.Structures. Now, sometimes some examples are more than that - they are instances (or constructions), and then they belong inside, and named thus.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/ualib/agda-algebras/pull/97#pullrequestreview-717425754, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA25MJCTR3R2W6EPEC4AV43T2BQONANCNFSM5BFBGWAA .

[williamdemeo]

But it seems if I use a names like Exercises.UniversalAlgebra.Complexity.CSP there will be module name conflicts if, e.g., I have a module called UniversalAlgebra.Complexity.CSP and if some other module wants to import both. That's why I chose names like ExamplesOfSignatures, and CSPExamples (even though they are already inside the Examples library, so the Example part of the names may seem redundant).

Currently, we have

• agda-algebras/UniversalAlgebra (the main lib, with its own UniversalAlgebra.agda-lib file)
• agda-algebras/Examples/UniversalAlgebra (the examples lib, with its own UniversalAlgebraExamples.agda-lib file)
• agda-algebras/Exercises/UniversalAlgebra (exercise lib, with its own UniversalAlgebraExercises.agda-lib file)

Does this seem reasonable?

[JacquesCarette]

I think what happened is that I forgot that UniversalAlgebra was not actually part of all the module names. I meant for the latter module names to include Examples. and Exercises. in their names. That will get rid of all the clashes (which are indeed a problem).

[williamdemeo]

Okay, no problem. I think I understand now, and agree with you. We will have modules Examples and Exercises underneath UniversalAlgebra. I'll implement that organizational structure now.

[williamdemeo]

Thank you!! :bow: