hermit-0.3.1.0: hermit.cabal
Name: hermit
Version: 0.3.1.0
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 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.1.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.1.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.1.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.1.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 ...
$
@
Category: Language, Formal Methods, Optimization, Transformation, Refactoring, Reflection
License: BSD3
License-file: LICENSE
Author: Andrew Farmer, Andy Gill, Ed Komp, Neil Sculthorpe
Maintainer: Andy Gill <andygill@ku.edu>
Stability: alpha
build-type: Simple
Cabal-Version: >= 1.14
extra-source-files:
examples/concatVanishes/ConcatVanishes.hss
examples/concatVanishes/Flatten.hs
examples/concatVanishes/Flatten.hss
examples/concatVanishes/HList.hs
examples/concatVanishes/QSort.hs
examples/concatVanishes/QSort.hss
examples/concatVanishes/Rev.hs
examples/concatVanishes/Rev.hss
examples/evaluation/Eval.hs
examples/evaluation/Eval.hss
examples/factorial/Fac.hs
examples/factorial/Fac.hss
examples/fib-stream/Fib.hs
examples/fib-stream/Fib.hss
examples/fib-stream/Nat.hs
examples/fib-stream/Stream.hs
examples/fib-tuple/Fib.hs
examples/fib-tuple/Fib.hss
examples/flatten/HList.hs
examples/flatten/Flatten.hs
examples/flatten/Flatten.hss
examples/hanoi/Hanoi.hs
examples/hanoi/Hanoi.hss
examples/last/Last.hs
examples/last/Last.hss
examples/mean/Mean.hs
examples/mean/Mean.hss
examples/qsort/HList.hs
examples/qsort/QSort.hs
examples/qsort/QSort.hss
examples/reverse/HList.hs
examples/reverse/Reverse.hs
examples/reverse/Reverse.hss
Library
ghc-options: -Wall -fno-warn-orphans
Build-Depends: base >= 4 && < 5,
ansi-terminal >= 0.5.5,
array,
containers >= 0.5.0.0,
data-default >= 0.5.0,
ghc >= 7.6,
haskeline >= 0.7.0.3,
kure >= 2.14.0,
marked-pretty >= 0.1,
mtl >= 2.1.2,
operational >= 0.2.2.1,
process >= 1.1.0.2,
stm >= 2.4,
template-haskell >= 2.8.0.0,
temporary >= 1.1.2.4,
terminfo >= 0.3.2.5,
transformers
default-language: Haskell2010
Exposed-modules:
HERMIT
HERMIT.Context
HERMIT.Core
HERMIT.Dictionary
HERMIT.Driver
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.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.Undefined
HERMIT.Dictionary.Unfold
HERMIT.Dictionary.Unsafe
HERMIT.Dictionary.WorkerWrapper.Common
HERMIT.Dictionary.WorkerWrapper.Fix
HERMIT.Dictionary.WorkerWrapper.FixResult
HERMIT.External
HERMIT.GHC
HERMIT.Interp
HERMIT.Kernel
HERMIT.Kernel.Scoped
HERMIT.Kure
HERMIT.Kure.SumTypes
HERMIT.Monad
HERMIT.Optimize
HERMIT.Parser
HERMIT.ParserCore
HERMIT.Plugin
HERMIT.PrettyPrinter.AST
HERMIT.PrettyPrinter.Clean
HERMIT.PrettyPrinter.Common
HERMIT.PrettyPrinter.GHC
HERMIT.Shell.Command
HERMIT.Shell.Dictionary
HERMIT.Shell.Externals
HERMIT.Shell.ScriptToRewrite
HERMIT.Shell.Renderer
HERMIT.Shell.Types
Other-modules:
HERMIT.Syntax
HERMIT.Utilities
Paths_hermit
Hs-Source-Dirs: src
Executable hermit
Build-Depends: base >= 4 && < 5,
directory >= 1.2.0.0,
hermit,
process
default-language: Haskell2010
Main-Is: Main.hs
Hs-Source-Dirs: driver
Ghc-Options:
source-repository head
type: git
location: git://github.com/ku-fpg/hermit.git