Readme
# MLSpec: Machine Learning for QuickSpec #
This project constructs "theories" for the QuickSpec system to explore.
It reads from stdin or a filename argument, and parses a JSON array of
arrays of function descriptions.
A function description looks like:
{
"package" : "foo"
, "module" : "Bar.Baz"
, "name" : "quux"
, "type" : "Bar.T a -> Baz.U b"
, "arity" : 1
}
Each array will be turned into a QuickSpec signature and explored.
Equations found by all of these explorations are printed to stdout as JSON
objects, one per line.
## Formatting ##
### Equations ###
Each equation is an object with the following fields:
- `relation`: This has no real meaning, it's basically a tag for distinguishing
that this is an equation. The value will be `"~="`, to indicate that it was
found by QuickSpec and is hence only tested rather than formally proven.
- `lhs`: a term representing the left-hand-side of the equation. There's no
conceptual difference between the left and right, they're just names.
- `rhs`: a term representing the right-hand-side of the equation. Again, no
real difference from the left hand side except the name.
### Terms ###
A term is an object, with a `role` field containing one of `"constant"`,
`"variable"` or `"application"`. The other fields depend on the term's role:
- Constants
- `type`: The type of the constant, a string written in Haskell's type
notation. This is taken from the given function descriptions. For example
`"Int -> (Int -> Bool) -> IO Float"`
- `symbol`: The name of the constant, as a string. For example `"reverse"`.
- Variables
- `type`: The type of the variable, a string written in Haskell's type
notation. Variables are automatically added to a signature to be used as
arguments to the given functions. For example `"[Int]"`.
- `"id"`: A numeric ID for the variable. IDs start at `0`. Three variables
are added for each argument type. For example, to represent three integer
variables we might use `{"role": "variable", "type": "Int", "id":0}`,
`{"role": "variable", "type": "Int", "id":1}` and
`{"role": "variable", "type": "Int", "id":2}`.
- Applications
- `lhs`: A term representing a function to apply.
- `rhs`: A term representing the argument to apply the `lhs` function to.
Functions are curried, so calling with multiple arguments should be done
via a left-leaning tree.
## Implementation Notes ##
We use the `nix-eval` package to run QuickSpec with all of the required packages
available. If some packages aren't in the default GHC package database,
`nix-eval` will call the `nix-shell` command, so you'll need a working
installation of Nix in your path.
We include a Cabal test suite to check internal function behaviour. We also
include an executable `mlspec-test-quickspec` for integration tests which use
QuickSpec. We also have a `test.sh` script which invokes these as well as
running various examples through the `MLSpec` executable.
Repository
Clone this repository using: git clone http://chriswarbo.net/git/mlspec.git
Branches
- master: HLint Chris Warburton <chriswarbo@gmail.com> Sat Jun 2 02:24:59 PM UTC 2018
Generated by git2html.