name:          linearscan
version:       1.0.0
x-revision: 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. It has also been implemented in C++ by Mozilla.
  .
  This version of the algorithm was written and verified in Coq, containing
  over 231 proved lemmas, at over 10K 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.
  .
  This library's sole entry point is the function 'LinearScan.allocate', which
  takes a list of basic blocks, and a functional characterization of those
  blocks, and produces a new list, with register allocations applied to their
  component operations.

Source-repository head
  type:     git
  location: https://github.com/jwiegley/linearscan

library
  default-language: Haskell2010
  exposed-modules:
    LinearScan
  other-modules:
    LinearScan.Allocate
    LinearScan.Applicative
    LinearScan.Ascii
    LinearScan.Assign
    LinearScan.Blocks
    LinearScan.Build
    LinearScan.Choice
    LinearScan.Class
    LinearScan.Const
    LinearScan.Context
    LinearScan.Contravariant
    LinearScan.Cursor
    LinearScan.Datatypes
    LinearScan.Eqtype
    LinearScan.Fintype
    LinearScan.Functor
    LinearScan.Graph
    LinearScan.Identity
    LinearScan.Interval
    LinearScan.IntMap
    LinearScan.IntSet
    LinearScan.Lens
    LinearScan.Lib
    LinearScan.List0
    LinearScan.List1
    LinearScan.LiveSets
    LinearScan.Logic
    LinearScan.Loops
    LinearScan.Main
    LinearScan.Maybe
    LinearScan.Monad
    LinearScan.Morph
    LinearScan.Nat
    LinearScan.NonEmpty
    LinearScan.Prelude0
    LinearScan.Range
    LinearScan.Resolve
    LinearScan.ScanState
    LinearScan.Seq
    LinearScan.Specif
    LinearScan.Spill
    LinearScan.Split
    LinearScan.Ssr
    LinearScan.Ssrbool
    LinearScan.Ssreflect
    LinearScan.Ssrfun
    LinearScan.Ssrnat
    LinearScan.State
    LinearScan.State0
    LinearScan.String0
    LinearScan.Trace
    LinearScan.Tuple
    LinearScan.UsePos
    LinearScan.Vector0
    LinearScan.Verify
    Hask.Utils
  ghc-options:      -fno-warn-deprecated-flags
  other-extensions: Safe
  hs-source-dirs:   . Hask/haskell
  build-depends:
      base >=4.7 && <5.0
    , containers
    , transformers
    , mtl
    , ghc-prim