name:          linearscan
version:       0.3.0.1
synopsis:      Linear scan register allocator, formally verified in Coq
homepage:      http://github.com/jwiegley/linearscan
license:       BSD3
license-file:  LICENSE
author:        John Wiegley
maintainer:    johnw@newartisans.com
category:      Development
build-type:    Simple
cabal-version: >=1.10

description:
  The @linearscan@ library is an implementation -- in Coq, extracted to
  Haskell -- of a register allocation algorithm developed by Christian Wimmer.
  It is described in detail in his Masters thesis, which can be found at
  <http://www.christianwimmer.at/Publications/Wimmer04a/Wimmer04a.pdf>.  A
  Java implementation of this same algorithm, by that author, is used in
  Oracle's Graal project.
  .
  This version of the algorithm was written and verified in Coq, containing
  over 130 proved lemmas, at over 5K LOC.  It was funded as a research project
  by BAE Systems (<http://www.baesystems.com>), to be used in an in-house
  compiler written in Haskell.
  .
  In order for the Coq code to be usable from Haskell, it is first extracted
  from Coq as a Haskell library, during which many of Coq's fundamental types
  are mapped directly onto counterparts in the Haskell Prelude.  Thus, it
  should be within the performance range of an equivalent implementation
  written directly in Haskell.
  .
  Note that not every conceivable property of this library has been proven.
  For some of the lower layers this is true, because the algebraic constraints
  on these components could be exhaustively described in the context of their
  use.  However, higher-level components represent a great variety of use
  cases, and not every one of these cases has been proven correct.  This
  represents an ongoing effort, with the hope that proofs will entirely
  replace the necessity for ad hoc unit testing, and that at some point we can
  know that any allocation produced by this library must either fail, or be
  mathematically sound.
  .
  This library's sole entry point is the 'LinearScan.allocate' function, which
  takes a list of information about basic blocks to an equivalent list, with
  annotations indicating allocation choices.

library
  default-language: Haskell2010
  exposed-modules:
    LinearScan
  other-modules:
    LinearScan.Allocate
    LinearScan.Assign
    LinearScan.Blocks
    LinearScan.Build
    LinearScan.Choice
    LinearScan.Cursor
    LinearScan.Datatypes
    LinearScan.Eqtype
    LinearScan.Fintype
    LinearScan.Graph
    LinearScan.IState
    LinearScan.IntMap
    LinearScan.Interval
    LinearScan.Lib
    LinearScan.List0
    LinearScan.LiveSets
    LinearScan.Logic
    LinearScan.Main
    LinearScan.Morph
    LinearScan.NonEmpty0
    LinearScan.Order
    LinearScan.Range
    LinearScan.Resolve
    LinearScan.ScanState
    LinearScan.Seq
    LinearScan.Specif
    LinearScan.Split
    LinearScan.Ssrbool
    LinearScan.Ssreflect
    LinearScan.Ssrfun
    LinearScan.Ssrnat
    LinearScan.State
    LinearScan.UsePos
    LinearScan.Utils
    LinearScan.Vector0
  cpp-options:      -DMAX_REG=4 -DREG_SIZE=8
  ghc-options:      -fno-warn-deprecated-flags
  build-depends:    base >=4.7 && <4.8
                  , containers
                  , transformers

test-suite test
  default-language: Haskell2010
  type:             exitcode-stdio-1.0
  ghc-options:      -fno-warn-deprecated-flags
  hs-source-dirs:   test
  main-is:          Main.hs
  other-modules:    Tempest
  build-depends: 
        base >=3
      , linearscan
      , hspec              >= 1.4.4
      , hspec-expectations >= 0.3
      , containers         >= 0.5.5
      , transformers       >= 0.3.0.0
      , hoopl              >= 3.10.0.1
      , lens               >= 4.2
      , mtl
      , free