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.1 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.1 ... 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.1 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.1 ... 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
- HERMIT
- HERMIT.Context
- HERMIT.Core
- HERMIT.Dictionary
- HERMIT.Dictionary.AlphaConversion
- HERMIT.Dictionary.Common
- HERMIT.Dictionary.Composite
- HERMIT.Dictionary.Debug
- HERMIT.Dictionary.FixPoint
- HERMIT.Dictionary.Fold
- HERMIT.Dictionary.Function
- HERMIT.Dictionary.GHC
- HERMIT.Dictionary.Induction
- HERMIT.Dictionary.Inline
- HERMIT.Dictionary.Kure
- HERMIT.Dictionary.Local
- HERMIT.Dictionary.Local.Bind
- HERMIT.Dictionary.Local.Case
- HERMIT.Dictionary.Local.Cast
- HERMIT.Dictionary.Local.Let
- HERMIT.Dictionary.Navigation
- HERMIT.Dictionary.Navigation.Crumbs
- HERMIT.Dictionary.New
- HERMIT.Dictionary.Query
- HERMIT.Dictionary.Reasoning
- HERMIT.Dictionary.Remembered
- HERMIT.Dictionary.Rules
- HERMIT.Dictionary.Undefined
- HERMIT.Dictionary.Unfold
- HERMIT.Dictionary.Unsafe
- WorkerWrapper
- HERMIT.Dictionary.WorkerWrapper.Common
- HERMIT.Dictionary.WorkerWrapper.Fix
- HERMIT.Dictionary.WorkerWrapper.FixResult
- HERMIT.Driver
- HERMIT.External
- HERMIT.GHC
- HERMIT.GHC.Typechecker
- HERMIT.Kernel
- HERMIT.Kure
- HERMIT.Kure.Universes
- HERMIT.Lemma
- Libraries
- HERMIT.Libraries.Int
- HERMIT.Libraries.WW
- HERMIT.Monad
- HERMIT.Name
- HERMIT.Parser
- HERMIT.ParserCore
- HERMIT.ParserType
- HERMIT.Plugin
- HERMIT.Plugin.Builder
- HERMIT.Plugin.Display
- HERMIT.Plugin.Renderer
- HERMIT.Plugin.Types
- PrettyPrinter
- HERMIT.PrettyPrinter.AST
- HERMIT.PrettyPrinter.Clean
- HERMIT.PrettyPrinter.Common
- HERMIT.PrettyPrinter.GHC
- HERMIT.PrettyPrinter.Glyphs
- Shell
- HERMIT.Shell.Command
- HERMIT.Shell.Completion
- HERMIT.Shell.Dictionary
- HERMIT.Shell.Externals
- HERMIT.Shell.Interpreter
- HERMIT.Shell.KernelEffect
- HERMIT.Shell.Proof
- HERMIT.Shell.ScriptToRewrite
- HERMIT.Shell.ShellEffect
- HERMIT.Shell.Types
- HERMIT.Utilities
Downloads
- hermit-1.0.1.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
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.8 && <5), containers (>=0.5.0.0), data-default-class (>=0.0.1), directory (>=1.2.0.0), fail, ghc (==7.10.3), haskeline (>=0.7.0.3), hermit, kure (>=2.16.8 && <3.0), marked-pretty (>=0.1), mtl (>=2.2), process (>=1.1.0.2), semigroups (>=0.18), stm (>=2.4), temporary (>=1.2.0.3), terminal-size (>=0.3.2), transformers (>=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 1 made by ryanglscott at 2016-02-23T01:30:18Z |
Category | Language, Formal Methods, Optimization, Transformation, Refactoring, Reflection |
Source repo | head: git clone https://github.com/ku-fpg/hermit |
Uploaded | by ryanglscott at 2016-02-23T01:26:57Z |
Distributions | |
Reverse Dependencies | 2 direct, 0 indirect [details] |
Executables | hermit |
Downloads | 17033 total (46 in the last 30 days) |
Rating | (no votes yet) [estimated by Bayesian average] |
Your Rating | |
Status | Docs not available [build log] All reported builds failed as of 2016-11-27 [all 2 reports] |