Cabal revisions of linearscan-1.0.0
Hackage metadata revisions edit the .cabal file after upload; each diff below is one revision.
revision 1
-name: linearscan-version: 1.0.0-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.- .- 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. In the absence of some complete coverage, this version- of the library provides an optional, runtime verifier to confirm- expectations of correctness, since it is easier to prove the validity of- generated data, than of how it was generated.- .- 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+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