# Speculate

Speculate automatically discovers laws about Haskell functions.
Give Speculate a bunch of Haskell functions and it will discover laws like:

- equations, such as
`id x == x`

;
- inequalities, such as
`0 <= x * x`

;
- conditional equations, such as
`x <= 0 ==> x + abs x == 0`

.

Speculate is similar to, and inspired by, QuickSpec.

## Crash Course

Install pre-requisites:

```
$ cabal install cmdargs
$ cabal install leancheck
```

Clone and enter the repository:

```
$ git clone https://github.com/rudymatela/speculate
$ cd speculate
```

There are some examples in the `eg`

folter. For example `eg/plus-abs.hs`

:

```
$ cat eg/plus-abs.hs
...
...
```

Compile and run with:

```
$ ghc -isrc eg/plus-abs.hs
$ ./eg/plus-abs
...
```

## Installing Speculate

Pre-requisites are cmdargs and leancheck.
You can install them with:

```
$ cabal install cmdargs
$ cabal install leancheck
```

No `cabal`

package has been made yet. For now, clone the repository with:

```
$ git clone https://github.com/rudymatela/speculate
```

and compile programs that use it with:

```
$ ghc -ipath/to/speculate/src program.hs
```

## Using Speculate

Speculate is used as a library: import it, then call the function `speculate`

with relevant arguments. The following program Speculates about the functions
`(+)`

and `abs`

:

```
import Test.Speculate
main :: IO ()
main = speculate args
{ constants =
[ showConstant (0::Int)
, showConstant (1::Int)
, constant "+" ((+) :: Int -> Int -> Int)
, constant "abs" (abs :: Int -> Int)
]
}
```

when run, it prints the following:

```
_ :: Int (holes: Int)
0 :: Int
1 :: Int
(+) :: Int -> Int -> Int
abs :: Int -> Int
abs (abs x) == abs x
x + 0 == x
x + y == y + x
(x + y) + z == x + (y + z)
abs (x + abs x) == x + abs x
abs x + abs x == abs (x + x)
abs (1 + abs x) == 1 + abs x
x <= abs x
0 <= abs x
x <= x + 1
```

Now, if we add `<=`

and `<`

as background constants on `args`

```
, constants =
[ showConstant (0::Int)
, showConstant (1::Int)
, constant "+" ((+) :: Int -> Int -> Int)
, constant "abs" (abs :: Int -> Int)
, background
, constant "<=" ((<=) :: Int -> Int -> Bool)
, constant "<" ((<) :: Int -> Int -> Bool)
]
```

then run again, we get the following as well:

```
y <= x ==> abs (x + abs y) == x + abs y
x <= 0 ==> x + abs x == 0
abs x <= y ==> abs (x + y) == x + y
abs y <= x ==> abs (x + y) == x + y
```

For more examples, see the eg folder.

## Similarities and Differences to QuickSpec

Speculate is inspired by QuickSpec.
Like QuickSpec, Speculate uses testing to speculate equational laws about given
Haskell functions. There are some differences:

| | Speculate | QuickSpec |
| ----------------: | ------------------------- | --------------------------------- |
| testing | enumerative (LeanCheck) | random (QuickCheck) |
| equational laws | yes (after completion) | yes (as discovered) |
| inequational laws | yes | no |
| conditional laws | yes | restricted to a set of predicates |
| polymorphism | no | yes |
| performance | slower | faster |

For most examples, Speculate runs slower than QuickSpec 2 but faster than QuickSpec 1.

## More documentation

For more examples, see the eg and bench folders.