hermit: Haskell Equational Reasoning Model-to-Implementation Tunnel

[ bsd3, formal-methods, language, library, optimization, program, refactoring, reflection, transformation ] [ Propose Tags ]

HERMIT is a Haskell-specific toolkit designed to mechanize equational reasoning and program transformation during compilation in GHC.

Examples can be found in the examples sub-directory.

$ cd examples/reverse

Example of running a script.

$ hermit Reverse.hs Reverse.hss resume
[starting HERMIT v1.0.0.0 on Reverse.hs]
% ghc Reverse.hs -fforce-recomp -O2 -dcore-lint -fexpose-all-unfoldings -fsimple-list-literals -fplugin=HERMIT -fplugin-opt=HERMIT:Main:Reverse.hss -fplugin-opt=HERMIT:Main:resume
[1 of 2] Compiling HList            ( HList.hs, HList.o )
Loading package ghc-prim ... linking ... done.
...
Loading package hermit-1.0.0.0 ... linking ... done.
[2 of 2] Compiling Main             ( Reverse.hs, Reverse.o )
Linking Reverse ...
$ ./Reverse
....

Example of interactive use.

$ hermit Reverse.hs
[starting HERMIT v1.0.0.0 on Reverse.hs]
% ghc Reverse.hs -fforce-recomp -O2 -dcore-lint -fexpose-all-unfoldings -fsimple-list-literals -fplugin=HERMIT -fplugin-opt=HERMIT:*:
[1 of 2] Compiling HList            ( HList.hs, HList.o )
Loading package ghc-prim ... linking ... done.
...
Loading package hermit-1.0.0.0 ... linking ... done.
[2 of 2] Compiling Main             ( Reverse.hs, Reverse.o )
===================== Welcome to HERMIT =====================
HERMIT is a toolkit for the interactive transformation of GHC
core language programs. Documentation on HERMIT can be found
on the HERMIT web page at:
http://www.ittc.ku.edu/csdl/fpg/software/hermit.html

You have just loaded the interactive shell. To exit, type
"abort" or "resume" to abort or resume GHC compilation.

Type "help" for instructions on how to list or search the
available HERMIT commands.

To get started, you could try the following:
  - type "binding-of 'foo", where "foo" is a function
    defined in the module;
  - type "set-pp-type Show" to switch on typing information;
  - use natural numbers such as "0" and "1" to descend into
    the definition, and "up" to ascend;
  - type "info" for more information about the current node;
  - type "log" to display an activity log.
=============================================================
module main:Main where
  rev ∷ ∀ a . [a] -> [a]
  unwrap ∷ ∀ a . ([a] -> [a]) -> [a] -> H a
  wrap ∷ ∀ a . ([a] -> H a) -> [a] -> [a]
  main ∷ IO ()
  main ∷ IO ()
hermit<0>
...

To resume compilation, use resume.

...
hermit<0> resume
hermit<0> Linking Reverse ...
$

[Skip to Readme]

Modules

[Index]

Downloads

Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.0, 0.1.1.0, 0.1.1.1, 0.1.2.0, 0.1.4.0, 0.1.6.0, 0.1.8.0, 0.2.0.0, 0.3.0.0, 0.3.1.0, 0.3.2.0, 0.4.0.0, 0.5.0.0, 0.6.0.0, 0.7.0.0, 0.7.1.0, 1.0.0.0, 1.0.1
Dependencies ansi-terminal (>=0.5.5), array, base (>=4 && <5), base-compat (>=0.8.1), containers (>=0.5.0.0), data-default-class (>=0.0.1), directory (>=1.2.0.0), ghc (>=7.8 && <7.9 || ==7.10.1), haskeline (>=0.7.0.3), hermit, kure (>=2.16.8 && <3.0), marked-pretty (>=0.1), mtl (>=2.1.2), process (>=1.1.0.2), stm (>=2.4), temporary (>=1.2.0.3), terminfo (>=0.3.2.5), transformers (>=0.2), transformers-compat (>=0.4), Win32 [details]
License BSD-3-Clause
Author Andrew Farmer, Andy Gill, Ed Komp, Neil Sculthorpe
Maintainer Andrew Farmer <afarmer@ittc.ku.edu>
Revised Revision 2 made by ryanglscott at 2016-02-21T23:31:35Z
Category Language, Formal Methods, Optimization, Transformation, Refactoring, Reflection
Source repo head: git clone git://github.com/ku-fpg/hermit.git
Uploaded by AndrewFarmer at 2015-05-20T21:04:24Z
Distributions
Reverse Dependencies 2 direct, 0 indirect [details]
Executables hermit
Downloads 16849 total (42 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2015-05-23 [all 1 reports]

Readme for hermit-1.0.0.0

[back to package description]

HERMIT Hackage version Build Status

The Haskell Equational Reasoning Model-to-Implementation Tunnel.