name:                liquid-fixpoint
version:             0.4.0.0
x-revision: 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.10

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/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
                  , tests/neg/*.fq
                  , tests/pos/*.fq

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
  default-language: Haskell98
  Main-is: Fixpoint.hs
  Build-Depends: base >= 4.7 && < 5
               , array
               , syb
               , cmdargs
               , ansi-terminal
               , bifunctors
               , bytestring
               , containers
               , deepseq
               , directory
               , filepath
               , mtl
               , parsec
               , pretty
               , process
               , syb
               , text
               , hashable
               , unordered-containers
               , text-format
               , liquid-fixpoint


Executable fixpoint
  default-language: Haskell98
  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
  default-language: Haskell98
  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.Smt.Types,
                   Language.Fixpoint.Smt.Theories,
                   Language.Fixpoint.Smt.Serialize,
                   Language.Fixpoint.Smt.Interface,
                   Language.Fixpoint.Misc,
                   Language.Fixpoint.Solver.Solution,
                   Language.Fixpoint.Solver.Worklist,
                   Language.Fixpoint.Solver.Monad,
                   Language.Fixpoint.Solver.Deps,
                   Language.Fixpoint.Solver.Uniqify,
                   Language.Fixpoint.Solver.Eliminate,
                   Language.Fixpoint.Solver.Validate,
                   Language.Fixpoint.Partition,
                   Language.Fixpoint.Statistics,
                   Language.Fixpoint.Solver.Solve

  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.*,
                    tasty >= 0.10,
                    -- tasty-quickcheck,
                    tasty-hunit,
                    tasty-rerun >= 1.1,
                    text