hermit-0.1.6.0: hermit.cabal
Name: hermit
Version: 0.1.6.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 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 ...
$
@
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: pre-alpha
build-type: Simple
Cabal-Version: >= 1.14
extra-source-files:
examples/WWSplitTactic.hss
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
examples/reverse/ReverseWW.hss
Library
ghc-options: -Wall -fno-warn-orphans
Build-Depends: base >= 4 && < 5,
aeson >= 0.6.0.2,
ansi-terminal >= 0.5.5,
containers >= 0.5.0.0,
data-default >= 0.5.0,
ghc == 7.6.*,
haskeline >= 0.7.0.3,
kure >= 2.6.14,
marked-pretty >= 0.1,
mtl >= 2.1.2,
stm >= 2.4,
template-haskell >= 2.8.0.0,
text >= 0.11.2.3
default-language: Haskell2010
Exposed-modules:
HERMIT
Language.HERMIT.Context
Language.HERMIT.Core
Language.HERMIT.Dictionary
Language.HERMIT.Expr
Language.HERMIT.External
Language.HERMIT.Kernel
Language.HERMIT.Kernel.Scoped
Language.HERMIT.Kure
Language.HERMIT.Interp
Language.HERMIT.Monad
Language.HERMIT.Plugin
Language.HERMIT.Primitive.AlphaConversion
Language.HERMIT.Primitive.Debug
Language.HERMIT.Primitive.FixPoint
Language.HERMIT.Primitive.Fold
Language.HERMIT.Primitive.GHC
Language.HERMIT.Primitive.Inline
Language.HERMIT.Primitive.Kure
Language.HERMIT.Primitive.Local
Language.HERMIT.Primitive.Local.Let
Language.HERMIT.Primitive.Local.Case
Language.HERMIT.Primitive.Navigation
Language.HERMIT.Primitive.New
Language.HERMIT.Primitive.Unfold
Language.HERMIT.PrettyPrinter
Language.HERMIT.PrettyPrinter.AST
Language.HERMIT.PrettyPrinter.Clean
Language.HERMIT.PrettyPrinter.GHC
Language.HERMIT.PrettyPrinter.JSON
Language.HERMIT.Shell.Command
Other-modules:
Language.HERMIT.GHC
Language.HERMIT.Primitive.Common
Hs-Source-Dirs: src
Executable hermit
Build-Depends: base >= 4 && < 5,
directory >= 1.2.0.0,
process
default-language: Haskell2010
Main-Is: Main.hs
Hs-Source-Dirs: driver
Ghc-Options: