Last updated: 2018-06-02 15:24:59 +0100
Upstream URL: git clone http://chriswarbo.net/git/mlspec.git
Contents of README follows
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:
<pre><code>{ "package" : "foo" , "module" : "Bar.Baz" , "name" : "quux" , "type" : "Bar.T a -> Baz.U b" , "arity" : 1 }</code></pre>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.
Each equation is an object with the following fields:
<ul> <li><code>relation</code>: This has no real meaning, it’s basically a tag for distinguishing that this is an equation. The value will be <code>"~="</code>, to indicate that it was found by QuickSpec and is hence only tested rather than formally proven.</li> <li><code>lhs</code>: a term representing the left-hand-side of the equation. There’s no conceptual difference between the left and right, they’re just names.</li> <li><code>rhs</code>: a term representing the right-hand-side of the equation. Again, no real difference from the left hand side except the name.</li> </ul>A term is an object, with a <code>role</code> field containing one of <code>"constant"</code>, <code>"variable"</code> or <code>"application"</code>. The other fields depend on the term’s role:
<ul> <li>Constants <ul> <li><code>type</code>: The type of the constant, a string written in Haskell’s type notation. This is taken from the given function descriptions. For example <code>"Int -> (Int -> Bool) -> IO Float"</code></li> <li><code>symbol</code>: The name of the constant, as a string. For example <code>"reverse"</code>.</li> </ul></li> <li>Variables <ul> <li><code>type</code>: 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 <code>"[Int]"</code>.</li> <li><code>"id"</code>: A numeric ID for the variable. IDs start at <code>0</code>. Three variables are added for each argument type. For example, to represent three integer variables we might use <code>{"role": "variable", "type": "Int", "id":0}</code>, <code>{"role": "variable", "type": "Int", "id":1}</code> and <code>{"role": "variable", "type": "Int", "id":2}</code>.</li> </ul></li> <li>Applications <ul> <li><code>lhs</code>: A term representing a function to apply.</li> <li><code>rhs</code>: A term representing the argument to apply the <code>lhs</code> function to. Functions are curried, so calling with multiple arguments should be done via a left-leaning tree.</li> </ul></li> </ul>We use the <code>nix-eval</code> package to run QuickSpec with all of the required packages available. If some packages aren’t in the default GHC package database, <code>nix-eval</code> will call the <code>nix-shell</code> 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 <code>mlspec-test-quickspec</code> for integration tests which use QuickSpec. We also have a <code>test.sh</code> script which invokes these as well as running various examples through the <code>MLSpec</code> executable.