liquid-fixpoint-0.2.3.2: liquid-fixpoint.cabal

name:                liquid-fixpoint
version:             0.2.3.2
Copyright:           2010-15 Ranjit Jhala, University of California, San Diego.
synopsis:            Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
homepage:            https://github.com/ucsd-progsys/liquid-fixpoint
license:             BSD3
license-file:        LICENSE
author:              Ranjit Jhala, Niki Vazou, Eric Seidel
maintainer:          jhala@cs.ucsd.edu
category:            Language
build-type:          Custom 
cabal-version:       >=1.8

description:     This package is a Haskell wrapper to the SMTLIB-based
                 Horn-Clause/Logical Implication constraint solver used
                 for Liquid Types. 
                 .
                 The solver itself is written in Ocaml. 
                 .
                 The package includes: 
                 .
                 1. Types for Expressions, Predicates, Constraints, Solutions
                 .
                 2. Code for serializing the above
                 .
                 3. Code for parsing the results from the fixpoint.native binary
                 .
                 4. The Ocaml fixpoint code and pre-compiled binaries
                 .
                 5. (Deprecated) Z3 binaries if you want to link against the API.
                 .
                 Requirements
                 .
                 In addition to the .cabal dependencies you require 
                 .
                 - A Z3 (<http://z3.codeplex.com>) or CVC4 (<http://cvc4.cs.nyu.edu>) binary.
                   If on Windows, please make sure to place the binary and any associated DLLs
                   in your "cabal/bin" folder, right next to the fixpoint.native.exe binary.
                 .
                 - An ocaml compiler (if installing with -fbuild-external).

Extra-Source-Files: configure
                  , external/fixpoint/Makefile
                  , external/fixpoint/*.ml
                  , external/fixpoint/smtZ3.mem.ml
                  , external/fixpoint/smtZ3.nomem.ml
                  , external/fixpoint/*.mli
                  , external/fixpoint/*.mll
                  , external/fixpoint/*.mly
                  , external/misc/*.ml
                  , external/misc/*.mli
                  , external/ocamlgraph/.depend
                  , external/ocamlgraph/Makefile.in
                  , external/ocamlgraph/META.in
                  , external/ocamlgraph/configure
                  , external/ocamlgraph/configure.in
                  , external/ocamlgraph/lib/*.ml
                  , external/ocamlgraph/lib/*.mli
                  , external/ocamlgraph/src/*.ml
                  , external/ocamlgraph/src/*.mli
                  , external/ocamlgraph/src/*.mll
                  , external/ocamlgraph/src/*.mly
                  , external/z3/include/*.h
                  , external/z3/lib/libz3-a-32b
                  , external/z3/lib/libz3-a-64b
                  , external/z3/lib/libz3-so-32b
                  , external/z3/lib/libz3-so-64b
                  , external/z3/ocaml/build-lib.sh
                  , external/z3/ocaml/z3.ml
                  , external/z3/ocaml/*.c
                  , external/fixpoint/fixpoint.native-i386-linux
                  , external/fixpoint/fixpoint.native-i686-w64-mingw32
                  , external/fixpoint/fixpoint.native-x86_64-darwin
                  , external/fixpoint/fixpoint.native-x86_64-linux

Flag z3mem
  Description: Link to Z3
  Default:     False

Flag build-external
  Description: Build fixpoint.native binary from source (requires ocaml)
  Default:     False

Source-Repository head
  Type:        git
  Location:    https://github.com/ucsd-progsys/liquid-fixpoint/

-- FIXME: This is a terrible hack. We build Fixpoint.hs *twice*, once
-- targeting fixpoint.native so we can then *clobber* it with the
-- OCaml fixpoint.native. This is required for cabal-install to detect
-- fixpoint.native as an executable, and properly symlink it when
-- asked.
Executable fixpoint.native
  Main-is: Fixpoint.hs
  Build-Depends: base >= 4.7 && < 5
               , array
               , syb
               , cmdargs
               , ansi-terminal
               , bifunctors
               , bytestring
               , containers
               , deepseq
               , directory
               -- , filemanip
               , filepath
               , mtl
               , parsec
               , pretty
               , process
               , syb
               , text
               , hashable
               , unordered-containers
               , text-format
               , liquid-fixpoint
               

Executable fixpoint
  Main-is:       Fixpoint.hs
  Build-Depends: base >= 4.7 && < 5
               , array
               , syb
               , cmdargs
               , ansi-terminal
               , bifunctors
               , bytestring
               , containers
               , deepseq
               , directory
               -- , filemanip
               , filepath
               , mtl
               , parsec
               , pretty
               , process
               , syb
               , text
               , hashable
               , unordered-containers
               , text-format
               , liquid-fixpoint

Library
  hs-source-dirs:  src
  Exposed-Modules: Language.Fixpoint.Names,
                   Language.Fixpoint.Files,
                   Language.Fixpoint.Errors,
                   Language.Fixpoint.Config,
                   Language.Fixpoint.Types,
                   Language.Fixpoint.Bitvector,
                   Language.Fixpoint.Visitor,
                   Language.Fixpoint.Sort,
                   Language.Fixpoint.Interface, 
                   Language.Fixpoint.Parse,
                   Language.Fixpoint.PrettyPrint,
                   Language.Fixpoint.SmtLib2,
                   Language.Fixpoint.Misc
  
  Build-Depends: base >= 4.7 && < 5
               , array
               , attoparsec
               , syb
               , cmdargs
               , ansi-terminal
               , bifunctors
               , bytestring
               , containers
               , deepseq
               , directory
               , filemanip
               , filepath
               , ghc-prim
               , intern
               , mtl
               , parsec
               , pretty
               , process
               , syb
               , text
               , transformers
               , hashable
               , unordered-containers
               , text-format

-- test-suite test
--   default-language: Haskell98
--   type:              exitcode-stdio-1.0
--   hs-source-dirs:    tests
--   ghc-options:       -O2 -threaded
--   main-is:           test.hs
--   build-depends:     base,
--                      -- directory,
--                      -- filepath,
--                      -- process,
--                      -- tagged,
--                      liquid-fixpoint,
--                      -- optparse-applicative == 0.11.*,
--                      QuickCheck,
--                      tasty >= 0.10,
--                      tasty-quickcheck,
--                      tasty-rerun >= 1.1,
--                      text