tip-tools

Last updated: 2017-08-06 18:25:51 +0200

Upstream URL: git clone http://chriswarbo.net/git/tip-tools.git

Repo

View repository

View issue tracker

Contents of README.md follows


TIP: Tons of Inductive Problems - tools

This repository contains tools for working with the TIP suite of benchmarks for inductive theorem provers. The tools are currently rough around the edges but include:

<ul> <li><code>tip</code> - transform a TIP file or translate it to various formats</li> <li><code>tip-ghc</code> - translate a Haskell file to TIP format</li> <li><code>tip-spec</code> - invent conjectures about a TIP file</li> </ul>

Building the development version of the tools

With Haskell installed and this repository cloned:

<pre><code>stack setup stack install</code></pre>

The tools will be put in your <code>~/.local/bin</code> directory.

If you are modifying the TIP parser, you will also need to have BNFC installed, and to run ./make_parser.sh whenever you change the parser.

Working with TIP problems

You can find a large collection of problems in TIP format in the benchmarks repository under the directory <code>benchmarks</code>. You can use the <code>tip</code> tool to run transformations on these problems or translate them to another format.

To translate a TIP file to some other format, run:

<ul> <li><code>tip name-of-file.smt2 --why</code> to convert it to WhyML format;</li> <li><code>tip name-of-file.smt2 --smtlib</code> to convert it to a CVC4-compatible version of SMTLIB;</li> <li><code>tip name-of-file.smt2 --isabelle</code> to convert it to Isabelle;</li> <li><code>tip name-of-file.smt2 --haskell</code> to convert it to Haskell (plus scaffolding for running QuickSpec).</li> </ul>

You can also use <code>tip</code> to run various transformations on the input problem. For example, <code>tip name-of-file.smt2 --commute-match --simplify-aggressively</code> will first simplify the structure of <code>match</code> expressions in the problem and then run a general simplification pass. For a list of all passes run <code>tip --help</code>.

Translating Haskell to TIP

To translate a Haskell file to TIP, run <code>tip-ghc name-of-file.hs</code>. Properties to be proved must be written in a special syntax; to see some examples, look at the benchmarks repository under the directory <code>originals</code>.