hermit: Haskell Equational Reasoning Model-to-Implementation Tunnel

HERMIT uses Haskell to express semi-formal models, efficient implementations, and provide a bridging DSL to describe via stepwise refinement the connection between these models and implementations. The key transformation in the bridging DSL is the worker/wrapper transformation.

This is an alpha `please give feedback' release. Shortcomings/gotchas include:

• Command line completion is ad hoc at the moment.

• log command prints linearly, even if command history is a tree.

• RULES have issues with forall types.

• A number of rewrites don't enforce preconditions. eg: cast elimination always works, even if the cast is necessary

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 v0.3.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-0.3.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 v0.3.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:
[1 of 2] Compiling HList            ( HList.hs, HList.o )
Loading package ghc-prim ... linking ... done.
...
Loading package hermit-0.3.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 "consider '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 ...
$

Modules

[Index]

Downloads

• hermit-0.3.0.0.tar.gz [browse] (Cabal source package)
• Package description (revised from the package)

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

• AndrewFarmer, AndyGill, NeilSculthorpe, ryanglscott

For package maintainers and hackage trustees

• edit package information

Candidates

• No Candidates