hermit
Version 0.1.8.0 revision 0 uploaded by AndrewFarmer.
Package meta
- Synopsis
- Haskell Equational Reasoning Model-to-Implementation Tunnel
- Description
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.
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.8.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.1.8.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.8.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.1.8.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 compilation, use resume.
... hermit<0> resume hermit<0> Linking Reverse ... $
- Author
- Andrew Farmer, Andy Gill, Ed Komp, Neil Sculthorpe
- Bug reports
- n/a
- Category
- Language, Formal Methods, Optimization, Transformation, Refactoring, Reflection
- Copyright
- n/a
- Homepage
- n/a
- Maintainer
- Andy Gill <andygill@ku.edu>
- Package URL
- n/a
- Stability
- pre-alpha