This project was produced for the dissertation component of my Computer Science masters at University of Warwick. The accompanying thesis can be found here.
The aim of the project is to create an expressive framework for stating and solving simple grid puzzles. It aims to provide:
- A Haskell DSL for stating puzzles
- A solver for producing solutions
- A file format to state puzzles in plain text
- A front end to enter, inspect and solve puzzles
The project is packaged using IOHK's haskell.nix infrastructure, and uses both the sbv library and microsoft's z3 SMT solver under the hood.
The goal of the project is to provide a way to declaratively describe the rules of a puzzle using something close to predicate logic.
- Restructure the language as a Deep Embedding rather than a Shallow Embedding. This will allow for much easier parsing when reading from a textual format, and greater control over the language. For further reference on shallow vs deep embedding see here
- Implementing expressing of connectivity between two cells. In my initial report, I identified that this would greatly increase expressiveness (and allow a lot of 'standard' puzzles to be described).
Currently, building the project runs the test suite. This contains unit tests for checking that the language behaves as desired, and other tests to check that specific puzzles can be solved.
Ensure that nix is installed, then run:
nix run
Ensure that ghc 9.2.7 is installed, with a recent version of cabal (this can all be done via the ghcup utility), then run:
cabal run
I would like to give thanks to: