Work log 2016-08-24

Focus on writing a QuickSpec command, since that’s ‘off-the-shelf’.

TIP includes one, but reusing our Haskell-TE one would be better.

How to wrap QuickSpec?

smtlib   haskell pkg   QuickSpec
-----> X ----------> X --------> equations + times

We need to:

• Convert SMTlib to Haskell
• Take Haskell pkg, produce quickspec sig

We have these parts already, just not joined up!

Decided to give haskell-te a package, i.e. we can do nix-shell -p haskell-te and it provided scripts necessary to do the exploration and benchmarking.

It would be nice to run QuickSpec ‘standalone’ rather than via MLSpec, so made a script which tunrs smtlib into a Haskell package, annotates it and extracts everything quickspecable.

This roughly corresponds to what clustering with k=1 would do, but avoids all of the complications.