Mirror of http://chriswarbo.net/git/mlspec
License
Warbo/mlspec
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
# 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.
Releases
No releases published
Packages 0
No packages published