The hermit package

[Tags: bsd3, library, program]

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:

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.4.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.4.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.4.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.4.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 ...
$

Properties

Versions0.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
Dependenciesaeson (>=0.6.0.2), ansi-terminal (>=0.5.5), base (==4.*), containers (>=0.5.0.0), data-default (>=0.5.0), directory (>=1.2.0.0), ghc (==7.6.*), haskeline (>=0.7.0.3), kure (>=2.4.10), marked-pretty (>=0.1), mtl (>=2.1.2), process, stm (>=2.4), template-haskell (>=2.8.0.0), text (>=0.11.2.3)
LicenseBSD3
AuthorAndrew Farmer, Andy Gill, Ed Komp, Neil Sculthorpe
MaintainerAndy Gill <andygill@ku.edu>
Stabilitypre-alpha
CategoryLanguage, Formal Methods, Optimization, Transformation, Refactoring, Reflection
Executableshermit
UploadedFri Nov 30 22:50:32 UTC 2012 by AndrewFarmer
Downloads1270 total (89 in last 30 days)
StatusDocs uploaded by user
Build status unknown [no reports yet]

Modules

[Index]

Downloads

Maintainers' corner

For package maintainers and hackage trustees