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 a pre-alpha `please give feedback' release. Shortcomings/gotchas include:

• Command line completion is ad hoc at the moment.

• Parser needs to be reimplemented with a parsing library.

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

• The fold rewrite can only fold syntactically alpha-equivalent (up to parameters of the function you are folding) expressions.

• RULES have issues with forall types.

• Different core comes out depending on whether you ascribe explicit type signatures.

• A number of rewrites don't enforce preconditions. ex: 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.1.6.0 on Reverse.hs]
% ghc Reverse.hs -fforce-recomp -O2 -dcore-lint -fsimple-list-literals -fplugin=HERMIT -fplugin-opt=HERMIT:main:Main: -fplugin-opt=HERMIT:main:Main:resume
[1 of 2] Compiling HList            ( HList.hs, HList.o )
Loading package ghc-prim ... linking ... done.
...
Loading package hermit-0.1.6.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.1.6.0 on Reverse.hs]
% ghc Reverse.hs -fforce-recomp -O2 -dcore-lint -fsimple-list-literals -fplugin=HERMIT -fplugin-opt=HERMIT:main:Main:
[1 of 2] Compiling HList            ( HList.hs, HList.o )
Loading package ghc-prim ... linking ... done.
...
Loading package hermit-0.1.6.0 ... linking ... done.
[2 of 2] Compiling Main             ( Reverse.hs, Reverse.o )
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 compile, use resume.

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

Modules

[Last Documentation]

Downloads

• hermit-0.1.6.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